# HG changeset patch
# User paulson
# Date 1009270921 -3600
# Node ID 0480d02221b8d8098108d941fc621dafb6c1c74e
# Parent  5b9b0adca8aa5cdc94c1df6713837d66e205acae
conversion to Isar

diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/BCR.thy
--- a/src/ZF/Coind/BCR.thy	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/BCR.thy	Tue Dec 25 10:02:01 2001 +0100
@@ -3,25 +3,3 @@
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 *)
-
-BCR = Values + Types +
-
-(*Basic correspondence relation -- not completely specified, as it is a
-  parameter of the proof.  A concrete version could be defined inductively.*)
-
-consts
-  isof :: [i,i] => o
-rules
-  isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
-
-(*Its extension to environments*)
-
-consts
-  isofenv :: [i,i] => o
-defs
-  isofenv_def "isofenv(ve,te) ==                
-   ve_dom(ve) = te_dom(te) &            
-   ( \\<forall>x \\<in> ve_dom(ve).                          
-     \\<exists>c \\<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
-  
-end
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/Dynamic.thy
--- a/src/ZF/Coind/Dynamic.thy	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Dynamic.thy	Tue Dec 25 10:02:01 2001 +0100
@@ -4,38 +4,37 @@
     Copyright   1995  University of Cambridge
 *)
 
-Dynamic = Values +
+theory Dynamic = Values:
 
 consts
   EvalRel :: i
 inductive
   domains "EvalRel" <= "ValEnv * Exp * Val"
-  intrs
-    eval_constI
-      " [| ve \\<in> ValEnv; c \\<in> Const |] ==>   
+  intros
+    eval_constI:
+      " [| ve \<in> ValEnv; c \<in> Const |] ==>   
        <ve,e_const(c),v_const(c)>:EvalRel"
-    eval_varI
-      " [| ve \\<in> ValEnv; x \\<in> ExVar; x \\<in> ve_dom(ve) |] ==>   
+    eval_varI:
+      " [| ve \<in> ValEnv; x \<in> ExVar; x \<in> ve_dom(ve) |] ==>   
        <ve,e_var(x),ve_app(ve,x)>:EvalRel" 
-    eval_fnI
-      " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp |] ==>   
+    eval_fnI:
+      " [| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp |] ==>   
        <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "  
-    eval_fixI
-      " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val;   
+    eval_fixI:
+      " [| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val;   
           v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>   
        <ve,e_fix(f,x,e),cl>:EvalRel " 
-    eval_appI1
-      " [| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const;   
+    eval_appI1:
+      " [| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;   
           <ve,e1,v_const(c1)>:EvalRel;   
           <ve,e2,v_const(c2)>:EvalRel |] ==>   
        <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
-    eval_appI2
-      " [| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val;   
+    eval_appI2:
+      " [| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar; v \<in> Val;   
           <ve,e1,v_clos(xm,em,vem)>:EvalRel;   
           <ve,e2,v2>:EvalRel;   
           <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>   
        <ve,e_app(e1,e2),v>:EvalRel "
-  type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs"
+  type_intros c_appI ve_appI ve_empI ve_owrI Exp.intros Val_ValEnv.intros
 
-  
 end
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/ECR.ML
--- a/src/ZF/Coind/ECR.ML	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  Title:      ZF/Coind/ECR.ML
-    ID:         $Id$
-    Author:     Jacob Frost, Cambridge University Computer Laboratory
-    Copyright   1995  University of Cambridge
-*)
-
-(* Specialised co-induction rule *)
-
-Goal "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv;  \
-\        <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
-\        {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}: \
-\        Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |]    \
-\     ==> <v_clos(x, e, ve),t>:HasTyRel";
-by (rtac (singletonI RS HasTyRel.coinduct) 1);
-by (ALLGOALS Blast_tac);
-qed "htr_closCI";
-
-(* Specialised elimination rules *)
-
-val htr_constE = HasTyRel.mk_cases "<v_const(c),t>:HasTyRel";
-
-val htr_closE = HasTyRel.mk_cases "<v_clos(x,e,ve),t>:HasTyRel";
-
-(* Classical reasoning sets *)
-
-fun mk_htr_cs cs =
-  let open HasTyRel in 
-    ( cs 
-      addSIs [htr_constI] 
-      addSEs [htr_constE]
-      addIs [htr_closI,htr_closCI]
-      addEs [htr_closE])
-  end;
-
-claset_ref() := mk_htr_cs (claset());
-
-(* Properties of the pointwise extension to environments *)
-
-bind_thm ("HasTyRel_non_zero", 
-	  HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE);
-
-Goalw [hastyenv_def]
-  "[| ve \\<in> ValEnv; te \\<in> TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
-\   hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
-by (asm_full_simp_tac
-    (simpset() addsimps [ve_app_owr, HasTyRel_non_zero, ve_dom_owr]) 1);
-by Auto_tac;
-qed "hastyenv_owr";
-
-Goalw  [isofenv_def,hastyenv_def]
-  "[| ve \\<in> ValEnv; te \\<in> TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
-by Safe_tac;
-by (dtac bspec 1);
-by (assume_tac 1);
-by Safe_tac;
-by (dtac HasTyRel.htr_constI 1);
-by (assume_tac 2);
-by (etac te_appI 1);
-by (etac ve_domI 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "basic_consistency_lem";
-
-
-
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/ECR.thy
--- a/src/ZF/Coind/ECR.thy	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/ECR.thy	Tue Dec 25 10:02:01 2001 +0100
@@ -4,7 +4,7 @@
     Copyright   1995  University of Cambridge
 *)
 
-ECR = Static + Dynamic +
+theory ECR = Static + Dynamic:
 
 (* The extended correspondence relation *)
 
@@ -12,27 +12,161 @@
   HasTyRel :: i
 coinductive
   domains "HasTyRel" <= "Val * Ty"
-  intrs
-    htr_constI
-      "[| c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
-    htr_closI
-      "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv; 
-          <te,e_fn(x,e),t>:ElabRel;  
+  intros
+    htr_constI [intro!]:
+      "[| c \<in> Const; t \<in> Ty; isof(c,t) |] ==> <v_const(c),t> \<in> HasTyRel"
+    htr_closI [intro]:
+      "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv; 
+          <te,e_fn(x,e),t> \<in> ElabRel;  
           ve_dom(ve) = te_dom(te);   
-          {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}:Pow(HasTyRel)  
-      |] ==>   
-      <v_clos(x,e,ve),t>:HasTyRel" 
+          {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in> Pow(HasTyRel) |] 
+       ==> <v_clos(x,e,ve),t> \<in> HasTyRel" 
   monos  Pow_mono
-  type_intrs "Val_ValEnv.intrs"
+  type_intros Val_ValEnv.intros
   
 (* Pointwise extension to environments *)
  
-consts
-  hastyenv :: [i,i] => o
-defs
-  hastyenv_def 
-    " hastyenv(ve,te) ==                        
-     ve_dom(ve) = te_dom(te) &          
-     (\\<forall>x \\<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
+constdefs
+  hastyenv :: "[i,i] => o"
+    "hastyenv(ve,te) ==                        
+	 ve_dom(ve) = te_dom(te) &          
+	 (\<forall>x \<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)> \<in> HasTyRel)"
+
+(* Specialised co-induction rule *)
+
+lemma htr_closCI [intro]:
+     "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv;   
+         <te, e_fn(x, e), t> \<in> ElabRel; ve_dom(ve) = te_dom(te);  
+         {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in>
+           Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |]     
+      ==> <v_clos(x, e, ve),t> \<in> HasTyRel"
+apply (rule singletonI [THEN HasTyRel.coinduct])
+apply auto
+done
+
+(* Specialised elimination rules *)
+
+inductive_cases htr_constE [elim!]: "<v_const(c),t> \<in> HasTyRel"
+inductive_cases htr_closE  [elim]:  "<v_clos(x,e,ve),t> \<in> HasTyRel"
+
+
+(* Properties of the pointwise extension to environments *)
+
+lemmas HasTyRel_non_zero =
+       HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE, standard]
+
+lemma hastyenv_owr: 
+  "[| ve \<in> ValEnv; te \<in> TyEnv; hastyenv(ve,te); <v,t> \<in> HasTyRel |] 
+   ==> hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))"
+by (auto simp add: hastyenv_def ve_app_owr HasTyRel_non_zero)
+
+lemma basic_consistency_lem: 
+  "[| ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)"
+apply (unfold isofenv_def hastyenv_def)
+apply (force intro: te_appI ve_domI) 
+done
+
+
+(* ############################################################ *)
+(* The Consistency theorem                                      *)
+(* ############################################################ *)
+
+lemma consistency_const:
+     "[| c \<in> Const; hastyenv(ve,te);<te,e_const(c),t> \<in> ElabRel |] 
+      ==> <v_const(c), t> \<in> HasTyRel"
+by blast
+
+
+lemma consistency_var: 
+  "[| x \<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t> \<in> ElabRel |] ==>      
+   <ve_app(ve,x),t> \<in> HasTyRel"
+by (unfold hastyenv_def, blast)
+
+lemma consistency_fn: 
+  "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; hastyenv(ve,te);        
+           <te,e_fn(x,e),t> \<in> ElabRel   
+        |] ==> <v_clos(x, e, ve), t> \<in> HasTyRel"
+by (unfold hastyenv_def, blast)
+
+declare ElabRel.dom_subset [THEN subsetD, dest]
+
+declare Ty.intros [simp, intro!]
+declare TyEnv.intros [simp, intro!]
+declare Val_ValEnv.intros [simp, intro!]
+
+lemma consistency_fix: 
+  "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val;                
+      v_clos(x,e,ve_owr(ve,f,cl)) = cl;                           
+      hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel |] ==>        
+   <cl,t> \<in> HasTyRel"
+apply (unfold hastyenv_def)
+apply (erule elab_fixE)
+apply safe
+apply (rule subst, assumption) 
+apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI)
+apply simp_all
+apply (blast intro: ve_owrI) 
+apply (rule ElabRel.fnI)
+apply (simp_all add: ValNEE)
+apply force
+done
+
+
+lemma consistency_app1:
+ "[| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;    
+     <ve,e1,v_const(c1)> \<in> EvalRel;                       
+     \<forall>t te.                                          
+       hastyenv(ve,te) --> <te,e1,t> \<in> ElabRel --> <v_const(c1),t> \<in> HasTyRel;
+     <ve, e2, v_const(c2)> \<in> EvalRel;                   
+     \<forall>t te.                                          
+       hastyenv(ve,te) --> <te,e2,t> \<in> ElabRel --> <v_const(c2),t> \<in> HasTyRel;
+     hastyenv(ve, te);                                  
+     <te,e_app(e1,e2),t> \<in> ElabRel |] 
+  ==> <v_const(c_app(c1, c2)),t> \<in> HasTyRel"
+by (blast intro!: c_appI intro: isof_app)
+
+lemma consistency_app2:
+ "[| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar; 
+     v \<in> Val;   
+     <ve,e1,v_clos(xm,em,vem)> \<in> EvalRel;        
+     \<forall>t te. hastyenv(ve,te) -->                     
+            <te,e1,t> \<in> ElabRel --> <v_clos(xm,em,vem),t> \<in> HasTyRel;         
+     <ve,e2,v2> \<in> EvalRel;                       
+     \<forall>t te. hastyenv(ve,te) --> <te,e2,t> \<in> ElabRel --> <v2,t> \<in> HasTyRel;
+     <ve_owr(vem,xm,v2),em,v> \<in> EvalRel;         
+     \<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) -->      
+            <te,em,t> \<in> ElabRel --> <v,t> \<in> HasTyRel;
+     hastyenv(ve,te); <te,e_app(e1,e2),t> \<in> ElabRel |] 
+   ==> <v,t> \<in> HasTyRel"
+apply (erule elab_appE)
+apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
+apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
+apply (erule htr_closE)
+apply (erule elab_fnE)
+apply simp
+apply clarify
+apply (drule spec [THEN spec, THEN mp, THEN mp])
+prefer 2 apply assumption+
+apply (rule hastyenv_owr)
+apply assumption
+apply assumption 
+apply (simp add: hastyenv_def)
+apply blast+
+done
+
+lemma consistency [rule_format]:
+   "<ve,e,v> \<in> EvalRel 
+    ==> (\<forall>t te. hastyenv(ve,te) --> <te,e,t> \<in> ElabRel --> <v,t> \<in> HasTyRel)"
+apply (erule EvalRel.induct)
+apply (simp_all add: consistency_const consistency_var consistency_fn 
+                     consistency_fix consistency_app1)
+apply (blast intro: consistency_app2)
+done
+
+lemma basic_consistency:
+     "[| ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te);                    
+         <ve,e,v_const(c)> \<in> EvalRel; <te,e,t> \<in> ElabRel |] 
+      ==> isof(c,t)"
+by (blast dest: consistency intro!: basic_consistency_lem)
 
 end
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/Language.thy
--- a/src/ZF/Coind/Language.thy	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Language.thy	Tue Dec 25 10:02:01 2001 +0100
@@ -4,15 +4,17 @@
     Copyright   1995  University of Cambridge
 *)
 
-Language = Main +
+theory Language = Main:
 
 consts
   Const :: i                    (* Abstract type of constants *)
-  c_app :: [i,i] => i           (* Abstract constructor for fun application*)
+  c_app :: "[i,i] => i"         (* Abstract constructor for fun application*)
+
 
-rules
-  constNEE  "c \\<in> Const ==> c \\<noteq> 0"
-  c_appI    "[| c1 \\<in> Const; c2 \\<in> Const |] ==> c_app(c1,c2):Const"
+text{*these really can't be definitions without losing the abstraction*}
+axioms
+  constNEE:  "c \<in> Const ==> c \<noteq> 0"
+  c_appI:    "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const"
 
 
 consts
@@ -20,10 +22,10 @@
   ExVar :: i                    (* Abstract type of variables *)
 
 datatype
-  "Exp" = e_const ("c \\<in> Const")
-        | e_var ("x \\<in> ExVar")
-        | e_fn ("x \\<in> ExVar","e \\<in> Exp")
-        | e_fix ("x1 \\<in> ExVar","x2 \\<in> ExVar","e \\<in> Exp")
-        | e_app ("e1 \\<in> Exp","e2 \\<in> Exp")
+  "Exp" = e_const ("c \<in> Const")
+        | e_var ("x \<in> ExVar")
+        | e_fn ("x \<in> ExVar","e \<in> Exp")
+        | e_fix ("x1 \<in> ExVar","x2 \<in> ExVar","e \<in> Exp")
+        | e_app ("e1 \<in> Exp","e2 \<in> Exp")
 
 end
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/MT.ML
--- a/src/ZF/Coind/MT.ML	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,149 +0,0 @@
-(*  Title:      ZF/Coind/MT.ML
-    ID:         $Id$
-    Author:     Jacob Frost, Cambridge University Computer Laboratory
-    Copyright   1995  University of Cambridge
-*)
-
-(* ############################################################ *)
-(* The Consistency theorem                                      *)
-(* ############################################################ *)
-
-Goal "[| c \\<in> Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==>         \
-\       <v_const(c), t> \\<in> HasTyRel";
-by (Fast_tac 1);
-qed "consistency_const";
-
-
-Goalw [hastyenv_def]
-  "[| x \\<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==>     \
-\  <ve_app(ve,x),t>:HasTyRel";
-by (Fast_tac 1);
-qed "consistency_var";
-
-
-Goalw [hastyenv_def]
-  "[| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; hastyenv(ve,te);       \
-\          <te,e_fn(x,e),t>:ElabRel  \
-\       |] ==> <v_clos(x, e, ve), t> \\<in> HasTyRel";
-by (Blast_tac 1);
-qed "consistency_fn";
-
-AddDs [te_owrE, ElabRel.dom_subset RS subsetD];
-
-Addsimps [ve_dom_owr, ve_app_owr1, ve_app_owr2, 
-          te_app_owr1, te_app_owr2];
-
-val clean_tac = 
-  REPEAT_FIRST (fn i => 
-    (eq_assume_tac i) ORELSE 
-    (match_tac (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs) i) ORELSE
-    (ematch_tac [te_owrE] i));
-
-Goalw [hastyenv_def]
-  "[| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val;               \
-\     v_clos(x,e,ve_owr(ve,f,cl)) = cl;                         \ 
-\     hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==>       \
-\  <cl,t>:HasTyRel";
-by (etac elab_fixE 1);
-by Safe_tac;
-by (EVERY [ftac subst 1,atac 2,rtac htr_closCI 1]);
-by clean_tac;
-by (rtac ve_owrI 1);
-by clean_tac;
-by (dtac (ElabRel.dom_subset RS subsetD) 1);
-by (eres_inst_tac [("Q","te_owr(te,f,t_fun(t1,t2)):TyEnv")] 
-    (SigmaD1 RS te_owrE) 1);
-by (assume_tac 1);
-by (rtac ElabRel.fnI 1);
-by clean_tac;
-by (Asm_simp_tac 1);
-by (stac ve_dom_owr 1);
-by (assume_tac 1);
-by (etac subst 1);
-by (rtac v_closNE 1);
-by (Asm_simp_tac 1);
-
-by (rtac PowI 1);
-by (stac ve_dom_owr 1);
-by (assume_tac 1);
-by (etac subst 1);
-by (rtac v_closNE 1);
-by (rtac subsetI 1);
-by (etac RepFunE 1);
-by (case_tac "f=y" 1);
-by Auto_tac;
-qed "consistency_fix";
-
-
-Goal "[| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const;   \
-\     <ve,e1,v_const(c1)>:EvalRel;                      \
-\     \\<forall>t te.                                         \
-\       hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
-\     <ve, e2, v_const(c2)> \\<in> EvalRel;                  \
-\     \\<forall>t te.                                         \
-\       hastyenv(ve,te) --> <te,e2,t>:ElabRel --> <v_const(c2),t>:HasTyRel; \
-\     hastyenv(ve, te);                                 \
-\     <te,e_app(e1,e2),t>:ElabRel |] ==>                \
-\   <v_const(c_app(c1, c2)),t>:HasTyRel";
-by (etac elab_appE 1);
-by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
-qed "consistency_app1";
-
-Goal "[| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val;  \
-\        <ve,e1,v_clos(xm,em,vem)>:EvalRel;       \
-\        \\<forall>t te.                                \
-\          hastyenv(ve,te) -->                    \
-\          <te,e1,t>:ElabRel -->                  \
-\          <v_clos(xm,em,vem),t>:HasTyRel;        \
-\        <ve,e2,v2>:EvalRel;                      \
-\        \\<forall>t te.                                \
-\          hastyenv(ve,te) -->                    \
-\          <te,e2,t>:ElabRel -->                  \
-\          <v2,t>:HasTyRel;                       \
-\        <ve_owr(vem,xm,v2),em,v>:EvalRel;        \
-\        \\<forall>t te.                                \
-\          hastyenv(ve_owr(vem,xm,v2),te) -->     \
-\          <te,em,t>:ElabRel -->                  \
-\          <v,t>:HasTyRel;                        \
-\        hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==>      \
-\     <v,t>:HasTyRel ";
-by (etac elab_appE 1);
-by (dtac (spec RS spec RS mp RS mp) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (dtac (spec RS spec RS mp RS mp) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (etac htr_closE 1);
-by (etac elab_fnE 1);
-by (Full_simp_tac 1);
-by (Clarify_tac 1);
-by (dtac (spec RS spec RS mp RS mp) 1);
-by (assume_tac 3);
-by (assume_tac 2);
-by (rtac hastyenv_owr 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (assume_tac 2);
-by (asm_simp_tac (simpset() addsimps [hastyenv_def]) 1);
-by (Fast_tac 1);
-qed "consistency_app2";
-
-Goal "<ve,e,v>:EvalRel ==>         \
-\       (\\<forall>t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
-by (etac EvalRel.induct 1);
-by (blast_tac (claset() addIs [consistency_app2]) 6);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [consistency_const, consistency_var, consistency_fn, consistency_fix, consistency_app1])));
-qed "consistency";
-
-
-Goal "[| ve \\<in> ValEnv; te \\<in> TyEnv;              \
-\        isofenv(ve,te);                   \
-\        <ve,e,v_const(c)>:EvalRel;        \
-\        <te,e,t>:ElabRel                  \
-\     |] ==> isof(c,t)";
-by (rtac htr_constE 1);
-by (dtac consistency 1);
-by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
-by (assume_tac 1);
-qed "basic_consistency";
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/MT.thy
--- a/src/ZF/Coind/MT.thy	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-MT = ECR
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/Map.ML
--- a/src/ZF/Coind/Map.ML	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,206 +0,0 @@
-(*  Title:      ZF/Coind/Map.ML
-    ID:         $Id$
-    Author:     Jacob Frost, Cambridge University Computer Laboratory
-    Copyright   1995  University of Cambridge
-*)
-
-(** Some sample proofs of inclusions for the final coalgebra "U" (by lcp) **)
-
-Goalw [TMap_def] "{0,1} \\<subseteq> {1} Un TMap(I, {0,1})";
-by (Blast_tac 1);
-result();
-
-Goalw [TMap_def] "{0} Un TMap(I,1) \\<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))";
-by (Blast_tac 1);
-result();
-
-Goalw [TMap_def] "{0,1} Un TMap(I,2) \\<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))";
-by (Blast_tac 1);
-result();
-
-(*
-Goalw [TMap_def]
-     "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \\<subseteq> \
-\     {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))";
-by (Blast_tac 1);
-result();
-*)
-
-
-(* ############################################################ *)
-(* Lemmas                                                       *)
-(* ############################################################ *)
-
-Goal "Sigma(A,B)``{a} = (if a \\<in> A then B(a) else 0)";
-by Auto_tac;
-qed "qbeta_if";
-
-Goal "a \\<in> A ==> Sigma(A,B)``{a} = B(a)";
-by (Fast_tac 1);
-qed "qbeta";
-
-Goal "a\\<notin>A ==> Sigma(A,B)``{a} = 0";
-by (Fast_tac 1);
-qed "qbeta_emp";
-
-Goal "a \\<notin> A ==> Sigma(A,B)``{a}=0";
-by (Fast_tac 1);
-qed "image_Sigma1";
-
-
-(* ############################################################ *)
-(* Inclusion in Quine Universes                                 *)
-(* ############################################################ *)
-
-(* Lemmas *)
-
-Goalw [quniv_def]
-    "A \\<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \\<subseteq> quniv(X)";
-by (rtac Pow_mono 1);
-by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1);
-by (etac subset_trans 1);
-by (rtac (arg_subset_eclose RS univ_mono) 1);
-by (simp_tac (simpset() addsimps [Union_Pow_eq]) 1);
-qed "MapQU_lemma";
-
-(* Theorems *)
-
-val prems = goalw Map.thy [PMap_def,TMap_def]
-  "[| m \\<in> PMap(A,quniv(B)); !!x. x \\<in> A ==> x \\<in> univ(B) |] ==> m \\<in> quniv(B)";
-by (cut_facts_tac prems 1);
-by (rtac (MapQU_lemma RS subsetD) 1);
-by (rtac subsetI 1);
-by (eresolve_tac prems 1);
-by (Fast_tac 1);
-qed "mapQU";
-
-(* ############################################################ *)
-(* Monotonicity                                                 *)
-(* ############################################################ *)
-
-Goalw [PMap_def,TMap_def] "B \\<subseteq> C ==> PMap(A,B)<=PMap(A,C)";
-by (Blast_tac 1);
-qed "map_mono";
-
-(* Rename to pmap_mono *)
-
-(* ############################################################ *)
-(* Introduction Rules                                           *)
-(* ############################################################ *)
-
-(** map_emp **)
-
-Goalw [map_emp_def,PMap_def,TMap_def] "map_emp \\<in> PMap(A,B)";
-by Auto_tac;
-qed "pmap_empI";
-
-(** map_owr **)
-
-
-Goalw [map_owr_def,PMap_def,TMap_def] 
-  "[| m \\<in> PMap(A,B); a \\<in> A; b \\<in> B |]  ==> map_owr(m,a,b):PMap(A,B)";
-by Safe_tac;
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [if_iff])));
-by (Fast_tac 1);
-by (Fast_tac 1);
-by (Deepen_tac 2 1);
-(*Remaining subgoal*)
-by (rtac (excluded_middle RS disjE) 1);
-by (etac image_Sigma1 1);
-by (dres_inst_tac [("psi", "?uu \\<notin> B")] asm_rl 1);
-by (asm_full_simp_tac (simpset() addsimps [qbeta]) 1);
-by Safe_tac;
-by (dres_inst_tac [("psi", "?uu \\<notin> B")] asm_rl 3);
-by (ALLGOALS Asm_full_simp_tac);
-by (Fast_tac 1);
-qed "pmap_owrI";
-
-(** map_app **)
-
-Goalw [TMap_def,map_app_def] 
-  "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a) \\<noteq>0";
-by (etac domainE 1);
-by (dtac imageI 1);
-by (Fast_tac 1);
-by (etac not_emptyI 1);
-qed "tmap_app_notempty";
-
-Goalw [TMap_def,map_app_def,domain_def] 
-  "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a):B";
-by (Fast_tac 1);
-qed "tmap_appI";
-
-Goalw [PMap_def]
-  "[| m \\<in> PMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a):B";
-by (ftac tmap_app_notempty 1); 
-by (assume_tac 1);
-by (dtac tmap_appI 1); 
-by (assume_tac 1);
-by (Fast_tac 1);
-qed "pmap_appI";
-
-(** domain **)
-
-Goalw [TMap_def]
-  "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> a \\<in> A";
-by (Fast_tac 1);
-qed "tmap_domainD";
-
-Goalw [PMap_def,TMap_def]
-  "[| m \\<in> PMap(A,B); a \\<in> domain(m) |] ==> a \\<in> A";
-by (Fast_tac 1);
-qed "pmap_domainD";
-
-(* ############################################################ *)
-(* Equalities                                                   *)
-(* ############################################################ *)
-
-(** Domain **)
-
-(* Lemmas *)
-
-Goal  "domain(\\<Union>x \\<in> A. B(x)) = (\\<Union>x \\<in> A. domain(B(x)))";
-by (Fast_tac 1);
-qed "domain_UN";
-
-Goal  "domain(Sigma(A,B)) = {x \\<in> A. \\<exists>y. y \\<in> B(x)}";
-by (simp_tac (simpset() addsimps [domain_UN,domain_0,domain_cons]) 1);
-by (Fast_tac 1);
-qed "domain_Sigma";
-
-(* Theorems *)
-
-Goalw [map_emp_def] "domain(map_emp) = 0";
-by (Fast_tac 1);
-qed "map_domain_emp";
-
-Goalw [map_owr_def] 
-  "b \\<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
-by (simp_tac (simpset() addsimps [domain_Sigma]) 1);
-by (rtac equalityI 1);
-by (Fast_tac 1);
-by (rtac subsetI 1);
-by (rtac CollectI 1);
-by (assume_tac 1);
-by (etac UnE' 1);
-by (etac singletonE 1);
-by (Asm_simp_tac 1);
-by (Fast_tac 1);
-by (fast_tac (claset() addss (simpset())) 1);
-qed "map_domain_owr";
-
-(** Application **)
-
-Goalw [map_app_def,map_owr_def] 
-  "map_app(map_owr(f,a,b),c) = (if c=a then b else map_app(f,c))";
-by (asm_simp_tac (simpset() addsimps [qbeta_if]) 1);
-by (Fast_tac 1);
-qed "map_app_owr";
-
-Goal "map_app(map_owr(f,a,b),a) = b";
-by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
-qed "map_app_owr1";
-
-Goal "c \\<noteq> a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
-by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
-qed "map_app_owr2";
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Map.thy	Tue Dec 25 10:02:01 2001 +0100
@@ -2,25 +2,185 @@
     ID:         $Id$
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
+
+
+Some sample proofs of inclusions for the final coalgebra "U" (by lcp) 
+
 *)
 
-Map = Main +
+theory Map = Main:
 
 constdefs
-  TMap :: [i,i] => i
-   "TMap(A,B) == {m \\<in> Pow(A*Union(B)).\\<forall>a \\<in> A. m``{a} \\<in> B}"
+  TMap :: "[i,i] => i"
+   "TMap(A,B) == {m \<in> Pow(A*Union(B)).\<forall>a \<in> A. m``{a} \<in> B}"
 
-  PMap :: [i,i] => i
+  PMap :: "[i,i] => i"
    "PMap(A,B) == TMap(A,cons(0,B))"
 
-(* Note: 0 \\<in> B ==> TMap(A,B) = PMap(A,B) *)
+(* Note: 0 \<in> B ==> TMap(A,B) = PMap(A,B) *)
   
   map_emp :: i
    "map_emp == 0"
 
-  map_owr :: [i,i,i]=>i
-   "map_owr(m,a,b) == \\<Sigma>x \\<in> {a} Un domain(m). if x=a then b else m``{x}"
-  map_app :: [i,i]=>i
+  map_owr :: "[i,i,i]=>i"
+   "map_owr(m,a,b) == \<Sigma>x \<in> {a} Un domain(m). if x=a then b else m``{x}"
+
+  map_app :: "[i,i]=>i"
    "map_app(m,a) == m``{a}"
   
+lemma "{0,1} \<subseteq> {1} Un TMap(I, {0,1})"
+by (unfold TMap_def, blast)
+
+lemma "{0} Un TMap(I,1) \<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))"
+by (unfold TMap_def, blast)
+
+lemma "{0,1} Un TMap(I,2) \<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))"
+by (unfold TMap_def, blast)
+
+(*A bit too slow.
+lemma "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \<subseteq>  
+       {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))"
+by (unfold TMap_def, blast)
+*)
+
+(* ############################################################ *)
+(* Lemmas                                                       *)
+(* ############################################################ *)
+
+lemma qbeta_if: "Sigma(A,B)``{a} = (if a \<in> A then B(a) else 0)"
+by auto
+
+lemma qbeta: "a \<in> A ==> Sigma(A,B)``{a} = B(a)"
+by fast
+
+lemma qbeta_emp: "a\<notin>A ==> Sigma(A,B)``{a} = 0"
+by fast
+
+lemma image_Sigma1: "a \<notin> A ==> Sigma(A,B)``{a}=0"
+by fast
+
+
+(* ############################################################ *)
+(* Inclusion in Quine Universes                                 *)
+(* ############################################################ *)
+
+(* Lemmas *)
+
+lemma MapQU_lemma: 
+    "A \<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \<subseteq> quniv(X)"
+apply (unfold quniv_def)
+apply (rule Pow_mono)
+apply (rule subset_trans [OF Sigma_mono product_univ])
+apply (erule subset_trans)
+apply (rule arg_subset_eclose [THEN univ_mono])
+apply (simp add: Union_Pow_eq)
+done
+
+(* Theorems *)
+
+lemma mapQU:
+  "[| m \<in> PMap(A,quniv(B)); !!x. x \<in> A ==> x \<in> univ(B) |] ==> m \<in> quniv(B)"
+apply (unfold PMap_def TMap_def)
+apply (blast intro!: MapQU_lemma [THEN subsetD]) 
+done
+
+(* ############################################################ *)
+(* Monotonicity                                                 *)
+(* ############################################################ *)
+
+lemma PMap_mono: "B \<subseteq> C ==> PMap(A,B)<=PMap(A,C)"
+by (unfold PMap_def TMap_def, blast)
+
+
+(* ############################################################ *)
+(* Introduction Rules                                           *)
+(* ############################################################ *)
+
+(** map_emp **)
+
+lemma pmap_empI: "map_emp \<in> PMap(A,B)"
+by (unfold map_emp_def PMap_def TMap_def, auto)
+
+(** map_owr **)
+
+lemma pmap_owrI: 
+  "[| m \<in> PMap(A,B); a \<in> A; b \<in> B |]  ==> map_owr(m,a,b):PMap(A,B)"
+apply (unfold map_owr_def PMap_def TMap_def)
+apply safe
+apply (simp_all add: if_iff)
+apply auto
+(*Remaining subgoal*)
+apply (rule excluded_middle [THEN disjE])
+apply (erule image_Sigma1)
+apply (drule_tac psi = "?uu \<notin> B" in asm_rl)
+apply (auto simp add: qbeta)
+done
+
+(** map_app **)
+
+lemma tmap_app_notempty: 
+  "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> map_app(m,a) \<noteq>0"
+by (unfold TMap_def map_app_def, blast)
+
+lemma tmap_appI: 
+  "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B"
+by (unfold TMap_def map_app_def domain_def, blast)
+
+lemma pmap_appI: 
+  "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B"
+apply (unfold PMap_def)
+apply (frule tmap_app_notempty, assumption)
+apply (drule tmap_appI)
+apply auto
+done
+
+(** domain **)
+
+lemma tmap_domainD: 
+  "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> a \<in> A"
+by (unfold TMap_def, blast)
+
+lemma pmap_domainD: 
+  "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> a \<in> A"
+by (unfold PMap_def TMap_def, blast)
+
+
+(* ############################################################ *)
+(* Equalities                                                   *)
+(* ############################################################ *)
+
+(** Domain **)
+
+(* Lemmas *)
+
+lemma domain_UN: "domain(\<Union>x \<in> A. B(x)) = (\<Union>x \<in> A. domain(B(x)))"
+by fast
+
+
+lemma domain_Sigma: "domain(Sigma(A,B)) = {x \<in> A. \<exists>y. y \<in> B(x)}"
+by blast
+
+(* Theorems *)
+
+lemma map_domain_emp: "domain(map_emp) = 0"
+by (unfold map_emp_def, blast)
+
+lemma map_domain_owr: 
+  "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"
+apply (unfold map_owr_def)
+apply (auto simp add: domain_Sigma)
+done
+
+(** Application **)
+
+lemma map_app_owr: 
+  "map_app(map_owr(f,a,b),c) = (if c=a then b else map_app(f,c))"
+by (simp add: qbeta_if  map_app_def map_owr_def, blast)
+
+lemma map_app_owr1: "map_app(map_owr(f,a,b),a) = b"
+by (simp add: map_app_owr)
+
+lemma map_app_owr2: "c \<noteq> a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)"
+by (simp add: map_app_owr)
+
 end
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/ROOT.ML
--- a/src/ZF/Coind/ROOT.ML	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/ROOT.ML	Tue Dec 25 10:02:01 2001 +0100
@@ -13,4 +13,4 @@
     Report, Computer Lab, University of Cambridge (1995).
 *)
 
-time_use_thy "MT";
+time_use_thy "ECR";
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/Static.ML
--- a/src/ZF/Coind/Static.ML	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      ZF/Coind/Static.ML
-    ID:         $Id$
-    Author:     Jacob Frost, Cambridge University Computer Laboratory
-    Copyright   1995  University of Cambridge
-*)
-
-val elab_constE	= ElabRel.mk_cases "<te,e_const(c),t>:ElabRel";
-
-val elab_varE 	= ElabRel.mk_cases "<te,e_var(x),t>:ElabRel";
-
-val elab_fnE 	= ElabRel.mk_cases "<te,e_fn(x,e),t>:ElabRel";
-
-val elab_fixE 	= ElabRel.mk_cases "<te,e_fix(f,x,e),t>:ElabRel";
-
-val elab_appE 	= ElabRel.mk_cases "<te,e_app(e1,e2),t>:ElabRel";
-
-AddSEs [elab_constE, elab_varE, elab_fixE];
-
-AddSIs [ElabRel.constI, ElabRel.varI, ElabRel.fnI, ElabRel.fixI];
-
-AddIs  [ElabRel.appI];
-
-AddEs [elab_appE, elab_fnE];
-
-AddDs [ElabRel.dom_subset RS subsetD];
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/Static.thy
--- a/src/ZF/Coind/Static.thy	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Static.thy	Tue Dec 25 10:02:01 2001 +0100
@@ -4,33 +4,63 @@
     Copyright   1995  University of Cambridge
 *)
 
-Static = BCR +
+theory Static = Values + Types:
+
+(*** Basic correspondence relation -- not completely specified, as it is a
+     parameter of the proof.  A concrete version could be defined inductively.
+***)
+
+consts
+  isof :: "[i,i] => o"
+
+axioms
+  isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
+
+(*Its extension to environments*)
+
+constdefs
+  isofenv :: "[i,i] => o"
+   "isofenv(ve,te) ==                
+      ve_dom(ve) = te_dom(te) &            
+      (\<forall>x \<in> ve_dom(ve).                          
+	\<exists>c \<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
+  
+
+(*** Elaboration ***)
 
 consts  ElabRel :: i
 
 inductive
   domains "ElabRel" <= "TyEnv * Exp * Ty"
-  intrs
-    constI
-      " [| te \\<in> TyEnv; c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==>   
-       <te,e_const(c),t>:ElabRel "
-    varI
-      " [| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==>   
-       <te,e_var(x),te_app(te,x)>:ElabRel "
-    fnI
-      " [| te \\<in> TyEnv; x \\<in> ExVar; e \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty;   
-          <te_owr(te,x,t1),e,t2>:ElabRel |] ==>   
-       <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
-    fixI
-      " [| te \\<in> TyEnv; f \\<in> ExVar; x \\<in> ExVar; t1 \\<in> Ty; t2 \\<in> Ty;   
-          <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>   
-       <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
-    appI
-      " [| te \\<in> TyEnv; e1 \\<in> Exp; e2 \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty;   
-          <te,e1,t_fun(t1,t2)>:ElabRel;   
-          <te,e2,t1>:ElabRel |] ==>   
-       <te,e_app(e1,e2),t2>:ElabRel "
-  type_intrs "te_appI::Exp.intrs@Ty.intrs"
+  intros
+    constI [intro!]:
+      "[| te \<in> TyEnv; c \<in> Const; t \<in> Ty; isof(c,t) |] ==>   
+       <te,e_const(c),t> \<in> ElabRel"
+    varI [intro!]:
+      "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==>   
+       <te,e_var(x),te_app(te,x)> \<in> ElabRel"
+    fnI [intro!]:
+      "[| te \<in> TyEnv; x \<in> ExVar; e \<in> Exp; t1 \<in> Ty; t2 \<in> Ty;   
+          <te_owr(te,x,t1),e,t2> \<in> ElabRel |] ==>   
+       <te,e_fn(x,e),t_fun(t1,t2)> \<in> ElabRel"
+    fixI [intro!]:
+      "[| te \<in> TyEnv; f \<in> ExVar; x \<in> ExVar; t1 \<in> Ty; t2 \<in> Ty;   
+          <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2> \<in> ElabRel |] ==>   
+       <te,e_fix(f,x,e),t_fun(t1,t2)> \<in> ElabRel"
+    appI [intro]:
+      "[| te \<in> TyEnv; e1 \<in> Exp; e2 \<in> Exp; t1 \<in> Ty; t2 \<in> Ty;   
+          <te,e1,t_fun(t1,t2)> \<in> ElabRel;   
+          <te,e2,t1> \<in> ElabRel |] ==> <te,e_app(e1,e2),t2> \<in> ElabRel"
+  type_intros te_appI Exp.intros Ty.intros
+
+
+inductive_cases elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel"
+inductive_cases elab_varE   [elim!]: "<te,e_var(x),t> \<in> ElabRel"
+inductive_cases elab_fnE    [elim]:  "<te,e_fn(x,e),t> \<in> ElabRel"
+inductive_cases elab_fixE   [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel"
+inductive_cases elab_appE   [elim]:  "<te,e_app(e1,e2),t> \<in> ElabRel"
+
+declare ElabRel.dom_subset [THEN subsetD, dest]
 
 end
   
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/Types.ML
--- a/src/ZF/Coind/Types.ML	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:      ZF/Coind/Types.ML
-    ID:         $Id$
-    Author:     Jacob Frost, Cambridge University Computer Laboratory
-    Copyright   1995  University of Cambridge
-*)
-
-val te_owrE = TyEnv.mk_cases "te_owr(te,f,t):TyEnv";
-
-Goal "te_app(te_owr(te,x,t),x) = t";
-by (Simp_tac 1);
-qed "te_app_owr1";
-
-Goal "x \\<noteq> y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
-by Auto_tac;
-qed "te_app_owr2";
-
-Goal "[| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==> te_app(te,x):Ty";
-by (res_inst_tac [("P","x \\<in> te_dom(te)")] impE 1);
-by (assume_tac 2);
-by (assume_tac 2);
-by (etac TyEnv.induct 1);
-by (Simp_tac 1);
-by (case_tac "xa = x" 1);
-by Auto_tac;
-qed "te_appI";
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/Types.thy
--- a/src/ZF/Coind/Types.thy	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Types.thy	Tue Dec 25 10:02:01 2001 +0100
@@ -4,15 +4,15 @@
     Copyright   1995  University of Cambridge
 *)
 
-Types = Language +
+theory Types = Language:
 
 consts
-  Ty :: i                       (* Datatype of types *)
+  Ty :: i               (* Datatype of types *)
   TyConst :: i          (* Abstract type of type constants *)
 
 datatype
-  "Ty" = t_const ("tc \\<in> TyConst")
-       | t_fun ("t1 \\<in> Ty","t2 \\<in> Ty")
+  "Ty" = t_const ("tc \<in> TyConst")
+       | t_fun ("t1 \<in> Ty","t2 \<in> Ty")
   
 
 (* Definition of type environments and associated operators *)
@@ -22,24 +22,57 @@
 
 datatype
   "TyEnv" = te_emp
-          | te_owr ("te \\<in> TyEnv","x \\<in> ExVar","t \\<in> Ty") 
+          | te_owr ("te \<in> TyEnv","x \<in> ExVar","t \<in> Ty") 
 
 consts
-  te_dom :: i => i
-  te_app :: [i,i] => i
+  te_dom :: "i => i"
+  te_app :: "[i,i] => i"
 
 
 primrec (*domain of the type environment*)
   "te_dom (te_emp) = 0"
-  "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}"
+  "te_dom (te_owr(te,x,v)) = te_dom(te) Un {x}"
 
 primrec (*lookup up identifiers in the type environment*)
   "te_app (te_emp,x) = 0"
   "te_app (te_owr(te,y,t),x) = (if x=y then t else te_app(te,x))"
 
-end
+inductive_cases te_owrE [elim!]: "te_owr(te,f,t) \<in> TyEnv"
+
+(*redundant??*)
+lemma te_app_owr1: "te_app(te_owr(te,x,t),x) = t"
+by simp
+
+(*redundant??*)
+lemma te_app_owr2: "x \<noteq> y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)"
+by auto
+
+lemma te_app_owr [simp]:
+     "te_app(te_owr(te,x,t),y) = (if x=y then t else te_app(te,y))"
+by auto
+
+lemma te_appI:
+     "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> te_app(te,x) \<in> Ty"
+apply (erule_tac P = "x \<in> te_dom (te) " in rev_mp)
+apply (erule TyEnv.induct)
+apply auto
+done
 
 
 
 
 
+
+
+
+
+
+
+
+
+
+
+
+
+
+end
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/Values.ML
--- a/src/ZF/Coind/Values.ML	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-(*  Title:      ZF/Coind/Values.ML
-    ID:         $Id$
-    Author:     Jacob Frost, Cambridge University Computer Laboratory
-    Copyright   1995  University of Cambridge
-*)
-
-open Values;
-
-(* Elimination rules *)
-
-val prems = goalw Values.thy (Part_def::(tl (tl Val_ValEnv.defs)))
-  "[| ve \\<in> ValEnv; !!m.[| ve=ve_mk(m); m \\<in> PMap(ExVar,Val) |] ==> Q |] ==> Q";
-by (cut_facts_tac prems 1);
-by (etac CollectE 1);
-by (etac exE 1);
-by (etac Val_ValEnv.elim 1);
-by (eresolve_tac prems 3);
-by (rewrite_tac Val_ValEnv.con_defs);
-by (ALLGOALS Fast_tac);
-qed "ValEnvE";
-
-val prems = goalw Values.thy (Part_def::[hd (tl Val_ValEnv.defs)])
-  "[| v \\<in> Val; \
-\     !!c. [| v = v_const(c); c \\<in> Const |] ==> Q;\
-\     !!e ve x. \
-\       [| v = v_clos(x,e,ve); x \\<in> ExVar; e \\<in> Exp; ve \\<in> ValEnv |] ==> Q \
-\  |] ==> \
-\  Q";
-by (cut_facts_tac prems 1);
-by (etac CollectE 1);
-by (etac exE 1);
-by (etac Val_ValEnv.elim 1);
-by (eresolve_tac prems 1);
-by (assume_tac 1);
-by (eresolve_tac prems 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (rewrite_tac Val_ValEnv.con_defs);
-by (Fast_tac 1);
-qed "ValE";
-
-(* Nonempty sets *)
-
-Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
-  "v_clos(x,e,ve) \\<noteq> 0";
-by (Blast_tac 1);
-qed "v_closNE";
-
-Addsimps [v_closNE];
-AddSEs [v_closNE RS notE];
-
-Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
-  "c \\<in> Const ==> v_const(c) \\<noteq> 0";
-by (dtac constNEE 1);
-by Auto_tac;
-qed "v_constNE";
-
-Addsimps [v_constNE];
-
-(* Proving that the empty set is not a value *)
-
-Goal "v \\<in> Val ==> v \\<noteq> 0";
-by (etac ValE 1);
-by Auto_tac;
-qed "ValNEE";
-
-(* Equalities for value environments *)
-
-Goal "[| ve \\<in> ValEnv; v \\<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
-by (etac ValEnvE 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [map_domain_owr]));
-qed "ve_dom_owr";
-
-Goal "ve \\<in> ValEnv \
-\     ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))"; 
-by (etac ValEnvE 1);
-by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
-qed "ve_app_owr";
-
-Goal "ve \\<in> ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v"; 
-by (etac ValEnvE 1);
-by (Asm_full_simp_tac 1);
-by (rtac map_app_owr1 1);
-qed "ve_app_owr1";
-
-Goal "ve \\<in> ValEnv ==> x \\<noteq> y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
-by (etac ValEnvE 1);
-by (Asm_full_simp_tac 1);
-by (rtac map_app_owr2 1);
-by (Fast_tac 1);
-qed "ve_app_owr2";
-
-(* Introduction rules for operators on value environments *)
-
-Goal "[| ve \\<in> ValEnv; x \\<in> ve_dom(ve) |] ==> ve_app(ve,x):Val";
-by (etac ValEnvE 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
-by (rtac pmap_appI 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "ve_appI";
-
-Goal "[| ve \\<in> ValEnv; x \\<in> ve_dom(ve) |] ==> x \\<in> ExVar";
-by (etac ValEnvE 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
-by (rtac pmap_domainD 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "ve_domI";
-
-Goalw [ve_emp_def] "ve_emp \\<in> ValEnv";
-by (rtac Val_ValEnv.ve_mk_I 1);
-by (rtac pmap_empI 1);
-qed "ve_empI";
-
-Goal "[|ve \\<in> ValEnv; x \\<in> ExVar; v \\<in> Val |] ==> ve_owr(ve,x,v):ValEnv";
-by (etac ValEnvE 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
-by (rtac Val_ValEnv.ve_mk_I 1);
-by (etac pmap_owrI 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "ve_owrI";
-
-
-
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Values.thy	Tue Dec 25 10:02:01 2001 +0100
@@ -4,25 +4,27 @@
     Copyright   1995  University of Cambridge
 *)
 
-Values = Language + Map +
+theory Values = Language + Map:
 
 (* Values, values environments and associated operators *)
 
 consts
-  Val, ValEnv, Val_ValEnv  :: i
+  Val  :: i
+  ValEnv  :: i
+  Val_ValEnv  :: i;
 
 codatatype
-    "Val" = v_const ("c \\<in> Const")
-          | v_clos ("x \\<in> ExVar","e \\<in> Exp","ve \\<in> ValEnv")
+    "Val" = v_const ("c \<in> Const")
+          | v_clos ("x \<in> ExVar","e \<in> Exp","ve \<in> ValEnv")
   and
-    "ValEnv" = ve_mk ("m \\<in> PMap(ExVar,Val)")
-  monos       map_mono
-  type_intrs  A_into_univ, mapQU
+    "ValEnv" = ve_mk ("m \<in> PMap(ExVar,Val)")
+  monos       PMap_mono
+  type_intros  A_into_univ mapQU
 
 consts
-  ve_owr :: [i,i,i] => i
-  ve_dom :: i=>i
-  ve_app :: [i,i] => i
+  ve_owr :: "[i,i,i] => i"
+  ve_dom :: "i=>i"
+  ve_app :: "[i,i] => i"
 
 
 primrec "ve_owr(ve_mk(m), x, v) = ve_mk(map_owr(m,x,v))"
@@ -35,7 +37,87 @@
   ve_emp :: i
    "ve_emp == ve_mk(map_emp)"
 
-end
+
+(* Elimination rules *)
+
+lemma ValEnvE:
+  "[| ve \<in> ValEnv; !!m.[| ve=ve_mk(m); m \<in> PMap(ExVar,Val) |] ==> Q |] ==> Q"
+apply (unfold Part_def Val_def ValEnv_def)
+apply (clarify ); 
+apply (erule Val_ValEnv.cases) 
+apply (auto simp add: Val_def Part_def Val_ValEnv.con_defs)
+done
+
+lemma ValE:
+  "[| v \<in> Val;  
+      !!c. [| v = v_const(c); c \<in> Const |] ==> Q; 
+      !!e ve x.  
+        [| v = v_clos(x,e,ve); x \<in> ExVar; e \<in> Exp; ve \<in> ValEnv |] ==> Q  
+   |] ==>  
+   Q"
+apply (unfold Part_def Val_def ValEnv_def)
+apply (clarify ); 
+apply (erule Val_ValEnv.cases) 
+apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs);
+done
+
+(* Nonempty sets *)
+
+lemma v_closNE [simp]: "v_clos(x,e,ve) \<noteq> 0"
+apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
+apply blast
+done
+
+declare v_closNE [THEN notE, elim!]
+
+
+lemma v_constNE [simp]: "c \<in> Const ==> v_const(c) \<noteq> 0"
+apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
+apply (drule constNEE)
+apply auto
+done
 
 
+(* Proving that the empty set is not a value *)
 
+lemma ValNEE: "v \<in> Val ==> v \<noteq> 0"
+by (erule ValE, auto)
+
+(* Equalities for value environments *)
+
+lemma ve_dom_owr [simp]:
+     "[| ve \<in> ValEnv; v \<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}"
+apply (erule ValEnvE)
+apply (auto simp add: map_domain_owr)
+done
+
+lemma ve_app_owr [simp]:
+     "ve \<in> ValEnv  
+      ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))"
+by (erule ValEnvE, simp add: map_app_owr)
+
+(* Introduction rules for operators on value environments *)
+
+lemma ve_appI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> ve_app(ve,x):Val"
+by (erule ValEnvE, simp add: pmap_appI) 
+
+lemma ve_domI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> x \<in> ExVar"
+apply (erule ValEnvE)
+apply (simp ); 
+apply (blast dest: pmap_domainD)
+done
+
+lemma ve_empI: "ve_emp \<in> ValEnv"
+apply (unfold ve_emp_def)
+apply (rule Val_ValEnv.intros)
+apply (rule pmap_empI)
+done
+
+lemma ve_owrI:
+     "[|ve \<in> ValEnv; x \<in> ExVar; v \<in> Val |] ==> ve_owr(ve,x,v):ValEnv"
+apply (erule ValEnvE)
+apply simp
+apply (blast intro: pmap_owrI Val_ValEnv.intros)
+done
+
+end
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/IsaMakefile	Tue Dec 25 10:02:01 2001 +0100
@@ -75,10 +75,8 @@
 ZF-Coind: ZF $(LOG)/ZF-Coind.gz
 
 $(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \
-  Coind/ECR.ML Coind/ECR.thy Coind/Language.thy Coind/MT.ML Coind/MT.thy \
-  Coind/Map.ML Coind/Map.thy Coind/ROOT.ML Coind/Static.ML \
-  Coind/Static.thy Coind/Types.ML Coind/Types.thy Coind/Values.ML \
-  Coind/Values.thy
+  Coind/ECR.thy Coind/Language.thy Coind/Map.thy Coind/ROOT.ML \
+  Coind/Static.thy Coind/Types.thy Coind/Values.thy
 	@$(ISATOOL) usedir $(OUT)/ZF Coind
 
 
@@ -95,9 +93,9 @@
 
 ZF-Resid: ZF $(LOG)/ZF-Resid.gz
 
-$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy \
-  Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy \
-  Resid/Substitution.thy 
+$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML \
+  Resid/Confluence.thy  Resid/Redex.thy \
+  Resid/Reduction.thy Resid/Residuals.thy Resid/Substitution.thy 
 	@$(ISATOOL) usedir $(OUT)/ZF Resid
 
 
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Resid/Conversion.thy
--- a/src/ZF/Resid/Conversion.thy	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      Conversion.thy
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-
-*)
-
-Conversion = Confluence+
-
-consts
-  Sconv1        :: i
-  "<-1->"       :: [i,i]=>o (infixl 50)
-  Sconv         :: i
-  "<--->"       :: [i,i]=>o (infixl 50)
-
-translations
-  "a<-1->b"    == "<a,b>:Sconv1"
-  "a<--->b"    == "<a,b>:Sconv"
-  
-inductive
-  domains       "Sconv1" <= "lambda*lambda"
-  intrs
-    red1        "m -1-> n ==> m<-1->n"
-    expl        "n -1-> m ==> m<-1->n"
-  type_intrs    "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
-
-inductive
-  domains       "Sconv" <= "lambda*lambda"
-  intrs
-    one_step    "m<-1->n  ==> m<--->n"
-    refl        "m \\<in> lambda ==> m<--->m"
-    trans       "[|m<--->n; n<--->p|] ==> m<--->p"
-  type_intrs    "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
-end
-
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Resid/Cube.thy
--- a/src/ZF/Resid/Cube.thy	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(*  Title:      Cube.thy
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-*)
-
-Cube = Residuals
diff -r 5b9b0adca8aa -r 0480d02221b8 src/ZF/Resid/Terms.thy
--- a/src/ZF/Resid/Terms.thy	Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title:      Terms.thy
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-*)
-
-Terms = Cube+
-
-consts
-  lambda        :: i
-  unmark        :: i=>i
-  Apl           :: [i,i]=>i
-
-translations
-  "Apl(n,m)" == "App(0,n,m)"
-  
-inductive
-  domains       "lambda" <= "redexes"
-  intrs
-    Lambda_Var  "               n \\<in> nat ==>     Var(n):lambda"
-    Lambda_Fun  "            u \\<in> lambda ==>     Fun(u):lambda"
-    Lambda_App  "[|u \\<in> lambda; v \\<in> lambda|]==> Apl(u,v):lambda"
-  type_intrs    "redexes.intrs@bool_typechecks"
-
-primrec
-  "unmark(Var(n)) = Var(n)"
-  "unmark(Fun(u)) = Fun(unmark(u))"
-  "unmark(App(b,f,a)) = Apl(unmark(f), unmark(a))"
-
-end
-
-