moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.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)];