author | nipkow |
Wed, 10 Jan 2018 15:25:09 +0100 | |
changeset 67399 | eab6ce8368fa |
parent 67312 | 0d25e02759b7 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Fun_Cpo.thy |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
2 |
Author: Franz Regensburger |
40001 | 3 |
Author: Brian Huffman |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
4 |
*) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
5 |
|
62175 | 6 |
section \<open>Class instances for the full function space\<close> |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
7 |
|
40001 | 8 |
theory Fun_Cpo |
67312 | 9 |
imports Adm |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
10 |
begin |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
11 |
|
62175 | 12 |
subsection \<open>Full function space is a partial order\<close> |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
13 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29138
diff
changeset
|
14 |
instantiation "fun" :: (type, below) below |
25758 | 15 |
begin |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
16 |
|
67399 | 17 |
definition below_fun_def: "(\<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)" |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
18 |
|
25758 | 19 |
instance .. |
20 |
end |
|
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
21 |
|
25758 | 22 |
instance "fun" :: (type, po) po |
23 |
proof |
|
24 |
fix f :: "'a \<Rightarrow> 'b" |
|
25 |
show "f \<sqsubseteq> f" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29138
diff
changeset
|
26 |
by (simp add: below_fun_def) |
25758 | 27 |
next |
28 |
fix f g :: "'a \<Rightarrow> 'b" |
|
67312 | 29 |
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" then show "f = g" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39199
diff
changeset
|
30 |
by (simp add: below_fun_def fun_eq_iff below_antisym) |
25758 | 31 |
next |
32 |
fix f g h :: "'a \<Rightarrow> 'b" |
|
67312 | 33 |
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" then show "f \<sqsubseteq> h" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29138
diff
changeset
|
34 |
unfolding below_fun_def by (fast elim: below_trans) |
25758 | 35 |
qed |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
36 |
|
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
40001
diff
changeset
|
37 |
lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)" |
67312 | 38 |
by (simp add: below_fun_def) |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
39 |
|
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
40001
diff
changeset
|
40 |
lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g" |
67312 | 41 |
by (simp add: below_fun_def) |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
42 |
|
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
43 |
lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x" |
67312 | 44 |
by (simp add: below_fun_def) |
45 |
||
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
46 |
|
62175 | 47 |
subsection \<open>Full function space is chain complete\<close> |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
48 |
|
62175 | 49 |
text \<open>Properties of chains of functions.\<close> |
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
50 |
|
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
51 |
lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))" |
67312 | 52 |
by (auto simp: chain_def fun_below_iff) |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
53 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
54 |
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)" |
67312 | 55 |
by (simp add: chain_def below_fun_def) |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
56 |
|
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17831
diff
changeset
|
57 |
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S" |
67312 | 58 |
by (simp add: chain_def below_fun_def) |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
59 |
|
67312 | 60 |
text \<open>Type @{typ "'a::type \<Rightarrow> 'b::cpo"} is chain complete\<close> |
61 |
||
62 |
lemma 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) |
|
26028 | 64 |
|
67312 | 65 |
lemma 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 |
|
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
71 |
|
67312 | 72 |
lemma 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]) |
|
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
75 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
18291
diff
changeset
|
76 |
instance "fun" :: (type, cpo) cpo |
67312 | 77 |
by intro_classes (rule exI, erule is_lub_fun) |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
78 |
|
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
79 |
instance "fun" :: (type, discrete_cpo) discrete_cpo |
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
80 |
proof |
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
81 |
fix f g :: "'a \<Rightarrow> 'b" |
67312 | 82 |
show "f \<sqsubseteq> g \<longleftrightarrow> f = g" |
83 |
by (simp add: fun_below_iff fun_eq_iff) |
|
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
84 |
qed |
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
85 |
|
67312 | 86 |
|
62175 | 87 |
subsection \<open>Full function space is pointed\<close> |
17831 | 88 |
|
89 |
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f" |
|
67312 | 90 |
by (simp add: below_fun_def) |
17831 | 91 |
|
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
92 |
instance "fun" :: (type, pcpo) pcpo |
67312 | 93 |
by standard (fast intro: minimal_fun) |
17831 | 94 |
|
95 |
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)" |
|
67312 | 96 |
by (rule minimal_fun [THEN bottomI, symmetric]) |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
97 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
98 |
lemma app_strict [simp]: "\<bottom> x = \<bottom>" |
67312 | 99 |
by (simp add: inst_fun_pcpo) |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
100 |
|
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
101 |
lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>" |
67312 | 102 |
by (rule bottomI, rule minimal_fun) |
103 |
||
25786 | 104 |
|
62175 | 105 |
subsection \<open>Propagation of monotonicity and continuity\<close> |
25786 | 106 |
|
62175 | 107 |
text \<open>The lub of a chain of monotone functions is monotone.\<close> |
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
108 |
|
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
109 |
lemma adm_monofun: "adm monofun" |
67312 | 110 |
by (rule admI) (simp add: lub_fun fun_chain_iff monofun_def lub_mono) |
25786 | 111 |
|
62175 | 112 |
text \<open>The lub of a chain of continuous functions is continuous.\<close> |
25786 | 113 |
|
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
114 |
lemma adm_cont: "adm cont" |
67312 | 115 |
by (rule admI) (simp add: lub_fun fun_chain_iff) |
25786 | 116 |
|
62175 | 117 |
text \<open>Function application preserves monotonicity and continuity.\<close> |
25786 | 118 |
|
119 |
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)" |
|
67312 | 120 |
by (simp add: monofun_def fun_below_iff) |
25786 | 121 |
|
122 |
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)" |
|
67312 | 123 |
apply (rule contI2) |
124 |
apply (erule cont2mono [THEN mono2mono_fun]) |
|
125 |
apply (simp add: cont2contlubE lub_fun ch2ch_cont) |
|
126 |
done |
|
25786 | 127 |
|
40622
e40e9e9769f4
add lemma cont_fun; remove unused lemma monofun_app
huffman
parents:
40091
diff
changeset
|
128 |
lemma cont_fun: "cont (\<lambda>f. f x)" |
67312 | 129 |
using cont_id by (rule cont2cont_fun) |
40622
e40e9e9769f4
add lemma cont_fun; remove unused lemma monofun_app
huffman
parents:
40091
diff
changeset
|
130 |
|
62175 | 131 |
text \<open> |
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset
|
132 |
Lambda abstraction preserves monotonicity and continuity. |
62175 | 133 |
(Note \<open>(\<lambda>x. \<lambda>y. f x y) = f\<close>.) |
134 |
\<close> |
|
25786 | 135 |
|
67312 | 136 |
lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f" |
137 |
by (simp add: monofun_def fun_below_iff) |
|
25786 | 138 |
|
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset
|
139 |
lemma cont2cont_lambda [simp]: |
67312 | 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]) |
|
25786 | 143 |
|
62175 | 144 |
text \<open>What D.A.Schmidt calls continuity of abstraction; never used here\<close> |
25786 | 145 |
|
67312 | 146 |
lemma 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) |
|
25786 | 149 |
|
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
150 |
end |