author  huffman 
Sat, 27 Nov 2010 13:12:10 0800  
changeset 40771  1c6f7d4b110e 
parent 40592  f432973ce0f6 
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 
(* 

12 

13 
The definitions and proofs below are for the following recursive 

14 
datatypes: 

15 

16 
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

17 
and 'a bar = Bar (lazy "'a baz \<rightarrow> tr") 
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

18 
and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr") 
33591  19 

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

20 
TODO: add another type parameter that is strict, 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

21 
to show the different handling of LIFTDEFL vs. DEFL. 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

22 

33591  23 
*) 
24 

25 
(********************************************************************) 

26 

27 
subsection {* Step 1: Define the new type combinators *} 

28 

29 
text {* Start with the onestep nonrecursive version *} 

30 

31 
definition 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

32 
foo_bar_baz_deflF :: 
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

33 
"defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl" 
33591  34 
where 
40327  35 
"foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

36 
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2)) 
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset

37 
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr)) 
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset

38 
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))" 
33591  39 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

40 
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

41 
"foo_bar_baz_deflF\<cdot>a\<cdot>t = 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

42 
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t)))) 
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset

43 
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr)) 
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset

44 
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

45 
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

46 
by (simp add: split_def) 
33591  47 

48 
text {* Individual type combinators are projected from the fixed point. *} 

49 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

50 
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

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

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

53 
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

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

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

56 
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

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

36132  59 
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

60 
"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

61 
"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

62 
"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

63 
unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all 
36132  64 

33591  65 
text {* Unfold rules for each combinator. *} 
66 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

67 
lemma foo_defl_unfold: 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

68 
"foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

69 
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) 
33591  70 

40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset

71 
lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

72 
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) 
33591  73 

40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset

74 
lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

75 
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) 
33591  76 

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

78 
how the fixrec package works." 

79 

80 
(********************************************************************) 

81 

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

83 

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

85 

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

86 
pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))" 
40038
9d061b3d8f46
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents:
40037
diff
changeset

87 
by (rule defl_set_bottom, rule adm_defl_set) 
33591  88 

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

89 
pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))" 
40038
9d061b3d8f46
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents:
40037
diff
changeset

90 
by (rule defl_set_bottom, rule adm_defl_set) 
33591  91 

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

92 
pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>LIFTDEFL('a))" 
40038
9d061b3d8f46
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents:
40037
diff
changeset

93 
by (rule defl_set_bottom, rule adm_defl_set) 
33591  94 

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

96 

40497  97 
instantiation foo :: ("domain") liftdomain 
33591  98 
begin 
99 

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

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

101 
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)" 
33591  102 

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

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

104 
where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))" 
33591  105 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

106 
definition defl_foo :: "'a foo itself \<Rightarrow> defl" 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

107 
where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)" 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

108 

6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

109 
definition 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

110 
"(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb" 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

111 

6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

112 
definition 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

113 
"(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx" 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

114 

6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

115 
definition 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

116 
"liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)" 
33591  117 

118 
instance 

40575  119 
apply (rule typedef_liftdomain_class) 
33591  120 
apply (rule type_definition_foo) 
121 
apply (rule below_foo_def) 

122 
apply (rule emb_foo_def) 

123 
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

124 
apply (rule defl_foo_def) 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

125 
apply (rule liftemb_foo_def) 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

126 
apply (rule liftprj_foo_def) 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

127 
apply (rule liftdefl_foo_def) 
33591  128 
done 
129 

130 
end 

131 

40497  132 
instantiation bar :: ("domain") liftdomain 
33591  133 
begin 
134 

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

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

136 
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)" 
33591  137 

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

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

139 
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))" 
33591  140 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

141 
definition defl_bar :: "'a bar itself \<Rightarrow> defl" 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

142 
where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)" 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

143 

6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

144 
definition 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

145 
"(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb" 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

146 

6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

147 
definition 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

148 
"(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx" 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

149 

6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

150 
definition 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

151 
"liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)" 
33591  152 

153 
instance 

40575  154 
apply (rule typedef_liftdomain_class) 
33591  155 
apply (rule type_definition_bar) 
156 
apply (rule below_bar_def) 

157 
apply (rule emb_bar_def) 

158 
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

159 
apply (rule defl_bar_def) 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

160 
apply (rule liftemb_bar_def) 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

161 
apply (rule liftprj_bar_def) 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

162 
apply (rule liftdefl_bar_def) 
33591  163 
done 
164 

165 
end 

166 

40497  167 
instantiation baz :: ("domain") liftdomain 
33591  168 
begin 
169 

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

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

171 
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)" 
33591  172 

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

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

174 
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))" 
33591  175 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

176 
definition defl_baz :: "'a baz itself \<Rightarrow> defl" 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

177 
where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)" 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

178 

6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

179 
definition 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

180 
"(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb" 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

181 

6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

182 
definition 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

183 
"(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx" 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

184 

6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

185 
definition 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

186 
"liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)" 
33591  187 

188 
instance 

40575  189 
apply (rule typedef_liftdomain_class) 
33591  190 
apply (rule type_definition_baz) 
191 
apply (rule below_baz_def) 

192 
apply (rule emb_baz_def) 

193 
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

194 
apply (rule defl_baz_def) 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

195 
apply (rule liftemb_baz_def) 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

196 
apply (rule liftprj_baz_def) 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

197 
apply (rule liftdefl_baz_def) 
33591  198 
done 
199 

200 
end 

201 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

202 
text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *} 
33591  203 

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

204 
lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

205 
apply (rule typedef_DEFL) 
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

206 
apply (rule defl_foo_def) 
33591  207 
done 
208 

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

209 
lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

210 
apply (rule typedef_DEFL) 
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

211 
apply (rule defl_bar_def) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

212 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

213 

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

214 
lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

215 
apply (rule typedef_DEFL) 
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

216 
apply (rule defl_baz_def) 
33591  217 
done 
218 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

219 
text {* Prove DEFL equations using type combinator unfold lemmas. *} 
33591  220 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

221 
lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

222 
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

223 
by (rule foo_defl_unfold) 
33591  224 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

225 
lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)" 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

226 
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

227 
by (rule bar_defl_unfold) 
33591  228 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

229 
lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)" 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

230 
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

231 
by (rule baz_defl_unfold) 
33591  232 

233 
(********************************************************************) 

234 

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

236 

40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

237 
text {* Define them all using @{text prj} and @{text emb}! *} 
33591  238 

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

40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

240 
where "foo_rep \<equiv> prj oo emb" 
33591  241 

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

40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

243 
where "foo_abs \<equiv> prj oo emb" 
33591  244 

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

245 
definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>" 
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

246 
where "bar_rep \<equiv> prj oo emb" 
33591  247 

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

248 
definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar" 
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

249 
where "bar_abs \<equiv> prj oo emb" 
33591  250 

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

251 
definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>" 
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

252 
where "baz_rep \<equiv> prj oo emb" 
33591  253 

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

254 
definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz" 
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

255 
where "baz_abs \<equiv> prj oo emb" 
33779  256 

257 
text {* Prove isomorphism rules. *} 

258 

259 
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

260 
by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def]) 
33779  261 

262 
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

263 
by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def]) 
33779  264 

265 
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

266 
by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def]) 
33779  267 

268 
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

269 
by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def]) 
33779  270 

271 
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

272 
by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def]) 
33779  273 

274 
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

275 
by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def]) 
33591  276 

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

278 

279 
lemma isodefl_foo_abs: 

280 
"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

281 
by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def]) 
33591  282 

283 
lemma isodefl_bar_abs: 

284 
"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

285 
by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def]) 
33591  286 

287 
lemma isodefl_baz_abs: 

288 
"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

289 
by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def]) 
33591  290 

291 
(********************************************************************) 

292 

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

294 

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

296 

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

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

299 

300 
definition 

301 
foo_bar_baz_mapF :: 

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

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

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

304 
('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)" 
33591  305 
where 
40327  306 
"foo_bar_baz_mapF = (\<Lambda> f. Abs_cfun (\<lambda>(d1, d2, d3). 
33591  307 
( 
308 
foo_abs oo 

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

310 
oo foo_rep 

311 
, 

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

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

314 
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

315 
)))" 
33591  316 

317 
lemma foo_bar_baz_mapF_beta: 

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

319 
( 

320 
foo_abs oo 

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

322 
oo foo_rep 

323 
, 

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

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

326 
baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep 
33591  327 
)" 
328 
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

329 
by (simp add: split_def) 
33591  330 

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

332 

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

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

335 

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

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

338 

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

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

36132  342 
lemma map_apply_thms: 
343 
"foo_map\<cdot>f = fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))" 

344 
"bar_map\<cdot>f = fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))" 

345 
"baz_map\<cdot>f = snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))" 

346 
unfolding foo_map_def bar_map_def baz_map_def by simp_all 

347 

33591  348 
text {* Prove isodefl rules for all map functions simultaneously. *} 
349 

350 
lemma isodefl_foo_bar_baz: 

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

351 
assumes isodefl_d: "isodefl (u_map\<cdot>d) t" 
33591  352 
shows 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

353 
"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

354 
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

355 
isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)" 
36132  356 
unfolding map_apply_thms defl_apply_thms 
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset

357 
apply (rule parallel_fix_ind) 
33591  358 
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id) 
359 
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms) 

360 
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

361 
foo_bar_baz_deflF_beta 
33591  362 
fst_conv snd_conv) 
363 
apply (elim conjE) 

364 
apply (intro 

365 
conjI 

366 
isodefl_foo_abs 

367 
isodefl_bar_abs 

368 
isodefl_baz_abs 

40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

369 
domain_isodefl 
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

370 
isodefl_ID_DEFL isodefl_LIFTDEFL 
33591  371 
isodefl_d 
372 
) 

373 
apply assumption+ 

374 
done 

375 

376 
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1] 

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

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

379 

39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

380 
text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *} 
33591  381 

382 
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

383 
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

384 
apply (subst DEFL_foo) 
33591  385 
apply (rule isodefl_foo) 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

386 
apply (rule isodefl_LIFTDEFL) 
33591  387 
done 
388 

389 
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

390 
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

391 
apply (subst DEFL_bar) 
33591  392 
apply (rule isodefl_bar) 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

393 
apply (rule isodefl_LIFTDEFL) 
33591  394 
done 
395 

396 
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

397 
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

398 
apply (subst DEFL_baz) 
33591  399 
apply (rule isodefl_baz) 
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset

400 
apply (rule isodefl_LIFTDEFL) 
33591  401 
done 
402 

403 
(********************************************************************) 

404 

36132  405 
subsection {* Step 5: Define take functions, prove lubtake lemmas *} 
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

406 

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

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

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

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

411 
where 
36132  412 
"foo_bar_baz_takeF = (\<Lambda> p. 
413 
( foo_abs oo 

414 
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p)))) 

415 
oo foo_rep 

416 
, bar_abs oo 

417 
u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep 

418 
, baz_abs oo 

419 
u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep 

420 
))" 

421 

422 
lemma foo_bar_baz_takeF_beta: 

423 
"foo_bar_baz_takeF\<cdot>p = 

424 
( foo_abs oo 

425 
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p)))) 

426 
oo foo_rep 

427 
, bar_abs oo 

428 
u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep 

429 
, baz_abs oo 

430 
u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep 

431 
)" 

432 
unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp) 

433 

434 
definition 

435 
foo_take :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo" 

436 
where 

437 
"foo_take = (\<lambda>n. fst (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>))" 

438 

439 
definition 

440 
bar_take :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar" 

441 
where 

442 
"bar_take = (\<lambda>n. fst (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))" 

33591  443 

36132  444 
definition 
445 
baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz" 

446 
where 

447 
"baz_take = (\<lambda>n. snd (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))" 

448 

449 
lemma chain_take_thms: "chain foo_take" "chain bar_take" "chain baz_take" 

450 
unfolding foo_take_def bar_take_def baz_take_def 

451 
by (intro ch2ch_fst ch2ch_snd chain_iterate)+ 

452 

453 
lemma take_0_thms: "foo_take 0 = \<bottom>" "bar_take 0 = \<bottom>" "baz_take 0 = \<bottom>" 

454 
unfolding foo_take_def bar_take_def baz_take_def 

455 
by (simp only: iterate_0 fst_strict snd_strict)+ 

456 

457 
lemma take_Suc_thms: 

458 
"foo_take (Suc n) = 

459 
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" 

460 
"bar_take (Suc n) = 

461 
bar_abs oo u_map\<cdot>(cfun_map\<cdot>(baz_take n)\<cdot>ID) oo bar_rep" 

462 
"baz_take (Suc n) = 

463 
baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(foo_take n))\<cdot>ID) oo baz_rep" 

464 
unfolding foo_take_def bar_take_def baz_take_def 

465 
by (simp only: iterate_Suc foo_bar_baz_takeF_beta fst_conv snd_conv)+ 

466 

467 
lemma lub_take_lemma: 

468 
"(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n) 

469 
= (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))" 

40771  470 
apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms) 
36132  471 
apply (simp only: map_apply_thms pair_collapse) 
472 
apply (simp only: fix_def2) 

473 
apply (rule lub_eq) 

474 
apply (rule nat.induct) 

475 
apply (simp only: iterate_0 Pair_strict take_0_thms) 

476 
apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv 

477 
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

478 
done 
33591  479 

36132  480 
lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID" 
481 
apply (rule trans [OF _ foo_map_ID]) 

482 
using lub_take_lemma 

483 
apply (elim Pair_inject) 

484 
apply assumption 

485 
done 

33591  486 

36132  487 
lemma lub_bar_take: "(\<Squnion>n. bar_take n) = ID" 
488 
apply (rule trans [OF _ bar_map_ID]) 

489 
using lub_take_lemma 

490 
apply (elim Pair_inject) 

491 
apply assumption 

492 
done 

33591  493 

36132  494 
lemma lub_baz_take: "(\<Squnion>n. baz_take n) = ID" 
495 
apply (rule trans [OF _ baz_map_ID]) 

496 
using lub_take_lemma 

497 
apply (elim Pair_inject) 

498 
apply assumption 

499 
done 

33591  500 

501 
end 