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.10  by (simp add: oall_def)
    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.20  apply (simp add: oex_def cong add: conj_cong)
    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.30  by (simp add: rall_def)
    1.31  
    1.32  (*** Relativized existential quantifier ***)
    1.33 @@ -255,9 +258,16 @@
    1.34  by (simp add: rex_def)
    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)))"