author  huffman 
Tue, 19 Oct 2010 11:07:42 0700  
changeset 40038  9d061b3d8f46 
parent 40037  81e6b89d8f58 
child 40327  1dfdbd66093a 
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 

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 onestep nonrecursive 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 

40038
9d061b3d8f46
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents:
40037
diff
changeset

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

86 
by (rule defl_set_bottom, rule adm_defl_set) 
33591  87 

40038
9d061b3d8f46
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents:
40037
diff
changeset

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

89 
by (rule defl_set_bottom, rule adm_defl_set) 
33591  90 

40038
9d061b3d8f46
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents:
40037
diff
changeset

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

92 
by (rule defl_set_bottom, rule adm_defl_set) 
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 

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

203 
text {* Define them all using @{text prj} and @{text emb}! *} 
33591  204 

205 
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

206 
where "foo_rep \<equiv> prj oo emb" 
33591  207 

208 
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

209 
where "foo_abs \<equiv> prj oo emb" 
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>" 
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

212 
where "bar_rep \<equiv> prj oo emb" 
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" 
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

215 
where "bar_abs \<equiv> prj oo emb" 
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>" 
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

218 
where "baz_rep \<equiv> prj oo emb" 
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" 
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset

221 
where "baz_abs \<equiv> prj oo emb" 
33779  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 onestep nonrecursive 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 lubtake 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 