tidied
authorpaulson
Wed May 22 17:25:40 2002 +0200 (2002-05-22)
changeset 131709e23faed6c97
parent 13169 394a6c649547
child 13171 3208b614dc71
tidied
src/ZF/OrdQuant.thy
     1.1 --- a/src/ZF/OrdQuant.thy	Tue May 21 18:25:28 2002 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Wed May 22 17:25:40 2002 +0200
     1.3 @@ -203,28 +203,25 @@
     1.4  
     1.5  lemma oallI [intro!]:
     1.6      "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
     1.7 -by (simp add: oall_def); 
     1.8 +by (simp add: oall_def) 
     1.9  
    1.10  lemma ospec: "[| ALL x<A. P(x);  x<A |] ==> P(x)"
    1.11 -by (simp add: oall_def); 
    1.12 +by (simp add: oall_def) 
    1.13  
    1.14  lemma oallE:
    1.15      "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q"
    1.16 -apply (simp add: oall_def); 
    1.17 -apply (blast intro: elim:); 
    1.18 +apply (simp add: oall_def, blast) 
    1.19  done
    1.20  
    1.21  lemma rev_oallE [elim]:
    1.22      "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q"
    1.23 -apply (simp add: oall_def);
    1.24 -apply (blast intro: elim:);  
    1.25 +apply (simp add: oall_def, blast)  
    1.26  done
    1.27  
    1.28  
    1.29  (*Trival rewrite rule;   (ALL x<a.P)<->P holds only if a is not 0!*)
    1.30  lemma oall_simp [simp]: "(ALL x<a. True) <-> True"
    1.31 -apply (blast intro: elim:); 
    1.32 -done
    1.33 +by blast
    1.34  
    1.35  (*Congruence rule for rewriting*)
    1.36  lemma oall_cong [cong]:
    1.37 @@ -236,21 +233,18 @@
    1.38  
    1.39  lemma oexI [intro]:
    1.40      "[| P(x);  x<A |] ==> EX x<A. P(x)"
    1.41 -apply (simp add: oex_def); 
    1.42 -apply (blast intro: elim:); 
    1.43 +apply (simp add: oex_def, blast) 
    1.44  done
    1.45  
    1.46  (*Not of the general form for such rules; ~EX has become ALL~ *)
    1.47  lemma oexCI:
    1.48     "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A. P(x)"
    1.49 -apply (simp add: oex_def); 
    1.50 -apply (blast intro: elim:); 
    1.51 +apply (simp add: oex_def, blast) 
    1.52  done
    1.53  
    1.54  lemma oexE [elim!]:
    1.55      "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q |] ==> Q"
    1.56 -apply (simp add: oex_def); 
    1.57 -apply (blast intro: elim:); 
    1.58 +apply (simp add: oex_def, blast) 
    1.59  done
    1.60  
    1.61  lemma oex_cong [cong]:
    1.62 @@ -262,20 +256,15 @@
    1.63  (*** Rules for Ordinal-Indexed Unions ***)
    1.64  
    1.65  lemma OUN_I [intro]: "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))"
    1.66 -apply (unfold OUnion_def lt_def)
    1.67 -apply (blast)
    1.68 -done
    1.69 +by (unfold OUnion_def lt_def, blast)
    1.70  
    1.71  lemma OUN_E [elim!]:
    1.72      "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
    1.73 -apply (unfold OUnion_def lt_def)
    1.74 -apply (blast)
    1.75 +apply (unfold OUnion_def lt_def, blast)
    1.76  done
    1.77  
    1.78  lemma OUN_iff: "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
    1.79 -apply (unfold OUnion_def oex_def lt_def)
    1.80 -apply (blast intro: elim:); 
    1.81 -done
    1.82 +by (unfold OUnion_def oex_def lt_def, blast)
    1.83  
    1.84  lemma OUN_cong [cong]:
    1.85      "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
    1.86 @@ -288,8 +277,7 @@
    1.87      "[| i<k;  !!x.[| x<k;  ALL y<x. P(y) |] ==> P(x) |]  ==>  P(i)"
    1.88  apply (simp add: lt_def oall_def)
    1.89  apply (erule conjE) 
    1.90 -apply (erule Ord_induct, assumption)
    1.91 -apply (blast intro: elim:); 
    1.92 +apply (erule Ord_induct, assumption, blast) 
    1.93  done
    1.94  
    1.95  ML