Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Bool_Discrete.thy Sprache: Isabelle

Original von: 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

¤ 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.