Removed old inductive definition package.
--- 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);
--- 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;
--- 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;
--- 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;
--- 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
--- 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;
--- 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