From b7563eb7883da4489db8fc5ab5af550d81634649 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Tue, 12 Jan 2016 14:58:16 +1100 Subject: [PATCH] fix lib for isabelle 2016 --- lib/Eisbach_Compat.thy | 277 ------------------------ lib/Eisbach_Methods.thy | 38 ++-- lib/HaskellLib_H.thy | 4 +- lib/NICTACompat.thy | 6 +- lib/NICTATools.thy | 2 +- lib/NonDetMonadLemmaBucket.thy | 1 + lib/Rule_By_Method.thy | 8 +- lib/SplitRule.thy | 21 +- lib/Strengthen.thy | 6 +- lib/SubMonadLib.thy | 2 +- lib/WhileLoopRules.thy | 4 +- lib/crunch-cmd.ML | 10 +- lib/subgoal_focus/Subgoal_Focus.thy | 185 ---------------- lib/subgoal_focus/Subgoal_Methods.thy | 24 +- lib/wp/NonDetMonadVCG.thy | 2 +- lib/wp/WPC.thy | 8 +- lib/wp/WPEx.thy | 54 ++--- lib/wp/WPI.thy | 8 +- proof/invariant-abstract/Include_AI.thy | 2 +- 19 files changed, 101 insertions(+), 561 deletions(-) delete mode 100644 lib/Eisbach_Compat.thy delete mode 100644 lib/subgoal_focus/Subgoal_Focus.thy diff --git a/lib/Eisbach_Compat.thy b/lib/Eisbach_Compat.thy deleted file mode 100644 index 6d4c7728a..000000000 --- a/lib/Eisbach_Compat.thy +++ /dev/null @@ -1,277 +0,0 @@ -(* Hot-fixes for Eisbach *) - -theory Eisbach_Compat -imports "~~/src/HOL/Eisbach/Eisbach" -begin - -ML -\ -(* 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; - - -\ - -end diff --git a/lib/Eisbach_Methods.thy b/lib/Eisbach_Methods.thy index 42eef2eaa..e45e92866 100644 --- a/lib/Eisbach_Methods.thy +++ b/lib/Eisbach_Methods.thy @@ -24,7 +24,12 @@ section \Debugging methods\ method print_concl = (match conclusion in P for P \ \print_term P\) method_setup print_raw_goal = \Scan.succeed (fn ctxt => fn facts => - (fn st => (Output.writeln (Display.string_of_thm ctxt st); Seq.single ([],st))))\ + (fn (ctxt, st) => (Output.writeln (Thm.string_of_thm ctxt st); + Seq.make_results (Seq.single (ctxt, st)))))\ + +ML \fun method_evaluate text ctxt facts = + Method.NO_CONTEXT_TACTIC ctxt + (Method_Closure.method_evaluate text ctxt facts)\ method_setup print_headgoal = @@ -39,42 +44,39 @@ section \Simple Combinators\ method_setup defer_tac = \Scan.succeed (fn _ => SIMPLE_METHOD (defer_tac 1))\ method_setup all = - \Method_Closure.parse_method >> (fn m => fn ctxt => fn facts => + \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) \ method_setup determ = - \Method_Closure.parse_method >> (fn m => fn ctxt => fn facts => + \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) \ method_setup timeit = - \Method_Closure.parse_method >> (fn m => fn ctxt => fn facts => + \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) \ method_setup timeout = - \Scan.lift Parse.int -- Method_Closure.parse_method >> (fn (i,m) => fn ctxt => fn facts => + \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) \ @@ -99,10 +99,10 @@ text \The following @{text fails} and @{text succeeds} methods protect the The @{text fails} method inverts success, only succeeding if the given method would fail.\ method_setup fails = - \Method_Closure.parse_method >> (fn m => fn ctxt => fn facts => + \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 = \ method_setup succeeds = - \Method_Closure.parse_method >> (fn m => fn ctxt => fn facts => + \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) diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy index bd35c35c1..7c651bdba 100644 --- a/lib/HaskellLib_H.thy +++ b/lib/HaskellLib_H.thy @@ -88,7 +88,7 @@ declare curry1_def[simp] curry2_def[simp] definition "split1 \ id" definition - "split2 \ split" + "split2 \ case_prod" definition "split3 f \ \(a, b, c). f a b c" definition @@ -500,7 +500,7 @@ where else (\(ys, zs). (x # ys, zs)) (break f xs))" definition - "uncurry \ split" + "uncurry \ case_prod" definition sum :: "'a list \ 'a::{plus,zero}" where diff --git a/lib/NICTACompat.thy b/lib/NICTACompat.thy index bd3ef5b49..967faff96 100644 --- a/lib/NICTACompat.thy +++ b/lib/NICTACompat.thy @@ -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 \ bin_nth (numeral (num.Bit1 w)) n = bin_nth (numeral w) (n - 1)" by (cases n, simp_all) +abbreviation (input) + split :: "('a \ 'b \ 'c) \ 'a \ 'b \ 'c" +where + "split == case_prod" + end diff --git a/lib/NICTATools.thy b/lib/NICTATools.thy index 9df790f75..a73233436 100644 --- a/lib/NICTATools.thy +++ b/lib/NICTATools.thy @@ -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, ("", [])) diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy index 497038b7f..78146b870 100644 --- a/lib/NonDetMonadLemmaBucket.thy +++ b/lib/NonDetMonadLemmaBucket.thy @@ -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="\\", folded validE_R_def] lemma hoare_vcg_if_lift2: diff --git a/lib/Rule_By_Method.thy b/lib/Rule_By_Method.thy index 70fc66a84..b2374df57 100644 --- a/lib/Rule_By_Method.thy +++ b/lib/Rule_By_Method.thy @@ -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 diff --git a/lib/SplitRule.thy b/lib/SplitRule.thy index a79a3c259..4192991a2 100644 --- a/lib/SplitRule.thy +++ b/lib/SplitRule.thy @@ -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; diff --git a/lib/Strengthen.thy b/lib/Strengthen.thy index d4a68dfff..4ebb1ac08 100644 --- a/lib/Strengthen.thy +++ b/lib/Strengthen.thy @@ -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 = diff --git a/lib/SubMonadLib.thy b/lib/SubMonadLib.thy index 3cdabbbb4..adb31136b 100644 --- a/lib/SubMonadLib.thy +++ b/lib/SubMonadLib.thy @@ -66,7 +66,7 @@ lemma select_f_walk: assumes S: "fst S = {} \ snd S" shows "(do a \ m1; b \ select_f S; m2 a b od) = (do b \ select_f S; a \ 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 diff --git a/lib/WhileLoopRules.thy b/lib/WhileLoopRules.thy index 8a42bd947..fca5aa381 100644 --- a/lib/WhileLoopRules.thy +++ b/lib/WhileLoopRules.thy @@ -209,8 +209,8 @@ lemma whileLoop_results_induct_lemma3 [consumes 1]: and inv_start: "I r s" and inv_step: "\r s r' s'. \ I r s; C r s; (r', s') \ fst (B r s) \ \ 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 diff --git a/lib/crunch-cmd.ML b/lib/crunch-cmd.ML index 6012f92b1..38b91651c 100644 --- a/lib/crunch-cmd.ML +++ b/lib/crunch-cmd.ML @@ -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 diff --git a/lib/subgoal_focus/Subgoal_Focus.thy b/lib/subgoal_focus/Subgoal_Focus.thy deleted file mode 100644 index 4294fe7ba..000000000 --- a/lib/subgoal_focus/Subgoal_Focus.thy +++ /dev/null @@ -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 \ -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 "\" => 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; -\ - -end diff --git a/lib/subgoal_focus/Subgoal_Methods.thy b/lib/subgoal_focus/Subgoal_Methods.thy index 723b20b49..c43b1399e 100644 --- a/lib/subgoal_focus/Subgoal_Methods.thy +++ b/lib/subgoal_focus/Subgoal_Methods.thy @@ -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; \ diff --git a/lib/wp/NonDetMonadVCG.thy b/lib/wp/NonDetMonadVCG.thy index b6e6300b9..8cae0c34a 100644 --- a/lib/wp/NonDetMonadVCG.thy +++ b/lib/wp/NonDetMonadVCG.thy @@ -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: "\?Q\ (if A then returnOk else K fail) x \P\,\E\" +schematic_goal if_apply_test: "\?Q\ (if A then returnOk else K fail) x \P\,\E\" apply (wp | unfold K_def)+ done diff --git a/lib/wp/WPC.thy b/lib/wp/WPC.thy index 55b2bce90..48a3f0ef3 100644 --- a/lib/wp/WPC.thy +++ b/lib/wp/WPC.thy @@ -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; diff --git a/lib/wp/WPEx.thy b/lib/wp/WPEx.thy index b542224f4..2c1c8f393 100644 --- a/lib/wp/WPEx.thy +++ b/lib/wp/WPEx.thy @@ -67,12 +67,12 @@ lemma del_asm_rule: "\ PROP P; PROP Q \ \ PROP Q" by assumption -ML {* +ML \ -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; -*} +\ 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 diff --git a/lib/wp/WPI.thy b/lib/wp/WPI.thy index 46b885023..c8f63dc90 100644 --- a/lib/wp/WPI.thy +++ b/lib/wp/WPI.thy @@ -43,12 +43,12 @@ begin text \The ML version of repeat_new is slightly faster than the Eisbach one.\ method_setup repeat_new = - \Method_Closure.parse_method >> (fn m => fn ctxt => fn facts => + \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) \ @@ -264,7 +264,7 @@ private method_setup shared_frees = \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 )))\ private method uses_arg for C :: "'a \ 'b \ bool" = diff --git a/proof/invariant-abstract/Include_AI.thy b/proof/invariant-abstract/Include_AI.thy index 3b82cb18a..edc14501b 100644 --- a/proof/invariant-abstract/Include_AI.thy +++ b/proof/invariant-abstract/Include_AI.thy @@ -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