(* Title: HOL/HOLCF/IOA/ABP/Lemmas.thy
Author: Olaf Müller
*)
theory Lemmas
imports Main
begin
subsection \<open>Logic\<close>
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 \<open>Sets\<close>
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 \<open>2 Lemmas to add to \<open>set_lemmas\<close>, used also for action handling,
namely for Intersections and the empty list (compatibility of IOA!).\<close>
lemma singleton_set: "(\b.{x. x=f(b)}) = (\b.{f(b)})"
by blast
lemma de_morgan: "((A\B)=False) = ((\A)\(\B))"
by blast
subsection \<open>Lists\<close>
lemma cons_not_nil: "l \ [] \ (\x xs. l = (x#xs))"
by (induct l) simp_all
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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 ist noch experimentell.
|
