author  huffman 
Mon, 01 Mar 2010 23:54:50 0800  
changeset 35493  89b945fa0a31 
parent 33799  1d73cce2d630 
child 36132  6afa012a8f5c 
permissions  rwrr 
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 

11 
defaultsort rep 

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 onestep nonrecursive version *} 

29 

30 
definition 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

31 
foo_bar_baz_deflF :: 
33591  32 
"TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep" 
33 
where 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

34 
"foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

35 
( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2)) 
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

36 
, u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>REP(tr)) 
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

37 
, u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>REP(tr)))))" 
33591  38 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

39 
lemma foo_bar_baz_deflF_beta: 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

40 
"foo_bar_baz_deflF\<cdot>a\<cdot>t = 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

41 
( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t)))) 
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

42 
, u_defl\<cdot>(cfun_defl\<cdot>(snd (snd t))\<cdot>REP(tr)) 
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

43 
, u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(fst t))\<cdot>REP(tr)))" 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
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 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

49 
definition foo_defl :: "TypeRep \<rightarrow> TypeRep" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

50 
where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))" 
33591  51 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

52 
definition bar_defl :: "TypeRep \<rightarrow> TypeRep" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

53 
where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))" 
33591  54 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

55 
definition baz_defl :: "TypeRep \<rightarrow> TypeRep" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

56 
where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))" 
33591  57 

58 
text {* Unfold rules for each combinator. *} 

59 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

60 
lemma foo_defl_unfold: 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

61 
"foo_defl\<cdot>a = ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))" 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

62 
unfolding foo_defl_def bar_defl_def baz_defl_def 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

63 
by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) 
33591  64 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

65 
lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(baz_defl\<cdot>a)\<cdot>REP(tr))" 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

66 
unfolding foo_defl_def bar_defl_def baz_defl_def 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

67 
by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) 
33591  68 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

69 
lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a))\<cdot>REP(tr))" 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

70 
unfolding foo_defl_def bar_defl_def baz_defl_def 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

71 
by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) 
33591  72 

73 
text "The automation for the previous steps will be quite similar to 

74 
how the fixrec package works." 

75 

76 
(********************************************************************) 

77 

78 
subsection {* Step 2: Define types, prove class instances *} 

79 

80 
text {* Use @{text pcpodef} with the appropriate type combinator. *} 

81 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

82 
pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>REP('a)}" 
33591  83 
by (simp_all add: adm_in_deflation) 
84 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

85 
pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>REP('a)}" 
33591  86 
by (simp_all add: adm_in_deflation) 
87 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

88 
pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>REP('a)}" 
33591  89 
by (simp_all add: adm_in_deflation) 
90 

91 
text {* Prove rep instance using lemma @{text typedef_rep_class}. *} 

92 

93 
instantiation foo :: (rep) rep 

94 
begin 

95 

96 
definition emb_foo :: "'a foo \<rightarrow> udom" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

97 
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)" 
33591  98 

99 
definition prj_foo :: "udom \<rightarrow> 'a foo" 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

100 
where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>REP('a))\<cdot>y))" 
33591  101 

102 
definition approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo" 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

103 
where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_defl\<cdot>REP('a))" 
33591  104 

105 
instance 

106 
apply (rule typedef_rep_class) 

107 
apply (rule type_definition_foo) 

108 
apply (rule below_foo_def) 

109 
apply (rule emb_foo_def) 

110 
apply (rule prj_foo_def) 

111 
apply (rule approx_foo_def) 

112 
done 

113 

114 
end 

115 

116 
instantiation bar :: (rep) rep 

117 
begin 

118 

119 
definition emb_bar :: "'a bar \<rightarrow> udom" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

120 
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)" 
33591  121 

122 
definition prj_bar :: "udom \<rightarrow> 'a bar" 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

123 
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>REP('a))\<cdot>y))" 
33591  124 

125 
definition approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar" 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

126 
where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_defl\<cdot>REP('a))" 
33591  127 

128 
instance 

129 
apply (rule typedef_rep_class) 

130 
apply (rule type_definition_bar) 

131 
apply (rule below_bar_def) 

132 
apply (rule emb_bar_def) 

133 
apply (rule prj_bar_def) 

134 
apply (rule approx_bar_def) 

135 
done 

136 

137 
end 

138 

139 
instantiation baz :: (rep) rep 

140 
begin 

141 

142 
definition emb_baz :: "'a baz \<rightarrow> udom" 

33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset

143 
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)" 
33591  144 

145 
definition prj_baz :: "udom \<rightarrow> 'a baz" 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

146 
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>REP('a))\<cdot>y))" 
33591  147 

148 
definition approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz" 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

149 
where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_defl\<cdot>REP('a))" 
33591  150 

151 
instance 

152 
apply (rule typedef_rep_class) 

153 
apply (rule type_definition_baz) 

154 
apply (rule below_baz_def) 

155 
apply (rule emb_baz_def) 

156 
apply (rule prj_baz_def) 

157 
apply (rule approx_baz_def) 

158 
done 

159 

160 
end 

161 

162 
text {* Prove REP rules using lemma @{text typedef_REP}. *} 

163 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

164 
lemma REP_foo: "REP('a foo) = foo_defl\<cdot>REP('a)" 
33591  165 
apply (rule typedef_REP) 
166 
apply (rule type_definition_foo) 

167 
apply (rule below_foo_def) 

168 
apply (rule emb_foo_def) 

169 
apply (rule prj_foo_def) 

170 
done 

171 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

172 
lemma REP_bar: "REP('a bar) = bar_defl\<cdot>REP('a)" 
33591  173 
apply (rule typedef_REP) 
174 
apply (rule type_definition_bar) 

175 
apply (rule below_bar_def) 

176 
apply (rule emb_bar_def) 

177 
apply (rule prj_bar_def) 

178 
done 

179 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

180 
lemma REP_baz: "REP('a baz) = baz_defl\<cdot>REP('a)" 
33591  181 
apply (rule typedef_REP) 
182 
apply (rule type_definition_baz) 

183 
apply (rule below_baz_def) 

184 
apply (rule emb_baz_def) 

185 
apply (rule prj_baz_def) 

186 
done 

187 

188 
text {* Prove REP equations using type combinator unfold lemmas. *} 

189 

190 
lemma REP_foo': "REP('a foo) = REP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" 

191 
unfolding REP_foo REP_bar REP_baz REP_simps 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

192 
by (rule foo_defl_unfold) 
33591  193 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

194 
lemma REP_bar': "REP('a bar) = REP(('a baz \<rightarrow> tr)\<^sub>\<bottom>)" 
33591  195 
unfolding REP_foo REP_bar REP_baz REP_simps 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

196 
by (rule bar_defl_unfold) 
33591  197 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

198 
lemma REP_baz': "REP('a baz) = REP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)" 
35493  199 
unfolding REP_foo REP_bar REP_baz REP_simps REP_convex 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

200 
by (rule baz_defl_unfold) 
33591  201 

202 
(********************************************************************) 

203 

204 
subsection {* Step 3: Define rep and abs functions *} 

205 

206 
text {* Define them all using @{text coerce}! *} 

207 

208 
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" 

33779  209 
where "foo_rep \<equiv> coerce" 
33591  210 

211 
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo" 

33779  212 
where "foo_abs \<equiv> coerce" 
33591  213 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

214 
definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>" 
33779  215 
where "bar_rep \<equiv> coerce" 
33591  216 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

217 
definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar" 
33779  218 
where "bar_abs \<equiv> coerce" 
33591  219 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

220 
definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>" 
33779  221 
where "baz_rep \<equiv> coerce" 
33591  222 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

223 
definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz" 
33779  224 
where "baz_abs \<equiv> coerce" 
225 

226 
text {* Prove isomorphism rules. *} 

227 

228 
lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x" 

229 
by (rule domain_abs_iso [OF REP_foo' foo_abs_def foo_rep_def]) 

230 

231 
lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x" 

232 
by (rule domain_rep_iso [OF REP_foo' foo_abs_def foo_rep_def]) 

233 

234 
lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x" 

235 
by (rule domain_abs_iso [OF REP_bar' bar_abs_def bar_rep_def]) 

236 

237 
lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x" 

238 
by (rule domain_rep_iso [OF REP_bar' bar_abs_def bar_rep_def]) 

239 

240 
lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x" 

241 
by (rule domain_abs_iso [OF REP_baz' baz_abs_def baz_rep_def]) 

242 

243 
lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x" 

244 
by (rule domain_rep_iso [OF REP_baz' baz_abs_def baz_rep_def]) 

33591  245 

246 
text {* Prove isodefl rules using @{text isodefl_coerce}. *} 

247 

248 
lemma isodefl_foo_abs: 

249 
"isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t" 

33779  250 
by (rule isodefl_abs_rep [OF REP_foo' foo_abs_def foo_rep_def]) 
33591  251 

252 
lemma isodefl_bar_abs: 

253 
"isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t" 

33779  254 
by (rule isodefl_abs_rep [OF REP_bar' bar_abs_def bar_rep_def]) 
33591  255 

256 
lemma isodefl_baz_abs: 

257 
"isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t" 

33779  258 
by (rule isodefl_abs_rep [OF REP_baz' baz_abs_def baz_rep_def]) 
33591  259 

260 
(********************************************************************) 

261 

262 
subsection {* Step 4: Define map functions, prove isodefl property *} 

263 

264 
text {* Start with the onestep nonrecursive version. *} 

265 

266 
text {* Note that the type of the map function depends on which 

267 
variables are used in positive and negative positions. *} 

268 

269 
definition 

270 
foo_bar_baz_mapF :: 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

271 
"('a \<rightarrow> 'b) \<rightarrow> 
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

272 
('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

273 
('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)" 
33591  274 
where 
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

275 
"foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3). 
33591  276 
( 
277 
foo_abs oo 

278 
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2)) 

279 
oo foo_rep 

280 
, 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

281 
bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep 
33591  282 
, 
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

283 
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

284 
)))" 
33591  285 

286 
lemma foo_bar_baz_mapF_beta: 

287 
"foo_bar_baz_mapF\<cdot>f\<cdot>d = 

288 
( 

289 
foo_abs oo 

290 
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d)))) 

291 
oo foo_rep 

292 
, 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

293 
bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep 
33591  294 
, 
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

295 
baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep 
33591  296 
)" 
297 
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

298 
by (simp add: split_def) 
33591  299 

300 
text {* Individual map functions are projected from the fixed point. *} 

301 

302 
definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)" 

303 
where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))" 

304 

305 
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)" 

306 
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" 

307 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

308 
definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)" 
33591  309 
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" 
310 

311 
text {* Prove isodefl rules for all map functions simultaneously. *} 

312 

313 
lemma isodefl_foo_bar_baz: 

314 
assumes isodefl_d: "isodefl d t" 

315 
shows 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

316 
"isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and> 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

317 
isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and> 
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

318 
isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)" 
33591  319 
apply (simp add: foo_map_def bar_map_def baz_map_def) 
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

320 
apply (simp add: foo_defl_def bar_defl_def baz_defl_def) 
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

321 
apply (rule parallel_fix_ind) 
33591  322 
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id) 
323 
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms) 

324 
apply (simp only: foo_bar_baz_mapF_beta 

33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset

325 
foo_bar_baz_deflF_beta 
33591  326 
fst_conv snd_conv) 
327 
apply (elim conjE) 

328 
apply (intro 

329 
conjI 

330 
isodefl_foo_abs 

331 
isodefl_bar_abs 

332 
isodefl_baz_abs 

33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

333 
isodefl_ssum isodefl_sprod isodefl_ID_REP 
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

334 
isodefl_u isodefl_convex isodefl_cfun 
33591  335 
isodefl_d 
336 
) 

337 
apply assumption+ 

338 
done 

339 

340 
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1] 

341 
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1] 

342 
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2] 

343 

344 
text {* Prove map ID lemmas, using isodefl_REP_imp_ID *} 

345 

346 
lemma foo_map_ID: "foo_map\<cdot>ID = ID" 

347 
apply (rule isodefl_REP_imp_ID) 

348 
apply (subst REP_foo) 

349 
apply (rule isodefl_foo) 

350 
apply (rule isodefl_ID_REP) 

351 
done 

352 

353 
lemma bar_map_ID: "bar_map\<cdot>ID = ID" 

354 
apply (rule isodefl_REP_imp_ID) 

355 
apply (subst REP_bar) 

356 
apply (rule isodefl_bar) 

357 
apply (rule isodefl_ID_REP) 

358 
done 

359 

360 
lemma baz_map_ID: "baz_map\<cdot>ID = ID" 

361 
apply (rule isodefl_REP_imp_ID) 

362 
apply (subst REP_baz) 

363 
apply (rule isodefl_baz) 

364 
apply (rule isodefl_ID_REP) 

365 
done 

366 

367 
(********************************************************************) 

368 

369 
subsection {* Step 5: Define copy functions, prove reach lemmas *} 

370 

33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

371 
text {* Define copy functions just like the old domain package does. *} 
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 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

374 
foo_copy :: 
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" 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

377 
where 
33799  378 
"foo_copy = (\<Lambda> p. foo_abs oo 
379 
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p)))) 

33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

380 
oo foo_rep)" 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

381 

c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

382 
definition 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

383 
bar_copy :: 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

384 
"('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

385 
'a bar \<rightarrow> 'a bar" 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

386 
where 
33799  387 
"bar_copy = (\<Lambda> p. bar_abs oo 
388 
u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep)" 

33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

389 

c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

390 
definition 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

391 
baz_copy :: 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

392 
"('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

393 
'a baz \<rightarrow> 'a baz" 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

394 
where 
33799  395 
"baz_copy = (\<Lambda> p. baz_abs oo 
396 
u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep)" 

33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

397 

c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

398 
definition 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

399 
foo_bar_baz_copy :: 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

400 
"('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

401 
('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

402 
where 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

403 
"foo_bar_baz_copy = (\<Lambda> f. (foo_copy\<cdot>f, bar_copy\<cdot>f, baz_copy\<cdot>f))" 
33591  404 

405 
lemma fix_foo_bar_baz_copy: 

406 
"fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)" 

33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

407 
unfolding foo_map_def bar_map_def baz_map_def 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

408 
apply (subst beta_cfun, simp)+ 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

409 
apply (subst pair_collapse)+ 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

410 
apply (rule cfun_arg_cong) 
33799  411 
unfolding foo_bar_baz_mapF_def split_def 
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

412 
unfolding foo_bar_baz_copy_def 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

413 
unfolding foo_copy_def bar_copy_def baz_copy_def 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

414 
apply (subst beta_cfun, simp)+ 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

415 
apply (rule refl) 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

416 
done 
33591  417 

418 
lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x" 

33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

419 
unfolding fix_foo_bar_baz_copy fst_conv snd_conv 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

420 
unfolding foo_map_ID by (rule ID1) 
33591  421 

422 
lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x" 

33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

423 
unfolding fix_foo_bar_baz_copy fst_conv snd_conv 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

424 
unfolding bar_map_ID by (rule ID1) 
33591  425 

426 
lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x" 

33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

427 
unfolding fix_foo_bar_baz_copy fst_conv snd_conv 
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

428 
unfolding baz_map_ID by (rule ID1) 
33591  429 

430 
end 