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