x64 crefine/lib: move word lemmas out of Move_C into Word_Lemmas_64_Internal
Signed-off-by: Victor Phan <Victor.Phan@data61.csiro.au>
This commit is contained in:
Victor Phan
parent
c53cb66869
commit
a7ed68e75d
49
lib/Lib.thy
49
lib/Lib.thy
|
|
@ -1754,6 +1754,51 @@ lemma is_inv_inj2:
|
|||
"is_inv f g \<Longrightarrow> inj_on g (dom g)"
|
||||
using is_inv_com is_inv_inj by blast
|
||||
|
||||
text \<open>Map inversion (implicitly assuming injectivity).\<close>
|
||||
definition
|
||||
"the_inv_map m = (\<lambda>s. if s\<in>ran m then Some (THE x. m x = Some s) else None)"
|
||||
|
||||
text \<open>Map inversion can be expressed by function inversion.\<close>
|
||||
lemma the_inv_map_def2:
|
||||
"the_inv_map m = (Some \<circ> the_inv_into (dom m) (the \<circ> m)) |` (ran m)"
|
||||
apply (rule ext)
|
||||
apply (clarsimp simp: the_inv_map_def the_inv_into_def dom_def)
|
||||
apply (rule_tac f=The in arg_cong)
|
||||
apply (rule ext)
|
||||
apply auto
|
||||
done
|
||||
|
||||
text \<open>The domain of a function composition with Some is the universal set.\<close>
|
||||
lemma dom_comp_Some[simp]: "dom (comp Some f) = UNIV" by (simp add: dom_def)
|
||||
|
||||
text \<open>Assuming injectivity, map inversion produces an inversive map.\<close>
|
||||
lemma is_inv_the_inv_map:
|
||||
"inj_on m (dom m) \<Longrightarrow> is_inv m (the_inv_map m)"
|
||||
apply (simp add: is_inv_def)
|
||||
apply (intro conjI allI impI)
|
||||
apply (simp add: the_inv_map_def2)
|
||||
apply (auto simp add: the_inv_map_def inj_on_def dom_def intro: ranI)
|
||||
done
|
||||
|
||||
lemma the_the_inv_mapI:
|
||||
"inj_on m (dom m) \<Longrightarrow> m x = Some y \<Longrightarrow> the (the_inv_map m y) = x"
|
||||
by (auto simp: the_inv_map_def ran_def inj_on_def dom_def)
|
||||
|
||||
lemma eq_restrict_map_None[simp]:
|
||||
"restrict_map m A x = None \<longleftrightarrow> x ~: (A \<inter> dom m)"
|
||||
by (auto simp: restrict_map_def split: if_split_asm)
|
||||
|
||||
lemma eq_the_inv_map_None[simp]: "the_inv_map m x = None \<longleftrightarrow> x\<notin>ran m"
|
||||
by (simp add: the_inv_map_def2)
|
||||
|
||||
lemma is_inv_unique:
|
||||
"is_inv f g \<Longrightarrow> is_inv f h \<Longrightarrow> g=h"
|
||||
apply (rule ext)
|
||||
apply (clarsimp simp: is_inv_def dom_def Collect_eq ran_def)
|
||||
apply (drule_tac x=x in spec)+
|
||||
apply (case_tac "g x", clarsimp+)
|
||||
done
|
||||
|
||||
lemma range_convergence1:
|
||||
"\<lbrakk> \<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z > y. P (z :: 'a :: linorder) \<rbrakk> \<Longrightarrow> \<forall>z > x. P z"
|
||||
using not_le by blast
|
||||
|
|
@ -2179,10 +2224,6 @@ lemma zip_append_singleton:
|
|||
by (induct xs; case_tac ys; simp)
|
||||
(clarsimp simp: zip_append1 zip_take_length zip_singleton)
|
||||
|
||||
lemma ran_map_of_zip:
|
||||
"\<lbrakk>length xs = length ys; distinct xs\<rbrakk> \<Longrightarrow> ran (map_of (zip xs ys)) = set ys"
|
||||
by (induct rule: list_induct2) auto
|
||||
|
||||
lemma ranE:
|
||||
"\<lbrakk> v \<in> ran f; \<And>x. f x = Some v \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
|
||||
by (auto simp: ran_def)
|
||||
|
|
|
|||
|
|
@ -10,4 +10,47 @@ begin
|
|||
|
||||
lemmas unat_add_simple = iffD1[OF unat_add_lem[where 'a = 64, folded word_bits_def]]
|
||||
|
||||
lemma unat_length_4_helper:
|
||||
"\<lbrakk>unat (l::machine_word) = length args; \<not> l < 4\<rbrakk> \<Longrightarrow> \<exists>x xa xb xc xs. args = x#xa#xb#xc#xs"
|
||||
apply (case_tac args; clarsimp simp: unat_eq_0)
|
||||
by (rename_tac list, case_tac list, clarsimp, unat_arith)+
|
||||
|
||||
lemma ucast_drop_big_mask:
|
||||
"UCAST(64 \<rightarrow> 16) (x && 0xFFFF) = UCAST(64 \<rightarrow> 16) x"
|
||||
by word_bitwise
|
||||
|
||||
lemma first_port_last_port_compare:
|
||||
"UCAST(16 \<rightarrow> 32 signed) (UCAST(64 \<rightarrow> 16) (xa && 0xFFFF))
|
||||
<s UCAST(16 \<rightarrow> 32 signed) (UCAST(64 \<rightarrow> 16) (x && 0xFFFF))
|
||||
= (UCAST(64 \<rightarrow> 16) xa < UCAST(64 \<rightarrow> 16) x)"
|
||||
apply (clarsimp simp: word_sless_alt ucast_drop_big_mask)
|
||||
apply (subst sint_ucast_eq_uint, clarsimp simp: is_down)+
|
||||
by (simp add: word_less_alt)
|
||||
|
||||
lemma machine_word_and_3F_less_40:
|
||||
"(w :: machine_word) && 0x3F < 0x40"
|
||||
by (rule word_and_less', simp)
|
||||
|
||||
(* FIXME: move to GenericLib *)
|
||||
lemmas unat64_eq_of_nat = unat_eq_of_nat[where 'a=64, folded word_bits_def]
|
||||
|
||||
lemma unat_mask_3_less_8:
|
||||
"unat (p && mask 3 :: word64) < 8"
|
||||
apply (rule unat_less_helper)
|
||||
apply (rule order_le_less_trans, rule word_and_le1)
|
||||
apply (simp add: mask_def)
|
||||
done
|
||||
|
||||
lemma scast_specific_plus64:
|
||||
"scast (of_nat (word_ctz x) + 0x20 :: 64 signed word) = of_nat (word_ctz x) + (0x20 :: machine_word)"
|
||||
by (simp add: scast_down_add is_down_def target_size_def source_size_def word_size)
|
||||
|
||||
lemma scast_specific_plus64_signed:
|
||||
"scast (of_nat (word_ctz x) + 0x20 :: machine_word) = of_nat (word_ctz x) + (0x20 :: 64 signed word)"
|
||||
by (simp add: scast_down_add is_down_def target_size_def source_size_def word_size)
|
||||
|
||||
lemmas mask_64_id[simp] = mask_len_id[where 'a=64, folded word_bits_def]
|
||||
mask_len_id[where 'a=64, simplified]
|
||||
|
||||
|
||||
end
|
||||
|
|
@ -11,51 +11,6 @@ theory Move_C
|
|||
imports Include_C
|
||||
begin
|
||||
|
||||
text \<open>Map inversion (implicitly assuming injectivity).\<close>
|
||||
definition
|
||||
"the_inv_map m = (\<lambda>s. if s\<in>ran m then Some (THE x. m x = Some s) else None)"
|
||||
|
||||
text \<open>Map inversion can be expressed by function inversion.\<close>
|
||||
lemma the_inv_map_def2:
|
||||
"the_inv_map m = (Some \<circ> the_inv_into (dom m) (the \<circ> m)) |` (ran m)"
|
||||
apply (rule ext)
|
||||
apply (clarsimp simp: the_inv_map_def the_inv_into_def dom_def)
|
||||
apply (rule_tac f=The in arg_cong)
|
||||
apply (rule ext)
|
||||
apply auto
|
||||
done
|
||||
|
||||
text \<open>The domain of a function composition with Some is the universal set.\<close>
|
||||
lemma dom_comp_Some[simp]: "dom (comp Some f) = UNIV" by (simp add: dom_def)
|
||||
|
||||
text \<open>Assuming injectivity, map inversion produces an inversive map.\<close>
|
||||
lemma is_inv_the_inv_map:
|
||||
"inj_on m (dom m) \<Longrightarrow> is_inv m (the_inv_map m)"
|
||||
apply (simp add: is_inv_def)
|
||||
apply (intro conjI allI impI)
|
||||
apply (simp add: the_inv_map_def2)
|
||||
apply (auto simp add: the_inv_map_def inj_on_def dom_def)
|
||||
done
|
||||
|
||||
lemma the_the_inv_mapI:
|
||||
"inj_on m (dom m) \<Longrightarrow> m x = Some y \<Longrightarrow> the (the_inv_map m y) = x"
|
||||
by (auto simp: the_inv_map_def ran_def inj_on_def dom_def)
|
||||
|
||||
lemma eq_restrict_map_None[simp]:
|
||||
"restrict_map m A x = None \<longleftrightarrow> x ~: (A \<inter> dom m)"
|
||||
by (auto simp: restrict_map_def split: if_split_asm)
|
||||
|
||||
lemma eq_the_inv_map_None[simp]: "the_inv_map m x = None \<longleftrightarrow> x\<notin>ran m"
|
||||
by (simp add: the_inv_map_def2)
|
||||
|
||||
lemma is_inv_unique:
|
||||
"is_inv f g \<Longrightarrow> is_inv f h \<Longrightarrow> g=h"
|
||||
apply (rule ext)
|
||||
apply (clarsimp simp: is_inv_def dom_def Collect_eq ran_def)
|
||||
apply (drule_tac x=x in spec)+
|
||||
apply (case_tac "g x", clarsimp+)
|
||||
done
|
||||
|
||||
lemma dumb_bool_for_all: "(\<forall>x. x) = False"
|
||||
by auto
|
||||
|
||||
|
|
|
|||
|
|
@ -47,23 +47,6 @@ where
|
|||
"port_mask start end =
|
||||
mask (unat (end && mask wordRadix)) && ~~ mask (unat (start && mask wordRadix))"
|
||||
|
||||
lemma unat_length_4_helper:
|
||||
"\<lbrakk>unat (l::machine_word) = length args; \<not> l < 4\<rbrakk> \<Longrightarrow> \<exists>x xa xb xc xs. args = x#xa#xb#xc#xs"
|
||||
apply (case_tac args; clarsimp simp: unat_eq_0)
|
||||
by (rename_tac list, case_tac list, clarsimp, unat_arith)+
|
||||
|
||||
lemma ucast_drop_big_mask:
|
||||
"UCAST(64 \<rightarrow> 16) (x && 0xFFFF) = UCAST(64 \<rightarrow> 16) x"
|
||||
by word_bitwise
|
||||
|
||||
lemma first_port_last_port_compare:
|
||||
"UCAST(16 \<rightarrow> 32 signed) (UCAST(64 \<rightarrow> 16) (xa && 0xFFFF))
|
||||
<s UCAST(16 \<rightarrow> 32 signed) (UCAST(64 \<rightarrow> 16) (x && 0xFFFF))
|
||||
= (UCAST(64 \<rightarrow> 16) xa < UCAST(64 \<rightarrow> 16) x)"
|
||||
apply (clarsimp simp: word_sless_alt ucast_drop_big_mask)
|
||||
apply (subst sint_ucast_eq_uint, clarsimp simp: is_down)+
|
||||
by (simp add: word_less_alt)
|
||||
|
||||
declare word_neq_0_conv [simp del]
|
||||
|
||||
lemma unat_ucast_prio_L1_cmask_simp:
|
||||
|
|
@ -71,10 +54,6 @@ lemma unat_ucast_prio_L1_cmask_simp:
|
|||
using unat_ucast_prio_mask_simp[where m=6]
|
||||
by (simp add: mask_def)
|
||||
|
||||
lemma machine_word_and_3F_less_40:
|
||||
"(w :: machine_word) && 0x3F < 0x40"
|
||||
by (rule word_and_less', simp)
|
||||
|
||||
lemma ucast_shiftl_6_absorb:
|
||||
fixes f l :: "16 word"
|
||||
assumes "f \<le> l"
|
||||
|
|
@ -148,16 +127,6 @@ where
|
|||
\<and> x = word_rcat (map (underlying_memory (ksMachineState s))
|
||||
[p + 7, p + 6, p + 5, p + 4, p + 3, p + 2, p + 1, p])"
|
||||
|
||||
(* FIXME: move to GenericLib *)
|
||||
lemmas unat64_eq_of_nat = unat_eq_of_nat[where 'a=64, folded word_bits_def]
|
||||
|
||||
lemma unat_mask_3_less_8:
|
||||
"unat (p && mask 3 :: word64) < 8"
|
||||
apply (rule unat_less_helper)
|
||||
apply (rule order_le_less_trans, rule word_and_le1)
|
||||
apply (simp add: mask_def)
|
||||
done
|
||||
|
||||
lemma getMessageInfo_less_4:
|
||||
"\<lbrace>\<top>\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgExtraCaps rv < 4\<rbrace>"
|
||||
including no_pre
|
||||
|
|
@ -181,14 +150,6 @@ lemma getMessageInfo_msgLength':
|
|||
Types_H.msgExtraCapBits_def split: if_split )
|
||||
done
|
||||
|
||||
lemma scast_specific_plus64:
|
||||
"scast (of_nat (word_ctz x) + 0x20 :: 64 signed word) = of_nat (word_ctz x) + (0x20 :: machine_word)"
|
||||
by (simp add: scast_down_add is_down_def target_size_def source_size_def word_size)
|
||||
|
||||
lemma scast_specific_plus64_signed:
|
||||
"scast (of_nat (word_ctz x) + 0x20 :: machine_word) = of_nat (word_ctz x) + (0x20 :: 64 signed word)"
|
||||
by (simp add: scast_down_add is_down_def target_size_def source_size_def word_size)
|
||||
|
||||
lemma ucast_le_ucast_8_32:
|
||||
"(ucast x \<le> (ucast y :: word32)) = (x \<le> (y :: word8))"
|
||||
by (simp add: word_le_nat_alt is_up_8_32 unat_ucast_upcast)
|
||||
|
|
@ -203,9 +164,6 @@ lemma asid_shiftr_low_bits_less:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemmas mask_64_id[simp] = mask_len_id[where 'a=64, folded word_bits_def]
|
||||
mask_len_id[where 'a=64, simplified]
|
||||
|
||||
lemma addToBitmap_sets_L1Bitmap_same_dom:
|
||||
"\<lbrace>\<lambda>s. p \<le> maxPriority \<and> d' = d \<rbrace> addToBitmap d' p
|
||||
\<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrace>"
|
||||
|
|
|
|||
Loading…
Reference in New Issue