installation of new inductive/datatype sections
authorlcp
Fri Aug 12 12:51:34 1994 +0200 (1994-08-12)
changeset 5161957113f0d7d
parent 515 abcc438e7c27
child 517 a9f93400f307
installation of new inductive/datatype sections
src/ZF/CardinalArith.ML
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.ML
src/ZF/Datatype.ML
src/ZF/Datatype.thy
src/ZF/Finite.ML
src/ZF/Finite.thy
src/ZF/InfDatatype.ML
src/ZF/InfDatatype.thy
src/ZF/List.ML
src/ZF/List.thy
src/ZF/Makefile
src/ZF/QPair.ML
src/ZF/QPair.thy
src/ZF/ROOT.ML
src/ZF/Univ.ML
src/ZF/Univ.thy
src/ZF/ZF.ML
src/ZF/ZF.thy
src/ZF/Zorn.ML
src/ZF/Zorn.thy
src/ZF/add_ind_def.ML
src/ZF/add_ind_def.thy
src/ZF/constructor.ML
src/ZF/ind_syntax.ML
src/ZF/indrule.ML
src/ZF/inductive.ML
src/ZF/intr_elim.ML
src/ZF/intr_elim.thy
src/ZF/mono.ML
src/ZF/simpdata.ML
     1.1 --- a/src/ZF/CardinalArith.ML	Fri Aug 12 12:28:46 1994 +0200
     1.2 +++ b/src/ZF/CardinalArith.ML	Fri Aug 12 12:51:34 1994 +0200
     1.3 @@ -309,19 +309,24 @@
     1.4  
     1.5  (*** Infinite Cardinals are Limit Ordinals ***)
     1.6  
     1.7 -(*Using lam_injective might simplify this proof!*)
     1.8 +goalw CardinalArith.thy [lepoll_def]
     1.9 +    "!!i. nat <= A ==> succ(A) lepoll A";
    1.10 +by (res_inst_tac [("x",
    1.11 +    "lam z:succ(A). if(z=A, 0, if(z:nat, succ(z), z))")] exI 1);
    1.12 +by (res_inst_tac [("d", "%y. if(y:nat, nat_case(A,%z.z,y), y)")] 
    1.13 +    lam_injective 1);
    1.14 +by (fast_tac (ZF_cs addSIs [if_type, nat_0I, nat_succI]) 1);
    1.15 +by (asm_simp_tac 
    1.16 +    (ZF_ss addsimps [nat_case_0, nat_case_succ, nat_0I, nat_succI]
    1.17 +           setloop split_tac [expand_if]) 1);
    1.18 +val nat_succ_lepoll = result();
    1.19 +
    1.20  goalw CardinalArith.thy [lepoll_def, inj_def]
    1.21      "!!i. nat <= A ==> succ(A) lepoll A";
    1.22  by (res_inst_tac [("x",
    1.23     "lam z:succ(A). if(z=A, 0, if(z:nat, succ(z), z))")] exI 1);
    1.24  by (rtac (lam_type RS CollectI) 1);
    1.25 -by (rtac if_type 1);
    1.26 -by (etac ([asm_rl, nat_0I] MRS subsetD) 1);
    1.27 -by (etac succE 1);
    1.28 -by (contr_tac 1);
    1.29 -by (rtac if_type 1);
    1.30 -by (assume_tac 2);
    1.31 -by (etac ([asm_rl, nat_succI] MRS subsetD) 1 THEN assume_tac 1);
    1.32 +by (fast_tac (ZF_cs addSIs [if_type, nat_0I, nat_succI]) 1);
    1.33  by (REPEAT (rtac ballI 1));
    1.34  by (asm_simp_tac 
    1.35      (ZF_ss addsimps [succ_inject_iff, succ_not_0, succ_not_0 RS not_sym]
     2.1 --- a/src/ZF/CardinalArith.thy	Fri Aug 12 12:28:46 1994 +0200
     2.2 +++ b/src/ZF/CardinalArith.thy	Fri Aug 12 12:51:34 1994 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  Cardinal Arithmetic
     2.5  *)
     2.6  
     2.7 -CardinalArith = Cardinal + OrderArith + Arith + Fin + 
     2.8 +CardinalArith = Cardinal + OrderArith + Arith + Finite + 
     2.9  consts
    2.10  
    2.11    InfCard     :: "i=>o"
     3.1 --- a/src/ZF/Cardinal_AC.ML	Fri Aug 12 12:28:46 1994 +0200
     3.2 +++ b/src/ZF/Cardinal_AC.ML	Fri Aug 12 12:51:34 1994 +0200
     3.3 @@ -135,3 +135,15 @@
     3.4  by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);
     3.5  val cardinal_UN_Ord_lt_csucc = result();
     3.6  
     3.7 +goal Cardinal_AC.thy
     3.8 +    "!!K. [| InfCard(K);  |I| le K;  ALL i:I. j(i) < csucc(K) |] ==> \
     3.9 +\         (UN i:I. j(i)) < csucc(K)";
    3.10 +by (asm_full_simp_tac
    3.11 +    (ZF_ss addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1);
    3.12 +by (eresolve_tac [exE] 1);
    3.13 +by (resolve_tac [lt_trans1] 1);
    3.14 +by (resolve_tac [cardinal_UN_Ord_lt_csucc] 2);
    3.15 +by (assume_tac 2);
    3.16 +
    3.17 +val ?cardinal_UN_Ord_lt_csucc = result();
    3.18 +
     4.1 --- a/src/ZF/Datatype.ML	Fri Aug 12 12:28:46 1994 +0200
     4.2 +++ b/src/ZF/Datatype.ML	Fri Aug 12 12:51:34 1994 +0200
     4.3 @@ -1,57 +1,12 @@
     4.4 -(*  Title: 	ZF/datatype.ML
     4.5 +(*  Title:      ZF/Datatype.ML
     4.6      ID:         $Id$
     4.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.9      Copyright   1993  University of Cambridge
    4.10  
    4.11  (Co)Datatype Definitions for Zermelo-Fraenkel Set Theory
    4.12  *)
    4.13  
    4.14  
    4.15 -(*Datatype definitions use least fixedpoints, standard products and sums*)
    4.16 -functor Datatype_Fun (Const: CONSTRUCTOR) 
    4.17 -         : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
    4.18 -struct
    4.19 -structure Constructor = Constructor_Fun (structure Const=Const and 
    4.20 -  		                      Pr=Standard_Prod and Su=Standard_Sum);
    4.21 -open Const Constructor;
    4.22 -
    4.23 -structure Inductive = Inductive_Fun
    4.24 -        (val thy = con_thy;
    4.25 -         val thy_name = thy_name;
    4.26 -	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
    4.27 -	 val sintrs = sintrs;
    4.28 -	 val monos = monos;
    4.29 -	 val con_defs = con_defs;
    4.30 -	 val type_intrs = type_intrs;
    4.31 -	 val type_elims = type_elims);
    4.32 -
    4.33 -open Inductive
    4.34 -end;
    4.35 -
    4.36 -
    4.37 -(*Codatatype definitions use greatest fixedpoints, Quine products and sums*)
    4.38 -functor CoDatatype_Fun (Const: CONSTRUCTOR) 
    4.39 -         : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
    4.40 -struct
    4.41 -structure Constructor = Constructor_Fun (structure Const=Const and 
    4.42 -  		                      Pr=Quine_Prod and Su=Quine_Sum);
    4.43 -open Const Constructor;
    4.44 -
    4.45 -structure CoInductive = CoInductive_Fun
    4.46 -        (val thy = con_thy;
    4.47 -         val thy_name = thy_name;
    4.48 -	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
    4.49 -	 val sintrs = sintrs;
    4.50 -	 val monos = monos;
    4.51 -	 val con_defs = con_defs;
    4.52 -	 val type_intrs = type_intrs;
    4.53 -	 val type_elims = type_elims);
    4.54 -
    4.55 -open CoInductive
    4.56 -end;
    4.57 -
    4.58 -
    4.59 -
    4.60  (*For most datatypes involving univ*)
    4.61  val datatype_intrs = 
    4.62      [SigmaI, InlI, InrI,
    4.63 @@ -69,3 +24,110 @@
    4.64  
    4.65  val codatatype_elims = [make_elim QInlD, make_elim QInrD];
    4.66  
    4.67 +signature INDUCTIVE_THMS =
    4.68 +  sig
    4.69 +  val monos      : thm list		(*monotonicity of each M operator*)
    4.70 +  val type_intrs : thm list		(*type-checking intro rules*)
    4.71 +  val type_elims : thm list		(*type-checking elim rules*)
    4.72 +  end;
    4.73 +
    4.74 +functor Data_section_Fun
    4.75 + (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
    4.76 +    : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
    4.77 +struct
    4.78 +
    4.79 +structure Con = Constructor_Fun 
    4.80 + 	(structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
    4.81 +
    4.82 +structure Inductive = Ind_section_Fun
    4.83 +   (open Arg; 
    4.84 +    val con_defs = Con.con_defs
    4.85 +    val type_intrs = Arg.type_intrs @ datatype_intrs
    4.86 +    val type_elims = Arg.type_elims @ datatype_elims);
    4.87 +
    4.88 +open Inductive Con
    4.89 +end;
    4.90 +
    4.91 +
    4.92 +functor CoData_section_Fun
    4.93 + (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
    4.94 +    : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
    4.95 +struct
    4.96 +
    4.97 +structure Con = Constructor_Fun 
    4.98 + 	(structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
    4.99 +
   4.100 +structure CoInductive = CoInd_section_Fun
   4.101 +   (open Arg; 
   4.102 +    val con_defs = Con.con_defs
   4.103 +    val type_intrs = Arg.type_intrs @ codatatype_intrs
   4.104 +    val type_elims = Arg.type_elims @ codatatype_elims);
   4.105 +
   4.106 +open CoInductive Con
   4.107 +end;
   4.108 +
   4.109 +
   4.110 +(*For installing the theory section.   co is either "" or "Co"*)
   4.111 +fun datatype_decl co =
   4.112 +  let open ThyParse Ind_Syntax
   4.113 +      (*generate strings*)
   4.114 +      fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
   4.115 +      val mk_data = mk_list o map mk_const o snd
   4.116 +      val mk_scons = mk_big_list o map mk_data
   4.117 +      fun mk_intr_name s =  (*the "op" cancels any infix status*)
   4.118 +	  if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_"
   4.119 +      fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) =
   4.120 +        let val rec_names = map (scan_to_id o trim o fst) rec_pairs
   4.121 +	    val big_rec_name = space_implode "_" rec_names
   4.122 +	    and srec_tms = mk_list (map fst rec_pairs)
   4.123 +            and scons    = mk_scons rec_pairs
   4.124 +            and sdom	 = (*default domain?*)
   4.125 +		if dom = ""  then co ^ "data_domain rec_tms"
   4.126 +		else "replicate " ^ string_of_int (length rec_names) ^  
   4.127 +		     " (readtm (sign_of thy) iT " ^ dom ^ ")"
   4.128 +            val stri_name = big_rec_name ^ "_Intrnl"
   4.129 +            val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
   4.130 +        in
   4.131 +	   (";\n\n\
   4.132 +            \structure " ^ stri_name ^ " =\n\
   4.133 +            \ let open Ind_Syntax in\n\
   4.134 +            \  struct\n\
   4.135 +            \  val rec_tms\t= map (readtm (sign_of thy) iT) " ^ srec_tms ^ "\n\
   4.136 +            \  val domts\t= " ^ sdom ^ "\n\
   4.137 +            \  and con_ty_lists\t= read_constructs (sign_of thy)\n" 
   4.138 +	           ^ scons ^ "\n\
   4.139 +            \  val intr_tms\t= mk_all_intr_tms (rec_tms, con_ty_lists)\n\
   4.140 +            \  end\n\
   4.141 +            \ end;\n\n\
   4.142 +            \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ 
   4.143 +	         mk_list (map quote rec_names) ^ ", " ^ 
   4.144 +                 stri_name ^ ".con_ty_lists) \n\
   4.145 +            \              |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
   4.146 +	       stri_name ^ ".rec_tms, " ^
   4.147 +               stri_name ^ ".domts, " ^
   4.148 +               stri_name ^ ".intr_tms)"
   4.149 +           ,
   4.150 +	    "structure " ^ big_rec_name ^ " =\n\
   4.151 +            \  struct\n\
   4.152 +            \  val _ = writeln \"" ^ co ^ 
   4.153 +	               "Datatype definition " ^ big_rec_name ^ "\"\n\
   4.154 +            \  structure Result = " ^ co ^ "Data_section_Fun\n\
   4.155 +            \  (open " ^ stri_name ^ "\n\
   4.156 +            \   val thy\t\t= thy\n\
   4.157 +            \   val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\
   4.158 +            \   val monos\t\t= " ^ monos ^ "\n\
   4.159 +            \   val type_intrs\t= " ^ type_intrs ^ "\n\
   4.160 +            \   val type_elims\t= " ^ type_elims ^ ");\n\n\
   4.161 +            \  val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
   4.162 +            \  open Result\n\
   4.163 +            \  end\n"
   4.164 +	   )
   4.165 +	end
   4.166 +      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
   4.167 +      val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
   4.168 +      val construct = name -- string_list -- opt_mixfix;
   4.169 +  in optional ("<=" $$-- string) "" --
   4.170 +     enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
   4.171 +     optstring "monos" -- optstring "type_intrs" -- optstring "type_elims"
   4.172 +     >> mk_params
   4.173 +end;
     5.1 --- a/src/ZF/Datatype.thy	Fri Aug 12 12:28:46 1994 +0200
     5.2 +++ b/src/ZF/Datatype.thy	Fri Aug 12 12:51:34 1994 +0200
     5.3 @@ -1,4 +1,5 @@
     5.4  (*Dummy theory to document dependencies *)
     5.5  
     5.6 -Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
     5.7 -               (*this must be capital to avoid conflicts with ML's "datatype" *)
     5.8 \ No newline at end of file
     5.9 +Datatype = "constructor" + "inductive" + Univ + QUniv
    5.10 +
    5.11 +(*Datatype must be capital to avoid conflicts with ML's "datatype" *)
    5.12 \ No newline at end of file
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/ZF/Finite.ML	Fri Aug 12 12:51:34 1994 +0200
     6.3 @@ -0,0 +1,94 @@
     6.4 +(*  Title: 	ZF/Finite.ML
     6.5 +    ID:         $Id$
     6.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 +    Copyright   1994  University of Cambridge
     6.8 +
     6.9 +Finite powerset operator
    6.10 +
    6.11 +prove X:Fin(A) ==> |X| < nat
    6.12 +
    6.13 +prove:  b: Fin(A) ==> inj(b,b)<=surj(b,b)
    6.14 +*)
    6.15 +
    6.16 +open Finite;
    6.17 +
    6.18 +goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
    6.19 +by (rtac lfp_mono 1);
    6.20 +by (REPEAT (rtac Fin.bnd_mono 1));
    6.21 +by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
    6.22 +val Fin_mono = result();
    6.23 +
    6.24 +(* A : Fin(B) ==> A <= B *)
    6.25 +val FinD = Fin.dom_subset RS subsetD RS PowD;
    6.26 +
    6.27 +(** Induction on finite sets **)
    6.28 +
    6.29 +(*Discharging x~:y entails extra work*)
    6.30 +val major::prems = goal Finite.thy 
    6.31 +    "[| b: Fin(A);  \
    6.32 +\       P(0);        \
    6.33 +\       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
    6.34 +\    |] ==> P(b)";
    6.35 +by (rtac (major RS Fin.induct) 1);
    6.36 +by (excluded_middle_tac "a:b" 2);
    6.37 +by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);	    (*backtracking!*)
    6.38 +by (REPEAT (ares_tac prems 1));
    6.39 +val Fin_induct = result();
    6.40 +
    6.41 +(** Simplification for Fin **)
    6.42 +val Fin_ss = arith_ss addsimps Fin.intrs;
    6.43 +
    6.44 +(*The union of two finite sets is finite.*)
    6.45 +val major::prems = goal Finite.thy
    6.46 +    "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
    6.47 +by (rtac (major RS Fin_induct) 1);
    6.48 +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
    6.49 +val Fin_UnI = result();
    6.50 +
    6.51 +(*The union of a set of finite sets is finite.*)
    6.52 +val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
    6.53 +by (rtac (major RS Fin_induct) 1);
    6.54 +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
    6.55 +val Fin_UnionI = result();
    6.56 +
    6.57 +(*Every subset of a finite set is finite.*)
    6.58 +goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
    6.59 +by (etac Fin_induct 1);
    6.60 +by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
    6.61 +by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
    6.62 +by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
    6.63 +by (ALLGOALS (asm_simp_tac Fin_ss));
    6.64 +val Fin_subset_lemma = result();
    6.65 +
    6.66 +goal Finite.thy "!!c b A. [| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
    6.67 +by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
    6.68 +val Fin_subset = result();
    6.69 +
    6.70 +val major::prems = goal Finite.thy 
    6.71 +    "[| c: Fin(A);  b: Fin(A);  				\
    6.72 +\       P(b);       						\
    6.73 +\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
    6.74 +\    |] ==> c<=b --> P(b-c)";
    6.75 +by (rtac (major RS Fin_induct) 1);
    6.76 +by (rtac (Diff_cons RS ssubst) 2);
    6.77 +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 
    6.78 +				Diff_subset RS Fin_subset]))));
    6.79 +val Fin_0_induct_lemma = result();
    6.80 +
    6.81 +val prems = goal Finite.thy 
    6.82 +    "[| b: Fin(A);  						\
    6.83 +\       P(b);        						\
    6.84 +\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
    6.85 +\    |] ==> P(0)";
    6.86 +by (rtac (Diff_cancel RS subst) 1);
    6.87 +by (rtac (Fin_0_induct_lemma RS mp) 1);
    6.88 +by (REPEAT (ares_tac (subset_refl::prems) 1));
    6.89 +val Fin_0_induct = result();
    6.90 +
    6.91 +(*Functions from a finite ordinal*)
    6.92 +val prems = goal Finite.thy "n: nat ==> n->A <= Fin(nat*A)";
    6.93 +by (nat_ind_tac "n" prems 1);
    6.94 +by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin.emptyI, subset_iff, cons_iff]) 1);
    6.95 +by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
    6.96 +by (fast_tac (ZF_cs addSIs [Fin.consI]) 1);
    6.97 +val nat_fun_subset_Fin = result();
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/ZF/Finite.thy	Fri Aug 12 12:51:34 1994 +0200
     7.3 @@ -0,0 +1,18 @@
     7.4 +(*  Title: 	ZF/Finite.thy
     7.5 +    ID:         $Id$
     7.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 +    Copyright   1994  University of Cambridge
     7.8 +
     7.9 +Finite powerset operator
    7.10 +*)
    7.11 +
    7.12 +Finite = Arith + 
    7.13 +consts Fin :: "i=>i"
    7.14 +inductive
    7.15 +  domains   "Fin(A)" <= "Pow(A)"
    7.16 +  intrs
    7.17 +    emptyI  "0 : Fin(A)"
    7.18 +    consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
    7.19 +  type_intrs "[empty_subsetI, cons_subsetI, PowI]"
    7.20 +  type_elims "[make_elim PowD]"
    7.21 +end
     8.1 --- a/src/ZF/InfDatatype.ML	Fri Aug 12 12:28:46 1994 +0200
     8.2 +++ b/src/ZF/InfDatatype.ML	Fri Aug 12 12:51:34 1994 +0200
     8.3 @@ -3,14 +3,90 @@
     8.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     8.5      Copyright   1994  University of Cambridge
     8.6  
     8.7 -Infinite-Branching Datatype Definitions
     8.8 +Datatype Definitions involving ->
     8.9 +	Even infinite-branching!
    8.10  *)
    8.11  
    8.12 +(*** Closure under finite powerset ***)
    8.13 +
    8.14 +val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy);
    8.15 +
    8.16 +goal Fin_Univ_thy
    8.17 +   "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
    8.18 +by (eresolve_tac [Fin_induct] 1);
    8.19 +by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1);
    8.20 +by (safe_tac ZF_cs);
    8.21 +by (eresolve_tac [Limit_VfromE] 1);
    8.22 +by (assume_tac 1);
    8.23 +by (res_inst_tac [("x", "xa Un j")] exI 1);
    8.24 +by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, 
    8.25 +			   Un_least_lt]) 1);
    8.26 +val Fin_Vfrom_lemma = result();
    8.27 +
    8.28 +goal Fin_Univ_thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
    8.29 +by (rtac subsetI 1);
    8.30 +by (dresolve_tac [Fin_Vfrom_lemma] 1);
    8.31 +by (safe_tac ZF_cs);
    8.32 +by (resolve_tac [Vfrom RS ssubst] 1);
    8.33 +by (fast_tac (ZF_cs addSDs [ltD]) 1);
    8.34 +val Fin_VLimit = result();
    8.35 +
    8.36 +val Fin_subset_VLimit = 
    8.37 +    [Fin_mono, Fin_VLimit] MRS subset_trans |> standard;
    8.38 +
    8.39 +goal Fin_Univ_thy
    8.40 +    "!!i. [| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
    8.41 +by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
    8.42 +by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
    8.43 +		      nat_subset_VLimit, subset_refl] 1));
    8.44 +val nat_fun_VLimit = result();
    8.45 +
    8.46 +val nat_fun_subset_VLimit = 
    8.47 +    [Pi_mono, nat_fun_VLimit] MRS subset_trans |> standard;
    8.48 +
    8.49 +
    8.50 +goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)";
    8.51 +by (rtac (Limit_nat RS Fin_VLimit) 1);
    8.52 +val Fin_univ = result();
    8.53 +
    8.54 +val Fin_subset_univ = [Fin_mono, Fin_univ] MRS subset_trans |> standard;
    8.55 +
    8.56 +goalw Fin_Univ_thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
    8.57 +by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
    8.58 +val nat_fun_univ = result();
    8.59 +
    8.60 +val nat_fun_subset_univ = [Pi_mono, nat_fun_univ] MRS subset_trans |> standard;
    8.61 +
    8.62 +goal Fin_Univ_thy
    8.63 +    "!!f. [| f: n -> B;  B <= univ(A);  n : nat |] ==> f : univ(A)";
    8.64 +by (REPEAT (ares_tac [nat_fun_subset_univ RS subsetD] 1));
    8.65 +val nat_fun_into_univ = result();
    8.66 +
    8.67 +
    8.68 +(*** Infinite branching ***)
    8.69 +
    8.70  val fun_Limit_VfromE = 
    8.71      [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
    8.72  	|> standard;
    8.73  
    8.74  goal InfDatatype.thy
    8.75 +    "!!K. [| f: I -> Vfrom(A,csucc(K));  |I| le K;  InfCard(K)	\
    8.76 +\         |] ==> EX j. f: I -> Vfrom(A,j) & j < csucc(K)";
    8.77 +by (res_inst_tac [("x", "UN x:I. LEAST i. f`x : Vfrom(A,i)")] exI 1);
    8.78 +by (resolve_tac [conjI] 1);
    8.79 +by (resolve_tac [ballI RSN (2,cardinal_UN_Ord_lt_csucc)] 2);
    8.80 +by (eresolve_tac [fun_Limit_VfromE] 3 THEN REPEAT_SOME assume_tac);
    8.81 +by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2);
    8.82 +by (resolve_tac [Pi_type] 1);
    8.83 +by (rename_tac "k" 2);
    8.84 +by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac);
    8.85 +by (subgoal_tac "f`k : Vfrom(A, LEAST i. f`k : Vfrom(A,i))" 1);
    8.86 +by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2);
    8.87 +by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);
    8.88 +by (assume_tac 1);
    8.89 +val fun_Vcsucc_lemma = result();
    8.90 +
    8.91 +goal InfDatatype.thy
    8.92      "!!K. [| f: K -> Vfrom(A,csucc(K));  InfCard(K)	\
    8.93  \         |] ==> EX j. f: K -> Vfrom(A,j) & j < csucc(K)";
    8.94  by (res_inst_tac [("x", "UN k:K. LEAST i. f`k : Vfrom(A,i)")] exI 1);
    8.95 @@ -25,11 +101,11 @@
    8.96  by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2);
    8.97  by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);
    8.98  by (assume_tac 1);
    8.99 -val fun_Vfrom_csucc_lemma = result();
   8.100 +val fun_Vcsucc_lemma = result();
   8.101  
   8.102  goal InfDatatype.thy
   8.103      "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
   8.104 -by (safe_tac (ZF_cs addSDs [fun_Vfrom_csucc_lemma]));
   8.105 +by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma]));
   8.106  by (resolve_tac [Vfrom RS ssubst] 1);
   8.107  by (eresolve_tac [PiE] 1);
   8.108  (*This level includes the function, and is below csucc(K)*)
   8.109 @@ -42,35 +118,34 @@
   8.110  		      Limit_has_succ, Un_least_lt] 1));
   8.111  by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS lt_csucc] 1);
   8.112  by (assume_tac 1);
   8.113 -val fun_Vfrom_csucc = result();
   8.114 +val fun_Vcsucc = result();
   8.115  
   8.116  goal InfDatatype.thy
   8.117      "!!K. [| f: K -> Vfrom(A, csucc(K));  InfCard(K) \
   8.118  \         |] ==> f: Vfrom(A,csucc(K))";
   8.119 -by (REPEAT (ares_tac [fun_Vfrom_csucc RS subsetD] 1));
   8.120 -val fun_in_Vfrom_csucc = result();
   8.121 +by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
   8.122 +val fun_in_Vcsucc = result();
   8.123  
   8.124 -val fun_subset_Vfrom_csucc = 
   8.125 -	[Pi_mono, fun_Vfrom_csucc] MRS subset_trans |> standard;
   8.126 +val fun_subset_Vcsucc = 
   8.127 +	[Pi_mono, fun_Vcsucc] MRS subset_trans |> standard;
   8.128  
   8.129  goal InfDatatype.thy
   8.130      "!!f. [| f: K -> B;  B <= Vfrom(A,csucc(K));  InfCard(K) \
   8.131  \         |] ==> f: Vfrom(A,csucc(K))";
   8.132 -by (REPEAT (ares_tac [fun_subset_Vfrom_csucc RS subsetD] 1));
   8.133 -val fun_into_Vfrom_csucc = result();
   8.134 +by (REPEAT (ares_tac [fun_subset_Vcsucc RS subsetD] 1));
   8.135 +val fun_into_Vcsucc = result();
   8.136  
   8.137  val Limit_csucc = InfCard_csucc RS InfCard_is_Limit |> standard;
   8.138  
   8.139 -val Pair_in_Vfrom_csucc = Limit_csucc RSN (3, Pair_in_Vfrom_Limit) |> standard;
   8.140 -val Inl_in_Vfrom_csucc  = Limit_csucc RSN (2, Inl_in_Vfrom_Limit) |> standard;
   8.141 -val Inr_in_Vfrom_csucc  = Limit_csucc RSN (2, Inr_in_Vfrom_Limit) |> standard;
   8.142 -val zero_in_Vfrom_csucc = Limit_csucc RS zero_in_Vfrom_Limit |> standard;
   8.143 -val nat_into_Vfrom_csucc = Limit_csucc RSN (2, nat_into_Vfrom_Limit) 
   8.144 -			   |> standard;
   8.145 +val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard;
   8.146 +val Inl_in_Vcsucc  = Limit_csucc RSN (2, Inl_in_VLimit) |> standard;
   8.147 +val Inr_in_Vcsucc  = Limit_csucc RSN (2, Inr_in_VLimit) |> standard;
   8.148 +val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit |> standard;
   8.149 +val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) |> standard;
   8.150  
   8.151  (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
   8.152  val inf_datatype_intrs =  
   8.153 -    [fun_in_Vfrom_csucc, InfCard_nat, Pair_in_Vfrom_csucc, 
   8.154 -     Inl_in_Vfrom_csucc, Inr_in_Vfrom_csucc, 
   8.155 -     zero_in_Vfrom_csucc, A_into_Vfrom, nat_into_Vfrom_csucc] @ datatype_intrs;
   8.156 +    [fun_in_Vcsucc, InfCard_nat, Pair_in_Vcsucc, 
   8.157 +     Inl_in_Vcsucc, Inr_in_Vcsucc, 
   8.158 +     zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc] @ datatype_intrs;
   8.159  
     9.1 --- a/src/ZF/InfDatatype.thy	Fri Aug 12 12:28:46 1994 +0200
     9.2 +++ b/src/ZF/InfDatatype.thy	Fri Aug 12 12:51:34 1994 +0200
     9.3 @@ -1,1 +1,1 @@
     9.4 -InfDatatype = Datatype + Univ + Cardinal_AC
     9.5 +InfDatatype = Datatype + Univ + Finite + Cardinal_AC
    10.1 --- a/src/ZF/List.ML	Fri Aug 12 12:28:46 1994 +0200
    10.2 +++ b/src/ZF/List.ML	Fri Aug 12 12:51:34 1994 +0200
    10.3 @@ -6,52 +6,42 @@
    10.4  Datatype definition of Lists
    10.5  *)
    10.6  
    10.7 -structure List = Datatype_Fun
    10.8 - (val thy        = Univ.thy
    10.9 -  val thy_name   = "List"
   10.10 -  val rec_specs  = [("list", "univ(A)",
   10.11 -                      [(["Nil"],    "i", 	NoSyn), 
   10.12 -                       (["Cons"],   "[i,i]=>i",	NoSyn)])]
   10.13 -  val rec_styp   = "i=>i"
   10.14 -  val sintrs     = ["Nil : list(A)",
   10.15 -                    "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]
   10.16 -  val monos      = []
   10.17 -  val type_intrs = datatype_intrs
   10.18 -  val type_elims = datatype_elims);
   10.19 +open List;
   10.20  
   10.21 -val [NilI, ConsI] = List.intrs;
   10.22 +(*** Aspects of the datatype definition ***)
   10.23  
   10.24  (*An elimination rule, for type-checking*)
   10.25 -val ConsE = List.mk_cases List.con_defs "Cons(a,l) : list(A)";
   10.26 +val ConsE = list.mk_cases list.con_defs "Cons(a,l) : list(A)";
   10.27  
   10.28  (*Proving freeness results*)
   10.29 -val Cons_iff     = List.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
   10.30 -val Nil_Cons_iff = List.mk_free "~ Nil=Cons(a,l)";
   10.31 +val Cons_iff     = list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
   10.32 +val Nil_Cons_iff = list.mk_free "~ Nil=Cons(a,l)";
   10.33  
   10.34  (*Perform induction on l, then prove the major premise using prems. *)
   10.35  fun list_ind_tac a prems i = 
   10.36 -    EVERY [res_inst_tac [("x",a)] List.induct i,
   10.37 +    EVERY [res_inst_tac [("x",a)] list.induct i,
   10.38  	   rename_last_tac a ["1"] (i+2),
   10.39  	   ares_tac prems i];
   10.40  
   10.41  goal List.thy "list(A) = {0} + (A * list(A))";
   10.42 -by (rtac (List.unfold RS trans) 1);
   10.43 -bws List.con_defs;
   10.44 -by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs)
   10.45 -		     addDs [List.dom_subset RS subsetD]
   10.46 - 	             addEs [A_into_univ]) 1);
   10.47 +by (rtac (list.unfold RS trans) 1);
   10.48 +bws list.con_defs;
   10.49 +br equalityI 1;
   10.50 +by (fast_tac sum_cs 1);
   10.51 +by (fast_tac (sum_cs addIs datatype_intrs
   10.52 +		     addDs [list.dom_subset RS subsetD]) 1);
   10.53  val list_unfold = result();
   10.54  
   10.55  (**  Lemmas to justify using "list" in other recursive type definitions **)
   10.56  
   10.57 -goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)";
   10.58 +goalw List.thy list.defs "!!A B. A<=B ==> list(A) <= list(B)";
   10.59  by (rtac lfp_mono 1);
   10.60 -by (REPEAT (rtac List.bnd_mono 1));
   10.61 +by (REPEAT (rtac list.bnd_mono 1));
   10.62  by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
   10.63  val list_mono = result();
   10.64  
   10.65  (*There is a similar proof by list induction.*)
   10.66 -goalw List.thy (List.defs@List.con_defs) "list(univ(A)) <= univ(A)";
   10.67 +goalw List.thy (list.defs@list.con_defs) "list(univ(A)) <= univ(A)";
   10.68  by (rtac lfp_lowerbound 1);
   10.69  by (rtac (A_subset_univ RS univ_mono) 2);
   10.70  by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
   10.71 @@ -69,18 +59,374 @@
   10.72  \       c: C(Nil);       \
   10.73  \       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))  \
   10.74  \    |] ==> list_case(c,h,l) : C(l)";
   10.75 -by (rtac (major RS List.induct) 1);
   10.76 -by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.case_eqns @ prems))));
   10.77 +by (rtac (major RS list.induct) 1);
   10.78 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (list.case_eqns @ prems))));
   10.79  val list_case_type = result();
   10.80  
   10.81  
   10.82  (** For recursion **)
   10.83  
   10.84 -goalw List.thy List.con_defs "rank(a) < rank(Cons(a,l))";
   10.85 +goalw List.thy list.con_defs "rank(a) < rank(Cons(a,l))";
   10.86  by (simp_tac rank_ss 1);
   10.87  val rank_Cons1 = result();
   10.88  
   10.89 -goalw List.thy List.con_defs "rank(l) < rank(Cons(a,l))";
   10.90 +goalw List.thy list.con_defs "rank(l) < rank(Cons(a,l))";
   10.91  by (simp_tac rank_ss 1);
   10.92  val rank_Cons2 = result();
   10.93  
   10.94 +
   10.95 +(*** List functions ***)
   10.96 +
   10.97 +(** hd and tl **)
   10.98 +
   10.99 +goalw List.thy [hd_def] "hd(Cons(a,l)) = a";
  10.100 +by (resolve_tac list.case_eqns 1);
  10.101 +val hd_Cons = result();
  10.102 +
  10.103 +goalw List.thy [tl_def] "tl(Nil) = Nil";
  10.104 +by (resolve_tac list.case_eqns 1);
  10.105 +val tl_Nil = result();
  10.106 +
  10.107 +goalw List.thy [tl_def] "tl(Cons(a,l)) = l";
  10.108 +by (resolve_tac list.case_eqns 1);
  10.109 +val tl_Cons = result();
  10.110 +
  10.111 +goal List.thy "!!l. l: list(A) ==> tl(l) : list(A)";
  10.112 +by (etac list.elim 1);
  10.113 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (list.intrs @ [tl_Nil,tl_Cons]))));
  10.114 +val tl_type = result();
  10.115 +
  10.116 +(** drop **)
  10.117 +
  10.118 +goalw List.thy [drop_def] "drop(0, l) = l";
  10.119 +by (rtac rec_0 1);
  10.120 +val drop_0 = result();
  10.121 +
  10.122 +goalw List.thy [drop_def] "!!i. i:nat ==> drop(i, Nil) = Nil";
  10.123 +by (etac nat_induct 1);
  10.124 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Nil])));
  10.125 +val drop_Nil = result();
  10.126 +
  10.127 +goalw List.thy [drop_def]
  10.128 +    "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
  10.129 +by (etac nat_induct 1);
  10.130 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Cons])));
  10.131 +val drop_succ_Cons = result();
  10.132 +
  10.133 +goalw List.thy [drop_def] 
  10.134 +    "!!i l. [| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
  10.135 +by (etac nat_induct 1);
  10.136 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_type])));
  10.137 +val drop_type = result();
  10.138 +
  10.139 +(** list_rec -- by Vset recursion **)
  10.140 +
  10.141 +goal List.thy "list_rec(Nil,c,h) = c";
  10.142 +by (rtac (list_rec_def RS def_Vrec RS trans) 1);
  10.143 +by (simp_tac (ZF_ss addsimps list.case_eqns) 1);
  10.144 +val list_rec_Nil = result();
  10.145 +
  10.146 +goal List.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
  10.147 +by (rtac (list_rec_def RS def_Vrec RS trans) 1);
  10.148 +by (simp_tac (rank_ss addsimps (rank_Cons2::list.case_eqns)) 1);
  10.149 +val list_rec_Cons = result();
  10.150 +
  10.151 +(*Type checking -- proved by induction, as usual*)
  10.152 +val prems = goal List.thy
  10.153 +    "[| l: list(A);    \
  10.154 +\       c: C(Nil);       \
  10.155 +\       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
  10.156 +\    |] ==> list_rec(l,c,h) : C(l)";
  10.157 +by (list_ind_tac "l" prems 1);
  10.158 +by (ALLGOALS (asm_simp_tac
  10.159 +	      (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons]))));
  10.160 +val list_rec_type = result();
  10.161 +
  10.162 +(** Versions for use with definitions **)
  10.163 +
  10.164 +val [rew] = goal List.thy
  10.165 +    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
  10.166 +by (rewtac rew);
  10.167 +by (rtac list_rec_Nil 1);
  10.168 +val def_list_rec_Nil = result();
  10.169 +
  10.170 +val [rew] = goal List.thy
  10.171 +    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
  10.172 +by (rewtac rew);
  10.173 +by (rtac list_rec_Cons 1);
  10.174 +val def_list_rec_Cons = result();
  10.175 +
  10.176 +fun list_recs def = map standard
  10.177 +    	([def] RL [def_list_rec_Nil, def_list_rec_Cons]);
  10.178 +
  10.179 +(** map **)
  10.180 +
  10.181 +val [map_Nil,map_Cons] = list_recs map_def;
  10.182 +
  10.183 +val prems = goalw List.thy [map_def] 
  10.184 +    "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
  10.185 +by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
  10.186 +val map_type = result();
  10.187 +
  10.188 +val [major] = goal List.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";
  10.189 +by (rtac (major RS map_type) 1);
  10.190 +by (etac RepFunI 1);
  10.191 +val map_type2 = result();
  10.192 +
  10.193 +(** length **)
  10.194 +
  10.195 +val [length_Nil,length_Cons] = list_recs length_def;
  10.196 +
  10.197 +goalw List.thy [length_def] 
  10.198 +    "!!l. l: list(A) ==> length(l) : nat";
  10.199 +by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
  10.200 +val length_type = result();
  10.201 +
  10.202 +(** app **)
  10.203 +
  10.204 +val [app_Nil,app_Cons] = list_recs app_def;
  10.205 +
  10.206 +goalw List.thy [app_def] 
  10.207 +    "!!xs ys. [| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
  10.208 +by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
  10.209 +val app_type = result();
  10.210 +
  10.211 +(** rev **)
  10.212 +
  10.213 +val [rev_Nil,rev_Cons] = list_recs rev_def;
  10.214 +
  10.215 +goalw List.thy [rev_def] 
  10.216 +    "!!xs. xs: list(A) ==> rev(xs) : list(A)";
  10.217 +by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
  10.218 +val rev_type = result();
  10.219 +
  10.220 +
  10.221 +(** flat **)
  10.222 +
  10.223 +val [flat_Nil,flat_Cons] = list_recs flat_def;
  10.224 +
  10.225 +goalw List.thy [flat_def] 
  10.226 +    "!!ls. ls: list(list(A)) ==> flat(ls) : list(A)";
  10.227 +by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
  10.228 +val flat_type = result();
  10.229 +
  10.230 +
  10.231 +(** list_add **)
  10.232 +
  10.233 +val [list_add_Nil,list_add_Cons] = list_recs list_add_def;
  10.234 +
  10.235 +goalw List.thy [list_add_def] 
  10.236 +    "!!xs. xs: list(nat) ==> list_add(xs) : nat";
  10.237 +by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
  10.238 +val list_add_type = result();
  10.239 +
  10.240 +(** List simplification **)
  10.241 +
  10.242 +val list_typechecks =
  10.243 +    list.intrs @
  10.244 +    [list_rec_type, map_type, map_type2, app_type, length_type, 
  10.245 +     rev_type, flat_type, list_add_type];
  10.246 +
  10.247 +val list_ss = arith_ss 
  10.248 +    addsimps list.case_eqns
  10.249 +    addsimps [list_rec_Nil, list_rec_Cons, 
  10.250 +	      map_Nil, map_Cons, app_Nil, app_Cons,
  10.251 +	      length_Nil, length_Cons, rev_Nil, rev_Cons,
  10.252 +	      flat_Nil, flat_Cons, list_add_Nil, list_add_Cons]
  10.253 +    setsolver (type_auto_tac list_typechecks);
  10.254 +
  10.255 +
  10.256 +(*** theorems about map ***)
  10.257 +
  10.258 +val prems = goal List.thy
  10.259 +    "l: list(A) ==> map(%u.u, l) = l";
  10.260 +by (list_ind_tac "l" prems 1);
  10.261 +by (ALLGOALS (asm_simp_tac list_ss));
  10.262 +val map_ident = result();
  10.263 +
  10.264 +val prems = goal List.thy
  10.265 +    "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
  10.266 +by (list_ind_tac "l" prems 1);
  10.267 +by (ALLGOALS (asm_simp_tac list_ss));
  10.268 +val map_compose = result();
  10.269 +
  10.270 +val prems = goal List.thy
  10.271 +    "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
  10.272 +by (list_ind_tac "xs" prems 1);
  10.273 +by (ALLGOALS (asm_simp_tac list_ss));
  10.274 +val map_app_distrib = result();
  10.275 +
  10.276 +val prems = goal List.thy
  10.277 +    "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
  10.278 +by (list_ind_tac "ls" prems 1);
  10.279 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
  10.280 +val map_flat = result();
  10.281 +
  10.282 +val prems = goal List.thy
  10.283 +    "l: list(A) ==> \
  10.284 +\    list_rec(map(h,l), c, d) = \
  10.285 +\    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
  10.286 +by (list_ind_tac "l" prems 1);
  10.287 +by (ALLGOALS (asm_simp_tac list_ss));
  10.288 +val list_rec_map = result();
  10.289 +
  10.290 +(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
  10.291 +
  10.292 +(* c : list(Collect(B,P)) ==> c : list(B) *)
  10.293 +val list_CollectD = standard (Collect_subset RS list_mono RS subsetD);
  10.294 +
  10.295 +val prems = goal List.thy
  10.296 +    "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
  10.297 +by (list_ind_tac "l" prems 1);
  10.298 +by (ALLGOALS (asm_simp_tac list_ss));
  10.299 +val map_list_Collect = result();
  10.300 +
  10.301 +(*** theorems about length ***)
  10.302 +
  10.303 +val prems = goal List.thy
  10.304 +    "xs: list(A) ==> length(map(h,xs)) = length(xs)";
  10.305 +by (list_ind_tac "xs" prems 1);
  10.306 +by (ALLGOALS (asm_simp_tac list_ss));
  10.307 +val length_map = result();
  10.308 +
  10.309 +val prems = goal List.thy
  10.310 +    "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
  10.311 +by (list_ind_tac "xs" prems 1);
  10.312 +by (ALLGOALS (asm_simp_tac list_ss));
  10.313 +val length_app = result();
  10.314 +
  10.315 +(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m 
  10.316 +   Used for rewriting below*)
  10.317 +val add_commute_succ = nat_succI RSN (2,add_commute);
  10.318 +
  10.319 +val prems = goal List.thy
  10.320 +    "xs: list(A) ==> length(rev(xs)) = length(xs)";
  10.321 +by (list_ind_tac "xs" prems 1);
  10.322 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ])));
  10.323 +val length_rev = result();
  10.324 +
  10.325 +val prems = goal List.thy
  10.326 +    "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
  10.327 +by (list_ind_tac "ls" prems 1);
  10.328 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
  10.329 +val length_flat = result();
  10.330 +
  10.331 +(** Length and drop **)
  10.332 +
  10.333 +(*Lemma for the inductive step of drop_length*)
  10.334 +goal List.thy
  10.335 +    "!!xs. xs: list(A) ==> \
  10.336 +\          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
  10.337 +by (etac list.induct 1);
  10.338 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [drop_0,drop_succ_Cons])));
  10.339 +by (fast_tac ZF_cs 1);
  10.340 +val drop_length_Cons_lemma = result();
  10.341 +val drop_length_Cons = standard (drop_length_Cons_lemma RS spec);
  10.342 +
  10.343 +goal List.thy
  10.344 +    "!!l. l: list(A) ==> ALL i: length(l).  EX z zs. drop(i,l) = Cons(z,zs)";
  10.345 +by (etac list.induct 1);
  10.346 +by (ALLGOALS (asm_simp_tac (list_ss addsimps bquant_simps)));
  10.347 +by (rtac conjI 1);
  10.348 +by (etac drop_length_Cons 1);
  10.349 +by (rtac ballI 1);
  10.350 +by (rtac natE 1);
  10.351 +by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
  10.352 +by (assume_tac 1);
  10.353 +by (asm_simp_tac (list_ss addsimps [drop_0]) 1);
  10.354 +by (fast_tac ZF_cs 1);
  10.355 +by (asm_simp_tac (list_ss addsimps [drop_succ_Cons]) 1);
  10.356 +by (dtac bspec 1);
  10.357 +by (fast_tac ZF_cs 2);
  10.358 +by (fast_tac (ZF_cs addEs [succ_in_naturalD,length_type]) 1);
  10.359 +val drop_length_lemma = result();
  10.360 +val drop_length = standard (drop_length_lemma RS bspec);
  10.361 +
  10.362 +
  10.363 +(*** theorems about app ***)
  10.364 +
  10.365 +val [major] = goal List.thy "xs: list(A) ==> xs@Nil=xs";
  10.366 +by (rtac (major RS list.induct) 1);
  10.367 +by (ALLGOALS (asm_simp_tac list_ss));
  10.368 +val app_right_Nil = result();
  10.369 +
  10.370 +val prems = goal List.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
  10.371 +by (list_ind_tac "xs" prems 1);
  10.372 +by (ALLGOALS (asm_simp_tac list_ss));
  10.373 +val app_assoc = result();
  10.374 +
  10.375 +val prems = goal List.thy
  10.376 +    "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
  10.377 +by (list_ind_tac "ls" prems 1);
  10.378 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
  10.379 +val flat_app_distrib = result();
  10.380 +
  10.381 +(*** theorems about rev ***)
  10.382 +
  10.383 +val prems = goal List.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
  10.384 +by (list_ind_tac "l" prems 1);
  10.385 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
  10.386 +val rev_map_distrib = result();
  10.387 +
  10.388 +(*Simplifier needs the premises as assumptions because rewriting will not
  10.389 +  instantiate the variable ?A in the rules' typing conditions; note that
  10.390 +  rev_type does not instantiate ?A.  Only the premises do.
  10.391 +*)
  10.392 +goal List.thy
  10.393 +    "!!xs. [| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
  10.394 +by (etac list.induct 1);
  10.395 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
  10.396 +val rev_app_distrib = result();
  10.397 +
  10.398 +val prems = goal List.thy "l: list(A) ==> rev(rev(l))=l";
  10.399 +by (list_ind_tac "l" prems 1);
  10.400 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
  10.401 +val rev_rev_ident = result();
  10.402 +
  10.403 +val prems = goal List.thy
  10.404 +    "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
  10.405 +by (list_ind_tac "ls" prems 1);
  10.406 +by (ALLGOALS (asm_simp_tac (list_ss addsimps 
  10.407 +       [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
  10.408 +val rev_flat = result();
  10.409 +
  10.410 +
  10.411 +(*** theorems about list_add ***)
  10.412 +
  10.413 +val prems = goal List.thy
  10.414 +    "[| xs: list(nat);  ys: list(nat) |] ==> \
  10.415 +\    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
  10.416 +by (cut_facts_tac prems 1);
  10.417 +by (list_ind_tac "xs" prems 1);
  10.418 +by (ALLGOALS 
  10.419 +    (asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym])));
  10.420 +by (rtac (add_commute RS subst_context) 1);
  10.421 +by (REPEAT (ares_tac [refl, list_add_type] 1));
  10.422 +val list_add_app = result();
  10.423 +
  10.424 +val prems = goal List.thy
  10.425 +    "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
  10.426 +by (list_ind_tac "l" prems 1);
  10.427 +by (ALLGOALS
  10.428 +    (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right])));
  10.429 +val list_add_rev = result();
  10.430 +
  10.431 +val prems = goal List.thy
  10.432 +    "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
  10.433 +by (list_ind_tac "ls" prems 1);
  10.434 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app])));
  10.435 +by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
  10.436 +val list_add_flat = result();
  10.437 +
  10.438 +(** New induction rule **)
  10.439 +
  10.440 +val major::prems = goal List.thy
  10.441 +    "[| l: list(A);  \
  10.442 +\       P(Nil);        \
  10.443 +\       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x]) \
  10.444 +\    |] ==> P(l)";
  10.445 +by (rtac (major RS rev_rev_ident RS subst) 1);
  10.446 +by (rtac (major RS rev_type RS list.induct) 1);
  10.447 +by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
  10.448 +val list_append_induct = result();
  10.449 +
    11.1 --- a/src/ZF/List.thy	Fri Aug 12 12:28:46 1994 +0200
    11.2 +++ b/src/ZF/List.thy	Fri Aug 12 12:51:34 1994 +0200
    11.3 @@ -1,3 +1,57 @@
    11.4 -(*Dummy theory to document dependencies *)
    11.5 +(*  Title: 	ZF/List
    11.6 +    ID:         $Id$
    11.7 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    11.8 +    Copyright   1994  University of Cambridge
    11.9 +
   11.10 +Lists in Zermelo-Fraenkel Set Theory 
   11.11 +
   11.12 +map is a binding operator -- it applies to meta-level functions, not 
   11.13 +object-level functions.  This simplifies the final form of term_rec_conv,
   11.14 +although complicating its derivation.
   11.15 +*)
   11.16 +
   11.17 +List = "Datatype" + Univ + 
   11.18 +
   11.19 +consts
   11.20 +  "@"	     :: "[i,i]=>i"      			(infixr 60)
   11.21 +  list_rec   :: "[i, i, [i,i,i]=>i] => i"
   11.22 +  map 	     :: "[i=>i, i] => i"
   11.23 +  length,rev :: "i=>i"
   11.24 +  flat       :: "i=>i"
   11.25 +  list_add   :: "i=>i"
   11.26 +  hd,tl      :: "i=>i"
   11.27 +  drop	     :: "[i,i]=>i"
   11.28 +
   11.29 + (* List Enumeration *)
   11.30 + "[]"        :: "i" 	                           	("[]")
   11.31 + "@List"     :: "is => i" 	                   	("[(_)]")
   11.32  
   11.33 -List = Univ + "Datatype" + "intr_elim"
   11.34 +  list	     :: "i=>i"
   11.35 +
   11.36 +  
   11.37 +datatype
   11.38 +  "list(A)" = "Nil" | "Cons" ("a:A", "l: list(A)")
   11.39 +
   11.40 +
   11.41 +translations
   11.42 +  "[x, xs]"     == "Cons(x, [xs])"
   11.43 +  "[x]"         == "Cons(x, [])"
   11.44 +  "[]"          == "Nil"
   11.45 +
   11.46 +
   11.47 +rules
   11.48 +
   11.49 +  hd_def	"hd(l)	     == list_case(0, %x xs.x, l)"
   11.50 +  tl_def	"tl(l)       == list_case(Nil, %x xs.xs, l)"
   11.51 +  drop_def	"drop(i,l)   == rec(i, l, %j r. tl(r))"
   11.52 +
   11.53 +  list_rec_def
   11.54 +      "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
   11.55 +
   11.56 +  map_def       "map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"
   11.57 +  length_def    "length(l)   == list_rec(l,  0,  %x xs r. succ(r))"
   11.58 +  app_def       "xs@ys       == list_rec(xs, ys, %x xs r. Cons(x,r))"
   11.59 +  rev_def       "rev(l)      == list_rec(l,  Nil,  %x xs r. r @ [x])"
   11.60 +  flat_def      "flat(ls)    == list_rec(ls, Nil,  %l ls r. l @ r)"
   11.61 +  list_add_def  "list_add(l) == list_rec(l, 0,  %x xs r. x#+r)"
   11.62 +end
    12.1 --- a/src/ZF/Makefile	Fri Aug 12 12:28:46 1994 +0200
    12.2 +++ b/src/ZF/Makefile	Fri Aug 12 12:51:34 1994 +0200
    12.3 @@ -21,7 +21,8 @@
    12.4  FILES = ROOT.ML ZF.thy ZF.ML upair.ML subset.ML pair.ML domrange.ML \
    12.5  	func.ML AC.thy AC.ML simpdata.ML Bool.thy Bool.ML \
    12.6  	Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \
    12.7 -	ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \
    12.8 +	ind_syntax.ML add_ind_def.thy add_ind_def.ML \
    12.9 +\       intr_elim.ML indrule.ML inductive.ML \
   12.10  	equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \
   12.11  	WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
   12.12  	Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
   12.13 @@ -29,25 +30,23 @@
   12.14  	OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \
   12.15  	Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \
   12.16  	Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \
   12.17 -	Zorn0.thy Zorn0.ML Zorn.thy Zorn.ML Nat.thy Nat.ML Fin.ML \
   12.18 -	List.ML ListFn.thy ListFn.ML
   12.19 +	Zorn.thy Zorn.ML Nat.thy Nat.ML Finite.thy Finite.ML \
   12.20 +	List.thy List.ML
   12.21  
   12.22 -IMP_FILES = IMP/ROOT.ML IMP/Aexp.ML IMP/Aexp.thy IMP/Assign.ML IMP/Assign.thy\
   12.23 -            IMP/Bexp.ML IMP/Bexp.thy IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
   12.24 -            IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/Evala0.thy\
   12.25 -            IMP/Evala.ML IMP/Evala.thy IMP/Evalb0.thy IMP/Evalb.ML\
   12.26 -            IMP/Evalb.thy IMP/Evalc0.thy IMP/Evalc.ML IMP/Evalc.thy
   12.27 +IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
   12.28 +            IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy
   12.29  
   12.30 -EX_FILES = ex/ROOT.ML ex/Acc.ML ex/Bin.ML ex/BinFn.ML ex/BinFn.thy\
   12.31 -	   ex/BT.ML ex/BT_Fn.ML ex/BT_Fn.thy ex/Comb.ML\
   12.32 -	   ex/Contract0.ML ex/Contract0.thy ex/CoUnit.ML ex/Data.ML\
   12.33 -	   ex/Enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\
   12.34 -	   ex/ListN.ML ex/LList.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\
   12.35 -	   ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\
   12.36 -	   ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\
   12.37 -	   ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy \
   12.38 -	   ex/Ntree.ML ex/Brouwer.ML \
   12.39 -	   ex/TF.ML ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML
   12.40 +EX_FILES = ex/ROOT.ML ex/misc.ML ex/Ramsey.ML ex/Ramsey.thy\
   12.41 +	   ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\
   12.42 +           ex/twos_compl.ML ex/Bin.thy ex/Bin.ML\
   12.43 +	   ex/BT.thy ex/BT.ML ex/Term.thy ex/Term.ML \
   12.44 +	   ex/TF.thy ex/TF.ML ex/Ntree.thy ex/Ntree.ML \
   12.45 +           ex/Brouwer.thy ex/Brouwer.ML \
   12.46 +	   ex/Data.thy ex/Data.ML ex/Enum.thy ex/Enum.ML \
   12.47 +	   ex/Rmap.thy ex/Rmap.ML ex/PropLog.ML ex/PropLog.thy \
   12.48 +	   ex/ListN.thy ex/ListN.ML ex/Acc.thy ex/Acc.ML\
   12.49 +	   ex/Comb.thy ex/Comb.ML ex/Primrec.thy ex/Primrec.ML\
   12.50 +           ex/LList.thy ex/LList.ML ex/CoUnit.thy ex/CoUnit.ML
   12.51  
   12.52  #Uses cp rather than make_database because Poly/ML allows only 3 levels
   12.53  $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
    13.1 --- a/src/ZF/QPair.ML	Fri Aug 12 12:28:46 1994 +0200
    13.2 +++ b/src/ZF/QPair.ML	Fri Aug 12 12:51:34 1994 +0200
    13.3 @@ -208,8 +208,8 @@
    13.4  val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE);
    13.5  
    13.6  val qsum_cs = 
    13.7 -    ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
    13.8 -          addSDs [QInl_inject,QInr_inject];
    13.9 +    qpair_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
   13.10 +             addSDs [QInl_inject,QInr_inject];
   13.11  
   13.12  goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A";
   13.13  by (fast_tac qsum_cs 1);
    14.1 --- a/src/ZF/QPair.thy	Fri Aug 12 12:28:46 1994 +0200
    14.2 +++ b/src/ZF/QPair.thy	Fri Aug 12 12:51:34 1994 +0200
    14.3 @@ -45,4 +45,4 @@
    14.4  ML
    14.5  
    14.6  val print_translation =
    14.7 -  [("QSigma", dependent_tr' ("@QSUM", " <*>"))];
    14.8 +  [("QSigma", dependent_tr' ("@QSUM", "<*>"))];
    15.1 --- a/src/ZF/ROOT.ML	Fri Aug 12 12:28:46 1994 +0200
    15.2 +++ b/src/ZF/ROOT.ML	Fri Aug 12 12:51:34 1994 +0200
    15.3 @@ -28,8 +28,20 @@
    15.4  
    15.5  print_depth 1;
    15.6  
    15.7 +(*Add user sections for inductive/datatype definitions*)
    15.8 +use_thy "Datatype";
    15.9 +structure ThySyn = ThySynFun
   15.10 + (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
   15.11 +		       "and", "|", "<=", "domains", "intrs", "monos", 
   15.12 +		       "con_defs", "type_intrs", "type_elims"] 
   15.13 +  and user_sections = [("inductive",  inductive_decl ""),
   15.14 +		       ("coinductive",  inductive_decl "Co"),
   15.15 +		       ("datatype",  datatype_decl ""),
   15.16 +		       ("codatatype",  datatype_decl "Co")]);
   15.17 +init_thy_reader ();
   15.18 +
   15.19  use_thy "InfDatatype";
   15.20 -use_thy "ListFn";
   15.21 +use_thy "List";
   15.22  
   15.23  (*printing functions are inherited from FOL*)
   15.24  print_depth 8;
    16.1 --- a/src/ZF/Univ.ML	Fri Aug 12 12:28:46 1994 +0200
    16.2 +++ b/src/ZF/Univ.ML	Fri Aug 12 12:51:34 1994 +0200
    16.3 @@ -202,14 +202,14 @@
    16.4  by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
    16.5  val Limit_VfromE = result();
    16.6  
    16.7 -val zero_in_Vfrom_Limit = Limit_has_0 RS ltD RS zero_in_Vfrom;
    16.8 +val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom;
    16.9  
   16.10  val [major,limiti] = goal Univ.thy
   16.11      "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
   16.12  by (rtac ([major,limiti] MRS Limit_VfromE) 1);
   16.13  by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
   16.14  by (etac (limiti RS Limit_has_succ) 1);
   16.15 -val singleton_in_Vfrom_Limit = result();
   16.16 +val singleton_in_VLimit = result();
   16.17  
   16.18  val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
   16.19  and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
   16.20 @@ -224,7 +224,7 @@
   16.21  by (etac Vfrom_UnI1 1);
   16.22  by (etac Vfrom_UnI2 1);
   16.23  by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
   16.24 -val doubleton_in_Vfrom_Limit = result();
   16.25 +val doubleton_in_VLimit = result();
   16.26  
   16.27  val [aprem,bprem,limiti] = goal Univ.thy
   16.28      "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
   16.29 @@ -237,83 +237,48 @@
   16.30  by (etac Vfrom_UnI1 1);
   16.31  by (etac Vfrom_UnI2 1);
   16.32  by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
   16.33 -val Pair_in_Vfrom_Limit = result();
   16.34 +val Pair_in_VLimit = result();
   16.35  
   16.36  goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)";
   16.37 -by (REPEAT (ares_tac [subsetI,Pair_in_Vfrom_Limit] 1
   16.38 +by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1
   16.39       ORELSE eresolve_tac [SigmaE, ssubst] 1));
   16.40 -val product_Vfrom_Limit = result();
   16.41 +val product_VLimit = result();
   16.42  
   16.43 -val Sigma_subset_Vfrom_Limit = 
   16.44 -    [Sigma_mono, product_Vfrom_Limit] MRS subset_trans |> standard;
   16.45 +val Sigma_subset_VLimit = 
   16.46 +    [Sigma_mono, product_VLimit] MRS subset_trans |> standard;
   16.47  
   16.48 -val nat_subset_Vfrom_Limit = 
   16.49 +val nat_subset_VLimit = 
   16.50      [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans 
   16.51  	|> standard;
   16.52  
   16.53  goal Univ.thy "!!i. [| n: nat;  Limit(i) |] ==> n : Vfrom(A,i)";
   16.54 -by (REPEAT (ares_tac [nat_subset_Vfrom_Limit RS subsetD] 1));
   16.55 -val nat_into_Vfrom_Limit = result();
   16.56 +by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1));
   16.57 +val nat_into_VLimit = result();
   16.58  
   16.59  (** Closure under disjoint union **)
   16.60  
   16.61 -val zero_in_Vfrom_Limit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard;
   16.62 +val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard;
   16.63  
   16.64  goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)";
   16.65 -by (REPEAT (ares_tac [nat_into_Vfrom_Limit, nat_0I, nat_succI] 1));
   16.66 -val one_in_Vfrom_Limit = result();
   16.67 +by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1));
   16.68 +val one_in_VLimit = result();
   16.69  
   16.70  goalw Univ.thy [Inl_def]
   16.71      "!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)";
   16.72 -by (REPEAT (ares_tac [zero_in_Vfrom_Limit, Pair_in_Vfrom_Limit] 1));
   16.73 -val Inl_in_Vfrom_Limit = result();
   16.74 +by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1));
   16.75 +val Inl_in_VLimit = result();
   16.76  
   16.77  goalw Univ.thy [Inr_def]
   16.78      "!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)";
   16.79 -by (REPEAT (ares_tac [one_in_Vfrom_Limit, Pair_in_Vfrom_Limit] 1));
   16.80 -val Inr_in_Vfrom_Limit = result();
   16.81 +by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1));
   16.82 +val Inr_in_VLimit = result();
   16.83  
   16.84  goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
   16.85 -by (fast_tac (sum_cs addSIs [Inl_in_Vfrom_Limit, Inr_in_Vfrom_Limit]) 1);
   16.86 -val sum_Vfrom_Limit = result();
   16.87 -
   16.88 -val sum_subset_Vfrom_Limit = 
   16.89 -    [sum_mono, sum_Vfrom_Limit] MRS subset_trans |> standard;
   16.90 -
   16.91 -
   16.92 -(** Closure under finite powerset **)
   16.93 +by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
   16.94 +val sum_VLimit = result();
   16.95  
   16.96 -goal Univ.thy
   16.97 -   "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
   16.98 -by (eresolve_tac [Fin_induct] 1);
   16.99 -by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1);
  16.100 -by (safe_tac ZF_cs);
  16.101 -by (eresolve_tac [Limit_VfromE] 1);
  16.102 -by (assume_tac 1);
  16.103 -by (res_inst_tac [("x", "xa Un j")] exI 1);
  16.104 -by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, 
  16.105 -			   Un_least_lt]) 1);
  16.106 -val Fin_Vfrom_lemma = result();
  16.107 -
  16.108 -goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
  16.109 -by (rtac subsetI 1);
  16.110 -by (dresolve_tac [Fin_Vfrom_lemma] 1);
  16.111 -by (safe_tac ZF_cs);
  16.112 -by (resolve_tac [Vfrom RS ssubst] 1);
  16.113 -by (fast_tac (ZF_cs addSDs [ltD]) 1);
  16.114 -val Fin_Vfrom_Limit = result();
  16.115 -
  16.116 -val Fin_subset_Vfrom_Limit = 
  16.117 -    [Fin_mono, Fin_Vfrom_Limit] MRS subset_trans |> standard;
  16.118 -
  16.119 -goal Univ.thy "!!i. [| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
  16.120 -by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
  16.121 -by (REPEAT (ares_tac [Fin_subset_Vfrom_Limit, Sigma_subset_Vfrom_Limit,
  16.122 -		      nat_subset_Vfrom_Limit, subset_refl] 1));
  16.123 -val nat_fun_Vfrom_Limit = result();
  16.124 -
  16.125 -val nat_fun_subset_Vfrom_Limit = 
  16.126 -    [Pi_mono, nat_fun_Vfrom_Limit] MRS subset_trans |> standard;
  16.127 +val sum_subset_VLimit = 
  16.128 +    [sum_mono, sum_VLimit] MRS subset_trans |> standard;
  16.129  
  16.130  
  16.131  
  16.132 @@ -344,8 +309,8 @@
  16.133  \          <a,b> : Vfrom(A,i)";
  16.134  by (etac (Transset_Pair_subset RS conjE) 1);
  16.135  by (etac Transset_Vfrom 1);
  16.136 -by (REPEAT (ares_tac [Pair_in_Vfrom_Limit] 1));
  16.137 -val Transset_Pair_subset_Vfrom_Limit = result();
  16.138 +by (REPEAT (ares_tac [Pair_in_VLimit] 1));
  16.139 +val Transset_Pair_subset_VLimit = result();
  16.140  
  16.141  
  16.142  (*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
  16.143 @@ -368,7 +333,7 @@
  16.144  by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
  16.145  by (rtac (succI1 RS UnI2) 2);
  16.146  by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1));
  16.147 -val in_Vfrom_Limit = result();
  16.148 +val in_VLimit = result();
  16.149  
  16.150  (** products **)
  16.151  
  16.152 @@ -384,10 +349,10 @@
  16.153  val [aprem,bprem,limiti,transset] = goal Univ.thy
  16.154    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
  16.155  \  a*b : Vfrom(A,i)";
  16.156 -by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1);
  16.157 +by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
  16.158  by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset,
  16.159  		      limiti RS Limit_has_succ] 1));
  16.160 -val prod_in_Vfrom_Limit = result();
  16.161 +val prod_in_VLimit = result();
  16.162  
  16.163  (** Disjoint sums, aka Quine ordered pairs **)
  16.164  
  16.165 @@ -404,10 +369,10 @@
  16.166  val [aprem,bprem,limiti,transset] = goal Univ.thy
  16.167    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
  16.168  \  a+b : Vfrom(A,i)";
  16.169 -by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1);
  16.170 +by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
  16.171  by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset,
  16.172  		      limiti RS Limit_has_succ] 1));
  16.173 -val sum_in_Vfrom_Limit = result();
  16.174 +val sum_in_VLimit = result();
  16.175  
  16.176  (** function space! **)
  16.177  
  16.178 @@ -429,10 +394,10 @@
  16.179  val [aprem,bprem,limiti,transset] = goal Univ.thy
  16.180    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
  16.181  \  a->b : Vfrom(A,i)";
  16.182 -by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1);
  16.183 +by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
  16.184  by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset,
  16.185  		      limiti RS Limit_has_succ] 1));
  16.186 -val fun_in_Vfrom_Limit = result();
  16.187 +val fun_in_VLimit = result();
  16.188  
  16.189  
  16.190  (*** The set Vset(i) ***)
  16.191 @@ -594,21 +559,21 @@
  16.192  (** Closure under unordered and ordered pairs **)
  16.193  
  16.194  goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
  16.195 -by (REPEAT (ares_tac [singleton_in_Vfrom_Limit, Limit_nat] 1));
  16.196 +by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1));
  16.197  val singleton_in_univ = result();
  16.198  
  16.199  goalw Univ.thy [univ_def] 
  16.200      "!!A a. [| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
  16.201 -by (REPEAT (ares_tac [doubleton_in_Vfrom_Limit, Limit_nat] 1));
  16.202 +by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1));
  16.203  val doubleton_in_univ = result();
  16.204  
  16.205  goalw Univ.thy [univ_def]
  16.206      "!!A a. [| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
  16.207 -by (REPEAT (ares_tac [Pair_in_Vfrom_Limit, Limit_nat] 1));
  16.208 +by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1));
  16.209  val Pair_in_univ = result();
  16.210  
  16.211  goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)";
  16.212 -by (rtac (Limit_nat RS product_Vfrom_Limit) 1);
  16.213 +by (rtac (Limit_nat RS product_VLimit) 1);
  16.214  val product_univ = result();
  16.215  
  16.216  val Sigma_subset_univ = 
  16.217 @@ -616,7 +581,7 @@
  16.218  
  16.219  goalw Univ.thy [univ_def]
  16.220      "!!a b.[| <a,b> <= univ(A);  Transset(A) |] ==> <a,b> : univ(A)";
  16.221 -by (etac Transset_Pair_subset_Vfrom_Limit 1);
  16.222 +by (etac Transset_Pair_subset_VLimit 1);
  16.223  by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
  16.224  val Transset_Pair_subset_univ = result();
  16.225  
  16.226 @@ -633,7 +598,7 @@
  16.227  (** instances for 1 and 2 **)
  16.228  
  16.229  goalw Univ.thy [univ_def] "1 : univ(A)";
  16.230 -by (rtac (Limit_nat RS one_in_Vfrom_Limit) 1);
  16.231 +by (rtac (Limit_nat RS one_in_VLimit) 1);
  16.232  val one_in_univ = result();
  16.233  
  16.234  (*unused!*)
  16.235 @@ -651,38 +616,20 @@
  16.236  (** Closure under disjoint union **)
  16.237  
  16.238  goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
  16.239 -by (etac (Limit_nat RSN (2,Inl_in_Vfrom_Limit)) 1);
  16.240 +by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1);
  16.241  val Inl_in_univ = result();
  16.242  
  16.243  goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
  16.244 -by (etac (Limit_nat RSN (2,Inr_in_Vfrom_Limit)) 1);
  16.245 +by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1);
  16.246  val Inr_in_univ = result();
  16.247  
  16.248  goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)";
  16.249 -by (rtac (Limit_nat RS sum_Vfrom_Limit) 1);
  16.250 +by (rtac (Limit_nat RS sum_VLimit) 1);
  16.251  val sum_univ = result();
  16.252  
  16.253  val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans |> standard;
  16.254  
  16.255  
  16.256 -(** Closure under finite powerset **)
  16.257 -
  16.258 -goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)";
  16.259 -by (rtac (Limit_nat RS Fin_Vfrom_Limit) 1);
  16.260 -val Fin_univ = result();
  16.261 -
  16.262 -val Fin_subset_univ = [Fin_mono, Fin_univ] MRS subset_trans |> standard;
  16.263 -
  16.264 -goalw Univ.thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
  16.265 -by (etac (Limit_nat RSN (2,nat_fun_Vfrom_Limit)) 1);
  16.266 -val nat_fun_univ = result();
  16.267 -
  16.268 -val nat_fun_subset_univ = [Pi_mono, nat_fun_univ] MRS subset_trans |> standard;
  16.269 -
  16.270 -goal Univ.thy "!!f. [| f: n -> B;  B <= univ(A);  n : nat |] ==> f : univ(A)";
  16.271 -by (REPEAT (ares_tac [nat_fun_subset_univ RS subsetD] 1));
  16.272 -val nat_fun_into_univ = result();
  16.273 -
  16.274  (** Closure under binary union -- use Un_least **)
  16.275  (** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
  16.276  (** Closure under RepFun -- use   RepFun_subset  **)
    17.1 --- a/src/ZF/Univ.thy	Fri Aug 12 12:28:46 1994 +0200
    17.2 +++ b/src/ZF/Univ.thy	Fri Aug 12 12:51:34 1994 +0200
    17.3 @@ -6,9 +6,12 @@
    17.4  The cumulative hierarchy and a small universe for recursive types
    17.5  
    17.6  Standard notation for Vset(i) is V(i), but users might want V for a variable
    17.7 +
    17.8 +NOTE: univ(A) could be a translation; would simplify many proofs!
    17.9 +  But Ind_Syntax.univ refers to the constant "univ"
   17.10  *)
   17.11  
   17.12 -Univ = Arith + Sum + Fin + "mono" +
   17.13 +Univ = Arith + Sum + "mono" +
   17.14  consts
   17.15      Vfrom       :: "[i,i]=>i"
   17.16      Vset        :: "i=>i"
    18.1 --- a/src/ZF/ZF.ML	Fri Aug 12 12:28:46 1994 +0200
    18.2 +++ b/src/ZF/ZF.ML	Fri Aug 12 12:51:34 1994 +0200
    18.3 @@ -10,69 +10,70 @@
    18.4  
    18.5  signature ZF_LEMMAS = 
    18.6    sig
    18.7 -  val ballE	: thm
    18.8 -  val ballI	: thm
    18.9 -  val ball_cong	: thm
   18.10 -  val ball_simp	: thm
   18.11 -  val ball_tac	: int -> tactic
   18.12 -  val bexCI	: thm
   18.13 -  val bexE	: thm
   18.14 -  val bexI	: thm
   18.15 -  val bex_cong	: thm
   18.16 -  val bspec	: thm
   18.17 -  val CollectD1	: thm
   18.18 -  val CollectD2	: thm
   18.19 -  val CollectE	: thm
   18.20 -  val CollectI	: thm
   18.21 +  val ballE		: thm
   18.22 +  val ballI		: thm
   18.23 +  val ball_cong		: thm
   18.24 +  val ball_simp		: thm
   18.25 +  val ball_tac		: int -> tactic
   18.26 +  val bexCI		: thm
   18.27 +  val bexE		: thm
   18.28 +  val bexI		: thm
   18.29 +  val bex_cong		: thm
   18.30 +  val bspec		: thm
   18.31 +  val CollectD1		: thm
   18.32 +  val CollectD2		: thm
   18.33 +  val CollectE		: thm
   18.34 +  val CollectI		: thm
   18.35    val Collect_cong	: thm
   18.36 -  val emptyE	: thm
   18.37 +  val emptyE		: thm
   18.38    val empty_subsetI	: thm
   18.39    val equalityCE	: thm
   18.40    val equalityD1	: thm
   18.41    val equalityD2	: thm
   18.42 -  val equalityE	: thm
   18.43 -  val equalityI	: thm
   18.44 +  val equalityE		: thm
   18.45 +  val equalityI		: thm
   18.46    val equality_iffI	: thm
   18.47 -  val equals0D	: thm
   18.48 -  val equals0I	: thm
   18.49 +  val equals0D		: thm
   18.50 +  val equals0I		: thm
   18.51    val ex1_functional	: thm
   18.52 -  val InterD	: thm
   18.53 -  val InterE	: thm
   18.54 -  val InterI	: thm
   18.55 -  val Inter_iff : thm
   18.56 -  val INT_E	: thm
   18.57 -  val INT_I	: thm
   18.58 -  val INT_cong	: thm
   18.59 -  val lemmas_cs	: claset
   18.60 -  val PowD	: thm
   18.61 -  val PowI	: thm
   18.62 -  val RepFunE	: thm
   18.63 -  val RepFunI	: thm
   18.64 +  val InterD		: thm
   18.65 +  val InterE		: thm
   18.66 +  val InterI		: thm
   18.67 +  val Inter_iff 	: thm
   18.68 +  val INT_E		: thm
   18.69 +  val INT_I		: thm
   18.70 +  val INT_cong		: thm
   18.71 +  val lemmas_cs		: claset
   18.72 +  val PowD		: thm
   18.73 +  val PowI		: thm
   18.74 +  val RepFunE		: thm
   18.75 +  val RepFunI		: thm
   18.76    val RepFun_eqI	: thm
   18.77    val RepFun_cong	: thm
   18.78    val RepFun_iff	: thm
   18.79 -  val ReplaceE	: thm
   18.80 -  val ReplaceE2	: thm
   18.81 -  val ReplaceI	: thm
   18.82 +  val ReplaceE		: thm
   18.83 +  val ReplaceE2		: thm
   18.84 +  val ReplaceI		: thm
   18.85    val Replace_iff	: thm
   18.86    val Replace_cong	: thm
   18.87 -  val rev_ballE	: thm
   18.88 -  val rev_bspec	: thm
   18.89 +  val rev_ballE		: thm
   18.90 +  val rev_bspec		: thm
   18.91    val rev_subsetD	: thm
   18.92    val separation	: thm
   18.93    val setup_induction	: thm
   18.94    val set_mp_tac	: int -> tactic
   18.95 -  val subsetCE	: thm
   18.96 -  val subsetD	: thm
   18.97 -  val subsetI	: thm
   18.98 +  val subsetCE		: thm
   18.99 +  val subsetD		: thm
  18.100 +  val subsetI		: thm
  18.101    val subset_iff	: thm
  18.102    val subset_refl	: thm
  18.103    val subset_trans	: thm
  18.104 -  val UnionE	: thm
  18.105 -  val UnionI	: thm
  18.106 -  val UN_E	: thm
  18.107 -  val UN_I	: thm
  18.108 -  val UN_cong	: thm
  18.109 +  val UnionE		: thm
  18.110 +  val UnionI		: thm
  18.111 +  val Union_in_Pow	: thm
  18.112 +  val UN_E		: thm
  18.113 +  val UN_I		: thm
  18.114 +  val UN_cong		: thm
  18.115    end;
  18.116  
  18.117  
  18.118 @@ -479,6 +480,11 @@
  18.119  	  CollectE, emptyE]
  18.120    addEs [rev_ballE, InterD, make_elim InterD, subsetD, subsetCE];
  18.121  
  18.122 +(*Lemma for the inductive definition in Zorn.thy*)
  18.123 +val Union_in_Pow = prove_goal ZF.thy
  18.124 +    "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"
  18.125 + (fn _ => [fast_tac lemmas_cs 1]);
  18.126 +
  18.127  end;
  18.128  
  18.129  open ZF_Lemmas;
    19.1 --- a/src/ZF/ZF.thy	Fri Aug 12 12:28:46 1994 +0200
    19.2 +++ b/src/ZF/ZF.thy	Fri Aug 12 12:51:34 1994 +0200
    19.3 @@ -91,11 +91,11 @@
    19.4    "`"   :: "[i, i] => i"    (infixl 90) (*function application*)
    19.5  
    19.6    (*Except for their translations, * and -> are right and ~: left associative infixes*)
    19.7 -  " *"  :: "[i, i] => i"    ("(_ */ _)" [81, 80] 80) (*Cartesian product*)
    19.8 +  "*"  :: "[i, i] => i"    ("(_ */ _)" [81, 80] 80) (*Cartesian product*)
    19.9    "Int" :: "[i, i] => i"    (infixl 70) (*binary intersection*)
   19.10    "Un"  :: "[i, i] => i"    (infixl 65) (*binary union*)
   19.11    "-"   :: "[i, i] => i"    (infixl 65) (*set difference*)
   19.12 -  " ->" :: "[i, i] => i"    ("(_ ->/ _)" [61, 60] 60) (*function space*)
   19.13 +  "->" :: "[i, i] => i"    ("(_ ->/ _)" [61, 60] 60) (*function space*)
   19.14    "<="  :: "[i, i] => o"    (infixl 50) (*subset relation*)
   19.15    ":"   :: "[i, i] => o"    (infixl 50) (*membership relation*)
   19.16    "~:"  :: "[i, i] => o"    ("(_ ~:/ _)" [50, 51] 50) (*negated membership relation*)
   19.17 @@ -215,6 +215,6 @@
   19.18  (* 'Dependent' type operators *)
   19.19  
   19.20  val print_translation =
   19.21 -  [("Pi", dependent_tr' ("@PROD", " ->")),
   19.22 -   ("Sigma", dependent_tr' ("@SUM", " *"))];
   19.23 +  [("Pi", dependent_tr' ("@PROD", "->")),
   19.24 +   ("Sigma", dependent_tr' ("@SUM", "*"))];
   19.25  
    20.1 --- a/src/ZF/Zorn.ML	Fri Aug 12 12:28:46 1994 +0200
    20.2 +++ b/src/ZF/Zorn.ML	Fri Aug 12 12:51:34 1994 +0200
    20.3 @@ -3,30 +3,52 @@
    20.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    20.5      Copyright   1994  University of Cambridge
    20.6  
    20.7 -Conclusion to proofs from the paper
    20.8 +Proofs from the paper
    20.9      Abrial & Laffitte, 
   20.10      Towards the Mechanization of the Proofs of Some 
   20.11      Classical Theorems of Set Theory. 
   20.12  *)
   20.13  
   20.14 +open Zorn;
   20.15  
   20.16 -structure Zorn = Inductive_Fun
   20.17 - (val thy        = Zorn0.thy |> add_consts [("TFin", "[i,i]=>i", NoSyn)]
   20.18 -  val thy_name   = "Zorn"
   20.19 -  val rec_doms   = [("TFin","Pow(S)")]
   20.20 -  val sintrs     = ["[| x : TFin(S,next);  next: increasing(S) \
   20.21 -\                    |] ==> next`x : TFin(S,next)",
   20.22 -                    "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"]
   20.23 -  val monos      = [Pow_mono]
   20.24 -  val con_defs   = []
   20.25 -  val type_intrs = [next_bounded, Union_in_Pow]
   20.26 -  val type_elims = []);
   20.27 +(*** Section 1.  Mathematical Preamble ***)
   20.28 +
   20.29 +goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
   20.30 +by (fast_tac ZF_cs 1);
   20.31 +val Union_lemma0 = result();
   20.32 +
   20.33 +goal ZF.thy
   20.34 +    "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
   20.35 +by (fast_tac ZF_cs 1);
   20.36 +val Inter_lemma0 = result();
   20.37 +
   20.38 +
   20.39 +(*** Section 2.  The Transfinite Construction ***)
   20.40 +
   20.41 +goalw Zorn.thy [increasing_def]
   20.42 +    "!!f A. f: increasing(A) ==> f: Pow(A)->Pow(A)";
   20.43 +by (eresolve_tac [CollectD1] 1);
   20.44 +val increasingD1 = result();
   20.45 +
   20.46 +goalw Zorn.thy [increasing_def]
   20.47 +    "!!f A. [| f: increasing(A); x<=A |] ==> x <= f`x";
   20.48 +by (eresolve_tac [CollectD2 RS spec RS mp] 1);
   20.49 +by (assume_tac 1);
   20.50 +val increasingD2 = result();
   20.51 +
   20.52 +(*????????????????????????????????????????????????????????????????
   20.53 +goal Zorn.thy
   20.54 +    "!!next S. [| X : Pow(S);  next: increasing(S) |] ==> next`X : Pow(S)";
   20.55 +by (eresolve_tac [increasingD1 RS apply_type] 1);
   20.56 +by (assume_tac 1);
   20.57 +val next_bounded = result();
   20.58 +*)
   20.59  
   20.60  (*Introduction rules*)
   20.61 -val [TFin_nextI, Pow_TFin_UnionI] = Zorn.intrs;
   20.62 +val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs;
   20.63  val TFin_UnionI = PowI RS Pow_TFin_UnionI;
   20.64  
   20.65 -val TFin_is_subset = Zorn.dom_subset RS subsetD RS PowD;
   20.66 +val TFin_is_subset = TFin.dom_subset RS subsetD RS PowD;
   20.67  
   20.68  
   20.69  (** Structural induction on TFin(S,next) **)
   20.70 @@ -36,7 +58,7 @@
   20.71  \     !!x. [| x : TFin(S,next);  P(x);  next: increasing(S) |] ==> P(next`x); \
   20.72  \     !!Y. [| Y <= TFin(S,next);  ALL y:Y. P(y) |] ==> P(Union(Y)) \
   20.73  \  |] ==> P(n)";
   20.74 -by (rtac (major RS Zorn.induct) 1);
   20.75 +by (rtac (major RS TFin.induct) 1);
   20.76  by (ALLGOALS (fast_tac (ZF_cs addIs prems)));
   20.77  val TFin_induct = result();
   20.78  
   20.79 @@ -240,7 +262,7 @@
   20.80  by (resolve_tac [refl] 2);
   20.81  by (asm_full_simp_tac 
   20.82      (ZF_ss addsimps [subset_refl RS TFin_UnionI RS
   20.83 -		     (Zorn.dom_subset RS subsetD)]
   20.84 +		     (TFin.dom_subset RS subsetD)]
   20.85             setloop split_tac [expand_if]) 1);
   20.86  by (eresolve_tac [choice_not_equals RS notE] 1);
   20.87  by (REPEAT (assume_tac 1));
    21.1 --- a/src/ZF/Zorn.thy	Fri Aug 12 12:28:46 1994 +0200
    21.2 +++ b/src/ZF/Zorn.thy	Fri Aug 12 12:51:34 1994 +0200
    21.3 @@ -1,3 +1,51 @@
    21.4 -(*Dummy theory to document dependencies *)
    21.5 +(*  Title: 	ZF/Zorn.thy
    21.6 +    ID:         $Id$
    21.7 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    21.8 +    Copyright   1994  University of Cambridge
    21.9 +
   21.10 +Based upon the article
   21.11 +    Abrial & Laffitte, 
   21.12 +    Towards the Mechanization of the Proofs of Some 
   21.13 +    Classical Theorems of Set Theory. 
   21.14 +
   21.15 +Union_in_Pow is proved in ZF.ML
   21.16 +*)
   21.17 +
   21.18 +Zorn = OrderArith + AC + "inductive" +
   21.19 +
   21.20 +consts
   21.21 +  Subset_rel      :: "i=>i"
   21.22 +  increasing      :: "i=>i"
   21.23 +  chain, maxchain :: "i=>i"
   21.24 +  super           :: "[i,i]=>i"
   21.25 +
   21.26 +rules
   21.27 +  Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
   21.28 +  increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
   21.29  
   21.30 -Zorn = Zorn0
   21.31 +  chain_def      "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
   21.32 +  super_def      "super(A,c)    == {d: chain(A). c<=d & c~=d}"
   21.33 +  maxchain_def   "maxchain(A)   == {c: chain(A). super(A,c)=0}"
   21.34 +
   21.35 +
   21.36 +(** We could make the inductive definition conditional on next: increasing(S)
   21.37 +    but instead we make this a side-condition of an introduction rule.  Thus
   21.38 +    the induction rule lets us assume that condition!  Many inductive proofs
   21.39 +    are therefore unconditional.
   21.40 +**)
   21.41 +consts
   21.42 +  "TFin" :: "[i,i]=>i"
   21.43 +
   21.44 +inductive
   21.45 +  domains       "TFin(S,next)" <= "Pow(S)"
   21.46 +  intrs
   21.47 +    nextI	"[| x : TFin(S,next);  next: increasing(S) \
   21.48 +\                |] ==> next`x : TFin(S,next)"
   21.49 +
   21.50 +    Pow_UnionI	"Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
   21.51 +
   21.52 +  monos         "[Pow_mono]"
   21.53 +  con_defs      "[increasing_def]"
   21.54 +  type_intrs    "[CollectD1 RS apply_funtype, Union_in_Pow]"
   21.55 +  
   21.56 +end
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/ZF/add_ind_def.ML	Fri Aug 12 12:51:34 1994 +0200
    22.3 @@ -0,0 +1,267 @@
    22.4 +(*  Title: 	ZF/add_ind_def.ML
    22.5 +    ID:         $Id$
    22.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7 +    Copyright   1994  University of Cambridge
    22.8 +
    22.9 +Fixedpoint definition module -- for Inductive/Coinductive Definitions
   22.10 +
   22.11 +Features:
   22.12 +* least or greatest fixedpoints
   22.13 +* user-specified product and sum constructions
   22.14 +* mutually recursive definitions
   22.15 +* definitions involving arbitrary monotone operators
   22.16 +* automatically proves introduction and elimination rules
   22.17 +
   22.18 +The recursive sets must *already* be declared as constants in parent theory!
   22.19 +
   22.20 +  Introduction rules have the form
   22.21 +  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
   22.22 +  where M is some monotone operator (usually the identity)
   22.23 +  P(x) is any (non-conjunctive) side condition on the free variables
   22.24 +  ti, t are any terms
   22.25 +  Sj, Sk are two of the sets being defined in mutual recursion
   22.26 +
   22.27 +Sums are used only for mutual recursion;
   22.28 +Products are used only to derive "streamlined" induction rules for relations
   22.29 +*)
   22.30 +
   22.31 +signature FP =		(** Description of a fixed point operator **)
   22.32 +  sig
   22.33 +  val oper	: term			(*fixed point operator*)
   22.34 +  val bnd_mono	: term			(*monotonicity predicate*)
   22.35 +  val bnd_monoI	: thm			(*intro rule for bnd_mono*)
   22.36 +  val subs	: thm			(*subset theorem for fp*)
   22.37 +  val Tarski	: thm			(*Tarski's fixed point theorem*)
   22.38 +  val induct	: thm			(*induction/coinduction rule*)
   22.39 +  end;
   22.40 +
   22.41 +signature PR =			(** Description of a Cartesian product **)
   22.42 +  sig
   22.43 +  val sigma	: term			(*Cartesian product operator*)
   22.44 +  val pair	: term			(*pairing operator*)
   22.45 +  val split_const  : term		(*splitting operator*)
   22.46 +  val fsplit_const : term		(*splitting operator for formulae*)
   22.47 +  val pair_iff	: thm			(*injectivity of pairing, using <->*)
   22.48 +  val split_eq	: thm			(*equality rule for split*)
   22.49 +  val fsplitI	: thm			(*intro rule for fsplit*)
   22.50 +  val fsplitD	: thm			(*destruct rule for fsplit*)
   22.51 +  val fsplitE	: thm			(*elim rule for fsplit*)
   22.52 +  end;
   22.53 +
   22.54 +signature SU =			(** Description of a disjoint sum **)
   22.55 +  sig
   22.56 +  val sum	: term			(*disjoint sum operator*)
   22.57 +  val inl	: term			(*left injection*)
   22.58 +  val inr	: term			(*right injection*)
   22.59 +  val elim	: term			(*case operator*)
   22.60 +  val case_inl	: thm			(*inl equality rule for case*)
   22.61 +  val case_inr	: thm			(*inr equality rule for case*)
   22.62 +  val inl_iff	: thm			(*injectivity of inl, using <->*)
   22.63 +  val inr_iff	: thm			(*injectivity of inr, using <->*)
   22.64 +  val distinct	: thm			(*distinctness of inl, inr using <->*)
   22.65 +  val distinct'	: thm			(*distinctness of inr, inl using <->*)
   22.66 +  end;
   22.67 +
   22.68 +signature ADD_INDUCTIVE_DEF =
   22.69 +  sig 
   22.70 +  val add_fp_def_i : term list * term list * term list -> theory -> theory
   22.71 +  val add_fp_def   : (string*string) list * string list -> theory -> theory
   22.72 +  val add_constructs_def :
   22.73 +        string list * ((string*typ*mixfix) * 
   22.74 +                       string * term list * term list) list list ->
   22.75 +        theory -> theory
   22.76 +  end;
   22.77 +
   22.78 +
   22.79 +
   22.80 +(*Declares functions to add fixedpoint/constructor defs to a theory*)
   22.81 +functor Add_inductive_def_Fun 
   22.82 +    (structure Fp: FP and Pr : PR and Su : SU) : ADD_INDUCTIVE_DEF =
   22.83 +struct
   22.84 +open Logic Ind_Syntax;
   22.85 +
   22.86 +(*internal version*)
   22.87 +fun add_fp_def_i (rec_tms, domts, intr_tms) thy = 
   22.88 +  let
   22.89 +    val sign = sign_of thy;
   22.90 +
   22.91 +    (*recT and rec_params should agree for all mutually recursive components*)
   22.92 +    val (Const(_,recT),rec_params) = strip_comb (hd rec_tms)
   22.93 +    and rec_hds = map head_of rec_tms;
   22.94 +
   22.95 +    val rec_names = map (#1 o dest_Const) rec_hds;
   22.96 +
   22.97 +    val _ = assert_all Syntax.is_identifier rec_names
   22.98 +       (fn a => "Name of recursive set not an identifier: " ^ a);
   22.99 +
  22.100 +    val _ = assert_all (is_some o lookup_const sign) rec_names
  22.101 +       (fn a => "Recursive set not previously declared as constant: " ^ a);
  22.102 +
  22.103 +    local (*Checking the introduction rules*)
  22.104 +      val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
  22.105 +      fun intr_ok set =
  22.106 +	  case head_of set of Const(a,recT) => a mem rec_names | _ => false;
  22.107 +    in
  22.108 +      val _ =  assert_all intr_ok intr_sets
  22.109 +	 (fn t => "Conclusion of rule does not name a recursive set: " ^ 
  22.110 +		  Sign.string_of_term sign t);
  22.111 +    end;
  22.112 +
  22.113 +    val _ = assert_all is_Free rec_params
  22.114 +	(fn t => "Param in recursion term not a free variable: " ^
  22.115 +		 Sign.string_of_term sign t);
  22.116 +
  22.117 +    (*** Construct the lfp definition ***)
  22.118 +    val mk_variant = variant (foldr add_term_names (intr_tms,[]));
  22.119 +
  22.120 +    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
  22.121 +
  22.122 +    fun dest_tprop (Const("Trueprop",_) $ P) = P
  22.123 +      | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
  22.124 +			      Sign.string_of_term sign Q);
  22.125 +
  22.126 +    (*Makes a disjunct from an introduction rule*)
  22.127 +    fun lfp_part intr = (*quantify over rule's free vars except parameters*)
  22.128 +      let val prems = map dest_tprop (strip_imp_prems intr)
  22.129 +	  val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
  22.130 +	  val exfrees = term_frees intr \\ rec_params
  22.131 +	  val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
  22.132 +      in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
  22.133 +
  22.134 +    val dom_sum = fold_bal (app Su.sum) domts;
  22.135 +
  22.136 +    (*The Part(A,h) terms -- compose injections to make h*)
  22.137 +    fun mk_Part (Bound 0) = Free(X',iT)	(*no mutual rec, no Part needed*)
  22.138 +      | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
  22.139 +
  22.140 +    (*Access to balanced disjoint sums via injections*)
  22.141 +    val parts = 
  22.142 +	map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 
  22.143 +				  (length rec_tms));
  22.144 +
  22.145 +    (*replace each set by the corresponding Part(A,h)*)
  22.146 +    val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
  22.147 +
  22.148 +    val lfp_abs = absfree(X', iT, 
  22.149 +		     mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
  22.150 +
  22.151 +    val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
  22.152 +
  22.153 +    val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
  22.154 +			       "Illegal occurrence of recursion operator")
  22.155 +	     rec_hds;
  22.156 +
  22.157 +    (*** Make the new theory ***)
  22.158 +
  22.159 +    (*A key definition:
  22.160 +      If no mutual recursion then it equals the one recursive set.
  22.161 +      If mutual recursion then it differs from all the recursive sets. *)
  22.162 +    val big_rec_name = space_implode "_" rec_names;
  22.163 +
  22.164 +    (*Big_rec... is the union of the mutually recursive sets*)
  22.165 +    val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
  22.166 +
  22.167 +    (*The individual sets must already be declared*)
  22.168 +    val axpairs = map mk_defpair 
  22.169 +	  ((big_rec_tm, lfp_rhs) ::
  22.170 +	   (case parts of 
  22.171 +	       [_] => [] 			(*no mutual recursion*)
  22.172 +	     | _ => rec_tms ~~		(*define the sets as Parts*)
  22.173 +		    map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
  22.174 +
  22.175 +  in  thy |> add_defns_i axpairs  end
  22.176 +
  22.177 +
  22.178 +(*external, string-based version; needed?*)
  22.179 +fun add_fp_def (rec_doms, sintrs) thy = 
  22.180 +  let val sign = sign_of thy;
  22.181 +      val rec_tms = map (readtm sign iT o fst) rec_doms
  22.182 +      and domts   = map (readtm sign iT o snd) rec_doms
  22.183 +      val intr_tms = map (readtm sign propT) sintrs
  22.184 +  in  add_fp_def_i (rec_tms, domts, intr_tms) thy  end
  22.185 +
  22.186 +
  22.187 +(*Expects the recursive sets to have been defined already.
  22.188 +  con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
  22.189 +fun add_constructs_def (rec_names, con_ty_lists) thy = 
  22.190 +  let
  22.191 +    val _ = writeln"  Defining the constructor functions...";
  22.192 +    val case_name = "f";		(*name for case variables*)
  22.193 +
  22.194 +    (** Define the constructors **)
  22.195 +
  22.196 +    (*The empty tuple is 0*)
  22.197 +    fun mk_tuple [] = Const("0",iT)
  22.198 +      | mk_tuple args = foldr1 (app Pr.pair) args;
  22.199 +
  22.200 +    fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k;
  22.201 +
  22.202 +    val npart = length rec_names;	(*total # of mutually recursive parts*)
  22.203 +
  22.204 +    (*Make constructor definition; kpart is # of this mutually recursive part*)
  22.205 +    fun mk_con_defs (kpart, con_ty_list) = 
  22.206 +      let val ncon = length con_ty_list	   (*number of constructors*)
  22.207 +	  fun mk_def (((id,T,syn), name, args, prems), kcon) =
  22.208 +		(*kcon is index of constructor*)
  22.209 +	      mk_defpair (list_comb (Const(name,T), args),
  22.210 +			  mk_inject npart kpart
  22.211 +			  (mk_inject ncon kcon (mk_tuple args)))
  22.212 +      in  map mk_def (con_ty_list ~~ (1 upto ncon))  end;
  22.213 +
  22.214 +    (** Define the case operator **)
  22.215 +
  22.216 +    (*Combine split terms using case; yields the case operator for one part*)
  22.217 +    fun call_case case_list = 
  22.218 +      let fun call_f (free,args) = 
  22.219 +	      ap_split Pr.split_const free (map (#2 o dest_Free) args)
  22.220 +      in  fold_bal (app Su.elim) (map call_f case_list)  end;
  22.221 +
  22.222 +    (** Generating function variables for the case definition
  22.223 +	Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
  22.224 +
  22.225 +    (*Treatment of a single constructor*)
  22.226 +    fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =
  22.227 +	if Syntax.is_identifier id
  22.228 +	then (opno,   
  22.229 +	      (Free(case_name ^ "_" ^ id, T), args) :: cases)
  22.230 +	else (opno+1, 
  22.231 +	      (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: 
  22.232 +	      cases)
  22.233 +
  22.234 +    (*Treatment of a list of constructors, for one part*)
  22.235 +    fun add_case_list (con_ty_list, (opno,case_lists)) =
  22.236 +	let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
  22.237 +	in (opno', case_list :: case_lists) end;
  22.238 +
  22.239 +    (*Treatment of all parts*)
  22.240 +    val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
  22.241 +
  22.242 +    val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
  22.243 +
  22.244 +    val big_rec_name = space_implode "_" rec_names;
  22.245 +
  22.246 +    val big_case_name = big_rec_name ^ "_case";
  22.247 +
  22.248 +    (*The list of all the function variables*)
  22.249 +    val big_case_args = flat (map (map #1) case_lists);
  22.250 +
  22.251 +    val big_case_tm = 
  22.252 +	list_comb (Const(big_case_name, big_case_typ), big_case_args); 
  22.253 +
  22.254 +    val big_case_def = mk_defpair  
  22.255 +	(big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); 
  22.256 +
  22.257 +    (** Build the new theory **)
  22.258 +
  22.259 +    val const_decs =
  22.260 +	(big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
  22.261 +
  22.262 +    val axpairs =
  22.263 +	big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))
  22.264 +
  22.265 +    in  thy |> add_consts_i const_decs |> add_defns_i axpairs  end;
  22.266 +end;
  22.267 +
  22.268 +
  22.269 +
  22.270 +
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/ZF/add_ind_def.thy	Fri Aug 12 12:51:34 1994 +0200
    23.3 @@ -0,0 +1,3 @@
    23.4 +(*Dummy theory to document dependencies *)
    23.5 +
    23.6 +add_ind_def = Fixedpt + "ind_syntax"
    24.1 --- a/src/ZF/constructor.ML	Fri Aug 12 12:28:46 1994 +0200
    24.2 +++ b/src/ZF/constructor.ML	Fri Aug 12 12:51:34 1994 +0200
    24.3 @@ -3,39 +3,21 @@
    24.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    24.5      Copyright   1993  University of Cambridge
    24.6  
    24.7 -Constructor function module -- for Datatype Definitions
    24.8 -
    24.9 -Defines constructors and a case-style eliminator (no primitive recursion)
   24.10 -
   24.11 -Features:
   24.12 -* least or greatest fixedpoints
   24.13 -* user-specified product and sum constructions
   24.14 -* mutually recursive datatypes
   24.15 -* recursion over arbitrary monotone operators
   24.16 -* flexible: can derive any reasonable set of introduction rules
   24.17 -* automatically constructs a case analysis operator (but no recursion op)
   24.18 -* efficient treatment of large declarations (e.g. 60 constructors)
   24.19 +Constructor function module -- for (Co)Datatype Definitions
   24.20  *)
   24.21  
   24.22 -(** STILL NEEDS: some treatment of recursion **)
   24.23 -
   24.24 -signature CONSTRUCTOR =
   24.25 +signature CONSTRUCTOR_ARG =
   24.26    sig
   24.27 -  val thy        : theory		(*parent theory*)
   24.28 -  val thy_name   : string               (*name of generated theory*)
   24.29 -  val rec_specs  : (string * string * (string list * string * mixfix)list) list
   24.30 -                      (*recursion ops, types, domains, constructors*)
   24.31 -  val rec_styp	 : string		(*common type of all recursion ops*)
   24.32 -  val sintrs     : string list		(*desired introduction rules*)
   24.33 -  val monos      : thm list		(*monotonicity of each M operator*)
   24.34 -  val type_intrs : thm list		(*type-checking intro rules*)
   24.35 -  val type_elims : thm list		(*type-checking elim rules*)
   24.36 +  val thy    	   : theory		(*parent containing constructor defs*)
   24.37 +  val big_rec_name : string		(*name of mutually recursive set*)
   24.38 +  val con_ty_lists : ((string*typ*mixfix) * 
   24.39 +		      string * term list * term list) list list
   24.40 +					(*description of constructors*)
   24.41    end;
   24.42  
   24.43  signature CONSTRUCTOR_RESULT =
   24.44    sig
   24.45 -  val con_thy	 : theory		(*theory defining the constructors*)
   24.46 -  val con_defs	 : thm list		(*definitions made in con_thy*)
   24.47 +  val con_defs	 : thm list		(*definitions made in thy*)
   24.48    val case_eqns  : thm list		(*equations for case operator*)
   24.49    val free_iffs  : thm list		(*freeness rewrite rules*)
   24.50    val free_SEs   : thm list		(*freeness destruct rules*)
   24.51 @@ -43,140 +25,35 @@
   24.52    end;
   24.53  
   24.54  
   24.55 -functor Constructor_Fun (structure Const: CONSTRUCTOR and
   24.56 +(*Proves theorems relating to constructors*)
   24.57 +functor Constructor_Fun (structure Const: CONSTRUCTOR_ARG and
   24.58                        Pr : PR and Su : SU) : CONSTRUCTOR_RESULT =
   24.59  struct
   24.60 -open Logic Const;
   24.61 -
   24.62 -val dummy = writeln"Defining the constructor functions...";
   24.63 -
   24.64 -val case_name = "f";		(*name for case variables*)
   24.65 -
   24.66 -(** Extract basic information from arguments **)
   24.67 -
   24.68 -val sign = sign_of thy;
   24.69 -val rdty = typ_of o read_ctyp sign;
   24.70 -
   24.71 -val rec_names = map #1 rec_specs;
   24.72 -
   24.73 -val dummy = assert_all Syntax.is_identifier rec_names
   24.74 -   (fn a => "Name of recursive set not an identifier: " ^ a);
   24.75 -
   24.76 -(*Expands multiple constant declarations*)
   24.77 -fun flatten_consts ((names, typ, mfix) :: cs) =
   24.78 -      let fun mk_const name = (name, typ, mfix)
   24.79 -      in (map mk_const names) @ (flatten_consts cs) end
   24.80 -  | flatten_consts [] = [];
   24.81 -
   24.82 -(*Parse type string of constructor*)
   24.83 -fun read_typ (names, st, mfix) = (names, rdty st, mfix);
   24.84 -
   24.85 -(*Constructors with types and arguments*)
   24.86 -fun mk_con_ty_list cons_pairs = 
   24.87 -  let fun mk_con_ty (id, T, syn) =
   24.88 -        let val args = mk_frees "xa" (binder_types T);
   24.89 -            val name = const_name id syn;
   24.90 -                            (* because of mixfix annotations the internal name 
   24.91 -                               can be different from 'id' *)
   24.92 -	in (name, T, args) end;
   24.93 -
   24.94 -      fun pairtypes c = flatten_consts [read_typ c];
   24.95 -  in map mk_con_ty (flat (map pairtypes cons_pairs))  end;
   24.96 -
   24.97 -val con_ty_lists = map (mk_con_ty_list o #3) rec_specs;
   24.98 -
   24.99 -(** Define the constructors **)
  24.100 -
  24.101 -(*We identify 0 (the empty set) with the empty tuple*)
  24.102 -fun mk_tuple [] = Const("0",iT)
  24.103 -  | mk_tuple args = foldr1 (app Pr.pair) args;
  24.104 +open Logic Const Ind_Syntax;
  24.105  
  24.106 -fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k;
  24.107 -
  24.108 -val npart = length rec_names;		(*number of mutually recursive parts*)
  24.109 -
  24.110 -(*Make constructor definition*)
  24.111 -fun mk_con_defs (kpart, con_ty_list) = 
  24.112 -  let val ncon = length con_ty_list	   (*number of constructors*)
  24.113 -      fun mk_def ((a,T,args), kcon) = (*kcon = index of this constructor*)
  24.114 -	  mk_defpair sign 
  24.115 -	     (list_comb (Const(a,T), args),
  24.116 -	      mk_inject npart kpart (mk_inject ncon kcon (mk_tuple args)))
  24.117 -  in  map mk_def (con_ty_list ~~ (1 upto ncon))  end;
  24.118 -
  24.119 -(** Define the case operator **)
  24.120 -
  24.121 -(*Combine split terms using case; yields the case operator for one part*)
  24.122 -fun call_case case_list = 
  24.123 -  let fun call_f (free,args) = 
  24.124 -          ap_split Pr.split_const free (map (#2 o dest_Free) args)
  24.125 -  in  fold_bal (app Su.elim) (map call_f case_list)  end;
  24.126 -
  24.127 -(** Generating function variables for the case definition
  24.128 -    Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
  24.129 -
  24.130 -(*Treatment of a single constructor*)
  24.131 -fun add_case ((a,T,args), (opno,cases)) =
  24.132 -    if Syntax.is_identifier a
  24.133 -    then (opno,   
  24.134 -	  (Free(case_name ^ "_" ^ a, T), args) :: cases)
  24.135 -    else (opno+1, 
  24.136 -	  (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases);
  24.137 -
  24.138 -(*Treatment of a list of constructors, for one part*)
  24.139 -fun add_case_list (con_ty_list, (opno,case_lists)) =
  24.140 -    let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
  24.141 -    in (opno', case_list :: case_lists) end;
  24.142 -
  24.143 -(*Treatment of all parts*)
  24.144 -val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
  24.145 -
  24.146 -val big_case_typ = flat (map (map #2) con_ty_lists) ---> (iT-->iT);
  24.147 -
  24.148 -val big_rec_name = space_implode "_" rec_names;
  24.149 -
  24.150 +(*1st element is the case definition; others are the constructors*)
  24.151  val big_case_name = big_rec_name ^ "_case";
  24.152  
  24.153 -(*The list of all the function variables*)
  24.154 -val big_case_args = flat (map (map #1) case_lists);
  24.155 -
  24.156 -val big_case_tm = 
  24.157 -    list_comb (Const(big_case_name, big_case_typ), big_case_args); 
  24.158 -
  24.159 -val big_case_def = 
  24.160 -  mk_defpair sign 
  24.161 -    (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); 
  24.162 -
  24.163 -(** Build the new theory **)
  24.164 -
  24.165 -val axpairs =
  24.166 -    big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists));
  24.167 -
  24.168 -val const_decs = flatten_consts
  24.169 -		   (([big_case_name], big_case_typ, NoSyn) ::
  24.170 -		    (big_rec_name ins rec_names, rdty rec_styp, NoSyn) ::
  24.171 -		    map read_typ (flat (map #3 rec_specs)));
  24.172 -
  24.173 -val con_thy = thy
  24.174 -              |> add_consts_i const_decs
  24.175 -              |> add_axioms_i axpairs
  24.176 -              |> add_thyname (big_rec_name ^ "_Constructors");
  24.177 -
  24.178 -(*1st element is the case definition; others are the constructors*)
  24.179 -val con_defs = map (get_axiom con_thy o #1) axpairs;
  24.180 +val con_defs = get_def thy big_case_name :: 
  24.181 +               map (get_def thy o #2) (flat con_ty_lists);
  24.182  
  24.183  (** Prove the case theorem **)
  24.184  
  24.185 +(*Get the case term from its definition*)
  24.186 +val Const("==",_) $ big_case_tm $ _ =
  24.187 +    hd con_defs |> rep_thm |> #prop |> unvarify;
  24.188 +
  24.189 +val (_, big_case_args) = strip_comb big_case_tm;
  24.190 +
  24.191  (*Each equation has the form 
  24.192    rec_case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
  24.193 -fun mk_case_equation ((a,T,args), case_free) = 
  24.194 -  mk_tprop 
  24.195 -   (eq_const $ (big_case_tm $ (list_comb (Const(a,T), args)))
  24.196 -	     $ (list_comb (case_free, args)));
  24.197 +fun mk_case_equation (((id,T,syn), name, args, prems), case_free) = 
  24.198 +    mk_tprop (eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
  24.199 +		         $ (list_comb (case_free, args))) ;
  24.200  
  24.201  val case_trans = hd con_defs RS def_trans;
  24.202  
  24.203 -(*proves a single case equation*)
  24.204 +(*Proves a single case equation.  Could use simp_tac, but it's slower!*)
  24.205  fun case_tacsf con_def _ = 
  24.206    [rewtac con_def,
  24.207     rtac case_trans 1,
  24.208 @@ -185,7 +62,7 @@
  24.209  			Su.case_inr RS trans] 1)];
  24.210  
  24.211  fun prove_case_equation (arg,con_def) =
  24.212 -    prove_term (sign_of con_thy) [] 
  24.213 +    prove_term (sign_of thy) [] 
  24.214          (mk_case_equation arg, case_tacsf con_def);
  24.215  
  24.216  val free_iffs = 
  24.217 @@ -199,7 +76,7 @@
  24.218  (*Typical theorems have the form ~con1=con2, con1=con2==>False,
  24.219    con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
  24.220  fun mk_free s =
  24.221 -    prove_goalw con_thy con_defs s
  24.222 +    prove_goalw thy con_defs s
  24.223        (fn prems => [cut_facts_tac prems 1, fast_tac free_cs 1]);
  24.224  
  24.225  val case_eqns = map prove_case_equation 
    25.1 --- a/src/ZF/ind_syntax.ML	Fri Aug 12 12:28:46 1994 +0200
    25.2 +++ b/src/ZF/ind_syntax.ML	Fri Aug 12 12:51:34 1994 +0200
    25.3 @@ -6,9 +6,13 @@
    25.4  Abstract Syntax functions for Inductive Definitions
    25.5  *)
    25.6  
    25.7 -
    25.8 -(*Make a definition, lhs==rhs, checking that vars on lhs contain *)
    25.9 -fun mk_defpair sign (lhs, rhs) = 
   25.10 +(*The structure protects these items from redeclaration (somewhat!).  The 
   25.11 +  datatype definitions in theory files refer to these items by name!
   25.12 +*)
   25.13 +structure Ind_Syntax =
   25.14 +struct
   25.15 +(*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*)
   25.16 +fun mk_defpair (lhs, rhs) = 
   25.17    let val Const(name, _) = head_of lhs
   25.18        val dummy = assert (term_vars rhs subset term_vars lhs
   25.19  		          andalso
   25.20 @@ -20,6 +24,8 @@
   25.21  	          ("Extra variables on RHS in definition of " ^ name)
   25.22    in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
   25.23  
   25.24 +fun get_def thy s = get_axiom thy (s^"_def");
   25.25 +
   25.26  fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
   25.27  
   25.28  (*export to Pure/library?  *)
   25.29 @@ -64,7 +70,6 @@
   25.30  fun mk_all_imp (A,P) = 
   25.31      all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
   25.32  
   25.33 -
   25.34  val Part_const = Const("Part", [iT,iT-->iT]--->iT);
   25.35  
   25.36  val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
   25.37 @@ -85,14 +90,62 @@
   25.38  (*Read an assumption in the given theory*)
   25.39  fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
   25.40  
   25.41 +fun readtm sign T a = 
   25.42 +    read_cterm sign (a,T) |> term_of
   25.43 +    handle ERROR => error ("The error above occurred for " ^ a);
   25.44 +
   25.45 +(*Skipping initial blanks, find the first identifier*)
   25.46 +fun scan_to_id s = 
   25.47 +    s |> explode |> take_prefix is_blank |> #2 |> Lexicon.scan_id |> #1
   25.48 +    handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
   25.49 +
   25.50 +fun is_backslash c = c = "\\";
   25.51 +
   25.52 +(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
   25.53 +  Does not handle the \ddd form;  no error checking*)
   25.54 +fun escape [] = []
   25.55 +  | escape cs = (case take_prefix (not o is_backslash) cs of
   25.56 +	 (front, []) => front
   25.57 +       | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
   25.58 +       | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
   25.59 +       | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
   25.60 +       | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
   25.61 +       | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
   25.62 +       | (front, b::c::rest) => 
   25.63 +	   if is_blank c   (*remove any further blanks and the following \ *)
   25.64 +	   then front @ escape (tl (snd (take_prefix is_blank rest)))
   25.65 +	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
   25.66 +
   25.67 +(*Remove the first and last charaters -- presumed to be quotes*)
   25.68 +val trim = implode o escape o rev o tl o rev o tl o explode;
   25.69 +
   25.70 +(*simple error-checking in the premises of an inductive definition*)
   25.71 +fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
   25.72 +	error"Premises may not be conjuctive"
   25.73 +  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
   25.74 +	deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol"
   25.75 +  | chk_prem rec_hd t = 
   25.76 +	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
   25.77 +
   25.78 +
   25.79 +(*Inverse of varifyT.  Move to Pure/type.ML?*)
   25.80 +fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
   25.81 +  | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
   25.82 +  | unvarifyT T = T;
   25.83 +
   25.84 +(*Inverse of varify.  Move to Pure/logic.ML?*)
   25.85 +fun unvarify (Const(a,T))    = Const(a, unvarifyT T)
   25.86 +  | unvarify (Var((a,0), T)) = Free(a, unvarifyT T)
   25.87 +  | unvarify (Var(ixn,T))    = Var(ixn, unvarifyT T)	(*non-zero index!*)
   25.88 +  | unvarify (Abs (a,T,body)) = Abs (a, unvarifyT T, unvarify body)
   25.89 +  | unvarify (f$t) = unvarify f $ unvarify t
   25.90 +  | unvarify t = t;
   25.91 +
   25.92 +
   25.93  (*Make distinct individual variables a1, a2, a3, ..., an. *)
   25.94  fun mk_frees a [] = []
   25.95    | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
   25.96  
   25.97 -(*Used by intr-elim.ML and in individual datatype definitions*)
   25.98 -val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
   25.99 -		   ex_mono, Collect_mono, Part_mono, in_mono];
  25.100 -
  25.101  (*Return the conclusion of a rule, of the form t:X*)
  25.102  fun rule_concl rl = 
  25.103      let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
  25.104 @@ -118,27 +171,55 @@
  25.105  fun gen_make_elim elim_rls rl = 
  25.106        standard (tryres (rl, elim_rls @ [revcut_rl]));
  25.107  
  25.108 -(** For constructor.ML **)
  25.109 +(** For datatype definitions **)
  25.110 +
  25.111 +fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
  25.112 +  | dest_mem _ = error "Constructor specifications must have the form x:A";
  25.113 +
  25.114 +(*read a constructor specification*)
  25.115 +fun read_construct sign (id, sprems, syn) =
  25.116 +    let val prems = map (readtm sign oT) sprems
  25.117 +	val args = map (#1 o dest_mem) prems
  25.118 +	val T = (map (#2 o dest_Free) args) ---> iT
  25.119 +		handle TERM _ => error 
  25.120 +		    "Bad variable in constructor specification"
  25.121 +        val name = const_name id syn  (*handle infix constructors*)
  25.122 +    in ((id,T,syn), name, args, prems) end;
  25.123 +
  25.124 +val read_constructs = map o map o read_construct;
  25.125  
  25.126 -(*Avoids duplicate definitions by removing constants already declared mixfix*)
  25.127 -fun remove_mixfixes None decs = decs
  25.128 -  | remove_mixfixes (Some sext) decs =
  25.129 -      let val mixtab = Symtab.st_of_declist(Syntax.constants sext, Symtab.null)
  25.130 -	  fun is_mix c = case Symtab.lookup(mixtab,c) of
  25.131 -			     None=>false | Some _ => true
  25.132 -      in  map (fn (cs,styp)=> (filter_out is_mix cs, styp)) decs
  25.133 -      end;
  25.134 +(*convert constructor specifications into introduction rules*)
  25.135 +fun mk_intr_tms (rec_tm, constructs) =
  25.136 +  let fun mk_intr ((id,T,syn), name, args, prems) =
  25.137 +	  Logic.list_implies
  25.138 +	      (map mk_tprop prems,
  25.139 +	       mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
  25.140 +  in  map mk_intr constructs  end;
  25.141 +
  25.142 +val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
  25.143  
  25.144 -fun ext_constants None        = []
  25.145 -  | ext_constants (Some sext) = Syntax.constants sext;
  25.146 +val Un		= Const("op Un", [iT,iT]--->iT)
  25.147 +and empty	= Const("0", iT)
  25.148 +and univ	= Const("univ", iT-->iT)
  25.149 +and quniv	= Const("quniv", iT-->iT);
  25.150  
  25.151 +(*Make a datatype's domain: form the union of its set parameters*)
  25.152 +fun union_params rec_tm =
  25.153 +  let val (_,args) = strip_comb rec_tm
  25.154 +  in  case (filter (fn arg => type_of arg = iT) args) of
  25.155 +         []    => empty
  25.156 +       | iargs => fold_bal (app Un) iargs
  25.157 +  end;
  25.158 +
  25.159 +fun data_domain rec_tms =
  25.160 +  replicate (length rec_tms) (univ $ union_params (hd rec_tms));
  25.161 +
  25.162 +fun Codata_domain rec_tms =
  25.163 +  replicate (length rec_tms) (quniv $ union_params (hd rec_tms));
  25.164  
  25.165  (*Could go to FOL, but it's hardly general*)
  25.166 -val [def] = goal IFOL.thy "a==b ==> a=c <-> c=b";
  25.167 -by (rewtac def);
  25.168 -by (rtac iffI 1);
  25.169 -by (REPEAT (etac sym 1));
  25.170 -val def_swap_iff = result();
  25.171 +val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
  25.172 + (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
  25.173  
  25.174  val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
  25.175    (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
  25.176 @@ -147,3 +228,5 @@
  25.177  val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
  25.178       (fn _ => [assume_tac 1]);
  25.179  
  25.180 +end;
  25.181 +
    26.1 --- a/src/ZF/indrule.ML	Fri Aug 12 12:28:46 1994 +0200
    26.2 +++ b/src/ZF/indrule.ML	Fri Aug 12 12:51:34 1994 +0200
    26.3 @@ -1,7 +1,7 @@
    26.4  (*  Title: 	ZF/indrule.ML
    26.5      ID:         $Id$
    26.6      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    26.7 -    Copyright   1993  University of Cambridge
    26.8 +    Copyright   1994  University of Cambridge
    26.9  
   26.10  Induction rule module -- for Inductive/Coinductive Definitions
   26.11  
   26.12 @@ -15,19 +15,25 @@
   26.13    end;
   26.14  
   26.15  
   26.16 -functor Indrule_Fun (structure Ind: INDUCTIVE and 
   26.17 -		     Pr: PR and Intr_elim: INTR_ELIM) : INDRULE  =
   26.18 +functor Indrule_Fun
   26.19 +    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end
   26.20 +     and Pr: PR and Intr_elim: INTR_ELIM) : INDRULE  =
   26.21  struct
   26.22 -open Logic Ind Intr_elim;
   26.23 +open Logic Ind_Syntax Inductive Intr_elim;
   26.24 +
   26.25 +val sign = sign_of thy;
   26.26  
   26.27 -val dummy = writeln "Proving the induction rules...";
   26.28 +val (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
   26.29 +
   26.30 +val big_rec_name = space_implode "_" rec_names;
   26.31 +val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
   26.32 +
   26.33 +val _ = writeln "  Proving the induction rules...";
   26.34  
   26.35  (*** Prove the main induction rule ***)
   26.36  
   26.37  val pred_name = "P";		(*name for predicate variables*)
   26.38  
   26.39 -val prove = prove_term (sign_of Intr_elim.thy);
   26.40 -
   26.41  val big_rec_def::part_rec_defs = Intr_elim.defs;
   26.42  
   26.43  (*Used to make induction rules;
   26.44 @@ -63,7 +69,7 @@
   26.45  val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;
   26.46  
   26.47  val quant_induct = 
   26.48 -    prove part_rec_defs 
   26.49 +    prove_term sign part_rec_defs 
   26.50        (list_implies (ind_prems, mk_tprop (mk_all_imp(big_rec_tm,pred))),
   26.51         fn prems =>
   26.52         [rtac (impI RS allI) 1,
   26.53 @@ -112,7 +118,7 @@
   26.54  and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);
   26.55  
   26.56  val lemma = (*makes the link between the two induction rules*)
   26.57 -    prove part_rec_defs 
   26.58 +    prove_term sign part_rec_defs 
   26.59  	  (mk_implies (induct_concl,mutual_induct_concl), 
   26.60  	   fn prems =>
   26.61  	   [cut_facts_tac prems 1,
   26.62 @@ -139,7 +145,7 @@
   26.63  	i  THEN mutual_ind_tac prems (i-1);
   26.64  
   26.65  val mutual_induct_fsplit = 
   26.66 -    prove []
   26.67 +    prove_term sign []
   26.68  	  (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
   26.69  			 mutual_induct_concl),
   26.70  	   fn prems =>
    27.1 --- a/src/ZF/inductive.ML	Fri Aug 12 12:28:46 1994 +0200
    27.2 +++ b/src/ZF/inductive.ML	Fri Aug 12 12:51:34 1994 +0200
    27.3 @@ -3,15 +3,17 @@
    27.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    27.5      Copyright   1993  University of Cambridge
    27.6  
    27.7 -Inductive Definitions for Zermelo-Fraenkel Set Theory
    27.8 +(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory
    27.9  
   27.10 -Uses least fixedpoints with standard products and sums
   27.11 +Inductive definitions use least fixedpoints with standard products and sums
   27.12 +Coinductive definitions use greatest fixedpoints with Quine products and sums
   27.13  
   27.14  Sums are used only for mutual recursion;
   27.15  Products are used only to derive "streamlined" induction rules for relations
   27.16  *)
   27.17  
   27.18 -
   27.19 +local open Ind_Syntax
   27.20 +in
   27.21  structure Lfp =
   27.22    struct
   27.23    val oper	= Const("lfp",      [iT,iT-->iT]--->iT)
   27.24 @@ -48,16 +50,179 @@
   27.25    val distinct	= Inl_Inr_iff
   27.26    val distinct' = Inr_Inl_iff
   27.27    end;
   27.28 +end;
   27.29  
   27.30 -functor Inductive_Fun (Ind: INDUCTIVE) : sig include INTR_ELIM INDRULE end =
   27.31 +functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
   27.32 +  : sig include INTR_ELIM INDRULE end =
   27.33  struct
   27.34  structure Intr_elim = 
   27.35 -    Intr_elim_Fun(structure Ind=Ind and Fp=Lfp and 
   27.36 +    Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
   27.37  		  Pr=Standard_Prod and Su=Standard_Sum);
   27.38  
   27.39 -structure Indrule = Indrule_Fun (structure Ind=Ind and 
   27.40 +structure Indrule = Indrule_Fun (structure Inductive=Inductive and 
   27.41  		                 Pr=Standard_Prod and Intr_elim=Intr_elim);
   27.42  
   27.43  open Intr_elim Indrule
   27.44  end;
   27.45  
   27.46 +
   27.47 +structure Ind = Add_inductive_def_Fun
   27.48 +    (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
   27.49 +
   27.50 +
   27.51 +signature INDUCTIVE_STRING =
   27.52 +  sig
   27.53 +  val thy_name   : string 		(*name of the new theory*)
   27.54 +  val rec_doms   : (string*string) list	(*recursion terms and their domains*)
   27.55 +  val sintrs     : string list		(*desired introduction rules*)
   27.56 +  end;
   27.57 +
   27.58 +
   27.59 +(*For upwards compatibility: can be called directly from ML*)
   27.60 +functor Inductive_Fun
   27.61 + (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
   27.62 +   : sig include INTR_ELIM INDRULE end =
   27.63 +Ind_section_Fun
   27.64 +   (open Inductive Ind_Syntax
   27.65 +    val sign = sign_of thy;
   27.66 +    val rec_tms = map (readtm sign iT o #1) rec_doms
   27.67 +    and domts   = map (readtm sign iT o #2) rec_doms
   27.68 +    and intr_tms = map (readtm sign propT) sintrs;
   27.69 +    val thy = thy |> Ind.add_fp_def_i(rec_tms, domts, intr_tms) 
   27.70 +                  |> add_thyname thy_name);
   27.71 +
   27.72 +
   27.73 +
   27.74 +local open Ind_Syntax
   27.75 +in
   27.76 +structure Gfp =
   27.77 +  struct
   27.78 +  val oper	= Const("gfp",      [iT,iT-->iT]--->iT)
   27.79 +  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
   27.80 +  val bnd_monoI	= bnd_monoI
   27.81 +  val subs	= def_gfp_subset
   27.82 +  val Tarski	= def_gfp_Tarski
   27.83 +  val induct	= def_Collect_coinduct
   27.84 +  end;
   27.85 +
   27.86 +structure Quine_Prod =
   27.87 +  struct
   27.88 +  val sigma	= Const("QSigma", [iT, iT-->iT]--->iT)
   27.89 +  val pair	= Const("QPair", [iT,iT]--->iT)
   27.90 +  val split_const	= Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
   27.91 +  val fsplit_const	= Const("qfsplit", [[iT,iT]--->oT, iT]--->oT)
   27.92 +  val pair_iff	= QPair_iff
   27.93 +  val split_eq	= qsplit
   27.94 +  val fsplitI	= qfsplitI
   27.95 +  val fsplitD	= qfsplitD
   27.96 +  val fsplitE	= qfsplitE
   27.97 +  end;
   27.98 +
   27.99 +structure Quine_Sum =
  27.100 +  struct
  27.101 +  val sum	= Const("op <+>", [iT,iT]--->iT)
  27.102 +  val inl	= Const("QInl", iT-->iT)
  27.103 +  val inr	= Const("QInr", iT-->iT)
  27.104 +  val elim	= Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
  27.105 +  val case_inl	= qcase_QInl
  27.106 +  val case_inr	= qcase_QInr
  27.107 +  val inl_iff	= QInl_iff
  27.108 +  val inr_iff	= QInr_iff
  27.109 +  val distinct	= QInl_QInr_iff
  27.110 +  val distinct' = QInr_QInl_iff
  27.111 +  end;
  27.112 +end;
  27.113 +
  27.114 +
  27.115 +signature COINDRULE =
  27.116 +  sig
  27.117 +  val coinduct : thm
  27.118 +  end;
  27.119 +
  27.120 +
  27.121 +functor CoInd_section_Fun
  27.122 + (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
  27.123 +    : sig include INTR_ELIM COINDRULE end =
  27.124 +struct
  27.125 +structure Intr_elim = 
  27.126 +    Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
  27.127 +		  Pr=Quine_Prod and Su=Quine_Sum);
  27.128 +
  27.129 +open Intr_elim 
  27.130 +val coinduct = raw_induct
  27.131 +end;
  27.132 +
  27.133 +
  27.134 +structure CoInd = 
  27.135 +    Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
  27.136 +
  27.137 +
  27.138 +(*For upwards compatibility: can be called directly from ML*)
  27.139 +functor CoInductive_Fun
  27.140 + (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
  27.141 +   : sig include INTR_ELIM COINDRULE end =
  27.142 +CoInd_section_Fun
  27.143 +   (open Inductive Ind_Syntax
  27.144 +    val sign = sign_of thy;
  27.145 +    val rec_tms = map (readtm sign iT o #1) rec_doms
  27.146 +    and domts   = map (readtm sign iT o #2) rec_doms
  27.147 +    and intr_tms = map (readtm sign propT) sintrs;
  27.148 +    val thy = thy |> CoInd.add_fp_def_i(rec_tms, domts, intr_tms) 
  27.149 +                  |> add_thyname thy_name);
  27.150 +
  27.151 +
  27.152 +
  27.153 +(*For installing the theory section.   co is either "" or "Co"*)
  27.154 +fun inductive_decl co =
  27.155 +  let open ThyParse Ind_Syntax
  27.156 +      fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
  27.157 +	  if Syntax.is_identifier s then "op " ^ s  else "_"
  27.158 +      fun mk_params (((((domains: (string*string) list, ipairs), 
  27.159 +			monos), con_defs), type_intrs), type_elims) =
  27.160 +        let val big_rec_name = space_implode "_" 
  27.161 +		             (map (scan_to_id o trim o #1) domains)
  27.162 +	    and srec_tms = mk_list (map #1 domains)
  27.163 +            and sdoms    = mk_list (map #2 domains)
  27.164 +	    and sintrs   = mk_big_list (map snd ipairs)
  27.165 +            val stri_name = big_rec_name ^ "_Intrnl"
  27.166 +        in
  27.167 +	   (";\n\n\
  27.168 +            \structure " ^ stri_name ^ " =\n\
  27.169 +            \ let open Ind_Syntax in\n\
  27.170 +            \  struct\n\
  27.171 +            \  val rec_tms\t= map (readtm (sign_of thy) iT) "
  27.172 +	                     ^ srec_tms ^ "\n\
  27.173 +            \  and domts\t= map (readtm (sign_of thy) iT) "
  27.174 +	                     ^ sdoms ^ "\n\
  27.175 +            \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
  27.176 +	                     ^ sintrs ^ "\n\
  27.177 +            \  end\n\
  27.178 +            \ end;\n\n\
  27.179 +            \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
  27.180 +	       stri_name ^ ".rec_tms, " ^
  27.181 +               stri_name ^ ".domts, " ^
  27.182 +               stri_name ^ ".intr_tms)"
  27.183 +           ,
  27.184 +	    "structure " ^ big_rec_name ^ " =\n\
  27.185 +            \  struct\n\
  27.186 +            \  val _ = writeln \"" ^ co ^ 
  27.187 +	               "Inductive definition " ^ big_rec_name ^ "\"\n\
  27.188 +            \  structure Result = " ^ co ^ "Ind_section_Fun\n\
  27.189 +            \  (open " ^ stri_name ^ "\n\
  27.190 +            \   val thy\t\t= thy\n\
  27.191 +            \   val monos\t\t= " ^ monos ^ "\n\
  27.192 +            \   val con_defs\t\t= " ^ con_defs ^ "\n\
  27.193 +            \   val type_intrs\t= " ^ type_intrs ^ "\n\
  27.194 +            \   val type_elims\t= " ^ type_elims ^ ");\n\n\
  27.195 +            \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
  27.196 +            \  open Result\n\
  27.197 +            \  end\n"
  27.198 +	   )
  27.199 +	end
  27.200 +      val domains = "domains" $$-- repeat1 (string --$$ "<=" -- !! string)
  27.201 +      val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
  27.202 +      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
  27.203 +  in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
  27.204 +             -- optstring "type_intrs" -- optstring "type_elims"
  27.205 +     >> mk_params
  27.206 +  end;
    28.1 --- a/src/ZF/intr_elim.ML	Fri Aug 12 12:28:46 1994 +0200
    28.2 +++ b/src/ZF/intr_elim.ML	Fri Aug 12 12:51:34 1994 +0200
    28.3 @@ -1,83 +1,31 @@
    28.4  (*  Title: 	ZF/intr-elim.ML
    28.5      ID:         $Id$
    28.6      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    28.7 -    Copyright   1993  University of Cambridge
    28.8 +    Copyright   1994  University of Cambridge
    28.9  
   28.10  Introduction/elimination rule module -- for Inductive/Coinductive Definitions
   28.11 -
   28.12 -Features:
   28.13 -* least or greatest fixedpoints
   28.14 -* user-specified product and sum constructions
   28.15 -* mutually recursive definitions
   28.16 -* definitions involving arbitrary monotone operators
   28.17 -* automatically proves introduction and elimination rules
   28.18 -
   28.19 -The recursive sets must *already* be declared as constants in parent theory!
   28.20 -
   28.21 -  Introduction rules have the form
   28.22 -  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
   28.23 -  where M is some monotone operator (usually the identity)
   28.24 -  P(x) is any (non-conjunctive) side condition on the free variables
   28.25 -  ti, t are any terms
   28.26 -  Sj, Sk are two of the sets being defined in mutual recursion
   28.27 -
   28.28 -Sums are used only for mutual recursion;
   28.29 -Products are used only to derive "streamlined" induction rules for relations
   28.30  *)
   28.31  
   28.32 -signature FP =		(** Description of a fixed point operator **)
   28.33 -  sig
   28.34 -  val oper	: term			(*fixed point operator*)
   28.35 -  val bnd_mono	: term			(*monotonicity predicate*)
   28.36 -  val bnd_monoI	: thm			(*intro rule for bnd_mono*)
   28.37 -  val subs	: thm			(*subset theorem for fp*)
   28.38 -  val Tarski	: thm			(*Tarski's fixed point theorem*)
   28.39 -  val induct	: thm			(*induction/coinduction rule*)
   28.40 -  end;
   28.41 -
   28.42 -signature PR =			(** Description of a Cartesian product **)
   28.43 +signature INDUCTIVE_ARG =	(** Description of a (co)inductive def **)
   28.44    sig
   28.45 -  val sigma	: term			(*Cartesian product operator*)
   28.46 -  val pair	: term			(*pairing operator*)
   28.47 -  val split_const  : term		(*splitting operator*)
   28.48 -  val fsplit_const : term		(*splitting operator for formulae*)
   28.49 -  val pair_iff	: thm			(*injectivity of pairing, using <->*)
   28.50 -  val split_eq	: thm			(*equality rule for split*)
   28.51 -  val fsplitI	: thm			(*intro rule for fsplit*)
   28.52 -  val fsplitD	: thm			(*destruct rule for fsplit*)
   28.53 -  val fsplitE	: thm			(*elim rule for fsplit*)
   28.54 -  end;
   28.55 -
   28.56 -signature SU =			(** Description of a disjoint sum **)
   28.57 -  sig
   28.58 -  val sum	: term			(*disjoint sum operator*)
   28.59 -  val inl	: term			(*left injection*)
   28.60 -  val inr	: term			(*right injection*)
   28.61 -  val elim	: term			(*case operator*)
   28.62 -  val case_inl	: thm			(*inl equality rule for case*)
   28.63 -  val case_inr	: thm			(*inr equality rule for case*)
   28.64 -  val inl_iff	: thm			(*injectivity of inl, using <->*)
   28.65 -  val inr_iff	: thm			(*injectivity of inr, using <->*)
   28.66 -  val distinct	: thm			(*distinctness of inl, inr using <->*)
   28.67 -  val distinct'	: thm			(*distinctness of inr, inl using <->*)
   28.68 -  end;
   28.69 -
   28.70 -signature INDUCTIVE =		(** Description of a (co)inductive defn **)
   28.71 -  sig
   28.72 -  val thy        : theory		(*parent theory*)
   28.73 -  val thy_name   : string               (*name of generated theory*)
   28.74 -  val rec_doms   : (string*string) list	(*recursion ops and their domains*)
   28.75 -  val sintrs     : string list		(*desired introduction rules*)
   28.76 +  val thy        : theory               (*new theory with inductive defs*)
   28.77    val monos      : thm list		(*monotonicity of each M operator*)
   28.78    val con_defs   : thm list		(*definitions of the constructors*)
   28.79    val type_intrs : thm list		(*type-checking intro rules*)
   28.80    val type_elims : thm list		(*type-checking elim rules*)
   28.81    end;
   28.82  
   28.83 +(*internal items*)
   28.84 +signature INDUCTIVE_I =
   28.85 +  sig
   28.86 +  val rec_tms    : term list		(*the recursive sets*)
   28.87 +  val domts      : term list		(*their domains*)
   28.88 +  val intr_tms   : term list		(*terms for the introduction rules*)
   28.89 +  end;
   28.90 +
   28.91  signature INTR_ELIM =
   28.92    sig
   28.93 -  val thy        : theory		(*new theory*)
   28.94 -  val thy_name   : string               (*name of generated theory*)
   28.95 +  val thy        : theory               (*copy of input theory*)
   28.96    val defs	 : thm list		(*definitions made in thy*)
   28.97    val bnd_mono   : thm			(*monotonicity for the lfp definition*)
   28.98    val unfold     : thm			(*fixed-point equation*)
   28.99 @@ -86,145 +34,36 @@
  28.100    val elim       : thm			(*case analysis theorem*)
  28.101    val raw_induct : thm			(*raw induction rule from Fp.induct*)
  28.102    val mk_cases : thm list -> string -> thm	(*generates case theorems*)
  28.103 -  (*internal items...*)
  28.104 -  val big_rec_tm : term			(*the lhs of the fixedpoint defn*)
  28.105 -  val rec_tms    : term list		(*the mutually recursive sets*)
  28.106 -  val domts      : term list		(*domains of the recursive sets*)
  28.107 -  val intr_tms   : term list		(*terms for the introduction rules*)
  28.108 -  val rec_params : term list		(*parameters of the recursion*)
  28.109 +  val rec_names  : string list		(*names of recursive sets*)
  28.110    val sumprod_free_SEs : thm list       (*destruct rules for Su and Pr*)
  28.111    end;
  28.112  
  28.113 -
  28.114 -functor Intr_elim_Fun (structure Ind: INDUCTIVE and 
  28.115 -		       Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
  28.116 +(*prove intr/elim rules for a fixedpoint definition*)
  28.117 +functor Intr_elim_Fun
  28.118 +    (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end  
  28.119 +     and Fp: FP and Pr : PR and Su : SU) : INTR_ELIM =
  28.120  struct
  28.121 -open Logic Ind;
  28.122 -
  28.123 -(*** Extract basic information from arguments ***)
  28.124 -
  28.125 -val sign = sign_of Ind.thy;
  28.126 -
  28.127 -fun rd T a = 
  28.128 -    read_cterm sign (a,T)
  28.129 -    handle ERROR => error ("The error above occurred for " ^ a);
  28.130 -
  28.131 -val rec_names = map #1 rec_doms
  28.132 -and domts     = map (term_of o rd iT o #2) rec_doms;
  28.133 -
  28.134 -val dummy = assert_all Syntax.is_identifier rec_names
  28.135 -   (fn a => "Name of recursive set not an identifier: " ^ a);
  28.136 -
  28.137 -val dummy = assert_all (is_some o lookup_const sign) rec_names
  28.138 -   (fn a => "Name of recursive set not declared as constant: " ^ a);
  28.139 -
  28.140 -val intr_tms = map (term_of o rd propT) sintrs;
  28.141 -
  28.142 -local (*Checking the introduction rules*)
  28.143 -  val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
  28.144 -
  28.145 -  fun intr_ok set =
  28.146 -      case head_of set of Const(a,recT) => a mem rec_names | _ => false;
  28.147 -
  28.148 -  val dummy =  assert_all intr_ok intr_sets
  28.149 -     (fn t => "Conclusion of rule does not name a recursive set: " ^ 
  28.150 -	      Sign.string_of_term sign t);
  28.151 -in
  28.152 -val (Const(_,recT),rec_params) = strip_comb (hd intr_sets)
  28.153 -end;
  28.154 -
  28.155 -val rec_hds = map (fn a=> Const(a,recT)) rec_names;
  28.156 -val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
  28.157 -
  28.158 -val dummy = assert_all is_Free rec_params
  28.159 -    (fn t => "Param in recursion term not a free variable: " ^
  28.160 -             Sign.string_of_term sign t);
  28.161 -
  28.162 -(*** Construct the lfp definition ***)
  28.163 -
  28.164 -val mk_variant = variant (foldr add_term_names (intr_tms,[]));
  28.165 +open Logic Inductive Ind_Syntax;
  28.166  
  28.167 -val z' = mk_variant"z"
  28.168 -and X' = mk_variant"X"
  28.169 -and w' = mk_variant"w";
  28.170 -
  28.171 -(*simple error-checking in the premises*)
  28.172 -fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
  28.173 -	error"Premises may not be conjuctive"
  28.174 -  | chk_prem rec_hd (Const("op :",_) $ t $ X) = 
  28.175 -	deny (rec_hd occs t) "Recursion term on left of member symbol"
  28.176 -  | chk_prem rec_hd t = 
  28.177 -	deny (rec_hd occs t) "Recursion term in side formula";
  28.178 -
  28.179 -fun dest_tprop (Const("Trueprop",_) $ P) = P
  28.180 -  | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
  28.181 -			  Sign.string_of_term sign Q);
  28.182 -
  28.183 -(*Makes a disjunct from an introduction rule*)
  28.184 -fun lfp_part intr = (*quantify over rule's free vars except parameters*)
  28.185 -  let val prems = map dest_tprop (strip_imp_prems intr)
  28.186 -      val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
  28.187 -      val exfrees = term_frees intr \\ rec_params
  28.188 -      val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
  28.189 -  in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
  28.190 -
  28.191 -val dom_sum = fold_bal (app Su.sum) domts;
  28.192 -
  28.193 -(*The Part(A,h) terms -- compose injections to make h*)
  28.194 -fun mk_Part (Bound 0) = Free(X',iT)	(*no mutual rec, no Part needed*)
  28.195 -  | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
  28.196 -
  28.197 -(*Access to balanced disjoint sums via injections*)
  28.198 -val parts = 
  28.199 -    map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 
  28.200 -		              (length rec_doms));
  28.201 -
  28.202 -(*replace each set by the corresponding Part(A,h)*)
  28.203 -val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
  28.204 -
  28.205 -val lfp_abs = absfree(X', iT, 
  28.206 -	         mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
  28.207 -
  28.208 -val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
  28.209 -
  28.210 -val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
  28.211 -			   "Illegal occurrence of recursion operator")
  28.212 -	 rec_hds;
  28.213 -
  28.214 -(*** Make the new theory ***)
  28.215 -
  28.216 -(*A key definition:
  28.217 -  If no mutual recursion then it equals the one recursive set.
  28.218 -  If mutual recursion then it differs from all the recursive sets. *)
  28.219 +val rec_names = map (#1 o dest_Const o head_of) rec_tms;
  28.220  val big_rec_name = space_implode "_" rec_names;
  28.221  
  28.222 -(*Big_rec... is the union of the mutually recursive sets*)
  28.223 -val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
  28.224 -
  28.225 -(*The individual sets must already be declared*)
  28.226 -val axpairs = map (mk_defpair sign) 
  28.227 -      ((big_rec_tm, lfp_rhs) ::
  28.228 -       (case parts of 
  28.229 -	   [_] => [] 			(*no mutual recursion*)
  28.230 -	 | _ => rec_tms ~~		(*define the sets as Parts*)
  28.231 -		map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
  28.232 +(*fetch fp definitions from the theory*)
  28.233 +val big_rec_def::part_rec_defs = 
  28.234 +  map (get_def thy)
  28.235 +      (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names);
  28.236  
  28.237 -val thy = 
  28.238 -  Ind.thy
  28.239 -  |> add_axioms_i axpairs
  28.240 -  |> add_thyname thy_name;
  28.241  
  28.242 -val defs = map (get_axiom thy o #1) axpairs;
  28.243 -
  28.244 -val big_rec_def::part_rec_defs = defs;
  28.245 -
  28.246 -val prove = prove_term (sign_of thy);
  28.247 +val sign = sign_of thy;
  28.248  
  28.249  (********)
  28.250 -val dummy = writeln "Proving monotonicity...";
  28.251 +val _ = writeln "  Proving monotonicity...";
  28.252 +
  28.253 +val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
  28.254 +    big_rec_def |> rep_thm |> #prop |> unvarify;
  28.255  
  28.256  val bnd_mono = 
  28.257 -    prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs), 
  28.258 +    prove_term sign [] (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs), 
  28.259         fn _ =>
  28.260         [rtac (Collect_subset RS bnd_monoI) 1,
  28.261  	REPEAT (ares_tac (basic_monos @ monos) 1)]);
  28.262 @@ -234,7 +73,7 @@
  28.263  val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski));
  28.264  
  28.265  (********)
  28.266 -val dummy = writeln "Proving the introduction rules...";
  28.267 +val _ = writeln "  Proving the introduction rules...";
  28.268  
  28.269  (*Mutual recursion: Needs subset rules for the individual sets???*)
  28.270  val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD];
  28.271 @@ -252,22 +91,22 @@
  28.272     rewrite_goals_tac con_defs,
  28.273     (*Now can solve the trivial equation*)
  28.274     REPEAT (rtac refl 2),
  28.275 -   REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
  28.276 -		      ORELSE' hyp_subst_tac
  28.277 -		      ORELSE' dresolve_tac rec_typechecks)),
  28.278 +   REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
  28.279 +		      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
  28.280 +		      ORELSE' hyp_subst_tac)),
  28.281     DEPTH_SOLVE (swap_res_tac (SigmaI::type_intrs) 1)];
  28.282  
  28.283  (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
  28.284  val mk_disj_rls = 
  28.285      let fun f rl = rl RS disjI1
  28.286 -        and g rl = rl RS disjI2
  28.287 +	and g rl = rl RS disjI2
  28.288      in  accesses_bal(f, g, asm_rl)  end;
  28.289  
  28.290 -val intrs = map (prove part_rec_defs) 
  28.291 +val intrs = map (prove_term sign part_rec_defs) 
  28.292  	       (intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));
  28.293  
  28.294  (********)
  28.295 -val dummy = writeln "Proving the elimination rule...";
  28.296 +val _ = writeln "  Proving the elimination rule...";
  28.297  
  28.298  (*Includes rules for succ and Pair since they are common constructions*)
  28.299  val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
  28.300 @@ -276,13 +115,13 @@
  28.301  
  28.302  val sumprod_free_SEs = 
  28.303      map (gen_make_elim [conjE,FalseE])
  28.304 -        ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
  28.305 +	([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
  28.306  	 RL [iffD1]);
  28.307  
  28.308  (*Breaks down logical connectives in the monotonic function*)
  28.309  val basic_elim_tac =
  28.310      REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs)
  28.311 -              ORELSE' bound_hyp_subst_tac))
  28.312 +	      ORELSE' bound_hyp_subst_tac))
  28.313      THEN prune_params_tac;
  28.314  
  28.315  val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
  28.316 @@ -301,5 +140,5 @@
  28.317  val defs = big_rec_def::part_rec_defs;
  28.318  
  28.319  val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
  28.320 +end;
  28.321  
  28.322 -end;
    29.1 --- a/src/ZF/intr_elim.thy	Fri Aug 12 12:28:46 1994 +0200
    29.2 +++ b/src/ZF/intr_elim.thy	Fri Aug 12 12:51:34 1994 +0200
    29.3 @@ -1,3 +1,3 @@
    29.4  (*Dummy theory to document dependencies *)
    29.5  
    29.6 -intr_elim = Fixedpt + "ind_syntax"
    29.7 +intr_elim = "add_ind_def"
    30.1 --- a/src/ZF/mono.ML	Fri Aug 12 12:28:46 1994 +0200
    30.2 +++ b/src/ZF/mono.ML	Fri Aug 12 12:51:34 1994 +0200
    30.3 @@ -190,3 +190,8 @@
    30.4      "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
    30.5  by (fast_tac (FOL_cs addIs [PQimp RS mp]) 1);
    30.6  val all_mono = result();
    30.7 +
    30.8 +(*Used in intr_elim.ML and in individual datatype definitions*)
    30.9 +val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
   30.10 +		   ex_mono, Collect_mono, Part_mono, in_mono];
   30.11 +
    31.1 --- a/src/ZF/simpdata.ML	Fri Aug 12 12:28:46 1994 +0200
    31.2 +++ b/src/ZF/simpdata.ML	Fri Aug 12 12:51:34 1994 +0200
    31.3 @@ -50,9 +50,8 @@
    31.4  
    31.5  val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
    31.6  
    31.7 -(*To instantiate variables in typing conditions; 
    31.8 -  to perform type checking faster than rewriting can
    31.9 -  NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
   31.10 +(*Instantiates variables in typing conditions.
   31.11 +  drawback: does not simplify conjunctions*)
   31.12  fun type_auto_tac tyrls hyps = SELECT_GOAL
   31.13      (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
   31.14             ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));