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<p & (∀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 "(⋃x. B x) = (⋃x∈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 "(⋃x∈A. B x) = {y. ∃x∈A. y ∈ B x}" by blast lemma "⋃S = (⋃x∈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. B x) = {y. ∀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