theory Examples
imports Complex_Main
begin
declare [[eta_contract = false]]
text ‹ membership, intersection›
text ‹ difference and empty set›
text ‹ complement, union and universal set›
lemma "(x ∈ A ∩ B) = (x ∈ A ∧ x ∈ B)"
by blast
text ‹ @{thm[display] IntI[no_vars]}
\rulename {IntI}
@{thm[display] IntD1[no_vars]}
\rulename {IntD1}
@{thm[display] IntD2[no_vars]}
\rulename {IntD2}
›
lemma "(x ∈ -A) = (x ∉ A)"
by blast
text ‹ @{thm[display] Compl_iff[no_vars]}
\rulename {Compl_iff}
›
lemma "- (A ∪ B) = -A ∩ -B"
by blast
text ‹ @{thm[display] Compl_Un[no_vars]}
\rulename {Compl_Un}
›
lemma "A-A = {}"
by blast
text ‹ @{thm[display] Diff_disjoint[no_vars]}
\rulename {Diff_disjoint}
›
lemma "A ∪ -A = UNIV"
by blast
text ‹ @{thm[display] Compl_partition[no_vars]}
\rulename {Compl_partition}
›
text ‹ subset relation›
text ‹ @{thm[display] subsetI[no_vars]}
\rulename {subsetI}
@{thm[display] subsetD[no_vars]}
\rulename {subsetD}
›
lemma "((A ∪ B) ⊆ C) = (A ⊆ C ∧ B ⊆ C)"
by blast
text ‹ @{thm[display] Un_subset_iff[no_vars]}
\rulename {Un_subset_iff}
›
lemma "(A ⊆ -B) = (B ⊆ -A)"
by blast
lemma "(A <= -B) = (B <= -A)"
oops
text ‹ ASCII version: blast fails because of overloading because it doesn't have to be sets ›
lemma "((A:: 'a set) <= -B) = (B <= -A)"
by blast
text ‹ A type constraint lets it work›
text ‹ An issue here: how do we discuss the distinction between ASCII and symbol notation? Here the latter disambiguates. ›
text ‹ set extensionality
@{thm[display] set_eqI[no_vars]}
\rulename {set_eqI}
@{thm[display] equalityI[no_vars]}
\rulename {equalityI}
@{thm[display] equalityE[no_vars]}
\rulename {equalityE}
›
text ‹ finite sets: insertion and membership relation›
text ‹ finite set notation›
lemma "insert x A = {x} ∪ A"
by blast
text ‹ @{thm[display] insert_is_Un[no_vars]}
\rulename {insert_is_Un}
›
lemma "{a,b} ∪ {c,d} = {a,b,c,d}"
by blast
lemma "{a,b} ∩ {b,c} = {b}"
apply auto
oops
text ‹ fails because it isn't valid›
lemma "{a,b} ∩ {b,c} = (if a=c then {a,b} else {b})"
apply simp
by blast
text ‹ or just force or auto. blast alone can't handle the if-then-else›
text ‹ next: some comprehension examples›
lemma "(a ∈ {z. P z}) = P a"
by blast
text ‹ @{thm[display] mem_Collect_eq[no_vars]}
\rulename {mem_Collect_eq}
›
lemma "{x. x ∈ A} = A"
by blast
text ‹ @{thm[display] Collect_mem_eq[no_vars]}
\rulename {Collect_mem_eq}
›
lemma "{x. P x ∨ x ∈ A} = {x. P x} ∪ A"
by blast
lemma "{x. P x ⟶ Q x} = -{x. P x} ∪ {x. Q x}"
by blast
definition prime ::
"nat set" where
"prime == {p. 1∀
m. m dvd p
⟶ m=1
∨ m=p)}"
lemma "{p*q | p q. p∈ prime ∧ q∈ prime} =
{z. ∃ p q. z = p*q ∧ p∈ prime ∧ q∈ prime}"
by (rule refl)
text ‹ binders›
text ‹ bounded quantifiers›
lemma "(∃ x∈ A. P x) = (∃ x. x∈ A ∧ P x)"
by blast
text ‹ @{thm[display] bexI[no_vars]}
\rulename {bexI}
›
text ‹ @{thm[display] bexE[no_vars]}
\rulename {bexE}
›
lemma "(∀ x∈ A. P x) = (∀ x. x∈ A ⟶ P x)"
by blast
text ‹ @{thm[display] ballI[no_vars]}
\rulename {ballI}
›
text ‹ @{thm[display] bspec[no_vars]}
\rulename {bspec}
›
text ‹ indexed unions and variations›
lemma "(∪ ∪ ∈ UNIV. B x)"
by blast
text ‹ @{thm[display] UN_iff[no_vars]}
\rulename {UN_iff}
›
text ‹ @{thm[display] Union_iff[no_vars]}
\rulename {Union_iff}
›
lemma "(∪ ∈ A. B x) = {y. ∃ x∈ A. y ∈ B x}"
by blast
lemma "∪ ∪ ∈ S. x)"
by blast
text ‹ @{thm[display] UN_I[no_vars]}
\rulename {UN_I}
›
text ‹ @{thm[display] UN_E[no_vars]}
\rulename {UN_E}
›
text ‹ indexed intersections›
lemma "(∩ ∀ x. y ∈ B x}"
by blast
text ‹ @{thm[display] INT_iff[no_vars]}
\rulename {INT_iff}
›
text ‹ @{thm[display] Inter_iff[no_vars]}
\rulename {Inter_iff}
›
text ‹ mention also card, Pow, etc.›
text ‹ @{thm[display] card_Un_Int[no_vars]}
\rulename {card_Un_Int}
@{thm[display] card_Pow[no_vars]}
\rulename {card_Pow}
@{thm[display] n_subsets[no_vars]}
\rulename {n_subsets}
›
end
Messung V0.5 in Prozent C=49 H=100 G=78
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
