# HG changeset patch # User wenzelm # Date 1565684841 -7200 # Node ID 11d8517d9384d9fc8c9e7b5b7675d86ad8d9f754 # Parent 67580f2ded908d146f3b8d9a9da4eeb828834c36 clarified modules; diff -r 67580f2ded90 -r 11d8517d9384 src/HOL/Eisbach/Eisbach.thy --- 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)))))\ ML \fun method_evaluate text ctxt facts = - Method.NO_CONTEXT_TACTIC ctxt + NO_CONTEXT_TACTIC ctxt (Method.evaluate_runtime text ctxt facts)\ method_setup timeit = diff -r 67580f2ded90 -r 11d8517d9384 src/HOL/Fun_Def.thy --- 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 \Tools/Function/induction_schema.ML\ method_setup induction_schema = \ - Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac) + Scan.succeed (CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac) \ "prove an induction principle" diff -r 67580f2ded90 -r 11d8517d9384 src/HOL/Nominal/nominal_primrec.ML --- 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; diff -r 67580f2ded90 -r 11d8517d9384 src/HOL/Tools/coinduction.ML --- 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 diff -r 67580f2ded90 -r 11d8517d9384 src/Pure/Isar/element.ML --- 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 = diff -r 67580f2ded90 -r 11d8517d9384 src/Pure/Isar/method.ML --- 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>\tactic\ (parse_tactic >> (K o METHOD)) "ML tactic as proof method" #> - setup \<^binding>\raw_tactic\ (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac)) + setup \<^binding>\raw_tactic\ (parse_tactic >> (fn tac => fn _ => Context_Tactic.CONTEXT_TACTIC o tac)) "ML tactic as raw proof method" #> setup \<^binding>\use\ (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; diff -r 67580f2ded90 -r 11d8517d9384 src/Pure/Isar/proof.ML --- 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])))))))); diff -r 67580f2ded90 -r 11d8517d9384 src/Pure/ROOT.ML --- 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"; diff -r 67580f2ded90 -r 11d8517d9384 src/Pure/context_tactic.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; diff -r 67580f2ded90 -r 11d8517d9384 src/Tools/induct.ML --- 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; diff -r 67580f2ded90 -r 11d8517d9384 src/Tools/induction.ML --- 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>\induction\ induction_context_tactic);