src/HOL/equalities.ML
author paulson
Tue, 10 Feb 1998 10:27:30 +0100
changeset 4615 67457d16cdbc
parent 4609 b435c5a320b0
child 4634 83d364462ce1
permissions -rw-r--r--
New Addsimps for Compl rules
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
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    15
goal thy "{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
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    20
goal thy "(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
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    25
goalw thy [psubset_def] "~ (A < {})";
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
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
    30
section "insert";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    32
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    33
goal thy "insert a A = {a} Un A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    34
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    35
qed "insert_is_Un";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    36
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    37
goal thy "insert a A ~= {}";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    38
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
    39
qed"insert_not_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    40
Addsimps[insert_not_empty];
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
    41
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
    42
bind_thm("empty_not_insert",insert_not_empty RS not_sym);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    43
Addsimps[empty_not_insert];
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
    44
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    45
goal thy "!!a. a:A ==> insert a A = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    46
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
qed "insert_absorb";
4605
579e0ef2df6b Added `remdups'
nipkow
parents: 4477
diff changeset
    48
(* Addsimps [insert_absorb] causes recursive (ie quadtratic) calls
579e0ef2df6b Added `remdups'
nipkow
parents: 4477
diff changeset
    49
   in case of nested inserts!
579e0ef2df6b Added `remdups'
nipkow
parents: 4477
diff changeset
    50
*)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    52
goal thy "insert x (insert x A) = insert x A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    53
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    54
qed "insert_absorb2";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    55
Addsimps [insert_absorb2];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    56
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    57
goal thy "insert x (insert y A) = insert y (insert x A)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    58
by (Blast_tac 1);
1879
83c70ad381c1 Added insert_commute
paulson
parents: 1843
diff changeset
    59
qed "insert_commute";
83c70ad381c1 Added insert_commute
paulson
parents: 1843
diff changeset
    60
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    61
goal thy "(insert x A <= B) = (x:B & A <= B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    62
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    63
qed "insert_subset";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    64
Addsimps[insert_subset];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    65
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    66
goal thy "!!a. 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
    67
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    68
qed "insert_lim";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    69
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    70
(* use new B rather than (A-{a}) to avoid infinite unfolding *)
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    71
goal thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
1553
4eb4a9c7d736 Ran expandshort
paulson
parents: 1548
diff changeset
    72
by (res_inst_tac [("x","A-{a}")] exI 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    73
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    74
qed "mk_disjoint_insert";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    76
goal thy
1843
a6d7aef48c2f Removed the unused eq_cs, and added some distributive laws
paulson
parents: 1786
diff changeset
    77
    "!!A. 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
    78
by (Blast_tac 1);
1843
a6d7aef48c2f Removed the unused eq_cs, and added some distributive laws
paulson
parents: 1786
diff changeset
    79
qed "UN_insert_distrib";
a6d7aef48c2f Removed the unused eq_cs, and added some distributive laws
paulson
parents: 1786
diff changeset
    80
1660
8cb42cd97579 *** empty log message ***
oheimb
parents: 1618
diff changeset
    81
section "``";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    83
goal thy "f``{} = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    84
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    85
qed "image_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    86
Addsimps[image_empty];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    87
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    88
goal thy "f``insert a B = insert (f a) (f``B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
    89
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    90
qed "image_insert";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
    91
Addsimps[image_insert];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    92
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    93
goal thy  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    94
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    95
qed "image_UNION";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    96
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
    97
goal thy "(%x. x) `` Y = Y";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    98
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
    99
qed "image_id";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   100
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   101
goal thy "f``(g``A) = (%x. f (g x)) `` A";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3426
diff changeset
   102
by (Blast_tac 1);
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   103
qed "image_image";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   104
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   105
goal thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   106
by (Blast_tac 1);
1884
5a1f81da3e12 Proved insert_image
paulson
parents: 1879
diff changeset
   107
qed "insert_image";
5a1f81da3e12 Proved insert_image
paulson
parents: 1879
diff changeset
   108
Addsimps [insert_image];
5a1f81da3e12 Proved insert_image
paulson
parents: 1879
diff changeset
   109
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   110
goal thy "(f``A = {}) = (A = {})";
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   111
by (blast_tac (claset() addSEs [equalityCE]) 1);
3415
c068bd2f0bbd Moved image_is_empty from Finite.ML to equalities.ML
nipkow
parents: 3384
diff changeset
   112
qed "image_is_empty";
c068bd2f0bbd Moved image_is_empty from Finite.ML to equalities.ML
nipkow
parents: 3384
diff changeset
   113
AddIffs [image_is_empty];
c068bd2f0bbd Moved image_is_empty from Finite.ML to equalities.ML
nipkow
parents: 3384
diff changeset
   114
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   115
goalw thy [image_def]
1763
fb07e359b59f expanded TABs
berghofe
parents: 1754
diff changeset
   116
"(%x. if P x then f x else g x) `` S                    \
4200
5a2cd204f8b4 Rationalized the theorem if_image_distrib.
paulson
parents: 4192
diff changeset
   117
\ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
2031
03a843f0f447 Ran expandshort
paulson
parents: 2024
diff changeset
   118
by (split_tac [expand_if] 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   119
by (Blast_tac 1);
1748
88650ba93c10 Added if_image_distrib.
nipkow
parents: 1660
diff changeset
   120
qed "if_image_distrib";
88650ba93c10 Added if_image_distrib.
nipkow
parents: 1660
diff changeset
   121
Addsimps[if_image_distrib];
88650ba93c10 Added if_image_distrib.
nipkow
parents: 1660
diff changeset
   122
4136
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   123
val prems= goal thy "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   124
by (rtac set_ext 1);
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   125
by (simp_tac (simpset() addsimps image_def::prems) 1);
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   126
qed "image_cong";
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   127
1748
88650ba93c10 Added if_image_distrib.
nipkow
parents: 1660
diff changeset
   128
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   129
section "Int";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   130
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   131
goal thy "A Int A = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   132
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   133
qed "Int_absorb";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   134
Addsimps[Int_absorb];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   135
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   136
goal thy " A Int (A Int B) = A Int B";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   137
by (Blast_tac 1);
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   138
qed "Int_left_absorb";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   139
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   140
goal thy "A Int B  =  B Int A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   141
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   142
qed "Int_commute";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   143
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   144
goal thy "A Int (B Int C) = B Int (A Int C)";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   145
by (Blast_tac 1);
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   146
qed "Int_left_commute";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   147
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   148
goal thy "(A Int B) Int C  =  A Int (B Int C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   149
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   150
qed "Int_assoc";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   151
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   152
(*Intersection is an AC-operator*)
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   153
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
   154
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   155
goal thy "{} Int B = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   156
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   157
qed "Int_empty_left";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   158
Addsimps[Int_empty_left];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   159
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   160
goal thy "A Int {} = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   161
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   162
qed "Int_empty_right";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   163
Addsimps[Int_empty_right];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   164
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   165
goal thy "(A Int B = {}) = (A <= Compl B)";
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   166
by (blast_tac (claset() addSEs [equalityCE]) 1);
3356
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   167
qed "disjoint_eq_subset_Compl";
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   168
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   169
goal thy "UNIV Int B = B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   170
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   171
qed "Int_UNIV_left";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   172
Addsimps[Int_UNIV_left];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   173
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   174
goal thy "A Int UNIV = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   175
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   176
qed "Int_UNIV_right";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   177
Addsimps[Int_UNIV_right];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   178
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   179
goal thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   180
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   181
qed "Int_Un_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   182
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   183
goal thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   184
by (Blast_tac 1);
1618
372880456b5b Library changes for mutilated checkerboard
paulson
parents: 1564
diff changeset
   185
qed "Int_Un_distrib2";
372880456b5b Library changes for mutilated checkerboard
paulson
parents: 1564
diff changeset
   186
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   187
goal thy "(A<=B) = (A Int B = A)";
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   188
by (blast_tac (claset() addSEs [equalityCE]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   189
qed "subset_Int_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   190
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   191
goal thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   192
by (blast_tac (claset() addEs [equalityCE]) 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   193
qed "Int_UNIV";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   194
Addsimps[Int_UNIV];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   195
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   196
section "Un";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   197
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   198
goal thy "A Un A = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   199
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   200
qed "Un_absorb";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   201
Addsimps[Un_absorb];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   202
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   203
goal thy " 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
   204
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   205
qed "Un_left_absorb";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   206
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   207
goal thy "A Un B  =  B Un A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   208
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   209
qed "Un_commute";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   210
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   211
goal thy "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
   212
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   213
qed "Un_left_commute";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   214
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   215
goal thy "(A Un B) Un C  =  A Un (B Un C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   216
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   217
qed "Un_assoc";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   218
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   219
(*Union is an AC-operator*)
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   220
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
   221
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   222
goal thy "{} Un B = B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   223
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   224
qed "Un_empty_left";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   225
Addsimps[Un_empty_left];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   226
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   227
goal thy "A Un {} = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   228
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   229
qed "Un_empty_right";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   230
Addsimps[Un_empty_right];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   231
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   232
goal thy "UNIV Un B = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   233
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   234
qed "Un_UNIV_left";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   235
Addsimps[Un_UNIV_left];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   236
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   237
goal thy "A Un UNIV = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   238
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   239
qed "Un_UNIV_right";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   240
Addsimps[Un_UNIV_right];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   241
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   242
goal thy "(insert a B) Un C = insert a (B Un C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   243
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   244
qed "Un_insert_left";
3384
5ef99c94e1fb Now Un_insert_left, Un_insert_right are default rewrite rules
paulson
parents: 3356
diff changeset
   245
Addsimps[Un_insert_left];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   246
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   247
goal thy "A Un (insert a B) = insert a (A Un B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   248
by (Blast_tac 1);
1917
27b71d839d50 Added proof of Un_insert_right
paulson
parents: 1884
diff changeset
   249
qed "Un_insert_right";
3384
5ef99c94e1fb Now Un_insert_left, Un_insert_right are default rewrite rules
paulson
parents: 3356
diff changeset
   250
Addsimps[Un_insert_right];
1917
27b71d839d50 Added proof of Un_insert_right
paulson
parents: 1884
diff changeset
   251
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   252
goal thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   253
\                                      else        B Int C)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   254
by (simp_tac (simpset() addsplits [expand_if]) 1);
3356
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   255
by (Blast_tac 1);
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   256
qed "Int_insert_left";
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   257
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   258
goal thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   259
\                                      else        A Int B)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   260
by (simp_tac (simpset() addsplits [expand_if]) 1);
3356
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   261
by (Blast_tac 1);
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   262
qed "Int_insert_right";
9b899eb8a036 New theorem disjoint_eq_subset_Compl
paulson
parents: 3348
diff changeset
   263
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   264
goal thy "A Un (B Int C)  =  (A Un B) Int (A Un C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   265
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   266
qed "Un_Int_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   267
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   268
goal thy "(B Int C) Un A =  (B Un A) Int (C Un A)";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   269
by (Blast_tac 1);
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   270
qed "Un_Int_distrib2";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   271
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   272
goal thy
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   273
 "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   274
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   275
qed "Un_Int_crazy";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   276
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   277
goal thy "(A<=B) = (A Un B = B)";
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   278
by (blast_tac (claset() addSEs [equalityCE]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   279
qed "subset_Un_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   280
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   281
goal thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   282
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   283
qed "subset_insert_iff";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   284
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   285
goal thy "(A Un B = {}) = (A = {} & B = {})";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   286
by (blast_tac (claset() addEs [equalityCE]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   287
qed "Un_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   288
Addsimps[Un_empty];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   289
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   290
section "Compl";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   291
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   292
goal thy "A Int Compl(A) = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   293
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   294
qed "Compl_disjoint";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   295
Addsimps[Compl_disjoint];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   296
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   297
goal thy "A Un Compl(A) = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   298
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   299
qed "Compl_partition";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   300
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   301
goal thy "Compl(Compl(A)) = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   302
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   303
qed "double_complement";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   304
Addsimps[double_complement];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   305
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   306
goal thy "Compl(A Un B) = Compl(A) Int Compl(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   307
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   308
qed "Compl_Un";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   309
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   310
goal thy "Compl(A Int B) = Compl(A) Un Compl(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   311
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   312
qed "Compl_Int";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   313
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   314
goal thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   315
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   316
qed "Compl_UN";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   317
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   318
goal thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   319
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   320
qed "Compl_INT";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   321
4615
67457d16cdbc New Addsimps for Compl rules
paulson
parents: 4609
diff changeset
   322
Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT];
67457d16cdbc New Addsimps for Compl rules
paulson
parents: 4609
diff changeset
   323
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   324
(*Halmos, Naive Set Theory, page 16.*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   325
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   326
goal thy "((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
   327
by (blast_tac (claset() addSEs [equalityCE]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   328
qed "Un_Int_assoc_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   329
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   330
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   331
section "Union";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   332
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   333
goal thy "Union({}) = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   334
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   335
qed "Union_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   336
Addsimps[Union_empty];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   337
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   338
goal thy "Union(UNIV) = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   339
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   340
qed "Union_UNIV";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   341
Addsimps[Union_UNIV];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   342
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   343
goal thy "Union(insert a B) = a Un Union(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   344
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   345
qed "Union_insert";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   346
Addsimps[Union_insert];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   347
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   348
goal thy "Union(A Un B) = Union(A) Un Union(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   349
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   350
qed "Union_Un_distrib";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   351
Addsimps[Union_Un_distrib];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   352
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   353
goal thy "Union(A Int B) <= Union(A) Int Union(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   354
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   355
qed "Union_Int_subset";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   356
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   357
goal thy "(Union M = {}) = (! A : M. A = {})"; 
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   358
by (blast_tac (claset() addEs [equalityCE]) 1);
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   359
qed "Union_empty_conv"; 
4003
nipkow
parents: 3919
diff changeset
   360
AddIffs [Union_empty_conv];
nipkow
parents: 3919
diff changeset
   361
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   362
goal thy "(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
   363
by (blast_tac (claset() addSEs [equalityCE]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   364
qed "Union_disjoint";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   365
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   366
section "Inter";
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   367
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   368
goal thy "Inter({}) = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   369
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   370
qed "Inter_empty";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   371
Addsimps[Inter_empty];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   372
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   373
goal thy "Inter(UNIV) = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   374
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   375
qed "Inter_UNIV";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   376
Addsimps[Inter_UNIV];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   377
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   378
goal thy "Inter(insert a B) = a Int Inter(B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   379
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   380
qed "Inter_insert";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   381
Addsimps[Inter_insert];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   382
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   383
goal thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   384
by (Blast_tac 1);
1564
822575c737bd Deleted faulty comment; proved new rule Inter_Un_subset
paulson
parents: 1553
diff changeset
   385
qed "Inter_Un_subset";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   386
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   387
goal thy "Inter(A Un B) = Inter(A) Int Inter(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 "Inter_Un_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   390
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   391
section "UN and INT";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   392
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   393
(*Basic identities*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   394
4200
5a2cd204f8b4 Rationalized the theorem if_image_distrib.
paulson
parents: 4192
diff changeset
   395
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
   396
(*Addsimps[not_empty];*)
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   397
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   398
goal thy "(UN x:{}. B x) = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   399
by (Blast_tac 1);
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
   400
qed "UN_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   401
Addsimps[UN_empty];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   402
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   403
goal thy "(UN x:A. {}) = {}";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3426
diff changeset
   404
by (Blast_tac 1);
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   405
qed "UN_empty2";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   406
Addsimps[UN_empty2];
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   407
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   408
goal thy "(INT x:{}. B x) = UNIV";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   409
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   410
qed "INT_empty";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   411
Addsimps[INT_empty];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   412
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   413
goal thy "(UN x:insert a A. B x) = B a Un UNION A B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   414
by (Blast_tac 1);
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
   415
qed "UN_insert";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   416
Addsimps[UN_insert];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   417
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   418
goal thy "(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
   419
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   420
qed "UN_Un";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   421
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   422
goal thy "(INT x:insert a A. B x) = B a Int INTER A 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 "INT_insert";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   425
Addsimps[INT_insert];
1179
7678408f9751 Added insert_not_empty, UN_empty and UN_insert (to set_ss).
nipkow
parents: 923
diff changeset
   426
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   427
goal thy
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   428
    "!!A. 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
   429
by (Blast_tac 1);
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   430
qed "INT_insert_distrib";
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   431
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   432
goal thy "Union(B``A) = (UN x:A. B(x))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   433
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   434
qed "Union_image_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   435
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   436
goal thy "Inter(B``A) = (INT x:A. B(x))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   437
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   438
qed "Inter_image_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   439
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   440
goal thy "!!A. A~={} ==> (UN y:A. c) = c";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   441
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   442
qed "UN_constant";
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   443
Addsimps[UN_constant];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   444
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   445
goal thy "!!A. A~={} ==> (INT y:A. c) = c";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   446
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   447
qed "INT_constant";
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   448
Addsimps[INT_constant];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   449
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   450
goal thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   451
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   452
qed "UN_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   453
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   454
(*Look: it has an EXISTENTIAL quantifier*)
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   455
goal thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   456
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   457
qed "INT_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   458
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   459
goalw thy [o_def] "UNION A (g o f) = UNION (f``A) g";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   460
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   461
qed "UNION_o";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   462
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   463
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   464
(*Distributive laws...*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   465
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   466
goal thy "A Int Union(B) = (UN C:B. A Int C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   467
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   468
qed "Int_Union";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   469
4306
ddbe1a9722ab Tidying and using equalityCE instead of the slower equalityE
paulson
parents: 4231
diff changeset
   470
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   471
   Union of a family of unions **)
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   472
goal thy "(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
   473
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   474
qed "Un_Union_image";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   475
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   476
(*Equivalent version*)
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   477
goal thy "(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
   478
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   479
qed "UN_Un_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   480
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   481
goal thy "A Un Inter(B) = (INT C:B. A Un C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   482
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   483
qed "Un_Inter";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   484
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   485
goal thy "(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
   486
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   487
qed "Int_Inter_image";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   488
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   489
(*Equivalent version*)
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   490
goal thy "(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
   491
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   492
qed "INT_Int_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   493
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   494
(*Halmos, Naive Set Theory, page 35.*)
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   495
goal thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   496
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   497
qed "Int_UN_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   498
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   499
goal thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   500
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   501
qed "Un_INT_distrib";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   502
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   503
goal thy
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   504
    "(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
   505
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   506
qed "Int_UN_distrib2";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   507
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   508
goal thy
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   509
    "(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
   510
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   511
qed "Un_INT_distrib2";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   512
2512
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   513
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   514
section"Bounded quantifiers";
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   515
3860
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   516
(** The following are not added to the default simpset because
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   517
    (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
   518
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   519
goal thy "(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
   520
by (Blast_tac 1);
2519
761e3094e32f New rewrites for bounded quantifiers
paulson
parents: 2513
diff changeset
   521
qed "ball_Un";
761e3094e32f New rewrites for bounded quantifiers
paulson
parents: 2513
diff changeset
   522
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   523
goal thy "(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
   524
by (Blast_tac 1);
2519
761e3094e32f New rewrites for bounded quantifiers
paulson
parents: 2513
diff changeset
   525
qed "bex_Un";
2512
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   526
0231e4f467f2 Got rid of Alls in List.
nipkow
parents: 2031
diff changeset
   527
1548
afe750876848 Added 'section' commands
nipkow
parents: 1531
diff changeset
   528
section "-";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   529
4609
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   530
goal thy "A-B = A Int Compl B";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   531
by (Blast_tac 1);
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   532
qed "Diff_eq_Int_Compl";
b435c5a320b0 AC and other rewrite rules for Un and Int
paulson
parents: 4605
diff changeset
   533
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   534
goal thy "A-A = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   535
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   536
qed "Diff_cancel";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   537
Addsimps[Diff_cancel];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   538
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   539
goal thy "{}-A = {}";
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 "empty_Diff";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   542
Addsimps[empty_Diff];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   543
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   544
goal thy "A-{} = A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   545
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   546
qed "Diff_empty";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   547
Addsimps[Diff_empty];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   548
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   549
goal thy "A-UNIV = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   550
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   551
qed "Diff_UNIV";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   552
Addsimps[Diff_UNIV];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   553
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   554
goal thy "!!x. x~:A ==> A - insert x B = A-B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   555
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   556
qed "Diff_insert0";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   557
Addsimps [Diff_insert0];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   558
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   559
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   560
goal thy "A - insert a B = A - B - {a}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   561
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   562
qed "Diff_insert";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   563
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   564
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   565
goal thy "A - insert a B = A - {a} - B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   566
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   567
qed "Diff_insert2";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   568
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   569
goal thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   570
by (simp_tac (simpset() addsplits [expand_if]) 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   571
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   572
qed "insert_Diff_if";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   573
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   574
goal thy "!!x. x:B ==> insert x A - B = A-B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   575
by (Blast_tac 1);
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   576
qed "insert_Diff1";
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   577
Addsimps [insert_Diff1];
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   578
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   579
goal thy "!!a. a:A ==> insert a (A-{a}) = A";
2922
580647a879cf Using Blast_tac
paulson
parents: 2912
diff changeset
   580
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   581
qed "insert_Diff";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   582
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   583
goal thy "A Int (B-A) = {}";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   584
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   585
qed "Diff_disjoint";
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1465
diff changeset
   586
Addsimps[Diff_disjoint];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   587
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   588
goal thy "!!A. A<=B ==> A Un (B-A) = B";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   589
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   590
qed "Diff_partition";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   591
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   592
goal thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   593
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   594
qed "double_diff";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   595
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   596
goal thy "A - (B Un C) = (A-B) Int (A-C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   597
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   598
qed "Diff_Un";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   599
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   600
goal thy "A - (B Int C) = (A-B) Un (A-C)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2519
diff changeset
   601
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   602
qed "Diff_Int";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   603
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   604
goal thy "(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
   605
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   606
qed "Un_Diff";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   607
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   608
goal thy "(A Int B) - C = (A - C) Int (B - C)";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   609
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   610
qed "Int_Diff";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   611
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   612
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   613
section "Miscellany";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   614
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   615
goal thy "(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
   616
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   617
qed "set_eq_subset";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   618
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   619
goal thy "A <= B =  (! t. t:A --> t:B)";
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   620
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   621
qed "subset_iff";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   622
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   623
goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   624
by (Blast_tac 1);
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 2922
diff changeset
   625
qed "subset_iff_psubset_eq";
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   626
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   627
goal thy "(!x. x ~: A) = (A={})";
4423
a129b817b58a expandshort;
wenzelm
parents: 4306
diff changeset
   628
by (Blast_tac 1);
3896
ee8ebb74ec00 Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents: 3860
diff changeset
   629
qed "all_not_in_conv";
3907
51c00e87bd6e AddIffs [all_not_in_conv];
nipkow
parents: 3896
diff changeset
   630
AddIffs [all_not_in_conv];
3896
ee8ebb74ec00 Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents: 3860
diff changeset
   631
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   632
goalw thy [Pow_def] "Pow {} = {{}}";
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4423
diff changeset
   633
by Auto_tac;
3348
3f9a806f061e Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents: 3222
diff changeset
   634
qed "Pow_empty";
3f9a806f061e Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents: 3222
diff changeset
   635
Addsimps [Pow_empty];
3f9a806f061e Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents: 3222
diff changeset
   636
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   637
goal thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
3724
f33e301a89f5 Step_tac -> Safe_tac
paulson
parents: 3457
diff changeset
   638
by Safe_tac;
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3426
diff changeset
   639
by (etac swap 1);
3348
3f9a806f061e Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents: 3222
diff changeset
   640
by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
3f9a806f061e Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents: 3222
diff changeset
   641
by (ALLGOALS Blast_tac);
3f9a806f061e Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents: 3222
diff changeset
   642
qed "Pow_insert";
3f9a806f061e Two useful facts about Powersets suggested by Florian Kammueller
paulson
parents: 3222
diff changeset
   643
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   644
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   645
(** Miniscoping: pushing in big Unions and Intersections **)
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   646
local
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 4003
diff changeset
   647
  fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   648
in
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   649
val UN_simps = map prover 
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   650
    ["!!C. C ~= {} ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   651
     "!!C. C ~= {} ==> (UN x:C. A x Un B)   = ((UN x:C. A x) Un B)",
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   652
     "!!C. C ~= {} ==> (UN x:C. A Un B x)   = (A Un (UN x:C. B x))",
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   653
     "(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
   654
     "(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
   655
     "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
4231
a73f5a63f197 Removed
nipkow
parents: 4200
diff changeset
   656
     "(UN x:C. A - B x)    = (A - (INT x:C. B x))",
a73f5a63f197 Removed
nipkow
parents: 4200
diff changeset
   657
     "(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
   658
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   659
val INT_simps = map prover
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   660
    ["!!C. C ~= {} ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   661
     "!!C. C ~= {} ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))",
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   662
     "!!C. C ~= {} ==> (INT x:C. A x - B)   = ((INT x:C. A x) - B)",
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   663
     "!!C. C ~= {} ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   664
     "(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
   665
     "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
4231
a73f5a63f197 Removed
nipkow
parents: 4200
diff changeset
   666
     "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",
a73f5a63f197 Removed
nipkow
parents: 4200
diff changeset
   667
     "(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
   668
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   669
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   670
val ball_simps = map prover
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   671
    ["(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
   672
     "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
3422
16ae2c20801c New miniscoping rules for ALL
paulson
parents: 3415
diff changeset
   673
     "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",
16ae2c20801c New miniscoping rules for ALL
paulson
parents: 3415
diff changeset
   674
     "(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
   675
     "(ALL x:{}. P x) = True",
4136
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   676
     "(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
   677
     "(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
   678
     "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
3860
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   679
     "(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
   680
     "(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
   681
     "(~(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
   682
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   683
val ball_conj_distrib = 
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   684
    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
   685
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   686
val bex_simps = map prover
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   687
    ["(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
   688
     "(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
   689
     "(EX x:{}. P x) = False",
4136
ba267836dd7a removed redundant ball_image
oheimb
parents: 4089
diff changeset
   690
     "(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
   691
     "(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
   692
     "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
3860
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
   693
     "(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
   694
     "(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
   695
     "(~(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
   696
3426
9aa5864a7eea The name bex_conj_distrib was WRONG
paulson
parents: 3422
diff changeset
   697
val bex_disj_distrib = 
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2512
diff changeset
   698
    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
   699
2021
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   700
end;
dd5866263153 Added miniscoping for UN and INT
paulson
parents: 1917
diff changeset
   701
4159
4aff9b7e5597 UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents: 4136
diff changeset
   702
Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);