Quelle Sfun.thy Sprache: Isabelle

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

section \<open>The Strict Function Type\<close>

theory Sfun
  imports Cfun
begin

pcpodef ('a::pcpo, 'b::pcpo) sfun (infixr \<open>\<rightarrow>!\<close> 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
  by simp_all

type_notation (ASCII)
  sfun  (infixr \<open>->!\<close> 0)

text \<open>TODO: Define nice syntax for abstraction, application.\<close>

definition sfun_abs :: "('a::pcpo \ 'b::pcpo) \ ('a \! 'b)"
  where "sfun_abs = (\ f. Abs_sfun (strictify\f))"

definition sfun_rep :: "('a::pcpo \! 'b::pcpo) \ 'a \ 'b"
  where "sfun_rep = (\ f. Rep_sfun f)"

lemma sfun_rep_beta: "sfun_rep\f = Rep_sfun f"
  by (simp add: sfun_rep_def cont_Rep_sfun)

lemma sfun_rep_strict1 [simp]: "sfun_rep\\ = \"
  unfolding sfun_rep_beta by (rule Rep_sfun_strict)

lemma sfun_rep_strict2 [simp]: "sfun_rep\f\\ = \"
  unfolding sfun_rep_beta by (rule Rep_sfun [simplified])

lemma strictify_cancel: "f\\ = \ \ strictify\f = f"
  by (simp add: cfun_eq_iff strictify_conv_if)

lemma sfun_abs_sfun_rep [simp]: "sfun_abs\(sfun_rep\f) = f"
  unfolding sfun_abs_def sfun_rep_def
  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
  apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
  apply (simp add: cfun_eq_iff strictify_conv_if)
  apply (simp add: Rep_sfun [simplified])
  done

lemma sfun_rep_sfun_abs [simp]: "sfun_rep\(sfun_abs\f) = strictify\f"
  unfolding sfun_abs_def sfun_rep_def
  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
  apply (simp add: Abs_sfun_inverse)
  done

lemma sfun_eq_iff: "f = g \ sfun_rep\f = sfun_rep\g"
  by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject)

lemma sfun_below_iff: "f \ g \ sfun_rep\f \ sfun_rep\g"
  by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def)

end

quality100%

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