INSTALLATION OF INDUCTIVE DEFINITIONS
HOL/Sexp, List, LList: updated for inductive defs; streamlined proofs
HOL/List, Subst/UTerm, ex/Simult, ex/Term: updated refs to Sexp intr rules
HOL/Univ/diag_eqI: new
HOL/intr_elim: now checks that the inductive name does not clash with
existing theory names
HOL/Sum: now type + is an infixr, to agree with type *
HOL/Set: added Pow and the derived rules PowI, PowD, Pow_bottom, Pow_top
HOL/Fun/set_cs: now includes Pow rules
HOL/mono/Pow_mono: new
HOL/Makefile: now has Inductive.thy,.ML and ex/Acc.thy,.ML
HOL/Sexp,List,LList,ex/Term: converted as follows
node *set -> item
Sexp -> sexp
LList_corec -> <self>
LList_ -> llist_
LList\> -> llist
List_case -> <self>
List_rec -> <self>
List_ -> list_
List\> -> list
Term_rec -> <self>
Term_ -> term_
Term\> -> term
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Finite.ML Thu Aug 25 11:01:45 1994 +0200
@@ -0,0 +1,84 @@
+(* Title: HOL/Finite.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Finite powerset operator
+*)
+
+open Finite;
+
+goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
+br lfp_mono 1;
+by (REPEAT (ares_tac basic_monos 1));
+val Fin_mono = result();
+
+goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
+by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1);
+val Fin_subset_Pow = result();
+
+(* A : Fin(B) ==> A <= B *)
+val FinD = Fin_subset_Pow RS subsetD RS PowD;
+
+(*Discharging ~ x:y entails extra work*)
+val major::prems = goal Finite.thy
+ "[| F:Fin(A); P({}); \
+\ !!F x. [| x:A; F:Fin(A); x~:F; P(F) |] ==> P(insert(x,F)) \
+\ |] ==> P(F)";
+by (rtac (major RS Fin.induct) 1);
+by (excluded_middle_tac "a:b" 2);
+by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*)
+by (REPEAT (ares_tac prems 1));
+val Fin_induct = result();
+
+(** Simplification for Fin **)
+
+val Fin_ss = set_ss addsimps Fin.intrs;
+
+(*The union of two finite sets is finite*)
+val major::prems = goal Finite.thy
+ "[| F: Fin(A); G: Fin(A) |] ==> F Un G : Fin(A)";
+by (rtac (major RS Fin_induct) 1);
+by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left]))));
+val Fin_UnI = result();
+
+(*Every subset of a finite set is finite*)
+val [subs,fin] = goal Finite.thy "[| A<=B; B: Fin(M) |] ==> A: Fin(M)";
+by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)",
+ rtac mp, etac spec,
+ rtac subs]);
+by (rtac (fin RS Fin_induct) 1);
+by (simp_tac (Fin_ss addsimps [subset_Un_eq]) 1);
+by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
+by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
+by (ALLGOALS (asm_simp_tac Fin_ss));
+val Fin_subset = result();
+
+(*The image of a finite set is finite*)
+val major::_ = goal Finite.thy
+ "F: Fin(A) ==> h``F : Fin(h``A)";
+by (rtac (major RS Fin_induct) 1);
+by (simp_tac Fin_ss 1);
+by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
+val Fin_imageI = result();
+
+val major::prems = goal Finite.thy
+ "[| c: Fin(A); b: Fin(A); \
+\ P(b); \
+\ !!(x::'a) y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
+\ |] ==> c<=b --> P(b-c)";
+by (rtac (major RS Fin_induct) 1);
+by (rtac (Diff_insert RS ssubst) 2);
+by (ALLGOALS (asm_simp_tac
+ (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
+val Fin_empty_induct_lemma = result();
+
+val prems = goal Finite.thy
+ "[| b: Fin(A); \
+\ P(b); \
+\ !!x y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
+\ |] ==> P({})";
+by (rtac (Diff_cancel RS subst) 1);
+by (rtac (Fin_empty_induct_lemma RS mp) 1);
+by (REPEAT (ares_tac (subset_refl::prems) 1));
+val Fin_empty_induct = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Finite.thy Thu Aug 25 11:01:45 1994 +0200
@@ -0,0 +1,17 @@
+(* Title: HOL/Finite.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Finite powerset operator
+*)
+
+Finite = Lfp +
+consts Fin :: "'a set => 'a set set"
+
+inductive "Fin(A)"
+ intrs
+ emptyI "{} : Fin(A)"
+ insertI "[| a: A; b: Fin(A) |] ==> insert(a,b) : Fin(A)"
+
+end
--- a/Fun.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Fun.ML Thu Aug 25 11:01:45 1994 +0200
@@ -167,10 +167,10 @@
(*** Set reasoning tools ***)
val set_cs = HOL_cs
- addSIs [ballI, subsetI, InterI, INT_I, INT1_I, CollectI,
+ addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI,
ComplI, IntI, DiffI, UnCI, insertCI]
addIs [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]
- addSEs [bexE, UnionE, UN_E, UN1_E, DiffE,
+ addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]
addEs [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
subsetD, subsetCE];
--- a/Gfp.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Gfp.ML Thu Aug 25 11:01:45 1994 +0200
@@ -113,6 +113,15 @@
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct]) 1));
val def_coinduct = result();
+(*The version used in the induction/coinduction package*)
+val prems = goal Gfp.thy
+ "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); \
+\ a: X; !!z. z: X ==> P(X Un A, z) |] ==> \
+\ a : A";
+by (rtac def_coinduct 1);
+by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1));
+val def_Collect_coinduct = result();
+
val rew::prems = goal Gfp.thy
"[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x.f(x) Un X Un A)) |] ==> a: A";
by (rewtac rew);
--- a/HOL.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/HOL.ML Thu Aug 25 11:01:45 1994 +0200
@@ -11,57 +11,58 @@
signature HOL_LEMMAS =
sig
- val allE: thm
- val all_dupE: thm
- val allI: thm
- val arg_cong: thm
- val fun_cong: thm
+ val allE : thm
+ val all_dupE : thm
+ val allI : thm
+ val arg_cong : thm
+ val fun_cong : thm
val box_equals: thm
- val case_tac: string -> int -> tactic
- val ccontr: thm
- val classical: thm
- val cong: thm
- val conjunct1: thm
- val conjunct2: thm
- val conjE: thm
- val conjI: thm
- val contrapos: thm
- val disjCI: thm
- val disjE: thm
- val disjI1: thm
- val disjI2: thm
- val eqTrueI: thm
- val eqTrueE: thm
- val ex1E: thm
- val ex1I: thm
- val exCI: thm
- val exI: thm
- val exE: thm
- val excluded_middle: thm
- val FalseE: thm
- val False_neq_True: thm
- val iffCE : thm
- val iffD1: thm
- val iffD2: thm
- val iffE: thm
- val iffI: thm
- val impCE: thm
- val impE: thm
- val not_sym: thm
- val notE: thm
- val notI: thm
- val notnotD : thm
- val rev_mp: thm
- val select_equality: thm
- val spec: thm
- val sstac: thm list -> int -> tactic
- val ssubst: thm
- val stac: thm -> int -> tactic
- val strip_tac: int -> tactic
- val swap: thm
- val sym: thm
- val trans: thm
- val TrueI: thm
+ val case_tac : string -> int -> tactic
+ val ccontr : thm
+ val classical : thm
+ val cong : thm
+ val conjunct1 : thm
+ val conjunct2 : thm
+ val conjE : thm
+ val conjI : thm
+ val contrapos : thm
+ val disjCI : thm
+ val disjE : thm
+ val disjI1 : thm
+ val disjI2 : thm
+ val eqTrueI : thm
+ val eqTrueE : thm
+ val ex1E : thm
+ val ex1I : thm
+ val exCI : thm
+ val exI : thm
+ val exE : thm
+ val excluded_middle : thm
+ val excluded_middle_tac : string -> int -> tactic
+ val False_neq_True : thm
+ val FalseE : thm
+ val iffCE : thm
+ val iffD1 : thm
+ val iffD2 : thm
+ val iffE : thm
+ val iffI : thm
+ val impCE : thm
+ val impE : thm
+ val not_sym : thm
+ val notE : thm
+ val notI : thm
+ val notnotD : thm
+ val rev_mp : thm
+ val select_equality : thm
+ val spec : thm
+ val sstac : thm list -> int -> tactic
+ val ssubst : thm
+ val stac : thm -> int -> tactic
+ val strip_tac : int -> tactic
+ val swap : thm
+ val sym : thm
+ val trans : thm
+ val TrueI : thm
end;
structure HOL_Lemmas : HOL_LEMMAS =
@@ -287,6 +288,10 @@
val excluded_middle = prove_goal HOL.thy "~P | P"
(fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
+(*For disjunctive case analysis*)
+fun excluded_middle_tac sP =
+ res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
+
(*Classical implies (-->) elimination. *)
val impCE = prove_goal HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R"
(fn major::prems=>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Inductive.ML Thu Aug 25 11:01:45 1994 +0200
@@ -0,0 +1,141 @@
+(* 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
+*)
+
+local open Ind_Syntax
+in
+
+fun gen_fp_oper a (X,T,t) =
+ let val setT = mk_set T
+ in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t) end;
+
+structure Lfp_items =
+ struct
+ val oper = gen_fp_oper "lfp"
+ val Tarski = def_lfp_Tarski
+ val induct = def_induct
+ end;
+
+structure Gfp_items =
+ struct
+ val oper = gen_fp_oper "gfp"
+ val Tarski = def_gfp_Tarski
+ val induct = def_Collect_coinduct
+ end;
+
+end;
+
+
+functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end)
+ : sig include INTR_ELIM INDRULE end =
+struct
+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);
+
+open Intr_elim Indrule
+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;
+
+
+(*For upwards compatibility: can be called 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)
+ |> add_thyname 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);
+
+
+
+(*For installing the theory section. co is either "" or "Co"*)
+fun inductive_decl co =
+ let open ThyParse Ind_Syntax
+ fun mk_intr_name (s,_) = (*the "op" cancels any infix status*)
+ if Syntax.is_identifier s then "op " ^ s else "_"
+ fun mk_params (((recs, ipairs), monos), con_defs) =
+ let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
+ and srec_tms = mk_list recs
+ and sintrs = mk_big_list (map snd ipairs)
+ val stri_name = big_rec_name ^ "_Intrnl"
+ in
+ (";\n\n\
+ \structure " ^ stri_name ^ " =\n\
+ \ let open Ind_Syntax in\n\
+ \ struct\n\
+ \ val _ = writeln \"" ^ co ^
+ "Inductive definition " ^ big_rec_name ^ "\"\n\
+ \ val rec_tms\t= map (readtm (sign_of thy) termTVar) "
+ ^ srec_tms ^ "\n\
+ \ and intr_tms\t= map (readtm (sign_of thy) propT)\n"
+ ^ sintrs ^ "\n\
+ \ end\n\
+ \ end;\n\n\
+ \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^
+ stri_name ^ ".rec_tms, " ^
+ stri_name ^ ".intr_tms)"
+ ,
+ "structure " ^ big_rec_name ^ " =\n\
+ \ struct\n\
+ \ structure Result = " ^ co ^ "Ind_section_Fun\n\
+ \ (open " ^ stri_name ^ "\n\
+ \ val thy\t\t= thy\n\
+ \ val monos\t\t= " ^ monos ^ "\n\
+ \ val con_defs\t\t= " ^ con_defs ^ ");\n\n\
+ \ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
+ \ open Result\n\
+ \ end\n"
+ )
+ end
+ val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
+ fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
+ in repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs"
+ >> mk_params
+ end;
--- a/LList.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/LList.ML Thu Aug 25 11:01:45 1994 +0200
@@ -3,11 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-For llist.thy.
-
SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
-
-TOO LONG! needs splitting up
*)
open LList;
@@ -23,55 +19,46 @@
delsimps [Pair_eq];
-(** the llist functional **)
-
-val LList_unfold = rewrite_rule [List_Fun_def]
- (List_Fun_mono RS (LList_def RS def_gfp_Tarski));
+(*This justifies using llist in other recursive type definitions*)
+goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
+by (rtac gfp_mono 1);
+by (REPEAT (ares_tac basic_monos 1));
+val llist_mono = result();
-(*This justifies using LList in other recursive type definitions*)
-goalw LList.thy [LList_def] "!!A B. A<=B ==> LList(A) <= LList(B)";
-by (rtac gfp_mono 1);
-by (etac List_Fun_mono2 1);
-val LList_mono = result();
-(*Elimination is case analysis, not induction.*)
-val [major,prem1,prem2] = goalw LList.thy [NIL_def,CONS_def]
- "[| L : LList(A); \
-\ L=NIL ==> P; \
-\ !!M N. [| M:A; N: LList(A); L=CONS(M,N) |] ==> P \
-\ |] ==> P";
-by (rtac (major RS (LList_unfold RS equalityD1 RS subsetD RS usumE)) 1);
-by (etac uprodE 2);
-by (rtac prem2 2);
-by (rtac prem1 1);
-by (REPEAT (ares_tac [refl] 1
- ORELSE eresolve_tac [singletonE,ssubst] 1));
-val LListE = result();
+goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
+let val rew = rewrite_rule [NIL_def, CONS_def] in
+by (fast_tac (univ_cs addSIs (equalityI :: map rew llist.intrs)
+ addEs [rew llist.elim]) 1)
+end;
+val llist_unfold = result();
-(*** Type checking by co-induction, using List_Fun ***)
-
-val prems = goalw LList.thy [LList_def]
- "[| M : X; X <= List_Fun(A, X Un LList(A)) |] ==> M : LList(A)";
-by (REPEAT (resolve_tac (prems@[List_Fun_mono RS coinduct]) 1));
-val LList_coinduct = result();
-
-(** Rules to prove the 2nd premise of LList_coinduct **)
+(*** Type checking by coinduction, using list_Fun
+ THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
+***)
-goalw LList.thy [List_Fun_def,NIL_def] "NIL: List_Fun(A,X)";
-by (resolve_tac [singletonI RS usum_In0I] 1);
-val List_Fun_NIL_I = result();
+goalw LList.thy [list_Fun_def]
+ "!!M. [| M : X; X <= list_Fun(A, X Un llist(A)) |] ==> M : llist(A)";
+be llist.coinduct 1;
+be (subsetD RS CollectD) 1;
+ba 1;
+val llist_coinduct = result();
-goalw LList.thy [List_Fun_def,CONS_def]
- "!!M N. [| M: A; N: X |] ==> CONS(M,N) : List_Fun(A,X)";
-by (REPEAT (ares_tac [uprodI RS usum_In1I] 1));
-val List_Fun_CONS_I = result();
+goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun(A,X)";
+by (fast_tac set_cs 1);
+val list_Fun_NIL_I = result();
+
+goalw LList.thy [list_Fun_def,CONS_def]
+ "!!M N. [| M: A; N: X |] ==> CONS(M,N) : list_Fun(A,X)";
+by (fast_tac set_cs 1);
+val list_Fun_CONS_I = result();
(*Utilise the "strong" part, i.e. gfp(f)*)
-goalw LList.thy [LList_def]
- "!!M N. M: LList(A) ==> M : List_Fun(A, X Un LList(A))";
-by (etac (List_Fun_mono RS gfp_fun_UnI2) 1);
-val List_Fun_LList_I = result();
+goalw LList.thy (llist.defs @ [list_Fun_def])
+ "!!M N. M: llist(A) ==> M : list_Fun(A, X Un llist(A))";
+by (etac (llist.mono RS gfp_fun_UnI2) 1);
+val list_Fun_llist_I = result();
(*** LList_corec satisfies the desired recurion equation ***)
@@ -137,119 +124,140 @@
(*A typical use of co-induction to show membership in the gfp.
Bisimulation is range(%x. LList_corec(x,f)) *)
-goal LList.thy "LList_corec(a,f) : LList({u.True})";
-by (res_inst_tac [("X", "range(%x.LList_corec(x,?g))")] LList_coinduct 1);
+goal LList.thy "LList_corec(a,f) : llist({u.True})";
+by (res_inst_tac [("X", "range(%x.LList_corec(x,?g))")] llist_coinduct 1);
by (rtac rangeI 1);
by (safe_tac set_cs);
by (stac LList_corec 1);
-by (simp_tac (llist_ss addsimps [List_Fun_NIL_I,List_Fun_CONS_I, CollectI]
+by (simp_tac (llist_ss addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
|> add_eqI) 1);
val LList_corec_type = result();
(*Lemma for the proof of llist_corec*)
goal LList.thy
"LList_corec(a, %z.sum_case(Inl, split(%v w.Inr(<Leaf(v),w>)), f(z))) : \
-\ LList(range(Leaf))";
-by (res_inst_tac [("X", "range(%x.LList_corec(x,?g))")] LList_coinduct 1);
+\ llist(range(Leaf))";
+by (res_inst_tac [("X", "range(%x.LList_corec(x,?g))")] llist_coinduct 1);
by (rtac rangeI 1);
by (safe_tac set_cs);
by (stac LList_corec 1);
-by (asm_simp_tac (llist_ss addsimps [List_Fun_NIL_I, Pair_eq]) 1);
-by (fast_tac (set_cs addSIs [List_Fun_CONS_I]) 1);
+by (asm_simp_tac (llist_ss addsimps [list_Fun_NIL_I]) 1);
+by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1);
val LList_corec_type2 = result();
-(**** LList equality as a gfp; the bisimulation principle ****)
+
+(**** llist equality as a gfp; the bisimulation principle ****)
-goalw LList.thy [LListD_Fun_def] "mono(LListD_Fun(r))";
-by (REPEAT (ares_tac [monoI, subset_refl, dsum_mono, dprod_mono] 1));
-val LListD_Fun_mono = result();
-
-val LListD_unfold = rewrite_rule [LListD_Fun_def]
- (LListD_Fun_mono RS (LListD_def RS def_gfp_Tarski));
+(*This theorem is actually used, unlike the many similar ones in ZF*)
+goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
+let val rew = rewrite_rule [NIL_def, CONS_def] in
+by (fast_tac (univ_cs addSIs (equalityI :: map rew LListD.intrs)
+ addEs [rew LListD.elim]) 1)
+end;
+val LListD_unfold = result();
goal LList.thy "!M N. <M,N> : LListD(diag(A)) --> ntrunc(k,M) = ntrunc(k,N)";
by (res_inst_tac [("n", "k")] less_induct 1);
by (safe_tac set_cs);
-by (etac (LListD_unfold RS equalityD1 RS subsetD RS dsumE) 1);
-by (safe_tac (set_cs addSEs [Pair_inject, dprodE, diagE]));
+by (etac LListD.elim 1);
+by (safe_tac (prod_cs addSEs [diagE]));
by (res_inst_tac [("n", "n")] natE 1);
by (asm_simp_tac (univ_ss addsimps [ntrunc_0]) 1);
-by (res_inst_tac [("n", "xb")] natE 1);
-by (asm_simp_tac (univ_ss addsimps [ntrunc_one_In1]) 1);
-by (asm_simp_tac (univ_ss addsimps [ntrunc_In1, ntrunc_Scons]) 1);
+by (rename_tac "n'" 1);
+by (res_inst_tac [("n", "n'")] natE 1);
+by (asm_simp_tac (univ_ss addsimps [CONS_def, ntrunc_one_In1]) 1);
+by (asm_simp_tac (univ_ss addsimps [CONS_def, ntrunc_In1, ntrunc_Scons]) 1);
val LListD_implies_ntrunc_equality = result();
-goalw LList.thy [LList_def,List_Fun_def] "fst``LListD(diag(A)) <= LList(A)";
+(*The domain of the LListD relation*)
+goalw LList.thy (llist.defs @ [NIL_def, CONS_def])
+ "fst``LListD(diag(A)) <= llist(A)";
by (rtac gfp_upperbound 1);
+(*avoids unfolding LListD on the rhs*)
by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1);
by (simp_tac fst_image_ss 1);
+by (fast_tac univ_cs 1);
val fst_image_LListD = result();
(*This inclusion justifies the use of coinduction to show M=N*)
-goal LList.thy "LListD(diag(A)) <= diag(LList(A))";
+goal LList.thy "LListD(diag(A)) <= diag(llist(A))";
by (rtac subsetI 1);
by (res_inst_tac [("p","x")] PairE 1);
by (safe_tac HOL_cs);
-by (res_inst_tac [("s","xa")] subst 1);
+by (rtac diag_eqI 1);
by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS
ntrunc_equality) 1);
by (assume_tac 1);
-by (rtac diagI 1);
by (etac (fst_imageI RS (fst_image_LListD RS subsetD)) 1);
val LListD_subset_diag = result();
-(*This converse inclusion helps to strengthen LList_equalityI*)
-goalw LList.thy [LListD_def] "diag(LList(A)) <= LListD(diag(A))";
-by (rtac gfp_upperbound 1);
+(** Coinduction, using LListD_Fun
+ THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
+ **)
+
+goalw LList.thy [LListD_Fun_def]
+ "!!M. [| M : X; X <= LListD_Fun(r, X Un LListD(r)) |] ==> M : LListD(r)";
+be LListD.coinduct 1;
+be (subsetD RS CollectD) 1;
+ba 1;
+val LListD_coinduct = result();
+
+goalw LList.thy [LListD_Fun_def,NIL_def] "<NIL,NIL> : LListD_Fun(r,s)";
+by (fast_tac set_cs 1);
+val LListD_Fun_NIL_I = result();
+
+goalw LList.thy [LListD_Fun_def,CONS_def]
+ "!!x. [| x:A; <M,N>:s |] ==> <CONS(x,M), CONS(x,N)> : LListD_Fun(diag(A),s)";
+by (fast_tac univ_cs 1);
+val LListD_Fun_CONS_I = result();
+
+(*Utilise the "strong" part, i.e. gfp(f)*)
+goalw LList.thy (LListD.defs @ [LListD_Fun_def])
+ "!!M N. M: LListD(r) ==> M : LListD_Fun(r, X Un LListD(r))";
+by (etac (LListD.mono RS gfp_fun_UnI2) 1);
+val LListD_Fun_LListD_I = result();
+
+
+(*This converse inclusion helps to strengthen llist_equalityI*)
+goal LList.thy "diag(llist(A)) <= LListD(diag(A))";
by (rtac subsetI 1);
-by (etac diagE 1);
-by (etac ssubst 1);
-by (etac (LList_unfold RS equalityD1 RS subsetD RS usumE) 1);
-by (rewtac LListD_Fun_def);
-by (ALLGOALS (fast_tac univ_cs));
+by (etac LListD_coinduct 1);
+by (rtac subsetI 1);
+by (eresolve_tac [diagE] 1);
+by (eresolve_tac [ssubst] 1);
+by (eresolve_tac [llist.elim] 1);
+by (ALLGOALS
+ (asm_simp_tac (llist_ss addsimps [diagI, LListD_Fun_NIL_I,
+ LListD_Fun_CONS_I])));
val diag_subset_LListD = result();
-goal LList.thy "LListD(diag(A)) = diag(LList(A))";
+goal LList.thy "LListD(diag(A)) = diag(llist(A))";
by (REPEAT (resolve_tac [equalityI, LListD_subset_diag,
diag_subset_LListD] 1));
val LListD_eq_diag = result();
+goal LList.thy
+ "!!M N. M: llist(A) ==> <M,M> : LListD_Fun(diag(A), X Un diag(llist(A)))";
+by (rtac (LListD_eq_diag RS subst) 1);
+br LListD_Fun_LListD_I 1;
+by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag, diagI]) 1);
+val LListD_Fun_diag_I = result();
+
+
(** To show two LLists are equal, exhibit a bisimulation!
[also admits true equality]
Replace "A" by some particular set, like {x.True}??? *)
goal LList.thy
- "!!r. [| <M,N> : r; r <= LListD_Fun(diag(A), r Un diag(LList(A))) \
+ "!!r. [| <M,N> : r; r <= LListD_Fun(diag(A), r Un diag(llist(A))) \
\ |] ==> M=N";
-by (rtac (rewrite_rule [LListD_def]
- (LListD_subset_diag RS subsetD RS diagE)) 1);
-by (etac (LListD_Fun_mono RS coinduct) 1);
-by (etac (rewrite_rule [LListD_def] LListD_eq_diag RS ssubst) 1);
-by (safe_tac univ_cs);
-val LList_equalityI = result();
-
-(** Rules to prove the 2nd premise of LList_equalityI **)
-
-goalw LList.thy [LListD_Fun_def,NIL_def] "<NIL,NIL> : LListD_Fun(r,s)";
-by (rtac (singletonI RS diagI RS dsum_In0I) 1);
-val LListD_Fun_NIL_I = result();
-
-val prems = goalw LList.thy [LListD_Fun_def,CONS_def]
- "[| x:A; <M,N>:s |] ==> <CONS(x,M), CONS(x,N)> : LListD_Fun(diag(A),s)";
-by (rtac (dprodI RS dsum_In1I) 1);
-by (REPEAT (resolve_tac (diagI::prems) 1));
-val LListD_Fun_CONS_I = result();
-
-(*Utilise the "strong" part, i.e. gfp(f)*)
-goal LList.thy
- "!!M N. M: LList(A) ==> <M,M> : LListD_Fun(diag(A), X Un diag(LList(A)))";
-br (rewrite_rule [LListD_def] LListD_eq_diag RS subst) 1;
-br (LListD_Fun_mono RS gfp_fun_UnI2) 1;
-br (rewrite_rule [LListD_def] LListD_eq_diag RS ssubst) 1;
-be diagI 1;
-val LListD_Fun_diag_I = result();
+by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
+by (etac LListD_coinduct 1);
+by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag]) 1);
+by (safe_tac prod_cs);
+val llist_equalityI = result();
-(*** Finality of LList(A): Uniqueness of functions defined by corecursion ***)
+(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
(*abstract proof using a bisimulation*)
val [prem1,prem2] = goal LList.thy
@@ -259,7 +267,7 @@
by (rtac ext 1);
(*next step avoids an unknown (and flexflex pair) in simplification*)
by (res_inst_tac [("A", "{u.True}"),
- ("r", "range(%u. <h1(u),h2(u)>)")] LList_equalityI 1);
+ ("r", "range(%u. <h1(u),h2(u)>)")] llist_equalityI 1);
by (rtac rangeI 1);
by (safe_tac set_cs);
by (stac prem1 1);
@@ -317,11 +325,11 @@
(*A typical use of co-induction to show membership in the gfp.
The containing set is simply the singleton {Lconst(M)}. *)
-goal LList.thy "!!M A. M:A ==> Lconst(M): LList(A)";
-by (rtac (singletonI RS LList_coinduct) 1);
+goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)";
+by (rtac (singletonI RS llist_coinduct) 1);
by (safe_tac set_cs);
by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
-by (REPEAT (ares_tac [List_Fun_CONS_I, singletonI, UnI1] 1));
+by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
val Lconst_type = result();
goal LList.thy "Lconst(M) = LList_corec(M, %x.Inr(<x,x>))";
@@ -338,39 +346,23 @@
val gfp_Lconst_eq_LList_corec = result();
-(** Introduction rules for LList constructors **)
-
-(* c : {Numb(0)} <+> A <*> LList(A) ==> c : LList(A) *)
-val LListI = LList_unfold RS equalityD2 RS subsetD;
-
-(*This justifies the type definition: LList(A) is nonempty.*)
-goalw LList.thy [NIL_def] "NIL: LList(A)";
-by (rtac (singletonI RS usum_In0I RS LListI) 1);
-val NIL_LListI = result();
-
-val prems = goalw LList.thy [CONS_def]
- "[| M: A; N: LList(A) |] ==> CONS(M,N) : LList(A)";
-by (rtac (uprodI RS usum_In1I RS LListI) 1);
-by (REPEAT (resolve_tac prems 1));
-val CONS_LListI = result();
-
(*** Isomorphisms ***)
-goal LList.thy "inj(Rep_LList)";
+goal LList.thy "inj(Rep_llist)";
by (rtac inj_inverseI 1);
-by (rtac Rep_LList_inverse 1);
-val inj_Rep_LList = result();
+by (rtac Rep_llist_inverse 1);
+val inj_Rep_llist = result();
-goal LList.thy "inj_onto(Abs_LList,LList(range(Leaf)))";
+goal LList.thy "inj_onto(Abs_llist,llist(range(Leaf)))";
by (rtac inj_onto_inverseI 1);
-by (etac Abs_LList_inverse 1);
-val inj_onto_Abs_LList = result();
+by (etac Abs_llist_inverse 1);
+val inj_onto_Abs_llist = result();
(** Distinctness of constructors **)
goalw LList.thy [LNil_def,LCons_def] "~ LCons(x,xs) = LNil";
-by (rtac (CONS_not_NIL RS (inj_onto_Abs_LList RS inj_onto_contraD)) 1);
-by (REPEAT (resolve_tac [rangeI, NIL_LListI, CONS_LListI, Rep_LList] 1));
+by (rtac (CONS_not_NIL RS (inj_onto_Abs_llist RS inj_onto_contraD)) 1);
+by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
val LCons_not_LNil = result();
val LNil_not_LCons = standard (LCons_not_LNil RS not_sym);
@@ -381,15 +373,15 @@
(** llist constructors **)
goalw LList.thy [LNil_def]
- "Rep_LList(LNil) = NIL";
-by (rtac (NIL_LListI RS Abs_LList_inverse) 1);
-val Rep_LList_LNil = result();
+ "Rep_llist(LNil) = NIL";
+by (rtac (llist.NIL_I RS Abs_llist_inverse) 1);
+val Rep_llist_LNil = result();
goalw LList.thy [LCons_def]
- "Rep_LList(LCons(x,l)) = CONS(Leaf(x),Rep_LList(l))";
-by (REPEAT (resolve_tac [CONS_LListI RS Abs_LList_inverse,
- rangeI, Rep_LList] 1));
-val Rep_LList_LCons = result();
+ "Rep_llist(LCons(x,l)) = CONS(Leaf(x),Rep_llist(l))";
+by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse,
+ rangeI, Rep_llist] 1));
+val Rep_llist_LCons = result();
(** Injectiveness of CONS and LCons **)
@@ -401,49 +393,49 @@
(*For reasoning about abstract llist constructors*)
-val LList_cs = set_cs addIs [Rep_LList, NIL_LListI, CONS_LListI]
+val llist_cs = set_cs addIs [Rep_llist]@llist.intrs
addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject]
- addSDs [inj_onto_Abs_LList RS inj_ontoD,
- inj_Rep_LList RS injD, Leaf_inject];
+ addSDs [inj_onto_Abs_llist RS inj_ontoD,
+ inj_Rep_llist RS injD, Leaf_inject];
goalw LList.thy [LCons_def] "(LCons(x,xs)=LCons(y,ys)) = (x=y & xs=ys)";
-by (fast_tac LList_cs 1);
+by (fast_tac llist_cs 1);
val LCons_LCons_eq = result();
val LCons_inject = standard (LCons_LCons_eq RS iffD1 RS conjE);
-val [major] = goal LList.thy "CONS(M,N): LList(A) ==> M: A & N: LList(A)";
-by (rtac (major RS LListE) 1);
+val [major] = goal LList.thy "CONS(M,N): llist(A) ==> M: A & N: llist(A)";
+by (rtac (major RS llist.elim) 1);
by (etac CONS_neq_NIL 1);
-by (fast_tac LList_cs 1);
+by (fast_tac llist_cs 1);
val CONS_D = result();
-(****** Reasoning about LList(A) ******)
+(****** Reasoning about llist(A) ******)
(*Don't use llist_ss, as it does case splits!*)
val List_case_ss = univ_ss addsimps [List_case_NIL, List_case_CONS];
(*A special case of list_equality for functions over lazy lists*)
-val [MList,gMList,NILcase,CONScase] = goal LList.thy
- "[| M: LList(A); g(NIL): LList(A); \
+val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy
+ "[| M: llist(A); g(NIL): llist(A); \
\ f(NIL)=g(NIL); \
-\ !!x l. [| x:A; l: LList(A) |] ==> \
+\ !!x l. [| x:A; l: llist(A) |] ==> \
\ <f(CONS(x,l)),g(CONS(x,l))> : \
-\ LListD_Fun(diag(A), (%u.<f(u),g(u)>)``LList(A) Un \
-\ diag(LList(A))) \
+\ LListD_Fun(diag(A), (%u.<f(u),g(u)>)``llist(A) Un \
+\ diag(llist(A))) \
\ |] ==> f(M) = g(M)";
-by (rtac LList_equalityI 1);
-br (MList RS imageI) 1;
+by (rtac llist_equalityI 1);
+br (Mlist RS imageI) 1;
by (rtac subsetI 1);
by (etac imageE 1);
by (etac ssubst 1);
-by (etac LListE 1);
+by (etac llist.elim 1);
by (etac ssubst 1);
by (stac NILcase 1);
-br (gMList RS LListD_Fun_diag_I) 1;
+br (gMlist RS LListD_Fun_diag_I) 1;
by (etac ssubst 1);
by (REPEAT (ares_tac [CONScase] 1));
-val LList_fun_equalityI = result();
+val llist_fun_equalityI = result();
(*** The functional "Lmap" ***)
@@ -460,17 +452,17 @@
(*Another type-checking proof by coinduction*)
val [major,minor] = goal LList.thy
- "[| M: LList(A); !!x. x:A ==> f(x):B |] ==> Lmap(f,M): LList(B)";
-by (rtac (major RS imageI RS LList_coinduct) 1);
+ "[| M: llist(A); !!x. x:A ==> f(x):B |] ==> Lmap(f,M): llist(B)";
+by (rtac (major RS imageI RS llist_coinduct) 1);
by (safe_tac set_cs);
-by (etac LListE 1);
+by (etac llist.elim 1);
by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS])));
-by (REPEAT (ares_tac [List_Fun_NIL_I, List_Fun_CONS_I,
+by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I,
minor, imageI, UnI1] 1));
val Lmap_type = result();
(*This type checking rule synthesises a sufficiently large set for f*)
-val [major] = goal LList.thy "M: LList(A) ==> Lmap(f,M): LList(f``A)";
+val [major] = goal LList.thy "M: llist(A) ==> Lmap(f,M): llist(f``A)";
by (rtac (major RS Lmap_type) 1);
by (etac imageI 1);
val Lmap_type2 = result();
@@ -478,19 +470,19 @@
(** Two easy results about Lmap **)
val [prem] = goalw LList.thy [o_def]
- "M: LList(A) ==> Lmap(f o g, M) = Lmap(f, Lmap(g, M))";
-by (rtac (prem RS imageI RS LList_equalityI) 1);
+ "M: llist(A) ==> Lmap(f o g, M) = Lmap(f, Lmap(g, M))";
+by (rtac (prem RS imageI RS llist_equalityI) 1);
by (safe_tac set_cs);
-by (etac LListE 1);
+by (etac llist.elim 1);
by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS])));
by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
rangeI RS LListD_Fun_CONS_I] 1));
val Lmap_compose = result();
-val [prem] = goal LList.thy "M: LList(A) ==> Lmap(%x.x, M) = M";
-by (rtac (prem RS imageI RS LList_equalityI) 1);
+val [prem] = goal LList.thy "M: llist(A) ==> Lmap(%x.x, M) = M";
+by (rtac (prem RS imageI RS llist_equalityI) 1);
by (safe_tac set_cs);
-by (etac LListE 1);
+by (etac llist.elim 1);
by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS])));
by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
rangeI RS LListD_Fun_CONS_I] 1));
@@ -517,17 +509,17 @@
val Lappend_CONS = result();
val Lappend_ss =
- List_case_ss addsimps [NIL_LListI, Lappend_NIL_NIL, Lappend_NIL_CONS,
+ List_case_ss addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS,
Lappend_CONS, LListD_Fun_CONS_I]
|> add_eqI;
-goal LList.thy "!!M. M: LList(A) ==> Lappend(NIL,M) = M";
-by (etac LList_fun_equalityI 1);
+goal LList.thy "!!M. M: llist(A) ==> Lappend(NIL,M) = M";
+by (etac llist_fun_equalityI 1);
by (ALLGOALS (asm_simp_tac Lappend_ss));
val Lappend_NIL = result();
-goal LList.thy "!!M. M: LList(A) ==> Lappend(M,NIL) = M";
-by (etac LList_fun_equalityI 1);
+goal LList.thy "!!M. M: llist(A) ==> Lappend(M,NIL) = M";
+by (etac llist_fun_equalityI 1);
by (ALLGOALS (asm_simp_tac Lappend_ss));
val Lappend_NIL2 = result();
@@ -535,62 +527,63 @@
(*weak co-induction: bisimulation and case analysis on both variables*)
goal LList.thy
- "!!M N. [| M: LList(A); N: LList(A) |] ==> Lappend(M,N): LList(A)";
+ "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend(M,N): llist(A)";
by (res_inst_tac
- [("X", "UN u:LList(A). UN v: LList(A). {Lappend(u,v)}")] LList_coinduct 1);
+ [("X", "UN u:llist(A). UN v: llist(A). {Lappend(u,v)}")] llist_coinduct 1);
by (fast_tac set_cs 1);
by (safe_tac set_cs);
-by (eres_inst_tac [("L", "u")] LListE 1);
-by (eres_inst_tac [("L", "v")] LListE 1);
+by (eres_inst_tac [("a", "u")] llist.elim 1);
+by (eres_inst_tac [("a", "v")] llist.elim 1);
by (ALLGOALS
(asm_simp_tac Lappend_ss THEN'
- fast_tac (set_cs addSIs [NIL_LListI,List_Fun_NIL_I,List_Fun_CONS_I]) ));
+ fast_tac (set_cs addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
val Lappend_type = result();
(*strong co-induction: bisimulation and case analysis on one variable*)
goal LList.thy
- "!!M N. [| M: LList(A); N: LList(A) |] ==> Lappend(M,N): LList(A)";
-by (res_inst_tac [("X", "(%u.Lappend(u,N))``LList(A)")] LList_coinduct 1);
+ "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend(M,N): llist(A)";
+by (res_inst_tac [("X", "(%u.Lappend(u,N))``llist(A)")] llist_coinduct 1);
be imageI 1;
br subsetI 1;
be imageE 1;
-by (eres_inst_tac [("L", "u")] LListE 1);
-by (asm_simp_tac (Lappend_ss addsimps [Lappend_NIL, List_Fun_LList_I]) 1);
+by (eres_inst_tac [("a", "u")] llist.elim 1);
+by (asm_simp_tac (Lappend_ss addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
by (asm_simp_tac Lappend_ss 1);
-by (fast_tac (set_cs addSIs [List_Fun_CONS_I]) 1);
+by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1);
val Lappend_type = result();
(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
(** llist_case: case analysis for 'a llist **)
-val Rep_LList_simps =
+val Rep_llist_simps =
[List_case_NIL, List_case_CONS,
- Abs_LList_inverse, Rep_LList_inverse, NIL_LListI, CONS_LListI,
- Rep_LList, rangeI, inj_Leaf, Inv_f_f];
-val Rep_LList_ss = llist_ss addsimps Rep_LList_simps;
+ Abs_llist_inverse, Rep_llist_inverse,
+ Rep_llist, rangeI, inj_Leaf, Inv_f_f]
+ @ llist.intrs;
+val Rep_llist_ss = llist_ss addsimps Rep_llist_simps;
goalw LList.thy [llist_case_def,LNil_def] "llist_case(c, d, LNil) = c";
-by (simp_tac Rep_LList_ss 1);
+by (simp_tac Rep_llist_ss 1);
val llist_case_LNil = result();
goalw LList.thy [llist_case_def,LCons_def]
"llist_case(c, d, LCons(M,N)) = d(M,N)";
-by (simp_tac Rep_LList_ss 1);
+by (simp_tac Rep_llist_ss 1);
val llist_case_LCons = result();
(*Elimination is case analysis, not induction.*)
val [prem1,prem2] = goalw LList.thy [NIL_def,CONS_def]
"[| l=LNil ==> P; !!x l'. l=LCons(x,l') ==> P \
\ |] ==> P";
-by (rtac (Rep_LList RS LListE) 1);
-by (rtac (inj_Rep_LList RS injD RS prem1) 1);
-by (stac Rep_LList_LNil 1);
+by (rtac (Rep_llist RS llist.elim) 1);
+by (rtac (inj_Rep_llist RS injD RS prem1) 1);
+by (stac Rep_llist_LNil 1);
by (assume_tac 1);
by (etac rangeE 1);
-by (rtac (inj_Rep_LList RS injD RS prem2) 1);
-by (asm_simp_tac (HOL_ss addsimps [Rep_LList_LCons]) 1);
-by (etac (Abs_LList_inverse RS ssubst) 1);
+by (rtac (inj_Rep_llist RS injD RS prem2) 1);
+by (asm_simp_tac (HOL_ss addsimps [Rep_llist_LCons]) 1);
+by (etac (Abs_llist_inverse RS ssubst) 1);
by (rtac refl 1);
val llistE = result();
@@ -601,11 +594,11 @@
\ split(%z w. LCons(z, llist_corec(w,f))), f(a))";
by (stac LList_corec 1);
by (res_inst_tac [("s","f(a)")] sumE 1);
-by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_LList_inverse]) 1);
+by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1);
by (res_inst_tac [("p","y")] PairE 1);
-by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_LList_inverse]) 1);
+by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1);
(*FIXME: correct case splits usd to be found automatically:
-by (ASM_SIMP_TAC(llist_ss addsimps [LList_corec_type2,Abs_LList_inverse]) 1);*)
+by (ASM_SIMP_TAC(llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1);*)
val llist_corec = result();
(*definitional version of same*)
@@ -620,53 +613,53 @@
(*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
-val prems = goalw LList.thy [LListD_Fun_def]
- "r <= Sigma(LList(A), %x.LList(A)) ==> \
-\ LListD_Fun(diag(A),r) <= Sigma(LList(A), %x.LList(A))";
-by (stac LList_unfold 1);
-by (cut_facts_tac prems 1);
+goalw LList.thy [LListD_Fun_def]
+ "!!r A. r <= Sigma(llist(A), %x.llist(A)) ==> \
+\ LListD_Fun(diag(A),r) <= Sigma(llist(A), %x.llist(A))";
+by (stac llist_unfold 1);
+by (simp_tac (HOL_ss addsimps [NIL_def, CONS_def]) 1);
by (fast_tac univ_cs 1);
-val LListD_Fun_subset_Sigma_LList = result();
+val LListD_Fun_subset_Sigma_llist = result();
goal LList.thy
- "prod_fun(Rep_LList,Rep_LList) `` r <= \
-\ Sigma(LList(range(Leaf)), %x.LList(range(Leaf)))";
-by (fast_tac (prod_cs addIs [Rep_LList]) 1);
-val subset_Sigma_LList = result();
+ "prod_fun(Rep_llist,Rep_llist) `` r <= \
+\ Sigma(llist(range(Leaf)), %x.llist(range(Leaf)))";
+by (fast_tac (prod_cs addIs [Rep_llist]) 1);
+val subset_Sigma_llist = result();
val [prem] = goal LList.thy
- "r <= Sigma(LList(range(Leaf)), %x.LList(range(Leaf))) ==> \
-\ prod_fun(Rep_LList o Abs_LList, Rep_LList o Abs_LList) `` r <= r";
+ "r <= Sigma(llist(range(Leaf)), %x.llist(range(Leaf))) ==> \
+\ prod_fun(Rep_llist o Abs_llist, Rep_llist o Abs_llist) `` r <= r";
by (safe_tac prod_cs);
by (rtac (prem RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
-by (asm_simp_tac (HOL_ss addsimps [o_def,prod_fun,Abs_LList_inverse]) 1);
+by (asm_simp_tac (HOL_ss addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
val prod_fun_lemma = result();
goal LList.thy
- "prod_fun(Rep_LList, Rep_LList) `` range(%x. <x, x>) = \
-\ diag(LList(range(Leaf)))";
+ "prod_fun(Rep_llist, Rep_llist) `` range(%x. <x, x>) = \
+\ diag(llist(range(Leaf)))";
br equalityI 1;
-by (fast_tac (univ_cs addIs [Rep_LList]) 1);
-by (fast_tac (univ_cs addSEs [Abs_LList_inverse RS subst]) 1);
+by (fast_tac (univ_cs addIs [Rep_llist]) 1);
+by (fast_tac (univ_cs addSEs [Abs_llist_inverse RS subst]) 1);
val prod_fun_range_eq_diag = result();
(** To show two llists are equal, exhibit a bisimulation!
[also admits true equality] **)
val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]
"[| <l1,l2> : r; r <= llistD_Fun(r Un range(%x.<x,x>)) |] ==> l1=l2";
-by (rtac (inj_Rep_LList RS injD) 1);
-by (res_inst_tac [("r", "prod_fun(Rep_LList,Rep_LList)``r"),
+by (rtac (inj_Rep_llist RS injD) 1);
+by (res_inst_tac [("r", "prod_fun(Rep_llist,Rep_llist)``r"),
("A", "range(Leaf)")]
- LList_equalityI 1);
+ llist_equalityI 1);
by (rtac (prem1 RS prod_fun_imageI) 1);
by (rtac (prem2 RS image_mono RS subset_trans) 1);
by (rtac (image_compose RS subst) 1);
by (rtac (prod_fun_compose RS subst) 1);
by (rtac (image_Un RS ssubst) 1);
by (stac prod_fun_range_eq_diag 1);
-by (rtac (LListD_Fun_subset_Sigma_LList RS prod_fun_lemma) 1);
-by (rtac (subset_Sigma_LList RS Un_least) 1);
+by (rtac (LListD_Fun_subset_Sigma_llist RS prod_fun_lemma) 1);
+by (rtac (subset_Sigma_llist RS Un_least) 1);
by (rtac diag_subset_Sigma 1);
val llist_equalityI = result();
@@ -684,11 +677,11 @@
(*Utilise the "strong" part, i.e. gfp(f)*)
goalw LList.thy [llistD_Fun_def]
"!!l. <l,l> : llistD_Fun(r Un range(%x.<x,x>))";
-br (Rep_LList_inverse RS subst) 1;
+br (Rep_llist_inverse RS subst) 1;
br prod_fun_imageI 1;
by (rtac (image_Un RS ssubst) 1);
by (stac prod_fun_range_eq_diag 1);
-br (Rep_LList RS LListD_Fun_diag_I) 1;
+br (Rep_llist RS LListD_Fun_diag_I) 1;
val llistD_Fun_range_I = result();
(*A special case of list_equality for functions over lazy lists*)
--- a/LList.thy Thu Aug 25 10:47:33 1994 +0200
+++ b/LList.thy Thu Aug 25 11:01:45 1994 +0200
@@ -1,11 +1,11 @@
-(* Title: HOL/llist.thy
+(* Title: HOL/LList.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
+ Copyright 1994 University of Cambridge
Definition of type 'a llist by a greatest fixed point
-Shares NIL, CONS, List_Fun, List_case with list.thy
+Shares NIL, CONS, List_case with List.thy
Still needs filter and flatten functions -- hard because they need
bounds on the amount of lookahead required.
@@ -32,50 +32,64 @@
llist :: (term)term
consts
- LList :: "'a node set set => 'a node set set"
+ list_Fun :: "['a item set, 'a item set] => 'a item set"
LListD_Fun ::
- "[('a node set * 'a node set)set, ('a node set * 'a node set)set] => \
-\ ('a node set * 'a node set)set"
- LListD ::
- "('a node set * 'a node set)set => ('a node set * 'a node set)set"
+ "[('a item * 'a item)set, ('a item * 'a item)set] => \
+\ ('a item * 'a item)set"
+
+ llist :: "'a item set => 'a item set"
+ LListD :: "('a item * 'a item)set => ('a item * 'a item)set"
llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
- Rep_LList :: "'a llist => 'a node set"
- Abs_LList :: "'a node set => 'a llist"
+ Rep_llist :: "'a llist => 'a item"
+ Abs_llist :: "'a item => 'a llist"
LNil :: "'a llist"
LCons :: "['a, 'a llist] => 'a llist"
llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
- LList_corec_fun :: "[nat, 'a=>unit+('b node set * 'a), 'a] => 'b node set"
- LList_corec :: "['a, 'a => unit + ('b node set * 'a)] => 'b node set"
+ LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
+ LList_corec :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
llist_corec :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
- Lmap :: "('a node set => 'b node set) => ('a node set => 'b node set)"
+ Lmap :: "('a item => 'b item) => ('a item => 'b item)"
lmap :: "('a=>'b) => ('a llist => 'b llist)"
iterates :: "['a => 'a, 'a] => 'a llist"
- Lconst :: "'a node set => 'a node set"
- Lappend :: "['a node set, 'a node set] => 'a node set"
+ Lconst :: "'a item => 'a item"
+ Lappend :: "['a item, 'a item] => 'a item"
lappend :: "['a llist, 'a llist] => 'a llist"
-rules
- LListD_Fun_def "LListD_Fun(r) == (%Z.diag({Numb(0)}) <++> r <**> Z)"
- LList_def "LList(A) == gfp(List_Fun(A))"
- LListD_def "LListD(r) == gfp(LListD_Fun(r))"
- (*faking a type definition...*)
- Rep_LList "Rep_LList(xs): LList(range(Leaf))"
- Rep_LList_inverse "Abs_LList(Rep_LList(xs)) = xs"
- Abs_LList_inverse "M: LList(range(Leaf)) ==> Rep_LList(Abs_LList(M)) = M"
- (*defining the abstract constructors*)
- LNil_def "LNil == Abs_LList(NIL)"
- LCons_def "LCons(x,xs) == Abs_LList(CONS(Leaf(x), Rep_LList(xs)))"
+coinductive "llist(A)"
+ intrs
+ NIL_I "NIL: llist(A)"
+ CONS_I "[| a: A; M: llist(A) |] ==> CONS(a,M) : llist(A)"
+
+coinductive "LListD(r)"
+ intrs
+ NIL_I "<NIL, NIL> : LListD(r)"
+ CONS_I "[| <a,b>: r; <M,N> : LListD(r) \
+\ |] ==> <CONS(a,M), CONS(b,N)> : LListD(r)"
+
+defs
+ (*Now used exclusively for abbreviating the coinduction rule*)
+ list_Fun_def "list_Fun(A,X) == \
+\ {z. z = NIL | (? M a. z = CONS(a, M) & a : A & M : X)}"
+
+ LListD_Fun_def "LListD_Fun(r,X) == \
+\ {z. z = <NIL, NIL> | \
+\ (? M N a b. z = <CONS(a, M), CONS(b, N)> & \
+\ <a, b> : r & <M, N> : X)}"
+
+ (*defining the abstract constructors*)
+ LNil_def "LNil == Abs_llist(NIL)"
+ LCons_def "LCons(x,xs) == Abs_llist(CONS(Leaf(x), Rep_llist(xs)))"
llist_case_def
"llist_case(c,d,l) == \
-\ List_case(c, %x y. d(Inv(Leaf,x), Abs_LList(y)), Rep_LList(l))"
+\ List_case(c, %x y. d(Inv(Leaf,x), Abs_llist(y)), Rep_llist(l))"
LList_corec_fun_def
"LList_corec_fun(k,f) == \
@@ -87,14 +101,14 @@
llist_corec_def
"llist_corec(a,f) == \
-\ Abs_LList(LList_corec(a, %z.sum_case(%x.Inl(x), \
+\ Abs_llist(LList_corec(a, %z.sum_case(%x.Inl(x), \
\ split(%v w. Inr(<Leaf(v), w>)), f(z))))"
llistD_Fun_def
"llistD_Fun(r) == \
-\ prod_fun(Abs_LList,Abs_LList) `` \
+\ prod_fun(Abs_llist,Abs_llist) `` \
\ LListD_Fun(diag(range(Leaf)), \
-\ prod_fun(Rep_LList,Rep_LList) `` r)"
+\ prod_fun(Rep_llist,Rep_llist) `` r)"
Lconst_def "Lconst(M) == lfp(%N. CONS(M, N))"
@@ -122,4 +136,10 @@
\ split(llist_case(llist_case(Inl(Unity), %n1 n2. Inr(<n1, <LNil,n2>>)), \
\ %l1 l2 n. Inr(<l1, <l2,n>>))))"
+rules
+ (*faking a type definition...*)
+ Rep_llist "Rep_llist(xs): llist(range(Leaf))"
+ Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
+ Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
+
end
--- a/Lfp.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Lfp.ML Thu Aug 25 11:01:45 1994 +0200
@@ -60,7 +60,7 @@
val def_lfp_Tarski = result();
val rew::prems = goal Lfp.thy
- "[| A == lfp(f); a:A; mono(f); \
+ "[| A == lfp(f); mono(f); a:A; \
\ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \
\ |] ==> P(a)";
by (EVERY1 [rtac induct, (*backtracking to force correct induction*)
--- a/List.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/List.ML Thu Aug 25 11:01:45 1994 +0200
@@ -3,60 +3,43 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-For List.thy.
+Definition of type 'a list by a least fixed point
*)
open List;
-(** the list functional **)
-
-goalw List.thy [List_Fun_def] "mono(List_Fun(A))";
-by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono] 1));
-val List_Fun_mono = result();
+val list_con_defs = [NIL_def, CONS_def];
-goalw List.thy [List_Fun_def]
- "!!A B. A<=B ==> List_Fun(A,Z) <= List_Fun(B,Z)";
-by (REPEAT (ares_tac [subset_refl, usum_mono, uprod_mono] 1));
-val List_Fun_mono2 = result();
-
-(*This justifies using List in other recursive type definitions*)
-goalw List.thy [List_def] "!!A B. A<=B ==> List(A) <= List(B)";
-by (rtac lfp_mono 1);
-by (etac List_Fun_mono2 1);
-val List_mono = result();
-
-(** Type checking rules -- List creates well-founded sets **)
+goal List.thy "list(A) = {Numb(0)} <+> (A <*> list(A))";
+let val rew = rewrite_rule list_con_defs in
+by (fast_tac (univ_cs addSIs (equalityI :: map rew list.intrs)
+ addEs [rew list.elim]) 1)
+end;
+val list_unfold = result();
-val prems = goalw List.thy [List_def,List_Fun_def] "List(Sexp) <= Sexp";
-by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs [Sexp_NumbI,Sexp_In0I,Sexp_In1I,Sexp_SconsI]) 1);
-val List_Sexp = result();
-
-(* A <= Sexp ==> List(A) <= Sexp *)
-val List_subset_Sexp = standard
- (List_mono RS (List_Sexp RSN (2,subset_trans)));
-
-(** Induction **)
+(*This justifies using list in other recursive type definitions*)
+goalw List.thy list.defs "!!A B. A<=B ==> list(A) <= list(B)";
+by (rtac lfp_mono 1);
+by (REPEAT (ares_tac basic_monos 1));
+val list_mono = result();
-(*Induction for the set List(A) *)
-val major::prems = goalw List.thy [NIL_def,CONS_def]
- "[| M: List(A); P(NIL); \
-\ !!M N. [| M: A; N: List(A); P(N) |] ==> P(CONS(M,N)) |] \
-\ ==> P(M)";
-by (rtac (major RS (List_def RS def_induct)) 1);
-by (rtac List_Fun_mono 1);
-by (rewtac List_Fun_def);
-by (fast_tac (set_cs addIs prems addEs [usumE,uprodE]) 1);
-val List_induct = result();
+(*Type checking -- list creates well-founded sets*)
+goalw List.thy (list_con_defs @ list.defs) "list(sexp) <= sexp";
+by (rtac lfp_lowerbound 1);
+by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
+val list_sexp = result();
+
+(* A <= sexp ==> list(A) <= sexp *)
+val list_subset_sexp = standard ([list_mono, list_sexp] MRS subset_trans);
(*Induction for the type 'a list *)
val prems = goalw List.thy [Nil_def,Cons_def]
"[| P(Nil); \
\ !!x xs. P(xs) ==> P(x # xs) |] ==> P(l)";
-by (rtac (Rep_List_inverse RS subst) 1); (*types force good instantiation*)
-by (rtac (Rep_List RS List_induct) 1);
+by (rtac (Rep_list_inverse RS subst) 1); (*types force good instantiation*)
+by (rtac (Rep_list RS list.induct) 1);
by (REPEAT (ares_tac prems 1
- ORELSE eresolve_tac [rangeE, ssubst, Abs_List_inverse RS subst] 1));
+ ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1));
val list_induct = result();
(*Perform induction on xs. *)
@@ -64,39 +47,21 @@
EVERY [res_inst_tac [("l",a)] list_induct M,
rename_last_tac a ["1"] (M+1)];
-(** Introduction rules for List constructors **)
-
-val List_unfold = rewrite_rule [List_Fun_def]
- (List_Fun_mono RS (List_def RS def_lfp_Tarski));
-
-(* c : {Numb(0)} <+> A <*> List(A) ==> c : List(A) *)
-val ListI = List_unfold RS equalityD2 RS subsetD;
-
-(* NIL is a List -- this also justifies the type definition*)
-goalw List.thy [NIL_def] "NIL: List(A)";
-by (rtac (singletonI RS usum_In0I RS ListI) 1);
-val NIL_I = result();
-
-goalw List.thy [CONS_def]
- "!!a A M. [| a: A; M: List(A) |] ==> CONS(a,M) : List(A)";
-by (REPEAT (ares_tac [uprodI RS usum_In1I RS ListI] 1));
-val CONS_I = result();
-
(*** Isomorphisms ***)
-goal List.thy "inj(Rep_List)";
+goal List.thy "inj(Rep_list)";
by (rtac inj_inverseI 1);
-by (rtac Rep_List_inverse 1);
-val inj_Rep_List = result();
+by (rtac Rep_list_inverse 1);
+val inj_Rep_list = result();
-goal List.thy "inj_onto(Abs_List,List(range(Leaf)))";
+goal List.thy "inj_onto(Abs_list,list(range(Leaf)))";
by (rtac inj_onto_inverseI 1);
-by (etac Abs_List_inverse 1);
-val inj_onto_Abs_List = result();
+by (etac Abs_list_inverse 1);
+val inj_onto_Abs_list = result();
(** Distinctness of constructors **)
-goalw List.thy [NIL_def,CONS_def] "CONS(M,N) ~= NIL";
+goalw List.thy list_con_defs "CONS(M,N) ~= NIL";
by (rtac In1_not_In0 1);
val CONS_not_NIL = result();
val NIL_not_CONS = standard (CONS_not_NIL RS not_sym);
@@ -105,8 +70,8 @@
val NIL_neq_CONS = sym RS CONS_neq_NIL;
goalw List.thy [Nil_def,Cons_def] "x # xs ~= Nil";
-by (rtac (CONS_not_NIL RS (inj_onto_Abs_List RS inj_onto_contraD)) 1);
-by (REPEAT (resolve_tac [rangeI, NIL_I, CONS_I, Rep_List] 1));
+by (rtac (CONS_not_NIL RS (inj_onto_Abs_list RS inj_onto_contraD)) 1);
+by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
val Cons_not_Nil = result();
val Nil_not_Cons = standard (Cons_not_Nil RS not_sym);
@@ -123,37 +88,37 @@
val CONS_inject = standard (CONS_CONS_eq RS iffD1 RS conjE);
(*For reasoning about abstract list constructors*)
-val List_cs = set_cs addIs [Rep_List, NIL_I, CONS_I]
+val list_cs = set_cs addIs [Rep_list] @ list.intrs
addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject]
- addSDs [inj_onto_Abs_List RS inj_ontoD,
- inj_Rep_List RS injD, Leaf_inject];
+ addSDs [inj_onto_Abs_list RS inj_ontoD,
+ inj_Rep_list RS injD, Leaf_inject];
goalw List.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
-by (fast_tac List_cs 1);
+by (fast_tac list_cs 1);
val Cons_Cons_eq = result();
val Cons_inject = standard (Cons_Cons_eq RS iffD1 RS conjE);
-val [major] = goal List.thy "CONS(M,N): List(A) ==> M: A & N: List(A)";
+val [major] = goal List.thy "CONS(M,N): list(A) ==> M: A & N: list(A)";
by (rtac (major RS setup_induction) 1);
-by (etac List_induct 1);
-by (ALLGOALS (fast_tac List_cs));
+by (etac list.induct 1);
+by (ALLGOALS (fast_tac list_cs));
val CONS_D = result();
val prems = goalw List.thy [CONS_def,In1_def]
- "CONS(M,N): Sexp ==> M: Sexp & N: Sexp";
+ "CONS(M,N): sexp ==> M: sexp & N: sexp";
by (cut_facts_tac prems 1);
by (fast_tac (set_cs addSDs [Scons_D]) 1);
-val Sexp_CONS_D = result();
+val sexp_CONS_D = result();
(*Basic ss with constructors and their freeness*)
val list_free_simps = [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq,
- CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq,
- NIL_I, CONS_I];
+ CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq]
+ @ list.intrs;
val list_free_ss = HOL_ss addsimps list_free_simps;
-goal List.thy "!!N. N: List(A) ==> !M. N ~= CONS(M,N)";
-by (etac List_induct 1);
+goal List.thy "!!N. N: list(A) ==> !M. N ~= CONS(M,N)";
+by (etac list.induct 1);
by (ALLGOALS (asm_simp_tac list_free_ss));
val not_CONS_self = result();
@@ -180,34 +145,35 @@
by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1);
val List_case_CONS = result();
-(*** List_rec -- by wf recursion on pred_Sexp ***)
+(*** List_rec -- by wf recursion on pred_sexp ***)
+
+(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
+ hold if pred_sexp^+ were changed to pred_sexp. *)
-(* The trancl(pred_sexp) is essential because pred_Sexp_CONS_I1,2 would not
- hold if pred_Sexp^+ were changed to pred_Sexp. *)
+val List_rec_unfold = [List_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec
+ |> standard;
-val List_rec_unfold = wf_pred_Sexp RS wf_trancl RS (List_rec_def RS def_wfrec);
-
-(** pred_Sexp lemmas **)
+(** pred_sexp lemmas **)
goalw List.thy [CONS_def,In1_def]
- "!!M. [| M: Sexp; N: Sexp |] ==> <M, CONS(M,N)> : pred_Sexp^+";
-by (asm_simp_tac pred_Sexp_ss 1);
-val pred_Sexp_CONS_I1 = result();
+ "!!M. [| M: sexp; N: sexp |] ==> <M, CONS(M,N)> : pred_sexp^+";
+by (asm_simp_tac pred_sexp_ss 1);
+val pred_sexp_CONS_I1 = result();
goalw List.thy [CONS_def,In1_def]
- "!!M. [| M: Sexp; N: Sexp |] ==> <N, CONS(M,N)> : pred_Sexp^+";
-by (asm_simp_tac pred_Sexp_ss 1);
-val pred_Sexp_CONS_I2 = result();
+ "!!M. [| M: sexp; N: sexp |] ==> <N, CONS(M,N)> : pred_sexp^+";
+by (asm_simp_tac pred_sexp_ss 1);
+val pred_sexp_CONS_I2 = result();
val [prem] = goal List.thy
- "<CONS(M1,M2), N> : pred_Sexp^+ ==> \
-\ <M1,N> : pred_Sexp^+ & <M2,N> : pred_Sexp^+";
-by (rtac (prem RS (pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS
+ "<CONS(M1,M2), N> : pred_sexp^+ ==> \
+\ <M1,N> : pred_sexp^+ & <M2,N> : pred_sexp^+";
+by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS
subsetD RS SigmaE2)) 1);
-by (etac (Sexp_CONS_D RS conjE) 1);
-by (REPEAT (ares_tac [conjI, pred_Sexp_CONS_I1, pred_Sexp_CONS_I2,
+by (etac (sexp_CONS_D RS conjE) 1);
+by (REPEAT (ares_tac [conjI, pred_sexp_CONS_I1, pred_sexp_CONS_I2,
prem RSN (2, trans_trancl RS transD)] 1));
-val pred_Sexp_CONS_D = result();
+val pred_sexp_CONS_D = result();
(** Conversion rules for List_rec **)
@@ -216,24 +182,25 @@
by (simp_tac (HOL_ss addsimps [List_case_NIL]) 1);
val List_rec_NIL = result();
-goal List.thy "!!M. [| M: Sexp; N: Sexp |] ==> \
+goal List.thy "!!M. [| M: sexp; N: sexp |] ==> \
\ List_rec(CONS(M,N), c, h) = h(M, N, List_rec(N,c,h))";
by (rtac (List_rec_unfold RS trans) 1);
by (asm_simp_tac
- (HOL_ss addsimps [List_case_CONS, CONS_I, pred_Sexp_CONS_I2, cut_apply])1);
+ (HOL_ss addsimps [List_case_CONS, list.CONS_I, pred_sexp_CONS_I2,
+ cut_apply])1);
val List_rec_CONS = result();
(*** list_rec -- by List_rec ***)
-val Rep_List_in_Sexp =
- [range_Leaf_subset_Sexp RS List_subset_Sexp, Rep_List] MRS subsetD;
+val Rep_list_in_sexp =
+ [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
local
val list_rec_simps = list_free_simps @
[List_rec_NIL, List_rec_CONS,
- Abs_List_inverse, Rep_List_inverse,
- Rep_List, rangeI, inj_Leaf, Inv_f_f,
- Sexp_LeafI, Rep_List_in_Sexp]
+ Abs_list_inverse, Rep_list_inverse,
+ Rep_list, rangeI, inj_Leaf, Inv_f_f,
+ sexp.LeafI, Rep_list_in_sexp]
in
val list_rec_Nil = prove_goalw List.thy [list_rec_def, Nil_def]
"list_rec(Nil,c,h) = c"
@@ -250,16 +217,16 @@
(*Type checking. Useful?*)
-val major::A_subset_Sexp::prems = goal List.thy
- "[| M: List(A); \
-\ A<=Sexp; \
+val major::A_subset_sexp::prems = goal List.thy
+ "[| M: list(A); \
+\ A<=sexp; \
\ c: C(NIL); \
-\ !!x y r. [| x: A; y: List(A); r: C(y) |] ==> h(x,y,r): C(CONS(x,y)) \
-\ |] ==> List_rec(M,c,h) : C(M :: 'a node set)";
-val Sexp_ListA_I = A_subset_Sexp RS List_subset_Sexp RS subsetD;
-val Sexp_A_I = A_subset_Sexp RS subsetD;
-by (rtac (major RS List_induct) 1);
-by (ALLGOALS(asm_simp_tac (list_ss addsimps ([Sexp_A_I,Sexp_ListA_I]@prems))));
+\ !!x y r. [| x: A; y: list(A); r: C(y) |] ==> h(x,y,r): C(CONS(x,y)) \
+\ |] ==> List_rec(M,c,h) : C(M :: 'a item)";
+val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
+val sexp_A_I = A_subset_sexp RS subsetD;
+by (rtac (major RS list.induct) 1);
+by (ALLGOALS(asm_simp_tac (list_ss addsimps ([sexp_A_I,sexp_ListA_I]@prems))));
val List_rec_type = result();
(** Generalized map functionals **)
@@ -273,7 +240,7 @@
by (rtac list_rec_Cons 1);
val Rep_map_Cons = result();
-goalw List.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map(f,xs): List(A)";
+goalw List.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map(f,xs): list(A)";
by (rtac list_induct 1);
by(ALLGOALS(asm_simp_tac list_ss));
val Rep_map_type = result();
@@ -283,7 +250,7 @@
val Abs_map_NIL = result();
val prems = goalw List.thy [Abs_map_def]
- "[| M: Sexp; N: Sexp |] ==> \
+ "[| M: sexp; N: sexp |] ==> \
\ Abs_map(g, CONS(M,N)) = g(M) # Abs_map(g,N)";
by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
val Abs_map_CONS = result();
@@ -380,11 +347,11 @@
map_Nil, map_Cons];
val map_ss = list_free_ss addsimps map_simps;
-val [major,A_subset_Sexp,minor] = goal List.thy
- "[| M: List(A); A<=Sexp; !!z. z: A ==> f(g(z)) = z |] \
+val [major,A_subset_sexp,minor] = goal List.thy
+ "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |] \
\ ==> Rep_map(f, Abs_map(g,M)) = M";
-by (rtac (major RS List_induct) 1);
-by (ALLGOALS (asm_simp_tac(map_ss addsimps [Sexp_A_I,Sexp_ListA_I,minor])));
+by (rtac (major RS list.induct) 1);
+by (ALLGOALS (asm_simp_tac(map_ss addsimps [sexp_A_I,sexp_ListA_I,minor])));
val Abs_map_inverse = result();
(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
@@ -417,11 +384,11 @@
by (ALLGOALS (asm_simp_tac map_ss));
val map_compose = result();
-goal List.thy "!!f. (!!x. f(x): Sexp) ==> \
+goal List.thy "!!f. (!!x. f(x): sexp) ==> \
\ Abs_map(g, Rep_map(f,xs)) = map(%t. g(f(t)), xs)";
by (list_ind_tac "xs" 1);
by(ALLGOALS(asm_simp_tac(map_ss addsimps
- [Rep_map_type,List_Sexp RS subsetD])));
+ [Rep_map_type,list_sexp RS subsetD])));
val Abs_Rep_map = result();
val list_ss = list_ss addsimps
--- a/List.thy Thu Aug 25 10:47:33 1994 +0200
+++ b/List.thy Thu Aug 25 11:01:45 1994 +0200
@@ -5,9 +5,9 @@
Definition of type 'a list by a least fixed point
-We use List(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
-and not List == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
-so that List can serve as a "functor" for defining other recursive types
+We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
+and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
+so that list can serve as a "functor" for defining other recursive types
*)
List = Sexp +
@@ -21,19 +21,19 @@
consts
- List_Fun :: "['a node set set, 'a node set set] => 'a node set set"
- List :: "'a node set set => 'a node set set"
- Rep_List :: "'a list => 'a node set"
- Abs_List :: "'a node set => 'a list"
- NIL :: "'a node set"
- CONS :: "['a node set, 'a node set] => 'a node set"
+ list :: "'a item set => 'a item set"
+ Rep_list :: "'a list => 'a item"
+ Abs_list :: "'a item => 'a list"
+ NIL :: "'a item"
+ CONS :: "['a item, 'a item] => 'a item"
Nil :: "'a list"
"#" :: "['a, 'a list] => 'a list" (infixr 65)
- List_case :: "['b, ['a node set, 'a node set]=>'b, 'a node set] => 'b"
- List_rec :: "['a node set, 'b, ['a node set, 'a node set, 'b]=>'b] => 'b"
+ List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
+ List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
+ list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
- Rep_map :: "('b => 'a node set) => ('b list => 'a node set)"
- Abs_map :: "('a node set => 'b) => 'a node set => 'b list"
+ Rep_map :: "('b => 'a item) => ('b list => 'a item)"
+ Abs_map :: "('a item => 'b) => 'a item => 'b list"
null :: "'a list => bool"
hd :: "'a list => 'a"
tl,ttl :: "'a list => 'a list"
@@ -41,13 +41,12 @@
list_all :: "('a => bool) => ('a list => bool)"
map :: "('a=>'b) => ('a list => 'b list)"
"@" :: "['a list, 'a list] => 'a list" (infixr 65)
- list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
filter :: "['a => bool, 'a list] => 'a list"
- (* List Enumeration *)
+ (* list Enumeration *)
"[]" :: "'a list" ("[]")
- "@List" :: "args => 'a list" ("[(_)]")
+ "@list" :: "args => 'a list" ("[(_)]")
(* Special syntax for list_all and filter *)
"@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
@@ -63,51 +62,51 @@
"[x:xs . P]" == "filter(%x.P,xs)"
"Alls x:xs.P" == "list_all(%x.P,xs)"
-rules
-
- List_Fun_def "List_Fun(A) == (%Z. {Numb(0)} <+> A <*> Z)"
- List_def "List(A) == lfp(List_Fun(A))"
-
- (* Faking a Type Definition ... *)
-
- Rep_List "Rep_List(xs): List(range(Leaf))"
- Rep_List_inverse "Abs_List(Rep_List(xs)) = xs"
- Abs_List_inverse "M: List(range(Leaf)) ==> Rep_List(Abs_List(M)) = M"
-
+defs
(* Defining the Concrete Constructors *)
-
NIL_def "NIL == In0(Numb(0))"
CONS_def "CONS(M, N) == In1(M $ N)"
- (* Defining the Abstract Constructors *)
+inductive "list(A)"
+ intrs
+ NIL_I "NIL: list(A)"
+ CONS_I "[| a: A; M: list(A) |] ==> CONS(a,M) : list(A)"
- Nil_def "Nil == Abs_List(NIL)"
- Cons_def "x#xs == Abs_List(CONS(Leaf(x), Rep_List(xs)))"
+rules
+ (* Faking a Type Definition ... *)
+ Rep_list "Rep_list(xs): list(range(Leaf))"
+ Rep_list_inverse "Abs_list(Rep_list(xs)) = xs"
+ Abs_list_inverse "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
+
+
+defs
+ (* Defining the Abstract Constructors *)
+ Nil_def "Nil == Abs_list(NIL)"
+ Cons_def "x#xs == Abs_list(CONS(Leaf(x), Rep_list(xs)))"
List_case_def "List_case(c, d) == Case(%x.c, Split(d))"
- (* List Recursion -- the trancl is Essential; see list.ML *)
+ (* list Recursion -- the trancl is Essential; see list.ML *)
List_rec_def
- "List_rec(M, c, d) == wfrec(trancl(pred_Sexp), M, \
+ "List_rec(M, c, d) == wfrec(trancl(pred_sexp), M, \
\ List_case(%g.c, %x y g. d(x, y, g(y))))"
list_rec_def
"list_rec(l, c, d) == \
-\ List_rec(Rep_List(l), c, %x y r. d(Inv(Leaf, x), Abs_List(y), r))"
+\ List_rec(Rep_list(l), c, %x y r. d(Inv(Leaf, x), Abs_list(y), r))"
(* Generalized Map Functionals *)
- Rep_map_def
- "Rep_map(f, xs) == list_rec(xs, NIL, %x l r. CONS(f(x), r))"
- Abs_map_def
- "Abs_map(g, M) == List_rec(M, Nil, %N L r. g(N)#r)"
+ Rep_map_def "Rep_map(f, xs) == list_rec(xs, NIL, %x l r. CONS(f(x), r))"
+ Abs_map_def "Abs_map(g, M) == List_rec(M, Nil, %N L r. g(N)#r)"
null_def "null(xs) == list_rec(xs, True, %x xs r.False)"
hd_def "hd(xs) == list_rec(xs, @x.True, %x xs r.x)"
tl_def "tl(xs) == list_rec(xs, @xs.True, %x xs r.xs)"
(* a total version of tl: *)
ttl_def "ttl(xs) == list_rec(xs, [], %x xs r.xs)"
+
mem_def "x mem xs == \
\ list_rec(xs, False, %y ys r. if(y=x, True, r))"
list_all_def "list_all(P, xs) == list_rec(xs, True, %x l r. P(x) & r)"
@@ -115,6 +114,7 @@
append_def "xs@ys == list_rec(xs, ys, %x l r. x#r)"
filter_def "filter(P,xs) == \
\ list_rec(xs, [], %x xs r. if(P(x), x#r, r))"
+
list_case_def "list_case(a, f, xs) == list_rec(xs, a, %x xs r.f(x, xs))"
end
--- a/Makefile Thu Aug 25 10:47:33 1994 +0200
+++ b/Makefile Thu Aug 25 11:01:45 1994 +0200
@@ -23,15 +23,18 @@
equalities.thy equalities.ML \
Prod.thy Prod.ML Sum.thy Sum.ML WF.thy WF.ML \
mono.thy mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML \
+ add_ind_def.ML ind_syntax.ML indrule.ML Inductive.ML \
+ intr_elim.ML Datatype.ML ../Pure/section_utils.ML\
+ Finite.ML Finite.thy\
Arith.thy Arith.ML Sexp.thy Sexp.ML Univ.thy Univ.ML \
LList.thy LList.ML List.thy List.ML \
- Datatype.ML \
../Provers/classical.ML ../Provers/simplifier.ML \
../Provers/splitter.ML ../Provers/ind.ML
-EX_FILES = ex/ROOT.ML ex/cla.ML ex/Finite.ML ex/Finite.thy\
+EX_FILES = ex/ROOT.ML ex/cla.ML \
ex/LexProd.ML ex/LexProd.thy ex/meson.ML ex/mesontest.ML\
- ex/MT.ML ex/MT.thy ex/PL.ML ex/PL.thy ex/Puzzle.ML ex/Puzzle.thy\
+ ex/MT.ML ex/MT.thy ex/Acc.ML ex/Acc.thy \
+ ex/PL.ML ex/PL.thy ex/Puzzle.ML ex/Puzzle.thy\
ex/Qsort.thy ex/Qsort.ML\
ex/Rec.ML ex/Rec.thy ex/rel.ML ex/set.ML ex/Simult.ML ex/Simult.thy\
ex/Term.ML ex/Term.thy
--- a/Nat.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Nat.ML Thu Aug 25 11:01:45 1994 +0200
@@ -31,8 +31,7 @@
val major::prems = goal Nat.thy
"[| i: Nat; P(Zero_Rep); \
\ !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |] ==> P(i)";
-by (rtac (major RS (Nat_def RS def_induct)) 1);
-by (rtac Nat_fun_mono 1);
+by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
by (fast_tac (set_cs addIs prems) 1);
val Nat_induct = result();
--- a/Prod.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Prod.ML Thu Aug 25 11:01:45 1994 +0200
@@ -102,6 +102,10 @@
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
val splitE = result();
+goal Prod.thy "!!R a b. split(R,<a,b>) ==> R(a,b)";
+by (etac (split RS iffD1) 1);
+val splitD = result();
+
goal Prod.thy "!!a b c. z: c(a,b) ==> z: split(c, <a,b>)";
by (asm_simp_tac pair_ss 1);
val mem_splitI = result();
--- a/ROOT.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/ROOT.ML Thu Aug 25 11:01:45 1994 +0200
@@ -10,13 +10,7 @@
val banner = "Higher-Order Logic";
writeln banner;
-(* Add user section "datatype" *)
-use "Datatype.ML";
-structure ThySyn =
- ThySynFun(val user_keywords = ["|", "datatype", "primrec"]
- and user_sections = [("datatype", datatype_decls),
- ("primrec", primrec_decl)]);
-init_thy_reader ();
+init_thy_reader();
print_depth 1;
eta_contract := true;
@@ -81,6 +75,29 @@
use_thy "equalities";
use_thy "Prod";
use_thy "Sum";
+use_thy "Gfp";
+use_thy "Nat";
+
+(* Add user sections *)
+use "Datatype.ML";
+use "../Pure/section_utils.ML";
+use "ind_syntax.ML";
+use "add_ind_def.ML";
+use "intr_elim.ML";
+use "indrule.ML";
+use "Inductive.ML";
+
+structure ThySyn = ThySynFun
+ (val user_keywords = ["|", "datatype", "primrec",
+ "inductive", "coinductive", "intrs",
+ "monos", "con_defs"]
+ and user_sections = [("inductive", inductive_decl ""),
+ ("coinductive", inductive_decl "Co"),
+ ("datatype", datatype_decls),
+ ("primrec", primrec_decl)]);
+init_thy_reader ();
+
+use_thy "Finite";
use_thy "LList";
use "../Pure/install_pp.ML";
--- a/Set.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Set.ML Thu Aug 25 11:01:45 1994 +0200
@@ -434,3 +434,14 @@
by (rtac (major RS INT_E) 1);
by (REPEAT (eresolve_tac prems 1));
val InterE = result();
+
+(*** Powerset ***)
+
+val PowI = prove_goalw Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)"
+ (fn _ => [ (etac CollectI 1) ]);
+
+val PowD = prove_goalw Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B"
+ (fn _=> [ (etac CollectD 1) ]);
+
+val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *)
+val Pow_top = subset_refl RS PowI; (* A : Pow(A) *)
--- a/Set.thy Thu Aug 25 10:47:33 1994 +0200
+++ b/Set.thy Thu Aug 25 11:01:45 1994 +0200
@@ -27,6 +27,7 @@
UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10)
INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10)
Union, Inter :: "(('a set)set) => 'a set" (*of a set*)
+ Pow :: "'a set => 'a set set" (*powerset*)
range :: "('a => 'b) => 'b set" (*of function*)
Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*)
inj, surj :: "('a => 'b) => bool" (*inj/surjective*)
@@ -80,8 +81,8 @@
mem_Collect_eq "(a : {x.P(x)}) = P(a)"
Collect_mem_eq "{x.x:A} = A"
- (* Definitions *)
+defs
Ball_def "Ball(A, P) == ! x. x:A --> P(x)"
Bex_def "Bex(A, P) == ? x. x:A & P(x)"
subset_def "A <= B == ! x:A. x:B"
@@ -95,6 +96,7 @@
UNION1_def "UNION1(B) == UNION({x.True}, B)"
Inter_def "Inter(S) == (INT x:S. x)"
Union_def "Union(S) == (UN x:S. x)"
+ Pow_def "Pow(A) == {B. B <= A}"
empty_def "{} == {x. False}"
insert_def "insert(a, B) == {x.x=a} Un B"
range_def "range(f) == {y. ? x. y=f(x)}"
--- a/Sexp.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Sexp.ML Thu Aug 25 11:01:45 1994 +0200
@@ -1,166 +1,135 @@
-(* Title: HOL/sexp
+(* Title: HOL/Sexp
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-For sexp.thy. S-expressions.
+S-expressions, general binary trees for defining recursive data structures
*)
open Sexp;
-(** the sexp functional **)
-
-goal Sexp.thy "mono(%Z. range(Leaf) Un range(Numb) Un Z<*>Z)";
-by (REPEAT (ares_tac [monoI, subset_refl, Un_mono, uprod_mono] 1));
-val Sexp_fun_mono = result();
-
-val Sexp_unfold = Sexp_fun_mono RS (Sexp_def RS def_lfp_Tarski);
+(** sexp_case **)
-(** Induction **)
-
-val major::prems = goal Sexp.thy
- "[| ii: Sexp; !!a. P(Leaf(a)); !!k. P(Numb(k)); \
-\ !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i$j) \
-\ |] ==> P(ii)";
-by (rtac (major RS (Sexp_def RS def_induct)) 1);
-by (rtac Sexp_fun_mono 1);
-by (fast_tac (set_cs addIs prems addSEs [uprodE]) 1);
-val Sexp_induct = result();
+val sexp_free_cs =
+ set_cs addSDs [Leaf_inject, Numb_inject, Scons_inject]
+ addSEs [Leaf_neq_Scons, Leaf_neq_Numb,
+ Numb_neq_Scons, Numb_neq_Leaf,
+ Scons_neq_Leaf, Scons_neq_Numb];
-(** Sexp_case **)
-
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, Leaf(a)) = c(a)";
-by (fast_tac (HOL_cs addIs [select_equality]
- addSDs [Leaf_inject]
- addSEs [Leaf_neq_Scons, Leaf_neq_Numb]) 1);
-val Sexp_case_Leaf = result();
+goalw Sexp.thy [sexp_case_def] "sexp_case(c, d, e, Leaf(a)) = c(a)";
+by (resolve_tac [select_equality] 1);
+by (ALLGOALS (fast_tac sexp_free_cs));
+val sexp_case_Leaf = result();
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, Numb(k)) = d(k)";
-by (fast_tac (HOL_cs addIs [select_equality]
- addSDs [Numb_inject]
- addSEs [Numb_neq_Scons, Numb_neq_Leaf]) 1);
-val Sexp_case_Numb = result();
+goalw Sexp.thy [sexp_case_def] "sexp_case(c, d, e, Numb(k)) = d(k)";
+by (resolve_tac [select_equality] 1);
+by (ALLGOALS (fast_tac sexp_free_cs));
+val sexp_case_Numb = result();
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, M$N) = e(M,N)";
-by (fast_tac (HOL_cs addIs [select_equality]
- addSDs [Scons_inject]
- addSEs [Scons_neq_Leaf, Scons_neq_Numb]) 1);
-val Sexp_case_Scons = result();
+goalw Sexp.thy [sexp_case_def] "sexp_case(c, d, e, M$N) = e(M,N)";
+by (resolve_tac [select_equality] 1);
+by (ALLGOALS (fast_tac sexp_free_cs));
+val sexp_case_Scons = result();
-(** Introduction rules for Sexp constructors **)
-
-val SexpI = Sexp_unfold RS equalityD2 RS subsetD;
-
-goal Sexp.thy "Leaf(a): Sexp";
-by (fast_tac (set_cs addIs [SexpI]) 1);
-val Sexp_LeafI = result();
-
-goal Sexp.thy "Numb(a): Sexp";
-by (fast_tac (set_cs addIs [SexpI]) 1);
-val Sexp_NumbI = result();
-
-val prems = goal Sexp.thy
- "[| M: Sexp; N: Sexp |] ==> M$N : Sexp";
-by (fast_tac (set_cs addIs ([uprodI,SexpI]@prems)) 1);
-val Sexp_SconsI = result();
+(** Introduction rules for sexp constructors **)
val [prem] = goalw Sexp.thy [In0_def]
- "M: Sexp ==> In0(M) : Sexp";
-by (rtac (prem RS (Sexp_NumbI RS Sexp_SconsI)) 1);
-val Sexp_In0I = result();
+ "M: sexp ==> In0(M) : sexp";
+by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
+val sexp_In0I = result();
val [prem] = goalw Sexp.thy [In1_def]
- "M: Sexp ==> In1(M) : Sexp";
-by (rtac (prem RS (Sexp_NumbI RS Sexp_SconsI)) 1);
-val Sexp_In1I = result();
+ "M: sexp ==> In1(M) : sexp";
+by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
+val sexp_In1I = result();
+
+val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI];
-goal Sexp.thy "range(Leaf) <= Sexp";
-by (fast_tac (set_cs addIs [SexpI]) 1);
-val range_Leaf_subset_Sexp = result();
+goal Sexp.thy "range(Leaf) <= sexp";
+by (fast_tac sexp_cs 1);
+val range_Leaf_subset_sexp = result();
-val [major] = goal Sexp.thy "M$N : Sexp ==> M: Sexp & N: Sexp";
+val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
by (rtac (major RS setup_induction) 1);
-by (etac Sexp_induct 1);
+by (etac sexp.induct 1);
by (ALLGOALS
(fast_tac (set_cs addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
val Scons_D = result();
-(** Introduction rules for 'pred_Sexp' **)
-
-val sexp_cs = set_cs addIs [SigmaI, uprodI, SexpI];
+(** Introduction rules for 'pred_sexp' **)
-goalw Sexp.thy [pred_Sexp_def] "pred_Sexp <= Sigma(Sexp, %u.Sexp)";
+goalw Sexp.thy [pred_sexp_def] "pred_sexp <= Sigma(sexp, %u.sexp)";
by (fast_tac sexp_cs 1);
-val pred_Sexp_subset_Sigma = result();
+val pred_sexp_subset_Sigma = result();
-(* <a,b> : pred_Sexp^+ ==> a : Sexp *)
-val trancl_pred_SexpD1 =
- pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
-and trancl_pred_SexpD2 =
- pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
+(* <a,b> : pred_sexp^+ ==> a : sexp *)
+val trancl_pred_sexpD1 =
+ pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
+and trancl_pred_sexpD2 =
+ pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
-val prems = goalw Sexp.thy [pred_Sexp_def]
- "[| M: Sexp; N: Sexp |] ==> <M, M$N> : pred_Sexp";
+val prems = goalw Sexp.thy [pred_sexp_def]
+ "[| M: sexp; N: sexp |] ==> <M, M$N> : pred_sexp";
by (fast_tac (set_cs addIs prems) 1);
-val pred_SexpI1 = result();
+val pred_sexpI1 = result();
-val prems = goalw Sexp.thy [pred_Sexp_def]
- "[| M: Sexp; N: Sexp |] ==> <N, M$N> : pred_Sexp";
+val prems = goalw Sexp.thy [pred_sexp_def]
+ "[| M: sexp; N: sexp |] ==> <N, M$N> : pred_sexp";
by (fast_tac (set_cs addIs prems) 1);
-val pred_SexpI2 = result();
+val pred_sexpI2 = result();
(*Combinations involving transitivity and the rules above*)
-val pred_Sexp_t1 = pred_SexpI1 RS r_into_trancl
-and pred_Sexp_t2 = pred_SexpI2 RS r_into_trancl;
+val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
+and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
-val pred_Sexp_trans1 = pred_Sexp_t1 RSN (2, trans_trancl RS transD)
-and pred_Sexp_trans2 = pred_Sexp_t2 RSN (2, trans_trancl RS transD);
+val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
+and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
-(*Proves goals of the form <M,N>:pred_Sexp^+ provided M,N:Sexp*)
-val pred_Sexp_simps =
- [Sexp_LeafI, Sexp_NumbI, Sexp_SconsI,
- pred_Sexp_t1, pred_Sexp_t2,
- pred_Sexp_trans1, pred_Sexp_trans2, cut_apply];
-val pred_Sexp_ss = HOL_ss addsimps pred_Sexp_simps;
+(*Proves goals of the form <M,N>:pred_sexp^+ provided M,N:sexp*)
+val pred_sexp_simps =
+ sexp.intrs @
+ [pred_sexp_t1, pred_sexp_t2,
+ pred_sexp_trans1, pred_sexp_trans2, cut_apply];
+val pred_sexp_ss = HOL_ss addsimps pred_sexp_simps;
-val major::prems = goalw Sexp.thy [pred_Sexp_def]
- "[| p : pred_Sexp; \
-\ !!M N. [| p = <M, M$N>; M: Sexp; N: Sexp |] ==> R; \
-\ !!M N. [| p = <N, M$N>; M: Sexp; N: Sexp |] ==> R \
+val major::prems = goalw Sexp.thy [pred_sexp_def]
+ "[| p : pred_sexp; \
+\ !!M N. [| p = <M, M$N>; M: sexp; N: sexp |] ==> R; \
+\ !!M N. [| p = <N, M$N>; M: sexp; N: sexp |] ==> R \
\ |] ==> R";
by (cut_facts_tac [major] 1);
by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
-val pred_SexpE = result();
+val pred_sexpE = result();
-goal Sexp.thy "wf(pred_Sexp)";
-by (rtac (pred_Sexp_subset_Sigma RS wfI) 1);
-by (etac Sexp_induct 1);
-by (fast_tac (HOL_cs addSEs [mp, pred_SexpE, Pair_inject, Scons_inject]) 3);
-by (fast_tac (HOL_cs addSEs [mp, pred_SexpE, Pair_inject, Numb_neq_Scons]) 2);
-by (fast_tac (HOL_cs addSEs [mp, pred_SexpE, Pair_inject, Leaf_neq_Scons]) 1);
-val wf_pred_Sexp = result();
+goal Sexp.thy "wf(pred_sexp)";
+by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
+by (etac sexp.induct 1);
+by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
+by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
+by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
+val wf_pred_sexp = result();
-(*** Sexp_rec -- by wf recursion on pred_Sexp ***)
+(*** sexp_rec -- by wf recursion on pred_sexp ***)
(** conversion rules **)
-val Sexp_rec_unfold = wf_pred_Sexp RS (Sexp_rec_def RS def_wfrec);
+val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
-goal Sexp.thy "Sexp_rec(Leaf(a), c, d, h) = c(a)";
-by (stac Sexp_rec_unfold 1);
-by (rtac Sexp_case_Leaf 1);
-val Sexp_rec_Leaf = result();
+goal Sexp.thy "sexp_rec(Leaf(a), c, d, h) = c(a)";
+by (stac sexp_rec_unfold 1);
+by (rtac sexp_case_Leaf 1);
+val sexp_rec_Leaf = result();
-goal Sexp.thy "Sexp_rec(Numb(k), c, d, h) = d(k)";
-by (stac Sexp_rec_unfold 1);
-by (rtac Sexp_case_Numb 1);
-val Sexp_rec_Numb = result();
+goal Sexp.thy "sexp_rec(Numb(k), c, d, h) = d(k)";
+by (stac sexp_rec_unfold 1);
+by (rtac sexp_case_Numb 1);
+val sexp_rec_Numb = result();
-goal Sexp.thy "!!M. [| M: Sexp; N: Sexp |] ==> \
-\ Sexp_rec(M$N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))";
-by (rtac (Sexp_rec_unfold RS trans) 1);
+goal Sexp.thy "!!M. [| M: sexp; N: sexp |] ==> \
+\ sexp_rec(M$N, c, d, h) = h(M, N, sexp_rec(M,c,d,h), sexp_rec(N,c,d,h))";
+by (rtac (sexp_rec_unfold RS trans) 1);
by (asm_simp_tac(HOL_ss addsimps
- [Sexp_case_Scons,pred_SexpI1,pred_SexpI2,cut_apply])1);
-val Sexp_rec_Scons = result();
+ [sexp_case_Scons,pred_sexpI1,pred_sexpI2,cut_apply])1);
+val sexp_rec_Scons = result();
--- a/Sexp.thy Thu Aug 25 10:47:33 1994 +0200
+++ b/Sexp.thy Thu Aug 25 11:01:45 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/sexp
+(* Title: HOL/Sexp
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
@@ -8,29 +8,34 @@
Sexp = Univ +
consts
- Sexp :: "'a node set set"
+ sexp :: "'a item set"
- Sexp_case :: "['a=>'b, nat=>'b, ['a node set, 'a node set]=>'b, \
-\ 'a node set] => 'b"
+ sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, \
+\ 'a item] => 'b"
- Sexp_rec :: "['a node set, 'a=>'b, nat=>'b, \
-\ ['a node set, 'a node set, 'b, 'b]=>'b] => 'b"
+ sexp_rec :: "['a item, 'a=>'b, nat=>'b, \
+\ ['a item, 'a item, 'b, 'b]=>'b] => 'b"
- pred_Sexp :: "('a node set * 'a node set)set"
+ pred_sexp :: "('a item * 'a item)set"
+
+inductive "sexp"
+ intrs
+ LeafI "Leaf(a): sexp"
+ NumbI "Numb(a): sexp"
+ SconsI "[| M: sexp; N: sexp |] ==> M$N : sexp"
rules
- Sexp_def "Sexp == lfp(%Z. range(Leaf) Un range(Numb) Un Z<*>Z)"
- Sexp_case_def
- "Sexp_case(c,d,e,M) == @ z. (? x. M=Leaf(x) & z=c(x)) \
+ sexp_case_def
+ "sexp_case(c,d,e,M) == @ z. (? x. M=Leaf(x) & z=c(x)) \
\ | (? k. M=Numb(k) & z=d(k)) \
\ | (? N1 N2. M = N1 $ N2 & z=e(N1,N2))"
- pred_Sexp_def
- "pred_Sexp == UN M: Sexp. UN N: Sexp. {<M, M$N>, <N, M$N>}"
+ pred_sexp_def
+ "pred_sexp == UN M: sexp. UN N: sexp. {<M, M$N>, <N, M$N>}"
- Sexp_rec_def
- "Sexp_rec(M,c,d,e) == wfrec(pred_Sexp, M, \
-\ %M g. Sexp_case(c, d, %N1 N2. e(N1, N2, g(N1), g(N2)), M))"
+ sexp_rec_def
+ "sexp_rec(M,c,d,e) == wfrec(pred_sexp, M, \
+\ %M g. sexp_case(c, d, %N1 N2. e(N1, N2, g(N1), g(N2)), M))"
end
--- a/Sum.thy Thu Aug 25 10:47:33 1994 +0200
+++ b/Sum.thy Thu Aug 25 11:01:45 1994 +0200
@@ -9,7 +9,7 @@
Sum = Prod +
types
- ('a,'b) "+" (infixl 10)
+ ('a,'b) "+" (infixr 10)
arities
"+" :: (term,term)term
--- a/Trancl.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Trancl.ML Thu Aug 25 11:01:45 1994 +0200
@@ -114,8 +114,7 @@
\ !!x. P(<x,x>); \
\ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \
\ ==> P(<a,b>)";
-by (rtac (major RS (rtrancl_def RS def_induct)) 1);
-by (rtac rtrancl_fun_mono 1);
+by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
by (fast_tac (comp_cs addIs prems) 1);
val rtrancl_full_induct = result();
--- a/Univ.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/Univ.ML Thu Aug 25 11:01:45 1994 +0200
@@ -496,9 +496,11 @@
(*** Equality : the diagonal relation ***)
-goalw Univ.thy [diag_def] "!!a A. a:A ==> <a,a> : diag(A)";
-by (REPEAT (ares_tac [singletonI,UN_I] 1));
-val diagI = result();
+goalw Univ.thy [diag_def] "!!a A. [| a=b; a:A |] ==> <a,b> : diag(A)";
+by (fast_tac set_cs 1);
+val diag_eqI = result();
+
+val diagI = refl RS diag_eqI |> standard;
(*The general elimination rule*)
val major::prems = goalw Univ.thy [diag_def]
--- a/Univ.thy Thu Aug 25 10:47:33 1994 +0200
+++ b/Univ.thy Thu Aug 25 11:01:45 1994 +0200
@@ -15,6 +15,7 @@
types
'a node
+ 'a item = "'a node set"
arities
node :: (term)term
@@ -31,25 +32,25 @@
Push_Node :: "[nat, 'a node] => 'a node"
ndepth :: "'a node => nat"
- Atom :: "('a+nat) => 'a node set"
- Leaf :: "'a => 'a node set"
- Numb :: "nat => 'a node set"
- "$" :: "['a node set, 'a node set]=> 'a node set" (infixr 60)
- In0,In1 :: "'a node set => 'a node set"
+ Atom :: "('a+nat) => 'a item"
+ Leaf :: "'a => 'a item"
+ Numb :: "nat => 'a item"
+ "$" :: "['a item, 'a item]=> 'a item" (infixr 60)
+ In0,In1 :: "'a item => 'a item"
- ntrunc :: "[nat, 'a node set] => 'a node set"
+ ntrunc :: "[nat, 'a item] => 'a item"
- "<*>" :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 80)
- "<+>" :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 70)
+ "<*>" :: "['a item set, 'a item set]=> 'a item set" (infixr 80)
+ "<+>" :: "['a item set, 'a item set]=> 'a item set" (infixr 70)
- Split :: "[['a node set, 'a node set]=>'b, 'a node set] => 'b"
- Case :: "[['a node set]=>'b, ['a node set]=>'b, 'a node set] => 'b"
+ Split :: "[['a item, 'a item]=>'b, 'a item] => 'b"
+ Case :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"
diag :: "'a set => ('a * 'a)set"
- "<**>" :: "[('a node set * 'a node set)set, ('a node set * 'a node set)set] \
-\ => ('a node set * 'a node set)set" (infixr 80)
- "<++>" :: "[('a node set * 'a node set)set, ('a node set * 'a node set)set] \
-\ => ('a node set * 'a node set)set" (infixr 70)
+ "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
+\ => ('a item * 'a item)set" (infixr 80)
+ "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
+\ => ('a item * 'a item)set" (infixr 70)
rules
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/add_ind_def.ML Thu Aug 25 11:01:45 1994 +0200
@@ -0,0 +1,242 @@
+(* 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 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 Logic Ind_Syntax;
+
+(*internal version*)
+fun add_fp_def_i (rec_tms, intr_tms) thy =
+ let
+ val sign = sign_of thy;
+
+ (*recT and rec_params should agree for all mutually recursive components*)
+ val (Const(_,recT),rec_params) = strip_comb (hd rec_tms)
+ and rec_hds = map head_of rec_tms;
+
+ val domTs = summands(dest_set (body_type recT));
+
+ val rec_names = map (#1 o dest_Const) rec_hds;
+
+ val _ = assert_all Syntax.is_identifier rec_names
+ (fn a => "Name of recursive set not an identifier: " ^ a);
+
+ val _ = assert_all (is_some o lookup_const sign) rec_names
+ (fn a => "Recursive set not previously declared as constant: " ^ 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";
+
+ val dom_sumT = fold_bal mk_sum domTs;
+ val dom_set = mk_set dom_sumT;
+
+ val freez = Free(z, dom_sumT)
+ and freeX = Free(X, dom_set);
+ (*type of w may be any of the domTs*)
+
+ 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 (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*)
+ val parts = map mk_Part
+ (accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs) ~~
+ domTs);
+
+ (*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))
+
+ val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs)
+ "Illegal occurrence of recursion operator")
+ rec_hds;
+
+ (*** 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_name = space_implode "_" rec_names;
+
+ (*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 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));
+
+ val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
+
+ in thy |> add_defs_i axpairs end
+
+
+(****************************************************************OMITTED
+
+(*Expects the recursive sets to have been defined already.
+ con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
+fun add_constructs_def (rec_names, con_ty_lists) thy =
+* let
+* val _ = writeln" Defining the constructor functions...";
+* val case_name = "f"; (*name for case variables*)
+
+* (** Define the constructors **)
+
+* (*The empty tuple is 0*)
+* fun mk_tuple [] = Const("0",iT)
+* | mk_tuple args = foldr1 mk_Pair args;
+
+* fun mk_inject n k u = access_bal(ap Inl, ap Inr, u) n k;
+
+* val npart = length rec_names; (*total # of mutually recursive parts*)
+
+* (*Make constructor definition; kpart is # of this mutually recursive part*)
+* fun mk_con_defs (kpart, con_ty_list) =
+* let val ncon = length con_ty_list (*number of constructors*)
+ fun mk_def (((id,T,syn), name, args, prems), kcon) =
+ (*kcon is index of constructor*)
+ mk_defpair (list_comb (Const(name,T), args),
+ mk_inject npart kpart
+ (mk_inject ncon kcon (mk_tuple args)))
+* in map mk_def (con_ty_list ~~ (1 upto ncon)) end;
+
+* (** Define the case operator **)
+
+* (*Combine split terms using case; yields the case operator for one part*)
+* fun call_case case_list =
+* let fun call_f (free,args) =
+ ap_split T free (map (#2 o dest_Free) args)
+* in fold_bal (app sum_case) (map call_f case_list) end;
+
+* (** Generating function variables for the case definition
+ Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
+
+* (*Treatment of a single constructor*)
+* fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =
+ if Syntax.is_identifier id
+ then (opno,
+ (Free(case_name ^ "_" ^ id, T), args) :: cases)
+ else (opno+1,
+ (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) ::
+ cases)
+
+* (*Treatment of a list of constructors, for one part*)
+* fun add_case_list (con_ty_list, (opno,case_lists)) =
+ let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
+ in (opno', case_list :: case_lists) end;
+
+* (*Treatment of all parts*)
+* val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
+
+* val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
+
+* val big_rec_name = space_implode "_" rec_names;
+
+* val big_case_name = big_rec_name ^ "_case";
+
+* (*The list of all the function variables*)
+* val big_case_args = flat (map (map #1) case_lists);
+
+* val big_case_tm =
+ list_comb (Const(big_case_name, big_case_typ), big_case_args);
+
+* val big_case_def = mk_defpair
+ (big_case_tm, fold_bal (app sum_case) (map call_case case_lists));
+
+* (** Build the new theory **)
+
+* val const_decs =
+ (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
+
+* val axpairs =
+ big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))
+
+* in thy |> add_consts_i const_decs |> add_defs_i axpairs end;
+****************************************************************)
+end;
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ind_syntax.ML Thu Aug 25 11:01:45 1994 +0200
@@ -0,0 +1,151 @@
+(* 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 ../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
+
+(** Abstract syntax definitions for HOL **)
+
+val termC: class = "term";
+val termS: sort = [termC];
+
+val termTVar = TVar(("'a",0),termS);
+
+val boolT = Type("bool",[]);
+val unitT = Type("unit",[]);
+
+val conj = Const("op &", [boolT,boolT]--->boolT)
+and disj = Const("op |", [boolT,boolT]--->boolT)
+and imp = Const("op -->", [boolT,boolT]--->boolT);
+
+fun eq_const T = Const("op =", [T,T]--->boolT);
+
+fun mk_set T = Type("set",[T]);
+
+fun dest_set (Type("set",[T])) = T
+ | dest_set _ = error "dest_set: set type expected"
+
+fun mk_mem (x,A) =
+ let val setT = fastype_of A
+ in Const("op :", [dest_set setT, setT]--->boolT) $ x $ A
+ end;
+
+fun Int_const T =
+ let val sT = mk_set T
+ in Const("op Int", [sT,sT]--->sT) end;
+
+fun exists_const T = Const("Ex", [T-->boolT]--->boolT);
+fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
+
+fun all_const T = Const("All", [T-->boolT]--->boolT);
+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_set (fastype_of A)
+ in all_const T $ Abs("v", T, imp $ (mk_mem (Bound 0, A)) $ (P $ Bound 0))
+ end;
+
+(** Cartesian product type **)
+
+fun mk_prod (T1,T2) = Type("*", [T1,T2]);
+
+fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
+ | factors T = [T];
+
+(*Make a correctly typed ordered pair*)
+fun mk_Pair (t1,t2) =
+ let val T1 = fastype_of t1
+ and T2 = fastype_of t2
+ in Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2 end;
+
+fun split_const(Ta,Tb,Tc) =
+ Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
+
+(*Given u expecting arguments of types [T1,...,Tn], create term of
+ type T1*...*Tn => Tc using split. Here * associates to the LEFT*)
+fun ap_split_l Tc u [ ] = Abs("null", unitT, u)
+ | ap_split_l Tc u [_] = u
+ | ap_split_l Tc u (Ta::Tb::Ts) = ap_split_l Tc (split_const(Ta,Tb,Tc) $ u)
+ (mk_prod(Ta,Tb) :: Ts);
+
+(*Given u expecting arguments of types [T1,...,Tn], create term of
+ type T1*...*Tn => i using split. Here * associates to the RIGHT*)
+fun ap_split Tc u [ ] = Abs("null", unitT, u)
+ | ap_split Tc u [_] = u
+ | ap_split Tc u [Ta,Tb] = split_const(Ta,Tb,Tc) $ u
+ | ap_split Tc u (Ta::Ts) =
+ split_const(Ta, foldr1 mk_prod Ts, Tc) $
+ (Abs("v", Ta, ap_split Tc (u $ Bound(length Ts - 2)) Ts));
+
+(** 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);
+
+fun Collect_const T = Const("Collect", [T-->boolT] ---> mk_set T);
+fun mk_Collect (a,T,t) = Collect_const T $ absfree(a, T, t);
+
+val Trueprop = Const("Trueprop",boolT-->propT);
+fun mk_tprop P = Trueprop $ P;
+
+
+(*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]);
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/indrule.ML Thu Aug 25 11:01:45 1994 +0200
@@ -0,0 +1,176 @@
+(* 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: INTR_ELIM) : INDRULE =
+struct
+open Logic Ind_Syntax Inductive Intr_elim;
+
+val sign = sign_of thy;
+
+val (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
+
+val elem_type = dest_set (body_type recT);
+val domTs = summands(elem_type);
+val big_rec_name = space_implode "_" rec_names;
+val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
+
+val _ = writeln " Proving the induction rules...";
+
+(*** 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 :: mk_tprop (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,
+ Int_const T $ rec_tm $ (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)
+ (strip_imp_prems intr,[])
+ val (t,X) = rule_concl intr
+ val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
+ val concl = mk_tprop (pred $ t)
+ in list_all_free (quantfrees, list_implies (iprems,concl)) end
+ handle Bind => error"Recursion term not found in conclusion";
+
+(*Avoids backtracking by delivering the correct premise to each goal*)
+fun ind_tac [] 0 = all_tac
+ | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI,prem] i) THEN
+ ind_tac prems (i-1);
+
+val pred = Free(pred_name, elem_type --> boolT);
+
+val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;
+
+val quant_induct =
+ prove_goalw_cterm part_rec_defs
+ (cterm_of sign (list_implies (ind_prems,
+ mk_tprop (mk_all_imp(big_rec_tm,pred)))))
+ (fn prems =>
+ [rtac (impI RS allI) 1,
+ etac raw_induct 1,
+ REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE,
+ ssubst])),
+ REPEAT (FIRSTGOAL (eresolve_tac [PartE, CollectE])),
+ ind_tac (rev prems) (length prems)])
+ handle e => print_sign_exn sign e;
+
+(*** Prove the simultaneous induction rule ***)
+
+(*Make distinct predicates for each inductive set;
+ Cartesian products in domT should nest ONLY to the left! *)
+
+(*Given a recursive set and its domain, return the "split" predicate
+ and a conclusion for the simultaneous induction rule*)
+fun mk_predpair (rec_tm,domT) =
+ let val rec_name = (#1 o dest_Const o head_of) rec_tm
+ val T = factors domT ---> boolT
+ val pfree = Free(pred_name ^ "_" ^ rec_name, T)
+ val frees = mk_frees "za" (binder_types T)
+ val qconcl =
+ foldr mk_all (frees,
+ imp $ (mk_mem (foldr1 mk_Pair frees, rec_tm))
+ $ (list_comb (pfree,frees)))
+ in (ap_split boolT pfree (binder_types T),
+ qconcl)
+ end;
+
+val (preds,qconcls) = split_list (map mk_predpair (rec_tms~~domTs));
+
+(*Used to form simultaneous induction lemma*)
+fun mk_rec_imp (rec_tm,pred) =
+ imp $ (mk_mem (Bound 0, rec_tm)) $ (pred $ Bound 0);
+
+(*To instantiate the main induction rule*)
+val induct_concl =
+ mk_tprop(mk_all_imp(big_rec_tm,
+ Abs("z", elem_type,
+ fold_bal (app conj)
+ (map mk_rec_imp (rec_tms~~preds)))))
+and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);
+
+val lemma = (*makes the link between the two induction rules*)
+ prove_goalw_cterm part_rec_defs
+ (cterm_of sign (mk_implies (induct_concl,mutual_induct_concl)))
+ (fn prems =>
+ [cut_facts_tac prems 1,
+ REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1
+ ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1
+ ORELSE dresolve_tac [spec, mp, splitD] 1)])
+ handle e => print_sign_exn sign e;
+
+(*Mutual induction follows by freeness of Inl/Inr.*)
+
+(*Removes Collects caused by M-operators in the intro rules*)
+val cmonos = [subset_refl RS Int_Collect_mono] RL 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 =
+ SELECT_GOAL
+ ((*unpackage and use "prem" in the corresponding place*)
+ REPEAT (FIRSTGOAL
+ (eresolve_tac ([conjE,mp]@cmonos) ORELSE'
+ ares_tac [prem,impI,conjI]))
+ (*prove remaining goals by contradiction*)
+ THEN rewrite_goals_tac (con_defs@part_rec_defs)
+ THEN REPEAT (eresolve_tac (PartE :: sumprod_free_SEs) 1))
+ i THEN mutual_ind_tac prems (i-1);
+
+val mutual_induct_split =
+ prove_goalw_cterm []
+ (cterm_of sign
+ (list_implies (map (induct_prem (rec_tms~~preds)) 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;
+
+(*Attempts to remove all occurrences of split*)
+val split_tac =
+ REPEAT (SOMEGOAL (FIRST' [rtac splitI,
+ dtac splitD,
+ etac splitE,
+ bound_hyp_subst_tac]))
+ THEN prune_params_tac;
+
+(*strip quantifier*)
+val induct = standard (quant_induct RS spec RSN (2,rev_mp));
+
+val mutual_induct = rule_by_tactic split_tac mutual_induct_split;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/intr_elim.ML Thu Aug 25 11:01:45 1994 +0200
@@ -0,0 +1,129 @@
+(* 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;
+
+(*internal items*)
+signature INDUCTIVE_I =
+ 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 unfold : thm (*fixed-point equation*)
+ val intrs : thm list (*introduction rules*)
+ val elim : thm (*case analysis theorem*)
+ val raw_induct : thm (*raw induction rule from Fp.induct*)
+ val mk_cases : thm list -> string -> thm (*generates case theorems*)
+ 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) : INTR_ELIM =
+struct
+open Logic Inductive Ind_Syntax;
+
+val rec_names = map (#1 o dest_Const o head_of) rec_tms;
+val big_rec_name = space_implode "_" rec_names;
+
+val _ = deny (big_rec_name mem map ! (stamps_of_thy 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 thy)
+ (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
+
+
+val sign = sign_of thy;
+
+(********)
+val _ = writeln " Proving monotonicity...";
+
+val Const("==",_) $ _ $ (Const(_,fpT) $ fp_abs) =
+ big_rec_def |> rep_thm |> #prop |> unvarify;
+
+(*For the type of the argument of mono*)
+val [monoT] = binder_types fpT;
+
+val mono =
+ prove_goalw_cterm []
+ (cterm_of sign (mk_tprop (Const("mono", monoT-->boolT) $ fp_abs)))
+ (fn _ =>
+ [rtac monoI 1,
+ REPEAT (ares_tac (basic_monos @ 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,
+ rtac (unfold RS ssubst) 1,
+ REPEAT (resolve_tac [Part_eqI,CollectI] 1),
+ (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
+ rtac disjIn 1,
+ REPEAT (ares_tac [refl,exI,conjI] 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 = map (uncurry (prove_goalw_cterm part_rec_defs))
+ (map (cterm_of sign) intr_tms ~~
+ map intro_tacsf (mk_disj_rls(length intr_tms)));
+
+(********)
+val _ = writeln " Proving the elimination rule...";
+
+(*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];
+
+(*Breaks down logical connectives in the monotonic function*)
+val basic_elim_tac =
+ REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
+ ORELSE' bound_hyp_subst_tac))
+ THEN prune_params_tac;
+
+val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
+
+(*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;
+
+(*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 thy s RS elim);
+
+val defs = big_rec_def::part_rec_defs;
+
+val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct);
+end;
+
--- a/mono.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/mono.ML Thu Aug 25 11:01:45 1994 +0200
@@ -6,15 +6,14 @@
Monotonicity of various operations
*)
-val [prem] = goal Set.thy
- "[| !!x. P(x) ==> Q(x) |] ==> Collect(P) <= Collect(Q)";
-by (fast_tac (set_cs addIs [prem]) 1);
-val Collect_mono = result();
-
goal Set.thy "!!A B. A<=B ==> f``A <= f``B";
by (fast_tac set_cs 1);
val image_mono = result();
+goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
+by (fast_tac set_cs 1);
+val Pow_mono = result();
+
goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)";
by (fast_tac set_cs 1);
val Union_mono = result();
@@ -70,3 +69,55 @@
addSEs [SigmaE]) 1);
val Sigma_mono = result();
+
+(** Monotonicity of implications. For inductive definitions **)
+
+goal Set.thy "!!A B x. A<=B ==> x:A --> x:B";
+by (rtac impI 1);
+by (etac subsetD 1);
+by (assume_tac 1);
+val in_mono = result();
+
+goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
+by (fast_tac HOL_cs 1);
+val conj_mono = result();
+
+goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
+by (fast_tac HOL_cs 1);
+val disj_mono = result();
+
+goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
+by (fast_tac HOL_cs 1);
+val imp_mono = result();
+
+goal HOL.thy "P-->P";
+by (rtac impI 1);
+by (assume_tac 1);
+val imp_refl = result();
+
+val [PQimp] = goal HOL.thy
+ "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
+by (fast_tac (HOL_cs addIs [PQimp RS mp]) 1);
+val ex_mono = result();
+
+val [PQimp] = goal HOL.thy
+ "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
+by (fast_tac (HOL_cs addIs [PQimp RS mp]) 1);
+val all_mono = result();
+
+val [PQimp] = goal Set.thy
+ "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
+by (fast_tac (set_cs addIs [PQimp RS mp]) 1);
+val Collect_mono = result();
+
+(*Used in indrule.ML*)
+val [subs,PQimp] = goal Set.thy
+ "[| A<=B; !!x. x:A ==> P(x) --> Q(x) \
+\ |] ==> A Int Collect(P) <= B Int Collect(Q)";
+by (fast_tac (set_cs addIs [subs RS subsetD, PQimp RS mp]) 1);
+val Int_Collect_mono = result();
+
+(*Used in intr_elim.ML and in individual datatype definitions*)
+val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,
+ ex_mono, Collect_mono, Part_mono, in_mono];
+