mirror of https://github.com/seL4/l4v.git
isabelle2021-1 lib: update Lib session, retire wpx
The benefit of the wpx method is not worth the maintenance effort. There are still a few instances of wpx left in AInvs, which will have to be fixed later. We are keeping the wps method from the same file (WPEx.thy), because that is used more widely and does not break with Isabelle2021-1 Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
Gerwin Klein
parent
7ce3ccb068
commit
0f633ce387
|
|
@ -634,17 +634,18 @@ fun continue i_opt m_opt =
|
|||
|
||||
fun markup_def rng =
|
||||
(Output.report
|
||||
[Markup.markup (Markup.entity "breakpoint" ""
|
||||
|> Markup.properties (Position.entity_properties_of true sr
|
||||
(Position.range_position rng))) ""]);
|
||||
[Markup.markup (
|
||||
Position.make_entity_markup {def=true} sr "breakpoint"
|
||||
("", Position.range_position rng))
|
||||
""]);
|
||||
|
||||
val _ = Option.map markup_def (get_latest_range (fst st''));
|
||||
val _ = Option.map markup_def (get_breakpoint_range (fst st''));
|
||||
|
||||
val _ =
|
||||
(Context_Position.report ctxt (Position.thread_data ())
|
||||
(Markup.entity "breakpoint" ""
|
||||
|> Markup.properties (Position.entity_properties_of false sr Position.none)))
|
||||
(Position.make_entity_markup {def=false} sr "breakpoint"
|
||||
("", Position.none)))
|
||||
|
||||
val _ = maybe_trace (#trace (get_break_opts ctxt)) st'';
|
||||
|
||||
|
|
|
|||
|
|
@ -23,7 +23,6 @@ local
|
|||
(
|
||||
type T = thm;
|
||||
val empty: T = Drule.dummy_thm;
|
||||
val extend = I;
|
||||
val merge : T * T -> T = (K Drule.dummy_thm);
|
||||
);
|
||||
|
||||
|
|
|
|||
|
|
@ -214,7 +214,7 @@ text \<open>
|
|||
\<close>
|
||||
setup \<open>
|
||||
Method.setup \<^binding>\<open>prop_tac\<close>
|
||||
(Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >>
|
||||
(Args.goal_spec -- Scan.lift (Scan.repeat1 Parse.embedded_inner_syntax -- Parse.for_fixes) >>
|
||||
(fn (quant, (props, fixes)) => fn ctxt =>
|
||||
(SIMPLE_METHOD'' quant
|
||||
(EVERY' (map (fn prop => Rule_Insts.subgoal_tac ctxt prop fixes) props)
|
||||
|
|
|
|||
|
|
@ -124,8 +124,6 @@ end
|
|||
|
||||
setup \<open>Add_Locale_Code_Defs.setup "eval_bool_test_locale"\<close>
|
||||
|
||||
setup \<open>Add_Locale_Code_Defs.setup "eval_bool_test_locale"\<close>
|
||||
|
||||
lemma "eval_bool_test_locale.z > 150"
|
||||
by eval_bool
|
||||
|
||||
|
|
|
|||
|
|
@ -66,14 +66,14 @@ fun then_eq_reflection thm = let
|
|||
in Thm.implies_elim rule thm end;
|
||||
|
||||
fun bool_conv_True thm =
|
||||
Thm.instantiate ([], [((("P", 0), @{typ bool}),
|
||||
Thm.dest_arg (Thm.cprop_of thm))])
|
||||
Thm.instantiate (TVars.empty, Vars.make [((("P", 0), @{typ bool}),
|
||||
Thm.dest_arg (Thm.cprop_of thm))])
|
||||
@{thm FP_Eval.bool_prop_eq_True}
|
||||
|> (fn conv => Thm.equal_elim conv thm);
|
||||
|
||||
fun bool_conv_False thm =
|
||||
Thm.instantiate ([], [((("P", 0), @{typ bool}),
|
||||
Thm.dest_arg (Thm.dest_arg (Thm.cprop_of thm)))])
|
||||
Thm.instantiate (TVars.empty, Vars.make [((("P", 0), @{typ bool}),
|
||||
Thm.dest_arg (Thm.dest_arg (Thm.cprop_of thm)))])
|
||||
@{thm FP_Eval.bool_prop_eq_False}
|
||||
|> (fn conv => Thm.equal_elim conv thm);
|
||||
|
||||
|
|
|
|||
|
|
@ -201,11 +201,10 @@ lemma lookup_tree_to_list_of_:
|
|||
(* this big blob just does case distinctions of both subtrees and
|
||||
all possible lookup results within each, then solves *)
|
||||
(* slow 10s *)
|
||||
apply (fastforce simp: apfst_def map_prod_def map_add_def
|
||||
split: prod.splits option.splits if_splits
|
||||
dest: lookup_tree_valid_empty lookup_tree_valid_range lookup_tree_valid_in_range
|
||||
elim: lookup_tree_valid_in_range_None)
|
||||
done
|
||||
by (fastforce simp: apfst_def map_prod_def map_add_def
|
||||
split: prod.splits option.splits if_splits
|
||||
dest: lookup_tree_valid_empty lookup_tree_valid_range lookup_tree_valid_in_range
|
||||
elim: lookup_tree_valid_in_range_None)
|
||||
|
||||
(* Standard form of above *)
|
||||
lemma lookup_tree_to_list_of:
|
||||
|
|
@ -363,22 +362,22 @@ fun conv_at skel conv ctxt ct = let
|
|||
fun mismatch current_skel current_ct =
|
||||
raise TERM ("conv_at mismatch", [current_skel, Thm.term_of current_ct, skel, Thm.term_of ct])
|
||||
|
||||
fun walk (Free ("HERE", _)) ctxt ct = conv ct
|
||||
fun walk (Free ("HERE", _)) _ ct = conv ct
|
||||
| walk (skel as skel_f $ skel_x) ctxt ct =
|
||||
(case Thm.term_of ct of
|
||||
f $ x => Conv.combination_conv (walk skel_f ctxt) (walk skel_x ctxt) ct
|
||||
_ $ _ => Conv.combination_conv (walk skel_f ctxt) (walk skel_x ctxt) ct
|
||||
| _ => mismatch skel ct)
|
||||
| walk (skel as Abs (_, _, skel_body)) ctxt ct =
|
||||
(case Thm.term_of ct of
|
||||
Abs _ => Conv.abs_conv (fn (v, ctxt') => walk skel_body ctxt') ctxt ct
|
||||
Abs _ => Conv.abs_conv (fn (_, ctxt') => walk skel_body ctxt') ctxt ct
|
||||
| _ => mismatch skel ct)
|
||||
(* Also check that Consts match the skeleton pattern *)
|
||||
| walk (skel as Const (skel_name, _)) ctxt ct =
|
||||
| walk (skel as Const (skel_name, _)) _ ct =
|
||||
if (case Thm.term_of ct of Const (name, _) => name = skel_name | _ => false)
|
||||
then Thm.reflexive ct
|
||||
else mismatch skel ct
|
||||
(* Default case *)
|
||||
| walk _ ctxt ct = Thm.reflexive ct
|
||||
| walk _ _ ct = Thm.reflexive ct
|
||||
in walk skel ctxt ct end
|
||||
|
||||
fun gconv_at_tac pat conv ctxt = Conv.gconv_rule (conv_at pat conv ctxt) 1 #> Seq.succeed
|
||||
|
|
|
|||
|
|
@ -314,7 +314,7 @@ lemma card_of_dom_bounded:
|
|||
by (simp add: assms card_mono)
|
||||
|
||||
lemma third_in: "(a, b, c) \<in> S \<Longrightarrow> c \<in> (snd \<circ> snd) ` S"
|
||||
by (metis (erased, hide_lams) map_set_in image_comp snd_conv)
|
||||
by (metis (erased, opaque_lifting) map_set_in image_comp snd_conv)
|
||||
|
||||
lemma third_in2: "(a \<in> (snd \<circ> snd) ` (set (enumerate i xs))) = (a \<in> snd ` (set xs))"
|
||||
by (metis map_map map_snd_enumerate set_map)
|
||||
|
|
@ -357,7 +357,7 @@ lemma distinct_map_via_ran: "distinct (map fst xs) \<Longrightarrow> ran (map_of
|
|||
by (simp add: ran_distinct)
|
||||
|
||||
lemma in_ran_in_set: "x \<in> ran (map_of xs) \<Longrightarrow> x \<in> set (map snd xs)"
|
||||
by (metis (mono_tags, hide_lams) map_set_in map_of_SomeD ranE set_map snd_conv)
|
||||
by (metis (mono_tags) map_set_in map_of_SomeD ranE set_map snd_conv)
|
||||
|
||||
lemma in_ran_map_app: "x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs"
|
||||
proof -
|
||||
|
|
|
|||
23
lib/Lib.thy
23
lib/Lib.thy
|
|
@ -2413,9 +2413,7 @@ lemma insert_subtract_new:
|
|||
"x \<notin> S \<Longrightarrow> (insert x S - S) = {x}"
|
||||
by auto
|
||||
|
||||
lemma zip_is_empty:
|
||||
"(zip xs ys = []) = (xs = [] \<or> ys = [])"
|
||||
by (cases xs; simp) (cases ys; simp)
|
||||
lemmas zip_is_empty = zip_eq_Nil_iff
|
||||
|
||||
lemma minus_Suc_0_lt:
|
||||
"a \<noteq> 0 \<Longrightarrow> a - Suc 0 < a"
|
||||
|
|
@ -2426,14 +2424,9 @@ lemma fst_last_zip_upt:
|
|||
fst (last (zip [0 ..< m] xs)) = (if length xs < m then length xs - 1 else m - 1)"
|
||||
apply (subst last_conv_nth, assumption)
|
||||
apply (simp only: One_nat_def)
|
||||
apply (subst nth_zip)
|
||||
apply (rule order_less_le_trans[OF minus_Suc_0_lt])
|
||||
apply (simp add: zip_is_empty)
|
||||
apply simp
|
||||
apply (rule order_less_le_trans[OF minus_Suc_0_lt])
|
||||
apply (simp add: zip_is_empty)
|
||||
apply simp
|
||||
apply (simp add: min_def zip_is_empty)
|
||||
apply (subst nth_zip; simp)
|
||||
apply (rule order_less_le_trans[OF minus_Suc_0_lt]; simp)
|
||||
apply (rule order_less_le_trans[OF minus_Suc_0_lt]; simp)
|
||||
done
|
||||
|
||||
lemma neq_into_nprefix:
|
||||
|
|
@ -2582,7 +2575,7 @@ lemma nat_int_mul:
|
|||
lemma int_shiftl_less_cancel:
|
||||
"n \<le> m \<Longrightarrow> ((x :: int) << n < y << m) = (x < y << (m - n))"
|
||||
apply (drule le_Suc_ex)
|
||||
apply (clarsimp simp: shiftl_int_def power_add)
|
||||
apply (clarsimp simp: shiftl_def shiftl_int_def power_add)
|
||||
done
|
||||
|
||||
lemma int_shiftl_lt_2p_bits:
|
||||
|
|
@ -2591,11 +2584,7 @@ lemma int_shiftl_lt_2p_bits:
|
|||
by (metis bit_take_bit_iff not_less take_bit_int_eq_self_iff)
|
||||
\<comment> \<open>TODO: The converse should be true as well, but seems hard to prove.\<close>
|
||||
|
||||
lemma int_eq_test_bit:
|
||||
"((x :: int) = y) = (\<forall>i. test_bit x i = test_bit y i)"
|
||||
apply simp
|
||||
apply (metis bin_eqI)
|
||||
done
|
||||
lemmas int_eq_test_bit = bin_eq_iff
|
||||
lemmas int_eq_test_bitI = int_eq_test_bit[THEN iffD2, rule_format]
|
||||
|
||||
lemma le_nat_shrink_left:
|
||||
|
|
|
|||
|
|
@ -86,7 +86,6 @@ structure WPCPredicateAndFinals = Theory_Data
|
|||
(struct
|
||||
type T = (cterm * thm) list
|
||||
val empty = []
|
||||
val extend = I
|
||||
fun merge (xs, ys) =
|
||||
(* Order of predicates is important, so we can't reorder *)
|
||||
let val tms = map (Thm.term_of o fst) xs
|
||||
|
|
@ -119,11 +118,11 @@ let
|
|||
val thm_pred_tvar = Term.dest_TVar (get_pred_tvar thm_pred);
|
||||
val pred_tvar = Thm.ctyp_of ctxt (get_pred_tvar pred);
|
||||
|
||||
val thm2 = Thm.instantiate ([(thm_pred_tvar, pred_tvar)], []) thm;
|
||||
val thm2 = Thm.instantiate (TVars.make [(thm_pred_tvar, pred_tvar)], Vars.empty) thm;
|
||||
|
||||
val thm2_pred = Term.dest_Var (get_concl_pred thm2);
|
||||
in
|
||||
Thm.instantiate ([], [(thm2_pred, pred)]) thm2
|
||||
Thm.instantiate (TVars.empty, Vars.make [(thm2_pred, pred)]) thm2
|
||||
end;
|
||||
|
||||
fun detect_term ctxt n thm tm =
|
||||
|
|
|
|||
|
|
@ -10,25 +10,15 @@ imports
|
|||
Strengthen
|
||||
begin
|
||||
|
||||
(* Only the wps method and wps_tac are left of this experiment: *)
|
||||
text \<open>WPEx - the WP Extension Experiment\<close>
|
||||
|
||||
definition
|
||||
mresults :: "('s, 'a) nondet_monad \<Rightarrow> ('a \<times> 's \<times> 's) set"
|
||||
where
|
||||
definition mresults :: "('s, 'a) nondet_monad \<Rightarrow> ('a \<times> 's \<times> 's) set" where
|
||||
"mresults f = {(rv, s', s). (rv, s') \<in> fst (f s)}"
|
||||
|
||||
definition
|
||||
assert_value_exported :: "'x \<times> 's \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('x \<Rightarrow> ('s, 'a) nondet_monad)"
|
||||
where
|
||||
"assert_value_exported x f y \<equiv>
|
||||
do s \<leftarrow> get; if x = (y, s) then f else fail od"
|
||||
|
||||
syntax
|
||||
"_assert_bind" :: "['a, 'b] => dobind" ("_ =<= _")
|
||||
|
||||
translations
|
||||
"do v =<= a; e od" == "a >>= CONST assert_value_exported v e"
|
||||
"doE v =<= a; e odE" == "a >>=E CONST assert_value_exported v e"
|
||||
definition assert_value_exported ::
|
||||
"'x \<times> 's \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('x \<Rightarrow> ('s, 'a) nondet_monad)" where
|
||||
"assert_value_exported x f y \<equiv> do s \<leftarrow> get; if x = (y, s) then f else fail od"
|
||||
|
||||
lemma in_mresults_export:
|
||||
"(rv, s', s) \<in> mresults (assert_value_exported (rv', s'') f rv'')
|
||||
|
|
@ -38,189 +28,32 @@ lemma in_mresults_export:
|
|||
lemma in_mresults_bind:
|
||||
"(rv, s', s) \<in> mresults (a >>= b)
|
||||
= (\<exists>rv' s''. (rv, s', s'') \<in> mresults (b rv') \<and> (rv', s'', s) \<in> mresults a)"
|
||||
apply (simp add: mresults_def bind_def)
|
||||
apply (auto elim: rev_bexI)
|
||||
done
|
||||
by (auto simp: mresults_def bind_def elim: rev_bexI)
|
||||
|
||||
lemma mresults_export_bindD:
|
||||
"(rv, s', s) \<in> mresults (a >>= assert_value_exported (rv', s'') b)
|
||||
\<Longrightarrow> (rv, s', s'') \<in> mresults b"
|
||||
"(rv, s', s) \<in> mresults (a >>= assert_value_exported (rv', s'') b)
|
||||
\<Longrightarrow> (rv', s'', s) \<in> mresults a"
|
||||
"(rv, s', s) \<in> mresults (a >>= assert_value_exported (rv', s'') b) \<Longrightarrow> (rv, s', s'') \<in> mresults b"
|
||||
"(rv, s', s) \<in> mresults (a >>= assert_value_exported (rv', s'') b) \<Longrightarrow> (rv', s'', s) \<in> mresults a"
|
||||
by (simp_all add: in_mresults_export in_mresults_bind)
|
||||
|
||||
definition "wpex_name_for_id = id"
|
||||
|
||||
definition "wpex_name_for_id_prop p \<equiv> (p :: prop)"
|
||||
|
||||
lemma wpex_name_for_id_propI:
|
||||
"PROP p \<Longrightarrow> PROP wpex_name_for_id_prop p"
|
||||
by (simp add: wpex_name_for_id_prop_def)
|
||||
|
||||
lemma wpex_name_for_id_propE:
|
||||
"PROP wpex_name_for_id_prop p \<Longrightarrow> PROP p"
|
||||
by (simp add: wpex_name_for_id_prop_def)
|
||||
|
||||
lemma del_asm_rule:
|
||||
"\<lbrakk> PROP P; PROP Q \<rbrakk> \<Longrightarrow> PROP Q"
|
||||
by assumption
|
||||
|
||||
ML \<open>
|
||||
|
||||
val p_prop_var = Term.dest_Var (Logic.varify_global @{term "P :: prop"});
|
||||
|
||||
fun del_asm_tac asm =
|
||||
eresolve0_tac [(Thm.instantiate ([], [(p_prop_var, asm)]) @{thm del_asm_rule})];
|
||||
|
||||
fun subgoal_asm_as_thm tac =
|
||||
Subgoal.FOCUS_PARAMS (fn focus => SUBGOAL (fn (t, _) => let
|
||||
val asms = Logic.strip_assums_hyp t;
|
||||
val ctxt = #context focus;
|
||||
fun asm_tac asm = (Subgoal.FOCUS_PREMS (fn focus => let
|
||||
fun is_asm asm' = asm aconv (Thm.concl_of asm');
|
||||
val (asm' :: _) = filter is_asm (#prems focus);
|
||||
in tac asm' end) (#context focus)
|
||||
THEN_ALL_NEW del_asm_tac (Thm.cterm_of ctxt asm)) 1;
|
||||
in
|
||||
FIRST (map asm_tac asms)
|
||||
end) 1);
|
||||
|
||||
exception SAME;
|
||||
|
||||
fun eta_flat (Abs (name, tp, (Abs a)))
|
||||
= eta_flat (Abs (name, tp, eta_flat (Abs a)))
|
||||
| eta_flat (Abs (_, _, t $ Bound 0))
|
||||
= if member (=) (loose_bnos t) 0 then raise SAME
|
||||
else subst_bound (Bound 0, t)
|
||||
| eta_flat (Abs (name, tp, t $ Abs a))
|
||||
= eta_flat (Abs (name, tp, t $ eta_flat (Abs a)))
|
||||
| eta_flat _ = raise SAME;
|
||||
|
||||
fun const_spine t = case strip_comb t of
|
||||
(Const c, xs) => SOME (c, xs)
|
||||
| (Abs v, []) => (const_spine (eta_flat (Abs v)) handle SAME => NONE)
|
||||
| (Abs _, (_ :: _)) => error "const_spine: term not beta expanded"
|
||||
| _ => NONE;
|
||||
|
||||
fun build_annotate' t wr ps = case (const_spine t, wr) of
|
||||
(SOME (bd as ("NonDetMonad.bind", _), [a, b]),
|
||||
"WPEx.mresults") => let
|
||||
val (a', ps') = build_annotate' a "WPEx.mresults" ps;
|
||||
in case const_spine b of
|
||||
SOME (ass as ("WPEx.assert_value_exported", _), [rvs, c])
|
||||
=> let
|
||||
val (c', ps'') = build_annotate' c "WPEx.mresults" ps'
|
||||
in (Const bd $ a' $ (Const ass $ rvs $ c'), ps'') end
|
||||
| _ => let
|
||||
val tp = fastype_of (Const bd);
|
||||
val btp = domain_type (range_type tp);
|
||||
val rtp = domain_type btp;
|
||||
val stp = domain_type (range_type btp);
|
||||
val mtp = range_type (range_type btp);
|
||||
val ass = Const ("WPEx.assert_value_exported",
|
||||
HOLogic.mk_prodT (rtp, stp) -->
|
||||
(stp --> mtp) --> rtp --> stp --> mtp);
|
||||
val rv = Bound (length ps');
|
||||
val s = Bound (length ps' + 1);
|
||||
val rvs = HOLogic.pair_const rtp stp $ rv $ s;
|
||||
val b' = betapply (b, Bound (length ps'));
|
||||
val borings = ["x", "y", "rv"];
|
||||
val rvnms = case b of
|
||||
Abs (rvnm, _, _) =>
|
||||
if member (=) borings rvnm then []
|
||||
else [(rvnm, rvnm ^ "_st")]
|
||||
| _ => [];
|
||||
val cnms = case const_spine a' of
|
||||
SOME ((cnm, _), _) => let
|
||||
val cnm' = List.last (space_explode "." cnm);
|
||||
in [(cnm' ^ "_rv", cnm' ^ "_st")] end
|
||||
| _ => [];
|
||||
val nms = hd (rvnms @ cnms @ [("rv", "s")]);
|
||||
val ps'' = ps' @ [(fst nms, rtp), (snd nms, stp)];
|
||||
val (b'', ps''') = build_annotate' b' "WPEx.mresults" ps'';
|
||||
in (Const bd $ a' $ (ass $ rvs $ b''), ps''') end
|
||||
end
|
||||
| _ => (t, ps);
|
||||
|
||||
fun build_annotate asm =
|
||||
case const_spine (HOLogic.dest_Trueprop (Envir.beta_norm asm)) of
|
||||
SOME (memb as ("Set.member", _), [x, st]) => (case const_spine st of
|
||||
SOME (mres as ("WPEx.mresults", _), [m]) => let
|
||||
val (m', ps) = build_annotate' m "WPEx.mresults" [];
|
||||
val _ = if null ps then raise SAME else ();
|
||||
val t = Const memb $ x $ (Const mres $ m');
|
||||
fun mk_exists ((s, tp), tm) = HOLogic.exists_const tp $ Abs (s, tp, tm);
|
||||
in HOLogic.mk_Trueprop (Library.foldr mk_exists (rev ps, t)) end
|
||||
| _ => raise SAME) | _ => raise SAME;
|
||||
|
||||
|
||||
val put_Lib_simpset = put_simpset (Simplifier.simpset_of (Proof_Context.init_global @{theory Lib}))
|
||||
|
||||
|
||||
fun in_mresults_ctxt ctxt = ctxt
|
||||
|> put_Lib_simpset
|
||||
|> (fn ctxt => ctxt addsimps [@{thm in_mresults_export}, @{thm in_mresults_bind}])
|
||||
|> Splitter.del_split @{thm if_split}
|
||||
|
||||
fun prove_qad ctxt term tac = Goal.prove ctxt [] [] term
|
||||
(K (if Config.get ctxt quick_and_dirty andalso false
|
||||
then ALLGOALS (Skip_Proof.cheat_tac ctxt)
|
||||
else tac));
|
||||
|
||||
fun preannotate_ss ctxt = ctxt
|
||||
|> put_simpset HOL_basic_ss
|
||||
|> (fn ctxt => ctxt addsimps [@{thm K_bind_def}])
|
||||
|> simpset_of
|
||||
|
||||
fun in_mresults_ss ctxt = ctxt
|
||||
|> put_Lib_simpset
|
||||
|> (fn ctxt => ctxt addsimps [@{thm in_mresults_export}, @{thm in_mresults_bind}])
|
||||
|> Splitter.del_split @{thm if_split}
|
||||
|> simpset_of
|
||||
|
||||
|
||||
val in_mresults_cs = Classical.claset_of (Proof_Context.init_global @{theory Lib});
|
||||
|
||||
fun annotate_tac ctxt asm = let
|
||||
val asm' = simplify (put_simpset (preannotate_ss ctxt) ctxt) asm;
|
||||
val annotated = build_annotate (Thm.concl_of asm');
|
||||
val ctxt' = Classical.put_claset in_mresults_cs (put_simpset (in_mresults_ss ctxt) ctxt)
|
||||
val thm = prove_qad ctxt (Logic.mk_implies (Thm.concl_of asm', annotated))
|
||||
(auto_tac ctxt'
|
||||
THEN ALLGOALS (TRY o blast_tac ctxt'));
|
||||
in
|
||||
cut_facts_tac [asm' RS thm] 1
|
||||
end
|
||||
handle SAME => no_tac;
|
||||
|
||||
fun annotate_goal_tac ctxt
|
||||
= REPEAT_DETERM1 (subgoal_asm_as_thm (annotate_tac ctxt) ctxt 1
|
||||
ORELSE (eresolve_tac ctxt [exE] 1));
|
||||
|
||||
val annotate_method =
|
||||
Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (annotate_goal_tac ctxt))
|
||||
: (Proof.context -> Method.method) context_parser;
|
||||
|
||||
\<close>
|
||||
|
||||
method_setup annotate = \<open>annotate_method\<close> "tries to annotate"
|
||||
definition wpex_name_for_id :: "'a \<Rightarrow> 'a" where
|
||||
"wpex_name_for_id = id"
|
||||
|
||||
lemma use_valid_mresults:
|
||||
"\<lbrakk> (rv, s', s) \<in> mresults f; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> P s \<longrightarrow> Q rv s'"
|
||||
by (auto simp: mresults_def valid_def)
|
||||
|
||||
lemma mresults_validI:
|
||||
"\<lbrakk> \<And>rv s' s. (rv, s', s) \<in> mresults f \<Longrightarrow> P s \<longrightarrow> Q rv s' \<rbrakk>
|
||||
\<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
|
||||
by (auto simp: mresults_def valid_def)
|
||||
lemma valid_strengthen_with_mresults:
|
||||
"\<lbrakk> \<And>s rv s'. \<lbrakk> (rv, s', s) \<in> mresults f; wpex_name_for_id (Q' s rv s') \<rbrakk> \<Longrightarrow> Q rv s';
|
||||
\<And>prev_s. \<lbrace>P prev_s\<rbrace> f \<lbrace>Q' prev_s\<rbrace> \<rbrakk>
|
||||
\<Longrightarrow> \<lbrace>\<lambda>s. P s s\<rbrace> f \<lbrace>Q\<rbrace>"
|
||||
by (clarsimp simp: valid_def mresults_def wpex_name_for_id_def) blast
|
||||
|
||||
lemma wpex_name_for_idE: "wpex_name_for_id P \<Longrightarrow> P"
|
||||
by (simp add: wpex_name_for_id_def)
|
||||
|
||||
ML \<open>
|
||||
|
||||
val use_valid_mresults = @{thm use_valid_mresults};
|
||||
|
||||
val mresults_export_bindD = @{thms mresults_export_bindD};
|
||||
|
||||
fun dest_mresults_tac t = Seq.of_list ([t] RL mresults_export_bindD);
|
||||
fun dest_mresults_tac t = Seq.of_list ([t] RL @{thms mresults_export_bindD});
|
||||
|
||||
(* take a rule of conclusion p --> q and decide whether to use it
|
||||
as an introduction rule or if of form ?P x --> ?P y to use it
|
||||
|
|
@ -238,7 +71,7 @@ fun get_rule_uses ctxt rule = let
|
|||
$ Bound (length argtps - n) $ x;
|
||||
val v' = fold_rev Term.abs (map (pair "x") argtps) eq;
|
||||
in rule
|
||||
|> Thm.instantiate ([], [(Term.dest_Var v, ct v')])
|
||||
|> Thm.instantiate (TVars.empty, Vars.make [(Term.dest_Var v, ct v')])
|
||||
|> simplify (put_simpset HOL_ss ctxt)
|
||||
end;
|
||||
in case (strip_comb p, strip_comb q) of
|
||||
|
|
@ -254,21 +87,12 @@ fun get_wp_simps_strgs ctxt rules asms = let
|
|||
val wp_rules = rules @ (WeakestPre.debug_get ctxt |> #rules |> WeakestPre.dest_rules);
|
||||
val wp_rules' = filter (null o Thm.prems_of) wp_rules;
|
||||
val asms' = maps (Seq.list_of o REPEAT dest_mresults_tac) asms;
|
||||
val uses = asms' RL [use_valid_mresults];
|
||||
val uses = asms' RL [@{thm use_valid_mresults}];
|
||||
val wp_rules'' = wp_rules' RL uses;
|
||||
in
|
||||
apply2 flat (map_split (get_rule_uses ctxt) wp_rules'')
|
||||
end;
|
||||
|
||||
fun tac_with_wp_simps_strgs ctxt rules tac =
|
||||
subgoal_asm_as_thm (fn asm => let
|
||||
val (simps, strgs) = get_wp_simps_strgs ctxt rules [asm]
|
||||
in
|
||||
cut_facts_tac [asm] 1 THEN tac (simps, strgs)
|
||||
end) ctxt;
|
||||
|
||||
val mresults_validI = @{thm mresults_validI};
|
||||
|
||||
fun postcond_ss ctxt = ctxt
|
||||
|> put_simpset HOL_basic_ss
|
||||
|> (fn ctxt => ctxt addsimps [@{thm pred_conj_def}])
|
||||
|
|
@ -279,82 +103,18 @@ fun wp_default_ss ctxt = ctxt
|
|||
|> Splitter.del_split @{thm if_split}
|
||||
|> simpset_of
|
||||
|
||||
fun raise_tac s = all_tac THEN (fn _ => error s);
|
||||
|
||||
fun wpx_tac ctxt rules
|
||||
= TRY (resolve_tac ctxt [mresults_validI] 1)
|
||||
THEN (full_simp_tac (put_simpset (postcond_ss ctxt) ctxt) 1)
|
||||
THEN TRY (annotate_goal_tac ctxt)
|
||||
THEN tac_with_wp_simps_strgs ctxt rules (fn (simps, strgs) =>
|
||||
REPEAT_DETERM1
|
||||
(CHANGED (full_simp_tac (put_simpset (wp_default_ss ctxt) ctxt addsimps simps) 1)
|
||||
ORELSE Strengthen.default_strengthen ctxt strgs 1)
|
||||
) 1;
|
||||
|
||||
val wpx_method = Attrib.thms >> curry (fn (ts, ctxt) =>
|
||||
Method.SIMPLE_METHOD (wpx_tac ctxt ts));
|
||||
|
||||
\<close>
|
||||
|
||||
method_setup wpx = \<open>wpx_method\<close> "experimental wp method"
|
||||
|
||||
lemma foo:
|
||||
"(rv, s', s) \<in> mresults (do x \<leftarrow> get; y \<leftarrow> get; put (x + y :: nat); return () od)
|
||||
\<Longrightarrow> s' = s + s"
|
||||
apply annotate
|
||||
apply wpx
|
||||
done
|
||||
|
||||
lemma foo2:
|
||||
"(rv, s', s) \<in> mresults (do x \<leftarrow> get; y \<leftarrow> get; put (if z = Suc 0 then x + y else x + y + z); return () od)
|
||||
\<Longrightarrow> s' = s + s + (if z = Suc 0 then 0 else z)"
|
||||
apply wpx
|
||||
apply simp
|
||||
done
|
||||
|
||||
text \<open>Have played around with it, the issues are:
|
||||
1: Need to deal with non-linear code, known issue.
|
||||
2: Using fastforce in annotate isn't cutting the mustard, need to automate better.
|
||||
Probably half the issue is that there are too many simp rules available.
|
||||
3: Related to (2), there's the question of whether you can simplify code enough
|
||||
once it's been annotated. This may re-raise the specter of annotation on demand.
|
||||
4: It's hard to tell whether it's worked or not.
|
||||
5: Structural rules don't really work - rules that want to transform the whole
|
||||
postcondition once we get up to a particular point. Related to 4, it's hard to
|
||||
say where that point is hit.
|
||||
6: Performance problems with getting the set of available rules.
|
||||
\<close>
|
||||
|
||||
lemma valid_strengthen_with_mresults:
|
||||
"\<lbrakk> \<And>s rv s'. \<lbrakk> (rv, s', s) \<in> mresults f;
|
||||
wpex_name_for_id (Q' s rv s') \<rbrakk> \<Longrightarrow> Q rv s';
|
||||
\<And>prev_s. \<lbrace>P prev_s\<rbrace> f \<lbrace>Q' prev_s\<rbrace> \<rbrakk>
|
||||
\<Longrightarrow> \<lbrace>\<lambda>s. P s s\<rbrace> f \<lbrace>Q\<rbrace>"
|
||||
apply atomize
|
||||
apply (clarsimp simp: valid_def mresults_def wpex_name_for_id_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma wpex_name_for_idE: "wpex_name_for_id P \<Longrightarrow> P"
|
||||
by (simp add: wpex_name_for_id_def)
|
||||
|
||||
ML \<open>
|
||||
|
||||
val valid_strengthen_with_mresults = @{thm valid_strengthen_with_mresults};
|
||||
val wpex_name_for_idE = @{thm wpex_name_for_idE};
|
||||
|
||||
fun wps_tac ctxt rules =
|
||||
let
|
||||
(* avoid duplicate simp rule etc warnings: *)
|
||||
val ctxt = Context_Position.set_visible false ctxt
|
||||
in
|
||||
resolve_tac ctxt [valid_strengthen_with_mresults]
|
||||
resolve_tac ctxt [@{thm valid_strengthen_with_mresults}]
|
||||
THEN' (safe_simp_tac (put_simpset (postcond_ss ctxt) ctxt))
|
||||
THEN' Subgoal.FOCUS (fn focus => let
|
||||
val ctxt = #context focus;
|
||||
val (simps, _) = get_wp_simps_strgs ctxt rules (#prems focus);
|
||||
in CHANGED (simp_tac (put_simpset (wp_default_ss ctxt) ctxt addsimps simps) 1) end) ctxt
|
||||
THEN' eresolve_tac ctxt [wpex_name_for_idE]
|
||||
THEN' eresolve_tac ctxt [@{thm wpex_name_for_idE}]
|
||||
end
|
||||
|
||||
val wps_method = Attrib.thms >> curry
|
||||
|
|
@ -364,11 +124,15 @@ val wps_method = Attrib.thms >> curry
|
|||
|
||||
method_setup wps = \<open>wps_method\<close> "experimental wp simp method"
|
||||
|
||||
lemma foo3:
|
||||
"\<lbrace>P\<rbrace> do v \<leftarrow> return (Suc 0); return (Suc (Suc 0)) od \<lbrace>(=)\<rbrace>"
|
||||
experiment
|
||||
begin
|
||||
|
||||
lemma "\<lbrace>P\<rbrace> do v \<leftarrow> return (Suc 0); return (Suc (Suc 0)) od \<lbrace>(=)\<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
apply (rule hoare_seq_ext)+
|
||||
apply (wps | rule hoare_vcg_prop)+
|
||||
oops
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -254,7 +254,7 @@ ML \<open>
|
|||
val frees = Term.add_frees t [];
|
||||
val frees' = Term.add_frees t' [];
|
||||
in
|
||||
exists (member (=) frees') frees
|
||||
exists (member (op =) frees') frees
|
||||
end
|
||||
\<close>
|
||||
|
||||
|
|
@ -511,7 +511,7 @@ end
|
|||
|
||||
|
||||
notepad begin
|
||||
fix f and Q P P' :: "int \<Rightarrow> 'a \<Rightarrow> bool" and Q' :: "'a \<Rightarrow> bool" and a
|
||||
fix f :: "'a \<Rightarrow> ('a,'b) nondet_monad" and Q P P' :: "int \<Rightarrow> 'a \<Rightarrow> bool" and Q' :: "'a \<Rightarrow> bool" and a :: 'a
|
||||
|
||||
{
|
||||
assume P[wp]: "\<And>PP x. \<lbrace>\<lambda>s. PP (P x s)\<rbrace> f a \<lbrace>\<lambda>r s. PP (P x s)\<rbrace>"
|
||||
|
|
|
|||
|
|
@ -76,8 +76,10 @@ in
|
|||
end
|
||||
|
||||
(* Setup the tool, stealing the "auto_solve_direct" option. *)
|
||||
val _ = Try.tool_setup ("unused_meta_forall",
|
||||
(1, @{system_option auto_solve_direct}, detect_unused_meta_forall))
|
||||
val _ = Try.tool_setup { name = "unused_meta_forall",
|
||||
weight = 1,
|
||||
auto_option = \<^system_option>\<open>auto_solve_direct\<close>,
|
||||
body = detect_unused_meta_forall }
|
||||
\<close>
|
||||
|
||||
lemma test_unused_meta_forall: "\<And>x. y \<or> \<not> y"
|
||||
|
|
|
|||
|
|
@ -11,11 +11,6 @@ imports
|
|||
Lib
|
||||
begin
|
||||
|
||||
instantiation nat :: semiring_bit_syntax
|
||||
begin
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation nat :: lsb
|
||||
begin
|
||||
|
||||
|
|
@ -45,34 +40,33 @@ definition
|
|||
|
||||
instance
|
||||
by intro_classes
|
||||
(simp add: set_bit_nat_def bit_nat_iff set_bit_int_def bin_nth_sc_gen bin_sc_pos
|
||||
bit_of_nat_iff_bit)
|
||||
|
||||
(metis (mono_tags) set_bit_nat_def bin_nth_sc_gen bin_sc_pos
|
||||
bit_nat_iff exp_eq_0_imp_not_bit int_eq_iff)
|
||||
end
|
||||
|
||||
|
||||
lemma nat_2p_eq_shiftl:
|
||||
"(2::nat)^x = 1 << x"
|
||||
by (simp add: shiftl_eq_push_bit)
|
||||
by simp
|
||||
|
||||
lemma shiftl_nat_alt_def:
|
||||
"(x::nat) << n = x * 2^n"
|
||||
by (simp add: push_bit_nat_def shiftl_eq_push_bit)
|
||||
by (simp add: push_bit_nat_def shiftl_def)
|
||||
|
||||
lemma shiftl_nat_def:
|
||||
"(x::nat) << y = nat (int x << y)"
|
||||
by (simp add: nat_int_mul shiftl_int_def shiftl_nat_alt_def)
|
||||
by (simp add: nat_int_mul push_bit_eq_mult shiftl_def)
|
||||
|
||||
lemma nat_shiftl_less_cancel:
|
||||
"n \<le> m \<Longrightarrow> ((x :: nat) << n < y << m) = (x < y << (m - n))"
|
||||
by (simp add: nat_int_comparison(2) shiftl_nat_def int_shiftl_less_cancel)
|
||||
apply (simp add: nat_int_comparison(2) shiftl_nat_def shiftl_def)
|
||||
by (metis int_shiftl_less_cancel shiftl_def)
|
||||
|
||||
|
||||
lemma nat_shiftl_lt_2p_bits:
|
||||
"(x::nat) < 1 << n \<Longrightarrow> \<forall>i \<ge> n. \<not> x !! i"
|
||||
apply (clarsimp simp: shiftl_nat_def zless_nat_eq_int_zless shiftl_eq_push_bit push_bit_of_1
|
||||
apply (clarsimp simp: shiftl_nat_def zless_nat_eq_int_zless
|
||||
dest!: le_Suc_ex)
|
||||
by (metis bit_take_bit_iff not_add_less1 take_bit_nat_eq_self_iff test_bit_eq_bit)
|
||||
by (metis bit_take_bit_iff not_add_less1 take_bit_nat_eq_self_iff)
|
||||
|
||||
lemmas nat_eq_test_bit = bit_eq_iff
|
||||
lemmas nat_eq_test_bitI = bit_eq_iff[THEN iffD2, rule_format]
|
||||
|
|
|
|||
|
|
@ -1003,13 +1003,13 @@ lemma zipWithM_If_cut:
|
|||
apply (cases "n < m")
|
||||
apply (cut_tac i=0 and j=n and k="m - n" in upt_add_eq_append)
|
||||
apply simp
|
||||
apply (simp add: min.absorb1 zipWithM_mapM)
|
||||
apply (simp add: zipWithM_mapM)
|
||||
apply (simp add: zip_append1 mapM_append zip_take_triv2 split_def)
|
||||
apply (intro bind_cong bind_apply_cong refl mapM_length_cong
|
||||
fun_cong[OF mapM_length_cong])
|
||||
apply (clarsimp simp: set_zip)
|
||||
apply (clarsimp simp: set_zip)
|
||||
apply (simp add: min.absorb2 zipWithM_mapM mapM_Nil)
|
||||
apply (simp add: zipWithM_mapM mapM_Nil)
|
||||
apply (intro mapM_length_cong refl)
|
||||
apply (clarsimp simp: set_zip)
|
||||
done
|
||||
|
|
@ -3028,12 +3028,12 @@ proof -
|
|||
apply (intro conjI)
|
||||
apply (rule set_eqI)
|
||||
apply (rule iffI)
|
||||
apply (clarsimp simp:Union_eq dest!: singletonD)
|
||||
apply (clarsimp simp:Union_eq)
|
||||
apply (frule fsame)
|
||||
apply clarsimp
|
||||
apply (frule gsame)
|
||||
apply (metis fst_conv snd_conv)
|
||||
apply (clarsimp simp:Union_eq dest!: singletonD)
|
||||
apply (clarsimp simp:Union_eq)
|
||||
apply (frule gsame)
|
||||
apply clarsimp
|
||||
apply (frule fsame)
|
||||
|
|
|
|||
|
|
@ -128,13 +128,13 @@ ML \<open>
|
|||
structure Partial_Prove = struct
|
||||
|
||||
fun inst_frees_tac _ Ps ct = REPEAT_DETERM o SUBGOAL (fn (t, _) =>
|
||||
fn thm => case Term.add_frees t [] |> filter (member (=) Ps)
|
||||
fn thm => case Term.add_frees t [] |> filter (member (op =) Ps)
|
||||
of [] => Seq.empty
|
||||
| (f :: _) => let
|
||||
val idx = Thm.maxidx_of thm + 1
|
||||
val var = ((fst f, idx), snd f)
|
||||
in thm |> Thm.generalize ([], [fst f]) idx
|
||||
|> Thm.instantiate ([], [(var, ct)])
|
||||
in thm |> Thm.generalize (Names.empty, Names.make_set [fst f]) idx
|
||||
|> Thm.instantiate (TVars.empty, Vars.make [(var, ct)])
|
||||
|> Seq.single
|
||||
end)
|
||||
|
||||
|
|
@ -172,7 +172,7 @@ fun partial_prove tactic ctxt i
|
|||
|
||||
fun method (ctxtg, []) = (fn ctxt => Method.SIMPLE_METHOD (test_start_partial_prove ctxt 1),
|
||||
(ctxtg, []))
|
||||
| method args = error "Partial_Prove: still working on that"
|
||||
| method _ = error "Partial_Prove: still working on that"
|
||||
|
||||
fun fin_method () = Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (test_end_partial_prove ctxt))
|
||||
|
||||
|
|
|
|||
|
|
@ -25,7 +25,6 @@ structure Data = Theory_Data
|
|||
(
|
||||
type T = (theory * qualify_args) option;
|
||||
val empty = NONE;
|
||||
val extend = I;
|
||||
fun merge ((_, _) : T * T) = NONE;
|
||||
);
|
||||
|
||||
|
|
|
|||
1
lib/ROOT
1
lib/ROOT
|
|
@ -97,7 +97,6 @@ session Lib (lib) = Word_Lib +
|
|||
"Monad_WP/wp/Eisbach_WP"
|
||||
"Monad_WP/wp/WPI"
|
||||
"Monad_WP/wp/WPC"
|
||||
"Monad_WP/wp/WPEx"
|
||||
"Monad_WP/wp/WP_Pre"
|
||||
"Monad_WP/wp/WP"
|
||||
"Monad_WP/Datatype_Schematic"
|
||||
|
|
|
|||
|
|
@ -442,7 +442,7 @@ proof (induct tree)
|
|||
([((start, end), v)]
|
||||
@ lookup_range_tree_to_list treeL
|
||||
@ lookup_range_tree_to_list treeR) x"
|
||||
using lookup_range_tree_to_list.simps append_assoc
|
||||
using lookup_range_tree_to_list.simps(2) append_assoc
|
||||
lookup_map_of_append_commute[OF treeL1_disjoint]
|
||||
lookup_map_of_append_cong[OF _ refl]
|
||||
by metis
|
||||
|
|
|
|||
|
|
@ -23,10 +23,10 @@ fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt);
|
|||
fun fix_schematics ctxt raw_st =
|
||||
let
|
||||
val ((schematic_types, [st']), ctxt1) = Variable.importT [raw_st] ctxt;
|
||||
fun certify_inst ctxt inst = map (apsnd (Thm.cterm_of ctxt)) (#2 inst)
|
||||
fun certify_inst ((_, terms), ctxt) = (Vars.map (K (Thm.cterm_of ctxt)) terms, ctxt);
|
||||
val (schematic_terms, ctxt2) =
|
||||
Variable.import_inst true [Thm.prop_of st'] ctxt1
|
||||
|>> certify_inst ctxt1;
|
||||
|> certify_inst;
|
||||
val schematics = (schematic_types, schematic_terms);
|
||||
in (Thm.instantiate schematics st', ctxt2) end
|
||||
|
||||
|
|
@ -60,7 +60,7 @@ let
|
|||
in
|
||||
Thm.implies_elim asm (Thm.trivial @{cprop "PROP A"})
|
||||
|> Drule.implies_intr_hyps
|
||||
|> Thm.generalize ([],["A"]) 1
|
||||
|> Thm.generalize (Names.empty, Names.make_set ["A"]) 1
|
||||
|> Drule.zero_var_indexes
|
||||
end
|
||||
|
||||
|
|
@ -77,7 +77,7 @@ in
|
|||
|> Thm.implies_elim (asm' COMP Drule.equal_elim_rule2)
|
||||
|> Drule.implies_intr_hyps
|
||||
|> Thm.permute_prems 0 ~1
|
||||
|> Thm.generalize ([],["A","P"]) 1
|
||||
|> Thm.generalize (Names.empty, Names.make_set ["A","P"]) 1
|
||||
|> Drule.zero_var_indexes
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -55,7 +55,7 @@ lemma Eq_TrueI_ByAssum:
|
|||
simproc_setup simp_strategy_ByAssum ("simp_strategy ByAssum b") =
|
||||
\<open>K (fn ss => fn ct => let
|
||||
val b = Thm.dest_arg ct
|
||||
val t = Thm.instantiate ([],[((("P",0),@{typ bool}), b)])
|
||||
val t = Thm.instantiate (TVars.empty, Vars.make [((("P",0),@{typ bool}), b)])
|
||||
@{thm Eq_TrueI_ByAssum}
|
||||
val prems = Raw_Simplifier.prems_of ss
|
||||
in get_first (try (fn p => p RS t)) prems end)\<close>
|
||||
|
|
@ -83,7 +83,7 @@ lemma simp_strategy_Eq_True:
|
|||
ML \<open>
|
||||
fun simp_strategy_True_conv ct = case Thm.term_of ct of
|
||||
(Const (@{const_name simp_strategy}, _) $ _ $ @{term True})
|
||||
=> Thm.instantiate ([], [((("name",0), @{typ nat}), Thm.dest_arg1 ct)])
|
||||
=> Thm.instantiate (TVars.empty, Vars.make [((("name",0), @{typ nat}), Thm.dest_arg1 ct)])
|
||||
@{thm simp_strategy_Eq_True}
|
||||
| _ => Conv.all_conv ct
|
||||
|
||||
|
|
|
|||
|
|
@ -183,9 +183,9 @@ fun attach_proof_annotations ctxt terms st =
|
|||
(* FIXME: this might affect st's maxidx *)
|
||||
val add_eqn =
|
||||
Thm.instantiate
|
||||
([],
|
||||
[((("P", 0), @{typ prop}), cconcl_of st),
|
||||
((("xs", 0), @{typ bool}), Thm.cterm_of ctxt container)])
|
||||
(TVars.empty,
|
||||
Vars.make [((("P", 0), @{typ prop}), cconcl_of st),
|
||||
((("xs", 0), @{typ bool}), Thm.cterm_of ctxt container)])
|
||||
@{thm proof_state_add}
|
||||
in
|
||||
rewrite_state_concl add_eqn st
|
||||
|
|
@ -208,9 +208,9 @@ fun detach_proof_annotations st =
|
|||
|> dest_term_container
|
||||
val remove_eqn =
|
||||
Thm.instantiate
|
||||
([],
|
||||
[((("P", 0), @{typ prop}), real_concl),
|
||||
((("xs", 0), @{typ bool}), ccontainer)])
|
||||
(TVars.empty,
|
||||
Vars.make [((("P", 0), @{typ prop}), real_concl),
|
||||
((("xs", 0), @{typ bool}), ccontainer)])
|
||||
@{thm proof_state_remove}
|
||||
in
|
||||
(terms, rewrite_state_concl remove_eqn st)
|
||||
|
|
@ -227,9 +227,9 @@ fun attach_rule_annotations ctxt terms thm =
|
|||
(* FIXME: this might affect thm's maxidx *)
|
||||
val add_eqn =
|
||||
Thm.instantiate
|
||||
([],
|
||||
[((("P", 0), @{typ prop}), Thm.cconcl_of thm),
|
||||
((("xs", 0), @{typ bool}), Thm.cterm_of ctxt container)])
|
||||
(TVars.empty,
|
||||
Vars.make [((("P", 0), @{typ prop}), Thm.cconcl_of thm),
|
||||
((("xs", 0), @{typ bool}), Thm.cterm_of ctxt container)])
|
||||
@{thm rule_add}
|
||||
in
|
||||
rewrite_state_concl add_eqn thm
|
||||
|
|
@ -349,7 +349,7 @@ fun instantiate_types ctxt _ tvar_insts term =
|
|||
val tyenv = Sign.typ_match (Proof_Context.theory_of ctxt) tvar_inst Vartab.empty
|
||||
val S = Vartab.dest tyenv
|
||||
val S' = map (fn (s,(t,u)) => ((s,t),u)) S
|
||||
in Term_Subst.instantiateT S' typ
|
||||
in Term_Subst.instantiateT (TVars.make S') typ
|
||||
end
|
||||
in fold (fn typs => Term.map_types (instantiateT typs)) tvar_insts term
|
||||
end
|
||||
|
|
|
|||
|
|
@ -30,7 +30,6 @@ structure Methods = Theory_Data
|
|||
(
|
||||
type T = Symtab.set;
|
||||
val empty = Symtab.empty;
|
||||
val extend = I;
|
||||
val merge = Symtab.merge (K true);
|
||||
);
|
||||
|
||||
|
|
|
|||
|
|
@ -60,7 +60,7 @@ fun term_pattern_antiquote ctxt s =
|
|||
end;
|
||||
val _ = Context.>> (Context.map_theory (
|
||||
ML_Antiquotation.inline @{binding "term_pat"}
|
||||
((Args.context -- Scan.lift Args.embedded_inner_syntax)
|
||||
((Args.context -- Scan.lift Parse.embedded_inner_syntax)
|
||||
>> uncurry Term_Pattern_Antiquote.term_pattern_antiquote)))
|
||||
\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -171,7 +171,7 @@ local
|
|||
in
|
||||
val _ = Context.>> (Context.map_theory (
|
||||
ML_Antiquotation.inline @{binding "mk_term"}
|
||||
((Args.context -- Scan.lift Args.embedded_inner_syntax -- (Scan.optional (Scan.lift ((comma_list Args.name))) []))
|
||||
((Args.context -- Scan.lift Parse.embedded_inner_syntax -- (Scan.optional (Scan.lift ((comma_list Args.name))) []))
|
||||
>> gen_constructor)))
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ fun fix_schematics ctxt raw_st =
|
|||
val ((_, inst), ctxt2) =
|
||||
Variable.import_inst true [Thm.prop_of st'] ctxt1;
|
||||
|
||||
val schematic_terms = map (apsnd (Thm.cterm_of ctxt2)) inst;
|
||||
val schematic_terms = Vars.map (K (Thm.cterm_of ctxt2)) inst;
|
||||
val schematics = (schematic_types, schematic_terms);
|
||||
|
||||
in (Thm.instantiate schematics st', ctxt2) end
|
||||
|
|
|
|||
|
|
@ -50,7 +50,6 @@ requalify_consts
|
|||
|
||||
lemma Suc_unat_mask_div_obfuscated:
|
||||
"Suc (unat (mask sz div (word_size::machine_word))) = 2 ^ (min sz word_bits - word_size_bits)"
|
||||
unfolding word_size_bits_def
|
||||
by (rule Suc_unat_mask_div)
|
||||
|
||||
lemma word_size_size_bits_nat:
|
||||
|
|
|
|||
Loading…
Reference in New Issue