# HG changeset patch # User berghofe # Date 1184146799 -7200 # Node ID 24eef53a9ad31c07a82646cc9726929ae3f97b16 # Parent 9cebbaccf8a2d25f840e77e6830707663e645c71 Reorganization due to introduction of inductive_set wrapper. diff -r 9cebbaccf8a2 -r 24eef53a9ad3 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Wed Jul 11 11:38:25 2007 +0200 +++ b/src/HOL/Tools/inductive_package.ML Wed Jul 11 11:39:59 2007 +0200 @@ -19,7 +19,7 @@ Pj, Pk are two of the predicates being defined in mutual recursion *) -signature INDUCTIVE_PACKAGE = +signature BASIC_INDUCTIVE_PACKAGE = sig val quiet_mode: bool ref type inductive_result @@ -57,6 +57,29 @@ val setup: theory -> theory end; +signature INDUCTIVE_PACKAGE = +sig + include BASIC_INDUCTIVE_PACKAGE + type add_ind_def + val declare_rules: bstring -> bool -> bool -> string list -> + thm list -> bstring list -> Attrib.src list list -> (thm * string list) list -> + thm -> local_theory -> thm list * thm list * thm * local_theory + val add_ind_def: add_ind_def + val gen_add_inductive_i: add_ind_def -> + bool -> bstring -> bool -> bool -> bool -> + (string * typ option * mixfix) list -> + (string * typ option) list -> ((bstring * Attrib.src list) * term) list -> thm list -> + local_theory -> inductive_result * local_theory + val gen_add_inductive: add_ind_def -> + bool -> bool -> (string * string option * mixfix) list -> + (string * string option * mixfix) list -> + ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list -> + local_theory -> inductive_result * local_theory + val gen_ind_decl: add_ind_def -> + bool -> OuterParse.token list -> + (Toplevel.transition -> Toplevel.transition) * OuterParse.token list +end; + structure InductivePackage: INDUCTIVE_PACKAGE = struct @@ -89,17 +112,17 @@ (** context data **) type inductive_result = - {preds: term list, defs: thm list, elims: thm list, raw_induct: thm, - induct: thm, intrs: thm list, mono: thm, unfold: thm}; + {preds: term list, elims: thm list, raw_induct: thm, + induct: thm, intrs: thm list}; -fun morph_result phi {preds, defs, elims, raw_induct: thm, induct, intrs, mono, unfold} = +fun morph_result phi {preds, elims, raw_induct: thm, induct, intrs} = let val term = Morphism.term phi; val thm = Morphism.thm phi; val fact = Morphism.fact phi; in - {preds = map term preds, defs = fact defs, elims = fact elims, raw_induct = thm raw_induct, - induct = thm induct, intrs = fact intrs, mono = thm mono, unfold = thm unfold} + {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct, + induct = thm induct, intrs = fact intrs} end; type inductive_info = @@ -162,7 +185,7 @@ [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL (resolve_tac [le_funI, le_boolI'])) thm))] | _ => [thm] - end; + end handle THM _ => error ("Bad monotonicity theorem:\n" ^ string_of_thm thm); val mono_add = Thm.declaration_attribute (map_monos o fold Drule.add_rule o mk_mono); val mono_del = Thm.declaration_attribute (map_monos o fold Drule.del_rule o mk_mono); @@ -227,13 +250,13 @@ local -fun err_in_rule thy name t msg = +fun err_in_rule ctxt name t msg = error (cat_lines ["Ill-formed introduction rule " ^ quote name, - Sign.string_of_term thy t, msg]); + ProofContext.string_of_term ctxt t, msg]); -fun err_in_prem thy name t p msg = - error (cat_lines ["Ill-formed premise", Sign.string_of_term thy p, - "in introduction rule " ^ quote name, Sign.string_of_term thy t, msg]); +fun err_in_prem ctxt name t p msg = + error (cat_lines ["Ill-formed premise", ProofContext.string_of_term ctxt p, + "in introduction rule " ^ quote name, ProofContext.string_of_term ctxt t, msg]); val bad_concl = "Conclusion of introduction rule must be an inductive predicate"; @@ -245,25 +268,26 @@ in -fun check_rule thy cs params ((name, att), rule) = +fun check_rule ctxt cs params ((name, att), rule) = let val params' = Term.variant_frees rule (Logic.strip_params rule); val frees = rev (map Free params'); val concl = subst_bounds (frees, Logic.strip_assums_concl rule); val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule); - val aprems = map (atomize_term thy) prems; + val rule' = Logic.list_implies (prems, concl); + val aprems = map (atomize_term (ProofContext.theory_of ctxt)) prems; val arule = list_all_free (params', Logic.list_implies (aprems, concl)); fun check_ind err t = case dest_predicate cs params t of NONE => err (bad_app ^ - commas (map (Sign.string_of_term thy) params)) + commas (map (ProofContext.string_of_term ctxt) params)) | SOME (_, _, ys, _) => if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs then err bad_ind_occ else (); fun check_prem' prem t = if head_of t mem cs then - check_ind (err_in_prem thy name rule prem) t + check_ind (err_in_prem ctxt name rule prem) t else (case t of Abs (_, _, t) => check_prem' prem t | t $ u => (check_prem' prem t; check_prem' prem u) @@ -271,15 +295,15 @@ fun check_prem (prem, aprem) = if can HOLogic.dest_Trueprop aprem then check_prem' prem prem - else err_in_prem thy name rule prem "Non-atomic premise"; + else err_in_prem ctxt name rule prem "Non-atomic premise"; in (case concl of Const ("Trueprop", _) $ t => if head_of t mem cs then - (check_ind (err_in_rule thy name rule) t; + (check_ind (err_in_rule ctxt name rule') t; List.app check_prem (prems ~~ aprems)) - else err_in_rule thy name rule bad_concl - | _ => err_in_rule thy name rule bad_concl); + else err_in_rule ctxt name rule' bad_concl + | _ => err_in_rule ctxt name rule' bad_concl); ((name, att), arule) end; @@ -400,9 +424,8 @@ val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; -fun simp_case_tac solved ss i = - EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i - THEN_MAYBE (if solved then no_tac else all_tac); (* FIXME !? *) +fun simp_case_tac ss i = + EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i; in @@ -415,13 +438,10 @@ error (Pretty.string_of (Pretty.block [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop])); - val P = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) handle TERM _ => - err "Object-logic proposition expected"; - val c = Term.head_name_of P; - val (_, {elims, ...}) = the_inductive ctxt c; + val elims = InductAttrib.find_casesS ctxt prop; val cprop = Thm.cterm_of thy prop; - val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac; + val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac; fun mk_elim rl = Thm.implies_intr cprop (Tactic.rule_by_tactic tac (Thm.assume cprop RS rl)) |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt); @@ -486,9 +506,11 @@ let val k = length Ts; val bs = map Bound (k - 1 downto 0); - val P = list_comb (List.nth (preds, i), ys @ bs); + val P = list_comb (List.nth (preds, i), + map (incr_boundvars k) ys @ bs); val Q = list_abs (mk_names "x" k ~~ Ts, - HOLogic.mk_binop inductive_conj_name (list_comb (s, bs), P)) + HOLogic.mk_binop inductive_conj_name + (list_comb (incr_boundvars k s, bs), P)) in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end | NONE => (case s of (t $ u) => (fst (subst t) $ fst (subst u), NONE) @@ -585,10 +607,13 @@ fun subst t = (case dest_predicate cs params t of SOME (_, i, ts, (Ts, Us)) => - let val zs = map Bound (length Us - 1 downto 0) + let + val l = length Us; + val zs = map Bound (l - 1 downto 0) in list_abs (map (pair "z") Us, list_comb (p, - make_bool_args' bs i @ make_args argTs ((ts ~~ Ts) @ (zs ~~ Us)))) + make_bool_args' bs i @ make_args argTs + ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us)))) end | NONE => (case t of t1 $ t2 => subst t1 $ subst t2 @@ -642,7 +667,7 @@ (list_comb (rec_const, params @ make_bool_args' bs i @ make_args argTs (xs ~~ Ts))))) end) (cnames_syn ~~ cs); - val (consts_defs, ctxt'') = fold_map (LocalTheory.def Thm.internalK) specs ctxt'; + val (consts_defs, ctxt'') = LocalTheory.defs Thm.internalK specs ctxt'; val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs); val mono = prove_mono predT fp_fun monos ctxt'' @@ -651,6 +676,56 @@ list_comb (rec_const, params), preds, argTs, bs, xs) end; +fun declare_rules rec_name coind no_ind cnames intrs intr_names intr_atts + elims raw_induct ctxt = + let + val ind_case_names = RuleCases.case_names intr_names; + val induct = + 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)]) + 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]); + + val (intrs', ctxt1) = + ctxt |> + note_theorems + (map (NameSpace.qualified rec_name) intr_names ~~ + intr_atts ~~ map (fn th => [([th], + [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>> + map (hd o snd); (* FIXME? *) + val (((_, elims'), (_, [induct'])), ctxt2) = + ctxt1 |> + note_theorem ((NameSpace.qualified rec_name "intros", []), intrs') ||>> + fold_map (fn (name, (elim, cases)) => + note_theorem ((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 (ContextRules.elim_query NONE))]), [elim]) #> + apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>> + note_theorem ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"), + map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); + + val ctxt3 = if no_ind orelse coind then ctxt2 else + let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct' + in + ctxt2 |> + note_theorems [((NameSpace.qualified rec_name "inducts", []), + 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 + end + in (intrs', elims', induct', ctxt3) end; + +type add_ind_def = bool -> bstring -> bool -> bool -> bool -> + term list -> ((string * Attrib.src list) * term) list -> thm list -> + term list -> (string * mixfix) list -> + local_theory -> inductive_result * local_theory + fun add_ind_def verbose alt_name coind no_elim no_ind cs intros monos params cnames_syn ctxt = let @@ -659,7 +734,8 @@ commas_quote (map fst cnames_syn)) else (); val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn; (* FIXME *) - val ((intr_names, intr_atts), intr_ts) = apfst split_list (split_list intros); + val ((intr_names, intr_atts), intr_ts) = + apfst split_list (split_list (map (check_rule ctxt cs params) intros)); val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds, argTs, bs, xs) = mk_ind_def alt_name coind cs intr_ts @@ -668,82 +744,44 @@ val (intrs, unfold) = prove_intrs coind mono fp_def (length bs + length xs) params intr_ts rec_preds_defs ctxt1; val elims = if no_elim then [] else - cnames ~~ prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt1; + prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt1; val raw_induct = zero_var_indexes (if no_ind then Drule.asm_rl else - if coind then ObjectLogic.rulify (rule_by_tactic - (rewrite_tac [le_fun_def, le_bool_def] THEN - fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct))) + if coind then + singleton (ProofContext.export + (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1) + (rotate_prems ~1 (ObjectLogic.rulify (rule_by_tactic + (rewrite_tac [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq] THEN + fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct))))) else prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def rec_preds_defs ctxt1); - val induct_cases = map (#1 o #1) intros; - val ind_case_names = RuleCases.case_names induct_cases; - val induct = - if coind then - (raw_induct, [RuleCases.case_names [rec_name], - RuleCases.case_conclusion (rec_name, induct_cases), - RuleCases.consumes 1]) - else if no_ind orelse length cs > 1 then - (raw_induct, [ind_case_names, RuleCases.consumes 0]) - else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]); - val (intrs', ctxt2) = - ctxt1 |> - note_theorems - (map (NameSpace.qualified rec_name) intr_names ~~ - intr_atts ~~ map (fn th => [([th], - [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>> - map (hd o snd); (* FIXME? *) - val (((_, elims'), (_, [induct'])), ctxt3) = - ctxt2 |> - note_theorem ((NameSpace.qualified rec_name "intros", []), intrs') ||>> - fold_map (fn (name, (elim, cases)) => - note_theorem ((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 (ContextRules.elim_query NONE))]), [elim]) #> - apfst (hd o snd)) elims ||>> - note_theorem ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"), - map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); - - val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set; - val ctxt4 = if no_ind then ctxt3 else - let val inducts = cnames ~~ ProjectRule.projects ctxt (1 upto length cnames) induct' - in - ctxt3 |> - note_theorems [((NameSpace.qualified rec_name (coind_prefix coind ^ "inducts"), []), - inducts |> map (fn (name, th) => ([th], - [Attrib.internal (K ind_case_names), - Attrib.internal (K (RuleCases.consumes 1)), - Attrib.internal (K (induct_att name))])))] |> snd - end; + val (intrs', elims', induct, ctxt2) = declare_rules rec_name coind no_ind + cnames intrs intr_names intr_atts elims raw_induct ctxt1; val names = map #1 cnames_syn; val result = {preds = preds, - defs = fp_def :: rec_preds_defs, - mono = mono, - unfold = unfold, intrs = intrs', elims = elims', raw_induct = rulify raw_induct, - induct = induct'}; + induct = induct}; - val ctxt5 = ctxt4 + val ctxt3 = ctxt2 |> Context.proof_map (put_inductives names ({names = names, coind = coind}, result)) |> LocalTheory.declaration (fn phi => let - val names' = map (LocalTheory.target_name ctxt4 o Morphism.name phi) names; + val names' = map (LocalTheory.target_name ctxt2 o Morphism.name phi) names; val result' = morph_result phi result; in put_inductives names' ({names = names', coind = coind}, result') end); - in (result, ctxt5) end; + in (result, ctxt3) end; (* external interfaces *) -fun add_inductive_i verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos ctxt = +fun gen_add_inductive_i mk_def verbose alt_name coind no_elim no_ind + cnames_syn pnames pre_intros monos ctxt = let val thy = ProofContext.theory_of ctxt; val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); @@ -797,16 +835,15 @@ member op = params t then I else insert op = v | _ => I) r []), r)); - val intros = map (apsnd (expand abbrevs') #> - check_rule thy cs params #> close_rule) pre_intros'; + val intros = map (apsnd (expand abbrevs') #> close_rule) pre_intros'; in ctxt |> - add_ind_def verbose alt_name coind no_elim no_ind cs intros monos + mk_def verbose alt_name coind no_elim no_ind cs intros monos params cnames_syn'' ||> fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs'' end; -fun add_inductive verbose coind cnames_syn pnames_syn intro_srcs raw_monos ctxt = +fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos ctxt = let val (_, ctxt') = Specification.read_specification (cnames_syn @ pnames_syn) [] ctxt; val intrs = map (fn ((name, att), s) => apsnd hd (hd (snd (fst @@ -820,9 +857,12 @@ (s, SOME (ProofContext.infer_type ctxt' s), mx)) cnames_syn; val (monos, ctxt'') = LocalTheory.theory_result (IsarCmd.apply_theorems raw_monos) ctxt; in - add_inductive_i verbose "" coind false false cnames_syn' pnames intrs monos ctxt'' + gen_add_inductive_i mk_def verbose "" coind false false cnames_syn' pnames intrs monos ctxt'' end; +val add_inductive_i = gen_add_inductive_i add_ind_def; +val add_inductive = gen_add_inductive add_ind_def; + fun add_inductive_global verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos = TheoryTarget.init NONE #> add_inductive_i verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos #> @@ -890,9 +930,9 @@ (* setup theory *) val setup = - Method.add_methods [("ind_cases2", ind_cases, (* FIXME "ind_cases" (?) *) + Method.add_methods [("ind_cases", ind_cases, "dynamic case analysis on predicates")] #> - Attrib.add_attributes [("mono2", Attrib.add_del_args mono_add mono_del, (* FIXME "mono" *) + Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del, "declaration of monotonicity rule")]; @@ -910,25 +950,27 @@ | ((b, _), _) => error ("Illegal simultaneous specification " ^ quote b)) | (a, _) => error ("Illegal local specification parameters for " ^ quote a)); -fun ind_decl coind = +fun gen_ind_decl mk_def coind = P.opt_target -- P.fixes -- P.for_fixes -- Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] -- Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] >> (fn ((((loc, preds), params), specs), monos) => Toplevel.local_theory loc - (fn lthy => lthy - |> add_inductive true coind preds params (flatten_specification specs) monos |> snd)); + (fn lthy => lthy |> gen_add_inductive mk_def true coind preds params + (flatten_specification specs) monos |> snd)); + +val ind_decl = gen_ind_decl add_ind_def; val inductiveP = - OuterSyntax.command "inductive2" "define inductive predicates" K.thy_decl (ind_decl false); + OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false); val coinductiveP = - OuterSyntax.command "coinductive2" "define coinductive predicates" K.thy_decl (ind_decl true); + OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true); val inductive_casesP = - OuterSyntax.command "inductive_cases2" + OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules (improper)" K.thy_script (P.opt_target -- P.and_list1 SpecParse.spec >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs)));