# HG changeset patch # User wenzelm # Date 1191501767 -7200 # Node ID a7b3ab44d993dbd94bb07f112951292c4427b056 # Parent e1214fa781cae3be1a8dd0acec4fee05e69b798d moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML; diff -r e1214fa781ca -r a7b3ab44d993 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Thu Oct 04 14:42:11 2007 +0200 +++ b/src/FOL/FOL.thy Thu Oct 04 14:42:47 2007 +0200 @@ -11,6 +11,7 @@ "~~/src/Provers/classical.ML" "~~/src/Provers/blast.ML" "~~/src/Provers/clasimp.ML" + "~~/src/Tools/induct.ML" ("cladata.ML") ("blastdata.ML") ("simpdata.ML") @@ -74,7 +75,7 @@ apply (erule r1) done -lemmas case_split = case_split_thm [case_names True False, cases type: o] +lemmas case_split = case_split_thm [case_names True False] (*HOL's more natural case analysis tactic*) ML {* @@ -273,15 +274,16 @@ text {* Method setup. *} ML {* - structure InductMethod = InductMethodFun - (struct + structure Induct = InductFun + ( val cases_default = @{thm case_split} val atomize = @{thms induct_atomize} val rulify = @{thms induct_rulify} val rulify_fallback = @{thms induct_rulify_fallback} - end); + ); *} -setup InductMethod.setup +setup Induct.setup +declare case_split [cases type: o] end diff -r e1214fa781ca -r a7b3ab44d993 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Thu Oct 04 14:42:11 2007 +0200 +++ b/src/FOL/IFOL.thy Thu Oct 04 14:42:47 2007 +0200 @@ -15,7 +15,6 @@ "~~/src/Tools/IsaPlanner/rw_tools.ML" "~~/src/Tools/IsaPlanner/rw_inst.ML" "~~/src/Provers/eqsubst.ML" - "~~/src/Provers/induct_method.ML" "~~/src/Provers/quantifier1.ML" "~~/src/Provers/project_rule.ML" ("fologic.ML") diff -r e1214fa781ca -r a7b3ab44d993 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Thu Oct 04 14:42:11 2007 +0200 +++ b/src/FOL/IsaMakefile Thu Oct 04 14:42:47 2007 +0200 @@ -35,7 +35,7 @@ $(SRC)/Tools/IsaPlanner/rw_tools.ML \ $(SRC)/Tools/IsaPlanner/rw_inst.ML \ $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ - $(SRC)/Provers/induct_method.ML \ + $(SRC)/Tools/induct.ML \ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML cladata.ML \ document/root.tex fologic.ML hypsubstdata.ML intprover.ML simpdata.ML diff -r e1214fa781ca -r a7b3ab44d993 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Oct 04 14:42:11 2007 +0200 +++ b/src/HOL/HOL.thy Thu Oct 04 14:42:47 2007 +0200 @@ -14,7 +14,6 @@ "~~/src/Tools/IsaPlanner/rw_tools.ML" "~~/src/Tools/IsaPlanner/rw_inst.ML" "~~/src/Provers/project_rule.ML" - "~~/src/Provers/induct_method.ML" "~~/src/Provers/hypsubst.ML" "~~/src/Provers/splitter.ML" "~~/src/Provers/classical.ML" @@ -29,6 +28,7 @@ "~~/src/Tools/code/code_target.ML" "~~/src/Tools/code/code_package.ML" "~~/src/Tools/nbe.ML" + "~~/src/Tools/induct.ML" begin subsection {* Primitive logic *} @@ -1545,17 +1545,16 @@ text {* Method setup. *} ML {* - structure InductMethod = InductMethodFun - (struct + structure Induct = InductFun + ( val cases_default = @{thm case_split} val atomize = @{thms induct_atomize} val rulify = @{thms induct_rulify} val rulify_fallback = @{thms induct_rulify_fallback} - end); + ); *} -setup InductMethod.setup - +setup Induct.setup subsection {* Other simple lemmas and lemma duplicates *} @@ -1711,7 +1710,7 @@ val all_conj_distrib = thm "all_conj_distrib"; val all_simps = thms "all_simps"; val atomize_not = thm "atomize_not"; -val case_split = thm "case_split_thm"; +val case_split = thm "case_split"; val case_split_thm = thm "case_split_thm" val cases_simp = thm "cases_simp"; val choice_eq = thm "choice_eq" diff -r e1214fa781ca -r a7b3ab44d993 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Oct 04 14:42:11 2007 +0200 +++ b/src/HOL/IsaMakefile Thu Oct 04 14:42:47 2007 +0200 @@ -79,10 +79,10 @@ $(SRC)/Tools/IsaPlanner/isand.ML \ $(SRC)/Tools/IsaPlanner/rw_inst.ML \ $(SRC)/Tools/IsaPlanner/rw_tools.ML \ - $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML \ + $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/induct.ML $(SRC)/Provers/blast.ML \ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ - $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML \ + $(SRC)/Provers/order.ML \ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \ $(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML\ diff -r e1214fa781ca -r a7b3ab44d993 src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/HOL/Nominal/nominal_induct.ML Thu Oct 04 14:42:47 2007 +0200 @@ -43,7 +43,7 @@ fun subst inst concl = let - val vars = InductAttrib.vars_of concl; + val vars = Induct.vars_of concl; val m = length vars and n = length inst; val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule"; val P :: x :: ys = vars; @@ -87,13 +87,13 @@ val thy = ProofContext.theory_of ctxt; val cert = Thm.cterm_of thy; - val ((insts, defs), defs_ctxt) = fold_map InductMethod.add_defs def_insts ctxt |>> split_list; + val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; val finish_rule = split_all_tuples #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding); - fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (InductMethod.rulified_term r); + fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r); in (fn i => fn st => rules @@ -103,18 +103,18 @@ (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => (CONJUNCTS (ALLGOALS (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1)) - THEN' InductMethod.fix_tac defs_ctxt + THEN' Induct.fix_tac defs_ctxt (nth concls (j - 1) + more_consumes) (nth_list fixings (j - 1)))) - THEN' InductMethod.inner_atomize_tac) j)) - THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' => - InductMethod.guess_instance - (finish_rule (InductMethod.internalize more_consumes rule)) i st' + THEN' Induct.inner_atomize_tac) j)) + THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' => + Induct.guess_instance + (finish_rule (Induct.internalize more_consumes rule)) i st' |> Seq.maps (fn rule' => CASES (rule_cases rule' cases) (Tactic.rtac (rename_params_rule false [] rule') i THEN PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) - THEN_ALL_NEW_CASES InductMethod.rulify_tac + THEN_ALL_NEW_CASES Induct.rulify_tac end; diff -r e1214fa781ca -r a7b3ab44d993 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Thu Oct 04 14:42:47 2007 +0200 @@ -148,7 +148,7 @@ | xs => error ("Missing equivariance theorem for predicate(s): " ^ commas_quote xs)); val induct_cases = map fst (fst (RuleCases.get (the - (InductAttrib.lookup_inductS ctxt (hd names))))); + (Induct.lookup_inductS ctxt (hd names))))); val raw_induct' = Logic.unvarify (prop_of raw_induct); val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb); diff -r e1214fa781ca -r a7b3ab44d993 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/HOL/Tools/datatype_package.ML Thu Oct 04 14:42:47 2007 +0200 @@ -205,7 +205,7 @@ | prep_var _ = NONE; fun prep_inst (concl, xs) = (*exception Library.UnequalLengths*) - let val vs = InductAttrib.vars_of concl + let val vs = Induct.vars_of concl in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end; in @@ -340,10 +340,10 @@ val inducts = ProjectRule.projections (ProofContext.init thy) induction; fun named_rules (name, {index, exhaustion, ...}: datatype_info) = - [(("", nth inducts index), [InductAttrib.induct_type name]), - (("", exhaustion), [InductAttrib.cases_type name])]; + [(("", nth inducts index), [Induct.induct_type name]), + (("", exhaustion), [Induct.cases_type name])]; fun unnamed_rule i = - (("", nth inducts i), [PureThy.kind_internal, InductAttrib.induct_type ""]); + (("", nth inducts i), [PureThy.kind_internal, Induct.induct_type ""]); in thy |> PureThy.add_thms (maps named_rules infos @ diff -r e1214fa781ca -r a7b3ab44d993 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Oct 04 14:42:47 2007 +0200 @@ -73,7 +73,7 @@ |> addsmps "psimps" [] psimps ||> fold_option (snd oo addsmps "simps" []) trsimps ||>> note_theorem ((qualify "pinduct", - [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts) + [Attrib.internal (K (Induct.induct_set ""))]), simple_pinducts) ||>> note_theorem ((qualify "termination", []), [termination]) ||> (snd o note_theorem ((qualify "cases", []), [cases])) ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros diff -r e1214fa781ca -r a7b3ab44d993 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/HOL/Tools/inductive_package.ML Thu Oct 04 14:42:47 2007 +0200 @@ -433,7 +433,7 @@ error (Pretty.string_of (Pretty.block [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop])); - val elims = InductAttrib.find_casesS ctxt prop; + val elims = Induct.find_casesS ctxt prop; val cprop = Thm.cterm_of thy prop; val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac; @@ -679,7 +679,7 @@ if coind then (raw_induct, [RuleCases.case_names [rec_name], RuleCases.case_conclusion (rec_name, intr_names), - RuleCases.consumes 1, InductAttrib.coinduct_set (hd cnames)]) + RuleCases.consumes 1, Induct.coinduct_set (hd cnames)]) else if no_ind orelse length cnames > 1 then (raw_induct, [ind_case_names, RuleCases.consumes 0]) else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]); @@ -698,7 +698,7 @@ LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases", [Attrib.internal (K (RuleCases.case_names cases)), Attrib.internal (K (RuleCases.consumes 1)), - Attrib.internal (K (InductAttrib.cases_set name)), + Attrib.internal (K (Induct.cases_set name)), Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #> apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>> LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"), @@ -712,7 +712,7 @@ inducts |> map (fn (name, th) => ([th], [Attrib.internal (K ind_case_names), Attrib.internal (K (RuleCases.consumes 1)), - Attrib.internal (K (InductAttrib.induct_set name))])))] |> snd + Attrib.internal (K (Induct.induct_set name))])))] |> snd end in (intrs', elims', induct', ctxt3) end; diff -r e1214fa781ca -r a7b3ab44d993 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/HOL/Tools/record_package.ML Thu Oct 04 14:42:47 2007 +0200 @@ -1372,8 +1372,8 @@ (* attributes *) fun case_names_fields x = RuleCases.case_names ["fields"] x; -fun induct_type_global name = [case_names_fields, InductAttrib.induct_type name]; -fun cases_type_global name = [case_names_fields, InductAttrib.cases_type name]; +fun induct_type_global name = [case_names_fields, Induct.induct_type name]; +fun cases_type_global name = [case_names_fields, Induct.cases_type name]; (* tactics *) diff -r e1214fa781ca -r a7b3ab44d993 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/HOL/Tools/typedef_package.ML Thu Oct 04 14:42:47 2007 +0200 @@ -176,13 +176,13 @@ ((Rep_name ^ "_inject", make Rep_inject), []), ((Abs_name ^ "_inject", abs_inject), []), ((Rep_name ^ "_cases", make Rep_cases), - [RuleCases.case_names [Rep_name], InductAttrib.cases_set full_name]), + [RuleCases.case_names [Rep_name], Induct.cases_set full_name]), ((Abs_name ^ "_cases", make Abs_cases), - [RuleCases.case_names [Abs_name], InductAttrib.cases_type full_tname]), + [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]), ((Rep_name ^ "_induct", make Rep_induct), - [RuleCases.case_names [Rep_name], InductAttrib.induct_set full_name]), + [RuleCases.case_names [Rep_name], Induct.induct_set full_name]), ((Abs_name ^ "_induct", make Abs_induct), - [RuleCases.case_names [Abs_name], InductAttrib.induct_type full_tname])]) + [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])]) ||> Sign.parent_path; val info = {rep_type = oldT, abs_type = newT, Rep_name = full Rep_name, Abs_name = full Abs_name, diff -r e1214fa781ca -r a7b3ab44d993 src/Provers/induct_method.ML --- a/src/Provers/induct_method.ML Thu Oct 04 14:42:11 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,550 +0,0 @@ -(* Title: Provers/induct_method.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -Proof by cases and induction on sets and types. -*) - -signature INDUCT_METHOD_DATA = -sig - val cases_default: thm - val atomize: thm list - val rulify: thm list - val rulify_fallback: thm list -end; - -signature INDUCT_METHOD = -sig - val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic - val add_defs: (string option * term) option list -> Proof.context -> - (term option list * thm list) * Proof.context - val atomize_term: theory -> term -> term - val atomize_tac: int -> tactic - val inner_atomize_tac: int -> tactic - val rulified_term: thm -> theory * term - val rulify_tac: int -> tactic - val internalize: int -> thm -> thm - val guess_instance: thm -> int -> thm -> thm Seq.seq - val cases_tac: Proof.context -> bool -> term option list list -> thm option -> - thm list -> int -> cases_tactic - val induct_tac: Proof.context -> bool -> (string option * term) option list list -> - (string * typ) list list -> term option list -> thm list option -> thm list -> int -> - cases_tactic - val coinduct_tac: Proof.context -> bool -> term option list -> term option list -> - thm option -> thm list -> int -> cases_tactic - val setup: theory -> theory -end; - -functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD = -struct - -val meta_spec = thm "Pure.meta_spec"; -val all_conjunction = thm "Pure.all_conjunction"; -val imp_conjunction = thm "Pure.imp_conjunction"; -val conjunction_imp = thm "Pure.conjunction_imp"; -val conjunction_congs = [all_conjunction, imp_conjunction]; - - - -(** misc utils **) - -(* alignment *) - -fun align_left msg xs ys = - let val m = length xs and n = length ys - in if m < n then error msg else (Library.take (n, xs) ~~ ys) end; - -fun align_right msg xs ys = - let val m = length xs and n = length ys - in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end; - - -(* prep_inst *) - -fun prep_inst thy align tune (tm, ts) = - let - val cert = Thm.cterm_of thy; - fun prep_var (x, SOME t) = - let - val cx = cert x; - val {T = xT, thy, ...} = Thm.rep_cterm cx; - val ct = cert (tune t); - in - if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct) - else error (Pretty.string_of (Pretty.block - [Pretty.str "Ill-typed instantiation:", Pretty.fbrk, - Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, - Display.pretty_ctyp (#T (Thm.crep_cterm ct))])) - end - | prep_var (_, NONE) = NONE; - val xs = InductAttrib.vars_of tm; - in - align "Rule has fewer variables than instantiations given" xs ts - |> map_filter prep_var - end; - - -(* trace_rules *) - -fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule") - | trace_rules ctxt _ rules = Method.trace ctxt rules; - - -(* make_cases *) - -fun make_cases is_open rule = - RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule); - -fun warn_open true = legacy_feature "open rule cases in proof method" - | warn_open false = (); - - - -(** cases method **) - -(* - rule selection scheme: - cases - default case split - `x:A` cases ... - set cases - cases t - type cases - ... cases ... r - explicit rule -*) - -local - -fun find_casesT ctxt ((SOME t :: _) :: _) = InductAttrib.find_casesT ctxt (Term.fastype_of t) - | find_casesT _ _ = []; - -fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt (Thm.concl_of fact) - | find_casesS _ _ = []; - -in - -fun cases_tac ctxt is_open insts opt_rule facts = - let - val _ = warn_open is_open; - val thy = ProofContext.theory_of ctxt; - val cert = Thm.cterm_of thy; - - fun inst_rule r = - if null insts then `RuleCases.get r - else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts - |> maps (prep_inst thy align_left I) - |> Drule.cterm_instantiate) r |> pair (RuleCases.get r); - - val ruleq = - (case opt_rule of - SOME r => Seq.single (inst_rule r) - | NONE => - (find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default]) - |> tap (trace_rules ctxt InductAttrib.casesN) - |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); - in - fn i => fn st => - ruleq - |> Seq.maps (RuleCases.consume [] facts) - |> Seq.maps (fn ((cases, (_, more_facts)), rule) => - CASES (make_cases is_open rule cases) - (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st) - end; - -end; - - - -(** induct method **) - -(* atomize *) - -fun atomize_term thy = - MetaSimplifier.rewrite_term thy Data.atomize [] - #> ObjectLogic.drop_judgment thy; - -val atomize_cterm = MetaSimplifier.rewrite true Data.atomize; - -val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize; - -val inner_atomize_tac = - Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac; - - -(* rulify *) - -fun rulify_term thy = - MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #> - MetaSimplifier.rewrite_term thy Data.rulify_fallback []; - -fun rulified_term thm = - let - val thy = Thm.theory_of_thm thm; - val rulify = rulify_term thy; - val (As, B) = Logic.strip_horn (Thm.prop_of thm); - in (thy, Logic.list_implies (map rulify As, rulify B)) end; - -val rulify_tac = - Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN' - Simplifier.rewrite_goal_tac Data.rulify_fallback THEN' - Goal.conjunction_tac THEN_ALL_NEW - (Simplifier.rewrite_goal_tac [conjunction_imp] THEN' Goal.norm_hhf_tac); - - -(* prepare rule *) - -fun rule_instance thy inst rule = - Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule; - -fun internalize k th = - th |> Thm.permute_prems 0 k - |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm); - - -(* guess rule instantiation -- cannot handle pending goal parameters *) - -local - -fun dest_env thy (env as Envir.Envir {iTs, ...}) = - let - val cert = Thm.cterm_of thy; - val certT = Thm.ctyp_of thy; - val pairs = Envir.alist_of env; - val ts = map (cert o Envir.norm_term env o #2 o #2) pairs; - val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts); - in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end; - -in - -fun guess_instance rule i st = - let - val {thy, maxidx, ...} = Thm.rep_thm st; - val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) - val params = rev (rename_wrt_term goal (Logic.strip_params goal)); - in - if not (null params) then - (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ - commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params)); - Seq.single rule) - else - let - val rule' = Thm.incr_indexes (maxidx + 1) rule; - val concl = Logic.strip_assums_concl goal; - in - Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] - (Envir.empty (#maxidx (Thm.rep_thm rule'))) - |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule') - end - end handle Subscript => Seq.empty; - -end; - - -(* special renaming of rule parameters *) - -fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] = - let - val x = ProofContext.revert_skolem ctxt z; - fun index i [] = [] - | index i (y :: ys) = - if x = y then x ^ string_of_int i :: index (i + 1) ys - else y :: index i ys; - fun rename_params [] = [] - | rename_params ((y, Type (U, _)) :: ys) = - (if U = T then x else y) :: rename_params ys - | rename_params ((y, _) :: ys) = y :: rename_params ys; - fun rename_asm A = - let - val xs = rename_params (Logic.strip_params A); - val xs' = - (case List.filter (equal x) xs of - [] => xs | [_] => xs | _ => index 1 xs); - in Logic.list_rename_params (xs', A) end; - fun rename_prop p = - let val (As, C) = Logic.strip_horn p - in Logic.list_implies (map rename_asm As, C) end; - val cp' = cterm_fun rename_prop (Thm.cprop_of thm); - val thm' = Thm.equal_elim (Thm.reflexive cp') thm; - in [RuleCases.save thm thm'] end - | special_rename_params _ _ ths = ths; - - -(* fix_tac *) - -local - -fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B) - | goal_prefix 0 _ = Term.dummy_pattern propT - | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B - | goal_prefix _ _ = Term.dummy_pattern propT; - -fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1 - | goal_params 0 _ = 0 - | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B - | goal_params _ _ = 0; - -fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) => - let - val thy = ProofContext.theory_of ctxt; - val cert = Thm.cterm_of thy; - val certT = Thm.ctyp_of thy; - - val v = Free (x, T); - fun spec_rule prfx (xs, body) = - meta_spec - |> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1) - |> Thm.lift_rule (cert prfx) - |> `(Thm.prop_of #> Logic.strip_assums_concl) - |-> (fn pred $ arg => - Drule.cterm_instantiate - [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))), - (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]); - - fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B - | goal_concl 0 xs B = - if not (Term.exists_subterm (fn t => t aconv v) B) then NONE - else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B)) - | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B - | goal_concl _ _ _ = NONE; - in - (case goal_concl n [] goal of - SOME concl => - (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i - | NONE => all_tac) - end); - -fun miniscope_tac p = - CONVERSION (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq])); - -in - -fun fix_tac _ _ [] = K all_tac - | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) => - (EVERY' (map (meta_spec_tac ctxt n) xs) THEN' - (miniscope_tac (goal_params n goal))) i); - -end; - - -(* add_defs *) - -fun add_defs def_insts = - let - fun add (SOME (SOME x, t)) ctxt = - let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt - in ((SOME lhs, [th]), ctxt') end - | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt) - | add NONE ctxt = ((NONE, []), ctxt); - in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; - - -(* induct_tac *) - -(* - rule selection scheme: - `x:A` induct ... - set induction - induct x - type induction - ... induct ... r - explicit rule -*) - -local - -fun find_inductT ctxt insts = - fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts) - |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]] - |> filter_out (forall PureThy.is_internal); - -fun find_inductS ctxt (fact :: _) = map single (InductAttrib.find_inductS ctxt (Thm.concl_of fact)) - | find_inductS _ _ = []; - -in - -fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts = - let - val _ = warn_open is_open; - val thy = ProofContext.theory_of ctxt; - val cert = Thm.cterm_of thy; - - val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; - val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; - - fun inst_rule (concls, r) = - (if null insts then `RuleCases.get r - else (align_left "Rule has fewer conclusions than arguments given" - (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts - |> maps (prep_inst thy align_right (atomize_term thy)) - |> Drule.cterm_instantiate) r |> pair (RuleCases.get r)) - |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th)); - - val ruleq = - (case opt_rule of - SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs)) - | NONE => - (find_inductS ctxt facts @ - map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts)) - |> map_filter (RuleCases.mutual_rule ctxt) - |> tap (trace_rules ctxt InductAttrib.inductN o map #2) - |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); - - fun rule_cases rule = - RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule); - in - (fn i => fn st => - ruleq - |> Seq.maps (RuleCases.consume (flat defs) facts) - |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => - (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => - (CONJUNCTS (ALLGOALS - (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1)) - THEN' fix_tac defs_ctxt - (nth concls (j - 1) + more_consumes) - (nth_list arbitrary (j - 1)))) - THEN' inner_atomize_tac) j)) - THEN' atomize_tac) i st |> Seq.maps (fn st' => - guess_instance (internalize more_consumes rule) i st' - |> Seq.map (rule_instance thy taking) - |> Seq.maps (fn rule' => - CASES (rule_cases rule' cases) - (Tactic.rtac rule' i THEN - PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) - THEN_ALL_NEW_CASES rulify_tac - end; - -end; - - - -(** coinduct method **) - -(* - rule selection scheme: - goal "x:A" coinduct ... - set coinduction - coinduct x - type coinduction - coinduct ... r - explicit rule -*) - -local - -fun find_coinductT ctxt (SOME t :: _) = InductAttrib.find_coinductT ctxt (Term.fastype_of t) - | find_coinductT _ _ = []; - -fun find_coinductS ctxt goal = InductAttrib.find_coinductS ctxt (Logic.strip_assums_concl goal); - -in - -fun coinduct_tac ctxt is_open inst taking opt_rule facts = - let - val _ = warn_open is_open; - val thy = ProofContext.theory_of ctxt; - val cert = Thm.cterm_of thy; - - fun inst_rule r = - if null inst then `RuleCases.get r - else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r - |> pair (RuleCases.get r); - - fun ruleq goal = - (case opt_rule of - SOME r => Seq.single (inst_rule r) - | NONE => - (find_coinductS ctxt goal @ find_coinductT ctxt inst) - |> tap (trace_rules ctxt InductAttrib.coinductN) - |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); - in - SUBGOAL_CASES (fn (goal, i) => fn st => - ruleq goal - |> Seq.maps (RuleCases.consume [] facts) - |> Seq.maps (fn ((cases, (_, more_facts)), rule) => - guess_instance rule i st - |> Seq.map (rule_instance thy taking) - |> Seq.maps (fn rule' => - CASES (make_cases is_open rule' cases) - (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) - end; - -end; - - - -(** concrete syntax **) - -val openN = "open"; -val arbitraryN = "arbitrary"; -val takingN = "taking"; -val ruleN = "rule"; - -local - -fun single_rule [rule] = rule - | single_rule _ = error "Single rule expected"; - -fun named_rule k arg get = - Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|-- - (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name => - (case get (Context.proof_of context) name of SOME x => x - | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))); - -fun rule get_type get_set = - named_rule InductAttrib.typeN Args.tyname get_type || - named_rule InductAttrib.setN Args.const get_set || - Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms; - -val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS >> single_rule; -val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS; -val coinduct_rule = - rule InductAttrib.lookup_coinductT InductAttrib.lookup_coinductS >> single_rule; - -val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; - -val def_inst = - ((Scan.lift (Args.name --| (Args.$$$ "\\" || Args.$$$ "==")) >> SOME) - -- Args.term) >> SOME || - inst >> Option.map (pair NONE); - -val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) => - error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t)); - -fun unless_more_args scan = Scan.unless (Scan.lift - ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN || - Args.$$$ InductAttrib.setN || Args.$$$ ruleN) -- Args.colon)) scan; - -val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |-- - Args.and_list1 (Scan.repeat (unless_more_args free))) []; - -val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |-- - Scan.repeat1 (unless_more_args inst)) []; - -in - -fun cases_meth src = - Method.syntax (Args.mode openN -- - (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src - #> (fn ((is_open, (insts, opt_rule)), ctxt) => - Method.METHOD_CASES (fn facts => - Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts)))); - -fun induct_meth src = - Method.syntax (Args.mode openN -- - (Args.and_list (Scan.repeat (unless_more_args def_inst)) -- - (arbitrary -- taking -- Scan.option induct_rule))) src - #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) => - Method.RAW_METHOD_CASES (fn facts => - Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts)))); - -fun coinduct_meth src = - Method.syntax (Args.mode openN -- - (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src - #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) => - Method.RAW_METHOD_CASES (fn facts => - Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts)))); - -end; - - - -(** theory setup **) - -val setup = - Method.add_methods - [(InductAttrib.casesN, cases_meth, "case analysis on types or sets"), - (InductAttrib.inductN, induct_meth, "induction on types or sets"), - (InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")]; - -end; diff -r e1214fa781ca -r a7b3ab44d993 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Oct 04 14:42:11 2007 +0200 +++ b/src/Pure/IsaMakefile Thu Oct 04 14:42:47 2007 +0200 @@ -35,7 +35,7 @@ Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \ Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML \ Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \ - Isar/find_theorems.ML Isar/induct_attrib.ML Isar/instance.ML Isar/isar_cmd.ML \ + Isar/find_theorems.ML Isar/instance.ML Isar/isar_cmd.ML \ Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \ Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \ Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \ diff -r e1214fa781ca -r a7b3ab44d993 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/Pure/Isar/ROOT.ML Thu Oct 04 14:42:47 2007 +0200 @@ -41,7 +41,6 @@ use "proof.ML"; use "element.ML"; use "net_rules.ML"; -use "induct_attrib.ML"; (*derived theory and proof elements*) use "calculation.ML"; diff -r e1214fa781ca -r a7b3ab44d993 src/Pure/Isar/induct_attrib.ML --- a/src/Pure/Isar/induct_attrib.ML Thu Oct 04 14:42:11 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,224 +0,0 @@ -(* Title: Pure/Isar/induct_attrib.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -Declaration of rules for cases and induction. -*) - -signature INDUCT_ATTRIB = -sig - val vars_of: term -> term list - val dest_rules: Proof.context -> - {type_cases: (string * thm) list, set_cases: (string * thm) list, - type_induct: (string * thm) list, set_induct: (string * thm) list, - type_coinduct: (string * thm) list, set_coinduct: (string * thm) list} - val print_rules: Proof.context -> unit - val lookup_casesT : Proof.context -> string -> thm option - val lookup_casesS : Proof.context -> string -> thm option - val lookup_inductT : Proof.context -> string -> thm option - val lookup_inductS : Proof.context -> string -> thm option - val lookup_coinductT : Proof.context -> string -> thm option - val lookup_coinductS : Proof.context -> string -> thm option - val find_casesT: Proof.context -> typ -> thm list - val find_casesS: Proof.context -> term -> thm list - val find_inductT: Proof.context -> typ -> thm list - val find_inductS: Proof.context -> term -> thm list - val find_coinductT: Proof.context -> typ -> thm list - val find_coinductS: Proof.context -> term -> thm list - val cases_type: string -> attribute - val cases_set: string -> attribute - val induct_type: string -> attribute - val induct_set: string -> attribute - val coinduct_type: string -> attribute - val coinduct_set: string -> attribute - val casesN: string - val inductN: string - val coinductN: string - val typeN: string - val setN: string -end; - -structure InductAttrib: INDUCT_ATTRIB = -struct - - -(** misc utils **) - -(* encode_type -- for indexing purposes *) - -fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) - | encode_type (TFree (a, _)) = Free (a, dummyT) - | encode_type (TVar (a, _)) = Var (a, dummyT); - - -(* variables -- ordered left-to-right, preferring right *) - -fun vars_of tm = - rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [])); - -local - -val mk_var = encode_type o #2 o Term.dest_Var; - -fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty => - raise THM ("No variables in conclusion of rule", 0, [thm]); - -in - -fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty => - raise THM ("No variables in major premise of rule", 0, [thm]); - -val left_var_concl = concl_var hd; -val right_var_concl = concl_var List.last; - -end; - - - -(** induct data **) - -(* rules *) - -type rules = (string * thm) NetRules.T; - -val init_rules = - NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso - Thm.eq_thm_prop (th1, th2)); - -fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs); - -fun pretty_rules ctxt kind rs = - let val thms = map snd (NetRules.rules rs) - in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end; - - -(* context data *) - -structure Induct = GenericDataFun -( - type T = (rules * rules) * (rules * rules) * (rules * rules); - val empty = - ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)), - (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)), - (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2))); - val extend = I; - fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)), - ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) = - ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)), - (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)), - (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2))); -); - -val get_local = Induct.get o Context.Proof; - -fun dest_rules ctxt = - let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in - {type_cases = NetRules.rules casesT, - set_cases = NetRules.rules casesS, - type_induct = NetRules.rules inductT, - set_induct = NetRules.rules inductS, - type_coinduct = NetRules.rules coinductT, - set_coinduct = NetRules.rules coinductS} - end; - -fun print_rules ctxt = - let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in - [pretty_rules ctxt "coinduct type:" coinductT, - pretty_rules ctxt "coinduct set:" coinductS, - pretty_rules ctxt "induct type:" inductT, - pretty_rules ctxt "induct set:" inductS, - pretty_rules ctxt "cases type:" casesT, - pretty_rules ctxt "cases set:" casesS] - |> Pretty.chunks |> Pretty.writeln - end; - - -(* access rules *) - -val lookup_casesT = lookup_rule o #1 o #1 o get_local; -val lookup_casesS = lookup_rule o #2 o #1 o get_local; -val lookup_inductT = lookup_rule o #1 o #2 o get_local; -val lookup_inductS = lookup_rule o #2 o #2 o get_local; -val lookup_coinductT = lookup_rule o #1 o #3 o get_local; -val lookup_coinductS = lookup_rule o #2 o #3 o get_local; - - -fun find_rules which how ctxt x = - map snd (NetRules.retrieve (which (get_local ctxt)) (how x)); - -val find_casesT = find_rules (#1 o #1) encode_type; -val find_casesS = find_rules (#2 o #1) I; -val find_inductT = find_rules (#1 o #2) encode_type; -val find_inductS = find_rules (#2 o #2) I; -val find_coinductT = find_rules (#1 o #3) encode_type; -val find_coinductS = find_rules (#2 o #3) I; - - - -(** attributes **) - -local - -fun mk_att f g name arg = - let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end; - -fun map1 f (x, y, z) = (f x, y, z); -fun map2 f (x, y, z) = (x, f y, z); -fun map3 f (x, y, z) = (x, y, f z); - -fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x; -fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x; -fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x; -fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x; -fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x; -fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x; - -fun consumes0 x = RuleCases.consumes_default 0 x; -fun consumes1 x = RuleCases.consumes_default 1 x; - -in - -val cases_type = mk_att add_casesT consumes0; -val cases_set = mk_att add_casesS consumes1; -val induct_type = mk_att add_inductT consumes0; -val induct_set = mk_att add_inductS consumes1; -val coinduct_type = mk_att add_coinductT consumes0; -val coinduct_set = mk_att add_coinductS consumes1; - -end; - - - -(** concrete syntax **) - -val casesN = "cases"; -val inductN = "induct"; -val coinductN = "coinduct"; - -val typeN = "type"; -val setN = "set"; - -local - -fun spec k arg = - Scan.lift (Args.$$$ k -- Args.colon) |-- arg || - Scan.lift (Args.$$$ k) >> K ""; - -fun attrib add_type add_set = - Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set); - -in - -val cases_att = attrib cases_type cases_set; -val induct_att = attrib induct_type induct_set; -val coinduct_att = attrib coinduct_type coinduct_set; - -end; - -val _ = Context.add_setup - (Attrib.add_attributes - [(casesN, cases_att, "declaration of cases rule for type or set"), - (inductN, induct_att, "declaration of induction rule for type or set"), - (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]); - -end; diff -r e1214fa781ca -r a7b3ab44d993 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Thu Oct 04 14:42:47 2007 +0200 @@ -85,7 +85,6 @@ val print_attributes: Toplevel.transition -> Toplevel.transition val print_simpset: Toplevel.transition -> Toplevel.transition val print_rules: Toplevel.transition -> Toplevel.transition - val print_induct_rules: Toplevel.transition -> Toplevel.transition val print_trans_rules: Toplevel.transition -> Toplevel.transition val print_methods: Toplevel.transition -> Toplevel.transition val print_antiquotations: Toplevel.transition -> Toplevel.transition @@ -472,9 +471,6 @@ val print_rules = Toplevel.unknown_context o Toplevel.keep (ContextRules.print_rules o Toplevel.context_of); -val print_induct_rules = Toplevel.unknown_context o - Toplevel.keep (InductAttrib.print_rules o Toplevel.context_of); - val print_trans_rules = Toplevel.unknown_context o Toplevel.keep (Calculation.print_rules o Toplevel.context_of); diff -r e1214fa781ca -r a7b3ab44d993 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Oct 04 14:42:47 2007 +0200 @@ -799,10 +799,6 @@ OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules)); -val print_induct_rulesP = - OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" K.diag - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_induct_rules)); - val print_trans_rulesP = OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); @@ -1005,7 +1001,8 @@ simproc_setupP, parse_ast_translationP, parse_translationP, print_translationP, typed_print_translationP, print_ast_translationP, token_translationP, oracleP, contextP, - localeP, classP, instanceP, instantiationP, instance_proofP, code_datatypeP, + localeP, classP, instanceP, instantiationP, instance_proofP, + code_datatypeP, (*proof commands*) theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP, assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP, @@ -1020,12 +1017,11 @@ print_configsP, print_contextP, print_theoryP, print_syntaxP, print_abbrevsP, print_factsP, print_theoremsP, print_localesP, print_localeP, print_registrationsP, print_attributesP, - print_simpsetP, print_rulesP, print_induct_rulesP, - print_trans_rulesP, print_methodsP, print_antiquotationsP, - thy_depsP, class_depsP, thm_depsP, find_theoremsP, print_bindsP, - print_casesP, print_stmtsP, print_thmsP, print_prfsP, - print_full_prfsP, print_propP, print_termP, print_typeP, - print_codesetupP, + print_simpsetP, print_rulesP, print_trans_rulesP, print_methodsP, + print_antiquotationsP, thy_depsP, class_depsP, thm_depsP, + find_theoremsP, print_bindsP, print_casesP, print_stmtsP, + print_thmsP, print_prfsP, print_full_prfsP, print_propP, + print_termP, print_typeP, print_codesetupP, (*system commands*) cdP, pwdP, use_thyP, touch_thyP, touch_child_thysP, remove_thyP, kill_thyP, display_draftsP, print_draftsP, prP, disable_prP, diff -r e1214fa781ca -r a7b3ab44d993 src/Tools/induct.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/induct.ML Thu Oct 04 14:42:47 2007 +0200 @@ -0,0 +1,762 @@ +(* Title: Tools/induct.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + +Proof by cases and induction. +*) + +signature INDUCT_DATA = +sig + val cases_default: thm + val atomize: thm list + val rulify: thm list + val rulify_fallback: thm list +end; + +signature INDUCT = +sig + (*rule declarations*) + val vars_of: term -> term list + val dest_rules: Proof.context -> + {type_cases: (string * thm) list, set_cases: (string * thm) list, + type_induct: (string * thm) list, set_induct: (string * thm) list, + type_coinduct: (string * thm) list, set_coinduct: (string * thm) list} + val print_rules: Proof.context -> unit + val lookup_casesT: Proof.context -> string -> thm option + val lookup_casesS: Proof.context -> string -> thm option + val lookup_inductT: Proof.context -> string -> thm option + val lookup_inductS: Proof.context -> string -> thm option + val lookup_coinductT: Proof.context -> string -> thm option + val lookup_coinductS: Proof.context -> string -> thm option + val find_casesT: Proof.context -> typ -> thm list + val find_casesS: Proof.context -> term -> thm list + val find_inductT: Proof.context -> typ -> thm list + val find_inductS: Proof.context -> term -> thm list + val find_coinductT: Proof.context -> typ -> thm list + val find_coinductS: Proof.context -> term -> thm list + val cases_type: string -> attribute + val cases_set: string -> attribute + val induct_type: string -> attribute + val induct_set: string -> attribute + val coinduct_type: string -> attribute + val coinduct_set: string -> attribute + val casesN: string + val inductN: string + val coinductN: string + val typeN: string + val setN: string + (*proof methods*) + val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic + val add_defs: (string option * term) option list -> Proof.context -> + (term option list * thm list) * Proof.context + val atomize_term: theory -> term -> term + val atomize_tac: int -> tactic + val inner_atomize_tac: int -> tactic + val rulified_term: thm -> theory * term + val rulify_tac: int -> tactic + val internalize: int -> thm -> thm + val guess_instance: thm -> int -> thm -> thm Seq.seq + val cases_tac: Proof.context -> bool -> term option list list -> thm option -> + thm list -> int -> cases_tactic + val induct_tac: Proof.context -> bool -> (string option * term) option list list -> + (string * typ) list list -> term option list -> thm list option -> thm list -> int -> + cases_tactic + val coinduct_tac: Proof.context -> bool -> term option list -> term option list -> + thm option -> thm list -> int -> cases_tactic + val setup: theory -> theory +end; + +functor InductFun(Data: INDUCT_DATA): INDUCT = +struct + + +(** misc utils **) + +(* encode_type -- for indexing purposes *) + +fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) + | encode_type (TFree (a, _)) = Free (a, dummyT) + | encode_type (TVar (a, _)) = Var (a, dummyT); + + +(* variables -- ordered left-to-right, preferring right *) + +fun vars_of tm = + rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [])); + +local + +val mk_var = encode_type o #2 o Term.dest_Var; + +fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty => + raise THM ("No variables in conclusion of rule", 0, [thm]); + +in + +fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty => + raise THM ("No variables in major premise of rule", 0, [thm]); + +val left_var_concl = concl_var hd; +val right_var_concl = concl_var List.last; + +end; + + + +(** induct data **) + +(* rules *) + +type rules = (string * thm) NetRules.T; + +val init_rules = + NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso + Thm.eq_thm_prop (th1, th2)); + +fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs); + +fun pretty_rules ctxt kind rs = + let val thms = map snd (NetRules.rules rs) + in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end; + + +(* context data *) + +structure Induct = GenericDataFun +( + type T = (rules * rules) * (rules * rules) * (rules * rules); + val empty = + ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)), + (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)), + (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2))); + val extend = I; + fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)), + ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) = + ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)), + (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)), + (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2))); +); + +val get_local = Induct.get o Context.Proof; + +fun dest_rules ctxt = + let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in + {type_cases = NetRules.rules casesT, + set_cases = NetRules.rules casesS, + type_induct = NetRules.rules inductT, + set_induct = NetRules.rules inductS, + type_coinduct = NetRules.rules coinductT, + set_coinduct = NetRules.rules coinductS} + end; + +fun print_rules ctxt = + let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in + [pretty_rules ctxt "coinduct type:" coinductT, + pretty_rules ctxt "coinduct set:" coinductS, + pretty_rules ctxt "induct type:" inductT, + pretty_rules ctxt "induct set:" inductS, + pretty_rules ctxt "cases type:" casesT, + pretty_rules ctxt "cases set:" casesS] + |> Pretty.chunks |> Pretty.writeln + end; + +val _ = OuterSyntax.add_parsers [ + OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" + OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o + Toplevel.keep (print_rules o Toplevel.context_of)))]; + + +(* access rules *) + +val lookup_casesT = lookup_rule o #1 o #1 o get_local; +val lookup_casesS = lookup_rule o #2 o #1 o get_local; +val lookup_inductT = lookup_rule o #1 o #2 o get_local; +val lookup_inductS = lookup_rule o #2 o #2 o get_local; +val lookup_coinductT = lookup_rule o #1 o #3 o get_local; +val lookup_coinductS = lookup_rule o #2 o #3 o get_local; + + +fun find_rules which how ctxt x = + map snd (NetRules.retrieve (which (get_local ctxt)) (how x)); + +val find_casesT = find_rules (#1 o #1) encode_type; +val find_casesS = find_rules (#2 o #1) I; +val find_inductT = find_rules (#1 o #2) encode_type; +val find_inductS = find_rules (#2 o #2) I; +val find_coinductT = find_rules (#1 o #3) encode_type; +val find_coinductS = find_rules (#2 o #3) I; + + + +(** attributes **) + +local + +fun mk_att f g name arg = + let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end; + +fun map1 f (x, y, z) = (f x, y, z); +fun map2 f (x, y, z) = (x, f y, z); +fun map3 f (x, y, z) = (x, y, f z); + +fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x; +fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x; +fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x; +fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x; +fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x; +fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x; + +fun consumes0 x = RuleCases.consumes_default 0 x; +fun consumes1 x = RuleCases.consumes_default 1 x; + +in + +val cases_type = mk_att add_casesT consumes0; +val cases_set = mk_att add_casesS consumes1; +val induct_type = mk_att add_inductT consumes0; +val induct_set = mk_att add_inductS consumes1; +val coinduct_type = mk_att add_coinductT consumes0; +val coinduct_set = mk_att add_coinductS consumes1; + +end; + + + +(** attribute syntax **) + +val casesN = "cases"; +val inductN = "induct"; +val coinductN = "coinduct"; + +val typeN = "type"; +val setN = "set"; + +local + +fun spec k arg = + Scan.lift (Args.$$$ k -- Args.colon) |-- arg || + Scan.lift (Args.$$$ k) >> K ""; + +fun attrib add_type add_set = + Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set); + +val cases_att = attrib cases_type cases_set; +val induct_att = attrib induct_type induct_set; +val coinduct_att = attrib coinduct_type coinduct_set; + +in + +val attrib_setup = Attrib.add_attributes + [(casesN, cases_att, "declaration of cases rule for type or set"), + (inductN, induct_att, "declaration of induction rule for type or set"), + (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]; + +end; + + + +(** method utils **) + +(* alignment *) + +fun align_left msg xs ys = + let val m = length xs and n = length ys + in if m < n then error msg else (Library.take (n, xs) ~~ ys) end; + +fun align_right msg xs ys = + let val m = length xs and n = length ys + in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end; + + +(* prep_inst *) + +fun prep_inst thy align tune (tm, ts) = + let + val cert = Thm.cterm_of thy; + fun prep_var (x, SOME t) = + let + val cx = cert x; + val {T = xT, thy, ...} = Thm.rep_cterm cx; + val ct = cert (tune t); + in + if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct) + else error (Pretty.string_of (Pretty.block + [Pretty.str "Ill-typed instantiation:", Pretty.fbrk, + Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, + Display.pretty_ctyp (#T (Thm.crep_cterm ct))])) + end + | prep_var (_, NONE) = NONE; + val xs = vars_of tm; + in + align "Rule has fewer variables than instantiations given" xs ts + |> map_filter prep_var + end; + + +(* trace_rules *) + +fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule") + | trace_rules ctxt _ rules = Method.trace ctxt rules; + + +(* make_cases *) + +fun make_cases is_open rule = + RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule); + +fun warn_open true = legacy_feature "open rule cases in proof method" + | warn_open false = (); + + + +(** cases method **) + +(* + rule selection scheme: + cases - default case split + `x:A` cases ... - set cases + cases t - type cases + ... cases ... r - explicit rule +*) + +local + +fun get_casesT ctxt ((SOME t :: _) :: _) = find_casesT ctxt (Term.fastype_of t) + | get_casesT _ _ = []; + +fun get_casesS ctxt (fact :: _) = find_casesS ctxt (Thm.concl_of fact) + | get_casesS _ _ = []; + +in + +fun cases_tac ctxt is_open insts opt_rule facts = + let + val _ = warn_open is_open; + val thy = ProofContext.theory_of ctxt; + val cert = Thm.cterm_of thy; + + fun inst_rule r = + if null insts then `RuleCases.get r + else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts + |> maps (prep_inst thy align_left I) + |> Drule.cterm_instantiate) r |> pair (RuleCases.get r); + + val ruleq = + (case opt_rule of + SOME r => Seq.single (inst_rule r) + | NONE => + (get_casesS ctxt facts @ get_casesT ctxt insts @ [Data.cases_default]) + |> tap (trace_rules ctxt casesN) + |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); + in + fn i => fn st => + ruleq + |> Seq.maps (RuleCases.consume [] facts) + |> Seq.maps (fn ((cases, (_, more_facts)), rule) => + CASES (make_cases is_open rule cases) + (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st) + end; + +end; + + + +(** induct method **) + +val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}]; + + +(* atomize *) + +fun atomize_term thy = + MetaSimplifier.rewrite_term thy Data.atomize [] + #> ObjectLogic.drop_judgment thy; + +val atomize_cterm = MetaSimplifier.rewrite true Data.atomize; + +val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize; + +val inner_atomize_tac = + Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac; + + +(* rulify *) + +fun rulify_term thy = + MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #> + MetaSimplifier.rewrite_term thy Data.rulify_fallback []; + +fun rulified_term thm = + let + val thy = Thm.theory_of_thm thm; + val rulify = rulify_term thy; + val (As, B) = Logic.strip_horn (Thm.prop_of thm); + in (thy, Logic.list_implies (map rulify As, rulify B)) end; + +val rulify_tac = + Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN' + Simplifier.rewrite_goal_tac Data.rulify_fallback THEN' + Goal.conjunction_tac THEN_ALL_NEW + (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac); + + +(* prepare rule *) + +fun rule_instance thy inst rule = + Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule; + +fun internalize k th = + th |> Thm.permute_prems 0 k + |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm); + + +(* guess rule instantiation -- cannot handle pending goal parameters *) + +local + +fun dest_env thy (env as Envir.Envir {iTs, ...}) = + let + val cert = Thm.cterm_of thy; + val certT = Thm.ctyp_of thy; + val pairs = Envir.alist_of env; + val ts = map (cert o Envir.norm_term env o #2 o #2) pairs; + val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts); + in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end; + +in + +fun guess_instance rule i st = + let + val {thy, maxidx, ...} = Thm.rep_thm st; + val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) + val params = rev (rename_wrt_term goal (Logic.strip_params goal)); + in + if not (null params) then + (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ + commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params)); + Seq.single rule) + else + let + val rule' = Thm.incr_indexes (maxidx + 1) rule; + val concl = Logic.strip_assums_concl goal; + in + Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] + (Envir.empty (#maxidx (Thm.rep_thm rule'))) + |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule') + end + end handle Subscript => Seq.empty; + +end; + + +(* special renaming of rule parameters *) + +fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] = + let + val x = ProofContext.revert_skolem ctxt z; + fun index i [] = [] + | index i (y :: ys) = + if x = y then x ^ string_of_int i :: index (i + 1) ys + else y :: index i ys; + fun rename_params [] = [] + | rename_params ((y, Type (U, _)) :: ys) = + (if U = T then x else y) :: rename_params ys + | rename_params ((y, _) :: ys) = y :: rename_params ys; + fun rename_asm A = + let + val xs = rename_params (Logic.strip_params A); + val xs' = + (case List.filter (equal x) xs of + [] => xs | [_] => xs | _ => index 1 xs); + in Logic.list_rename_params (xs', A) end; + fun rename_prop p = + let val (As, C) = Logic.strip_horn p + in Logic.list_implies (map rename_asm As, C) end; + val cp' = cterm_fun rename_prop (Thm.cprop_of thm); + val thm' = Thm.equal_elim (Thm.reflexive cp') thm; + in [RuleCases.save thm thm'] end + | special_rename_params _ _ ths = ths; + + +(* fix_tac *) + +local + +fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B) + | goal_prefix 0 _ = Term.dummy_pattern propT + | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B + | goal_prefix _ _ = Term.dummy_pattern propT; + +fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1 + | goal_params 0 _ = 0 + | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B + | goal_params _ _ = 0; + +fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) => + let + val thy = ProofContext.theory_of ctxt; + val cert = Thm.cterm_of thy; + val certT = Thm.ctyp_of thy; + + val v = Free (x, T); + fun spec_rule prfx (xs, body) = + @{thm Pure.meta_spec} + |> Thm.rename_params_rule ([ProofContext.revert_skolem ctxt x], 1) + |> Thm.lift_rule (cert prfx) + |> `(Thm.prop_of #> Logic.strip_assums_concl) + |-> (fn pred $ arg => + Drule.cterm_instantiate + [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))), + (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]); + + fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B + | goal_concl 0 xs B = + if not (Term.exists_subterm (fn t => t aconv v) B) then NONE + else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B)) + | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B + | goal_concl _ _ _ = NONE; + in + (case goal_concl n [] goal of + SOME concl => + (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i + | NONE => all_tac) + end); + +fun miniscope_tac p = + CONVERSION (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq])); + +in + +fun fix_tac _ _ [] = K all_tac + | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) => + (EVERY' (map (meta_spec_tac ctxt n) xs) THEN' + (miniscope_tac (goal_params n goal))) i); + +end; + + +(* add_defs *) + +fun add_defs def_insts = + let + fun add (SOME (SOME x, t)) ctxt = + let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt + in ((SOME lhs, [th]), ctxt') end + | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt) + | add NONE ctxt = ((NONE, []), ctxt); + in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; + + +(* induct_tac *) + +(* + rule selection scheme: + `x:A` induct ... - set induction + induct x - type induction + ... induct ... r - explicit rule +*) + +local + +fun get_inductT ctxt insts = + fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts) + |> map (find_inductT ctxt o Term.fastype_of)) [[]] + |> filter_out (forall PureThy.is_internal); + +fun get_inductS ctxt (fact :: _) = map single (find_inductS ctxt (Thm.concl_of fact)) + | get_inductS _ _ = []; + +in + +fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts = + let + val _ = warn_open is_open; + val thy = ProofContext.theory_of ctxt; + val cert = Thm.cterm_of thy; + + val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; + val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; + + fun inst_rule (concls, r) = + (if null insts then `RuleCases.get r + else (align_left "Rule has fewer conclusions than arguments given" + (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts + |> maps (prep_inst thy align_right (atomize_term thy)) + |> Drule.cterm_instantiate) r |> pair (RuleCases.get r)) + |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th)); + + val ruleq = + (case opt_rule of + SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs)) + | NONE => + (get_inductS ctxt facts @ + map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts)) + |> map_filter (RuleCases.mutual_rule ctxt) + |> tap (trace_rules ctxt inductN o map #2) + |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); + + fun rule_cases rule = + RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule); + in + (fn i => fn st => + ruleq + |> Seq.maps (RuleCases.consume (flat defs) facts) + |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => + (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => + (CONJUNCTS (ALLGOALS + (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1)) + THEN' fix_tac defs_ctxt + (nth concls (j - 1) + more_consumes) + (nth_list arbitrary (j - 1)))) + THEN' inner_atomize_tac) j)) + THEN' atomize_tac) i st |> Seq.maps (fn st' => + guess_instance (internalize more_consumes rule) i st' + |> Seq.map (rule_instance thy taking) + |> Seq.maps (fn rule' => + CASES (rule_cases rule' cases) + (Tactic.rtac rule' i THEN + PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) + THEN_ALL_NEW_CASES rulify_tac + end; + +end; + + + +(** coinduct method **) + +(* + rule selection scheme: + goal "x:A" coinduct ... - set coinduction + coinduct x - type coinduction + coinduct ... r - explicit rule +*) + +local + +fun get_coinductT ctxt (SOME t :: _) = find_coinductT ctxt (Term.fastype_of t) + | get_coinductT _ _ = []; + +fun get_coinductS ctxt goal = find_coinductS ctxt (Logic.strip_assums_concl goal); + +in + +fun coinduct_tac ctxt is_open inst taking opt_rule facts = + let + val _ = warn_open is_open; + val thy = ProofContext.theory_of ctxt; + val cert = Thm.cterm_of thy; + + fun inst_rule r = + if null inst then `RuleCases.get r + else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r + |> pair (RuleCases.get r); + + fun ruleq goal = + (case opt_rule of + SOME r => Seq.single (inst_rule r) + | NONE => + (get_coinductS ctxt goal @ get_coinductT ctxt inst) + |> tap (trace_rules ctxt coinductN) + |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); + in + SUBGOAL_CASES (fn (goal, i) => fn st => + ruleq goal + |> Seq.maps (RuleCases.consume [] facts) + |> Seq.maps (fn ((cases, (_, more_facts)), rule) => + guess_instance rule i st + |> Seq.map (rule_instance thy taking) + |> Seq.maps (fn rule' => + CASES (make_cases is_open rule' cases) + (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) + end; + +end; + + + +(** concrete syntax **) + +val openN = "open"; +val arbitraryN = "arbitrary"; +val takingN = "taking"; +val ruleN = "rule"; + +local + +fun single_rule [rule] = rule + | single_rule _ = error "Single rule expected"; + +fun named_rule k arg get = + Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|-- + (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name => + (case get (Context.proof_of context) name of SOME x => x + | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))); + +fun rule get_type get_set = + named_rule typeN Args.tyname get_type || + named_rule setN Args.const get_set || + Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms; + +val cases_rule = rule lookup_casesT lookup_casesS >> single_rule; +val induct_rule = rule lookup_inductT lookup_inductS; +val coinduct_rule = rule lookup_coinductT lookup_coinductS >> single_rule; + +val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; + +val def_inst = + ((Scan.lift (Args.name --| (Args.$$$ "\\" || Args.$$$ "==")) >> SOME) + -- Args.term) >> SOME || + inst >> Option.map (pair NONE); + +val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) => + error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t)); + +fun unless_more_args scan = Scan.unless (Scan.lift + ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN || + Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan; + +val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |-- + Args.and_list1 (Scan.repeat (unless_more_args free))) []; + +val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |-- + Scan.repeat1 (unless_more_args inst)) []; + +in + +fun cases_meth src = + Method.syntax (Args.mode openN -- + (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src + #> (fn ((is_open, (insts, opt_rule)), ctxt) => + Method.METHOD_CASES (fn facts => + Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts)))); + +fun induct_meth src = + Method.syntax (Args.mode openN -- + (Args.and_list (Scan.repeat (unless_more_args def_inst)) -- + (arbitrary -- taking -- Scan.option induct_rule))) src + #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) => + Method.RAW_METHOD_CASES (fn facts => + Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts)))); + +fun coinduct_meth src = + Method.syntax (Args.mode openN -- + (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src + #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) => + Method.RAW_METHOD_CASES (fn facts => + Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts)))); + +end; + + + +(** theory setup **) + +val setup = + attrib_setup #> + Method.add_methods + [(casesN, cases_meth, "case analysis on types or sets"), + (inductN, induct_meth, "induction on types or sets"), + (coinductN, coinduct_meth, "coinduction on types or sets")]; + +end; diff -r e1214fa781ca -r a7b3ab44d993 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu Oct 04 14:42:11 2007 +0200 +++ b/src/ZF/Tools/inductive_package.ML Thu Oct 04 14:42:47 2007 +0200 @@ -506,7 +506,7 @@ val ([induct', mutual_induct'], thy') = thy |> PureThy.add_thms [((co_prefix ^ "induct", induct), - [case_names, InductAttrib.induct_set big_rec_name]), + [case_names, Induct.induct_set big_rec_name]), (("mutual_induct", mutual_induct), [case_names])]; in ((thy', induct'), mutual_induct') end; (*of induction_rules*) @@ -528,7 +528,7 @@ |> PureThy.add_thms [(("bnd_mono", bnd_mono), []), (("dom_subset", dom_subset), []), - (("cases", elim), [case_names, InductAttrib.cases_set big_rec_name])] + (("cases", elim), [case_names, Induct.cases_set big_rec_name])] ||>> (PureThy.add_thmss o map Thm.no_attributes) [("defs", defs), ("intros", intrs)];