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