author | huffman |
Mon, 11 Oct 2010 21:35:31 -0700 | |
changeset 40002 | c5b5f7a3a3b1 |
parent 40001 | 666c3751227c |
child 40004 | 9f6ed6840e8d |
permissions | -rw-r--r-- |
40001 | 1 |
(* Title: 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 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
6 |
header {* Class instances for the full function space *} |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
7 |
|
40001 | 8 |
theory Fun_Cpo |
25786 | 9 |
imports Cont |
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 |
|
18291 | 12 |
subsection {* Full function space is a partial order *} |
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 |
|
25758 | 17 |
definition |
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
|
18 |
below_fun_def: "(op \<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
|
19 |
|
25758 | 20 |
instance .. |
21 |
end |
|
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
22 |
|
25758 | 23 |
instance "fun" :: (type, po) po |
24 |
proof |
|
25 |
fix f :: "'a \<Rightarrow> 'b" |
|
26 |
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
|
27 |
by (simp add: below_fun_def) |
25758 | 28 |
next |
29 |
fix f g :: "'a \<Rightarrow> 'b" |
|
30 |
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "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
|
31 |
by (simp add: below_fun_def fun_eq_iff below_antisym) |
25758 | 32 |
next |
33 |
fix f g h :: "'a \<Rightarrow> 'b" |
|
34 |
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "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
|
35 |
unfolding below_fun_def by (fast elim: below_trans) |
25758 | 36 |
qed |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
37 |
|
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
|
38 |
lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)" |
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
|
39 |
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
|
40 |
|
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
|
41 |
lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g" |
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
|
42 |
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
|
43 |
|
18291 | 44 |
subsection {* Full function space is chain complete *} |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
45 |
|
25786 | 46 |
text {* function application is monotone *} |
47 |
||
48 |
lemma monofun_app: "monofun (\<lambda>f. f x)" |
|
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
|
49 |
by (rule monofunI, simp add: below_fun_def) |
25786 | 50 |
|
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
51 |
text {* chains of functions yield chains in the po range *} |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
52 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
53 |
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)" |
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
|
54 |
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
|
55 |
|
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17831
diff
changeset
|
56 |
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S" |
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
|
57 |
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
|
58 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
59 |
text {* upper bounds of function chains yield upper bound in the po range *} |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
60 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
61 |
lemma ub2ub_fun: |
26028 | 62 |
"range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x" |
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
|
63 |
by (auto simp add: is_ub_def below_fun_def) |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
64 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
65 |
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
66 |
|
26028 | 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) |
|
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
|
72 |
apply (rule fun_belowI) |
26028 | 73 |
apply (rule is_ub_lub [OF f]) |
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
|
74 |
apply (rule fun_belowI) |
26028 | 75 |
apply (rule is_lub_lub [OF f]) |
76 |
apply (erule ub2ub_fun) |
|
77 |
done |
|
78 |
||
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
79 |
lemma lub_fun: |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
80 |
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
81 |
\<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)" |
26028 | 82 |
apply (rule is_lub_lambda) |
83 |
apply (rule cpo_lubI) |
|
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
84 |
apply (erule ch2ch_fun) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
85 |
done |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
86 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
87 |
lemma thelub_fun: |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
88 |
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) |
27413 | 89 |
\<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)" |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
90 |
by (rule lub_fun [THEN thelubI]) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
91 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
92 |
lemma cpo_fun: |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
93 |
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x" |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
94 |
by (rule exI, erule lub_fun) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
95 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
18291
diff
changeset
|
96 |
instance "fun" :: (type, cpo) cpo |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
97 |
by intro_classes (rule cpo_fun) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
98 |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
99 |
instance "fun" :: (finite, finite_po) finite_po .. |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
100 |
|
26025 | 101 |
instance "fun" :: (type, discrete_cpo) discrete_cpo |
102 |
proof |
|
103 |
fix f g :: "'a \<Rightarrow> 'b" |
|
104 |
show "f \<sqsubseteq> g \<longleftrightarrow> f = g" |
|
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
|
105 |
unfolding fun_below_iff fun_eq_iff |
26025 | 106 |
by simp |
107 |
qed |
|
108 |
||
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
109 |
text {* chain-finite function spaces *} |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
110 |
|
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
111 |
lemma maxinch2maxinch_lambda: |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
112 |
"(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39199
diff
changeset
|
113 |
unfolding max_in_chain_def fun_eq_iff by simp |
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
114 |
|
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
115 |
lemma maxinch_mono: |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
116 |
"\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
117 |
unfolding max_in_chain_def |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
118 |
proof (intro allI impI) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
119 |
fix k |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
120 |
assume Y: "\<forall>n\<ge>i. Y i = Y n" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
121 |
assume ij: "i \<le> j" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
122 |
assume jk: "j \<le> k" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
123 |
from ij jk have ik: "i \<le> k" by simp |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
124 |
from Y ij have Yij: "Y i = Y j" by simp |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
125 |
from Y ik have Yik: "Y i = Y k" by simp |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
126 |
from Yij Yik show "Y j = Y k" by auto |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
127 |
qed |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
128 |
|
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
129 |
instance "fun" :: (finite, chfin) chfin |
25921 | 130 |
proof |
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
131 |
fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
132 |
let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
133 |
assume "chain Y" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
134 |
hence "\<And>x. chain (\<lambda>i. Y i x)" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
135 |
by (rule ch2ch_fun) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
136 |
hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)" |
25921 | 137 |
by (rule chfin) |
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
138 |
hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
139 |
by (rule LeastI_ex) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
140 |
hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
141 |
by (rule maxinch_mono [OF _ Max_ge], simp_all) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
142 |
hence "max_in_chain (Max (range ?n)) Y" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
143 |
by (rule maxinch2maxinch_lambda) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
144 |
thus "\<exists>n. max_in_chain n Y" .. |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
145 |
qed |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset
|
146 |
|
18291 | 147 |
subsection {* Full function space is pointed *} |
17831 | 148 |
|
149 |
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<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
|
150 |
by (simp add: below_fun_def) |
17831 | 151 |
|
25786 | 152 |
lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y" |
17831 | 153 |
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI) |
154 |
apply (rule minimal_fun [THEN allI]) |
|
155 |
done |
|
156 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
18291
diff
changeset
|
157 |
instance "fun" :: (type, pcpo) pcpo |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
158 |
by intro_classes (rule least_fun) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
159 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
160 |
text {* for compatibility with old HOLCF-Version *} |
17831 | 161 |
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)" |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
162 |
by (rule minimal_fun [THEN UU_I, symmetric]) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
163 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
164 |
text {* function application is strict in the left argument *} |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
165 |
lemma app_strict [simp]: "\<bottom> x = \<bottom>" |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
166 |
by (simp add: inst_fun_pcpo) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
167 |
|
25786 | 168 |
text {* |
169 |
The following results are about application for functions in @{typ "'a=>'b"} |
|
170 |
*} |
|
171 |
||
172 |
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x" |
|
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
|
173 |
by (simp add: below_fun_def) |
25786 | 174 |
|
175 |
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" |
|
176 |
by (rule monofunE) |
|
177 |
||
178 |
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y" |
|
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
|
179 |
by (rule below_trans [OF monofun_fun_arg monofun_fun_fun]) |
25786 | 180 |
|
181 |
subsection {* Propagation of monotonicity and continuity *} |
|
182 |
||
183 |
text {* the lub of a chain of monotone functions is monotone *} |
|
184 |
||
185 |
lemma monofun_lub_fun: |
|
186 |
"\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk> |
|
187 |
\<Longrightarrow> monofun (\<Squnion>i. F i)" |
|
188 |
apply (rule monofunI) |
|
189 |
apply (simp add: thelub_fun) |
|
25923 | 190 |
apply (rule lub_mono) |
25786 | 191 |
apply (erule ch2ch_fun) |
192 |
apply (erule ch2ch_fun) |
|
193 |
apply (simp add: monofunE) |
|
194 |
done |
|
195 |
||
196 |
text {* the lub of a chain of continuous functions is continuous *} |
|
197 |
||
198 |
lemma cont_lub_fun: |
|
199 |
"\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)" |
|
35914 | 200 |
apply (rule contI2) |
25786 | 201 |
apply (erule monofun_lub_fun) |
202 |
apply (simp add: cont2mono) |
|
35914 | 203 |
apply (simp add: thelub_fun cont2contlubE) |
204 |
apply (simp add: diag_lub ch2ch_fun ch2ch_cont) |
|
25786 | 205 |
done |
206 |
||
207 |
lemma cont2cont_lub: |
|
208 |
"\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)" |
|
209 |
by (simp add: thelub_fun [symmetric] cont_lub_fun) |
|
210 |
||
211 |
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)" |
|
212 |
apply (rule monofunI) |
|
213 |
apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun]) |
|
214 |
done |
|
215 |
||
216 |
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)" |
|
35914 | 217 |
apply (rule contI2) |
25786 | 218 |
apply (erule cont2mono [THEN mono2mono_fun]) |
219 |
apply (simp add: cont2contlubE) |
|
220 |
apply (simp add: thelub_fun ch2ch_cont) |
|
221 |
done |
|
222 |
||
223 |
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *} |
|
224 |
||
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset
|
225 |
lemma mono2mono_lambda: |
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset
|
226 |
assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f" |
25786 | 227 |
apply (rule monofunI) |
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
|
228 |
apply (rule fun_belowI) |
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset
|
229 |
apply (erule monofunE [OF f]) |
25786 | 230 |
done |
231 |
||
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset
|
232 |
lemma cont2cont_lambda [simp]: |
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset
|
233 |
assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f" |
35914 | 234 |
apply (rule contI2) |
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset
|
235 |
apply (simp add: mono2mono_lambda cont2mono f) |
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
|
236 |
apply (rule fun_belowI) |
35914 | 237 |
apply (simp add: thelub_fun cont2contlubE [OF f]) |
25786 | 238 |
done |
239 |
||
240 |
text {* What D.A.Schmidt calls continuity of abstraction; never used here *} |
|
241 |
||
242 |
lemma contlub_lambda: |
|
243 |
"(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo)) |
|
244 |
\<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))" |
|
245 |
by (simp add: thelub_fun ch2ch_lambda) |
|
246 |
||
247 |
lemma contlub_abstraction: |
|
248 |
"\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow> |
|
249 |
(\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))" |
|
250 |
apply (rule thelub_fun [symmetric]) |
|
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset
|
251 |
apply (simp add: ch2ch_cont) |
25786 | 252 |
done |
253 |
||
254 |
lemma mono2mono_app: |
|
255 |
"\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))" |
|
256 |
apply (rule monofunI) |
|
257 |
apply (simp add: monofun_fun monofunE) |
|
258 |
done |
|
259 |
||
260 |
lemma cont2cont_app: |
|
261 |
"\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))" |
|
35914 | 262 |
apply (erule cont_apply [where t=t]) |
263 |
apply (erule spec) |
|
264 |
apply (erule cont2cont_fun) |
|
265 |
done |
|
25786 | 266 |
|
267 |
lemmas cont2cont_app2 = cont2cont_app [rule_format] |
|
268 |
||
269 |
lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))" |
|
270 |
by (rule cont2cont_app2 [OF cont_const]) |
|
271 |
||
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
272 |
end |