Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
    Author:     Lukas Bulwahn
    Copyright   2010 TU Muenchen
*)

theory Quickcheck_Lattice_Examples
imports Main
begin

declare [[quickcheck_finite_type_size=5]]

text \<open>We show how other default types help to find counterexamples to propositions if
  the standard default type \<^typ>\<open>int\<close> is insufficient.\<close>

notation
  less_eq  (infix "\" 50) and
  less  (infix "\" 50) and
  top ("\") and
  bot ("\") and
  inf (infixl "\" 70) and
  sup (infixl "\" 65)

declare [[quickcheck_narrowing_active = false, quickcheck_timeout = 3600]]

subsection \<open>Distributive lattices\<close>

lemma sup_inf_distrib2:
"((y :: 'a :: distrib_lattice) \ z) \ x = (y \ x) \ (z \ x)"
  quickcheck[expect = no_counterexample]
by(simp add: inf_sup_aci sup_inf_distrib1)

lemma sup_inf_distrib2_1:
"((y :: 'a :: lattice) \ z) \ x = (y \ x) \ (z \ x)"
  quickcheck[expect = counterexample]
  oops

lemma sup_inf_distrib2_2:
"((y :: 'a :: distrib_lattice) \ z') \ x = (y \ x) \ (z \ x)"
  quickcheck[expect = counterexample]
  oops

lemma inf_sup_distrib1_1:
"(x :: 'a :: distrib_lattice) \ (y \ z) = (x \ y) \ (x' \ z)"
  quickcheck[expect = counterexample]
  oops

lemma inf_sup_distrib2_1:
"((y :: 'a :: distrib_lattice) \ z) \ x = (y \ x) \ (y \ x)"
  quickcheck[expect = counterexample]
  oops

subsection \<open>Bounded lattices\<close>

lemma inf_bot_left [simp]:
  "\ \ (x :: 'a :: bounded_lattice_bot) = \"
  quickcheck[expect = no_counterexample]
  by (rule inf_absorb1) simp

lemma inf_bot_left_1:
  "\ \ (x :: 'a :: bounded_lattice_bot) = x"
  quickcheck[expect = counterexample]
  oops

lemma inf_bot_left_2:
  "y \ (x :: 'a :: bounded_lattice_bot) = \"
  quickcheck[expect = counterexample]
  oops

lemma inf_bot_left_3:
  "x \ \ ==> y \ (x :: 'a :: bounded_lattice_bot) \ \"
  quickcheck[expect = counterexample]
  oops

lemma inf_bot_right [simp]:
  "(x :: 'a :: bounded_lattice_bot) \ \ = \"
  quickcheck[expect = no_counterexample]
  by (rule inf_absorb2) simp

lemma inf_bot_right_1:
  "x \ \ ==> (x :: 'a :: bounded_lattice_bot) \ \ = y"
  quickcheck[expect = counterexample]
  oops

lemma inf_bot_right_2:
  "(x :: 'a :: bounded_lattice_bot) \ \ ~= \"
  quickcheck[expect = counterexample]
  oops

lemma sup_bot_right [simp]:
  "(x :: 'a :: bounded_lattice_bot) \ \ = \"
  quickcheck[expect = counterexample]
  oops

lemma sup_bot_left [simp]:
  "\ \ (x :: 'a :: bounded_lattice_bot) = x"
  quickcheck[expect = no_counterexample]
  by (rule sup_absorb2) simp

lemma sup_bot_right_2 [simp]:
  "(x :: 'a :: bounded_lattice_bot) \ \ = x"
  quickcheck[expect = no_counterexample]
  by (rule sup_absorb1) simp

lemma sup_eq_bot_iff [simp]:
  "(x :: 'a :: bounded_lattice_bot) \ y = \ \ x = \ \ y = \"
  quickcheck[expect = no_counterexample]
  by (simp add: eq_iff)

lemma sup_top_left [simp]:
  "\ \ (x :: 'a :: bounded_lattice_top) = \"
  quickcheck[expect = no_counterexample]
  by (rule sup_absorb1) simp

lemma sup_top_right [simp]:
  "(x :: 'a :: bounded_lattice_top) \ \ = \"
  quickcheck[expect = no_counterexample]
  by (rule sup_absorb2) simp

lemma inf_top_left [simp]:
  "\ \ x = (x :: 'a :: bounded_lattice_top)"
  quickcheck[expect = no_counterexample]
  by (rule inf_absorb2) simp

lemma inf_top_right [simp]:
  "x \ \ = (x :: 'a :: bounded_lattice_top)"
  quickcheck[expect = no_counterexample]
  by (rule inf_absorb1) simp

lemma inf_eq_top_iff [simp]:
  "(x :: 'a :: bounded_lattice_top) \ y = \ \ x = \ \ y = \"
  quickcheck[expect = no_counterexample]
  by (simp add: eq_iff)

no_notation
  less_eq  (infix "\" 50) and
  less (infix "\" 50) and
  inf  (infixl "\" 70) and
  sup  (infixl "\" 65) and
  top ("\") and
  bot ("\")

end

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.