# HG changeset patch # User berghofe # Date 899232395 -7200 # Node ID f6f225a9d5a72d3475352e61472d50e8a7f32e50 # Parent 48e70d9fe05f919644604ab4e5b9b7962e7a6397 Removed old inductive definition package. diff -r 48e70d9fe05f -r f6f225a9d5a7 src/HOL/Inductive.ML --- a/src/HOL/Inductive.ML Tue Jun 30 20:43:36 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,99 +0,0 @@ -(* Title: HOL/inductive.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -(Co)Inductive Definitions for HOL - -Inductive definitions use least fixedpoints with standard products and sums -Coinductive definitions use greatest fixedpoints with Quine products and sums - -Sums are used only for mutual recursion; -Products are used only to derive "streamlined" induction rules for relations -*) - -fun gen_fp_oper a (X,T,t) = - let val setT = Ind_Syntax.mk_setT T - in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t) end; - -structure Lfp_items = - struct - val checkThy = (fn thy => Theory.requires thy "Lfp" "inductive definitions") - val oper = gen_fp_oper "lfp" - val Tarski = def_lfp_Tarski - val induct = def_induct - end; - -structure Gfp_items = - struct - val checkThy = (fn thy => Theory.requires thy "Gfp" "coinductive definitions") - val oper = gen_fp_oper "gfp" - val Tarski = def_gfp_Tarski - val induct = def_Collect_coinduct - end; - - -functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) - : sig include INTR_ELIM INDRULE end = -let - structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and - Fp=Lfp_items); - - structure Indrule = Indrule_Fun - (structure Inductive=Inductive and Intr_elim=Intr_elim); -in - struct - val thy = Intr_elim.thy - val defs = Intr_elim.defs - val mono = Intr_elim.mono - val intrs = Intr_elim.intrs - val elim = Intr_elim.elim - val mk_cases = Intr_elim.mk_cases - open Indrule - end -end; - - -structure Ind = Add_inductive_def_Fun (Lfp_items); - - -signature INDUCTIVE_STRING = - sig - val thy_name : string (*name of the new theory*) - val srec_tms : string list (*recursion terms*) - val sintrs : string list (*desired introduction rules*) - end; - - -(*Called by the theory sections or directly from ML*) -functor Inductive_Fun - (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end) - : sig include INTR_ELIM INDRULE end = -Ind_section_Fun - (open Inductive Ind_Syntax - val sign = sign_of thy; - val rec_tms = map (readtm sign termTVar) srec_tms - and intr_tms = map (readtm sign propT) sintrs; - val thy = thy |> Ind.add_fp_def_i(rec_tms, intr_tms) - |> Theory.add_name thy_name); - - - -signature COINDRULE = - sig - val coinduct : thm - end; - - -functor CoInd_section_Fun - (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) - : sig include INTR_ELIM COINDRULE end = -struct -structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp_items); - -open Intr_elim -val coinduct = raw_induct -end; - - -structure CoInd = Add_inductive_def_Fun(Gfp_items); diff -r 48e70d9fe05f -r f6f225a9d5a7 src/HOL/add_ind_def.ML --- a/src/HOL/add_ind_def.ML Tue Jun 30 20:43:36 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,168 +0,0 @@ -(* Title: HOL/add_ind_def.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Fixedpoint definition module -- for Inductive/Coinductive Definitions - -Features: -* least or greatest fixedpoints -* user-specified product and sum constructions -* mutually recursive definitions -* definitions involving arbitrary monotone operators -* automatically proves introduction and elimination rules - -The recursive sets must *already* be declared as constants in parent theory! - - Introduction rules have the form - [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |] - where M is some monotone operator (usually the identity) - P(x) is any (non-conjunctive) side condition on the free variables - ti, t are any terms - Sj, Sk are two of the sets being defined in mutual recursion - -Sums are used only for mutual recursion; -Products are used only to derive "streamlined" induction rules for relations - -Nestings of disjoint sum types: - (a+(b+c)) for 3, ((a+b)+(c+d)) for 4, ((a+b)+(c+(d+e))) for 5, - ((a+(b+c))+(d+(e+f))) for 6 -*) - -signature FP = (** Description of a fixed point operator **) - sig - val checkThy : theory -> unit (*signals error if Lfp/Gfp is missing*) - val oper : string * typ * term -> term (*fixed point operator*) - val Tarski : thm (*Tarski's fixed point theorem*) - val induct : thm (*induction/coinduction rule*) - end; - - -signature ADD_INDUCTIVE_DEF = - sig - val add_fp_def_i : term list * term list -> theory -> theory - end; - - - -(*Declares functions to add fixedpoint/constructor defs to a theory*) -functor Add_inductive_def_Fun (Fp: FP) : ADD_INDUCTIVE_DEF = -struct -open Ind_Syntax; - -(*internal version*) -fun add_fp_def_i (rec_tms, intr_tms) thy = - let - val dummy = Fp.checkThy thy (*has essential ancestors?*) - - val sign = sign_of thy; - - (*rec_params should agree for all mutually recursive components*) - val rec_hds = map head_of rec_tms; - - val _ = assert_all is_Const rec_hds - (fn t => "Recursive set not previously declared as constant: " ^ - Sign.string_of_term sign t); - - (*Now we know they are all Consts, so get their names, type and params*) - val rec_names = map (#1 o dest_Const) rec_hds - and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); - - val rec_base_names = map Sign.base_name rec_names; - val _ = assert_all Syntax.is_identifier rec_base_names - (fn a => "Base name of recursive set not an identifier: " ^ a); - - local (*Checking the introduction rules*) - val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; - fun intr_ok set = - case head_of set of Const(a,_) => a mem rec_names | _ => false; - in - val _ = assert_all intr_ok intr_sets - (fn t => "Conclusion of rule does not name a recursive set: " ^ - Sign.string_of_term sign t); - end; - - val _ = assert_all is_Free rec_params - (fn t => "Param in recursion term not a free variable: " ^ - Sign.string_of_term sign t); - - (*** Construct the lfp definition ***) - val mk_variant = variant (foldr add_term_names (intr_tms,[])); - - val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w"; - - (*Mutual recursion ?? *) - val dom_set = body_type recT - val dom_sumT = dest_setT dom_set - - val freez = Free(z, dom_sumT) - and freeX = Free(X, dom_set); - - fun dest_tprop (Const("Trueprop",_) $ P) = P - | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ - Sign.string_of_term sign Q); - - (*Makes a disjunct from an introduction rule*) - fun lfp_part intr = (*quantify over rule's free vars except parameters*) - let val prems = map dest_tprop (Logic.strip_imp_prems intr) - val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds - val exfrees = term_frees intr \\ rec_params - val zeq = eq_const dom_sumT $ freez $ (#1 (rule_concl intr)) - in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end; - - (*The Part(A,h) terms -- compose injections to make h*) - fun mk_Part (Bound 0, _) = freeX (*no mutual rec, no Part needed*) - | mk_Part (h, domT) = - let val goodh = mend_sum_types (h, dom_sumT) - and Part_const = - Const("Part", [dom_set, domT-->dom_sumT]---> dom_set) - in Part_const $ freeX $ Abs(w,domT,goodh) end; - - (*Access to balanced disjoint sums via injections?? - Mutual recursion is NOT supported*) - val parts = ListPair.map mk_Part - (accesses_bal (ap Inl, ap Inr, Bound 0) 1, - [dom_set]); - - (*replace each set by the corresponding Part(A,h)*) - val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; - - val lfp_rhs = Fp.oper(X, dom_sumT, - mk_Collect(z, dom_sumT, - fold_bal (app disj) part_intrs)) - - - (*** Make the new theory ***) - - (*A key definition: - If no mutual recursion then it equals the one recursive set. - If mutual recursion then it differs from all the recursive sets. *) - val big_rec_base_name = space_implode "_" rec_base_names; - val big_rec_name = Sign.intern_const sign big_rec_base_name; - - (*Big_rec... is the union of the mutually recursive sets*) - val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); - - (*The individual sets must already be declared*) - val axpairs = map Logic.mk_defpair - ((big_rec_tm, lfp_rhs) :: - (case parts of - [_] => [] (*no mutual recursion*) - | _ => rec_tms ~~ (*define the sets as Parts*) - map (subst_atomic [(freeX, big_rec_tm)]) parts)); - - (*tracing: print the fixedpoint definition*) - val _ = if !Ind_Syntax.trace then - seq (writeln o Sign.string_of_term sign o #2) axpairs - else () - - (*Detect occurrences of operator, even with other types!*) - val _ = (case rec_names inter (add_term_names (lfp_rhs,[])) of - [] => () - | x::_ => error ("Illegal occurrence of recursion op: " ^ x ^ - "\n\t*Consider adding type constraints*")) - - in thy |> PureThy.add_defs_i (map Attribute.none axpairs) end - - -end; diff -r 48e70d9fe05f -r f6f225a9d5a7 src/HOL/ind_syntax.ML --- a/src/HOL/ind_syntax.ML Tue Jun 30 20:43:36 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,101 +0,0 @@ -(* Title: HOL/ind_syntax.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Abstract Syntax functions for Inductive Definitions -See also hologic.ML and ../Pure/section-utils.ML -*) - -(*The structure protects these items from redeclaration (somewhat!). The - datatype definitions in theory files refer to these items by name! -*) -structure Ind_Syntax = -struct - -(*Print tracing messages during processing of "inductive" theory sections*) -val trace = ref false; - -(** Abstract syntax definitions for HOL **) - -open HOLogic; - -fun Int_const T = - let val sT = mk_setT T - in Const("op Int", [sT,sT]--->sT) end; - -fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P)); - -fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P)); - -(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) -fun mk_all_imp (A,P) = - let val T = dest_setT (fastype_of A) - in all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ - betapply(P, Bound 0)) - end; - -(** Disjoint sum type **) - -fun mk_sum (T1,T2) = Type("+", [T1,T2]); -val Inl = Const("Inl", dummyT) -and Inr = Const("Inr", dummyT); (*correct types added later!*) -(*val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)*) - -fun summands (Type("+", [T1,T2])) = summands T1 @ summands T2 - | summands T = [T]; - -(*Given the destination type, fills in correct types of an Inl/Inr nest*) -fun mend_sum_types (h,T) = - (case (h,T) of - (Const("Inl",_) $ h1, Type("+", [T1,T2])) => - Const("Inl", T1 --> T) $ (mend_sum_types (h1, T1)) - | (Const("Inr",_) $ h2, Type("+", [T1,T2])) => - Const("Inr", T2 --> T) $ (mend_sum_types (h2, T2)) - | _ => h); - - - -(*simple error-checking in the premises of an inductive definition*) -fun chk_prem rec_hd (Const("op &",_) $ _ $ _) = - error"Premises may not be conjuctive" - | chk_prem rec_hd (Const("op :",_) $ t $ X) = - deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol" - | chk_prem rec_hd t = - deny (Logic.occs(rec_hd,t)) "Recursion term in side formula"; - -(*Return the conclusion of a rule, of the form t:X*) -fun rule_concl rl = - let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = - Logic.strip_imp_concl rl - in (t,X) end; - -(*As above, but return error message if bad*) -fun rule_concl_msg sign rl = rule_concl rl - handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ - Sign.string_of_term sign rl); - -(*For simplifying the elimination rule*) -val sumprod_free_SEs = - Pair_inject :: - map make_elim [(*Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject*)]; - -(*For deriving cases rules. - read_instantiate replaces a propositional variable by a formula variable*) -val equals_CollectD = - read_instantiate [("W","?Q")] - (make_elim (equalityD1 RS subsetD RS CollectD)); - -(*Delete needless equality assumptions*) -val refl_thin = prove_goal HOL.thy "!!P. [| a=a; P |] ==> P" - (fn _ => [assume_tac 1]); - -(*Includes rules for Suc and Pair since they are common constructions*) -val elim_rls = [asm_rl, FalseE, (*Suc_neq_Zero, Zero_neq_Suc, - make_elim Suc_inject, *) - refl_thin, conjE, exE, disjE]; - -end; - - -val trace_induct = Ind_Syntax.trace; diff -r 48e70d9fe05f -r f6f225a9d5a7 src/HOL/indrule.ML --- a/src/HOL/indrule.ML Tue Jun 30 20:43:36 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,259 +0,0 @@ -(* Title: HOL/indrule.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Induction rule module -- for Inductive/Coinductive Definitions - -Proves a strong induction rule and a mutual induction rule -*) - -signature INDRULE = - sig - val induct : thm (*main induction rule*) - val mutual_induct : thm (*mutual induction rule*) - end; - - -functor Indrule_Fun - (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end and - Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE = -let - -val sign = sign_of Inductive.thy; - -val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms); - -val elem_type = Ind_Syntax.dest_setT (body_type recT); -val big_rec_name = space_implode "_" Intr_elim.rec_names; -val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); - -val _ = writeln " Proving the induction rule..."; - -(*** Prove the main induction rule ***) - -val pred_name = "P"; (*name for predicate variables*) - -val big_rec_def::part_rec_defs = Intr_elim.defs; - -(*Used to express induction rules: adds induction hypotheses. - ind_alist = [(rec_tm1,pred1),...] -- associates predicates with rec ops - prem is a premise of an intr rule*) -fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ - (Const("op :",_)$t$X), iprems) = - (case gen_assoc (op aconv) (ind_alist, X) of - Some pred => prem :: Ind_Syntax.mk_Trueprop (pred $ t) :: iprems - | None => (*possibly membership in M(rec_tm), for M monotone*) - let fun mk_sb (rec_tm,pred) = - (case binder_types (fastype_of pred) of - [T] => (rec_tm, - Ind_Syntax.Int_const T $ rec_tm $ - (Ind_Syntax.Collect_const T $ pred)) - | _ => error - "Bug: add_induct_prem called with non-unary predicate") - in subst_free (map mk_sb ind_alist) prem :: iprems end) - | add_induct_prem ind_alist (prem,iprems) = prem :: iprems; - -(*Make a premise of the induction rule.*) -fun induct_prem ind_alist intr = - let val quantfrees = map dest_Free (term_frees intr \\ rec_params) - val iprems = foldr (add_induct_prem ind_alist) - (Logic.strip_imp_prems intr,[]) - val (t,X) = Ind_Syntax.rule_concl intr - val (Some pred) = gen_assoc (op aconv) (ind_alist, X) - val concl = Ind_Syntax.mk_Trueprop (pred $ t) - in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end - handle Bind => error"Recursion term not found in conclusion"; - -(*Minimizes backtracking by delivering the correct premise to each goal*) -fun ind_tac [] 0 = all_tac - | ind_tac(prem::prems) i = - DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN - ind_tac prems (i-1); - -val pred = Free(pred_name, elem_type --> Ind_Syntax.boolT); - -val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) - Inductive.intr_tms; - -val _ = if !Ind_Syntax.trace then - (writeln "ind_prems = "; - seq (writeln o Sign.string_of_term sign) ind_prems; - writeln "raw_induct = "; print_thm Intr_elim.raw_induct) - else (); - - -(*We use a MINIMAL simpset because others (such as HOL_ss) contain too many - simplifications. If the premises get simplified, then the proofs could - fail. This arose with a premise of the form {(F n,G n)|n . True}, which - expanded to something containing ...&True. *) -val min_ss = HOL_basic_ss; - -val quant_induct = - prove_goalw_cterm part_rec_defs - (cterm_of sign - (Logic.list_implies (ind_prems, - Ind_Syntax.mk_Trueprop (Ind_Syntax.mk_all_imp - (big_rec_tm,pred))))) - (fn prems => - [rtac (impI RS allI) 1, - DETERM (etac Intr_elim.raw_induct 1), - full_simp_tac (min_ss addsimps [Part_Collect]) 1, - (*This CollectE and disjE separates out the introduction rules*) - REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])), - (*Now break down the individual cases. No disjE here in case - some premise involves disjunction.*) - REPEAT (FIRSTGOAL (eresolve_tac [CollectE, IntE, exE, conjE] - ORELSE' hyp_subst_tac)), - ind_tac (rev prems) (length prems)]) - handle e => print_sign_exn sign e; - -val _ = if !Ind_Syntax.trace then - (writeln "quant_induct = "; print_thm quant_induct) - else (); - - -(*** Prove the simultaneous induction rule ***) - -(*Make distinct predicates for each inductive set. - Splits cartesian products in elem_type, however nested*) - -(*The components of the element type, several if it is a product*) -val elem_factors = Prod_Syntax.factors elem_type; -val elem_frees = mk_frees "za" elem_factors; -val elem_tuple = Prod_Syntax.mk_tuple elem_type elem_frees; - -(*Given a recursive set, return the "split" predicate - and a conclusion for the simultaneous induction rule*) -fun mk_predpair rec_tm = - let val rec_name = (#1 o dest_Const o head_of) rec_tm - val pfree = Free(pred_name ^ "_" ^ rec_name, - elem_factors ---> Ind_Syntax.boolT) - val qconcl = - foldr Ind_Syntax.mk_all - (elem_frees, - Ind_Syntax.imp $ (Ind_Syntax.mk_mem (elem_tuple, rec_tm)) - $ (list_comb (pfree, elem_frees))) - in (Prod_Syntax.ap_split elem_type Ind_Syntax.boolT pfree, - qconcl) - end; - -val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms); - -(*Used to form simultaneous induction lemma*) -fun mk_rec_imp (rec_tm,pred) = - Ind_Syntax.imp $ (Ind_Syntax.mk_mem (Bound 0, rec_tm)) $ (pred $ Bound 0); - -(*To instantiate the main induction rule*) -val induct_concl = - Ind_Syntax.mk_Trueprop - (Ind_Syntax.mk_all_imp - (big_rec_tm, - Abs("z", elem_type, - fold_bal (app Ind_Syntax.conj) - (ListPair.map mk_rec_imp (Inductive.rec_tms,preds))))) -and mutual_induct_concl = - Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls); - -val _ = if !Ind_Syntax.trace then - (writeln ("induct_concl = " ^ - Sign.string_of_term sign induct_concl); - writeln ("mutual_induct_concl = " ^ - Sign.string_of_term sign mutual_induct_concl)) - else (); - - -val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp], - resolve_tac [allI, impI, conjI, Part_eqI, refl], - dresolve_tac [spec, mp, splitD]]; - -val need_mutual = length Intr_elim.rec_names > 1; - -val lemma = (*makes the link between the two induction rules*) - if need_mutual then - (writeln " Proving the mutual induction rule..."; - prove_goalw_cterm part_rec_defs - (cterm_of sign (Logic.mk_implies (induct_concl, - mutual_induct_concl))) - (fn prems => - [cut_facts_tac prems 1, - REPEAT (rewrite_goals_tac [split RS eq_reflection] THEN - lemma_tac 1)]) - handle e => print_sign_exn sign e) - else (writeln " [ No mutual induction rule needed ]"; - TrueI); - -val _ = if !Ind_Syntax.trace then - (writeln "lemma = "; print_thm lemma) - else (); - - -(*Mutual induction follows by freeness of Inl/Inr.*) - -(*Simplification largely reduces the mutual induction rule to the - standard rule*) -val mut_ss = min_ss addsimps [Inl_not_Inr, Inr_not_Inl, Inl_eq, Inr_eq, split]; - -val all_defs = [split RS eq_reflection] @ Inductive.con_defs @ part_rec_defs; - -(*Removes Collects caused by M-operators in the intro rules*) -val cmonos = [subset_refl RS Int_Collect_mono] RL Inductive.monos RLN - (2,[rev_subsetD]); - -(*Avoids backtracking by delivering the correct premise to each goal*) -fun mutual_ind_tac [] 0 = all_tac - | mutual_ind_tac(prem::prems) i = - DETERM - (SELECT_GOAL - ( - (*Simplify the assumptions and goal by unfolding Part and - using freeness of the Sum constructors; proves all but one - conjunct by contradiction*) - rewrite_goals_tac all_defs THEN - simp_tac (mut_ss addsimps [Part_def]) 1 THEN - IF_UNSOLVED (*simp_tac may have finished it off!*) - ((*simplify assumptions*) - full_simp_tac mut_ss 1 THEN - (*unpackage and use "prem" in the corresponding place*) - REPEAT (rtac impI 1) THEN - rtac (rewrite_rule all_defs prem) 1 THEN - (*prem must not be REPEATed below: could loop!*) - DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' - eresolve_tac (conjE::mp::cmonos)))) - ) i) - THEN mutual_ind_tac prems (i-1); - -val mutual_induct_split = - if need_mutual then - prove_goalw_cterm [] - (cterm_of sign - (Logic.list_implies (map (induct_prem (Inductive.rec_tms ~~ preds)) - Inductive.intr_tms, - mutual_induct_concl))) - (fn prems => - [rtac (quant_induct RS lemma) 1, - mutual_ind_tac (rev prems) (length prems)]) - handle e => print_sign_exn sign e - else TrueI; - -(** Uncurrying the predicate in the ordinary induction rule **) - -val xvar = cterm_of sign (Var(("x",0), elem_type)); - -(*strip quantifier and instantiate the variable to a tuple*) -val induct0 = quant_induct RS spec RSN (2,rev_mp) |> - zero_var_indexes |> - freezeT |> (*Because elem_type contains TFrees not TVars*) - instantiate ([], [(xvar, cterm_of sign elem_tuple)]); - -val Const ("Trueprop", _) $ (pred_var $ _) = concl_of induct0 - - -in - struct - val induct = standard (Prod_Syntax.split_rule_var (pred_var, induct0)); - - (*Just "True" unless there's true mutual recursion. This saves storage.*) - val mutual_induct = Prod_Syntax.remove_split mutual_induct_split - end -end; diff -r 48e70d9fe05f -r f6f225a9d5a7 src/HOL/indrule.thy --- a/src/HOL/indrule.thy Tue Jun 30 20:43:36 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ - -indrule = intr_elim diff -r 48e70d9fe05f -r f6f225a9d5a7 src/HOL/intr_elim.ML --- a/src/HOL/intr_elim.ML Tue Jun 30 20:43:36 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,153 +0,0 @@ -(* Title: HOL/intr_elim.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Introduction/elimination rule module -- for Inductive/Coinductive Definitions -*) - -signature INDUCTIVE_ARG = (** Description of a (co)inductive def **) - sig - val thy : theory (*new theory with inductive defs*) - val monos : thm list (*monotonicity of each M operator*) - val con_defs : thm list (*definitions of the constructors*) - end; - - -signature INDUCTIVE_I = (** Terms read from the theory section **) - sig - val rec_tms : term list (*the recursive sets*) - val intr_tms : term list (*terms for the introduction rules*) - end; - -signature INTR_ELIM = - sig - val thy : theory (*copy of input theory*) - val defs : thm list (*definitions made in thy*) - val mono : thm (*monotonicity for the lfp definition*) - val intrs : thm list (*introduction rules*) - val elim : thm (*case analysis theorem*) - val mk_cases : thm list -> string -> thm (*generates case theorems*) - end; - -signature INTR_ELIM_AUX = (** Used to make induction rules **) - sig - val raw_induct : thm (*raw induction rule from Fp.induct*) - val rec_names : string list (*names of recursive sets*) - end; - -(*prove intr/elim rules for a fixedpoint definition*) -functor Intr_elim_Fun - (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end - and Fp: FP) - : sig include INTR_ELIM INTR_ELIM_AUX end = -let -val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms; -val big_rec_name = space_implode "_" rec_names; - -val _ = deny (big_rec_name mem (Sign.stamp_names_of (sign_of Inductive.thy))) - ("Definition " ^ big_rec_name ^ - " would clash with the theory of the same name!"); - -(*fetch fp definitions from the theory*) -val big_rec_def::part_rec_defs = - map (get_def Inductive.thy) - (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names); - - -val sign = sign_of Inductive.thy; - -(********) -val _ = writeln " Proving monotonicity..."; - -val Const("==",_) $ _ $ (Const(_,fpT) $ fp_abs) = - big_rec_def |> rep_thm |> #prop |> Logic.unvarify; - -(*For the type of the argument of mono*) -val [monoT] = binder_types fpT; - -val mono = - prove_goalw_cterm [] - (cterm_of sign (Ind_Syntax.mk_Trueprop - (Const("mono", monoT --> Ind_Syntax.boolT) $ fp_abs))) - (fn _ => - [rtac monoI 1, - REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]); - -val unfold = standard (mono RS (big_rec_def RS Fp.Tarski)); - -(********) -val _ = writeln " Proving the introduction rules..."; - -fun intro_tacsf disjIn prems = - [(*insert prems and underlying sets*) - cut_facts_tac prems 1, - stac unfold 1, - REPEAT (resolve_tac [Part_eqI,CollectI] 1), - (*Now 1-2 subgoals: the disjunction, perhaps equality.*) - rtac disjIn 1, - (*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), - (*Now solve the equations like Inl 0 = Inl ?b2*) - rewrite_goals_tac Inductive.con_defs, - REPEAT (rtac refl 1)]; - - -(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*) -val mk_disj_rls = - let fun f rl = rl RS disjI1 - and g rl = rl RS disjI2 - in accesses_bal(f, g, asm_rl) end; - -val intrs = ListPair.map (uncurry (prove_goalw_cterm part_rec_defs)) - (map (cterm_of sign) Inductive.intr_tms, - map intro_tacsf (mk_disj_rls(length Inductive.intr_tms))); - -(********) -val _ = writeln " Proving the elimination rule..."; - -(*Breaks down logical connectives in the monotonic function*) -val basic_elim_tac = - REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ - Ind_Syntax.sumprod_free_SEs) - ORELSE' bound_hyp_subst_tac)) - THEN prune_params_tac; - -(*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. -fun con_elim_tac defs = - rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs; - *) -fun con_elim_tac simps = - let val elim_tac = REPEAT o (eresolve_tac (Ind_Syntax.elim_rls @ - Ind_Syntax.sumprod_free_SEs)) - in ALLGOALS(EVERY'[elim_tac, - asm_full_simp_tac (simpset_of Nat.thy addsimps simps), - elim_tac, - REPEAT o bound_hyp_subst_tac]) - THEN prune_params_tac - end; - - -in - struct - val thy = Inductive.thy - and defs = big_rec_def :: part_rec_defs - and mono = mono - and intrs = intrs; - - val elim = rule_by_tactic basic_elim_tac - (unfold RS Ind_Syntax.equals_CollectD); - - (*String s should have the form t:Si where Si is an inductive set*) - fun mk_cases defs s = - rule_by_tactic (con_elim_tac defs) - (assume_read Inductive.thy s RS elim) - |> standard; - - val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct) - and rec_names = rec_names - end -end; diff -r 48e70d9fe05f -r f6f225a9d5a7 src/HOL/intr_elim.thy --- a/src/HOL/intr_elim.thy Tue Jun 30 20:43:36 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ - -intr_elim = Nat