src/ZF/OrdQuant.thy
changeset 46820 c656222c4dc1
parent 45625 750c5a47400b
child 46953 2b6e55924af3
     1.1 --- a/src/ZF/OrdQuant.thy	Sun Mar 04 23:20:43 2012 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Tue Mar 06 15:15:49 2012 +0000
     1.3 @@ -11,11 +11,11 @@
     1.4  definition
     1.5    (* Ordinal Quantifiers *)
     1.6    oall :: "[i, i => o] => o"  where
     1.7 -    "oall(A, P) == ALL x. x<A --> P(x)"
     1.8 +    "oall(A, P) == \<forall>x. x<A \<longrightarrow> P(x)"
     1.9  
    1.10  definition
    1.11    oex :: "[i, i => o] => o"  where
    1.12 -    "oex(A, P)  == EX x. x<A & P(x)"
    1.13 +    "oex(A, P)  == \<exists>x. x<A & P(x)"
    1.14  
    1.15  definition
    1.16    (* Ordinal Union *)
    1.17 @@ -48,18 +48,18 @@
    1.18  (*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
    1.19    is proved.  Ord_atomize would convert this rule to
    1.20      x < 0 ==> P(x) == True, which causes dire effects!*)
    1.21 -lemma [simp]: "(ALL x<0. P(x))"
    1.22 +lemma [simp]: "(\<forall>x<0. P(x))"
    1.23  by (simp add: oall_def)
    1.24  
    1.25 -lemma [simp]: "~(EX x<0. P(x))"
    1.26 +lemma [simp]: "~(\<exists>x<0. P(x))"
    1.27  by (simp add: oex_def)
    1.28  
    1.29 -lemma [simp]: "(ALL x<succ(i). P(x)) <-> (Ord(i) --> P(i) & (ALL x<i. P(x)))"
    1.30 +lemma [simp]: "(\<forall>x<succ(i). P(x)) <-> (Ord(i) \<longrightarrow> P(i) & (\<forall>x<i. P(x)))"
    1.31  apply (simp add: oall_def le_iff)
    1.32  apply (blast intro: lt_Ord2)
    1.33  done
    1.34  
    1.35 -lemma [simp]: "(EX x<succ(i). P(x)) <-> (Ord(i) & (P(i) | (EX x<i. P(x))))"
    1.36 +lemma [simp]: "(\<exists>x<succ(i). P(x)) <-> (Ord(i) & (P(i) | (\<exists>x<i. P(x))))"
    1.37  apply (simp add: oex_def le_iff)
    1.38  apply (blast intro: lt_Ord2)
    1.39  done
    1.40 @@ -84,12 +84,11 @@
    1.41  lemma Limit_OUN_eq: "Limit(i) ==> (\<Union>x<i. x) = i"
    1.42  by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord)
    1.43  
    1.44 -(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
    1.45 +(* No < version of this theorem: consider that @{term"(\<Union>i\<in>nat.i)=nat"}! *)
    1.46  lemma OUN_least:
    1.47       "(!!x. x<A ==> B(x) \<subseteq> C) ==> (\<Union>x<A. B(x)) \<subseteq> C"
    1.48  by (simp add: OUnion_def UN_least ltI)
    1.49  
    1.50 -(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
    1.51  lemma OUN_least_le:
    1.52       "[| Ord(i);  !!x. x<A ==> b(x) \<le> i |] ==> (\<Union>x<A. b(x)) \<le> i"
    1.53  by (simp add: OUnion_def UN_least_le ltI Ord_0_le)
    1.54 @@ -105,34 +104,34 @@
    1.55  
    1.56  lemma OUN_Union_eq:
    1.57       "(!!x. x:X ==> Ord(x))
    1.58 -      ==> (\<Union>z < Union(X). C(z)) = (\<Union>x\<in>X. \<Union>z < x. C(z))"
    1.59 +      ==> (\<Union>z < \<Union>(X). C(z)) = (\<Union>x\<in>X. \<Union>z < x. C(z))"
    1.60  by (simp add: OUnion_def)
    1.61  
    1.62 -(*So that rule_format will get rid of ALL x<A...*)
    1.63 +(*So that rule_format will get rid of this quantifier...*)
    1.64  lemma atomize_oall [symmetric, rulify]:
    1.65 -     "(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))"
    1.66 +     "(!!x. x<A ==> P(x)) == Trueprop (\<forall>x<A. P(x))"
    1.67  by (simp add: oall_def atomize_all atomize_imp)
    1.68  
    1.69  subsubsection {*universal quantifier for ordinals*}
    1.70  
    1.71  lemma oallI [intro!]:
    1.72 -    "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
    1.73 +    "[| !!x. x<A ==> P(x) |] ==> \<forall>x<A. P(x)"
    1.74  by (simp add: oall_def)
    1.75  
    1.76 -lemma ospec: "[| ALL x<A. P(x);  x<A |] ==> P(x)"
    1.77 +lemma ospec: "[| \<forall>x<A. P(x);  x<A |] ==> P(x)"
    1.78  by (simp add: oall_def)
    1.79  
    1.80  lemma oallE:
    1.81 -    "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q"
    1.82 +    "[| \<forall>x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q"
    1.83  by (simp add: oall_def, blast)
    1.84  
    1.85  lemma rev_oallE [elim]:
    1.86 -    "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q"
    1.87 +    "[| \<forall>x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q"
    1.88  by (simp add: oall_def, blast)
    1.89  
    1.90  
    1.91 -(*Trival rewrite rule;   (ALL x<a.P)<->P holds only if a is not 0!*)
    1.92 -lemma oall_simp [simp]: "(ALL x<a. True) <-> True"
    1.93 +(*Trival rewrite rule.  @{term"(\<forall>x<a.P)<->P"} holds only if a is not 0!*)
    1.94 +lemma oall_simp [simp]: "(\<forall>x<a. True) <-> True"
    1.95  by blast
    1.96  
    1.97  (*Congruence rule for rewriting*)
    1.98 @@ -145,18 +144,18 @@
    1.99  subsubsection {*existential quantifier for ordinals*}
   1.100  
   1.101  lemma oexI [intro]:
   1.102 -    "[| P(x);  x<A |] ==> EX x<A. P(x)"
   1.103 +    "[| P(x);  x<A |] ==> \<exists>x<A. P(x)"
   1.104  apply (simp add: oex_def, blast)
   1.105  done
   1.106  
   1.107 -(*Not of the general form for such rules; ~EX has become ALL~ *)
   1.108 +(*Not of the general form for such rules... *)
   1.109  lemma oexCI:
   1.110 -   "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A. P(x)"
   1.111 +   "[| \<forall>x<A. ~P(x) ==> P(a);  a<A |] ==> \<exists>x<A. P(x)"
   1.112  apply (simp add: oex_def, blast)
   1.113  done
   1.114  
   1.115  lemma oexE [elim!]:
   1.116 -    "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q |] ==> Q"
   1.117 +    "[| \<exists>x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q |] ==> Q"
   1.118  apply (simp add: oex_def, blast)
   1.119  done
   1.120  
   1.121 @@ -173,11 +172,11 @@
   1.122  by (unfold OUnion_def lt_def, blast)
   1.123  
   1.124  lemma OUN_E [elim!]:
   1.125 -    "[| b : (\<Union>z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
   1.126 +    "[| b \<in> (\<Union>z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
   1.127  apply (unfold OUnion_def lt_def, blast)
   1.128  done
   1.129  
   1.130 -lemma OUN_iff: "b : (\<Union>x<i. B(x)) <-> (EX x<i. b : B(x))"
   1.131 +lemma OUN_iff: "b \<in> (\<Union>x<i. B(x)) <-> (\<exists>x<i. b \<in> B(x))"
   1.132  by (unfold OUnion_def oex_def lt_def, blast)
   1.133  
   1.134  lemma OUN_cong [cong]:
   1.135 @@ -185,7 +184,7 @@
   1.136  by (simp add: OUnion_def lt_def OUN_iff)
   1.137  
   1.138  lemma lt_induct:
   1.139 -    "[| i<k;  !!x.[| x<k;  ALL y<x. P(y) |] ==> P(x) |]  ==>  P(i)"
   1.140 +    "[| i<k;  !!x.[| x<k;  \<forall>y<x. P(y) |] ==> P(x) |]  ==>  P(i)"
   1.141  apply (simp add: lt_def oall_def)
   1.142  apply (erule conjE)
   1.143  apply (erule Ord_induct, assumption, blast)
   1.144 @@ -196,11 +195,11 @@
   1.145  
   1.146  definition
   1.147    "rall"     :: "[i=>o, i=>o] => o"  where
   1.148 -    "rall(M, P) == ALL x. M(x) --> P(x)"
   1.149 +    "rall(M, P) == \<forall>x. M(x) \<longrightarrow> P(x)"
   1.150  
   1.151  definition
   1.152    "rex"      :: "[i=>o, i=>o] => o"  where
   1.153 -    "rex(M, P) == EX x. M(x) & P(x)"
   1.154 +    "rex(M, P) == \<exists>x. M(x) & P(x)"
   1.155  
   1.156  syntax
   1.157    "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3ALL _[_]./ _)" 10)
   1.158 @@ -220,18 +219,18 @@
   1.159  
   1.160  subsubsection{*Relativized universal quantifier*}
   1.161  
   1.162 -lemma rallI [intro!]: "[| !!x. M(x) ==> P(x) |] ==> ALL x[M]. P(x)"
   1.163 +lemma rallI [intro!]: "[| !!x. M(x) ==> P(x) |] ==> \<forall>x[M]. P(x)"
   1.164  by (simp add: rall_def)
   1.165  
   1.166 -lemma rspec: "[| ALL x[M]. P(x); M(x) |] ==> P(x)"
   1.167 +lemma rspec: "[| \<forall>x[M]. P(x); M(x) |] ==> P(x)"
   1.168  by (simp add: rall_def)
   1.169  
   1.170  (*Instantiates x first: better for automatic theorem proving?*)
   1.171  lemma rev_rallE [elim]:
   1.172 -    "[| ALL x[M]. P(x);  ~ M(x) ==> Q;  P(x) ==> Q |] ==> Q"
   1.173 +    "[| \<forall>x[M]. P(x);  ~ M(x) ==> Q;  P(x) ==> Q |] ==> Q"
   1.174  by (simp add: rall_def, blast)
   1.175  
   1.176 -lemma rallE: "[| ALL x[M]. P(x);  P(x) ==> Q;  ~ M(x) ==> Q |] ==> Q"
   1.177 +lemma rallE: "[| \<forall>x[M]. P(x);  P(x) ==> Q;  ~ M(x) ==> Q |] ==> Q"
   1.178  by blast
   1.179  
   1.180  (*Trival rewrite rule;   (ALL x[M].P)<->P holds only if A is nonempty!*)
   1.181 @@ -240,24 +239,24 @@
   1.182  
   1.183  (*Congruence rule for rewriting*)
   1.184  lemma rall_cong [cong]:
   1.185 -    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (ALL x[M]. P(x)) <-> (ALL x[M]. P'(x))"
   1.186 +    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (\<forall>x[M]. P(x)) <-> (\<forall>x[M]. P'(x))"
   1.187  by (simp add: rall_def)
   1.188  
   1.189  
   1.190  subsubsection{*Relativized existential quantifier*}
   1.191  
   1.192 -lemma rexI [intro]: "[| P(x); M(x) |] ==> EX x[M]. P(x)"
   1.193 +lemma rexI [intro]: "[| P(x); M(x) |] ==> \<exists>x[M]. P(x)"
   1.194  by (simp add: rex_def, blast)
   1.195  
   1.196  (*The best argument order when there is only one M(x)*)
   1.197 -lemma rev_rexI: "[| M(x);  P(x) |] ==> EX x[M]. P(x)"
   1.198 +lemma rev_rexI: "[| M(x);  P(x) |] ==> \<exists>x[M]. P(x)"
   1.199  by blast
   1.200  
   1.201 -(*Not of the general form for such rules; ~EX has become ALL~ *)
   1.202 -lemma rexCI: "[| ALL x[M]. ~P(x) ==> P(a); M(a) |] ==> EX x[M]. P(x)"
   1.203 +(*Not of the general form for such rules... *)
   1.204 +lemma rexCI: "[| \<forall>x[M]. ~P(x) ==> P(a); M(a) |] ==> \<exists>x[M]. P(x)"
   1.205  by blast
   1.206  
   1.207 -lemma rexE [elim!]: "[| EX x[M]. P(x);  !!x. [| M(x); P(x) |] ==> Q |] ==> Q"
   1.208 +lemma rexE [elim!]: "[| \<exists>x[M]. P(x);  !!x. [| M(x); P(x) |] ==> Q |] ==> Q"
   1.209  by (simp add: rex_def, blast)
   1.210  
   1.211  (*We do not even have (EX x[M]. True) <-> True unless A is nonempty!!*)
   1.212 @@ -265,7 +264,7 @@
   1.213  by (simp add: rex_def)
   1.214  
   1.215  lemma rex_cong [cong]:
   1.216 -    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (EX x[M]. P(x)) <-> (EX x[M]. P'(x))"
   1.217 +    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (\<exists>x[M]. P(x)) <-> (\<exists>x[M]. P'(x))"
   1.218  by (simp add: rex_def cong: conj_cong)
   1.219  
   1.220  lemma rall_is_ball [simp]: "(\<forall>x[%z. z\<in>A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
   1.221 @@ -274,68 +273,68 @@
   1.222  lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
   1.223  by blast
   1.224  
   1.225 -lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (ALL x[M]. P(x))";
   1.226 +lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))";
   1.227  by (simp add: rall_def atomize_all atomize_imp)
   1.228  
   1.229  declare atomize_rall [symmetric, rulify]
   1.230  
   1.231  lemma rall_simps1:
   1.232 -     "(ALL x[M]. P(x) & Q)   <-> (ALL x[M]. P(x)) & ((ALL x[M]. False) | Q)"
   1.233 -     "(ALL x[M]. P(x) | Q)   <-> ((ALL x[M]. P(x)) | Q)"
   1.234 -     "(ALL x[M]. P(x) --> Q) <-> ((EX x[M]. P(x)) --> Q)"
   1.235 -     "(~(ALL x[M]. P(x))) <-> (EX x[M]. ~P(x))"
   1.236 +     "(\<forall>x[M]. P(x) & Q)   <-> (\<forall>x[M]. P(x)) & ((\<forall>x[M]. False) | Q)"
   1.237 +     "(\<forall>x[M]. P(x) | Q)   <-> ((\<forall>x[M]. P(x)) | Q)"
   1.238 +     "(\<forall>x[M]. P(x) \<longrightarrow> Q) <-> ((\<exists>x[M]. P(x)) \<longrightarrow> Q)"
   1.239 +     "(~(\<forall>x[M]. P(x))) <-> (\<exists>x[M]. ~P(x))"
   1.240  by blast+
   1.241  
   1.242  lemma rall_simps2:
   1.243 -     "(ALL x[M]. P & Q(x))   <-> ((ALL x[M]. False) | P) & (ALL x[M]. Q(x))"
   1.244 -     "(ALL x[M]. P | Q(x))   <-> (P | (ALL x[M]. Q(x)))"
   1.245 -     "(ALL x[M]. P --> Q(x)) <-> (P --> (ALL x[M]. Q(x)))"
   1.246 +     "(\<forall>x[M]. P & Q(x))   <-> ((\<forall>x[M]. False) | P) & (\<forall>x[M]. Q(x))"
   1.247 +     "(\<forall>x[M]. P | Q(x))   <-> (P | (\<forall>x[M]. Q(x)))"
   1.248 +     "(\<forall>x[M]. P \<longrightarrow> Q(x)) <-> (P \<longrightarrow> (\<forall>x[M]. Q(x)))"
   1.249  by blast+
   1.250  
   1.251  lemmas rall_simps [simp] = rall_simps1 rall_simps2
   1.252  
   1.253  lemma rall_conj_distrib:
   1.254 -    "(ALL x[M]. P(x) & Q(x)) <-> ((ALL x[M]. P(x)) & (ALL x[M]. Q(x)))"
   1.255 +    "(\<forall>x[M]. P(x) & Q(x)) <-> ((\<forall>x[M]. P(x)) & (\<forall>x[M]. Q(x)))"
   1.256  by blast
   1.257  
   1.258  lemma rex_simps1:
   1.259 -     "(EX x[M]. P(x) & Q) <-> ((EX x[M]. P(x)) & Q)"
   1.260 -     "(EX x[M]. P(x) | Q) <-> (EX x[M]. P(x)) | ((EX x[M]. True) & Q)"
   1.261 -     "(EX x[M]. P(x) --> Q) <-> ((ALL x[M]. P(x)) --> ((EX x[M]. True) & Q))"
   1.262 -     "(~(EX x[M]. P(x))) <-> (ALL x[M]. ~P(x))"
   1.263 +     "(\<exists>x[M]. P(x) & Q) <-> ((\<exists>x[M]. P(x)) & Q)"
   1.264 +     "(\<exists>x[M]. P(x) | Q) <-> (\<exists>x[M]. P(x)) | ((\<exists>x[M]. True) & Q)"
   1.265 +     "(\<exists>x[M]. P(x) \<longrightarrow> Q) <-> ((\<forall>x[M]. P(x)) \<longrightarrow> ((\<exists>x[M]. True) & Q))"
   1.266 +     "(~(\<exists>x[M]. P(x))) <-> (\<forall>x[M]. ~P(x))"
   1.267  by blast+
   1.268  
   1.269  lemma rex_simps2:
   1.270 -     "(EX x[M]. P & Q(x)) <-> (P & (EX x[M]. Q(x)))"
   1.271 -     "(EX x[M]. P | Q(x)) <-> ((EX x[M]. True) & P) | (EX x[M]. Q(x))"
   1.272 -     "(EX x[M]. P --> Q(x)) <-> (((ALL x[M]. False) | P) --> (EX x[M]. Q(x)))"
   1.273 +     "(\<exists>x[M]. P & Q(x)) <-> (P & (\<exists>x[M]. Q(x)))"
   1.274 +     "(\<exists>x[M]. P | Q(x)) <-> ((\<exists>x[M]. True) & P) | (\<exists>x[M]. Q(x))"
   1.275 +     "(\<exists>x[M]. P \<longrightarrow> Q(x)) <-> (((\<forall>x[M]. False) | P) \<longrightarrow> (\<exists>x[M]. Q(x)))"
   1.276  by blast+
   1.277  
   1.278  lemmas rex_simps [simp] = rex_simps1 rex_simps2
   1.279  
   1.280  lemma rex_disj_distrib:
   1.281 -    "(EX x[M]. P(x) | Q(x)) <-> ((EX x[M]. P(x)) | (EX x[M]. Q(x)))"
   1.282 +    "(\<exists>x[M]. P(x) | Q(x)) <-> ((\<exists>x[M]. P(x)) | (\<exists>x[M]. Q(x)))"
   1.283  by blast
   1.284  
   1.285  
   1.286  subsubsection{*One-point rule for bounded quantifiers*}
   1.287  
   1.288 -lemma rex_triv_one_point1 [simp]: "(EX x[M]. x=a) <-> ( M(a))"
   1.289 +lemma rex_triv_one_point1 [simp]: "(\<exists>x[M]. x=a) <-> ( M(a))"
   1.290  by blast
   1.291  
   1.292 -lemma rex_triv_one_point2 [simp]: "(EX x[M]. a=x) <-> ( M(a))"
   1.293 +lemma rex_triv_one_point2 [simp]: "(\<exists>x[M]. a=x) <-> ( M(a))"
   1.294  by blast
   1.295  
   1.296 -lemma rex_one_point1 [simp]: "(EX x[M]. x=a & P(x)) <-> ( M(a) & P(a))"
   1.297 +lemma rex_one_point1 [simp]: "(\<exists>x[M]. x=a & P(x)) <-> ( M(a) & P(a))"
   1.298  by blast
   1.299  
   1.300 -lemma rex_one_point2 [simp]: "(EX x[M]. a=x & P(x)) <-> ( M(a) & P(a))"
   1.301 +lemma rex_one_point2 [simp]: "(\<exists>x[M]. a=x & P(x)) <-> ( M(a) & P(a))"
   1.302  by blast
   1.303  
   1.304 -lemma rall_one_point1 [simp]: "(ALL x[M]. x=a --> P(x)) <-> ( M(a) --> P(a))"
   1.305 +lemma rall_one_point1 [simp]: "(\<forall>x[M]. x=a \<longrightarrow> P(x)) <-> ( M(a) \<longrightarrow> P(a))"
   1.306  by blast
   1.307  
   1.308 -lemma rall_one_point2 [simp]: "(ALL x[M]. a=x --> P(x)) <-> ( M(a) --> P(a))"
   1.309 +lemma rall_one_point2 [simp]: "(\<forall>x[M]. a=x \<longrightarrow> P(x)) <-> ( M(a) \<longrightarrow> P(a))"
   1.310  by blast
   1.311  
   1.312  
   1.313 @@ -343,9 +342,9 @@
   1.314  
   1.315  definition
   1.316    setclass :: "[i,i] => o"       ("##_" [40] 40)  where
   1.317 -   "setclass(A) == %x. x : A"
   1.318 +   "setclass(A) == %x. x \<in> A"
   1.319  
   1.320 -lemma setclass_iff [simp]: "setclass(A,x) <-> x : A"
   1.321 +lemma setclass_iff [simp]: "setclass(A,x) <-> x \<in> A"
   1.322  by (simp add: setclass_def)
   1.323  
   1.324  lemma rall_setclass_is_ball [simp]: "(\<forall>x[##A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
   1.325 @@ -368,14 +367,14 @@
   1.326  
   1.327  text {* Setting up the one-point-rule simproc *}
   1.328  
   1.329 -simproc_setup defined_rex ("EX x[M]. P(x) & Q(x)") = {*
   1.330 +simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = {*
   1.331    let
   1.332      val unfold_rex_tac = unfold_tac @{thms rex_def};
   1.333      fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
   1.334    in fn _ => fn ss => Quantifier1.rearrange_bex (prove_rex_tac ss) ss end
   1.335  *}
   1.336  
   1.337 -simproc_setup defined_rall ("ALL x[M]. P(x) --> Q(x)") = {*
   1.338 +simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = {*
   1.339    let
   1.340      val unfold_rall_tac = unfold_tac @{thms rall_def};
   1.341      fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;