src/CCL/Set.thy
author wenzelm
Wed, 12 Jan 2011 16:33:04 +0100
changeset 41526 54b4686704af
parent 39128 93a7365fb4ee
child 42156 df219e736a5d
permissions -rw-r--r--
eliminated global prems;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
     1
header {* Extending FOL by a modified version of HOL set theory *}
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
     2
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
     3
theory Set
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
     4
imports FOL
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
     5
begin
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
39128
93a7365fb4ee turned eta_contract into proper configuration option;
wenzelm
parents: 38499
diff changeset
     7
declare [[eta_contract]]
93a7365fb4ee turned eta_contract into proper configuration option;
wenzelm
parents: 38499
diff changeset
     8
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
     9
typedecl 'a set
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    10
arities set :: ("term") "term"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  Collect       :: "['a => o] => 'a set"                    (*comprehension*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  Compl         :: "('a set) => 'a set"                     (*complement*)
24825
c4f13ab78f9d avoid unnamed infixes;
wenzelm
parents: 20140
diff changeset
    15
  Int           :: "['a set, 'a set] => 'a set"         (infixl "Int" 70)
c4f13ab78f9d avoid unnamed infixes;
wenzelm
parents: 20140
diff changeset
    16
  Un            :: "['a set, 'a set] => 'a set"         (infixl "Un" 65)
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    17
  Union         :: "(('a set)set) => 'a set"                (*...of a set*)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    18
  Inter         :: "(('a set)set) => 'a set"                (*...of a set*)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    19
  UNION         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    20
  INTER         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    21
  Ball          :: "['a set, 'a => o] => o"                 (*bounded quants*)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    22
  Bex           :: "['a set, 'a => o] => o"                 (*bounded quants*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  mono          :: "['a set => 'b set] => o"                (*monotonicity*)
24825
c4f13ab78f9d avoid unnamed infixes;
wenzelm
parents: 20140
diff changeset
    24
  mem           :: "['a, 'a set] => o"                  (infixl ":" 50) (*membership*)
c4f13ab78f9d avoid unnamed infixes;
wenzelm
parents: 20140
diff changeset
    25
  subset        :: "['a set, 'a set] => o"              (infixl "<=" 50)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  singleton     :: "'a => 'a set"                       ("{_}")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  empty         :: "'a set"                             ("{}")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
3935
52c14fe8f16b adapted to qualified names;
wenzelm
parents: 3837
diff changeset
    29
syntax
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35054
diff changeset
    30
  "_Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  (* Big Intersection / Union *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35054
diff changeset
    34
  "_INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35054
diff changeset
    35
  "_UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  (* Bounded Quantifiers *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35054
diff changeset
    39
  "_Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35054
diff changeset
    40
  "_Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
translations
35054
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 32153
diff changeset
    43
  "{x. P}"      == "CONST Collect(%x. P)"
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 32153
diff changeset
    44
  "INT x:A. B"  == "CONST INTER(A, %x. B)"
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 32153
diff changeset
    45
  "UN x:A. B"   == "CONST UNION(A, %x. B)"
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 32153
diff changeset
    46
  "ALL x:A. P"  == "CONST Ball(A, %x. P)"
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 32153
diff changeset
    47
  "EX x:A. P"   == "CONST Bex(A, %x. P)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    49
axioms
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    50
  mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    51
  set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    53
defs
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    54
  Ball_def:      "Ball(A, P)  == ALL x. x:A --> P(x)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    55
  Bex_def:       "Bex(A, P)   == EX x. x:A & P(x)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    56
  mono_def:      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    57
  subset_def:    "A <= B      == ALL x:A. x:B"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    58
  singleton_def: "{a}         == {x. x=a}"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    59
  empty_def:     "{}          == {x. False}"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    60
  Un_def:        "A Un B      == {x. x:A | x:B}"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    61
  Int_def:       "A Int B     == {x. x:A & x:B}"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    62
  Compl_def:     "Compl(A)    == {x. ~x:A}"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    63
  INTER_def:     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    64
  UNION_def:     "UNION(A, B) == {y. EX x:A. y: B(x)}"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    65
  Inter_def:     "Inter(S)    == (INT x:S. x)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    66
  Union_def:     "Union(S)    == (UN x:S. x)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3935
diff changeset
    67
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    68
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    69
lemma CollectI: "[| P(a) |] ==> a : {x. P(x)}"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    70
  apply (rule mem_Collect_iff [THEN iffD2])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    71
  apply assumption
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    72
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    73
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    74
lemma CollectD: "[| a : {x. P(x)} |] ==> P(a)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    75
  apply (erule mem_Collect_iff [THEN iffD1])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    76
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    77
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    78
lemmas CollectE = CollectD [elim_format]
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    79
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    80
lemma set_ext: "[| !!x. x:A <-> x:B |] ==> A = B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    81
  apply (rule set_extension [THEN iffD2])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    82
  apply simp
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    83
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    84
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    85
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    86
subsection {* Bounded quantifiers *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    87
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    88
lemma ballI: "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    89
  by (simp add: Ball_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    90
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    91
lemma bspec: "[| ALL x:A. P(x);  x:A |] ==> P(x)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    92
  by (simp add: Ball_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    93
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    94
lemma ballE: "[| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    95
  unfolding Ball_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    96
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    97
lemma bexI: "[| P(x);  x:A |] ==> EX x:A. P(x)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    98
  unfolding Bex_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    99
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   100
lemma bexCI: "[| EX x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A. P(x)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   101
  unfolding Bex_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   102
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   103
lemma bexE: "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   104
  unfolding Bex_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   105
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   106
(*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   107
lemma ball_rew: "(ALL x:A. True) <-> True"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   108
  by (blast intro: ballI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   109
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   110
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   111
subsection {* Congruence rules *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   112
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   113
lemma ball_cong:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   114
  "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   115
    (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   116
  by (blast intro: ballI elim: ballE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   117
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   118
lemma bex_cong:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   119
  "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   120
    (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   121
  by (blast intro: bexI elim: bexE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   122
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   123
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   124
subsection {* Rules for subsets *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   125
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   126
lemma subsetI: "(!!x. x:A ==> x:B) ==> A <= B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   127
  unfolding subset_def by (blast intro: ballI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   128
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   129
(*Rule in Modus Ponens style*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   130
lemma subsetD: "[| A <= B;  c:A |] ==> c:B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   131
  unfolding subset_def by (blast elim: ballE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   132
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   133
(*Classical elimination rule*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   134
lemma subsetCE: "[| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   135
  by (blast dest: subsetD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   136
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   137
lemma subset_refl: "A <= A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   138
  by (blast intro: subsetI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   139
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   140
lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   141
  by (blast intro: subsetI dest: subsetD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   142
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   143
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   144
subsection {* Rules for equality *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   145
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   146
(*Anti-symmetry of the subset relation*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   147
lemma subset_antisym: "[| A <= B;  B <= A |] ==> A = B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   148
  by (blast intro: set_ext dest: subsetD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   149
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   150
lemmas equalityI = subset_antisym
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   151
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   152
(* Equality rules from ZF set theory -- are they appropriate here? *)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   153
lemma equalityD1: "A = B ==> A<=B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   154
  and equalityD2: "A = B ==> B<=A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   155
  by (simp_all add: subset_refl)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   156
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   157
lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   158
  by (simp add: subset_refl)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   159
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   160
lemma equalityCE:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   161
    "[| A = B;  [| c:A; c:B |] ==> P;  [| ~ c:A; ~ c:B |] ==> P |]  ==>  P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   162
  by (blast elim: equalityE subsetCE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   163
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   164
lemma trivial_set: "{x. x:A} = A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   165
  by (blast intro: equalityI subsetI CollectI dest: CollectD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   166
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   167
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   168
subsection {* Rules for binary union *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   169
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   170
lemma UnI1: "c:A ==> c : A Un B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   171
  and UnI2: "c:B ==> c : A Un B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   172
  unfolding Un_def by (blast intro: CollectI)+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   173
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   174
(*Classical introduction rule: no commitment to A vs B*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   175
lemma UnCI: "(~c:B ==> c:A) ==> c : A Un B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   176
  by (blast intro: UnI1 UnI2)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   177
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   178
lemma UnE: "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   179
  unfolding Un_def by (blast dest: CollectD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   180
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   181
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   182
subsection {* Rules for small intersection *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   183
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   184
lemma IntI: "[| c:A;  c:B |] ==> c : A Int B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   185
  unfolding Int_def by (blast intro: CollectI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   186
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   187
lemma IntD1: "c : A Int B ==> c:A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   188
  and IntD2: "c : A Int B ==> c:B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   189
  unfolding Int_def by (blast dest: CollectD)+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   190
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   191
lemma IntE: "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   192
  by (blast dest: IntD1 IntD2)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   193
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   194
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   195
subsection {* Rules for set complement *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   196
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   197
lemma ComplI: "[| c:A ==> False |] ==> c : Compl(A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   198
  unfolding Compl_def by (blast intro: CollectI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   199
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   200
(*This form, with negated conclusion, works well with the Classical prover.
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   201
  Negated assumptions behave like formulae on the right side of the notional
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   202
  turnstile...*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   203
lemma ComplD: "[| c : Compl(A) |] ==> ~c:A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   204
  unfolding Compl_def by (blast dest: CollectD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   205
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   206
lemmas ComplE = ComplD [elim_format]
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   207
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   208
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   209
subsection {* Empty sets *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   210
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   211
lemma empty_eq: "{x. False} = {}"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   212
  by (simp add: empty_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   213
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   214
lemma emptyD: "a : {} ==> P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   215
  unfolding empty_def by (blast dest: CollectD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   216
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   217
lemmas emptyE = emptyD [elim_format]
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   218
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   219
lemma not_emptyD:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   220
  assumes "~ A={}"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   221
  shows "EX x. x:A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   222
proof -
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   223
  have "\<not> (EX x. x:A) \<Longrightarrow> A = {}"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   224
    by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+
41526
54b4686704af eliminated global prems;
wenzelm
parents: 39128
diff changeset
   225
  with assms show ?thesis by blast
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   226
qed
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   227
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   228
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   229
subsection {* Singleton sets *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   230
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   231
lemma singletonI: "a : {a}"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   232
  unfolding singleton_def by (blast intro: CollectI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   233
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   234
lemma singletonD: "b : {a} ==> b=a"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   235
  unfolding singleton_def by (blast dest: CollectD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   236
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   237
lemmas singletonE = singletonD [elim_format]
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   238
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   239
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   240
subsection {* Unions of families *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   241
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   242
(*The order of the premises presupposes that A is rigid; b may be flexible*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   243
lemma UN_I: "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   244
  unfolding UNION_def by (blast intro: bexI CollectI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   245
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   246
lemma UN_E: "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   247
  unfolding UNION_def by (blast dest: CollectD elim: bexE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   248
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   249
lemma UN_cong:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   250
  "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==>
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   251
    (UN x:A. C(x)) = (UN x:B. D(x))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   252
  by (simp add: UNION_def cong: bex_cong)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   253
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   254
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   255
subsection {* Intersections of families *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   256
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   257
lemma INT_I: "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   258
  unfolding INTER_def by (blast intro: CollectI ballI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   259
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   260
lemma INT_D: "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   261
  unfolding INTER_def by (blast dest: CollectD bspec)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   262
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   263
(*"Classical" elimination rule -- does not require proving X:C *)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   264
lemma INT_E: "[| b : (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   265
  unfolding INTER_def by (blast dest: CollectD bspec)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   266
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   267
lemma INT_cong:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   268
  "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==>
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   269
    (INT x:A. C(x)) = (INT x:B. D(x))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   270
  by (simp add: INTER_def cong: ball_cong)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   271
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   272
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   273
subsection {* Rules for Unions *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   274
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   275
(*The order of the premises presupposes that C is rigid; A may be flexible*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   276
lemma UnionI: "[| X:C;  A:X |] ==> A : Union(C)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   277
  unfolding Union_def by (blast intro: UN_I)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   278
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   279
lemma UnionE: "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   280
  unfolding Union_def by (blast elim: UN_E)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   281
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   282
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   283
subsection {* Rules for Inter *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   284
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   285
lemma InterI: "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   286
  unfolding Inter_def by (blast intro: INT_I)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   287
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   288
(*A "destruct" rule -- every X in C contains A as an element, but
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   289
  A:X can hold when X:C does not!  This rule is analogous to "spec". *)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   290
lemma InterD: "[| A : Inter(C);  X:C |] ==> A:X"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   291
  unfolding Inter_def by (blast dest: INT_D)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   292
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   293
(*"Classical" elimination rule -- does not require proving X:C *)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   294
lemma InterE: "[| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   295
  unfolding Inter_def by (blast elim: INT_E)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   296
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   297
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   298
section {* Derived rules involving subsets; Union and Intersection as lattice operations *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   299
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   300
subsection {* Big Union -- least upper bound of a set *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   301
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   302
lemma Union_upper: "B:A ==> B <= Union(A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   303
  by (blast intro: subsetI UnionI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   304
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   305
lemma Union_least: "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   306
  by (blast intro: subsetI dest: subsetD elim: UnionE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   307
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   308
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   309
subsection {* Big Intersection -- greatest lower bound of a set *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   310
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   311
lemma Inter_lower: "B:A ==> Inter(A) <= B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   312
  by (blast intro: subsetI dest: InterD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   313
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   314
lemma Inter_greatest: "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   315
  by (blast intro: subsetI InterI dest: subsetD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   316
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   317
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   318
subsection {* Finite Union -- the least upper bound of 2 sets *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   319
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   320
lemma Un_upper1: "A <= A Un B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   321
  by (blast intro: subsetI UnI1)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   322
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   323
lemma Un_upper2: "B <= A Un B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   324
  by (blast intro: subsetI UnI2)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   325
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   326
lemma Un_least: "[| A<=C;  B<=C |] ==> A Un B <= C"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   327
  by (blast intro: subsetI elim: UnE dest: subsetD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   328
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   329
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   330
subsection {* Finite Intersection -- the greatest lower bound of 2 sets *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   331
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   332
lemma Int_lower1: "A Int B <= A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   333
  by (blast intro: subsetI elim: IntE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   334
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   335
lemma Int_lower2: "A Int B <= B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   336
  by (blast intro: subsetI elim: IntE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   337
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   338
lemma Int_greatest: "[| C<=A;  C<=B |] ==> C <= A Int B"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   339
  by (blast intro: subsetI IntI dest: subsetD)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   340
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   341
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   342
subsection {* Monotonicity *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   343
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   344
lemma monoI: "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   345
  unfolding mono_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   346
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   347
lemma monoD: "[| mono(f);  A <= B |] ==> f(A) <= f(B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   348
  unfolding mono_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   349
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   350
lemma mono_Un: "mono(f) ==> f(A) Un f(B) <= f(A Un B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   351
  by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   352
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   353
lemma mono_Int: "mono(f) ==> f(A Int B) <= f(A) Int f(B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   354
  by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   355
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   356
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   357
subsection {* Automated reasoning setup *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   358
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   359
lemmas [intro!] = ballI subsetI InterI INT_I CollectI ComplI IntI UnCI singletonI
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   360
  and [intro] = bexI UnionI UN_I
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   361
  and [elim!] = bexE UnionE UN_E CollectE ComplE IntE UnE emptyE singletonE
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   362
  and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   363
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   364
lemma mem_rews:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   365
  "(a : A Un B)   <->  (a:A | a:B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   366
  "(a : A Int B)  <->  (a:A & a:B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   367
  "(a : Compl(B)) <->  (~a:B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   368
  "(a : {b})      <->  (a=b)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   369
  "(a : {})       <->   False"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   370
  "(a : {x. P(x)}) <->  P(a)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   371
  by blast+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   372
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   373
lemmas [simp] = trivial_set empty_eq mem_rews
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   374
  and [cong] = ball_cong bex_cong INT_cong UN_cong
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   375
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   376
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   377
section {* Equalities involving union, intersection, inclusion, etc. *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   378
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   379
subsection {* Binary Intersection *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   380
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   381
lemma Int_absorb: "A Int A = A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   382
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   383
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   384
lemma Int_commute: "A Int B  =  B Int A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   385
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   386
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   387
lemma Int_assoc: "(A Int B) Int C  =  A Int (B Int C)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   388
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   389
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   390
lemma Int_Un_distrib: "(A Un B) Int C  =  (A Int C) Un (B Int C)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   391
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   392
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   393
lemma subset_Int_eq: "(A<=B) <-> (A Int B = A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   394
  by (blast intro: equalityI elim: equalityE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   395
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   396
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   397
subsection {* Binary Union *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   398
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   399
lemma Un_absorb: "A Un A = A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   400
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   401
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   402
lemma Un_commute: "A Un B  =  B Un A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   403
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   404
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   405
lemma Un_assoc: "(A Un B) Un C  =  A Un (B Un C)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   406
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   407
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   408
lemma Un_Int_distrib: "(A Int B) Un C  =  (A Un C) Int (B Un C)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   409
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   410
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   411
lemma Un_Int_crazy:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   412
    "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   413
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   414
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   415
lemma subset_Un_eq: "(A<=B) <-> (A Un B = B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   416
  by (blast intro: equalityI elim: equalityE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   417
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   418
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   419
subsection {* Simple properties of @{text "Compl"} -- complement of a set *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   420
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   421
lemma Compl_disjoint: "A Int Compl(A) = {x. False}"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   422
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   423
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   424
lemma Compl_partition: "A Un Compl(A) = {x. True}"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   425
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   426
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   427
lemma double_complement: "Compl(Compl(A)) = A"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   428
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   429
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   430
lemma Compl_Un: "Compl(A Un B) = Compl(A) Int Compl(B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   431
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   432
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   433
lemma Compl_Int: "Compl(A Int B) = Compl(A) Un Compl(B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   434
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   435
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   436
lemma Compl_UN: "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   437
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   438
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   439
lemma Compl_INT: "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   440
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   441
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   442
(*Halmos, Naive Set Theory, page 16.*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   443
lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   444
  by (blast intro: equalityI elim: equalityE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   445
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   446
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   447
subsection {* Big Union and Intersection *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   448
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   449
lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   450
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   451
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   452
lemma Union_disjoint:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   453
    "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   454
  by (blast intro: equalityI elim: equalityE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   455
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   456
lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   457
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   458
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   459
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   460
subsection {* Unions and Intersections of Families *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   461
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   462
lemma UN_eq: "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   463
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   464
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   465
(*Look: it has an EXISTENTIAL quantifier*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   466
lemma INT_eq: "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   467
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   468
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   469
lemma Int_Union_image: "A Int Union(B) = (UN C:B. A Int C)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   470
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   471
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   472
lemma Un_Inter_image: "A Un Inter(B) = (INT C:B. A Un C)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   473
  by (blast intro: equalityI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   474
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   475
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   476
section {* Monotonicity of various operations *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   477
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   478
lemma Union_mono: "A<=B ==> Union(A) <= Union(B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   479
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   480
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   481
lemma Inter_anti_mono: "[| B<=A |] ==> Inter(A) <= Inter(B)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   482
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   483
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   484
lemma UN_mono:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   485
  "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==>  
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   486
    (UN x:A. f(x)) <= (UN x:B. g(x))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   487
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   488
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   489
lemma INT_anti_mono:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   490
  "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==>  
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   491
    (INT x:A. f(x)) <= (INT x:A. g(x))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   492
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   493
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   494
lemma Un_mono: "[| A<=C;  B<=D |] ==> A Un B <= C Un D"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   495
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   496
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   497
lemma Int_mono: "[| A<=C;  B<=D |] ==> A Int B <= C Int D"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   498
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   499
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   500
lemma Compl_anti_mono: "[| A<=B |] ==> Compl(B) <= Compl(A)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   501
  by blast
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   502
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   503
end