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