src/ZF/ZF.thy
 changeset 65464 f3cd78ba687c parent 65386 e3fb3036a00e parent 65453 b2562bdda54e child 68490 eb53f944c8cd
equal inserted replaced
65438:f556a7a9080c 65464:f3cd78ba687c
`     1 (*  Title:      ZF/ZF.thy`
`     1 section\<open>Main ZF Theory: Everything Except AC\<close>`
`     2     Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory`
`       `
`     3     Copyright   1993  University of Cambridge`
`       `
`     4 *)`
`       `
`     5 `
`     2 `
`     6 section \<open>Zermelo-Fraenkel Set Theory\<close>`
`     3 theory ZF imports List_ZF IntDiv_ZF CardinalArith begin`
`     7 `
`     4 `
`     8 theory ZF`
`     5 (*The theory of "iterates" logically belongs to Nat, but can't go there because`
`     9 imports "~~/src/FOL/FOL"`
`     6   primrec isn't available into after Datatype.*)`
`    10 begin`
`       `
`    11 `
`     7 `
`    12 subsection \<open>Signature\<close>`
`     8 subsection\<open>Iteration of the function @{term F}\<close>`
`    13 `
`     9 `
`    14 declare [[eta_contract = false]]`
`    10 consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)`
`    15 `
`    11 `
`    16 typedecl i`
`    12 primrec`
`    17 instance i :: "term" ..`
`    13     "F^0 (x) = x"`
`       `
`    14     "F^(succ(n)) (x) = F(F^n (x))"`
`    18 `
`    15 `
`    19 axiomatization mem :: "[i, i] \<Rightarrow> o"  (infixl "\<in>" 50)  \<comment> \<open>membership relation\<close>`
`    16 definition`
`    20   and zero :: "i"  ("0")  \<comment> \<open>the empty set\<close>`
`    17   iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) where`
`    21   and Pow :: "i \<Rightarrow> i"  \<comment> \<open>power sets\<close>`
`    18     "F^\<omega> (x) == \<Union>n\<in>nat. F^n (x)"`
`    22   and Inf :: "i"  \<comment> \<open>infinite set\<close>`
`       `
`    23   and Union :: "i \<Rightarrow> i"  ("\<Union>_" [90] 90)`
`       `
`    24   and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"`
`       `
`    25 `
`    19 `
`    26 abbreviation not_mem :: "[i, i] \<Rightarrow> o"  (infixl "\<notin>" 50)  \<comment> \<open>negated membership relation\<close>`
`    20 lemma iterates_triv:`
`    27   where "x \<notin> y \<equiv> \<not> (x \<in> y)"`
`    21      "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"`
`       `
`    22 by (induct n rule: nat_induct, simp_all)`
`       `
`    23 `
`       `
`    24 lemma iterates_type [TC]:`
`       `
`    25      "[| n \<in> nat;  a \<in> A; !!x. x \<in> A ==> F(x) \<in> A |]`
`       `
`    26       ==> F^n (a) \<in> A"`
`       `
`    27 by (induct n rule: nat_induct, simp_all)`
`       `
`    28 `
`       `
`    29 lemma iterates_omega_triv:`
`       `
`    30     "F(x) = x ==> F^\<omega> (x) = x"`
`       `
`    31 by (simp add: iterates_omega_def iterates_triv)`
`       `
`    32 `
`       `
`    33 lemma Ord_iterates [simp]:`
`       `
`    34      "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |]`
`       `
`    35       ==> Ord(F^n (x))"`
`       `
`    36 by (induct n rule: nat_induct, simp_all)`
`       `
`    37 `
`       `
`    38 lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"`
`       `
`    39 by (induct_tac n, simp_all)`
`    28 `
`    40 `
`    29 `
`    41 `
`    30 subsection \<open>Bounded Quantifiers\<close>`
`    42 subsection\<open>Transfinite Recursion\<close>`
`    31 `
`    43 `
`    32 definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o"`
`    44 text\<open>Transfinite recursion for definitions based on the`
`    33   where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)"`
`    45     three cases of ordinals\<close>`
`    34 `
`    46 `
`    35 definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o"`
`    47 definition`
`    36   where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"`
`    48   transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where`
`       `
`    49     "transrec3(k, a, b, c) ==`
`       `
`    50        transrec(k, \<lambda>x r.`
`       `
`    51          if x=0 then a`
`       `
`    52          else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)`
`       `
`    53          else b(Arith.pred(x), r ` Arith.pred(x)))"`
`    37 `
`    54 `
`    38 syntax`
`    55 lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"`
`    39   "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<forall>_\<in>_./ _)" 10)`
`    56 by (rule transrec3_def [THEN def_transrec, THEN trans], simp)`
`    40   "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<exists>_\<in>_./ _)" 10)`
`    57 `
`    41 translations`
`    58 lemma transrec3_succ [simp]:`
`    42   "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"`
`    59      "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"`
`    43   "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"`
`    60 by (rule transrec3_def [THEN def_transrec, THEN trans], simp)`
`       `
`    61 `
`       `
`    62 lemma transrec3_Limit:`
`       `
`    63      "Limit(i) ==>`
`       `
`    64       transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"`
`       `
`    65 by (rule transrec3_def [THEN def_transrec, THEN trans], force)`
`    44 `
`    66 `
`    45 `
`    67 `
`    46 subsection \<open>Variations on Replacement\<close>`
`    68 declaration \<open>fn _ =>`
`    47 `
`    69   Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>`
`    48 (* Derived form of replacement, restricting P to its functional part.`
`    70     map mk_eq o Ord_atomize o Variable.gen_all ctxt))`
`    49    The resulting set (for functional P) is the same as with`
`    71 \<close>`
`    50    PrimReplace, but the rules are simpler. *)`
`       `
`    51 definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"`
`       `
`    52   where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"`
`       `
`    53 `
`       `
`    54 syntax`
`       `
`    55   "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")`
`       `
`    56 translations`
`       `
`    57   "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"`
`       `
`    58 `
`       `
`    59 `
`       `
`    60 (* Functional form of replacement -- analgous to ML's map functional *)`
`       `
`    61 `
`       `
`    62 definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i"`
`       `
`    63   where "RepFun(A,f) == {y . x\<in>A, y=f(x)}"`
`       `
`    64 `
`       `
`    65 syntax`
`       `
`    66   "_RepFun" :: "[i, pttrn, i] => i"  ("(1{_ ./ _ \<in> _})" [51,0,51])`
`       `
`    67 translations`
`       `
`    68   "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"`
`       `
`    69 `
`       `
`    70 `
`       `
`    71 (* Separation and Pairing can be derived from the Replacement`
`       `
`    72    and Powerset Axioms using the following definitions. *)`
`       `
`    73 definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i"`
`       `
`    74   where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"`
`       `
`    75 `
`       `
`    76 syntax`
`       `
`    77   "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  ("(1{_ \<in> _ ./ _})")`
`       `
`    78 translations`
`       `
`    79   "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"`
`       `
`    80 `
`       `
`    81 `
`       `
`    82 subsection \<open>General union and intersection\<close>`
`       `
`    83 `
`       `
`    84 definition Inter :: "i => i"  ("\<Inter>_" [90] 90)`
`       `
`    85   where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"`
`       `
`    86 `
`       `
`    87 syntax`
`       `
`    88   "_UNION" :: "[pttrn, i, i] => i"  ("(3\<Union>_\<in>_./ _)" 10)`
`       `
`    89   "_INTER" :: "[pttrn, i, i] => i"  ("(3\<Inter>_\<in>_./ _)" 10)`
`       `
`    90 translations`
`       `
`    91   "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"`
`       `
`    92   "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"`
`       `
`    93 `
`       `
`    94 `
`       `
`    95 subsection \<open>Finite sets and binary operations\<close>`
`       `
`    96 `
`       `
`    97 (*Unordered pairs (Upair) express binary union/intersection and cons;`
`       `
`    98   set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)`
`       `
`    99 `
`       `
`   100 definition Upair :: "[i, i] => i"`
`       `
`   101   where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"`
`       `
`   102 `
`       `
`   103 definition Subset :: "[i, i] \<Rightarrow> o"  (infixl "\<subseteq>" 50)  \<comment> \<open>subset relation\<close>`
`       `
`   104   where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B"`
`       `
`   105 `
`       `
`   106 definition Diff :: "[i, i] \<Rightarrow> i"  (infixl "-" 65)  \<comment> \<open>set difference\<close>`
`       `
`   107   where "A - B == { x\<in>A . ~(x\<in>B) }"`
`       `
`   108 `
`       `
`   109 definition Un :: "[i, i] \<Rightarrow> i"  (infixl "\<union>" 65)  \<comment> \<open>binary union\<close>`
`       `
`   110   where "A \<union> B == \<Union>(Upair(A,B))"`
`       `
`   111 `
`       `
`   112 definition Int :: "[i, i] \<Rightarrow> i"  (infixl "\<inter>" 70)  \<comment> \<open>binary intersection\<close>`
`       `
`   113   where "A \<inter> B == \<Inter>(Upair(A,B))"`
`       `
`   114 `
`       `
`   115 definition cons :: "[i, i] => i"`
`       `
`   116   where "cons(a,A) == Upair(a,a) \<union> A"`
`       `
`   117 `
`       `
`   118 definition succ :: "i => i"`
`       `
`   119   where "succ(i) == cons(i, i)"`
`       `
`   120 `
`       `
`   121 nonterminal "is"`
`       `
`   122 syntax`
`       `
`   123   "" :: "i \<Rightarrow> is"  ("_")`
`       `
`   124   "_Enum" :: "[i, is] \<Rightarrow> is"  ("_,/ _")`
`       `
`   125   "_Finset" :: "is \<Rightarrow> i"  ("{(_)}")`
`       `
`   126 translations`
`       `
`   127   "{x, xs}" == "CONST cons(x, {xs})"`
`       `
`   128   "{x}" == "CONST cons(x, 0)"`
`       `
`   129 `
`       `
`   130 `
`       `
`   131 subsection \<open>Axioms\<close>`
`       `
`   132 `
`       `
`   133 (* ZF axioms -- see Suppes p.238`
`       `
`   134    Axioms for Union, Pow and Replace state existence only,`
`       `
`   135    uniqueness is derivable using extensionality. *)`
`       `
`   136 `
`       `
`   137 axiomatization`
`       `
`   138 where`
`       `
`   139   extension:     "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and`
`       `
`   140   Union_iff:     "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and`
`       `
`   141   Pow_iff:       "A \<in> Pow(B) \<longleftrightarrow> A \<subseteq> B" and`
`       `
`   142 `
`       `
`   143   (*We may name this set, though it is not uniquely defined.*)`
`       `
`   144   infinity:      "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and`
`       `
`   145 `
`       `
`   146   (*This formulation facilitates case analysis on A.*)`
`       `
`   147   foundation:    "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and`
`       `
`   148 `
`       `
`   149   (*Schema axiom since predicate P is a higher-order variable*)`
`       `
`   150   replacement:   "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow>`
`       `
`   151                          b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))"`
`       `
`   152 `
`       `
`   153 `
`       `
`   154 subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>`
`       `
`   155 `
`       `
`   156 definition The :: "(i \<Rightarrow> o) \<Rightarrow> i"  (binder "THE " 10)`
`       `
`   157   where the_def: "The(P)    == \<Union>({y . x \<in> {0}, P(y)})"`
`       `
`   158 `
`       `
`   159 definition If :: "[o, i, i] \<Rightarrow> i"  ("(if (_)/ then (_)/ else (_))" [10] 10)`
`       `
`   160   where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b"`
`       `
`   161 `
`       `
`   162 abbreviation (input)`
`       `
`   163   old_if :: "[o, i, i] => i"  ("if '(_,_,_')")`
`       `
`   164   where "if(P,a,b) == If(P,a,b)"`
`       `
`   165 `
`       `
`   166 `
`       `
`   167 subsection \<open>Ordered Pairing\<close>`
`       `
`   168 `
`       `
`   169 (* this "symmetric" definition works better than {{a}, {a,b}} *)`
`       `
`   170 definition Pair :: "[i, i] => i"`
`       `
`   171   where "Pair(a,b) == {{a,a}, {a,b}}"`
`       `
`   172 `
`       `
`   173 definition fst :: "i \<Rightarrow> i"`
`       `
`   174   where "fst(p) == THE a. \<exists>b. p = Pair(a, b)"`
`       `
`   175 `
`       `
`   176 definition snd :: "i \<Rightarrow> i"`
`       `
`   177   where "snd(p) == THE b. \<exists>a. p = Pair(a, b)"`
`       `
`   178 `
`       `
`   179 definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>`
`       `
`   180   where "split(c) == \<lambda>p. c(fst(p), snd(p))"`
`       `
`   181 `
`       `
`   182 (* Patterns -- extends pre-defined type "pttrn" used in abstractions *)`
`       `
`   183 nonterminal patterns`
`       `
`   184 syntax`
`       `
`   185   "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")`
`       `
`   186   ""          :: "pttrn => patterns"         ("_")`
`       `
`   187   "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")`
`       `
`   188   "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")`
`       `
`   189 translations`
`       `
`   190   "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"`
`       `
`   191   "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"`
`       `
`   192   "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"`
`       `
`   193   "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"`
`       `
`   194 `
`       `
`   195 definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"`
`       `
`   196   where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"`
`       `
`   197 `
`       `
`   198 abbreviation cart_prod :: "[i, i] => i"  (infixr "\<times>" 80)  \<comment> \<open>Cartesian product\<close>`
`       `
`   199   where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"`
`       `
`   200 `
`       `
`   201 `
`       `
`   202 subsection \<open>Relations and Functions\<close>`
`       `
`   203 `
`       `
`   204 (*converse of relation r, inverse of function*)`
`       `
`   205 definition converse :: "i \<Rightarrow> i"`
`       `
`   206   where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}"`
`       `
`   207 `
`       `
`   208 definition domain :: "i \<Rightarrow> i"`
`       `
`   209   where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}"`
`       `
`   210 `
`       `
`   211 definition range :: "i \<Rightarrow> i"`
`       `
`   212   where "range(r) == domain(converse(r))"`
`       `
`   213 `
`       `
`   214 definition field :: "i \<Rightarrow> i"`
`       `
`   215   where "field(r) == domain(r) \<union> range(r)"`
`       `
`   216 `
`       `
`   217 definition relation :: "i \<Rightarrow> o"  \<comment> \<open>recognizes sets of pairs\<close>`
`       `
`   218   where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>"`
`       `
`   219 `
`       `
`   220 definition "function" :: "i \<Rightarrow> o"  \<comment> \<open>recognizes functions; can have non-pairs\<close>`
`       `
`   221   where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"`
`       `
`   222 `
`       `
`   223 definition Image :: "[i, i] \<Rightarrow> i"  (infixl "``" 90)  \<comment> \<open>image\<close>`
`       `
`   224   where image_def: "r `` A  == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}"`
`       `
`   225 `
`       `
`   226 definition vimage :: "[i, i] \<Rightarrow> i"  (infixl "-``" 90)  \<comment> \<open>inverse image\<close>`
`       `
`   227   where vimage_def: "r -`` A == converse(r)``A"`
`       `
`   228 `
`       `
`   229 (* Restrict the relation r to the domain A *)`
`       `
`   230 definition restrict :: "[i, i] \<Rightarrow> i"`
`       `
`   231   where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}"`
`       `
`   232 `
`       `
`   233 `
`       `
`   234 (* Abstraction, application and Cartesian product of a family of sets *)`
`       `
`   235 `
`       `
`   236 definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i"`
`       `
`   237   where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}"`
`       `
`   238 `
`       `
`   239 definition "apply" :: "[i, i] \<Rightarrow> i"  (infixl "`" 90)  \<comment> \<open>function application\<close>`
`       `
`   240   where "f`a == \<Union>(f``{a})"`
`       `
`   241 `
`       `
`   242 definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i"`
`       `
`   243   where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}"`
`       `
`   244 `
`       `
`   245 abbreviation function_space :: "[i, i] \<Rightarrow> i"  (infixr "->" 60)  \<comment> \<open>function space\<close>`
`       `
`   246   where "A -> B \<equiv> Pi(A, \<lambda>_. B)"`
`       `
`   247 `
`       `
`   248 `
`       `
`   249 (* binder syntax *)`
`       `
`   250 `
`       `
`   251 syntax`
`       `
`   252   "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Prod>_\<in>_./ _)" 10)`
`       `
`   253   "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sum>_\<in>_./ _)" 10)`
`       `
`   254   "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)`
`       `
`   255 translations`
`       `
`   256   "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"`
`       `
`   257   "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"`
`       `
`   258   "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"`
`       `
`   259 `
`       `
`   260 `
`       `
`   261 subsection \<open>ASCII syntax\<close>`
`       `
`   262 `
`       `
`   263 notation (ASCII)`
`       `
`   264   cart_prod       (infixr "*" 80) and`
`       `
`   265   Int             (infixl "Int" 70) and`
`       `
`   266   Un              (infixl "Un" 65) and`
`       `
`   267   function_space  (infixr "\<rightarrow>" 60) and`
`       `
`   268   Subset          (infixl "<=" 50) and`
`       `
`   269   mem             (infixl ":" 50) and`
`       `
`   270   not_mem         (infixl "~:" 50)`
`       `
`   271 `
`       `
`   272 syntax (ASCII)`
`       `
`   273   "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)`
`       `
`   274   "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)`
`       `
`   275   "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")`
`       `
`   276   "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")`
`       `
`   277   "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])`
`       `
`   278   "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)`
`       `
`   279   "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)`
`       `
`   280   "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)`
`       `
`   281   "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)`
`       `
`   282   "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)`
`       `
`   283   "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")`
`       `
`   284   "_pattern"  :: "patterns => pttrn"         ("<_>")`
`       `
`   285 `
`       `
`   286 `
`       `
`   287 subsection \<open>Substitution\<close>`
`       `
`   288 `
`       `
`   289 (*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)`
`       `
`   290 lemma subst_elem: "[| b\<in>A;  a=b |] ==> a\<in>A"`
`       `
`   291 by (erule ssubst, assumption)`
`       `
`   292 `
`       `
`   293 `
`       `
`   294 subsection\<open>Bounded universal quantifier\<close>`
`       `
`   295 `
`       `
`   296 lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)"`
`       `
`   297 by (simp add: Ball_def)`
`       `
`   298 `
`       `
`   299 lemmas strip = impI allI ballI`
`       `
`   300 `
`       `
`   301 lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x);  x: A |] ==> P(x)"`
`       `
`   302 by (simp add: Ball_def)`
`       `
`   303 `
`       `
`   304 (*Instantiates x first: better for automatic theorem proving?*)`
`       `
`   305 lemma rev_ballE [elim]:`
`       `
`   306     "[| \<forall>x\<in>A. P(x);  x\<notin>A ==> Q;  P(x) ==> Q |] ==> Q"`
`       `
`   307 by (simp add: Ball_def, blast)`
`       `
`   308 `
`       `
`   309 lemma ballE: "[| \<forall>x\<in>A. P(x);  P(x) ==> Q;  x\<notin>A ==> Q |] ==> Q"`
`       `
`   310 by blast`
`       `
`   311 `
`       `
`   312 (*Used in the datatype package*)`
`       `
`   313 lemma rev_bspec: "[| x: A;  \<forall>x\<in>A. P(x) |] ==> P(x)"`
`       `
`   314 by (simp add: Ball_def)`
`       `
`   315 `
`       `
`   316 (*Trival rewrite rule;   @{term"(\<forall>x\<in>A.P)<->P"} holds only if A is nonempty!*)`
`       `
`   317 lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<longrightarrow> P)"`
`       `
`   318 by (simp add: Ball_def)`
`       `
`   319 `
`       `
`   320 (*Congruence rule for rewriting*)`
`       `
`   321 lemma ball_cong [cong]:`
`       `
`   322     "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))"`
`       `
`   323 by (simp add: Ball_def)`
`       `
`   324 `
`       `
`   325 lemma atomize_ball:`
`       `
`   326     "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"`
`       `
`   327   by (simp only: Ball_def atomize_all atomize_imp)`
`       `
`   328 `
`       `
`   329 lemmas [symmetric, rulify] = atomize_ball`
`       `
`   330   and [symmetric, defn] = atomize_ball`
`       `
`   331 `
`       `
`   332 `
`       `
`   333 subsection\<open>Bounded existential quantifier\<close>`
`       `
`   334 `
`       `
`   335 lemma bexI [intro]: "[| P(x);  x: A |] ==> \<exists>x\<in>A. P(x)"`
`       `
`   336 by (simp add: Bex_def, blast)`
`       `
`   337 `
`       `
`   338 (*The best argument order when there is only one @{term"x\<in>A"}*)`
`       `
`   339 lemma rev_bexI: "[| x\<in>A;  P(x) |] ==> \<exists>x\<in>A. P(x)"`
`       `
`   340 by blast`
`       `
`   341 `
`       `
`   342 (*Not of the general form for such rules. The existential quanitifer becomes universal. *)`
`       `
`   343 lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a);  a: A |] ==> \<exists>x\<in>A. P(x)"`
`       `
`   344 by blast`
`       `
`   345 `
`       `
`   346 lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x);  !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q"`
`       `
`   347 by (simp add: Bex_def, blast)`
`       `
`   348 `
`       `
`   349 (*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty!!*)`
`       `
`   350 lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)"`
`       `
`   351 by (simp add: Bex_def)`
`       `
`   352 `
`       `
`   353 lemma bex_cong [cong]:`
`       `
`   354     "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |]`
`       `
`   355      ==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))"`
`       `
`   356 by (simp add: Bex_def cong: conj_cong)`
`       `
`   357 `
`       `
`   358 `
`       `
`   359 `
`       `
`   360 subsection\<open>Rules for subsets\<close>`
`       `
`   361 `
`       `
`   362 lemma subsetI [intro!]:`
`       `
`   363     "(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B"`
`       `
`   364 by (simp add: subset_def)`
`       `
`   365 `
`       `
`   366 (*Rule in Modus Ponens style [was called subsetE] *)`
`       `
`   367 lemma subsetD [elim]: "[| A \<subseteq> B;  c\<in>A |] ==> c\<in>B"`
`       `
`   368 apply (unfold subset_def)`
`       `
`   369 apply (erule bspec, assumption)`
`       `
`   370 done`
`       `
`   371 `
`       `
`   372 (*Classical elimination rule*)`
`       `
`   373 lemma subsetCE [elim]:`
`       `
`   374     "[| A \<subseteq> B;  c\<notin>A ==> P;  c\<in>B ==> P |] ==> P"`
`       `
`   375 by (simp add: subset_def, blast)`
`       `
`   376 `
`       `
`   377 (*Sometimes useful with premises in this order*)`
`       `
`   378 lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B"`
`       `
`   379 by blast`
`       `
`   380 `
`       `
`   381 lemma contra_subsetD: "[| A \<subseteq> B; c \<notin> B |] ==> c \<notin> A"`
`       `
`   382 by blast`
`       `
`   383 `
`       `
`   384 lemma rev_contra_subsetD: "[| c \<notin> B;  A \<subseteq> B |] ==> c \<notin> A"`
`       `
`   385 by blast`
`       `
`   386 `
`       `
`   387 lemma subset_refl [simp]: "A \<subseteq> A"`
`       `
`   388 by blast`
`       `
`   389 `
`       `
`   390 lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"`
`       `
`   391 by blast`
`       `
`   392 `
`       `
`   393 (*Useful for proving A<=B by rewriting in some cases*)`
`       `
`   394 lemma subset_iff:`
`       `
`   395      "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"`
`       `
`   396 apply (unfold subset_def Ball_def)`
`       `
`   397 apply (rule iff_refl)`
`       `
`   398 done`
`       `
`   399 `
`       `
`   400 text\<open>For calculations\<close>`
`       `
`   401 declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]`
`       `
`   402 `
`       `
`   403 `
`       `
`   404 subsection\<open>Rules for equality\<close>`
`       `
`   405 `
`       `
`   406 (*Anti-symmetry of the subset relation*)`
`       `
`   407 lemma equalityI [intro]: "[| A \<subseteq> B;  B \<subseteq> A |] ==> A = B"`
`       `
`   408 by (rule extension [THEN iffD2], rule conjI)`
`       `
`   409 `
`       `
`   410 `
`       `
`   411 lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B"`
`       `
`   412 by (rule equalityI, blast+)`
`       `
`   413 `
`       `
`   414 lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1]`
`       `
`   415 lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]`
`       `
`   416 `
`       `
`   417 lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"`
`       `
`   418 by (blast dest: equalityD1 equalityD2)`
`       `
`   419 `
`       `
`   420 lemma equalityCE:`
`       `
`   421     "[| A = B;  [| c\<in>A; c\<in>B |] ==> P;  [| c\<notin>A; c\<notin>B |] ==> P |]  ==>  P"`
`       `
`   422 by (erule equalityE, blast)`
`       `
`   423 `
`       `
`   424 lemma equality_iffD:`
`       `
`   425   "A = B ==> (!!x. x \<in> A <-> x \<in> B)"`
`       `
`   426   by auto`
`       `
`   427 `
`       `
`   428 `
`       `
`   429 subsection\<open>Rules for Replace -- the derived form of replacement\<close>`
`       `
`   430 `
`       `
`   431 lemma Replace_iff:`
`       `
`   432     "b \<in> {y. x\<in>A, P(x,y)}  <->  (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) \<longrightarrow> y=b))"`
`       `
`   433 apply (unfold Replace_def)`
`       `
`   434 apply (rule replacement [THEN iff_trans], blast+)`
`       `
`   435 done`
`       `
`   436 `
`       `
`   437 (*Introduction; there must be a unique y such that P(x,y), namely y=b. *)`
`       `
`   438 lemma ReplaceI [intro]:`
`       `
`   439     "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==>`
`       `
`   440      b \<in> {y. x\<in>A, P(x,y)}"`
`       `
`   441 by (rule Replace_iff [THEN iffD2], blast)`
`       `
`   442 `
`       `
`   443 (*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)`
`       `
`   444 lemma ReplaceE:`
`       `
`   445     "[| b \<in> {y. x\<in>A, P(x,y)};`
`       `
`   446         !!x. [| x: A;  P(x,b);  \<forall>y. P(x,y)\<longrightarrow>y=b |] ==> R`
`       `
`   447      |] ==> R"`
`       `
`   448 by (rule Replace_iff [THEN iffD1, THEN bexE], simp+)`
`       `
`   449 `
`       `
`   450 (*As above but without the (generally useless) 3rd assumption*)`
`       `
`   451 lemma ReplaceE2 [elim!]:`
`       `
`   452     "[| b \<in> {y. x\<in>A, P(x,y)};`
`       `
`   453         !!x. [| x: A;  P(x,b) |] ==> R`
`       `
`   454      |] ==> R"`
`       `
`   455 by (erule ReplaceE, blast)`
`       `
`   456 `
`       `
`   457 lemma Replace_cong [cong]:`
`       `
`   458     "[| A=B;  !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==>`
`       `
`   459      Replace(A,P) = Replace(B,Q)"`
`       `
`   460 apply (rule equality_iffI)`
`       `
`   461 apply (simp add: Replace_iff)`
`       `
`   462 done`
`       `
`   463 `
`       `
`   464 `
`       `
`   465 subsection\<open>Rules for RepFun\<close>`
`       `
`   466 `
`       `
`   467 lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}"`
`       `
`   468 by (simp add: RepFun_def Replace_iff, blast)`
`       `
`   469 `
`       `
`   470 (*Useful for coinduction proofs*)`
`       `
`   471 lemma RepFun_eqI [intro]: "[| b=f(a);  a \<in> A |] ==> b \<in> {f(x). x\<in>A}"`
`       `
`   472 apply (erule ssubst)`
`       `
`   473 apply (erule RepFunI)`
`       `
`   474 done`
`       `
`   475 `
`       `
`   476 lemma RepFunE [elim!]:`
`       `
`   477     "[| b \<in> {f(x). x\<in>A};`
`       `
`   478         !!x.[| x\<in>A;  b=f(x) |] ==> P |] ==>`
`       `
`   479      P"`
`       `
`   480 by (simp add: RepFun_def Replace_iff, blast)`
`       `
`   481 `
`       `
`   482 lemma RepFun_cong [cong]:`
`       `
`   483     "[| A=B;  !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"`
`       `
`   484 by (simp add: RepFun_def)`
`       `
`   485 `
`       `
`   486 lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))"`
`       `
`   487 by (unfold Bex_def, blast)`
`       `
`   488 `
`       `
`   489 lemma triv_RepFun [simp]: "{x. x\<in>A} = A"`
`       `
`   490 by blast`
`       `
`   491 `
`       `
`   492 `
`       `
`   493 subsection\<open>Rules for Collect -- forming a subset by separation\<close>`
`       `
`   494 `
`       `
`   495 (*Separation is derivable from Replacement*)`
`       `
`   496 lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A & P(a)"`
`       `
`   497 by (unfold Collect_def, blast)`
`       `
`   498 `
`       `
`   499 lemma CollectI [intro!]: "[| a\<in>A;  P(a) |] ==> a \<in> {x\<in>A. P(x)}"`
`       `
`   500 by simp`
`       `
`   501 `
`       `
`   502 lemma CollectE [elim!]: "[| a \<in> {x\<in>A. P(x)};  [| a\<in>A; P(a) |] ==> R |] ==> R"`
`       `
`   503 by simp`
`       `
`   504 `
`       `
`   505 lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A"`
`       `
`   506 by (erule CollectE, assumption)`
`       `
`   507 `
`       `
`   508 lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)"`
`       `
`   509 by (erule CollectE, assumption)`
`       `
`   510 `
`       `
`   511 lemma Collect_cong [cong]:`
`       `
`   512     "[| A=B;  !!x. x\<in>B ==> P(x) <-> Q(x) |]`
`       `
`   513      ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))"`
`       `
`   514 by (simp add: Collect_def)`
`       `
`   515 `
`       `
`   516 `
`       `
`   517 subsection\<open>Rules for Unions\<close>`
`       `
`   518 `
`       `
`   519 declare Union_iff [simp]`
`       `
`   520 `
`       `
`   521 (*The order of the premises presupposes that C is rigid; A may be flexible*)`
`       `
`   522 lemma UnionI [intro]: "[| B: C;  A: B |] ==> A: \<Union>(C)"`
`       `
`   523 by (simp, blast)`
`       `
`   524 `
`       `
`   525 lemma UnionE [elim!]: "[| A \<in> \<Union>(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"`
`       `
`   526 by (simp, blast)`
`       `
`   527 `
`       `
`   528 `
`       `
`   529 subsection\<open>Rules for Unions of families\<close>`
`       `
`   530 (* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *)`
`       `
`   531 `
`       `
`   532 lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))"`
`       `
`   533 by (simp add: Bex_def, blast)`
`       `
`   534 `
`       `
`   535 (*The order of the premises presupposes that A is rigid; b may be flexible*)`
`       `
`   536 lemma UN_I: "[| a: A;  b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))"`
`       `
`   537 by (simp, blast)`
`       `
`   538 `
`       `
`   539 `
`       `
`   540 lemma UN_E [elim!]:`
`       `
`   541     "[| b \<in> (\<Union>x\<in>A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"`
`       `
`   542 by blast`
`       `
`   543 `
`       `
`   544 lemma UN_cong:`
`       `
`   545     "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))"`
`       `
`   546 by simp`
`       `
`   547 `
`       `
`   548 `
`       `
`   549 (*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*)`
`       `
`   550 `
`       `
`   551 (* UN_E appears before UnionE so that it is tried first, to avoid expensive`
`       `
`   552   calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: would enlarge`
`       `
`   553   the search space.*)`
`       `
`   554 `
`       `
`   555 `
`       `
`   556 subsection\<open>Rules for the empty set\<close>`
`       `
`   557 `
`       `
`   558 (*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0`
`       `
`   559   See Suppes, page 21.*)`
`       `
`   560 lemma not_mem_empty [simp]: "a \<notin> 0"`
`       `
`   561 apply (cut_tac foundation)`
`       `
`   562 apply (best dest: equalityD2)`
`       `
`   563 done`
`       `
`   564 `
`       `
`   565 lemmas emptyE [elim!] = not_mem_empty [THEN notE]`
`       `
`   566 `
`       `
`   567 `
`       `
`   568 lemma empty_subsetI [simp]: "0 \<subseteq> A"`
`       `
`   569 by blast`
`       `
`   570 `
`       `
`   571 lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0"`
`       `
`   572 by blast`
`       `
`   573 `
`       `
`   574 lemma equals0D [dest]: "A=0 ==> a \<notin> A"`
`       `
`   575 by blast`
`       `
`   576 `
`       `
`   577 declare sym [THEN equals0D, dest]`
`       `
`   578 `
`       `
`   579 lemma not_emptyI: "a\<in>A ==> A \<noteq> 0"`
`       `
`   580 by blast`
`       `
`   581 `
`       `
`   582 lemma not_emptyE:  "[| A \<noteq> 0;  !!x. x\<in>A ==> R |] ==> R"`
`       `
`   583 by blast`
`       `
`   584 `
`       `
`   585 `
`       `
`   586 subsection\<open>Rules for Inter\<close>`
`       `
`   587 `
`       `
`   588 (*Not obviously useful for proving InterI, InterD, InterE*)`
`       `
`   589 lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0"`
`       `
`   590 by (simp add: Inter_def Ball_def, blast)`
`       `
`   591 `
`       `
`   592 (* Intersection is well-behaved only if the family is non-empty! *)`
`       `
`   593 lemma InterI [intro!]:`
`       `
`   594     "[| !!x. x: C ==> A: x;  C\<noteq>0 |] ==> A \<in> \<Inter>(C)"`
`       `
`   595 by (simp add: Inter_iff)`
`       `
`   596 `
`       `
`   597 (*A "destruct" rule -- every B in C contains A as an element, but`
`       `
`   598   A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)`
`       `
`   599 lemma InterD [elim, Pure.elim]: "[| A \<in> \<Inter>(C);  B \<in> C |] ==> A \<in> B"`
`       `
`   600 by (unfold Inter_def, blast)`
`       `
`   601 `
`       `
`   602 (*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *)`
`       `
`   603 lemma InterE [elim]:`
`       `
`   604     "[| A \<in> \<Inter>(C);  B\<notin>C ==> R;  A\<in>B ==> R |] ==> R"`
`       `
`   605 by (simp add: Inter_def, blast)`
`       `
`   606 `
`       `
`   607 `
`       `
`   608 subsection\<open>Rules for Intersections of families\<close>`
`       `
`   609 `
`       `
`   610 (* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *)`
`       `
`   611 `
`       `
`   612 lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0"`
`       `
`   613 by (force simp add: Inter_def)`
`       `
`   614 `
`       `
`   615 lemma INT_I: "[| !!x. x: A ==> b: B(x);  A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))"`
`       `
`   616 by blast`
`       `
`   617 `
`       `
`   618 lemma INT_E: "[| b \<in> (\<Inter>x\<in>A. B(x));  a: A |] ==> b \<in> B(a)"`
`       `
`   619 by blast`
`       `
`   620 `
`       `
`   621 lemma INT_cong:`
`       `
`   622     "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))"`
`       `
`   623 by simp`
`       `
`   624 `
`       `
`   625 (*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*)`
`       `
`   626 `
`       `
`   627 `
`       `
`   628 subsection\<open>Rules for Powersets\<close>`
`       `
`   629 `
`       `
`   630 lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)"`
`       `
`   631 by (erule Pow_iff [THEN iffD2])`
`       `
`   632 `
`       `
`   633 lemma PowD: "A \<in> Pow(B)  ==>  A<=B"`
`       `
`   634 by (erule Pow_iff [THEN iffD1])`
`       `
`   635 `
`       `
`   636 declare Pow_iff [iff]`
`       `
`   637 `
`       `
`   638 lemmas Pow_bottom = empty_subsetI [THEN PowI]    \<comment>\<open>@{term"0 \<in> Pow(B)"}\<close>`
`       `
`   639 lemmas Pow_top = subset_refl [THEN PowI]         \<comment>\<open>@{term"A \<in> Pow(A)"}\<close>`
`       `
`   640 `
`       `
`   641 `
`       `
`   642 subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close>`
`       `
`   643 `
`       `
`   644 (*The search is undirected.  Allowing redundant introduction rules may`
`       `
`   645   make it diverge.  Variable b represents ANY map, such as`
`       `
`   646   (lam x\<in>A.b(x)): A->Pow(A). *)`
`       `
`   647 lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S"`
`       `
`   648 by (best elim!: equalityCE del: ReplaceI RepFun_eqI)`
`       `
`   649 `
`    72 `
`   650 end`
`    73 end`