simplified type Proof.method;
authorwenzelm
Tue Aug 19 12:05:11 2014 +0200 (2014-08-19)
changeset 580020ed1e999a0fb
parent 58001 934d85f14d1d
child 58003 250ecd2502ad
simplified type Proof.method;
src/HOL/Fun_Def.thy
src/HOL/Nominal/nominal_induct.ML
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/Tools/induct.ML
     1.1 --- a/src/HOL/Fun_Def.thy	Mon Aug 18 15:46:27 2014 +0200
     1.2 +++ b/src/HOL/Fun_Def.thy	Tue Aug 19 12:05:11 2014 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  ML_file "Tools/Function/induction_schema.ML"
     1.5  
     1.6  method_setup induction_schema = {*
     1.7 -  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
     1.8 +  Scan.succeed (NO_CASES oo Induction_Schema.induction_schema_tac)
     1.9  *} "prove an induction principle"
    1.10  
    1.11  setup {*
     2.1 --- a/src/HOL/Nominal/nominal_induct.ML	Mon Aug 18 15:46:27 2014 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Aug 19 12:05:11 2014 +0200
     2.3 @@ -172,9 +172,8 @@
     2.4    Scan.lift (Args.mode Induct.no_simpN) --
     2.5    (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
     2.6      avoiding -- fixing -- rule_spec) >>
     2.7 -  (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
     2.8 -    RAW_METHOD_CASES (fn facts =>
     2.9 -      HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));
    2.10 +  (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
    2.11 +    HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
    2.12  
    2.13  end;
    2.14  
     3.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Mon Aug 18 15:46:27 2014 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Aug 19 12:05:11 2014 +0200
     3.3 @@ -373,9 +373,10 @@
     3.4            |> snd
     3.5          end)
     3.6        [goals] |>
     3.7 -    Proof.apply (Method.Basic (fn ctxt => RAW_METHOD (fn _ =>
     3.8 -      rewrite_goals_tac ctxt defs_thms THEN
     3.9 -      compose_tac (false, rule, length rule_prems) 1))) |>
    3.10 +    Proof.apply (Method.Basic (fn ctxt => fn _ =>
    3.11 +      NO_CASES
    3.12 +       (rewrite_goals_tac ctxt defs_thms THEN
    3.13 +        compose_tac (false, rule, length rule_prems) 1))) |>
    3.14      Seq.hd
    3.15    end;
    3.16  
     4.1 --- a/src/HOL/Tools/coinduction.ML	Mon Aug 18 15:46:27 2014 +0200
     4.2 +++ b/src/HOL/Tools/coinduction.ML	Tue Aug 19 12:05:11 2014 +0200
     4.3 @@ -149,9 +149,8 @@
     4.4  val setup =
     4.5    Method.setup @{binding coinduction}
     4.6      (arbitrary -- Scan.option coinduct_rule >>
     4.7 -      (fn (arbitrary, opt_rule) => fn ctxt =>
     4.8 -        RAW_METHOD_CASES (fn facts =>
     4.9 -          Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts))))
    4.10 +      (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
    4.11 +        Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
    4.12      "coinduction on types or predicates/sets";
    4.13  
    4.14  end;
     5.1 --- a/src/Pure/Isar/element.ML	Mon Aug 18 15:46:27 2014 +0200
     5.2 +++ b/src/Pure/Isar/element.ML	Tue Aug 19 12:05:11 2014 +0200
     5.3 @@ -270,8 +270,8 @@
     5.4  local
     5.5  
     5.6  val refine_witness =
     5.7 -  Proof.refine (Method.Basic (K (RAW_METHOD
     5.8 -    (K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI))))))))));
     5.9 +  Proof.refine (Method.Basic (K (NO_CASES o
    5.10 +    K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI)))))))));
    5.11  
    5.12  fun gen_witness_proof proof after_qed wit_propss eq_props =
    5.13    let
     6.1 --- a/src/Pure/Isar/method.ML	Mon Aug 18 15:46:27 2014 +0200
     6.2 +++ b/src/Pure/Isar/method.ML	Tue Aug 19 12:05:11 2014 +0200
     6.3 @@ -6,10 +6,7 @@
     6.4  
     6.5  signature METHOD =
     6.6  sig
     6.7 -  type method
     6.8 -  val apply: (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
     6.9 -  val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
    6.10 -  val RAW_METHOD: (thm list -> tactic) -> method
    6.11 +  type method = thm list -> cases_tactic
    6.12    val METHOD_CASES: (thm list -> cases_tactic) -> method
    6.13    val METHOD: (thm list -> tactic) -> method
    6.14    val fail: method
    6.15 @@ -90,18 +87,10 @@
    6.16  
    6.17  (* datatype method *)
    6.18  
    6.19 -datatype method = Meth of thm list -> cases_tactic;
    6.20 -
    6.21 -fun apply meth ctxt = let val Meth m = meth ctxt in m end;
    6.22 -
    6.23 -val RAW_METHOD_CASES = Meth;
    6.24 +type method = thm list -> cases_tactic;
    6.25  
    6.26 -fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
    6.27 -
    6.28 -fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts =>
    6.29 -  Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts));
    6.30 -
    6.31 -fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Goal.conjunction_tac THEN tac facts);
    6.32 +fun METHOD_CASES tac facts = Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
    6.33 +fun METHOD tac facts = NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
    6.34  
    6.35  val fail = METHOD (K no_tac);
    6.36  val succeed = METHOD (K all_tac);
    6.37 @@ -154,7 +143,7 @@
    6.38  fun atomize false ctxt =
    6.39        SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
    6.40    | atomize true ctxt =
    6.41 -      RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)));
    6.42 +      NO_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
    6.43  
    6.44  
    6.45  (* this -- resolve facts directly *)
    6.46 @@ -277,7 +266,7 @@
    6.47    in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end;
    6.48  
    6.49  fun tactic source ctxt = METHOD (ml_tactic source ctxt);
    6.50 -fun raw_tactic source ctxt = RAW_METHOD (ml_tactic source ctxt);
    6.51 +fun raw_tactic source ctxt = NO_CASES o ml_tactic source ctxt;
    6.52  
    6.53  
    6.54  
    6.55 @@ -376,7 +365,7 @@
    6.56      val (src1, meth) = check_src ctxt0 src0;
    6.57      val src2 = Args.init_assignable src1;
    6.58      val ctxt = Context_Position.not_really ctxt0;
    6.59 -    val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
    6.60 +    val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm));
    6.61    in Args.closure src2 end;
    6.62  
    6.63  fun method_cmd ctxt = method ctxt o method_closure ctxt;
    6.64 @@ -553,8 +542,6 @@
    6.65  
    6.66  end;
    6.67  
    6.68 -val RAW_METHOD_CASES = Method.RAW_METHOD_CASES;
    6.69 -val RAW_METHOD = Method.RAW_METHOD;
    6.70  val METHOD_CASES = Method.METHOD_CASES;
    6.71  val METHOD = Method.METHOD;
    6.72  val SIMPLE_METHOD = Method.SIMPLE_METHOD;
     7.1 --- a/src/Pure/Isar/proof.ML	Mon Aug 18 15:46:27 2014 +0200
     7.2 +++ b/src/Pure/Isar/proof.ML	Tue Aug 19 12:05:11 2014 +0200
     7.3 @@ -401,7 +401,7 @@
     7.4        find_goal state;
     7.5      val ctxt = if current_context then context_of state else goal_ctxt;
     7.6    in
     7.7 -    Method.apply method ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
     7.8 +    method ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
     7.9        state
    7.10        |> map_goal
    7.11            (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
    7.12 @@ -892,9 +892,9 @@
    7.13    in map (Logic.mk_term o Var) vars end;
    7.14  
    7.15  fun refine_terms n =
    7.16 -  refine (Method.Basic (K (RAW_METHOD
    7.17 -    (K (HEADGOAL (PRECISE_CONJUNCTS n
    7.18 -      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))))
    7.19 +  refine (Method.Basic (K (NO_CASES o
    7.20 +    K (HEADGOAL (PRECISE_CONJUNCTS n
    7.21 +      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))
    7.22    #> Seq.hd;
    7.23  
    7.24  in
     8.1 --- a/src/Tools/induct.ML	Mon Aug 18 15:46:27 2014 +0200
     8.2 +++ b/src/Tools/induct.ML	Tue Aug 19 12:05:11 2014 +0200
     8.3 @@ -932,15 +932,13 @@
     8.4            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
     8.5      "case analysis on types or predicates/sets";
     8.6  
     8.7 -fun gen_induct_setup binding itac =
     8.8 +fun gen_induct_setup binding tac =
     8.9    Method.setup binding
    8.10      (Scan.lift (Args.mode no_simpN) --
    8.11        (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
    8.12          (arbitrary -- taking -- Scan.option induct_rule)) >>
    8.13 -      (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
    8.14 -        RAW_METHOD_CASES (fn facts =>
    8.15 -          Seq.DETERM
    8.16 -            (HEADGOAL (itac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
    8.17 +      (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt => fn facts =>
    8.18 +        Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
    8.19      "induction on types or predicates/sets";
    8.20  
    8.21  val induct_setup = gen_induct_setup @{binding induct} induct_tac;
    8.22 @@ -948,9 +946,8 @@
    8.23  val coinduct_setup =
    8.24    Method.setup @{binding coinduct}
    8.25      (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
    8.26 -      (fn ((insts, taking), opt_rule) => fn ctxt =>
    8.27 -        RAW_METHOD_CASES (fn facts =>
    8.28 -          Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))))
    8.29 +      (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
    8.30 +        Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
    8.31      "coinduction on types or predicates/sets";
    8.32  
    8.33  end;