Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Boolean_Algebra.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Boolean_Algebra.thy
    Author:     Brian Huffman
*)

section \<open>Boolean Algebras\<close>

theory Boolean_Algebra
  imports Main
begin

locale boolean_algebra = conj: abel_semigroup "(\<^bold>\)" + disj: abel_semigroup "(\<^bold>\)"
  for conj :: "'a \ 'a \ 'a" (infixr "\<^bold>\" 70)
    and disj :: "'a \ 'a \ 'a" (infixr "\<^bold>\" 65) +
  fixes compl :: "'a \ 'a" ("\ _" [81] 80)
    and zero :: "'a"  ("\")
    and one  :: "'a"  ("\")
  assumes conj_disj_distrib: "x \<^bold>\ (y \<^bold>\ z) = (x \<^bold>\ y) \<^bold>\ (x \<^bold>\ z)"
    and disj_conj_distrib: "x \<^bold>\ (y \<^bold>\ z) = (x \<^bold>\ y) \<^bold>\ (x \<^bold>\ z)"
    and conj_one_right: "x \<^bold>\ \ = x"
    and disj_zero_right: "x \<^bold>\ \ = x"
    and conj_cancel_right [simp]: "x \<^bold>\ \ x = \"
    and disj_cancel_right [simp]: "x \<^bold>\ \ x = \"
begin

sublocale conj: semilattice_neutr "(\<^bold>\)" "\"
proof
  show "x \<^bold>\ \ = x" for x
    by (fact conj_one_right)
  show "x \<^bold>\ x = x" for x
  proof -
    have "x \<^bold>\ x = (x \<^bold>\ x) \<^bold>\ \"
      by (simp add: disj_zero_right)
    also have "\ = (x \<^bold>\ x) \<^bold>\ (x \<^bold>\ \ x)"
      by simp
    also have "\ = x \<^bold>\ (x \<^bold>\ \ x)"
      by (simp only: conj_disj_distrib)
    also have "\ = x \<^bold>\ \"
      by simp
    also have "\ = x"
      by (simp add: conj_one_right)
    finally show ?thesis .
  qed
qed

sublocale disj: semilattice_neutr "(\<^bold>\)" "\"
proof
  show "x \<^bold>\ \ = x" for x
    by (fact disj_zero_right)
  show "x \<^bold>\ x = x" for x
  proof -
    have "x \<^bold>\ x = (x \<^bold>\ x) \<^bold>\ \"
      by simp
    also have "\ = (x \<^bold>\ x) \<^bold>\ (x \<^bold>\ \ x)"
      by simp
    also have "\ = x \<^bold>\ (x \<^bold>\ \ x)"
      by (simp only: disj_conj_distrib)
    also have "\ = x \<^bold>\ \"
      by simp
    also have "\ = x"
      by (simp add: disj_zero_right)
    finally show ?thesis .
  qed
qed

subsection \<open>Complement\<close>

lemma complement_unique:
  assumes 1: "a \<^bold>\ x = \"
  assumes 2: "a \<^bold>\ x = \"
  assumes 3: "a \<^bold>\ y = \"
  assumes 4: "a \<^bold>\ y = \"
  shows "x = y"
proof -
  from 1 3 have "(a \<^bold>\ x) \<^bold>\ (x \<^bold>\ y) = (a \<^bold>\ y) \<^bold>\ (x \<^bold>\ y)"
    by simp
  then have "(x \<^bold>\ a) \<^bold>\ (x \<^bold>\ y) = (y \<^bold>\ a) \<^bold>\ (y \<^bold>\ x)"
    by (simp add: ac_simps)
  then have "x \<^bold>\ (a \<^bold>\ y) = y \<^bold>\ (a \<^bold>\ x)"
    by (simp add: conj_disj_distrib)
  with 2 4 have "x \<^bold>\ \ = y \<^bold>\ \"
    by simp
  then show "x = y"
    by simp
qed

lemma compl_unique: "x \<^bold>\ y = \ \ x \<^bold>\ y = \ \ \ x = y"
  by (rule complement_unique [OF conj_cancel_right disj_cancel_right])

lemma double_compl [simp]: "\ (\ x) = x"
proof (rule compl_unique)
  show "\ x \<^bold>\ x = \"
    by (simp only: conj_cancel_right conj.commute)
  show "\ x \<^bold>\ x = \"
    by (simp only: disj_cancel_right disj.commute)
qed

lemma compl_eq_compl_iff [simp]: "\ x = \ y \ x = y"
  by (rule inj_eq [OF inj_on_inverseI]) (rule double_compl)

subsection \<open>Conjunction\<close>

lemma conj_zero_right [simp]: "x \<^bold>\ \ = \"
  using conj.left_idem conj_cancel_right by fastforce

lemma compl_one [simp]: "\ \ = \"
  by (rule compl_unique [OF conj_zero_right disj_zero_right])

lemma conj_zero_left [simp]: "\ \<^bold>\ x = \"
  by (subst conj.commute) (rule conj_zero_right)

lemma conj_cancel_left [simp]: "\ x \<^bold>\ x = \"
  by (subst conj.commute) (rule conj_cancel_right)

lemma conj_disj_distrib2: "(y \<^bold>\ z) \<^bold>\ x = (y \<^bold>\ x) \<^bold>\ (z \<^bold>\ x)"
  by (simp only: conj.commute conj_disj_distrib)

lemmas conj_disj_distribs = conj_disj_distrib conj_disj_distrib2

lemma conj_assoc: "(x \<^bold>\ y) \<^bold>\ z = x \<^bold>\ (y \<^bold>\ z)"
  by (fact ac_simps)

lemma conj_commute: "x \<^bold>\ y = y \<^bold>\ x"
  by (fact ac_simps)

lemmas conj_left_commute = conj.left_commute
lemmas conj_ac = conj.assoc conj.commute conj.left_commute

lemma conj_one_left: "\ \<^bold>\ x = x"
  by (fact conj.left_neutral)

lemma conj_left_absorb: "x \<^bold>\ (x \<^bold>\ y) = x \<^bold>\ y"
  by (fact conj.left_idem)

lemma conj_absorb: "x \<^bold>\ x = x"
  by (fact conj.idem)

subsection \<open>Disjunction\<close>

interpretation dual: boolean_algebra "(\<^bold>\)" "(\<^bold>\)" compl \ \
  apply standard
       apply (rule disj_conj_distrib)
      apply (rule conj_disj_distrib)
     apply simp_all
  done

lemma compl_zero [simp]: "\ \ = \"
  by (fact dual.compl_one)

lemma disj_one_right [simp]: "x \<^bold>\ \ = \"
  by (fact dual.conj_zero_right)

lemma disj_one_left [simp]: "\ \<^bold>\ x = \"
  by (fact dual.conj_zero_left)

lemma disj_cancel_left [simp]: "\ x \<^bold>\ x = \"
  by (rule dual.conj_cancel_left)

lemma disj_conj_distrib2: "(y \<^bold>\ z) \<^bold>\ x = (y \<^bold>\ x) \<^bold>\ (z \<^bold>\ x)"
  by (rule dual.conj_disj_distrib2)

lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2

lemma disj_assoc: "(x \<^bold>\ y) \<^bold>\ z = x \<^bold>\ (y \<^bold>\ z)"
  by (fact ac_simps)

lemma disj_commute: "x \<^bold>\ y = y \<^bold>\ x"
  by (fact ac_simps)

lemmas disj_left_commute = disj.left_commute

lemmas disj_ac = disj.assoc disj.commute disj.left_commute

lemma disj_zero_left: "\ \<^bold>\ x = x"
  by (fact disj.left_neutral)

lemma disj_left_absorb: "x \<^bold>\ (x \<^bold>\ y) = x \<^bold>\ y"
  by (fact disj.left_idem)

lemma disj_absorb: "x \<^bold>\ x = x"
  by (fact disj.idem)

subsection \<open>De Morgan's Laws\<close>

lemma de_Morgan_conj [simp]: "\ (x \<^bold>\ y) = \ x \<^bold>\ \ y"
proof (rule compl_unique)
  have "(x \<^bold>\ y) \<^bold>\ (\ x \<^bold>\ \ y) = ((x \<^bold>\ y) \<^bold>\ \ x) \<^bold>\ ((x \<^bold>\ y) \<^bold>\ \ y)"
    by (rule conj_disj_distrib)
  also have "\ = (y \<^bold>\ (x \<^bold>\ \ x)) \<^bold>\ (x \<^bold>\ (y \<^bold>\ \ y))"
    by (simp only: conj_ac)
  finally show "(x \<^bold>\ y) \<^bold>\ (\ x \<^bold>\ \ y) = \"
    by (simp only: conj_cancel_right conj_zero_right disj_zero_right)
next
  have "(x \<^bold>\ y) \<^bold>\ (\ x \<^bold>\ \ y) = (x \<^bold>\ (\ x \<^bold>\ \ y)) \<^bold>\ (y \<^bold>\ (\ x \<^bold>\ \ y))"
    by (rule disj_conj_distrib2)
  also have "\ = (\ y \<^bold>\ (x \<^bold>\ \ x)) \<^bold>\ (\ x \<^bold>\ (y \<^bold>\ \ y))"
    by (simp only: disj_ac)
  finally show "(x \<^bold>\ y) \<^bold>\ (\ x \<^bold>\ \ y) = \"
    by (simp only: disj_cancel_right disj_one_right conj_one_right)
qed

lemma de_Morgan_disj [simp]: "\ (x \<^bold>\ y) = \ x \<^bold>\ \ y"
  using dual.boolean_algebra_axioms by (rule boolean_algebra.de_Morgan_conj)

subsection \<open>Symmetric Difference\<close>

definition xor :: "'a \ 'a \ 'a" (infixr "\" 65)
  where "x \ y = (x \<^bold>\ \ y) \<^bold>\ (\ x \<^bold>\ y)"

sublocale xor: comm_monoid xor \<zero>
proof
  fix x y z :: 'a
  let ?t = "(x \<^bold>\ y \<^bold>\ z) \<^bold>\ (x \<^bold>\ \ y \<^bold>\ \ z) \<^bold>\ (\ x \<^bold>\ y \<^bold>\ \ z) \<^bold>\ (\ x \<^bold>\ \ y \<^bold>\ z)"
  have "?t \<^bold>\ (z \<^bold>\ x \<^bold>\ \ x) \<^bold>\ (z \<^bold>\ y \<^bold>\ \ y) = ?t \<^bold>\ (x \<^bold>\ y \<^bold>\ \ y) \<^bold>\ (x \<^bold>\ z \<^bold>\ \ z)"
    by (simp only: conj_cancel_right conj_zero_right)
  then show "(x \ y) \ z = x \ (y \ z)"
    by (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
      (simp only: conj_disj_distribs conj_ac disj_ac)
  show "x \ y = y \ x"
    by (simp only: xor_def conj_commute disj_commute)
  show "x \ \ = x"
    by (simp add: xor_def)
qed

lemmas xor_assoc = xor.assoc
lemmas xor_commute = xor.commute
lemmas xor_left_commute = xor.left_commute

lemmas xor_ac = xor.assoc xor.commute xor.left_commute

lemma xor_def2: "x \ y = (x \<^bold>\ y) \<^bold>\ (\ x \<^bold>\ \ y)"
  using conj.commute conj_disj_distrib2 disj.commute xor_def by auto

lemma xor_zero_right [simp]: "x \ \ = x"
  by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)

lemma xor_zero_left [simp]: "\ \ x = x"
  by (subst xor_commute) (rule xor_zero_right)

lemma xor_one_right [simp]: "x \ \ = \ x"
  by (simp only: xor_def compl_one conj_zero_right conj_one_right disj_zero_left)

lemma xor_one_left [simp]: "\ \ x = \ x"
  by (subst xor_commute) (rule xor_one_right)

lemma xor_self [simp]: "x \ x = \"
  by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right)

lemma xor_left_self [simp]: "x \ (x \ y) = y"
  by (simp only: xor_assoc [symmetric] xor_self xor_zero_left)

lemma xor_compl_left [simp]: "\ x \ y = \ (x \ y)"
  by (metis xor_assoc xor_one_left)

lemma xor_compl_right [simp]: "x \ \ y = \ (x \ y)"
  using xor_commute xor_compl_left by auto

lemma xor_cancel_right: "x \ \ x = \"
  by (simp only: xor_compl_right xor_self compl_zero)

lemma xor_cancel_left: "\ x \ x = \"
  by (simp only: xor_compl_left xor_self compl_zero)

lemma conj_xor_distrib: "x \<^bold>\ (y \ z) = (x \<^bold>\ y) \ (x \<^bold>\ z)"
proof -
  have *: "(x \<^bold>\ y \<^bold>\ \ z) \<^bold>\ (x \<^bold>\ \ y \<^bold>\ z) =
        (y \<^bold>\<sqinter> x \<^bold>\<sqinter> \<sim> x) \<^bold>\<squnion> (z \<^bold>\<sqinter> x \<^bold>\<sqinter> \<sim> x) \<^bold>\<squnion> (x \<^bold>\<sqinter> y \<^bold>\<sqinter> \<sim> z) \<^bold>\<squnion> (x \<^bold>\<sqinter> \<sim> y \<^bold>\<sqinter> z)"
    by (simp only: conj_cancel_right conj_zero_right disj_zero_left)
  then show "x \<^bold>\ (y \ z) = (x \<^bold>\ y) \ (x \<^bold>\ z)"
    by (simp (no_asm_use) only:
        xor_def de_Morgan_disj de_Morgan_conj double_compl
        conj_disj_distribs conj_ac disj_ac)
qed

lemma conj_xor_distrib2: "(y \ z) \<^bold>\ x = (y \<^bold>\ x) \ (z \<^bold>\ x)"
  by (simp add: conj.commute conj_xor_distrib)

lemmas conj_xor_distribs = conj_xor_distrib conj_xor_distrib2

end

end

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.