Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Quickcheck_Examples/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 4 kB

Quelle Quickcheck_Lattice_Examples.thy Sprache: 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>

unbundle lattice_syntax

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)

unbundle no lattice_syntax

end

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.