adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

fix lib for isabelle 2016

This commit is contained in:
Daniel Matichuk 2016-01-12 14:58:16 +11:00
parent a0131b5f3d
commit b7563eb788
19 changed files with 101 additions and 561 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

277
lib/Eisbach_Compat.thy
View File

@ -1,277 +0,0 @@
(* Hot-fixes for Eisbach *)
theory Eisbach_Compat
imports "~~/src/HOL/Eisbach/Eisbach"
begin
ML
\<open>
(* Clagged from Isabelle-2015 *)
(* Title: HOL/Eisbach/eisbach_rule_insts.ML
Author: Daniel Matichuk, NICTA/UNSW
Eisbach-aware variants of the "where" and "of" attributes.
Alternate syntax for rule_insts.ML participates in token closures by
examining the behaviour of Rule_Insts.where_rule and instantiating token
values accordingly. Instantiations in re-interpretation are done with
Drule.cterm_instantiate.
FIX: Correctly handle case where term instantiation is TYPE('a)
*)
structure Eisbach_Rule_Insts : sig end =
struct
fun restore_tags thm = Thm.map_tags (K (Thm.get_tags thm));
val mk_term_type_internal = Logic.protect o Logic.mk_term o Logic.mk_type;
fun term_type_cases f g t = case (try (Logic.dest_type o Logic.dest_term o Logic.unprotect) t) of
SOME T => f T
| NONE => case (try Logic.dest_term t) of
SOME t => g t
| NONE => raise Fail "Lost encoded instantiation"
fun add_thm_insts thm =
let
val thy = Thm.theory_of_thm thm;
val tyvars = Thm.fold_terms Term.add_tvars thm [];
val tyvars' = tyvars |> map (mk_term_type_internal o TVar);
val tvars = Thm.fold_terms Term.add_vars thm [];
val tvars' = tvars |> map (Logic.mk_term o Var);
val conj =
Logic.mk_conjunction_list (tyvars' @ tvars') |> Thm.global_cterm_of thy |> Drule.mk_term;
in
((tyvars, tvars), Conjunction.intr thm conj)
end;
fun get_thm_insts thm =
let
val (thm', insts) = Conjunction.elim thm;
val insts' = insts
|> Drule.dest_term
|> Thm.term_of
|> Logic.dest_conjunction_list
|> (fn f => fold (fn t => fn (tys, ts) =>
term_type_cases (fn T => (T :: tys, ts)) (fn t => (tys, t :: ts)) t) f ([], []))
||> rev
|>> rev;
in
(thm', insts')
end;
fun instantiate_xis insts thm =
let
val tyvars = Thm.fold_terms Term.add_tvars thm [];
val tvars = Thm.fold_terms Term.add_vars thm [];
val cert = Thm.global_cterm_of (Thm.theory_of_thm thm);
val certT = Thm.global_ctyp_of (Thm.theory_of_thm thm);
fun add_inst (xi, t) (Ts, ts) =
(case AList.lookup (op =) tyvars xi of
SOME S => ((certT (TVar (xi, S)), certT (Logic.dest_type t)) :: Ts, ts)
| NONE =>
(case AList.lookup (op =) tvars xi of
SOME T => (Ts, (cert (Var (xi, T)), cert t) :: ts)
| NONE => error "indexname not found in thm"));
val (cTinsts, cinsts) = fold add_inst insts ([], []);
in
(Thm.instantiate (cTinsts, []) thm
|> Drule.cterm_instantiate cinsts
COMP_INCR asm_rl)
|> Thm.adjust_maxidx_thm ~1
|> restore_tags thm
end;
(* FIXME unused *)
fun read_instantiate_no_thm ctxt insts fixes =
let
val (type_insts, term_insts) =
List.partition (fn (((x, _) : indexname), _) => String.isPrefix "'" x) insts;
val ctxt1 =
ctxt
|> Context_Position.not_really
|> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
val typs =
map snd type_insts
|> Syntax.read_typs ctxt1
|> Syntax.check_typs ctxt1;
val typ_insts' = map2 (fn (xi, _) => fn T => (xi,T)) type_insts typs;
val terms =
map snd term_insts
|> Syntax.read_terms ctxt1
|> Syntax.check_terms ctxt1;
val term_insts' = map2 (fn (xi, _) => fn t => (xi, t)) term_insts terms;
in (typ_insts',term_insts') end;
datatype rule_inst =
Named_Insts of ((indexname * string) * (term -> unit)) list * (binding * string option * mixfix) list
(*| Unchecked_Of_Insts of (string option list * string option list) * (binding * string option * mixfix) list*)
| Term_Insts of (indexname * term) list
| Unchecked_Term_Insts of term option list * term option list;
fun mk_pair (t, t') = Logic.mk_conjunction (Logic.mk_term t, Logic.mk_term t');
fun dest_pair t = apply2 Logic.dest_term (Logic.dest_conjunction t);
fun embed_indexname ((xi, s), f) =
let fun wrap_xi xi t = mk_pair (Var (xi, fastype_of t), t);
in ((xi, s), f o wrap_xi xi) end;
fun unembed_indexname t = dest_pair t |> apfst (Term.dest_Var #> fst);
fun read_where_insts (insts, fixes) =
let
val insts' =
if forall (fn (_, v) => Parse_Tools.is_real_val v) insts
then Term_Insts (map (unembed_indexname o Parse_Tools.the_real_val o snd) insts)
else
Named_Insts (map (fn (xi, p) => embed_indexname
((xi, Parse_Tools.the_parse_val p), Parse_Tools.the_parse_fun p)) insts, fixes);
in insts' end;
fun of_rule thm (args, concl_args) =
let
fun zip_vars _ [] = []
| zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
| zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest
| zip_vars [] _ = error "More instantiations than variables in theorem";
val insts =
zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
in insts end;
val inst = Args.maybe Parse_Tools.name_term;
val concl = Args.$$$ "concl" -- Args.colon;
fun close_unchecked_insts context ((insts,concl_inst), fixes) =
let
val ctxt = Context.proof_of context;
val ctxt1 = ctxt
|> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
val insts' = insts @ concl_inst;
val term_insts =
map (the_list o (Option.map Parse_Tools.the_parse_val)) insts'
|> burrow (Syntax.read_terms ctxt1
#> Syntax.check_terms ctxt1
#> Variable.export_terms ctxt1 ctxt)
|> map (try the_single);
val _ =
(insts', term_insts)
|> ListPair.app (fn (SOME p, SOME t) => Parse_Tools.the_parse_fun p t | _ => ());
val (insts'',concl_insts'') = chop (length insts) term_insts;
in Unchecked_Term_Insts (insts'', concl_insts'') end;
fun read_of_insts checked context ((insts, concl_insts), fixes) =
if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts)
then
if checked
then
(fn _ =>
Term_Insts
(map (unembed_indexname o Parse_Tools.the_real_val) (map_filter I (insts @ concl_insts))))
else
(fn _ =>
Unchecked_Term_Insts
(map (Option.map Parse_Tools.the_real_val) insts,
map (Option.map Parse_Tools.the_real_val) concl_insts))
else
if checked
then
(fn thm =>
Named_Insts
(apply2
(map (Option.map (fn p => (Parse_Tools.the_parse_val p, Parse_Tools.the_parse_fun p))))
(insts, concl_insts)
|> of_rule thm |> map ((fn (xi, (nm, f)) => embed_indexname ((xi, nm), f))), fixes))
else
let val result = close_unchecked_insts context ((insts, concl_insts), fixes);
in fn _ => result end;
fun read_instantiate_closed ctxt (Named_Insts (insts, fixes)) thm =
let
val insts' = map (fn ((v, t), _) => ((v, Position.none), t)) insts;
val (thm_insts, thm') = add_thm_insts thm
val (thm'', thm_insts') =
Rule_Insts.where_rule ctxt insts' fixes thm'
|> get_thm_insts;
val tyinst =
ListPair.zip (fst thm_insts, fst thm_insts') |> map (fn ((xi, _), typ) => (xi, typ));
val tinst =
ListPair.zip (snd thm_insts, snd thm_insts') |> map (fn ((xi, _), t) => (xi, t));
val _ =
map (fn ((xi, _), f) =>
(case AList.lookup (op =) tyinst xi of
SOME typ => f (Logic.mk_type typ)
| NONE =>
(case AList.lookup (op =) tinst xi of
SOME t => f t
| NONE => error "Lost indexname in instantiated theorem"))) insts;
in
(thm'' |> restore_tags thm)
end
| read_instantiate_closed ctxt (Unchecked_Term_Insts insts) thm =
let
val (xis, ts) = ListPair.unzip (of_rule thm insts);
val ctxt' = Variable.declare_maxidx (Thm.maxidx_of thm) ctxt;
val (ts', ctxt'') = Variable.import_terms false ts ctxt';
val ts'' = Variable.export_terms ctxt'' ctxt ts';
val insts' = ListPair.zip (xis, ts'');
in instantiate_xis insts' thm end
| read_instantiate_closed _ (Term_Insts insts) thm = instantiate_xis insts thm;
val _ =
Theory.setup
(Attrib.setup @{binding "where"}
(Scan.lift
(Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
>> (fn args => let val args' = read_where_insts args in Thm.rule_attribute (fn context =>
read_instantiate_closed (Context.proof_of context) args') end))
"named instantiation of theorem");
val _ =
Theory.setup
(Attrib.setup @{binding "of"}
(Scan.lift
(Args.mode "unchecked" --
(Scan.repeat (Scan.unless concl inst) --
Scan.optional (concl |-- Scan.repeat inst) [] --
Parse.for_fixes)) -- Scan.state >>
(fn ((unchecked, args), context) =>
let
val read_insts = read_of_insts (not unchecked) context args;
in
Thm.rule_attribute (fn context => fn thm =>
if Method_Closure.is_free_thm thm andalso unchecked
then Method_Closure.dummy_free_thm
else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm)
end))
"positional instantiation of theorem");
end;
\<close>
end

38
lib/Eisbach_Methods.thy
View File

@ -24,7 +24,12 @@ section \<open>Debugging methods\<close>
method print_concl = (match conclusion in P for P \<Rightarrow> \<open>print_term P\<close>)
method_setup print_raw_goal = \<open>Scan.succeed (fn ctxt => fn facts =>
(fn st => (Output.writeln (Display.string_of_thm ctxt st); Seq.single ([],st))))\<close>
(fn (ctxt, st) => (Output.writeln (Thm.string_of_thm ctxt st);
Seq.make_results (Seq.single (ctxt, st)))))\<close>
ML \<open>fun method_evaluate text ctxt facts =
Method.NO_CONTEXT_TACTIC ctxt
(Method_Closure.method_evaluate text ctxt facts)\<close>
method_setup print_headgoal =
@ -39,42 +44,39 @@ section \<open>Simple Combinators\<close>
method_setup defer_tac = \<open>Scan.succeed (fn _ => SIMPLE_METHOD (defer_tac 1))\<close>
method_setup all =
\<open>Method_Closure.parse_method >> (fn m => fn ctxt => fn facts =>
\<open>Method_Closure.method_text >> (fn m => fn ctxt => fn facts =>
let
fun tac i st' =
Goal.restrict i 1 st'
|> Method_Closure.method_evaluate m ctxt facts
|> Seq.map (Goal.unrestrict i o snd)
|> method_evaluate m ctxt facts
|> Seq.map (Goal.unrestrict i)
in SIMPLE_METHOD (ALLGOALS tac) facts end)
\<close>
method_setup determ =
\<open>Method_Closure.parse_method >> (fn m => fn ctxt => fn facts =>
\<open>Method_Closure.method_text >> (fn m => fn ctxt => fn facts =>
let
fun tac st' =
Method_Closure.method_evaluate m ctxt facts st'
|> Seq.map snd
fun tac st' = method_evaluate m ctxt facts st'
in SIMPLE_METHOD (DETERM tac) facts end)
\<close>
method_setup timeit =
\<open>Method_Closure.parse_method >> (fn m => fn ctxt => fn facts =>
\<open>Method_Closure.method_text >> (fn m => fn ctxt => fn facts =>
let
fun timed_tac st seq = Seq.make (fn () => Option.map (apsnd (timed_tac st))
(timeit (fn () => (Seq.pull seq))));
fun tac st' =
timed_tac st' (Method_Closure.method_evaluate m ctxt facts st')
|> Seq.map snd;
timed_tac st' (method_evaluate m ctxt facts st');
in SIMPLE_METHOD tac [] end)
\<close>
method_setup timeout =
\<open>Scan.lift Parse.int -- Method_Closure.parse_method >> (fn (i,m) => fn ctxt => fn facts =>
\<open>Scan.lift Parse.int -- Method_Closure.method_text >> (fn (i,m) => fn ctxt => fn facts =>
let
fun str_of_goal th = Pretty.string_of (Goal_Display.pretty_goal ctxt th);
@ -84,10 +86,8 @@ method_setup timeout =
fun timed_tac st seq = Seq.make (limit st (fn () => Option.map (apsnd (timed_tac st))
(Seq.pull seq)));
fun tac st' =
timed_tac st' (Method_Closure.method_evaluate m ctxt facts st')
|> Seq.map snd;
timed_tac st' (method_evaluate m ctxt facts st');
in SIMPLE_METHOD tac [] end)
\<close>
@ -99,10 +99,10 @@ text \<open>The following @{text fails} and @{text succeeds} methods protect the
The @{text fails} method inverts success, only succeeding if the given method would fail.\<close>
method_setup fails =
\<open>Method_Closure.parse_method >> (fn m => fn ctxt => fn facts =>
\<open>Method_Closure.method_text >> (fn m => fn ctxt => fn facts =>
let
fun fail_tac st' =
(case Seq.pull (Method_Closure.method_evaluate m ctxt facts st') of
(case Seq.pull (method_evaluate m ctxt facts st') of
SOME _ => Seq.empty
| NONE => Seq.single st')
@ -110,10 +110,10 @@ method_setup fails =
\<close>
method_setup succeeds =
\<open>Method_Closure.parse_method >> (fn m => fn ctxt => fn facts =>
\<open>Method_Closure.method_text >> (fn m => fn ctxt => fn facts =>
let
fun can_tac st' =
(case Seq.pull (Method_Closure.method_evaluate m ctxt facts st') of
(case Seq.pull (method_evaluate m ctxt facts st') of
SOME (st'',_) => Seq.single st'
| NONE => Seq.empty)

4
lib/HaskellLib_H.thy
View File

@ -88,7 +88,7 @@ declare curry1_def[simp] curry2_def[simp]
definition
"split1 \<equiv> id"
definition
"split2 \<equiv> split"
"split2 \<equiv> case_prod"
definition
"split3 f \<equiv> \<lambda>(a, b, c). f a b c"
definition
@ -500,7 +500,7 @@ where
else (\<lambda>(ys, zs). (x # ys, zs)) (break f xs))"
definition
"uncurry \<equiv> split"
"uncurry \<equiv> case_prod"
definition
sum :: "'a list \<Rightarrow> 'a::{plus,zero}" where

6
lib/NICTACompat.thy
View File

@ -17,7 +17,6 @@ imports
"~~/src/HOL/Word/WordBitwise"
SignedWords
NICTATools
Eisbach_Compat
begin
(* all theories should import from NICTACompat rather than any ancestors *)
@ -183,4 +182,9 @@ lemma bin_nth_minus_Bit1[simp]:
"0 < n \<Longrightarrow> bin_nth (numeral (num.Bit1 w)) n = bin_nth (numeral w) (n - 1)"
by (cases n, simp_all)
abbreviation (input)
split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
where
"split == case_prod"
end

2
lib/NICTATools.thy
View File

@ -66,7 +66,7 @@ let
* we can produce a "warning" icon in Isabelle/jEdit. *)
val _ =
if length results > 0 then
warning (message results |> Pretty.str_of)
warning (message results |> Pretty.string_of)
else ()
in
(false, ("", []))

1
lib/NonDetMonadLemmaBucket.thy
View File

@ -1175,6 +1175,7 @@ lemma list_cases_weak_wp:
apply (simp, rule hoare_weaken_pre, rule assms, simp)+
done
lemmas hoare_FalseE_R = hoare_FalseE[where E="\<top>\<top>", folded validE_R_def]
lemma hoare_vcg_if_lift2:

8
lib/Rule_By_Method.thy
View File

@ -204,18 +204,20 @@ val parse_flags = Args.mode "schematic" -- Args.mode "raw_prop" >> (fn (b,b') =>
val parse_method = Method_Closure.method_text o apfst (Config.put_generic Method.old_section_parser true)
fun tac m ctxt = Method_Closure.method_evaluate m ctxt [] #> Seq.map snd;
fun tac m ctxt =
Method.NO_CONTEXT_TACTIC ctxt
(Method_Closure.method_evaluate m ctxt []);
val (rule_prems_by_method : attribute context_parser) = Scan.lift parse_flags :-- (fn flags =>
position (Scan.repeat1
(with_rule_prems (not (#vars flags)) parse_method ||
Scan.lift (Args.$$$ "_" >> (K Method.succeed_text))))) >>
(fn (flags,(ms,pos)) => Thm.rule_attribute (fn context =>
(fn (flags,(ms,pos)) => Thm.rule_attribute [] (fn context =>
rule_by_tac (Context.proof_of context) flags (K all_tac) (map tac ms) pos))
val (rule_concl_by_method : attribute context_parser) = Scan.lift parse_flags :-- (fn flags =>
position (with_rule_prems (not (#vars flags)) parse_method)) >>
(fn (flags,(m,pos)) => Thm.rule_attribute (fn context =>
(fn (flags,(m,pos)) => Thm.rule_attribute [] (fn context =>
rule_by_tac (Context.proof_of context) flags (tac m) [] pos))
val _ = Theory.setup

21
lib/SplitRule.thy
View File

@ -14,7 +14,7 @@ begin
ML {*
fun str_of_term t = Pretty.str_of (Syntax.pretty_term @{context} t)
fun str_of_term t = Pretty.string_of (Syntax.pretty_term @{context} t)
structure SplitSimps = struct
@ -29,9 +29,9 @@ fun was_split t = let
in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
handle TERM _ => false;
fun apply_split split t = Seq.of_list let
val (t', thaw) = Misc_Legacy.freeze_thaw t;
in (map thaw (filter (was_split o Thm.prop_of) ([t'] RL [split]))) end;
fun apply_split ctxt split t = Seq.of_list let
val (t', thaw) = Misc_Legacy.freeze_thaw_robust ctxt t;
in (map (thaw 0) (filter (was_split o Thm.prop_of) ([t'] RL [split]))) end;
fun forward_tac rules t = Seq.of_list ([t] RL rules);
@ -42,22 +42,23 @@ val get_rules_once_split =
THEN REPEAT (forward_tac [spec])
THEN (forward_tac [refl_imp]);
fun do_split split = let
fun do_split ctxt split = let
val split' = split RS iffD1;
val split_rhs = Thm.concl_of (fst (Misc_Legacy.freeze_thaw split'));
val split_rhs = Thm.concl_of (fst (Misc_Legacy.freeze_thaw_robust ctxt split'));
in if was_split split_rhs
then apply_split split' THEN get_rules_once_split
then apply_split ctxt split' THEN get_rules_once_split
else raise TERM ("malformed split rule: " ^ (str_of_term split_rhs), [split_rhs])
end;
val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq];
fun better_split splitthms thm = conjunct_rules
fun better_split ctxt splitthms thm = conjunct_rules
(Seq.list_of ((TRY atomize_meta_eq
THEN (REPEAT (FIRST (map do_split splitthms)))) thm));
THEN (REPEAT (FIRST (map (do_split ctxt) splitthms)))) thm));
val split_att
= Attrib.thms >> (Thm.rule_attribute o K o better_split);
= Attrib.thms >>
(fn thms => Thm.rule_attribute thms (fn context => better_split (Context.proof_of context) thms));
end;

6
lib/Strengthen.thy
View File

@ -173,7 +173,7 @@ val arg_pars = Scan.option (Scan.first (map Args.$$$ ["I", "I'", "D", "D'", "lhs
val setup =
Attrib.setup @{binding "mk_strg"}
((Scan.lift arg_pars -- Args.context)
>> (fn (args, ctxt) => Thm.rule_attribute (K (mk_strg_args args ctxt))))
>> (fn (args, ctxt) => Thm.rule_attribute [] (K (mk_strg_args args ctxt))))
"put rule in 'strengthen' form"
end
@ -227,7 +227,7 @@ val setup =
"strengthening congruence rules";
val do_elim = SUBGOAL (fn (t, i) => case (head_of (Logic.strip_assums_concl t)) of
@{term elim} => etac @{thm do_elim} i
@{term elim} => eresolve0_tac @{thms do_elim} i
| _ => all_tac)
infix 1 THEN_TRY_ALL_NEW;
@ -253,7 +253,7 @@ fun do_strg ctxt congs rules
fun strengthen ctxt thms = let
val congs = Congs.get (Proof_Context.theory_of ctxt)
val rules = map (Make_Strengthen_Rule.auto_mk ctxt) thms
in rtac @{thm use_strengthen_imp}
in resolve0_tac @{thms use_strengthen_imp}
THEN' do_strg ctxt congs rules end
val strengthen_args =

2
lib/SubMonadLib.thy
View File

@ -66,7 +66,7 @@ lemma select_f_walk:
assumes S: "fst S = {} \<Longrightarrow> snd S"
shows "(do a \<leftarrow> m1; b \<leftarrow> select_f S; m2 a b od) = (do b \<leftarrow> select_f S; a \<leftarrow> m1; m2 a b od)"
apply (rule ext)
apply (subst Pair_fst_snd_eq)
apply (rule prod.expand)
apply (rule conjI)
apply (simp add: select_f_def bind_def split_def)
apply fastforce

4
lib/WhileLoopRules.thy
View File

@ -209,8 +209,8 @@ lemma whileLoop_results_induct_lemma3 [consumes 1]:
and inv_start: "I r s"
and inv_step: "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> I r' s'"
shows "I r' s'"
apply (rule whileLoop_results_induct_lemma2 [where P="split I" and y="(r', s')" and x="(r, s)",
simplified split_def, simplified])
apply (rule whileLoop_results_induct_lemma2 [where P="case_prod I" and y="(r', s')" and x="(r, s)",
simplified case_prod_unfold, simplified])
apply (rule result)
apply simp
apply simp

10
lib/crunch-cmd.ML
View File

@ -212,12 +212,12 @@ fun unfold ctxt const triple nmspce =
val const_defn = const |> Long_Name.base_name |> def_of;
val const_def = deep_search_thms ctxt const_defn const_term nmspce
|> hd |> Simpdata.safe_mk_meta_eq;
val _ = Pretty.writeln (Pretty.block [Pretty.str ("const_def: " ^ PolyML.makestring const_defn), Display.pretty_thm ctxt const_def])
val _ = Pretty.writeln (Pretty.block [Pretty.str ("const_def: " ^ PolyML.makestring const_defn), Thm.pretty_thm ctxt const_def])
val trivial_rule = Thm.trivial triple
val _ = Pretty.writeln (Pretty.block [Pretty.str "trivial_rule: ", Display.pretty_thm ctxt trivial_rule])
val _ = Pretty.writeln (Pretty.block [Pretty.str "trivial_rule: ", Thm.pretty_thm ctxt trivial_rule])
val unfold_rule = trivial_rule
|> Simplifier.rewrite_goals_rule ctxt [const_def];
val _ = Pretty.writeln (Pretty.block [Pretty.str "unfold_rule: ", Display.pretty_thm ctxt unfold_rule])
val _ = Pretty.writeln (Pretty.block [Pretty.str "unfold_rule: ", Thm.pretty_thm ctxt unfold_rule])
val ms = unfold_rule
|> Simplifier.rewrite_goals_rule ctxt unfold_get_params
|> Thm.prems_of |> maps (monads_of ctxt);
@ -266,7 +266,7 @@ fun induct_inst ctxt const goal nmspce =
val n = const_term |> fastype_of |> num_args;
val t = mk_abs (Instance.magic $ mk_apps const_term n 0) n
|> Syntax.check_term ctxt |> Logic.varify_global |> Thm.cterm_of ctxt;
val P = Thm.concl_of induct_thm |> HOLogic.dest_Trueprop |> head_of |> Thm.cterm_of ctxt;
val P = Thm.concl_of induct_thm |> HOLogic.dest_Trueprop |> head_of |> Term.dest_Var;
val trivial_rule = Thm.trivial goal;
val induct_inst = Thm.instantiate ([], [(P, t)]) induct_thm
RS trivial_rule;
@ -446,7 +446,7 @@ fun crunch cfg pre extra stack const' thms =
in (Goal.prove ctxt''' [] [] goal_prop2
( (*DupSkip.goal_prove_wrapper *) (fn _ =>
rtac unfold_rule 1
resolve_tac ctxt''' [unfold_rule] 1
THEN maybe_cheat_tac ctxt'''
THEN ALLGOALS (fn n =>
simp_tac ctxt''' n

185
lib/subgoal_focus/Subgoal_Focus.thy
View File

@ -1,185 +0,0 @@
(* Title: Subgoal_Focus.thy
Author: Daniel Matichuk, NICTA/UNSW
Author: Makarius
Support for structured proof "scripts", via subgoal focus command.
TODO:
- discontinue 'premises' binding: use general 'supply';
- prefer explicit "using prems" over implicit "apply (insert prems)" (!?);
- speculatively: 'premises' avoids inserting prems into focused goal (???);
*)
theory Subgoal_Focus
imports Main
keywords
"subgoal" :: prf_goal and
"premises"
begin
ML \<open>
signature SUBGOAL_FOCUS =
sig
val subgoal_focus: Attrib.binding -> Attrib.binding option ->
bool * (bstring option * Position.T) list -> Proof.state -> Proof.state
val subgoal_focus_cmd: Attrib.binding -> Attrib.binding option ->
bool * (bstring option * Position.T) list -> Proof.state -> Proof.state
end;
structure Subgoal_Focus: SUBGOAL_FOCUS =
struct
local
fun cert_var v ctxt = apfst hd (Proof_Context.cert_vars [v] ctxt);
fun subst_cterm (in_ct, in_ct') ct =
let
val abs = Thm.dest_arg (Thm.cprop_of (Thm.abstract_rule "_dummy_" in_ct (Thm.reflexive ct)));
val ct' = Drule.beta_conv abs in_ct';
in ct' end;
fun unprotect_cterm ct = Thm.cprop_of (Goal.conclude (Thm.assume ct));
fun focus_named_params ctxt do_prems (param_suffix, raw_param_specs) subgoal =
let
val goal_params = Logic.strip_params (Thm.term_of subgoal);
val internal_params =
goal_params
|> Variable.variant_frees ctxt [Thm.term_of subgoal]
|> map (Name.internal o fst);
val n = length goal_params;
val m = length raw_param_specs;
val _ =
m <= n orelse
error ("Excessive subgoal parameter specification" ^
Position.here_list (map snd (drop n raw_param_specs)));
val param_specs =
raw_param_specs |> map
(fn (NONE, _) => NONE
| (SOME x, pos) =>
let val b = #1 (#1 (cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
in SOME (Variable.check_name b) end)
|> param_suffix ? append (replicate (n - m) NONE);
val (param_specs',ctxt1) = fold_burrow Variable.variant_fixes (map the_list param_specs) ctxt
|>> map (find_first (K true))
val ((_, [st]), ctxt2) = Variable.importT [Thm.reflexive subgoal] ctxt1;
val subgoal1 = Thm.dest_arg (Thm.cprop_of st);
val renamed =
subgoal1
|> Thm.renamed_term (Logic.list_rename_params internal_params (Thm.term_of subgoal1));
val ((goal_params', subgoal2), ctxt3) =
Variable.focus_cterm renamed ctxt2
|> apfst (apfst (map snd));
fun rename_free ct opt_n = case opt_n of SOME n =>
let
val (_,T) = Term.dest_Free (Thm.term_of ct);
in Thm.cterm_of ctxt2 (Free (n,T)) end
| NONE => ct
fun rename_list (opt_x :: xs) (y :: ys) = (rename_free y opt_x :: rename_list xs ys)
| rename_list _ ys = ys;
val goal_params'' = rename_list param_specs' goal_params';
val ctxt4 = fold (Variable.declare_constraints o Thm.term_of) goal_params'' ctxt3;
val subgoal3 = fold subst_cterm (ListPair.zip (goal_params', goal_params'')) subgoal2;
val subgoal4 =
if do_prems then subgoal3 else Thm.apply (Thm.cterm_of ctxt3 Logic.protectC) subgoal3;
val (focus, _) = Subgoal.focus ctxt4 1 (Goal.init subgoal4);
val params_out = map (fn ct => (fst (Term.dest_Free (Thm.term_of ct)), ct)) goal_params'';
val concl = if do_prems then #concl focus else unprotect_cterm (#concl focus);
in
{asms = #asms focus, prems = #prems focus, concl = concl, params = params_out,
context = #context focus}
end;
fun primitive_raw_text r = Method.Basic (fn ctxt => fn _ => EMPTY_CASES (PRIMITIVE (r ctxt)));
fun gen_focus prep_atts
raw_binding raw_prems_binding param_specs state =
let
val _ = Proof.assert_backward state;
val ctxt = Proof.context_of state;
val goal = #goal (Proof.raw_goal state);
val binding = apsnd (map (prep_atts ctxt)) raw_binding;
val opt_prems_binding = Option.map (apsnd (map (prep_atts ctxt))) raw_prems_binding;
val prems_binding = the_default (Binding.empty, []) opt_prems_binding;
val do_prems = is_some opt_prems_binding;
val subgoal = Thm.cprem_of goal 1;
val focus = focus_named_params ctxt do_prems param_specs subgoal;
val focus_ctxt = #context focus;
fun after_qed [[res]] state' = (* FIXME continue with state' *)
let
val retrofit =
Subgoal.retrofit focus_ctxt ctxt (#params focus) (#asms focus) 1
(Goal.protect 0 res) (Goal.init subgoal)
|> Seq.hd
|> Goal.conclude;
val result = Raw_Simplifier.norm_hhf ctxt retrofit;
in
state
|> Proof.refine (primitive_raw_text (fn _ =>
Thm.bicompose NONE {flatten = false, match = false, incremented = false}
(false, retrofit, 0) 1 #> Seq.hd))
|> Seq.hd
|> Proof.map_context (snd o Proof_Context.note_thmss "" [(binding, [([result], [])])])
end;
in
(* FIXME more conventional block structure, like Proof.begin_block *)
Proof.begin_notepad focus_ctxt
|> Proof.map_context (snd o
Proof_Context.note_thmss ""
[(prems_binding, [(#prems focus, [])])])
|> Proof.local_goal (K (K ())) (K I) (pair o rpair I) "subgoal" NONE after_qed
[(Thm.empty_binding, [Thm.term_of (#concl focus)])]
end;
in
val subgoal_focus = gen_focus Attrib.attribute;
val subgoal_focus_cmd = gen_focus Attrib.attribute_cmd;
end;
val fact_binding = (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty);
val opt_fact_binding = Scan.optional fact_binding Attrib.empty_binding;
val dots = Parse.sym_ident :-- (fn "\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
val for_params =
Scan.optional
(@{keyword "for"} |--
Parse.!!! ((Scan.option dots >> is_some) --
(Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
(false, []);
val _ =
Outer_Syntax.command @{command_keyword subgoal} "focus subgoal"
(opt_fact_binding --
(Scan.option (@{keyword "premises"} |-- Parse.!!! opt_fact_binding)) --
for_params >>
(fn ((a, b), c) =>
Toplevel.proofs (Seq.make_results o Seq.single o subgoal_focus_cmd a b c)));
end;
\<close>
end

24
lib/subgoal_focus/Subgoal_Methods.thy
View File

@ -40,10 +40,12 @@ fun push_outer_params ctxt th =
fun fix_schematics ctxt raw_st =
let
val ((schematic_types, [st']), ctxt1) = Variable.importT [raw_st] ctxt;
val ((_, schematic_terms), ctxt2) =
Variable.import_inst true [Thm.prop_of st'] ctxt1
|>> Thm.certify_inst (Thm.theory_of_thm st');
val ((_, inst), ctxt2) =
Variable.import_inst true [Thm.prop_of st'] ctxt1;
val schematic_terms = map (apsnd (Thm.cterm_of ctxt2)) inst;
val schematics = (schematic_types, schematic_terms);
in (Thm.instantiate schematics st', ctxt2) end
val strip_params = Term.strip_all_vars;
@ -134,7 +136,7 @@ fun distinct_subgoals ctxt raw_st =
|> Seq.hd;
val subgoals' = subgoals
|> inter (op aconvc) (#hyps (Thm.crep_thm st'))
|> inter (op aconvc) (Thm.chyps_of st')
|> distinct (op aconvc);
in
Drule.implies_intr_list subgoals' st'
@ -162,7 +164,7 @@ fun trim_prems_tac ctxt rules =
let
fun matches (prem,rule) =
let
val ((_,prem'),ctxt') = Variable.focus prem ctxt;
val ((_,prem'),ctxt') = Variable.focus NONE prem ctxt;
val rule_prop = Thm.prop_of rule;
in Unify.matches_list (Context.Proof ctxt') [rule_prop] [prem'] end;
@ -178,13 +180,6 @@ fun unfold_subgoals_tac ctxt =
TRY (adhoc_conjunction_tac 1)
THEN (PRIMITIVE (Raw_Simplifier.norm_hhf ctxt));
fun subgoal_cases ctxt st =
let
val ((_,[st']),ctxt') = Variable.importT [st] ctxt
val (case_names,_) = Rule_Cases.get st';
val cases = Rule_Cases.make_common ctxt' (Thm.prop_of st') case_names;
in CASES cases all_tac st' end;
val _ =
Theory.setup
(Method.setup @{binding fold_subgoals}
@ -199,10 +194,7 @@ val _ =
Method.setup @{binding trim}
(Attrib.thms >> (fn thms => fn ctxt =>
SIMPLE_METHOD (HEADGOAL (trim_prems_tac ctxt thms))))
"trim all premises that match the given rules" #>
Method.setup @{binding goals}
(Scan.succeed (fn ctxt => METHOD_CASES (K (subgoal_cases ctxt))))
"make cases from all subgoals");
"trim all premises that match the given rules");
end;
\<close>

2
lib/wp/NonDetMonadVCG.thy
View File

@ -1426,7 +1426,7 @@ lemmas hoare_wp_simps [wp_split] =
vcg_rhs_simps [THEN hoare_post_eqE2] vcg_rhs_simps [THEN hoare_post_eqE_R]
if_apply_reduct if_apply_reductE if_apply_reductE_R TrueI
schematic_lemma if_apply_test: "\<lbrace>?Q\<rbrace> (if A then returnOk else K fail) x \<lbrace>P\<rbrace>,\<lbrace>E\<rbrace>"
schematic_goal if_apply_test: "\<lbrace>?Q\<rbrace> (if A then returnOk else K fail) x \<lbrace>P\<rbrace>,\<lbrace>E\<rbrace>"
apply (wp | unfold K_def)+
done

8
lib/wp/WPC.thy
View File

@ -118,14 +118,14 @@ let
val get_concl_pred = (fst o strip_comb o HOLogic.dest_Trueprop o Thm.concl_of);
val get_concl_predC = (Thm.cterm_of ctxt o get_concl_pred);
val get_pred_tvar = (Thm.ctyp_of ctxt o domain_type o Thm.typ_of o Thm.ctyp_of_cterm);
val get_pred_tvar = domain_type o Thm.typ_of o Thm.ctyp_of_cterm;
val thm_pred = get_concl_predC thm;
val thm_pred_tvar = get_pred_tvar thm_pred;
val pred_tvar = get_pred_tvar pred;
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_pred = get_concl_predC thm2;
val thm2_pred = Term.dest_Var (get_concl_pred thm2);
in
Thm.instantiate ([], [(thm2_pred, pred)]) thm2
end;

54
lib/wp/WPEx.thy
View File

@ -67,12 +67,12 @@ lemma del_asm_rule:
"\<lbrakk> PROP P; PROP Q \<rbrakk> \<Longrightarrow> PROP Q"
by assumption
ML {*
ML \<open>
val p_prop_var = Thm.cterm_of @{context} (Logic.varify_global @{term "P :: prop"});
val p_prop_var = Term.dest_Var (Logic.varify_global @{term "P :: prop"});
fun del_asm_tac asm =
etac (cterm_instantiate [(p_prop_var, asm)] @{thm del_asm_rule});
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
@ -155,8 +155,12 @@ fun build_annotate asm =
in HOLogic.mk_Trueprop (Library.foldr mk_exists (rev ps, t)) end
| _ => raise SAME) | _ => raise SAME;
val in_mresults_ctxt =
Proof_Context.init_global @{theory Lib}
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 split_if}
@ -165,24 +169,24 @@ fun prove_qad ctxt term tac = Goal.prove ctxt [] [] term
then ALLGOALS (Skip_Proof.cheat_tac ctxt)
else tac));
val preannotate_ss =
Proof_Context.init_global @{theory Lib}
fun preannotate_ss ctxt = ctxt
|> put_simpset HOL_basic_ss
|> (fn ctxt => ctxt addsimps [@{thm K_bind_def}])
|> simpset_of
val in_mresults_ss =
Proof_Context.init_global @{theory Lib}
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 split_if}
|> simpset_of
val in_mresults_cs = Classical.claset_of (Proof_Context.init_global @{theory Lib})
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) asm;
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)
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'));
@ -193,13 +197,13 @@ fun annotate_tac ctxt asm = let
fun annotate_goal_tac ctxt
= REPEAT_DETERM1 (subgoal_asm_as_thm (annotate_tac ctxt) ctxt 1
ORELSE etac exE 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 = {* annotate_method *} "tries to annotate"
@ -236,7 +240,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 ([], [(ct v, ct v')])
|> Thm.instantiate ([], [(Term.dest_Var v, ct v')])
|> simplify (put_simpset HOL_ss ctxt)
end;
in case (strip_comb p, strip_comb q) of
@ -267,14 +271,12 @@ fun tac_with_wp_simps_strgs ctxt rules tac =
val mresults_validI = @{thm mresults_validI};
val postcond_ss =
Proof_Context.init_global @{theory Lib}
fun postcond_ss ctxt = ctxt
|> put_simpset HOL_basic_ss
|> (fn ctxt => ctxt addsimps [@{thm pred_conj_def}])
|> simpset_of
val wp_default_ss =
Proof_Context.init_global @{theory Lib}
fun wp_default_ss ctxt = ctxt
|> put_simpset HOL_ss
|> Splitter.del_split @{thm split_if}
|> simpset_of
@ -282,12 +284,12 @@ val wp_default_ss =
fun raise_tac s = all_tac THEN (fn _ => error s);
fun wpx_tac ctxt rules
= TRY (rtac mresults_validI 1)
THEN (full_simp_tac (put_simpset postcond_ss ctxt) 1)
= 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 addsimps simps) 1)
(CHANGED (full_simp_tac (put_simpset (wp_default_ss ctxt) ctxt addsimps simps) 1)
ORELSE Strengthen.strengthen ctxt strgs 1)
) 1;
@ -348,13 +350,13 @@ let
(* avoid duplicate simp rule etc warnings: *)
val ctxt = Context_Position.set_visible false ctxt
in
rtac valid_strengthen_with_mresults 1
THEN (safe_simp_tac (put_simpset postcond_ss ctxt) 1)
resolve_tac ctxt [valid_strengthen_with_mresults] 1
THEN (safe_simp_tac (put_simpset (postcond_ss ctxt) ctxt) 1)
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 addsimps simps) 1) end) ctxt 1
THEN etac wpex_name_for_idE 1
in CHANGED (simp_tac (put_simpset (wp_default_ss ctxt) ctxt addsimps simps) 1) end) ctxt 1
THEN eresolve_tac ctxt [wpex_name_for_idE] 1
end
val wps_method = Attrib.thms >> curry

8
lib/wp/WPI.thy
View File

@ -43,12 +43,12 @@ begin
text \<open>The ML version of repeat_new is slightly faster than the Eisbach one.\<close>
method_setup repeat_new =
\<open>Method_Closure.parse_method >> (fn m => fn ctxt => fn facts =>
\<open>Method_Closure.method_text >> (fn m => fn ctxt => fn facts =>
let
fun tac i st' =
Goal.restrict i 1 st'
|> Method_Closure.method_evaluate m ctxt facts
|> Seq.map (Goal.unrestrict i o snd)
|> method_evaluate m ctxt facts
|> Seq.map (Goal.unrestrict i)
in SIMPLE_METHOD (SUBGOAL (fn (_,i) => REPEAT_ALL_NEW tac i) 1) facts end)
\<close>
@ -264,7 +264,7 @@ private method_setup shared_frees =
\<open>Args.term -- Args.term >>
(fn (t,t') => (fn _ =>
SIMPLE_METHOD (fn st =>
if Method_Closure.is_dummy st then Seq.empty else
if Method.detect_closure_state st then Seq.empty else
if has_shared_frees t t' then Seq.single st else Seq.empty )))\<close>
private method uses_arg for C :: "'a \<Rightarrow> 'b \<Rightarrow> bool" =

2
proof/invariant-abstract/Include_AI.thy
View File

@ -22,7 +22,7 @@ no_notation bind_drop (infixl ">>" 60)
(* Clagged from Bits_R *)
crunch_ignore (add:
bind return when get gets fail
bind return "when" get gets fail
assert put modify unless select
alternative assert_opt gets_the
returnOk throwError lift bindE