1(* Title: HOL/HOLCF/Sfun.thy 2 Author: Brian Huffman 3*) 4 5section \<open>The Strict Function Type\<close> 6 7theory Sfun 8 imports Cfun 9begin 10 11pcpodef ('a, 'b) sfun (infixr "\<rightarrow>!" 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}" 12 by simp_all 13 14type_notation (ASCII) 15 sfun (infixr "->!" 0) 16 17text \<open>TODO: Define nice syntax for abstraction, application.\<close> 18 19definition sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)" 20 where "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))" 21 22definition sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b" 23 where "sfun_rep = (\<Lambda> f. Rep_sfun f)" 24 25lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f" 26 by (simp add: sfun_rep_def cont_Rep_sfun) 27 28lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>" 29 unfolding sfun_rep_beta by (rule Rep_sfun_strict) 30 31lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>" 32 unfolding sfun_rep_beta by (rule Rep_sfun [simplified]) 33 34lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f" 35 by (simp add: cfun_eq_iff strictify_conv_if) 36 37lemma sfun_abs_sfun_rep [simp]: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f" 38 unfolding sfun_abs_def sfun_rep_def 39 apply (simp add: cont_Abs_sfun cont_Rep_sfun) 40 apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse) 41 apply (simp add: cfun_eq_iff strictify_conv_if) 42 apply (simp add: Rep_sfun [simplified]) 43 done 44 45lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f" 46 unfolding sfun_abs_def sfun_rep_def 47 apply (simp add: cont_Abs_sfun cont_Rep_sfun) 48 apply (simp add: Abs_sfun_inverse) 49 done 50 51lemma sfun_eq_iff: "f = g \<longleftrightarrow> sfun_rep\<cdot>f = sfun_rep\<cdot>g" 52 by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject) 53 54lemma sfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> sfun_rep\<cdot>f \<sqsubseteq> sfun_rep\<cdot>g" 55 by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def) 56 57end 58