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
  notation? Here the latter disambiguates.›


text‹
  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