src/HOL/HOLCF/Fun_Cpo.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 62175 8ffc4d0e652d
child 67312 0d25e02759b7
permissions -rw-r--r--
tuned;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Fun_Cpo.thy
huffman@16202
     2
    Author:     Franz Regensburger
huffman@40001
     3
    Author:     Brian Huffman
huffman@16202
     4
*)
huffman@16202
     5
wenzelm@62175
     6
section \<open>Class instances for the full function space\<close>
huffman@16202
     7
huffman@40001
     8
theory Fun_Cpo
huffman@40011
     9
imports Adm
huffman@16202
    10
begin
huffman@16202
    11
wenzelm@62175
    12
subsection \<open>Full function space is a partial order\<close>
huffman@16202
    13
huffman@31076
    14
instantiation "fun"  :: (type, below) below
huffman@25758
    15
begin
huffman@16202
    16
huffman@25758
    17
definition
huffman@31076
    18
  below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
huffman@16202
    19
huffman@25758
    20
instance ..
huffman@25758
    21
end
huffman@16202
    22
huffman@25758
    23
instance "fun" :: (type, po) po
huffman@25758
    24
proof
huffman@25758
    25
  fix f :: "'a \<Rightarrow> 'b"
huffman@25758
    26
  show "f \<sqsubseteq> f"
huffman@31076
    27
    by (simp add: below_fun_def)
huffman@25758
    28
next
huffman@25758
    29
  fix f g :: "'a \<Rightarrow> 'b"
huffman@25758
    30
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
nipkow@39302
    31
    by (simp add: below_fun_def fun_eq_iff below_antisym)
huffman@25758
    32
next
huffman@25758
    33
  fix f g h :: "'a \<Rightarrow> 'b"
huffman@25758
    34
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
huffman@31076
    35
    unfolding below_fun_def by (fast elim: below_trans)
huffman@25758
    36
qed
huffman@16202
    37
huffman@40002
    38
lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)"
huffman@31076
    39
by (simp add: below_fun_def)
huffman@16202
    40
huffman@40002
    41
lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
huffman@31076
    42
by (simp add: below_fun_def)
huffman@16202
    43
huffman@40011
    44
lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
huffman@40011
    45
by (simp add: below_fun_def)
huffman@40011
    46
wenzelm@62175
    47
subsection \<open>Full function space is chain complete\<close>
huffman@16202
    48
wenzelm@62175
    49
text \<open>Properties of chains of functions.\<close>
huffman@40011
    50
huffman@40011
    51
lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
huffman@40011
    52
unfolding chain_def fun_below_iff by auto
huffman@16202
    53
huffman@16202
    54
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
huffman@31076
    55
by (simp add: chain_def below_fun_def)
huffman@16202
    56
huffman@18092
    57
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
huffman@31076
    58
by (simp add: chain_def below_fun_def)
huffman@16202
    59
wenzelm@62175
    60
text \<open>Type @{typ "'a::type => 'b::cpo"} is chain complete\<close>
huffman@16202
    61
huffman@26028
    62
lemma is_lub_lambda:
huffman@40011
    63
  "(\<And>x. range (\<lambda>i. Y i x) <<| f x) \<Longrightarrow> range Y <<| f"
huffman@40011
    64
unfolding is_lub_def is_ub_def below_fun_def by simp
huffman@26028
    65
huffman@41030
    66
lemma is_lub_fun:
huffman@16202
    67
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
huffman@16202
    68
    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
huffman@26028
    69
apply (rule is_lub_lambda)
huffman@26028
    70
apply (rule cpo_lubI)
huffman@16202
    71
apply (erule ch2ch_fun)
huffman@16202
    72
done
huffman@16202
    73
huffman@41030
    74
lemma lub_fun:
huffman@16202
    75
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
huffman@27413
    76
    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
huffman@41030
    77
by (rule is_lub_fun [THEN lub_eqI])
huffman@16202
    78
krauss@20523
    79
instance "fun"  :: (type, cpo) cpo
huffman@41030
    80
by intro_classes (rule exI, erule is_lub_fun)
huffman@16202
    81
huffman@40011
    82
instance "fun" :: (type, discrete_cpo) discrete_cpo
huffman@40011
    83
proof
huffman@40011
    84
  fix f g :: "'a \<Rightarrow> 'b"
huffman@40011
    85
  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
huffman@40011
    86
    unfolding fun_below_iff fun_eq_iff
huffman@40011
    87
    by simp
huffman@40011
    88
qed
huffman@40011
    89
wenzelm@62175
    90
subsection \<open>Full function space is pointed\<close>
huffman@17831
    91
huffman@17831
    92
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
huffman@31076
    93
by (simp add: below_fun_def)
huffman@17831
    94
huffman@40011
    95
instance "fun"  :: (type, pcpo) pcpo
wenzelm@61169
    96
by standard (fast intro: minimal_fun)
huffman@17831
    97
huffman@17831
    98
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
huffman@41430
    99
by (rule minimal_fun [THEN bottomI, symmetric])
huffman@16202
   100
huffman@16202
   101
lemma app_strict [simp]: "\<bottom> x = \<bottom>"
huffman@16202
   102
by (simp add: inst_fun_pcpo)
huffman@16202
   103
huffman@40011
   104
lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
huffman@41430
   105
by (rule bottomI, rule minimal_fun)
huffman@25786
   106
wenzelm@62175
   107
subsection \<open>Propagation of monotonicity and continuity\<close>
huffman@25786
   108
wenzelm@62175
   109
text \<open>The lub of a chain of monotone functions is monotone.\<close>
huffman@40011
   110
huffman@40011
   111
lemma adm_monofun: "adm monofun"
huffman@41030
   112
by (rule admI, simp add: lub_fun fun_chain_iff monofun_def lub_mono)
huffman@25786
   113
wenzelm@62175
   114
text \<open>The lub of a chain of continuous functions is continuous.\<close>
huffman@25786
   115
huffman@40011
   116
lemma adm_cont: "adm cont"
huffman@41030
   117
by (rule admI, simp add: lub_fun fun_chain_iff)
huffman@25786
   118
wenzelm@62175
   119
text \<open>Function application preserves monotonicity and continuity.\<close>
huffman@25786
   120
huffman@25786
   121
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
huffman@40011
   122
by (simp add: monofun_def fun_below_iff)
huffman@25786
   123
huffman@25786
   124
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
huffman@35914
   125
apply (rule contI2)
huffman@25786
   126
apply (erule cont2mono [THEN mono2mono_fun])
huffman@41030
   127
apply (simp add: cont2contlubE lub_fun ch2ch_cont)
huffman@25786
   128
done
huffman@25786
   129
huffman@40622
   130
lemma cont_fun: "cont (\<lambda>f. f x)"
huffman@40622
   131
using cont_id by (rule cont2cont_fun)
huffman@40622
   132
wenzelm@62175
   133
text \<open>
huffman@40011
   134
  Lambda abstraction preserves monotonicity and continuity.
wenzelm@62175
   135
  (Note \<open>(\<lambda>x. \<lambda>y. f x y) = f\<close>.)
wenzelm@62175
   136
\<close>
huffman@25786
   137
huffman@26452
   138
lemma mono2mono_lambda:
huffman@26452
   139
  assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
huffman@40011
   140
using f by (simp add: monofun_def fun_below_iff)
huffman@25786
   141
huffman@26452
   142
lemma cont2cont_lambda [simp]:
huffman@26452
   143
  assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
huffman@40011
   144
by (rule contI, rule is_lub_lambda, rule contE [OF f])
huffman@25786
   145
wenzelm@62175
   146
text \<open>What D.A.Schmidt calls continuity of abstraction; never used here\<close>
huffman@25786
   147
huffman@25786
   148
lemma contlub_lambda:
huffman@25786
   149
  "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
huffman@25786
   150
    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
huffman@41030
   151
by (simp add: lub_fun ch2ch_lambda)
huffman@25786
   152
huffman@16202
   153
end