(* Title: CCL/Set.thy ID: $Id: Set.thy,v 1.5 2005/09/17 15:35:28 wenzelm Exp $ *) header {* Extending FOL by a modified version of HOL set theory *} theory Set imports FOL begin global typedecl 'a set arities set :: ("term") "term" consts Collect :: "['a => o] => 'a set" (*comprehension*) Compl :: "('a set) => 'a set" (*complement*) Int :: "['a set, 'a set] => 'a set" (infixl 70) Un :: "['a set, 'a set] => 'a set" (infixl 65) Union :: "(('a set)set) => 'a set" (*...of a set*) Inter :: "(('a set)set) => 'a set" (*...of a set*) UNION :: "['a set, 'a => 'b set] => 'b set" (*general*) INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) Ball :: "['a set, 'a => o] => o" (*bounded quants*) Bex :: "['a set, 'a => o] => o" (*bounded quants*) mono :: "['a set => 'b set] => o" (*monotonicity*) ":" :: "['a, 'a set] => o" (infixl 50) (*membership*) "<=" :: "['a set, 'a set] => o" (infixl 50) singleton :: "'a => 'a set" ("{_}") empty :: "'a set" ("{}") "oo" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) (*composition*) syntax "@Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*) (* Big Intersection / Union *) "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) "@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(UN _:_./ _)" [0, 0, 0] 10) (* Bounded Quantifiers *) "@Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10) "@Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10) translations "{x. P}" == "Collect(%x. P)" "INT x:A. B" == "INTER(A, %x. B)" "UN x:A. B" == "UNION(A, %x. B)" "ALL x:A. P" == "Ball(A, %x. P)" "EX x:A. P" == "Bex(A, %x. P)" local axioms mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)" set_extension: "A=B <-> (ALL x. x:A <-> x:B)" defs Ball_def: "Ball(A, P) == ALL x. x:A --> P(x)" Bex_def: "Bex(A, P) == EX x. x:A & P(x)" mono_def: "mono(f) == (ALL A B. A <= B --> f(A) <= f(B))" subset_def: "A <= B == ALL x:A. x:B" singleton_def: "{a} == {x. x=a}" empty_def: "{} == {x. False}" Un_def: "A Un B == {x. x:A | x:B}" Int_def: "A Int B == {x. x:A & x:B}" Compl_def: "Compl(A) == {x. ~x:A}" INTER_def: "INTER(A, B) == {y. ALL x:A. y: B(x)}" UNION_def: "UNION(A, B) == {y. EX x:A. y: B(x)}" Inter_def: "Inter(S) == (INT x:S. x)" Union_def: "Union(S) == (UN x:S. x)" ML {* use_legacy_bindings (the_context ()) *} end
theorem CollectI:
P(a) ==> a : Collect(P)
theorem CollectD:
a : Collect(P) ==> P(a)
theorem set_ext:
(!!x. x : A <-> x : B) ==> A = B
theorem ballI:
(!!x. x : A ==> P(x)) ==> Ball(A, P)
theorem bspec:
[| Ball(A, P); x : A |] ==> P(x)
theorem ballE:
[| Ball(A, P); P(x) ==> Q; ¬ x : A ==> Q |] ==> Q
theorem bexI:
[| P(x); x : A |] ==> Bex(A, P)
theorem bexCI:
[| EX x:A. ¬ P(x) ==> P(a); a : A |] ==> Bex(A, P)
theorem bexE:
[| Bex(A, P); !!x. [| x : A; P(x) |] ==> Q |] ==> Q
theorem ball_rew:
(ALL x:A. True) <-> True
theorem ball_cong:
[| A = A'; !!x. x : A' ==> P(x) <-> P'(x) |] ==> Ball(A, P) <-> Ball(A', P')
theorem bex_cong:
[| A = A'; !!x. x : A' ==> P(x) <-> P'(x) |] ==> Bex(A, P) <-> Bex(A', P')
theorem subsetI:
(!!x. x : A ==> x : B) ==> A <= B
theorem subsetD:
[| A <= B; c : A |] ==> c : B
theorem subsetCE:
[| A <= B; ¬ c : A ==> P; c : B ==> P |] ==> P
theorem subset_refl:
A <= A
theorem subset_trans:
[| A <= B; B <= C |] ==> A <= C
theorem subset_antisym:
[| A <= B; B <= A |] ==> A = B
theorem equalityD1:
A = B ==> A <= B
theorem equalityD2:
A = B ==> B <= A
theorem equalityE:
[| A = B; [| A <= B; B <= A |] ==> P |] ==> P
theorem equalityCE:
[| A = B; [| c : A; c : B |] ==> P; [| ¬ c : A; ¬ c : B |] ==> P |] ==> P
theorem setup_induction:
[| p : A; !!z. z : A ==> p = z --> R |] ==> R
theorem trivial_set:
{x. x : A} = A
theorem UnI1:
c : A ==> c : A Un B
theorem UnI2:
c : B ==> c : A Un B
theorem UnCI:
(¬ c : B ==> c : A) ==> c : A Un B
theorem UnE:
[| c : A Un B; c : A ==> P; c : B ==> P |] ==> P
theorem IntI:
[| c : A; c : B |] ==> c : A Int B
theorem IntD1:
c : A Int B ==> c : A
theorem IntD2:
c : A Int B ==> c : B
theorem IntE:
[| c : A Int B; [| c : A; c : B |] ==> P |] ==> P
theorem ComplI:
(c : A ==> False) ==> c : Compl(A)
theorem ComplD:
c : Compl(A) ==> ¬ c : A
theorem empty_eq:
{x. False} = {}
theorem emptyD:
a : {} ==> P
theorem not_emptyD:
A ≠ {} ==> ∃x. x : A
theorem singletonI:
a : {a}
theorem singletonD:
b : {a} ==> b = a
theorem UN_I:
[| a : A; b : B(a) |] ==> b : UNION(A, B)
theorem UN_E:
[| b : UNION(A, B); !!x. [| x : A; b : B(x) |] ==> R |] ==> R
theorem UN_cong:
[| A = B; !!x. x : B ==> C(x) = D(x) |] ==> UNION(A, C) = UNION(B, D)
theorem INT_I:
(!!x. x : A ==> b : B(x)) ==> b : INTER(A, B)
theorem INT_D:
[| b : INTER(A, B); a : A |] ==> b : B(a)
theorem INT_E:
[| b : INTER(A, B); b : B(a) ==> R; ¬ a : A ==> R |] ==> R
theorem INT_cong:
[| A = B; !!x. x : B ==> C(x) = D(x) |] ==> INTER(A, C) = INTER(B, D)
theorem UnionI:
[| X : C; A : X |] ==> A : Union(C)
theorem UnionE:
[| A : Union(C); !!X. [| A : X; X : C |] ==> R |] ==> R
theorem InterI:
(!!X. X : C ==> A : X) ==> A : Inter(C)
theorem InterD:
[| A : Inter(C); X : C |] ==> A : X
theorem InterE:
[| A : Inter(C); A : X ==> R; ¬ X : C ==> R |] ==> R