moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
authorwenzelm
Thu Oct 04 14:42:47 2007 +0200 (2007-10-04)
changeset 24830a7b3ab44d993
parent 24829 e1214fa781ca
child 24831 887d1b32a1a5
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/FOL/IsaMakefile
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
src/Provers/induct_method.ML
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Tools/induct.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/FOL/FOL.thy	Thu Oct 04 14:42:11 2007 +0200
     1.2 +++ b/src/FOL/FOL.thy	Thu Oct 04 14:42:47 2007 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    "~~/src/Provers/classical.ML"
     1.5    "~~/src/Provers/blast.ML"
     1.6    "~~/src/Provers/clasimp.ML"
     1.7 +  "~~/src/Tools/induct.ML"
     1.8    ("cladata.ML")
     1.9    ("blastdata.ML")
    1.10    ("simpdata.ML")
    1.11 @@ -74,7 +75,7 @@
    1.12    apply (erule r1)
    1.13    done
    1.14  
    1.15 -lemmas case_split = case_split_thm [case_names True False, cases type: o]
    1.16 +lemmas case_split = case_split_thm [case_names True False]
    1.17  
    1.18  (*HOL's more natural case analysis tactic*)
    1.19  ML {*
    1.20 @@ -273,15 +274,16 @@
    1.21  text {* Method setup. *}
    1.22  
    1.23  ML {*
    1.24 -  structure InductMethod = InductMethodFun
    1.25 -  (struct
    1.26 +  structure Induct = InductFun
    1.27 +  (
    1.28      val cases_default = @{thm case_split}
    1.29      val atomize = @{thms induct_atomize}
    1.30      val rulify = @{thms induct_rulify}
    1.31      val rulify_fallback = @{thms induct_rulify_fallback}
    1.32 -  end);
    1.33 +  );
    1.34  *}
    1.35  
    1.36 -setup InductMethod.setup
    1.37 +setup Induct.setup
    1.38 +declare case_split [cases type: o]
    1.39  
    1.40  end
     2.1 --- a/src/FOL/IFOL.thy	Thu Oct 04 14:42:11 2007 +0200
     2.2 +++ b/src/FOL/IFOL.thy	Thu Oct 04 14:42:47 2007 +0200
     2.3 @@ -15,7 +15,6 @@
     2.4    "~~/src/Tools/IsaPlanner/rw_tools.ML"
     2.5    "~~/src/Tools/IsaPlanner/rw_inst.ML"
     2.6    "~~/src/Provers/eqsubst.ML"
     2.7 -  "~~/src/Provers/induct_method.ML"
     2.8    "~~/src/Provers/quantifier1.ML"
     2.9    "~~/src/Provers/project_rule.ML"
    2.10    ("fologic.ML")
     3.1 --- a/src/FOL/IsaMakefile	Thu Oct 04 14:42:11 2007 +0200
     3.2 +++ b/src/FOL/IsaMakefile	Thu Oct 04 14:42:47 2007 +0200
     3.3 @@ -35,7 +35,7 @@
     3.4    $(SRC)/Tools/IsaPlanner/rw_tools.ML	\
     3.5    $(SRC)/Tools/IsaPlanner/rw_inst.ML \
     3.6    $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
     3.7 -  $(SRC)/Provers/induct_method.ML			\
     3.8 +  $(SRC)/Tools/induct.ML			\
     3.9    $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
    3.10    $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML cladata.ML 		\
    3.11    document/root.tex fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
     4.1 --- a/src/HOL/HOL.thy	Thu Oct 04 14:42:11 2007 +0200
     4.2 +++ b/src/HOL/HOL.thy	Thu Oct 04 14:42:47 2007 +0200
     4.3 @@ -14,7 +14,6 @@
     4.4    "~~/src/Tools/IsaPlanner/rw_tools.ML"
     4.5    "~~/src/Tools/IsaPlanner/rw_inst.ML"
     4.6    "~~/src/Provers/project_rule.ML"
     4.7 -  "~~/src/Provers/induct_method.ML"
     4.8    "~~/src/Provers/hypsubst.ML"
     4.9    "~~/src/Provers/splitter.ML"
    4.10    "~~/src/Provers/classical.ML"
    4.11 @@ -29,6 +28,7 @@
    4.12    "~~/src/Tools/code/code_target.ML"
    4.13    "~~/src/Tools/code/code_package.ML"
    4.14    "~~/src/Tools/nbe.ML"
    4.15 +  "~~/src/Tools/induct.ML"
    4.16  begin
    4.17  
    4.18  subsection {* Primitive logic *}
    4.19 @@ -1545,17 +1545,16 @@
    4.20  text {* Method setup. *}
    4.21  
    4.22  ML {*
    4.23 -  structure InductMethod = InductMethodFun
    4.24 -  (struct
    4.25 +  structure Induct = InductFun
    4.26 +  (
    4.27      val cases_default = @{thm case_split}
    4.28      val atomize = @{thms induct_atomize}
    4.29      val rulify = @{thms induct_rulify}
    4.30      val rulify_fallback = @{thms induct_rulify_fallback}
    4.31 -  end);
    4.32 +  );
    4.33  *}
    4.34  
    4.35 -setup InductMethod.setup
    4.36 -
    4.37 +setup Induct.setup
    4.38  
    4.39  
    4.40  subsection {* Other simple lemmas and lemma duplicates *}
    4.41 @@ -1711,7 +1710,7 @@
    4.42  val all_conj_distrib = thm "all_conj_distrib";
    4.43  val all_simps = thms "all_simps";
    4.44  val atomize_not = thm "atomize_not";
    4.45 -val case_split = thm "case_split_thm";
    4.46 +val case_split = thm "case_split";
    4.47  val case_split_thm = thm "case_split_thm"
    4.48  val cases_simp = thm "cases_simp";
    4.49  val choice_eq = thm "choice_eq"
     5.1 --- a/src/HOL/IsaMakefile	Thu Oct 04 14:42:11 2007 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Thu Oct 04 14:42:47 2007 +0200
     5.3 @@ -79,10 +79,10 @@
     5.4    $(SRC)/Tools/IsaPlanner/isand.ML					\
     5.5    $(SRC)/Tools/IsaPlanner/rw_inst.ML					\
     5.6    $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
     5.7 -  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML		\
     5.8 +  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/induct.ML $(SRC)/Provers/blast.ML		\
     5.9    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
    5.10    $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
    5.11 -  $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML		\
    5.12 +  $(SRC)/Provers/order.ML		\
    5.13    $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
    5.14    $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML			\
    5.15    $(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML\
     6.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Oct 04 14:42:11 2007 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Oct 04 14:42:47 2007 +0200
     6.3 @@ -43,7 +43,7 @@
     6.4  
     6.5      fun subst inst concl =
     6.6        let
     6.7 -        val vars = InductAttrib.vars_of concl;
     6.8 +        val vars = Induct.vars_of concl;
     6.9          val m = length vars and n = length inst;
    6.10          val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
    6.11          val P :: x :: ys = vars;
    6.12 @@ -87,13 +87,13 @@
    6.13      val thy = ProofContext.theory_of ctxt;
    6.14      val cert = Thm.cterm_of thy;
    6.15  
    6.16 -    val ((insts, defs), defs_ctxt) = fold_map InductMethod.add_defs def_insts ctxt |>> split_list;
    6.17 +    val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
    6.18      val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
    6.19  
    6.20      val finish_rule =
    6.21        split_all_tuples
    6.22        #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding);
    6.23 -    fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (InductMethod.rulified_term r);
    6.24 +    fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
    6.25    in
    6.26      (fn i => fn st =>
    6.27        rules
    6.28 @@ -103,18 +103,18 @@
    6.29          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    6.30            (CONJUNCTS (ALLGOALS
    6.31              (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
    6.32 -              THEN' InductMethod.fix_tac defs_ctxt
    6.33 +              THEN' Induct.fix_tac defs_ctxt
    6.34                  (nth concls (j - 1) + more_consumes)
    6.35                  (nth_list fixings (j - 1))))
    6.36 -          THEN' InductMethod.inner_atomize_tac) j))
    6.37 -        THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' =>
    6.38 -            InductMethod.guess_instance
    6.39 -              (finish_rule (InductMethod.internalize more_consumes rule)) i st'
    6.40 +          THEN' Induct.inner_atomize_tac) j))
    6.41 +        THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
    6.42 +            Induct.guess_instance
    6.43 +              (finish_rule (Induct.internalize more_consumes rule)) i st'
    6.44              |> Seq.maps (fn rule' =>
    6.45                CASES (rule_cases rule' cases)
    6.46                  (Tactic.rtac (rename_params_rule false [] rule') i THEN
    6.47                    PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
    6.48 -    THEN_ALL_NEW_CASES InductMethod.rulify_tac
    6.49 +    THEN_ALL_NEW_CASES Induct.rulify_tac
    6.50    end;
    6.51  
    6.52  
     7.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 04 14:42:11 2007 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 04 14:42:47 2007 +0200
     7.3 @@ -148,7 +148,7 @@
     7.4        | xs => error ("Missing equivariance theorem for predicate(s): " ^
     7.5            commas_quote xs));
     7.6      val induct_cases = map fst (fst (RuleCases.get (the
     7.7 -      (InductAttrib.lookup_inductS ctxt (hd names)))));
     7.8 +      (Induct.lookup_inductS ctxt (hd names)))));
     7.9      val raw_induct' = Logic.unvarify (prop_of raw_induct);
    7.10      val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
    7.11        HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
     8.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Oct 04 14:42:11 2007 +0200
     8.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 04 14:42:47 2007 +0200
     8.3 @@ -205,7 +205,7 @@
     8.4    | prep_var _ = NONE;
     8.5  
     8.6  fun prep_inst (concl, xs) = (*exception Library.UnequalLengths*)
     8.7 -  let val vs = InductAttrib.vars_of concl
     8.8 +  let val vs = Induct.vars_of concl
     8.9    in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    8.10  
    8.11  in
    8.12 @@ -340,10 +340,10 @@
    8.13      val inducts = ProjectRule.projections (ProofContext.init thy) induction;
    8.14  
    8.15      fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
    8.16 -      [(("", nth inducts index), [InductAttrib.induct_type name]),
    8.17 -       (("", exhaustion), [InductAttrib.cases_type name])];
    8.18 +      [(("", nth inducts index), [Induct.induct_type name]),
    8.19 +       (("", exhaustion), [Induct.cases_type name])];
    8.20      fun unnamed_rule i =
    8.21 -      (("", nth inducts i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
    8.22 +      (("", nth inducts i), [PureThy.kind_internal, Induct.induct_type ""]);
    8.23    in
    8.24      thy |> PureThy.add_thms
    8.25        (maps named_rules infos @
     9.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 04 14:42:11 2007 +0200
     9.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 04 14:42:47 2007 +0200
     9.3 @@ -73,7 +73,7 @@
     9.4              |> addsmps "psimps" [] psimps
     9.5              ||> fold_option (snd oo addsmps "simps" []) trsimps
     9.6              ||>> note_theorem ((qualify "pinduct",
     9.7 -                                [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)
     9.8 +                                [Attrib.internal (K (Induct.induct_set ""))]), simple_pinducts)
     9.9              ||>> note_theorem ((qualify "termination", []), [termination])
    9.10              ||> (snd o note_theorem ((qualify "cases", []), [cases]))
    9.11              ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
    10.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Oct 04 14:42:11 2007 +0200
    10.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 04 14:42:47 2007 +0200
    10.3 @@ -433,7 +433,7 @@
    10.4        error (Pretty.string_of (Pretty.block
    10.5          [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop]));
    10.6  
    10.7 -    val elims = InductAttrib.find_casesS ctxt prop;
    10.8 +    val elims = Induct.find_casesS ctxt prop;
    10.9  
   10.10      val cprop = Thm.cterm_of thy prop;
   10.11      val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
   10.12 @@ -679,7 +679,7 @@
   10.13        if coind then
   10.14          (raw_induct, [RuleCases.case_names [rec_name],
   10.15            RuleCases.case_conclusion (rec_name, intr_names),
   10.16 -          RuleCases.consumes 1, InductAttrib.coinduct_set (hd cnames)])
   10.17 +          RuleCases.consumes 1, Induct.coinduct_set (hd cnames)])
   10.18        else if no_ind orelse length cnames > 1 then
   10.19          (raw_induct, [ind_case_names, RuleCases.consumes 0])
   10.20        else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]);
   10.21 @@ -698,7 +698,7 @@
   10.22          LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases",
   10.23            [Attrib.internal (K (RuleCases.case_names cases)),
   10.24             Attrib.internal (K (RuleCases.consumes 1)),
   10.25 -           Attrib.internal (K (InductAttrib.cases_set name)),
   10.26 +           Attrib.internal (K (Induct.cases_set name)),
   10.27             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
   10.28          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
   10.29        LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
   10.30 @@ -712,7 +712,7 @@
   10.31            inducts |> map (fn (name, th) => ([th],
   10.32              [Attrib.internal (K ind_case_names),
   10.33               Attrib.internal (K (RuleCases.consumes 1)),
   10.34 -             Attrib.internal (K (InductAttrib.induct_set name))])))] |> snd
   10.35 +             Attrib.internal (K (Induct.induct_set name))])))] |> snd
   10.36        end
   10.37    in (intrs', elims', induct', ctxt3) end;
   10.38  
    11.1 --- a/src/HOL/Tools/record_package.ML	Thu Oct 04 14:42:11 2007 +0200
    11.2 +++ b/src/HOL/Tools/record_package.ML	Thu Oct 04 14:42:47 2007 +0200
    11.3 @@ -1372,8 +1372,8 @@
    11.4  (* attributes *)
    11.5  
    11.6  fun case_names_fields x = RuleCases.case_names ["fields"] x;
    11.7 -fun induct_type_global name = [case_names_fields, InductAttrib.induct_type name];
    11.8 -fun cases_type_global name = [case_names_fields, InductAttrib.cases_type name];
    11.9 +fun induct_type_global name = [case_names_fields, Induct.induct_type name];
   11.10 +fun cases_type_global name = [case_names_fields, Induct.cases_type name];
   11.11  
   11.12  (* tactics *)
   11.13  
    12.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Oct 04 14:42:11 2007 +0200
    12.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Oct 04 14:42:47 2007 +0200
    12.3 @@ -176,13 +176,13 @@
    12.4                  ((Rep_name ^ "_inject", make Rep_inject), []),
    12.5                  ((Abs_name ^ "_inject", abs_inject), []),
    12.6                  ((Rep_name ^ "_cases", make Rep_cases),
    12.7 -                  [RuleCases.case_names [Rep_name], InductAttrib.cases_set full_name]),
    12.8 +                  [RuleCases.case_names [Rep_name], Induct.cases_set full_name]),
    12.9                  ((Abs_name ^ "_cases", make Abs_cases),
   12.10 -                  [RuleCases.case_names [Abs_name], InductAttrib.cases_type full_tname]),
   12.11 +                  [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
   12.12                  ((Rep_name ^ "_induct", make Rep_induct),
   12.13 -                  [RuleCases.case_names [Rep_name], InductAttrib.induct_set full_name]),
   12.14 +                  [RuleCases.case_names [Rep_name], Induct.induct_set full_name]),
   12.15                  ((Abs_name ^ "_induct", make Abs_induct),
   12.16 -                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type full_tname])])
   12.17 +                  [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
   12.18              ||> Sign.parent_path;
   12.19            val info = {rep_type = oldT, abs_type = newT,
   12.20              Rep_name = full Rep_name, Abs_name = full Abs_name,
    13.1 --- a/src/Provers/induct_method.ML	Thu Oct 04 14:42:11 2007 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,550 +0,0 @@
    13.4 -(*  Title:      Provers/induct_method.ML
    13.5 -    ID:         $Id$
    13.6 -    Author:     Markus Wenzel, TU Muenchen
    13.7 -
    13.8 -Proof by cases and induction on sets and types.
    13.9 -*)
   13.10 -
   13.11 -signature INDUCT_METHOD_DATA =
   13.12 -sig
   13.13 -  val cases_default: thm
   13.14 -  val atomize: thm list
   13.15 -  val rulify: thm list
   13.16 -  val rulify_fallback: thm list
   13.17 -end;
   13.18 -
   13.19 -signature INDUCT_METHOD =
   13.20 -sig
   13.21 -  val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
   13.22 -  val add_defs: (string option * term) option list -> Proof.context ->
   13.23 -    (term option list * thm list) * Proof.context
   13.24 -  val atomize_term: theory -> term -> term
   13.25 -  val atomize_tac: int -> tactic
   13.26 -  val inner_atomize_tac: int -> tactic
   13.27 -  val rulified_term: thm -> theory * term
   13.28 -  val rulify_tac: int -> tactic
   13.29 -  val internalize: int -> thm -> thm
   13.30 -  val guess_instance: thm -> int -> thm -> thm Seq.seq
   13.31 -  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
   13.32 -    thm list -> int -> cases_tactic
   13.33 -  val induct_tac: Proof.context -> bool -> (string option * term) option list list ->
   13.34 -    (string * typ) list list -> term option list -> thm list option -> thm list -> int ->
   13.35 -    cases_tactic
   13.36 -  val coinduct_tac: Proof.context -> bool -> term option list -> term option list ->
   13.37 -    thm option -> thm list -> int -> cases_tactic
   13.38 -  val setup: theory -> theory
   13.39 -end;
   13.40 -
   13.41 -functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD =
   13.42 -struct
   13.43 -
   13.44 -val meta_spec = thm "Pure.meta_spec";
   13.45 -val all_conjunction = thm "Pure.all_conjunction";
   13.46 -val imp_conjunction = thm "Pure.imp_conjunction";
   13.47 -val conjunction_imp = thm "Pure.conjunction_imp";
   13.48 -val conjunction_congs = [all_conjunction, imp_conjunction];
   13.49 -
   13.50 -
   13.51 -
   13.52 -(** misc utils **)
   13.53 -
   13.54 -(* alignment *)
   13.55 -
   13.56 -fun align_left msg xs ys =
   13.57 -  let val m = length xs and n = length ys
   13.58 -  in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
   13.59 -
   13.60 -fun align_right msg xs ys =
   13.61 -  let val m = length xs and n = length ys
   13.62 -  in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
   13.63 -
   13.64 -
   13.65 -(* prep_inst *)
   13.66 -
   13.67 -fun prep_inst thy align tune (tm, ts) =
   13.68 -  let
   13.69 -    val cert = Thm.cterm_of thy;
   13.70 -    fun prep_var (x, SOME t) =
   13.71 -          let
   13.72 -            val cx = cert x;
   13.73 -            val {T = xT, thy, ...} = Thm.rep_cterm cx;
   13.74 -            val ct = cert (tune t);
   13.75 -          in
   13.76 -            if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
   13.77 -            else error (Pretty.string_of (Pretty.block
   13.78 -             [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
   13.79 -              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
   13.80 -              Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
   13.81 -          end
   13.82 -      | prep_var (_, NONE) = NONE;
   13.83 -    val xs = InductAttrib.vars_of tm;
   13.84 -  in
   13.85 -    align "Rule has fewer variables than instantiations given" xs ts
   13.86 -    |> map_filter prep_var
   13.87 -  end;
   13.88 -
   13.89 -
   13.90 -(* trace_rules *)
   13.91 -
   13.92 -fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule")
   13.93 -  | trace_rules ctxt _ rules = Method.trace ctxt rules;
   13.94 -
   13.95 -
   13.96 -(* make_cases *)
   13.97 -
   13.98 -fun make_cases is_open rule =
   13.99 -  RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
  13.100 -
  13.101 -fun warn_open true = legacy_feature "open rule cases in proof method"
  13.102 -  | warn_open false = ();
  13.103 -
  13.104 -
  13.105 -
  13.106 -(** cases method **)
  13.107 -
  13.108 -(*
  13.109 -  rule selection scheme:
  13.110 -          cases         - default case split
  13.111 -    `x:A` cases ...     - set cases
  13.112 -          cases t       - type cases
  13.113 -    ...   cases ... r   - explicit rule
  13.114 -*)
  13.115 -
  13.116 -local
  13.117 -
  13.118 -fun find_casesT ctxt ((SOME t :: _) :: _) = InductAttrib.find_casesT ctxt (Term.fastype_of t)
  13.119 -  | find_casesT _ _ = [];
  13.120 -
  13.121 -fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt (Thm.concl_of fact)
  13.122 -  | find_casesS _ _ = [];
  13.123 -
  13.124 -in
  13.125 -
  13.126 -fun cases_tac ctxt is_open insts opt_rule facts =
  13.127 -  let
  13.128 -    val _ = warn_open is_open;
  13.129 -    val thy = ProofContext.theory_of ctxt;
  13.130 -    val cert = Thm.cterm_of thy;
  13.131 -
  13.132 -    fun inst_rule r =
  13.133 -      if null insts then `RuleCases.get r
  13.134 -      else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
  13.135 -        |> maps (prep_inst thy align_left I)
  13.136 -        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
  13.137 -
  13.138 -    val ruleq =
  13.139 -      (case opt_rule of
  13.140 -        SOME r => Seq.single (inst_rule r)
  13.141 -      | NONE =>
  13.142 -          (find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default])
  13.143 -          |> tap (trace_rules ctxt InductAttrib.casesN)
  13.144 -          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
  13.145 -  in
  13.146 -    fn i => fn st =>
  13.147 -      ruleq
  13.148 -      |> Seq.maps (RuleCases.consume [] facts)
  13.149 -      |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
  13.150 -        CASES (make_cases is_open rule cases)
  13.151 -          (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
  13.152 -  end;
  13.153 -
  13.154 -end;
  13.155 -
  13.156 -
  13.157 -
  13.158 -(** induct method **)
  13.159 -
  13.160 -(* atomize *)
  13.161 -
  13.162 -fun atomize_term thy =
  13.163 -  MetaSimplifier.rewrite_term thy Data.atomize []
  13.164 -  #> ObjectLogic.drop_judgment thy;
  13.165 -
  13.166 -val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
  13.167 -
  13.168 -val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize;
  13.169 -
  13.170 -val inner_atomize_tac =
  13.171 -  Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
  13.172 -
  13.173 -
  13.174 -(* rulify *)
  13.175 -
  13.176 -fun rulify_term thy =
  13.177 -  MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
  13.178 -  MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
  13.179 -
  13.180 -fun rulified_term thm =
  13.181 -  let
  13.182 -    val thy = Thm.theory_of_thm thm;
  13.183 -    val rulify = rulify_term thy;
  13.184 -    val (As, B) = Logic.strip_horn (Thm.prop_of thm);
  13.185 -  in (thy, Logic.list_implies (map rulify As, rulify B)) end;
  13.186 -
  13.187 -val rulify_tac =
  13.188 -  Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
  13.189 -  Simplifier.rewrite_goal_tac Data.rulify_fallback THEN'
  13.190 -  Goal.conjunction_tac THEN_ALL_NEW
  13.191 -  (Simplifier.rewrite_goal_tac [conjunction_imp] THEN' Goal.norm_hhf_tac);
  13.192 -
  13.193 -
  13.194 -(* prepare rule *)
  13.195 -
  13.196 -fun rule_instance thy inst rule =
  13.197 -  Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
  13.198 -
  13.199 -fun internalize k th =
  13.200 -  th |> Thm.permute_prems 0 k
  13.201 -  |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
  13.202 -
  13.203 -
  13.204 -(* guess rule instantiation -- cannot handle pending goal parameters *)
  13.205 -
  13.206 -local
  13.207 -
  13.208 -fun dest_env thy (env as Envir.Envir {iTs, ...}) =
  13.209 -  let
  13.210 -    val cert = Thm.cterm_of thy;
  13.211 -    val certT = Thm.ctyp_of thy;
  13.212 -    val pairs = Envir.alist_of env;
  13.213 -    val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
  13.214 -    val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
  13.215 -  in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
  13.216 -
  13.217 -in
  13.218 -
  13.219 -fun guess_instance rule i st =
  13.220 -  let
  13.221 -    val {thy, maxidx, ...} = Thm.rep_thm st;
  13.222 -    val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
  13.223 -    val params = rev (rename_wrt_term goal (Logic.strip_params goal));
  13.224 -  in
  13.225 -    if not (null params) then
  13.226 -      (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
  13.227 -        commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params));
  13.228 -      Seq.single rule)
  13.229 -    else
  13.230 -      let
  13.231 -        val rule' = Thm.incr_indexes (maxidx + 1) rule;
  13.232 -        val concl = Logic.strip_assums_concl goal;
  13.233 -      in
  13.234 -        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
  13.235 -          (Envir.empty (#maxidx (Thm.rep_thm rule')))
  13.236 -        |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
  13.237 -      end
  13.238 -  end handle Subscript => Seq.empty;
  13.239 -
  13.240 -end;
  13.241 -
  13.242 -
  13.243 -(* special renaming of rule parameters *)
  13.244 -
  13.245 -fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
  13.246 -      let
  13.247 -        val x = ProofContext.revert_skolem ctxt z;
  13.248 -        fun index i [] = []
  13.249 -          | index i (y :: ys) =
  13.250 -              if x = y then x ^ string_of_int i :: index (i + 1) ys
  13.251 -              else y :: index i ys;
  13.252 -        fun rename_params [] = []
  13.253 -          | rename_params ((y, Type (U, _)) :: ys) =
  13.254 -              (if U = T then x else y) :: rename_params ys
  13.255 -          | rename_params ((y, _) :: ys) = y :: rename_params ys;
  13.256 -        fun rename_asm A =
  13.257 -          let
  13.258 -            val xs = rename_params (Logic.strip_params A);
  13.259 -            val xs' =
  13.260 -              (case List.filter (equal x) xs of
  13.261 -                [] => xs | [_] => xs | _ => index 1 xs);
  13.262 -          in Logic.list_rename_params (xs', A) end;
  13.263 -        fun rename_prop p =
  13.264 -          let val (As, C) = Logic.strip_horn p
  13.265 -          in Logic.list_implies (map rename_asm As, C) end;
  13.266 -        val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
  13.267 -        val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
  13.268 -      in [RuleCases.save thm thm'] end
  13.269 -  | special_rename_params _ _ ths = ths;
  13.270 -
  13.271 -
  13.272 -(* fix_tac *)
  13.273 -
  13.274 -local
  13.275 -
  13.276 -fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
  13.277 -  | goal_prefix 0 _ = Term.dummy_pattern propT
  13.278 -  | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
  13.279 -  | goal_prefix _ _ = Term.dummy_pattern propT;
  13.280 -
  13.281 -fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
  13.282 -  | goal_params 0 _ = 0
  13.283 -  | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B
  13.284 -  | goal_params _ _ = 0;
  13.285 -
  13.286 -fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
  13.287 -  let
  13.288 -    val thy = ProofContext.theory_of ctxt;
  13.289 -    val cert = Thm.cterm_of thy;
  13.290 -    val certT = Thm.ctyp_of thy;
  13.291 -
  13.292 -    val v = Free (x, T);
  13.293 -    fun spec_rule prfx (xs, body) =
  13.294 -      meta_spec
  13.295 -      |> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1)
  13.296 -      |> Thm.lift_rule (cert prfx)
  13.297 -      |> `(Thm.prop_of #> Logic.strip_assums_concl)
  13.298 -      |-> (fn pred $ arg =>
  13.299 -        Drule.cterm_instantiate
  13.300 -          [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
  13.301 -           (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
  13.302 -
  13.303 -    fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
  13.304 -      | goal_concl 0 xs B =
  13.305 -          if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
  13.306 -          else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
  13.307 -      | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
  13.308 -      | goal_concl _ _ _ = NONE;
  13.309 -  in
  13.310 -    (case goal_concl n [] goal of
  13.311 -      SOME concl =>
  13.312 -        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
  13.313 -    | NONE => all_tac)
  13.314 -  end);
  13.315 -
  13.316 -fun miniscope_tac p =
  13.317 -  CONVERSION (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
  13.318 -
  13.319 -in
  13.320 -
  13.321 -fun fix_tac _ _ [] = K all_tac
  13.322 -  | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
  13.323 -     (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
  13.324 -      (miniscope_tac (goal_params n goal))) i);
  13.325 -
  13.326 -end;
  13.327 -
  13.328 -
  13.329 -(* add_defs *)
  13.330 -
  13.331 -fun add_defs def_insts =
  13.332 -  let
  13.333 -    fun add (SOME (SOME x, t)) ctxt =
  13.334 -          let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt
  13.335 -          in ((SOME lhs, [th]), ctxt') end
  13.336 -      | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
  13.337 -      | add NONE ctxt = ((NONE, []), ctxt);
  13.338 -  in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
  13.339 -
  13.340 -
  13.341 -(* induct_tac *)
  13.342 -
  13.343 -(*
  13.344 -  rule selection scheme:
  13.345 -    `x:A` induct ...     - set induction
  13.346 -          induct x       - type induction
  13.347 -    ...   induct ... r   - explicit rule
  13.348 -*)
  13.349 -
  13.350 -local
  13.351 -
  13.352 -fun find_inductT ctxt insts =
  13.353 -  fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts)
  13.354 -    |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]]
  13.355 -  |> filter_out (forall PureThy.is_internal);
  13.356 -
  13.357 -fun find_inductS ctxt (fact :: _) = map single (InductAttrib.find_inductS ctxt (Thm.concl_of fact))
  13.358 -  | find_inductS _ _ = [];
  13.359 -
  13.360 -in
  13.361 -
  13.362 -fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
  13.363 -  let
  13.364 -    val _ = warn_open is_open;
  13.365 -    val thy = ProofContext.theory_of ctxt;
  13.366 -    val cert = Thm.cterm_of thy;
  13.367 -
  13.368 -    val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
  13.369 -    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
  13.370 -
  13.371 -    fun inst_rule (concls, r) =
  13.372 -      (if null insts then `RuleCases.get r
  13.373 -       else (align_left "Rule has fewer conclusions than arguments given"
  13.374 -          (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
  13.375 -        |> maps (prep_inst thy align_right (atomize_term thy))
  13.376 -        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
  13.377 -      |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
  13.378 -
  13.379 -    val ruleq =
  13.380 -      (case opt_rule of
  13.381 -        SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
  13.382 -      | NONE =>
  13.383 -          (find_inductS ctxt facts @
  13.384 -            map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts))
  13.385 -          |> map_filter (RuleCases.mutual_rule ctxt)
  13.386 -          |> tap (trace_rules ctxt InductAttrib.inductN o map #2)
  13.387 -          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
  13.388 -
  13.389 -    fun rule_cases rule =
  13.390 -      RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule);
  13.391 -  in
  13.392 -    (fn i => fn st =>
  13.393 -      ruleq
  13.394 -      |> Seq.maps (RuleCases.consume (flat defs) facts)
  13.395 -      |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
  13.396 -        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
  13.397 -          (CONJUNCTS (ALLGOALS
  13.398 -            (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
  13.399 -              THEN' fix_tac defs_ctxt
  13.400 -                (nth concls (j - 1) + more_consumes)
  13.401 -                (nth_list arbitrary (j - 1))))
  13.402 -          THEN' inner_atomize_tac) j))
  13.403 -        THEN' atomize_tac) i st |> Seq.maps (fn st' =>
  13.404 -            guess_instance (internalize more_consumes rule) i st'
  13.405 -            |> Seq.map (rule_instance thy taking)
  13.406 -            |> Seq.maps (fn rule' =>
  13.407 -              CASES (rule_cases rule' cases)
  13.408 -                (Tactic.rtac rule' i THEN
  13.409 -                  PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
  13.410 -    THEN_ALL_NEW_CASES rulify_tac
  13.411 -  end;
  13.412 -
  13.413 -end;
  13.414 -
  13.415 -
  13.416 -
  13.417 -(** coinduct method **)
  13.418 -
  13.419 -(*
  13.420 -  rule selection scheme:
  13.421 -    goal "x:A" coinduct ...   - set coinduction
  13.422 -               coinduct x     - type coinduction
  13.423 -               coinduct ... r - explicit rule
  13.424 -*)
  13.425 -
  13.426 -local
  13.427 -
  13.428 -fun find_coinductT ctxt (SOME t :: _) = InductAttrib.find_coinductT ctxt (Term.fastype_of t)
  13.429 -  | find_coinductT _ _ = [];
  13.430 -
  13.431 -fun find_coinductS ctxt goal = InductAttrib.find_coinductS ctxt (Logic.strip_assums_concl goal);
  13.432 -
  13.433 -in
  13.434 -
  13.435 -fun coinduct_tac ctxt is_open inst taking opt_rule facts =
  13.436 -  let
  13.437 -    val _ = warn_open is_open;
  13.438 -    val thy = ProofContext.theory_of ctxt;
  13.439 -    val cert = Thm.cterm_of thy;
  13.440 -
  13.441 -    fun inst_rule r =
  13.442 -      if null inst then `RuleCases.get r
  13.443 -      else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r
  13.444 -        |> pair (RuleCases.get r);
  13.445 -
  13.446 -    fun ruleq goal =
  13.447 -      (case opt_rule of
  13.448 -        SOME r => Seq.single (inst_rule r)
  13.449 -      | NONE =>
  13.450 -          (find_coinductS ctxt goal @ find_coinductT ctxt inst)
  13.451 -          |> tap (trace_rules ctxt InductAttrib.coinductN)
  13.452 -          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
  13.453 -  in
  13.454 -    SUBGOAL_CASES (fn (goal, i) => fn st =>
  13.455 -      ruleq goal
  13.456 -      |> Seq.maps (RuleCases.consume [] facts)
  13.457 -      |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
  13.458 -        guess_instance rule i st
  13.459 -        |> Seq.map (rule_instance thy taking)
  13.460 -        |> Seq.maps (fn rule' =>
  13.461 -          CASES (make_cases is_open rule' cases)
  13.462 -            (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
  13.463 -  end;
  13.464 -
  13.465 -end;
  13.466 -
  13.467 -
  13.468 -
  13.469 -(** concrete syntax **)
  13.470 -
  13.471 -val openN = "open";
  13.472 -val arbitraryN = "arbitrary";
  13.473 -val takingN = "taking";
  13.474 -val ruleN = "rule";
  13.475 -
  13.476 -local
  13.477 -
  13.478 -fun single_rule [rule] = rule
  13.479 -  | single_rule _ = error "Single rule expected";
  13.480 -
  13.481 -fun named_rule k arg get =
  13.482 -  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
  13.483 -    (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
  13.484 -      (case get (Context.proof_of context) name of SOME x => x
  13.485 -      | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
  13.486 -
  13.487 -fun rule get_type get_set =
  13.488 -  named_rule InductAttrib.typeN Args.tyname get_type ||
  13.489 -  named_rule InductAttrib.setN Args.const get_set ||
  13.490 -  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
  13.491 -
  13.492 -val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS >> single_rule;
  13.493 -val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS;
  13.494 -val coinduct_rule =
  13.495 -  rule InductAttrib.lookup_coinductT InductAttrib.lookup_coinductS >> single_rule;
  13.496 -
  13.497 -val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
  13.498 -
  13.499 -val def_inst =
  13.500 -  ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
  13.501 -      -- Args.term) >> SOME ||
  13.502 -    inst >> Option.map (pair NONE);
  13.503 -
  13.504 -val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
  13.505 -  error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
  13.506 -
  13.507 -fun unless_more_args scan = Scan.unless (Scan.lift
  13.508 -  ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN ||
  13.509 -    Args.$$$ InductAttrib.setN || Args.$$$ ruleN) -- Args.colon)) scan;
  13.510 -
  13.511 -val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
  13.512 -  Args.and_list1 (Scan.repeat (unless_more_args free))) [];
  13.513 -
  13.514 -val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
  13.515 -  Scan.repeat1 (unless_more_args inst)) [];
  13.516 -
  13.517 -in
  13.518 -
  13.519 -fun cases_meth src =
  13.520 -  Method.syntax (Args.mode openN --
  13.521 -    (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src
  13.522 -  #> (fn ((is_open, (insts, opt_rule)), ctxt) =>
  13.523 -    Method.METHOD_CASES (fn facts =>
  13.524 -      Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts))));
  13.525 -
  13.526 -fun induct_meth src =
  13.527 -  Method.syntax (Args.mode openN --
  13.528 -    (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
  13.529 -    (arbitrary -- taking -- Scan.option induct_rule))) src
  13.530 -  #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) =>
  13.531 -    Method.RAW_METHOD_CASES (fn facts =>
  13.532 -      Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts))));
  13.533 -
  13.534 -fun coinduct_meth src =
  13.535 -  Method.syntax (Args.mode openN --
  13.536 -    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src
  13.537 -  #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) =>
  13.538 -    Method.RAW_METHOD_CASES (fn facts =>
  13.539 -      Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts))));
  13.540 -
  13.541 -end;
  13.542 -
  13.543 -
  13.544 -
  13.545 -(** theory setup **)
  13.546 -
  13.547 -val setup =
  13.548 -  Method.add_methods
  13.549 -    [(InductAttrib.casesN, cases_meth, "case analysis on types or sets"),
  13.550 -     (InductAttrib.inductN, induct_meth, "induction on types or sets"),
  13.551 -     (InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")];
  13.552 -
  13.553 -end;
    14.1 --- a/src/Pure/IsaMakefile	Thu Oct 04 14:42:11 2007 +0200
    14.2 +++ b/src/Pure/IsaMakefile	Thu Oct 04 14:42:47 2007 +0200
    14.3 @@ -35,7 +35,7 @@
    14.4    Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
    14.5    Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML		\
    14.6    Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML			\
    14.7 -  Isar/find_theorems.ML Isar/induct_attrib.ML Isar/instance.ML Isar/isar_cmd.ML	\
    14.8 +  Isar/find_theorems.ML Isar/instance.ML Isar/isar_cmd.ML			\
    14.9    Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML			\
   14.10    Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML		\
   14.11    Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML			\
    15.1 --- a/src/Pure/Isar/ROOT.ML	Thu Oct 04 14:42:11 2007 +0200
    15.2 +++ b/src/Pure/Isar/ROOT.ML	Thu Oct 04 14:42:47 2007 +0200
    15.3 @@ -41,7 +41,6 @@
    15.4  use "proof.ML";
    15.5  use "element.ML";
    15.6  use "net_rules.ML";
    15.7 -use "induct_attrib.ML";
    15.8  
    15.9  (*derived theory and proof elements*)
   15.10  use "calculation.ML";
    16.1 --- a/src/Pure/Isar/induct_attrib.ML	Thu Oct 04 14:42:11 2007 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,224 +0,0 @@
    16.4 -(*  Title:      Pure/Isar/induct_attrib.ML
    16.5 -    ID:         $Id$
    16.6 -    Author:     Markus Wenzel, TU Muenchen
    16.7 -
    16.8 -Declaration of rules for cases and induction.
    16.9 -*)
   16.10 -
   16.11 -signature INDUCT_ATTRIB =
   16.12 -sig
   16.13 -  val vars_of: term -> term list
   16.14 -  val dest_rules: Proof.context ->
   16.15 -    {type_cases: (string * thm) list, set_cases: (string * thm) list,
   16.16 -      type_induct: (string * thm) list, set_induct: (string * thm) list,
   16.17 -      type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
   16.18 -  val print_rules: Proof.context -> unit
   16.19 -  val lookup_casesT : Proof.context -> string -> thm option
   16.20 -  val lookup_casesS : Proof.context -> string -> thm option
   16.21 -  val lookup_inductT : Proof.context -> string -> thm option
   16.22 -  val lookup_inductS : Proof.context -> string -> thm option
   16.23 -  val lookup_coinductT : Proof.context -> string -> thm option
   16.24 -  val lookup_coinductS : Proof.context -> string -> thm option
   16.25 -  val find_casesT: Proof.context -> typ -> thm list
   16.26 -  val find_casesS: Proof.context -> term -> thm list
   16.27 -  val find_inductT: Proof.context -> typ -> thm list
   16.28 -  val find_inductS: Proof.context -> term -> thm list
   16.29 -  val find_coinductT: Proof.context -> typ -> thm list
   16.30 -  val find_coinductS: Proof.context -> term -> thm list
   16.31 -  val cases_type: string -> attribute
   16.32 -  val cases_set: string -> attribute
   16.33 -  val induct_type: string -> attribute
   16.34 -  val induct_set: string -> attribute
   16.35 -  val coinduct_type: string -> attribute
   16.36 -  val coinduct_set: string -> attribute
   16.37 -  val casesN: string
   16.38 -  val inductN: string
   16.39 -  val coinductN: string
   16.40 -  val typeN: string
   16.41 -  val setN: string
   16.42 -end;
   16.43 -
   16.44 -structure InductAttrib: INDUCT_ATTRIB =
   16.45 -struct
   16.46 -
   16.47 -
   16.48 -(** misc utils **)
   16.49 -
   16.50 -(* encode_type -- for indexing purposes *)
   16.51 -
   16.52 -fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
   16.53 -  | encode_type (TFree (a, _)) = Free (a, dummyT)
   16.54 -  | encode_type (TVar (a, _)) = Var (a, dummyT);
   16.55 -
   16.56 -
   16.57 -(* variables -- ordered left-to-right, preferring right *)
   16.58 -
   16.59 -fun vars_of tm =
   16.60 -  rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
   16.61 -
   16.62 -local
   16.63 -
   16.64 -val mk_var = encode_type o #2 o Term.dest_Var;
   16.65 -
   16.66 -fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
   16.67 -  raise THM ("No variables in conclusion of rule", 0, [thm]);
   16.68 -
   16.69 -in
   16.70 -
   16.71 -fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
   16.72 -  raise THM ("No variables in major premise of rule", 0, [thm]);
   16.73 -
   16.74 -val left_var_concl = concl_var hd;
   16.75 -val right_var_concl = concl_var List.last;
   16.76 -
   16.77 -end;
   16.78 -
   16.79 -
   16.80 -
   16.81 -(** induct data **)
   16.82 -
   16.83 -(* rules *)
   16.84 -
   16.85 -type rules = (string * thm) NetRules.T;
   16.86 -
   16.87 -val init_rules =
   16.88 -  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
   16.89 -    Thm.eq_thm_prop (th1, th2));
   16.90 -
   16.91 -fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
   16.92 -
   16.93 -fun pretty_rules ctxt kind rs =
   16.94 -  let val thms = map snd (NetRules.rules rs)
   16.95 -  in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
   16.96 -
   16.97 -
   16.98 -(* context data *)
   16.99 -
  16.100 -structure Induct = GenericDataFun
  16.101 -(
  16.102 -  type T = (rules * rules) * (rules * rules) * (rules * rules);
  16.103 -  val empty =
  16.104 -    ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
  16.105 -     (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
  16.106 -     (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
  16.107 -  val extend = I;
  16.108 -  fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
  16.109 -      ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
  16.110 -    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
  16.111 -      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
  16.112 -      (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
  16.113 -);
  16.114 -
  16.115 -val get_local = Induct.get o Context.Proof;
  16.116 -
  16.117 -fun dest_rules ctxt =
  16.118 -  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
  16.119 -    {type_cases = NetRules.rules casesT,
  16.120 -     set_cases = NetRules.rules casesS,
  16.121 -     type_induct = NetRules.rules inductT,
  16.122 -     set_induct = NetRules.rules inductS,
  16.123 -     type_coinduct = NetRules.rules coinductT,
  16.124 -     set_coinduct = NetRules.rules coinductS}
  16.125 -  end;
  16.126 -
  16.127 -fun print_rules ctxt =
  16.128 -  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
  16.129 -   [pretty_rules ctxt "coinduct type:" coinductT,
  16.130 -    pretty_rules ctxt "coinduct set:" coinductS,
  16.131 -    pretty_rules ctxt "induct type:" inductT,
  16.132 -    pretty_rules ctxt "induct set:" inductS,
  16.133 -    pretty_rules ctxt "cases type:" casesT,
  16.134 -    pretty_rules ctxt "cases set:" casesS]
  16.135 -    |> Pretty.chunks |> Pretty.writeln
  16.136 -  end;
  16.137 -
  16.138 -
  16.139 -(* access rules *)
  16.140 -
  16.141 -val lookup_casesT = lookup_rule o #1 o #1 o get_local;
  16.142 -val lookup_casesS = lookup_rule o #2 o #1 o get_local;
  16.143 -val lookup_inductT = lookup_rule o #1 o #2 o get_local;
  16.144 -val lookup_inductS = lookup_rule o #2 o #2 o get_local;
  16.145 -val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
  16.146 -val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
  16.147 -
  16.148 -
  16.149 -fun find_rules which how ctxt x =
  16.150 -  map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
  16.151 -
  16.152 -val find_casesT = find_rules (#1 o #1) encode_type;
  16.153 -val find_casesS = find_rules (#2 o #1) I;
  16.154 -val find_inductT = find_rules (#1 o #2) encode_type;
  16.155 -val find_inductS = find_rules (#2 o #2) I;
  16.156 -val find_coinductT = find_rules (#1 o #3) encode_type;
  16.157 -val find_coinductS = find_rules (#2 o #3) I;
  16.158 -
  16.159 -
  16.160 -
  16.161 -(** attributes **)
  16.162 -
  16.163 -local
  16.164 -
  16.165 -fun mk_att f g name arg =
  16.166 -  let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
  16.167 -
  16.168 -fun map1 f (x, y, z) = (f x, y, z);
  16.169 -fun map2 f (x, y, z) = (x, f y, z);
  16.170 -fun map3 f (x, y, z) = (x, y, f z);
  16.171 -
  16.172 -fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
  16.173 -fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x;
  16.174 -fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
  16.175 -fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x;
  16.176 -fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
  16.177 -fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x;
  16.178 -
  16.179 -fun consumes0 x = RuleCases.consumes_default 0 x;
  16.180 -fun consumes1 x = RuleCases.consumes_default 1 x;
  16.181 -
  16.182 -in
  16.183 -
  16.184 -val cases_type = mk_att add_casesT consumes0;
  16.185 -val cases_set = mk_att add_casesS consumes1;
  16.186 -val induct_type = mk_att add_inductT consumes0;
  16.187 -val induct_set = mk_att add_inductS consumes1;
  16.188 -val coinduct_type = mk_att add_coinductT consumes0;
  16.189 -val coinduct_set = mk_att add_coinductS consumes1;
  16.190 -
  16.191 -end;
  16.192 -
  16.193 -
  16.194 -
  16.195 -(** concrete syntax **)
  16.196 -
  16.197 -val casesN = "cases";
  16.198 -val inductN = "induct";
  16.199 -val coinductN = "coinduct";
  16.200 -
  16.201 -val typeN = "type";
  16.202 -val setN = "set";
  16.203 -
  16.204 -local
  16.205 -
  16.206 -fun spec k arg =
  16.207 -  Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
  16.208 -  Scan.lift (Args.$$$ k) >> K "";
  16.209 -
  16.210 -fun attrib add_type add_set =
  16.211 -  Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
  16.212 -
  16.213 -in
  16.214 -
  16.215 -val cases_att = attrib cases_type cases_set;
  16.216 -val induct_att = attrib induct_type induct_set;
  16.217 -val coinduct_att = attrib coinduct_type coinduct_set;
  16.218 -
  16.219 -end;
  16.220 -
  16.221 -val _ = Context.add_setup
  16.222 - (Attrib.add_attributes
  16.223 -  [(casesN, cases_att, "declaration of cases rule for type or set"),
  16.224 -   (inductN, induct_att, "declaration of induction rule for type or set"),
  16.225 -   (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]);
  16.226 -
  16.227 -end;
    17.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Oct 04 14:42:11 2007 +0200
    17.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Oct 04 14:42:47 2007 +0200
    17.3 @@ -85,7 +85,6 @@
    17.4    val print_attributes: Toplevel.transition -> Toplevel.transition
    17.5    val print_simpset: Toplevel.transition -> Toplevel.transition
    17.6    val print_rules: Toplevel.transition -> Toplevel.transition
    17.7 -  val print_induct_rules: Toplevel.transition -> Toplevel.transition
    17.8    val print_trans_rules: Toplevel.transition -> Toplevel.transition
    17.9    val print_methods: Toplevel.transition -> Toplevel.transition
   17.10    val print_antiquotations: Toplevel.transition -> Toplevel.transition
   17.11 @@ -472,9 +471,6 @@
   17.12  val print_rules = Toplevel.unknown_context o
   17.13    Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);
   17.14  
   17.15 -val print_induct_rules = Toplevel.unknown_context o
   17.16 -  Toplevel.keep (InductAttrib.print_rules o Toplevel.context_of);
   17.17 -
   17.18  val print_trans_rules = Toplevel.unknown_context o
   17.19    Toplevel.keep (Calculation.print_rules o Toplevel.context_of);
   17.20  
    18.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Oct 04 14:42:11 2007 +0200
    18.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 04 14:42:47 2007 +0200
    18.3 @@ -799,10 +799,6 @@
    18.4    OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag
    18.5      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
    18.6  
    18.7 -val print_induct_rulesP =
    18.8 -  OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" K.diag
    18.9 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_induct_rules));
   18.10 -
   18.11  val print_trans_rulesP =
   18.12    OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag
   18.13      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
   18.14 @@ -1005,7 +1001,8 @@
   18.15    simproc_setupP, parse_ast_translationP, parse_translationP,
   18.16    print_translationP, typed_print_translationP,
   18.17    print_ast_translationP, token_translationP, oracleP, contextP,
   18.18 -  localeP, classP, instanceP, instantiationP, instance_proofP, code_datatypeP,
   18.19 +  localeP, classP, instanceP, instantiationP, instance_proofP,
   18.20 +  code_datatypeP,
   18.21    (*proof commands*)
   18.22    theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   18.23    assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
   18.24 @@ -1020,12 +1017,11 @@
   18.25    print_configsP, print_contextP, print_theoryP, print_syntaxP,
   18.26    print_abbrevsP, print_factsP, print_theoremsP, print_localesP,
   18.27    print_localeP, print_registrationsP, print_attributesP,
   18.28 -  print_simpsetP, print_rulesP, print_induct_rulesP,
   18.29 -  print_trans_rulesP, print_methodsP, print_antiquotationsP,
   18.30 -  thy_depsP, class_depsP, thm_depsP, find_theoremsP, print_bindsP,
   18.31 -  print_casesP, print_stmtsP, print_thmsP, print_prfsP,
   18.32 -  print_full_prfsP, print_propP, print_termP, print_typeP,
   18.33 -  print_codesetupP,
   18.34 +  print_simpsetP, print_rulesP, print_trans_rulesP, print_methodsP,
   18.35 +  print_antiquotationsP, thy_depsP, class_depsP, thm_depsP,
   18.36 +  find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
   18.37 +  print_thmsP, print_prfsP, print_full_prfsP, print_propP,
   18.38 +  print_termP, print_typeP, print_codesetupP,
   18.39    (*system commands*)
   18.40    cdP, pwdP, use_thyP, touch_thyP, touch_child_thysP, remove_thyP,
   18.41    kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/Tools/induct.ML	Thu Oct 04 14:42:47 2007 +0200
    19.3 @@ -0,0 +1,762 @@
    19.4 +(*  Title:      Tools/induct.ML
    19.5 +    ID:         $Id$
    19.6 +    Author:     Markus Wenzel, TU Muenchen
    19.7 +
    19.8 +Proof by cases and induction.
    19.9 +*)
   19.10 +
   19.11 +signature INDUCT_DATA =
   19.12 +sig
   19.13 +  val cases_default: thm
   19.14 +  val atomize: thm list
   19.15 +  val rulify: thm list
   19.16 +  val rulify_fallback: thm list
   19.17 +end;
   19.18 +
   19.19 +signature INDUCT =
   19.20 +sig
   19.21 +  (*rule declarations*)
   19.22 +  val vars_of: term -> term list
   19.23 +  val dest_rules: Proof.context ->
   19.24 +    {type_cases: (string * thm) list, set_cases: (string * thm) list,
   19.25 +      type_induct: (string * thm) list, set_induct: (string * thm) list,
   19.26 +      type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
   19.27 +  val print_rules: Proof.context -> unit
   19.28 +  val lookup_casesT: Proof.context -> string -> thm option
   19.29 +  val lookup_casesS: Proof.context -> string -> thm option
   19.30 +  val lookup_inductT: Proof.context -> string -> thm option
   19.31 +  val lookup_inductS: Proof.context -> string -> thm option
   19.32 +  val lookup_coinductT: Proof.context -> string -> thm option
   19.33 +  val lookup_coinductS: Proof.context -> string -> thm option
   19.34 +  val find_casesT: Proof.context -> typ -> thm list
   19.35 +  val find_casesS: Proof.context -> term -> thm list
   19.36 +  val find_inductT: Proof.context -> typ -> thm list
   19.37 +  val find_inductS: Proof.context -> term -> thm list
   19.38 +  val find_coinductT: Proof.context -> typ -> thm list
   19.39 +  val find_coinductS: Proof.context -> term -> thm list
   19.40 +  val cases_type: string -> attribute
   19.41 +  val cases_set: string -> attribute
   19.42 +  val induct_type: string -> attribute
   19.43 +  val induct_set: string -> attribute
   19.44 +  val coinduct_type: string -> attribute
   19.45 +  val coinduct_set: string -> attribute
   19.46 +  val casesN: string
   19.47 +  val inductN: string
   19.48 +  val coinductN: string
   19.49 +  val typeN: string
   19.50 +  val setN: string
   19.51 +  (*proof methods*)
   19.52 +  val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
   19.53 +  val add_defs: (string option * term) option list -> Proof.context ->
   19.54 +    (term option list * thm list) * Proof.context
   19.55 +  val atomize_term: theory -> term -> term
   19.56 +  val atomize_tac: int -> tactic
   19.57 +  val inner_atomize_tac: int -> tactic
   19.58 +  val rulified_term: thm -> theory * term
   19.59 +  val rulify_tac: int -> tactic
   19.60 +  val internalize: int -> thm -> thm
   19.61 +  val guess_instance: thm -> int -> thm -> thm Seq.seq
   19.62 +  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
   19.63 +    thm list -> int -> cases_tactic
   19.64 +  val induct_tac: Proof.context -> bool -> (string option * term) option list list ->
   19.65 +    (string * typ) list list -> term option list -> thm list option -> thm list -> int ->
   19.66 +    cases_tactic
   19.67 +  val coinduct_tac: Proof.context -> bool -> term option list -> term option list ->
   19.68 +    thm option -> thm list -> int -> cases_tactic
   19.69 +  val setup: theory -> theory
   19.70 +end;
   19.71 +
   19.72 +functor InductFun(Data: INDUCT_DATA): INDUCT =
   19.73 +struct
   19.74 +
   19.75 +
   19.76 +(** misc utils **)
   19.77 +
   19.78 +(* encode_type -- for indexing purposes *)
   19.79 +
   19.80 +fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
   19.81 +  | encode_type (TFree (a, _)) = Free (a, dummyT)
   19.82 +  | encode_type (TVar (a, _)) = Var (a, dummyT);
   19.83 +
   19.84 +
   19.85 +(* variables -- ordered left-to-right, preferring right *)
   19.86 +
   19.87 +fun vars_of tm =
   19.88 +  rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
   19.89 +
   19.90 +local
   19.91 +
   19.92 +val mk_var = encode_type o #2 o Term.dest_Var;
   19.93 +
   19.94 +fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
   19.95 +  raise THM ("No variables in conclusion of rule", 0, [thm]);
   19.96 +
   19.97 +in
   19.98 +
   19.99 +fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
  19.100 +  raise THM ("No variables in major premise of rule", 0, [thm]);
  19.101 +
  19.102 +val left_var_concl = concl_var hd;
  19.103 +val right_var_concl = concl_var List.last;
  19.104 +
  19.105 +end;
  19.106 +
  19.107 +
  19.108 +
  19.109 +(** induct data **)
  19.110 +
  19.111 +(* rules *)
  19.112 +
  19.113 +type rules = (string * thm) NetRules.T;
  19.114 +
  19.115 +val init_rules =
  19.116 +  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
  19.117 +    Thm.eq_thm_prop (th1, th2));
  19.118 +
  19.119 +fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
  19.120 +
  19.121 +fun pretty_rules ctxt kind rs =
  19.122 +  let val thms = map snd (NetRules.rules rs)
  19.123 +  in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
  19.124 +
  19.125 +
  19.126 +(* context data *)
  19.127 +
  19.128 +structure Induct = GenericDataFun
  19.129 +(
  19.130 +  type T = (rules * rules) * (rules * rules) * (rules * rules);
  19.131 +  val empty =
  19.132 +    ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
  19.133 +     (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
  19.134 +     (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
  19.135 +  val extend = I;
  19.136 +  fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
  19.137 +      ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
  19.138 +    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
  19.139 +      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
  19.140 +      (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
  19.141 +);
  19.142 +
  19.143 +val get_local = Induct.get o Context.Proof;
  19.144 +
  19.145 +fun dest_rules ctxt =
  19.146 +  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
  19.147 +    {type_cases = NetRules.rules casesT,
  19.148 +     set_cases = NetRules.rules casesS,
  19.149 +     type_induct = NetRules.rules inductT,
  19.150 +     set_induct = NetRules.rules inductS,
  19.151 +     type_coinduct = NetRules.rules coinductT,
  19.152 +     set_coinduct = NetRules.rules coinductS}
  19.153 +  end;
  19.154 +
  19.155 +fun print_rules ctxt =
  19.156 +  let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
  19.157 +   [pretty_rules ctxt "coinduct type:" coinductT,
  19.158 +    pretty_rules ctxt "coinduct set:" coinductS,
  19.159 +    pretty_rules ctxt "induct type:" inductT,
  19.160 +    pretty_rules ctxt "induct set:" inductS,
  19.161 +    pretty_rules ctxt "cases type:" casesT,
  19.162 +    pretty_rules ctxt "cases set:" casesS]
  19.163 +    |> Pretty.chunks |> Pretty.writeln
  19.164 +  end;
  19.165 +
  19.166 +val _ = OuterSyntax.add_parsers [
  19.167 +  OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
  19.168 +    OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
  19.169 +      Toplevel.keep (print_rules o Toplevel.context_of)))];
  19.170 +
  19.171 +
  19.172 +(* access rules *)
  19.173 +
  19.174 +val lookup_casesT = lookup_rule o #1 o #1 o get_local;
  19.175 +val lookup_casesS = lookup_rule o #2 o #1 o get_local;
  19.176 +val lookup_inductT = lookup_rule o #1 o #2 o get_local;
  19.177 +val lookup_inductS = lookup_rule o #2 o #2 o get_local;
  19.178 +val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
  19.179 +val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
  19.180 +
  19.181 +
  19.182 +fun find_rules which how ctxt x =
  19.183 +  map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
  19.184 +
  19.185 +val find_casesT = find_rules (#1 o #1) encode_type;
  19.186 +val find_casesS = find_rules (#2 o #1) I;
  19.187 +val find_inductT = find_rules (#1 o #2) encode_type;
  19.188 +val find_inductS = find_rules (#2 o #2) I;
  19.189 +val find_coinductT = find_rules (#1 o #3) encode_type;
  19.190 +val find_coinductS = find_rules (#2 o #3) I;
  19.191 +
  19.192 +
  19.193 +
  19.194 +(** attributes **)
  19.195 +
  19.196 +local
  19.197 +
  19.198 +fun mk_att f g name arg =
  19.199 +  let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
  19.200 +
  19.201 +fun map1 f (x, y, z) = (f x, y, z);
  19.202 +fun map2 f (x, y, z) = (x, f y, z);
  19.203 +fun map3 f (x, y, z) = (x, y, f z);
  19.204 +
  19.205 +fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
  19.206 +fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x;
  19.207 +fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
  19.208 +fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x;
  19.209 +fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
  19.210 +fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x;
  19.211 +
  19.212 +fun consumes0 x = RuleCases.consumes_default 0 x;
  19.213 +fun consumes1 x = RuleCases.consumes_default 1 x;
  19.214 +
  19.215 +in
  19.216 +
  19.217 +val cases_type = mk_att add_casesT consumes0;
  19.218 +val cases_set = mk_att add_casesS consumes1;
  19.219 +val induct_type = mk_att add_inductT consumes0;
  19.220 +val induct_set = mk_att add_inductS consumes1;
  19.221 +val coinduct_type = mk_att add_coinductT consumes0;
  19.222 +val coinduct_set = mk_att add_coinductS consumes1;
  19.223 +
  19.224 +end;
  19.225 +
  19.226 +
  19.227 +
  19.228 +(** attribute syntax **)
  19.229 +
  19.230 +val casesN = "cases";
  19.231 +val inductN = "induct";
  19.232 +val coinductN = "coinduct";
  19.233 +
  19.234 +val typeN = "type";
  19.235 +val setN = "set";
  19.236 +
  19.237 +local
  19.238 +
  19.239 +fun spec k arg =
  19.240 +  Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
  19.241 +  Scan.lift (Args.$$$ k) >> K "";
  19.242 +
  19.243 +fun attrib add_type add_set =
  19.244 +  Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
  19.245 +
  19.246 +val cases_att = attrib cases_type cases_set;
  19.247 +val induct_att = attrib induct_type induct_set;
  19.248 +val coinduct_att = attrib coinduct_type coinduct_set;
  19.249 +
  19.250 +in
  19.251 +
  19.252 +val attrib_setup = Attrib.add_attributes
  19.253 + [(casesN, cases_att, "declaration of cases rule for type or set"),
  19.254 +  (inductN, induct_att, "declaration of induction rule for type or set"),
  19.255 +  (coinductN, coinduct_att, "declaration of coinduction rule for type or set")];
  19.256 +
  19.257 +end;
  19.258 +
  19.259 +
  19.260 +
  19.261 +(** method utils **)
  19.262 +
  19.263 +(* alignment *)
  19.264 +
  19.265 +fun align_left msg xs ys =
  19.266 +  let val m = length xs and n = length ys
  19.267 +  in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
  19.268 +
  19.269 +fun align_right msg xs ys =
  19.270 +  let val m = length xs and n = length ys
  19.271 +  in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
  19.272 +
  19.273 +
  19.274 +(* prep_inst *)
  19.275 +
  19.276 +fun prep_inst thy align tune (tm, ts) =
  19.277 +  let
  19.278 +    val cert = Thm.cterm_of thy;
  19.279 +    fun prep_var (x, SOME t) =
  19.280 +          let
  19.281 +            val cx = cert x;
  19.282 +            val {T = xT, thy, ...} = Thm.rep_cterm cx;
  19.283 +            val ct = cert (tune t);
  19.284 +          in
  19.285 +            if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
  19.286 +            else error (Pretty.string_of (Pretty.block
  19.287 +             [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
  19.288 +              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
  19.289 +              Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
  19.290 +          end
  19.291 +      | prep_var (_, NONE) = NONE;
  19.292 +    val xs = vars_of tm;
  19.293 +  in
  19.294 +    align "Rule has fewer variables than instantiations given" xs ts
  19.295 +    |> map_filter prep_var
  19.296 +  end;
  19.297 +
  19.298 +
  19.299 +(* trace_rules *)
  19.300 +
  19.301 +fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule")
  19.302 +  | trace_rules ctxt _ rules = Method.trace ctxt rules;
  19.303 +
  19.304 +
  19.305 +(* make_cases *)
  19.306 +
  19.307 +fun make_cases is_open rule =
  19.308 +  RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
  19.309 +
  19.310 +fun warn_open true = legacy_feature "open rule cases in proof method"
  19.311 +  | warn_open false = ();
  19.312 +
  19.313 +
  19.314 +
  19.315 +(** cases method **)
  19.316 +
  19.317 +(*
  19.318 +  rule selection scheme:
  19.319 +          cases         - default case split
  19.320 +    `x:A` cases ...     - set cases
  19.321 +          cases t       - type cases
  19.322 +    ...   cases ... r   - explicit rule
  19.323 +*)
  19.324 +
  19.325 +local
  19.326 +
  19.327 +fun get_casesT ctxt ((SOME t :: _) :: _) = find_casesT ctxt (Term.fastype_of t)
  19.328 +  | get_casesT _ _ = [];
  19.329 +
  19.330 +fun get_casesS ctxt (fact :: _) = find_casesS ctxt (Thm.concl_of fact)
  19.331 +  | get_casesS _ _ = [];
  19.332 +
  19.333 +in
  19.334 +
  19.335 +fun cases_tac ctxt is_open insts opt_rule facts =
  19.336 +  let
  19.337 +    val _ = warn_open is_open;
  19.338 +    val thy = ProofContext.theory_of ctxt;
  19.339 +    val cert = Thm.cterm_of thy;
  19.340 +
  19.341 +    fun inst_rule r =
  19.342 +      if null insts then `RuleCases.get r
  19.343 +      else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
  19.344 +        |> maps (prep_inst thy align_left I)
  19.345 +        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
  19.346 +
  19.347 +    val ruleq =
  19.348 +      (case opt_rule of
  19.349 +        SOME r => Seq.single (inst_rule r)
  19.350 +      | NONE =>
  19.351 +          (get_casesS ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
  19.352 +          |> tap (trace_rules ctxt casesN)
  19.353 +          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
  19.354 +  in
  19.355 +    fn i => fn st =>
  19.356 +      ruleq
  19.357 +      |> Seq.maps (RuleCases.consume [] facts)
  19.358 +      |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
  19.359 +        CASES (make_cases is_open rule cases)
  19.360 +          (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
  19.361 +  end;
  19.362 +
  19.363 +end;
  19.364 +
  19.365 +
  19.366 +
  19.367 +(** induct method **)
  19.368 +
  19.369 +val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}];
  19.370 +
  19.371 +
  19.372 +(* atomize *)
  19.373 +
  19.374 +fun atomize_term thy =
  19.375 +  MetaSimplifier.rewrite_term thy Data.atomize []
  19.376 +  #> ObjectLogic.drop_judgment thy;
  19.377 +
  19.378 +val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
  19.379 +
  19.380 +val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize;
  19.381 +
  19.382 +val inner_atomize_tac =
  19.383 +  Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
  19.384 +
  19.385 +
  19.386 +(* rulify *)
  19.387 +
  19.388 +fun rulify_term thy =
  19.389 +  MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
  19.390 +  MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
  19.391 +
  19.392 +fun rulified_term thm =
  19.393 +  let
  19.394 +    val thy = Thm.theory_of_thm thm;
  19.395 +    val rulify = rulify_term thy;
  19.396 +    val (As, B) = Logic.strip_horn (Thm.prop_of thm);
  19.397 +  in (thy, Logic.list_implies (map rulify As, rulify B)) end;
  19.398 +
  19.399 +val rulify_tac =
  19.400 +  Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
  19.401 +  Simplifier.rewrite_goal_tac Data.rulify_fallback THEN'
  19.402 +  Goal.conjunction_tac THEN_ALL_NEW
  19.403 +  (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
  19.404 +
  19.405 +
  19.406 +(* prepare rule *)
  19.407 +
  19.408 +fun rule_instance thy inst rule =
  19.409 +  Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
  19.410 +
  19.411 +fun internalize k th =
  19.412 +  th |> Thm.permute_prems 0 k
  19.413 +  |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
  19.414 +
  19.415 +
  19.416 +(* guess rule instantiation -- cannot handle pending goal parameters *)
  19.417 +
  19.418 +local
  19.419 +
  19.420 +fun dest_env thy (env as Envir.Envir {iTs, ...}) =
  19.421 +  let
  19.422 +    val cert = Thm.cterm_of thy;
  19.423 +    val certT = Thm.ctyp_of thy;
  19.424 +    val pairs = Envir.alist_of env;
  19.425 +    val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
  19.426 +    val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
  19.427 +  in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
  19.428 +
  19.429 +in
  19.430 +
  19.431 +fun guess_instance rule i st =
  19.432 +  let
  19.433 +    val {thy, maxidx, ...} = Thm.rep_thm st;
  19.434 +    val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
  19.435 +    val params = rev (rename_wrt_term goal (Logic.strip_params goal));
  19.436 +  in
  19.437 +    if not (null params) then
  19.438 +      (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
  19.439 +        commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params));
  19.440 +      Seq.single rule)
  19.441 +    else
  19.442 +      let
  19.443 +        val rule' = Thm.incr_indexes (maxidx + 1) rule;
  19.444 +        val concl = Logic.strip_assums_concl goal;
  19.445 +      in
  19.446 +        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
  19.447 +          (Envir.empty (#maxidx (Thm.rep_thm rule')))
  19.448 +        |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
  19.449 +      end
  19.450 +  end handle Subscript => Seq.empty;
  19.451 +
  19.452 +end;
  19.453 +
  19.454 +
  19.455 +(* special renaming of rule parameters *)
  19.456 +
  19.457 +fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
  19.458 +      let
  19.459 +        val x = ProofContext.revert_skolem ctxt z;
  19.460 +        fun index i [] = []
  19.461 +          | index i (y :: ys) =
  19.462 +              if x = y then x ^ string_of_int i :: index (i + 1) ys
  19.463 +              else y :: index i ys;
  19.464 +        fun rename_params [] = []
  19.465 +          | rename_params ((y, Type (U, _)) :: ys) =
  19.466 +              (if U = T then x else y) :: rename_params ys
  19.467 +          | rename_params ((y, _) :: ys) = y :: rename_params ys;
  19.468 +        fun rename_asm A =
  19.469 +          let
  19.470 +            val xs = rename_params (Logic.strip_params A);
  19.471 +            val xs' =
  19.472 +              (case List.filter (equal x) xs of
  19.473 +                [] => xs | [_] => xs | _ => index 1 xs);
  19.474 +          in Logic.list_rename_params (xs', A) end;
  19.475 +        fun rename_prop p =
  19.476 +          let val (As, C) = Logic.strip_horn p
  19.477 +          in Logic.list_implies (map rename_asm As, C) end;
  19.478 +        val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
  19.479 +        val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
  19.480 +      in [RuleCases.save thm thm'] end
  19.481 +  | special_rename_params _ _ ths = ths;
  19.482 +
  19.483 +
  19.484 +(* fix_tac *)
  19.485 +
  19.486 +local
  19.487 +
  19.488 +fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
  19.489 +  | goal_prefix 0 _ = Term.dummy_pattern propT
  19.490 +  | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
  19.491 +  | goal_prefix _ _ = Term.dummy_pattern propT;
  19.492 +
  19.493 +fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
  19.494 +  | goal_params 0 _ = 0
  19.495 +  | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B
  19.496 +  | goal_params _ _ = 0;
  19.497 +
  19.498 +fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
  19.499 +  let
  19.500 +    val thy = ProofContext.theory_of ctxt;
  19.501 +    val cert = Thm.cterm_of thy;
  19.502 +    val certT = Thm.ctyp_of thy;
  19.503 +
  19.504 +    val v = Free (x, T);
  19.505 +    fun spec_rule prfx (xs, body) =
  19.506 +      @{thm Pure.meta_spec}
  19.507 +      |> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1)
  19.508 +      |> Thm.lift_rule (cert prfx)
  19.509 +      |> `(Thm.prop_of #> Logic.strip_assums_concl)
  19.510 +      |-> (fn pred $ arg =>
  19.511 +        Drule.cterm_instantiate
  19.512 +          [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
  19.513 +           (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
  19.514 +
  19.515 +    fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
  19.516 +      | goal_concl 0 xs B =
  19.517 +          if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
  19.518 +          else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
  19.519 +      | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
  19.520 +      | goal_concl _ _ _ = NONE;
  19.521 +  in
  19.522 +    (case goal_concl n [] goal of
  19.523 +      SOME concl =>
  19.524 +        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
  19.525 +    | NONE => all_tac)
  19.526 +  end);
  19.527 +
  19.528 +fun miniscope_tac p =
  19.529 +  CONVERSION (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
  19.530 +
  19.531 +in
  19.532 +
  19.533 +fun fix_tac _ _ [] = K all_tac
  19.534 +  | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
  19.535 +     (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
  19.536 +      (miniscope_tac (goal_params n goal))) i);
  19.537 +
  19.538 +end;
  19.539 +
  19.540 +
  19.541 +(* add_defs *)
  19.542 +
  19.543 +fun add_defs def_insts =
  19.544 +  let
  19.545 +    fun add (SOME (SOME x, t)) ctxt =
  19.546 +          let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt
  19.547 +          in ((SOME lhs, [th]), ctxt') end
  19.548 +      | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
  19.549 +      | add NONE ctxt = ((NONE, []), ctxt);
  19.550 +  in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
  19.551 +
  19.552 +
  19.553 +(* induct_tac *)
  19.554 +
  19.555 +(*
  19.556 +  rule selection scheme:
  19.557 +    `x:A` induct ...     - set induction
  19.558 +          induct x       - type induction
  19.559 +    ...   induct ... r   - explicit rule
  19.560 +*)
  19.561 +
  19.562 +local
  19.563 +
  19.564 +fun get_inductT ctxt insts =
  19.565 +  fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts)
  19.566 +    |> map (find_inductT ctxt o Term.fastype_of)) [[]]
  19.567 +  |> filter_out (forall PureThy.is_internal);
  19.568 +
  19.569 +fun get_inductS ctxt (fact :: _) = map single (find_inductS ctxt (Thm.concl_of fact))
  19.570 +  | get_inductS _ _ = [];
  19.571 +
  19.572 +in
  19.573 +
  19.574 +fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
  19.575 +  let
  19.576 +    val _ = warn_open is_open;
  19.577 +    val thy = ProofContext.theory_of ctxt;
  19.578 +    val cert = Thm.cterm_of thy;
  19.579 +
  19.580 +    val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
  19.581 +    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
  19.582 +
  19.583 +    fun inst_rule (concls, r) =
  19.584 +      (if null insts then `RuleCases.get r
  19.585 +       else (align_left "Rule has fewer conclusions than arguments given"
  19.586 +          (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
  19.587 +        |> maps (prep_inst thy align_right (atomize_term thy))
  19.588 +        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
  19.589 +      |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
  19.590 +
  19.591 +    val ruleq =
  19.592 +      (case opt_rule of
  19.593 +        SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
  19.594 +      | NONE =>
  19.595 +          (get_inductS ctxt facts @
  19.596 +            map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
  19.597 +          |> map_filter (RuleCases.mutual_rule ctxt)
  19.598 +          |> tap (trace_rules ctxt inductN o map #2)
  19.599 +          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
  19.600 +
  19.601 +    fun rule_cases rule =
  19.602 +      RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule);
  19.603 +  in
  19.604 +    (fn i => fn st =>
  19.605 +      ruleq
  19.606 +      |> Seq.maps (RuleCases.consume (flat defs) facts)
  19.607 +      |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
  19.608 +        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
  19.609 +          (CONJUNCTS (ALLGOALS
  19.610 +            (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
  19.611 +              THEN' fix_tac defs_ctxt
  19.612 +                (nth concls (j - 1) + more_consumes)
  19.613 +                (nth_list arbitrary (j - 1))))
  19.614 +          THEN' inner_atomize_tac) j))
  19.615 +        THEN' atomize_tac) i st |> Seq.maps (fn st' =>
  19.616 +            guess_instance (internalize more_consumes rule) i st'
  19.617 +            |> Seq.map (rule_instance thy taking)
  19.618 +            |> Seq.maps (fn rule' =>
  19.619 +              CASES (rule_cases rule' cases)
  19.620 +                (Tactic.rtac rule' i THEN
  19.621 +                  PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
  19.622 +    THEN_ALL_NEW_CASES rulify_tac
  19.623 +  end;
  19.624 +
  19.625 +end;
  19.626 +
  19.627 +
  19.628 +
  19.629 +(** coinduct method **)
  19.630 +
  19.631 +(*
  19.632 +  rule selection scheme:
  19.633 +    goal "x:A" coinduct ...   - set coinduction
  19.634 +               coinduct x     - type coinduction
  19.635 +               coinduct ... r - explicit rule
  19.636 +*)
  19.637 +
  19.638 +local
  19.639 +
  19.640 +fun get_coinductT ctxt (SOME t :: _) = find_coinductT ctxt (Term.fastype_of t)
  19.641 +  | get_coinductT _ _ = [];
  19.642 +
  19.643 +fun get_coinductS ctxt goal = find_coinductS ctxt (Logic.strip_assums_concl goal);
  19.644 +
  19.645 +in
  19.646 +
  19.647 +fun coinduct_tac ctxt is_open inst taking opt_rule facts =
  19.648 +  let
  19.649 +    val _ = warn_open is_open;
  19.650 +    val thy = ProofContext.theory_of ctxt;
  19.651 +    val cert = Thm.cterm_of thy;
  19.652 +
  19.653 +    fun inst_rule r =
  19.654 +      if null inst then `RuleCases.get r
  19.655 +      else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r
  19.656 +        |> pair (RuleCases.get r);
  19.657 +
  19.658 +    fun ruleq goal =
  19.659 +      (case opt_rule of
  19.660 +        SOME r => Seq.single (inst_rule r)
  19.661 +      | NONE =>
  19.662 +          (get_coinductS ctxt goal @ get_coinductT ctxt inst)
  19.663 +          |> tap (trace_rules ctxt coinductN)
  19.664 +          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
  19.665 +  in
  19.666 +    SUBGOAL_CASES (fn (goal, i) => fn st =>
  19.667 +      ruleq goal
  19.668 +      |> Seq.maps (RuleCases.consume [] facts)
  19.669 +      |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
  19.670 +        guess_instance rule i st
  19.671 +        |> Seq.map (rule_instance thy taking)
  19.672 +        |> Seq.maps (fn rule' =>
  19.673 +          CASES (make_cases is_open rule' cases)
  19.674 +            (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
  19.675 +  end;
  19.676 +
  19.677 +end;
  19.678 +
  19.679 +
  19.680 +
  19.681 +(** concrete syntax **)
  19.682 +
  19.683 +val openN = "open";
  19.684 +val arbitraryN = "arbitrary";
  19.685 +val takingN = "taking";
  19.686 +val ruleN = "rule";
  19.687 +
  19.688 +local
  19.689 +
  19.690 +fun single_rule [rule] = rule
  19.691 +  | single_rule _ = error "Single rule expected";
  19.692 +
  19.693 +fun named_rule k arg get =
  19.694 +  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
  19.695 +    (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
  19.696 +      (case get (Context.proof_of context) name of SOME x => x
  19.697 +      | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
  19.698 +
  19.699 +fun rule get_type get_set =
  19.700 +  named_rule typeN Args.tyname get_type ||
  19.701 +  named_rule setN Args.const get_set ||
  19.702 +  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
  19.703 +
  19.704 +val cases_rule = rule lookup_casesT lookup_casesS >> single_rule;
  19.705 +val induct_rule = rule lookup_inductT lookup_inductS;
  19.706 +val coinduct_rule = rule lookup_coinductT lookup_coinductS >> single_rule;
  19.707 +
  19.708 +val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
  19.709 +
  19.710 +val def_inst =
  19.711 +  ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
  19.712 +      -- Args.term) >> SOME ||
  19.713 +    inst >> Option.map (pair NONE);
  19.714 +
  19.715 +val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
  19.716 +  error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
  19.717 +
  19.718 +fun unless_more_args scan = Scan.unless (Scan.lift
  19.719 +  ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||
  19.720 +    Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
  19.721 +
  19.722 +val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
  19.723 +  Args.and_list1 (Scan.repeat (unless_more_args free))) [];
  19.724 +
  19.725 +val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
  19.726 +  Scan.repeat1 (unless_more_args inst)) [];
  19.727 +
  19.728 +in
  19.729 +
  19.730 +fun cases_meth src =
  19.731 +  Method.syntax (Args.mode openN --
  19.732 +    (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src
  19.733 +  #> (fn ((is_open, (insts, opt_rule)), ctxt) =>
  19.734 +    Method.METHOD_CASES (fn facts =>
  19.735 +      Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts))));
  19.736 +
  19.737 +fun induct_meth src =
  19.738 +  Method.syntax (Args.mode openN --
  19.739 +    (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
  19.740 +    (arbitrary -- taking -- Scan.option induct_rule))) src
  19.741 +  #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) =>
  19.742 +    Method.RAW_METHOD_CASES (fn facts =>
  19.743 +      Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts))));
  19.744 +
  19.745 +fun coinduct_meth src =
  19.746 +  Method.syntax (Args.mode openN --
  19.747 +    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src
  19.748 +  #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) =>
  19.749 +    Method.RAW_METHOD_CASES (fn facts =>
  19.750 +      Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts))));
  19.751 +
  19.752 +end;
  19.753 +
  19.754 +
  19.755 +
  19.756 +(** theory setup **)
  19.757 +
  19.758 +val setup =
  19.759 +  attrib_setup #>
  19.760 +  Method.add_methods
  19.761 +    [(casesN, cases_meth, "case analysis on types or sets"),
  19.762 +     (inductN, induct_meth, "induction on types or sets"),
  19.763 +     (coinductN, coinduct_meth, "coinduction on types or sets")];
  19.764 +
  19.765 +end;
    20.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Oct 04 14:42:11 2007 +0200
    20.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Oct 04 14:42:47 2007 +0200
    20.3 @@ -506,7 +506,7 @@
    20.4       val ([induct', mutual_induct'], thy') =
    20.5         thy
    20.6         |> PureThy.add_thms [((co_prefix ^ "induct", induct),
    20.7 -             [case_names, InductAttrib.induct_set big_rec_name]),
    20.8 +             [case_names, Induct.induct_set big_rec_name]),
    20.9             (("mutual_induct", mutual_induct), [case_names])];
   20.10      in ((thy', induct'), mutual_induct')
   20.11      end;  (*of induction_rules*)
   20.12 @@ -528,7 +528,7 @@
   20.13      |> PureThy.add_thms
   20.14        [(("bnd_mono", bnd_mono), []),
   20.15         (("dom_subset", dom_subset), []),
   20.16 -       (("cases", elim), [case_names, InductAttrib.cases_set big_rec_name])]
   20.17 +       (("cases", elim), [case_names, Induct.cases_set big_rec_name])]
   20.18      ||>> (PureThy.add_thmss o map Thm.no_attributes)
   20.19          [("defs", defs),
   20.20           ("intros", intrs)];