diff --git a/proof/crefine/ARM/IpcCancel_C.thy b/proof/crefine/ARM/IpcCancel_C.thy index 5a7a7e1216..0f79e156a5 100644 --- a/proof/crefine/ARM/IpcCancel_C.thy +++ b/proof/crefine/ARM/IpcCancel_C.thy @@ -30,7 +30,7 @@ proof - qed lemmas cready_queues_index_to_C_in_range = - cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def] + cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val] lemma cready_queues_index_to_C_inj: "\ cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; diff --git a/proof/crefine/ARM/Wellformed_C.thy b/proof/crefine/ARM/Wellformed_C.thy index 938283c309..4e964d3559 100644 --- a/proof/crefine/ARM/Wellformed_C.thy +++ b/proof/crefine/ARM/Wellformed_C.thy @@ -426,31 +426,31 @@ lemma maxDom_sgt_0_maxDomain: lemma num_domains_calculation: "num_domains = numDomains" - unfolding num_domains_def by eval + unfolding num_domains_val by eval private lemma num_domains_card_explicit: "num_domains = CARD(num_domains)" - by (simp add: num_domains_def) + by (simp add: num_domains_val) lemmas num_domains_index_updates = - index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] - index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a specific number expressed as a word, so we must introduce these. However, being explicit means lack of discipline can lead to a violation. *) -lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]: +lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]: "x < Kernel_Config.numDomains \ x < num_domains" by (simp add: num_domains_calculation) -lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]: +lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]: "unat x < Kernel_Config.numDomains \ (ucast (x::domain) :: machine_word) < of_nat num_domains" apply (rule word_less_nat_alt[THEN iffD2]) apply transfer apply simp - apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def) + apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val) done lemmas maxDomain_le_unat_ucast_explicit = @@ -475,7 +475,7 @@ value_type num_tcb_queues = "numDomains * numPriorities" lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities" - unfolding num_tcb_queues_def by eval + unfolding num_tcb_queues_val by eval abbreviation(input) diff --git a/proof/crefine/ARM_HYP/IpcCancel_C.thy b/proof/crefine/ARM_HYP/IpcCancel_C.thy index ba7082881e..b307286b81 100644 --- a/proof/crefine/ARM_HYP/IpcCancel_C.thy +++ b/proof/crefine/ARM_HYP/IpcCancel_C.thy @@ -30,7 +30,7 @@ proof - qed lemmas cready_queues_index_to_C_in_range = - cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def] + cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val] lemma cready_queues_index_to_C_inj: "\ cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy index 4a6b608e94..f81475ee60 100644 --- a/proof/crefine/ARM_HYP/Wellformed_C.thy +++ b/proof/crefine/ARM_HYP/Wellformed_C.thy @@ -456,31 +456,31 @@ lemma maxDom_sgt_0_maxDomain: lemma num_domains_calculation: "num_domains = numDomains" - unfolding num_domains_def by eval + unfolding num_domains_val by eval private lemma num_domains_card_explicit: "num_domains = CARD(num_domains)" - by (simp add: num_domains_def) + by (simp add: num_domains_val) lemmas num_domains_index_updates = - index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] - index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a specific number expressed as a word, so we must introduce these. However, being explicit means lack of discipline can lead to a violation. *) -lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]: +lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]: "x < Kernel_Config.numDomains \ x < num_domains" by (simp add: num_domains_calculation) -lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]: +lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]: "unat x < Kernel_Config.numDomains \ (ucast (x::domain) :: machine_word) < of_nat num_domains" apply (rule word_less_nat_alt[THEN iffD2]) apply transfer apply simp - apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def) + apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val) done lemmas maxDomain_le_unat_ucast_explicit = @@ -505,7 +505,7 @@ value_type num_tcb_queues = "numDomains * numPriorities" lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities" - unfolding num_tcb_queues_def by eval + unfolding num_tcb_queues_val by eval (* Input abbreviations for API object types *) diff --git a/proof/crefine/RISCV64/IpcCancel_C.thy b/proof/crefine/RISCV64/IpcCancel_C.thy index f06b9d102c..fc510629a6 100644 --- a/proof/crefine/RISCV64/IpcCancel_C.thy +++ b/proof/crefine/RISCV64/IpcCancel_C.thy @@ -29,7 +29,7 @@ proof - qed lemmas cready_queues_index_to_C_in_range = - cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def] + cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val] lemma cready_queues_index_to_C_inj: "\ cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; diff --git a/proof/crefine/RISCV64/Wellformed_C.thy b/proof/crefine/RISCV64/Wellformed_C.thy index f3c815622b..f28a56f303 100644 --- a/proof/crefine/RISCV64/Wellformed_C.thy +++ b/proof/crefine/RISCV64/Wellformed_C.thy @@ -429,31 +429,31 @@ lemma maxDom_sgt_0_maxDomain: lemma num_domains_calculation: "num_domains = numDomains" - unfolding num_domains_def by eval + unfolding num_domains_val by eval private lemma num_domains_card_explicit: "num_domains = CARD(num_domains)" - by (simp add: num_domains_def) + by (simp add: num_domains_val) lemmas num_domains_index_updates = - index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] - index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a specific number expressed as a word, so we must introduce these. However, being explicit means lack of discipline can lead to a violation. *) -lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]: +lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]: "x < Kernel_Config.numDomains \ x < num_domains" by (simp add: num_domains_calculation) -lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]: +lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]: "unat x < Kernel_Config.numDomains \ (ucast (x::domain) :: machine_word) < of_nat num_domains" apply (rule word_less_nat_alt[THEN iffD2]) apply transfer apply simp - apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def) + apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val) done lemmas maxDomain_le_unat_ucast_explicit = @@ -478,7 +478,7 @@ value_type num_tcb_queues = "numDomains * numPriorities" lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities" - unfolding num_tcb_queues_def by eval + unfolding num_tcb_queues_val by eval (* Input abbreviations for API object types *) diff --git a/proof/crefine/X64/IpcCancel_C.thy b/proof/crefine/X64/IpcCancel_C.thy index cca60bcadd..b8a475cf6d 100644 --- a/proof/crefine/X64/IpcCancel_C.thy +++ b/proof/crefine/X64/IpcCancel_C.thy @@ -28,7 +28,7 @@ proof - qed lemmas cready_queues_index_to_C_in_range = - cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def] + cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val] lemma cready_queues_index_to_C_inj: "\ cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; diff --git a/proof/crefine/X64/Wellformed_C.thy b/proof/crefine/X64/Wellformed_C.thy index f3b4521ceb..ed017823e2 100644 --- a/proof/crefine/X64/Wellformed_C.thy +++ b/proof/crefine/X64/Wellformed_C.thy @@ -472,31 +472,31 @@ lemma maxDom_sgt_0_maxDomain: lemma num_domains_calculation: "num_domains = numDomains" - unfolding num_domains_def by eval + unfolding num_domains_val by eval private lemma num_domains_card_explicit: "num_domains = CARD(num_domains)" - by (simp add: num_domains_def) + by (simp add: num_domains_val) lemmas num_domains_index_updates = - index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] - index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def, + index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val, simplified num_domains_calculation] (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a specific number expressed as a word, so we must introduce these. However, being explicit means lack of discipline can lead to a violation. *) -lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]: +lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]: "x < Kernel_Config.numDomains \ x < num_domains" by (simp add: num_domains_calculation) -lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]: +lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]: "unat x < Kernel_Config.numDomains \ (ucast (x::domain) :: machine_word) < of_nat num_domains" apply (rule word_less_nat_alt[THEN iffD2]) apply transfer apply simp - apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def) + apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val) done lemmas maxDomain_le_unat_ucast_explicit = @@ -521,7 +521,7 @@ value_type num_tcb_queues = "numDomains * numPriorities" lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities" - unfolding num_tcb_queues_def by eval + unfolding num_tcb_queues_val by eval (* Input abbreviations for API object types *) diff --git a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy index 9180267283..e42dd1b32e 100644 --- a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy @@ -2403,7 +2403,7 @@ lemma pptrTop_ucast_ppn: ucast (ucast (p >> pageBits)::ppn) = p >> pageBits" apply (drule below_pptrTop_ipa_size) apply word_eqI - using ppn_len_def'[unfolded ppn_len_def] + using ppn_len_def'[unfolded ppn_len_val] by (fastforce dest: bit_imp_le_length) lemma kernel_window_range_addrFromPPtr: @@ -2470,7 +2470,7 @@ lemma pt_slot_offset_pt_range: lemma ucast_ucast_ppn: "ucast (ucast ptr::ppn) = ptr && mask ppn_len" for ptr::obj_ref - by (simp add: ucast_ucast_mask ppn_len_def) + by (simp add: ucast_ucast_mask ppn_len_val) lemma pte_base_addr_PageTablePTE[simp]: "pte_base_addr (PageTablePTE ppn) = paddr_from_ppn ppn" diff --git a/proof/refine/AARCH64/ADT_H.thy b/proof/refine/AARCH64/ADT_H.thy index 4f93f4044c..d509b4b577 100644 --- a/proof/refine/AARCH64/ADT_H.thy +++ b/proof/refine/AARCH64/ADT_H.thy @@ -745,7 +745,7 @@ proof - apply (rule ucast_leq_mask) apply (clarsimp simp: bit_simps) apply (clarsimp simp: pte_relation_def ucast_ucast_mask ge_mask_eq vs_index_bits_def) - apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_def) + apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_val) (* NormalPT_T is an exact duplicate of the VSRootPT_T case, but I don't see any good way to factor out the commonality *) @@ -815,7 +815,7 @@ proof - apply (rule ucast_leq_mask) apply (clarsimp simp: bit_simps) apply (clarsimp simp: pte_relation_def ucast_ucast_mask ge_mask_eq vs_index_bits_def) - apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_def) + apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_val) apply (in_case "DataPage ?p ?sz") apply (clarsimp split: if_splits)