2016: partial progress updating CRefine
This commit is contained in:
parent
eb1fa521bc
commit
a333cd3d52
|
@ -1739,13 +1739,13 @@ lemma finish_ceqv_Seq_Skip_cases:
|
|||
|
||||
ML {*
|
||||
fun tac ctxt =
|
||||
rtac @{thm ccorres_abstract[where xf'="\<lambda>s. ()"]} 1
|
||||
resolve_tac ctxt [@{thm ccorres_abstract[where xf'="\<lambda>s. ()"]}] 1
|
||||
THEN (REPEAT_DETERM
|
||||
(resolve_tac ctxt @{thms While_ceqv[OF impI, OF refl] Cond_ceqv[OF impI, OF refl]
|
||||
ceqv_Seq_Skip_cases ceqv_Guard_UNIV[THEN iffD2]
|
||||
Guard_ceqv[OF impI, OF refl] ceqv_refl
|
||||
finish_ceqv_Seq_Skip_cases} 1
|
||||
ORELSE (rtac @{thm xpresI} THEN' simp_tac (ctxt |> Splitter.del_split @{thm "split_if"})) 1
|
||||
ORELSE (resolve_tac ctxt [@{thm xpresI}] THEN' simp_tac (ctxt |> Splitter.del_split @{thm "split_if"})) 1
|
||||
))
|
||||
THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms com.case}) 1
|
||||
*}
|
||||
|
|
|
@ -63,7 +63,7 @@ fun prim_trace_tac b depth s ctxt t thm = prim_trace_tac' b depth s ctxt (fn _ =
|
|||
are inifinite, for example *)
|
||||
fun nres_trace_tac ctxt s t thm = let
|
||||
val r = t thm
|
||||
fun p1 (t, s) = s ^ " ALT:\n" ^ Display.string_of_thm ctxt t ^ "\n"
|
||||
fun p1 (t, s) = s ^ " ALT:\n" ^ Thm.string_of_thm ctxt t ^ "\n"
|
||||
val _ = tracing (foldl p1 s (Seq.list_of r))
|
||||
in
|
||||
r
|
||||
|
@ -333,24 +333,24 @@ fun apply_ceqv_xpres_rules ctxt _ n = DETERM
|
|||
(warning ("apply_ceqv_xpres_rules: no rule applied"
|
||||
^ " - see CtacImpl.apply_ceqv_xpres_rules_trace");
|
||||
apply_ceqv_xpres_rules_trace := t;
|
||||
rtac ceqv_xpres_FalseI n)) n));
|
||||
resolve_tac ctxt [ceqv_xpres_FalseI] n)) n));
|
||||
|
||||
fun addcongs thms ss = foldl (uncurry Simplifier.add_cong) ss thms
|
||||
fun delsplits thms ss = foldl (uncurry Splitter.del_split) ss thms
|
||||
|
||||
fun solve_ceqv_xpres_rewrite_basic ctxt n = DETERM
|
||||
(safe_simp_tac (addcongs [ceqv_xpres_rewrite_basic_left_cong] (put_simpset HOL_basic_ss ctxt)) n
|
||||
THEN rtac ceqv_xpres_rewrite_basic_refl n);
|
||||
THEN resolve_tac ctxt [ceqv_xpres_rewrite_basic_refl] n);
|
||||
|
||||
fun solve_ceqv_xpres_basic_preserves ctxt n = DETERM
|
||||
((rtac ceqv_xpres_basic_preserves_TrueI n
|
||||
((resolve_tac ctxt [ceqv_xpres_basic_preserves_TrueI] n
|
||||
THEN SOLVE' (safe_simp_tac ctxt) n)
|
||||
ORELSE rtac ceqv_xpres_basic_preserves_FalseI n);
|
||||
ORELSE resolve_tac ctxt [ceqv_xpres_basic_preserves_FalseI] n);
|
||||
|
||||
fun solve_ceqv_xpres_lvar ctxt n = DETERM
|
||||
((rtac ceqv_xpres_lvar_nondet_init_TrueI n
|
||||
((resolve_tac ctxt [ceqv_xpres_lvar_nondet_init_TrueI] n
|
||||
THEN SOLVE' (safe_simp_tac ctxt) n)
|
||||
ORELSE rtac ceqv_xpres_lvar_nondet_init_FalseI n);
|
||||
ORELSE resolve_tac ctxt [ceqv_xpres_lvar_nondet_init_FalseI] n);
|
||||
|
||||
fun abstract_upds ctxt t = let
|
||||
val sT = domain_type (fastype_of t)
|
||||
|
@ -390,11 +390,11 @@ fun ceqv_restore_args_tac ctxt = SUBGOAL (fn (t, n) => case
|
|||
in Abs ("s", sT, updC $ Abs ("x", dummyT, accC $ Bound 1)
|
||||
$ (f $ Bound 0)) end
|
||||
val g = fold add_upd new_upds f |> Syntax.check_term ctxt |> Thm.cterm_of ctxt
|
||||
val thm = cterm_instantiate [(@{cpat "?f :: ?'a => ?'a"}, Thm.cterm_of ctxt f),
|
||||
(@{cpat "?g :: ?'a => ?'a"}, g)]
|
||||
val thm = infer_instantiate ctxt [(("f",0), Thm.cterm_of ctxt f),
|
||||
(("g",0), g)]
|
||||
@{thm ceqv_xpres_call_restore_argsI}
|
||||
|> Drule.generalize ([], map (dest_Free #> fst) xs)
|
||||
in rtac thm n THEN simp_tac ctxt n end)
|
||||
in resolve_tac ctxt [thm] n THEN simp_tac ctxt n end)
|
||||
|
||||
fun ceqv2_consts_and_tacs ctxt = map (apfst (fst o dest_Const)) [
|
||||
(@{term ceqv_xpres}, apply_ceqv_xpres_rules ctxt),
|
||||
|
@ -415,8 +415,8 @@ fun ceqv2_all_tacs ctxt = SUBGOAL (fn (t, n) =>
|
|||
|
||||
fun ceqv2_tac ctxt n = let
|
||||
in
|
||||
rtac ceqv_xpres_ceqvI n THEN
|
||||
SELECT_GOAL (REPEAT_DETERM (etac thin_rl 1)
|
||||
resolve_tac ctxt [ceqv_xpres_ceqvI] n THEN
|
||||
SELECT_GOAL (REPEAT_DETERM (eresolve_tac ctxt [thin_rl] 1)
|
||||
THEN REPEAT_DETERM (ceqv2_all_tacs ctxt 1)) n
|
||||
end;
|
||||
|
||||
|
@ -440,7 +440,7 @@ fun corres_pre_lift_tac lift_thm trace depth ctxt xf =
|
|||
val var_name = (unsuffix "_'" base_xf handle Fail _ => "rv")
|
||||
in if base_xf = "globals"
|
||||
then resolve_tac ctxt [my_thm ctxt "ccorres_special_trim_Int"]
|
||||
else EVERY' [TRY o rtac (my_thm ctxt "ccorres_introduce_UNIV_Int_when_needed"),
|
||||
else EVERY' [TRY o resolve_tac ctxt [my_thm ctxt "ccorres_introduce_UNIV_Int_when_needed"],
|
||||
Rule_Insts.res_inst_tac ctxt [((("xf'", 0), Position.none), xf)] [] (my_thm ctxt "ccorres_tmp_lift1"),
|
||||
rename_fresh_tac var_name,
|
||||
resolve_tac ctxt [my_thm ctxt lift_thm],
|
||||
|
@ -731,9 +731,8 @@ fun instantiate_xf_type ctxt tp which thms = let
|
|||
val ctp = Thm.ctyp_of ctxt tp
|
||||
fun inst_type_vars thm = let
|
||||
val (Const ("Pure.all", _) $ Abs (_, tpv, _)) = nth (Thm.prems_of thm) which
|
||||
val ctpv = Thm.ctyp_of ctxt tpv
|
||||
in
|
||||
Thm.instantiate ([(ctpv, ctp)], []) thm
|
||||
Thm.instantiate ([(dest_TVar tpv, ctp)], []) thm
|
||||
end;
|
||||
in
|
||||
map inst_type_vars thms
|
||||
|
@ -780,7 +779,7 @@ fun corres_trim_lvar_nondet_init_tac trace depth ctxt known_guard = let
|
|||
else "ccorres_lift_rhs_remove_lvar_init_unknown_guard")
|
||||
in
|
||||
prim_trace_tac' (#trace_this trace) depth "LVAR_INIT" ctxt
|
||||
((rtac remove_lvar_init)
|
||||
((resolve_tac ctxt [remove_lvar_init])
|
||||
THEN_ALL_NEW (ccorres_norename_cleanup trace depth ctxt)) i
|
||||
end;
|
||||
in
|
||||
|
|
|
@ -226,7 +226,7 @@ proof -
|
|||
have pno': "pspace_no_overlap' frame (objBitsKO ko) \<sigma>"
|
||||
by (simp add:objBits_simps pno ko_def archObjSize_def al)
|
||||
|
||||
have al': "is_aligned frame (objBitsKO (ko\<Colon>kernel_object))"
|
||||
have al': "is_aligned frame (objBitsKO (ko::kernel_object))"
|
||||
by (simp add:objBits_simps ko_def archObjSize_def al)
|
||||
|
||||
(* s/obj/obj'/ *)
|
||||
|
|
|
@ -790,7 +790,7 @@ lemmas cteInsert_if_helper' = cteInsert_if_helper [OF _ forget_Q']
|
|||
*)
|
||||
declare word_neq_0_conv [simp del]
|
||||
|
||||
schematic_lemma ccap_relation_tag_Master:
|
||||
schematic_goal ccap_relation_tag_Master:
|
||||
"\<And>ccap. \<lbrakk> ccap_relation cap ccap \<rbrakk>
|
||||
\<Longrightarrow> cap_get_tag ccap =
|
||||
case_capability ?a ?b ?c ?d ?e ?f ?g
|
||||
|
@ -992,7 +992,7 @@ lemma capBlockSize_CL_maxSize:
|
|||
done
|
||||
|
||||
lemma t2p_shiftr:
|
||||
"\<lbrakk>b\<le> a;a < word_bits \<rbrakk> \<Longrightarrow> (2\<Colon>word32) ^ a >> b = 2 ^ (a - b)"
|
||||
"\<lbrakk>b\<le> a;a < word_bits \<rbrakk> \<Longrightarrow> (2::word32) ^ a >> b = 2 ^ (a - b)"
|
||||
apply (subst shiftr_w2p)
|
||||
apply (simp add:word_bits_def)
|
||||
apply (subst shiftr_w2p[where x = "a - b"])
|
||||
|
|
|
@ -688,7 +688,7 @@ lemma induction_setup_helper:
|
|||
\<Longrightarrow> Q s slot exposed"
|
||||
by auto
|
||||
|
||||
schematic_lemma finaliseSlot_ccorres_induction_helper:
|
||||
schematic_goal finaliseSlot_ccorres_induction_helper:
|
||||
"\<And>s slot exposed. ?P s slot exposed
|
||||
\<Longrightarrow> ccorres (cintr \<currency> (\<lambda>(success, irqopt) (success', irq'). success' = from_bool success \<and> irq_opt_relation irqopt irq'))
|
||||
(liftxf errstate finaliseSlot_ret_C.status_C (\<lambda>v. (success_C v, finaliseSlot_ret_C.irq_C v))
|
||||
|
|
|
@ -27,6 +27,14 @@ lemma word_and_notzeroD:
|
|||
context kernel_m
|
||||
begin
|
||||
|
||||
(* TODO: move *)
|
||||
lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
|
||||
apply (cut_tac m = q and n = c in mod_less_divisor)
|
||||
apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
|
||||
apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
|
||||
apply (simp add: add_mult_distrib2)
|
||||
done
|
||||
|
||||
lemma cready_queues_index_to_C_in_range':
|
||||
assumes prems: "qdom \<le> ucast maxDom" "prio \<le> ucast maxPrio"
|
||||
shows "cready_queues_index_to_C qdom prio < numDomains * numPriorities"
|
||||
|
|
|
@ -2412,7 +2412,7 @@ definition
|
|||
if (x = scast seL4_ARM_PageDirectoryObject) then ArchTypes_H.PageDirectoryObject else
|
||||
undefined)))))))))))"
|
||||
|
||||
theorems Kernel_C_defs =
|
||||
lemmas Kernel_C_defs =
|
||||
seL4_UntypedObject_def
|
||||
seL4_TCBObject_def
|
||||
seL4_EndpointObject_def
|
||||
|
@ -4785,8 +4785,8 @@ end
|
|||
|
||||
definition "placeNewObject_with_memset regionBase us \<equiv>
|
||||
(do x \<leftarrow> placeNewObject regionBase UserData us;
|
||||
doMachineOp (mapM_x (\<lambda>p\<Colon>word32. storeWord p (0\<Colon>word32))
|
||||
[regionBase , regionBase + (4\<Colon>word32) .e. regionBase + (2\<Colon>word32) ^ (pageBits + us) - (1\<Colon>word32)])
|
||||
doMachineOp (mapM_x (\<lambda>p::word32. storeWord p (0::word32))
|
||||
[regionBase , regionBase + (4::word32) .e. regionBase + (2::word32) ^ (pageBits + us) - (1::word32)])
|
||||
od)"
|
||||
|
||||
crunch gsMaxObjectSize[wp]: placeNewObject_with_memset, createObject "\<lambda>s. P (gsMaxObjectSize s)"
|
||||
|
|
|
@ -1841,7 +1841,7 @@ lemma user_word_at_cross_over:
|
|||
apply (simp add: shiftr_over_and_dist mask_def pageBits_def uint_and)
|
||||
apply (insert int_and_leR [where a="uint (p >> 2)" and b=1023], clarsimp)[1]
|
||||
apply (simp add: field_lvalue_def
|
||||
field_lookup_offset_eq[OF trans, OF _ arg_cong[where f=Some, symmetric], OF _ pair_collapse]
|
||||
field_lookup_offset_eq[OF trans, OF _ arg_cong[where f=Some, symmetric], OF _ prod.collapse]
|
||||
word32_shift_by_2 shiftr_shiftl1 is_aligned_andI1)
|
||||
apply (drule_tac x="ucast (p >> 2)" in spec)
|
||||
apply (simp add: byte_to_word_heap_def Let_def ucast_ucast_mask)
|
||||
|
@ -1885,7 +1885,7 @@ lemma user_memory_cross_over:
|
|||
hrs_mem_def)
|
||||
apply (cut_tac p=ptr in unat_mask_2_less_4)
|
||||
apply (subgoal_tac "(ptr && ~~ mask 2) + (ptr && mask 2) = ptr")
|
||||
apply (subgoal_tac "!n x. n < 4 \<longrightarrow> (unat (x\<Colon>word32) = n) = (x = of_nat n)")
|
||||
apply (subgoal_tac "!n x. n < 4 \<longrightarrow> (unat (x::word32) = n) = (x = of_nat n)")
|
||||
apply (auto simp add: eval_nat_numeral unat_eq_0 add.commute
|
||||
elim!: less_SucE)[1]
|
||||
apply (clarsimp simp add: unat32_eq_of_nat word_bits_def)
|
||||
|
|
|
@ -28,7 +28,7 @@ shows
|
|||
lemma of_nat_shiftl:
|
||||
"(of_nat x << n) = (of_nat (x * 2 ^ n) :: ('a::len) word)"
|
||||
proof -
|
||||
have "(of_nat x\<Colon>'a word) << n = of_nat (2 ^ n) * of_nat x"
|
||||
have "(of_nat x::'a word) << n = of_nat (2 ^ n) * of_nat x"
|
||||
using shiftl_t2n by auto
|
||||
thus ?thesis by simp
|
||||
qed
|
||||
|
|
|
@ -57,7 +57,7 @@ declare psubset_singleton[simp]
|
|||
lemma gts_eq:
|
||||
"st_tcb_at' (\<lambda>st. st = state) t s
|
||||
\<Longrightarrow> (getThreadState t s = return state s)"
|
||||
apply (simp add: Pair_fst_snd_eq return_def)
|
||||
apply (simp add: prod_eq_iff return_def)
|
||||
apply (subst conj_commute, rule context_conjI)
|
||||
apply (rule no_failD[OF no_fail_getThreadState])
|
||||
apply (erule pred_tcb_at')
|
||||
|
|
|
@ -1826,7 +1826,7 @@ lemma register_from_H_inj:
|
|||
|
||||
(* FIXME: move *)
|
||||
lemmas register_from_H_eq_iff[simp]
|
||||
= inj_on_iff [OF register_from_H_inj, simplified]
|
||||
= inj_on_eq_iff [OF register_from_H_inj, simplified]
|
||||
|
||||
lemma setRegister_ccorres:
|
||||
"ccorres dc xfdc \<top>
|
||||
|
|
Loading…
Reference in New Issue