author | huffman |
Mon, 11 Oct 2010 08:32:09 -0700 | |
changeset 39989 | ad60d7311f43 |
parent 39986 | 38677db30cad |
child 40037 | 81e6b89d8f58 |
permissions | -rw-r--r-- |
33591 | 1 |
(* Title: HOLCF/ex/Domain_Proofs.thy |
2 |
Author: Brian Huffman |
|
3 |
*) |
|
4 |
||
5 |
header {* Internal domain package proofs done manually *} |
|
6 |
||
7 |
theory Domain_Proofs |
|
8 |
imports HOLCF |
|
9 |
begin |
|
10 |
||
39986 | 11 |
default_sort bifinite |
33591 | 12 |
|
13 |
(* |
|
14 |
||
15 |
The definitions and proofs below are for the following recursive |
|
16 |
datatypes: |
|
17 |
||
18 |
domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar") |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
19 |
and 'a bar = Bar (lazy "'a baz \<rightarrow> tr") |
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
20 |
and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr") |
33591 | 21 |
|
22 |
*) |
|
23 |
||
24 |
(********************************************************************) |
|
25 |
||
26 |
subsection {* Step 1: Define the new type combinators *} |
|
27 |
||
28 |
text {* Start with the one-step non-recursive version *} |
|
29 |
||
30 |
definition |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
31 |
foo_bar_baz_deflF :: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
32 |
"defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl" |
33591 | 33 |
where |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
34 |
"foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
35 |
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2)) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
36 |
, u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr)) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
37 |
, u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))" |
33591 | 38 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
39 |
lemma foo_bar_baz_deflF_beta: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
40 |
"foo_bar_baz_deflF\<cdot>a\<cdot>t = |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
41 |
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t)))) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
42 |
, u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>DEFL(tr)) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
43 |
, u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>DEFL(tr)))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
44 |
unfolding foo_bar_baz_deflF_def |
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
45 |
by (simp add: split_def) |
33591 | 46 |
|
47 |
text {* Individual type combinators are projected from the fixed point. *} |
|
48 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
49 |
definition foo_defl :: "defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
50 |
where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))" |
33591 | 51 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
52 |
definition bar_defl :: "defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
53 |
where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))" |
33591 | 54 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
55 |
definition baz_defl :: "defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
56 |
where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))" |
33591 | 57 |
|
36132 | 58 |
lemma defl_apply_thms: |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
59 |
"foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
60 |
"bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
61 |
"baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
62 |
unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all |
36132 | 63 |
|
33591 | 64 |
text {* Unfold rules for each combinator. *} |
65 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
66 |
lemma foo_defl_unfold: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
67 |
"foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
68 |
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) |
33591 | 69 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
70 |
lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>DEFL(tr))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
71 |
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) |
33591 | 72 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
73 |
lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>DEFL(tr))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
74 |
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) |
33591 | 75 |
|
76 |
text "The automation for the previous steps will be quite similar to |
|
77 |
how the fixrec package works." |
|
78 |
||
79 |
(********************************************************************) |
|
80 |
||
81 |
subsection {* Step 2: Define types, prove class instances *} |
|
82 |
||
83 |
text {* Use @{text pcpodef} with the appropriate type combinator. *} |
|
84 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
85 |
pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>DEFL('a)}" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
86 |
by (simp_all add: adm_in_defl) |
33591 | 87 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
88 |
pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>DEFL('a)}" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
89 |
by (simp_all add: adm_in_defl) |
33591 | 90 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
91 |
pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>DEFL('a)}" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
92 |
by (simp_all add: adm_in_defl) |
33591 | 93 |
|
94 |
text {* Prove rep instance using lemma @{text typedef_rep_class}. *} |
|
95 |
||
39986 | 96 |
instantiation foo :: (bifinite) bifinite |
33591 | 97 |
begin |
98 |
||
99 |
definition emb_foo :: "'a foo \<rightarrow> udom" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
100 |
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)" |
33591 | 101 |
|
102 |
definition prj_foo :: "udom \<rightarrow> 'a foo" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
103 |
where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))" |
33591 | 104 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
105 |
definition defl_foo :: "'a foo itself \<Rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
106 |
where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)" |
33591 | 107 |
|
108 |
instance |
|
109 |
apply (rule typedef_rep_class) |
|
110 |
apply (rule type_definition_foo) |
|
111 |
apply (rule below_foo_def) |
|
112 |
apply (rule emb_foo_def) |
|
113 |
apply (rule prj_foo_def) |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
114 |
apply (rule defl_foo_def) |
33591 | 115 |
done |
116 |
||
117 |
end |
|
118 |
||
39986 | 119 |
instantiation bar :: (bifinite) bifinite |
33591 | 120 |
begin |
121 |
||
122 |
definition emb_bar :: "'a bar \<rightarrow> udom" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
123 |
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)" |
33591 | 124 |
|
125 |
definition prj_bar :: "udom \<rightarrow> 'a bar" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
126 |
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))" |
33591 | 127 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
128 |
definition defl_bar :: "'a bar itself \<Rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
129 |
where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)" |
33591 | 130 |
|
131 |
instance |
|
132 |
apply (rule typedef_rep_class) |
|
133 |
apply (rule type_definition_bar) |
|
134 |
apply (rule below_bar_def) |
|
135 |
apply (rule emb_bar_def) |
|
136 |
apply (rule prj_bar_def) |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
137 |
apply (rule defl_bar_def) |
33591 | 138 |
done |
139 |
||
140 |
end |
|
141 |
||
39986 | 142 |
instantiation baz :: (bifinite) bifinite |
33591 | 143 |
begin |
144 |
||
145 |
definition emb_baz :: "'a baz \<rightarrow> udom" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
146 |
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)" |
33591 | 147 |
|
148 |
definition prj_baz :: "udom \<rightarrow> 'a baz" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
149 |
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))" |
33591 | 150 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
151 |
definition defl_baz :: "'a baz itself \<Rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
152 |
where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)" |
33591 | 153 |
|
154 |
instance |
|
155 |
apply (rule typedef_rep_class) |
|
156 |
apply (rule type_definition_baz) |
|
157 |
apply (rule below_baz_def) |
|
158 |
apply (rule emb_baz_def) |
|
159 |
apply (rule prj_baz_def) |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
160 |
apply (rule defl_baz_def) |
33591 | 161 |
done |
162 |
||
163 |
end |
|
164 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
165 |
text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *} |
33591 | 166 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
167 |
lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
168 |
apply (rule typedef_DEFL) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
169 |
apply (rule defl_foo_def) |
33591 | 170 |
done |
171 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
172 |
lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
173 |
apply (rule typedef_DEFL) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
174 |
apply (rule defl_bar_def) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset
|
175 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset
|
176 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
177 |
lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
178 |
apply (rule typedef_DEFL) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
179 |
apply (rule defl_baz_def) |
33591 | 180 |
done |
181 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
182 |
text {* Prove DEFL equations using type combinator unfold lemmas. *} |
33591 | 183 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
184 |
lemmas DEFL_simps = |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
185 |
DEFL_ssum DEFL_sprod DEFL_u DEFL_cfun |
33591 | 186 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
187 |
lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
188 |
unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
189 |
by (rule foo_defl_unfold) |
33591 | 190 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
191 |
lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
192 |
unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
193 |
by (rule bar_defl_unfold) |
33591 | 194 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
195 |
lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
196 |
unfolding DEFL_foo DEFL_bar DEFL_baz DEFL_simps DEFL_convex |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
197 |
by (rule baz_defl_unfold) |
33591 | 198 |
|
199 |
(********************************************************************) |
|
200 |
||
201 |
subsection {* Step 3: Define rep and abs functions *} |
|
202 |
||
203 |
text {* Define them all using @{text coerce}! *} |
|
204 |
||
205 |
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" |
|
33779 | 206 |
where "foo_rep \<equiv> coerce" |
33591 | 207 |
|
208 |
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo" |
|
33779 | 209 |
where "foo_abs \<equiv> coerce" |
33591 | 210 |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
211 |
definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>" |
33779 | 212 |
where "bar_rep \<equiv> coerce" |
33591 | 213 |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
214 |
definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar" |
33779 | 215 |
where "bar_abs \<equiv> coerce" |
33591 | 216 |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
217 |
definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>" |
33779 | 218 |
where "baz_rep \<equiv> coerce" |
33591 | 219 |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
220 |
definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz" |
33779 | 221 |
where "baz_abs \<equiv> coerce" |
222 |
||
223 |
text {* Prove isomorphism rules. *} |
|
224 |
||
225 |
lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
226 |
by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def]) |
33779 | 227 |
|
228 |
lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
229 |
by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def]) |
33779 | 230 |
|
231 |
lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
232 |
by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def]) |
33779 | 233 |
|
234 |
lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
235 |
by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def]) |
33779 | 236 |
|
237 |
lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
238 |
by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def]) |
33779 | 239 |
|
240 |
lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
241 |
by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def]) |
33591 | 242 |
|
243 |
text {* Prove isodefl rules using @{text isodefl_coerce}. *} |
|
244 |
||
245 |
lemma isodefl_foo_abs: |
|
246 |
"isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
247 |
by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def]) |
33591 | 248 |
|
249 |
lemma isodefl_bar_abs: |
|
250 |
"isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
251 |
by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def]) |
33591 | 252 |
|
253 |
lemma isodefl_baz_abs: |
|
254 |
"isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
255 |
by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def]) |
33591 | 256 |
|
257 |
(********************************************************************) |
|
258 |
||
259 |
subsection {* Step 4: Define map functions, prove isodefl property *} |
|
260 |
||
261 |
text {* Start with the one-step non-recursive version. *} |
|
262 |
||
263 |
text {* Note that the type of the map function depends on which |
|
264 |
variables are used in positive and negative positions. *} |
|
265 |
||
266 |
definition |
|
267 |
foo_bar_baz_mapF :: |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
268 |
"('a \<rightarrow> 'b) \<rightarrow> |
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
269 |
('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow> |
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
270 |
('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)" |
33591 | 271 |
where |
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
272 |
"foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3). |
33591 | 273 |
( |
274 |
foo_abs oo |
|
275 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2)) |
|
276 |
oo foo_rep |
|
277 |
, |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
278 |
bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep |
33591 | 279 |
, |
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
280 |
baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep |
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
281 |
)))" |
33591 | 282 |
|
283 |
lemma foo_bar_baz_mapF_beta: |
|
284 |
"foo_bar_baz_mapF\<cdot>f\<cdot>d = |
|
285 |
( |
|
286 |
foo_abs oo |
|
287 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d)))) |
|
288 |
oo foo_rep |
|
289 |
, |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
290 |
bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep |
33591 | 291 |
, |
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
292 |
baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep |
33591 | 293 |
)" |
294 |
unfolding foo_bar_baz_mapF_def |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
295 |
by (simp add: split_def) |
33591 | 296 |
|
297 |
text {* Individual map functions are projected from the fixed point. *} |
|
298 |
||
299 |
definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)" |
|
300 |
where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))" |
|
301 |
||
302 |
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)" |
|
303 |
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" |
|
304 |
||
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
305 |
definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)" |
33591 | 306 |
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" |
307 |
||
36132 | 308 |
lemma map_apply_thms: |
309 |
"foo_map\<cdot>f = fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))" |
|
310 |
"bar_map\<cdot>f = fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))" |
|
311 |
"baz_map\<cdot>f = snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))" |
|
312 |
unfolding foo_map_def bar_map_def baz_map_def by simp_all |
|
313 |
||
33591 | 314 |
text {* Prove isodefl rules for all map functions simultaneously. *} |
315 |
||
316 |
lemma isodefl_foo_bar_baz: |
|
317 |
assumes isodefl_d: "isodefl d t" |
|
318 |
shows |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
319 |
"isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and> |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
320 |
isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and> |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
321 |
isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)" |
36132 | 322 |
unfolding map_apply_thms defl_apply_thms |
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
323 |
apply (rule parallel_fix_ind) |
33591 | 324 |
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id) |
325 |
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms) |
|
326 |
apply (simp only: foo_bar_baz_mapF_beta |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
327 |
foo_bar_baz_deflF_beta |
33591 | 328 |
fst_conv snd_conv) |
329 |
apply (elim conjE) |
|
330 |
apply (intro |
|
331 |
conjI |
|
332 |
isodefl_foo_abs |
|
333 |
isodefl_bar_abs |
|
334 |
isodefl_baz_abs |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
335 |
isodefl_ssum isodefl_sprod isodefl_ID_DEFL |
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
336 |
isodefl_u isodefl_convex isodefl_cfun |
33591 | 337 |
isodefl_d |
338 |
) |
|
339 |
apply assumption+ |
|
340 |
done |
|
341 |
||
342 |
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1] |
|
343 |
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1] |
|
344 |
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2] |
|
345 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
346 |
text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *} |
33591 | 347 |
|
348 |
lemma foo_map_ID: "foo_map\<cdot>ID = ID" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
349 |
apply (rule isodefl_DEFL_imp_ID) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
350 |
apply (subst DEFL_foo) |
33591 | 351 |
apply (rule isodefl_foo) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
352 |
apply (rule isodefl_ID_DEFL) |
33591 | 353 |
done |
354 |
||
355 |
lemma bar_map_ID: "bar_map\<cdot>ID = ID" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
356 |
apply (rule isodefl_DEFL_imp_ID) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
357 |
apply (subst DEFL_bar) |
33591 | 358 |
apply (rule isodefl_bar) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
359 |
apply (rule isodefl_ID_DEFL) |
33591 | 360 |
done |
361 |
||
362 |
lemma baz_map_ID: "baz_map\<cdot>ID = ID" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
363 |
apply (rule isodefl_DEFL_imp_ID) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
364 |
apply (subst DEFL_baz) |
33591 | 365 |
apply (rule isodefl_baz) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
366 |
apply (rule isodefl_ID_DEFL) |
33591 | 367 |
done |
368 |
||
369 |
(********************************************************************) |
|
370 |
||
36132 | 371 |
subsection {* Step 5: Define take functions, prove lub-take lemmas *} |
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
372 |
|
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
373 |
definition |
36132 | 374 |
foo_bar_baz_takeF :: |
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
375 |
"('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow> |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
376 |
('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)" |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
377 |
where |
36132 | 378 |
"foo_bar_baz_takeF = (\<Lambda> p. |
379 |
( foo_abs oo |
|
380 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p)))) |
|
381 |
oo foo_rep |
|
382 |
, bar_abs oo |
|
383 |
u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep |
|
384 |
, baz_abs oo |
|
385 |
u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep |
|
386 |
))" |
|
387 |
||
388 |
lemma foo_bar_baz_takeF_beta: |
|
389 |
"foo_bar_baz_takeF\<cdot>p = |
|
390 |
( foo_abs oo |
|
391 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p)))) |
|
392 |
oo foo_rep |
|
393 |
, bar_abs oo |
|
394 |
u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep |
|
395 |
, baz_abs oo |
|
396 |
u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep |
|
397 |
)" |
|
398 |
unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp) |
|
399 |
||
400 |
definition |
|
401 |
foo_take :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo" |
|
402 |
where |
|
403 |
"foo_take = (\<lambda>n. fst (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>))" |
|
404 |
||
405 |
definition |
|
406 |
bar_take :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar" |
|
407 |
where |
|
408 |
"bar_take = (\<lambda>n. fst (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))" |
|
33591 | 409 |
|
36132 | 410 |
definition |
411 |
baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz" |
|
412 |
where |
|
413 |
"baz_take = (\<lambda>n. snd (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))" |
|
414 |
||
415 |
lemma chain_take_thms: "chain foo_take" "chain bar_take" "chain baz_take" |
|
416 |
unfolding foo_take_def bar_take_def baz_take_def |
|
417 |
by (intro ch2ch_fst ch2ch_snd chain_iterate)+ |
|
418 |
||
419 |
lemma take_0_thms: "foo_take 0 = \<bottom>" "bar_take 0 = \<bottom>" "baz_take 0 = \<bottom>" |
|
420 |
unfolding foo_take_def bar_take_def baz_take_def |
|
421 |
by (simp only: iterate_0 fst_strict snd_strict)+ |
|
422 |
||
423 |
lemma take_Suc_thms: |
|
424 |
"foo_take (Suc n) = |
|
425 |
foo_abs oo ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(bar_take n))) oo foo_rep" |
|
426 |
"bar_take (Suc n) = |
|
427 |
bar_abs oo u_map\<cdot>(cfun_map\<cdot>(baz_take n)\<cdot>ID) oo bar_rep" |
|
428 |
"baz_take (Suc n) = |
|
429 |
baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(foo_take n))\<cdot>ID) oo baz_rep" |
|
430 |
unfolding foo_take_def bar_take_def baz_take_def |
|
431 |
by (simp only: iterate_Suc foo_bar_baz_takeF_beta fst_conv snd_conv)+ |
|
432 |
||
433 |
lemma lub_take_lemma: |
|
434 |
"(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n) |
|
435 |
= (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))" |
|
436 |
apply (simp only: thelub_Pair [symmetric] ch2ch_Pair chain_take_thms) |
|
437 |
apply (simp only: map_apply_thms pair_collapse) |
|
438 |
apply (simp only: fix_def2) |
|
439 |
apply (rule lub_eq) |
|
440 |
apply (rule nat.induct) |
|
441 |
apply (simp only: iterate_0 Pair_strict take_0_thms) |
|
442 |
apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv |
|
443 |
foo_bar_baz_mapF_beta take_Suc_thms simp_thms) |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
444 |
done |
33591 | 445 |
|
36132 | 446 |
lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID" |
447 |
apply (rule trans [OF _ foo_map_ID]) |
|
448 |
using lub_take_lemma |
|
449 |
apply (elim Pair_inject) |
|
450 |
apply assumption |
|
451 |
done |
|
33591 | 452 |
|
36132 | 453 |
lemma lub_bar_take: "(\<Squnion>n. bar_take n) = ID" |
454 |
apply (rule trans [OF _ bar_map_ID]) |
|
455 |
using lub_take_lemma |
|
456 |
apply (elim Pair_inject) |
|
457 |
apply assumption |
|
458 |
done |
|
33591 | 459 |
|
36132 | 460 |
lemma lub_baz_take: "(\<Squnion>n. baz_take n) = ID" |
461 |
apply (rule trans [OF _ baz_map_ID]) |
|
462 |
using lub_take_lemma |
|
463 |
apply (elim Pair_inject) |
|
464 |
apply assumption |
|
465 |
done |
|
33591 | 466 |
|
467 |
end |