--- a/src/HOL/Eisbach/Eisbach.thy Mon Aug 12 21:22:40 2019 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Tue Aug 13 10:27:21 2019 +0200
@@ -41,7 +41,7 @@
(Seq.make_results (Seq.single (ctxt', thm)))))\<close>
ML \<open>fun method_evaluate text ctxt facts =
- Method.NO_CONTEXT_TACTIC ctxt
+ NO_CONTEXT_TACTIC ctxt
(Method.evaluate_runtime text ctxt facts)\<close>
method_setup timeit =
--- a/src/HOL/Fun_Def.thy Mon Aug 12 21:22:40 2019 +0200
+++ b/src/HOL/Fun_Def.thy Tue Aug 13 10:27:21 2019 +0200
@@ -98,7 +98,7 @@
ML_file \<open>Tools/Function/induction_schema.ML\<close>
method_setup induction_schema = \<open>
- Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac)
+ Scan.succeed (CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac)
\<close> "prove an induction principle"
--- a/src/HOL/Nominal/nominal_primrec.ML Mon Aug 12 21:22:40 2019 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Aug 13 10:27:21 2019 +0200
@@ -373,7 +373,7 @@
end)
[goals] |>
Proof.refine_singleton (Method.Basic (fn ctxt => fn _ =>
- Method.CONTEXT_TACTIC
+ CONTEXT_TACTIC
(rewrite_goals_tac ctxt defs_thms THEN
compose_tac ctxt (false, rule, length rule_prems) 1)))
end;
--- a/src/HOL/Tools/coinduction.ML Mon Aug 12 21:22:40 2019 +0200
+++ b/src/HOL/Tools/coinduction.ML Tue Aug 13 10:27:21 2019 +0200
@@ -125,7 +125,7 @@
end);
fun coinduction_tac ctxt x1 x2 x3 x4 =
- Method.NO_CONTEXT_TACTIC ctxt (coinduction_context_tactic x1 x2 x3 x4);
+ NO_CONTEXT_TACTIC ctxt (coinduction_context_tactic x1 x2 x3 x4);
local
--- a/src/Pure/Isar/element.ML Mon Aug 12 21:22:40 2019 +0200
+++ b/src/Pure/Isar/element.ML Tue Aug 13 10:27:21 2019 +0200
@@ -281,7 +281,7 @@
local
val refine_witness =
- Proof.refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
+ Proof.refine_singleton (Method.Basic (fn ctxt => CONTEXT_TACTIC o
K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac ctxt [Drule.protectI]))))))));
fun gen_witness_proof proof after_qed wit_propss eq_props =
--- a/src/Pure/Isar/method.ML Mon Aug 12 21:22:40 2019 +0200
+++ b/src/Pure/Isar/method.ML Tue Aug 13 10:27:21 2019 +0200
@@ -4,24 +4,9 @@
Isar proof methods.
*)
-infix 1 CONTEXT_THEN_ALL_NEW;
-
-signature BASIC_METHOD =
-sig
- type context_state = Proof.context * thm
- type context_tactic = context_state -> context_state Seq.result Seq.seq
- val CONTEXT_CASES: Rule_Cases.cases -> tactic -> context_tactic
- val CONTEXT_SUBGOAL: (term * int -> context_tactic) -> int -> context_tactic
- val CONTEXT_THEN_ALL_NEW: (int -> context_tactic) * (int -> tactic) -> int -> context_tactic
-end;
-
signature METHOD =
sig
- include BASIC_METHOD
type method = thm list -> context_tactic
- val CONTEXT: Proof.context -> thm Seq.seq -> context_state Seq.result Seq.seq
- val CONTEXT_TACTIC: tactic -> context_tactic
- val NO_CONTEXT_TACTIC: Proof.context -> context_tactic -> tactic
val CONTEXT_METHOD: (thm list -> context_tactic) -> method
val METHOD: (thm list -> tactic) -> method
val fail: method
@@ -115,35 +100,6 @@
(** proof methods **)
-(* tactics with proof context / cases *)
-
-type context_state = Proof.context * thm;
-type context_tactic = context_state -> context_state Seq.result Seq.seq;
-
-fun CONTEXT ctxt : thm Seq.seq -> context_state Seq.result Seq.seq =
- Seq.map (Seq.Result o pair ctxt);
-
-fun CONTEXT_TACTIC tac : context_tactic =
- fn (ctxt, st) => CONTEXT ctxt (tac st);
-
-fun NO_CONTEXT_TACTIC ctxt (tac: context_tactic) st =
- tac (ctxt, st) |> Seq.filter_results |> Seq.map snd;
-
-fun CONTEXT_CASES cases tac : context_tactic =
- fn (ctxt, st) => CONTEXT (Proof_Context.update_cases cases ctxt) (tac st);
-
-fun CONTEXT_SUBGOAL tac i : context_tactic =
- fn (ctxt, st) =>
- (case try Logic.nth_prem (i, Thm.prop_of st) of
- SOME goal => tac (goal, i) (ctxt, st)
- | NONE => Seq.empty);
-
-fun (tac1 CONTEXT_THEN_ALL_NEW tac2) i : context_tactic =
- fn (ctxt, st) =>
- (ctxt, st) |> tac1 i |> Seq.maps_results (fn (ctxt', st') =>
- CONTEXT ctxt' ((Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st'));
-
-
(* type method *)
type method = thm list -> context_tactic;
@@ -165,16 +121,17 @@
EVERY (map (fn r => resolve_tac ctxt [Drule.forall_intr_vars r COMP_INCR revcut_rl] i) facts);
fun insert thms =
- CONTEXT_METHOD (fn _ => fn (ctxt, st) => st |> ALLGOALS (insert_tac ctxt thms) |> CONTEXT ctxt);
+ CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
+ st |> ALLGOALS (insert_tac ctxt thms) |> TACTIC_CONTEXT ctxt);
fun SIMPLE_METHOD tac =
CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
- st |> (ALLGOALS (insert_tac ctxt facts) THEN tac) |> CONTEXT ctxt);
+ st |> (ALLGOALS (insert_tac ctxt facts) THEN tac) |> TACTIC_CONTEXT ctxt);
fun SIMPLE_METHOD'' quant tac =
CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
- st |> quant (insert_tac ctxt facts THEN' tac) |> CONTEXT ctxt);
+ st |> quant (insert_tac ctxt facts THEN' tac) |> TACTIC_CONTEXT ctxt);
val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL;
@@ -195,7 +152,7 @@
fun cheating int = CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
if int orelse Config.get ctxt quick_and_dirty then
- CONTEXT ctxt (ALLGOALS (Skip_Proof.cheat_tac ctxt) st)
+ TACTIC_CONTEXT ctxt (ALLGOALS (Skip_Proof.cheat_tac ctxt) st)
else error "Cheating requires quick_and_dirty mode!");
@@ -216,7 +173,8 @@
fun atomize false ctxt =
SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
| atomize true ctxt =
- CONTEXT_TACTIC o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
+ Context_Tactic.CONTEXT_TACTIC o
+ K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
(* this -- resolve facts directly *)
@@ -530,7 +488,7 @@
fn result =>
(case result of
Seq.Error _ => Seq.single result
- | Seq.Result (ctxt, st) => tac st |> CONTEXT ctxt);
+ | Seq.Result (ctxt, st) => tac st |> TACTIC_CONTEXT ctxt);
val preparation = BYPASS_CONTEXT (ALLGOALS Goal.conjunction_tac);
@@ -839,7 +797,7 @@
"rotate assumptions of goal" #>
setup \<^binding>\<open>tactic\<close> (parse_tactic >> (K o METHOD))
"ML tactic as proof method" #>
- setup \<^binding>\<open>raw_tactic\<close> (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac))
+ setup \<^binding>\<open>raw_tactic\<close> (parse_tactic >> (fn tac => fn _ => Context_Tactic.CONTEXT_TACTIC o tac))
"ML tactic as raw proof method" #>
setup \<^binding>\<open>use\<close>
(Attrib.thms -- (Scan.lift (Parse.$$$ "in") |-- text_closure) >>
@@ -853,9 +811,6 @@
end;
-structure Basic_Method: BASIC_METHOD = Method;
-open Basic_Method;
-
val CONTEXT_METHOD = Method.CONTEXT_METHOD;
val METHOD = Method.METHOD;
val SIMPLE_METHOD = Method.SIMPLE_METHOD;
--- a/src/Pure/Isar/proof.ML Mon Aug 12 21:22:40 2019 +0200
+++ b/src/Pure/Isar/proof.ML Tue Aug 13 10:27:21 2019 +0200
@@ -432,7 +432,7 @@
refine_singleton (Method.Basic (K (Method.insert ths)));
fun refine_primitive r =
- refine_singleton (Method.Basic (fn ctxt => fn _ => Method.CONTEXT_TACTIC (PRIMITIVE (r ctxt))));
+ refine_singleton (Method.Basic (fn ctxt => fn _ => CONTEXT_TACTIC (PRIMITIVE (r ctxt))));
end;
@@ -973,7 +973,7 @@
in map (Logic.mk_term o Var) vars end;
fun refine_terms n =
- refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
+ refine_singleton (Method.Basic (fn ctxt => CONTEXT_TACTIC o
K (HEADGOAL (PRECISE_CONJUNCTS n
(HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))));
--- a/src/Pure/ROOT.ML Mon Aug 12 21:22:40 2019 +0200
+++ b/src/Pure/ROOT.ML Tue Aug 13 10:27:21 2019 +0200
@@ -243,6 +243,7 @@
section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";
(*basic proof engine*)
+ML_file "context_tactic.ML";
ML_file "par_tactical.ML";
ML_file "Isar/proof_display.ML";
ML_file "Isar/attrib.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/context_tactic.ML Tue Aug 13 10:27:21 2019 +0200
@@ -0,0 +1,58 @@
+(* Title: Pure/context_tactic.ML
+ Author: Makarius
+
+Tactics with proof context / cases -- as basis for Isar proof methods.
+*)
+
+infix 1 CONTEXT_THEN_ALL_NEW;
+
+signature BASIC_CONTEXT_TACTIC =
+sig
+ type context_state = Proof.context * thm
+ type context_tactic = context_state -> context_state Seq.result Seq.seq
+ val TACTIC_CONTEXT: Proof.context -> thm Seq.seq -> context_state Seq.result Seq.seq
+ val CONTEXT_TACTIC: tactic -> context_tactic
+ val NO_CONTEXT_TACTIC: Proof.context -> context_tactic -> tactic
+ val CONTEXT_CASES: Rule_Cases.cases -> tactic -> context_tactic
+ val CONTEXT_SUBGOAL: (term * int -> context_tactic) -> int -> context_tactic
+ val CONTEXT_THEN_ALL_NEW: (int -> context_tactic) * (int -> tactic) -> int -> context_tactic
+end;
+
+signature CONTEXT_TACTIC =
+sig
+ include BASIC_CONTEXT_TACTIC
+end;
+
+structure Context_Tactic: CONTEXT_TACTIC =
+struct
+
+type context_state = Proof.context * thm;
+type context_tactic = context_state -> context_state Seq.result Seq.seq;
+
+fun TACTIC_CONTEXT ctxt : thm Seq.seq -> context_state Seq.result Seq.seq =
+ Seq.map (Seq.Result o pair ctxt);
+
+fun CONTEXT_TACTIC tac : context_tactic =
+ fn (ctxt, st) => TACTIC_CONTEXT ctxt (tac st);
+
+fun NO_CONTEXT_TACTIC ctxt (tac: context_tactic) st =
+ tac (ctxt, st) |> Seq.filter_results |> Seq.map snd;
+
+fun CONTEXT_CASES cases tac : context_tactic =
+ fn (ctxt, st) => TACTIC_CONTEXT (Proof_Context.update_cases cases ctxt) (tac st);
+
+fun CONTEXT_SUBGOAL tac i : context_tactic =
+ fn (ctxt, st) =>
+ (case try Logic.nth_prem (i, Thm.prop_of st) of
+ SOME goal => tac (goal, i) (ctxt, st)
+ | NONE => Seq.empty);
+
+fun (tac1 CONTEXT_THEN_ALL_NEW tac2) i : context_tactic =
+ fn (ctxt, st) =>
+ (ctxt, st) |> tac1 i |> Seq.maps_results (fn (ctxt', st') =>
+ TACTIC_CONTEXT ctxt' ((Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st'));
+
+end;
+
+structure Basic_Context_Tactic: BASIC_CONTEXT_TACTIC = Context_Tactic;
+open Basic_Context_Tactic;
--- a/src/Tools/induct.ML Mon Aug 12 21:22:40 2019 +0200
+++ b/src/Tools/induct.ML Tue Aug 13 10:27:21 2019 +0200
@@ -535,7 +535,7 @@
end;
fun cases_tac ctxt x1 x2 x3 x4 x5 =
- Method.NO_CONTEXT_TACTIC ctxt (cases_context_tactic x1 x2 x3 x4 x5);
+ NO_CONTEXT_TACTIC ctxt (cases_context_tactic x1 x2 x3 x4 x5);
end;
@@ -828,10 +828,10 @@
val induct_context_tactic = gen_induct_context_tactic I;
fun gen_induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 x8 =
- Method.NO_CONTEXT_TACTIC ctxt (gen_induct_context_tactic x1 x2 x3 x4 x5 x6 x7 x8);
+ NO_CONTEXT_TACTIC ctxt (gen_induct_context_tactic x1 x2 x3 x4 x5 x6 x7 x8);
fun induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
- Method.NO_CONTEXT_TACTIC ctxt (induct_context_tactic x1 x2 x3 x4 x5 x6 x7);
+ NO_CONTEXT_TACTIC ctxt (induct_context_tactic x1 x2 x3 x4 x5 x6 x7);
@@ -882,7 +882,7 @@
end);
fun coinduct_tac ctxt x1 x2 x3 x4 x5 =
- Method.NO_CONTEXT_TACTIC ctxt (coinduct_context_tactic x1 x2 x3 x4 x5);
+ NO_CONTEXT_TACTIC ctxt (coinduct_context_tactic x1 x2 x3 x4 x5);
end;
--- a/src/Tools/induction.ML Mon Aug 12 21:22:40 2019 +0200
+++ b/src/Tools/induction.ML Tue Aug 13 10:27:21 2019 +0200
@@ -47,7 +47,7 @@
in ((cases', consumes), th) end);
fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
- Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
+ NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
val _ =
Theory.local_setup (Induct.gen_induct_setup \<^binding>\<open>induction\<close> induction_context_tactic);