17456

1 
(* Title: CCL/Set.thy

0

2 
ID: $Id$


3 
*)


4 

17456

5 
header {* Extending FOL by a modified version of HOL set theory *}


6 


7 
theory Set


8 
imports FOL


9 
begin

0

10 

3935

11 
global


12 

17456

13 
typedecl 'a set


14 
arities set :: ("term") "term"

0

15 


16 
consts


17 
Collect :: "['a => o] => 'a set" (*comprehension*)


18 
Compl :: "('a set) => 'a set" (*complement*)


19 
Int :: "['a set, 'a set] => 'a set" (infixl 70)


20 
Un :: "['a set, 'a set] => 'a set" (infixl 65)

17456

21 
Union :: "(('a set)set) => 'a set" (*...of a set*)


22 
Inter :: "(('a set)set) => 'a set" (*...of a set*)


23 
UNION :: "['a set, 'a => 'b set] => 'b set" (*general*)


24 
INTER :: "['a set, 'a => 'b set] => 'b set" (*general*)


25 
Ball :: "['a set, 'a => o] => o" (*bounded quants*)


26 
Bex :: "['a set, 'a => o] => o" (*bounded quants*)

0

27 
mono :: "['a set => 'b set] => o" (*monotonicity*)


28 
":" :: "['a, 'a set] => o" (infixl 50) (*membership*)


29 
"<=" :: "['a set, 'a set] => o" (infixl 50)


30 
singleton :: "'a => 'a set" ("{_}")


31 
empty :: "'a set" ("{}")


32 
"oo" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) (*composition*)


33 

3935

34 
syntax

0

35 
"@Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*)


36 


37 
(* Big Intersection / Union *)


38 


39 
"@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10)


40 
"@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(UN _:_./ _)" [0, 0, 0] 10)


41 


42 
(* Bounded Quantifiers *)


43 


44 
"@Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10)


45 
"@Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10)


46 


47 
translations


48 
"{x. P}" == "Collect(%x. P)"


49 
"INT x:A. B" == "INTER(A, %x. B)"


50 
"UN x:A. B" == "UNION(A, %x. B)"


51 
"ALL x:A. P" == "Ball(A, %x. P)"


52 
"EX x:A. P" == "Bex(A, %x. P)"


53 

3935

54 
local

0

55 

17456

56 
axioms


57 
mem_Collect_iff: "(a : {x. P(x)}) <> P(a)"


58 
set_extension: "A=B <> (ALL x. x:A <> x:B)"

0

59 

17456

60 
defs


61 
Ball_def: "Ball(A, P) == ALL x. x:A > P(x)"


62 
Bex_def: "Bex(A, P) == EX x. x:A & P(x)"


63 
mono_def: "mono(f) == (ALL A B. A <= B > f(A) <= f(B))"


64 
subset_def: "A <= B == ALL x:A. x:B"


65 
singleton_def: "{a} == {x. x=a}"


66 
empty_def: "{} == {x. False}"


67 
Un_def: "A Un B == {x. x:A  x:B}"


68 
Int_def: "A Int B == {x. x:A & x:B}"


69 
Compl_def: "Compl(A) == {x. ~x:A}"


70 
INTER_def: "INTER(A, B) == {y. ALL x:A. y: B(x)}"


71 
UNION_def: "UNION(A, B) == {y. EX x:A. y: B(x)}"


72 
Inter_def: "Inter(S) == (INT x:S. x)"


73 
Union_def: "Union(S) == (UN x:S. x)"


74 

20140

75 


76 
lemma CollectI: "[ P(a) ] ==> a : {x. P(x)}"


77 
apply (rule mem_Collect_iff [THEN iffD2])


78 
apply assumption


79 
done


80 


81 
lemma CollectD: "[ a : {x. P(x)} ] ==> P(a)"


82 
apply (erule mem_Collect_iff [THEN iffD1])


83 
done


84 


85 
lemmas CollectE = CollectD [elim_format]


86 


87 
lemma set_ext: "[ !!x. x:A <> x:B ] ==> A = B"


88 
apply (rule set_extension [THEN iffD2])


89 
apply simp


90 
done


91 


92 


93 
subsection {* Bounded quantifiers *}


94 


95 
lemma ballI: "[ !!x. x:A ==> P(x) ] ==> ALL x:A. P(x)"


96 
by (simp add: Ball_def)


97 


98 
lemma bspec: "[ ALL x:A. P(x); x:A ] ==> P(x)"


99 
by (simp add: Ball_def)


100 


101 
lemma ballE: "[ ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q ] ==> Q"


102 
unfolding Ball_def by blast


103 


104 
lemma bexI: "[ P(x); x:A ] ==> EX x:A. P(x)"


105 
unfolding Bex_def by blast


106 


107 
lemma bexCI: "[ EX x:A. ~P(x) ==> P(a); a:A ] ==> EX x:A. P(x)"


108 
unfolding Bex_def by blast


109 


110 
lemma bexE: "[ EX x:A. P(x); !!x. [ x:A; P(x) ] ==> Q ] ==> Q"


111 
unfolding Bex_def by blast


112 


113 
(*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*)


114 
lemma ball_rew: "(ALL x:A. True) <> True"


115 
by (blast intro: ballI)


116 


117 


118 
subsection {* Congruence rules *}


119 


120 
lemma ball_cong:


121 
"[ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==>


122 
(ALL x:A. P(x)) <> (ALL x:A'. P'(x))"


123 
by (blast intro: ballI elim: ballE)


124 


125 
lemma bex_cong:


126 
"[ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==>


127 
(EX x:A. P(x)) <> (EX x:A'. P'(x))"


128 
by (blast intro: bexI elim: bexE)


129 


130 


131 
subsection {* Rules for subsets *}


132 


133 
lemma subsetI: "(!!x. x:A ==> x:B) ==> A <= B"


134 
unfolding subset_def by (blast intro: ballI)


135 


136 
(*Rule in Modus Ponens style*)


137 
lemma subsetD: "[ A <= B; c:A ] ==> c:B"


138 
unfolding subset_def by (blast elim: ballE)


139 


140 
(*Classical elimination rule*)


141 
lemma subsetCE: "[ A <= B; ~(c:A) ==> P; c:B ==> P ] ==> P"


142 
by (blast dest: subsetD)


143 


144 
lemma subset_refl: "A <= A"


145 
by (blast intro: subsetI)


146 


147 
lemma subset_trans: "[ A<=B; B<=C ] ==> A<=C"


148 
by (blast intro: subsetI dest: subsetD)


149 


150 


151 
subsection {* Rules for equality *}


152 


153 
(*Antisymmetry of the subset relation*)


154 
lemma subset_antisym: "[ A <= B; B <= A ] ==> A = B"


155 
by (blast intro: set_ext dest: subsetD)


156 


157 
lemmas equalityI = subset_antisym


158 


159 
(* Equality rules from ZF set theory  are they appropriate here? *)


160 
lemma equalityD1: "A = B ==> A<=B"


161 
and equalityD2: "A = B ==> B<=A"


162 
by (simp_all add: subset_refl)


163 


164 
lemma equalityE: "[ A = B; [ A<=B; B<=A ] ==> P ] ==> P"


165 
by (simp add: subset_refl)


166 


167 
lemma equalityCE:


168 
"[ A = B; [ c:A; c:B ] ==> P; [ ~ c:A; ~ c:B ] ==> P ] ==> P"


169 
by (blast elim: equalityE subsetCE)


170 


171 
lemma trivial_set: "{x. x:A} = A"


172 
by (blast intro: equalityI subsetI CollectI dest: CollectD)


173 


174 


175 
subsection {* Rules for binary union *}


176 


177 
lemma UnI1: "c:A ==> c : A Un B"


178 
and UnI2: "c:B ==> c : A Un B"


179 
unfolding Un_def by (blast intro: CollectI)+


180 


181 
(*Classical introduction rule: no commitment to A vs B*)


182 
lemma UnCI: "(~c:B ==> c:A) ==> c : A Un B"


183 
by (blast intro: UnI1 UnI2)


184 


185 
lemma UnE: "[ c : A Un B; c:A ==> P; c:B ==> P ] ==> P"


186 
unfolding Un_def by (blast dest: CollectD)


187 


188 


189 
subsection {* Rules for small intersection *}


190 


191 
lemma IntI: "[ c:A; c:B ] ==> c : A Int B"


192 
unfolding Int_def by (blast intro: CollectI)


193 


194 
lemma IntD1: "c : A Int B ==> c:A"


195 
and IntD2: "c : A Int B ==> c:B"


196 
unfolding Int_def by (blast dest: CollectD)+


197 


198 
lemma IntE: "[ c : A Int B; [ c:A; c:B ] ==> P ] ==> P"


199 
by (blast dest: IntD1 IntD2)


200 


201 


202 
subsection {* Rules for set complement *}


203 


204 
lemma ComplI: "[ c:A ==> False ] ==> c : Compl(A)"


205 
unfolding Compl_def by (blast intro: CollectI)


206 


207 
(*This form, with negated conclusion, works well with the Classical prover.


208 
Negated assumptions behave like formulae on the right side of the notional


209 
turnstile...*)


210 
lemma ComplD: "[ c : Compl(A) ] ==> ~c:A"


211 
unfolding Compl_def by (blast dest: CollectD)


212 


213 
lemmas ComplE = ComplD [elim_format]


214 


215 


216 
subsection {* Empty sets *}


217 


218 
lemma empty_eq: "{x. False} = {}"


219 
by (simp add: empty_def)


220 


221 
lemma emptyD: "a : {} ==> P"


222 
unfolding empty_def by (blast dest: CollectD)


223 


224 
lemmas emptyE = emptyD [elim_format]


225 


226 
lemma not_emptyD:


227 
assumes "~ A={}"


228 
shows "EX x. x:A"


229 
proof 


230 
have "\<not> (EX x. x:A) \<Longrightarrow> A = {}"


231 
by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+


232 
with prems show ?thesis by blast


233 
qed


234 


235 


236 
subsection {* Singleton sets *}


237 


238 
lemma singletonI: "a : {a}"


239 
unfolding singleton_def by (blast intro: CollectI)


240 


241 
lemma singletonD: "b : {a} ==> b=a"


242 
unfolding singleton_def by (blast dest: CollectD)


243 


244 
lemmas singletonE = singletonD [elim_format]


245 


246 


247 
subsection {* Unions of families *}


248 


249 
(*The order of the premises presupposes that A is rigid; b may be flexible*)


250 
lemma UN_I: "[ a:A; b: B(a) ] ==> b: (UN x:A. B(x))"


251 
unfolding UNION_def by (blast intro: bexI CollectI)


252 


253 
lemma UN_E: "[ b : (UN x:A. B(x)); !!x.[ x:A; b: B(x) ] ==> R ] ==> R"


254 
unfolding UNION_def by (blast dest: CollectD elim: bexE)


255 


256 
lemma UN_cong:


257 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==>


258 
(UN x:A. C(x)) = (UN x:B. D(x))"


259 
by (simp add: UNION_def cong: bex_cong)


260 


261 


262 
subsection {* Intersections of families *}


263 


264 
lemma INT_I: "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"


265 
unfolding INTER_def by (blast intro: CollectI ballI)


266 


267 
lemma INT_D: "[ b : (INT x:A. B(x)); a:A ] ==> b: B(a)"


268 
unfolding INTER_def by (blast dest: CollectD bspec)


269 


270 
(*"Classical" elimination rule  does not require proving X:C *)


271 
lemma INT_E: "[ b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R ] ==> R"


272 
unfolding INTER_def by (blast dest: CollectD bspec)


273 


274 
lemma INT_cong:


275 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==>


276 
(INT x:A. C(x)) = (INT x:B. D(x))"


277 
by (simp add: INTER_def cong: ball_cong)


278 


279 


280 
subsection {* Rules for Unions *}


281 


282 
(*The order of the premises presupposes that C is rigid; A may be flexible*)


283 
lemma UnionI: "[ X:C; A:X ] ==> A : Union(C)"


284 
unfolding Union_def by (blast intro: UN_I)


285 


286 
lemma UnionE: "[ A : Union(C); !!X.[ A:X; X:C ] ==> R ] ==> R"


287 
unfolding Union_def by (blast elim: UN_E)


288 


289 


290 
subsection {* Rules for Inter *}


291 


292 
lemma InterI: "[ !!X. X:C ==> A:X ] ==> A : Inter(C)"


293 
unfolding Inter_def by (blast intro: INT_I)


294 


295 
(*A "destruct" rule  every X in C contains A as an element, but


296 
A:X can hold when X:C does not! This rule is analogous to "spec". *)


297 
lemma InterD: "[ A : Inter(C); X:C ] ==> A:X"


298 
unfolding Inter_def by (blast dest: INT_D)


299 


300 
(*"Classical" elimination rule  does not require proving X:C *)


301 
lemma InterE: "[ A : Inter(C); A:X ==> R; ~ X:C ==> R ] ==> R"


302 
unfolding Inter_def by (blast elim: INT_E)


303 


304 


305 
section {* Derived rules involving subsets; Union and Intersection as lattice operations *}


306 


307 
subsection {* Big Union  least upper bound of a set *}


308 


309 
lemma Union_upper: "B:A ==> B <= Union(A)"


310 
by (blast intro: subsetI UnionI)


311 


312 
lemma Union_least: "[ !!X. X:A ==> X<=C ] ==> Union(A) <= C"


313 
by (blast intro: subsetI dest: subsetD elim: UnionE)


314 


315 


316 
subsection {* Big Intersection  greatest lower bound of a set *}


317 


318 
lemma Inter_lower: "B:A ==> Inter(A) <= B"


319 
by (blast intro: subsetI dest: InterD)


320 


321 
lemma Inter_greatest: "[ !!X. X:A ==> C<=X ] ==> C <= Inter(A)"


322 
by (blast intro: subsetI InterI dest: subsetD)


323 


324 


325 
subsection {* Finite Union  the least upper bound of 2 sets *}


326 


327 
lemma Un_upper1: "A <= A Un B"


328 
by (blast intro: subsetI UnI1)


329 


330 
lemma Un_upper2: "B <= A Un B"


331 
by (blast intro: subsetI UnI2)


332 


333 
lemma Un_least: "[ A<=C; B<=C ] ==> A Un B <= C"


334 
by (blast intro: subsetI elim: UnE dest: subsetD)


335 


336 


337 
subsection {* Finite Intersection  the greatest lower bound of 2 sets *}


338 


339 
lemma Int_lower1: "A Int B <= A"


340 
by (blast intro: subsetI elim: IntE)


341 


342 
lemma Int_lower2: "A Int B <= B"


343 
by (blast intro: subsetI elim: IntE)


344 


345 
lemma Int_greatest: "[ C<=A; C<=B ] ==> C <= A Int B"


346 
by (blast intro: subsetI IntI dest: subsetD)


347 


348 


349 
subsection {* Monotonicity *}


350 


351 
lemma monoI: "[ !!A B. A <= B ==> f(A) <= f(B) ] ==> mono(f)"


352 
unfolding mono_def by blast


353 


354 
lemma monoD: "[ mono(f); A <= B ] ==> f(A) <= f(B)"


355 
unfolding mono_def by blast


356 


357 
lemma mono_Un: "mono(f) ==> f(A) Un f(B) <= f(A Un B)"


358 
by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2)


359 


360 
lemma mono_Int: "mono(f) ==> f(A Int B) <= f(A) Int f(B)"


361 
by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2)


362 


363 


364 
subsection {* Automated reasoning setup *}


365 


366 
lemmas [intro!] = ballI subsetI InterI INT_I CollectI ComplI IntI UnCI singletonI


367 
and [intro] = bexI UnionI UN_I


368 
and [elim!] = bexE UnionE UN_E CollectE ComplE IntE UnE emptyE singletonE


369 
and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE


370 


371 
lemma mem_rews:


372 
"(a : A Un B) <> (a:A  a:B)"


373 
"(a : A Int B) <> (a:A & a:B)"


374 
"(a : Compl(B)) <> (~a:B)"


375 
"(a : {b}) <> (a=b)"


376 
"(a : {}) <> False"


377 
"(a : {x. P(x)}) <> P(a)"


378 
by blast+


379 


380 
lemmas [simp] = trivial_set empty_eq mem_rews


381 
and [cong] = ball_cong bex_cong INT_cong UN_cong


382 


383 


384 
section {* Equalities involving union, intersection, inclusion, etc. *}


385 


386 
subsection {* Binary Intersection *}


387 


388 
lemma Int_absorb: "A Int A = A"


389 
by (blast intro: equalityI)


390 


391 
lemma Int_commute: "A Int B = B Int A"


392 
by (blast intro: equalityI)


393 


394 
lemma Int_assoc: "(A Int B) Int C = A Int (B Int C)"


395 
by (blast intro: equalityI)


396 


397 
lemma Int_Un_distrib: "(A Un B) Int C = (A Int C) Un (B Int C)"


398 
by (blast intro: equalityI)


399 


400 
lemma subset_Int_eq: "(A<=B) <> (A Int B = A)"


401 
by (blast intro: equalityI elim: equalityE)


402 


403 


404 
subsection {* Binary Union *}


405 


406 
lemma Un_absorb: "A Un A = A"


407 
by (blast intro: equalityI)


408 


409 
lemma Un_commute: "A Un B = B Un A"


410 
by (blast intro: equalityI)


411 


412 
lemma Un_assoc: "(A Un B) Un C = A Un (B Un C)"


413 
by (blast intro: equalityI)


414 


415 
lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)"


416 
by (blast intro: equalityI)


417 


418 
lemma Un_Int_crazy:


419 
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"


420 
by (blast intro: equalityI)


421 


422 
lemma subset_Un_eq: "(A<=B) <> (A Un B = B)"


423 
by (blast intro: equalityI elim: equalityE)


424 


425 


426 
subsection {* Simple properties of @{text "Compl"}  complement of a set *}


427 


428 
lemma Compl_disjoint: "A Int Compl(A) = {x. False}"


429 
by (blast intro: equalityI)


430 


431 
lemma Compl_partition: "A Un Compl(A) = {x. True}"


432 
by (blast intro: equalityI)


433 


434 
lemma double_complement: "Compl(Compl(A)) = A"


435 
by (blast intro: equalityI)


436 


437 
lemma Compl_Un: "Compl(A Un B) = Compl(A) Int Compl(B)"


438 
by (blast intro: equalityI)


439 


440 
lemma Compl_Int: "Compl(A Int B) = Compl(A) Un Compl(B)"


441 
by (blast intro: equalityI)


442 


443 
lemma Compl_UN: "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"


444 
by (blast intro: equalityI)


445 


446 
lemma Compl_INT: "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"


447 
by (blast intro: equalityI)


448 


449 
(*Halmos, Naive Set Theory, page 16.*)


450 
lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) <> (C<=A)"


451 
by (blast intro: equalityI elim: equalityE)


452 


453 


454 
subsection {* Big Union and Intersection *}


455 


456 
lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"


457 
by (blast intro: equalityI)


458 


459 
lemma Union_disjoint:


460 
"(Union(C) Int A = {x. False}) <> (ALL B:C. B Int A = {x. False})"


461 
by (blast intro: equalityI elim: equalityE)


462 


463 
lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)"


464 
by (blast intro: equalityI)


465 


466 


467 
subsection {* Unions and Intersections of Families *}


468 


469 
lemma UN_eq: "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"


470 
by (blast intro: equalityI)


471 


472 
(*Look: it has an EXISTENTIAL quantifier*)


473 
lemma INT_eq: "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"


474 
by (blast intro: equalityI)


475 


476 
lemma Int_Union_image: "A Int Union(B) = (UN C:B. A Int C)"


477 
by (blast intro: equalityI)


478 


479 
lemma Un_Inter_image: "A Un Inter(B) = (INT C:B. A Un C)"


480 
by (blast intro: equalityI)


481 


482 


483 
section {* Monotonicity of various operations *}


484 


485 
lemma Union_mono: "A<=B ==> Union(A) <= Union(B)"


486 
by blast


487 


488 
lemma Inter_anti_mono: "[ B<=A ] ==> Inter(A) <= Inter(B)"


489 
by blast


490 


491 
lemma UN_mono:


492 
"[ A<=B; !!x. x:A ==> f(x)<=g(x) ] ==>


493 
(UN x:A. f(x)) <= (UN x:B. g(x))"


494 
by blast


495 


496 
lemma INT_anti_mono:


497 
"[ B<=A; !!x. x:A ==> f(x)<=g(x) ] ==>


498 
(INT x:A. f(x)) <= (INT x:A. g(x))"


499 
by blast


500 


501 
lemma Un_mono: "[ A<=C; B<=D ] ==> A Un B <= C Un D"


502 
by blast


503 


504 
lemma Int_mono: "[ A<=C; B<=D ] ==> A Int B <= C Int D"


505 
by blast


506 


507 
lemma Compl_anti_mono: "[ A<=B ] ==> Compl(B) <= Compl(A)"


508 
by blast

0

509 


510 
end
