Theory Lemmas
theory Lemmas
imports Main
begin
subsection ‹Logic›
lemma and_de_morgan_and_absorbe: "(¬(A∧B)) = ((¬A)∧B∨ ¬B)"
by blast
lemma bool_if_impl_or: "(if C then A else B) ⟶ (A∨B)"
by auto
lemma exis_elim: "(∃x. x=P ∧ Q(x)) = Q(P)"
by blast
subsection ‹Sets›
lemma set_lemmas:
"f(x) ∈ (⋃x. {f(x)})"
"f x y ∈ (⋃x y. {f x y})"
"⋀a. (∀x. a ≠ f(x)) ⟹ a ∉ (⋃x. {f(x)})"
"⋀a. (∀x y. a ≠ f x y) ==> a ∉ (⋃x y. {f x y})"
by auto
text ‹2 Lemmas to add to ‹set_lemmas›, used also for action handling,
namely for Intersections and the empty list (compatibility of IOA!).›
lemma singleton_set: "(⋃b.{x. x=f(b)}) = (⋃b.{f(b)})"
by blast
lemma de_morgan: "((A∨B)=False) = ((¬A)∧(¬B))"
by blast
subsection ‹Lists›
lemma cons_not_nil: "l ≠ [] ⟶ (∃x xs. l = (x#xs))"
by (induct l) simp_all
end