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