author  nipkow 
Mon, 23 Nov 2020 19:57:55 +0100  
changeset 72688  8cb82e7f1743 
parent 62175  8ffc4d0e652d 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/ex/Domain_Proofs.thy 
33591  2 
Author: Brian Huffman 
3 
*) 

4 

62175  5 
section \<open>Internal domain package proofs done manually\<close> 
33591  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 

20 
*) 

21 

22 
(********************************************************************) 

23 

62175  24 
subsection \<open>Step 1: Define the new type combinators\<close> 
33591  25 

62175  26 
text \<open>Start with the onestep nonrecursive version\<close> 
33591  27 

28 
definition 

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

29 
foo_bar_baz_deflF :: 
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
40774
diff
changeset

30 
"udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl" 
33591  31 
where 
40327  32 
"foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
41437  33 
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2)) 
34 
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr)) 

35 
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))" 

33591  36 

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

37 
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

38 
"foo_bar_baz_deflF\<cdot>a\<cdot>t = 
41437  39 
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t)))) 
40 
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr)) 

41 
, 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

42 
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

43 
by (simp add: split_def) 
33591  44 

62175  45 
text \<open>Individual type combinators are projected from the fixed point.\<close> 
33591  46 

41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
40774
diff
changeset

47 
definition foo_defl :: "udom defl \<rightarrow> udom defl" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

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

41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
40774
diff
changeset

50 
definition bar_defl :: "udom defl \<rightarrow> udom defl" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

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

41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
40774
diff
changeset

53 
definition baz_defl :: "udom defl \<rightarrow> udom defl" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

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

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

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

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

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

60 
unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all 
36132  61 

62175  62 
text \<open>Unfold rules for each combinator.\<close> 
33591  63 

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

64 
lemma foo_defl_unfold: 
41437  65 
"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)))" 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

66 
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) 
33591  67 

41437  68 
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

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

41437  71 
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

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

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

75 
how the fixrec package works." 

76 

77 
(********************************************************************) 

78 

62175  79 
subsection \<open>Step 2: Define types, prove class instances\<close> 
33591  80 

62175  81 
text \<open>Use \<open>pcpodef\<close> with the appropriate type combinator.\<close> 
33591  82 

49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
44066
diff
changeset

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

84 
by (rule defl_set_bottom, rule adm_defl_set) 
33591  85 

49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
44066
diff
changeset

86 
pcpodef 'a bar = "defl_set (bar_defl\<cdot>DEFL('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 

49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
44066
diff
changeset

89 
pcpodef 'a baz = "defl_set (baz_defl\<cdot>DEFL('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 

62175  92 
text \<open>Prove rep instance using lemma \<open>typedef_rep_class\<close>.\<close> 
33591  93 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

94 
instantiation foo :: ("domain") "domain" 
33591  95 
begin 
96 

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

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

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

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

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

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

41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
40774
diff
changeset

103 
definition defl_foo :: "'a foo itself \<Rightarrow> udom defl" 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

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

105 

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

106 
definition 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

107 
"(liftemb :: 'a foo u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb" 
40491
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 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

110 
"(liftprj :: udom u \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj" 
40491
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 
41436  113 
"liftdefl \<equiv> \<lambda>(t::'a foo itself). liftdefl_of\<cdot>DEFL('a foo)" 
33591  114 

115 
instance 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

116 
apply (rule typedef_domain_class) 
33591  117 
apply (rule type_definition_foo) 
118 
apply (rule below_foo_def) 

119 
apply (rule emb_foo_def) 

120 
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

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

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

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

124 
apply (rule liftdefl_foo_def) 
33591  125 
done 
126 

127 
end 

128 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

129 
instantiation bar :: ("domain") "domain" 
33591  130 
begin 
131 

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

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

133 
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)" 
33591  134 

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

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

136 
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))" 
33591  137 

41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
40774
diff
changeset

138 
definition defl_bar :: "'a bar itself \<Rightarrow> udom defl" 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

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

140 

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

141 
definition 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

142 
"(liftemb :: 'a bar u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb" 
40491
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 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

145 
"(liftprj :: udom u \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj" 
40491
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 
41436  148 
"liftdefl \<equiv> \<lambda>(t::'a bar itself). liftdefl_of\<cdot>DEFL('a bar)" 
33591  149 

150 
instance 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

151 
apply (rule typedef_domain_class) 
33591  152 
apply (rule type_definition_bar) 
153 
apply (rule below_bar_def) 

154 
apply (rule emb_bar_def) 

155 
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

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

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

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

159 
apply (rule liftdefl_bar_def) 
33591  160 
done 
161 

162 
end 

163 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

164 
instantiation baz :: ("domain") "domain" 
33591  165 
begin 
166 

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

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

168 
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)" 
33591  169 

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

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

171 
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))" 
33591  172 

41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
40774
diff
changeset

173 
definition defl_baz :: "'a baz itself \<Rightarrow> udom defl" 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

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

175 

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

176 
definition 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

177 
"(liftemb :: 'a baz u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb" 
40491
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 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

180 
"(liftprj :: udom u \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj" 
40491
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 
41436  183 
"liftdefl \<equiv> \<lambda>(t::'a baz itself). liftdefl_of\<cdot>DEFL('a baz)" 
33591  184 

185 
instance 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

186 
apply (rule typedef_domain_class) 
33591  187 
apply (rule type_definition_baz) 
188 
apply (rule below_baz_def) 

189 
apply (rule emb_baz_def) 

190 
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

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

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

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

194 
apply (rule liftdefl_baz_def) 
33591  195 
done 
196 

197 
end 

198 

62175  199 
text \<open>Prove DEFL rules using lemma \<open>typedef_DEFL\<close>.\<close> 
33591  200 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

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

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

203 
apply (rule defl_foo_def) 
33591  204 
done 
205 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

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

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

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

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

210 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

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

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

213 
apply (rule defl_baz_def) 
33591  214 
done 
215 

62175  216 
text \<open>Prove DEFL equations using type combinator unfold lemmas.\<close> 
33591  217 

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

218 
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

219 
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

220 
by (rule foo_defl_unfold) 
33591  221 

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

222 
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

223 
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

224 
by (rule bar_defl_unfold) 
33591  225 

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

226 
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

227 
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

228 
by (rule baz_defl_unfold) 
33591  229 

230 
(********************************************************************) 

231 

62175  232 
subsection \<open>Step 3: Define rep and abs functions\<close> 
33591  233 

62175  234 
text \<open>Define them all using \<open>prj\<close> and \<open>emb\<close>!\<close> 
33591  235 

236 
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

237 
where "foo_rep \<equiv> prj oo emb" 
33591  238 

239 
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

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

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

242 
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

243 
where "bar_rep \<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_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

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

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

248 
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

249 
where "baz_rep \<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_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

252 
where "baz_abs \<equiv> prj oo emb" 
33779  253 

62175  254 
text \<open>Prove isomorphism rules.\<close> 
33779  255 

256 
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

257 
by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def]) 
33779  258 

259 
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

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

262 
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

263 
by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def]) 
33779  264 

265 
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

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

268 
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

269 
by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def]) 
33779  270 

271 
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

272 
by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def]) 
33591  273 

62175  274 
text \<open>Prove isodefl rules using \<open>isodefl_coerce\<close>.\<close> 
33591  275 

276 
lemma isodefl_foo_abs: 

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

278 
by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def]) 
33591  279 

280 
lemma isodefl_bar_abs: 

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

282 
by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def]) 
33591  283 

284 
lemma isodefl_baz_abs: 

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

286 
by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def]) 
33591  287 

288 
(********************************************************************) 

289 

62175  290 
subsection \<open>Step 4: Define map functions, prove isodefl property\<close> 
33591  291 

62175  292 
text \<open>Start with the onestep nonrecursive version.\<close> 
33591  293 

62175  294 
text \<open>Note that the type of the map function depends on which 
295 
variables are used in positive and negative positions.\<close> 

33591  296 

297 
definition 

298 
foo_bar_baz_mapF :: 

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

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

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

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

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

307 
oo foo_rep 

308 
, 

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

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

311 
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

312 
)))" 
33591  313 

314 
lemma foo_bar_baz_mapF_beta: 

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

316 
( 

317 
foo_abs oo 

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

319 
oo foo_rep 

320 
, 

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

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

323 
baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep 
33591  324 
)" 
325 
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

326 
by (simp add: split_def) 
33591  327 

62175  328 
text \<open>Individual map functions are projected from the fixed point.\<close> 
33591  329 

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

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

332 

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

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

335 

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

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

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

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

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

343 
unfolding foo_map_def bar_map_def baz_map_def by simp_all 

344 

62175  345 
text \<open>Prove isodefl rules for all map functions simultaneously.\<close> 
33591  346 

347 
lemma isodefl_foo_bar_baz: 

41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

348 
assumes isodefl_d: "isodefl d t" 
33591  349 
shows 
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset

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

351 
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

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

354 
apply (rule parallel_fix_ind) 
33591  355 
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id) 
356 
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms) 

357 
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

358 
foo_bar_baz_deflF_beta 
33591  359 
fst_conv snd_conv) 
360 
apply (elim conjE) 

361 
apply (intro 

362 
conjI 

363 
isodefl_foo_abs 

364 
isodefl_bar_abs 

365 
isodefl_baz_abs 

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

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

367 
isodefl_ID_DEFL isodefl_LIFTDEFL 
33591  368 
isodefl_d 
369 
) 

370 
apply assumption+ 

371 
done 

372 

373 
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1] 

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

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

376 

62175  377 
text \<open>Prove map ID lemmas, using isodefl_DEFL_imp_ID\<close> 
33591  378 

379 
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

380 
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

381 
apply (subst DEFL_foo) 
33591  382 
apply (rule isodefl_foo) 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

383 
apply (rule isodefl_ID_DEFL) 
33591  384 
done 
385 

386 
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

387 
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

388 
apply (subst DEFL_bar) 
33591  389 
apply (rule isodefl_bar) 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

390 
apply (rule isodefl_ID_DEFL) 
33591  391 
done 
392 

393 
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

394 
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

395 
apply (subst DEFL_baz) 
33591  396 
apply (rule isodefl_baz) 
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset

397 
apply (rule isodefl_ID_DEFL) 
33591  398 
done 
399 

400 
(********************************************************************) 

401 

62175  402 
subsection \<open>Step 5: Define take functions, prove lubtake lemmas\<close> 
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset

403 

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

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

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

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

408 
where 
36132  409 
"foo_bar_baz_takeF = (\<Lambda> p. 
410 
( foo_abs oo 

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

412 
oo foo_rep 

413 
, bar_abs oo 

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

415 
, baz_abs oo 

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

417 
))" 

418 

419 
lemma foo_bar_baz_takeF_beta: 

420 
"foo_bar_baz_takeF\<cdot>p = 

421 
( foo_abs oo 

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

423 
oo foo_rep 

424 
, bar_abs oo 

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

426 
, baz_abs oo 

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

428 
)" 

429 
unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp) 

430 

431 
definition 

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

433 
where 

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

435 

436 
definition 

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

438 
where 

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

33591  440 

36132  441 
definition 
442 
baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz" 

443 
where 

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

445 

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

447 
unfolding foo_take_def bar_take_def baz_take_def 

448 
by (intro ch2ch_fst ch2ch_snd chain_iterate)+ 

449 

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

451 
unfolding foo_take_def bar_take_def baz_take_def 

452 
by (simp only: iterate_0 fst_strict snd_strict)+ 

453 

454 
lemma take_Suc_thms: 

455 
"foo_take (Suc n) = 

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

457 
"bar_take (Suc n) = 

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

459 
"baz_take (Suc n) = 

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

461 
unfolding foo_take_def bar_take_def baz_take_def 

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

463 

464 
lemma lub_take_lemma: 

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

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

40771  467 
apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms) 
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58880
diff
changeset

468 
apply (simp only: map_apply_thms prod.collapse) 
36132  469 
apply (simp only: fix_def2) 
470 
apply (rule lub_eq) 

471 
apply (rule nat.induct) 

472 
apply (simp only: iterate_0 Pair_strict take_0_thms) 

44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
42151
diff
changeset

473 
apply (simp only: iterate_Suc prod_eq_iff fst_conv snd_conv 
36132  474 
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

475 
done 
33591  476 

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

479 
using lub_take_lemma 

480 
apply (elim Pair_inject) 

481 
apply assumption 

482 
done 

33591  483 

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

486 
using lub_take_lemma 

487 
apply (elim Pair_inject) 

488 
apply assumption 

489 
done 

33591  490 

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

493 
using lub_take_lemma 

494 
apply (elim Pair_inject) 

495 
apply assumption 

496 
done 

33591  497 

498 
end 