section‹Extending FOL by a modified version of HOL set theory›
theory Set imports FOL begin
declare [[eta_contract]]
typedecl 'a set instance set :: ("term") "term" ..
subsection‹Set comprehension and membership›
axiomatization Collect :: "['a ==> o] ==> 'a set" and mem :: "['a, 'a set] ==> o" (infixl‹:› 50) where mem_Collect_iff: "(a : Collect(P)) ⟷ P(a)" and set_extension: "A = B ⟷ (ALL x. x:A ⟷ x:B)"
lemma subset_refl: "A <= A" by (blast intro: subsetI)
lemma subset_trans: "[A <= B; B <= C]==> A <= C" by (blast intro: subsetI dest: subsetD)
subsection‹Rules for equality›
(*Anti-symmetry of the subset relation*) lemma subset_antisym: "[A <= B; B <= A]==> A = B" by (blast intro: set_ext dest: subsetD)
lemmas equalityI = subset_antisym
(* Equality rules from ZF set theory -- are they appropriate here? *) lemma equalityD1: "A = B ==> A<=B" and equalityD2: "A = B ==> B<=A" by (simp_all add: subset_refl)
lemma equalityE: "[A = B; [A <= B; B <= A]==> P]==> P" by (simp add: subset_refl)
lemma UnI1: "c:A ==> c : A Un B" and UnI2: "c:B ==> c : A Un B" unfolding Un_def by (blast intro: CollectI)+
(*Classical introduction rule: no commitment to A vs B*) lemma UnCI: "(¬c:B ==> c:A) ==> c : A Un B" by (blast intro: UnI1 UnI2)
lemma UnE: "[c : A Un B; c:A ==> P; c:B ==> P]==> P" unfolding Un_def by (blast dest: CollectD)
subsection‹Rules for small intersection›
lemma IntI: "[c:A; c:B]==> c : A Int B" unfolding Int_def by (blast intro: CollectI)
lemma IntD1: "c : A Int B ==> c:A" and IntD2: "c : A Int B ==> c:B" unfolding Int_def by (blast dest: CollectD)+
lemma IntE: "[c : A Int B; [c:A; c:B]==> P]==> P" by (blast dest: IntD1 IntD2)
subsection‹Rules for set complement›
lemma ComplI: "(c:A ==> False) ==> c : Compl(A)" unfolding Compl_def by (blast intro: CollectI)
(*This form, with negated conclusion, works well with the Classical prover. Negated assumptions behave like formulae on the right side of the notional turnstile...*) lemma ComplD: "c : Compl(A) ==>¬c:A" unfolding Compl_def by (blast dest: CollectD)
lemmas ComplE = ComplD [elim_format]
subsection‹Empty sets›
lemma empty_eq: "{x. False} = {}" by (simp add: empty_def)
lemma emptyD: "a : {} ==> P" unfolding empty_def by (blast dest: CollectD)
lemmas emptyE = emptyD [elim_format]
lemma not_emptyD: assumes"¬ A={}" shows"EX x. x:A" proof - have"¬ (EX x. x:A) ==> A = {}" by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+ with assms show ?thesis by blast qed
subsection‹Singleton sets›
lemma singletonI: "a : {a}" unfolding singleton_def by (blast intro: CollectI)
(*The order of the premises presupposes that A is rigid; b may be flexible*) lemma UN_I: "[a:A; b: B(a)]==> b: (UN x:A. B(x))" unfolding UNION_def by (blast intro: bexI CollectI)
(*The order of the premises presupposes that C is rigid; A may be flexible*) lemma UnionI: "[X:C; A:X]==> A : Union(C)" unfolding Union_def by (blast intro: UN_I)
lemma InterI: "(∧X. X:C ==> A:X) ==> A : Inter(C)" unfolding Inter_def by (blast intro: INT_I)
(*A "destruct" rule -- every X in C contains A as an element, but A:X can hold when X:C does not! This rule is analogous to "spec". *) lemma InterD: "[A : Inter(C); X:C]==> A:X" unfolding Inter_def by (blast dest: INT_D)
(*"Classical" elimination rule -- does not require proving X:C *) lemma InterE: "[A : Inter(C); A:X ==> R; ¬ X:C ==> R]==> R" unfolding Inter_def by (blast elim: INT_E)
section‹Derived rules involving subsets; Union and Intersection as lattice operations›
subsection‹Big Union -- least upper bound of a set›
lemma Union_upper: "B:A ==> B <= Union(A)" by (blast intro: subsetI UnionI)
lemma Un_mono: "[A <= C; B <= D]==> A Un B <= C Un D" by blast
lemma Int_mono: "[A <= C; B <= D]==> A Int B <= C Int D" by blast
lemma Compl_anti_mono: "A <= B ==> Compl(B) <= Compl(A)" by blast
end
Messung V0.5 in Prozent
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.2Bemerkung:
(vorverarbeitet am 2026-04-26)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
