# HG changeset patch # User wenzelm # Date 1191614415 -7200 # Node ID cc669ca5f38253556fbaec5502a898d18cf0a03d # Parent ceb634874e0ca44ed86fa5c4702f47b0b9a9f178 tuned Induct interface: prefer pred'' over set''; diff -r ceb634874e0c -r cc669ca5f382 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Oct 05 22:00:13 2007 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Oct 05 22:00:15 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 - (Induct.lookup_inductS ctxt (hd names))))); + (Induct.lookup_inductP 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 ceb634874e0c -r cc669ca5f382 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Fri Oct 05 22:00:13 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Fri Oct 05 22:00:15 2007 +0200 @@ -73,7 +73,7 @@ |> addsmps "psimps" [] psimps ||> fold_option (snd oo addsmps "simps" []) trsimps ||>> note_theorem ((qualify "pinduct", - [Attrib.internal (K (Induct.induct_set ""))]), simple_pinducts) + [Attrib.internal (K (Induct.induct_pred ""))]), 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 ceb634874e0c -r cc669ca5f382 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Fri Oct 05 22:00:13 2007 +0200 +++ b/src/HOL/Tools/inductive_package.ML Fri Oct 05 22:00:15 2007 +0200 @@ -433,7 +433,7 @@ error (Pretty.string_of (Pretty.block [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop])); - val elims = Induct.find_casesS ctxt prop; + val elims = Induct.find_casesP 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, Induct.coinduct_set (hd cnames)]) + RuleCases.consumes 1, Induct.coinduct_pred (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 (Induct.cases_set name)), + Attrib.internal (K (Induct.cases_pred 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 (Induct.induct_set name))])))] |> snd + Attrib.internal (K (Induct.induct_pred name))])))] |> snd end in (intrs', elims', induct', ctxt3) end; diff -r ceb634874e0c -r cc669ca5f382 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Fri Oct 05 22:00:13 2007 +0200 +++ b/src/HOL/Tools/typedef_package.ML Fri Oct 05 22:00:15 2007 +0200 @@ -176,11 +176,11 @@ ((Rep_name ^ "_inject", make Rep_inject), []), ((Abs_name ^ "_inject", abs_inject), []), ((Rep_name ^ "_cases", make Rep_cases), - [RuleCases.case_names [Rep_name], Induct.cases_set full_name]), + [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]), ((Abs_name ^ "_cases", make Abs_cases), [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]), ((Rep_name ^ "_induct", make Rep_induct), - [RuleCases.case_names [Rep_name], Induct.induct_set full_name]), + [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]), ((Abs_name ^ "_induct", make Abs_induct), [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])]) ||> Sign.parent_path; diff -r ceb634874e0c -r cc669ca5f382 src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Oct 05 22:00:13 2007 +0200 +++ b/src/Tools/induct.ML Fri Oct 05 22:00:15 2007 +0200 @@ -18,32 +18,33 @@ (*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} + {type_cases: (string * thm) list, pred_cases: (string * thm) list, + type_induct: (string * thm) list, pred_induct: (string * thm) list, + type_coinduct: (string * thm) list, pred_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_casesP: Proof.context -> string -> thm option val lookup_inductT: Proof.context -> string -> thm option - val lookup_inductS: Proof.context -> string -> thm option + val lookup_inductP: Proof.context -> string -> thm option val lookup_coinductT: Proof.context -> string -> thm option - val lookup_coinductS: Proof.context -> string -> thm option + val lookup_coinductP: Proof.context -> string -> thm option val find_casesT: Proof.context -> typ -> thm list - val find_casesS: Proof.context -> term -> thm list + val find_casesP: Proof.context -> term -> thm list val find_inductT: Proof.context -> typ -> thm list - val find_inductS: Proof.context -> term -> thm list + val find_inductP: Proof.context -> term -> thm list val find_coinductT: Proof.context -> typ -> thm list - val find_coinductS: Proof.context -> term -> thm list + val find_coinductP: Proof.context -> term -> thm list val cases_type: string -> attribute - val cases_set: string -> attribute + val cases_pred: string -> attribute val induct_type: string -> attribute - val induct_set: string -> attribute + val induct_pred: string -> attribute val coinduct_type: string -> attribute - val coinduct_set: string -> attribute + val coinduct_pred: string -> attribute val casesN: string val inductN: string val coinductN: string val typeN: string + val predN: string val setN: string (*proof methods*) val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic @@ -130,33 +131,33 @@ (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))); + fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)), + ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) = + ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesP1, casesP2)), + (NetRules.merge (inductT1, inductT2), NetRules.merge (inductP1, inductP2)), + (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductP1, coinductP2))); ); val get_local = Induct.get o Context.Proof; fun dest_rules ctxt = - let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in + let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in {type_cases = NetRules.rules casesT, - set_cases = NetRules.rules casesS, + pred_cases = NetRules.rules casesP, type_induct = NetRules.rules inductT, - set_induct = NetRules.rules inductS, + pred_induct = NetRules.rules inductP, type_coinduct = NetRules.rules coinductT, - set_coinduct = NetRules.rules coinductS} + pred_coinduct = NetRules.rules coinductP} end; fun print_rules ctxt = - let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in + let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in [pretty_rules ctxt "coinduct type:" coinductT, - pretty_rules ctxt "coinduct set:" coinductS, + pretty_rules ctxt "coinduct pred:" coinductP, pretty_rules ctxt "induct type:" inductT, - pretty_rules ctxt "induct set:" inductS, + pretty_rules ctxt "induct pred:" inductP, pretty_rules ctxt "cases type:" casesT, - pretty_rules ctxt "cases set:" casesS] + pretty_rules ctxt "cases pred:" casesP] |> Pretty.chunks |> Pretty.writeln end; @@ -169,22 +170,22 @@ (* 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_casesP = 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_inductP = 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; +val lookup_coinductP = 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_casesP = 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_inductP = 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; +val find_coinductP = find_rules (#2 o #3) I; @@ -200,11 +201,11 @@ 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_casesP 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_inductP 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 add_coinductP rule x = map3 (apsnd (NetRules.insert rule)) x; fun consumes0 x = RuleCases.consumes_default 0 x; fun consumes1 x = RuleCases.consumes_default 1 x; @@ -212,11 +213,11 @@ in val cases_type = mk_att add_casesT consumes0; -val cases_set = mk_att add_casesS consumes1; +val cases_pred = mk_att add_casesP consumes1; val induct_type = mk_att add_inductT consumes0; -val induct_set = mk_att add_inductS consumes1; +val induct_pred = mk_att add_inductP consumes1; val coinduct_type = mk_att add_coinductT consumes0; -val coinduct_set = mk_att add_coinductS consumes1; +val coinduct_pred = mk_att add_coinductP consumes1; end; @@ -229,6 +230,7 @@ val coinductN = "coinduct"; val typeN = "type"; +val predN = "pred"; val setN = "set"; local @@ -237,19 +239,21 @@ 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); +fun attrib add_type add_pred = Attrib.syntax + (spec typeN Args.tyname >> add_type || + spec predN Args.const >> add_pred || + spec setN Args.const >> add_pred); -val cases_att = attrib cases_type cases_set; -val induct_att = attrib induct_type induct_set; -val coinduct_att = attrib coinduct_type coinduct_set; +val cases_att = attrib cases_type cases_pred; +val induct_att = attrib induct_type induct_pred; +val coinduct_att = attrib coinduct_type coinduct_pred; 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")]; + [(casesN, cases_att, "declaration of cases rule for type or predicate/set"), + (inductN, induct_att, "declaration of induction rule for type or predicate/set"), + (coinductN, coinduct_att, "declaration of coinduction rule for type or predicate/set")]; end; @@ -314,7 +318,7 @@ (* rule selection scheme: cases - default case split - `x:A` cases ... - set cases + `A t` cases ... - predicate/set cases cases t - type cases ... cases ... r - explicit rule *) @@ -324,8 +328,8 @@ 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 _ _ = []; +fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact) + | get_casesP _ _ = []; in @@ -345,7 +349,7 @@ (case opt_rule of SOME r => Seq.single (inst_rule r) | NONE => - (get_casesS ctxt facts @ get_casesT ctxt insts @ [Data.cases_default]) + (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default]) |> tap (trace_rules ctxt casesN) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); in @@ -551,7 +555,7 @@ (* rule selection scheme: - `x:A` induct ... - set induction + `A x` induct ... - predicate/set induction induct x - type induction ... induct ... r - explicit rule *) @@ -563,8 +567,8 @@ |> 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 _ _ = []; +fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact)) + | get_inductP _ _ = []; in @@ -589,7 +593,7 @@ (case opt_rule of SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs)) | NONE => - (get_inductS ctxt facts @ + (get_inductP 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) @@ -627,7 +631,7 @@ (* rule selection scheme: - goal "x:A" coinduct ... - set coinduction + goal "A x" coinduct ... - predicate/set coinduction coinduct x - type coinduction coinduct ... r - explicit rule *) @@ -637,7 +641,10 @@ 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); +fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal); + +fun main_prop_of th = + if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th; in @@ -649,14 +656,14 @@ 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 + else Drule.cterm_instantiate (prep_inst thy align_right I (main_prop_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) + (get_coinductP ctxt goal @ get_coinductT ctxt inst) |> tap (trace_rules ctxt coinductN) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); in @@ -693,14 +700,15 @@ (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 = +fun rule get_type get_pred = named_rule typeN Args.tyname get_type || - named_rule setN Args.const get_set || + named_rule predN Args.const get_pred || + named_rule setN Args.const get_pred || 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 cases_rule = rule lookup_casesT lookup_casesP >> single_rule; +val induct_rule = rule lookup_inductT lookup_inductP; +val coinduct_rule = rule lookup_coinductT lookup_coinductP >> single_rule; val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; @@ -714,7 +722,7 @@ fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN || - Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan; + Args.$$$ predN || 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))) []; @@ -755,8 +763,8 @@ 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")]; + [(casesN, cases_meth, "case analysis on types or predicates/sets"), + (inductN, induct_meth, "induction on types or predicates/sets"), + (coinductN, coinduct_meth, "coinduction on types or predicates/sets")]; end; diff -r ceb634874e0c -r cc669ca5f382 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Oct 05 22:00:13 2007 +0200 +++ b/src/ZF/Tools/inductive_package.ML Fri Oct 05 22:00:15 2007 +0200 @@ -506,7 +506,7 @@ val ([induct', mutual_induct'], thy') = thy |> PureThy.add_thms [((co_prefix ^ "induct", induct), - [case_names, Induct.induct_set big_rec_name]), + [case_names, Induct.induct_pred 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, Induct.cases_set big_rec_name])] + (("cases", elim), [case_names, Induct.cases_pred big_rec_name])] ||>> (PureThy.add_thmss o map Thm.no_attributes) [("defs", defs), ("intros", intrs)];