src/ZF/OrdQuant.thy
changeset 12825 f1f7964ed05c
parent 12820 02e2ff3e4d37
child 13118 336b0bcbd27c
     1.1 --- a/src/ZF/OrdQuant.thy	Mon Jan 21 14:47:47 2002 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Mon Jan 21 14:47:55 2002 +0100
     1.3 @@ -36,6 +36,28 @@
     1.4    "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
     1.5  
     1.6  
     1.7 +(** simplification of the new quantifiers **)
     1.8 +
     1.9 +
    1.10 +(*MOST IMPORTANT that this is added to the simpset BEFORE OrdQuant.ML
    1.11 +  is loaded: it's Ord_atomize would convert this rule to 
    1.12 +    x < 0 ==> P(x) == True, which causes dire effects!*)
    1.13 +lemma [simp]: "(ALL x<0. P(x))"
    1.14 +by (simp add: oall_def) 
    1.15 +
    1.16 +lemma [simp]: "~(EX x<0. P(x))"
    1.17 +by (simp add: oex_def) 
    1.18 +
    1.19 +lemma [simp]: "(ALL x<succ(i). P(x)) <-> (Ord(i) --> P(i) & (ALL x<i. P(x)))"
    1.20 +apply (simp add: oall_def le_iff) 
    1.21 +apply (blast intro: lt_Ord2) 
    1.22 +done
    1.23 +
    1.24 +lemma [simp]: "(EX x<succ(i). P(x)) <-> (Ord(i) & (P(i) | (EX x<i. P(x))))"
    1.25 +apply (simp add: oex_def le_iff) 
    1.26 +apply (blast intro: lt_Ord2) 
    1.27 +done
    1.28 +
    1.29  declare Ord_Un [intro,simp,TC]
    1.30  declare Ord_UN [intro,simp,TC]
    1.31  declare Ord_Union [intro,simp,TC]
    1.32 @@ -62,11 +84,11 @@
    1.33  lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)"
    1.34  apply (simp add: Limit_def lt_Ord2, clarify)
    1.35  apply (drule_tac i=y in ltD) 
    1.36 -apply (blast intro: lt_trans1 succ_leI ltI lt_Ord2)
    1.37 +apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2)
    1.38  done
    1.39  
    1.40  lemma UN_upper_lt:
    1.41 -     "\<lbrakk>a\<in> A;  i < b(a);  Ord(\<Union>x\<in>A. b(x))\<rbrakk> \<Longrightarrow> i < (\<Union>x\<in>A. b(x))"
    1.42 +     "\<lbrakk>a\<in>A;  i < b(a);  Ord(\<Union>x\<in>A. b(x))\<rbrakk> \<Longrightarrow> i < (\<Union>x\<in>A. b(x))"
    1.43  by (unfold lt_def, blast) 
    1.44  
    1.45  lemma lt_imp_0_lt: "j<i \<Longrightarrow> 0<i"