src/HOL/equalities.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10234 c8726d4ee89a
child 10832 e33b47e4246d
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
     1
(*  Title:      HOL/equalities
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
Equalities involving union, intersection, inclusion, etc.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
writeln"File HOL/equalities";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
1754
852093aeb0ab Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents: 1748
diff changeset
    11
AddSIs [equalityI];
852093aeb0ab Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents: 1748
diff changeset
    12
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
    13
section "{}";
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
    14
7824
1a85ba81d019 new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents: 7713
diff changeset
    15
(*supersedes Collect_False_empty*)
1a85ba81d019 new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents: 7713
diff changeset
    16
Goal "{s. P} = (if P then UNIV else {})";
1a85ba81d019 new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents: 7713
diff changeset
    17
by (Force_tac 1);
1a85ba81d019 new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents: 7713
diff changeset
    18
qed "Collect_const";
1a85ba81d019 new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents: 7713
diff changeset
    19
Addsimps [Collect_const];
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    20
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
    21
Goal "(A <= {}) = (A = {})";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    22
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    23
qed "subset_empty";
9338
fcf7f29a3447 re-added subset_empty to simpset
oheimb
parents: 9312
diff changeset
    24
Addsimps[subset_empty];
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    25
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
    26
Goalw [psubset_def] "~ (A < {})";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    27
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    28
qed "not_psubset_empty";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    29
AddIffs [not_psubset_empty];
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    30
9206
eaaee6bd74ba tidied and deleted two redundant theories
paulson
parents: 9098
diff changeset
    31
Goal "(Collect P = {}) = (ALL x. ~ P x)";
7958
f531589c9fc1 added various little lemmas
oheimb
parents: 7914
diff changeset
    32
by Auto_tac;
f531589c9fc1 added various little lemmas
oheimb
parents: 7914
diff changeset
    33
qed "Collect_empty_eq";
f531589c9fc1 added various little lemmas
oheimb
parents: 7914
diff changeset
    34
Addsimps[Collect_empty_eq];
f531589c9fc1 added various little lemmas
oheimb
parents: 7914
diff changeset
    35
8993
cbfebff56cc0 Collect_neg_eq;
wenzelm
parents: 8333
diff changeset
    36
Goal "{x. ~ (P x)} = - {x. P x}";
cbfebff56cc0 Collect_neg_eq;
wenzelm
parents: 8333
diff changeset
    37
by (Blast_tac 1);
cbfebff56cc0 Collect_neg_eq;
wenzelm
parents: 8333
diff changeset
    38
qed "Collect_neg_eq";
cbfebff56cc0 Collect_neg_eq;
wenzelm
parents: 8333
diff changeset
    39
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
    40
Goal "{x. P x | Q x} = {x. P x} Un {x. Q x}";
4748
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
    41
by (Blast_tac 1);
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
    42
qed "Collect_disj_eq";
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
    43
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
    44
Goal "{x. P x & Q x} = {x. P x} Int {x. Q x}";
4748
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
    45
by (Blast_tac 1);
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
    46
qed "Collect_conj_eq";
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
    47
7845
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    48
Goal "{x. ALL y. P x y} = (INT y. {x. P x y})";
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    49
by (Blast_tac 1);
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    50
qed "Collect_all_eq";
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    51
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    52
Goal "{x. ALL y: A. P x y} = (INT y: A. {x. P x y})";
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    53
by (Blast_tac 1);
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    54
qed "Collect_ball_eq";
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    55
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    56
Goal "{x. EX y. P x y} = (UN y. {x. P x y})";
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    57
by (Blast_tac 1);
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    58
qed "Collect_ex_eq";
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    59
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    60
Goal "{x. EX y: A. P x y} = (UN y: A. {x. P x y})";
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    61
by (Blast_tac 1);
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    62
qed "Collect_bex_eq";
3561e0da35b8 more Collect laws
paulson
parents: 7824
diff changeset
    63
4748
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
    64
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
    65
section "insert";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    66
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    67
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
    68
Goal "insert a A = {a} Un A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    69
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    70
qed "insert_is_Un";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    71
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
    72
Goal "insert a A ~= {}";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    73
by (blast_tac (claset() addEs [equalityCE]) 1);
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
    74
qed"insert_not_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    75
Addsimps[insert_not_empty];
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
    76
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
    77
bind_thm("empty_not_insert",insert_not_empty RS not_sym);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    78
Addsimps[empty_not_insert];
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
    79
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    80
Goal "a:A ==> insert a A = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    81
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
qed "insert_absorb";
6832
0c92ccb3c4ba moved image_UNION to Fun/image_UN
paulson
parents: 6301
diff changeset
    83
(* Addsimps [insert_absorb] causes recursive calls
0c92ccb3c4ba moved image_UNION to Fun/image_UN
paulson
parents: 6301
diff changeset
    84
   when there are nested inserts, with QUADRATIC running time
4605
579e0ef2df6b Added `remdups'
nipkow
parents: 4477
diff changeset
    85
*)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    86
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
    87
Goal "insert x (insert x A) = insert x A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    88
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    89
qed "insert_absorb2";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    90
Addsimps [insert_absorb2];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    91
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
    92
Goal "insert x (insert y A) = insert y (insert x A)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    93
by (Blast_tac 1);
1879
83c70ad381c1 Added insert_commute
paulson
parents: 1843
diff changeset
    94
qed "insert_commute";
83c70ad381c1 Added insert_commute
paulson
parents: 1843
diff changeset
    95
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
    96
Goal "(insert x A <= B) = (x:B & A <= B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    97
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    98
qed "insert_subset";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    99
Addsimps[insert_subset];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   100
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   101
(* use new B rather than (A-{a}) to avoid infinite unfolding *)
9206
eaaee6bd74ba tidied and deleted two redundant theories
paulson
parents: 9098
diff changeset
   102
Goal "a:A ==> EX B. A = insert a B & a ~: B";
1553
4eb4a9c7d736 Ran expandshort
paulson
parents: 1548
diff changeset
   103
by (res_inst_tac [("x","A-{a}")] exI 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   104
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   105
qed "mk_disjoint_insert";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   106
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9608
diff changeset
   107
Goal "insert a (Collect P) = {u. u ~= a --> P u}";
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9608
diff changeset
   108
by Auto_tac;
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9608
diff changeset
   109
qed "insert_Collect";
4882
379314255a04 added insert_Collect
oheimb
parents: 4771
diff changeset
   110
5941
1db9fad40a4f better miniscoping rules: the premise C~={} is not good
paulson
parents: 5931
diff changeset
   111
Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   112
by (Blast_tac 1);
1843
a6d7aef48c2f Removed the unused eq_cs, and added some distributive laws
paulson
parents: 1786
diff changeset
   113
qed "UN_insert_distrib";
a6d7aef48c2f Removed the unused eq_cs, and added some distributive laws
paulson
parents: 1786
diff changeset
   114
1660
8cb42cd97579 *** empty log message ***
oheimb
parents: 1618
diff changeset
   115
section "``";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   116
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   117
Goal "f``{} = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   118
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   119
qed "image_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   120
Addsimps[image_empty];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   121
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   122
Goal "f``insert a B = insert (f a) (f``B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   123
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   124
qed "image_insert";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   125
Addsimps[image_insert];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   126
6292
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   127
Goal "x:A ==> (%x. c) `` A = {c}";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   128
by (Blast_tac 1);
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   129
qed "image_constant";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   130
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   131
Goal "f``(g``A) = (%x. f (g x)) `` A";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3426
diff changeset
   132
by (Blast_tac 1);
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   133
qed "image_image";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   134
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   135
Goal "x:A ==> insert (f x) (f``A) = f``A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   136
by (Blast_tac 1);
1884
5a1f81da3e12 Proved insert_image
paulson
parents: 1879
diff changeset
   137
qed "insert_image";
5a1f81da3e12 Proved insert_image
paulson
parents: 1879
diff changeset
   138
Addsimps [insert_image];
5a1f81da3e12 Proved insert_image
paulson
parents: 1879
diff changeset
   139
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   140
Goal "(f``A = {}) = (A = {})";
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   141
by (blast_tac (claset() addSEs [equalityCE]) 1);
3415
c068bd2f0bbd Moved image_is_empty from Finite.ML to equalities.ML
nipkow
parents: 3384
diff changeset
   142
qed "image_is_empty";
c068bd2f0bbd Moved image_is_empty from Finite.ML to equalities.ML
nipkow
parents: 3384
diff changeset
   143
AddIffs [image_is_empty];
c068bd2f0bbd Moved image_is_empty from Finite.ML to equalities.ML
nipkow
parents: 3384
diff changeset
   144
5281
f4d16517b360 List now contains some lexicographic orderings.
nipkow
parents: 5278
diff changeset
   145
Goal "f `` {x. P x} = {f x | x. P x}";
5319
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   146
by (Blast_tac 1);
5281
f4d16517b360 List now contains some lexicographic orderings.
nipkow
parents: 5278
diff changeset
   147
qed "image_Collect";
f4d16517b360 List now contains some lexicographic orderings.
nipkow
parents: 5278
diff changeset
   148
Addsimps [image_Collect];
f4d16517b360 List now contains some lexicographic orderings.
nipkow
parents: 5278
diff changeset
   149
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   150
Goalw [image_def] "(%x. if P x then f x else g x) `` S   \
477fc12adceb white space
paulson
parents: 5521
diff changeset
   151
\                = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4674
diff changeset
   152
by (Simp_tac 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   153
by (Blast_tac 1);
1748
88650ba93c10 Added if_image_distrib.
nipkow
parents: 1660
diff changeset
   154
qed "if_image_distrib";
88650ba93c10 Added if_image_distrib.
nipkow
parents: 1660
diff changeset
   155
Addsimps[if_image_distrib];
88650ba93c10 Added if_image_distrib.
nipkow
parents: 1660
diff changeset
   156
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   157
val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
4136
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   158
by (simp_tac (simpset() addsimps image_def::prems) 1);
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   159
qed "image_cong";
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   160
1748
88650ba93c10 Added if_image_distrib.
nipkow
parents: 1660
diff changeset
   161
7958
f531589c9fc1 added various little lemmas
oheimb
parents: 7914
diff changeset
   162
section "range";
f531589c9fc1 added various little lemmas
oheimb
parents: 7914
diff changeset
   163
9206
eaaee6bd74ba tidied and deleted two redundant theories
paulson
parents: 9098
diff changeset
   164
Goal "{u. EX x. u = f x} = range f";
7958
f531589c9fc1 added various little lemmas
oheimb
parents: 7914
diff changeset
   165
by Auto_tac;
f531589c9fc1 added various little lemmas
oheimb
parents: 7914
diff changeset
   166
qed "full_SetCompr_eq";
f531589c9fc1 added various little lemmas
oheimb
parents: 7914
diff changeset
   167
8161
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 8121
diff changeset
   168
Goal "range (%x. f (g x)) = f``range g";
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 8121
diff changeset
   169
by (stac image_image 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 8121
diff changeset
   170
by (Simp_tac 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 8121
diff changeset
   171
qed "range_composition";
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 8121
diff changeset
   172
Addsimps[range_composition];
7958
f531589c9fc1 added various little lemmas
oheimb
parents: 7914
diff changeset
   173
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   174
section "Int";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   175
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   176
Goal "A Int A = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   177
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   178
qed "Int_absorb";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   179
Addsimps[Int_absorb];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   180
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   181
Goal "A Int (A Int B) = A Int B";
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   182
by (Blast_tac 1);
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   183
qed "Int_left_absorb";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   184
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   185
Goal "A Int B = B Int A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   186
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   187
qed "Int_commute";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   188
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   189
Goal "A Int (B Int C) = B Int (A Int C)";
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   190
by (Blast_tac 1);
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   191
qed "Int_left_commute";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   192
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   193
Goal "(A Int B) Int C = A Int (B Int C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   194
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   195
qed "Int_assoc";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   196
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   197
(*Intersection is an AC-operator*)
7648
8258b93cdd32 bind_thms;
wenzelm
parents: 7516
diff changeset
   198
bind_thms ("Int_ac", [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]);
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   199
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   200
Goal "B<=A ==> A Int B = B";
4662
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   201
by (Blast_tac 1);
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   202
qed "Int_absorb1";
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   203
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   204
Goal "A<=B ==> A Int B = A";
4662
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   205
by (Blast_tac 1);
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   206
qed "Int_absorb2";
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   207
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   208
Goal "{} Int B = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   209
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   210
qed "Int_empty_left";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   211
Addsimps[Int_empty_left];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   212
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   213
Goal "A Int {} = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   214
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   215
qed "Int_empty_right";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   216
Addsimps[Int_empty_right];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   217
5490
85855f65d0c6 From Compl(A) to -A
paulson
parents: 5331
diff changeset
   218
Goal "(A Int B = {}) = (A <= -B)";
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   219
by (blast_tac (claset() addSEs [equalityCE]) 1);
3356
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   220
qed "disjoint_eq_subset_Compl";
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   221
7877
e5e019d60f71 new thm disjoint_iff_not_equal
paulson
parents: 7845
diff changeset
   222
Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";
e5e019d60f71 new thm disjoint_iff_not_equal
paulson
parents: 7845
diff changeset
   223
by  (Blast_tac 1);
e5e019d60f71 new thm disjoint_iff_not_equal
paulson
parents: 7845
diff changeset
   224
qed "disjoint_iff_not_equal";
e5e019d60f71 new thm disjoint_iff_not_equal
paulson
parents: 7845
diff changeset
   225
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   226
Goal "UNIV Int B = B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   227
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   228
qed "Int_UNIV_left";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   229
Addsimps[Int_UNIV_left];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   230
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   231
Goal "A Int UNIV = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   232
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   233
qed "Int_UNIV_right";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   234
Addsimps[Int_UNIV_right];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   235
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   236
Goal "A Int B = Inter{A,B}";
4634
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   237
by (Blast_tac 1);
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   238
qed "Int_eq_Inter";
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   239
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   240
Goal "A Int (B Un C) = (A Int B) Un (A Int C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   241
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   242
qed "Int_Un_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   243
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   244
Goal "(B Un C) Int A = (B Int A) Un (C Int A)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   245
by (Blast_tac 1);
1618
372880456b5b Library changes for mutilated checkerboard
paulson
parents: 1564
diff changeset
   246
qed "Int_Un_distrib2";
372880456b5b Library changes for mutilated checkerboard
paulson
parents: 1564
diff changeset
   247
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   248
Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   249
by (blast_tac (claset() addEs [equalityCE]) 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   250
qed "Int_UNIV";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   251
Addsimps[Int_UNIV];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   252
5319
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   253
Goal "(C <= A Int B) = (C <= A & C <= B)";
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   254
by (Blast_tac 1);
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   255
qed "Int_subset_iff";
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   256
7713
f4fe9d620107 Additional rules for inductive package.
berghofe
parents: 7648
diff changeset
   257
Goal "(x : A Int {x. P x}) = (x : A & P x)";
f4fe9d620107 Additional rules for inductive package.
berghofe
parents: 7648
diff changeset
   258
by (Blast_tac 1);
f4fe9d620107 Additional rules for inductive package.
berghofe
parents: 7648
diff changeset
   259
qed "Int_Collect";
5319
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   260
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   261
section "Un";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   262
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   263
Goal "A Un A = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   264
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   265
qed "Un_absorb";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   266
Addsimps[Un_absorb];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   267
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   268
Goal " A Un (A Un B) = A Un B";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   269
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   270
qed "Un_left_absorb";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   271
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   272
Goal "A Un B = B Un A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   273
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   274
qed "Un_commute";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   275
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   276
Goal "A Un (B Un C) = B Un (A Un C)";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   277
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   278
qed "Un_left_commute";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   279
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   280
Goal "(A Un B) Un C = A Un (B Un C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   281
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   282
qed "Un_assoc";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   283
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   284
(*Union is an AC-operator*)
7648
8258b93cdd32 bind_thms;
wenzelm
parents: 7516
diff changeset
   285
bind_thms ("Un_ac", [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]);
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   286
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   287
Goal "A<=B ==> A Un B = B";
4662
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   288
by (Blast_tac 1);
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   289
qed "Un_absorb1";
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   290
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   291
Goal "B<=A ==> A Un B = A";
4662
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   292
by (Blast_tac 1);
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   293
qed "Un_absorb2";
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   294
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   295
Goal "{} Un B = B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   296
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   297
qed "Un_empty_left";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   298
Addsimps[Un_empty_left];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   299
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   300
Goal "A Un {} = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   301
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   302
qed "Un_empty_right";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   303
Addsimps[Un_empty_right];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   304
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   305
Goal "UNIV Un B = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   306
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   307
qed "Un_UNIV_left";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   308
Addsimps[Un_UNIV_left];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   309
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   310
Goal "A Un UNIV = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   311
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   312
qed "Un_UNIV_right";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   313
Addsimps[Un_UNIV_right];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   314
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   315
Goal "A Un B = Union{A,B}";
4634
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   316
by (Blast_tac 1);
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   317
qed "Un_eq_Union";
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   318
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   319
Goal "(insert a B) Un C = insert a (B Un C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   320
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   321
qed "Un_insert_left";
3384
5ef99c94e1fb Now Un_insert_left, Un_insert_right are default rewrite rules
paulson
parents: 3356
diff changeset
   322
Addsimps[Un_insert_left];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   323
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   324
Goal "A Un (insert a B) = insert a (A Un B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   325
by (Blast_tac 1);
1917
27b71d839d50 Added proof of Un_insert_right
paulson
parents: 1884
diff changeset
   326
qed "Un_insert_right";
3384
5ef99c94e1fb Now Un_insert_left, Un_insert_right are default rewrite rules
paulson
parents: 3356
diff changeset
   327
Addsimps[Un_insert_right];
1917
27b71d839d50 Added proof of Un_insert_right
paulson
parents: 1884
diff changeset
   328
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   329
Goal "(insert a B) Int C = (if a:C then insert a (B Int C) \
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   330
\                                  else        B Int C)";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4674
diff changeset
   331
by (Simp_tac 1);
3356
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   332
by (Blast_tac 1);
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   333
qed "Int_insert_left";
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   334
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   335
Goal "A Int (insert a B) = (if a:A then insert a (A Int B) \
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   336
\                                  else        A Int B)";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4674
diff changeset
   337
by (Simp_tac 1);
3356
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   338
by (Blast_tac 1);
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   339
qed "Int_insert_right";
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   340
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   341
Goal "A Un (B Int C) = (A Un B) Int (A Un C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   342
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   343
qed "Un_Int_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   344
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   345
Goal "(B Int C) Un A = (B Un A) Int (C Un A)";
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   346
by (Blast_tac 1);
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   347
qed "Un_Int_distrib2";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   348
5590
477fc12adceb white space
paulson
parents: 5521
diff changeset
   349
Goal "(A Int B) Un (B Int C) Un (C Int A) = \
477fc12adceb white space
paulson
parents: 5521
diff changeset
   350
\     (A Un B) Int (B Un C) Int (C Un A)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   351
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   352
qed "Un_Int_crazy";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   353
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   354
Goal "(A<=B) = (A Un B = B)";
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   355
by (blast_tac (claset() addSEs [equalityCE]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   356
qed "subset_Un_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   357
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   358
Goal "(A Un B = {}) = (A = {} & B = {})";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   359
by (blast_tac (claset() addEs [equalityCE]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   360
qed "Un_empty";
9098
3a0912a127ec new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents: 9077
diff changeset
   361
AddIffs[Un_empty];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   362
5319
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   363
Goal "(A Un B <= C) = (A <= C & B <= C)";
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   364
by (Blast_tac 1);
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   365
qed "Un_subset_iff";
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   366
5331
3d27b96a08b0 new theorem Un_Diff_Int
paulson
parents: 5319
diff changeset
   367
Goal "(A - B) Un (A Int B) = A";
3d27b96a08b0 new theorem Un_Diff_Int
paulson
parents: 5319
diff changeset
   368
by (Blast_tac 1);
3d27b96a08b0 new theorem Un_Diff_Int
paulson
parents: 5319
diff changeset
   369
qed "Un_Diff_Int";
3d27b96a08b0 new theorem Un_Diff_Int
paulson
parents: 5319
diff changeset
   370
5319
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5316
diff changeset
   371
5931
325300576da7 Finally removing "Compl" from HOL
paulson
parents: 5854
diff changeset
   372
section "Set complement";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   373
8333
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   374
Goal "A Int -A = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   375
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   376
qed "Compl_disjoint";
8333
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   377
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   378
Goal "-A Int A = {}";
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   379
by (Blast_tac 1);
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   380
qed "Compl_disjoint2";
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   381
Addsimps[Compl_disjoint, Compl_disjoint2];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   382
7127
48e235179ffb added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents: 6832
diff changeset
   383
Goal "A Un (-A) = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   384
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   385
qed "Compl_partition";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   386
7127
48e235179ffb added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents: 6832
diff changeset
   387
Goal "- (-A) = (A:: 'a set)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   388
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   389
qed "double_complement";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   390
Addsimps[double_complement];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   391
7127
48e235179ffb added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents: 6832
diff changeset
   392
Goal "-(A Un B) = (-A) Int (-B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   393
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   394
qed "Compl_Un";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   395
7127
48e235179ffb added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents: 6832
diff changeset
   396
Goal "-(A Int B) = (-A) Un (-B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   397
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   398
qed "Compl_Int";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   399
5490
85855f65d0c6 From Compl(A) to -A
paulson
parents: 5331
diff changeset
   400
Goal "-(UN x:A. B(x)) = (INT x:A. -B(x))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   401
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   402
qed "Compl_UN";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   403
5490
85855f65d0c6 From Compl(A) to -A
paulson
parents: 5331
diff changeset
   404
Goal "-(INT x:A. B(x)) = (UN x:A. -B(x))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   405
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   406
qed "Compl_INT";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   407
4615
67457d16cdbc New Addsimps for Compl rules
paulson
parents: 4609
diff changeset
   408
Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT];
67457d16cdbc New Addsimps for Compl rules
paulson
parents: 4609
diff changeset
   409
8121
4a53041acb28 new theorem subset_Compl_self_eq
paulson
parents: 8030
diff changeset
   410
Goal "(A <= -A) = (A = {})";
4a53041acb28 new theorem subset_Compl_self_eq
paulson
parents: 8030
diff changeset
   411
by (Blast_tac 1);
4a53041acb28 new theorem subset_Compl_self_eq
paulson
parents: 8030
diff changeset
   412
qed "subset_Compl_self_eq";
4a53041acb28 new theorem subset_Compl_self_eq
paulson
parents: 8030
diff changeset
   413
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   414
(*Halmos, Naive Set Theory, page 16.*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   415
Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   416
by (blast_tac (claset() addSEs [equalityCE]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   417
qed "Un_Int_assoc_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   418
8333
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   419
Goal "-UNIV = {}";
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   420
by (Blast_tac 1);
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   421
qed "Compl_UNIV_eq";
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   422
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   423
Goal "-{} = UNIV";
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   424
by (Blast_tac 1);
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   425
qed "Compl_empty_eq";
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   426
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   427
Addsimps [Compl_UNIV_eq, Compl_empty_eq];
226d12ac76e2 improved reasoning about {} and UNIV
paulson
parents: 8313
diff changeset
   428
9447
e5180c869772 *** empty log message ***
nipkow
parents: 9422
diff changeset
   429
Goal "(-A <= -B) = (B <= (A::'a set))";
e5180c869772 *** empty log message ***
nipkow
parents: 9422
diff changeset
   430
by(Blast_tac 1);
e5180c869772 *** empty log message ***
nipkow
parents: 9422
diff changeset
   431
qed "Compl_subset_Compl_iff";
e5180c869772 *** empty log message ***
nipkow
parents: 9422
diff changeset
   432
AddIffs [Compl_subset_Compl_iff];
e5180c869772 *** empty log message ***
nipkow
parents: 9422
diff changeset
   433
e5180c869772 *** empty log message ***
nipkow
parents: 9422
diff changeset
   434
Goal "(-A = -B) = (A = (B::'a set))";
e5180c869772 *** empty log message ***
nipkow
parents: 9422
diff changeset
   435
by(Blast_tac 1);
e5180c869772 *** empty log message ***
nipkow
parents: 9422
diff changeset
   436
qed "Compl_eq_Compl_iff";
e5180c869772 *** empty log message ***
nipkow
parents: 9422
diff changeset
   437
AddIffs [Compl_eq_Compl_iff];
e5180c869772 *** empty log message ***
nipkow
parents: 9422
diff changeset
   438
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   439
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   440
section "Union";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   441
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   442
Goal "Union({}) = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   443
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   444
qed "Union_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   445
Addsimps[Union_empty];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   446
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   447
Goal "Union(UNIV) = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   448
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   449
qed "Union_UNIV";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   450
Addsimps[Union_UNIV];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   451
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   452
Goal "Union(insert a B) = a Un Union(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   453
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   454
qed "Union_insert";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   455
Addsimps[Union_insert];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   456
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   457
Goal "Union(A Un B) = Union(A) Un Union(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   458
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   459
qed "Union_Un_distrib";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   460
Addsimps[Union_Un_distrib];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   461
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   462
Goal "Union(A Int B) <= Union(A) Int Union(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   463
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   464
qed "Union_Int_subset";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   465
9098
3a0912a127ec new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents: 9077
diff changeset
   466
Goal "(Union A = {}) = (ALL x:A. x={})";
3a0912a127ec new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents: 9077
diff changeset
   467
by Auto_tac; 
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   468
qed "Union_empty_conv"; 
4003
nipkow
parents: 3919
diff changeset
   469
AddIffs [Union_empty_conv];
nipkow
parents: 3919
diff changeset
   470
9206
eaaee6bd74ba tidied and deleted two redundant theories
paulson
parents: 9098
diff changeset
   471
Goal "(Union(C) Int A = {}) = (ALL B:C. B Int A = {})";
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   472
by (blast_tac (claset() addSEs [equalityCE]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   473
qed "Union_disjoint";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   474
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   475
section "Inter";
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   476
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   477
Goal "Inter({}) = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   478
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   479
qed "Inter_empty";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   480
Addsimps[Inter_empty];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   481
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   482
Goal "Inter(UNIV) = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   483
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   484
qed "Inter_UNIV";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   485
Addsimps[Inter_UNIV];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   486
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   487
Goal "Inter(insert a B) = a Int Inter(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   488
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   489
qed "Inter_insert";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   490
Addsimps[Inter_insert];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   491
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   492
Goal "Inter(A) Un Inter(B) <= Inter(A Int B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   493
by (Blast_tac 1);
1564
822575c737bd Deleted faulty comment; proved new rule Inter_Un_subset
paulson
parents: 1553
diff changeset
   494
qed "Inter_Un_subset";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   495
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   496
Goal "Inter(A Un B) = Inter(A) Int Inter(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   497
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   498
qed "Inter_Un_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   499
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   500
section "UN and INT";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   501
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   502
(*Basic identities*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   503
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   504
Goal "(UN x:{}. B x) = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   505
by (Blast_tac 1);
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
   506
qed "UN_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   507
Addsimps[UN_empty];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   508
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   509
Goal "(UN x:A. {}) = {}";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3426
diff changeset
   510
by (Blast_tac 1);
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   511
qed "UN_empty2";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   512
Addsimps[UN_empty2];
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   513
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   514
Goal "(UN x:A. {x}) = A";
4645
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   515
by (Blast_tac 1);
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   516
qed "UN_singleton";
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   517
Addsimps [UN_singleton];
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   518
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   519
Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
4634
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   520
by (Blast_tac 1);
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   521
qed "UN_absorb";
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   522
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   523
Goal "(INT x:{}. B x) = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   524
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   525
qed "INT_empty";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   526
Addsimps[INT_empty];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   527
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   528
Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
4634
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   529
by (Blast_tac 1);
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   530
qed "INT_absorb";
83d364462ce1 Four new Union/Intersection laws
paulson
parents: 4615
diff changeset
   531
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   532
Goal "(UN x:insert a A. B x) = B a Un UNION A B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   533
by (Blast_tac 1);
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
   534
qed "UN_insert";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   535
Addsimps[UN_insert];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   536
5999
84fe61a08c17 new theorem INT_Un
paulson
parents: 5967
diff changeset
   537
Goal "(UN i: A Un B. M i) = (UN i: A. M i) Un (UN i:B. M i)";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   538
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   539
qed "UN_Un";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   540
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   541
Goal "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)";
4771
f1bacbbe02a8 new theorems
paulson
parents: 4748
diff changeset
   542
by (Blast_tac 1);
f1bacbbe02a8 new theorems
paulson
parents: 4748
diff changeset
   543
qed "UN_UN_flatten";
f1bacbbe02a8 new theorems
paulson
parents: 4748
diff changeset
   544
6292
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   545
Goal "((UN i:I. A i) <= B) = (ALL i:I. A i <= B)";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   546
by (Blast_tac 1);
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   547
qed "UN_subset_iff";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   548
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   549
Goal "(B <= (INT i:I. A i)) = (ALL i:I. B <= A i)";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   550
by (Blast_tac 1);
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   551
qed "INT_subset_iff";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   552
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   553
Goal "(INT x:insert a A. B x) = B a Int INTER A B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   554
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   555
qed "INT_insert";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   556
Addsimps[INT_insert];
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
   557
5999
84fe61a08c17 new theorem INT_Un
paulson
parents: 5967
diff changeset
   558
Goal "(INT i: A Un B. M i) = (INT i: A. M i) Int (INT i:B. M i)";
84fe61a08c17 new theorem INT_Un
paulson
parents: 5967
diff changeset
   559
by (Blast_tac 1);
84fe61a08c17 new theorem INT_Un
paulson
parents: 5967
diff changeset
   560
qed "INT_Un";
84fe61a08c17 new theorem INT_Un
paulson
parents: 5967
diff changeset
   561
5941
1db9fad40a4f better miniscoping rules: the premise C~={} is not good
paulson
parents: 5931
diff changeset
   562
Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   563
by (Blast_tac 1);
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   564
qed "INT_insert_distrib";
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   565
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   566
Goal "Union(B``A) = (UN x:A. B(x))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   567
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   568
qed "Union_image_eq";
6292
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   569
Addsimps [Union_image_eq];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   570
6283
e3096df44326 new theorem image_Union_eq
paulson
parents: 6007
diff changeset
   571
Goal "f `` Union S = (UN x:S. f `` x)";
e3096df44326 new theorem image_Union_eq
paulson
parents: 6007
diff changeset
   572
by (Blast_tac 1);
8176
db112d36a426 renamed image_Union_eq -> image_Union
paulson
parents: 8161
diff changeset
   573
qed "image_Union";
6283
e3096df44326 new theorem image_Union_eq
paulson
parents: 6007
diff changeset
   574
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   575
Goal "Inter(B``A) = (INT x:A. B(x))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   576
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   577
qed "Inter_image_eq";
6292
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   578
Addsimps [Inter_image_eq];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   579
8313
c7a87e79e9b1 replaced UN_constant, INT_constant by unconditional versions that rewrite
paulson
parents: 8176
diff changeset
   580
Goal "(UN y:A. c) = (if A={} then {} else c)";
c7a87e79e9b1 replaced UN_constant, INT_constant by unconditional versions that rewrite
paulson
parents: 8176
diff changeset
   581
by Auto_tac;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   582
qed "UN_constant";
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   583
Addsimps[UN_constant];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   584
8313
c7a87e79e9b1 replaced UN_constant, INT_constant by unconditional versions that rewrite
paulson
parents: 8176
diff changeset
   585
Goal "(INT y:A. c) = (if A={} then UNIV else c)";
c7a87e79e9b1 replaced UN_constant, INT_constant by unconditional versions that rewrite
paulson
parents: 8176
diff changeset
   586
by Auto_tac;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   587
qed "INT_constant";
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   588
Addsimps[INT_constant];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   589
9206
eaaee6bd74ba tidied and deleted two redundant theories
paulson
parents: 9098
diff changeset
   590
Goal "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   591
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   592
qed "UN_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   593
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   594
(*Look: it has an EXISTENTIAL quantifier*)
9206
eaaee6bd74ba tidied and deleted two redundant theories
paulson
parents: 9098
diff changeset
   595
Goal "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   596
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   597
qed "INT_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   598
9098
3a0912a127ec new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents: 9077
diff changeset
   599
Goal "(UNION A B = {}) = (ALL x:A. B x = {})";
3a0912a127ec new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents: 9077
diff changeset
   600
by Auto_tac; 
9312
a93a7b6bb654 fixed name: UN_empty3;
wenzelm
parents: 9206
diff changeset
   601
qed "UN_empty3";
a93a7b6bb654 fixed name: UN_empty3;
wenzelm
parents: 9206
diff changeset
   602
AddIffs [UN_empty3];
9098
3a0912a127ec new theorem UN_empty; it and Un_empty inserted by AddIffs
paulson
parents: 9077
diff changeset
   603
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   604
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   605
(*Distributive laws...*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   606
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   607
Goal "A Int Union(B) = (UN C:B. A Int C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   608
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   609
qed "Int_Union";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   610
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   611
Goal "Union(B) Int A = (UN C:B. C Int A)";
4674
248b876c2fa8 New theorems
paulson
parents: 4662
diff changeset
   612
by (Blast_tac 1);
248b876c2fa8 New theorems
paulson
parents: 4662
diff changeset
   613
qed "Int_Union2";
248b876c2fa8 New theorems
paulson
parents: 4662
diff changeset
   614
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   615
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   616
   Union of a family of unions **)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   617
Goal "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   618
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   619
qed "Un_Union_image";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   620
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   621
(*Equivalent version*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   622
Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   623
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   624
qed "UN_Un_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   625
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   626
Goal "A Un Inter(B) = (INT C:B. A Un C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   627
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   628
qed "Un_Inter";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   629
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   630
Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   631
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   632
qed "Int_Inter_image";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   633
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   634
(*Equivalent version*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   635
Goal "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   636
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   637
qed "INT_Int_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   638
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   639
(*Halmos, Naive Set Theory, page 35.*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   640
Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   641
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   642
qed "Int_UN_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   643
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   644
Goal "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   645
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   646
qed "Un_INT_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   647
5278
a903b66822e2 even more tidying of Goal commands
paulson
parents: 5238
diff changeset
   648
Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   649
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   650
qed "Int_UN_distrib2";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   651
5278
a903b66822e2 even more tidying of Goal commands
paulson
parents: 5238
diff changeset
   652
Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   653
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   654
qed "Un_INT_distrib2";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   655
2512
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   656
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   657
section"Bounded quantifiers";
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   658
3860
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   659
(** The following are not added to the default simpset because
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   660
    (a) they duplicate the body and (b) there are no similar rules for Int. **)
2512
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   661
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   662
Goal "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   663
by (Blast_tac 1);
2519
761e3094e32f New rewrites for bounded quantifiers
paulson
parents: 2513
diff changeset
   664
qed "ball_Un";
761e3094e32f New rewrites for bounded quantifiers
paulson
parents: 2513
diff changeset
   665
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   666
Goal "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   667
by (Blast_tac 1);
2519
761e3094e32f New rewrites for bounded quantifiers
paulson
parents: 2513
diff changeset
   668
qed "bex_Un";
2512
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   669
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   670
Goal "(ALL z: UNION A B. P z) = (ALL x:A. ALL z:B x. P z)";
4771
f1bacbbe02a8 new theorems
paulson
parents: 4748
diff changeset
   671
by (Blast_tac 1);
f1bacbbe02a8 new theorems
paulson
parents: 4748
diff changeset
   672
qed "ball_UN";
f1bacbbe02a8 new theorems
paulson
parents: 4748
diff changeset
   673
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   674
Goal "(EX z: UNION A B. P z) = (EX x:A. EX z:B x. P z)";
4771
f1bacbbe02a8 new theorems
paulson
parents: 4748
diff changeset
   675
by (Blast_tac 1);
f1bacbbe02a8 new theorems
paulson
parents: 4748
diff changeset
   676
qed "bex_UN";
f1bacbbe02a8 new theorems
paulson
parents: 4748
diff changeset
   677
2512
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   678
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   679
section "-";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   680
7127
48e235179ffb added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents: 6832
diff changeset
   681
Goal "A-B = A Int (-B)";
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   682
by (Blast_tac 1);
4662
73ba4d19f802 New absorbsion laws, etc
paulson
parents: 4645
diff changeset
   683
qed "Diff_eq";
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   684
7516
a1d476251238 moved identity theorems to Fun.ML
paulson
parents: 7127
diff changeset
   685
Goal "(A-B = {}) = (A<=B)";
a1d476251238 moved identity theorems to Fun.ML
paulson
parents: 7127
diff changeset
   686
by (Blast_tac 1);
a1d476251238 moved identity theorems to Fun.ML
paulson
parents: 7127
diff changeset
   687
qed "Diff_eq_empty_iff";
a1d476251238 moved identity theorems to Fun.ML
paulson
parents: 7127
diff changeset
   688
Addsimps[Diff_eq_empty_iff];
a1d476251238 moved identity theorems to Fun.ML
paulson
parents: 7127
diff changeset
   689
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   690
Goal "A-A = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   691
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   692
qed "Diff_cancel";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   693
Addsimps[Diff_cancel];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   694
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   695
Goal "A Int B = {} ==> A-B = A";
4674
248b876c2fa8 New theorems
paulson
parents: 4662
diff changeset
   696
by (blast_tac (claset() addEs [equalityE]) 1);
248b876c2fa8 New theorems
paulson
parents: 4662
diff changeset
   697
qed "Diff_triv";
248b876c2fa8 New theorems
paulson
parents: 4662
diff changeset
   698
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   699
Goal "{}-A = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   700
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   701
qed "empty_Diff";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   702
Addsimps[empty_Diff];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   703
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   704
Goal "A-{} = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   705
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   706
qed "Diff_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   707
Addsimps[Diff_empty];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   708
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   709
Goal "A-UNIV = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   710
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   711
qed "Diff_UNIV";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   712
Addsimps[Diff_UNIV];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   713
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   714
Goal "x~:A ==> A - insert x B = A-B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   715
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   716
qed "Diff_insert0";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   717
Addsimps [Diff_insert0];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   718
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   719
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   720
Goal "A - insert a B = A - B - {a}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   721
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   722
qed "Diff_insert";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   723
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   724
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   725
Goal "A - insert a B = A - {a} - B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   726
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   727
qed "Diff_insert2";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   728
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   729
Goal "insert x A - B = (if x:B then A-B else insert x (A-B))";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4674
diff changeset
   730
by (Simp_tac 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   731
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   732
qed "insert_Diff_if";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   733
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   734
Goal "x:B ==> insert x A - B = A-B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   735
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   736
qed "insert_Diff1";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   737
Addsimps [insert_Diff1];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   738
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   739
Goal "a:A ==> insert a (A-{a}) = A";
2922
580647a879cf Using Blast_tac
paulson
parents: 2912
diff changeset
   740
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   741
qed "insert_Diff";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   742
7824
1a85ba81d019 new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents: 7713
diff changeset
   743
Goal "x ~: A ==> (insert x A) - {x} = A";
1a85ba81d019 new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents: 7713
diff changeset
   744
by Auto_tac;
1a85ba81d019 new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents: 7713
diff changeset
   745
qed "Diff_insert_absorb";
1a85ba81d019 new default simprule Collect_const and new them Diff_insert_absorb
paulson
parents: 7713
diff changeset
   746
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   747
Goal "A Int (B-A) = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   748
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   749
qed "Diff_disjoint";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   750
Addsimps[Diff_disjoint];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   751
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   752
Goal "A<=B ==> A Un (B-A) = B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   753
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   754
qed "Diff_partition";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   755
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   756
Goal "[| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   757
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   758
qed "double_diff";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   759
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   760
Goal "A Un (B-A) = A Un B";
4645
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   761
by (Blast_tac 1);
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   762
qed "Un_Diff_cancel";
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   763
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   764
Goal "(B-A) Un A = B Un A";
4645
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   765
by (Blast_tac 1);
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   766
qed "Un_Diff_cancel2";
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   767
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   768
Addsimps [Un_Diff_cancel, Un_Diff_cancel2];
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   769
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   770
Goal "A - (B Un C) = (A-B) Int (A-C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   771
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   772
qed "Diff_Un";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   773
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   774
Goal "A - (B Int C) = (A-B) Un (A-C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   775
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   776
qed "Diff_Int";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   777
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   778
Goal "(A Un B) - C = (A - C) Un (B - C)";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   779
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   780
qed "Un_Diff";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   781
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   782
Goal "(A Int B) - C = A Int (B - C)";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   783
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   784
qed "Int_Diff";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   785
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   786
Goal "C Int (A-B) = (C Int A) - (C Int B)";
4748
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
   787
by (Blast_tac 1);
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
   788
qed "Diff_Int_distrib";
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
   789
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   790
Goal "(A-B) Int C = (A Int C) - (B Int C)";
4645
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   791
by (Blast_tac 1);
4748
2b8ead8e9393 more thms
paulson
parents: 4686
diff changeset
   792
qed "Diff_Int_distrib2";
4645
f5f957ab73eb New laws for union
paulson
parents: 4634
diff changeset
   793
7127
48e235179ffb added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents: 6832
diff changeset
   794
Goal "A - (- B) = A Int B";
5632
5682dce02591 new theorem
paulson
parents: 5590
diff changeset
   795
by Auto_tac;
5682dce02591 new theorem
paulson
parents: 5590
diff changeset
   796
qed "Diff_Compl";
5682dce02591 new theorem
paulson
parents: 5590
diff changeset
   797
Addsimps [Diff_Compl];
5682dce02591 new theorem
paulson
parents: 5590
diff changeset
   798
9608
a50dcf0475ad new thm and simprule Compl_Diff_eq
paulson
parents: 9447
diff changeset
   799
Goal "- (A-B) = -A Un B";
a50dcf0475ad new thm and simprule Compl_Diff_eq
paulson
parents: 9447
diff changeset
   800
by (blast_tac (claset() addIs []) 1); 
a50dcf0475ad new thm and simprule Compl_Diff_eq
paulson
parents: 9447
diff changeset
   801
qed "Compl_Diff_eq";
a50dcf0475ad new thm and simprule Compl_Diff_eq
paulson
parents: 9447
diff changeset
   802
Addsimps [Compl_Diff_eq];
a50dcf0475ad new thm and simprule Compl_Diff_eq
paulson
parents: 9447
diff changeset
   803
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   804
5238
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   805
section "Quantification over type \"bool\"";
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   806
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   807
Goal "(ALL b::bool. P b) = (P True & P False)";
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   808
by Auto_tac;
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   809
by (case_tac "b" 1);
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   810
by Auto_tac;
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   811
qed "all_bool_eq";
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   812
5762
149d435aa4d7 Added theorem bool_induct (for rep_datatype).
berghofe
parents: 5632
diff changeset
   813
bind_thm ("bool_induct", conjI RS (all_bool_eq RS iffD2) RS spec);
149d435aa4d7 Added theorem bool_induct (for rep_datatype).
berghofe
parents: 5632
diff changeset
   814
5238
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   815
Goal "(EX b::bool. P b) = (P True | P False)";
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   816
by Auto_tac;
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   817
by (case_tac "b" 1);
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   818
by Auto_tac;
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   819
qed "ex_bool_eq";
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   820
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   821
Goal "A Un B = (UN b. if b then A else B)";
8026
paulson
parents: 8017
diff changeset
   822
by (auto_tac(claset(), simpset() addsimps [split_if_mem2]));
5238
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   823
qed "Un_eq_UN";
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   824
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   825
Goal "(UN b::bool. A b) = (A True Un A False)";
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   826
by Auto_tac;
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   827
by (case_tac "b" 1);
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   828
by Auto_tac;
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   829
qed "UN_bool_eq";
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   830
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   831
Goal "(INT b::bool. A b) = (A True Int A False)";
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   832
by Auto_tac;
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   833
by (case_tac "b" 1);
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   834
by Auto_tac;
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   835
qed "INT_bool_eq";
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   836
c449f23728df Boolean quantification
paulson
parents: 5233
diff changeset
   837
6292
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   838
section "Pow";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   839
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   840
Goalw [Pow_def] "Pow {} = {{}}";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   841
by Auto_tac;
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   842
qed "Pow_empty";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   843
Addsimps [Pow_empty];
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   844
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   845
Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
10234
c8726d4ee89a tidied some awkward proofs
paulson
parents: 9969
diff changeset
   846
by (blast_tac (claset() addIs [inst "x" "?u-{a}" image_eqI]) 1);
6292
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   847
qed "Pow_insert";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   848
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   849
Goal "Pow (- A) = {-B |B. A: Pow B}";
10234
c8726d4ee89a tidied some awkward proofs
paulson
parents: 9969
diff changeset
   850
by (blast_tac (claset() addIs [inst "x" "- ?u" exI]) 1);
6292
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   851
qed "Pow_Compl";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   852
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   853
Goal "Pow UNIV = UNIV";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   854
by (Blast_tac 1);
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   855
qed "Pow_UNIV";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   856
Addsimps [Pow_UNIV];
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   857
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   858
Goal "Pow(A) Un Pow(B) <= Pow(A Un B)";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   859
by (Blast_tac 1);
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   860
qed "Un_Pow_subset";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   861
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   862
Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   863
by (Blast_tac 1);
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   864
qed "UN_Pow_subset";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   865
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   866
Goal "A <= Pow(Union(A))";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   867
by (Blast_tac 1);
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   868
qed "subset_Pow_Union";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   869
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   870
Goal "Union(Pow(A)) = A";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   871
by (Blast_tac 1);
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   872
qed "Union_Pow_eq";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   873
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   874
Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   875
by (Blast_tac 1);
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   876
qed "Pow_Int_eq";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   877
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   878
Goal "Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   879
by (Blast_tac 1);
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   880
qed "Pow_INT_eq";
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   881
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   882
Addsimps [Union_Pow_eq, Pow_Int_eq];
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   883
e50e1142dd06 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
paulson
parents: 6283
diff changeset
   884
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   885
section "Miscellany";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   886
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   887
Goal "(A = B) = ((A <= (B::'a set)) & (B<=A))";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   888
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   889
qed "set_eq_subset";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   890
9206
eaaee6bd74ba tidied and deleted two redundant theories
paulson
parents: 9098
diff changeset
   891
Goal "A <= B =  (ALL t. t:A --> t:B)";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   892
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   893
qed "subset_iff";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   894
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4882
diff changeset
   895
Goalw [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   896
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   897
qed "subset_iff_psubset_eq";
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   898
9206
eaaee6bd74ba tidied and deleted two redundant theories
paulson
parents: 9098
diff changeset
   899
Goal "(ALL x. x ~: A) = (A={})";
4423
a129b817b58a expandshort;
wenzelm
parents: 4306
diff changeset
   900
by (Blast_tac 1);
3896
ee8ebb74ec00 Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents: 3860
diff changeset
   901
qed "all_not_in_conv";
3907
51c00e87bd6e AddIffs [all_not_in_conv];
nipkow
parents: 3896
diff changeset
   902
AddIffs [all_not_in_conv];
3896
ee8ebb74ec00 Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents: 3860
diff changeset
   903
6007
91070f559b4d new theorem Pow_UNIV
paulson
parents: 5999
diff changeset
   904
5189
362e4d6213c5 Added theorem distinct_lemma (needed for datatypes).
berghofe
parents: 5148
diff changeset
   905
(** for datatypes **)
362e4d6213c5 Added theorem distinct_lemma (needed for datatypes).
berghofe
parents: 5148
diff changeset
   906
Goal "f x ~= f y ==> x ~= y";
362e4d6213c5 Added theorem distinct_lemma (needed for datatypes).
berghofe
parents: 5148
diff changeset
   907
by (Fast_tac 1);
362e4d6213c5 Added theorem distinct_lemma (needed for datatypes).
berghofe
parents: 5148
diff changeset
   908
qed "distinct_lemma";
362e4d6213c5 Added theorem distinct_lemma (needed for datatypes).
berghofe
parents: 5148
diff changeset
   909
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   910
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   911
(** Miniscoping: pushing in big Unions and Intersections **)
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   912
local
9422
4b6bc2b347e5 avoid referencing thy value;
wenzelm
parents: 9399
diff changeset
   913
  fun prover s = prove_goal (the_context ()) s (fn _ => [Blast_tac 1])
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   914
in
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   915
val UN_simps = map prover 
5941
1db9fad40a4f better miniscoping rules: the premise C~={} is not good
paulson
parents: 5931
diff changeset
   916
    ["!!C. c: C ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",
1db9fad40a4f better miniscoping rules: the premise C~={} is not good
paulson
parents: 5931
diff changeset
   917
     "!!C. c: C ==> (UN x:C. A x Un B)   = ((UN x:C. A x) Un B)",
1db9fad40a4f better miniscoping rules: the premise C~={} is not good
paulson
parents: 5931
diff changeset
   918
     "!!C. c: C ==> (UN x:C. A Un B x)   = (A Un (UN x:C. B x))",
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   919
     "(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   920
     "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   921
     "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
4231
a73f5a63f197 Removed
nipkow
parents: 4200
diff changeset
   922
     "(UN x:C. A - B x)    = (A - (INT x:C. B x))",
7914
5bfde29f1dbb new default simprules for UN and INT
paulson
parents: 7877
diff changeset
   923
     "(UN x: Union A. B x) = (UN y:A. UN x:y. B x)",
5bfde29f1dbb new default simprules for UN and INT
paulson
parents: 7877
diff changeset
   924
     "(UN z: UNION A B. C z) = (UN  x:A. UN z: B(x). C z)",
4231
a73f5a63f197 Removed
nipkow
parents: 4200
diff changeset
   925
     "(UN x:f``A. B x)     = (UN a:A. B(f a))"];
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   926
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   927
val INT_simps = map prover
5941
1db9fad40a4f better miniscoping rules: the premise C~={} is not good
paulson
parents: 5931
diff changeset
   928
    ["!!C. c: C ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
1db9fad40a4f better miniscoping rules: the premise C~={} is not good
paulson
parents: 5931
diff changeset
   929
     "!!C. c: C ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))",
1db9fad40a4f better miniscoping rules: the premise C~={} is not good
paulson
parents: 5931
diff changeset
   930
     "!!C. c: C ==> (INT x:C. A x - B)   = ((INT x:C. A x) - B)",
1db9fad40a4f better miniscoping rules: the premise C~={} is not good
paulson
parents: 5931
diff changeset
   931
     "!!C. c: C ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   932
     "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   933
     "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
4231
a73f5a63f197 Removed
nipkow
parents: 4200
diff changeset
   934
     "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",
7914
5bfde29f1dbb new default simprules for UN and INT
paulson
parents: 7877
diff changeset
   935
     "(INT x: Union A. B x) = (INT y:A. INT x:y. B x)",
5bfde29f1dbb new default simprules for UN and INT
paulson
parents: 7877
diff changeset
   936
     "(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)",
4231
a73f5a63f197 Removed
nipkow
parents: 4200
diff changeset
   937
     "(INT x:f``A. B x)    = (INT a:A. B(f a))"];
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   938
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   939
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   940
val ball_simps = map prover
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   941
    ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   942
     "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
3422
16ae2c20801c New miniscoping rules for ALL
paulson
parents: 3415
diff changeset
   943
     "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",
16ae2c20801c New miniscoping rules for ALL
paulson
parents: 3415
diff changeset
   944
     "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)",
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   945
     "(ALL x:{}. P x) = True",
4136
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   946
     "(ALL x:UNIV. P x) = (ALL x. P x)",
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   947
     "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   948
     "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
5233
3571ff68ceda New rewrite rules for quantification over bounded UNIONs
paulson
parents: 5189
diff changeset
   949
     "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)",
3860
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   950
     "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   951
     "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   952
     "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   953
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   954
val ball_conj_distrib = 
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   955
    prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))";
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   956
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   957
val bex_simps = map prover
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   958
    ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   959
     "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   960
     "(EX x:{}. P x) = False",
4136
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   961
     "(EX x:UNIV. P x) = (EX x. P x)",
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   962
     "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   963
     "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
5233
3571ff68ceda New rewrite rules for quantification over bounded UNIONs
paulson
parents: 5189
diff changeset
   964
     "(EX x: UNION A B. P x) = (EX a:A. EX x: B a.  P x)",
3860
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   965
     "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   966
     "(EX x:f``A. P x) = (EX x:A. P(f x))",
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   967
     "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   968
3426
9aa5864a7eea The name bex_conj_distrib was WRONG
paulson
parents: 3422
diff changeset
   969
val bex_disj_distrib = 
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   970
    prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   971
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   972
end;
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   973
7648
8258b93cdd32 bind_thms;
wenzelm
parents: 7516
diff changeset
   974
bind_thms ("UN_simps", UN_simps);
8258b93cdd32 bind_thms;
wenzelm
parents: 7516
diff changeset
   975
bind_thms ("INT_simps", INT_simps);
8258b93cdd32 bind_thms;
wenzelm
parents: 7516
diff changeset
   976
bind_thms ("ball_simps", ball_simps);
8258b93cdd32 bind_thms;
wenzelm
parents: 7516
diff changeset
   977
bind_thms ("bex_simps", bex_simps);
8258b93cdd32 bind_thms;
wenzelm
parents: 7516
diff changeset
   978
bind_thm ("ball_conj_distrib", ball_conj_distrib);
8258b93cdd32 bind_thms;
wenzelm
parents: 7516
diff changeset
   979
bind_thm ("bex_disj_distrib", bex_disj_distrib);
8258b93cdd32 bind_thms;
wenzelm
parents: 7516
diff changeset
   980
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   981
Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);