# HG changeset patch
# User paulson
# Date 1009530674 -3600
# Node ID cf1715a5f5ec73f4d62878f7fd6ab5d27a8760ed
# Parent  c198367640f6c233db8fb8b380e8b1559d8f98a5
conversion to Isar/ZF

diff -r c198367640f6 -r cf1715a5f5ec src/ZF/Coind/BCR.thy
--- a/src/ZF/Coind/BCR.thy	Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-(*  Title:      ZF/Coind/BCR.thy
-    ID:         $Id$
-    Author:     Jacob Frost, Cambridge University Computer Laboratory
-    Copyright   1995  University of Cambridge
-*)
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/IMP/Com.ML
--- a/src/ZF/IMP/Com.ML	Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(*  Title:      ZF/IMP/Com.ML
-    ID:         $Id$
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
-    Copyright   1994 TUM
-*)
-
-val type_cs = claset() addSDs [evala.dom_subset RS subsetD,
-			      evalb.dom_subset RS subsetD,
-			      evalc.dom_subset RS subsetD];
-
-(**********     type_intrs for evala     **********)
-
-val evala_type_intrs = 
- map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!a.<a,sigma> -a-> n ==> a \\<in> aexp",
-  "!!a.<a,sigma> -a-> n ==> sigma \\<in> loc->nat",
-  "!!a.<a,sigma> -a-> n ==> n \\<in> nat"];
-
-
-(**********     type_intrs for evalb     **********)
-
-val evalb_type_intrs = 
- map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!b.<b,sigma> -b-> w ==> b \\<in> bexp",
-  "!!b.<b,sigma> -b-> w ==> sigma \\<in> loc->nat",
-  "!!b.<b,sigma> -b-> w ==> w \\<in> bool"];
-
-
-(**********     type_intrs for evalb     **********)
-
-val evalc_type_intrs = 
- map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!c.<c,sigma> -c-> sigma' ==> c \\<in> com",
-  "!!c.<c,sigma> -c-> sigma' ==> sigma \\<in> loc->nat",
-  "!!c.<c,sigma> -c-> sigma' ==> sigma':loc->nat"];
-
-
-val op_type_intrs = evala_type_intrs@evalb_type_intrs@evalc_type_intrs;
-
-
-val aexp_elim_cases = 
-   [
-    evala.mk_cases "<N(n),sigma> -a-> i",
-    evala.mk_cases "<X(x),sigma> -a-> i",
-    evala.mk_cases "<Op1(f,e),sigma> -a-> i",
-    evala.mk_cases "<Op2(f,a1,a2),sigma>  -a-> i"
-   ];
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Fri Dec 28 10:10:55 2001 +0100
+++ b/src/ZF/IMP/Com.thy	Fri Dec 28 10:11:14 2001 +0100
@@ -8,34 +8,33 @@
 And their Operational semantics
 *)
 
-Com = Main +
+theory Com = Main:
 
 (** Arithmetic expressions **)
 consts  loc  :: i
         aexp :: i
 
 datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
-  "aexp" = N ("n \\<in> nat")
-         | X ("x \\<in> loc")
-         | Op1 ("f \\<in> nat -> nat", "a \\<in> aexp")
-         | Op2 ("f \\<in> (nat*nat) -> nat", "a0 \\<in> aexp", "a1 \\<in> aexp")
+  "aexp" = N ("n \<in> nat")
+         | X ("x \<in> loc")
+         | Op1 ("f \<in> nat -> nat", "a \<in> aexp")
+         | Op2 ("f \<in> (nat*nat) -> nat", "a0 \<in> aexp", "a1 \<in> aexp")
 
 
 (** Evaluation of arithmetic expressions **)
-consts  evala    :: i
-        "-a->"   :: [i,i] => o                  (infixl 50)
+consts  evala    :: "i"
+        "-a->"   :: "[i,i] => o"                  (infixl 50)
 translations
-    "p -a-> n" == "<p,n> \\<in> evala"
+    "p -a-> n" == "<p,n> \<in> evala"
 inductive
   domains "evala" <= "(aexp * (loc -> nat)) * nat"
-  intrs 
-    N   "[| n \\<in> nat;  sigma \\<in> loc->nat |] ==> <N(n),sigma> -a-> n"
-    X   "[| x \\<in> loc;  sigma \\<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
-    Op1 "[| <e,sigma> -a-> n;  f \\<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
-    Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f \\<in> (nat*nat) -> nat |] 
-           ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
-
-  type_intrs "aexp.intrs@[apply_funtype]"
+  intros 
+    N:   "[| n \<in> nat;  sigma \<in> loc->nat |] ==> <N(n),sigma> -a-> n"
+    X:   "[| x \<in> loc;  sigma \<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
+    Op1: "[| <e,sigma> -a-> n; f \<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
+    Op2: "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f \<in> (nat*nat) -> nat |] 
+          ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
+  type_intros aexp.intros apply_funtype
 
 
 (** Boolean expressions **)
@@ -44,35 +43,34 @@
 datatype <= "univ(aexp Un ((nat*nat)->bool) )"
   "bexp" = true
          | false
-         | ROp  ("f \\<in> (nat*nat)->bool", "a0 \\<in> aexp", "a1 \\<in> aexp")
-         | noti ("b \\<in> bexp")
-         | andi ("b0 \\<in> bexp", "b1 \\<in> bexp")      (infixl 60)
-         | ori  ("b0 \\<in> bexp", "b1 \\<in> bexp")      (infixl 60)
+         | ROp  ("f \<in> (nat*nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
+         | noti ("b \<in> bexp")
+         | andi ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl 60)
+         | ori  ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl 60)
 
 
 (** Evaluation of boolean expressions **)
-consts evalb    :: i    
-       "-b->"   :: [i,i] => o                   (infixl 50)
+consts evalb    :: "i"
+       "-b->"   :: "[i,i] => o"                   (infixl 50)
 
 translations
-    "p -b-> b" == "<p,b> \\<in> evalb"
+    "p -b-> b" == "<p,b> \<in> evalb"
 
 inductive
   domains "evalb" <= "(bexp * (loc -> nat)) * bool"
-  intrs (*avoid clash with ML constructors true, false*)
-    tru   "[| sigma \\<in> loc -> nat |] ==> <true,sigma> -b-> 1"
-    fls   "[| sigma \\<in> loc -> nat |] ==> <false,sigma> -b-> 0"
-    ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \\<in> (nat*nat)->bool |] 
+  intros (*avoid clash with ML constructors true, false*)
+    tru:   "[| sigma \<in> loc -> nat |] ==> <true,sigma> -b-> 1"
+    fls:   "[| sigma \<in> loc -> nat |] ==> <false,sigma> -b-> 0"
+    ROp:   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \<in> (nat*nat)->bool |] 
            ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
-    noti  "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
-    andi  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
+    noti:  "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
+    andi:  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
           ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
-    ori   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
+    ori:   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
             ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
-
-  type_intrs "bexp.intrs @   
-              [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
-  type_elims "[make_elim(evala.dom_subset RS subsetD)]"
+  type_intros  bexp.intros 
+               apply_funtype and_type or_type bool_1I bool_0I not_type
+  type_elims   evala.dom_subset [THEN subsetD, elim_format]
 
 
 (** Commands **)
@@ -80,50 +78,83 @@
 
 datatype 
   "com" = skip
-        | asgt  ("x \\<in> loc", "a \\<in> aexp")             (infixl 60)
-        | semic ("c0 \\<in> com", "c1 \\<in> com")            ("_; _"  [60, 60] 10)
-        | while ("b \\<in> bexp", "c \\<in> com")             ("while _ do _"  60)
-        | ifc   ("b \\<in> bexp", "c0 \\<in> com", "c1 \\<in> com")  ("ifc _ then _ else _"  60)
+        | asgt ("x \<in> loc", "a \<in> aexp")             (infixl 60)
+        | semic("c0 \<in> com", "c1 \<in> com")            ("_; _"  [60, 60] 10)
+        | while("b \<in> bexp", "c \<in> com")             ("while _ do _"  60)
+        | ifc  ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com") ("ifc _ then _ else _" 60)
 
 (*Constructor ";" has low precedence to avoid syntactic ambiguities
-  with [| m \\<in> nat; x \\<in> loc; ... |] ==> ...  It usually will need parentheses.*)
+  with [| m \<in> nat; x \<in> loc; ... |] ==> ...  It usually will need parentheses.*)
 
 (** Execution of commands **)
-consts  evalc    :: i
-        "-c->"   :: [i,i] => o                   (infixl 50)
+consts  evalc    :: "i"
+        "-c->"   :: "[i,i] => o"                   (infixl 50)
 
 translations
-       "p -c-> s" == "<p,s> \\<in> evalc"
-
+       "p -c-> s" == "<p,s> \<in> evalc"
 
 inductive
   domains "evalc" <= "(com * (loc -> nat)) * (loc -> nat)"
-  intrs
-    skip    "[| sigma \\<in> loc -> nat |] ==> <skip,sigma> -c-> sigma"
+  intros
+    skip:    "[| sigma \<in> loc -> nat |] ==> <skip,sigma> -c-> sigma"
+
+    assign:  "[| m \<in> nat; x \<in> loc; <a,sigma> -a-> m |] 
+              ==> <x asgt a,sigma> -c-> sigma(x:=m)"
 
-    assign  "[| m \\<in> nat; x \\<in> loc; <a,sigma> -a-> m |] ==> 
-            <x asgt a,sigma> -c-> sigma(x:=m)"
+    semi:    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] 
+              ==> <c0 ; c1, sigma> -c-> sigma1"
+
+    ifc1:    "[| b \<in> bexp; c1 \<in> com; sigma \<in> loc->nat;   
+                 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] 
+              ==> <ifc b then c0 else c1, sigma> -c-> sigma1"
 
-    semi    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> 
-            <c0 ; c1, sigma> -c-> sigma1"
+    ifc0:    "[| b \<in> bexp; c0 \<in> com; sigma \<in> loc->nat;   
+                 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] 
+               ==> <ifc b then c0 else c1, sigma> -c-> sigma1"
+
+    while0:   "[| c \<in> com; <b, sigma> -b-> 0 |] 
+               ==> <while b do c,sigma> -c-> sigma"
 
-    ifc1     "[| b \\<in> bexp; c1 \\<in> com; sigma \\<in> loc->nat;   
-                 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> 
-             <ifc b then c0 else c1, sigma> -c-> sigma1"
+    while1:   "[| c \<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; 
+                  <while b do c, sigma2> -c-> sigma1 |] 
+               ==> <while b do c, sigma> -c-> sigma1"
+
+  type_intros  com.intros update_type
+  type_elims   evala.dom_subset [THEN subsetD, elim_format]
+               evalb.dom_subset [THEN subsetD, elim_format]
+
+
+(*** type_intros for evala ***)
 
-    ifc0     "[| b \\<in> bexp; c0 \\<in> com; sigma \\<in> loc->nat;   
-                 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> 
-             <ifc b then c0 else c1, sigma> -c-> sigma1"
+lemmas evala_1 [simp] = 
+       evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
+lemmas evala_2 [simp] = 
+       evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
+lemmas evala_3 [simp] = 
+       evala.dom_subset [THEN subsetD, THEN SigmaD2]
 
-    while0   "[| c \\<in> com; <b, sigma> -b-> 0 |] ==> 
-             <while b do c,sigma> -c-> sigma "
+
+(*** type_intros for evalb ***)
 
-    while1   "[| c \\<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; 
-                <while b do c, sigma2> -c-> sigma1 |] ==> 
-             <while b do c, sigma> -c-> sigma1 "
+lemmas evalb_1 [simp] = 
+       evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
+lemmas evalb_2 [simp] = 
+       evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
+lemmas evalb_3 [simp] = 
+       evalb.dom_subset [THEN subsetD, THEN SigmaD2]
+
+(*** type_intros for evalc ***)
 
-  type_intrs "com.intrs @ [update_type]"
-  type_elims "[make_elim(evala.dom_subset RS subsetD),   
-               make_elim(evalb.dom_subset RS subsetD) ]"
+lemmas evalc_1 [simp] = 
+       evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1]
+lemmas evalc_2 [simp] = 
+       evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2]
+lemmas evalc_3 [simp] = 
+       evalc.dom_subset [THEN subsetD, THEN SigmaD2]
+
+inductive_cases evala_N_E [elim!]: "<N(n),sigma> -a-> i"
+inductive_cases evala_X_E [elim!]: "<X(x),sigma> -a-> i"
+inductive_cases evala_Op1_E [elim!]: "<Op1(f,e),sigma> -a-> i"
+inductive_cases evala_Op2_E [elim!]: "<Op2(f,a1,a2),sigma>  -a-> i"
 
 end
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/IMP/Denotation.ML
--- a/src/ZF/IMP/Denotation.ML	Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(*  Title:      ZF/IMP/Denotation.ML
-    ID:         $Id$
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
-    Copyright   1994 TUM
-*)
-
-(** Rewrite Rules for A,B,C **)
-Addsimps [A_nat_def,A_loc_def,A_op1_def,A_op2_def];
-Addsimps [B_true_def,B_false_def,B_op_def,B_not_def,B_and_def,B_or_def];
-Addsimps [C_skip_def,C_assign_def,C_comp_def,C_if_def,C_while_def]; 
-
-(** Type_intr for A **)
-
-Goal "[|a \\<in> aexp; sigma \\<in> loc->nat|] ==> A(a,sigma):nat";
-by (etac aexp.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (claset() addSIs [apply_type])));
-qed "A_type";
-
-(** Type_intr for B **)
-
-Goal "[|b \\<in> bexp; sigma \\<in> loc->nat|] ==> B(b,sigma):bool";
-by (etac bexp.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (claset() addSIs [apply_type,A_type]@bool_typechecks)));
-qed "B_type";
-
-(** C_subset **)
-
-Goal "c \\<in> com ==> C(c) \\<subseteq> (loc->nat)*(loc->nat)";
-by (etac com.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (claset() addDs [lfp_subset RS subsetD])));
-qed "C_subset";
-
-(** Type_elims for C **)
-
-Goal "[| <x,y>:C(c); c \\<in> com |] ==> x \\<in> loc->nat & y \\<in> loc->nat";
-by (blast_tac (claset() addDs [C_subset RS subsetD]) 1);
-qed "C_type_D";
-
-Goal "[| x \\<in> C(c); c \\<in> com |] ==> fst(x):loc->nat";
-by (dtac (C_subset RS subsetD) 1);
-by (atac 1);
-by (etac SigmaE 1);
-by (Asm_simp_tac 1);
-qed "C_type_fst";
-
-AddDs [C_type_D, C_type_fst];
-
-(** bnd_mono (nat->nat*nat->nat,Gamma(b,c) **)
-
-Goalw [bnd_mono_def,Gamma_def]
-     "c \\<in> com ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,c))";
-by (Blast_tac 1);
-qed "Gamma_bnd_mono";
-
-(** End ***)
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/IMP/Denotation.thy
--- a/src/ZF/IMP/Denotation.thy	Fri Dec 28 10:10:55 2001 +0100
+++ b/src/ZF/IMP/Denotation.thy	Fri Dec 28 10:11:14 2001 +0100
@@ -6,41 +6,82 @@
 Denotational semantics of expressions & commands
 *)
 
-Denotation = Com + 
+theory Denotation = Com:
+
 
 consts
-  A     :: i => i => i
-  B     :: i => i => i
-  C     :: i => i
-  Gamma :: [i,i,i] => i
+  A     :: "i => i => i"
+  B     :: "i => i => i"
+  C     :: "i => i"
+
+constdefs
+  Gamma :: "[i,i,i] => i"
+    "Gamma(b,cden) == (%phi.{io \<in> (phi O cden). B(b,fst(io))=1} Un 
+                         {io \<in> id(loc->nat). B(b,fst(io))=0})"
 
-rules   (*NOT definitional*)
-  A_nat_def     "A(N(n)) == (%sigma. n)"
-  A_loc_def     "A(X(x)) == (%sigma. sigma`x)" 
-  A_op1_def     "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
-  A_op2_def     "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
+primrec
+    "A(N(n), sigma) = n"
+    "A(X(x), sigma) = sigma`x" 
+    "A(Op1(f,a), sigma) = f`A(a,sigma)"
+    "A(Op2(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
+
+
+primrec
+    "B(true, sigma) = 1"
+    "B(false, sigma) = 0"
+    "B(ROp(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>" 
+    "B(noti(b), sigma) = not(B(b,sigma))"
+    "B(b0 andi b1, sigma) = B(b0,sigma) and B(b1,sigma)"
+    "B(b0 ori b1, sigma) = B(b0,sigma) or B(b1,sigma)"
 
 
-  B_true_def    "B(true) == (%sigma. 1)"
-  B_false_def   "B(false) == (%sigma. 0)"
-  B_op_def      "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)" 
+primrec
+    "C(skip) = id(loc->nat)"
+
+    "C(x asgt a) = {io:(loc->nat)*(loc->nat). 
+                    snd(io) = fst(io)(x := A(a,fst(io)))}"
+
+    "C(c0 ; c1) = C(c1) O C(c0)"
+
+    "C(ifc b then c0 else c1) = {io \<in> C(c0). B(b,fst(io))=1} Un 
+                                             {io \<in> C(c1). B(b,fst(io))=0}"
+
+    "C(while b do c) = lfp((loc->nat)*(loc->nat), Gamma(b,C(c)))"
+
+
+(** Type_intr for A **)
+
+lemma A_type [TC]: "[|a \<in> aexp; sigma \<in> loc->nat|] ==> A(a,sigma) \<in> nat"
+by (erule aexp.induct, simp_all)
 
 
-  B_not_def     "B(noti(b)) == (%sigma. not(B(b,sigma)))"
-  B_and_def     "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
-  B_or_def      "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
+(** Type_intr for B **)
+
+lemma B_type [TC]: "[|b \<in> bexp; sigma \<in> loc->nat|] ==> B(b,sigma) \<in> bool"
+by (erule bexp.induct, simp_all)
 
-  C_skip_def    "C(skip) == id(loc->nat)"
-  C_assign_def  "C(x asgt a) == {io:(loc->nat)*(loc->nat). 
-                               snd(io) = fst(io)(x := A(a,fst(io)))}"
+(** C_subset **)
+
+lemma C_subset: "c \<in> com ==> C(c) \<subseteq> (loc->nat)*(loc->nat)"
+apply (erule com.induct)
+apply simp_all
+apply (blast dest: lfp_subset [THEN subsetD])+
+done
 
-  C_comp_def    "C(c0 ; c1) == C(c1) O C(c0)"
-  C_if_def      "C(ifc b then c0 else c1) == {io \\<in> C(c0). B(b,fst(io))=1} Un 
-                                             {io \\<in> C(c1). B(b,fst(io))=0}"
+(** Type_elims for C **)
+
+lemma C_type_D [dest]:
+     "[| <x,y> \<in> C(c); c \<in> com |] ==> x \<in> loc->nat & y \<in> loc->nat"
+by (blast dest: C_subset [THEN subsetD])
 
-  Gamma_def     "Gamma(b,c) == (%phi.{io \\<in> (phi O C(c)). B(b,fst(io))=1} Un 
-                                     {io \\<in> id(loc->nat). B(b,fst(io))=0})"
+lemma C_type_fst [dest]: "[| x \<in> C(c); c \<in> com |] ==> fst(x) \<in> loc->nat"
+by (auto dest!: C_subset [THEN subsetD])
+
+(** bnd_mono (nat->nat*nat->nat,Gamma(b,c) **)
 
-  C_while_def   "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
+lemma Gamma_bnd_mono: 
+     "cden <= (loc->nat)*(loc->nat) 
+      ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,cden))"
+by (unfold bnd_mono_def Gamma_def, blast)
 
 end
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/IMP/Equiv.ML
--- a/src/ZF/IMP/Equiv.ML	Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-(*  Title:      ZF/IMP/Equiv.ML
-    ID:         $Id$
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
-    Copyright   1994 TUM
-*)
-
-Goal "[| a \\<in> aexp; sigma: loc -> nat |] ==> \
-\        <a,sigma> -a-> n <-> A(a,sigma) = n";
-by (res_inst_tac [("x","n")] spec 1);                       (* quantify n *)
-by (etac aexp.induct 1);
-by (ALLGOALS (fast_tac (claset() addSIs evala.intrs
-                                 addSEs aexp_elim_cases 
-                                 addss (simpset()))));
-qed "aexp_iff";
-
-
-val aexp1 = aexp_iff RS iffD1;
-val aexp2 = aexp_iff RS iffD2;
-
-
-val bexp_elim_cases = 
-   [
-    evalb.mk_cases "<true,sigma> -b-> x",
-    evalb.mk_cases "<false,sigma> -b-> x",
-    evalb.mk_cases "<ROp(f,a0,a1),sigma> -b-> x",
-    evalb.mk_cases "<noti(b),sigma> -b-> x",
-    evalb.mk_cases "<b0 andi b1,sigma> -b-> x",
-    evalb.mk_cases "<b0 ori b1,sigma> -b-> x"
-   ];
-
-
-Goal "[| b \\<in> bexp; sigma: loc -> nat |] ==> \
-\        <b,sigma> -b-> w <-> B(b,sigma) = w";
-by (res_inst_tac [("x","w")] spec 1);
-by (etac bexp.induct 1);
-by (ALLGOALS (fast_tac (claset() addSIs evalb.intrs
-                                 addSEs bexp_elim_cases 
-                                 addss (simpset() addsimps [aexp_iff]))));
-qed "bexp_iff";
-
-val bexp1 = bexp_iff RS iffD1;
-val bexp2 = bexp_iff RS iffD2;
-
-
-Goal "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \\<in> C(c)";
-by (etac evalc.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [bexp1])));
-(* skip *)
-by (Fast_tac 1);
-(* assign *)
-by (asm_full_simp_tac (simpset() addsimps 
-		       [aexp1, update_type] @ op_type_intrs) 1);
-(* comp *)
-by (Fast_tac 1);
-(* while *)
-by (etac (Gamma_bnd_mono RS lfp_unfold RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
-by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
-(* recursive case of while *)
-by (etac (Gamma_bnd_mono RS lfp_unfold RS ssubst) 1);
-by (asm_full_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
-by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
-val com1 = result();
-
-
-AddSIs [aexp2,bexp2,B_type,A_type];
-AddIs  evalc.intrs;
-
-
-Goal "c \\<in> com ==> \\<forall>x \\<in> C(c). <c,fst(x)> -c-> snd(x)";
-by (etac com.induct 1);
-(* comp *)
-by (Force_tac 3); 
-(* assign *)
-by (Force_tac 2); 
-(* skip *)
-by (Force_tac 1); 
-(* while *)
-by Safe_tac;
-by (ALLGOALS Asm_full_simp_tac);
-by (EVERY1 [ftac Gamma_bnd_mono , etac induct, atac]);
-by (rewtac Gamma_def);  
-by Safe_tac;
-by (EVERY1 [dtac bspec, atac]);
-by (ALLGOALS Asm_full_simp_tac);
-(* while, if *)
-by (ALLGOALS Blast_tac);
-val com2 = result();
-
-
-(**** Proof of Equivalence ****)
-
-Goal "\\<forall>c \\<in> com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
-by (fast_tac (claset() addIs [C_subset RS subsetD]
-		       addEs [com2 RS bspec]
-		       addDs [com1]
-		       addss (simpset())) 1);
-val com_equivalence = result();
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/IMP/Equiv.thy
--- a/src/ZF/IMP/Equiv.thy	Fri Dec 28 10:10:55 2001 +0100
+++ b/src/ZF/IMP/Equiv.thy	Fri Dec 28 10:11:14 2001 +0100
@@ -4,4 +4,84 @@
     Copyright   1994 TUM
 *)
 
-Equiv = Denotation + Com
+theory Equiv = Denotation + Com:
+
+lemma aexp_iff [rule_format]:
+     "[| a \<in> aexp; sigma: loc -> nat |] 
+      ==> ALL n. <a,sigma> -a-> n <-> A(a,sigma) = n"
+apply (erule aexp.induct) 
+apply (force intro!: evala.intros)+
+done
+
+declare aexp_iff [THEN iffD1, simp]
+        aexp_iff [THEN iffD2, intro!]
+
+inductive_cases [elim!]: "<true,sigma> -b-> x"
+inductive_cases [elim!]: "<false,sigma> -b-> x"
+inductive_cases [elim!]: "<ROp(f,a0,a1),sigma> -b-> x"
+inductive_cases [elim!]: "<noti(b),sigma> -b-> x"
+inductive_cases [elim!]: "<b0 andi b1,sigma> -b-> x"
+inductive_cases [elim!]: "<b0 ori b1,sigma> -b-> x"
+
+
+lemma bexp_iff [rule_format]:
+     "[| b \<in> bexp; sigma: loc -> nat |] 
+      ==> ALL w. <b,sigma> -b-> w <-> B(b,sigma) = w"
+apply (erule bexp.induct) 
+apply (auto intro!: evalb.intros)
+done
+
+declare bexp_iff [THEN iffD1, simp]
+        bexp_iff [THEN iffD2, intro!]
+
+lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)"
+apply (erule evalc.induct)
+apply simp_all
+(* skip *)
+apply fast
+(* assign *)
+apply (simp add: update_type)
+(* comp *)
+apply fast
+(* while *)
+apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
+apply (simp add: Gamma_def)
+apply (force ) 
+(* recursive case of while *)
+apply (erule Gamma_bnd_mono [THEN lfp_unfold, THEN ssubst, OF C_subset])
+apply (simp add: Gamma_def)
+apply auto
+done
+
+
+declare B_type [intro!] A_type [intro!]
+declare evalc.intros [intro]
+
+
+lemma com2 [rule_format]: "c \<in> com ==> \<forall>x \<in> C(c). <c,fst(x)> -c-> snd(x)"
+apply (erule com.induct)
+(* skip *)
+apply force
+(* assign *)
+apply force
+(* comp *)
+apply force
+(* while *)
+apply safe
+apply simp_all
+apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
+apply (unfold Gamma_def)
+apply force
+(* if *)
+apply auto
+done
+
+
+(**** Proof of Equivalence ****)
+
+lemma com_equivalence:
+     "\<forall>c \<in> com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}"
+by (force intro: C_subset [THEN subsetD] elim: com2 dest: com1)
+
+end
+
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Fri Dec 28 10:10:55 2001 +0100
+++ b/src/ZF/IsaMakefile	Fri Dec 28 10:11:14 2001 +0100
@@ -74,7 +74,7 @@
 
 ZF-Coind: ZF $(LOG)/ZF-Coind.gz
 
-$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \
+$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.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
@@ -84,8 +84,8 @@
 
 ZF-IMP: ZF $(LOG)/ZF-IMP.gz
 
-$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \
-  IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/ROOT.ML
+$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy \
+  IMP/Denotation.thy IMP/Equiv.thy IMP/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/ZF IMP
 
 
@@ -131,9 +131,9 @@
 ZF-ex: ZF $(LOG)/ZF-ex.gz
 
 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML \
-  ex/BinEx.thy ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
-  ex/Limit.ML ex/Limit.thy ex/LList.ML ex/LList.thy ex/Primes.ML ex/Primes.thy \
-  ex/NatSum.ML ex/NatSum.thy ex/Ramsey.ML ex/Ramsey.thy ex/misc.thy
+  ex/BinEx.thy ex/CoUnit.thy ex/Commutation.thy \
+  ex/Limit.ML ex/Limit.thy ex/LList.thy ex/Primes.thy \
+  ex/NatSum.thy ex/Ramsey.thy ex/misc.thy
 	@$(ISATOOL) usedir $(OUT)/ZF ex
 
 
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/ex/Commutation.ML
--- a/src/ZF/ex/Commutation.ML	Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-(*  Title:      HOL/Lambda/Commutation.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow & Sidi Ould Ehmety
-    Copyright   1995  TU Muenchen
-
-Commutation theory for proving the Church Rosser theorem
-	ported from Isabelle/HOL  by Sidi Ould Ehmety
-*)
-
-Goalw [square_def] "square(r,s,t,u) ==> square(s,r,u,t)";
-by (Blast_tac 1);
-qed "square_sym";                
-
-
-Goalw [square_def] "[| square(r,s,t,u); t \\<subseteq> t' |] ==> square(r,s,t',u)";
-by (Blast_tac 1);
-qed "square_subset"; 
-
-
-Goalw [square_def]
- "field(s)<=field(t)==> square(r,s,s,t) --> square(r^*,s,s,t^*)";
-by (Clarify_tac 1);
-by (etac rtrancl_induct 1);
-by (blast_tac (claset()  addIs [rtrancl_refl]) 1);
-by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
-qed_spec_mp "square_rtrancl";                 
-
-(* A special case of square_rtrancl_on *)
-Goalw [diamond_def, commute_def, strip_def]
- "diamond(r) ==> strip(r)";
-by (rtac square_rtrancl 1);
-by (ALLGOALS(Asm_simp_tac));
-qed "diamond_strip";
-
-(*** commute ***)
-
-Goalw [commute_def] 
-    "commute(r,s) ==> commute(s,r)";
-by (blast_tac (claset() addIs [square_sym]) 1);
-qed "commute_sym";
-
-Goalw [commute_def] 
-"commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)";
-by (Clarify_tac 1);
-by (rtac square_rtrancl 1);
-by (rtac square_sym  2);
-by (rtac square_rtrancl 2);
-by (rtac square_sym  3);
-by (ALLGOALS(asm_simp_tac 
-        (simpset() addsimps [rtrancl_field])));
-qed_spec_mp "commute_rtrancl";
-
-
-Goalw [strip_def,confluent_def, diamond_def]
-"strip(r) ==> confluent(r)";
-by (dtac commute_rtrancl 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() 
-   addsimps [rtrancl_field])));
-qed "strip_confluent";
-
-
-Goalw [commute_def,square_def]
-  "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)";
-by (Blast_tac 1);
-qed "commute_Un";
-
-
-Goalw [diamond_def]
-  "[| diamond(r); diamond(s); commute(r, s) |] \
-\ ==> diamond(r Un s)";
-by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
-qed "diamond_Un";                                           
-
-
-Goalw [diamond_def,confluent_def] 
-    "diamond(r) ==> confluent(r)";
-by (etac commute_rtrancl 1);
-by (Simp_tac 1);
-qed "diamond_confluent";            
-
-
-Goalw [confluent_def]
- "[| confluent(r); confluent(s); commute(r^*, s^*); \
-\           r \\<subseteq> Sigma(A,B); s \\<subseteq> Sigma(C,D) |] ==> confluent(r Un s)";
-by (rtac (rtrancl_Un_rtrancl RS subst) 1);
-by (blast_tac (claset() addDs [diamond_Un] 
-     addIs [rewrite_rule [confluent_def] diamond_confluent]) 3);
-by Auto_tac;
-qed "confluent_Un";
-
-
-Goal
- "[| diamond(r); s \\<subseteq> r; r<= s^* |] ==> confluent(s)";
-by (dresolve_tac [rtrancl_subset RS sym] 1);
-by (assume_tac 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps[confluent_def])));
-by (resolve_tac [rewrite_rule [confluent_def] diamond_confluent] 1);
-by (Asm_simp_tac 1);
-qed "diamond_to_confluence";               
-
-(*** Church_Rosser ***)
-
-Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]
-  "Church_Rosser(r) ==> confluent(r)";
-by Auto_tac;
-by (dtac converseI 1);
-by (full_simp_tac (simpset() 
-                   addsimps [rtrancl_converse RS sym]) 1);
-by (dres_inst_tac [("x", "b")] spec 1);
-by (dres_inst_tac [("x1", "c")] (spec RS mp) 1);
-by (res_inst_tac [("b", "a")] rtrancl_trans 1);
-by (REPEAT(blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1));
-qed "Church_Rosser1";
-
-
-Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]  
-"confluent(r) ==> Church_Rosser(r)";
-by Auto_tac;
-by (ftac fieldI1 1);
-by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1);
-by (etac rtrancl_induct 1);
-by (ALLGOALS(Clarify_tac));
-by (blast_tac (claset() addIs [rtrancl_refl]) 1);
-by (blast_tac (claset() delrules [rtrancl_refl] 
-                        addIs [r_into_rtrancl, rtrancl_trans]) 1);
-qed "Church_Rosser2";
-
-
-Goal "Church_Rosser(r) <-> confluent(r)";
-by (blast_tac(claset() addIs [Church_Rosser1,Church_Rosser2]) 1);
-qed "Church_Rosser";
\ No newline at end of file
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/ex/LList.ML
--- a/src/ZF/ex/LList.ML	Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,195 +0,0 @@
-(*  Title:      ZF/ex/LList.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Codatatype definition of Lazy Lists
-*)
-
-(*These commands cause classical reasoning to regard the subset relation
-  as primitive, not reducing it to membership*)
-  
-Delrules [subsetI, subsetCE];
-AddSIs [subset_refl, cons_subsetI, subset_consI, 
-	Union_least, UN_least, Un_least, 
-	Inter_greatest, Int_greatest, RepFun_subset,
-	Un_upper1, Un_upper2, Int_lower1, Int_lower2];
-
-(*An elimination rule, for type-checking*)
-val LConsE = llist.mk_cases "LCons(a,l) \\<in> llist(A)";
-
-(*Proving freeness results*)
-val LCons_iff      = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
-val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)";
-
-Goal "llist(A) = {0} <+> (A <*> llist(A))";
-let open llist  val rew = rewrite_rule con_defs in  
-by (fast_tac (claset() addSIs (subsetI ::map rew intrs) addEs [rew elim]) 1)
-end;
-qed "llist_unfold";
-
-(*** Lemmas to justify using "llist" in other recursive type definitions ***)
-
-Goalw llist.defs "A \\<subseteq> B ==> llist(A) \\<subseteq> llist(B)";
-by (rtac gfp_mono 1);
-by (REPEAT (rtac llist.bnd_mono 1));
-by (REPEAT (ares_tac (quniv_mono::basic_monos) 1));
-qed "llist_mono";
-
-(** Closure of quniv(A) under llist -- why so complex?  Its a gfp... **)
-
-AddSIs [QPair_Int_Vset_subset_UN RS subset_trans, 
-                                 QPair_subset_univ,
-                                 empty_subsetI, one_in_quniv RS qunivD];
-AddSDs [qunivD];
-AddSEs [Ord_in_Ord];
-
-Goal "Ord(i) ==> \\<forall>l \\<in> llist(quniv(A)). l Int Vset(i) \\<subseteq> univ(eclose(A))";
-by (etac trans_induct 1);
-by (rtac ballI 1);
-by (etac llist.elim 1);
-by (rewrite_goals_tac ([QInl_def,QInr_def]@llist.con_defs));
-(*LNil case*)
-by (Asm_simp_tac 1);
-(*LCons case*)
-by (deepen_tac (claset() addIs [Ord_trans, Int_lower1 RS subset_trans]) 2 1);
-qed "llist_quniv_lemma";
-
-Goal "llist(quniv(A)) \\<subseteq> quniv(A)";
-by (rtac (qunivI RS subsetI) 1);
-by (rtac Int_Vset_subset 1);
-by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
-qed "llist_quniv";
-
-bind_thm ("llist_subset_quniv",
-    (llist_mono RS (llist_quniv RSN (2,subset_trans))));
-
-
-(*** Lazy List Equality: lleq ***)
-
-AddSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono];
-AddSEs [Ord_in_Ord, Pair_inject];
-
-(*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
-Goal "Ord(i) ==> \\<forall>l l'. <l,l'> \\<in> lleq(A) --> l Int Vset(i) \\<subseteq> l'";
-by (etac trans_induct 1);
-by (REPEAT (resolve_tac [allI, impI] 1));
-by (etac lleq.elim 1);
-by (rewrite_goals_tac (QInr_def::llist.con_defs));
-by Safe_tac;
-by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
-qed "lleq_Int_Vset_subset_lemma";
-
-bind_thm ("lleq_Int_Vset_subset",
-        (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp));
-
-
-(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
-val [prem] = goal LList.thy "<l,l'> \\<in> lleq(A) ==> <l',l> \\<in> lleq(A)";
-by (rtac (prem RS converseI RS lleq.coinduct) 1);
-by (rtac (lleq.dom_subset RS converse_type) 1);
-by Safe_tac;
-by (etac lleq.elim 1);
-by (ALLGOALS Fast_tac);
-qed "lleq_symmetric";
-
-Goal "<l,l'> \\<in> lleq(A) ==> l=l'";
-by (rtac equalityI 1);
-by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
-     ORELSE etac lleq_symmetric 1));
-qed "lleq_implies_equal";
-
-val [eqprem,lprem] = goal LList.thy
-    "[| l=l';  l \\<in> llist(A) |] ==> <l,l'> \\<in> lleq(A)";
-by (res_inst_tac [("X", "{<l,l>. l \\<in> llist(A)}")] lleq.coinduct 1);
-by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
-by Safe_tac;
-by (etac llist.elim 1);
-by (ALLGOALS Fast_tac);
-qed "equal_llist_implies_leq";
-
-
-(*** Lazy List Functions ***)
-
-(*Examples of coinduction for type-checking and to prove llist equations*)
-
-(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
-
-Goalw llist.con_defs "bnd_mono(univ(a), %l. LCons(a,l))";
-by (rtac bnd_monoI 1);
-by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
-by (REPEAT (ares_tac [subset_refl, A_subset_univ, 
-                      QInr_subset_univ, QPair_subset_univ] 1));
-qed "lconst_fun_bnd_mono";
-
-(* lconst(a) = LCons(a,lconst(a)) *)
-bind_thm ("lconst",
-    ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_unfold));
-
-val lconst_subset = lconst_def RS def_lfp_subset;
-
-bind_thm ("member_subset_Union_eclose", (arg_into_eclose RS Union_upper));
-
-Goal "a \\<in> A ==> lconst(a) \\<in> quniv(A)";
-by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
-by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
-qed "lconst_in_quniv";
-
-Goal "a \\<in> A ==> lconst(a): llist(A)";
-by (rtac (singletonI RS llist.coinduct) 1);
-by (etac (lconst_in_quniv RS singleton_subsetI) 1);
-by (fast_tac (claset() addSIs [lconst]) 1);
-qed "lconst_type";
-
-(*** flip --- equations merely assumed; certain consequences proved ***)
-
-Addsimps [flip_LNil, flip_LCons, not_type];
-
-goal QUniv.thy "!!b. b \\<in> bool ==> b Int X \\<subseteq> univ(eclose(A))";
-by (fast_tac (claset() addIs [Int_lower1 RS subset_trans] addSEs [boolE]) 1);
-qed "bool_Int_subset_univ";
-
-AddSIs [not_type];
-AddIs  [bool_Int_subset_univ];
-
-(*Reasoning borrowed from lleq.ML; a similar proof works for all
-  "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
-Goal "Ord(i) ==> \\<forall>l \\<in> llist(bool). flip(l) Int Vset(i) \\<subseteq> \
-\                   univ(eclose(bool))";
-by (etac trans_induct 1);
-by (rtac ballI 1);
-by (etac llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS 
-    (asm_simp_tac (simpset() addsimps [QInl_def,QInr_def] @ llist.con_defs)));
-(*LCons case*)
-by (deepen_tac (claset() addIs [Ord_trans, Int_lower1 RS subset_trans]) 2 1);
-qed "flip_llist_quniv_lemma";
-
-Goal "l \\<in> llist(bool) ==> flip(l) \\<in> quniv(bool)";
-by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
-by (REPEAT (assume_tac 1));
-qed "flip_in_quniv";
-
-val [prem] = goal LList.thy "l \\<in> llist(bool) ==> flip(l): llist(bool)";
-by (res_inst_tac [("X", "{flip(l) . l \\<in> llist(bool)}")]
-       llist.coinduct 1);
-by (rtac (prem RS RepFunI) 1);
-by (fast_tac (claset() addSIs [flip_in_quniv]) 1);
-by (etac RepFunE 1);
-by (etac llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
-qed "flip_type";
-
-val [prem] = goal LList.thy
-    "l \\<in> llist(bool) ==> flip(flip(l)) = l";
-by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l \\<in> llist(bool)}")]
-       (lleq.coinduct RS lleq_implies_equal) 1);
-by (rtac (prem RS RepFunI) 1);
-by (fast_tac (claset() addSIs [flip_type]) 1);
-by (etac RepFunE 1);
-by (etac llist.elim 1);
-by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [flip_type, not_not]) 1);
-qed "flip_flip";
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/ex/NatSum.ML
--- a/src/ZF/ex/NatSum.ML	Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  Title:      HOL/ex/NatSum.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow & Lawrence C Paulson
-
-Summing natural numbers, squares, cubes, etc.
-
-Originally demonstrated permutative rewriting, but add_ac is no longer needed
-  thanks to new simprocs.
-
-Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
-  http://www.research.att.com/~njas/sequences/
-*)
-
-Addsimps [zadd_zmult_distrib, zadd_zmult_distrib2];
-Addsimps [zdiff_zmult_distrib, zdiff_zmult_distrib2];
-
-(*The sum of the first n odd numbers equals n squared.*)
-Goal "n \\<in> nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_odds";
-
-(*The sum of the first n odd squares*)
-Goal "n \\<in> nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
-\     $#n $* (#4 $* $#n $* $#n $- #1)";
-by (induct_tac "n" 1);
-by Auto_tac;  
-qed "sum_of_odd_squares";
-
-(*The sum of the first n odd cubes*)
-Goal "n \\<in> nat \
-\     ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
-\         $#n $* $#n $* (#2 $* $#n $* $#n $- #1)";
-by (induct_tac "n" 1);
-by Auto_tac;  
-qed "sum_of_odd_cubes";
-
-(*The sum of the first n positive integers equals n(n+1)/2.*)
-Goal "n \\<in> nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_naturals";
-
-Goal "n \\<in> nat ==> #6 $* sum (%i. i$*i, succ(n)) = \
-\                $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_squares";
-
-Goal "n \\<in> nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = \
-\                $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_cubes";
-
-(** Sum of fourth powers **)
-
-Goal "n \\<in> nat ==> \
-\     #30 $* sum (%i. i$*i$*i$*i, succ(n)) = \
-\     $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* \
-\     (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_fourth_powers";
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/ex/Primes.ML
--- a/src/ZF/ex/Primes.ML	Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,435 +0,0 @@
-(*  Title:      ZF/ex/Primes.ML
-    ID:         $Id$
-    Author:     Christophe Tabacznyj and Lawrence C Paulson
-    Copyright   1996  University of Cambridge
-
-The "divides" relation, the greatest common divisor and Euclid's algorithm
-*)
-
-(************************************************)
-(** Divides Relation                           **)
-(************************************************)
-
-Goalw [dvd_def] "m dvd n ==> m \\<in> nat & n \\<in> nat & (\\<exists>k \\<in> nat. n = m#*k)";
-by (assume_tac 1);
-qed "dvdD";
-
-Goal "!!P. [|m dvd n;  !!k. [|m \\<in> nat; n \\<in> nat; k \\<in> nat; n = m#*k|] ==> P|] \
-\          ==> P";
-by (blast_tac (claset() addSDs [dvdD]) 1); 
-qed "dvdE";
-
-bind_thm ("dvd_imp_nat1", dvdD RS conjunct1);
-bind_thm ("dvd_imp_nat2", dvdD RS conjunct2 RS conjunct1);
-
-
-Goalw [dvd_def] "m \\<in> nat ==> m dvd 0";
-by (fast_tac (claset() addIs [nat_0I, mult_0_right RS sym]) 1);
-qed "dvd_0_right";
-Addsimps [dvd_0_right];
-
-Goalw [dvd_def] "0 dvd m ==> m = 0";
-by (fast_tac (claset() addss (simpset())) 1);
-qed "dvd_0_left";
-
-Goalw [dvd_def] "m \\<in> nat ==> m dvd m";
-by (fast_tac (claset() addIs [nat_1I, mult_1_right RS sym]) 1);
-qed "dvd_refl";
-Addsimps [dvd_refl];
-
-Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
-by (fast_tac (claset() addIs [mult_assoc, mult_type] ) 1);
-qed "dvd_trans";
-
-Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
-by (fast_tac (claset() addDs [mult_eq_self_implies_10]
-                    addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
-qed "dvd_anti_sym";
-
-Goalw [dvd_def] "[|(i#*j) dvd k; i \\<in> nat|] ==> i dvd k";
-by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
-by (Blast_tac 1);
-qed "dvd_mult_left";
-
-Goalw [dvd_def] "[|(i#*j) dvd k; j \\<in> nat|] ==> j dvd k";
-by (Clarify_tac 1);
-by (res_inst_tac [("x","i#*k")] bexI 1);
-by (simp_tac (simpset() addsimps mult_ac) 1);
-by (rtac mult_type 1); 
-qed "dvd_mult_right";
-
-
-(************************************************)
-(** Greatest Common Divisor                    **)
-(************************************************)
-
-(* GCD by Euclid's Algorithm *)
-
-Goalw [gcd_def] "gcd(m,0) = natify(m)";
-by (stac transrec 1);
-by (Asm_simp_tac 1);
-qed "gcd_0";
-Addsimps [gcd_0];
-
-Goal "gcd(natify(m),n) = gcd(m,n)";
-by (simp_tac (simpset() addsimps [gcd_def]) 1); 
-qed "gcd_natify1";
-
-Goal "gcd(m, natify(n)) = gcd(m,n)";
-by (simp_tac (simpset() addsimps [gcd_def]) 1); 
-qed "gcd_natify2";
-Addsimps [gcd_natify1,gcd_natify2];
-
-Goalw [gcd_def]
-    "[| 0<n;  n \\<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)";
-by (res_inst_tac [("P", "%z. ?left(z) = ?right")] (transrec RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq RS not_sym,
-                                      mod_less_divisor RS ltD]) 1);
-qed "gcd_non_0_raw";
-
-Goal "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)";
-by (cut_inst_tac [("m","m"),("n","natify(n)")] gcd_non_0_raw 1);
-by Auto_tac; 
-qed "gcd_non_0";
-
-Goal "gcd(m,1) = 1";
-by (asm_simp_tac (simpset() addsimps [gcd_non_0]) 1); 
-qed "gcd_1";
-Addsimps [gcd_1];
-
-Goalw [dvd_def] "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)";
-by (fast_tac (claset() addIs [add_mult_distrib_left RS sym, add_type]) 1);
-qed "dvd_add";
-
-Goalw [dvd_def] "k dvd n ==> k dvd (m #* n)";
-by (fast_tac (claset() addIs [mult_left_commute, mult_type]) 1);
-qed "dvd_mult";
-
-Goal "k dvd m ==> k dvd (m #* n)";
-by (stac mult_commute 1); 
-by (blast_tac (claset() addIs [dvd_mult]) 1); 
-qed "dvd_mult2";
-
-(* k dvd (m*k) *)
-bind_thm ("dvdI1", dvd_refl RS dvd_mult);
-bind_thm ("dvdI2", dvd_refl RS dvd_mult2);
-Addsimps [dvdI1, dvdI2];
-
-Goal "[| a \\<in> nat; b \\<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a";
-by (div_undefined_case_tac "b=0" 1);
-by (blast_tac 
-    (claset() addIs [mod_div_equality RS subst]
-              addEs  [dvdE]
-              addSIs [dvd_add, dvd_mult, mult_type,mod_type,div_type]) 1);
-qed "dvd_mod_imp_dvd_raw";
-
-Goal "[| k dvd (a mod b); k dvd b; a \\<in> nat |] ==> k dvd a";
-by (cut_inst_tac [("b","natify(b)")] dvd_mod_imp_dvd_raw 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [dvd_def]) 1);  
-qed "dvd_mod_imp_dvd";
-
-(*Imitating TFL*)
-Goal "[| n \\<in> nat; \
-\        \\<forall>m \\<in> nat. P(m,0); \
-\        \\<forall>m \\<in> nat. \\<forall>n \\<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |] \
-\     ==> \\<forall>m \\<in> nat. P (m,n)";
-by (eres_inst_tac [("i","n")] complete_induct 1);
-by (case_tac "x=0" 1);
-by (Asm_simp_tac 1); 
-by (Clarify_tac 1); 
-by (dres_inst_tac [("x1","m"),("x","x")] (bspec RS bspec) 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_0_lt_iff])));
-by (blast_tac (claset() addIs [mod_less_divisor RS ltD]) 1); 
-qed_spec_mp "gcd_induct_lemma";
-
-Goal "!!P. [| m \\<in> nat; n \\<in> nat; \
-\        !!m. m \\<in> nat ==> P(m,0); \
-\        !!m n. [|m \\<in> nat; n \\<in> nat; 0<n; P(n, m mod n)|] ==> P(m,n) |] \
-\     ==> P (m,n)";
-by (blast_tac (claset() addIs [gcd_induct_lemma]) 1); 
-qed "gcd_induct"; 
-
-
-(* gcd type *)
-
-Goal "gcd(m, n) \\<in> nat";
-by (subgoal_tac "gcd(natify(m), natify(n)) \\<in> nat" 1);
-by (Asm_full_simp_tac 1); 
-by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_induct 1); 
-by Auto_tac; 
-by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1); 
-qed "gcd_type";
-Addsimps [gcd_type];
-
-(* Property 1: gcd(a,b) divides a and b *)
-
-Goal "[| m \\<in> nat; n \\<in> nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); 
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0])));
-by (blast_tac
-    (claset() addIs [dvd_mod_imp_dvd_raw, nat_into_Ord RS Ord_0_lt]) 1);
-qed "gcd_dvd_both";
-
-Goal "m \\<in> nat ==> gcd(m,n) dvd m";
-by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_dvd_both 1); 
-by Auto_tac; 
-qed "gcd_dvd1";
-Addsimps [gcd_dvd1];
-
-Goal "n \\<in> nat ==> gcd(m,n) dvd n";
-by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_dvd_both 1); 
-by Auto_tac; 
-qed "gcd_dvd2";
-Addsimps [gcd_dvd2];
-
-(* if f divides a and b then f divides gcd(a,b) *)
-
-Goalw [dvd_def] "[| f dvd a; f dvd b |] ==> f dvd (a mod b)";
-by (div_undefined_case_tac "b=0" 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1);  
-qed "dvd_mod";
-
-(* Property 2: for all a,b,f naturals, 
-               if f divides a and f divides b then f divides gcd(a,b)*)
-
-Goal "[| m \\<in> nat; n \\<in> nat; f \\<in> nat |]   \
-\     ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_non_0, dvd_mod])));
-qed_spec_mp "gcd_greatest_raw";
-
-Goal "[| f dvd m;  f dvd n;  f \\<in> nat |] ==> f dvd gcd(m,n)";
-by (rtac gcd_greatest_raw 1); 
-by (auto_tac (claset(), simpset() addsimps [dvd_def])); 
-qed "gcd_greatest";
-
-Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
-\     ==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)";
-by (blast_tac (claset() addSIs [gcd_greatest, gcd_dvd1, gcd_dvd2] 
-                        addIs [dvd_trans]) 1); 
-qed "gcd_greatest_iff";
-Addsimps [gcd_greatest_iff];
-
-(* GCD PROOF: GCD exists and gcd fits the definition *)
-
-Goalw [is_gcd_def] "[| m \\<in> nat; n \\<in> nat |] ==> is_gcd(gcd(m,n), m, n)";
-by (Asm_simp_tac 1);
-qed "is_gcd";
-
-(* GCD is unique *)
-
-Goalw [is_gcd_def] "[|is_gcd(m,a,b); is_gcd(n,a,b); m\\<in>nat; n\\<in>nat|] ==> m=n";
-by (blast_tac (claset() addIs [dvd_anti_sym]) 1);
-qed "is_gcd_unique";
-
-Goalw [is_gcd_def] "is_gcd(k,m,n) <-> is_gcd(k,n,m)";
-by (Blast_tac 1); 
-qed "is_gcd_commute";
-
-Goal "[| m \\<in> nat; n \\<in> nat |] ==> gcd(m,n) = gcd(n,m)";
-by (rtac is_gcd_unique 1); 
-by (rtac is_gcd 1); 
-by (rtac (is_gcd_commute RS iffD1) 3); 
-by (rtac is_gcd 3); 
-by Auto_tac; 
-qed "gcd_commute_raw";
-
-Goal "gcd(m,n) = gcd(n,m)";
-by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_commute_raw 1); 
-by Auto_tac; 
-qed "gcd_commute";
-
-Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
-\     ==> gcd (gcd (k, m), n) = gcd (k, gcd (m, n))";
-by (rtac is_gcd_unique 1); 
-by (rtac is_gcd 1); 
-by (asm_full_simp_tac (simpset() addsimps [is_gcd_def]) 3);
-by (blast_tac (claset() addIs [gcd_dvd1, gcd_dvd2, gcd_type] 
-                        addIs [dvd_trans]) 3); 
-by Auto_tac; 
-qed "gcd_assoc_raw";
-
-Goal "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))";
-by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")] 
-    gcd_assoc_raw 1); 
-by Auto_tac; 
-qed "gcd_assoc";
-
-Goal "gcd (0, m) = natify(m)";
-by (asm_simp_tac (simpset() addsimps [inst "m" "0" gcd_commute]) 1); 
-qed "gcd_0_left"; 
-Addsimps [gcd_0_left];
-
-Goal "gcd (1, m) = 1";
-by (asm_simp_tac (simpset() addsimps [inst "m" "1" gcd_commute]) 1); 
-qed "gcd_1_left"; 
-Addsimps [gcd_1_left];
-
-
-(* Multiplication laws *)
-
-Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
-\     ==> k #* gcd (m, n) = gcd (k #* m, k #* n)";
-by (eres_inst_tac [("m","m"),("n","n")] gcd_induct 1); 
-by (assume_tac 1); 
-by (Asm_simp_tac 1); 
-by (case_tac "k = 0" 1);
-by (Asm_full_simp_tac 1); 
-by (asm_full_simp_tac (simpset() addsimps [mod_geq, gcd_non_0, 
-                                    mod_mult_distrib2, Ord_0_lt_iff]) 1); 
-qed "gcd_mult_distrib2_raw";
-
-Goal "k #* gcd (m, n) = gcd (k #* m, k #* n)";
-by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")] 
-    gcd_mult_distrib2_raw 1); 
-by Auto_tac; 
-qed "gcd_mult_distrib2";
-
-Goal "gcd (k, k #* n) = natify(k)";
-by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1);
-by Auto_tac; 
-qed "gcd_mult";
-Addsimps [gcd_mult];
-
-Goal "gcd (k, k) = natify(k)";
-by (cut_inst_tac [("k","k"),("n","1")] gcd_mult 1);
-by Auto_tac; 
-qed "gcd_self";
-Addsimps [gcd_self];
-
-Goal "[| gcd (k,n) = 1;  k dvd (m #* n);  m \\<in> nat |] \
-\     ==> k dvd m";
-by (cut_inst_tac [("k","m"),("m","k"),("n","n")] gcd_mult_distrib2 1);
-by Auto_tac; 
-by (eres_inst_tac [("b","m")] ssubst 1);
-by (asm_full_simp_tac (simpset() addsimps [dvd_imp_nat1]) 1);  
-qed "relprime_dvd_mult";
-
-Goal "[| gcd (k,n) = 1;  m \\<in> nat |] \
-\     ==> k dvd (m #* n) <-> k dvd m";
-by (blast_tac (claset() addIs [dvdI2, relprime_dvd_mult, dvd_trans]) 1); 
-qed "relprime_dvd_mult_iff";
-
-Goalw [prime_def]
-     "[| p \\<in> prime;  ~ (p dvd n);  n \\<in> nat |] ==> gcd (p, n) = 1";
-by (Clarify_tac 1); 
-by (dres_inst_tac [("x","gcd(p,n)")] bspec 1);
-by Auto_tac;  
-by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd2 1);
-by Auto_tac;
-qed "prime_imp_relprime";
-
-Goalw [prime_def] "p \\<in> prime ==> p \\<in> nat";
-by Auto_tac; 
-qed "prime_into_nat";
-
-Goalw [prime_def] "p \\<in> prime \\<Longrightarrow> p\\<noteq>0";
-by Auto_tac; 
-qed "prime_nonzero";
-
-
-(*This theorem leads immediately to a proof of the uniqueness of
-  factorization.  If p divides a product of primes then it is
-  one of those primes.*)
-
-Goal "[|p dvd m #* n; p \\<in> prime; m \\<in> nat; n \\<in> nat |] ==> p dvd m \\<or> p dvd n";
-by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime, 
-                               prime_into_nat]) 1); 
-qed "prime_dvd_mult";
-
-
-(** Addition laws **)
-
-Goal "gcd (m #+ n, n) = gcd (m, n)";
-by (subgoal_tac "gcd (m #+ natify(n), natify(n)) = gcd (m, natify(n))" 1);
-by (Asm_full_simp_tac 1); 
-by (case_tac "natify(n) = 0" 1);
-by (auto_tac (claset(), simpset() addsimps [Ord_0_lt_iff, gcd_non_0])); 
-qed "gcd_add1"; 
-Addsimps [gcd_add1];
-
-Goal "gcd (m, m #+ n) = gcd (m, n)";
-by (rtac (gcd_commute RS trans) 1); 
-by (stac add_commute 1); 
-by (Simp_tac 1);
-by (rtac gcd_commute 1); 
-qed "gcd_add2"; 
-Addsimps [gcd_add2];
-
-Goal "gcd (m, n #+ m) = gcd (m, n)";
-by (stac add_commute 1); 
-by (rtac gcd_add2 1); 
-qed "gcd_add2'"; 
-Addsimps [gcd_add2'];
-
-Goal "k \\<in> nat ==> gcd (m, k #* m #+ n) = gcd (m, n)";
-by (etac nat_induct 1); 
-by (auto_tac (claset(), simpset() addsimps [gcd_add2, add_assoc])); 
-qed "gcd_add_mult_raw";
-
-Goal "gcd (m, k #* m #+ n) = gcd (m, n)";
-by (cut_inst_tac [("k","natify(k)")] gcd_add_mult_raw 1);
-by Auto_tac; 
-qed "gcd_add_mult";
-
-
-(* More multiplication laws *)
-
-Goal "[|gcd (k,n) = 1; m \\<in> nat; n \\<in> nat|] ==> gcd (k #* m, n) = gcd (m, n)";
-by (rtac dvd_anti_sym 1);
- by (rtac gcd_greatest 1);
-  by (rtac (inst "n" "k" relprime_dvd_mult) 1);
-by (asm_full_simp_tac (simpset() addsimps [gcd_assoc]) 1); 
-by (asm_full_simp_tac (simpset() addsimps [gcd_commute]) 1); 
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
-by (blast_tac (claset() addIs [dvdI1, gcd_dvd1, dvd_trans]) 1); 
-qed "gcd_mult_cancel_raw";
-
-
-Goal "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)";
-by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_mult_cancel_raw 1); 
-by Auto_tac; 
-qed "gcd_mult_cancel";
-
-
-(*** The square root of a prime is irrational: key lemma ***)
-
-Goal "\\<lbrakk>n#*n = p#*(k#*k); p \\<in> prime; n \\<in> nat\\<rbrakk> \\<Longrightarrow> p dvd n";
-by (subgoal_tac "p dvd n#*n" 1); 
- by (blast_tac (claset() addDs [prime_dvd_mult]) 1);
-by (res_inst_tac [("j","k#*k")] dvd_mult_left 1);
- by (auto_tac (claset(), simpset() addsimps [prime_def])); 
-qed "prime_dvd_other_side";
-
-Goal "\\<lbrakk>k#*k = p#*(j#*j); p \\<in> prime; 0 < k; j \\<in> nat; k \\<in> nat\\<rbrakk> \
-\     \\<Longrightarrow> k < p#*j & 0 < j";
-by (rtac ccontr 1);
-by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le, prime_into_nat]) 1); 
-by (etac disjE 1);
- by (ftac mult_le_mono 1 THEN REPEAT (assume_tac 1));
-by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
-by (auto_tac (claset() addSDs [natify_eqE], 
-              simpset() addsimps [not_lt_iff_le, prime_into_nat, 
-                                  mult_le_cancel_le1])); 
-by (asm_full_simp_tac (simpset() addsimps [prime_def]) 1); 
-by (blast_tac (claset() addDs [lt_trans1]) 1); 
-qed "reduction";
-
-
-Goal "j #* (p#*j) = k#*k \\<Longrightarrow> k#*k = p#*(j#*j)";
-by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); 
-qed "rearrange";
-
-Goal "\\<lbrakk>m \\<in> nat; p \\<in> prime\\<rbrakk> \\<Longrightarrow> \\<forall>k \\<in> nat. 0<k \\<longrightarrow> m#*m \\<noteq> p#*(k#*k)";
-by (etac complete_induct 1); 
-by (Clarify_tac 1); 
-by (ftac prime_dvd_other_side 1);
-by (assume_tac 1); 
-by (assume_tac 1); 
-by (etac dvdE 1);
-by (asm_full_simp_tac (simpset() addsimps [mult_assoc, mult_cancel1, 
-                                           prime_nonzero, prime_into_nat]) 1); 
-by (blast_tac (claset() addDs [rearrange, reduction, ltD]) 1); 
-qed "prime_not_square";
diff -r c198367640f6 -r cf1715a5f5ec src/ZF/ex/Ramsey.ML
--- a/src/ZF/ex/Ramsey.ML	Fri Dec 28 10:10:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,204 +0,0 @@
-(*  Title:      ZF/ex/ramsey.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Ramsey's Theorem (finite exponent 2 version)
-
-Based upon the article
-    D Basin and M Kaufmann,
-    The Boyer-Moore Prover and Nuprl: An Experimental Comparison.
-    In G Huet and G Plotkin, editors, Logical Frameworks.
-    (CUP, 1991), pages 89--119
-
-See also
-    M Kaufmann,
-    An example in NQTHM: Ramsey's Theorem
-    Internal Note, Computational Logic, Inc., Austin, Texas 78703
-    Available from the author: kaufmann@cli.com
-*)
-
-(*** Cliques and Independent sets ***)
-
-Goalw [Clique_def] "Clique(0,V,E)";
-by (Fast_tac 1);
-qed "Clique0";
-
-Goalw [Clique_def] "[| Clique(C,V',E);  V'<=V |] ==> Clique(C,V,E)";
-by (Fast_tac 1);
-qed "Clique_superset";
-
-Goalw [Indept_def] "Indept(0,V,E)";
-by (Fast_tac 1);
-qed "Indept0";
-
-Goalw [Indept_def] "[| Indept(I,V',E);  V'<=V |] ==> Indept(I,V,E)";
-by (Fast_tac 1);
-qed "Indept_superset";
-
-(*** Atleast ***)
-
-Goalw [Atleast_def, inj_def, Pi_def, function_def] "Atleast(0,A)";
-by (Fast_tac 1);
-qed "Atleast0";
-
-Goalw [Atleast_def]
-    "Atleast(succ(m),A) ==> \\<exists>x \\<in> A. Atleast(m, A-{x})";
-by (fast_tac (claset() addEs [inj_is_fun RS apply_type, inj_succ_restrict]) 1);
-qed "Atleast_succD";
-
-Goalw [Atleast_def]
-    "[| Atleast(n,A);  A \\<subseteq> B |] ==> Atleast(n,B)";
-by (fast_tac (claset() addEs [inj_weaken_type]) 1);
-qed "Atleast_superset";
-
-Goalw [Atleast_def,succ_def]
-    "[| Atleast(m,B);  b\\<notin> B |] ==> Atleast(succ(m), cons(b,B))";
-by (etac exE 1);
-by (rtac exI 1);
-by (etac inj_extend 1);
-by (rtac mem_not_refl 1);
-by (assume_tac 1);
-qed "Atleast_succI";
-
-Goal "[| Atleast(m, B-{x});  x \\<in> B |] ==> Atleast(succ(m), B)";
-by (etac (Atleast_succI RS Atleast_superset) 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
-qed "Atleast_Diff_succI";
-
-(*** Main Cardinality Lemma ***)
-
-(*The #-succ(0) strengthens the original theorem statement, but precisely
-  the same proof could be used!!*)
-Goal "m \\<in> nat ==> \
-\     \\<forall>n \\<in> nat. \\<forall>A B. Atleast((m#+n) #- succ(0), A Un B) -->   \
-\                          Atleast(m,A) | Atleast(n,B)";
-by (induct_tac "m" 1);
-by (fast_tac (claset() addSIs [Atleast0]) 1);
-by (Asm_simp_tac 1);
-by (rtac ballI 1);
-by (rename_tac "m' n" 1);       (*simplifier does NOT preserve bound names!*)
-by (induct_tac "n" 1);
-by (fast_tac (claset() addSIs [Atleast0]) 1);
-by (Asm_simp_tac 1);
-by Safe_tac;
-by (etac (Atleast_succD RS bexE) 1);
-by (rename_tac "n' A B z" 1);
-by (etac UnE 1);
-(**case z \\<in> B.  Instantiate the '\\<forall>A B' induction hypothesis. **)
-by (dres_inst_tac [("x1","A"), ("x","B-{z}")] (spec RS spec) 2);
-by (etac (mp RS disjE) 2);
-(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
-by (REPEAT (eresolve_tac [asm_rl, notE, Atleast_Diff_succI] 3));
-(*proving the condition*)
-by (etac Atleast_superset 2 THEN Fast_tac 2);
-(**case z \\<in> A.  Instantiate the '\\<forall>n \\<in> nat. \\<forall>A B' induction hypothesis. **)
-by (dres_inst_tac [("x2","succ(n')"), ("x1","A-{z}"), ("x","B")] 
-    (bspec RS spec RS spec) 1);
-by (etac nat_succI 1);
-by (etac (mp RS disjE) 1);
-(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
-by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
-(*proving the condition*)
-by (Asm_simp_tac 1);
-by (etac Atleast_superset 1 THEN Fast_tac 1);
-qed_spec_mp "pigeon2";
-
-
-(**** Ramsey's Theorem ****)
-
-(** Base cases of induction; they now admit ANY Ramsey number **)
-
-Goalw [Ramsey_def] "Ramsey(n,0,j)";
-by (fast_tac (claset() addIs [Clique0,Atleast0]) 1);
-qed "Ramsey0j";
-
-Goalw [Ramsey_def] "Ramsey(n,i,0)";
-by (fast_tac (claset() addIs [Indept0,Atleast0]) 1);
-qed "Ramseyi0";
-
-(** Lemmas for induction step **)
-
-(*The use of succ(m) here, rather than #-succ(0), simplifies the proof of 
-  Ramsey_step_lemma.*)
-Goal "[| Atleast(m #+ n, A);  m \\<in> nat;  n \\<in> nat |]  \
-\     ==> Atleast(succ(m), {x \\<in> A. ~P(x)}) | Atleast(n, {x \\<in> A. P(x)})";
-by (rtac (nat_succI RS pigeon2) 1);
-by (Asm_simp_tac 3);
-by (rtac Atleast_superset 3);
-by Auto_tac;
-qed "Atleast_partition";
-
-(*For the Atleast part, proves ~(a \\<in> I) from the second premise!*)
-Goalw [Symmetric_def,Indept_def]
-    "[| Symmetric(E);  Indept(I, {z \\<in> V-{a}. <a,z> \\<notin> E}, E);  a \\<in> V;  \
-\       Atleast(j,I) |] ==>   \
-\    Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
-by (blast_tac (claset() addSIs [Atleast_succI]) 1);
-qed "Indept_succ";
-
-Goalw [Symmetric_def,Clique_def]
-    "[| Symmetric(E);  Clique(C, {z \\<in> V-{a}. <a,z>:E}, E);  a \\<in> V;  \
-\       Atleast(j,C) |] ==>   \
-\    Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))";
-by (blast_tac (claset() addSIs [Atleast_succI]) 1);
-qed "Clique_succ";
-
-(** Induction step **)
-
-(*Published proofs gloss over the need for Ramsey numbers to be POSITIVE.*)
-val ram1::ram2::prems = goalw Ramsey.thy [Ramsey_def] 
-   "[| Ramsey(succ(m), succ(i), j);  Ramsey(n, i, succ(j));  \
-\      m \\<in> nat;  n \\<in> nat |] ==> \
-\   Ramsey(succ(m#+n), succ(i), succ(j))";
-by Safe_tac;
-by (etac (Atleast_succD RS bexE) 1);
-by (eres_inst_tac [("P1","%z.<x,z>:E")] (Atleast_partition RS disjE) 1);
-by (REPEAT (resolve_tac prems 1));
-(*case m*)
-by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1);
-by (Fast_tac 1);
-by (fast_tac (claset() addEs [Clique_superset]) 1); (*easy -- given a Clique*)
-by Safe_tac;
-by (eresolve_tac (swapify [exI]) 1);             (*ignore main \\<exists>quantifier*)
-by (REPEAT (ares_tac [Indept_succ] 1));          (*make a bigger Indept*)
-(*case n*)
-by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1);
-by (Fast_tac 1);
-by Safe_tac;
-by (rtac exI 1);
-by (REPEAT (ares_tac [Clique_succ] 1));          (*make a bigger Clique*)
-by (fast_tac (claset() addEs [Indept_superset]) 1); (*easy -- given an Indept*)
-qed "Ramsey_step_lemma";
-
-
-(** The actual proof **)
-
-(*Again, the induction requires Ramsey numbers to be positive.*)
-Goal "i \\<in> nat ==> \\<forall>j \\<in> nat. \\<exists>n \\<in> nat. Ramsey(succ(n), i, j)";
-by (induct_tac "i" 1);
-by (fast_tac (claset() addSIs [Ramsey0j]) 1);
-by (rtac ballI 1);
-by (induct_tac "j" 1);
-by (fast_tac (claset() addSIs [Ramseyi0]) 1);
-by (fast_tac (claset() addSDs [bspec]
- 		       addSIs [add_type,Ramsey_step_lemma]) 1);
-qed "ramsey_lemma";
-
-(*Final statement in a tidy form, without succ(...) *)
-Goal "[| i \\<in> nat;  j \\<in> nat |] ==> \\<exists>n \\<in> nat. Ramsey(n,i,j)";
-by (best_tac (claset() addDs [ramsey_lemma]) 1);
-qed "ramsey";
-
-(*Compute Ramsey numbers according to proof above -- which, actually,
-  does not constrain the base case values at all!*)
-fun ram 0 j = 1
-  | ram i 0 = 1
-  | ram i j = ram (i-1) j + ram i (j-1);
-
-(*Previous proof gave the following Ramsey numbers, which are smaller than
-  those above by one!*)
-fun ram' 0 j = 0
-  | ram' i 0 = 0
-  | ram' i j = ram' (i-1) j + ram' i (j-1) + 1;