ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
authorlcp
Thu Aug 25 12:09:21 1994 +0200 (1994-08-25)
changeset 578efc648d29dd0
parent 577 776b5ba748d8
child 579 08f465e23dc5
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
the keyword "inductive" making the theory file fail

ZF/Makefile: now has Inductive.thy,.ML

ZF/Datatype,Finite,Zorn: depend upon Inductive
ZF/intr_elim: now checks that the inductive name does not clash with
existing theory names
ZF/ind_section: deleted things replicated in Pure/section_utils.ML
ZF/ROOT: now loads Pure/section_utils
src/ZF/Datatype.thy
src/ZF/Finite.thy
src/ZF/Inductive.ML
src/ZF/Inductive.thy
src/ZF/Makefile
src/ZF/Order.thy
src/ZF/ROOT.ML
src/ZF/Zorn.thy
src/ZF/ex/Acc.thy
src/ZF/ind_syntax.ML
src/ZF/intr_elim.ML
     1.1 --- a/src/ZF/Datatype.thy	Thu Aug 25 10:41:17 1994 +0200
     1.2 +++ b/src/ZF/Datatype.thy	Thu Aug 25 12:09:21 1994 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  (*Dummy theory to document dependencies *)
     1.5  
     1.6 -Datatype = "constructor" + "inductive" + Univ + QUniv
     1.7 +Datatype = "constructor" + "Inductive" + Univ + QUniv
     1.8  
     1.9  (*Datatype must be capital to avoid conflicts with ML's "datatype" *)
    1.10 \ No newline at end of file
     2.1 --- a/src/ZF/Finite.thy	Thu Aug 25 10:41:17 1994 +0200
     2.2 +++ b/src/ZF/Finite.thy	Thu Aug 25 12:09:21 1994 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  Finite powerset operator
     2.5  *)
     2.6  
     2.7 -Finite = Arith + 
     2.8 +Finite = Arith + "Inductive" +
     2.9  consts
    2.10    Fin 	    :: "i=>i"
    2.11    FiniteFun :: "[i,i]=>i"		("(_ -||>/ _)" [61, 60] 60)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/Inductive.ML	Thu Aug 25 12:09:21 1994 +0200
     3.3 @@ -0,0 +1,228 @@
     3.4 +(*  Title: 	ZF/Inductive.ML
     3.5 +    ID:         $Id$
     3.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1993  University of Cambridge
     3.8 +
     3.9 +(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory
    3.10 +
    3.11 +Inductive definitions use least fixedpoints with standard products and sums
    3.12 +Coinductive definitions use greatest fixedpoints with Quine products and sums
    3.13 +
    3.14 +Sums are used only for mutual recursion;
    3.15 +Products are used only to derive "streamlined" induction rules for relations
    3.16 +*)
    3.17 +
    3.18 +local open Ind_Syntax
    3.19 +in
    3.20 +structure Lfp =
    3.21 +  struct
    3.22 +  val oper	= Const("lfp",      [iT,iT-->iT]--->iT)
    3.23 +  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
    3.24 +  val bnd_monoI	= bnd_monoI
    3.25 +  val subs	= def_lfp_subset
    3.26 +  val Tarski	= def_lfp_Tarski
    3.27 +  val induct	= def_induct
    3.28 +  end;
    3.29 +
    3.30 +structure Standard_Prod =
    3.31 +  struct
    3.32 +  val sigma	= Const("Sigma", [iT, iT-->iT]--->iT)
    3.33 +  val pair	= Const("Pair", [iT,iT]--->iT)
    3.34 +  val split_const	= Const("split", [[iT,iT]--->iT, iT]--->iT)
    3.35 +  val fsplit_const	= Const("fsplit", [[iT,iT]--->oT, iT]--->oT)
    3.36 +  val pair_iff	= Pair_iff
    3.37 +  val split_eq	= split
    3.38 +  val fsplitI	= fsplitI
    3.39 +  val fsplitD	= fsplitD
    3.40 +  val fsplitE	= fsplitE
    3.41 +  end;
    3.42 +
    3.43 +structure Standard_Sum =
    3.44 +  struct
    3.45 +  val sum	= Const("op +", [iT,iT]--->iT)
    3.46 +  val inl	= Const("Inl", iT-->iT)
    3.47 +  val inr	= Const("Inr", iT-->iT)
    3.48 +  val elim	= Const("case", [iT-->iT, iT-->iT, iT]--->iT)
    3.49 +  val case_inl	= case_Inl
    3.50 +  val case_inr	= case_Inr
    3.51 +  val inl_iff	= Inl_iff
    3.52 +  val inr_iff	= Inr_iff
    3.53 +  val distinct	= Inl_Inr_iff
    3.54 +  val distinct' = Inr_Inl_iff
    3.55 +  end;
    3.56 +end;
    3.57 +
    3.58 +functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
    3.59 +  : sig include INTR_ELIM INDRULE end =
    3.60 +struct
    3.61 +structure Intr_elim = 
    3.62 +    Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
    3.63 +		  Pr=Standard_Prod and Su=Standard_Sum);
    3.64 +
    3.65 +structure Indrule = Indrule_Fun (structure Inductive=Inductive and 
    3.66 +		                 Pr=Standard_Prod and Intr_elim=Intr_elim);
    3.67 +
    3.68 +open Intr_elim Indrule
    3.69 +end;
    3.70 +
    3.71 +
    3.72 +structure Ind = Add_inductive_def_Fun
    3.73 +    (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
    3.74 +
    3.75 +
    3.76 +signature INDUCTIVE_STRING =
    3.77 +  sig
    3.78 +  val thy_name   : string 		(*name of the new theory*)
    3.79 +  val rec_doms   : (string*string) list	(*recursion terms and their domains*)
    3.80 +  val sintrs     : string list		(*desired introduction rules*)
    3.81 +  end;
    3.82 +
    3.83 +
    3.84 +(*For upwards compatibility: can be called directly from ML*)
    3.85 +functor Inductive_Fun
    3.86 + (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
    3.87 +   : sig include INTR_ELIM INDRULE end =
    3.88 +Ind_section_Fun
    3.89 +   (open Inductive Ind_Syntax
    3.90 +    val sign = sign_of thy;
    3.91 +    val rec_tms = map (readtm sign iT o #1) rec_doms
    3.92 +    and domts   = map (readtm sign iT o #2) rec_doms
    3.93 +    and intr_tms = map (readtm sign propT) sintrs;
    3.94 +    val thy = thy |> Ind.add_fp_def_i(rec_tms, domts, intr_tms) 
    3.95 +                  |> add_thyname thy_name);
    3.96 +
    3.97 +
    3.98 +
    3.99 +local open Ind_Syntax
   3.100 +in
   3.101 +structure Gfp =
   3.102 +  struct
   3.103 +  val oper	= Const("gfp",      [iT,iT-->iT]--->iT)
   3.104 +  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
   3.105 +  val bnd_monoI	= bnd_monoI
   3.106 +  val subs	= def_gfp_subset
   3.107 +  val Tarski	= def_gfp_Tarski
   3.108 +  val induct	= def_Collect_coinduct
   3.109 +  end;
   3.110 +
   3.111 +structure Quine_Prod =
   3.112 +  struct
   3.113 +  val sigma	= Const("QSigma", [iT, iT-->iT]--->iT)
   3.114 +  val pair	= Const("QPair", [iT,iT]--->iT)
   3.115 +  val split_const	= Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
   3.116 +  val fsplit_const	= Const("qfsplit", [[iT,iT]--->oT, iT]--->oT)
   3.117 +  val pair_iff	= QPair_iff
   3.118 +  val split_eq	= qsplit
   3.119 +  val fsplitI	= qfsplitI
   3.120 +  val fsplitD	= qfsplitD
   3.121 +  val fsplitE	= qfsplitE
   3.122 +  end;
   3.123 +
   3.124 +structure Quine_Sum =
   3.125 +  struct
   3.126 +  val sum	= Const("op <+>", [iT,iT]--->iT)
   3.127 +  val inl	= Const("QInl", iT-->iT)
   3.128 +  val inr	= Const("QInr", iT-->iT)
   3.129 +  val elim	= Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
   3.130 +  val case_inl	= qcase_QInl
   3.131 +  val case_inr	= qcase_QInr
   3.132 +  val inl_iff	= QInl_iff
   3.133 +  val inr_iff	= QInr_iff
   3.134 +  val distinct	= QInl_QInr_iff
   3.135 +  val distinct' = QInr_QInl_iff
   3.136 +  end;
   3.137 +end;
   3.138 +
   3.139 +
   3.140 +signature COINDRULE =
   3.141 +  sig
   3.142 +  val coinduct : thm
   3.143 +  end;
   3.144 +
   3.145 +
   3.146 +functor CoInd_section_Fun
   3.147 + (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
   3.148 +    : sig include INTR_ELIM COINDRULE end =
   3.149 +struct
   3.150 +structure Intr_elim = 
   3.151 +    Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
   3.152 +		  Pr=Quine_Prod and Su=Quine_Sum);
   3.153 +
   3.154 +open Intr_elim 
   3.155 +val coinduct = raw_induct
   3.156 +end;
   3.157 +
   3.158 +
   3.159 +structure CoInd = 
   3.160 +    Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
   3.161 +
   3.162 +
   3.163 +(*For upwards compatibility: can be called directly from ML*)
   3.164 +functor CoInductive_Fun
   3.165 + (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
   3.166 +   : sig include INTR_ELIM COINDRULE end =
   3.167 +CoInd_section_Fun
   3.168 +   (open Inductive Ind_Syntax
   3.169 +    val sign = sign_of thy;
   3.170 +    val rec_tms = map (readtm sign iT o #1) rec_doms
   3.171 +    and domts   = map (readtm sign iT o #2) rec_doms
   3.172 +    and intr_tms = map (readtm sign propT) sintrs;
   3.173 +    val thy = thy |> CoInd.add_fp_def_i(rec_tms, domts, intr_tms) 
   3.174 +                  |> add_thyname thy_name);
   3.175 +
   3.176 +
   3.177 +
   3.178 +(*For installing the theory section.   co is either "" or "Co"*)
   3.179 +fun inductive_decl co =
   3.180 +  let open ThyParse Ind_Syntax
   3.181 +      fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
   3.182 +	  if Syntax.is_identifier s then "op " ^ s  else "_"
   3.183 +      fun mk_params (((((domains: (string*string) list, ipairs), 
   3.184 +			monos), con_defs), type_intrs), type_elims) =
   3.185 +        let val big_rec_name = space_implode "_" 
   3.186 +		             (map (scan_to_id o trim o #1) domains)
   3.187 +	    and srec_tms = mk_list (map #1 domains)
   3.188 +            and sdoms    = mk_list (map #2 domains)
   3.189 +	    and sintrs   = mk_big_list (map snd ipairs)
   3.190 +            val stri_name = big_rec_name ^ "_Intrnl"
   3.191 +        in
   3.192 +	   (";\n\n\
   3.193 +            \structure " ^ stri_name ^ " =\n\
   3.194 +            \ let open Ind_Syntax in\n\
   3.195 +            \  struct\n\
   3.196 +            \  val _ = writeln \"" ^ co ^ 
   3.197 +	               "Inductive definition " ^ big_rec_name ^ "\"\n\
   3.198 +            \  val rec_tms\t= map (readtm (sign_of thy) iT) "
   3.199 +	                     ^ srec_tms ^ "\n\
   3.200 +            \  and domts\t= map (readtm (sign_of thy) iT) "
   3.201 +	                     ^ sdoms ^ "\n\
   3.202 +            \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
   3.203 +	                     ^ sintrs ^ "\n\
   3.204 +            \  end\n\
   3.205 +            \ end;\n\n\
   3.206 +            \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
   3.207 +	       stri_name ^ ".rec_tms, " ^
   3.208 +               stri_name ^ ".domts, " ^
   3.209 +               stri_name ^ ".intr_tms)"
   3.210 +           ,
   3.211 +	    "structure " ^ big_rec_name ^ " =\n\
   3.212 +            \  struct\n\
   3.213 +            \  structure Result = " ^ co ^ "Ind_section_Fun\n\
   3.214 +            \  (open " ^ stri_name ^ "\n\
   3.215 +            \   val thy\t\t= thy\n\
   3.216 +            \   val monos\t\t= " ^ monos ^ "\n\
   3.217 +            \   val con_defs\t\t= " ^ con_defs ^ "\n\
   3.218 +            \   val type_intrs\t= " ^ type_intrs ^ "\n\
   3.219 +            \   val type_elims\t= " ^ type_elims ^ ");\n\n\
   3.220 +            \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
   3.221 +            \  open Result\n\
   3.222 +            \  end\n"
   3.223 +	   )
   3.224 +	end
   3.225 +      val domains = "domains" $$-- repeat1 (string --$$ "<=" -- !! string)
   3.226 +      val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
   3.227 +      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
   3.228 +  in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
   3.229 +             -- optstring "type_intrs" -- optstring "type_elims"
   3.230 +     >> mk_params
   3.231 +  end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/Inductive.thy	Thu Aug 25 12:09:21 1994 +0200
     4.3 @@ -0,0 +1,3 @@
     4.4 +(*Dummy theory to document dependencies *)
     4.5 +
     4.6 +Inductive = "indrule"
     5.1 --- a/src/ZF/Makefile	Thu Aug 25 10:41:17 1994 +0200
     5.2 +++ b/src/ZF/Makefile	Thu Aug 25 12:09:21 1994 +0200
     5.3 @@ -23,9 +23,10 @@
     5.4  	func.thy func.ML AC.thy AC.ML simpdata.thy simpdata.ML\
     5.5  	equalities.thy equalities.ML Bool.thy Bool.ML \
     5.6  	Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \
     5.7 -	ind_syntax.thy ind_syntax.ML add_ind_def.thy add_ind_def.ML \
     5.8 +	../Pure/section_utils.ML ind_syntax.thy ind_syntax.ML \
     5.9 +         add_ind_def.thy add_ind_def.ML \
    5.10  	intr_elim.thy intr_elim.ML indrule.thy indrule.ML \
    5.11 -	inductive.thy inductive.ML \
    5.12 +	Inductive.thy Inductive.ML \
    5.13  	Perm.thy Perm.ML Rel.thy Rel.ML EquivClass.ML EquivClass.thy \
    5.14  	Trancl.thy Trancl.ML \
    5.15  	WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
     6.1 --- a/src/ZF/Order.thy	Thu Aug 25 10:41:17 1994 +0200
     6.2 +++ b/src/ZF/Order.thy	Thu Aug 25 12:09:21 1994 +0200
     6.3 @@ -14,7 +14,7 @@
     6.4    ord_iso         :: "[i,i,i,i]=>i"	(*Order isomorphisms*)
     6.5    pred            :: "[i,i,i]=>i"	(*Set of predecessors*)
     6.6  
     6.7 -rules
     6.8 +defs
     6.9    part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
    6.10  
    6.11    linear_def   "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
     7.1 --- a/src/ZF/ROOT.ML	Thu Aug 25 10:41:17 1994 +0200
     7.2 +++ b/src/ZF/ROOT.ML	Thu Aug 25 12:09:21 1994 +0200
     7.3 @@ -29,6 +29,7 @@
     7.4  print_depth 1;
     7.5  
     7.6  (*Add user sections for inductive/datatype definitions*)
     7.7 +use     "../Pure/section_utils.ML";
     7.8  use_thy "Datatype";
     7.9  structure ThySyn = ThySynFun
    7.10   (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
     8.1 --- a/src/ZF/Zorn.thy	Thu Aug 25 10:41:17 1994 +0200
     8.2 +++ b/src/ZF/Zorn.thy	Thu Aug 25 12:09:21 1994 +0200
     8.3 @@ -11,7 +11,7 @@
     8.4  Union_in_Pow is proved in ZF.ML
     8.5  *)
     8.6  
     8.7 -Zorn = OrderArith + AC + "inductive" +
     8.8 +Zorn = OrderArith + AC + "Inductive" +
     8.9  
    8.10  consts
    8.11    Subset_rel      :: "i=>i"
     9.1 --- a/src/ZF/ex/Acc.thy	Thu Aug 25 10:41:17 1994 +0200
     9.2 +++ b/src/ZF/ex/Acc.thy	Thu Aug 25 12:09:21 1994 +0200
     9.3 @@ -9,10 +9,10 @@
     9.4  Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
     9.5  *)
     9.6  
     9.7 -Acc = WF + "inductive" +
     9.8 +Acc = WF + "Inductive" +
     9.9  
    9.10  consts
    9.11 -  "acc" :: "i=>i"
    9.12 +  acc :: "i=>i"
    9.13  
    9.14  inductive
    9.15    domains "acc(r)" <= "field(r)"
    10.1 --- a/src/ZF/ind_syntax.ML	Thu Aug 25 10:41:17 1994 +0200
    10.2 +++ b/src/ZF/ind_syntax.ML	Thu Aug 25 12:09:21 1994 +0200
    10.3 @@ -11,23 +11,12 @@
    10.4  *)
    10.5  structure Ind_Syntax =
    10.6  struct
    10.7 -(*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*)
    10.8 -fun mk_defpair (lhs, rhs) = 
    10.9 -  let val Const(name, _) = head_of lhs
   10.10 -  in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
   10.11 -
   10.12 -fun get_def thy s = get_axiom thy (s^"_def");
   10.13 -
   10.14 -fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
   10.15  
   10.16  (** Abstract syntax definitions for FOL and ZF **)
   10.17  
   10.18  val iT = Type("i",[])
   10.19  and oT = Type("o",[]);
   10.20  
   10.21 -fun ap t u = t$u;
   10.22 -fun app t (u1,u2) = t $ u1 $ u2;
   10.23 -
   10.24  (*Given u expecting arguments of types [T1,...,Tn], create term of 
   10.25    type T1*...*Tn => i using split*)
   10.26  fun ap_split split u [ ]   = Abs("null", iT, u)
   10.27 @@ -62,38 +51,6 @@
   10.28  val Trueprop = Const("Trueprop",oT-->propT);
   10.29  fun mk_tprop P = Trueprop $ P;
   10.30  
   10.31 -(*Read an assumption in the given theory*)
   10.32 -fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
   10.33 -
   10.34 -fun readtm sign T a = 
   10.35 -    read_cterm sign (a,T) |> term_of
   10.36 -    handle ERROR => error ("The error above occurred for " ^ a);
   10.37 -
   10.38 -(*Skipping initial blanks, find the first identifier*)
   10.39 -fun scan_to_id s = 
   10.40 -    s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
   10.41 -    handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
   10.42 -
   10.43 -fun is_backslash c = c = "\\";
   10.44 -
   10.45 -(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
   10.46 -  Does not handle the \ddd form;  no error checking*)
   10.47 -fun escape [] = []
   10.48 -  | escape cs = (case take_prefix (not o is_backslash) cs of
   10.49 -	 (front, []) => front
   10.50 -       | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
   10.51 -       | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
   10.52 -       | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
   10.53 -       | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
   10.54 -       | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
   10.55 -       | (front, b::c::rest) => 
   10.56 -	   if is_blank c   (*remove any further blanks and the following \ *)
   10.57 -	   then front @ escape (tl (snd (take_prefix is_blank rest)))
   10.58 -	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
   10.59 -
   10.60 -(*Remove the first and last charaters -- presumed to be quotes*)
   10.61 -val trim = implode o escape o rev o tl o rev o tl o explode;
   10.62 -
   10.63  (*simple error-checking in the premises of an inductive definition*)
   10.64  fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
   10.65  	error"Premises may not be conjuctive"
   10.66 @@ -102,10 +59,6 @@
   10.67    | chk_prem rec_hd t = 
   10.68  	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
   10.69  
   10.70 -(*Make distinct individual variables a1, a2, a3, ..., an. *)
   10.71 -fun mk_frees a [] = []
   10.72 -  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
   10.73 -
   10.74  (*Return the conclusion of a rule, of the form t:X*)
   10.75  fun rule_concl rl = 
   10.76      let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
   10.77 @@ -124,13 +77,6 @@
   10.78          (make_elim (equalityD1 RS subsetD RS CollectD2));
   10.79  
   10.80  
   10.81 -(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
   10.82 -fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
   10.83 -  | tryres (th, []) = raise THM("tryres", 0, [th]);
   10.84 -
   10.85 -fun gen_make_elim elim_rls rl = 
   10.86 -      standard (tryres (rl, elim_rls @ [revcut_rl]));
   10.87 -
   10.88  (** For datatype definitions **)
   10.89  
   10.90  fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
    11.1 --- a/src/ZF/intr_elim.ML	Thu Aug 25 10:41:17 1994 +0200
    11.2 +++ b/src/ZF/intr_elim.ML	Thu Aug 25 12:09:21 1994 +0200
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title: 	ZF/intr-elim.ML
    11.5 +(*  Title: 	ZF/intr_elim.ML
    11.6      ID:         $Id$
    11.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    11.8      Copyright   1994  University of Cambridge
    11.9 @@ -48,6 +48,10 @@
   11.10  val rec_names = map (#1 o dest_Const o head_of) rec_tms;
   11.11  val big_rec_name = space_implode "_" rec_names;
   11.12  
   11.13 +val _ = deny (big_rec_name  mem  map ! (stamps_of_thy thy))
   11.14 +             ("Definition " ^ big_rec_name ^ 
   11.15 +	      " would clash with the theory of the same name!");
   11.16 +
   11.17  (*fetch fp definitions from the theory*)
   11.18  val big_rec_def::part_rec_defs = 
   11.19    map (get_def thy)
   11.20 @@ -89,9 +93,10 @@
   11.21     (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
   11.22     rtac disjIn 2,
   11.23     REPEAT (ares_tac [refl,exI,conjI] 2),
   11.24 +   (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
   11.25     rewrite_goals_tac con_defs,
   11.26 -   (*Now can solve the trivial equation*)
   11.27     REPEAT (rtac refl 2),
   11.28 +   (*Typechecking; this can fail*)
   11.29     REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
   11.30  		      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
   11.31  		      ORELSE' hyp_subst_tac)),