src/Tools/induct.ML
changeset 45014 0e847655b2d8
parent 44942 a05ab4d803f2
child 45130 563caf031b50
     1.1 --- a/src/Tools/induct.ML	Tue Sep 20 01:32:04 2011 +0200
     1.2 +++ b/src/Tools/induct.ML	Tue Sep 20 05:47:11 2011 +0200
     1.3 @@ -74,11 +74,21 @@
     1.4    val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
     1.5      thm list -> int -> cases_tactic
     1.6    val get_inductT: Proof.context -> term option list list -> thm list list
     1.7 +  type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
     1.8 +  val gen_induct_tac: (theory -> case_data * thm -> case_data * thm) ->
     1.9 +    Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    1.10 +    (string * typ) list list -> term option list -> thm list option ->
    1.11 +    thm list -> int -> cases_tactic
    1.12    val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    1.13      (string * typ) list list -> term option list -> thm list option ->
    1.14      thm list -> int -> cases_tactic
    1.15    val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
    1.16      thm list -> int -> cases_tactic
    1.17 +  val gen_induct_setup: binding ->
    1.18 +   (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    1.19 +    (string * typ) list list -> term option list -> thm list option ->
    1.20 +    thm list -> int -> cases_tactic) ->
    1.21 +   theory -> theory
    1.22    val setup: theory -> theory
    1.23  end;
    1.24  
    1.25 @@ -721,7 +731,9 @@
    1.26  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
    1.27    | get_inductP _ _ = [];
    1.28  
    1.29 -fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts =
    1.30 +type case_data = (((string * string list) * string list) list * int)
    1.31 +
    1.32 +fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
    1.33    let
    1.34      val thy = Proof_Context.theory_of ctxt;
    1.35  
    1.36 @@ -734,6 +746,7 @@
    1.37            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
    1.38          |> maps (prep_inst ctxt align_right (atomize_term thy))
    1.39          |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
    1.40 +      |> mod_cases thy
    1.41        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    1.42  
    1.43      val ruleq =
    1.44 @@ -791,7 +804,7 @@
    1.45         THEN_ALL_NEW rulify_tac)
    1.46    end;
    1.47  
    1.48 -
    1.49 +val induct_tac = gen_induct_tac (K I);
    1.50  
    1.51  (** coinduct method **)
    1.52  
    1.53 @@ -910,16 +923,18 @@
    1.54            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
    1.55      "case analysis on types or predicates/sets";
    1.56  
    1.57 -val induct_setup =
    1.58 -  Method.setup @{binding induct}
    1.59 +fun gen_induct_setup binding itac =
    1.60 +  Method.setup binding
    1.61      (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.62        (arbitrary -- taking -- Scan.option induct_rule)) >>
    1.63        (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
    1.64          RAW_METHOD_CASES (fn facts =>
    1.65            Seq.DETERM
    1.66 -            (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
    1.67 +            (HEADGOAL (itac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
    1.68      "induction on types or predicates/sets";
    1.69  
    1.70 +val induct_setup = gen_induct_setup @{binding induct} induct_tac;
    1.71 +
    1.72  val coinduct_setup =
    1.73    Method.setup @{binding coinduct}
    1.74      (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>