# HG changeset patch # User lcp # Date 776688694 -7200 # Node ID 1957113f0d7da7aa89d37d3ca8eed18fa6bdf280 # Parent abcc438e7c27f906f71007a20283bda6792557bc installation of new inductive/datatype sections diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/CardinalArith.ML --- 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] diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/CardinalArith.thy --- 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" diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Cardinal_AC.ML --- 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(); + diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Datatype.ML --- 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; diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Datatype.thy --- 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 diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Finite.ML --- /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(); diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Finite.thy --- /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 diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/InfDatatype.ML --- 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 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; diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/InfDatatype.thy --- 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 diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/List.ML --- 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(); + diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/List.thy --- 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 diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Makefile --- 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) diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/QPair.ML --- 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); diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/QPair.thy --- 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", "<*>"))]; diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/ROOT.ML --- 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; diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Univ.ML --- 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 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 @@ \ : 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) |] ==> : 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.[| <= univ(A); Transset(A) |] ==> : 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 **) diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Univ.thy --- 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" diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/ZF.ML --- 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; diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/ZF.thy --- 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", "*"))]; diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Zorn.ML --- 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)); diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/Zorn.thy --- 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}" + 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 diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/add_ind_def.ML --- /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; + + + + diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/add_ind_def.thy --- /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" diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/constructor.ML --- 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 diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/ind_syntax.ML --- 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; + diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/indrule.ML --- 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 => diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/inductive.ML --- 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; diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/intr_elim.ML --- 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; diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/intr_elim.thy --- 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" diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/mono.ML --- 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]; + diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/simpdata.ML --- 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));