src/HOLCF/Fun_Cpo.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 40004 9f6ed6840e8d
child 40011 b974cf829099
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/Fun_Cpo.thy
     2     Author:     Franz Regensburger
     3     Author:     Brian Huffman
     4 *)
     5 
     6 header {* Class instances for the full function space *}
     7 
     8 theory Fun_Cpo
     9 imports Cont
    10 begin
    11 
    12 subsection {* Full function space is a partial order *}
    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 subsection {* Full function space is chain complete *}
    45 
    46 text {* function application is monotone *}
    47 
    48 lemma monofun_app: "monofun (\<lambda>f. f x)"
    49 by (rule monofunI, simp add: below_fun_def)
    50 
    51 text {* chains of functions yield chains in the po range *}
    52 
    53 lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
    54 by (simp add: chain_def below_fun_def)
    55 
    56 lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
    57 by (simp add: chain_def below_fun_def)
    58 
    59 text {* upper bounds of function chains yield upper bound in the po range *}
    60 
    61 lemma ub2ub_fun:
    62   "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
    63 by (auto simp add: is_ub_def below_fun_def)
    64 
    65 text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
    66 
    67 lemma is_lub_lambda:
    68   assumes f: "\<And>x. range (\<lambda>i. Y i x) <<| f x"
    69   shows "range Y <<| f"
    70 apply (rule is_lubI)
    71 apply (rule ub_rangeI)
    72 apply (rule fun_belowI)
    73 apply (rule is_ub_lub [OF f])
    74 apply (rule fun_belowI)
    75 apply (rule is_lub_lub [OF f])
    76 apply (erule ub2ub_fun)
    77 done
    78 
    79 lemma lub_fun:
    80   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    81     \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
    82 apply (rule is_lub_lambda)
    83 apply (rule cpo_lubI)
    84 apply (erule ch2ch_fun)
    85 done
    86 
    87 lemma thelub_fun:
    88   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    89     \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
    90 by (rule lub_fun [THEN thelubI])
    91 
    92 instance "fun"  :: (type, cpo) cpo
    93 by intro_classes (rule exI, erule lub_fun)
    94 
    95 instance "fun" :: (finite, finite_po) finite_po ..
    96 
    97 instance "fun" :: (type, discrete_cpo) discrete_cpo
    98 proof
    99   fix f g :: "'a \<Rightarrow> 'b"
   100   show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
   101     unfolding fun_below_iff fun_eq_iff
   102     by simp
   103 qed
   104 
   105 text {* chain-finite function spaces *}
   106 
   107 lemma maxinch2maxinch_lambda:
   108   "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
   109 unfolding max_in_chain_def fun_eq_iff by simp
   110 
   111 lemma maxinch_mono:
   112   "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
   113 unfolding max_in_chain_def
   114 proof (intro allI impI)
   115   fix k
   116   assume Y: "\<forall>n\<ge>i. Y i = Y n"
   117   assume ij: "i \<le> j"
   118   assume jk: "j \<le> k"
   119   from ij jk have ik: "i \<le> k" by simp
   120   from Y ij have Yij: "Y i = Y j" by simp
   121   from Y ik have Yik: "Y i = Y k" by simp
   122   from Yij Yik show "Y j = Y k" by auto
   123 qed
   124 
   125 instance "fun" :: (finite, chfin) chfin
   126 proof
   127   fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
   128   let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
   129   assume "chain Y"
   130   hence "\<And>x. chain (\<lambda>i. Y i x)"
   131     by (rule ch2ch_fun)
   132   hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
   133     by (rule chfin)
   134   hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
   135     by (rule LeastI_ex)
   136   hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
   137     by (rule maxinch_mono [OF _ Max_ge], simp_all)
   138   hence "max_in_chain (Max (range ?n)) Y"
   139     by (rule maxinch2maxinch_lambda)
   140   thus "\<exists>n. max_in_chain n Y" ..
   141 qed
   142 
   143 subsection {* Full function space is pointed *}
   144 
   145 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
   146 by (simp add: below_fun_def)
   147 
   148 lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
   149 apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
   150 apply (rule minimal_fun [THEN allI])
   151 done
   152 
   153 instance "fun"  :: (type, pcpo) pcpo
   154 by intro_classes (rule least_fun)
   155 
   156 text {* for compatibility with old HOLCF-Version *}
   157 lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
   158 by (rule minimal_fun [THEN UU_I, symmetric])
   159 
   160 text {* function application is strict in the left argument *}
   161 lemma app_strict [simp]: "\<bottom> x = \<bottom>"
   162 by (simp add: inst_fun_pcpo)
   163 
   164 text {*
   165   The following results are about application for functions in @{typ "'a=>'b"}
   166 *}
   167 
   168 lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
   169 by (simp add: below_fun_def)
   170 
   171 lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
   172 by (rule monofunE)
   173 
   174 lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
   175 by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
   176 
   177 subsection {* Propagation of monotonicity and continuity *}
   178 
   179 text {* the lub of a chain of monotone functions is monotone *}
   180 
   181 lemma monofun_lub_fun:
   182   "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
   183     \<Longrightarrow> monofun (\<Squnion>i. F i)"
   184 apply (rule monofunI)
   185 apply (simp add: thelub_fun)
   186 apply (rule lub_mono)
   187 apply (erule ch2ch_fun)
   188 apply (erule ch2ch_fun)
   189 apply (simp add: monofunE)
   190 done
   191 
   192 text {* the lub of a chain of continuous functions is continuous *}
   193 
   194 lemma cont_lub_fun:
   195   "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
   196 apply (rule contI2)
   197 apply (erule monofun_lub_fun)
   198 apply (simp add: cont2mono)
   199 apply (simp add: thelub_fun cont2contlubE)
   200 apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
   201 done
   202 
   203 lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
   204 apply (rule monofunI)
   205 apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
   206 done
   207 
   208 lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
   209 apply (rule contI2)
   210 apply (erule cont2mono [THEN mono2mono_fun])
   211 apply (simp add: cont2contlubE)
   212 apply (simp add: thelub_fun ch2ch_cont)
   213 done
   214 
   215 text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
   216 
   217 lemma mono2mono_lambda:
   218   assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
   219 apply (rule monofunI)
   220 apply (rule fun_belowI)
   221 apply (erule monofunE [OF f])
   222 done
   223 
   224 lemma cont2cont_lambda [simp]:
   225   assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
   226 apply (rule contI2)
   227 apply (simp add: mono2mono_lambda cont2mono f)
   228 apply (rule fun_belowI)
   229 apply (simp add: thelub_fun cont2contlubE [OF f])
   230 done
   231 
   232 text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
   233 
   234 lemma contlub_lambda:
   235   "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
   236     \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
   237 by (simp add: thelub_fun ch2ch_lambda)
   238 
   239 end