(* Title: HOL/HOLCF/Sfun.thy Author: Brian Huffman \<open>The Strict Function Type\<close> theory Sfunimports Cfunbegin pcpodef ('a::pcpo, ' b::pcpo) sfun (infixr \<open>\<rightarrow>!\<close> 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}" by simp_allinfixr \<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_defapply (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_defapply (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 quality 100%
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
