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.24
1.25 -lemma [simp]: "~(EX x<0. P(x))"
1.26 +lemma [simp]: "~(\<exists>x<0. P(x))"
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.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.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.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.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.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.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.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.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;
```