clarified modules;
authorwenzelm
Tue, 13 Aug 2019 10:27:21 +0200
changeset 70706 11d8517d9384
parent 70705 67580f2ded90
child 70707 9ddd66d53130
clarified modules;
src/HOL/Eisbach/Eisbach.thy
src/HOL/Fun_Def.thy
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/coinduction.ML
src/Pure/Isar/element.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/ROOT.ML
src/Pure/context_tactic.ML
src/Tools/induct.ML
src/Tools/induction.ML
--- 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);