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


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 28.9.2014 mit Größe 18 kB

Quelle Bool_Discrete.thy Sprache: Isabelle

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

section \<open>Discrete cpo instance for booleans\<close>

theory Bool_Discrete
imports HOLCF
begin

text \<open>Discrete cpo instance for \<^typ>\<open>bool\<close>.\<close>

instantiation bool :: discrete_cpo
begin

definition below_bool_def:
  "(x::bool) \ y \ x = y"

instance proof
qed (rule below_bool_def)

end

text \<open>
  TODO: implement a command to automate discrete predomain instances.
\<close>

instantiation bool :: predomain
begin

definition
  "(liftemb :: bool u \ udom u) \ liftemb oo u_map\(\ x. Discr x)"

definition
  "(liftprj :: udom u \ bool u) \ u_map\(\ y. undiscr y) oo liftprj"

definition
  "liftdefl \ (\(t::bool itself). LIFTDEFL(bool discr))"

instance proof
  show "ep_pair liftemb (liftprj :: udom u \ bool u)"
    unfolding liftemb_bool_def liftprj_bool_def
    apply (rule ep_pair_comp)
    apply (rule ep_pair_u_map)
    apply (simp add: ep_pair.intro)
    apply (rule predomain_ep)
    done
  show "cast\LIFTDEFL(bool) = liftemb oo (liftprj :: udom u \ bool u)"
    unfolding liftemb_bool_def liftprj_bool_def liftdefl_bool_def
    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
    apply (simp add: ID_def [symmetric] u_map_ID)
    done
qed

end

lemma cont2cont_if [simp, cont2cont]:
  assumes b: "cont b" and f: "cont f" and g: "cont g"
  shows "cont (\x. if b x then f x else g x)"
by (rule cont_apply [OF b cont_discrete_cpo], simp add: f g)

lemma cont2cont_eq [simp, cont2cont]:
  fixes f g :: "'a::cpo \ 'b::discrete_cpo"
  assumes f: "cont f" and g: "cont g"
  shows "cont (\x. f x = g x)"
apply (rule cont_apply [OF f cont_discrete_cpo])
apply (rule cont_apply [OF g cont_discrete_cpo])
apply (rule cont_const)
done

end

quality96%

¤ Dauer der Verarbeitung: 0.0 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.