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