src/ZF/OrdQuant.thy
author paulson
Fri May 17 16:54:25 2002 +0200 (2002-05-17)
changeset 13162 660a71e712af
parent 13149 773657d466cb
child 13169 394a6c649547
permissions -rw-r--r--
New theorems from Constructible, and moving some Isar material from Main
     1 (*  Title:      ZF/AC/OrdQuant.thy
     2     ID:         $Id$
     3     Authors:    Krzysztof Grabczewski and L C Paulson
     4 
     5 Quantifiers and union operator for ordinals. 
     6 *)
     7 
     8 theory OrdQuant = Ordinal:
     9 
    10 constdefs
    11   
    12   (* Ordinal Quantifiers *)
    13   oall :: "[i, i => o] => o"
    14     "oall(A, P) == ALL x. x<A --> P(x)"
    15   
    16   oex :: "[i, i => o] => o"
    17     "oex(A, P)  == EX x. x<A & P(x)"
    18 
    19   (* Ordinal Union *)
    20   OUnion :: "[i, i => i] => i"
    21     "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
    22   
    23 syntax
    24   "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
    25   "@oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
    26   "@OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
    27 
    28 translations
    29   "ALL x<a. P"  == "oall(a, %x. P)"
    30   "EX x<a. P"   == "oex(a, %x. P)"
    31   "UN x<a. B"   == "OUnion(a, %x. B)"
    32 
    33 syntax (xsymbols)
    34   "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    35   "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    36   "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    37 
    38 
    39 (** simplification of the new quantifiers **)
    40 
    41 
    42 (*MOST IMPORTANT that this is added to the simpset BEFORE OrdQuant.ML
    43   is loaded: it's Ord_atomize would convert this rule to 
    44     x < 0 ==> P(x) == True, which causes dire effects!*)
    45 lemma [simp]: "(ALL x<0. P(x))"
    46 by (simp add: oall_def) 
    47 
    48 lemma [simp]: "~(EX x<0. P(x))"
    49 by (simp add: oex_def) 
    50 
    51 lemma [simp]: "(ALL x<succ(i). P(x)) <-> (Ord(i) --> P(i) & (ALL x<i. P(x)))"
    52 apply (simp add: oall_def le_iff) 
    53 apply (blast intro: lt_Ord2) 
    54 done
    55 
    56 lemma [simp]: "(EX x<succ(i). P(x)) <-> (Ord(i) & (P(i) | (EX x<i. P(x))))"
    57 apply (simp add: oex_def le_iff) 
    58 apply (blast intro: lt_Ord2) 
    59 done
    60 
    61 declare Ord_Un [intro,simp,TC]
    62 declare Ord_UN [intro,simp,TC]
    63 declare Ord_Union [intro,simp,TC]
    64 
    65 (** Now some very basic ZF theorems **)
    66 
    67 lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
    68 by blast
    69 
    70 lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
    71 by blast
    72 
    73 lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
    74 by (unfold trans_def trans_on_def, blast)
    75 
    76 lemma image_is_UN: "[| function(g); x <= domain(g) |] ==> g``x = (UN k:x. {g`k})"
    77 by (blast intro: function_apply_equality [THEN sym] function_apply_Pair) 
    78 
    79 lemma functionI: 
    80      "[| !!x y y'. [| <x,y>:r; <x,y'>:r |] ==> y=y' |] ==> function(r)"
    81 by (simp add: function_def, blast) 
    82 
    83 lemma function_lam: "function (lam x:A. b(x))"
    84 by (simp add: function_def lam_def) 
    85 
    86 lemma relation_lam: "relation (lam x:A. b(x))"  
    87 by (simp add: relation_def lam_def) 
    88 
    89 lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
    90 by (simp add: restrict_def) 
    91 
    92 (** These mostly belong to theory Ordinal **)
    93 
    94 lemma Union_upper_le:
    95      "[| j: J;  i\<le>j;  Ord(\<Union>(J)) |] ==> i \<le> \<Union>J"
    96 apply (subst Union_eq_UN)  
    97 apply (rule UN_upper_le, auto)
    98 done
    99 
   100 lemma zero_not_Limit [iff]: "~ Limit(0)"
   101 by (simp add: Limit_def)
   102 
   103 lemma Limit_has_1: "Limit(i) ==> 1 < i"
   104 by (blast intro: Limit_has_0 Limit_has_succ)
   105 
   106 lemma Limit_Union [rule_format]: "[| I \<noteq> 0;  \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)"
   107 apply (simp add: Limit_def lt_def)
   108 apply (blast intro!: equalityI)
   109 done
   110 
   111 lemma increasing_LimitI: "[| 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y |] ==> Limit(l)"
   112 apply (simp add: Limit_def lt_Ord2, clarify)
   113 apply (drule_tac i=y in ltD) 
   114 apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2)
   115 done
   116 
   117 lemma UN_upper_lt:
   118      "[| a\<in>A;  i < b(a);  Ord(\<Union>x\<in>A. b(x)) |] ==> i < (\<Union>x\<in>A. b(x))"
   119 by (unfold lt_def, blast) 
   120 
   121 lemma lt_imp_0_lt: "j<i ==> 0<i"
   122 by (blast intro: lt_trans1 Ord_0_le [OF lt_Ord]) 
   123 
   124 lemma Ord_set_cases:
   125    "\<forall>i\<in>I. Ord(i) ==> I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))"
   126 apply (clarify elim!: not_emptyE) 
   127 apply (cases "\<Union>(I)" rule: Ord_cases) 
   128    apply (blast intro: Ord_Union)
   129   apply (blast intro: subst_elem)
   130  apply auto 
   131 apply (clarify elim!: equalityE succ_subsetE)
   132 apply (simp add: Union_subset_iff)
   133 apply (subgoal_tac "B = succ(j)", blast )
   134 apply (rule le_anti_sym) 
   135  apply (simp add: le_subset_iff) 
   136 apply (simp add: ltI)
   137 done
   138 
   139 lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x);  \<Union>X = succ(j)|] ==> succ(j) \<in> X"
   140 by (drule Ord_set_cases, auto)
   141 
   142 (*See also Transset_iff_Union_succ*)
   143 lemma Ord_Union_succ_eq: "Ord(i) ==> \<Union>(succ(i)) = i"
   144 by (blast intro: Ord_trans)
   145 
   146 lemma lt_Union_iff: "\<forall>i\<in>A. Ord(i) ==> (j < \<Union>(A)) <-> (\<exists>i\<in>A. j<i)"
   147 by (auto simp: lt_def Ord_Union)
   148 
   149 lemma Un_upper1_lt: "[|k < i; Ord(j)|] ==> k < i Un j"
   150 by (simp add: lt_def) 
   151 
   152 lemma Un_upper2_lt: "[|k < j; Ord(i)|] ==> k < i Un j"
   153 by (simp add: lt_def) 
   154 
   155 lemma Ord_OUN [intro,simp]:
   156      "[| !!x. x<A ==> Ord(B(x)) |] ==> Ord(\<Union>x<A. B(x))"
   157 by (simp add: OUnion_def ltI Ord_UN) 
   158 
   159 lemma OUN_upper_lt:
   160      "[| a<A;  i < b(a);  Ord(\<Union>x<A. b(x)) |] ==> i < (\<Union>x<A. b(x))"
   161 by (unfold OUnion_def lt_def, blast )
   162 
   163 lemma OUN_upper_le:
   164      "[| a<A;  i\<le>b(a);  Ord(\<Union>x<A. b(x)) |] ==> i \<le> (\<Union>x<A. b(x))"
   165 apply (unfold OUnion_def, auto)
   166 apply (rule UN_upper_le )
   167 apply (auto simp add: lt_def) 
   168 done
   169 
   170 lemma Limit_OUN_eq: "Limit(i) ==> (UN x<i. x) = i"
   171 by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord)
   172 
   173 (* No < version; consider (UN i:nat.i)=nat *)
   174 lemma OUN_least:
   175      "(!!x. x<A ==> B(x) \<subseteq> C) ==> (UN x<A. B(x)) \<subseteq> C"
   176 by (simp add: OUnion_def UN_least ltI)
   177 
   178 (* No < version; consider (UN i:nat.i)=nat *)
   179 lemma OUN_least_le:
   180      "[| Ord(i);  !!x. x<A ==> b(x) \<le> i |] ==> (UN x<A. b(x)) \<le> i"
   181 by (simp add: OUnion_def UN_least_le ltI Ord_0_le)
   182 
   183 lemma le_implies_OUN_le_OUN:
   184      "[| !!x. x<A ==> c(x) \<le> d(x) |] ==> (UN x<A. c(x)) \<le> (UN x<A. d(x))"
   185 by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN)
   186 
   187 lemma OUN_UN_eq:
   188      "(!!x. x:A ==> Ord(B(x)))
   189       ==> (UN z < (UN x:A. B(x)). C(z)) = (UN  x:A. UN z < B(x). C(z))"
   190 by (simp add: OUnion_def) 
   191 
   192 lemma OUN_Union_eq:
   193      "(!!x. x:X ==> Ord(x))
   194       ==> (UN z < Union(X). C(z)) = (UN x:X. UN z < x. C(z))"
   195 by (simp add: OUnion_def) 
   196 
   197 (*So that rule_format will get rid of ALL x<A...*)
   198 lemma atomize_oall [symmetric, rulify]:
   199      "(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))"
   200 by (simp add: oall_def atomize_all atomize_imp)
   201 
   202 end