# HG changeset patch # User wenzelm # Date 1177594924 -7200 # Node ID 4cd25f1706bbb4b9cc80f48010f9367ae1d10532 # Parent 882513df24720f46f289c15afd3ac3228544ba64 removed lagacy ML files; diff -r 882513df2472 -r 4cd25f1706bb src/ZF/Datatype.ML --- a/src/ZF/Datatype.ML Thu Apr 26 15:41:49 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,105 +0,0 @@ -(* Title: ZF/Datatype.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory -*) - - -(*Typechecking rules for most datatypes involving univ*) -structure Data_Arg = - struct - val intrs = - [SigmaI, InlI, InrI, - Pair_in_univ, Inl_in_univ, Inr_in_univ, - zero_in_univ, A_into_univ, nat_into_univ, UnCI]; - - - val elims = [make_elim InlD, make_elim InrD, (*for mutual recursion*) - SigmaE, sumE]; (*allows * and + in spec*) - end; - - -structure Data_Package = - Add_datatype_def_Fun - (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP - and Su=Standard_Sum - and Ind_Package = Ind_Package - and Datatype_Arg = Data_Arg - val coind = false); - - -(*Typechecking rules for most codatatypes involving quniv*) -structure CoData_Arg = - struct - val intrs = - [QSigmaI, QInlI, QInrI, - QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, - zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI]; - - val elims = [make_elim QInlD, make_elim QInrD, (*for mutual recursion*) - QSigmaE, qsumE]; (*allows * and + in spec*) - end; - -structure CoData_Package = - Add_datatype_def_Fun - (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP - and Su=Quine_Sum - and Ind_Package = CoInd_Package - and Datatype_Arg = CoData_Arg - val coind = true); - - - -(*Simproc for freeness reasoning: compare datatype constructors for equality*) -structure DataFree = -struct - val trace = ref false; - - fun mk_new ([],[]) = Const("True",FOLogic.oT) - | mk_new (largs,rargs) = - fold_bal FOLogic.mk_conj - (map FOLogic.mk_eq (ListPair.zip (largs,rargs))); - - val datatype_ss = simpset (); - - fun proc sg ss old = - let val _ = if !trace then writeln ("data_free: OLD = " ^ - string_of_cterm (cterm_of sg old)) - else () - val (lhs,rhs) = FOLogic.dest_eq old - val (lhead, largs) = strip_comb lhs - and (rhead, rargs) = strip_comb rhs - val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; - val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; - val lcon_info = the (Symtab.lookup (ConstructorsData.get sg) lname) - handle Option => raise Match; - val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname) - handle Option => raise Match; - val new = - if #big_rec_name lcon_info = #big_rec_name rcon_info - andalso not (null (#free_iffs lcon_info)) then - if lname = rname then mk_new (largs, rargs) - else Const("False",FOLogic.oT) - else raise Match - val _ = if !trace then - writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new)) - else (); - val goal = Logic.mk_equals (old, new) - val thm = Goal.prove (Simplifier.the_context ss) [] [] goal - (fn _ => rtac iff_reflection 1 THEN - simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1) - handle ERROR msg => - (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal); - raise Match) - in SOME thm end - handle Match => NONE; - - - val conv = Simplifier.simproc (theory "ZF") "data_free" ["(x::i) = y"] proc; - -end; - - -Addsimprocs [DataFree.conv]; diff -r 882513df2472 -r 4cd25f1706bb src/ZF/Datatype.thy --- a/src/ZF/Datatype.thy Thu Apr 26 15:41:49 2007 +0200 +++ b/src/ZF/Datatype.thy Thu Apr 26 15:42:04 2007 +0200 @@ -7,9 +7,108 @@ header{*Datatype and CoDatatype Definitions*} -theory Datatype imports Inductive Univ QUniv - uses - "Tools/datatype_package.ML" - "Tools/numeral_syntax.ML" begin (*belongs to theory Bin*) +theory Datatype +imports Inductive Univ QUniv +uses "Tools/datatype_package.ML" +begin + +ML_setup {* +(*Typechecking rules for most datatypes involving univ*) +structure Data_Arg = + struct + val intrs = + [SigmaI, InlI, InrI, + Pair_in_univ, Inl_in_univ, Inr_in_univ, + zero_in_univ, A_into_univ, nat_into_univ, UnCI]; + + + val elims = [make_elim InlD, make_elim InrD, (*for mutual recursion*) + SigmaE, sumE]; (*allows * and + in spec*) + end; + + +structure Data_Package = + Add_datatype_def_Fun + (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP + and Su=Standard_Sum + and Ind_Package = Ind_Package + and Datatype_Arg = Data_Arg + val coind = false); + + +(*Typechecking rules for most codatatypes involving quniv*) +structure CoData_Arg = + struct + val intrs = + [QSigmaI, QInlI, QInrI, + QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, + zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI]; + + val elims = [make_elim QInlD, make_elim QInrD, (*for mutual recursion*) + QSigmaE, qsumE]; (*allows * and + in spec*) + end; + +structure CoData_Package = + Add_datatype_def_Fun + (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP + and Su=Quine_Sum + and Ind_Package = CoInd_Package + and Datatype_Arg = CoData_Arg + val coind = true); + + + +(*Simproc for freeness reasoning: compare datatype constructors for equality*) +structure DataFree = +struct + val trace = ref false; + + fun mk_new ([],[]) = Const("True",FOLogic.oT) + | mk_new (largs,rargs) = + fold_bal FOLogic.mk_conj + (map FOLogic.mk_eq (ListPair.zip (largs,rargs))); + + val datatype_ss = @{simpset}; + + fun proc sg ss old = + let val _ = if !trace then writeln ("data_free: OLD = " ^ + string_of_cterm (cterm_of sg old)) + else () + val (lhs,rhs) = FOLogic.dest_eq old + val (lhead, largs) = strip_comb lhs + and (rhead, rargs) = strip_comb rhs + val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; + val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; + val lcon_info = the (Symtab.lookup (ConstructorsData.get sg) lname) + handle Option => raise Match; + val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname) + handle Option => raise Match; + val new = + if #big_rec_name lcon_info = #big_rec_name rcon_info + andalso not (null (#free_iffs lcon_info)) then + if lname = rname then mk_new (largs, rargs) + else Const("False",FOLogic.oT) + else raise Match + val _ = if !trace then + writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new)) + else (); + val goal = Logic.mk_equals (old, new) + val thm = Goal.prove (Simplifier.the_context ss) [] [] goal + (fn _ => rtac iff_reflection 1 THEN + simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1) + handle ERROR msg => + (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal); + raise Match) + in SOME thm end + handle Match => NONE; + + + val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc; + +end; + + +Addsimprocs [DataFree.conv]; +*} end diff -r 882513df2472 -r 4cd25f1706bb src/ZF/Inductive.ML --- a/src/ZF/Inductive.ML Thu Apr 26 15:41:49 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,108 +0,0 @@ -(* Title: ZF/Inductive.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory - -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 -*) - -val iT = Ind_Syntax.iT -and oT = FOLogic.oT; - -structure Lfp = - struct - val oper = Const("Fixedpt.lfp", [iT,iT-->iT]--->iT) - val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT) - val bnd_monoI = bnd_monoI - val subs = def_lfp_subset - val Tarski = def_lfp_unfold - val induct = def_induct - end; - -structure Standard_Prod = - struct - val sigma = Const("Sigma", [iT, iT-->iT]--->iT) - val pair = Const("Pair", [iT,iT]--->iT) - val split_name = "split" - val pair_iff = Pair_iff - val split_eq = split - val fsplitI = splitI - val fsplitD = splitD - val fsplitE = splitE - end; - -structure Standard_CP = CartProd_Fun (Standard_Prod); - -structure Standard_Sum = - struct - val sum = Const("op +", [iT,iT]--->iT) - val inl = Const("Inl", iT-->iT) - val inr = Const("Inr", iT-->iT) - val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT) - val case_inl = case_Inl - val case_inr = case_Inr - val inl_iff = Inl_iff - val inr_iff = Inr_iff - val distinct = Inl_Inr_iff - val distinct' = Inr_Inl_iff - val free_SEs = Ind_Syntax.mk_free_SEs - [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff] - end; - - -structure Ind_Package = - Add_inductive_def_Fun - (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP - and Su=Standard_Sum val coind = false); - - -structure Gfp = - struct - val oper = Const("Fixedpt.gfp", [iT,iT-->iT]--->iT) - val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT) - val bnd_monoI = bnd_monoI - val subs = def_gfp_subset - val Tarski = def_gfp_unfold - val induct = def_Collect_coinduct - end; - -structure Quine_Prod = - struct - val sigma = Const("QPair.QSigma", [iT, iT-->iT]--->iT) - val pair = Const("QPair.QPair", [iT,iT]--->iT) - val split_name = "QPair.qsplit" - val pair_iff = QPair_iff - val split_eq = qsplit - val fsplitI = qsplitI - val fsplitD = qsplitD - val fsplitE = qsplitE - end; - -structure Quine_CP = CartProd_Fun (Quine_Prod); - -structure Quine_Sum = - struct - val sum = Const("QPair.op <+>", [iT,iT]--->iT) - val inl = Const("QPair.QInl", iT-->iT) - val inr = Const("QPair.QInr", iT-->iT) - val elim = Const("QPair.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 - val free_SEs = Ind_Syntax.mk_free_SEs - [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff] - end; - - -structure CoInd_Package = - Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP - and Su=Quine_Sum val coind = true); diff -r 882513df2472 -r 4cd25f1706bb src/ZF/Inductive.thy --- a/src/ZF/Inductive.thy Thu Apr 26 15:41:49 2007 +0200 +++ b/src/ZF/Inductive.thy Thu Apr 26 15:42:04 2007 +0200 @@ -3,6 +3,11 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge +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 *) header{*Inductive and Coinductive Definitions*} @@ -19,4 +24,102 @@ setup IndCases.setup setup DatatypeTactics.setup +ML_setup {* +val iT = Ind_Syntax.iT +and oT = FOLogic.oT; + +structure Lfp = + struct + val oper = Const("Fixedpt.lfp", [iT,iT-->iT]--->iT) + val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT) + val bnd_monoI = bnd_monoI + val subs = def_lfp_subset + val Tarski = def_lfp_unfold + val induct = def_induct + end; + +structure Standard_Prod = + struct + val sigma = Const("Sigma", [iT, iT-->iT]--->iT) + val pair = Const("Pair", [iT,iT]--->iT) + val split_name = "split" + val pair_iff = Pair_iff + val split_eq = split + val fsplitI = splitI + val fsplitD = splitD + val fsplitE = splitE + end; + +structure Standard_CP = CartProd_Fun (Standard_Prod); + +structure Standard_Sum = + struct + val sum = Const("op +", [iT,iT]--->iT) + val inl = Const("Inl", iT-->iT) + val inr = Const("Inr", iT-->iT) + val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT) + val case_inl = case_Inl + val case_inr = case_Inr + val inl_iff = Inl_iff + val inr_iff = Inr_iff + val distinct = Inl_Inr_iff + val distinct' = Inr_Inl_iff + val free_SEs = Ind_Syntax.mk_free_SEs + [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff] + end; + + +structure Ind_Package = + Add_inductive_def_Fun + (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP + and Su=Standard_Sum val coind = false); + + +structure Gfp = + struct + val oper = Const("Fixedpt.gfp", [iT,iT-->iT]--->iT) + val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT) + val bnd_monoI = bnd_monoI + val subs = def_gfp_subset + val Tarski = def_gfp_unfold + val induct = def_Collect_coinduct + end; + +structure Quine_Prod = + struct + val sigma = Const("QPair.QSigma", [iT, iT-->iT]--->iT) + val pair = Const("QPair.QPair", [iT,iT]--->iT) + val split_name = "QPair.qsplit" + val pair_iff = QPair_iff + val split_eq = qsplit + val fsplitI = qsplitI + val fsplitD = qsplitD + val fsplitE = qsplitE + end; + +structure Quine_CP = CartProd_Fun (Quine_Prod); + +structure Quine_Sum = + struct + val sum = Const("QPair.op <+>", [iT,iT]--->iT) + val inl = Const("QPair.QInl", iT-->iT) + val inr = Const("QPair.QInr", iT-->iT) + val elim = Const("QPair.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 + val free_SEs = Ind_Syntax.mk_free_SEs + [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff] + end; + + +structure CoInd_Package = + Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP + and Su=Quine_Sum val coind = true); + +*} + end diff -r 882513df2472 -r 4cd25f1706bb src/ZF/Integ/Bin.thy --- a/src/ZF/Integ/Bin.thy Thu Apr 26 15:41:49 2007 +0200 +++ b/src/ZF/Integ/Bin.thy Thu Apr 26 15:42:04 2007 +0200 @@ -16,7 +16,10 @@ header{*Arithmetic on Binary Integers*} -theory Bin imports Int Datatype begin +theory Bin +imports Int Datatype +uses "Tools/numeral_syntax.ML" +begin consts bin :: i datatype diff -r 882513df2472 -r 4cd25f1706bb src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Thu Apr 26 15:41:49 2007 +0200 +++ b/src/ZF/IsaMakefile Thu Apr 26 15:42:04 2007 +0200 @@ -28,24 +28,18 @@ FOL: @cd $(SRC)/FOL; $(ISATOOL) make FOL -$(OUT)/ZF$(ML_SUFFIX): $(OUT)/FOL$(ML_SUFFIX) AC.thy Arith.thy \ - ArithSimp.thy Bool.thy Cardinal.thy \ - CardinalArith.thy Cardinal_AC.thy \ - Datatype.ML Datatype.thy Epsilon.thy Finite.thy \ - Fixedpt.thy Inductive.ML Inductive.thy \ - InfDatatype.thy Integ/Bin.thy \ - Integ/EquivClass.thy Integ/Int.thy Integ/IntArith.thy \ - Integ/IntDiv.thy Integ/int_arith.ML \ - List.thy Main.ML Main.thy \ - Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \ - OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy \ - QPair.thy QUniv.thy ROOT.ML \ - Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \ - Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \ - Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ - Trancl.thy Univ.thy \ - WF.thy ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \ - ind_syntax.ML pair.thy simpdata.ML upair.thy +$(OUT)/ZF$(ML_SUFFIX): $(OUT)/FOL$(ML_SUFFIX) AC.thy Arith.thy \ + ArithSimp.thy Bool.thy Cardinal.thy CardinalArith.thy Cardinal_AC.thy \ + Datatype.thy Epsilon.thy Finite.thy Fixedpt.thy Inductive.thy \ + InfDatatype.thy Integ/Bin.thy Integ/EquivClass.thy Integ/Int.thy \ + Integ/IntArith.thy Integ/IntDiv.thy Integ/int_arith.ML List.thy \ + Main.thy Main_ZFC.thy Nat.thy OrdQuant.thy Order.thy OrderArith.thy \ + OrderType.thy Ordinal.thy Perm.thy QPair.thy QUniv.thy ROOT.ML Sum.thy \ + Tools/cartprod.ML Tools/datatype_package.ML Tools/ind_cases.ML \ + Tools/induct_tacs.ML Tools/inductive_package.ML \ + Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ + Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML \ + equalities.thy func.thy ind_syntax.ML pair.thy simpdata.ML upair.thy @$(ISATOOL) usedir -b -r $(OUT)/FOL ZF diff -r 882513df2472 -r 4cd25f1706bb src/ZF/Main.ML --- a/src/ZF/Main.ML Thu Apr 26 15:41:49 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ - -(* $Id$ *) - -structure Main = -struct - val thy = the_context (); -end; diff -r 882513df2472 -r 4cd25f1706bb src/ZF/Main.thy --- a/src/ZF/Main.thy Thu Apr 26 15:41:49 2007 +0200 +++ b/src/ZF/Main.thy Thu Apr 26 15:42:04 2007 +0200 @@ -5,8 +5,8 @@ theory Main imports List IntDiv CardinalArith begin (*The theory of "iterates" logically belongs to Nat, but can't go there because - primrec isn't available into after Datatype. The only theories defined - after Datatype are List and the Integ theories.*) + primrec isn't available into after Datatype.*) + subsection{* Iteration of the function @{term F} *} consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60) diff -r 882513df2472 -r 4cd25f1706bb src/ZF/Main_ZFC.ML --- a/src/ZF/Main_ZFC.ML Thu Apr 26 15:41:49 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,92 +0,0 @@ -structure Main_ZFC = -struct - val thy = the_context (); -end; - -(* legacy ML bindings *) - -(* from AC *) -val AC_Pi = thm "AC_Pi"; -val AC_ball_Pi = thm "AC_ball_Pi"; -val AC_Pi_Pow = thm "AC_Pi_Pow"; -val AC_func = thm "AC_func"; -val non_empty_family = thm "non_empty_family"; -val AC_func0 = thm "AC_func0"; -val AC_func_Pow = thm "AC_func_Pow"; -val AC_Pi0 = thm "AC_Pi0"; -val choice_Diff = thm "choice_Diff"; - -(* from Zorn *) -val Union_lemma0 = thm "Union_lemma0"; -val Inter_lemma0 = thm "Inter_lemma0"; -val increasingD1 = thm "increasingD1"; -val increasingD2 = thm "increasingD2"; -val TFin_UnionI = thm "TFin_UnionI"; -val TFin_is_subset = thm "TFin_is_subset"; -val TFin_induct = thm "TFin_induct"; -val increasing_trans = thm "increasing_trans"; -val TFin_linear_lemma1 = thm "TFin_linear_lemma1"; -val TFin_linear_lemma2 = thm "TFin_linear_lemma2"; -val TFin_subsetD = thm "TFin_subsetD"; -val TFin_subset_linear = thm "TFin_subset_linear"; -val equal_next_upper = thm "equal_next_upper"; -val equal_next_Union = thm "equal_next_Union"; -val chain_subset_Pow = thm "chain_subset_Pow"; -val super_subset_chain = thm "super_subset_chain"; -val maxchain_subset_chain = thm "maxchain_subset_chain"; -val choice_super = thm "choice_super"; -val choice_not_equals = thm "choice_not_equals"; -val Hausdorff_next_exists = thm "Hausdorff_next_exists"; -val TFin_chain_lemma4 = thm "TFin_chain_lemma4"; -val Hausdorff = thm "Hausdorff"; -val chain_extend = thm "chain_extend"; -val Zorn = thm "Zorn"; -val TFin_well_lemma5 = thm "TFin_well_lemma5"; -val well_ord_TFin_lemma = thm "well_ord_TFin_lemma"; -val well_ord_TFin = thm "well_ord_TFin"; -val Zermelo_next_exists = thm "Zermelo_next_exists"; -val choice_imp_injection = thm "choice_imp_injection"; -val AC_well_ord = thm "AC_well_ord"; - -(* from Cardinal_AC *) -val cardinal_eqpoll = thm "cardinal_eqpoll"; -val cardinal_idem = thm "cardinal_idem"; -val cardinal_eqE = thm "cardinal_eqE"; -val cardinal_eqpoll_iff = thm "cardinal_eqpoll_iff"; -val cardinal_disjoint_Un = thm "cardinal_disjoint_Un"; -val lepoll_imp_Card_le = thm "lepoll_imp_Card_le"; -val cadd_assoc = thm "cadd_assoc"; -val cmult_assoc = thm "cmult_assoc"; -val cadd_cmult_distrib = thm "cadd_cmult_distrib"; -val InfCard_square_eq = thm "InfCard_square_eq"; -val Card_le_imp_lepoll = thm "Card_le_imp_lepoll"; -val le_Card_iff = thm "le_Card_iff"; -val surj_implies_inj = thm "surj_implies_inj"; -val surj_implies_cardinal_le = thm "surj_implies_cardinal_le"; -val cardinal_UN_le = thm "cardinal_UN_le"; -val cardinal_UN_lt_csucc = thm "cardinal_UN_lt_csucc"; -val cardinal_UN_Ord_lt_csucc = thm "cardinal_UN_Ord_lt_csucc"; -val inj_UN_subset = thm "inj_UN_subset"; -val le_UN_Ord_lt_csucc = thm "le_UN_Ord_lt_csucc"; - -(* from InfDatatype *) -val fun_Limit_VfromE = thm "fun_Limit_VfromE"; -val fun_Vcsucc_lemma = thm "fun_Vcsucc_lemma"; -val subset_Vcsucc = thm "subset_Vcsucc"; -val fun_Vcsucc = thm "fun_Vcsucc"; -val fun_in_Vcsucc = thm "fun_in_Vcsucc"; -val fun_in_Vcsucc' = thm "fun_in_Vcsucc'"; -val Card_fun_Vcsucc = thm "Card_fun_Vcsucc"; -val Card_fun_in_Vcsucc = thm "Card_fun_in_Vcsucc"; -val Limit_csucc = thm "Limit_csucc"; -val Pair_in_Vcsucc = thm "Pair_in_Vcsucc"; -val Inl_in_Vcsucc = thm "Inl_in_Vcsucc"; -val Inr_in_Vcsucc = thm "Inr_in_Vcsucc"; -val zero_in_Vcsucc = thm "zero_in_Vcsucc"; -val nat_into_Vcsucc = thm "nat_into_Vcsucc"; -val InfCard_nat_Un_cardinal = thm "InfCard_nat_Un_cardinal"; -val le_nat_Un_cardinal = thm "le_nat_Un_cardinal"; -val UN_upper_cardinal = thm "UN_upper_cardinal"; - -val inf_datatype_intrs = thms "inf_datatype_intros"; -