# HG changeset patch # User wenzelm # Date 977608294 -3600 # Node ID dfaf75f0076f5924fba2c17d19fa27eff2e390f8 # Parent 66604af28f945498c817dca70c99e1fb8e2c778e simplified quick_and_dirty stuff; tuned; diff -r 66604af28f94 -r dfaf75f0076f src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Sat Dec 23 22:51:01 2000 +0100 +++ b/src/HOL/Tools/inductive_package.ML Sat Dec 23 22:51:34 2000 +0100 @@ -1,7 +1,8 @@ (* Title: HOL/Tools/inductive_package.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Stefan Berghofer, TU Muenchen + Author: Stefan Berghofer, TU Muenchen + Author: Markus Wenzel, TU Muenchen Copyright 1994 University of Cambridge 1998 TU Muenchen @@ -39,6 +40,10 @@ val mono_add_global: theory attribute val mono_del_global: theory attribute val get_monos: theory -> thm list + val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text + -> theory -> theory + val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text + -> theory -> theory val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> theory attribute list -> ((bstring * term) * theory attribute list) list -> thm list -> thm list -> theory -> theory * @@ -49,10 +54,6 @@ (xstring * Args.src list) list -> theory -> theory * {defs: thm list, elims: thm list, raw_induct: thm, induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} - val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text - -> theory -> theory - val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text - -> theory -> theory val setup: (theory -> theory) list end; @@ -62,7 +63,13 @@ (** theory context references **) -val mk_inductive_conj = HOLogic.mk_binop "Inductive.conj"; +val mono_name = "Ord.mono"; +val gfp_name = "Gfp.gfp"; +val lfp_name = "Lfp.lfp"; +val vimage_name = "Inverse_Image.vimage"; +val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD); + +val inductive_conj_name = "Inductive.conj"; val inductive_conj_def = thm "conj_def"; val inductive_conj = thms "inductive_conj"; val inductive_atomize = thms "inductive_atomize"; @@ -71,7 +78,7 @@ -(*** theory data ***) +(** theory data **) (* data kind 'HOL/inductive' *) @@ -150,20 +157,18 @@ -(** utilities **) - -(* messages *) +(** misc utilities **) val quiet_mode = ref false; -fun message s = if !quiet_mode then () else writeln s; +fun message s = if ! quiet_mode then () else writeln s; +fun clean_message s = if ! quick_and_dirty then () else message s; fun coind_prefix true = "co" | coind_prefix false = ""; -(* the following code ensures that each recursive set *) -(* always has the same type in all introduction rules *) - +(*the following code ensures that each recursive set always has the + same type in all introduction rules*) fun unify_consts sign cs intr_ts = (let val {tsig, ...} = Sign.rep_sg sign; @@ -192,15 +197,7 @@ (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts)); -(* misc *) - -val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD); - -val vimage_name = Sign.intern_const (Theory.sign_of Inverse_Image.thy) "vimage"; -val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono"; - -(* make injections needed in mutually recursive definitions *) - +(*make injections used in mutually recursive definitions*) fun mk_inj cs sumT c x = let fun mk_inj' T n i = @@ -216,8 +213,7 @@ in mk_inj' sumT (length cs) (1 + find_index_eq c cs) end; -(* make "vimage" terms for selecting out components of mutually rec.def. *) - +(*make "vimage" terms for selecting out components of mutually rec.def*) fun mk_vimage cs sumT t c = if length cs < 2 then t else let val cT = HOLogic.dest_setT (fastype_of c); @@ -274,20 +270,13 @@ full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o full_simplify inductive_conj; -fun rulified x = Drule.rule_attribute (K rulify) x; - end; -fun try' f msg sign t = (case (try f t) of - Some x => x - | None => error (msg ^ Sign.string_of_term sign t)); - +(** properties of (co)inductive sets **) -(*** properties of (co)inductive sets ***) - -(** elimination rules **) +(* elimination rules *) fun mk_elims cs cTs params intr_ts intr_names = let @@ -319,8 +308,7 @@ end; - -(** premises and conclusions of induction rules **) +(* premises and conclusions of induction rules *) fun mk_indrule cs cTs params intr_ts = let @@ -343,7 +331,7 @@ fun subst (s as ((m as Const ("op :", T)) $ t $ u)) = (case pred_of u of None => (m $ fst (subst t) $ fst (subst u), None) - | Some P => (mk_inductive_conj (s, P $ t), Some (s, P $ t))) + | Some P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), Some (s, P $ t))) | subst s = (case pred_of s of Some P => (HOLogic.mk_binop "op Int" @@ -388,8 +376,7 @@ end; - -(** prepare cases and induct rules **) +(* prepare cases and induct rules *) (* transform mutual rule: @@ -424,27 +411,23 @@ -(*** proofs for (co)inductive sets ***) +(** proofs for (co)inductive sets **) -(** prove monotonicity **) +(* prove monotonicity -- NOT subject to quick_and_dirty! *) fun prove_mono setT fp_fun monos thy = - let - val _ = message " Proving monotonicity ..."; - - val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop + (message " Proving monotonicity ..."; + Goals.prove_goalw_cterm [] (*NO SkipProof.prove_goalw_cterm here!*) + (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun))) - (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]) - - in mono end; + (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])); - -(** prove introduction rules **) +(* prove introduction rules *) fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = let - val _ = message " Proving the introduction rules ..."; + val _ = clean_message " Proving the introduction rules ..."; val unfold = standard (mono RS (fp_def RS (if coind then def_gfp_unfold else def_lfp_unfold))); @@ -453,8 +436,8 @@ | select_disj _ 1 = [rtac disjI1] | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1)); - val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs - (cterm_of (Theory.sign_of thy) intr) (fn prems => + val intrs = map (fn (i, intr) => SkipProof.prove_goalw_cterm thy rec_sets_defs + (Thm.cterm_of (Theory.sign_of thy) intr) (fn prems => [(*insert prems and underlying sets*) cut_facts_tac prems 1, stac unfold 1, @@ -463,7 +446,7 @@ EVERY1 (select_disj (length intr_ts) i), (*Not ares_tac, since refl must be tried before any equality assumptions; backtracking may occur if the premises have extra variables!*) - DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1), + DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1), (*Now solve the equations like Inl 0 = Inl ?b2*) rewrite_goals_tac con_defs, REPEAT (rtac refl 1)]) @@ -472,41 +455,37 @@ in (intrs, unfold) end; - -(** prove elimination rules **) +(* prove elimination rules *) fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy = let - val _ = message " Proving the elimination rules ..."; + val _ = clean_message " Proving the elimination rules ..."; val rules1 = [CollectE, disjE, make_elim vimageD, exE]; - val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ - map make_elim [Inl_inject, Inr_inject]; + val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject]; in - map (fn (t, cases) => prove_goalw_cterm rec_sets_defs - (cterm_of (Theory.sign_of thy) t) (fn prems => + map (fn (t, cases) => SkipProof.prove_goalw_cterm thy rec_sets_defs + (Thm.cterm_of (Theory.sign_of thy) t) (fn prems => [cut_facts_tac [hd prems] 1, dtac (unfold RS subst) 1, REPEAT (FIRSTGOAL (eresolve_tac rules1)), REPEAT (FIRSTGOAL (eresolve_tac rules2)), - EVERY (map (fn prem => - DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]) + EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]) |> rulify |> RuleCases.name cases) (mk_elims cs cTs params intr_ts intr_names) end; -(** derivation of simplified elimination rules **) +(* derivation of simplified elimination rules *) (*Applies freeness of the given constructors, which *must* be unfolded by the given defs. Cannot simply use the local con_defs because con_defs=[] - for inference systems. - *) + for inference systems. (??) *) (*cprop should have the form t:Si where Si is an inductive set*) -val mk_cases_err = "mk_cases: proposition not of form 't : S_i'"; +val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\""; fun mk_cases_i elims ss cprop = let @@ -561,13 +540,12 @@ val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name)); - -(** prove induction rule **) +(* prove induction rule *) fun prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def rec_sets_defs thy = let - val _ = message " Proving the induction rule ..."; + val _ = clean_message " Proving the induction rule ..."; val sign = Theory.sign_of thy; @@ -597,15 +575,14 @@ (* simplification rules for vimage and Collect *) val vimage_simps = if length cs < 2 then [] else - map (fn c => prove_goalw_cterm [] (cterm_of sign + map (fn c => SkipProof.prove_goalw_cterm thy [] (Thm.cterm_of sign (HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $ nth_elem (find_index_eq c cs, preds))))) - (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, - rtac refl 1])) cs; + (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs; - val induct = prove_goalw_cterm [inductive_conj_def] (cterm_of sign + val induct = SkipProof.prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign (Logic.list_implies (ind_prems, ind_concl))) (fn prems => [rtac (impI RS allI) 1, DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1), @@ -620,7 +597,7 @@ EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); - val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign + val lemma = SkipProof.prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems => [cut_facts_tac prems 1, REPEAT (EVERY @@ -633,9 +610,7 @@ -(*** specification of (co)inductive sets ****) - -(** definitional introduction of (co)inductive sets **) +(** specification of (co)inductive sets **) fun cond_declare_consts declare_consts cs paramTs cnames = if declare_consts then @@ -648,8 +623,7 @@ val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; val setT = HOLogic.mk_setT sumT; - val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp" - else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp"; + val fp_name = if coind then gfp_name else lfp_name; val used = foldr add_term_names (intr_ts, []); val [sname, xname] = variantlist (["S", "x"], used); @@ -688,7 +662,7 @@ (Const (full_rec_name, paramTs ---> setT), params); val fp_def_term = Logic.mk_equals (rec_const, - Const (fp_name, (setT --> setT) --> setT) $ fp_fun) + Const (fp_name, (setT --> setT) --> setT) $ fp_fun); val def_terms = fp_def_term :: (if length cs < 2 then [] else map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs); @@ -703,15 +677,14 @@ val mono = prove_mono setT fp_fun monos thy' - in - (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) - end; + in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end; fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos con_defs thy params paramTs cTs cnames induct_cases = let - val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ - commas_quote cnames) else (); + val _ = + if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ + commas_quote cnames) else (); val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); @@ -735,17 +708,14 @@ val (thy2, intrs') = thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts); - val (thy3, [intrs'']) = - thy2 - |> PureThy.add_thmss [(("intros", intrs'), atts)] - |>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])]) - |>> (if no_ind then I else #1 o PureThy.add_thms - [((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])]) + val (thy3, ([intrs'', elims'], [induct'])) = + thy2 + |> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])] + |>>> PureThy.add_thms + [((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])] |>> Theory.parent_path; - val elims' = if no_elim then elims else PureThy.get_thms thy3 "elims"; (* FIXME improve *) - val induct' = if no_ind then induct else PureThy.get_thm thy3 (coind_prefix coind ^ "induct"); (* FIXME improve *) in (thy3, - {defs = fp_def::rec_sets_defs, + {defs = fp_def :: rec_sets_defs, mono = mono, unfold = unfold, intrs = intrs'', @@ -756,59 +726,12 @@ end; - -(** axiomatic introduction of (co)inductive sets **) - -fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs - atts intros monos con_defs thy params paramTs cTs cnames induct_cases = - let - val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames); - - val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); - val (thy1, _, fp_def, rec_sets_defs, _, _) = - mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy - params paramTs cTs cnames; - val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names); - val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; - val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl); - - val (thy2, [intrs, raw_elims]) = - thy1 - |> PureThy.add_axiomss_i - [(("raw_intros", intr_ts), [rulified]), - (("raw_elims", elim_ts), [rulified])] - |>> (if coind then I else - #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]); +(* external interfaces *) - val elims = map2 (fn (th, cases) => RuleCases.name cases th) (raw_elims, elim_cases); - val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy2 "raw_induct"; - val induct = if coind orelse length cs > 1 then raw_induct - else standard (raw_induct RSN (2, rev_mp)); - - val (thy3, intrs') = - thy2 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts); - val (thy4, [intrs'', elims']) = - thy3 - |> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])] - |>> (if coind then I - else #1 o PureThy.add_thms [(("induct", rulify induct), - [RuleCases.case_names induct_cases])]) - |>> Theory.parent_path; - val induct' = if coind then raw_induct else PureThy.get_thm thy4 "induct"; - in (thy4, - {defs = fp_def :: rec_sets_defs, - mono = Drule.asm_rl, - unfold = Drule.asm_rl, - intrs = intrs'', - elims = elims', - mk_cases = mk_cases elims', - raw_induct = rulify raw_induct, - induct = induct'}) - end; - - - -(** introduction of (co)inductive sets **) +fun try_term f msg sign t = + (case Library.try f t of + Some x => x + | None => error (msg ^ Sign.string_of_term sign t)); fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs atts pre_intros monos con_defs thy = @@ -818,13 +741,13 @@ (*parameters should agree for all mutually recursive components*) val (_, params) = strip_comb (hd cs); - val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\ + val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\ \ component is not a free variable: " sign) params; - val cTs = map (try' (HOLogic.dest_setT o fastype_of) + val cTs = map (try_term (HOLogic.dest_setT o fastype_of) "Recursive component not of type set: " sign) cs; - val full_cnames = map (try' (fst o dest_Const o head_of) + val full_cnames = map (try_term (fst o dest_Const o head_of) "Recursive set not previously declared as constant: " sign) cs; val cnames = map Sign.base_name full_cnames; @@ -834,18 +757,13 @@ val induct_cases = map (#1 o #1) intros; val (thy1, result as {elims, induct, ...}) = - (if ! quick_and_dirty andalso not coind (* FIXME *) then add_ind_axm else add_ind_def) - verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos + add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos con_defs thy params paramTs cTs cnames induct_cases; val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result) |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases; in (thy2, result) end; - - -(** external interface **) - fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = let val sign = Theory.sign_of thy; @@ -915,5 +833,4 @@ end; - end;