Quelle Int_Discrete.thy Sprache: Isabelle

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

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

theory Int_Discrete
imports HOLCF
begin

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

instantiation int :: discrete_cpo
begin

definition below_int_def:
  "(x::int) \ y \ x = y"

instance proof
qed (rule below_int_def)

end

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

instantiation int :: predomain
begin

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

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

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

instance proof
  show "ep_pair liftemb (liftprj :: udom u \ int u)"
    unfolding liftemb_int_def liftprj_int_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(int) = liftemb oo (liftprj :: udom u \ int u)"
    unfolding liftemb_int_def liftprj_int_def liftdefl_int_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.5 Sekunden ¤

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.