# HG changeset patch
# User paulson
# Date 1009046555 -3600
# Node ID cd35fe5947d41e13cdad100c2c258546e1d34e44
# Parent  0eb1685a00b467ce1e909cfbce05dfa984ced67c
Resid converted to Isar/ZF

diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/IsaMakefile	Sat Dec 22 19:42:35 2001 +0100
@@ -95,12 +95,9 @@
 
 ZF-Resid: ZF $(LOG)/ZF-Resid.gz
 
-$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \
-  Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
-  Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
-  Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
-  Resid/Substitution.ML \
-  Resid/Substitution.thy Resid/Terms.ML Resid/Terms.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 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Confluence.ML
--- a/src/ZF/Resid/Confluence.ML	Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(*  Title:      Confluence.ML
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-*)
-
-open Confluence;
-
-(* ------------------------------------------------------------------------- *)
-(*        strip lemmas                                                       *)
-(* ------------------------------------------------------------------------- *)
-
-Goalw [confluence_def,strip_def] 
-    "[|confluence(Spar_red1)|]==> strip";
-by (resolve_tac [impI RS allI RS allI] 1);
-by (etac Spar_red.induct 1);
-by (Fast_tac  1);
-by (fast_tac (claset() addIs [Spar_red.trans]) 1);
-qed "strip_lemma_r";
-
-
-Goalw [confluence_def,strip_def] 
-    "strip==> confluence(Spar_red)";
-by (resolve_tac [impI RS allI RS allI] 1);
-by (etac Spar_red.induct 1);
-by (Blast_tac 1);
-by (Clarify_tac 1);
-by (dres_inst_tac [("x1","z")] (spec RS mp) 1);
-by (blast_tac (claset() addIs [Spar_red.trans]) 2);
-by (assume_tac 1);
-qed "strip_lemma_l";
-
-(* ------------------------------------------------------------------------- *)
-(*      Confluence                                                           *)
-(* ------------------------------------------------------------------------- *)
-
-
-Goalw [confluence_def] "confluence(Spar_red1)";
-by (Clarify_tac 1);
-by (ftac simulation 1);
-by (forw_inst_tac [("n","z")] simulation 1);
-by (Clarify_tac 1);
-by (forw_inst_tac [("v","va")] paving 1);
-by (TRYALL assume_tac);
-by (fast_tac (claset() addIs [completeness] addss (simpset())) 1);
-qed "parallel_moves";
-
-bind_thm ("confluence_parallel_reduction",
-	  parallel_moves RS strip_lemma_r RS strip_lemma_l);
-
-Goalw [confluence_def] 
-    "[|confluence(Spar_red)|]==> confluence(Sred)";
-by (blast_tac (claset() addIs [par_red_red, red_par_red]) 1);
-val lemma1 = result();
-
-bind_thm ("confluence_beta_reduction",
-	  confluence_parallel_reduction RS lemma1);
-
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Confluence.thy
--- a/src/ZF/Resid/Confluence.thy	Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/Confluence.thy	Sat Dec 22 19:42:35 2001 +0100
@@ -5,17 +5,119 @@
     Logic Image: ZF
 *)
 
-Confluence = Reduction+
+theory Confluence = Reduction:
+
+constdefs
+  confluence    :: "i=>o"
+    "confluence(R) ==   
+       \<forall>x y. <x,y> \<in> R --> (\<forall>z.<x,z> \<in> R --> (\<exists>u.<y,u> \<in> R & <z,u> \<in> R))"
+
+  strip         :: "o"
+    "strip == \<forall>x y. (x ===> y) --> 
+                    (\<forall>z.(x =1=> z) --> (\<exists>u.(y =1=> u) & (z===>u)))" 
+
+
+(* ------------------------------------------------------------------------- *)
+(*        strip lemmas                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+lemma strip_lemma_r: 
+    "[|confluence(Spar_red1)|]==> strip"
+apply (unfold confluence_def strip_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule Spar_red.induct)
+apply fast
+apply (fast intro: Spar_red.trans)
+done
+
+
+lemma strip_lemma_l: 
+    "strip==> confluence(Spar_red)"
+apply (unfold confluence_def strip_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule Spar_red.induct)
+apply blast
+apply clarify
+apply (blast intro: Spar_red.trans)
+done
+
+(* ------------------------------------------------------------------------- *)
+(*      Confluence                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+
+lemma parallel_moves: "confluence(Spar_red1)"
+apply (unfold confluence_def)
+apply clarify
+apply (frule simulation)
+apply (frule_tac n = "z" in simulation)
+apply clarify
+apply (frule_tac v = "va" in paving)
+apply (force intro: completeness)+
+done
+
+lemmas confluence_parallel_reduction =
+      parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard]
+
+lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)"
+apply (unfold confluence_def, blast intro: par_red_red red_par_red)
+done
+
+lemmas confluence_beta_reduction =
+       confluence_parallel_reduction [THEN lemma1, standard]
+
+
+(**** Conversion ****)
 
 consts
-  confluence    :: i=>o
-  strip         :: o
+  Sconv1        :: "i"
+  "<-1->"       :: "[i,i]=>o"   (infixl 50)
+  Sconv         :: "i"
+  "<--->"       :: "[i,i]=>o"   (infixl 50)
+
+translations
+  "a<-1->b"    == "<a,b> \<in> Sconv1"
+  "a<--->b"    == "<a,b> \<in> Sconv"
+  
+inductive
+  domains       "Sconv1" <= "lambda*lambda"
+  intros
+    red1:        "m -1-> n ==> m<-1->n"
+    expl:        "n -1-> m ==> m<-1->n"
+  type_intros    red1D1 red1D2 lambda.intros bool_typechecks
+
+declare Sconv1.intros [intro]
 
-defs
-  confluence_def "confluence(R) ==   
-                  \\<forall>x y. <x,y>:R --> (\\<forall>z.<x,z>:R -->   
-                                         (\\<exists>u.<y,u>:R & <z,u>:R))"
-  strip_def      "strip == \\<forall>x y. (x ===> y) --> (\\<forall>z.(x =1=> z) -->   
-                                         (\\<exists>u.(y =1=> u) & (z===>u)))" 
+inductive
+  domains       "Sconv" <= "lambda*lambda"
+  intros
+    one_step:    "m<-1->n  ==> m<--->n"
+    refl:        "m \<in> lambda ==> m<--->m"
+    trans:       "[|m<--->n; n<--->p|] ==> m<--->p"
+  type_intros    Sconv1.dom_subset [THEN subsetD] lambda.intros bool_typechecks
+
+declare Sconv.intros [intro]
+
+lemma conv_sym: "m<--->n ==> n<--->m"
+apply (erule Sconv.induct)
+apply (erule Sconv1.induct)
+apply blast+
+done
+
+(* ------------------------------------------------------------------------- *)
+(*      Church_Rosser Theorem                                                *)
+(* ------------------------------------------------------------------------- *)
+
+lemma Church_Rosser: "m<--->n ==> \<exists>p.(m --->p) & (n ---> p)"
+apply (erule Sconv.induct)
+apply (erule Sconv1.induct)
+apply (blast intro: red1D1 redD2)
+apply (blast intro: red1D1 redD2)
+apply (blast intro: red1D1 redD2)
+apply (cut_tac confluence_beta_reduction)
+apply (unfold confluence_def)
+apply (blast intro: Sred.trans)
+done
+
 end
 
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Conversion.ML
--- a/src/ZF/Resid/Conversion.ML	Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(*  Title:      Conversion.ML
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-*)
-
-open Conversion;
-
-AddIs (Sconv.intrs @ Sconv1.intrs);
-
-Goal "m<--->n ==> n<--->m";
-by (etac Sconv.induct 1);
-by (etac Sconv1.induct 1);
-by (ALLGOALS Blast_tac);
-qed "conv_sym";
-
-(* ------------------------------------------------------------------------- *)
-(*      Church_Rosser Theorem                                                *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "m<--->n ==> \\<exists>p.(m --->p) & (n ---> p)";
-by (etac Sconv.induct 1);
-by (etac Sconv1.induct 1);
-by (blast_tac (claset() addIs [red1D1,redD2]) 1);
-by (blast_tac (claset() addIs [red1D1,redD2]) 1);
-by (blast_tac (claset() addIs [red1D1,redD2]) 1);
-by (cut_facts_tac [confluence_beta_reduction]  1);
-by (rewtac confluence_def);
-by (blast_tac (claset() addIs [Sred.trans]) 1);
-qed "Church_Rosser";
-
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Cube.ML
--- a/src/ZF/Resid/Cube.ML	Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(*  Title:      Cube.ML
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-*)
-
-Addsimps [commutation, residuals_preserve_comp, sub_preserve_reg,
-	  residuals_preserve_reg, sub_comp, sub_comp RS comp_sym];
-
-(* ------------------------------------------------------------------------- *)
-(*         Prism theorem                                                     *)
-(*         =============                                                     *)
-(* ------------------------------------------------------------------------- *)
-
-(* Having more assumptions than needed -- removed below  *)
-Goal "v<==u ==> \
-\   regular(u) --> (\\<forall>w. w~v --> w~u -->  \
-\                          w |> u = (w|>v) |> (u|>v))";
-by (etac Ssub.induct 1);
-by Auto_tac;
-qed_spec_mp "prism_l";
-
-Goal "[|v <== u; regular(u); w~v|]==> \
-\       w |> u = (w|>v) |> (u|>v)";
-by (rtac prism_l 1);
-by (rtac comp_trans 4);
-by Auto_tac;
-qed "prism";
-
-
-(* ------------------------------------------------------------------------- *)
-(*    Levy's Cube Lemma                                                      *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "[|u~v; regular(v); regular(u); w~u|]==>  \
-\          (w|>u) |> (v|>u) = (w|>v) |> (u|>v)";
-by (stac preservation 1 
-    THEN assume_tac 1 THEN assume_tac 1);
-by (stac preservation 1 
-    THEN etac comp_sym 1 THEN assume_tac 1);
-by (stac (prism RS sym) 1);
-by (asm_full_simp_tac (simpset() addsimps 
-		       [prism RS sym,union_l,union_preserve_regular,
-			comp_sym_iff, union_sym]) 4);
-by (asm_simp_tac (simpset() addsimps [union_r, comp_sym_iff]) 1);
-by (asm_simp_tac (simpset() addsimps 
-		  [union_preserve_regular, comp_sym_iff]) 1);
-by (etac comp_trans 1);
-by (atac 1);
-qed "cube";
-
-
-(* ------------------------------------------------------------------------- *)
-(*           paving theorem                                                  *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "[|w~u; w~v; regular(u); regular(v)|]==> \
-\          \\<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
-\            regular(vu) & (w|>v)~uv & regular(uv) ";
-by (subgoal_tac "u~v" 1);
-by (safe_tac (claset() addSIs [exI]));
-by (rtac cube 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [comp_sym_iff])));
-by (ALLGOALS (blast_tac (claset() addIs [residuals_preserve_comp, 
-					comp_trans, comp_sym])));
-qed "paving";
-
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/ROOT.ML
--- a/src/ZF/Resid/ROOT.ML	Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/ROOT.ML	Sat Dec 22 19:42:35 2001 +0100
@@ -12,4 +12,4 @@
 J. Functional Programming 4(3) 1994, 371-394.
 *)
 
-time_use_thy "Conversion";
+time_use_thy "Confluence";
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Redex.ML
--- a/src/ZF/Resid/Redex.ML	Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(*  Title:      Redex.ML
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-*)
-
-Addsimps redexes.intrs;
-
-fun rotate n i = EVERY(replicate n (etac revcut_rl i));    
-(* ------------------------------------------------------------------------- *)
-(*    Specialisation of comp-rules                                           *)
-(* ------------------------------------------------------------------------- *)
-
-val compD1 = Scomp.dom_subset RS subsetD RS SigmaD1;
-val compD2 = Scomp.dom_subset RS subsetD RS SigmaD2;
-
-val regD = Sreg.dom_subset RS subsetD;
-
-(* ------------------------------------------------------------------------- *)
-(*    Equality rules for union                                               *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "n \\<in> nat==>Var(n) un Var(n)=Var(n)";
-by (asm_simp_tac (simpset() addsimps [union_def]) 1);
-qed "union_Var";
-
-Goal "[|u \\<in> redexes; v \\<in> redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
-by (asm_simp_tac (simpset() addsimps [union_def]) 1);
-qed "union_Fun";
- 
-Goal "[|b1 \\<in> bool; b2 \\<in> bool; u1 \\<in> redexes; v1 \\<in> redexes; u2 \\<in> redexes; v2 \\<in> redexes|]==> \
-\     App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
-by (asm_simp_tac (simpset() addsimps [union_def]) 1);
-qed "union_App";
-
-Addsimps (Ssub.intrs@bool_typechecks@
-	  Sreg.intrs@Scomp.intrs@
-	  [or_1 RSN (3,or_commute RS trans),
-	   or_0 RSN (3,or_commute RS trans),
-	   union_App,union_Fun,union_Var,compD2,compD1,regD]);
-
-AddIs Scomp.intrs;
-AddSEs [Sreg.mk_cases "regular(App(b,f,a))",
-	Sreg.mk_cases "regular(Fun(b))",
-	Sreg.mk_cases "regular(Var(b))",
-	Scomp.mk_cases "Fun(u) ~ Fun(t)",
-	Scomp.mk_cases "u ~ Fun(t)",
-	Scomp.mk_cases "u ~ Var(n)",
-	Scomp.mk_cases "u ~ App(b,t,a)",
-	Scomp.mk_cases "Fun(t) ~ v",
-	Scomp.mk_cases "App(b,f,a) ~ v",
-	Scomp.mk_cases "Var(n) ~ u"];
-
-
-
-(* ------------------------------------------------------------------------- *)
-(*    comp proofs                                                            *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u \\<in> redexes ==> u ~ u";
-by (etac redexes.induct 1);
-by (ALLGOALS Fast_tac);
-qed "comp_refl";
-
-Goal "u ~ v ==> v ~ u";
-by (etac Scomp.induct 1);
-by (ALLGOALS Fast_tac);
-qed "comp_sym";
-
-Goal "u ~ v <-> v ~ u";
-by (fast_tac (claset() addIs [comp_sym]) 1);
-qed "comp_sym_iff";
-
-
-Goal "u ~ v ==> \\<forall>w. v ~ w-->u ~ w";
-by (etac Scomp.induct 1);
-by (ALLGOALS Fast_tac);
-qed_spec_mp "comp_trans";
-
-(* ------------------------------------------------------------------------- *)
-(*   union proofs                                                            *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u ~ v ==> u <== (u un v)";
-by (etac Scomp.induct 1);
-by (etac boolE 3);
-by (ALLGOALS Asm_simp_tac);
-qed "union_l";
-
-Goal "u ~ v ==> v <== (u un v)";
-by (etac Scomp.induct 1);
-by (eres_inst_tac [("c","b2")] boolE 3);
-by (ALLGOALS Asm_simp_tac);
-qed "union_r";
-
-Goal "u ~ v ==> u un v = v un u";
-by (etac Scomp.induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [or_commute])));
-qed "union_sym";
-
-(* ------------------------------------------------------------------------- *)
-(*      regular proofs                                                       *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
-by (etac Scomp.induct 1);
-by Auto_tac;
-by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
-by (Asm_full_simp_tac 1);
-qed_spec_mp "union_preserve_regular";
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/Redex.thy	Sat Dec 22 19:42:35 2001 +0100
@@ -5,77 +5,186 @@
     Logic Image: ZF
 *)
 
-Redex = Main +
+theory Redex = Main:
 consts
   redexes     :: i
 
 datatype
-  "redexes" = Var ("n \\<in> nat")            
-            | Fun ("t \\<in> redexes")
-            | App ("b \\<in> bool" ,"f \\<in> redexes" , "a \\<in> redexes")
+  "redexes" = Var ("n \<in> nat")            
+            | Fun ("t \<in> redexes")
+            | App ("b \<in> bool" ,"f \<in> redexes" , "a \<in> redexes")
 
 
 consts
-  Ssub,Scomp,Sreg  :: i
-  "<==","~"        :: [i,i]=>o (infixl 70)
-  un               :: [i,i]=>i (infixl 70)
-  union_aux        :: i=>i
-  regular          :: i=>o
+  Ssub  :: "i"
+  Scomp :: "i"
+  Sreg  :: "i"
+  union_aux        :: "i=>i"
+  regular          :: "i=>o"
   
+(*syntax??*)
+  un               :: "[i,i]=>i"  (infixl 70)
+  "<=="            :: "[i,i]=>o"  (infixl 70)
+  "~"              :: "[i,i]=>o"  (infixl 70)
+
+
 translations
-  "a<==b"        == "<a,b>:Ssub"
-  "a ~ b"        == "<a,b>:Scomp"
-  "regular(a)"   == "a \\<in> Sreg"
+  "a<==b"        == "<a,b> \<in> Ssub"
+  "a ~ b"        == "<a,b> \<in> Scomp"
+  "regular(a)"   == "a \<in> Sreg"
 
 
 primrec (*explicit lambda is required because both arguments of "un" vary*)
   "union_aux(Var(n)) =
-     (\\<lambda>t \\<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
+     (\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
 
   "union_aux(Fun(u)) =
-     (\\<lambda>t \\<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
+     (\<lambda>t \<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
 	 			  %b y z. 0, t))"
 
   "union_aux(App(b,f,a)) =
-     (\\<lambda>t \\<in> redexes.
+     (\<lambda>t \<in> redexes.
         redexes_case(%j. 0, %y. 0,
 		     %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
 
 defs
-  union_def  "u un v == union_aux(u)`v"
+  union_def:  "u un v == union_aux(u)`v"
 
+syntax (xsymbols)
+  "op un"             :: "[i,i]=>i"  (infixl "\<squnion>" 70)
+  "op <=="            :: "[i,i]=>o"  (infixl "\<Longleftarrow>" 70)
+  "op ~"              :: "[i,i]=>o"  (infixl "\<sim>" 70)
 
 inductive
   domains       "Ssub" <= "redexes*redexes"
-  intrs
-    Sub_Var     "n \\<in> nat ==> Var(n)<== Var(n)"
-    Sub_Fun     "[|u<== v|]==> Fun(u)<== Fun(v)"
-    Sub_App1    "[|u1<== v1; u2<== v2; b \\<in> bool|]==>   
+  intros
+    Sub_Var:     "n \<in> nat ==> Var(n)<== Var(n)"
+    Sub_Fun:     "[|u<== v|]==> Fun(u)<== Fun(v)"
+    Sub_App1:    "[|u1<== v1; u2<== v2; b \<in> bool|]==>   
                      App(0,u1,u2)<== App(b,v1,v2)"
-    Sub_App2    "[|u1<== v1; u2<== v2|]==>   
-                     App(1,u1,u2)<== App(1,v1,v2)"
-  type_intrs    "redexes.intrs@bool_typechecks"
+    Sub_App2:    "[|u1<== v1; u2<== v2|]==> App(1,u1,u2)<== App(1,v1,v2)"
+  type_intros    redexes.intros bool_typechecks
 
 inductive
   domains       "Scomp" <= "redexes*redexes"
-  intrs
-    Comp_Var    "n \\<in> nat ==> Var(n) ~ Var(n)"
-    Comp_Fun    "[|u ~ v|]==> Fun(u) ~ Fun(v)"
-    Comp_App    "[|u1 ~ v1; u2 ~ v2; b1 \\<in> bool; b2 \\<in> bool|]==>   
-                     App(b1,u1,u2) ~ App(b2,v1,v2)"
-  type_intrs    "redexes.intrs@bool_typechecks"
+  intros
+    Comp_Var:    "n \<in> nat ==> Var(n) ~ Var(n)"
+    Comp_Fun:    "[|u ~ v|]==> Fun(u) ~ Fun(v)"
+    Comp_App:    "[|u1 ~ v1; u2 ~ v2; b1 \<in> bool; b2 \<in> bool|]
+                  ==> App(b1,u1,u2) ~ App(b2,v1,v2)"
+  type_intros    redexes.intros bool_typechecks
 
 inductive
   domains       "Sreg" <= "redexes"
-  intrs
-    Reg_Var     "n \\<in> nat ==> regular(Var(n))"
-    Reg_Fun     "[|regular(u)|]==> regular(Fun(u))"
-    Reg_App1    "[|regular(Fun(u)); regular(v) 
-                     |]==>regular(App(1,Fun(u),v))"
-    Reg_App2    "[|regular(u); regular(v) 
-                     |]==>regular(App(0,u,v))"
-  type_intrs    "redexes.intrs@bool_typechecks"
+  intros
+    Reg_Var:     "n \<in> nat ==> regular(Var(n))"
+    Reg_Fun:     "[|regular(u)|]==> regular(Fun(u))"
+    Reg_App1:    "[|regular(Fun(u)); regular(v) |]==>regular(App(1,Fun(u),v))"
+    Reg_App2:    "[|regular(u); regular(v) |]==>regular(App(0,u,v))"
+  type_intros    redexes.intros bool_typechecks
+
+
+declare redexes.intros [simp]
+
+(* ------------------------------------------------------------------------- *)
+(*    Specialisation of comp-rules                                           *)
+(* ------------------------------------------------------------------------- *)
+
+lemmas compD1 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas compD2 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD2]
+lemmas regD [simp] = Sreg.dom_subset [THEN subsetD]
+
+(* ------------------------------------------------------------------------- *)
+(*    Equality rules for union                                               *)
+(* ------------------------------------------------------------------------- *)
+
+lemma union_Var [simp]: "n \<in> nat ==> Var(n) un Var(n)=Var(n)"
+by (simp add: union_def)
+
+lemma union_Fun [simp]: "v \<in> redexes ==> Fun(u) un Fun(v) = Fun(u un v)"
+by (simp add: union_def)
+ 
+lemma union_App [simp]:
+     "[|b2 \<in> bool; u2 \<in> redexes; v2 \<in> redexes|]
+      ==> App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)"
+by (simp add: union_def)
+
+
+lemma or_1_right [simp]: "a or 1 = 1"
+by (simp add: or_def cond_def) 
+
+lemma or_0_right [simp]: "a \<in> bool \<Longrightarrow> a or 0 = a"
+by (simp add: or_def cond_def bool_def, auto) 
+
+
+
+declare Ssub.intros [simp]
+declare bool_typechecks [simp]
+declare Sreg.intros [simp]
+declare Scomp.intros [simp]
+
+declare Scomp.intros [intro]
 
+inductive_cases [elim!]: "regular(App(b,f,a))"
+inductive_cases [elim!]: "regular(Fun(b))"
+inductive_cases [elim!]: "regular(Var(b))"
+inductive_cases [elim!]: "Fun(u) ~ Fun(t)"
+inductive_cases [elim!]: "u ~ Fun(t)"
+inductive_cases [elim!]: "u ~ Var(n)"
+inductive_cases [elim!]: "u ~ App(b,t,a)"
+inductive_cases [elim!]: "Fun(t) ~ v"
+inductive_cases [elim!]: "App(b,f,a) ~ v"
+inductive_cases [elim!]: "Var(n) ~ u"
+
+
+
+(* ------------------------------------------------------------------------- *)
+(*    comp proofs                                                            *)
+(* ------------------------------------------------------------------------- *)
+
+lemma comp_refl [simp]: "u \<in> redexes ==> u ~ u"
+by (erule redexes.induct, blast+)
+
+lemma comp_sym: "u ~ v ==> v ~ u"
+by (erule Scomp.induct, blast+)
+
+lemma comp_sym_iff: "u ~ v <-> v ~ u"
+by (blast intro: comp_sym)
+
+lemma comp_trans [rule_format]: "u ~ v ==> \<forall>w. v ~ w-->u ~ w"
+by (erule Scomp.induct, blast+)
+
+(* ------------------------------------------------------------------------- *)
+(*   union proofs                                                            *)
+(* ------------------------------------------------------------------------- *)
+
+lemma union_l: "u ~ v ==> u <== (u un v)"
+apply (erule Scomp.induct)
+apply (erule_tac [3] boolE)
+apply simp_all
+done
+
+lemma union_r: "u ~ v ==> v <== (u un v)"
+apply (erule Scomp.induct)
+apply (erule_tac [3] c = "b2" in boolE)
+apply simp_all
+done
+
+lemma union_sym: "u ~ v ==> u un v = v un u"
+by (erule Scomp.induct, simp_all add: or_commute)
+
+(* ------------------------------------------------------------------------- *)
+(*      regular proofs                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+lemma union_preserve_regular [rule_format]:
+     "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"
+apply (erule Scomp.induct)
+apply auto
+(*select the given assumption for simplification*)
+apply (erule_tac P = "regular (Fun (?u) un ?v) " in rev_mp)
+apply simp
+done
 
 end
 
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Reduction.ML
--- a/src/ZF/Resid/Reduction.ML	Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(*  Title:      Reduction.ML
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-*)
-
-(* ------------------------------------------------------------------------- *)
-(*     Setting up rulelists for reduction                                    *)
-(* ------------------------------------------------------------------------- *)
-
-val red1D1     = Sred1.dom_subset RS subsetD RS SigmaD1;
-val red1D2     = Sred1.dom_subset RS subsetD RS SigmaD2;
-val redD1      = Sred.dom_subset RS subsetD RS SigmaD1;
-val redD2      = Sred.dom_subset RS subsetD RS SigmaD2;
-val par_red1D1 = Spar_red1.dom_subset RS subsetD RS SigmaD1;
-val par_red1D2 = Spar_red1.dom_subset RS subsetD RS SigmaD2;
-val par_redD1  = Spar_red.dom_subset RS subsetD RS SigmaD1;
-val par_redD2  = Spar_red.dom_subset RS subsetD RS SigmaD2;
-
-
-AddIs (Sred1.intrs@[Sred.one_step, Sred.refl]@Spar_red1.intrs@
-       [Spar_red.one_step, lambda.dom_subset RS subsetD,
-	unmark_type]@lambda.intrs@bool_typechecks);
-AddSEs [Spar_red1.mk_cases "Fun(t) =1=> Fun(u)"];
-
-Addsimps (Sred1.intrs@[Sred.one_step, Sred.refl]@Spar_red1.intrs@
-	  [Spar_red.one_step, substL_type, redD1, redD2, par_redD1, 
-	   par_redD2, par_red1D2, unmark_type]);
-
-
-(* ------------------------------------------------------------------------- *)
-(*     Lemmas for reduction                                                  *)
-(* ------------------------------------------------------------------------- *)
-
-Goal  "m--->n ==> Fun(m) ---> Fun(n)";
-by (etac Sred.induct 1);
-by (resolve_tac [Sred.trans] 3);
-by (ALLGOALS (Asm_simp_tac ));
-qed "red_Fun";
-
-Goal "[|n \\<in> lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)";
-by (etac Sred.induct 1);
-by (resolve_tac [Sred.trans] 3);
-by (ALLGOALS (Asm_simp_tac ));
-qed "red_Apll";
-
-Goal "[|n \\<in> lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')";
-by (etac Sred.induct 1);
-by (resolve_tac [Sred.trans] 3);
-by (ALLGOALS (Asm_simp_tac ));
-qed "red_Aplr";
-
-Goal "[|m ---> m'; n--->n'|]==> Apl(m,n)--->Apl(m',n')";
-by (res_inst_tac [("n","Apl(m',n)")] Sred.trans 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apll,red_Aplr]) ));
-qed "red_Apl";
-
-Goal "[|m \\<in> lambda; m':lambda; n \\<in> lambda; n':lambda; m ---> m'; n--->n'|]==> \
-\              Apl(Fun(m),n)---> n'/m'";
-by (res_inst_tac [("n","Apl(Fun(m'),n')")] Sred.trans 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apl,red_Fun]) ));
-qed "red_beta";
-
-
-(* ------------------------------------------------------------------------- *)
-(*      Lemmas for parallel reduction                                        *)
-(* ------------------------------------------------------------------------- *)
-
-
-Goal "m \\<in> lambda==> m =1=> m";
-by (etac lambda.induct 1);
-by (ALLGOALS (Asm_simp_tac ));
-qed "refl_par_red1";
-
-Goal "m-1->n ==> m=1=>n";
-by (etac Sred1.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [refl_par_red1]) ));
-qed "red1_par_red1";
-
-Goal "m--->n ==> m===>n";
-by (etac Sred.induct 1);
-by (resolve_tac [Spar_red.trans] 3);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [refl_par_red1,red1_par_red1]) ));
-qed "red_par_red";
-
-Goal "m===>n ==> m--->n";
-by (etac Spar_red.induct 1);
-by (etac Spar_red1.induct 1);
-by (resolve_tac [Sred.trans] 5);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Fun,red_beta,red_Apl]) ));
-qed "par_red_red";
-
-
-(* ------------------------------------------------------------------------- *)
-(*      Simulation                                                           *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "m=1=>n ==> \\<exists>v. m|>v = n & m~v & regular(v)";
-by (etac Spar_red1.induct 1);
-by Safe_tac;
-by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI])));
-by (TRYALL(resolve_tac [res_redex,res_App,res_Fun,res_Var]));
-by (ALLGOALS (asm_simp_tac (simpset())));
-qed "simulation";
-
-
-(* ------------------------------------------------------------------------- *)
-(*           commuting of unmark and subst                                   *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
-by (etac redexes.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
-qed "unmmark_lift_rec";
-
-Goal "v \\<in> redexes ==> \\<forall>k \\<in> nat. \\<forall>u \\<in> redexes.  \
-\         unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)";
-by (etac redexes.induct 1);
-by (ALLGOALS (asm_simp_tac 
-	      (simpset() addsimps [unmmark_lift_rec, subst_Var])));
-qed "unmmark_subst_rec";
-
-
-(* ------------------------------------------------------------------------- *)
-(*        Completeness                                                       *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)";
-by (etac Scomp.induct 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [unmmark_subst_rec]));
-by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1);
-by Auto_tac;
-qed_spec_mp "completeness_l";
-
-Goal "[|u \\<in> lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)";
-by (dtac completeness_l 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lambda_unmark]) ));
-qed "completeness";
-
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Reduction.thy
--- a/src/ZF/Resid/Reduction.thy	Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/Reduction.thy	Sat Dec 22 19:42:35 2001 +0100
@@ -5,56 +5,246 @@
     Logic Image: ZF
 *)
 
-Reduction = Terms+
+theory Reduction = Residuals:
+
+(**** Lambda-terms ****)
 
 consts
-  Sred1, Sred,  Spar_red1,Spar_red    :: i
-  "-1->","--->","=1=>",   "===>"      :: [i,i]=>o (infixl 50)
+  lambda        :: "i"
+  unmark        :: "i=>i"
+  Apl           :: "[i,i]=>i"
 
 translations
-  "a -1-> b" == "<a,b>:Sred1"
-  "a ---> b" == "<a,b>:Sred"
-  "a =1=> b" == "<a,b>:Spar_red1"
-  "a ===> b" == "<a,b>:Spar_red"
+  "Apl(n,m)" == "App(0,n,m)"
+  
+inductive
+  domains       "lambda" <= "redexes"
+  intros
+    Lambda_Var:  "               n \<in> nat ==>     Var(n) \<in> lambda"
+    Lambda_Fun:  "            u \<in> lambda ==>     Fun(u) \<in> lambda"
+    Lambda_App:  "[|u \<in> lambda; v \<in> lambda|] ==> Apl(u,v) \<in> lambda"
+  type_intros    redexes.intros bool_typechecks
+
+declare lambda.intros [intro]
+
+primrec
+  "unmark(Var(n)) = Var(n)"
+  "unmark(Fun(u)) = Fun(unmark(u))"
+  "unmark(App(b,f,a)) = Apl(unmark(f), unmark(a))"
+
+
+declare lambda.intros [simp] 
+declare lambda.dom_subset [THEN subsetD, simp, intro]
+
+
+(* ------------------------------------------------------------------------- *)
+(*        unmark lemmas                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+lemma unmark_type [intro, simp]:
+     "u \<in> redexes ==> unmark(u) \<in> lambda"
+by (erule redexes.induct, simp_all)
+
+lemma lambda_unmark: "u \<in> lambda ==> unmark(u) = u"
+by (erule lambda.induct, simp_all)
+
+
+(* ------------------------------------------------------------------------- *)
+(*         lift and subst preserve lambda                                    *)
+(* ------------------------------------------------------------------------- *)
+
+lemma liftL_type [rule_format]:
+     "v \<in> lambda ==> \<forall>k \<in> nat. lift_rec(v,k) \<in> lambda"
+by (erule lambda.induct, simp_all add: lift_rec_Var)
+
+lemma substL_type [rule_format, simp]:
+     "v \<in> lambda ==>  \<forall>n \<in> nat. \<forall>u \<in> lambda. subst_rec(u,v,n) \<in> lambda"
+by (erule lambda.induct, simp_all add: liftL_type subst_Var)
+
+
+(* ------------------------------------------------------------------------- *)
+(*        type-rule for reduction definitions                               *)
+(* ------------------------------------------------------------------------- *)
+
+lemmas red_typechecks = substL_type nat_typechecks lambda.intros 
+                        bool_typechecks
+
+consts
+  Sred1     :: "i"
+  Sred      :: "i"
+  Spar_red1 :: "i"
+  Spar_red  :: "i"
+  "-1->"    :: "[i,i]=>o"  (infixl 50)
+  "--->"    :: "[i,i]=>o"  (infixl 50)
+  "=1=>"    :: "[i,i]=>o"  (infixl 50)
+  "===>"    :: "[i,i]=>o"  (infixl 50)
+
+translations
+  "a -1-> b" == "<a,b> \<in> Sred1"
+  "a ---> b" == "<a,b> \<in> Sred"
+  "a =1=> b" == "<a,b> \<in> Spar_red1"
+  "a ===> b" == "<a,b> \<in> Spar_red"
   
   
 inductive
   domains       "Sred1" <= "lambda*lambda"
-  intrs
-    beta        "[|m \\<in> lambda; n \\<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m"
-    rfun        "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
-    apl_l       "[|m2 \\<in> lambda; m1 -1-> n1|] ==>   
-                                  Apl(m1,m2) -1-> Apl(n1,m2)"
-    apl_r       "[|m1 \\<in> lambda; m2 -1-> n2|] ==>   
-                                  Apl(m1,m2) -1-> Apl(m1,n2)"
-  type_intrs    "red_typechecks"
+  intros
+    beta:       "[|m \<in> lambda; n \<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m"
+    rfun:       "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
+    apl_l:      "[|m2 \<in> lambda; m1 -1-> n1|] ==> Apl(m1,m2) -1-> Apl(n1,m2)"
+    apl_r:      "[|m1 \<in> lambda; m2 -1-> n2|] ==> Apl(m1,m2) -1-> Apl(m1,n2)"
+  type_intros    red_typechecks
+
+declare Sred1.intros [intro, simp]
 
 inductive
   domains       "Sred" <= "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    "[Sred1.dom_subset RS subsetD]@red_typechecks"
+  intros
+    one_step:   "m-1->n ==> m--->n"
+    refl:       "m \<in> lambda==>m --->m"
+    trans:      "[|m--->n; n--->p|] ==>m--->p"
+  type_intros    Sred1.dom_subset [THEN subsetD] red_typechecks
+
+declare Sred.one_step [intro, simp]
+declare Sred.refl     [intro, simp]
 
 inductive
   domains       "Spar_red1" <= "lambda*lambda"
-  intrs
-    beta        "[|m =1=> m';   
-                 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
-    rvar        "n \\<in> nat==> Var(n) =1=> Var(n)"
-    rfun        "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
-    rapl        "[|m =1=> m';   
-                 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
-  type_intrs    "red_typechecks"
+  intros
+    beta:       "[|m =1=> m'; n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
+    rvar:       "n \<in> nat ==> Var(n) =1=> Var(n)"
+    rfun:       "m =1=> m' ==> Fun(m) =1=> Fun(m')"
+    rapl:       "[|m =1=> m'; n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
+  type_intros    red_typechecks
+
+declare Spar_red1.intros [intro, simp]
+
+inductive
+  domains "Spar_red" <= "lambda*lambda"
+  intros
+    one_step:   "m =1=> n ==> m ===> n"
+    trans:      "[|m===>n; n===>p|] ==> m===>p"
+  type_intros    Spar_red1.dom_subset [THEN subsetD] red_typechecks
+
+declare Spar_red.one_step [intro, simp]
+
+
+
+(* ------------------------------------------------------------------------- *)
+(*     Setting up rule lists for reduction                                   *)
+(* ------------------------------------------------------------------------- *)
+
+lemmas red1D1 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas red1D2 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD2]
+lemmas redD1 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas redD2 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD2]
+
+lemmas par_red1D1 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas par_red1D2 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD2]
+lemmas par_redD1 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas par_redD2 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD2]
+
+declare bool_typechecks [intro]
+
+inductive_cases  [elim!]: "Fun(t) =1=> Fun(u)"
+
+
+
+(* ------------------------------------------------------------------------- *)
+(*     Lemmas for reduction                                                  *)
+(* ------------------------------------------------------------------------- *)
+
+lemma red_Fun: "m--->n ==> Fun(m) ---> Fun(n)"
+apply (erule Sred.induct)
+apply (rule_tac [3] Sred.trans)
+apply simp_all
+done
+
+lemma red_Apll: "[|n \<in> lambda; m ---> m'|] ==> Apl(m,n)--->Apl(m',n)"
+apply (erule Sred.induct)
+apply (rule_tac [3] Sred.trans)
+apply simp_all
+done
+
+lemma red_Aplr: "[|n \<in> lambda; m ---> m'|] ==> Apl(n,m)--->Apl(n,m')"
+apply (erule Sred.induct)
+apply (rule_tac [3] Sred.trans)
+apply simp_all
+done
+
+lemma red_Apl: "[|m ---> m'; n--->n'|] ==> Apl(m,n)--->Apl(m',n')"
+apply (rule_tac n = "Apl (m',n) " in Sred.trans)
+apply (simp_all add: red_Apll red_Aplr)
+done
 
-  inductive
-  domains       "Spar_red" <= "lambda*lambda"
-  intrs
-    one_step    "[|m =1=> n|] ==> m ===> n"
-    trans       "[|m===>n; n===>p|]==>m===>p"
-  type_intrs    "[Spar_red1.dom_subset RS subsetD]@red_typechecks"
+lemma red_beta: "[|m \<in> lambda; m':lambda; n \<in> lambda; n':lambda; m ---> m'; n--->n'|] ==>  
+               Apl(Fun(m),n)---> n'/m'"
+apply (rule_tac n = "Apl (Fun (m') ,n') " in Sred.trans)
+apply (simp_all add: red_Apl red_Fun)
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(*      Lemmas for parallel reduction                                        *)
+(* ------------------------------------------------------------------------- *)
+
+
+lemma refl_par_red1: "m \<in> lambda==> m =1=> m"
+by (erule lambda.induct, simp_all)
+
+lemma red1_par_red1: "m-1->n ==> m=1=>n"
+by (erule Sred1.induct, simp_all add: refl_par_red1)
+
+lemma red_par_red: "m--->n ==> m===>n"
+apply (erule Sred.induct)
+apply (rule_tac [3] Spar_red.trans)
+apply (simp_all add: refl_par_red1 red1_par_red1)
+done
+
+lemma par_red_red: "m===>n ==> m--->n"
+apply (erule Spar_red.induct)
+apply (erule Spar_red1.induct)
+apply (rule_tac [5] Sred.trans)
+apply (simp_all add: red_Fun red_beta red_Apl)
+done
+
 
+(* ------------------------------------------------------------------------- *)
+(*      Simulation                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+lemma simulation: "m=1=>n ==> \<exists>v. m|>v = n & m~v & regular(v)"
+by (erule Spar_red1.induct, force+)
+
+
+(* ------------------------------------------------------------------------- *)
+(*           commuting of unmark and subst                                   *)
+(* ------------------------------------------------------------------------- *)
+
+lemma unmmark_lift_rec:
+     "u \<in> redexes ==> \<forall>k \<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)"
+by (erule redexes.induct, simp_all add: lift_rec_Var)
+
+lemma unmmark_subst_rec:
+ "v \<in> redexes ==> \<forall>k \<in> nat. \<forall>u \<in> redexes.   
+                  unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)"
+by (erule redexes.induct, simp_all add: unmmark_lift_rec subst_Var)
+
+
+(* ------------------------------------------------------------------------- *)
+(*        Completeness                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+lemma completeness_l [rule_format]:
+     "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)"
+apply (erule Scomp.induct)
+apply (auto simp add: unmmark_subst_rec)
+apply (drule_tac psi = "Fun (?u) =1=> ?w" in asm_rl)
+apply auto
+done
+
+lemma completeness: "[|u \<in> lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)"
+by (drule completeness_l, simp_all add: lambda_unmark)
 
 end
 
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Residuals.ML
--- a/src/ZF/Resid/Residuals.ML	Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,182 +0,0 @@
-(*  Title:      Residuals.ML
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-*)
-
-(* ------------------------------------------------------------------------- *)
-(*       Setting up rule lists                                               *)
-(* ------------------------------------------------------------------------- *)
-
-AddIs (Sres.intrs @ Sreg.intrs @ [subst_type]); 
-AddSEs (map Sres.mk_cases
-	     ["residuals(Var(n),Var(n),v)",
-	      "residuals(Fun(t),Fun(u),v)",
-	      "residuals(App(b, u1, u2), App(0, v1, v2),v)",
-	      "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)",
-	      "residuals(Var(n),u,v)",
-	      "residuals(Fun(t),u,v)",
-	      "residuals(App(b, u1, u2), w,v)",
-	      "residuals(u,Var(n),v)",
-	      "residuals(u,Fun(t),v)",
-	      "residuals(w,App(b, u1, u2),v)"]);
-
-AddSEs (map Ssub.mk_cases
-	     ["Var(n) <== u",
-	      "Fun(n) <== u",
-	      "u <== Fun(n)",
-	      "App(1,Fun(t),a) <== u",
-	      "App(0,t,a) <== u"]);
-
-AddSEs [redexes.mk_cases "Fun(t):redexes"];
-
-Addsimps Sres.intrs;
-val resD1 = Sres.dom_subset RS subsetD RS SigmaD1;
-val resD2 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD1;
-val resD3 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD2;
-
-
-(* ------------------------------------------------------------------------- *)
-(*       residuals is a  partial function                                    *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "residuals(u,v,w) ==> \\<forall>w1. residuals(u,v,w1) --> w1 = w";
-by (etac Sres.induct 1);
-by (ALLGOALS Force_tac);
-qed_spec_mp "residuals_function";
-
-Goal "u~v ==> regular(v) --> (\\<exists>w. residuals(u,v,w))";
-by (etac Scomp.induct 1);
-by (ALLGOALS Fast_tac);
-qed "residuals_intro";
-
-Goal "[| u~v;  regular(v) |] ==> residuals(u,v,THE w. residuals(u, v, w))";
-by (resolve_tac [residuals_intro RS mp RS exE] 1);
-by (stac the_equality 3);
-by (ALLGOALS (blast_tac (claset() addIs [residuals_function])));
-qed "comp_resfuncD";
-
-
-(* ------------------------------------------------------------------------- *)
-(*               Residual function                                           *)
-(* ------------------------------------------------------------------------- *)
-
-Goalw [res_func_def] "n \\<in> nat ==> Var(n) |> Var(n) = Var(n)";
-by (Blast_tac 1);
-qed "res_Var";
-
-Goalw [res_func_def]
-    "[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)";
-by (blast_tac (claset() addSDs [comp_resfuncD]
-			addIs [residuals_function]) 1);
-qed "res_Fun";
-
-Goalw [res_func_def]
-    "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \
-\           App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)";
-by (blast_tac (claset() addSDs [comp_resfuncD]
-			addIs [residuals_function]) 1);
-qed "res_App";
-
-Goalw [res_func_def]
-    "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \
-\           App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)";
-by (blast_tac (claset() addSEs redexes.free_SEs
-			addSDs [comp_resfuncD]
-			addIs [residuals_function]) 1);
-qed "res_redex";
-
-Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t \\<in> redexes";
-by (etac Scomp.induct 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [res_Var,res_Fun,res_App,res_redex]));
-by (dres_inst_tac [("psi", "Fun(?u) |> ?v \\<in> redexes")] asm_rl 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [res_Fun]));
-qed "resfunc_type";
-
-Addsimps [res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp,
-	  lift_rec_preserve_reg, subst_rec_preserve_comp, resfunc_type,
-	  subst_rec_preserve_reg];
-
-
-(* ------------------------------------------------------------------------- *)
-(*     Commutation theorem                                                   *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u<==v ==> u~v";
-by (etac Ssub.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "sub_comp";
-
-Goal "u<==v  ==> regular(v) --> regular(u)";
-by (etac Ssub.induct 1);
-by Auto_tac;
-qed_spec_mp "sub_preserve_reg";
-
-Goal "[|u~v; k \\<in> nat|]==> regular(v)--> (\\<forall>n \\<in> nat.  \
-\        lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))";
-by (etac Scomp.induct 1);
-by Safe_tac;
-by (ALLGOALS
-    (asm_full_simp_tac
-     (simpset() addsimps [lift_rec_Var,subst_Var,lift_subst])));
-by (rotate_tac ~2 1);
-by (Asm_full_simp_tac 1);
-qed "residuals_lift_rec";
-
-Goal "u1~u2 ==>  \\<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\
-\   (\\<forall>n \\<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
-\              subst_rec(v1 |> v2, u1 |> u2,n))";
-by (etac Scomp.induct 1);
-by Safe_tac;
-by (ALLGOALS
-    (asm_simp_tac
-     (simpset() addsimps [lift_rec_Var,subst_Var,residuals_lift_rec])));
-by (dres_inst_tac [("psi", "\\<forall>x.?P(x)")] asm_rl 1);
-by (asm_full_simp_tac (simpset() addsimps [substitution]) 1);
-qed "residuals_subst_rec";
-
-
-Goal "[|u1~u2; v1~v2; regular(u2); regular(v2)|]==>\
-\       (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)";
-by (asm_simp_tac (simpset() addsimps [residuals_subst_rec]) 1);
-qed "commutation";
-
-(* ------------------------------------------------------------------------- *)
-(*     Residuals are comp and regular                                        *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u~v ==> \\<forall>w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
-by (etac Scomp.induct 1);
-by (ALLGOALS Force_tac);
-qed_spec_mp "residuals_preserve_comp";
-
-
-Goal "u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
-by (etac Scomp.induct 1);
-by Safe_tac;
-by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl));
-by Auto_tac;
-qed_spec_mp "residuals_preserve_reg";
-
-(* ------------------------------------------------------------------------- *)
-(*     Preservation lemma                                                    *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u~v ==> v ~ (u un v)";
-by (etac Scomp.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "union_preserve_comp";
-
-Goal "u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
-by (etac Scomp.induct 1);
-by Safe_tac;
-by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3);
-by (auto_tac (claset(), 
-	      simpset() addsimps [union_preserve_comp,comp_sym_iff]));
-by (asm_full_simp_tac (simpset() addsimps 
-                       [union_preserve_comp RS comp_sym,
-                        comp_sym RS union_preserve_comp RS comp_sym]) 1);
-qed_spec_mp "preservation";
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Residuals.thy
--- a/src/ZF/Resid/Residuals.thy	Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/Residuals.thy	Sat Dec 22 19:42:35 2001 +0100
@@ -6,31 +6,249 @@
 
 *)
 
-Residuals = Substitution+
+theory Residuals = Substitution:
 
 consts
-  Sres          :: i
-  residuals     :: [i,i,i]=>i
-  "|>"          :: [i,i]=>i     (infixl 70)
-  
+  Sres          :: "i"
+  residuals     :: "[i,i,i]=>i"
+  "|>"          :: "[i,i]=>i"     (infixl 70)
+
 translations
-  "residuals(u,v,w)"  == "<u,v,w>:Sres"
+  "residuals(u,v,w)"  == "<u,v,w> \<in> Sres"
 
 inductive
   domains       "Sres" <= "redexes*redexes*redexes"
-  intrs
-    Res_Var     "n \\<in> nat ==> residuals(Var(n),Var(n),Var(n))"
-    Res_Fun     "[|residuals(u,v,w)|]==>   
+  intros
+    Res_Var:    "n \<in> nat ==> residuals(Var(n),Var(n),Var(n))"
+    Res_Fun:    "[|residuals(u,v,w)|]==>   
                      residuals(Fun(u),Fun(v),Fun(w))"
-    Res_App     "[|residuals(u1,v1,w1);   
-                   residuals(u2,v2,w2); b \\<in> bool|]==>   
+    Res_App:    "[|residuals(u1,v1,w1);   
+                   residuals(u2,v2,w2); b \<in> bool|]==>   
                  residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
-    Res_redex   "[|residuals(u1,v1,w1);   
-                   residuals(u2,v2,w2); b \\<in> bool|]==>   
+    Res_redex:  "[|residuals(u1,v1,w1);   
+                   residuals(u2,v2,w2); b \<in> bool|]==>   
                  residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
-  type_intrs    "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
+  type_intros    subst_type nat_typechecks redexes.intros bool_typechecks
+
+defs
+  res_func_def:  "u |> v == THE w. residuals(u,v,w)"
+
+
+(* ------------------------------------------------------------------------- *)
+(*       Setting up rule lists                                               *)
+(* ------------------------------------------------------------------------- *)
+
+declare Sres.intros [intro]
+declare Sreg.intros [intro]
+declare subst_type [intro]
+
+inductive_cases [elim!]: "residuals(Var(n),Var(n),v)"
+inductive_cases [elim!]: "residuals(Fun(t),Fun(u),v)"
+inductive_cases [elim!]: "residuals(App(b, u1, u2), App(0, v1, v2),v)"
+inductive_cases [elim!]: "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)"
+inductive_cases [elim!]: "residuals(Var(n),u,v)"
+inductive_cases [elim!]: "residuals(Fun(t),u,v)"
+inductive_cases [elim!]: "residuals(App(b, u1, u2), w,v)"
+inductive_cases [elim!]: "residuals(u,Var(n),v)"
+inductive_cases [elim!]: "residuals(u,Fun(t),v)"
+inductive_cases [elim!]: "residuals(w,App(b, u1, u2),v)"
+
+
+inductive_cases [elim!]: "Var(n) <== u"
+inductive_cases [elim!]: "Fun(n) <== u"
+inductive_cases [elim!]: "u <== Fun(n)"
+inductive_cases [elim!]: "App(1,Fun(t),a) <== u"
+inductive_cases [elim!]: "App(0,t,a) <== u"
+
+inductive_cases [elim!]: "Fun(t):redexes"
+
+declare Sres.intros [simp]
+
+
+(* ------------------------------------------------------------------------- *)
+(*       residuals is a  partial function                                    *)
+(* ------------------------------------------------------------------------- *)
+
+lemma residuals_function [rule_format]:
+     "residuals(u,v,w) ==> \<forall>w1. residuals(u,v,w1) --> w1 = w"
+by (erule Sres.induct, force+)
+
+lemma residuals_intro [rule_format]:
+     "u~v ==> regular(v) --> (\<exists>w. residuals(u,v,w))"
+by (erule Scomp.induct, force+)
+
+lemma comp_resfuncD:
+     "[| u~v;  regular(v) |] ==> residuals(u, v, THE w. residuals(u, v, w))"
+apply (frule residuals_intro, assumption)
+apply clarify
+apply (subst the_equality)
+apply (blast intro: residuals_function)+
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(*               Residual function                                           *)
+(* ------------------------------------------------------------------------- *)
+
+lemma res_Var [simp]: "n \<in> nat ==> Var(n) |> Var(n) = Var(n)"
+by (unfold res_func_def, blast)
+
+lemma res_Fun [simp]: 
+    "[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"
+apply (unfold res_func_def)
+apply (blast intro: comp_resfuncD residuals_function) 
+done
+
+lemma res_App [simp]: 
+    "[|s~u; regular(u); t~v; regular(v); b \<in> bool|]
+     ==> App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"
+apply (unfold res_func_def) 
+apply (blast dest!: comp_resfuncD intro: residuals_function)
+done
+
+lemma res_redex [simp]: 
+    "[|s~u; regular(u); t~v; regular(v); b \<in> bool|]
+     ==> App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"
+apply (unfold res_func_def)
+apply (blast elim!: redexes.free_elims dest!: comp_resfuncD 
+             intro: residuals_function)
+done
+
+lemma resfunc_type [simp]:
+     "[|s~t; regular(t)|]==> regular(t) --> s |> t \<in> redexes"
+apply (erule Scomp.induct)
+apply auto
+apply (drule_tac psi = "Fun (?u) |> ?v \<in> redexes" in asm_rl)
+apply auto
+done
+
+(* ------------------------------------------------------------------------- *)
+(*     Commutation theorem                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+lemma sub_comp [simp]: "u<==v ==> u~v"
+by (erule Ssub.induct, simp_all)
+
+lemma sub_preserve_reg [rule_format, simp]:
+     "u<==v  ==> regular(v) --> regular(u)"
+by (erule Ssub.induct, auto)
 
-rules
-  res_func_def  "u |> v == THE w. residuals(u,v,w)"
+lemma residuals_lift_rec: "[|u~v; k \<in> nat|]==> regular(v)--> (\<forall>n \<in> nat.   
+         lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"
+apply (erule Scomp.induct)
+apply safe
+apply (simp_all add: lift_rec_Var subst_Var lift_subst)
+apply (rotate_tac -2)
+apply simp
+done
+
+lemma residuals_subst_rec:
+     "u1~u2 ==>  \<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) --> 
+                  (\<forall>n \<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) =  
+                    subst_rec(v1 |> v2, u1 |> u2,n))"
+apply (erule Scomp.induct)
+apply safe
+apply (simp_all add: lift_rec_Var subst_Var residuals_lift_rec)
+apply (drule_tac psi = "\<forall>x.?P (x) " in asm_rl)
+apply (simp add: substitution)
+done
+
+
+lemma commutation [simp]:
+     "[|u1~u2; v1~v2; regular(u2); regular(v2)|]
+      ==> (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)"
+by (simp add: residuals_subst_rec)
+
+
+(* ------------------------------------------------------------------------- *)
+(*     Residuals are comp and regular                                        *)
+(* ------------------------------------------------------------------------- *)
+
+lemma residuals_preserve_comp [rule_format, simp]:
+     "u~v ==> \<forall>w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)"
+by (erule Scomp.induct, force+)
+
+lemma residuals_preserve_reg [rule_format, simp]:
+     "u~v ==> regular(u) --> regular(v) --> regular(u|>v)"
+apply (erule Scomp.induct)
+apply auto
+apply (drule_tac psi = "regular (Fun (?u) |> ?v)" in asm_rl, force)+
+done
+
+(* ------------------------------------------------------------------------- *)
+(*     Preservation lemma                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+lemma union_preserve_comp: "u~v ==> v ~ (u un v)"
+by (erule Scomp.induct, simp_all)
+
+lemma preservation [rule_format]:
+     "u ~ v ==> regular(v) --> u|>v = (u un v)|>v"
+apply (erule Scomp.induct)
+apply safe
+apply (drule_tac [3] psi = "Fun (?u) |> ?v = ?w" in asm_rl)
+apply (auto simp add: union_preserve_comp comp_sym_iff)
+done
+
+
+(**** And now the Cube ***)
+
+declare sub_comp [THEN comp_sym, simp]
+
+(* ------------------------------------------------------------------------- *)
+(*         Prism theorem                                                     *)
+(*         =============                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+(* Having more assumptions than needed -- removed below  *)
+lemma prism_l [rule_format]:
+     "v<==u ==>  
+       regular(u) --> (\<forall>w. w~v --> w~u -->   
+                            w |> u = (w|>v) |> (u|>v))"
+apply (erule Ssub.induct)
+apply force+
+done
+
+lemma prism:
+     "[|v <== u; regular(u); w~v|] ==> w |> u = (w|>v) |> (u|>v)"
+apply (rule prism_l)
+apply (rule_tac [4] comp_trans)
+apply auto
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(*    Levy's Cube Lemma                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+lemma cube: "[|u~v; regular(v); regular(u); w~u|]==>   
+           (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"
+apply (subst preservation , assumption , assumption)
+apply (subst preservation , erule comp_sym , assumption)
+apply (subst prism [symmetric])
+apply (simp add: union_r comp_sym_iff)
+apply (simp add: union_preserve_regular comp_sym_iff)
+apply (erule comp_trans)
+apply assumption
+apply (simp add: prism [symmetric] union_l union_preserve_regular 
+                 comp_sym_iff union_sym)
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(*           paving theorem                                                  *)
+(* ------------------------------------------------------------------------- *)
+
+lemma paving: "[|w~u; w~v; regular(u); regular(v)|]==>  
+           \<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu & 
+             regular(vu) & (w|>v)~uv & regular(uv) "
+apply (subgoal_tac "u~v")
+apply (safe intro!: exI)
+apply (rule cube)
+apply (simp_all add: comp_sym_iff)
+apply (blast intro: residuals_preserve_comp comp_trans comp_sym)+
+done
+
+
 end
 
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Substitution.ML
--- a/src/ZF/Resid/Substitution.ML	Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,257 +0,0 @@
-(*  Title:      Substitution.ML
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-*)
-
-(* ------------------------------------------------------------------------- *)
-(*   Arithmetic extensions                                                   *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "[| p < n; n \\<in> nat|] ==> n\\<noteq>p";
-by (Fast_tac 1);
-qed "gt_not_eq";
-
-Goal "[|j \\<in> nat; i \\<in> nat|] ==> i < j --> succ(j #- 1) = j";
-by (induct_tac "j" 1);
-by (Fast_tac 1);
-by (Asm_simp_tac 1);
-qed "succ_pred";
-
-Goal "[|succ(x)<n; n \\<in> nat; x \\<in> nat|] ==> x < n #- 1 ";
-by (rtac succ_leE 1);
-by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
-qed "lt_pred";
-
-Goal "[|n < succ(x); p<n; p \\<in> nat; n \\<in> nat; x \\<in> nat|] ==> n #- 1 < x ";
-by (rtac succ_leE 1);
-by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
-qed "gt_pred";
-
-
-Addsimps [not_lt_iff_le, if_P, if_not_P];
-
-
-(* ------------------------------------------------------------------------- *)
-(*     lift_rec equality rules                                               *)
-(* ------------------------------------------------------------------------- *)
-Goal "[|n \\<in> nat; i \\<in> nat|] \
-\     ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))";
-by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
-qed "lift_rec_Var";
-
-Goal "[|n \\<in> nat; i \\<in> nat; k \\<in> nat; k le i|] ==> lift_rec(Var(i),k) = Var(succ(i))";
-by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
-qed "lift_rec_le";
-
-Goal "[|i \\<in> nat; k \\<in> nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)";
-by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
-qed "lift_rec_gt";
-
-Goal "[|n \\<in> nat; k \\<in> nat|] ==>   \
-\        lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
-by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
-qed "lift_rec_Fun";
-
-Goal "[|n \\<in> nat; k \\<in> nat|] ==>   \
-\        lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
-by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
-qed "lift_rec_App";
-
-
-(* ------------------------------------------------------------------------- *)
-(*    substitution quality rules                                             *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "[|i \\<in> nat; k \\<in> nat; u \\<in> redexes|]  \
-\     ==> subst_rec(u,Var(i),k) =  \
-\         (if k<i then Var(i #- 1) else if k=i then u else Var(i))";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
-qed "subst_Var";
-
-Goal "[|n \\<in> nat; u \\<in> redexes|] ==> subst_rec(u,Var(n),n) = u";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
-qed "subst_eq";
-
-Goal "[|n \\<in> nat; u \\<in> redexes; p \\<in> nat; p<n|] ==>  \
-\     subst_rec(u,Var(n),p) = Var(n #- 1)";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
-qed "subst_gt";
-
-Goal "[|n \\<in> nat; u \\<in> redexes; p \\<in> nat; n<p|] ==>  \
-\     subst_rec(u,Var(n),p) = Var(n)";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
-qed "subst_lt";
-
-Goal "[|p \\<in> nat; u \\<in> redexes|] ==>  \
-\     subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
-qed "subst_Fun";
-
-Goal "[|p \\<in> nat; u \\<in> redexes|] ==>  \
-\     subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
-qed "subst_App";
-
-(*But not lift_rec_Var, subst_Var: too many case splits*)
-Addsimps [subst_Fun, subst_App];
-
-
-Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. lift_rec(u,k):redexes";
-by (etac redexes.induct 1);
-by (ALLGOALS
-    (asm_simp_tac (simpset() addsimps [lift_rec_Var,
-				       lift_rec_Fun, lift_rec_App])));
-qed_spec_mp "lift_rec_type";
-
-Goal "v \\<in> redexes ==>  \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. subst_rec(u,v,n):redexes";
-by (etac redexes.induct 1);
-by (ALLGOALS(asm_simp_tac 
-    (simpset() addsimps [subst_Var, lift_rec_type])));
-qed_spec_mp "subst_type";
-
-
-Addsimps [subst_eq, subst_gt, subst_lt, subst_type,
-	  lift_rec_le, lift_rec_gt, lift_rec_Fun, lift_rec_App,
-	  lift_rec_type];
-
-
-(* ------------------------------------------------------------------------- *)
-(*    lift and  substitution proofs                                          *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u \\<in> redexes ==> \\<forall>n \\<in> nat. \\<forall>i \\<in> nat. i le n -->   \
-\       (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
-by (etac redexes.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by Safe_tac;
-by (case_tac "n < i" 1);
-by ((ftac lt_trans2 1) THEN (assume_tac 1));
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
-qed "lift_lift_rec";
-
-Goal "[|u \\<in> redexes; n \\<in> nat|] ==>  \
-\      lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))";
-by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1);
-qed "lift_lift";
-
-Goal "v \\<in> redexes ==>  \
-\      \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. n le m-->\
-\         lift_rec(subst_rec(u,v,n),m) = \
-\              subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)";
-by ((etac redexes.induct 1)
-    THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift]))));
-by Safe_tac;
-by (excluded_middle_tac "n < x" 1);
-by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("j","n")] leE 1);
-by (asm_simp_tac (simpset() setloop (split_inside_tac [split_if])
-			 addsimps [lift_rec_Var,subst_Var,
-				   leI,gt_pred,succ_pred]) 1);
-by (hyp_subst_tac 1);
-by (Asm_simp_tac 1);
-by (forw_inst_tac [("j","x")] lt_trans2 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [leI]) 1);
-qed "lift_rec_subst_rec";
-
-Goal "[|v \\<in> redexes; u \\<in> redexes; n \\<in> nat|] ==>  \
-\        lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))";
-by (asm_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
-qed "lift_subst";
-
-
-Goal "v \\<in> redexes ==>  \
-\      \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. m le n-->\
-\         lift_rec(subst_rec(u,v,n),m) = \
-\              subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))";
-by (etac redexes.induct 1
-    THEN ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])));
-by Safe_tac;
-by (excluded_middle_tac "n < x" 1);
-by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("i","x")] leE 1);
-by (ftac lt_trans1 1 THEN assume_tac 1);
-by (ALLGOALS(asm_simp_tac 
-             (simpset() addsimps [succ_pred,leI,gt_pred])));
-by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
-by (case_tac "n < xa" 1);
-by (Asm_full_simp_tac 2);
-by (asm_simp_tac (simpset() addsimps [leI]) 1);
-qed "lift_rec_subst_rec_lt";
-
-
-Goal "u \\<in> redexes ==>  \
-\       \\<forall>n \\<in> nat. \\<forall>v \\<in> redexes. subst_rec(v,lift_rec(u,n),n) =  u";
-by (etac redexes.induct 1);
-by Auto_tac;
-by (case_tac "n < na" 1);
-by Auto_tac;
-qed "subst_rec_lift_rec";
-
-Goal "v \\<in> redexes ==>  \
-\       \\<forall>m \\<in> nat. \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. \\<forall>w \\<in> redexes. m le  n --> \
-\    subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
-\    subst_rec(w,subst_rec(u,v,m),n)";
-by (etac redexes.induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps 
-			   [lift_lift RS sym,lift_rec_subst_rec_lt])));
-by Safe_tac;
-by (excluded_middle_tac "n  le succ(xa)" 1);
-by (Asm_full_simp_tac 1);
-by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
-by (etac leE 1);
-by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 2);
-by (forward_tac [succ_leI RS lt_trans] 1 THEN assume_tac 1);
-by (forw_inst_tac [("i","x")] 
-    (nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 1);
-by (eres_inst_tac [("i","n")] leE 1);
-by (asm_simp_tac (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2);
-by (excluded_middle_tac "n < x" 1);
-by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("j","n")] leE 1);
-by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
-by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1);
-by (ftac lt_trans2 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
-qed "subst_rec_subst_rec";
-
-
-Goal "[|v \\<in> redexes; u \\<in> redexes; w \\<in> redexes; n \\<in> nat|] ==>  \
-\       subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)";
-by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1);
-qed "substitution";
-
-(* ------------------------------------------------------------------------- *)
-(*          Preservation lemmas                                              *)
-(*          Substitution preserves comp and regular                          *)
-(* ------------------------------------------------------------------------- *)
-
-
-Goal "[|n \\<in> nat; u ~ v|] ==> \\<forall>m \\<in> nat. lift_rec(u,m) ~ lift_rec(v,m)";
-by (etac Scomp.induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl])));
-qed "lift_rec_preserve_comp";
-
-Goal "u2 ~ v2 ==> \\<forall>m \\<in> nat. \\<forall>u1 \\<in> redexes. \\<forall>v1 \\<in> redexes.\
-\            u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
-by (etac Scomp.induct 1);
-by (ALLGOALS
-    (asm_simp_tac
-     (simpset() addsimps [subst_Var, lift_rec_preserve_comp, comp_refl])));
-qed "subst_rec_preserve_comp";
-
-Goal "regular(u) ==> \\<forall>m \\<in> nat. regular(lift_rec(u,m))";
-by (etac Sreg.induct 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var])));
-qed "lift_rec_preserve_reg";
-
-Goal "regular(v) ==>  \
-\       \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. regular(u)-->regular(subst_rec(u,v,m))";
-by (etac Sreg.induct 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_Var,
-						    lift_rec_preserve_reg])));
-qed "subst_rec_preserve_reg";
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Substitution.thy
--- a/src/ZF/Resid/Substitution.thy	Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/Substitution.thy	Sat Dec 22 19:42:35 2001 +0100
@@ -5,19 +5,19 @@
     Logic Image: ZF
 *)
 
-Substitution = Redex +
+theory Substitution = Redex:
 
 consts
-  lift_aux  :: i=> i
-  lift          :: i=> i
-  subst_aux :: i=> i
-  "'/"          :: [i,i]=>i  (infixl 70)  (*subst*)
+  lift_aux      :: "i=>i"
+  lift          :: "i=>i"
+  subst_aux     :: "i=>i"
+  "'/"          :: "[i,i]=>i"  (infixl 70)  (*subst*)
 
 constdefs
-  lift_rec      :: [i,i]=> i
+  lift_rec      :: "[i,i]=> i"
     "lift_rec(r,k) == lift_aux(r)`k"
 
-  subst_rec     :: [i,i,i]=> i	(**NOTE THE ARGUMENT ORDER BELOW**)
+  subst_rec     :: "[i,i,i]=> i"	(**NOTE THE ARGUMENT ORDER BELOW**)
     "subst_rec(u,r,k) == subst_aux(r)`u`k"
 
 translations
@@ -29,23 +29,246 @@
     in the recursive calls ***)
 
 primrec
-  "lift_aux(Var(i)) = (\\<lambda>k \\<in> nat. if i<k then Var(i) else Var(succ(i)))"
+  "lift_aux(Var(i)) = (\<lambda>k \<in> nat. if i<k then Var(i) else Var(succ(i)))"
 
-  "lift_aux(Fun(t)) = (\\<lambda>k \\<in> nat. Fun(lift_aux(t) ` succ(k)))"
+  "lift_aux(Fun(t)) = (\<lambda>k \<in> nat. Fun(lift_aux(t) ` succ(k)))"
 
-  "lift_aux(App(b,f,a)) = (\\<lambda>k \\<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
+  "lift_aux(App(b,f,a)) = (\<lambda>k \<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
 
 
   
 primrec
   "subst_aux(Var(i)) =
-     (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. if k<i then Var(i #- 1) 
+     (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. if k<i then Var(i #- 1) 
 				else if k=i then r else Var(i))"
   "subst_aux(Fun(t)) =
-     (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
+     (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
 
   "subst_aux(App(b,f,a)) = 
-     (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
+     (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
+
+
+(* ------------------------------------------------------------------------- *)
+(*   Arithmetic extensions                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+lemma gt_not_eq: "p < n ==> n\<noteq>p"
+by blast
+
+lemma succ_pred [rule_format, simp]: "j \<in> nat ==> i < j --> succ(j #- 1) = j"
+by (induct_tac "j", auto)
+
+lemma lt_pred: "[|succ(x)<n; n \<in> nat|] ==> x < n #- 1 "
+apply (rule succ_leE)
+apply (simp add: succ_pred)
+done
+
+lemma gt_pred: "[|n < succ(x); p<n; n \<in> nat|] ==> n #- 1 < x "
+apply (rule succ_leE)
+apply (simp add: succ_pred)
+done
+
+
+declare not_lt_iff_le [simp] if_P [simp] if_not_P [simp]
+
+
+(* ------------------------------------------------------------------------- *)
+(*     lift_rec equality rules                                               *)
+(* ------------------------------------------------------------------------- *)
+lemma lift_rec_Var:
+     "n \<in> nat ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))"
+by (simp add: lift_rec_def)
+
+lemma lift_rec_le [simp]:
+     "[|i \<in> nat; k\<le>i|] ==> lift_rec(Var(i),k) = Var(succ(i))"
+by (simp add: lift_rec_def le_in_nat)
+
+lemma lift_rec_gt [simp]: "[| k \<in> nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)"
+by (simp add: lift_rec_def)
+
+lemma lift_rec_Fun [simp]:
+     "k \<in> nat ==> lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"
+by (simp add: lift_rec_def)
+
+lemma lift_rec_App [simp]:
+     "k \<in> nat ==> lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))"
+by (simp add: lift_rec_def)
+
+
+(* ------------------------------------------------------------------------- *)
+(*    substitution quality rules                                             *)
+(* ------------------------------------------------------------------------- *)
+
+lemma subst_Var:
+     "[|k \<in> nat; u \<in> redexes|]   
+      ==> subst_rec(u,Var(i),k) =   
+          (if k<i then Var(i #- 1) else if k=i then u else Var(i))"
+by (simp add: subst_rec_def gt_not_eq leI)
+
+
+lemma subst_eq [simp]:
+     "[|n \<in> nat; u \<in> redexes|] ==> subst_rec(u,Var(n),n) = u"
+by (simp add: subst_rec_def)
+
+lemma subst_gt [simp]:
+     "[|u \<in> redexes; p \<in> nat; p<n|] ==> subst_rec(u,Var(n),p) = Var(n #- 1)"
+by (simp add: subst_rec_def)
+
+lemma subst_lt [simp]:
+     "[|u \<in> redexes; p \<in> nat; n<p|] ==> subst_rec(u,Var(n),p) = Var(n)"
+by (simp add: subst_rec_def gt_not_eq leI lt_nat_in_nat)
+
+lemma subst_Fun [simp]:
+     "[|p \<in> nat; u \<in> redexes|]
+      ==> subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) "
+by (simp add: subst_rec_def)
+
+lemma subst_App [simp]:
+     "[|p \<in> nat; u \<in> redexes|]
+      ==> subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))"
+by (simp add: subst_rec_def)
+
+
+lemma lift_rec_type [rule_format, simp]:
+     "u \<in> redexes ==> \<forall>k \<in> nat. lift_rec(u,k) \<in> redexes"
+apply (erule redexes.induct)
+apply (simp_all add: lift_rec_Var lift_rec_Fun lift_rec_App)
+done
+
+lemma subst_type [rule_format, simp]:
+     "v \<in> redexes ==>  \<forall>n \<in> nat. \<forall>u \<in> redexes. subst_rec(u,v,n) \<in> redexes"
+apply (erule redexes.induct)
+apply (simp_all add: subst_Var lift_rec_type)
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(*    lift and  substitution proofs                                          *)
+(* ------------------------------------------------------------------------- *)
+
+(*The i\<in>nat is redundant*)
+lemma lift_lift_rec [rule_format]:
+     "u \<in> redexes 
+      ==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>n -->    
+           (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"
+apply (erule redexes.induct)
+apply auto
+apply (case_tac "n < i")
+apply (frule lt_trans2, assumption)
+apply (simp_all add: lift_rec_Var leI)
+done
+
+lemma lift_lift:
+     "[|u \<in> redexes; n \<in> nat|] 
+      ==> lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"
+by (simp add: lift_lift_rec)
+
+lemma lt_not_m1_lt: "\<lbrakk>m < n; n \<in> nat; m \<in> nat\<rbrakk>\<Longrightarrow> ~ n #- 1 < m"
+by (erule natE, auto)
+
+lemma lift_rec_subst_rec [rule_format]:
+     "v \<in> redexes ==>   
+       \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. n\<le>m--> 
+          lift_rec(subst_rec(u,v,n),m) =  
+               subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"
+apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
+apply safe
+apply (case_tac "n < x")
+ apply (frule_tac j = "x" in lt_trans2, assumption)
+ apply (simp add: leI)
+apply simp
+apply (erule_tac j = "n" in leE)
+apply (auto simp add: lift_rec_Var subst_Var leI lt_not_m1_lt)
+done
+
+
+lemma lift_subst:
+     "[|v \<in> redexes; u \<in> redexes; n \<in> nat|] 
+      ==> lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"
+by (simp add: lift_rec_subst_rec)
+
+
+lemma lift_rec_subst_rec_lt [rule_format]:
+     "v \<in> redexes ==>   
+       \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>n--> 
+          lift_rec(subst_rec(u,v,n),m) =  
+               subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"
+apply (erule redexes.induct , simp_all (no_asm_simp) add: lift_lift)
+apply safe
+apply (case_tac "n < x")
+apply (case_tac "n < xa")
+apply (simp_all add: leI)
+apply (erule_tac i = "x" in leE)
+apply (frule lt_trans1, assumption)
+apply (simp_all add: succ_pred leI gt_pred)
+done
+
+
+lemma subst_rec_lift_rec [rule_format]:
+     "u \<in> redexes ==>   
+        \<forall>n \<in> nat. \<forall>v \<in> redexes. subst_rec(v,lift_rec(u,n),n) = u"
+apply (erule redexes.induct)
+apply auto
+apply (case_tac "n < na")
+apply auto
+done
+
+lemma subst_rec_subst_rec [rule_format]:
+     "v \<in> redexes ==>   
+        \<forall>m \<in> nat. \<forall>n \<in> nat. \<forall>u \<in> redexes. \<forall>w \<in> redexes. m\<le>n -->  
+	  subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) = 
+	  subst_rec(w,subst_rec(u,v,m),n)"
+apply (erule redexes.induct)
+apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt)
+apply safe
+apply (case_tac "n\<le>succ (xa) ")
+ apply (erule_tac i = "n" in leE)
+ apply (simp_all add: succ_pred subst_rec_lift_rec leI)
+ apply (case_tac "n < x")
+  apply (frule lt_trans2 , assumption, simp add: gt_pred)
+ apply simp
+ apply (erule_tac j = "n" in leE, simp add: gt_pred)
+ apply (simp add: subst_rec_lift_rec)
+(*final case*)
+apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans] , assumption)
+apply (erule leE)
+ apply (frule succ_leI [THEN lt_trans] , assumption)
+ apply (frule_tac i = "x" in nat_into_Ord [THEN le_refl, THEN lt_trans], 
+        assumption)
+ apply (simp_all add: succ_pred lt_pred)
+done
+
+
+lemma substitution:
+     "[|v \<in> redexes; u \<in> redexes; w \<in> redexes; n \<in> nat|]
+      ==> subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"
+by (simp add: subst_rec_subst_rec)
+
+
+(* ------------------------------------------------------------------------- *)
+(*          Preservation lemmas                                              *)
+(*          Substitution preserves comp and regular                          *)
+(* ------------------------------------------------------------------------- *)
+
+
+lemma lift_rec_preserve_comp [rule_format, simp]:
+     "u ~ v ==> \<forall>m \<in> nat. lift_rec(u,m) ~ lift_rec(v,m)"
+by (erule Scomp.induct, simp_all add: comp_refl)
+
+lemma subst_rec_preserve_comp [rule_format, simp]:
+     "u2 ~ v2 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> redexes. 
+                  u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"
+by (erule Scomp.induct, 
+    simp_all add: subst_Var lift_rec_preserve_comp comp_refl)
+
+lemma lift_rec_preserve_reg [simp]:
+     "regular(u) ==> \<forall>m \<in> nat. regular(lift_rec(u,m))"
+by (erule Sreg.induct, simp_all add: lift_rec_Var)
+
+lemma subst_rec_preserve_reg [simp]:
+     "regular(v) ==>   
+        \<forall>m \<in> nat. \<forall>u \<in> redexes. regular(u)-->regular(subst_rec(u,v,m))"
+by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)
 
 end
 
diff -r 0eb1685a00b4 -r cd35fe5947d4 src/ZF/Resid/Terms.ML
--- a/src/ZF/Resid/Terms.ML	Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(*  Title:      Terms.ML
-    ID:         $Id$
-    Author:     Ole Rasmussen
-    Copyright   1995  University of Cambridge
-    Logic Image: ZF
-*)
-
-Addsimps ([lambda.dom_subset RS subsetD] @ lambda.intrs);
-
-
-(* ------------------------------------------------------------------------- *)
-(*        unmark lemmas                                                      *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u \\<in> redexes ==> unmark(u):lambda";
-by (etac redexes.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "unmark_type";
-
-Goal "u \\<in> lambda ==> unmark(u) = u";
-by (etac lambda.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "lambda_unmark";
-
-
-(* ------------------------------------------------------------------------- *)
-(*         lift and subst preserve lambda                                    *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "v \\<in> lambda ==> \\<forall>k \\<in> nat. lift_rec(v,k):lambda";
-by (etac lambda.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
-qed_spec_mp "liftL_type";
-
-Goal "v \\<in> lambda ==>  \\<forall>n \\<in> nat. \\<forall>u \\<in> lambda. subst_rec(u,v,n):lambda";
-by (etac lambda.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
-qed_spec_mp "substL_type";
-
-
-(* ------------------------------------------------------------------------- *)
-(*        type-rule for reduction definitions                               *)
-(* ------------------------------------------------------------------------- *)
-
-val red_typechecks = [substL_type]@nat_typechecks@lambda.intrs@bool_typechecks;