Quelle Char_Discrete.thy Sprache: Isabelle

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

section \<open>Discrete cpo instance for 8-bit char type\<close>

theory Char_Discrete
imports HOLCF
begin

subsection \<open>Discrete cpo instance for \<^typ>\<open>char\<close>.\<close>

instantiation char :: discrete_cpo
begin

definition below_char_def:
  "(x::char) \ y \ x = y"

instance proof
qed (rule below_char_def)

end

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

instantiation char :: predomain
begin

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

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

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

instance proof
  show "ep_pair liftemb (liftprj :: udom u \ char u)"
    unfolding liftemb_char_def liftprj_char_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(char) = liftemb oo (liftprj :: udom u \ char u)"
    unfolding liftemb_char_def liftprj_char_def liftdefl_char_def
    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
    apply (simp add: ID_def [symmetric] u_map_ID)
    done
qed

end

end

quality100%

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.