Quelle  Char_Discrete.thy   Sprache: Isabelle

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

section ‹Discrete cpo instance for 8-bit char type›

theory Char_Discrete
imports HOLCF
begin

subsection ‹Discrete cpo instance for 🍋‹char›.›

instantiation char :: discrete_cpo
begin

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

instance proof
qed (rule below_char_def)

end

text ‹
  TODO: implement a command to automate discrete predomain instances.
›

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