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