# HG changeset patch
# User paulson
# Date 1021998328 -7200
# Node ID 394a6c64954710c63b4bafcedeed2303561c440a
# Parent  afcbca3498b0ba273a6ca7fb499a492608be086e
conversion of OrdQuant.ML to Isar

diff -r afcbca3498b0 -r 394a6c649547 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Tue May 21 13:06:36 2002 +0200
+++ b/src/ZF/IsaMakefile	Tue May 21 18:25:28 2002 +0200
@@ -39,7 +39,7 @@
   Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
   Main_ZFC.ML Main_ZFC.thy	\
   Nat.ML Nat.thy Order.thy OrderArith.thy	\
-  OrderType.thy Ordinal.thy OrdQuant.ML OrdQuant.thy Perm.ML Perm.thy	\
+  OrderType.thy Ordinal.thy OrdQuant.thy Perm.ML Perm.thy	\
   QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML	\
   Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
   Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
diff -r afcbca3498b0 -r 394a6c649547 src/ZF/OrdQuant.ML
--- a/src/ZF/OrdQuant.ML	Tue May 21 13:06:36 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,116 +0,0 @@
-(*  Title:      ZF/OrdQuant.ML
-    ID:         $Id$
-    Authors:    Krzysztof Grabczewski and L C Paulson
-
-Quantifiers and union operator for ordinals. 
-*)
-
-val oall_def = thm "oall_def";
-val oex_def = thm "oex_def"; 
-val OUnion_def = thm "OUnion_def";
-
-(*** universal quantifier for ordinals ***)
-
-val prems = Goalw [oall_def] 
-    "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)";
-by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ;
-qed "oallI";
-
-Goalw [oall_def] "[| ALL x<A. P(x);  x<A |] ==> P(x)";
-by (etac (spec RS mp) 1);
-by (assume_tac 1) ;
-qed "ospec";
-
-val major::prems = Goalw [oall_def] 
-    "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q";
-by (rtac (major RS allE) 1);
-by (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ;
-qed "oallE";
-
-val major::prems = Goal
-    "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q";
-by (rtac (major RS oallE) 1);
-by (REPEAT (eresolve_tac prems 1)) ;
-qed "rev_oallE";
-
-(*Trival rewrite rule;   (ALL x<a.P)<->P holds only if a is not 0!*)
-Goal "(ALL x<a. True) <-> True";
-by (REPEAT (ares_tac [TrueI,oallI,iffI] 1)) ;
-qed "oall_simp";
-
-(*Congruence rule for rewriting*)
-val prems = Goalw [oall_def] 
-    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')";
-by (simp_tac (simpset() addsimps prems) 1) ;
-qed "oall_cong";
-
-
-(*** existential quantifier for ordinals ***)
-
-val prems = Goalw [oex_def] 
-    "[| P(x);  x<A |] ==> EX x<A. P(x)";
-by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ;
-qed "oexI";
-
-(*Not of the general form for such rules; ~EX has become ALL~ *)
-val prems = Goal
-   "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A. P(x)";
-by (rtac classical 1);
-by (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ;
-qed "oexCI";
-
-val major::prems = Goalw [oex_def] 
-    "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q \
-\    |] ==> Q";
-by (rtac (major RS exE) 1);
-by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
-qed "oexE";
-
-val prems = Goalw [oex_def] 
-    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) \
-\    |] ==> oex(a,P) <-> oex(a',P')";
-by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1) ;
-qed "oex_cong";
-
-
-(*** Rules for Ordinal-Indexed Unions ***)
-
-Goalw [OUnion_def] "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))";
-by (blast_tac (claset() addSEs [ltE]) 1);
-qed "OUN_I";
-
-val major::prems = Goalw [OUnion_def] 
-    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R";
-by (rtac (major RS CollectE) 1);
-by (rtac UN_E 1);
-by (REPEAT (ares_tac (ltI::prems) 1)) ;
-qed "OUN_E";
-
-Goalw [oex_def] "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))";
-by (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ;
-qed "OUN_iff";
-
-val prems = Goal
-    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))";
-by (rtac equality_iffI 1);
-by (simp_tac (simpset() addcongs [oex_cong] addsimps OUN_iff::prems) 1) ;
-qed "OUN_cong";
-
-AddSIs [oallI];
-AddIs  [oexI, OUN_I];
-AddSEs [oexE, OUN_E];
-AddEs  [rev_oallE];
-
-val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
-
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
-                        addsimps [oall_simp, ltD RS beta]
-                        addcongs [oall_cong, oex_cong, OUN_cong];
-
-val major::prems = Goalw [lt_def, oall_def]
-    "[| i<k;  !!x.[| x<k;  ALL y<x. P(y) |] ==> P(x) \
-\    |]  ==>  P(i)";
-by (rtac (major RS conjE) 1);
-by (etac Ord_induct 1 THEN assume_tac 1);
-by (fast_tac (claset() addIs prems) 1);
-qed "lt_induct";
diff -r afcbca3498b0 -r 394a6c649547 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Tue May 21 13:06:36 2002 +0200
+++ b/src/ZF/OrdQuant.thy	Tue May 21 18:25:28 2002 +0200
@@ -39,8 +39,8 @@
 (** simplification of the new quantifiers **)
 
 
-(*MOST IMPORTANT that this is added to the simpset BEFORE OrdQuant.ML
-  is loaded: it's Ord_atomize would convert this rule to 
+(*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
+  is proved.  Ord_atomize would convert this rule to 
     x < 0 ==> P(x) == True, which causes dire effects!*)
 lemma [simp]: "(ALL x<0. P(x))"
 by (simp add: oall_def) 
@@ -199,4 +199,124 @@
      "(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))"
 by (simp add: oall_def atomize_all atomize_imp)
 
+(*** universal quantifier for ordinals ***)
+
+lemma oallI [intro!]:
+    "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
+by (simp add: oall_def); 
+
+lemma ospec: "[| ALL x<A. P(x);  x<A |] ==> P(x)"
+by (simp add: oall_def); 
+
+lemma oallE:
+    "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q"
+apply (simp add: oall_def); 
+apply (blast intro: elim:); 
+done
+
+lemma rev_oallE [elim]:
+    "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q"
+apply (simp add: oall_def);
+apply (blast intro: elim:);  
+done
+
+
+(*Trival rewrite rule;   (ALL x<a.P)<->P holds only if a is not 0!*)
+lemma oall_simp [simp]: "(ALL x<a. True) <-> True"
+apply (blast intro: elim:); 
+done
+
+(*Congruence rule for rewriting*)
+lemma oall_cong [cong]:
+    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')"
+by (simp add: oall_def)
+
+
+(*** existential quantifier for ordinals ***)
+
+lemma oexI [intro]:
+    "[| P(x);  x<A |] ==> EX x<A. P(x)"
+apply (simp add: oex_def); 
+apply (blast intro: elim:); 
+done
+
+(*Not of the general form for such rules; ~EX has become ALL~ *)
+lemma oexCI:
+   "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A. P(x)"
+apply (simp add: oex_def); 
+apply (blast intro: elim:); 
+done
+
+lemma oexE [elim!]:
+    "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q |] ==> Q"
+apply (simp add: oex_def); 
+apply (blast intro: elim:); 
+done
+
+lemma oex_cong [cong]:
+    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oex(a,P) <-> oex(a',P')"
+apply (simp add: oex_def cong add: conj_cong)
+done
+
+
+(*** Rules for Ordinal-Indexed Unions ***)
+
+lemma OUN_I [intro]: "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))"
+apply (unfold OUnion_def lt_def)
+apply (blast)
+done
+
+lemma OUN_E [elim!]:
+    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
+apply (unfold OUnion_def lt_def)
+apply (blast)
+done
+
+lemma OUN_iff: "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
+apply (unfold OUnion_def oex_def lt_def)
+apply (blast intro: elim:); 
+done
+
+lemma OUN_cong [cong]:
+    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
+by (simp add: OUnion_def lt_def OUN_iff)
+
+declare ltD [THEN beta, simp]
+
+
+lemma lt_induct: 
+    "[| i<k;  !!x.[| x<k;  ALL y<x. P(y) |] ==> P(x) |]  ==>  P(i)"
+apply (simp add: lt_def oall_def)
+apply (erule conjE) 
+apply (erule Ord_induct, assumption)
+apply (blast intro: elim:); 
+done
+
+ML
+{*
+val oall_def = thm "oall_def"
+val oex_def = thm "oex_def"
+val OUnion_def = thm "OUnion_def"
+
+val oallI = thm "oallI";
+val ospec = thm "ospec";
+val oallE = thm "oallE";
+val rev_oallE = thm "rev_oallE";
+val oall_simp = thm "oall_simp";
+val oall_cong = thm "oall_cong";
+val oexI = thm "oexI";
+val oexCI = thm "oexCI";
+val oexE = thm "oexE";
+val oex_cong = thm "oex_cong";
+val OUN_I = thm "OUN_I";
+val OUN_E = thm "OUN_E";
+val OUN_iff = thm "OUN_iff";
+val OUN_cong = thm "OUN_cong";
+val lt_induct = thm "lt_induct";
+
+val Ord_atomize =
+    atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
+*}
+
 end
diff -r afcbca3498b0 -r 394a6c649547 src/ZF/domrange.ML
--- a/src/ZF/domrange.ML	Tue May 21 13:06:36 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,233 +0,0 @@
-(*  Title:      ZF/domrange
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Converse, domain, range of a relation or function
-*)
-
-(*** converse ***)
-
-Goalw [converse_def] "<a,b>: converse(r) <-> <b,a>:r";
-by (Blast_tac 1) ;
-qed "converse_iff";
-
-Goalw [converse_def] "<a,b>:r ==> <b,a>:converse(r)";
-by (Blast_tac 1) ;
-qed "converseI";
-
-Goalw [converse_def] "<a,b> : converse(r) ==> <b,a> : r";
-by (Blast_tac 1) ;
-qed "converseD";
-
-val [major,minor]= Goalw [converse_def] 
-    "[| yx : converse(r);  \
-\       !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P \
-\    |] ==> P";
-by (rtac (major RS ReplaceE) 1);
-by (REPEAT (eresolve_tac [exE, conjE, minor] 1));
-by (hyp_subst_tac 1);
-by (assume_tac 1) ;
-qed "converseE";
-
-Addsimps [converse_iff];
-AddSIs [converseI];
-AddSEs [converseD,converseE];
-
-Goal "r<=Sigma(A,B) ==> converse(converse(r)) = r";
-by (Blast_tac 1) ;
-qed "converse_converse";
-
-Goal "r<=A*B ==> converse(r)<=B*A";
-by (Blast_tac 1) ;
-qed "converse_type";
-
-Goal "converse(A*B) = B*A";
-by (Blast_tac 1) ;
-qed "converse_prod";
-
-Goal "converse(0) = 0";
-by (Blast_tac 1) ;
-qed "converse_empty";
-
-Addsimps [converse_prod, converse_empty];
-
-Goal "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B";
-by (Blast_tac 1) ;
-qed "converse_subset_iff";
-
-
-(*** domain ***)
-
-Goalw [domain_def] "a: domain(r) <-> (EX y. <a,y>: r)";
-by (Blast_tac 1) ;
-qed "domain_iff";
-
-Goal "<a,b>: r ==> a: domain(r)";
-by (etac (exI RS (domain_iff RS iffD2)) 1) ;
-qed "domainI";
-
-val prems= Goal
-    "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P";
-by (rtac (domain_iff RS iffD1 RS exE) 1);
-by (REPEAT (ares_tac prems 1)) ;
-qed "domainE";
-
-AddIs  [domainI];
-AddSEs [domainE];
-
-Goal "domain(Sigma(A,B)) <= A";
-by (Blast_tac 1) ;
-qed "domain_subset";
-
-(*** range ***)
-
-Goalw [range_def]  "<a,b>: r ==> b : range(r)";
-by (etac (converseI RS domainI) 1) ;
-qed "rangeI";
-
-val major::prems= Goalw [range_def] 
-    "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P";
-by (rtac (major RS domainE) 1);
-by (resolve_tac prems 1);
-by (etac converseD 1) ;
-qed "rangeE";
-
-AddIs  [rangeI];
-AddSEs [rangeE];
-
-Goalw [range_def]  "range(A*B) <= B";
-by (stac converse_prod 1);
-by (rtac domain_subset 1) ;
-qed "range_subset";
-
-
-(*** field ***)
-
-Goalw [field_def]  "<a,b>: r ==> a : field(r)";
-by (Blast_tac 1) ;
-qed "fieldI1";
-
-Goalw [field_def]  "<a,b>: r ==> b : field(r)";
-by (Blast_tac 1) ;
-qed "fieldI2";
-
-val [prem]= Goalw [field_def] 
-    "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)";
-by (blast_tac (claset() addIs [prem]) 1) ;
-qed "fieldCI";
-
-val major::prems= Goalw [field_def] 
-     "[| a : field(r);  \
-\        !!x. <a,x>: r ==> P;  \
-\        !!x. <x,a>: r ==> P        |] ==> P";
-by (rtac (major RS UnE) 1);
-by (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ;
-qed "fieldE";
-
-AddIs  [fieldCI];
-AddSEs [fieldE];
-
-Goal "field(A*B) <= A Un B";
-by (Blast_tac 1) ;
-qed "field_subset";
-
-Goalw [field_def] "domain(r) <= field(r)";
-by (rtac Un_upper1 1) ;
-qed "domain_subset_field";
-
-Goalw [field_def] "range(r) <= field(r)";
-by (rtac Un_upper2 1) ;
-qed "range_subset_field";
-
-Goal "r <= Sigma(A,B) ==> r <= domain(r)*range(r)";
-by (Blast_tac 1) ;
-qed "domain_times_range";
-
-Goal "r <= Sigma(A,B) ==> r <= field(r)*field(r)";
-by (Blast_tac 1) ;
-qed "field_times_field";
-
-
-(*** Image of a set under a function/relation ***)
-
-Goalw [image_def] "b : r``A <-> (EX x:A. <x,b>:r)";
-by (Blast_tac 1);
-qed "image_iff";
-
-Goal "b : r``{a} <-> <a,b>:r";
-by (rtac (image_iff RS iff_trans) 1);
-by (Blast_tac 1) ;
-qed "image_singleton_iff";
-
-Goalw [image_def] "[| <a,b>: r;  a:A |] ==> b : r``A";
-by (Blast_tac 1) ;
-qed "imageI";
-
-val major::prems= Goalw [image_def] 
-    "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P";
-by (rtac (major RS CollectE) 1);
-by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
-qed "imageE";
-
-AddIs  [imageI];
-AddSEs [imageE];
-
-Goal "r <= A*B ==> r``C <= B";
-by (Blast_tac 1) ;
-qed "image_subset";
-
-
-(*** Inverse image of a set under a function/relation ***)
-
-Goalw [vimage_def,image_def,converse_def] 
-    "a : r-``B <-> (EX y:B. <a,y>:r)";
-by (Blast_tac 1) ;
-qed "vimage_iff";
-
-Goal "a : r-``{b} <-> <a,b>:r";
-by (rtac (vimage_iff RS iff_trans) 1);
-by (Blast_tac 1) ;
-qed "vimage_singleton_iff";
-
-Goalw [vimage_def] "[| <a,b>: r;  b:B |] ==> a : r-``B";
-by (Blast_tac 1) ;
-qed "vimageI";
-
-val major::prems= Goalw [vimage_def] 
-    "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P";
-by (rtac (major RS imageE) 1);
-by (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ;
-qed "vimageE";
-
-Goalw [vimage_def] "r <= A*B ==> r-``C <= A";
-by (etac (converse_type RS image_subset) 1) ;
-qed "vimage_subset";
-
-
-(** Theorem-proving for ZF set theory **)
-
-AddIs  [vimageI];
-AddSEs [vimageE];
-
-val ZF_cs = claset() delrules [equalityI];
-
-(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
-Goal "(ALL x:S. EX A B. x <= A*B) ==>  \
-\                 Union(S) <= domain(Union(S)) * range(Union(S))";
-by (Blast_tac 1);
-qed "rel_Union";
-
-(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
-Goal "[| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)";
-by (Blast_tac 1) ;
-qed "rel_Un";
-
-Goal "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
-by (Blast_tac 1);
-qed "domain_Diff_eq";
-
-Goal "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
-by (Blast_tac 1);
-qed "range_Diff_eq";
-
diff -r afcbca3498b0 -r 394a6c649547 src/ZF/domrange.thy
--- a/src/ZF/domrange.thy	Tue May 21 13:06:36 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-domrange = pair + subset
-
diff -r afcbca3498b0 -r 394a6c649547 src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Tue May 21 13:06:36 2002 +0200
+++ b/src/ZF/equalities.thy	Tue May 21 18:25:28 2002 +0200
@@ -15,70 +15,52 @@
 (*** converse ***)
 
 lemma converse_iff [iff]: "<a,b>: converse(r) <-> <b,a>:r"
-apply (unfold converse_def)
-apply blast
-done
+by (unfold converse_def, blast)
 
 lemma converseI: "<a,b>:r ==> <b,a>:converse(r)"
-apply (unfold converse_def)
-apply blast
-done
+by (unfold converse_def, blast)
 
 lemma converseD: "<a,b> : converse(r) ==> <b,a> : r"
-apply (unfold converse_def)
-apply blast
-done
+by (unfold converse_def, blast)
 
 lemma converseE [elim!]:
     "[| yx : converse(r);   
         !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P |]
      ==> P"
-apply (unfold converse_def)
-apply (blast intro: elim:); 
+apply (unfold converse_def, blast) 
 done
 
 lemma converse_converse: "r<=Sigma(A,B) ==> converse(converse(r)) = r"
-apply blast
-done
+by blast
 
 lemma converse_type: "r<=A*B ==> converse(r)<=B*A"
-apply blast
-done
+by blast
 
 lemma converse_prod [simp]: "converse(A*B) = B*A"
-apply blast
-done
+by blast
 
 lemma converse_empty [simp]: "converse(0) = 0"
-apply blast
-done
+by blast
 
 lemma converse_subset_iff: "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
-apply blast
-done
+by blast
 
 
 (*** domain ***)
 
 lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>: r)"
-apply (unfold domain_def)
-apply blast
-done
+by (unfold domain_def, blast)
 
 lemma domainI [intro]: "<a,b>: r ==> a: domain(r)"
-apply (unfold domain_def)
-apply blast
-done
+by (unfold domain_def, blast)
 
 lemma domainE [elim!]:
     "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
-apply (unfold domain_def)
-apply blast
+apply (unfold domain_def, blast)
 done
 
 lemma domain_subset: "domain(Sigma(A,B)) <= A"
-apply blast
-done
+by blast
 
 (*** range ***)
 
@@ -88,9 +70,7 @@
 done
 
 lemma rangeE [elim!]: "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
-apply (unfold range_def)
-apply (blast intro: elim:); 
-done
+by (unfold range_def, blast)
 
 lemma range_subset: "range(A*B) <= B"
 apply (unfold range_def)
@@ -102,32 +82,25 @@
 (*** field ***)
 
 lemma fieldI1: "<a,b>: r ==> a : field(r)"
-apply (unfold field_def)
-apply blast
-done
+by (unfold field_def, blast)
 
 lemma fieldI2: "<a,b>: r ==> b : field(r)"
-apply (unfold field_def)
-apply blast
-done
+by (unfold field_def, blast)
 
 lemma fieldCI [intro]: 
     "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
-apply (unfold field_def)
-apply blast
+apply (unfold field_def, blast)
 done
 
 lemma fieldE [elim!]: 
      "[| a : field(r);   
          !!x. <a,x>: r ==> P;   
          !!x. <x,a>: r ==> P        |] ==> P"
-apply (unfold field_def)
-apply blast
+apply (unfold field_def, blast)
 done
 
 lemma field_subset: "field(A*B) <= A Un B"
-apply blast
-done
+by blast
 
 lemma domain_subset_field: "domain(r) <= field(r)"
 apply (unfold field_def)
@@ -140,64 +113,48 @@
 done
 
 lemma domain_times_range: "r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
-apply blast
-done
+by blast
 
 lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)"
-apply blast
-done
+by blast
 
 
 (*** Image of a set under a function/relation ***)
 
 lemma image_iff: "b : r``A <-> (EX x:A. <x,b>:r)"
-apply (unfold image_def)
-apply blast
-done
+by (unfold image_def, blast)
 
 lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r"
-apply (rule image_iff [THEN iff_trans])
-apply blast
-done
+by (rule image_iff [THEN iff_trans], blast)
 
 lemma imageI [intro]: "[| <a,b>: r;  a:A |] ==> b : r``A"
-apply (unfold image_def)
-apply blast
-done
+by (unfold image_def, blast)
 
 lemma imageE [elim!]: 
     "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
-apply (unfold image_def)
-apply blast
+apply (unfold image_def, blast)
 done
 
 lemma image_subset: "r <= A*B ==> r``C <= B"
-apply blast
-done
+by blast
 
 
 (*** Inverse image of a set under a function/relation ***)
 
 lemma vimage_iff: 
     "a : r-``B <-> (EX y:B. <a,y>:r)"
-apply (unfold vimage_def image_def converse_def)
-apply blast
+apply (unfold vimage_def image_def converse_def, blast)
 done
 
 lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r"
-apply (rule vimage_iff [THEN iff_trans])
-apply blast
-done
+by (rule vimage_iff [THEN iff_trans], blast)
 
 lemma vimageI [intro]: "[| <a,b>: r;  b:B |] ==> a : r-``B"
-apply (unfold vimage_def)
-apply blast
-done
+by (unfold vimage_def, blast)
 
 lemma vimageE [elim!]: 
     "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P"
-apply (unfold vimage_def)
-apply blast
+apply (unfold vimage_def, blast)
 done
 
 lemma vimage_subset: "r <= A*B ==> r-``C <= A"
@@ -213,16 +170,13 @@
 
 (** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
 lemma rel_Un: "[| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
-apply blast
-done
+by blast
 
 lemma domain_Diff_eq: "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
-apply blast
-done
+by blast
 
 lemma range_Diff_eq: "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)"
-apply blast
-done
+by blast