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