src/ZF/OrdQuant.thy
 changeset 13289 53e201efdaa2 parent 13253 edbf32029d33 child 13298 b4f370679c65
```     1.1 --- a/src/ZF/OrdQuant.thy	Wed Jul 03 14:52:57 2002 +0200
1.2 +++ b/src/ZF/OrdQuant.thy	Thu Jul 04 10:50:24 2002 +0200
1.3 @@ -135,7 +135,8 @@
1.4
1.5  (*Congruence rule for rewriting*)
1.6  lemma oall_cong [cong]:
1.7 -    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')"
1.8 +    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |]
1.9 +     ==> oall(a, %x. P(x)) <-> oall(a', %x. P'(x))"
1.11
1.12
1.13 @@ -158,7 +159,8 @@
1.14  done
1.15
1.16  lemma oex_cong [cong]:
1.17 -    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oex(a,P) <-> oex(a',P')"
1.18 +    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |]
1.19 +     ==> oex(a, %x. P(x)) <-> oex(a', %x. P'(x))"
1.21  done
1.22
1.23 @@ -231,7 +233,8 @@
1.24
1.25  (*Congruence rule for rewriting*)
1.26  lemma rall_cong [cong]:
1.27 -    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> rall(M,P) <-> rall(M,P')"
1.28 +    "(!!x. M(x) ==> P(x) <-> P'(x))
1.29 +     ==> rall(M, %x. P(x)) <-> rall(M, %x. P'(x))"
1.31
1.32  (*** Relativized existential quantifier ***)
1.33 @@ -255,9 +258,16 @@
1.35
1.36  lemma rex_cong [cong]:
1.37 -    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> rex(M,P) <-> rex(M,P')"
1.38 +    "(!!x. M(x) ==> P(x) <-> P'(x))
1.39 +     ==> rex(M, %x. P(x)) <-> rex(M, %x. P'(x))"
1.40  by (simp add: rex_def cong: conj_cong)
1.41
1.42 +lemma rall_is_ball [simp]: "(\<forall>x[%z. z\<in>A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
1.43 +by blast
1.44 +
1.45 +lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
1.46 +by blast
1.47 +
1.48  lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (ALL x[M]. P(x))";
1.49  by (simp add: rall_def atomize_all atomize_imp)
1.50
1.51 @@ -276,7 +286,7 @@
1.52       "(ALL x[M]. P --> Q(x)) <-> (P --> (ALL x[M]. Q(x)))"
1.53  by blast+
1.54
1.55 -lemmas rall_simps = rall_simps1 rall_simps2
1.56 +lemmas rall_simps [simp] = rall_simps1 rall_simps2
1.57
1.58  lemma rall_conj_distrib:
1.59      "(ALL x[M]. P(x) & Q(x)) <-> ((ALL x[M]. P(x)) & (ALL x[M]. Q(x)))"
1.60 @@ -295,7 +305,7 @@
1.61       "(EX x[M]. P --> Q(x)) <-> (((ALL x[M]. False) | P) --> (EX x[M]. Q(x)))"
1.62  by blast+
1.63
1.64 -lemmas rex_simps = rex_simps1 rex_simps2
1.65 +lemmas rex_simps [simp] = rex_simps1 rex_simps2
1.66
1.67  lemma rex_disj_distrib:
1.68      "(EX x[M]. P(x) | Q(x)) <-> ((EX x[M]. P(x)) | (EX x[M]. Q(x)))"
```