isabelle-2021: AutoCorres update
includes Word_Lib tweaks Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein
Gerwin Klein
parent
7f94f3d8cb
commit
ee8dbcb09c
|
|
@ -361,6 +361,15 @@ lemma shiftr_numeral [simp]:
|
|||
\<open>(numeral k >> numeral n :: 'a::len word) = drop_bit (numeral n) (numeral k)\<close>
|
||||
by (fact shiftr_word_eq)
|
||||
|
||||
lemma shiftr_numeral_Suc [simp]:
|
||||
\<open>(numeral k >> Suc 0 :: 'a::len word) = drop_bit (Suc 0) (numeral k)\<close>
|
||||
by (fact shiftr_word_eq)
|
||||
|
||||
lemma drop_bit_numeral_bit0_1 [simp]:
|
||||
\<open>drop_bit (Suc 0) (numeral k) =
|
||||
(word_of_int (drop_bit (Suc 0) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
|
||||
by (metis Word_eq_word_of_int drop_bit_word.abs_eq of_int_numeral)
|
||||
|
||||
lemma nth_mask [simp]:
|
||||
\<open>(mask n :: 'a::len word) !! i \<longleftrightarrow> i < n \<and> i < size (mask n :: 'a word)\<close>
|
||||
by (auto simp add: test_bit_word_eq word_size Word.bit_mask_iff)
|
||||
|
|
|
|||
|
|
@ -48,12 +48,23 @@ imports
|
|||
Word_Lemmas_Prefix
|
||||
begin
|
||||
|
||||
declare word_induct2[induct type]
|
||||
declare word_nat_cases[cases type]
|
||||
|
||||
declare signed_take_bit_Suc [simp]
|
||||
|
||||
(* these generate take_bit terms, which we often don't want for concrete lengths *)
|
||||
lemmas of_int_and_nat = unsigned_of_nat unsigned_of_int signed_of_int signed_of_nat
|
||||
|
||||
bundle no_take_bit
|
||||
begin
|
||||
declare of_int_and_nat[simp del]
|
||||
end
|
||||
|
||||
lemmas bshiftr1_def = bshiftr1_eq
|
||||
lemmas is_down_def = is_down_eq
|
||||
lemmas is_up_def = is_up_eq
|
||||
lemmas mask_def = mask_eq_decr_exp
|
||||
lemmas mask_def = mask_eq
|
||||
lemmas scast_def = scast_eq
|
||||
lemmas shiftl1_def = shiftl1_eq
|
||||
lemmas shiftr1_def = shiftr1_eq
|
||||
|
|
|
|||
|
|
@ -33,6 +33,7 @@ begin
|
|||
declare word_neq_0_conv [simp del]
|
||||
declare neq0_conv [simp del]
|
||||
declare fun_upd_apply[simp del]
|
||||
declare of_int_and_nat[simp del]
|
||||
|
||||
(* Remove wp combinators which are problematic for AutoCorres
|
||||
and restore some prior configuration. *)
|
||||
|
|
|
|||
|
|
@ -30,6 +30,8 @@ val AUTOCORRES_SIMPSET =
|
|||
(* oversimplifies Spec sets prior to L2 stage
|
||||
(we will control this explicitly in L2Peephole) *)
|
||||
@ @{thms CollectPairFalse})
|
||||
(* avoid take_bit terms in word abstraction and user simps *)
|
||||
@ @{thms of_int_and_nat}
|
||||
addsimps (
|
||||
(* Needed for L2corres_spec *)
|
||||
@{thms globals_surj}
|
||||
|
|
|
|||
|
|
@ -79,9 +79,9 @@ lemma ccorresE_Seq:
|
|||
apply (rotate_tac 1, erule allE, erule impE, force)
|
||||
apply (monad_eq simp: split_def Bex_def Ball_def split: sum.splits)
|
||||
apply (case_tac s', simp_all)[1]
|
||||
apply fast
|
||||
subgoal by fastforce
|
||||
apply (erule exec_elim_cases)
|
||||
apply fastforce
|
||||
subgoal by fastforce
|
||||
apply (erule exec_elim_cases)
|
||||
apply clarsimp
|
||||
apply auto[1]
|
||||
|
|
|
|||
|
|
@ -701,26 +701,20 @@ lemma ccorresE_corresXF_merge:
|
|||
\<And>r s. rx' s = rx r (st1 s);
|
||||
\<And>s. G s \<longrightarrow> (s \<in> G1 \<and> G2 (st1 s)) \<rbrakk> \<Longrightarrow>
|
||||
ac_corres st ct \<Gamma> rx' G A B"
|
||||
apply (unfold ac_corres_def)
|
||||
unfolding ac_corres_def
|
||||
apply (clarsimp simp: ccorresE_def corresXF_def)
|
||||
apply (erule allE, erule impE, fastforce)
|
||||
apply (erule allE, erule impE, fastforce)
|
||||
apply clarsimp
|
||||
apply (clarsimp simp: ccorresE_def)
|
||||
apply (clarsimp simp: corresXF_def)
|
||||
apply (erule allE, erule impE, force)
|
||||
apply (erule allE, erule impE, force)
|
||||
apply clarsimp
|
||||
apply (erule allE, erule impE, force)
|
||||
apply (case_tac t)
|
||||
apply clarsimp
|
||||
apply (erule (1) my_BallE)
|
||||
apply (clarsimp split: sum.splits)
|
||||
apply clarsimp
|
||||
apply (erule (1) my_BallE)
|
||||
apply (clarsimp split: sum.splits)
|
||||
apply (drule no_throw_Inr, assumption)
|
||||
apply simp
|
||||
apply (clarsimp split: sum.splits)
|
||||
apply clarsimp
|
||||
apply simp
|
||||
apply (erule allE, erule impE, fastforce)
|
||||
apply (case_tac t; clarsimp)
|
||||
apply (erule (1) my_BallE)
|
||||
apply (clarsimp split: sum.splits)
|
||||
apply (erule (1) my_BallE)
|
||||
apply (clarsimp split: sum.splits)
|
||||
apply (drule no_throw_Inr, assumption)
|
||||
apply simp
|
||||
apply (clarsimp split: sum.splits)
|
||||
done
|
||||
|
||||
(* We can also merge corresXF statements. *)
|
||||
|
|
|
|||
|
|
@ -676,20 +676,20 @@ lemma align_of_array: "align_of TYPE(('a :: array_outer_max_size)['b' :: array_m
|
|||
lemma c_guard_array:
|
||||
"\<lbrakk> 0 \<le> k; nat k < CARD('b); c_guard (p :: (('a::array_outer_max_size)['b::array_max_count]) ptr) \<rbrakk>
|
||||
\<Longrightarrow> c_guard (ptr_coerce p +\<^sub>p k :: 'a ptr)"
|
||||
apply (clarsimp simp: ptr_add_def c_guard_def c_null_guard_def)
|
||||
apply (clarsimp simp: CTypesDefs.ptr_add_def c_guard_def c_null_guard_def)
|
||||
apply (rule conjI[rotated])
|
||||
apply (erule contrapos_nn)
|
||||
apply (clarsimp simp: intvl_def)
|
||||
apply (rename_tac i, rule_tac x = "nat k * size_of TYPE('a) + i" in exI)
|
||||
apply clarsimp
|
||||
apply (rule conjI)
|
||||
apply (simp add: field_simps of_nat_nat)
|
||||
apply (simp add: field_simps)
|
||||
apply (rule_tac y = "Suc (nat k) * size_of TYPE('a)" in less_le_trans)
|
||||
apply simp
|
||||
apply (metis less_eq_Suc_le mult_le_mono2 mult.commute)
|
||||
apply (subgoal_tac "ptr_aligned (ptr_coerce p :: 'a ptr)")
|
||||
apply (frule_tac p = "ptr_coerce p" and i = "k" in ptr_aligned_plus)
|
||||
apply (clarsimp simp: ptr_add_def)
|
||||
apply (clarsimp simp: CTypesDefs.ptr_add_def)
|
||||
apply (clarsimp simp: ptr_aligned_def align_of_array)
|
||||
done
|
||||
|
||||
|
|
@ -1135,42 +1135,30 @@ lemma abs_spec_modify_global[heap_abs]:
|
|||
|
||||
(* Signed words are stored on the heap as unsigned words. *)
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
lemma uint_scast:
|
||||
"uint (scast x :: 'a word) = uint (x :: 'a::len signed word)"
|
||||
apply (subst down_cast_same [symmetric])
|
||||
apply (clarsimp simp: cast_simps)
|
||||
apply (subst uint_up_ucast)
|
||||
apply (clarsimp simp: cast_simps)
|
||||
apply simp
|
||||
done
|
||||
"uint (scast x :: 'a word) = uint (x :: 'a::len signed word)"
|
||||
by (metis len_signed scast_nop2 uint_word_of_int_eq word_uint.Rep_inverse)
|
||||
|
||||
lemma to_bytes_signed_word:
|
||||
"to_bytes (x :: 'a::len8 signed word) p = to_bytes (scast x :: 'a word) p"
|
||||
"to_bytes (x :: 'a::len8 signed word) p = to_bytes (scast x :: 'a word) p"
|
||||
by (clarsimp simp: uint_scast to_bytes_def typ_info_word word_rsplit_def)
|
||||
|
||||
lemma from_bytes_signed_word:
|
||||
"length p = len_of TYPE('a) div 8 \<Longrightarrow>
|
||||
"length p = len_of TYPE('a) div 8 \<Longrightarrow>
|
||||
(from_bytes p :: 'a::len8 signed word) = ucast (from_bytes p :: 'a word)"
|
||||
by (clarsimp simp: from_bytes_def word_rcat_def
|
||||
scast_def cast_simps typ_info_word)
|
||||
by (clarsimp simp: from_bytes_def word_rcat_def typ_info_word)
|
||||
(metis len_signed word_ubin.Abs_norm)
|
||||
|
||||
lemma hrs_mem_update_signed_word:
|
||||
"hrs_mem_update (heap_update (ptr_coerce p :: 'a::len8 word ptr) (scast val :: 'a::len8 word))
|
||||
= hrs_mem_update (heap_update p (val :: 'a::len8 signed word))"
|
||||
apply (rule ext)
|
||||
apply (clarsimp simp: hrs_mem_update_def split_def)
|
||||
apply (clarsimp simp: heap_update_def to_bytes_signed_word
|
||||
size_of_def typ_info_word)
|
||||
done
|
||||
by (clarsimp simp: hrs_mem_update_def split_def heap_update_def to_bytes_signed_word
|
||||
size_of_def typ_info_word)
|
||||
|
||||
lemma h_val_signed_word:
|
||||
"(h_val a p :: 'a::len8 signed word) = ucast (h_val a (ptr_coerce p :: 'a word ptr))"
|
||||
apply (clarsimp simp: h_val_def)
|
||||
apply (subst from_bytes_signed_word)
|
||||
apply (clarsimp simp: size_of_def typ_info_word)
|
||||
apply (clarsimp simp: size_of_def typ_info_word)
|
||||
done
|
||||
|
||||
by (clarsimp simp: h_val_def size_of_def typ_info_word from_bytes_signed_word)
|
||||
|
||||
lemma align_of_signed_word:
|
||||
"align_of TYPE('a::len8 signed word) = align_of TYPE('a word)"
|
||||
|
|
@ -1184,20 +1172,16 @@ lemma c_guard_ptr_coerce:
|
|||
"\<lbrakk> align_of TYPE('a) = align_of TYPE('b);
|
||||
size_of TYPE('a) = size_of TYPE('b) \<rbrakk> \<Longrightarrow>
|
||||
c_guard (ptr_coerce p :: ('b::c_type) ptr) = c_guard (p :: ('a::c_type) ptr)"
|
||||
apply (clarsimp simp: c_guard_def ptr_aligned_def c_null_guard_def)
|
||||
done
|
||||
by (clarsimp simp: c_guard_def ptr_aligned_def c_null_guard_def)
|
||||
|
||||
lemma word_rsplit_signed:
|
||||
"(word_rsplit (ucast v' :: ('a::len) signed word) :: 8 word list) = word_rsplit (v' :: 'a word)"
|
||||
apply (clarsimp simp: word_rsplit_def)
|
||||
apply (clarsimp simp: cast_simps)
|
||||
done
|
||||
"(word_rsplit (ucast v' :: ('a::len) signed word) :: 8 word list) = word_rsplit (v' :: 'a word)"
|
||||
by (metis len_signed scast_ucast_id uint_scast word_rsplit_def)
|
||||
|
||||
lemma heap_update_signed_word:
|
||||
"heap_update (ptr_coerce p :: 'a word ptr) (scast v) = heap_update (p :: ('a::len8) signed word ptr) v"
|
||||
"heap_update (ptr_coerce p' :: 'a signed word ptr) (ucast v') = heap_update (p' :: ('a::len8) word ptr) v'"
|
||||
apply (auto simp: heap_update_def to_bytes_def typ_info_word word_rsplit_def cast_simps uint_scast)
|
||||
done
|
||||
"heap_update (ptr_coerce p :: 'a word ptr) (scast v) = heap_update (p :: ('a::len8) signed word ptr) v"
|
||||
"heap_update (ptr_coerce p' :: 'a signed word ptr) (ucast v') = heap_update (p' :: ('a::len8) word ptr) v'"
|
||||
by (auto simp: heap_update_def to_bytes_def typ_info_word word_rsplit_def cast_simps uint_scast)
|
||||
|
||||
lemma valid_typ_heap_c_guard:
|
||||
"\<lbrakk> valid_typ_heap st getter setter vgetter vsetter t_hrs t_hrs_update;
|
||||
|
|
@ -1205,15 +1189,11 @@ lemma valid_typ_heap_c_guard:
|
|||
by (clarsimp simp: valid_typ_heap_def)
|
||||
|
||||
abbreviation (input)
|
||||
scast_f :: "(('a::len) signed word ptr \<Rightarrow> 'a signed word)
|
||||
\<Rightarrow> ('a word ptr \<Rightarrow> 'a word)"
|
||||
where
|
||||
scast_f :: "(('a::len) signed word ptr \<Rightarrow> 'a signed word) \<Rightarrow> ('a word ptr \<Rightarrow> 'a word)" where
|
||||
"scast_f f \<equiv> (\<lambda>p. scast (f (ptr_coerce p)))"
|
||||
|
||||
abbreviation (input)
|
||||
ucast_f :: "(('a::len) word ptr \<Rightarrow> 'a word)
|
||||
\<Rightarrow> ('a signed word ptr \<Rightarrow> 'a signed word)"
|
||||
where
|
||||
ucast_f :: "(('a::len) word ptr \<Rightarrow> 'a word) \<Rightarrow> ('a signed word ptr \<Rightarrow> 'a signed word)" where
|
||||
"ucast_f f \<equiv> (\<lambda>p. ucast (f (ptr_coerce p)))"
|
||||
|
||||
abbreviation (input)
|
||||
|
|
@ -1369,7 +1349,7 @@ lemma signed_word_heap_opt [L2opt]:
|
|||
lemma signed_word_heap_ptr_coerce_opt [L2opt]:
|
||||
"(ptr_coerce (((\<lambda>x. ptr_coerce (a (ptr_coerce x))) (p := v :: 'a ptr)) (b :: 'a ptr ptr)))
|
||||
= ((a(ptr_coerce p := (ptr_coerce v :: 'b ptr))) ((ptr_coerce b) :: 'b ptr ptr))"
|
||||
by (auto simp: fun_upd_def scast_id ptr_coerce_eq)
|
||||
by (auto simp: fun_upd_def ptr_coerce_eq)
|
||||
|
||||
declare ptr_coerce_idem [L2opt]
|
||||
declare scast_ucast_id [L2opt]
|
||||
|
|
@ -1424,7 +1404,7 @@ lemma fold_heap_update_list_nmem_same:
|
|||
(to_bytes (val i h :: 'a) (pad i h)) h) [0..<n] h) (ptr_val p + of_nat k)"
|
||||
apply (induct n arbitrary: k)
|
||||
apply simp
|
||||
apply (clarsimp simp: ptr_add_def simp del: mult_Suc)
|
||||
apply (clarsimp simp: CTypesDefs.ptr_add_def simp del: mult_Suc)
|
||||
apply (subst heap_update_nmem_same)
|
||||
apply (subst len)
|
||||
apply simp
|
||||
|
|
@ -1456,9 +1436,8 @@ lemma heap_list_of_disjoint_fold_heap_update_list:
|
|||
apply (rule_tac t = "ptr_val (p +\<^sub>p int n) + of_nat i"
|
||||
and s = "ptr_val p + of_nat (n * size_of TYPE('a) + i)"
|
||||
in subst)
|
||||
apply (clarsimp simp: ptr_add_def)
|
||||
apply (rule fold_heap_update_list_nmem_same[symmetric])
|
||||
apply simp_all
|
||||
apply (clarsimp simp: CTypesDefs.ptr_add_def)
|
||||
apply (rule fold_heap_update_list_nmem_same[symmetric]; simp)
|
||||
done
|
||||
|
||||
(* remove false dependency *)
|
||||
|
|
@ -1560,7 +1539,7 @@ lemma array_update_split:
|
|||
apply (subst fold_heap_update_list[OF array_count_size])
|
||||
apply (rule fold_cong[OF refl refl])
|
||||
|
||||
apply (clarsimp simp: ptr_add_def)
|
||||
apply (clarsimp simp: CTypesDefs.ptr_add_def)
|
||||
apply (rule_tac f = "heap_update_list (ptr_val p + of_nat x * of_nat (size_of TYPE('a)))"
|
||||
in arg_cong)
|
||||
|
||||
|
|
@ -1681,7 +1660,7 @@ theorem heap_abs_array_update [heap_abs]:
|
|||
(* [0..<n] doesn't change *)
|
||||
apply (subst fold_update_id[where s = "st s"])
|
||||
apply assumption
|
||||
apply (clarsimp simp: ptr_add_def)
|
||||
apply (clarsimp simp: CTypesDefs.ptr_add_def)
|
||||
apply (subst of_nat_mult[symmetric])+
|
||||
apply (rule array_count_index)
|
||||
apply (erule less_trans, assumption)+
|
||||
|
|
@ -1690,7 +1669,7 @@ theorem heap_abs_array_update [heap_abs]:
|
|||
(* [Suc n..<CARD('b)] doesn't change *)
|
||||
apply (subst fold_update_id)
|
||||
apply assumption
|
||||
apply (clarsimp simp: ptr_add_def)
|
||||
apply (clarsimp simp: CTypesDefs.ptr_add_def)
|
||||
apply (subst of_nat_mult[symmetric])+
|
||||
apply (erule array_count_index)
|
||||
apply assumption
|
||||
|
|
@ -1698,7 +1677,7 @@ theorem heap_abs_array_update [heap_abs]:
|
|||
(* index n is disjoint *)
|
||||
apply (subst read_write_valid_def1[where r = getter and w = setter])
|
||||
apply assumption
|
||||
apply (clarsimp simp: ptr_add_def)
|
||||
apply (clarsimp simp: CTypesDefs.ptr_add_def)
|
||||
apply (subgoal_tac "of_nat (i * size_of TYPE('a)) \<noteq> of_nat (n s * size_of TYPE('a))")
|
||||
apply force
|
||||
apply (subst array_count_index[symmetric])
|
||||
|
|
|
|||
|
|
@ -14,34 +14,27 @@ begin
|
|||
named_theorems L1opt
|
||||
|
||||
lemma L1_seq_assoc [L1opt]: "(L1_seq (L1_seq X Y) Z) = (L1_seq X (L1_seq Y Z))"
|
||||
apply (clarsimp simp: L1_seq_def bindE_assoc)
|
||||
done
|
||||
by (clarsimp simp: L1_seq_def bindE_assoc)
|
||||
|
||||
lemma L1_seq_skip [L1opt]:
|
||||
"L1_seq A L1_skip = A"
|
||||
"L1_seq L1_skip A = A"
|
||||
apply (clarsimp simp: L1_seq_def L1_skip_def)+
|
||||
done
|
||||
by (clarsimp simp: L1_seq_def L1_skip_def)+
|
||||
|
||||
lemma L1_condition_true [L1opt]: "L1_condition (\<lambda>_. True) A B = A"
|
||||
apply (clarsimp simp: L1_condition_def condition_def)
|
||||
done
|
||||
by (clarsimp simp: L1_condition_def condition_def)
|
||||
|
||||
lemma L1_condition_false [L1opt]: "L1_condition (\<lambda>_. False) A B = B"
|
||||
apply (clarsimp simp: L1_condition_def condition_def)
|
||||
done
|
||||
by (clarsimp simp: L1_condition_def condition_def)
|
||||
|
||||
lemma L1_condition_same [L1opt]: "L1_condition C A A = A"
|
||||
apply (clarsimp simp: L1_defs condition_def)
|
||||
done
|
||||
by (clarsimp simp: L1_condition_def condition_def)
|
||||
|
||||
lemma L1_fail_seq [L1opt]: "L1_seq L1_fail X = L1_fail"
|
||||
apply (clarsimp simp: L1_seq_def L1_fail_def)
|
||||
done
|
||||
by (clarsimp simp: L1_seq_def L1_fail_def)
|
||||
|
||||
lemma L1_throw_seq [L1opt]: "L1_seq L1_throw X = L1_throw"
|
||||
apply (clarsimp simp: L1_seq_def L1_throw_def)
|
||||
done
|
||||
by (clarsimp simp: L1_seq_def L1_throw_def)
|
||||
|
||||
lemma L1_fail_propagates [L1opt]:
|
||||
"L1_seq L1_skip L1_fail = L1_fail"
|
||||
|
|
@ -50,70 +43,51 @@ lemma L1_fail_propagates [L1opt]:
|
|||
"L1_seq (L1_guard G) L1_fail = L1_fail"
|
||||
"L1_seq (L1_init I) L1_fail = L1_fail"
|
||||
"L1_seq L1_fail L1_fail = L1_fail"
|
||||
apply (unfold L1_defs)
|
||||
apply (auto intro!: bindE_fail_propagates empty_fail_bindE
|
||||
no_throw_bindE [where B="\<top>"] hoare_TrueI simp: empty_fail_error_bits)
|
||||
done
|
||||
unfolding L1_defs
|
||||
by (auto intro!: bindE_fail_propagates empty_fail_bindE no_throw_bindE [where B="\<top>"] hoare_TrueI
|
||||
simp: empty_fail_error_bits)
|
||||
|
||||
lemma L1_condition_distrib:
|
||||
"L1_seq (L1_condition C L R) X = L1_condition C (L1_seq L X) (L1_seq R X)"
|
||||
apply (unfold L1_defs)
|
||||
apply (rule ext)
|
||||
apply (clarsimp split: condition_splits)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: condition_def cong: bindE_apply_cong)
|
||||
apply (clarsimp simp: condition_def cong: bindE_apply_cong)
|
||||
done
|
||||
unfolding L1_defs
|
||||
by (fastforce simp: condition_def cong: bindE_apply_cong split: condition_splits)
|
||||
|
||||
lemmas L1_fail_propagate_condition [L1opt] = L1_condition_distrib [where X=L1_fail]
|
||||
|
||||
lemma L1_fail_propagate_catch [L1opt]:
|
||||
"(L1_seq (L1_catch L R) L1_fail) = (L1_catch (L1_seq L L1_fail) (L1_seq R L1_fail))"
|
||||
apply (unfold L1_defs)
|
||||
apply (clarsimp simp: bindE_def)
|
||||
apply (clarsimp simp: handleE'_def handleE_def)
|
||||
apply (clarsimp simp: bind_assoc)
|
||||
unfolding L1_defs
|
||||
apply (clarsimp simp: bindE_def handleE'_def handleE_def bind_assoc)
|
||||
apply (rule arg_cong [where f="NonDetMonad.bind L"])
|
||||
apply (rule ext)+
|
||||
apply (clarsimp split: sum.splits)
|
||||
apply (clarsimp simp: throwError_def)
|
||||
apply (fastforce split: sum.splits simp: throwError_def)
|
||||
done
|
||||
|
||||
lemma L1_guard_false [L1opt]:
|
||||
"L1_guard (\<lambda>_. False) = L1_fail"
|
||||
by (monad_eq simp: L1_defs)
|
||||
by (monad_eq simp: L1_guard_def L1_fail_def)
|
||||
|
||||
lemma L1_guard_true [L1opt]:
|
||||
"L1_guard (\<lambda>_. True) = L1_skip"
|
||||
by (monad_eq simp: L1_defs)
|
||||
by (monad_eq simp: L1_guard_def L1_skip_def)
|
||||
|
||||
lemma L1_condition_fail_lhs [L1opt]:
|
||||
"L1_condition C L1_fail A = L1_seq (L1_guard (\<lambda>s. \<not> C s)) A"
|
||||
apply (rule ext)
|
||||
apply (monad_eq simp: L1_defs Bex_def)
|
||||
apply blast
|
||||
done
|
||||
by (monad_eq simp: L1_condition_def L1_guard_def L1_fail_def L1_seq_def) blast
|
||||
|
||||
lemma L1_condition_fail_rhs [L1opt]:
|
||||
"L1_condition C A L1_fail = L1_seq (L1_guard C) A"
|
||||
apply (rule ext)
|
||||
apply (monad_eq simp: L1_defs Bex_def)
|
||||
done
|
||||
by (monad_eq simp: L1_condition_def L1_guard_def L1_fail_def L1_seq_def)
|
||||
|
||||
lemma L1_catch_fail [L1opt]: "L1_catch L1_fail A = L1_fail"
|
||||
apply (clarsimp simp: L1_catch_def L1_fail_def)
|
||||
done
|
||||
by (clarsimp simp: L1_catch_def L1_fail_def)
|
||||
|
||||
lemma L1_while_fail [L1opt]: "L1_while C L1_fail = L1_guard (\<lambda>s. \<not> C s)"
|
||||
apply (rule ext)
|
||||
apply (clarsimp simp: L1_defs)
|
||||
apply (subst whileLoopE_unroll)
|
||||
apply (clarsimp split: condition_splits)
|
||||
apply (monad_eq simp: L1_defs Bex_def)
|
||||
done
|
||||
unfolding L1_while_def
|
||||
by (clarsimp split: condition_splits simp: whileLoopE_unroll)
|
||||
(monad_eq simp: L1_fail_def L1_guard_def)
|
||||
|
||||
lemma L1_while_infinite [L1opt]: "L1_while C L1_skip = L1_guard (\<lambda>s. \<not> C s)"
|
||||
apply (clarsimp simp: L1_defs whileLoopE_def)
|
||||
apply (clarsimp simp: L1_while_def L1_guard_def L1_skip_def whileLoopE_def)
|
||||
apply (rule ext)
|
||||
apply (case_tac "C x")
|
||||
apply (rule whileLoop_rule_strong)
|
||||
|
|
@ -151,12 +125,13 @@ declare L1_set_to_pred_def [L1opt]
|
|||
*)
|
||||
|
||||
lemma in_set_to_pred [L1opt]: "(\<lambda>s. s \<in> {x. P x}) = P"
|
||||
apply simp
|
||||
done
|
||||
by simp
|
||||
|
||||
lemma in_set_if_then [L1opt]: "(s \<in> (if P then A else B)) = (if P then (s \<in> A) else (s \<in> B))"
|
||||
apply simp
|
||||
done
|
||||
by simp
|
||||
|
||||
lemmas if_simps =
|
||||
if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
|
||||
|
||||
declare empty_iff [L1opt]
|
||||
declare UNIV_I [L1opt]
|
||||
|
|
|
|||
|
|
@ -255,8 +255,8 @@ lemma ucast_scast_same [polish, L2opt, simp]:
|
|||
done
|
||||
|
||||
lemma [polish, L2opt, simp]:
|
||||
"word_of_int (int x) = of_nat x"
|
||||
by (clarsimp simp: word_of_nat)
|
||||
"word_of_int (int x) = of_nat x"
|
||||
by (fact of_int_of_nat_eq)
|
||||
|
||||
(* Optimising "if" constructs. *)
|
||||
|
||||
|
|
|
|||
|
|
@ -427,6 +427,7 @@ proof -
|
|||
apply simp
|
||||
done
|
||||
from assms show ?thesis
|
||||
supply unsigned_of_nat[simp del]
|
||||
apply (clarsimp simp: super_field_update_t_def)
|
||||
apply (rule ext)
|
||||
apply (clarsimp simp: field_lvalue_def split: option.splits)
|
||||
|
|
@ -492,8 +493,9 @@ lemma field_of_t_field_lookup:
|
|||
assumes b: "export_uinfo s = typ_uinfo_t TYPE('b::mem_type)"
|
||||
assumes n: "n = field_offset TYPE('a) f"
|
||||
shows "field_of_t (Ptr &(ptr\<rightarrow>f) :: ('b ptr)) (ptr :: 'a ptr)"
|
||||
supply unsigned_of_nat[simp del]
|
||||
apply (clarsimp simp del: field_lookup_offset_eq
|
||||
simp: field_of_t_def field_of_def)
|
||||
simp: field_of_t_def field_of_def)
|
||||
apply (subst td_set_field_lookup)
|
||||
apply (rule wf_desc_typ_tag)
|
||||
apply (rule exI [where x=f])
|
||||
|
|
@ -502,7 +504,7 @@ lemma field_of_t_field_lookup:
|
|||
apply (subst field_lookup_export_uinfo_Some)
|
||||
apply assumption
|
||||
apply (clarsimp simp del: field_lookup_offset_eq
|
||||
simp: field_lvalue_def unat_of_nat_field_offset)
|
||||
simp: field_lvalue_def unat_of_nat_field_offset)
|
||||
done
|
||||
|
||||
lemma simple_lift_field_update':
|
||||
|
|
@ -531,6 +533,7 @@ proof (rule ext)
|
|||
done
|
||||
|
||||
have equal_case: "?LHS ptr = ?RHS ptr"
|
||||
supply unsigned_of_nat[simp del]
|
||||
apply (insert cl)
|
||||
apply (clarsimp simp: simple_lift_def split: if_split_asm)
|
||||
apply (clarsimp simp: hrs_mem_update)
|
||||
|
|
@ -732,6 +735,7 @@ lemma zero_not_in_intvl_no_overflow:
|
|||
|
||||
lemma intvl_split:
|
||||
"\<lbrakk> n \<ge> a \<rbrakk> \<Longrightarrow> { p :: ('a :: len) word ..+ n } = { p ..+ a } \<union> { p + of_nat a ..+ (n - a)}"
|
||||
supply unsigned_of_nat[simp del]
|
||||
apply (rule set_eqI, rule iffI)
|
||||
apply (clarsimp simp: intvl_def not_less)
|
||||
apply (rule_tac x=k in exI)
|
||||
|
|
|
|||
|
|
@ -171,18 +171,18 @@ lemma unat_abstract_binops:
|
|||
by (auto simp: unat_plus_if' unat_div unat_mod UWORD_MAX_def le_to_less_plus_one
|
||||
WordAbstract.unat_mult_simple word_bits_def unat_sub word_le_nat_alt)
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
lemma unat_of_int:
|
||||
"\<lbrakk>i \<ge> 0; i < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (of_int i :: 'a::len word) = nat i"
|
||||
unfolding unat_def
|
||||
apply (subst eq_nat_nat_iff, clarsimp+)
|
||||
apply (simp add: word_of_int uint_word_of_int)
|
||||
done
|
||||
by (metis nat_less_numeral_power_cancel_iff of_nat_nat unat_of_nat_len)
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME generalises Word_Lemmas_32.unat_of_int_32 *)
|
||||
lemma unat_of_int_signed:
|
||||
"\<lbrakk>i \<ge> 0; i < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (of_int i :: 'a::len signed word) = nat i"
|
||||
by (simp add: unat_of_int)
|
||||
using unat_of_int by auto
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
lemma nat_sint:
|
||||
"0 <=s (x :: 'a::len signed word) \<Longrightarrow> nat (sint x) = unat x"
|
||||
apply (subst unat_of_int_signed[where 'a='a, symmetric])
|
||||
|
|
@ -198,7 +198,7 @@ lemma int_unat_nonneg:
|
|||
|
||||
lemma uint_xor:
|
||||
\<open>uint (x xor y) = uint x XOR uint y\<close>
|
||||
by transfer simp
|
||||
by (fact uint_xor)
|
||||
|
||||
lemma unat_bitwise_abstract_binops:
|
||||
"abstract_binop (\<lambda>a b. True) (unat :: 'a::len word \<Rightarrow> nat) (AND) (AND)"
|
||||
|
|
@ -243,29 +243,20 @@ lemma sint_bitwise_abstract_binops:
|
|||
"abstract_binop (\<lambda>a b. True) (sint :: 'a::len signed word \<Rightarrow> int) (AND) (AND)"
|
||||
"abstract_binop (\<lambda>a b. True) (sint :: 'a::len signed word \<Rightarrow> int) (OR) (OR)"
|
||||
"abstract_binop (\<lambda>a b. True) (sint :: 'a::len signed word \<Rightarrow> int) (XOR) (XOR)"
|
||||
apply (fastforce intro: int_eq_test_bitI
|
||||
simp: nth_sint bin_nth_ops test_bit_def'[symmetric]
|
||||
test_bit_wi[where 'a="'a signed", simplified word_of_int[symmetric]])+
|
||||
done
|
||||
by (fastforce intro: int_eq_test_bitI
|
||||
simp: nth_sint bin_nth_ops test_bit_def'[symmetric] test_bit_wi[where 'a="'a signed"])+
|
||||
|
||||
lemma abstract_val_signed_bitNOT:
|
||||
"abstract_val P x sint (x' :: 'a::len signed word) \<Longrightarrow>
|
||||
abstract_val P (NOT x) sint (NOT x')"
|
||||
apply (fastforce intro: int_eq_test_bitI
|
||||
simp: nth_sint bin_nth_ops word_nth_neq test_bit_def'[symmetric]
|
||||
test_bit_wi[where 'a="'a signed", simplified word_of_int[symmetric]])
|
||||
done
|
||||
by (fastforce intro: int_eq_test_bitI
|
||||
simp: nth_sint bin_nth_ops word_nth_neq test_bit_def'[symmetric] test_bit_wi[where 'a="'a signed"])
|
||||
|
||||
lemma abstract_val_signed_unary_minus:
|
||||
"\<lbrakk> abstract_val P r sint r' \<rbrakk> \<Longrightarrow>
|
||||
abstract_val (P \<and> (- r) \<le> WORD_MAX TYPE('a)) (- r) sint ( - (r' :: ('a :: len) signed word))"
|
||||
apply clarsimp
|
||||
using sint_range_size [where w=r']
|
||||
apply -
|
||||
apply (subst signed_arith_sint)
|
||||
apply (clarsimp simp: word_size WORD_MAX_def)
|
||||
apply simp
|
||||
done
|
||||
by (clarsimp simp: word_size WORD_MAX_def signed_arith_sint)
|
||||
|
||||
lemma bang_big_nonneg:
|
||||
"\<lbrakk> 0 <=s (x::'a::len signed word); n \<ge> size x - 1 \<rbrakk> \<Longrightarrow> (x !! n) = False"
|
||||
|
|
@ -372,20 +363,13 @@ lemma abstract_val_unsigned_shiftr_unsigned:
|
|||
"\<lbrakk> abstract_val Px x unat (x' :: ('a :: len) word);
|
||||
abstract_val Pn n unat (n' :: ('a :: len) word) \<rbrakk> \<Longrightarrow>
|
||||
abstract_val (Px \<and> Pn) (x >> n) unat (x' >> unat n')"
|
||||
apply (simp add: shiftr_div_2n' shiftr_nat_def shiftr_int_def)
|
||||
apply (simp flip: zdiv_int[where b="2^n" for n, simplified])
|
||||
done
|
||||
by (simp add: shiftr_eq_drop_bit unat_drop_bit_eq)
|
||||
|
||||
lemma abstract_val_unsigned_shiftr_signed:
|
||||
"\<lbrakk> abstract_val Px x unat (x' :: ('a :: len) word);
|
||||
abstract_val Pn n sint (n' :: ('b :: len) signed word) \<rbrakk> \<Longrightarrow>
|
||||
abstract_val (Px \<and> Pn \<and> 0 \<le> n) (x >> nat n) unat (x' >> unat n')"
|
||||
apply (clarsimp simp: shiftr_div_2n' shiftr_nat_def shiftr_int_def)
|
||||
apply (simp flip: zdiv_int[where b="2^n" for n, simplified])
|
||||
apply (subst sint_eq_uint)
|
||||
apply (simp add: word_msb_sint)
|
||||
apply (simp add: unat_def)
|
||||
done
|
||||
by (clarsimp simp: shiftr_eq_drop_bit word_sle_def nat_sint unat_drop_bit_eq)
|
||||
|
||||
lemma abstract_val_unsigned_shiftl_unsigned:
|
||||
"\<lbrakk> abstract_val Px x unat (x' :: ('a :: len) word);
|
||||
|
|
@ -401,9 +385,7 @@ lemma abstract_val_unsigned_shiftl_signed:
|
|||
(x << nat n) unat (x' << unat n')"
|
||||
apply (clarsimp simp: shiftl_t2n shiftl_nat_alt_def unat_mult_simple field_simps)
|
||||
apply (simp add: sint_eq_uint word_msb_sint)
|
||||
apply (simp flip: unat_def)
|
||||
apply (simp add: uint_nat unat_mult_simple)
|
||||
done
|
||||
by (metis nat_less_iff uint_ge_0 unat_def unat_of_nat_len unat_power_lower word_arith_nat_mult)
|
||||
|
||||
(* TODO: this would be useful for simplifying signed left shift c_guards,
|
||||
which are already implied by the generated word abs guard (premise #2).
|
||||
|
|
@ -504,7 +486,7 @@ lemma abstract_val_scast:
|
|||
apply (clarsimp simp: down_cast_same [symmetric] is_down unat_ucast)
|
||||
apply (subst sint_eq_uint)
|
||||
apply (clarsimp simp: word_msb_sint)
|
||||
apply (clarsimp simp: unat_def [symmetric])
|
||||
apply clarsimp
|
||||
apply (subst word_unat.norm_Rep [symmetric])
|
||||
apply clarsimp
|
||||
done
|
||||
|
|
@ -519,10 +501,7 @@ lemma abstract_val_scast_downcast:
|
|||
"\<lbrakk> len_of TYPE('b) < len_of TYPE('a::len);
|
||||
abstract_val P C' sint C \<rbrakk>
|
||||
\<Longrightarrow> abstract_val P (sbintrunc ((len_of TYPE('b::len) - 1)) C') sint (scast (C :: 'a signed word) :: 'b signed word)"
|
||||
apply (auto simp add: scast_def sint_uint simp flip: bintrunc_mod2p)
|
||||
apply transfer
|
||||
using sbintrunc_bintrunc_lt apply auto
|
||||
done
|
||||
by (auto simp add: scast_def sint_uint simp flip: bintrunc_mod2p)
|
||||
|
||||
lemma abstract_val_ucast_upcast:
|
||||
"\<lbrakk> len_of TYPE('a::len) \<le> len_of TYPE('b::len);
|
||||
|
|
@ -534,11 +513,10 @@ lemma abstract_val_ucast_downcast:
|
|||
"\<lbrakk> len_of TYPE('b::len) < len_of TYPE('a::len);
|
||||
abstract_val P C' unat C \<rbrakk>
|
||||
\<Longrightarrow> abstract_val P (C' mod (UWORD_MAX TYPE('b) + 1)) unat (ucast (C :: 'a word) :: 'b word)"
|
||||
apply (clarsimp simp: scast_def word_of_int_def sint_uint UWORD_MAX_def)
|
||||
apply (clarsimp simp: scast_def sint_uint UWORD_MAX_def)
|
||||
unfolding ucast_def unat_def
|
||||
apply (subst int_word_uint)
|
||||
apply (metis (hide_lams, mono_tags) uint_mod uint_power_lower
|
||||
unat_def unat_mod unat_power_lower)
|
||||
apply (metis (hide_lams, mono_tags) uint_mod uint_power_lower unat_def unat_mod unat_power_lower)
|
||||
done
|
||||
|
||||
(*
|
||||
|
|
@ -557,15 +535,15 @@ lemma valid_typ_abs_fn_id:
|
|||
|
||||
lemma valid_typ_abs_fn_unit:
|
||||
"valid_typ_abs_fn \<top> \<top> id (id :: unit \<Rightarrow> unit)"
|
||||
by clarsimp
|
||||
by (fact valid_typ_abs_fn_id)
|
||||
|
||||
lemma valid_typ_abs_fn_unat:
|
||||
"valid_typ_abs_fn (\<lambda>v. v \<le> UWORD_MAX TYPE('a::len)) \<top> (unat :: 'a word \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> 'a word)"
|
||||
by (clarsimp simp: unat_of_nat_eq UWORD_MAX_def le_to_less_plus_one)
|
||||
by (clarsimp simp: UWORD_MAX_def le_less_trans take_bit_nat_eq_self_iff)
|
||||
|
||||
lemma valid_typ_abs_fn_sint:
|
||||
"valid_typ_abs_fn (\<lambda>v. WORD_MIN TYPE('a::len) \<le> v \<and> v \<le> WORD_MAX TYPE('a)) \<top> (sint :: 'a signed word \<Rightarrow> int) (of_int :: int \<Rightarrow> 'a signed word)"
|
||||
by (clarsimp simp: sint_of_int_eq WORD_MIN_def WORD_MAX_def)
|
||||
by (clarsimp simp: sint_of_int_eq WORD_MIN_def WORD_MAX_def simp del: signed_of_int)
|
||||
|
||||
lemma valid_typ_abs_fn_tuple:
|
||||
"\<lbrakk> valid_typ_abs_fn P_a Q_a abs_a conc_a; valid_typ_abs_fn P_b Q_b abs_b conc_b \<rbrakk> \<Longrightarrow>
|
||||
|
|
@ -912,11 +890,11 @@ lemma abstract_val_case_prod_fun_app:
|
|||
|
||||
lemma abstract_val_of_nat:
|
||||
"abstract_val (r \<le> UWORD_MAX TYPE('a::len)) r unat (of_nat r :: 'a word)"
|
||||
by (clarsimp simp: unat_of_nat_eq UWORD_MAX_def le_to_less_plus_one)
|
||||
by (clarsimp simp: unat_of_nat_eq UWORD_MAX_def le_to_less_plus_one simp del: unsigned_of_nat)
|
||||
|
||||
lemma abstract_val_of_int:
|
||||
"abstract_val (WORD_MIN TYPE('a::len) \<le> r \<and> r \<le> WORD_MAX TYPE('a)) r sint (of_int r :: 'a signed word)"
|
||||
by (clarsimp simp: sint_of_int_eq WORD_MIN_def WORD_MAX_def)
|
||||
by (clarsimp simp: sint_of_int_eq WORD_MIN_def WORD_MAX_def simp del: signed_of_int)
|
||||
|
||||
lemma abstract_val_tuple:
|
||||
"\<lbrakk> abstract_val P a absL a';
|
||||
|
|
@ -953,7 +931,7 @@ lemma abstract_val_unwrap:
|
|||
lemma abstract_val_uint:
|
||||
"\<lbrakk> introduce_typ_abs_fn unat; abstract_val P x unat x' \<rbrakk>
|
||||
\<Longrightarrow> abstract_val P (int x) id (uint x')"
|
||||
by (clarsimp simp: uint_nat)
|
||||
by clarsimp
|
||||
|
||||
lemma corresTA_L2_recguard:
|
||||
"corresTA (\<lambda>s. P s) rx ex A A' \<Longrightarrow>
|
||||
|
|
@ -1051,11 +1029,8 @@ lemma scast_ucast_simps [simp, L2opt]:
|
|||
(ucast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a"
|
||||
"\<lbrakk> len_of TYPE('a) \<le> len_of TYPE('b) \<rbrakk> \<Longrightarrow>
|
||||
(scast (scast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = scast a"
|
||||
by (auto simp: is_up is_down
|
||||
scast_ucast_1 scast_ucast_3 scast_ucast_4
|
||||
ucast_scast_1 ucast_scast_3 ucast_scast_4
|
||||
scast_scast_a scast_scast_b
|
||||
ucast_ucast_a ucast_ucast_b)
|
||||
by (auto simp: is_up is_down scast_ucast_3 scast_ucast_4 ucast_scast_3 ucast_scast_4
|
||||
scast_scast_b ucast_ucast_a ucast_ucast_b)
|
||||
|
||||
declare len_signed [L2opt]
|
||||
|
||||
|
|
|
|||
|
|
@ -318,7 +318,7 @@ let
|
|||
val {base = locale_name,...} = OS.Path.splitBaseExt (OS.Path.file filename)
|
||||
val locale_name = case !(#c_locale opt) of NONE => locale_name
|
||||
| SOME l => l
|
||||
val lthy = case try (Named_Target.begin (locale_name, Position.none)) thy of
|
||||
val lthy = case try (Target_Context.context_begin_named_cmd [] (locale_name, Position.none)) thy of
|
||||
SOME lthy => lthy
|
||||
| NONE => error ("autocorres: no such locale: " ^ locale_name)
|
||||
|
||||
|
|
@ -722,7 +722,7 @@ let
|
|||
|
||||
in
|
||||
(* Exit context. *)
|
||||
Named_Target.exit lthy
|
||||
Target_Context.end_named_cmd lthy |> Context.the_theory
|
||||
end
|
||||
|
||||
end
|
||||
|
|
@ -61,6 +61,8 @@ signature AUTOCORRES_TRACE = sig
|
|||
Proof.context -> (cterm -> thm) -> thm -> bool -> thm * SimpTrace option
|
||||
|
||||
val print_ac_trace: thm RuleTrace -> string
|
||||
val print_ac_simp_trace: SimpTrace -> string
|
||||
|
||||
val writeFile: string -> string -> unit
|
||||
end;
|
||||
|
||||
|
|
@ -368,8 +370,18 @@ fun print_ac_trace' indent (RuleTrace tr) =
|
|||
indent' ^ "Step: " ^ print_thm (#step tr |> fst) ^ "\n\n" ^
|
||||
String.concat (map (print_ac_trace' indent') (#trace tr) |> intercalate ["\n"]))
|
||||
end
|
||||
|
||||
in
|
||||
val print_ac_trace = print_ac_trace' ""
|
||||
|
||||
fun print_ac_simp_trace (SimpTrace tr) =
|
||||
let val print_cterm = cterm_to_string true
|
||||
val print_thm = Thm.cprop_of #> print_cterm
|
||||
in
|
||||
"Equation: " ^ print_thm(#equation tr) ^ "\n" ^
|
||||
"Thms: \n" ^
|
||||
String.concat (map (fn (name, thm) => name ^ ": " ^ print_cterm thm) (#thms tr) |> intercalate ["\n"])
|
||||
end
|
||||
end
|
||||
|
||||
fun writeFile filename string =
|
||||
|
|
|
|||
|
|
@ -432,7 +432,7 @@ let
|
|||
* HACK: Exit and enter the context again, so the simpset created by the new
|
||||
* record gets imported in. No idea what the "correct" way of doing this is.
|
||||
*)
|
||||
val lthy = Local_Theory.exit_global lthy |> Named_Target.init (the (Named_Target.locale_of lthy))
|
||||
val lthy = Local_Theory.exit_global lthy |> Named_Target.init [] (the (Named_Target.locale_of lthy))
|
||||
|
||||
(* Generate a function mapping old globals to the new globals. *)
|
||||
val (lift_name, lift_def, simp_thms, lthy) = gen_heap_abs_fn
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ val the' = Utils.the'
|
|||
|
||||
(* Simpset we use for automated tactics. *)
|
||||
fun setup_l2_ss ctxt = put_simpset AUTOCORRES_SIMPSET ctxt
|
||||
addsimps [@{thm ucast_id}, @{thm pred_conj_def}]
|
||||
addsimps [@{thm pred_conj_def}]
|
||||
|
||||
(* Convert a set of variable names into an Isabelle list of strings. *)
|
||||
fun var_set_to_isa_list prog_info s =
|
||||
|
|
@ -56,8 +56,7 @@ fun var_set_to_isa_list prog_info s =
|
|||
*
|
||||
* would return ("x", @{term "x + b + c"}).
|
||||
*)
|
||||
fun convert_local_vars name_map term [] = ([], term)
|
||||
| convert_local_vars name_map term ((var_name, var_term) :: vars) =
|
||||
fun convert_local_vars name_map term [] = ([], term) | convert_local_vars name_map term ((var_name, var_term) :: vars) =
|
||||
if Utils.contains_subterm var_term term then
|
||||
let
|
||||
val free_var = name_map (var_name, fastype_of var_term)
|
||||
|
|
|
|||
|
|
@ -43,9 +43,7 @@ lemma heap_update_heap_update_list:
|
|||
apply (subst if_P)
|
||||
apply (fastforce intro: intvlI)
|
||||
apply (clarsimp simp: unat_of_nat word_bits_def)
|
||||
apply (subst (1 2) heap_update_list_value,
|
||||
simp add: addr_card,
|
||||
simp add: addr_card)
|
||||
apply (subst (1 2) heap_update_list_value, simp add: addr_card, simp add: addr_card)
|
||||
apply (case_tac "x \<in> {q..+length l}")
|
||||
apply (subst if_P, simp)
|
||||
apply (subst if_P)
|
||||
|
|
|
|||
|
|
@ -344,8 +344,7 @@ lemma ptr_offsets_eq2 [simp]:
|
|||
"\<lbrakk> unat i * size_of TYPE(word32) < 2 ^ len_of TYPE(addr_bitsize);
|
||||
unat j * size_of TYPE(word32) < 2 ^ len_of TYPE(addr_bitsize) \<rbrakk> \<Longrightarrow>
|
||||
(a +\<^sub>p uint i = a +\<^sub>p uint j) = (i = j)"
|
||||
by (simp add: uint_nat)
|
||||
|
||||
by (simp add: ptr_add_def word32_mult_cancel_right)
|
||||
|
||||
(* Array update simplification *)
|
||||
|
||||
|
|
@ -528,7 +527,7 @@ lemma partition_correct:
|
|||
apply (unfold partitioned_def)
|
||||
apply clarsimp
|
||||
apply (case_tac "i = unat aa")
|
||||
apply (simp add: uint_nat, unat_arith)
|
||||
apply (metis less_or_eq_imp_le not_less uint_nat word_less_nat_alt)
|
||||
apply (subgoal_tac "i < unat aa", simp)
|
||||
apply unat_arith
|
||||
apply (rule_tac n = "n" in array_valid_elem2, assumption+)
|
||||
|
|
@ -542,7 +541,7 @@ lemma partition_correct:
|
|||
apply clarsimp
|
||||
apply unat_arith
|
||||
defer
|
||||
apply (clarsimp simp: is_array_def array_loc_valid_def uint_nat)
|
||||
apply (clarsimp simp: is_array_def array_loc_valid_def)
|
||||
apply (intro conjI impI allI)
|
||||
apply simp
|
||||
apply (simp add: CTypesDefs.ptr_add_def)
|
||||
|
|
@ -550,12 +549,16 @@ lemma partition_correct:
|
|||
apply (simp add: CTypesDefs.ptr_add_def)
|
||||
apply unat_arith
|
||||
apply (simp add: CTypesDefs.ptr_add_def)
|
||||
apply (simp only: uint_nat)
|
||||
apply (subst (asm) (2) ptr_offsets_eq)
|
||||
apply (simp, unat_arith)
|
||||
apply (simp, unat_arith)
|
||||
apply (simp, unat_arith)
|
||||
apply clarsimp
|
||||
apply unat_arith
|
||||
apply (simp only: uint_nat)
|
||||
apply (subst (asm) ptr_offsets_eq, simp, unat_arith, simp, unat_arith)+
|
||||
apply simp
|
||||
apply (simp only: uint_nat)
|
||||
apply (subst (asm) (3) ptr_offsets_eq)
|
||||
apply (simp, unat_arith)
|
||||
apply (simp, unat_arith)
|
||||
|
|
@ -568,11 +571,13 @@ lemma partition_correct:
|
|||
apply (subgoal_tac "\<not> unat aa < unat (b + 1)", simp)
|
||||
apply simp
|
||||
apply unat_arith
|
||||
apply unat_arith
|
||||
apply (subst (asm) (4) ptr_offsets_eq)
|
||||
subgoal by unat_arith
|
||||
apply (simp only: uint_nat)
|
||||
apply (subst (asm) (3) ptr_offsets_eq)
|
||||
apply (simp, unat_arith)
|
||||
apply (simp, unat_arith)
|
||||
apply simp
|
||||
apply (simp only: uint_nat)
|
||||
apply (subst (asm) ptr_offsets_eq, simp, unat_arith, simp, unat_arith)+
|
||||
apply clarsimp
|
||||
apply (drule_tac x = "i" in spec)
|
||||
|
|
@ -602,22 +607,22 @@ lemma partition_correct:
|
|||
apply (subgoal_tac "a \<le> a +\<^sub>p uint b", simp)
|
||||
apply (rule_tac n = "n" in array_no_wrap2, simp, unat_arith)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "a +\<^sub>p uint b < a +\<^sub>p uint n", simp add: uint_nat)
|
||||
apply (subgoal_tac "a +\<^sub>p uint b < a +\<^sub>p uint n", simp)
|
||||
apply (erule_tac n = "n" in array_loc_strict_mono2, unat_arith)
|
||||
apply (subgoal_tac "a \<le> a +\<^sub>p uint (b + 1)", simp)
|
||||
apply (erule_tac n = "n" in array_no_wrap2, unat_arith)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "a +\<^sub>p uint aa < a +\<^sub>p uint n", simp add: uint_nat)
|
||||
apply (subgoal_tac "a +\<^sub>p uint aa < a +\<^sub>p uint n", simp)
|
||||
apply (rule_tac n = "n" in array_loc_strict_mono2, assumption+)
|
||||
apply (subgoal_tac "a \<le> a +\<^sub>p uint aa", simp)
|
||||
apply (rule_tac n = "n" in array_no_wrap2, assumption+)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "a +\<^sub>p uint aa < a +\<^sub>p uint n", simp add: uint_nat)
|
||||
apply (subgoal_tac "a +\<^sub>p uint aa < a +\<^sub>p uint n", simp)
|
||||
apply (rule_tac n = "n" in array_loc_strict_mono2, assumption+)
|
||||
apply (subgoal_tac "a \<le> a +\<^sub>p uint (b + 1)", simp)
|
||||
apply (erule_tac n = "n" in array_no_wrap2, unat_arith)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "a +\<^sub>p uint (b + 1) < a +\<^sub>p uint n", simp add: uint_nat)
|
||||
apply (subgoal_tac "a +\<^sub>p uint (b + 1) < a +\<^sub>p uint n", simp)
|
||||
apply (erule_tac n = "n" in array_loc_strict_mono2, unat_arith)
|
||||
done
|
||||
|
||||
|
|
@ -758,7 +763,7 @@ lemma partitioned_after_shuffling_left:
|
|||
\<Longrightarrow> partitioned s a (unat n) (unat pivot_idx)"
|
||||
apply (clarsimp simp: partitioned_def unmodified_outside_range_def)
|
||||
apply (subgoal_tac "heap_w32 s (a +\<^sub>p uint pivot_idx) =
|
||||
heap_w32 s0 (a +\<^sub>p uint pivot_idx)", simp add: uint_nat)
|
||||
heap_w32 s0 (a +\<^sub>p uint pivot_idx)", simp)
|
||||
apply (subgoal_tac "array_not_at_mem_end a (unat pivot_idx)")
|
||||
apply (case_tac "i < unat pivot_idx", clarsimp)
|
||||
apply (subgoal_tac "\<exists>j. (j < unat pivot_idx \<and>
|
||||
|
|
@ -766,7 +771,7 @@ lemma partitioned_after_shuffling_left:
|
|||
apply clarsimp
|
||||
apply (drule_tac x = "j" in spec)
|
||||
apply (subgoal_tac "j < unat n")
|
||||
apply (clarsimp simp: uint_nat)
|
||||
apply (clarsimp)
|
||||
apply unat_arith
|
||||
apply (erule old_array_elem, simp)
|
||||
apply (drule_tac x = "a +\<^sub>p int i" in spec)
|
||||
|
|
@ -780,7 +785,7 @@ lemma partitioned_after_shuffling_left:
|
|||
unat_arith)
|
||||
apply (drule_tac x = "a +\<^sub>p uint pivot_idx" in spec)
|
||||
apply (subgoal_tac "array_not_at_mem_end a (unat pivot_idx)")
|
||||
apply (simp add: uint_nat)
|
||||
apply (simp)
|
||||
apply (erule_tac s = "s0" and n = "unat n" in subarray_not_at_mem_end2,
|
||||
unat_arith)
|
||||
done
|
||||
|
|
@ -813,8 +818,8 @@ lemma partitioned_after_shuffling_right:
|
|||
apply (case_tac "i \<le> unat pivot_idx")
|
||||
apply (frule_tac x = "a +\<^sub>p int i" in spec)
|
||||
apply (subgoal_tac "a +\<^sub>p int i < a +\<^sub>p int (Suc (unat pivot_idx))")
|
||||
apply (simp add: uint_nat)
|
||||
apply (erule array_loc_strict_mono, simp)
|
||||
apply simp
|
||||
apply (erule array_loc_strict_mono, simp)
|
||||
apply (subgoal_tac "\<not> i < unat pivot_idx")
|
||||
prefer 2
|
||||
apply unat_arith
|
||||
|
|
@ -878,12 +883,13 @@ lemma partitioned_array_sorted:
|
|||
|
||||
lemma array_index_Suc:
|
||||
"a +\<^sub>p uint m +\<^sub>p 1 = a +\<^sub>p int (Suc (unat m))"
|
||||
by (simp add: uint_nat)
|
||||
by simp
|
||||
|
||||
lemma array_loc_le_Suc:
|
||||
"array_not_at_mem_end a (Suc (unat m)) \<Longrightarrow> a +\<^sub>p int (unat m) \<le> a +\<^sub>p 1 +\<^sub>p uint m"
|
||||
"array_not_at_mem_end a (Suc (unat m)) \<Longrightarrow> a +\<^sub>p uint m \<le> a +\<^sub>p 1 +\<^sub>p uint m"
|
||||
apply (subst ptr_add_commute)
|
||||
apply (subst array_index_Suc)
|
||||
apply (simp only: uint_nat)
|
||||
apply (rule array_loc_mono, simp+)
|
||||
done
|
||||
|
||||
|
|
@ -971,7 +977,7 @@ next
|
|||
apply (erule is_still_array)
|
||||
apply (rule disjI2, rule disjI1)
|
||||
apply (simp add: array_loc_le_Suc)
|
||||
apply (simp add: uint_nat)
|
||||
apply simp
|
||||
apply unat_arith
|
||||
apply unat_arith
|
||||
apply (rule_tac ?s1.0 = "s'a" and m = "Suc (unat rv)"
|
||||
|
|
@ -981,7 +987,7 @@ next
|
|||
in is_array_after_changing_left)
|
||||
apply unat_arith
|
||||
apply assumption+
|
||||
apply (simp add: uint_nat)+
|
||||
apply (simp)+
|
||||
apply (subgoal_tac "mset (the_array s'b a (unat n)) =
|
||||
mset (the_array s'a a (unat n))")
|
||||
apply (subgoal_tac "mset (the_array s'a a (unat n)) =
|
||||
|
|
@ -1006,15 +1012,16 @@ next
|
|||
apply (simp add: is_array_def)
|
||||
apply (rule disjI1, rule conjI)
|
||||
apply (erule subarray_not_at_mem_end2, unat_arith)
|
||||
apply simp
|
||||
apply (rule array_loc_le_Suc)
|
||||
apply (erule subarray_not_at_mem_end2, unat_arith)
|
||||
apply (simp add: uint_nat)
|
||||
apply simp
|
||||
apply (rule_tac ?s0.0 = "s'a" in partitioned_after_shuffling_right)
|
||||
apply (rule_tac ?s1.0 = "s'" and m = "unat rv" in is_array_after_changing_left)
|
||||
apply unat_arith
|
||||
apply assumption+
|
||||
apply (rule_tac ?s0.0 = "s'" in partitioned_after_shuffling_left, assumption+)
|
||||
apply (simp add: uint_nat)+
|
||||
apply simp+
|
||||
apply (erule unmodified_outside_range_trans)
|
||||
apply (rule_tac ?s2.0 = "s'a" in unmodified_outside_range_trans)
|
||||
apply (rule_tac m = "unat rv" in unmodified_outside_subrange1)
|
||||
|
|
@ -1023,7 +1030,7 @@ next
|
|||
apply unat_arith
|
||||
apply (rule_tac m = "Suc (unat rv)" in unmodified_outside_subrange2)
|
||||
apply (simp add: is_array_def)
|
||||
apply (simp add: uint_nat)
|
||||
apply simp
|
||||
apply unat_arith
|
||||
apply (case_tac "n = 1", simp)
|
||||
apply (subgoal_tac "n = 0", simp, unat_arith)
|
||||
|
|
|
|||
|
|
@ -212,7 +212,7 @@ lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_abs_S' (x
|
|||
lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32\<rbrace>
|
||||
U_shiftl_S_abs_S' (x::word32) (n::int)
|
||||
\<lbrace>\<lambda>r s. r = x << nat n\<rbrace>!"
|
||||
by (wpsimp simp: U_shiftl_S_abs_S'_def UINT_MAX_def unat_of_int)
|
||||
by (wpsimp simp: U_shiftl_S_abs_S'_def unat_of_int)
|
||||
|
||||
lemma "n <s 0 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_no_abs' (x :: word32) (n :: sword32))"
|
||||
by (monad_eq simp: U_shiftl_S_no_abs'_def no_fail_def word_sle_def word_sless_alt)
|
||||
|
|
@ -229,11 +229,11 @@ lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_US' (x :: i
|
|||
by (monad_eq simp: S_shiftl_U_abs_US'_def no_fail_def)
|
||||
lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_US' (x :: int) (n :: nat))"
|
||||
by (monad_eq simp: S_shiftl_U_abs_US'_def no_fail_def)
|
||||
lemma "x << nat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_US' (x :: int) (n :: nat))"
|
||||
lemma "x << n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_US' (x :: int) (n :: nat))"
|
||||
by (monad_eq simp: S_shiftl_U_abs_US'_def no_fail_def INT_MAX_def)
|
||||
lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 \<le> x \<and> x << nat n \<le> INT_MAX\<rbrace>
|
||||
lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 \<le> x \<and> x << n \<le> INT_MAX\<rbrace>
|
||||
S_shiftl_U_abs_US' (x::int) (n::nat)
|
||||
\<lbrace>\<lambda>r s. r = x << nat n\<rbrace>!"
|
||||
\<lbrace>\<lambda>r s. r = x << n\<rbrace>!"
|
||||
apply (wpsimp simp: S_shiftl_U_abs_US'_def INT_MAX_def shiftl_nat_def shiftl_int_def)
|
||||
apply (subst unat_of_int)
|
||||
apply simp
|
||||
|
|
@ -253,11 +253,14 @@ lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_U' (x
|
|||
apply (monad_eq simp: S_shiftl_U_abs_U'_def no_fail_def)
|
||||
oops \<comment> \<open>C parser issue: Jira VER-509\<close>
|
||||
lemma "sint x << n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_U' (x :: sword32) (n :: nat))"
|
||||
supply Word.of_nat_unat[simp del]
|
||||
by (monad_eq simp: S_shiftl_U_abs_U'_def no_fail_def shiftl_int_def INT_MAX_def
|
||||
nat_int_comparison(2) int_unat_nonneg)
|
||||
lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 <=s x \<and> sint x << nat n \<le> INT_MAX\<rbrace>
|
||||
|
||||
lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 <=s x \<and> sint x << n \<le> INT_MAX\<rbrace>
|
||||
S_shiftl_U_abs_U' (x::sword32) (n::nat)
|
||||
\<lbrace>\<lambda>r s. r = x << nat n\<rbrace>!"
|
||||
\<lbrace>\<lambda>r s. r = x << n\<rbrace>!"
|
||||
supply Word.of_nat_unat[simp del]
|
||||
by (wpsimp simp: S_shiftl_U_abs_U'_def INT_MAX_def shiftl_int_def
|
||||
nat_int_comparison(2) int_unat_nonneg)
|
||||
|
||||
|
|
@ -291,11 +294,13 @@ lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_no_abs' (x
|
|||
apply (monad_eq simp: S_shiftl_U_no_abs'_def no_fail_def)
|
||||
oops \<comment> \<open>C parser issue: Jira VER-509\<close>
|
||||
lemma "sint x << unat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_no_abs' (x :: sword32) (n :: word32))"
|
||||
supply Word.of_nat_unat[simp del]
|
||||
by (monad_eq simp: S_shiftl_U_no_abs'_def no_fail_def shiftl_int_def INT_MAX_def
|
||||
nat_int_comparison(2) int_unat_nonneg)
|
||||
lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 <=s x \<and> sint x << unat n \<le> INT_MAX\<rbrace>
|
||||
S_shiftl_U_no_abs' (x::sword32) (n::word32)
|
||||
\<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!"
|
||||
supply Word.of_nat_unat[simp del]
|
||||
by (wpsimp simp: S_shiftl_U_no_abs'_def INT_MAX_def shiftl_int_def
|
||||
nat_int_comparison(2) int_unat_nonneg)
|
||||
|
||||
|
|
@ -337,11 +342,13 @@ lemma "32 <=s n \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_U' (x ::
|
|||
apply (monad_eq simp: S_shiftl_S_abs_U'_def no_fail_def word_sle_def word_sless_alt)
|
||||
oops \<comment> \<open>C parser issue: Jira VER-509\<close>
|
||||
lemma "sint x << unat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_U' (x :: sword32) (n :: sword32))"
|
||||
supply Word.of_nat_unat[simp del]
|
||||
by (monad_eq simp: S_shiftl_S_abs_U'_def no_fail_def shiftl_int_def INT_MAX_def
|
||||
nat_int_comparison(2) int_unat_nonneg)
|
||||
lemma "\<lbrace>\<lambda>s. 0 <=s n \<and> n <s 32 \<and> 0 <=s x \<and> sint x << unat n \<le> INT_MAX\<rbrace>
|
||||
S_shiftl_S_abs_U' (x::sword32) (n::sword32)
|
||||
\<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!"
|
||||
supply Word.of_nat_unat[simp del]
|
||||
by (wpsimp simp: S_shiftl_S_abs_U'_def INT_MAX_def shiftl_int_def
|
||||
nat_int_comparison(2) int_unat_nonneg)
|
||||
|
||||
|
|
@ -351,22 +358,22 @@ lemma "n < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_S' (x :: in
|
|||
by (monad_eq simp: S_shiftl_S_abs_S'_def no_fail_def)
|
||||
lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_S' (x :: int) (n :: int))"
|
||||
by (monad_eq simp: S_shiftl_S_abs_S'_def no_fail_def)
|
||||
lemma "x << n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_S' (x :: int) (n :: int))"
|
||||
lemma "x << nat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_S' (x :: int) (n :: int))"
|
||||
by (monad_eq simp: S_shiftl_S_abs_S'_def no_fail_def INT_MAX_def)
|
||||
lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32 \<and> 0 \<le> x \<and> x << n \<le> INT_MAX\<rbrace>
|
||||
lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32 \<and> 0 \<le> x \<and> x << nat n \<le> INT_MAX\<rbrace>
|
||||
S_shiftl_S_abs_S' (x::int) (n::int)
|
||||
\<lbrace>\<lambda>r s. r = x << nat n\<rbrace>!"
|
||||
apply (wpsimp simp: S_shiftl_S_abs_S'_def INT_MAX_def shiftl_nat_def shiftl_int_def)
|
||||
apply (subst unat_of_int)
|
||||
apply simp
|
||||
apply (drule le_less_trans[where x="x*2^n" and z="2^32"])
|
||||
apply (drule le_less_trans[where x="x*2^nat n" and z="2^32"])
|
||||
apply simp
|
||||
apply (subst mult_less_cancel_left_pos[where c="2^n", symmetric])
|
||||
apply (subst mult_less_cancel_left_pos[where c="2^nat n", symmetric])
|
||||
apply simp
|
||||
apply (subst (asm) mult.commute)
|
||||
apply (erule less_le_trans)
|
||||
apply simp
|
||||
apply (simp add: le_unat_uoi[where z="32"])
|
||||
apply (simp add: unat_of_int_32)
|
||||
apply (simp flip: nat_mult_distrib nat_power_eq nat_numeral)
|
||||
done
|
||||
|
||||
|
|
@ -378,11 +385,13 @@ lemma "32 <=s n \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_no_abs' (x :
|
|||
apply (monad_eq simp: S_shiftl_S_no_abs'_def no_fail_def)
|
||||
oops \<comment> \<open>C parser issue: Jira VER-509\<close>
|
||||
lemma "sint x << unat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_no_abs' (x :: sword32) (n :: sword32))"
|
||||
supply Word.of_nat_unat[simp del]
|
||||
by (monad_eq simp: S_shiftl_S_no_abs'_def no_fail_def shiftl_int_def INT_MAX_def
|
||||
nat_int_comparison(2) int_unat_nonneg)
|
||||
lemma "\<lbrace>\<lambda>s. 0 <=s n \<and> n <s 32 \<and> 0 <=s x \<and> sint x << unat n \<le> INT_MAX\<rbrace>
|
||||
S_shiftl_S_no_abs' (x::sword32) (n::sword32)
|
||||
\<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!"
|
||||
supply Word.of_nat_unat[simp del]
|
||||
by (wpsimp simp: S_shiftl_S_no_abs'_def INT_MAX_def shiftl_int_def
|
||||
nat_int_comparison(2) int_unat_nonneg)
|
||||
|
||||
|
|
@ -447,14 +456,14 @@ lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_US' (x :: i
|
|||
by (monad_eq simp: S_shiftr_U_abs_US'_def no_fail_def)
|
||||
lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_US' (x :: int) (n :: nat))"
|
||||
by (monad_eq simp: S_shiftr_U_abs_US'_def no_fail_def)
|
||||
lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 \<le> x\<rbrace> S_shiftr_U_abs_US' (x::int) (n::nat) \<lbrace>\<lambda>r s. r = x >> nat n\<rbrace>!"
|
||||
lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 \<le> x\<rbrace> S_shiftr_U_abs_US' (x::int) (n::nat) \<lbrace>\<lambda>r s. r = x >> n\<rbrace>!"
|
||||
by (wpsimp simp: S_shiftr_U_abs_US'_def)
|
||||
|
||||
lemma "x <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_U' (x :: sword32) (n :: nat))"
|
||||
by (monad_eq simp: S_shiftr_U_abs_U'_def no_fail_def word_sle_def word_sless_alt)
|
||||
lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_U' (x :: sword32) (n :: nat))"
|
||||
by (monad_eq simp: S_shiftr_U_abs_U'_def no_fail_def)
|
||||
lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 <=s x\<rbrace> S_shiftr_U_abs_U' (x::sword32) (n::nat) \<lbrace>\<lambda>r s. r = x >> nat n\<rbrace>!"
|
||||
lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 <=s x\<rbrace> S_shiftr_U_abs_U' (x::sword32) (n::nat) \<lbrace>\<lambda>r s. r = x >> n\<rbrace>!"
|
||||
by (wpsimp simp: S_shiftr_U_abs_U'_def)
|
||||
|
||||
lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_S' (x :: int) (n :: word32))"
|
||||
|
|
|
|||
|
|
@ -93,9 +93,9 @@ fun accumulate f acc xs = let
|
|||
(* Define a constant "name" of type "term" into the local theory "lthy". *)
|
||||
fun define_const name term lthy =
|
||||
let
|
||||
val lthy = lthy |> Local_Theory.open_target |> snd
|
||||
val lthy = lthy |> Local_Theory.begin_nested |> snd
|
||||
val ((_, (_, thm)), lthy) = Local_Theory.define ((Binding.name name, NoSyn), (Binding.empty_atts, term)) lthy
|
||||
val lthy' = Local_Theory.close_target lthy
|
||||
val lthy' = Local_Theory.end_nested lthy
|
||||
val thm' = Morphism.thm (Local_Theory.target_morphism lthy) thm
|
||||
in
|
||||
(thm', lthy')
|
||||
|
|
@ -116,13 +116,13 @@ fun define_const_args name hidden term args lthy =
|
|||
val new_term = Logic.mk_equals (head, term)
|
||||
|
||||
(* Define the constant. *)
|
||||
val lthy = lthy |> Local_Theory.open_target |> snd
|
||||
val lthy = lthy |> Local_Theory.begin_nested |> snd
|
||||
val ((_, (_, thm)), lthy) =
|
||||
Specification.definition (SOME (maybe_hide (Binding.name name), NONE, NoSyn))
|
||||
[] [] (Binding.empty_atts, new_term) lthy
|
||||
|
||||
(* Integrate into the current locale. *)
|
||||
val lthy' = Local_Theory.close_target lthy
|
||||
val lthy' = Local_Theory.end_nested lthy
|
||||
val thm' = Morphism.thm (Local_Theory.target_morphism lthy) thm
|
||||
in
|
||||
(Thm.prop_of thm' |> lhs_of |> Term.head_of, thm', lthy')
|
||||
|
|
@ -131,14 +131,14 @@ fun define_const_args name hidden term args lthy =
|
|||
(* Define lemmas into the local theory. *)
|
||||
fun define_lemmas name thm_list lthy =
|
||||
let
|
||||
val lthy = lthy |> Local_Theory.open_target |> snd
|
||||
val lthy = lthy |> Local_Theory.begin_nested |> snd
|
||||
val ((_, thms), lthy) = Local_Theory.note ((Binding.name name, []), thm_list) lthy
|
||||
(*
|
||||
* Restore the theory; not entirely sure why this is needed, but prevents
|
||||
* definitions from taking O(n^2) time (where "n" is the number of
|
||||
* definitions previously made).
|
||||
*)
|
||||
val lthy' = Local_Theory.close_target lthy
|
||||
val lthy' = Local_Theory.end_nested lthy
|
||||
val thms' = map (Morphism.thm (Local_Theory.target_morphism lthy)) thms
|
||||
in
|
||||
(thms', lthy')
|
||||
|
|
@ -147,9 +147,9 @@ fun define_lemmas name thm_list lthy =
|
|||
(* Define a single lemma into the local theory. *)
|
||||
fun define_lemma name thm lthy =
|
||||
let
|
||||
val lthy = lthy |> Local_Theory.open_target |> snd
|
||||
val lthy = lthy |> Local_Theory.begin_nested |> snd
|
||||
val (thms, lthy) = define_lemmas name [thm] lthy
|
||||
val lthy = Local_Theory.close_target lthy
|
||||
val lthy = Local_Theory.end_nested lthy
|
||||
in
|
||||
(hd thms, lthy)
|
||||
end
|
||||
|
|
@ -538,13 +538,13 @@ let
|
|||
val function_bodies = map (fn (a,b,c) => mk_fun_term a b c) func_defs
|
||||
|
||||
(* Define the function. *)
|
||||
val lthy = lthy |> Local_Theory.open_target |> snd
|
||||
val lthy = lthy |> Local_Theory.begin_nested |> snd
|
||||
val ctxt' = Function.add_function
|
||||
function_bindings
|
||||
(map (fn x => ((Binding.empty_atts, x), [], [])) function_bodies)
|
||||
Function_Common.default_config pat_completeness_auto lthy
|
||||
|> snd
|
||||
|> Local_Theory.close_target
|
||||
|> Local_Theory.end_nested
|
||||
|> prove_termination
|
||||
|> snd
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue