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