Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Ndist.v Sprache: Coq

Original von: Isabelle^©

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

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

theory Sfun
  imports Cfun
begin

pcpodef ('a, 'b) sfun (infixr "\!" 0) = "{f :: 'a \ 'b. f\\ = \}"
  by simp_all

type_notation (ASCII)
  sfun  (infixr "->!" 0)

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

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

definition sfun_rep :: "('a \! 'b) \ '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

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.