--- a/src/ZF/CardinalArith.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/CardinalArith.ML Fri Aug 12 12:51:34 1994 +0200
@@ -309,19 +309,24 @@
(*** Infinite Cardinals are Limit Ordinals ***)
-(*Using lam_injective might simplify this proof!*)
+goalw CardinalArith.thy [lepoll_def]
+ "!!i. nat <= A ==> succ(A) lepoll A";
+by (res_inst_tac [("x",
+ "lam z:succ(A). if(z=A, 0, if(z:nat, succ(z), z))")] exI 1);
+by (res_inst_tac [("d", "%y. if(y:nat, nat_case(A,%z.z,y), y)")]
+ lam_injective 1);
+by (fast_tac (ZF_cs addSIs [if_type, nat_0I, nat_succI]) 1);
+by (asm_simp_tac
+ (ZF_ss addsimps [nat_case_0, nat_case_succ, nat_0I, nat_succI]
+ setloop split_tac [expand_if]) 1);
+val nat_succ_lepoll = result();
+
goalw CardinalArith.thy [lepoll_def, inj_def]
"!!i. nat <= A ==> succ(A) lepoll A";
by (res_inst_tac [("x",
"lam z:succ(A). if(z=A, 0, if(z:nat, succ(z), z))")] exI 1);
by (rtac (lam_type RS CollectI) 1);
-by (rtac if_type 1);
-by (etac ([asm_rl, nat_0I] MRS subsetD) 1);
-by (etac succE 1);
-by (contr_tac 1);
-by (rtac if_type 1);
-by (assume_tac 2);
-by (etac ([asm_rl, nat_succI] MRS subsetD) 1 THEN assume_tac 1);
+by (fast_tac (ZF_cs addSIs [if_type, nat_0I, nat_succI]) 1);
by (REPEAT (rtac ballI 1));
by (asm_simp_tac
(ZF_ss addsimps [succ_inject_iff, succ_not_0, succ_not_0 RS not_sym]
--- a/src/ZF/CardinalArith.thy Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/CardinalArith.thy Fri Aug 12 12:51:34 1994 +0200
@@ -6,7 +6,7 @@
Cardinal Arithmetic
*)
-CardinalArith = Cardinal + OrderArith + Arith + Fin +
+CardinalArith = Cardinal + OrderArith + Arith + Finite +
consts
InfCard :: "i=>o"
--- a/src/ZF/Cardinal_AC.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/Cardinal_AC.ML Fri Aug 12 12:51:34 1994 +0200
@@ -135,3 +135,15 @@
by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);
val cardinal_UN_Ord_lt_csucc = result();
+goal Cardinal_AC.thy
+ "!!K. [| InfCard(K); |I| le K; ALL i:I. j(i) < csucc(K) |] ==> \
+\ (UN i:I. j(i)) < csucc(K)";
+by (asm_full_simp_tac
+ (ZF_ss addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1);
+by (eresolve_tac [exE] 1);
+by (resolve_tac [lt_trans1] 1);
+by (resolve_tac [cardinal_UN_Ord_lt_csucc] 2);
+by (assume_tac 2);
+
+val ?cardinal_UN_Ord_lt_csucc = result();
+
--- a/src/ZF/Datatype.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/Datatype.ML Fri Aug 12 12:51:34 1994 +0200
@@ -1,57 +1,12 @@
-(* Title: ZF/datatype.ML
+(* Title: ZF/Datatype.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory
*)
-(*Datatype definitions use least fixedpoints, standard products and sums*)
-functor Datatype_Fun (Const: CONSTRUCTOR)
- : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
-struct
-structure Constructor = Constructor_Fun (structure Const=Const and
- Pr=Standard_Prod and Su=Standard_Sum);
-open Const Constructor;
-
-structure Inductive = Inductive_Fun
- (val thy = con_thy;
- val thy_name = thy_name;
- val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
- val sintrs = sintrs;
- val monos = monos;
- val con_defs = con_defs;
- val type_intrs = type_intrs;
- val type_elims = type_elims);
-
-open Inductive
-end;
-
-
-(*Codatatype definitions use greatest fixedpoints, Quine products and sums*)
-functor CoDatatype_Fun (Const: CONSTRUCTOR)
- : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
-struct
-structure Constructor = Constructor_Fun (structure Const=Const and
- Pr=Quine_Prod and Su=Quine_Sum);
-open Const Constructor;
-
-structure CoInductive = CoInductive_Fun
- (val thy = con_thy;
- val thy_name = thy_name;
- val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
- val sintrs = sintrs;
- val monos = monos;
- val con_defs = con_defs;
- val type_intrs = type_intrs;
- val type_elims = type_elims);
-
-open CoInductive
-end;
-
-
-
(*For most datatypes involving univ*)
val datatype_intrs =
[SigmaI, InlI, InrI,
@@ -69,3 +24,110 @@
val codatatype_elims = [make_elim QInlD, make_elim QInrD];
+signature INDUCTIVE_THMS =
+ sig
+ val monos : thm list (*monotonicity of each M operator*)
+ val type_intrs : thm list (*type-checking intro rules*)
+ val type_elims : thm list (*type-checking elim rules*)
+ end;
+
+functor Data_section_Fun
+ (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)
+ : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
+struct
+
+structure Con = Constructor_Fun
+ (structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
+
+structure Inductive = Ind_section_Fun
+ (open Arg;
+ val con_defs = Con.con_defs
+ val type_intrs = Arg.type_intrs @ datatype_intrs
+ val type_elims = Arg.type_elims @ datatype_elims);
+
+open Inductive Con
+end;
+
+
+functor CoData_section_Fun
+ (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)
+ : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
+struct
+
+structure Con = Constructor_Fun
+ (structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
+
+structure CoInductive = CoInd_section_Fun
+ (open Arg;
+ val con_defs = Con.con_defs
+ val type_intrs = Arg.type_intrs @ codatatype_intrs
+ val type_elims = Arg.type_elims @ codatatype_elims);
+
+open CoInductive Con
+end;
+
+
+(*For installing the theory section. co is either "" or "Co"*)
+fun datatype_decl co =
+ let open ThyParse Ind_Syntax
+ (*generate strings*)
+ fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
+ val mk_data = mk_list o map mk_const o snd
+ val mk_scons = mk_big_list o map mk_data
+ fun mk_intr_name s = (*the "op" cancels any infix status*)
+ if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_"
+ fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) =
+ let val rec_names = map (scan_to_id o trim o fst) rec_pairs
+ val big_rec_name = space_implode "_" rec_names
+ and srec_tms = mk_list (map fst rec_pairs)
+ and scons = mk_scons rec_pairs
+ and sdom = (*default domain?*)
+ if dom = "" then co ^ "data_domain rec_tms"
+ else "replicate " ^ string_of_int (length rec_names) ^
+ " (readtm (sign_of thy) iT " ^ dom ^ ")"
+ val stri_name = big_rec_name ^ "_Intrnl"
+ val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
+ in
+ (";\n\n\
+ \structure " ^ stri_name ^ " =\n\
+ \ let open Ind_Syntax in\n\
+ \ struct\n\
+ \ val rec_tms\t= map (readtm (sign_of thy) iT) " ^ srec_tms ^ "\n\
+ \ val domts\t= " ^ sdom ^ "\n\
+ \ and con_ty_lists\t= read_constructs (sign_of thy)\n"
+ ^ scons ^ "\n\
+ \ val intr_tms\t= mk_all_intr_tms (rec_tms, con_ty_lists)\n\
+ \ end\n\
+ \ end;\n\n\
+ \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^
+ mk_list (map quote rec_names) ^ ", " ^
+ stri_name ^ ".con_ty_lists) \n\
+ \ |> " ^ co ^ "Ind.add_fp_def_i \n (" ^
+ stri_name ^ ".rec_tms, " ^
+ stri_name ^ ".domts, " ^
+ stri_name ^ ".intr_tms)"
+ ,
+ "structure " ^ big_rec_name ^ " =\n\
+ \ struct\n\
+ \ val _ = writeln \"" ^ co ^
+ "Datatype definition " ^ big_rec_name ^ "\"\n\
+ \ structure Result = " ^ co ^ "Data_section_Fun\n\
+ \ (open " ^ stri_name ^ "\n\
+ \ val thy\t\t= thy\n\
+ \ val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\
+ \ val monos\t\t= " ^ monos ^ "\n\
+ \ val type_intrs\t= " ^ type_intrs ^ "\n\
+ \ val type_elims\t= " ^ type_elims ^ ");\n\n\
+ \ val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
+ \ open Result\n\
+ \ end\n"
+ )
+ end
+ fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
+ val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
+ val construct = name -- string_list -- opt_mixfix;
+ in optional ("<=" $$-- string) "" --
+ enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
+ optstring "monos" -- optstring "type_intrs" -- optstring "type_elims"
+ >> mk_params
+end;
--- a/src/ZF/Datatype.thy Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/Datatype.thy Fri Aug 12 12:51:34 1994 +0200
@@ -1,4 +1,5 @@
(*Dummy theory to document dependencies *)
-Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
- (*this must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file
+Datatype = "constructor" + "inductive" + Univ + QUniv
+
+(*Datatype must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Finite.ML Fri Aug 12 12:51:34 1994 +0200
@@ -0,0 +1,94 @@
+(* Title: ZF/Finite.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Finite powerset operator
+
+prove X:Fin(A) ==> |X| < nat
+
+prove: b: Fin(A) ==> inj(b,b)<=surj(b,b)
+*)
+
+open Finite;
+
+goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac Fin.bnd_mono 1));
+by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
+val Fin_mono = result();
+
+(* A : Fin(B) ==> A <= B *)
+val FinD = Fin.dom_subset RS subsetD RS PowD;
+
+(** Induction on finite sets **)
+
+(*Discharging x~:y entails extra work*)
+val major::prems = goal Finite.thy
+ "[| b: Fin(A); \
+\ P(0); \
+\ !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) \
+\ |] ==> P(b)";
+by (rtac (major RS Fin.induct) 1);
+by (excluded_middle_tac "a:b" 2);
+by (etac (cons_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 = arith_ss addsimps Fin.intrs;
+
+(*The union of two finite sets is finite.*)
+val major::prems = goal Finite.thy
+ "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)";
+by (rtac (major RS Fin_induct) 1);
+by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
+val Fin_UnI = result();
+
+(*The union of a set of finite sets is finite.*)
+val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
+by (rtac (major RS Fin_induct) 1);
+by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
+val Fin_UnionI = result();
+
+(*Every subset of a finite set is finite.*)
+goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
+by (etac Fin_induct 1);
+by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
+by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
+by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
+by (ALLGOALS (asm_simp_tac Fin_ss));
+val Fin_subset_lemma = result();
+
+goal Finite.thy "!!c b A. [| c<=b; b: Fin(A) |] ==> c: Fin(A)";
+by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
+val Fin_subset = result();
+
+val major::prems = goal Finite.thy
+ "[| c: Fin(A); b: Fin(A); \
+\ P(b); \
+\ !!x 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_cons RS ssubst) 2);
+by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff,
+ Diff_subset RS Fin_subset]))));
+val Fin_0_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(0)";
+by (rtac (Diff_cancel RS subst) 1);
+by (rtac (Fin_0_induct_lemma RS mp) 1);
+by (REPEAT (ares_tac (subset_refl::prems) 1));
+val Fin_0_induct = result();
+
+(*Functions from a finite ordinal*)
+val prems = goal Finite.thy "n: nat ==> n->A <= Fin(nat*A)";
+by (nat_ind_tac "n" prems 1);
+by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin.emptyI, subset_iff, cons_iff]) 1);
+by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
+by (fast_tac (ZF_cs addSIs [Fin.consI]) 1);
+val nat_fun_subset_Fin = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Finite.thy Fri Aug 12 12:51:34 1994 +0200
@@ -0,0 +1,18 @@
+(* Title: ZF/Finite.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Finite powerset operator
+*)
+
+Finite = Arith +
+consts Fin :: "i=>i"
+inductive
+ domains "Fin(A)" <= "Pow(A)"
+ intrs
+ emptyI "0 : Fin(A)"
+ consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"
+ type_intrs "[empty_subsetI, cons_subsetI, PowI]"
+ type_elims "[make_elim PowD]"
+end
--- a/src/ZF/InfDatatype.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/InfDatatype.ML Fri Aug 12 12:51:34 1994 +0200
@@ -3,14 +3,90 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Infinite-Branching Datatype Definitions
+Datatype Definitions involving ->
+ Even infinite-branching!
*)
+(*** Closure under finite powerset ***)
+
+val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy);
+
+goal Fin_Univ_thy
+ "!!i. [| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
+by (eresolve_tac [Fin_induct] 1);
+by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1);
+by (safe_tac ZF_cs);
+by (eresolve_tac [Limit_VfromE] 1);
+by (assume_tac 1);
+by (res_inst_tac [("x", "xa Un j")] exI 1);
+by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD,
+ Un_least_lt]) 1);
+val Fin_Vfrom_lemma = result();
+
+goal Fin_Univ_thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
+by (rtac subsetI 1);
+by (dresolve_tac [Fin_Vfrom_lemma] 1);
+by (safe_tac ZF_cs);
+by (resolve_tac [Vfrom RS ssubst] 1);
+by (fast_tac (ZF_cs addSDs [ltD]) 1);
+val Fin_VLimit = result();
+
+val Fin_subset_VLimit =
+ [Fin_mono, Fin_VLimit] MRS subset_trans |> standard;
+
+goal Fin_Univ_thy
+ "!!i. [| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
+by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
+by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
+ nat_subset_VLimit, subset_refl] 1));
+val nat_fun_VLimit = result();
+
+val nat_fun_subset_VLimit =
+ [Pi_mono, nat_fun_VLimit] MRS subset_trans |> standard;
+
+
+goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)";
+by (rtac (Limit_nat RS Fin_VLimit) 1);
+val Fin_univ = result();
+
+val Fin_subset_univ = [Fin_mono, Fin_univ] MRS subset_trans |> standard;
+
+goalw Fin_Univ_thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
+by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
+val nat_fun_univ = result();
+
+val nat_fun_subset_univ = [Pi_mono, nat_fun_univ] MRS subset_trans |> standard;
+
+goal Fin_Univ_thy
+ "!!f. [| f: n -> B; B <= univ(A); n : nat |] ==> f : univ(A)";
+by (REPEAT (ares_tac [nat_fun_subset_univ RS subsetD] 1));
+val nat_fun_into_univ = result();
+
+
+(*** Infinite branching ***)
+
val fun_Limit_VfromE =
[apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
|> standard;
goal InfDatatype.thy
+ "!!K. [| f: I -> Vfrom(A,csucc(K)); |I| le K; InfCard(K) \
+\ |] ==> EX j. f: I -> Vfrom(A,j) & j < csucc(K)";
+by (res_inst_tac [("x", "UN x:I. LEAST i. f`x : Vfrom(A,i)")] exI 1);
+by (resolve_tac [conjI] 1);
+by (resolve_tac [ballI RSN (2,cardinal_UN_Ord_lt_csucc)] 2);
+by (eresolve_tac [fun_Limit_VfromE] 3 THEN REPEAT_SOME assume_tac);
+by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2);
+by (resolve_tac [Pi_type] 1);
+by (rename_tac "k" 2);
+by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac);
+by (subgoal_tac "f`k : Vfrom(A, LEAST i. f`k : Vfrom(A,i))" 1);
+by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2);
+by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);
+by (assume_tac 1);
+val fun_Vcsucc_lemma = result();
+
+goal InfDatatype.thy
"!!K. [| f: K -> Vfrom(A,csucc(K)); InfCard(K) \
\ |] ==> EX j. f: K -> Vfrom(A,j) & j < csucc(K)";
by (res_inst_tac [("x", "UN k:K. LEAST i. f`k : Vfrom(A,i)")] exI 1);
@@ -25,11 +101,11 @@
by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2);
by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);
by (assume_tac 1);
-val fun_Vfrom_csucc_lemma = result();
+val fun_Vcsucc_lemma = result();
goal InfDatatype.thy
"!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
-by (safe_tac (ZF_cs addSDs [fun_Vfrom_csucc_lemma]));
+by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma]));
by (resolve_tac [Vfrom RS ssubst] 1);
by (eresolve_tac [PiE] 1);
(*This level includes the function, and is below csucc(K)*)
@@ -42,35 +118,34 @@
Limit_has_succ, Un_least_lt] 1));
by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS lt_csucc] 1);
by (assume_tac 1);
-val fun_Vfrom_csucc = result();
+val fun_Vcsucc = result();
goal InfDatatype.thy
"!!K. [| f: K -> Vfrom(A, csucc(K)); InfCard(K) \
\ |] ==> f: Vfrom(A,csucc(K))";
-by (REPEAT (ares_tac [fun_Vfrom_csucc RS subsetD] 1));
-val fun_in_Vfrom_csucc = result();
+by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
+val fun_in_Vcsucc = result();
-val fun_subset_Vfrom_csucc =
- [Pi_mono, fun_Vfrom_csucc] MRS subset_trans |> standard;
+val fun_subset_Vcsucc =
+ [Pi_mono, fun_Vcsucc] MRS subset_trans |> standard;
goal InfDatatype.thy
"!!f. [| f: K -> B; B <= Vfrom(A,csucc(K)); InfCard(K) \
\ |] ==> f: Vfrom(A,csucc(K))";
-by (REPEAT (ares_tac [fun_subset_Vfrom_csucc RS subsetD] 1));
-val fun_into_Vfrom_csucc = result();
+by (REPEAT (ares_tac [fun_subset_Vcsucc RS subsetD] 1));
+val fun_into_Vcsucc = result();
val Limit_csucc = InfCard_csucc RS InfCard_is_Limit |> standard;
-val Pair_in_Vfrom_csucc = Limit_csucc RSN (3, Pair_in_Vfrom_Limit) |> standard;
-val Inl_in_Vfrom_csucc = Limit_csucc RSN (2, Inl_in_Vfrom_Limit) |> standard;
-val Inr_in_Vfrom_csucc = Limit_csucc RSN (2, Inr_in_Vfrom_Limit) |> standard;
-val zero_in_Vfrom_csucc = Limit_csucc RS zero_in_Vfrom_Limit |> standard;
-val nat_into_Vfrom_csucc = Limit_csucc RSN (2, nat_into_Vfrom_Limit)
- |> standard;
+val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard;
+val Inl_in_Vcsucc = Limit_csucc RSN (2, Inl_in_VLimit) |> standard;
+val Inr_in_Vcsucc = Limit_csucc RSN (2, Inr_in_VLimit) |> standard;
+val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit |> standard;
+val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) |> standard;
(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
val inf_datatype_intrs =
- [fun_in_Vfrom_csucc, InfCard_nat, Pair_in_Vfrom_csucc,
- Inl_in_Vfrom_csucc, Inr_in_Vfrom_csucc,
- zero_in_Vfrom_csucc, A_into_Vfrom, nat_into_Vfrom_csucc] @ datatype_intrs;
+ [fun_in_Vcsucc, InfCard_nat, Pair_in_Vcsucc,
+ Inl_in_Vcsucc, Inr_in_Vcsucc,
+ zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc] @ datatype_intrs;
--- a/src/ZF/InfDatatype.thy Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/InfDatatype.thy Fri Aug 12 12:51:34 1994 +0200
@@ -1,1 +1,1 @@
-InfDatatype = Datatype + Univ + Cardinal_AC
+InfDatatype = Datatype + Univ + Finite + Cardinal_AC
--- a/src/ZF/List.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/List.ML Fri Aug 12 12:51:34 1994 +0200
@@ -6,52 +6,42 @@
Datatype definition of Lists
*)
-structure List = Datatype_Fun
- (val thy = Univ.thy
- val thy_name = "List"
- val rec_specs = [("list", "univ(A)",
- [(["Nil"], "i", NoSyn),
- (["Cons"], "[i,i]=>i", NoSyn)])]
- val rec_styp = "i=>i"
- val sintrs = ["Nil : list(A)",
- "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"]
- val monos = []
- val type_intrs = datatype_intrs
- val type_elims = datatype_elims);
+open List;
-val [NilI, ConsI] = List.intrs;
+(*** Aspects of the datatype definition ***)
(*An elimination rule, for type-checking*)
-val ConsE = List.mk_cases List.con_defs "Cons(a,l) : list(A)";
+val ConsE = list.mk_cases list.con_defs "Cons(a,l) : list(A)";
(*Proving freeness results*)
-val Cons_iff = List.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
-val Nil_Cons_iff = List.mk_free "~ Nil=Cons(a,l)";
+val Cons_iff = list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
+val Nil_Cons_iff = list.mk_free "~ Nil=Cons(a,l)";
(*Perform induction on l, then prove the major premise using prems. *)
fun list_ind_tac a prems i =
- EVERY [res_inst_tac [("x",a)] List.induct i,
+ EVERY [res_inst_tac [("x",a)] list.induct i,
rename_last_tac a ["1"] (i+2),
ares_tac prems i];
goal List.thy "list(A) = {0} + (A * list(A))";
-by (rtac (List.unfold RS trans) 1);
-bws List.con_defs;
-by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs)
- addDs [List.dom_subset RS subsetD]
- addEs [A_into_univ]) 1);
+by (rtac (list.unfold RS trans) 1);
+bws list.con_defs;
+br equalityI 1;
+by (fast_tac sum_cs 1);
+by (fast_tac (sum_cs addIs datatype_intrs
+ addDs [list.dom_subset RS subsetD]) 1);
val list_unfold = result();
(** Lemmas to justify using "list" in other recursive type definitions **)
-goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)";
+goalw List.thy list.defs "!!A B. A<=B ==> list(A) <= list(B)";
by (rtac lfp_mono 1);
-by (REPEAT (rtac List.bnd_mono 1));
+by (REPEAT (rtac list.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
val list_mono = result();
(*There is a similar proof by list induction.*)
-goalw List.thy (List.defs@List.con_defs) "list(univ(A)) <= univ(A)";
+goalw List.thy (list.defs@list.con_defs) "list(univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
@@ -69,18 +59,374 @@
\ c: C(Nil); \
\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \
\ |] ==> list_case(c,h,l) : C(l)";
-by (rtac (major RS List.induct) 1);
-by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.case_eqns @ prems))));
+by (rtac (major RS list.induct) 1);
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (list.case_eqns @ prems))));
val list_case_type = result();
(** For recursion **)
-goalw List.thy List.con_defs "rank(a) < rank(Cons(a,l))";
+goalw List.thy list.con_defs "rank(a) < rank(Cons(a,l))";
by (simp_tac rank_ss 1);
val rank_Cons1 = result();
-goalw List.thy List.con_defs "rank(l) < rank(Cons(a,l))";
+goalw List.thy list.con_defs "rank(l) < rank(Cons(a,l))";
by (simp_tac rank_ss 1);
val rank_Cons2 = result();
+
+(*** List functions ***)
+
+(** hd and tl **)
+
+goalw List.thy [hd_def] "hd(Cons(a,l)) = a";
+by (resolve_tac list.case_eqns 1);
+val hd_Cons = result();
+
+goalw List.thy [tl_def] "tl(Nil) = Nil";
+by (resolve_tac list.case_eqns 1);
+val tl_Nil = result();
+
+goalw List.thy [tl_def] "tl(Cons(a,l)) = l";
+by (resolve_tac list.case_eqns 1);
+val tl_Cons = result();
+
+goal List.thy "!!l. l: list(A) ==> tl(l) : list(A)";
+by (etac list.elim 1);
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (list.intrs @ [tl_Nil,tl_Cons]))));
+val tl_type = result();
+
+(** drop **)
+
+goalw List.thy [drop_def] "drop(0, l) = l";
+by (rtac rec_0 1);
+val drop_0 = result();
+
+goalw List.thy [drop_def] "!!i. i:nat ==> drop(i, Nil) = Nil";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Nil])));
+val drop_Nil = result();
+
+goalw List.thy [drop_def]
+ "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Cons])));
+val drop_succ_Cons = result();
+
+goalw List.thy [drop_def]
+ "!!i l. [| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_type])));
+val drop_type = result();
+
+(** list_rec -- by Vset recursion **)
+
+goal List.thy "list_rec(Nil,c,h) = c";
+by (rtac (list_rec_def RS def_Vrec RS trans) 1);
+by (simp_tac (ZF_ss addsimps list.case_eqns) 1);
+val list_rec_Nil = result();
+
+goal List.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
+by (rtac (list_rec_def RS def_Vrec RS trans) 1);
+by (simp_tac (rank_ss addsimps (rank_Cons2::list.case_eqns)) 1);
+val list_rec_Cons = result();
+
+(*Type checking -- proved by induction, as usual*)
+val prems = goal List.thy
+ "[| l: list(A); \
+\ c: C(Nil); \
+\ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \
+\ |] ==> list_rec(l,c,h) : C(l)";
+by (list_ind_tac "l" prems 1);
+by (ALLGOALS (asm_simp_tac
+ (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons]))));
+val list_rec_type = result();
+
+(** Versions for use with definitions **)
+
+val [rew] = goal List.thy
+ "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
+by (rewtac rew);
+by (rtac list_rec_Nil 1);
+val def_list_rec_Nil = result();
+
+val [rew] = goal List.thy
+ "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
+by (rewtac rew);
+by (rtac list_rec_Cons 1);
+val def_list_rec_Cons = result();
+
+fun list_recs def = map standard
+ ([def] RL [def_list_rec_Nil, def_list_rec_Cons]);
+
+(** map **)
+
+val [map_Nil,map_Cons] = list_recs map_def;
+
+val prems = goalw List.thy [map_def]
+ "[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
+by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
+val map_type = result();
+
+val [major] = goal List.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";
+by (rtac (major RS map_type) 1);
+by (etac RepFunI 1);
+val map_type2 = result();
+
+(** length **)
+
+val [length_Nil,length_Cons] = list_recs length_def;
+
+goalw List.thy [length_def]
+ "!!l. l: list(A) ==> length(l) : nat";
+by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
+val length_type = result();
+
+(** app **)
+
+val [app_Nil,app_Cons] = list_recs app_def;
+
+goalw List.thy [app_def]
+ "!!xs ys. [| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)";
+by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
+val app_type = result();
+
+(** rev **)
+
+val [rev_Nil,rev_Cons] = list_recs rev_def;
+
+goalw List.thy [rev_def]
+ "!!xs. xs: list(A) ==> rev(xs) : list(A)";
+by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
+val rev_type = result();
+
+
+(** flat **)
+
+val [flat_Nil,flat_Cons] = list_recs flat_def;
+
+goalw List.thy [flat_def]
+ "!!ls. ls: list(list(A)) ==> flat(ls) : list(A)";
+by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
+val flat_type = result();
+
+
+(** list_add **)
+
+val [list_add_Nil,list_add_Cons] = list_recs list_add_def;
+
+goalw List.thy [list_add_def]
+ "!!xs. xs: list(nat) ==> list_add(xs) : nat";
+by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
+val list_add_type = result();
+
+(** List simplification **)
+
+val list_typechecks =
+ list.intrs @
+ [list_rec_type, map_type, map_type2, app_type, length_type,
+ rev_type, flat_type, list_add_type];
+
+val list_ss = arith_ss
+ addsimps list.case_eqns
+ addsimps [list_rec_Nil, list_rec_Cons,
+ map_Nil, map_Cons, app_Nil, app_Cons,
+ length_Nil, length_Cons, rev_Nil, rev_Cons,
+ flat_Nil, flat_Cons, list_add_Nil, list_add_Cons]
+ setsolver (type_auto_tac list_typechecks);
+
+
+(*** theorems about map ***)
+
+val prems = goal List.thy
+ "l: list(A) ==> map(%u.u, l) = l";
+by (list_ind_tac "l" prems 1);
+by (ALLGOALS (asm_simp_tac list_ss));
+val map_ident = result();
+
+val prems = goal List.thy
+ "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
+by (list_ind_tac "l" prems 1);
+by (ALLGOALS (asm_simp_tac list_ss));
+val map_compose = result();
+
+val prems = goal List.thy
+ "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
+by (list_ind_tac "xs" prems 1);
+by (ALLGOALS (asm_simp_tac list_ss));
+val map_app_distrib = result();
+
+val prems = goal List.thy
+ "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
+by (list_ind_tac "ls" prems 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
+val map_flat = result();
+
+val prems = goal List.thy
+ "l: list(A) ==> \
+\ list_rec(map(h,l), c, d) = \
+\ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
+by (list_ind_tac "l" prems 1);
+by (ALLGOALS (asm_simp_tac list_ss));
+val list_rec_map = result();
+
+(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
+
+(* c : list(Collect(B,P)) ==> c : list(B) *)
+val list_CollectD = standard (Collect_subset RS list_mono RS subsetD);
+
+val prems = goal List.thy
+ "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
+by (list_ind_tac "l" prems 1);
+by (ALLGOALS (asm_simp_tac list_ss));
+val map_list_Collect = result();
+
+(*** theorems about length ***)
+
+val prems = goal List.thy
+ "xs: list(A) ==> length(map(h,xs)) = length(xs)";
+by (list_ind_tac "xs" prems 1);
+by (ALLGOALS (asm_simp_tac list_ss));
+val length_map = result();
+
+val prems = goal List.thy
+ "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
+by (list_ind_tac "xs" prems 1);
+by (ALLGOALS (asm_simp_tac list_ss));
+val length_app = result();
+
+(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m
+ Used for rewriting below*)
+val add_commute_succ = nat_succI RSN (2,add_commute);
+
+val prems = goal List.thy
+ "xs: list(A) ==> length(rev(xs)) = length(xs)";
+by (list_ind_tac "xs" prems 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ])));
+val length_rev = result();
+
+val prems = goal List.thy
+ "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
+by (list_ind_tac "ls" prems 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
+val length_flat = result();
+
+(** Length and drop **)
+
+(*Lemma for the inductive step of drop_length*)
+goal List.thy
+ "!!xs. xs: list(A) ==> \
+\ ALL x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
+by (etac list.induct 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [drop_0,drop_succ_Cons])));
+by (fast_tac ZF_cs 1);
+val drop_length_Cons_lemma = result();
+val drop_length_Cons = standard (drop_length_Cons_lemma RS spec);
+
+goal List.thy
+ "!!l. l: list(A) ==> ALL i: length(l). EX z zs. drop(i,l) = Cons(z,zs)";
+by (etac list.induct 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps bquant_simps)));
+by (rtac conjI 1);
+by (etac drop_length_Cons 1);
+by (rtac ballI 1);
+by (rtac natE 1);
+by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
+by (assume_tac 1);
+by (asm_simp_tac (list_ss addsimps [drop_0]) 1);
+by (fast_tac ZF_cs 1);
+by (asm_simp_tac (list_ss addsimps [drop_succ_Cons]) 1);
+by (dtac bspec 1);
+by (fast_tac ZF_cs 2);
+by (fast_tac (ZF_cs addEs [succ_in_naturalD,length_type]) 1);
+val drop_length_lemma = result();
+val drop_length = standard (drop_length_lemma RS bspec);
+
+
+(*** theorems about app ***)
+
+val [major] = goal List.thy "xs: list(A) ==> xs@Nil=xs";
+by (rtac (major RS list.induct) 1);
+by (ALLGOALS (asm_simp_tac list_ss));
+val app_right_Nil = result();
+
+val prems = goal List.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
+by (list_ind_tac "xs" prems 1);
+by (ALLGOALS (asm_simp_tac list_ss));
+val app_assoc = result();
+
+val prems = goal List.thy
+ "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
+by (list_ind_tac "ls" prems 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
+val flat_app_distrib = result();
+
+(*** theorems about rev ***)
+
+val prems = goal List.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
+by (list_ind_tac "l" prems 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
+val rev_map_distrib = result();
+
+(*Simplifier needs the premises as assumptions because rewriting will not
+ instantiate the variable ?A in the rules' typing conditions; note that
+ rev_type does not instantiate ?A. Only the premises do.
+*)
+goal List.thy
+ "!!xs. [| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
+by (etac list.induct 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
+val rev_app_distrib = result();
+
+val prems = goal List.thy "l: list(A) ==> rev(rev(l))=l";
+by (list_ind_tac "l" prems 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
+val rev_rev_ident = result();
+
+val prems = goal List.thy
+ "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
+by (list_ind_tac "ls" prems 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps
+ [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
+val rev_flat = result();
+
+
+(*** theorems about list_add ***)
+
+val prems = goal List.thy
+ "[| xs: list(nat); ys: list(nat) |] ==> \
+\ list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
+by (cut_facts_tac prems 1);
+by (list_ind_tac "xs" prems 1);
+by (ALLGOALS
+ (asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym])));
+by (rtac (add_commute RS subst_context) 1);
+by (REPEAT (ares_tac [refl, list_add_type] 1));
+val list_add_app = result();
+
+val prems = goal List.thy
+ "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
+by (list_ind_tac "l" prems 1);
+by (ALLGOALS
+ (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right])));
+val list_add_rev = result();
+
+val prems = goal List.thy
+ "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
+by (list_ind_tac "ls" prems 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app])));
+by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
+val list_add_flat = result();
+
+(** New induction rule **)
+
+val major::prems = goal List.thy
+ "[| l: list(A); \
+\ P(Nil); \
+\ !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) \
+\ |] ==> P(l)";
+by (rtac (major RS rev_rev_ident RS subst) 1);
+by (rtac (major RS rev_type RS list.induct) 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
+val list_append_induct = result();
+
--- a/src/ZF/List.thy Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/List.thy Fri Aug 12 12:51:34 1994 +0200
@@ -1,3 +1,57 @@
-(*Dummy theory to document dependencies *)
+(* Title: ZF/List
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Lists in Zermelo-Fraenkel Set Theory
+
+map is a binding operator -- it applies to meta-level functions, not
+object-level functions. This simplifies the final form of term_rec_conv,
+although complicating its derivation.
+*)
+
+List = "Datatype" + Univ +
+
+consts
+ "@" :: "[i,i]=>i" (infixr 60)
+ list_rec :: "[i, i, [i,i,i]=>i] => i"
+ map :: "[i=>i, i] => i"
+ length,rev :: "i=>i"
+ flat :: "i=>i"
+ list_add :: "i=>i"
+ hd,tl :: "i=>i"
+ drop :: "[i,i]=>i"
+
+ (* List Enumeration *)
+ "[]" :: "i" ("[]")
+ "@List" :: "is => i" ("[(_)]")
-List = Univ + "Datatype" + "intr_elim"
+ list :: "i=>i"
+
+
+datatype
+ "list(A)" = "Nil" | "Cons" ("a:A", "l: list(A)")
+
+
+translations
+ "[x, xs]" == "Cons(x, [xs])"
+ "[x]" == "Cons(x, [])"
+ "[]" == "Nil"
+
+
+rules
+
+ hd_def "hd(l) == list_case(0, %x xs.x, l)"
+ tl_def "tl(l) == list_case(Nil, %x xs.xs, l)"
+ drop_def "drop(i,l) == rec(i, l, %j r. tl(r))"
+
+ list_rec_def
+ "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
+
+ map_def "map(f,l) == list_rec(l, Nil, %x xs r. Cons(f(x), r))"
+ length_def "length(l) == list_rec(l, 0, %x xs r. succ(r))"
+ app_def "xs@ys == list_rec(xs, ys, %x xs r. Cons(x,r))"
+ rev_def "rev(l) == list_rec(l, Nil, %x xs r. r @ [x])"
+ flat_def "flat(ls) == list_rec(ls, Nil, %l ls r. l @ r)"
+ list_add_def "list_add(l) == list_rec(l, 0, %x xs r. x#+r)"
+end
--- a/src/ZF/Makefile Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/Makefile Fri Aug 12 12:51:34 1994 +0200
@@ -21,7 +21,8 @@
FILES = ROOT.ML ZF.thy ZF.ML upair.ML subset.ML pair.ML domrange.ML \
func.ML AC.thy AC.ML simpdata.ML Bool.thy Bool.ML \
Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \
- ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \
+ ind_syntax.ML add_ind_def.thy add_ind_def.ML \
+\ intr_elim.ML indrule.ML inductive.ML \
equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \
WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
@@ -29,25 +30,23 @@
OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \
Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \
Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \
- Zorn0.thy Zorn0.ML Zorn.thy Zorn.ML Nat.thy Nat.ML Fin.ML \
- List.ML ListFn.thy ListFn.ML
+ Zorn.thy Zorn.ML Nat.thy Nat.ML Finite.thy Finite.ML \
+ List.thy List.ML
-IMP_FILES = IMP/ROOT.ML IMP/Aexp.ML IMP/Aexp.thy IMP/Assign.ML IMP/Assign.thy\
- IMP/Bexp.ML IMP/Bexp.thy IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
- IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/Evala0.thy\
- IMP/Evala.ML IMP/Evala.thy IMP/Evalb0.thy IMP/Evalb.ML\
- IMP/Evalb.thy IMP/Evalc0.thy IMP/Evalc.ML IMP/Evalc.thy
+IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
+ IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy
-EX_FILES = ex/ROOT.ML ex/Acc.ML ex/Bin.ML ex/BinFn.ML ex/BinFn.thy\
- ex/BT.ML ex/BT_Fn.ML ex/BT_Fn.thy ex/Comb.ML\
- ex/Contract0.ML ex/Contract0.thy ex/CoUnit.ML ex/Data.ML\
- ex/Enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\
- ex/ListN.ML ex/LList.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\
- ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\
- ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\
- ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy \
- ex/Ntree.ML ex/Brouwer.ML \
- ex/TF.ML ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML
+EX_FILES = ex/ROOT.ML ex/misc.ML ex/Ramsey.ML ex/Ramsey.thy\
+ ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\
+ ex/twos_compl.ML ex/Bin.thy ex/Bin.ML\
+ ex/BT.thy ex/BT.ML ex/Term.thy ex/Term.ML \
+ ex/TF.thy ex/TF.ML ex/Ntree.thy ex/Ntree.ML \
+ ex/Brouwer.thy ex/Brouwer.ML \
+ ex/Data.thy ex/Data.ML ex/Enum.thy ex/Enum.ML \
+ ex/Rmap.thy ex/Rmap.ML ex/PropLog.ML ex/PropLog.thy \
+ ex/ListN.thy ex/ListN.ML ex/Acc.thy ex/Acc.ML\
+ ex/Comb.thy ex/Comb.ML ex/Primrec.thy ex/Primrec.ML\
+ ex/LList.thy ex/LList.ML ex/CoUnit.thy ex/CoUnit.ML
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/ZF: $(BIN)/FOL $(FILES)
--- a/src/ZF/QPair.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/QPair.ML Fri Aug 12 12:51:34 1994 +0200
@@ -208,8 +208,8 @@
val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE);
val qsum_cs =
- ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
- addSDs [QInl_inject,QInr_inject];
+ qpair_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
+ addSDs [QInl_inject,QInr_inject];
goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A";
by (fast_tac qsum_cs 1);
--- a/src/ZF/QPair.thy Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/QPair.thy Fri Aug 12 12:51:34 1994 +0200
@@ -45,4 +45,4 @@
ML
val print_translation =
- [("QSigma", dependent_tr' ("@QSUM", " <*>"))];
+ [("QSigma", dependent_tr' ("@QSUM", "<*>"))];
--- a/src/ZF/ROOT.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/ROOT.ML Fri Aug 12 12:51:34 1994 +0200
@@ -28,8 +28,20 @@
print_depth 1;
+(*Add user sections for inductive/datatype definitions*)
+use_thy "Datatype";
+structure ThySyn = ThySynFun
+ (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype",
+ "and", "|", "<=", "domains", "intrs", "monos",
+ "con_defs", "type_intrs", "type_elims"]
+ and user_sections = [("inductive", inductive_decl ""),
+ ("coinductive", inductive_decl "Co"),
+ ("datatype", datatype_decl ""),
+ ("codatatype", datatype_decl "Co")]);
+init_thy_reader ();
+
use_thy "InfDatatype";
-use_thy "ListFn";
+use_thy "List";
(*printing functions are inherited from FOL*)
print_depth 8;
--- a/src/ZF/Univ.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/Univ.ML Fri Aug 12 12:51:34 1994 +0200
@@ -202,14 +202,14 @@
by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
val Limit_VfromE = result();
-val zero_in_Vfrom_Limit = Limit_has_0 RS ltD RS zero_in_Vfrom;
+val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom;
val [major,limiti] = goal Univ.thy
"[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)";
by (rtac ([major,limiti] MRS Limit_VfromE) 1);
by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
by (etac (limiti RS Limit_has_succ) 1);
-val singleton_in_Vfrom_Limit = result();
+val singleton_in_VLimit = result();
val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
@@ -224,7 +224,7 @@
by (etac Vfrom_UnI1 1);
by (etac Vfrom_UnI2 1);
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
-val doubleton_in_Vfrom_Limit = result();
+val doubleton_in_VLimit = result();
val [aprem,bprem,limiti] = goal Univ.thy
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> \
@@ -237,83 +237,48 @@
by (etac Vfrom_UnI1 1);
by (etac Vfrom_UnI2 1);
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
-val Pair_in_Vfrom_Limit = result();
+val Pair_in_VLimit = result();
goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)";
-by (REPEAT (ares_tac [subsetI,Pair_in_Vfrom_Limit] 1
+by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1
ORELSE eresolve_tac [SigmaE, ssubst] 1));
-val product_Vfrom_Limit = result();
+val product_VLimit = result();
-val Sigma_subset_Vfrom_Limit =
- [Sigma_mono, product_Vfrom_Limit] MRS subset_trans |> standard;
+val Sigma_subset_VLimit =
+ [Sigma_mono, product_VLimit] MRS subset_trans |> standard;
-val nat_subset_Vfrom_Limit =
+val nat_subset_VLimit =
[nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans
|> standard;
goal Univ.thy "!!i. [| n: nat; Limit(i) |] ==> n : Vfrom(A,i)";
-by (REPEAT (ares_tac [nat_subset_Vfrom_Limit RS subsetD] 1));
-val nat_into_Vfrom_Limit = result();
+by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1));
+val nat_into_VLimit = result();
(** Closure under disjoint union **)
-val zero_in_Vfrom_Limit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard;
+val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard;
goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)";
-by (REPEAT (ares_tac [nat_into_Vfrom_Limit, nat_0I, nat_succI] 1));
-val one_in_Vfrom_Limit = result();
+by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1));
+val one_in_VLimit = result();
goalw Univ.thy [Inl_def]
"!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)";
-by (REPEAT (ares_tac [zero_in_Vfrom_Limit, Pair_in_Vfrom_Limit] 1));
-val Inl_in_Vfrom_Limit = result();
+by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1));
+val Inl_in_VLimit = result();
goalw Univ.thy [Inr_def]
"!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)";
-by (REPEAT (ares_tac [one_in_Vfrom_Limit, Pair_in_Vfrom_Limit] 1));
-val Inr_in_Vfrom_Limit = result();
+by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1));
+val Inr_in_VLimit = result();
goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
-by (fast_tac (sum_cs addSIs [Inl_in_Vfrom_Limit, Inr_in_Vfrom_Limit]) 1);
-val sum_Vfrom_Limit = result();
-
-val sum_subset_Vfrom_Limit =
- [sum_mono, sum_Vfrom_Limit] MRS subset_trans |> standard;
-
-
-(** Closure under finite powerset **)
+by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
+val sum_VLimit = result();
-goal Univ.thy
- "!!i. [| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
-by (eresolve_tac [Fin_induct] 1);
-by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1);
-by (safe_tac ZF_cs);
-by (eresolve_tac [Limit_VfromE] 1);
-by (assume_tac 1);
-by (res_inst_tac [("x", "xa Un j")] exI 1);
-by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD,
- Un_least_lt]) 1);
-val Fin_Vfrom_lemma = result();
-
-goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
-by (rtac subsetI 1);
-by (dresolve_tac [Fin_Vfrom_lemma] 1);
-by (safe_tac ZF_cs);
-by (resolve_tac [Vfrom RS ssubst] 1);
-by (fast_tac (ZF_cs addSDs [ltD]) 1);
-val Fin_Vfrom_Limit = result();
-
-val Fin_subset_Vfrom_Limit =
- [Fin_mono, Fin_Vfrom_Limit] MRS subset_trans |> standard;
-
-goal Univ.thy "!!i. [| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
-by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
-by (REPEAT (ares_tac [Fin_subset_Vfrom_Limit, Sigma_subset_Vfrom_Limit,
- nat_subset_Vfrom_Limit, subset_refl] 1));
-val nat_fun_Vfrom_Limit = result();
-
-val nat_fun_subset_Vfrom_Limit =
- [Pi_mono, nat_fun_Vfrom_Limit] MRS subset_trans |> standard;
+val sum_subset_VLimit =
+ [sum_mono, sum_VLimit] MRS subset_trans |> standard;
@@ -344,8 +309,8 @@
\ <a,b> : Vfrom(A,i)";
by (etac (Transset_Pair_subset RS conjE) 1);
by (etac Transset_Vfrom 1);
-by (REPEAT (ares_tac [Pair_in_Vfrom_Limit] 1));
-val Transset_Pair_subset_Vfrom_Limit = result();
+by (REPEAT (ares_tac [Pair_in_VLimit] 1));
+val Transset_Pair_subset_VLimit = result();
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i)
@@ -368,7 +333,7 @@
by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
by (rtac (succI1 RS UnI2) 2);
by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1));
-val in_Vfrom_Limit = result();
+val in_VLimit = result();
(** products **)
@@ -384,10 +349,10 @@
val [aprem,bprem,limiti,transset] = goal Univ.thy
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \
\ a*b : Vfrom(A,i)";
-by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1);
+by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset,
limiti RS Limit_has_succ] 1));
-val prod_in_Vfrom_Limit = result();
+val prod_in_VLimit = result();
(** Disjoint sums, aka Quine ordered pairs **)
@@ -404,10 +369,10 @@
val [aprem,bprem,limiti,transset] = goal Univ.thy
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \
\ a+b : Vfrom(A,i)";
-by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1);
+by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset,
limiti RS Limit_has_succ] 1));
-val sum_in_Vfrom_Limit = result();
+val sum_in_VLimit = result();
(** function space! **)
@@ -429,10 +394,10 @@
val [aprem,bprem,limiti,transset] = goal Univ.thy
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \
\ a->b : Vfrom(A,i)";
-by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1);
+by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset,
limiti RS Limit_has_succ] 1));
-val fun_in_Vfrom_Limit = result();
+val fun_in_VLimit = result();
(*** The set Vset(i) ***)
@@ -594,21 +559,21 @@
(** Closure under unordered and ordered pairs **)
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
-by (REPEAT (ares_tac [singleton_in_Vfrom_Limit, Limit_nat] 1));
+by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1));
val singleton_in_univ = result();
goalw Univ.thy [univ_def]
"!!A a. [| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)";
-by (REPEAT (ares_tac [doubleton_in_Vfrom_Limit, Limit_nat] 1));
+by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1));
val doubleton_in_univ = result();
goalw Univ.thy [univ_def]
"!!A a. [| a: univ(A); b: univ(A) |] ==> <a,b> : univ(A)";
-by (REPEAT (ares_tac [Pair_in_Vfrom_Limit, Limit_nat] 1));
+by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1));
val Pair_in_univ = result();
goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)";
-by (rtac (Limit_nat RS product_Vfrom_Limit) 1);
+by (rtac (Limit_nat RS product_VLimit) 1);
val product_univ = result();
val Sigma_subset_univ =
@@ -616,7 +581,7 @@
goalw Univ.thy [univ_def]
"!!a b.[| <a,b> <= univ(A); Transset(A) |] ==> <a,b> : univ(A)";
-by (etac Transset_Pair_subset_Vfrom_Limit 1);
+by (etac Transset_Pair_subset_VLimit 1);
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
val Transset_Pair_subset_univ = result();
@@ -633,7 +598,7 @@
(** instances for 1 and 2 **)
goalw Univ.thy [univ_def] "1 : univ(A)";
-by (rtac (Limit_nat RS one_in_Vfrom_Limit) 1);
+by (rtac (Limit_nat RS one_in_VLimit) 1);
val one_in_univ = result();
(*unused!*)
@@ -651,38 +616,20 @@
(** Closure under disjoint union **)
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
-by (etac (Limit_nat RSN (2,Inl_in_Vfrom_Limit)) 1);
+by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1);
val Inl_in_univ = result();
goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
-by (etac (Limit_nat RSN (2,Inr_in_Vfrom_Limit)) 1);
+by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1);
val Inr_in_univ = result();
goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)";
-by (rtac (Limit_nat RS sum_Vfrom_Limit) 1);
+by (rtac (Limit_nat RS sum_VLimit) 1);
val sum_univ = result();
val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans |> standard;
-(** Closure under finite powerset **)
-
-goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)";
-by (rtac (Limit_nat RS Fin_Vfrom_Limit) 1);
-val Fin_univ = result();
-
-val Fin_subset_univ = [Fin_mono, Fin_univ] MRS subset_trans |> standard;
-
-goalw Univ.thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
-by (etac (Limit_nat RSN (2,nat_fun_Vfrom_Limit)) 1);
-val nat_fun_univ = result();
-
-val nat_fun_subset_univ = [Pi_mono, nat_fun_univ] MRS subset_trans |> standard;
-
-goal Univ.thy "!!f. [| f: n -> B; B <= univ(A); n : nat |] ==> f : univ(A)";
-by (REPEAT (ares_tac [nat_fun_subset_univ RS subsetD] 1));
-val nat_fun_into_univ = result();
-
(** Closure under binary union -- use Un_least **)
(** Closure under Collect -- use (Collect_subset RS subset_trans) **)
(** Closure under RepFun -- use RepFun_subset **)
--- a/src/ZF/Univ.thy Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/Univ.thy Fri Aug 12 12:51:34 1994 +0200
@@ -6,9 +6,12 @@
The cumulative hierarchy and a small universe for recursive types
Standard notation for Vset(i) is V(i), but users might want V for a variable
+
+NOTE: univ(A) could be a translation; would simplify many proofs!
+ But Ind_Syntax.univ refers to the constant "univ"
*)
-Univ = Arith + Sum + Fin + "mono" +
+Univ = Arith + Sum + "mono" +
consts
Vfrom :: "[i,i]=>i"
Vset :: "i=>i"
--- a/src/ZF/ZF.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/ZF.ML Fri Aug 12 12:51:34 1994 +0200
@@ -10,69 +10,70 @@
signature ZF_LEMMAS =
sig
- val ballE : thm
- val ballI : thm
- val ball_cong : thm
- val ball_simp : thm
- val ball_tac : int -> tactic
- val bexCI : thm
- val bexE : thm
- val bexI : thm
- val bex_cong : thm
- val bspec : thm
- val CollectD1 : thm
- val CollectD2 : thm
- val CollectE : thm
- val CollectI : thm
+ val ballE : thm
+ val ballI : thm
+ val ball_cong : thm
+ val ball_simp : thm
+ val ball_tac : int -> tactic
+ val bexCI : thm
+ val bexE : thm
+ val bexI : thm
+ val bex_cong : thm
+ val bspec : thm
+ val CollectD1 : thm
+ val CollectD2 : thm
+ val CollectE : thm
+ val CollectI : thm
val Collect_cong : thm
- val emptyE : thm
+ val emptyE : thm
val empty_subsetI : thm
val equalityCE : thm
val equalityD1 : thm
val equalityD2 : thm
- val equalityE : thm
- val equalityI : thm
+ val equalityE : thm
+ val equalityI : thm
val equality_iffI : thm
- val equals0D : thm
- val equals0I : thm
+ val equals0D : thm
+ val equals0I : thm
val ex1_functional : thm
- val InterD : thm
- val InterE : thm
- val InterI : thm
- val Inter_iff : thm
- val INT_E : thm
- val INT_I : thm
- val INT_cong : thm
- val lemmas_cs : claset
- val PowD : thm
- val PowI : thm
- val RepFunE : thm
- val RepFunI : thm
+ val InterD : thm
+ val InterE : thm
+ val InterI : thm
+ val Inter_iff : thm
+ val INT_E : thm
+ val INT_I : thm
+ val INT_cong : thm
+ val lemmas_cs : claset
+ val PowD : thm
+ val PowI : thm
+ val RepFunE : thm
+ val RepFunI : thm
val RepFun_eqI : thm
val RepFun_cong : thm
val RepFun_iff : thm
- val ReplaceE : thm
- val ReplaceE2 : thm
- val ReplaceI : thm
+ val ReplaceE : thm
+ val ReplaceE2 : thm
+ val ReplaceI : thm
val Replace_iff : thm
val Replace_cong : thm
- val rev_ballE : thm
- val rev_bspec : thm
+ val rev_ballE : thm
+ val rev_bspec : thm
val rev_subsetD : thm
val separation : thm
val setup_induction : thm
val set_mp_tac : int -> tactic
- val subsetCE : thm
- val subsetD : thm
- val subsetI : thm
+ val subsetCE : thm
+ val subsetD : thm
+ val subsetI : thm
val subset_iff : thm
val subset_refl : thm
val subset_trans : thm
- val UnionE : thm
- val UnionI : thm
- val UN_E : thm
- val UN_I : thm
- val UN_cong : thm
+ val UnionE : thm
+ val UnionI : thm
+ val Union_in_Pow : thm
+ val UN_E : thm
+ val UN_I : thm
+ val UN_cong : thm
end;
@@ -479,6 +480,11 @@
CollectE, emptyE]
addEs [rev_ballE, InterD, make_elim InterD, subsetD, subsetCE];
+(*Lemma for the inductive definition in Zorn.thy*)
+val Union_in_Pow = prove_goal ZF.thy
+ "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"
+ (fn _ => [fast_tac lemmas_cs 1]);
+
end;
open ZF_Lemmas;
--- a/src/ZF/ZF.thy Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/ZF.thy Fri Aug 12 12:51:34 1994 +0200
@@ -91,11 +91,11 @@
"`" :: "[i, i] => i" (infixl 90) (*function application*)
(*Except for their translations, * and -> are right and ~: left associative infixes*)
- " *" :: "[i, i] => i" ("(_ */ _)" [81, 80] 80) (*Cartesian product*)
+ "*" :: "[i, i] => i" ("(_ */ _)" [81, 80] 80) (*Cartesian product*)
"Int" :: "[i, i] => i" (infixl 70) (*binary intersection*)
"Un" :: "[i, i] => i" (infixl 65) (*binary union*)
"-" :: "[i, i] => i" (infixl 65) (*set difference*)
- " ->" :: "[i, i] => i" ("(_ ->/ _)" [61, 60] 60) (*function space*)
+ "->" :: "[i, i] => i" ("(_ ->/ _)" [61, 60] 60) (*function space*)
"<=" :: "[i, i] => o" (infixl 50) (*subset relation*)
":" :: "[i, i] => o" (infixl 50) (*membership relation*)
"~:" :: "[i, i] => o" ("(_ ~:/ _)" [50, 51] 50) (*negated membership relation*)
@@ -215,6 +215,6 @@
(* 'Dependent' type operators *)
val print_translation =
- [("Pi", dependent_tr' ("@PROD", " ->")),
- ("Sigma", dependent_tr' ("@SUM", " *"))];
+ [("Pi", dependent_tr' ("@PROD", "->")),
+ ("Sigma", dependent_tr' ("@SUM", "*"))];
--- a/src/ZF/Zorn.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/Zorn.ML Fri Aug 12 12:51:34 1994 +0200
@@ -3,30 +3,52 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Conclusion to proofs from the paper
+Proofs from the paper
Abrial & Laffitte,
Towards the Mechanization of the Proofs of Some
Classical Theorems of Set Theory.
*)
+open Zorn;
-structure Zorn = Inductive_Fun
- (val thy = Zorn0.thy |> add_consts [("TFin", "[i,i]=>i", NoSyn)]
- val thy_name = "Zorn"
- val rec_doms = [("TFin","Pow(S)")]
- val sintrs = ["[| x : TFin(S,next); next: increasing(S) \
-\ |] ==> next`x : TFin(S,next)",
- "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"]
- val monos = [Pow_mono]
- val con_defs = []
- val type_intrs = [next_bounded, Union_in_Pow]
- val type_elims = []);
+(*** Section 1. Mathematical Preamble ***)
+
+goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
+by (fast_tac ZF_cs 1);
+val Union_lemma0 = result();
+
+goal ZF.thy
+ "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
+by (fast_tac ZF_cs 1);
+val Inter_lemma0 = result();
+
+
+(*** Section 2. The Transfinite Construction ***)
+
+goalw Zorn.thy [increasing_def]
+ "!!f A. f: increasing(A) ==> f: Pow(A)->Pow(A)";
+by (eresolve_tac [CollectD1] 1);
+val increasingD1 = result();
+
+goalw Zorn.thy [increasing_def]
+ "!!f A. [| f: increasing(A); x<=A |] ==> x <= f`x";
+by (eresolve_tac [CollectD2 RS spec RS mp] 1);
+by (assume_tac 1);
+val increasingD2 = result();
+
+(*????????????????????????????????????????????????????????????????
+goal Zorn.thy
+ "!!next S. [| X : Pow(S); next: increasing(S) |] ==> next`X : Pow(S)";
+by (eresolve_tac [increasingD1 RS apply_type] 1);
+by (assume_tac 1);
+val next_bounded = result();
+*)
(*Introduction rules*)
-val [TFin_nextI, Pow_TFin_UnionI] = Zorn.intrs;
+val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs;
val TFin_UnionI = PowI RS Pow_TFin_UnionI;
-val TFin_is_subset = Zorn.dom_subset RS subsetD RS PowD;
+val TFin_is_subset = TFin.dom_subset RS subsetD RS PowD;
(** Structural induction on TFin(S,next) **)
@@ -36,7 +58,7 @@
\ !!x. [| x : TFin(S,next); P(x); next: increasing(S) |] ==> P(next`x); \
\ !!Y. [| Y <= TFin(S,next); ALL y:Y. P(y) |] ==> P(Union(Y)) \
\ |] ==> P(n)";
-by (rtac (major RS Zorn.induct) 1);
+by (rtac (major RS TFin.induct) 1);
by (ALLGOALS (fast_tac (ZF_cs addIs prems)));
val TFin_induct = result();
@@ -240,7 +262,7 @@
by (resolve_tac [refl] 2);
by (asm_full_simp_tac
(ZF_ss addsimps [subset_refl RS TFin_UnionI RS
- (Zorn.dom_subset RS subsetD)]
+ (TFin.dom_subset RS subsetD)]
setloop split_tac [expand_if]) 1);
by (eresolve_tac [choice_not_equals RS notE] 1);
by (REPEAT (assume_tac 1));
--- a/src/ZF/Zorn.thy Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/Zorn.thy Fri Aug 12 12:51:34 1994 +0200
@@ -1,3 +1,51 @@
-(*Dummy theory to document dependencies *)
+(* Title: ZF/Zorn.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Based upon the article
+ Abrial & Laffitte,
+ Towards the Mechanization of the Proofs of Some
+ Classical Theorems of Set Theory.
+
+Union_in_Pow is proved in ZF.ML
+*)
+
+Zorn = OrderArith + AC + "inductive" +
+
+consts
+ Subset_rel :: "i=>i"
+ increasing :: "i=>i"
+ chain, maxchain :: "i=>i"
+ super :: "[i,i]=>i"
+
+rules
+ Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
+ increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
-Zorn = Zorn0
+ chain_def "chain(A) == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
+ super_def "super(A,c) == {d: chain(A). c<=d & c~=d}"
+ maxchain_def "maxchain(A) == {c: chain(A). super(A,c)=0}"
+
+
+(** We could make the inductive definition conditional on next: increasing(S)
+ but instead we make this a side-condition of an introduction rule. Thus
+ the induction rule lets us assume that condition! Many inductive proofs
+ are therefore unconditional.
+**)
+consts
+ "TFin" :: "[i,i]=>i"
+
+inductive
+ domains "TFin(S,next)" <= "Pow(S)"
+ intrs
+ nextI "[| x : TFin(S,next); next: increasing(S) \
+\ |] ==> next`x : TFin(S,next)"
+
+ Pow_UnionI "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
+
+ monos "[Pow_mono]"
+ con_defs "[increasing_def]"
+ type_intrs "[CollectD1 RS apply_funtype, Union_in_Pow]"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/add_ind_def.ML Fri Aug 12 12:51:34 1994 +0200
@@ -0,0 +1,267 @@
+(* Title: ZF/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
+*)
+
+signature FP = (** Description of a fixed point operator **)
+ sig
+ val oper : term (*fixed point operator*)
+ val bnd_mono : term (*monotonicity predicate*)
+ val bnd_monoI : thm (*intro rule for bnd_mono*)
+ val subs : thm (*subset theorem for fp*)
+ val Tarski : thm (*Tarski's fixed point theorem*)
+ val induct : thm (*induction/coinduction rule*)
+ end;
+
+signature PR = (** Description of a Cartesian product **)
+ sig
+ val sigma : term (*Cartesian product operator*)
+ val pair : term (*pairing operator*)
+ val split_const : term (*splitting operator*)
+ val fsplit_const : term (*splitting operator for formulae*)
+ val pair_iff : thm (*injectivity of pairing, using <->*)
+ val split_eq : thm (*equality rule for split*)
+ val fsplitI : thm (*intro rule for fsplit*)
+ val fsplitD : thm (*destruct rule for fsplit*)
+ val fsplitE : thm (*elim rule for fsplit*)
+ end;
+
+signature SU = (** Description of a disjoint sum **)
+ sig
+ val sum : term (*disjoint sum operator*)
+ val inl : term (*left injection*)
+ val inr : term (*right injection*)
+ val elim : term (*case operator*)
+ val case_inl : thm (*inl equality rule for case*)
+ val case_inr : thm (*inr equality rule for case*)
+ val inl_iff : thm (*injectivity of inl, using <->*)
+ val inr_iff : thm (*injectivity of inr, using <->*)
+ val distinct : thm (*distinctness of inl, inr using <->*)
+ val distinct' : thm (*distinctness of inr, inl using <->*)
+ end;
+
+signature ADD_INDUCTIVE_DEF =
+ sig
+ val add_fp_def_i : term list * term list * term list -> theory -> theory
+ val add_fp_def : (string*string) list * string list -> theory -> theory
+ val add_constructs_def :
+ string list * ((string*typ*mixfix) *
+ string * term list * term list) list list ->
+ theory -> theory
+ end;
+
+
+
+(*Declares functions to add fixedpoint/constructor defs to a theory*)
+functor Add_inductive_def_Fun
+ (structure Fp: FP and Pr : PR and Su : SU) : ADD_INDUCTIVE_DEF =
+struct
+open Logic Ind_Syntax;
+
+(*internal version*)
+fun add_fp_def_i (rec_tms, domts, 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 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,recT) => 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";
+
+ 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 $ (Free(z',iT)) $ (#1 (rule_concl intr))
+ in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
+
+ val dom_sum = fold_bal (app Su.sum) domts;
+
+ (*The Part(A,h) terms -- compose injections to make h*)
+ fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
+ | mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h);
+
+ (*Access to balanced disjoint sums via injections*)
+ val parts =
+ map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)
+ (length rec_tms));
+
+ (*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_abs = absfree(X', iT,
+ mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
+
+ val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
+
+ 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 [(Free(X',iT),big_rec_tm)]) parts));
+
+ in thy |> add_defns_i axpairs end
+
+
+(*external, string-based version; needed?*)
+fun add_fp_def (rec_doms, sintrs) thy =
+ let val sign = sign_of thy;
+ val rec_tms = map (readtm sign iT o fst) rec_doms
+ and domts = map (readtm sign iT o snd) rec_doms
+ val intr_tms = map (readtm sign propT) sintrs
+ in add_fp_def_i (rec_tms, domts, intr_tms) thy end
+
+
+(*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 (app Pr.pair) args;
+
+ fun mk_inject n k u = access_bal(ap Su.inl, ap Su.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 Pr.split_const free (map (#2 o dest_Free) args)
+ in fold_bal (app Su.elim) (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 Su.elim) (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_defns_i axpairs end;
+end;
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/add_ind_def.thy Fri Aug 12 12:51:34 1994 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+add_ind_def = Fixedpt + "ind_syntax"
--- a/src/ZF/constructor.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/constructor.ML Fri Aug 12 12:51:34 1994 +0200
@@ -3,39 +3,21 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Constructor function module -- for Datatype Definitions
-
-Defines constructors and a case-style eliminator (no primitive recursion)
-
-Features:
-* least or greatest fixedpoints
-* user-specified product and sum constructions
-* mutually recursive datatypes
-* recursion over arbitrary monotone operators
-* flexible: can derive any reasonable set of introduction rules
-* automatically constructs a case analysis operator (but no recursion op)
-* efficient treatment of large declarations (e.g. 60 constructors)
+Constructor function module -- for (Co)Datatype Definitions
*)
-(** STILL NEEDS: some treatment of recursion **)
-
-signature CONSTRUCTOR =
+signature CONSTRUCTOR_ARG =
sig
- val thy : theory (*parent theory*)
- val thy_name : string (*name of generated theory*)
- val rec_specs : (string * string * (string list * string * mixfix)list) list
- (*recursion ops, types, domains, constructors*)
- val rec_styp : string (*common type of all recursion ops*)
- val sintrs : string list (*desired introduction rules*)
- val monos : thm list (*monotonicity of each M operator*)
- val type_intrs : thm list (*type-checking intro rules*)
- val type_elims : thm list (*type-checking elim rules*)
+ val thy : theory (*parent containing constructor defs*)
+ val big_rec_name : string (*name of mutually recursive set*)
+ val con_ty_lists : ((string*typ*mixfix) *
+ string * term list * term list) list list
+ (*description of constructors*)
end;
signature CONSTRUCTOR_RESULT =
sig
- val con_thy : theory (*theory defining the constructors*)
- val con_defs : thm list (*definitions made in con_thy*)
+ val con_defs : thm list (*definitions made in thy*)
val case_eqns : thm list (*equations for case operator*)
val free_iffs : thm list (*freeness rewrite rules*)
val free_SEs : thm list (*freeness destruct rules*)
@@ -43,140 +25,35 @@
end;
-functor Constructor_Fun (structure Const: CONSTRUCTOR and
+(*Proves theorems relating to constructors*)
+functor Constructor_Fun (structure Const: CONSTRUCTOR_ARG and
Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
struct
-open Logic Const;
-
-val dummy = writeln"Defining the constructor functions...";
-
-val case_name = "f"; (*name for case variables*)
-
-(** Extract basic information from arguments **)
-
-val sign = sign_of thy;
-val rdty = typ_of o read_ctyp sign;
-
-val rec_names = map #1 rec_specs;
-
-val dummy = assert_all Syntax.is_identifier rec_names
- (fn a => "Name of recursive set not an identifier: " ^ a);
-
-(*Expands multiple constant declarations*)
-fun flatten_consts ((names, typ, mfix) :: cs) =
- let fun mk_const name = (name, typ, mfix)
- in (map mk_const names) @ (flatten_consts cs) end
- | flatten_consts [] = [];
-
-(*Parse type string of constructor*)
-fun read_typ (names, st, mfix) = (names, rdty st, mfix);
-
-(*Constructors with types and arguments*)
-fun mk_con_ty_list cons_pairs =
- let fun mk_con_ty (id, T, syn) =
- let val args = mk_frees "xa" (binder_types T);
- val name = const_name id syn;
- (* because of mixfix annotations the internal name
- can be different from 'id' *)
- in (name, T, args) end;
-
- fun pairtypes c = flatten_consts [read_typ c];
- in map mk_con_ty (flat (map pairtypes cons_pairs)) end;
-
-val con_ty_lists = map (mk_con_ty_list o #3) rec_specs;
-
-(** Define the constructors **)
-
-(*We identify 0 (the empty set) with the empty tuple*)
-fun mk_tuple [] = Const("0",iT)
- | mk_tuple args = foldr1 (app Pr.pair) args;
+open Logic Const Ind_Syntax;
-fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k;
-
-val npart = length rec_names; (*number of mutually recursive parts*)
-
-(*Make constructor definition*)
-fun mk_con_defs (kpart, con_ty_list) =
- let val ncon = length con_ty_list (*number of constructors*)
- fun mk_def ((a,T,args), kcon) = (*kcon = index of this constructor*)
- mk_defpair sign
- (list_comb (Const(a,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 Pr.split_const free (map (#2 o dest_Free) args)
- in fold_bal (app Su.elim) (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 ((a,T,args), (opno,cases)) =
- if Syntax.is_identifier a
- then (opno,
- (Free(case_name ^ "_" ^ a, 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) con_ty_lists) ---> (iT-->iT);
-
-val big_rec_name = space_implode "_" rec_names;
-
+(*1st element is the case definition; others are the constructors*)
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 sign
- (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists));
-
-(** Build the new theory **)
-
-val axpairs =
- big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists));
-
-val const_decs = flatten_consts
- (([big_case_name], big_case_typ, NoSyn) ::
- (big_rec_name ins rec_names, rdty rec_styp, NoSyn) ::
- map read_typ (flat (map #3 rec_specs)));
-
-val con_thy = thy
- |> add_consts_i const_decs
- |> add_axioms_i axpairs
- |> add_thyname (big_rec_name ^ "_Constructors");
-
-(*1st element is the case definition; others are the constructors*)
-val con_defs = map (get_axiom con_thy o #1) axpairs;
+val con_defs = get_def thy big_case_name ::
+ map (get_def thy o #2) (flat con_ty_lists);
(** Prove the case theorem **)
+(*Get the case term from its definition*)
+val Const("==",_) $ big_case_tm $ _ =
+ hd con_defs |> rep_thm |> #prop |> unvarify;
+
+val (_, big_case_args) = strip_comb big_case_tm;
+
(*Each equation has the form
rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
-fun mk_case_equation ((a,T,args), case_free) =
- mk_tprop
- (eq_const $ (big_case_tm $ (list_comb (Const(a,T), args)))
- $ (list_comb (case_free, args)));
+fun mk_case_equation (((id,T,syn), name, args, prems), case_free) =
+ mk_tprop (eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
+ $ (list_comb (case_free, args))) ;
val case_trans = hd con_defs RS def_trans;
-(*proves a single case equation*)
+(*Proves a single case equation. Could use simp_tac, but it's slower!*)
fun case_tacsf con_def _ =
[rewtac con_def,
rtac case_trans 1,
@@ -185,7 +62,7 @@
Su.case_inr RS trans] 1)];
fun prove_case_equation (arg,con_def) =
- prove_term (sign_of con_thy) []
+ prove_term (sign_of thy) []
(mk_case_equation arg, case_tacsf con_def);
val free_iffs =
@@ -199,7 +76,7 @@
(*Typical theorems have the form ~con1=con2, con1=con2==>False,
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
fun mk_free s =
- prove_goalw con_thy con_defs s
+ prove_goalw thy con_defs s
(fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]);
val case_eqns = map prove_case_equation
--- a/src/ZF/ind_syntax.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/ind_syntax.ML Fri Aug 12 12:51:34 1994 +0200
@@ -6,9 +6,13 @@
Abstract Syntax functions for Inductive Definitions
*)
-
-(*Make a definition, lhs==rhs, checking that vars on lhs contain *)
-fun mk_defpair sign (lhs, rhs) =
+(*The structure protects these items from redeclaration (somewhat!). The
+ datatype definitions in theory files refer to these items by name!
+*)
+structure Ind_Syntax =
+struct
+(*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*)
+fun mk_defpair (lhs, rhs) =
let val Const(name, _) = head_of lhs
val dummy = assert (term_vars rhs subset term_vars lhs
andalso
@@ -20,6 +24,8 @@
("Extra variables on RHS in definition of " ^ name)
in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
+fun get_def thy s = get_axiom thy (s^"_def");
+
fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
(*export to Pure/library? *)
@@ -64,7 +70,6 @@
fun mk_all_imp (A,P) =
all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
-
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
@@ -85,14 +90,62 @@
(*Read an assumption in the given theory*)
fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
+fun readtm sign T a =
+ read_cterm sign (a,T) |> term_of
+ handle ERROR => error ("The error above occurred for " ^ a);
+
+(*Skipping initial blanks, find the first identifier*)
+fun scan_to_id s =
+ s |> explode |> take_prefix is_blank |> #2 |> Lexicon.scan_id |> #1
+ handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
+
+fun is_backslash c = c = "\\";
+
+(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
+ Does not handle the \ddd form; no error checking*)
+fun escape [] = []
+ | escape cs = (case take_prefix (not o is_backslash) cs of
+ (front, []) => front
+ | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
+ | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
+ | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
+ | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
+ | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
+ | (front, b::c::rest) =>
+ if is_blank c (*remove any further blanks and the following \ *)
+ then front @ escape (tl (snd (take_prefix is_blank rest)))
+ else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
+
+(*Remove the first and last charaters -- presumed to be quotes*)
+val trim = implode o escape o rev o tl o rev o tl o explode;
+
+(*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";
+
+
+(*Inverse of varifyT. Move to Pure/type.ML?*)
+fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
+ | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
+ | unvarifyT T = T;
+
+(*Inverse of varify. Move to Pure/logic.ML?*)
+fun unvarify (Const(a,T)) = Const(a, unvarifyT T)
+ | unvarify (Var((a,0), T)) = Free(a, unvarifyT T)
+ | unvarify (Var(ixn,T)) = Var(ixn, unvarifyT T) (*non-zero index!*)
+ | unvarify (Abs (a,T,body)) = Abs (a, unvarifyT T, unvarify body)
+ | unvarify (f$t) = unvarify f $ unvarify t
+ | unvarify t = t;
+
+
(*Make distinct individual variables a1, a2, a3, ..., an. *)
fun mk_frees a [] = []
| mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
-(*Used by 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];
-
(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) =
@@ -118,27 +171,55 @@
fun gen_make_elim elim_rls rl =
standard (tryres (rl, elim_rls @ [revcut_rl]));
-(** For constructor.ML **)
+(** For datatype definitions **)
+
+fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
+ | dest_mem _ = error "Constructor specifications must have the form x:A";
+
+(*read a constructor specification*)
+fun read_construct sign (id, sprems, syn) =
+ let val prems = map (readtm sign oT) sprems
+ val args = map (#1 o dest_mem) prems
+ val T = (map (#2 o dest_Free) args) ---> iT
+ handle TERM _ => error
+ "Bad variable in constructor specification"
+ val name = const_name id syn (*handle infix constructors*)
+ in ((id,T,syn), name, args, prems) end;
+
+val read_constructs = map o map o read_construct;
-(*Avoids duplicate definitions by removing constants already declared mixfix*)
-fun remove_mixfixes None decs = decs
- | remove_mixfixes (Some sext) decs =
- let val mixtab = Symtab.st_of_declist(Syntax.constants sext, Symtab.null)
- fun is_mix c = case Symtab.lookup(mixtab,c) of
- None=>false | Some _ => true
- in map (fn (cs,styp)=> (filter_out is_mix cs, styp)) decs
- end;
+(*convert constructor specifications into introduction rules*)
+fun mk_intr_tms (rec_tm, constructs) =
+ let fun mk_intr ((id,T,syn), name, args, prems) =
+ Logic.list_implies
+ (map mk_tprop prems,
+ mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm))
+ in map mk_intr constructs end;
+
+val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
-fun ext_constants None = []
- | ext_constants (Some sext) = Syntax.constants sext;
+val Un = Const("op Un", [iT,iT]--->iT)
+and empty = Const("0", iT)
+and univ = Const("univ", iT-->iT)
+and quniv = Const("quniv", iT-->iT);
+(*Make a datatype's domain: form the union of its set parameters*)
+fun union_params rec_tm =
+ let val (_,args) = strip_comb rec_tm
+ in case (filter (fn arg => type_of arg = iT) args) of
+ [] => empty
+ | iargs => fold_bal (app Un) iargs
+ end;
+
+fun data_domain rec_tms =
+ replicate (length rec_tms) (univ $ union_params (hd rec_tms));
+
+fun Codata_domain rec_tms =
+ replicate (length rec_tms) (quniv $ union_params (hd rec_tms));
(*Could go to FOL, but it's hardly general*)
-val [def] = goal IFOL.thy "a==b ==> a=c <-> c=b";
-by (rewtac def);
-by (rtac iffI 1);
-by (REPEAT (etac sym 1));
-val def_swap_iff = result();
+val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
+ (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
val def_trans = prove_goal IFOL.thy "[| f==g; g(a)=b |] ==> f(a)=b"
(fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
@@ -147,3 +228,5 @@
val refl_thin = prove_goal IFOL.thy "!!P. [| a=a; P |] ==> P"
(fn _ => [assume_tac 1]);
+end;
+
--- a/src/ZF/indrule.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/indrule.ML Fri Aug 12 12:51:34 1994 +0200
@@ -1,7 +1,7 @@
(* Title: ZF/indrule.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1994 University of Cambridge
Induction rule module -- for Inductive/Coinductive Definitions
@@ -15,19 +15,25 @@
end;
-functor Indrule_Fun (structure Ind: INDUCTIVE and
- Pr: PR and Intr_elim: INTR_ELIM) : INDRULE =
+functor Indrule_Fun
+ (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
+ and Pr: PR and Intr_elim: INTR_ELIM) : INDRULE =
struct
-open Logic Ind Intr_elim;
+open Logic Ind_Syntax Inductive Intr_elim;
+
+val sign = sign_of thy;
-val dummy = writeln "Proving the induction rules...";
+val (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
+
+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 prove = prove_term (sign_of Intr_elim.thy);
-
val big_rec_def::part_rec_defs = Intr_elim.defs;
(*Used to make induction rules;
@@ -63,7 +69,7 @@
val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;
val quant_induct =
- prove part_rec_defs
+ prove_term sign part_rec_defs
(list_implies (ind_prems, mk_tprop (mk_all_imp(big_rec_tm,pred))),
fn prems =>
[rtac (impI RS allI) 1,
@@ -112,7 +118,7 @@
and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);
val lemma = (*makes the link between the two induction rules*)
- prove part_rec_defs
+ prove_term sign part_rec_defs
(mk_implies (induct_concl,mutual_induct_concl),
fn prems =>
[cut_facts_tac prems 1,
@@ -139,7 +145,7 @@
i THEN mutual_ind_tac prems (i-1);
val mutual_induct_fsplit =
- prove []
+ prove_term sign []
(list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
mutual_induct_concl),
fn prems =>
--- a/src/ZF/inductive.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/inductive.ML Fri Aug 12 12:51:34 1994 +0200
@@ -3,15 +3,17 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Inductive Definitions for Zermelo-Fraenkel Set Theory
+(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory
-Uses least fixedpoints with standard products and sums
+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
structure Lfp =
struct
val oper = Const("lfp", [iT,iT-->iT]--->iT)
@@ -48,16 +50,179 @@
val distinct = Inl_Inr_iff
val distinct' = Inr_Inl_iff
end;
+end;
-functor Inductive_Fun (Ind: INDUCTIVE) : sig include INTR_ELIM INDRULE 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 Ind=Ind and Fp=Lfp and
+ Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and
Pr=Standard_Prod and Su=Standard_Sum);
-structure Indrule = Indrule_Fun (structure Ind=Ind and
+structure Indrule = Indrule_Fun (structure Inductive=Inductive and
Pr=Standard_Prod and Intr_elim=Intr_elim);
open Intr_elim Indrule
end;
+
+structure Ind = Add_inductive_def_Fun
+ (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
+
+
+signature INDUCTIVE_STRING =
+ sig
+ val thy_name : string (*name of the new theory*)
+ val rec_doms : (string*string) list (*recursion terms and their domains*)
+ 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 iT o #1) rec_doms
+ and domts = map (readtm sign iT o #2) rec_doms
+ and intr_tms = map (readtm sign propT) sintrs;
+ val thy = thy |> Ind.add_fp_def_i(rec_tms, domts, intr_tms)
+ |> add_thyname thy_name);
+
+
+
+local open Ind_Syntax
+in
+structure Gfp =
+ struct
+ val oper = Const("gfp", [iT,iT-->iT]--->iT)
+ val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT)
+ val bnd_monoI = bnd_monoI
+ val subs = def_gfp_subset
+ val Tarski = def_gfp_Tarski
+ val induct = def_Collect_coinduct
+ end;
+
+structure Quine_Prod =
+ struct
+ val sigma = Const("QSigma", [iT, iT-->iT]--->iT)
+ val pair = Const("QPair", [iT,iT]--->iT)
+ val split_const = Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
+ val fsplit_const = Const("qfsplit", [[iT,iT]--->oT, iT]--->oT)
+ val pair_iff = QPair_iff
+ val split_eq = qsplit
+ val fsplitI = qfsplitI
+ val fsplitD = qfsplitD
+ val fsplitE = qfsplitE
+ end;
+
+structure Quine_Sum =
+ struct
+ val sum = Const("op <+>", [iT,iT]--->iT)
+ val inl = Const("QInl", iT-->iT)
+ val inr = Const("QInr", iT-->iT)
+ val elim = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
+ val case_inl = qcase_QInl
+ val case_inr = qcase_QInr
+ val inl_iff = QInl_iff
+ val inr_iff = QInr_iff
+ val distinct = QInl_QInr_iff
+ val distinct' = QInr_QInl_iff
+ end;
+end;
+
+
+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 and
+ Pr=Quine_Prod and Su=Quine_Sum);
+
+open Intr_elim
+val coinduct = raw_induct
+end;
+
+
+structure CoInd =
+ Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
+
+
+(*For upwards compatibility: can be called directly from ML*)
+functor CoInductive_Fun
+ (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
+ : sig include INTR_ELIM COINDRULE end =
+CoInd_section_Fun
+ (open Inductive Ind_Syntax
+ val sign = sign_of thy;
+ val rec_tms = map (readtm sign iT o #1) rec_doms
+ and domts = map (readtm sign iT o #2) rec_doms
+ and intr_tms = map (readtm sign propT) sintrs;
+ val thy = thy |> CoInd.add_fp_def_i(rec_tms, domts, intr_tms)
+ |> add_thyname thy_name);
+
+
+
+(*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 (((((domains: (string*string) list, ipairs),
+ monos), con_defs), type_intrs), type_elims) =
+ let val big_rec_name = space_implode "_"
+ (map (scan_to_id o trim o #1) domains)
+ and srec_tms = mk_list (map #1 domains)
+ and sdoms = mk_list (map #2 domains)
+ 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 rec_tms\t= map (readtm (sign_of thy) iT) "
+ ^ srec_tms ^ "\n\
+ \ and domts\t= map (readtm (sign_of thy) iT) "
+ ^ sdoms ^ "\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 ^ ".domts, " ^
+ stri_name ^ ".intr_tms)"
+ ,
+ "structure " ^ big_rec_name ^ " =\n\
+ \ struct\n\
+ \ val _ = writeln \"" ^ co ^
+ "Inductive definition " ^ big_rec_name ^ "\"\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\
+ \ val type_intrs\t= " ^ type_intrs ^ "\n\
+ \ val type_elims\t= " ^ type_elims ^ ");\n\n\
+ \ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
+ \ open Result\n\
+ \ end\n"
+ )
+ end
+ val domains = "domains" $$-- repeat1 (string --$$ "<=" -- !! string)
+ val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
+ fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
+ in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
+ -- optstring "type_intrs" -- optstring "type_elims"
+ >> mk_params
+ end;
--- a/src/ZF/intr_elim.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/intr_elim.ML Fri Aug 12 12:51:34 1994 +0200
@@ -1,83 +1,31 @@
(* Title: ZF/intr-elim.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1994 University of Cambridge
Introduction/elimination rule 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
*)
-signature FP = (** Description of a fixed point operator **)
- sig
- val oper : term (*fixed point operator*)
- val bnd_mono : term (*monotonicity predicate*)
- val bnd_monoI : thm (*intro rule for bnd_mono*)
- val subs : thm (*subset theorem for fp*)
- val Tarski : thm (*Tarski's fixed point theorem*)
- val induct : thm (*induction/coinduction rule*)
- end;
-
-signature PR = (** Description of a Cartesian product **)
+signature INDUCTIVE_ARG = (** Description of a (co)inductive def **)
sig
- val sigma : term (*Cartesian product operator*)
- val pair : term (*pairing operator*)
- val split_const : term (*splitting operator*)
- val fsplit_const : term (*splitting operator for formulae*)
- val pair_iff : thm (*injectivity of pairing, using <->*)
- val split_eq : thm (*equality rule for split*)
- val fsplitI : thm (*intro rule for fsplit*)
- val fsplitD : thm (*destruct rule for fsplit*)
- val fsplitE : thm (*elim rule for fsplit*)
- end;
-
-signature SU = (** Description of a disjoint sum **)
- sig
- val sum : term (*disjoint sum operator*)
- val inl : term (*left injection*)
- val inr : term (*right injection*)
- val elim : term (*case operator*)
- val case_inl : thm (*inl equality rule for case*)
- val case_inr : thm (*inr equality rule for case*)
- val inl_iff : thm (*injectivity of inl, using <->*)
- val inr_iff : thm (*injectivity of inr, using <->*)
- val distinct : thm (*distinctness of inl, inr using <->*)
- val distinct' : thm (*distinctness of inr, inl using <->*)
- end;
-
-signature INDUCTIVE = (** Description of a (co)inductive defn **)
- sig
- val thy : theory (*parent theory*)
- val thy_name : string (*name of generated theory*)
- val rec_doms : (string*string) list (*recursion ops and their domains*)
- val sintrs : string list (*desired introduction rules*)
+ 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*)
val type_intrs : thm list (*type-checking intro rules*)
val type_elims : thm list (*type-checking elim rules*)
end;
+(*internal items*)
+signature INDUCTIVE_I =
+ sig
+ val rec_tms : term list (*the recursive sets*)
+ val domts : term list (*their domains*)
+ val intr_tms : term list (*terms for the introduction rules*)
+ end;
+
signature INTR_ELIM =
sig
- val thy : theory (*new theory*)
- val thy_name : string (*name of generated theory*)
+ val thy : theory (*copy of input theory*)
val defs : thm list (*definitions made in thy*)
val bnd_mono : thm (*monotonicity for the lfp definition*)
val unfold : thm (*fixed-point equation*)
@@ -86,145 +34,36 @@
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*)
- (*internal items...*)
- val big_rec_tm : term (*the lhs of the fixedpoint defn*)
- val rec_tms : term list (*the mutually recursive sets*)
- val domts : term list (*domains of the recursive sets*)
- val intr_tms : term list (*terms for the introduction rules*)
- val rec_params : term list (*parameters of the recursion*)
+ val rec_names : string list (*names of recursive sets*)
val sumprod_free_SEs : thm list (*destruct rules for Su and Pr*)
end;
-
-functor Intr_elim_Fun (structure Ind: INDUCTIVE and
- Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
+(*prove intr/elim rules for a fixedpoint definition*)
+functor Intr_elim_Fun
+ (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
+ and Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
struct
-open Logic Ind;
-
-(*** Extract basic information from arguments ***)
-
-val sign = sign_of Ind.thy;
-
-fun rd T a =
- read_cterm sign (a,T)
- handle ERROR => error ("The error above occurred for " ^ a);
-
-val rec_names = map #1 rec_doms
-and domts = map (term_of o rd iT o #2) rec_doms;
-
-val dummy = assert_all Syntax.is_identifier rec_names
- (fn a => "Name of recursive set not an identifier: " ^ a);
-
-val dummy = assert_all (is_some o lookup_const sign) rec_names
- (fn a => "Name of recursive set not declared as constant: " ^ a);
-
-val intr_tms = map (term_of o rd propT) sintrs;
-
-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,recT) => a mem rec_names | _ => false;
-
- val dummy = assert_all intr_ok intr_sets
- (fn t => "Conclusion of rule does not name a recursive set: " ^
- Sign.string_of_term sign t);
-in
-val (Const(_,recT),rec_params) = strip_comb (hd intr_sets)
-end;
-
-val rec_hds = map (fn a=> Const(a,recT)) rec_names;
-val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
-
-val dummy = 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,[]));
+open Logic Inductive Ind_Syntax;
-val z' = mk_variant"z"
-and X' = mk_variant"X"
-and w' = mk_variant"w";
-
-(*simple error-checking in the premises*)
-fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
- error"Premises may not be conjuctive"
- | chk_prem rec_hd (Const("op :",_) $ t $ X) =
- deny (rec_hd occs t) "Recursion term on left of member symbol"
- | chk_prem rec_hd t =
- deny (rec_hd occs t) "Recursion term in side formula";
-
-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 dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
- val exfrees = term_frees intr \\ rec_params
- val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
- in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
-
-val dom_sum = fold_bal (app Su.sum) domts;
-
-(*The Part(A,h) terms -- compose injections to make h*)
-fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
- | mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h);
-
-(*Access to balanced disjoint sums via injections*)
-val parts =
- map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)
- (length rec_doms));
-
-(*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_abs = absfree(X', iT,
- mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
-
-val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
-
-val dummy = 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 rec_names = map (#1 o dest_Const o head_of) rec_tms;
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 sign)
- ((big_rec_tm, lfp_rhs) ::
- (case parts of
- [_] => [] (*no mutual recursion*)
- | _ => rec_tms ~~ (*define the sets as Parts*)
- map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
+(*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 thy =
- Ind.thy
- |> add_axioms_i axpairs
- |> add_thyname thy_name;
-val defs = map (get_axiom thy o #1) axpairs;
-
-val big_rec_def::part_rec_defs = defs;
-
-val prove = prove_term (sign_of thy);
+val sign = sign_of thy;
(********)
-val dummy = writeln "Proving monotonicity...";
+val _ = writeln " Proving monotonicity...";
+
+val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
+ big_rec_def |> rep_thm |> #prop |> unvarify;
val bnd_mono =
- prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs),
+ prove_term sign [] (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs),
fn _ =>
[rtac (Collect_subset RS bnd_monoI) 1,
REPEAT (ares_tac (basic_monos @ monos) 1)]);
@@ -234,7 +73,7 @@
val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));
(********)
-val dummy = writeln "Proving the introduction rules...";
+val _ = writeln " Proving the introduction rules...";
(*Mutual recursion: Needs subset rules for the individual sets???*)
val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];
@@ -252,22 +91,22 @@
rewrite_goals_tac con_defs,
(*Now can solve the trivial equation*)
REPEAT (rtac refl 2),
- REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
- ORELSE' hyp_subst_tac
- ORELSE' dresolve_tac rec_typechecks)),
+ REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks
+ ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
+ ORELSE' hyp_subst_tac)),
DEPTH_SOLVE (swap_res_tac (SigmaI::type_intrs) 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
+ and g rl = rl RS disjI2
in accesses_bal(f, g, asm_rl) end;
-val intrs = map (prove part_rec_defs)
+val intrs = map (prove_term sign part_rec_defs)
(intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));
(********)
-val dummy = writeln "Proving the elimination rule...";
+val _ = writeln " Proving the elimination rule...";
(*Includes rules for succ and Pair since they are common constructions*)
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0,
@@ -276,13 +115,13 @@
val sumprod_free_SEs =
map (gen_make_elim [conjE,FalseE])
- ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]
+ ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]
RL [iffD1]);
(*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))
+ ORELSE' bound_hyp_subst_tac))
THEN prune_params_tac;
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
@@ -301,5 +140,5 @@
val defs = big_rec_def::part_rec_defs;
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
+end;
-end;
--- a/src/ZF/intr_elim.thy Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/intr_elim.thy Fri Aug 12 12:51:34 1994 +0200
@@ -1,3 +1,3 @@
(*Dummy theory to document dependencies *)
-intr_elim = Fixedpt + "ind_syntax"
+intr_elim = "add_ind_def"
--- a/src/ZF/mono.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/mono.ML Fri Aug 12 12:51:34 1994 +0200
@@ -190,3 +190,8 @@
"[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
by (fast_tac (FOL_cs addIs [PQimp RS mp]) 1);
val all_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];
+
--- a/src/ZF/simpdata.ML Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/simpdata.ML Fri Aug 12 12:51:34 1994 +0200
@@ -50,9 +50,8 @@
val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
-(*To instantiate variables in typing conditions;
- to perform type checking faster than rewriting can
- NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
+(*Instantiates variables in typing conditions.
+ drawback: does not simplify conjunctions*)
fun type_auto_tac tyrls hyps = SELECT_GOAL
(DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));