src/HOL/HOLCF/Sfun.thy
author wenzelm
Mon, 01 Jan 2018 23:07:24 +0100
changeset 67312 0d25e02759b7
parent 62175 8ffc4d0e652d
permissions -rw-r--r--
misc tuning and modernization;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 40774
diff changeset
     1
(*  Title:      HOL/HOLCF/Sfun.thy
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
     3
*)
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
     4
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61998
diff changeset
     5
section \<open>The Strict Function Type\<close>
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
     6
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
     7
theory Sfun
67312
0d25e02759b7 misc tuning and modernization;
wenzelm
parents: 62175
diff changeset
     8
  imports Cfun
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
     9
begin
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    10
67312
0d25e02759b7 misc tuning and modernization;
wenzelm
parents: 62175
diff changeset
    11
pcpodef ('a, 'b) sfun (infixr "\<rightarrow>!" 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
0d25e02759b7 misc tuning and modernization;
wenzelm
parents: 62175
diff changeset
    12
  by simp_all
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    13
61998
b66d2ca1f907 clarified print modes;
wenzelm
parents: 58880
diff changeset
    14
type_notation (ASCII)
b66d2ca1f907 clarified print modes;
wenzelm
parents: 58880
diff changeset
    15
  sfun  (infixr "->!" 0)
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    16
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 61998
diff changeset
    17
text \<open>TODO: Define nice syntax for abstraction, application.\<close>
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    18
67312
0d25e02759b7 misc tuning and modernization;
wenzelm
parents: 62175
diff changeset
    19
definition sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
0d25e02759b7 misc tuning and modernization;
wenzelm
parents: 62175
diff changeset
    20
  where "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    21
67312
0d25e02759b7 misc tuning and modernization;
wenzelm
parents: 62175
diff changeset
    22
definition sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
0d25e02759b7 misc tuning and modernization;
wenzelm
parents: 62175
diff changeset
    23
  where "sfun_rep = (\<Lambda> f. Rep_sfun f)"
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    24
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    25
lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
67312
0d25e02759b7 misc tuning and modernization;
wenzelm
parents: 62175
diff changeset
    26
  by (simp add: sfun_rep_def cont_Rep_sfun)
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    27
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    28
lemma sfun_rep_strict1 [simp]: "sfun_rep\<cdot>\<bottom> = \<bottom>"
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    29
  unfolding sfun_rep_beta by (rule Rep_sfun_strict)
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    30
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    31
lemma sfun_rep_strict2 [simp]: "sfun_rep\<cdot>f\<cdot>\<bottom> = \<bottom>"
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    32
  unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    33
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    34
lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    35
  by (simp add: cfun_eq_iff strictify_conv_if)
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    36
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    37
lemma sfun_abs_sfun_rep [simp]: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    38
  unfolding sfun_abs_def sfun_rep_def
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    39
  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    40
  apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    41
  apply (simp add: cfun_eq_iff strictify_conv_if)
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    42
  apply (simp add: Rep_sfun [simplified])
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    43
  done
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    44
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    45
lemma sfun_rep_sfun_abs [simp]: "sfun_rep\<cdot>(sfun_abs\<cdot>f) = strictify\<cdot>f"
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    46
  unfolding sfun_abs_def sfun_rep_def
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    47
  apply (simp add: cont_Abs_sfun cont_Rep_sfun)
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    48
  apply (simp add: Abs_sfun_inverse)
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    49
  done
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    50
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    51
lemma sfun_eq_iff: "f = g \<longleftrightarrow> sfun_rep\<cdot>f = sfun_rep\<cdot>g"
67312
0d25e02759b7 misc tuning and modernization;
wenzelm
parents: 62175
diff changeset
    52
  by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject)
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    53
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    54
lemma sfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> sfun_rep\<cdot>f \<sqsubseteq> sfun_rep\<cdot>g"
67312
0d25e02759b7 misc tuning and modernization;
wenzelm
parents: 62175
diff changeset
    55
  by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def)
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    56
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
diff changeset
    57
end