src/HOLCF/Ffun.thy
 author huffman Mon May 11 08:28:09 2009 -0700 (2009-05-11) changeset 31095 b79d140f6d0b parent 31076 99fe356cbbc2 child 35914 91a7311177c4 permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
```     1 (*  Title:      HOLCF/FunCpo.thy
```
```     2     Author:     Franz Regensburger
```
```     3 *)
```
```     4
```
```     5 header {* Class instances for the full function space *}
```
```     6
```
```     7 theory Ffun
```
```     8 imports Cont
```
```     9 begin
```
```    10
```
```    11 subsection {* Full function space is a partial order *}
```
```    12
```
```    13 instantiation "fun"  :: (type, below) below
```
```    14 begin
```
```    15
```
```    16 definition
```
```    17   below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
```
```    18
```
```    19 instance ..
```
```    20 end
```
```    21
```
```    22 instance "fun" :: (type, po) po
```
```    23 proof
```
```    24   fix f :: "'a \<Rightarrow> 'b"
```
```    25   show "f \<sqsubseteq> f"
```
```    26     by (simp add: below_fun_def)
```
```    27 next
```
```    28   fix f g :: "'a \<Rightarrow> 'b"
```
```    29   assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
```
```    30     by (simp add: below_fun_def expand_fun_eq below_antisym)
```
```    31 next
```
```    32   fix f g h :: "'a \<Rightarrow> 'b"
```
```    33   assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
```
```    34     unfolding below_fun_def by (fast elim: below_trans)
```
```    35 qed
```
```    36
```
```    37 text {* make the symbol @{text "<<"} accessible for type fun *}
```
```    38
```
```    39 lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
```
```    40 by (simp add: below_fun_def)
```
```    41
```
```    42 lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
```
```    43 by (simp add: below_fun_def)
```
```    44
```
```    45 subsection {* Full function space is chain complete *}
```
```    46
```
```    47 text {* function application is monotone *}
```
```    48
```
```    49 lemma monofun_app: "monofun (\<lambda>f. f x)"
```
```    50 by (rule monofunI, simp add: below_fun_def)
```
```    51
```
```    52 text {* chains of functions yield chains in the po range *}
```
```    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 {* upper bounds of function chains yield upper bound in the po range *}
```
```    61
```
```    62 lemma ub2ub_fun:
```
```    63   "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
```
```    64 by (auto simp add: is_ub_def below_fun_def)
```
```    65
```
```    66 text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
```
```    67
```
```    68 lemma is_lub_lambda:
```
```    69   assumes f: "\<And>x. range (\<lambda>i. Y i x) <<| f x"
```
```    70   shows "range Y <<| f"
```
```    71 apply (rule is_lubI)
```
```    72 apply (rule ub_rangeI)
```
```    73 apply (rule below_fun_ext)
```
```    74 apply (rule is_ub_lub [OF f])
```
```    75 apply (rule below_fun_ext)
```
```    76 apply (rule is_lub_lub [OF f])
```
```    77 apply (erule ub2ub_fun)
```
```    78 done
```
```    79
```
```    80 lemma lub_fun:
```
```    81   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
```
```    82     \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
```
```    83 apply (rule is_lub_lambda)
```
```    84 apply (rule cpo_lubI)
```
```    85 apply (erule ch2ch_fun)
```
```    86 done
```
```    87
```
```    88 lemma thelub_fun:
```
```    89   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
```
```    90     \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
```
```    91 by (rule lub_fun [THEN thelubI])
```
```    92
```
```    93 lemma cpo_fun:
```
```    94   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
```
```    95 by (rule exI, erule lub_fun)
```
```    96
```
```    97 instance "fun"  :: (type, cpo) cpo
```
```    98 by intro_classes (rule cpo_fun)
```
```    99
```
```   100 instance "fun" :: (finite, finite_po) finite_po ..
```
```   101
```
```   102 instance "fun" :: (type, discrete_cpo) discrete_cpo
```
```   103 proof
```
```   104   fix f g :: "'a \<Rightarrow> 'b"
```
```   105   show "f \<sqsubseteq> g \<longleftrightarrow> f = g"
```
```   106     unfolding expand_fun_below expand_fun_eq
```
```   107     by simp
```
```   108 qed
```
```   109
```
```   110 text {* chain-finite function spaces *}
```
```   111
```
```   112 lemma maxinch2maxinch_lambda:
```
```   113   "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
```
```   114 unfolding max_in_chain_def expand_fun_eq by simp
```
```   115
```
```   116 lemma maxinch_mono:
```
```   117   "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
```
```   118 unfolding max_in_chain_def
```
```   119 proof (intro allI impI)
```
```   120   fix k
```
```   121   assume Y: "\<forall>n\<ge>i. Y i = Y n"
```
```   122   assume ij: "i \<le> j"
```
```   123   assume jk: "j \<le> k"
```
```   124   from ij jk have ik: "i \<le> k" by simp
```
```   125   from Y ij have Yij: "Y i = Y j" by simp
```
```   126   from Y ik have Yik: "Y i = Y k" by simp
```
```   127   from Yij Yik show "Y j = Y k" by auto
```
```   128 qed
```
```   129
```
```   130 instance "fun" :: (finite, chfin) chfin
```
```   131 proof
```
```   132   fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
```
```   133   let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
```
```   134   assume "chain Y"
```
```   135   hence "\<And>x. chain (\<lambda>i. Y i x)"
```
```   136     by (rule ch2ch_fun)
```
```   137   hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
```
```   138     by (rule chfin)
```
```   139   hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
```
```   140     by (rule LeastI_ex)
```
```   141   hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
```
```   142     by (rule maxinch_mono [OF _ Max_ge], simp_all)
```
```   143   hence "max_in_chain (Max (range ?n)) Y"
```
```   144     by (rule maxinch2maxinch_lambda)
```
```   145   thus "\<exists>n. max_in_chain n Y" ..
```
```   146 qed
```
```   147
```
```   148 subsection {* Full function space is pointed *}
```
```   149
```
```   150 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
```
```   151 by (simp add: below_fun_def)
```
```   152
```
```   153 lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
```
```   154 apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
```
```   155 apply (rule minimal_fun [THEN allI])
```
```   156 done
```
```   157
```
```   158 instance "fun"  :: (type, pcpo) pcpo
```
```   159 by intro_classes (rule least_fun)
```
```   160
```
```   161 text {* for compatibility with old HOLCF-Version *}
```
```   162 lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
```
```   163 by (rule minimal_fun [THEN UU_I, symmetric])
```
```   164
```
```   165 text {* function application is strict in the left argument *}
```
```   166 lemma app_strict [simp]: "\<bottom> x = \<bottom>"
```
```   167 by (simp add: inst_fun_pcpo)
```
```   168
```
```   169 text {*
```
```   170   The following results are about application for functions in @{typ "'a=>'b"}
```
```   171 *}
```
```   172
```
```   173 lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
```
```   174 by (simp add: below_fun_def)
```
```   175
```
```   176 lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
```
```   177 by (rule monofunE)
```
```   178
```
```   179 lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
```
```   180 by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
```
```   181
```
```   182 subsection {* Propagation of monotonicity and continuity *}
```
```   183
```
```   184 text {* the lub of a chain of monotone functions is monotone *}
```
```   185
```
```   186 lemma monofun_lub_fun:
```
```   187   "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
```
```   188     \<Longrightarrow> monofun (\<Squnion>i. F i)"
```
```   189 apply (rule monofunI)
```
```   190 apply (simp add: thelub_fun)
```
```   191 apply (rule lub_mono)
```
```   192 apply (erule ch2ch_fun)
```
```   193 apply (erule ch2ch_fun)
```
```   194 apply (simp add: monofunE)
```
```   195 done
```
```   196
```
```   197 text {* the lub of a chain of continuous functions is continuous *}
```
```   198
```
```   199 lemma contlub_lub_fun:
```
```   200   "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)"
```
```   201 apply (rule contlubI)
```
```   202 apply (simp add: thelub_fun)
```
```   203 apply (simp add: cont2contlubE)
```
```   204 apply (rule ex_lub)
```
```   205 apply (erule ch2ch_fun)
```
```   206 apply (simp add: ch2ch_cont)
```
```   207 done
```
```   208
```
```   209 lemma cont_lub_fun:
```
```   210   "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
```
```   211 apply (rule monocontlub2cont)
```
```   212 apply (erule monofun_lub_fun)
```
```   213 apply (simp add: cont2mono)
```
```   214 apply (erule (1) contlub_lub_fun)
```
```   215 done
```
```   216
```
```   217 lemma cont2cont_lub:
```
```   218   "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
```
```   219 by (simp add: thelub_fun [symmetric] cont_lub_fun)
```
```   220
```
```   221 lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
```
```   222 apply (rule monofunI)
```
```   223 apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
```
```   224 done
```
```   225
```
```   226 lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
```
```   227 apply (rule monocontlub2cont)
```
```   228 apply (erule cont2mono [THEN mono2mono_fun])
```
```   229 apply (rule contlubI)
```
```   230 apply (simp add: cont2contlubE)
```
```   231 apply (simp add: thelub_fun ch2ch_cont)
```
```   232 done
```
```   233
```
```   234 text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
```
```   235
```
```   236 lemma mono2mono_lambda:
```
```   237   assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
```
```   238 apply (rule monofunI)
```
```   239 apply (rule below_fun_ext)
```
```   240 apply (erule monofunE [OF f])
```
```   241 done
```
```   242
```
```   243 lemma cont2cont_lambda [simp]:
```
```   244   assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
```
```   245 apply (subgoal_tac "monofun f")
```
```   246 apply (rule monocontlub2cont)
```
```   247 apply assumption
```
```   248 apply (rule contlubI)
```
```   249 apply (rule ext)
```
```   250 apply (simp add: thelub_fun ch2ch_monofun)
```
```   251 apply (erule cont2contlubE [OF f])
```
```   252 apply (simp add: mono2mono_lambda cont2mono f)
```
```   253 done
```
```   254
```
```   255 text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
```
```   256
```
```   257 lemma contlub_lambda:
```
```   258   "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
```
```   259     \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
```
```   260 by (simp add: thelub_fun ch2ch_lambda)
```
```   261
```
```   262 lemma contlub_abstraction:
```
```   263   "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
```
```   264     (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
```
```   265 apply (rule thelub_fun [symmetric])
```
```   266 apply (simp add: ch2ch_cont)
```
```   267 done
```
```   268
```
```   269 lemma mono2mono_app:
```
```   270   "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
```
```   271 apply (rule monofunI)
```
```   272 apply (simp add: monofun_fun monofunE)
```
```   273 done
```
```   274
```
```   275 lemma cont2contlub_app:
```
```   276   "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))"
```
```   277 apply (rule contlubI)
```
```   278 apply (subgoal_tac "chain (\<lambda>i. f (Y i))")
```
```   279 apply (subgoal_tac "chain (\<lambda>i. t (Y i))")
```
```   280 apply (simp add: cont2contlubE thelub_fun)
```
```   281 apply (rule diag_lub)
```
```   282 apply (erule ch2ch_fun)
```
```   283 apply (drule spec)
```
```   284 apply (erule (1) ch2ch_cont)
```
```   285 apply (erule (1) ch2ch_cont)
```
```   286 apply (erule (1) ch2ch_cont)
```
```   287 done
```
```   288
```
```   289 lemma cont2cont_app:
```
```   290   "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
```
```   291 by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)
```
```   292
```
```   293 lemmas cont2cont_app2 = cont2cont_app [rule_format]
```
```   294
```
```   295 lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
```
```   296 by (rule cont2cont_app2 [OF cont_const])
```
```   297
```
```   298 end
```