src/ZF/OrdQuant.thy
changeset 13169 394a6c649547
parent 13162 660a71e712af
child 13170 9e23faed6c97
     1.1 --- a/src/ZF/OrdQuant.thy	Tue May 21 13:06:36 2002 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Tue May 21 18:25:28 2002 +0200
     1.3 @@ -39,8 +39,8 @@
     1.4  (** simplification of the new quantifiers **)
     1.5  
     1.6  
     1.7 -(*MOST IMPORTANT that this is added to the simpset BEFORE OrdQuant.ML
     1.8 -  is loaded: it's Ord_atomize would convert this rule to 
     1.9 +(*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
    1.10 +  is proved.  Ord_atomize would convert this rule to 
    1.11      x < 0 ==> P(x) == True, which causes dire effects!*)
    1.12  lemma [simp]: "(ALL x<0. P(x))"
    1.13  by (simp add: oall_def) 
    1.14 @@ -199,4 +199,124 @@
    1.15       "(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))"
    1.16  by (simp add: oall_def atomize_all atomize_imp)
    1.17  
    1.18 +(*** universal quantifier for ordinals ***)
    1.19 +
    1.20 +lemma oallI [intro!]:
    1.21 +    "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
    1.22 +by (simp add: oall_def); 
    1.23 +
    1.24 +lemma ospec: "[| ALL x<A. P(x);  x<A |] ==> P(x)"
    1.25 +by (simp add: oall_def); 
    1.26 +
    1.27 +lemma oallE:
    1.28 +    "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q"
    1.29 +apply (simp add: oall_def); 
    1.30 +apply (blast intro: elim:); 
    1.31 +done
    1.32 +
    1.33 +lemma rev_oallE [elim]:
    1.34 +    "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q"
    1.35 +apply (simp add: oall_def);
    1.36 +apply (blast intro: elim:);  
    1.37 +done
    1.38 +
    1.39 +
    1.40 +(*Trival rewrite rule;   (ALL x<a.P)<->P holds only if a is not 0!*)
    1.41 +lemma oall_simp [simp]: "(ALL x<a. True) <-> True"
    1.42 +apply (blast intro: elim:); 
    1.43 +done
    1.44 +
    1.45 +(*Congruence rule for rewriting*)
    1.46 +lemma oall_cong [cong]:
    1.47 +    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')"
    1.48 +by (simp add: oall_def)
    1.49 +
    1.50 +
    1.51 +(*** existential quantifier for ordinals ***)
    1.52 +
    1.53 +lemma oexI [intro]:
    1.54 +    "[| P(x);  x<A |] ==> EX x<A. P(x)"
    1.55 +apply (simp add: oex_def); 
    1.56 +apply (blast intro: elim:); 
    1.57 +done
    1.58 +
    1.59 +(*Not of the general form for such rules; ~EX has become ALL~ *)
    1.60 +lemma oexCI:
    1.61 +   "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A. P(x)"
    1.62 +apply (simp add: oex_def); 
    1.63 +apply (blast intro: elim:); 
    1.64 +done
    1.65 +
    1.66 +lemma oexE [elim!]:
    1.67 +    "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q |] ==> Q"
    1.68 +apply (simp add: oex_def); 
    1.69 +apply (blast intro: elim:); 
    1.70 +done
    1.71 +
    1.72 +lemma oex_cong [cong]:
    1.73 +    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oex(a,P) <-> oex(a',P')"
    1.74 +apply (simp add: oex_def cong add: conj_cong)
    1.75 +done
    1.76 +
    1.77 +
    1.78 +(*** Rules for Ordinal-Indexed Unions ***)
    1.79 +
    1.80 +lemma OUN_I [intro]: "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))"
    1.81 +apply (unfold OUnion_def lt_def)
    1.82 +apply (blast)
    1.83 +done
    1.84 +
    1.85 +lemma OUN_E [elim!]:
    1.86 +    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
    1.87 +apply (unfold OUnion_def lt_def)
    1.88 +apply (blast)
    1.89 +done
    1.90 +
    1.91 +lemma OUN_iff: "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
    1.92 +apply (unfold OUnion_def oex_def lt_def)
    1.93 +apply (blast intro: elim:); 
    1.94 +done
    1.95 +
    1.96 +lemma OUN_cong [cong]:
    1.97 +    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
    1.98 +by (simp add: OUnion_def lt_def OUN_iff)
    1.99 +
   1.100 +declare ltD [THEN beta, simp]
   1.101 +
   1.102 +
   1.103 +lemma lt_induct: 
   1.104 +    "[| i<k;  !!x.[| x<k;  ALL y<x. P(y) |] ==> P(x) |]  ==>  P(i)"
   1.105 +apply (simp add: lt_def oall_def)
   1.106 +apply (erule conjE) 
   1.107 +apply (erule Ord_induct, assumption)
   1.108 +apply (blast intro: elim:); 
   1.109 +done
   1.110 +
   1.111 +ML
   1.112 +{*
   1.113 +val oall_def = thm "oall_def"
   1.114 +val oex_def = thm "oex_def"
   1.115 +val OUnion_def = thm "OUnion_def"
   1.116 +
   1.117 +val oallI = thm "oallI";
   1.118 +val ospec = thm "ospec";
   1.119 +val oallE = thm "oallE";
   1.120 +val rev_oallE = thm "rev_oallE";
   1.121 +val oall_simp = thm "oall_simp";
   1.122 +val oall_cong = thm "oall_cong";
   1.123 +val oexI = thm "oexI";
   1.124 +val oexCI = thm "oexCI";
   1.125 +val oexE = thm "oexE";
   1.126 +val oex_cong = thm "oex_cong";
   1.127 +val OUN_I = thm "OUN_I";
   1.128 +val OUN_E = thm "OUN_E";
   1.129 +val OUN_iff = thm "OUN_iff";
   1.130 +val OUN_cong = thm "OUN_cong";
   1.131 +val lt_induct = thm "lt_induct";
   1.132 +
   1.133 +val Ord_atomize =
   1.134 +    atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
   1.135 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
   1.136 +*}
   1.137 +
   1.138  end