author  blanchet 
Mon, 20 Jan 2014 20:42:43 +0100  
changeset 55084  8ee9aabb2bca 
parent 53952  b2781a3ce958 
child 55415  05f5fdb8d093 
permissions  rwrr 
47325  1 
(* Title: HOL/Transfer.thy 
2 
Author: Brian Huffman, TU Muenchen 

51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

3 
Author: Ondrej Kuncar, TU Muenchen 
47325  4 
*) 
5 

6 
header {* Generic theorem transfer using relations *} 

7 

8 
theory Transfer 

55084  9 
imports Hilbert_Choice Basic_BNFs 
47325  10 
begin 
11 

12 
subsection {* Relator for function space *} 

13 

53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

14 
locale lifting_syntax 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

15 
begin 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

16 
notation fun_rel (infixr "===>" 55) 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

17 
notation map_fun (infixr ">" 55) 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

18 
end 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

19 

aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

20 
context 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

21 
begin 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

22 
interpretation lifting_syntax . 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

23 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47924
diff
changeset

24 
lemma fun_relD2: 
55084  25 
assumes "fun_rel A B f g" and "A x x" 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47924
diff
changeset

26 
shows "B (f x) (g x)" 
55084  27 
using assms by (rule fun_relD) 
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47924
diff
changeset

28 

47325  29 
lemma fun_relE: 
55084  30 
assumes "fun_rel A B f g" and "A x y" 
47325  31 
obtains "B (f x) (g y)" 
32 
using assms by (simp add: fun_rel_def) 

33 

55084  34 
lemmas fun_rel_eq = fun.rel_eq 
47325  35 

36 
lemma fun_rel_eq_rel: 

55084  37 
shows "fun_rel (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))" 
47325  38 
by (simp add: fun_rel_def) 
39 

40 

41 
subsection {* Transfer method *} 

42 

47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset

43 
text {* Explicit tag for relation membership allows for 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset

44 
backward proof methods. *} 
47325  45 

46 
definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" 

47 
where "Rel r \<equiv> r" 

48 

49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset

49 
text {* Handling of equality relations *} 
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset

50 

faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset

51 
definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset

52 
where "is_equality R \<longleftrightarrow> R = (op =)" 
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset

53 

51437
8739f8abbecb
fixing transfer tactic  unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset

54 
lemma is_equality_eq: "is_equality (op =)" 
8739f8abbecb
fixing transfer tactic  unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset

55 
unfolding is_equality_def by simp 
8739f8abbecb
fixing transfer tactic  unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset

56 

52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

57 
text {* Reverse implication for monotonicity rules *} 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

58 

acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

59 
definition rev_implies where 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

60 
"rev_implies x y \<longleftrightarrow> (y \<longrightarrow> x)" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

61 

47325  62 
text {* Handling of metalogic connectives *} 
63 

64 
definition transfer_forall where 

65 
"transfer_forall \<equiv> All" 

66 

67 
definition transfer_implies where 

68 
"transfer_implies \<equiv> op \<longrightarrow>" 

69 

47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset

70 
definition transfer_bforall :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset

71 
where "transfer_bforall \<equiv> (\<lambda>P Q. \<forall>x. P x \<longrightarrow> Q x)" 
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset

72 

47325  73 
lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))" 
74 
unfolding atomize_all transfer_forall_def .. 

75 

76 
lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)" 

77 
unfolding atomize_imp transfer_implies_def .. 

78 

47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset

79 
lemma transfer_bforall_unfold: 
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset

80 
"Trueprop (transfer_bforall P (\<lambda>x. Q x)) \<equiv> (\<And>x. P x \<Longrightarrow> Q x)" 
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset

81 
unfolding transfer_bforall_def atomize_imp atomize_all .. 
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset

82 

47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47637
diff
changeset

83 
lemma transfer_start: "\<lbrakk>P; Rel (op =) P Q\<rbrakk> \<Longrightarrow> Q" 
47325  84 
unfolding Rel_def by simp 
85 

47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47637
diff
changeset

86 
lemma transfer_start': "\<lbrakk>P; Rel (op \<longrightarrow>) P Q\<rbrakk> \<Longrightarrow> Q" 
47325  87 
unfolding Rel_def by simp 
88 

47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset

89 
lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y" 
47618
1568dadd598a
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents:
47612
diff
changeset

90 
by simp 
1568dadd598a
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents:
47612
diff
changeset

91 

52358
f4c4bcb0d564
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents:
52354
diff
changeset

92 
lemma untransfer_start: "\<lbrakk>Q; Rel (op =) P Q\<rbrakk> \<Longrightarrow> P" 
f4c4bcb0d564
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents:
52354
diff
changeset

93 
unfolding Rel_def by simp 
f4c4bcb0d564
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents:
52354
diff
changeset

94 

47325  95 
lemma Rel_eq_refl: "Rel (op =) x x" 
96 
unfolding Rel_def .. 

97 

47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset

98 
lemma Rel_app: 
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset

99 
assumes "Rel (A ===> B) f g" and "Rel A x y" 
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset

100 
shows "Rel B (f x) (g y)" 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset

101 
using assms unfolding Rel_def fun_rel_def by fast 
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset

102 

47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset

103 
lemma Rel_abs: 
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset

104 
assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)" 
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset

105 
shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)" 
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset

106 
using assms unfolding Rel_def fun_rel_def by fast 
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset

107 

53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

108 
end 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

109 

48891  110 
ML_file "Tools/transfer.ML" 
47325  111 
setup Transfer.setup 
112 

49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset

113 
declare refl [transfer_rule] 
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset

114 

47503  115 
declare fun_rel_eq [relator_eq] 
116 

47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset

117 
hide_const (open) Rel 
47325  118 

53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

119 
context 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

120 
begin 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

121 
interpretation lifting_syntax . 
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

122 

51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

123 
text {* Handling of domains *} 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

124 

a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

125 
lemma Domaimp_refl[transfer_domain_rule]: 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

126 
"Domainp T = Domainp T" .. 
47325  127 

128 
subsection {* Predicates on relations, i.e. ``class constraints'' *} 

129 

130 
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 

131 
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)" 

132 

133 
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 

134 
where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)" 

135 

136 
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 

137 
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)" 

138 

139 
definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 

140 
where "bi_unique R \<longleftrightarrow> 

141 
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and> 

142 
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" 

143 

53927  144 
lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z" 
145 
by(simp add: bi_unique_def) 

146 

147 
lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z" 

148 
by(simp add: bi_unique_def) 

149 

150 
lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A" 

151 
unfolding right_unique_def by blast 

152 

153 
lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z" 

154 
unfolding right_unique_def by blast 

155 

47325  156 
lemma right_total_alt_def: 
157 
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All" 

158 
unfolding right_total_def fun_rel_def 

159 
apply (rule iffI, fast) 

160 
apply (rule allI) 

161 
apply (drule_tac x="\<lambda>x. True" in spec) 

162 
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) 

163 
apply fast 

164 
done 

165 

166 
lemma right_unique_alt_def: 

167 
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)" 

168 
unfolding right_unique_def fun_rel_def by auto 

169 

170 
lemma bi_total_alt_def: 

171 
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All" 

172 
unfolding bi_total_def fun_rel_def 

173 
apply (rule iffI, fast) 

174 
apply safe 

175 
apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec) 

176 
apply (drule_tac x="\<lambda>y. True" in spec) 

177 
apply fast 

178 
apply (drule_tac x="\<lambda>x. True" in spec) 

179 
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) 

180 
apply fast 

181 
done 

182 

183 
lemma bi_unique_alt_def: 

184 
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)" 

185 
unfolding bi_unique_def fun_rel_def by auto 

186 

53944  187 
lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R" 
188 
by(auto simp add: bi_unique_def) 

189 

190 
lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R" 

191 
by(auto simp add: bi_total_def) 

192 

47660  193 
text {* Properties are preserved by relation composition. *} 
194 

195 
lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)" 

196 
by auto 

197 

198 
lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)" 

199 
unfolding bi_total_def OO_def by metis 

200 

201 
lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)" 

202 
unfolding bi_unique_def OO_def by metis 

203 

204 
lemma right_total_OO: 

205 
"\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)" 

206 
unfolding right_total_def OO_def by metis 

207 

208 
lemma right_unique_OO: 

209 
"\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)" 

210 
unfolding right_unique_def OO_def by metis 

211 

47325  212 

213 
subsection {* Properties of relators *} 

214 

215 
lemma right_total_eq [transfer_rule]: "right_total (op =)" 

216 
unfolding right_total_def by simp 

217 

218 
lemma right_unique_eq [transfer_rule]: "right_unique (op =)" 

219 
unfolding right_unique_def by simp 

220 

221 
lemma bi_total_eq [transfer_rule]: "bi_total (op =)" 

222 
unfolding bi_total_def by simp 

223 

224 
lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)" 

225 
unfolding bi_unique_def by simp 

226 

227 
lemma right_total_fun [transfer_rule]: 

228 
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)" 

229 
unfolding right_total_def fun_rel_def 

230 
apply (rule allI, rename_tac g) 

231 
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) 

232 
apply clarify 

233 
apply (subgoal_tac "(THE y. A x y) = y", simp) 

234 
apply (rule someI_ex) 

235 
apply (simp) 

236 
apply (rule the_equality) 

237 
apply assumption 

238 
apply (simp add: right_unique_def) 

239 
done 

240 

241 
lemma right_unique_fun [transfer_rule]: 

242 
"\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)" 

243 
unfolding right_total_def right_unique_def fun_rel_def 

244 
by (clarify, rule ext, fast) 

245 

246 
lemma bi_total_fun [transfer_rule]: 

247 
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)" 

248 
unfolding bi_total_def fun_rel_def 

249 
apply safe 

250 
apply (rename_tac f) 

251 
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI) 

252 
apply clarify 

253 
apply (subgoal_tac "(THE x. A x y) = x", simp) 

254 
apply (rule someI_ex) 

255 
apply (simp) 

256 
apply (rule the_equality) 

257 
apply assumption 

258 
apply (simp add: bi_unique_def) 

259 
apply (rename_tac g) 

260 
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) 

261 
apply clarify 

262 
apply (subgoal_tac "(THE y. A x y) = y", simp) 

263 
apply (rule someI_ex) 

264 
apply (simp) 

265 
apply (rule the_equality) 

266 
apply assumption 

267 
apply (simp add: bi_unique_def) 

268 
done 

269 

270 
lemma bi_unique_fun [transfer_rule]: 

271 
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)" 

272 
unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff 

273 
by (safe, metis, fast) 

274 

275 

47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset

276 
subsection {* Transfer rules *} 
47325  277 

53952  278 
lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)" 
279 
by auto 

280 

281 
lemma Domainp_forall_transfer [transfer_rule]: 

282 
assumes "right_total A" 

283 
shows "((A ===> op =) ===> op =) 

284 
(transfer_bforall (Domainp A)) transfer_forall" 

285 
using assms unfolding right_total_def 

286 
unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff 

287 
by metis 

288 

47684  289 
text {* Transfer rules using implication instead of equality on booleans. *} 
290 

52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

291 
lemma transfer_forall_transfer [transfer_rule]: 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

292 
"bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

293 
"right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

294 
"right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

295 
"bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

296 
"bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

297 
unfolding transfer_forall_def rev_implies_def fun_rel_def right_total_def bi_total_def 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

298 
by metis+ 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

299 

acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

300 
lemma transfer_implies_transfer [transfer_rule]: 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

301 
"(op = ===> op = ===> op = ) transfer_implies transfer_implies" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

302 
"(rev_implies ===> implies ===> implies ) transfer_implies transfer_implies" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

303 
"(rev_implies ===> op = ===> implies ) transfer_implies transfer_implies" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

304 
"(op = ===> implies ===> implies ) transfer_implies transfer_implies" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

305 
"(op = ===> op = ===> implies ) transfer_implies transfer_implies" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

306 
"(implies ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

307 
"(implies ===> op = ===> rev_implies) transfer_implies transfer_implies" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

308 
"(op = ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

309 
"(op = ===> op = ===> rev_implies) transfer_implies transfer_implies" 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

310 
unfolding transfer_implies_def rev_implies_def fun_rel_def by auto 
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset

311 

47684  312 
lemma eq_imp_transfer [transfer_rule]: 
313 
"right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)" 

314 
unfolding right_unique_alt_def . 

315 

47636  316 
lemma eq_transfer [transfer_rule]: 
47325  317 
assumes "bi_unique A" 
318 
shows "(A ===> A ===> op =) (op =) (op =)" 

319 
using assms unfolding bi_unique_def fun_rel_def by auto 

320 

51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

321 
lemma right_total_Ex_transfer[transfer_rule]: 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

322 
assumes "right_total A" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

323 
shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

324 
using assms unfolding right_total_def Bex_def fun_rel_def Domainp_iff[abs_def] 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

325 
by blast 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

326 

a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

327 
lemma right_total_All_transfer[transfer_rule]: 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

328 
assumes "right_total A" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

329 
shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

330 
using assms unfolding right_total_def Ball_def fun_rel_def Domainp_iff[abs_def] 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

331 
by blast 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset

332 

47636  333 
lemma All_transfer [transfer_rule]: 
47325  334 
assumes "bi_total A" 
335 
shows "((A ===> op =) ===> op =) All All" 

336 
using assms unfolding bi_total_def fun_rel_def by fast 

337 

47636  338 
lemma Ex_transfer [transfer_rule]: 
47325  339 
assumes "bi_total A" 
340 
shows "((A ===> op =) ===> op =) Ex Ex" 

341 
using assms unfolding bi_total_def fun_rel_def by fast 

342 

47636  343 
lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If" 
47325  344 
unfolding fun_rel_def by simp 
345 

47636  346 
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" 
47612  347 
unfolding fun_rel_def by simp 
348 

47636  349 
lemma id_transfer [transfer_rule]: "(A ===> A) id id" 
47625  350 
unfolding fun_rel_def by simp 
351 

47636  352 
lemma comp_transfer [transfer_rule]: 
47325  353 
"((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)" 
354 
unfolding fun_rel_def by simp 

355 

47636  356 
lemma fun_upd_transfer [transfer_rule]: 
47325  357 
assumes [transfer_rule]: "bi_unique A" 
358 
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" 

47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset

359 
unfolding fun_upd_def [abs_def] by transfer_prover 
47325  360 

47637  361 
lemma nat_case_transfer [transfer_rule]: 
362 
"(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case" 

363 
unfolding fun_rel_def by (simp split: nat.split) 

47627
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on nonbitotal relations
huffman
parents:
47625
diff
changeset

364 

47924  365 
lemma nat_rec_transfer [transfer_rule]: 
366 
"(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec" 

367 
unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all) 

368 

369 
lemma funpow_transfer [transfer_rule]: 

370 
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow" 

371 
unfolding funpow_def by transfer_prover 

372 

53952  373 
lemma mono_transfer[transfer_rule]: 
374 
assumes [transfer_rule]: "bi_total A" 

375 
assumes [transfer_rule]: "(A ===> A ===> op=) op\<le> op\<le>" 

376 
assumes [transfer_rule]: "(B ===> B ===> op=) op\<le> op\<le>" 

377 
shows "((A ===> B) ===> op=) mono mono" 

378 
unfolding mono_def[abs_def] by transfer_prover 

379 

380 
lemma right_total_relcompp_transfer[transfer_rule]: 

381 
assumes [transfer_rule]: "right_total B" 

382 
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) 

383 
(\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO" 

384 
unfolding OO_def[abs_def] by transfer_prover 

385 

386 
lemma relcompp_transfer[transfer_rule]: 

387 
assumes [transfer_rule]: "bi_total B" 

388 
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO" 

389 
unfolding OO_def[abs_def] by transfer_prover 

47627
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on nonbitotal relations
huffman
parents:
47625
diff
changeset

390 

53952  391 
lemma right_total_Domainp_transfer[transfer_rule]: 
392 
assumes [transfer_rule]: "right_total B" 

393 
shows "((A ===> B ===> op=) ===> A ===> op=) (\<lambda>T x. \<exists>y\<in>Collect(Domainp B). T x y) Domainp" 

394 
apply(subst(2) Domainp_iff[abs_def]) by transfer_prover 

395 

396 
lemma Domainp_transfer[transfer_rule]: 

397 
assumes [transfer_rule]: "bi_total B" 

398 
shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp" 

399 
unfolding Domainp_iff[abs_def] by transfer_prover 

400 

401 
lemma reflp_transfer[transfer_rule]: 

402 
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp" 

403 
"right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp" 

404 
"right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp" 

405 
"bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp" 

406 
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp" 

407 
using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def fun_rel_def 

408 
by fast+ 

409 

410 
lemma right_unique_transfer [transfer_rule]: 

411 
assumes [transfer_rule]: "right_total A" 

412 
assumes [transfer_rule]: "right_total B" 

413 
assumes [transfer_rule]: "bi_unique B" 

414 
shows "((A ===> B ===> op=) ===> implies) right_unique right_unique" 

415 
using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def 

416 
by metis 

47325  417 

418 
end 

53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

419 

aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and > local
kuncar
parents:
52358
diff
changeset

420 
end 