|
(* 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.2 Sekunden
(vorverarbeitet)
¤
|
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.
|
