src/ZF/equalities.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46821 ff6b0c1087f2
child 58860 fee7cfa69c50
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35762
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 24893
diff changeset
     1
(*  Title:      ZF/equalities.thy
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
     3
    Copyright   1992  University of Cambridge
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
     4
*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
     5
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
     6
header{*Basic Equalities and Inclusions*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14883
diff changeset
     8
theory equalities imports pair begin
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
     9
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
    10
text{*These cover union, intersection, converse, domain, range, etc.  Philippe
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
    11
de Groote proved many of the inclusions.*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
    12
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    13
lemma in_mono: "A\<subseteq>B ==> x\<in>A \<longrightarrow> x\<in>B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
    14
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
    15
13174
85d3c0981a16 more tidying
paulson
parents: 13172
diff changeset
    16
lemma the_eq_0 [simp]: "(THE x. False) = 0"
85d3c0981a16 more tidying
paulson
parents: 13172
diff changeset
    17
by (blast intro: the_0)
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    18
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
    19
subsection{*Bounded Quantifiers*}
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    20
text {* \medskip
13178
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    21
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    22
  The following are not added to the default simpset because
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
    23
  (a) they duplicate the body and (b) there are no similar rules for @{text Int}.*}
13178
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    24
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    25
lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
13178
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    26
  by blast
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    27
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    28
lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
13178
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    29
  by blast
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    30
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    31
lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
13178
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    32
  by blast
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    33
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    34
lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
13178
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    35
  by blast
bc54319f6875 new quantifier lemmas
paulson
parents: 13174
diff changeset
    36
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
    37
subsection{*Converse of a Relation*}
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    38
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    39
lemma converse_iff [simp]: "<a,b>\<in> converse(r) \<longleftrightarrow> <b,a>\<in>r"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    40
by (unfold converse_def, blast)
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    41
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
    42
lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    43
by (unfold converse_def, blast)
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    44
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
    45
lemma converseD: "<a,b> \<in> converse(r) ==> <b,a> \<in> r"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    46
by (unfold converse_def, blast)
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    47
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    48
lemma converseE [elim!]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    49
    "[| yx \<in> converse(r);
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
    50
        !!x y. [| yx=<y,x>;  <x,y>\<in>r |] ==> P |]
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    51
     ==> P"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    52
by (unfold converse_def, blast)
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    53
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
    54
lemma converse_converse: "r\<subseteq>Sigma(A,B) ==> converse(converse(r)) = r"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    55
by blast
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    56
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
    57
lemma converse_type: "r\<subseteq>A*B ==> converse(r)\<subseteq>B*A"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    58
by blast
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    59
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    60
lemma converse_prod [simp]: "converse(A*B) = B*A"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    61
by blast
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    62
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    63
lemma converse_empty [simp]: "converse(0) = 0"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    64
by blast
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    65
13174
85d3c0981a16 more tidying
paulson
parents: 13172
diff changeset
    66
lemma converse_subset_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    67
     "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) \<longleftrightarrow> A \<subseteq> B"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    68
by blast
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    69
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    70
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
    71
subsection{*Finite Set Constructions Using @{term cons}*}
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    72
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
    73
lemma cons_subsetI: "[| a\<in>C; B\<subseteq>C |] ==> cons(a,B) \<subseteq> C"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    74
by blast
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    75
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
    76
lemma subset_consI: "B \<subseteq> cons(a,B)"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    77
by blast
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    78
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    79
lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C \<longleftrightarrow> a\<in>C & B\<subseteq>C"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    80
by blast
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    81
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    82
(*A safe special case of subset elimination, adding no new variables
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
    83
  [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 42793
diff changeset
    84
lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    85
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    86
lemma subset_empty_iff: "A\<subseteq>0 \<longleftrightarrow> A=0"
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    87
by blast
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    88
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    89
lemma subset_cons_iff: "C\<subseteq>cons(a,B) \<longleftrightarrow> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
13169
394a6c649547 conversion of OrdQuant.ML to Isar
paulson
parents: 13168
diff changeset
    90
by blast
13168
afcbca3498b0 converted domrange to Isar and merged with equalities
paulson
parents: 13165
diff changeset
    91
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
    92
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    93
lemma cons_eq: "{a} \<union> B = cons(a,B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
    94
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
    95
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
    96
lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
    97
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
    98
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
    99
lemma cons_absorb: "a: B ==> cons(a,B) = B"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   100
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   101
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   102
lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   103
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   104
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   105
lemma Diff_cons_eq: "cons(a,B) - C = (if a\<in>C then B-C else cons(a,B-C))"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14046
diff changeset
   106
by auto
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14046
diff changeset
   107
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   108
lemma equal_singleton [rule_format]: "[| a: C;  \<forall>y\<in>C. y=b |] ==> C = {b}"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   109
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   110
13172
03a5afa7b888 tidying up
paulson
parents: 13169
diff changeset
   111
lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
03a5afa7b888 tidying up
paulson
parents: 13169
diff changeset
   112
by blast
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   113
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   114
(** singletons **)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   115
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   116
lemma singleton_subsetI: "a\<in>C ==> {a} \<subseteq> C"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   117
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   118
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   119
lemma singleton_subsetD: "{a} \<subseteq> C  ==>  a\<in>C"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   120
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   121
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   122
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   123
(** succ **)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   124
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   125
lemma subset_succI: "i \<subseteq> succ(i)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   126
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   127
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   128
(*But if j is an ordinal or is transitive, then @{term"i\<in>j"} implies @{term"i\<subseteq>j"}!
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   129
  See @{text"Ord_succ_subsetI}*)
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   130
lemma succ_subsetI: "[| i\<in>j;  i\<subseteq>j |] ==> succ(i)\<subseteq>j"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   131
by (unfold succ_def, blast)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   132
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   133
lemma succ_subsetE:
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   134
    "[| succ(i) \<subseteq> j;  [| i\<in>j;  i\<subseteq>j |] ==> P |] ==> P"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   135
by (unfold succ_def, blast)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   136
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   137
lemma succ_subset_iff: "succ(a) \<subseteq> B \<longleftrightarrow> (a \<subseteq> B & a \<in> B)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   138
by (unfold succ_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   139
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   140
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   141
subsection{*Binary Intersection*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   142
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   143
(** Intersection is the greatest lower bound of two sets **)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   144
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   145
lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A & C \<subseteq> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   146
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   147
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   148
lemma Int_lower1: "A \<inter> B \<subseteq> A"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   149
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   150
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   151
lemma Int_lower2: "A \<inter> B \<subseteq> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   152
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   153
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   154
lemma Int_greatest: "[| C\<subseteq>A;  C\<subseteq>B |] ==> C \<subseteq> A \<inter> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   155
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   156
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   157
lemma Int_cons: "cons(a,B) \<inter> C \<subseteq> cons(a, B \<inter> C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   158
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   159
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   160
lemma Int_absorb [simp]: "A \<inter> A = A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   161
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   162
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   163
lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   164
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   165
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   166
lemma Int_commute: "A \<inter> B = B \<inter> A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   167
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   168
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   169
lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   170
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   171
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   172
lemma Int_assoc: "(A \<inter> B) \<inter> C  =  A \<inter> (B \<inter> C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   173
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   174
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   175
(*Intersection is an AC-operator*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   176
lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   177
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   178
lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   179
  by blast
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   180
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   181
lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   182
  by blast
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   183
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   184
lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   185
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   186
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   187
lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   188
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   189
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   190
lemma subset_Int_iff: "A\<subseteq>B \<longleftrightarrow> A \<inter> B = A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   191
by (blast elim!: equalityE)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   192
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   193
lemma subset_Int_iff2: "A\<subseteq>B \<longleftrightarrow> B \<inter> A = A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   194
by (blast elim!: equalityE)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   195
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   196
lemma Int_Diff_eq: "C\<subseteq>A ==> (A-B) \<inter> C = C-B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   197
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   198
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14046
diff changeset
   199
lemma Int_cons_left:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   200
     "cons(a,A) \<inter> B = (if a \<in> B then cons(a, A \<inter> B) else A \<inter> B)"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14046
diff changeset
   201
by auto
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14046
diff changeset
   202
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14046
diff changeset
   203
lemma Int_cons_right:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   204
     "A \<inter> cons(a, B) = (if a \<in> A then cons(a, A \<inter> B) else A \<inter> B)"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14046
diff changeset
   205
by auto
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14046
diff changeset
   206
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14071
diff changeset
   207
lemma cons_Int_distrib: "cons(x, A \<inter> B) = cons(x, A) \<inter> cons(x, B)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14071
diff changeset
   208
by auto
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14071
diff changeset
   209
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   210
subsection{*Binary Union*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   211
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   212
(** Union is the least upper bound of two sets *)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   213
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   214
lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C & B \<subseteq> C"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   215
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   216
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   217
lemma Un_upper1: "A \<subseteq> A \<union> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   218
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   219
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   220
lemma Un_upper2: "B \<subseteq> A \<union> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   221
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   222
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   223
lemma Un_least: "[| A\<subseteq>C;  B\<subseteq>C |] ==> A \<union> B \<subseteq> C"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   224
by blast
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   225
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   226
lemma Un_cons: "cons(a,B) \<union> C = cons(a, B \<union> C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   227
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   228
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   229
lemma Un_absorb [simp]: "A \<union> A = A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   230
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   231
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   232
lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   233
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   234
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   235
lemma Un_commute: "A \<union> B = B \<union> A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   236
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   237
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   238
lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   239
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   240
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   241
lemma Un_assoc: "(A \<union> B) \<union> C  =  A \<union> (B \<union> C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   242
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   243
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   244
(*Union is an AC-operator*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   245
lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   246
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   247
lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   248
  by blast
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   249
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   250
lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   251
  by blast
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13919
diff changeset
   252
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   253
lemma Un_Int_distrib: "(A \<inter> B) \<union> C  =  (A \<union> C) \<inter> (B \<union> C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   254
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   255
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   256
lemma subset_Un_iff: "A\<subseteq>B \<longleftrightarrow> A \<union> B = B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   257
by (blast elim!: equalityE)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   258
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   259
lemma subset_Un_iff2: "A\<subseteq>B \<longleftrightarrow> B \<union> A = B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   260
by (blast elim!: equalityE)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   261
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   262
lemma Un_empty [iff]: "(A \<union> B = 0) \<longleftrightarrow> (A = 0 & B = 0)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   263
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   264
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   265
lemma Un_eq_Union: "A \<union> B = \<Union>({A, B})"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   266
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   267
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   268
subsection{*Set Difference*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   269
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   270
lemma Diff_subset: "A-B \<subseteq> A"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   271
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   272
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   273
lemma Diff_contains: "[| C\<subseteq>A;  C \<inter> B = 0 |] ==> C \<subseteq> A-B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   274
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   275
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   276
lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  \<longleftrightarrow>  B\<subseteq>A-C & c \<notin> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   277
by blast
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   278
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   279
lemma Diff_cancel: "A - A = 0"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   280
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   281
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   282
lemma Diff_triv: "A  \<inter> B = 0 ==> A - B = A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   283
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   284
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   285
lemma empty_Diff [simp]: "0 - A = 0"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   286
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   287
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   288
lemma Diff_0 [simp]: "A - 0 = A"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   289
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   290
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   291
lemma Diff_eq_0_iff: "A - B = 0 \<longleftrightarrow> A \<subseteq> B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   292
by (blast elim: equalityE)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   293
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   294
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   295
lemma Diff_cons: "A - cons(a,B) = A - B - {a}"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   296
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   297
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   298
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   299
lemma Diff_cons2: "A - cons(a,B) = A - {a} - B"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   300
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   301
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   302
lemma Diff_disjoint: "A \<inter> (B-A) = 0"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   303
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   304
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   305
lemma Diff_partition: "A\<subseteq>B ==> A \<union> (B-A) = B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   306
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   307
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   308
lemma subset_Un_Diff: "A \<subseteq> B \<union> (A - B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   309
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   310
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   311
lemma double_complement: "[| A\<subseteq>B; B\<subseteq>C |] ==> B-(C-A) = A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   312
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   313
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   314
lemma double_complement_Un: "(A \<union> B) - (B-A) = A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   315
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   316
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   317
lemma Un_Int_crazy:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   318
 "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   319
apply blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   320
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   321
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   322
lemma Diff_Un: "A - (B \<union> C) = (A-B) \<inter> (A-C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   323
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   324
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   325
lemma Diff_Int: "A - (B \<inter> C) = (A-B) \<union> (A-C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   326
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   327
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   328
lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   329
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   330
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   331
lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   332
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   333
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   334
lemma Diff_Int_distrib: "C \<inter> (A-B) = (C \<inter> A) - (C \<inter> B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   335
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   336
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   337
lemma Diff_Int_distrib2: "(A-B) \<inter> C = (A \<inter> C) - (B \<inter> C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   338
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   339
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   340
(*Halmos, Naive Set Theory, page 16.*)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   341
lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C)  \<longleftrightarrow>  C\<subseteq>A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   342
by (blast elim!: equalityE)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   343
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   344
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   345
subsection{*Big Union and Intersection*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   346
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   347
(** Big Union is the least upper bound of a set  **)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   348
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   349
lemma Union_subset_iff: "\<Union>(A) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. x \<subseteq> C)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   350
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   351
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   352
lemma Union_upper: "B\<in>A ==> B \<subseteq> \<Union>(A)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   353
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   354
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   355
lemma Union_least: "[| !!x. x\<in>A ==> x\<subseteq>C |] ==> \<Union>(A) \<subseteq> C"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   356
by blast
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   357
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   358
lemma Union_cons [simp]: "\<Union>(cons(a,B)) = a \<union> \<Union>(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   359
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   360
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   361
lemma Union_Un_distrib: "\<Union>(A \<union> B) = \<Union>(A) \<union> \<Union>(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   362
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   363
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   364
lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>(A) \<inter> \<Union>(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   365
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   366
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   367
lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = 0)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   368
by (blast elim!: equalityE)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   369
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   370
lemma Union_empty_iff: "\<Union>(A) = 0 \<longleftrightarrow> (\<forall>B\<in>A. B=0)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   371
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   372
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   373
lemma Int_Union2: "\<Union>(B) \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14077
diff changeset
   374
by blast
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14077
diff changeset
   375
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   376
(** Big Intersection is the greatest lower bound of a nonempty set **)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   377
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   378
lemma Inter_subset_iff: "A\<noteq>0  ==>  C \<subseteq> \<Inter>(A) \<longleftrightarrow> (\<forall>x\<in>A. C \<subseteq> x)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   379
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   380
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   381
lemma Inter_lower: "B\<in>A ==> \<Inter>(A) \<subseteq> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   382
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   383
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   384
lemma Inter_greatest: "[| A\<noteq>0;  !!x. x\<in>A ==> C\<subseteq>x |] ==> C \<subseteq> \<Inter>(A)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   385
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   386
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   387
(** Intersection of a family of sets  **)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   388
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   389
lemma INT_lower: "x\<in>A ==> (\<Inter>x\<in>A. B(x)) \<subseteq> B(x)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   390
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   391
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   392
lemma INT_greatest: "[| A\<noteq>0;  !!x. x\<in>A ==> C\<subseteq>B(x) |] ==> C \<subseteq> (\<Inter>x\<in>A. B(x))"
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   393
by force
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   394
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   395
lemma Inter_0 [simp]: "\<Inter>(0) = 0"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   396
by (unfold Inter_def, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   397
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   398
lemma Inter_Un_subset:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   399
     "[| z\<in>A; z\<in>B |] ==> \<Inter>(A) \<union> \<Inter>(B) \<subseteq> \<Inter>(A \<inter> B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   400
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   401
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   402
(* A good challenge: Inter is ill-behaved on the empty set *)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   403
lemma Inter_Un_distrib:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   404
     "[| A\<noteq>0;  B\<noteq>0 |] ==> \<Inter>(A \<union> B) = \<Inter>(A) \<inter> \<Inter>(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   405
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   406
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   407
lemma Union_singleton: "\<Union>({b}) = b"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   408
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   409
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   410
lemma Inter_singleton: "\<Inter>({b}) = b"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   411
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   412
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   413
lemma Inter_cons [simp]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   414
     "\<Inter>(cons(a,B)) = (if B=0 then a else a \<inter> \<Inter>(B))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   415
by force
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   416
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   417
subsection{*Unions and Intersections of Families*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   418
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   419
lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) \<longleftrightarrow> A = (\<Union>i\<in>I. A \<inter> B(i))"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   420
by (blast elim!: equalityE)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   421
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   422
lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. B(x) \<subseteq> C)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   423
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   424
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   425
lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   426
by (erule RepFunI [THEN Union_upper])
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   427
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   428
lemma UN_least: "[| !!x. x\<in>A ==> B(x)\<subseteq>C |] ==> (\<Union>x\<in>A. B(x)) \<subseteq> C"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   429
by blast
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   430
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   431
lemma Union_eq_UN: "\<Union>(A) = (\<Union>x\<in>A. x)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   432
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   433
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   434
lemma Inter_eq_INT: "\<Inter>(A) = (\<Inter>x\<in>A. x)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   435
by (unfold Inter_def, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   436
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   437
lemma UN_0 [simp]: "(\<Union>i\<in>0. A(i)) = 0"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   438
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   439
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   440
lemma UN_singleton: "(\<Union>x\<in>A. {x}) = A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   441
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   442
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   443
lemma UN_Un: "(\<Union>i\<in> A \<union> B. C(i)) = (\<Union>i\<in> A. C(i)) \<union> (\<Union>i\<in>B. C(i))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   444
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   445
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   446
lemma INT_Un: "(\<Inter>i\<in>I \<union> J. A(i)) =
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   447
               (if I=0 then \<Inter>j\<in>J. A(j)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   448
                       else if J=0 then \<Inter>i\<in>I. A(i)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   449
                       else ((\<Inter>i\<in>I. A(i)) \<inter>  (\<Inter>j\<in>J. A(j))))"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   450
by (simp, blast intro!: equalityI)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   451
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   452
lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B(y)). C(x)) = (\<Union>y\<in>A. \<Union>x\<in> B(y). C(x))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   453
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   454
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   455
(*Halmos, Naive Set Theory, page 35.*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   456
lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A(i)) = (\<Union>i\<in>I. B \<inter> A(i))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   457
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   458
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   459
lemma Un_INT_distrib: "I\<noteq>0 ==> B \<union> (\<Inter>i\<in>I. A(i)) = (\<Inter>i\<in>I. B \<union> A(i))"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   460
by auto
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   461
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   462
lemma Int_UN_distrib2:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   463
     "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) = (\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   464
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   465
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   466
lemma Un_INT_distrib2: "[| I\<noteq>0;  J\<noteq>0 |] ==>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   467
      (\<Inter>i\<in>I. A(i)) \<union> (\<Inter>j\<in>J. B(j)) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A(i) \<union> B(j))"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   468
by auto
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   469
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   470
lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A=0 then 0 else c)"
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   471
by force
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   472
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   473
lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A=0 then 0 else c)"
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   474
by force
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   475
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   476
lemma UN_RepFun [simp]: "(\<Union>y\<in> RepFun(A,f). B(y)) = (\<Union>x\<in>A. B(f(x)))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   477
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   478
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   479
lemma INT_RepFun [simp]: "(\<Inter>x\<in>RepFun(A,f). B(x))    = (\<Inter>a\<in>A. B(f(a)))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   480
by (auto simp add: Inter_def)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   481
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   482
lemma INT_Union_eq:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   483
     "0 \<notin> A ==> (\<Inter>x\<in> \<Union>(A). B(x)) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B(x))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   484
apply (subgoal_tac "\<forall>x\<in>A. x\<noteq>0")
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   485
 prefer 2 apply blast
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   486
apply (force simp add: Inter_def ball_conj_distrib)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   487
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   488
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   489
lemma INT_UN_eq:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   490
     "(\<forall>x\<in>A. B(x) \<noteq> 0)
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   491
      ==> (\<Inter>z\<in> (\<Union>x\<in>A. B(x)). C(z)) = (\<Inter>x\<in>A. \<Inter>z\<in> B(x). C(z))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   492
apply (subst INT_Union_eq, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   493
apply (simp add: Inter_def)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   494
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   495
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   496
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   497
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   498
    Union of a family of unions **)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   499
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   500
lemma UN_Un_distrib:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   501
     "(\<Union>i\<in>I. A(i) \<union> B(i)) = (\<Union>i\<in>I. A(i))  \<union>  (\<Union>i\<in>I. B(i))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   502
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   503
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   504
lemma INT_Int_distrib:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   505
     "I\<noteq>0 ==> (\<Inter>i\<in>I. A(i) \<inter> B(i)) = (\<Inter>i\<in>I. A(i)) \<inter> (\<Inter>i\<in>I. B(i))"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   506
by (blast elim!: not_emptyE)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   507
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   508
lemma UN_Int_subset:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   509
     "(\<Union>z\<in>I \<inter> J. A(z)) \<subseteq> (\<Union>z\<in>I. A(z)) \<inter> (\<Union>z\<in>J. A(z))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   510
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   511
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   512
(** Devlin, page 12, exercise 5: Complements **)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   513
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   514
lemma Diff_UN: "I\<noteq>0 ==> B - (\<Union>i\<in>I. A(i)) = (\<Inter>i\<in>I. B - A(i))"
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   515
by (blast elim!: not_emptyE)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   516
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   517
lemma Diff_INT: "I\<noteq>0 ==> B - (\<Inter>i\<in>I. A(i)) = (\<Union>i\<in>I. B - A(i))"
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   518
by (blast elim!: not_emptyE)
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   519
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   520
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   521
(** Unions and Intersections with General Sum **)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   522
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   523
(*Not suitable for rewriting: LOOPS!*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   524
lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) \<union> Sigma(B,C)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   525
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   526
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   527
(*Not suitable for rewriting: LOOPS!*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   528
lemma Sigma_cons2: "A * cons(b,B) = A*{b} \<union> A*B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   529
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   530
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   531
lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) \<union> Sigma(A,B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   532
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   533
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   534
lemma Sigma_succ2: "A * succ(B) = A*{B} \<union> A*B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   535
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   536
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   537
lemma SUM_UN_distrib1:
14171
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents: 14095
diff changeset
   538
     "(\<Sigma> x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma> x\<in>C(y). B(x))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   539
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   540
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   541
lemma SUM_UN_distrib2:
14171
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents: 14095
diff changeset
   542
     "(\<Sigma> i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma> i\<in>I. C(i,j))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   543
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   544
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   545
lemma SUM_Un_distrib1:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   546
     "(\<Sigma> i\<in>I \<union> J. C(i)) = (\<Sigma> i\<in>I. C(i)) \<union> (\<Sigma> j\<in>J. C(j))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   547
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   548
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   549
lemma SUM_Un_distrib2:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   550
     "(\<Sigma> i\<in>I. A(i) \<union> B(i)) = (\<Sigma> i\<in>I. A(i)) \<union> (\<Sigma> i\<in>I. B(i))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   551
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   552
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   553
(*First-order version of the above, for rewriting*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   554
lemma prod_Un_distrib2: "I * (A \<union> B) = I*A \<union> I*B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   555
by (rule SUM_Un_distrib2)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   556
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   557
lemma SUM_Int_distrib1:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   558
     "(\<Sigma> i\<in>I \<inter> J. C(i)) = (\<Sigma> i\<in>I. C(i)) \<inter> (\<Sigma> j\<in>J. C(j))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   559
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   560
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   561
lemma SUM_Int_distrib2:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   562
     "(\<Sigma> i\<in>I. A(i) \<inter> B(i)) = (\<Sigma> i\<in>I. A(i)) \<inter> (\<Sigma> i\<in>I. B(i))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   563
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   564
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   565
(*First-order version of the above, for rewriting*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   566
lemma prod_Int_distrib2: "I * (A \<inter> B) = I*A \<inter> I*B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   567
by (rule SUM_Int_distrib2)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   568
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   569
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
14171
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents: 14095
diff changeset
   570
lemma SUM_eq_UN: "(\<Sigma> i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   571
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   572
13544
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   573
lemma times_subset_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   574
     "(A'*B' \<subseteq> A*B) \<longleftrightarrow> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
13544
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   575
by blast
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   576
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   577
lemma Int_Sigma_eq:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   578
     "(\<Sigma> x \<in> A'. B'(x)) \<inter> (\<Sigma> x \<in> A. B(x)) = (\<Sigma> x \<in> A' \<inter> A. B'(x) \<inter> B(x))"
13544
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   579
by blast
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   580
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   581
(** Domain **)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   582
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   583
lemma domain_iff: "a: domain(r) \<longleftrightarrow> (\<exists>y. <a,y>\<in> r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   584
by (unfold domain_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   585
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   586
lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   587
by (unfold domain_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   588
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   589
lemma domainE [elim!]:
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   590
    "[| a \<in> domain(r);  !!y. <a,y>\<in> r ==> P |] ==> P"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   591
by (unfold domain_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   592
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   593
lemma domain_subset: "domain(Sigma(A,B)) \<subseteq> A"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   594
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   595
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   596
lemma domain_of_prod: "b\<in>B ==> domain(A*B) = A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   597
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   598
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   599
lemma domain_0 [simp]: "domain(0) = 0"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   600
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   601
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   602
lemma domain_cons [simp]: "domain(cons(<a,b>,r)) = cons(a, domain(r))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   603
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   604
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   605
lemma domain_Un_eq [simp]: "domain(A \<union> B) = domain(A) \<union> domain(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   606
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   607
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   608
lemma domain_Int_subset: "domain(A \<inter> B) \<subseteq> domain(A) \<inter> domain(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   609
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   610
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   611
lemma domain_Diff_subset: "domain(A) - domain(B) \<subseteq> domain(A - B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   612
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   613
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   614
lemma domain_UN: "domain(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. domain(B(x)))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   615
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   616
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   617
lemma domain_Union: "domain(\<Union>(A)) = (\<Union>x\<in>A. domain(x))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   618
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   619
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   620
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   621
(** Range **)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   622
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   623
lemma rangeI [intro]: "<a,b>\<in> r ==> b \<in> range(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   624
apply (unfold range_def)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   625
apply (erule converseI [THEN domainI])
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   626
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   627
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   628
lemma rangeE [elim!]: "[| b \<in> range(r);  !!x. <x,b>\<in> r ==> P |] ==> P"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   629
by (unfold range_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   630
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   631
lemma range_subset: "range(A*B) \<subseteq> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   632
apply (unfold range_def)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   633
apply (subst converse_prod)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   634
apply (rule domain_subset)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   635
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   636
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   637
lemma range_of_prod: "a\<in>A ==> range(A*B) = B"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   638
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   639
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   640
lemma range_0 [simp]: "range(0) = 0"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   641
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   642
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   643
lemma range_cons [simp]: "range(cons(<a,b>,r)) = cons(b, range(r))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   644
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   645
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   646
lemma range_Un_eq [simp]: "range(A \<union> B) = range(A) \<union> range(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   647
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   648
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   649
lemma range_Int_subset: "range(A \<inter> B) \<subseteq> range(A) \<inter> range(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   650
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   651
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   652
lemma range_Diff_subset: "range(A) - range(B) \<subseteq> range(A - B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   653
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   654
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   655
lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   656
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   657
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   658
lemma range_converse [simp]: "range(converse(r)) = domain(r)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   659
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   660
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   661
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   662
(** Field **)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   663
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   664
lemma fieldI1: "<a,b>\<in> r ==> a \<in> field(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   665
by (unfold field_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   666
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   667
lemma fieldI2: "<a,b>\<in> r ==> b \<in> field(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   668
by (unfold field_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   669
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   670
lemma fieldCI [intro]:
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   671
    "(~ <c,a>\<in>r ==> <a,b>\<in> r) ==> a \<in> field(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   672
apply (unfold field_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   673
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   674
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   675
lemma fieldE [elim!]:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   676
     "[| a \<in> field(r);
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   677
         !!x. <a,x>\<in> r ==> P;
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   678
         !!x. <x,a>\<in> r ==> P        |] ==> P"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   679
by (unfold field_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   680
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   681
lemma field_subset: "field(A*B) \<subseteq> A \<union> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   682
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   683
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   684
lemma domain_subset_field: "domain(r) \<subseteq> field(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   685
apply (unfold field_def)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   686
apply (rule Un_upper1)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   687
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   688
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   689
lemma range_subset_field: "range(r) \<subseteq> field(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   690
apply (unfold field_def)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   691
apply (rule Un_upper2)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   692
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   693
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   694
lemma domain_times_range: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> domain(r)*range(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   695
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   696
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   697
lemma field_times_field: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> field(r)*field(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   698
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   699
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   700
lemma relation_field_times_field: "relation(r) ==> r \<subseteq> field(r)*field(r)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   701
by (simp add: relation_def, blast)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   702
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   703
lemma field_of_prod: "field(A*A) = A"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   704
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   705
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   706
lemma field_0 [simp]: "field(0) = 0"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   707
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   708
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   709
lemma field_cons [simp]: "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   710
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   711
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   712
lemma field_Un_eq [simp]: "field(A \<union> B) = field(A) \<union> field(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   713
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   714
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   715
lemma field_Int_subset: "field(A \<inter> B) \<subseteq> field(A) \<inter> field(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   716
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   717
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   718
lemma field_Diff_subset: "field(A) - field(B) \<subseteq> field(A - B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   719
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   720
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   721
lemma field_converse [simp]: "field(converse(r)) = field(r)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   722
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   723
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   724
(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   725
lemma rel_Union: "(\<forall>x\<in>S. \<exists>A B. x \<subseteq> A*B) ==>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   726
                  \<Union>(S) \<subseteq> domain(\<Union>(S)) * range(\<Union>(S))"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   727
by blast
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   728
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   729
(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   730
lemma rel_Un: "[| r \<subseteq> A*B;  s \<subseteq> C*D |] ==> (r \<union> s) \<subseteq> (A \<union> C) * (B \<union> D)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   731
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   732
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   733
lemma domain_Diff_eq: "[| <a,c> \<in> r; c\<noteq>b |] ==> domain(r-{<a,b>}) = domain(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   734
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   735
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   736
lemma range_Diff_eq: "[| <c,b> \<in> r; c\<noteq>a |] ==> range(r-{<a,b>}) = range(r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   737
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   738
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   739
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   740
subsection{*Image of a Set under a Function or Relation*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   741
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   742
lemma image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. <x,b>\<in>r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   743
by (unfold image_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   744
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   745
lemma image_singleton_iff: "b \<in> r``{a} \<longleftrightarrow> <a,b>\<in>r"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   746
by (rule image_iff [THEN iff_trans], blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   747
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   748
lemma imageI [intro]: "[| <a,b>\<in> r;  a\<in>A |] ==> b \<in> r``A"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   749
by (unfold image_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   750
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   751
lemma imageE [elim!]:
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   752
    "[| b: r``A;  !!x.[| <x,b>\<in> r;  x\<in>A |] ==> P |] ==> P"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   753
by (unfold image_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   754
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   755
lemma image_subset: "r \<subseteq> A*B ==> r``C \<subseteq> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   756
by blast
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   757
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   758
lemma image_0 [simp]: "r``0 = 0"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   759
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   760
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   761
lemma image_Un [simp]: "r``(A \<union> B) = (r``A) \<union> (r``B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   762
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   763
14883
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14171
diff changeset
   764
lemma image_UN: "r `` (\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. r `` B(x))"
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14171
diff changeset
   765
by blast
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14171
diff changeset
   766
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14171
diff changeset
   767
lemma Collect_image_eq:
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14171
diff changeset
   768
     "{z \<in> Sigma(A,B). P(z)} `` C = (\<Union>x \<in> A. {y \<in> B(x). x \<in> C & P(<x,y>)})"
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14171
diff changeset
   769
by blast
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14171
diff changeset
   770
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   771
lemma image_Int_subset: "r``(A \<inter> B) \<subseteq> (r``A) \<inter> (r``B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   772
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   773
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   774
lemma image_Int_square_subset: "(r \<inter> A*A)``B \<subseteq> (r``B) \<inter> A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   775
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   776
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   777
lemma image_Int_square: "B\<subseteq>A ==> (r \<inter> A*A)``B = (r``B) \<inter> A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   778
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   779
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   780
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   781
(*Image laws for special relations*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   782
lemma image_0_left [simp]: "0``A = 0"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   783
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   784
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   785
lemma image_Un_left: "(r \<union> s)``A = (r``A) \<union> (s``A)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   786
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   787
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   788
lemma image_Int_subset_left: "(r \<inter> s)``A \<subseteq> (r``A) \<inter> (s``A)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   789
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   790
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   791
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   792
subsection{*Inverse Image of a Set under a Function or Relation*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   793
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   794
lemma vimage_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   795
    "a \<in> r-``B \<longleftrightarrow> (\<exists>y\<in>B. <a,y>\<in>r)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   796
by (unfold vimage_def image_def converse_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   797
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   798
lemma vimage_singleton_iff: "a \<in> r-``{b} \<longleftrightarrow> <a,b>\<in>r"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   799
by (rule vimage_iff [THEN iff_trans], blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   800
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   801
lemma vimageI [intro]: "[| <a,b>\<in> r;  b\<in>B |] ==> a \<in> r-``B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   802
by (unfold vimage_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   803
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   804
lemma vimageE [elim!]:
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   805
    "[| a: r-``B;  !!x.[| <a,x>\<in> r;  x\<in>B |] ==> P |] ==> P"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   806
apply (unfold vimage_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   807
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   808
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   809
lemma vimage_subset: "r \<subseteq> A*B ==> r-``C \<subseteq> A"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   810
apply (unfold vimage_def)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   811
apply (erule converse_type [THEN image_subset])
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   812
done
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   813
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   814
lemma vimage_0 [simp]: "r-``0 = 0"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   815
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   816
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   817
lemma vimage_Un [simp]: "r-``(A \<union> B) = (r-``A) \<union> (r-``B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   818
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   819
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   820
lemma vimage_Int_subset: "r-``(A \<inter> B) \<subseteq> (r-``A) \<inter> (r-``B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   821
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   822
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   823
(*NOT suitable for rewriting*)
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   824
lemma vimage_eq_UN: "f -``B = (\<Union>y\<in>B. f-``{y})"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   825
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   826
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   827
lemma function_vimage_Int:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   828
     "function(f) ==> f-``(A \<inter> B) = (f-``A)  \<inter>  (f-``B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   829
by (unfold function_def, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   830
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   831
lemma function_vimage_Diff: "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   832
by (unfold function_def, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   833
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   834
lemma function_image_vimage: "function(f) ==> f `` (f-`` A) \<subseteq> A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   835
by (unfold function_def, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   836
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   837
lemma vimage_Int_square_subset: "(r \<inter> A*A)-``B \<subseteq> (r-``B) \<inter> A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   838
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   839
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   840
lemma vimage_Int_square: "B\<subseteq>A ==> (r \<inter> A*A)-``B = (r-``B) \<inter> A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   841
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   842
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   843
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   844
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   845
(*Invese image laws for special relations*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   846
lemma vimage_0_left [simp]: "0-``A = 0"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   847
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   848
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   849
lemma vimage_Un_left: "(r \<union> s)-``A = (r-``A) \<union> (s-``A)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   850
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   851
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   852
lemma vimage_Int_subset_left: "(r \<inter> s)-``A \<subseteq> (r-``A) \<inter> (s-``A)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   853
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   854
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   855
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   856
(** Converse **)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   857
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   858
lemma converse_Un [simp]: "converse(A \<union> B) = converse(A) \<union> converse(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   859
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   860
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   861
lemma converse_Int [simp]: "converse(A \<inter> B) = converse(A) \<inter> converse(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   862
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   863
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   864
lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   865
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   866
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   867
lemma converse_UN [simp]: "converse(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. converse(B(x)))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   868
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   869
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   870
(*Unfolding Inter avoids using excluded middle on A=0*)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   871
lemma converse_INT [simp]:
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13611
diff changeset
   872
     "converse(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. converse(B(x)))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   873
apply (unfold Inter_def, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   874
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   875
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   876
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   877
subsection{*Powerset Operator*}
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   878
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   879
lemma Pow_0 [simp]: "Pow(0) = {0}"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   880
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   881
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   882
lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) \<union> {cons(a,X) . X: Pow(A)}"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   883
apply (rule equalityI, safe)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   884
apply (erule swap)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   885
apply (rule_tac a = "x-{a}" in RepFun_eqI, auto)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   886
done
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   887
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   888
lemma Un_Pow_subset: "Pow(A) \<union> Pow(B) \<subseteq> Pow(A \<union> B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   889
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   890
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   891
lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow(B(x))) \<subseteq> Pow(\<Union>x\<in>A. B(x))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   892
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   893
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   894
lemma subset_Pow_Union: "A \<subseteq> Pow(\<Union>(A))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   895
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   896
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   897
lemma Union_Pow_eq [simp]: "\<Union>(Pow(A)) = A"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   898
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   899
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   900
lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) \<longleftrightarrow> A \<in> Pow(Pow(B))"
14077
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14076
diff changeset
   901
by blast
37c964462747 Conversion of theory UNITY to Isar script
paulson
parents: 14076
diff changeset
   902
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   903
lemma Pow_Int_eq [simp]: "Pow(A \<inter> B) = Pow(A) \<inter> Pow(B)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   904
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   905
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   906
lemma Pow_INT_eq: "A\<noteq>0 ==> Pow(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. Pow(B(x)))"
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   907
by (blast elim!: not_emptyE)
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   908
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   909
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   910
subsection{*RepFun*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   911
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   912
lemma RepFun_subset: "[| !!x. x\<in>A ==> f(x) \<in> B |] ==> {f(x). x\<in>A} \<subseteq> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   913
by blast
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   914
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   915
lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 \<longleftrightarrow> A=0"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   916
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   917
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   918
lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})"
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   919
by force
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   920
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   921
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
   922
subsection{*Collect*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   923
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   924
lemma Collect_subset: "Collect(A,P) \<subseteq> A"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   925
by blast
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 520
diff changeset
   926
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   927
lemma Collect_Un: "Collect(A \<union> B, P) = Collect(A,P) \<union> Collect(B,P)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   928
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   929
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   930
lemma Collect_Int: "Collect(A \<inter> B, P) = Collect(A,P) \<inter> Collect(B,P)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   931
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   932
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   933
lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   934
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   935
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   936
lemma Collect_cons: "{x\<in>cons(a,B). P(x)} =
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
   937
      (if P(a) then cons(a, {x\<in>B. P(x)}) else {x\<in>B. P(x)})"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   938
by (simp, blast)
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   939
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   940
lemma Int_Collect_self_eq: "A \<inter> Collect(A,P) = Collect(A,P)"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   941
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   942
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   943
lemma Collect_Collect_eq [simp]:
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   944
     "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))"
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   945
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   946
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   947
lemma Collect_Int_Collect_eq:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   948
     "Collect(A,P) \<inter> Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   949
by blast
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   950
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13178
diff changeset
   951
lemma Collect_Union_eq [simp]:
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13178
diff changeset
   952
     "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13178
diff changeset
   953
by blast
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13178
diff changeset
   954
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   955
lemma Collect_Int_left: "{x\<in>A. P(x)} \<inter> B = {x \<in> A \<inter> B. P(x)}"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14077
diff changeset
   956
by blast
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14077
diff changeset
   957
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   958
lemma Collect_Int_right: "A \<inter> {x\<in>B. P(x)} = {x \<in> A \<inter> B. P(x)}"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14077
diff changeset
   959
by blast
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14077
diff changeset
   960
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   961
lemma Collect_disj_eq: "{x\<in>A. P(x) | Q(x)} = Collect(A, P) \<union> Collect(A, Q)"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14077
diff changeset
   962
by blast
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14077
diff changeset
   963
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   964
lemma Collect_conj_eq: "{x\<in>A. P(x) & Q(x)} = Collect(A, P) \<inter> Collect(A, Q)"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14077
diff changeset
   965
by blast
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14077
diff changeset
   966
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   967
lemmas subset_SIs = subset_refl cons_subsetI subset_consI
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   968
                    Union_least UN_least Un_least
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   969
                    Inter_greatest Int_greatest RepFun_subset
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   970
                    Un_upper1 Un_upper2 Int_lower1 Int_lower2
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   971
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
   972
ML {*
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35762
diff changeset
   973
val subset_cs =
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35762
diff changeset
   974
  claset_of (@{context}
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
   975
    delrules [@{thm subsetI}, @{thm subsetCE}]
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
   976
    addSIs @{thms subset_SIs}
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
   977
    addIs  [@{thm Union_upper}, @{thm Inter_lower}]
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35762
diff changeset
   978
    addSEs [@{thm cons_subsetE}]);
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 13248
diff changeset
   979
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35762
diff changeset
   980
val ZF_cs = claset_of (@{context} delrules [@{thm equalityI}]);
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   981
*}
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   982
13165
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   983
end
31d020705aff conversion of equalities and WF to Isar
paulson
parents: 2469
diff changeset
   984