author  kuncar 
Thu, 20 Feb 2014 16:56:33 +0100  
changeset 55610  9066b603dff6 
parent 55604  42e4e8c2e8dc 
child 55731  66df76dd2640 
permissions  rwrr 
47308  1 
(* Title: HOL/Lifting.thy 
2 
Author: Brian Huffman and Ondrej Kuncar 

3 
Author: Cezary Kaliszyk and Christian Urban 

4 
*) 

5 

6 
header {* Lifting package *} 

7 

8 
theory Lifting 

51112  9 
imports Equiv_Relations Transfer 
47308  10 
keywords 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

11 
"parametric" and 
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
53151
diff
changeset

12 
"print_quot_maps" "print_quotients" :: diag and 
47308  13 
"lift_definition" :: thy_goal and 
53651  14 
"setup_lifting" "lifting_forget" "lifting_update" :: thy_decl 
47308  15 
begin 
16 

47325  17 
subsection {* Function map *} 
47308  18 

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

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

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

21 
interpretation lifting_syntax . 
47308  22 

23 
lemma map_fun_id: 

24 
"(id > id) = id" 

25 
by (simp add: fun_eq_iff) 

26 

51994  27 
subsection {* Other predicates on relations *} 
28 

29 
definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 

30 
where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)" 

31 

32 
lemma left_totalI: 

33 
"(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R" 

34 
unfolding left_total_def by blast 

35 

36 
lemma left_totalE: 

37 
assumes "left_total R" 

38 
obtains "(\<And>x. \<exists>y. R x y)" 

39 
using assms unfolding left_total_def by blast 

40 

53952  41 
lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)" 
42 
unfolding left_total_def right_total_def bi_total_def by blast 

43 

53927  44 
lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R" 
45 
by(simp add: left_total_def right_total_def bi_total_def) 

46 

51994  47 
definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 
48 
where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" 

49 

53952  50 
lemma left_unique_transfer [transfer_rule]: 
51 
assumes [transfer_rule]: "right_total A" 

52 
assumes [transfer_rule]: "right_total B" 

53 
assumes [transfer_rule]: "bi_unique A" 

54 
shows "((A ===> B ===> op=) ===> implies) left_unique left_unique" 

55 
using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def 

56 
by metis 

57 

58 
lemma bi_unique_iff: "bi_unique A = (right_unique A \<and> left_unique A)" 

59 
unfolding left_unique_def right_unique_def bi_unique_def by blast 

60 

53927  61 
lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R" 
62 
by(auto simp add: left_unique_def right_unique_def bi_unique_def) 

63 

64 
lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A" 

65 
unfolding left_unique_def by blast 

66 

67 
lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y" 

68 
unfolding left_unique_def by blast 

69 

52036
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

70 
lemma left_total_fun: 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

71 
"\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)" 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

72 
unfolding left_total_def fun_rel_def 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

73 
apply (rule allI, rename_tac f) 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

74 
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI) 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

75 
apply clarify 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

76 
apply (subgoal_tac "(THE x. A x y) = x", simp) 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

77 
apply (rule someI_ex) 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

78 
apply (simp) 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

79 
apply (rule the_equality) 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

80 
apply assumption 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

81 
apply (simp add: left_unique_def) 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

82 
done 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

83 

1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

84 
lemma left_unique_fun: 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

85 
"\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)" 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

86 
unfolding left_total_def left_unique_def fun_rel_def 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

87 
by (clarify, rule ext, fast) 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

88 

1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

89 
lemma left_total_eq: "left_total op=" unfolding left_total_def by blast 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

90 

1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

91 
lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast 
1aa2e40df9ff
reflexivity rules for the function type and equality
kuncar
parents:
51994
diff
changeset

92 

53944  93 
lemma [simp]: 
94 
shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A" 

95 
and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A" 

96 
by(auto simp add: left_unique_def right_unique_def) 

97 

98 
lemma [simp]: 

99 
shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A" 

100 
and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A" 

101 
by(simp_all add: left_total_def right_total_def) 

102 

47308  103 
subsection {* Quotient Predicate *} 
104 

105 
definition 

106 
"Quotient R Abs Rep T \<longleftrightarrow> 

107 
(\<forall>a. Abs (Rep a) = a) \<and> 

108 
(\<forall>a. R (Rep a) (Rep a)) \<and> 

109 
(\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and> 

110 
T = (\<lambda>x y. R x x \<and> Abs x = y)" 

111 

112 
lemma QuotientI: 

113 
assumes "\<And>a. Abs (Rep a) = a" 

114 
and "\<And>a. R (Rep a) (Rep a)" 

115 
and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s" 

116 
and "T = (\<lambda>x y. R x x \<and> Abs x = y)" 

117 
shows "Quotient R Abs Rep T" 

118 
using assms unfolding Quotient_def by blast 

119 

47536  120 
context 
121 
fixes R Abs Rep T 

47308  122 
assumes a: "Quotient R Abs Rep T" 
47536  123 
begin 
124 

125 
lemma Quotient_abs_rep: "Abs (Rep a) = a" 

126 
using a unfolding Quotient_def 

47308  127 
by simp 
128 

47536  129 
lemma Quotient_rep_reflp: "R (Rep a) (Rep a)" 
130 
using a unfolding Quotient_def 

47308  131 
by blast 
132 

133 
lemma Quotient_rel: 

47536  134 
"R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s"  {* orientation does not loop on rewriting *} 
135 
using a unfolding Quotient_def 

47308  136 
by blast 
137 

47536  138 
lemma Quotient_cr_rel: "T = (\<lambda>x y. R x x \<and> Abs x = y)" 
47308  139 
using a unfolding Quotient_def 
140 
by blast 

141 

47536  142 
lemma Quotient_refl1: "R r s \<Longrightarrow> R r r" 
143 
using a unfolding Quotient_def 

144 
by fast 

145 

146 
lemma Quotient_refl2: "R r s \<Longrightarrow> R s s" 

147 
using a unfolding Quotient_def 

148 
by fast 

149 

150 
lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b" 

151 
using a unfolding Quotient_def 

152 
by metis 

153 

154 
lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r" 

47308  155 
using a unfolding Quotient_def 
156 
by blast 

157 

55610
9066b603dff6
refactoring; generate rep_eq always, not only when it would be accepted by the code generator
kuncar
parents:
55604
diff
changeset

158 
lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> op= \<Longrightarrow> Rep (Abs t) = t" 
9066b603dff6
refactoring; generate rep_eq always, not only when it would be accepted by the code generator
kuncar
parents:
55604
diff
changeset

159 
using a unfolding Quotient_def 
9066b603dff6
refactoring; generate rep_eq always, not only when it would be accepted by the code generator
kuncar
parents:
55604
diff
changeset

160 
by blast 
9066b603dff6
refactoring; generate rep_eq always, not only when it would be accepted by the code generator
kuncar
parents:
55604
diff
changeset

161 

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:
47936
diff
changeset

162 
lemma Quotient_rep_abs_fold_unmap: 
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:
47936
diff
changeset

163 
assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" 
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:
47936
diff
changeset

164 
shows "R (Rep' x') x" 
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:
47936
diff
changeset

165 
proof  
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:
47936
diff
changeset

166 
have "R (Rep x') x" using assms(12) Quotient_rep_abs by auto 
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:
47936
diff
changeset

167 
then show ?thesis using assms(3) by simp 
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:
47936
diff
changeset

168 
qed 
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:
47936
diff
changeset

169 

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:
47936
diff
changeset

170 
lemma Quotient_Rep_eq: 
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:
47936
diff
changeset

171 
assumes "x' \<equiv> Abs x" 
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:
47936
diff
changeset

172 
shows "Rep x' \<equiv> Rep x'" 
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:
47936
diff
changeset

173 
by simp 
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:
47936
diff
changeset

174 

47536  175 
lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s" 
176 
using a unfolding Quotient_def 

177 
by blast 

178 

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:
47936
diff
changeset

179 
lemma Quotient_rel_abs2: 
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:
47936
diff
changeset

180 
assumes "R (Rep x) y" 
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:
47936
diff
changeset

181 
shows "x = Abs y" 
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:
47936
diff
changeset

182 
proof  
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:
47936
diff
changeset

183 
from assms have "Abs (Rep x) = Abs y" by (auto intro: Quotient_rel_abs) 
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:
47936
diff
changeset

184 
then show ?thesis using assms(1) by (simp add: Quotient_abs_rep) 
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:
47936
diff
changeset

185 
qed 
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:
47936
diff
changeset

186 

47536  187 
lemma Quotient_symp: "symp R" 
47308  188 
using a unfolding Quotient_def using sympI by (metis (full_types)) 
189 

47536  190 
lemma Quotient_transp: "transp R" 
47308  191 
using a unfolding Quotient_def using transpI by (metis (full_types)) 
192 

47536  193 
lemma Quotient_part_equivp: "part_equivp R" 
194 
by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI) 

195 

196 
end 

47308  197 

198 
lemma identity_quotient: "Quotient (op =) id id (op =)" 

199 
unfolding Quotient_def by simp 

200 

47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

201 
text {* TODO: Use one of these alternatives as the real definition. *} 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

202 

47308  203 
lemma Quotient_alt_def: 
204 
"Quotient R Abs Rep T \<longleftrightarrow> 

205 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> 

206 
(\<forall>b. T (Rep b) b) \<and> 

207 
(\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)" 

208 
apply safe 

209 
apply (simp (no_asm_use) only: Quotient_def, fast) 

210 
apply (simp (no_asm_use) only: Quotient_def, fast) 

211 
apply (simp (no_asm_use) only: Quotient_def, fast) 

212 
apply (simp (no_asm_use) only: Quotient_def, fast) 

213 
apply (simp (no_asm_use) only: Quotient_def, fast) 

214 
apply (simp (no_asm_use) only: Quotient_def, fast) 

215 
apply (rule QuotientI) 

216 
apply simp 

217 
apply metis 

218 
apply simp 

219 
apply (rule ext, rule ext, metis) 

220 
done 

221 

222 
lemma Quotient_alt_def2: 

223 
"Quotient R Abs Rep T \<longleftrightarrow> 

224 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> 

225 
(\<forall>b. T (Rep b) b) \<and> 

226 
(\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))" 

227 
unfolding Quotient_alt_def by (safe, metis+) 

228 

47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

229 
lemma Quotient_alt_def3: 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

230 
"Quotient R Abs Rep T \<longleftrightarrow> 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

231 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

232 
(\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))" 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

233 
unfolding Quotient_alt_def2 by (safe, metis+) 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

234 

1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

235 
lemma Quotient_alt_def4: 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

236 
"Quotient R Abs Rep T \<longleftrightarrow> 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

237 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T" 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

238 
unfolding Quotient_alt_def3 fun_eq_iff by auto 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

239 

47308  240 
lemma fun_quotient: 
241 
assumes 1: "Quotient R1 abs1 rep1 T1" 

242 
assumes 2: "Quotient R2 abs2 rep2 T2" 

243 
shows "Quotient (R1 ===> R2) (rep1 > abs2) (abs1 > rep2) (T1 ===> T2)" 

244 
using assms unfolding Quotient_alt_def2 

245 
unfolding fun_rel_def fun_eq_iff map_fun_apply 

246 
by (safe, metis+) 

247 

248 
lemma apply_rsp: 

249 
fixes f g::"'a \<Rightarrow> 'c" 

250 
assumes q: "Quotient R1 Abs1 Rep1 T1" 

251 
and a: "(R1 ===> R2) f g" "R1 x y" 

252 
shows "R2 (f x) (g y)" 

253 
using a by (auto elim: fun_relE) 

254 

255 
lemma apply_rsp': 

256 
assumes a: "(R1 ===> R2) f g" "R1 x y" 

257 
shows "R2 (f x) (g y)" 

258 
using a by (auto elim: fun_relE) 

259 

260 
lemma apply_rsp'': 

261 
assumes "Quotient R Abs Rep T" 

262 
and "(R ===> S) f f" 

263 
shows "S (f (Rep x)) (f (Rep x))" 

264 
proof  

265 
from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp) 

266 
then show ?thesis using assms(2) by (auto intro: apply_rsp') 

267 
qed 

268 

269 
subsection {* Quotient composition *} 

270 

271 
lemma Quotient_compose: 

272 
assumes 1: "Quotient R1 Abs1 Rep1 T1" 

273 
assumes 2: "Quotient R2 Abs2 Rep2 T2" 

274 
shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)" 

51994  275 
using assms unfolding Quotient_alt_def4 by fastforce 
47308  276 

47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

277 
lemma equivp_reflp2: 
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

278 
"equivp R \<Longrightarrow> reflp R" 
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

279 
by (erule equivpE) 
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

280 

47544  281 
subsection {* Respects predicate *} 
282 

283 
definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set" 

284 
where "Respects R = {x. R x x}" 

285 

286 
lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x" 

287 
unfolding Respects_def by simp 

288 

47308  289 
subsection {* Invariant *} 
290 

291 
definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 

292 
where "invariant R = (\<lambda>x y. R x \<and> x = y)" 

293 

294 
lemma invariant_to_eq: 

295 
assumes "invariant P x y" 

296 
shows "x = y" 

297 
using assms by (simp add: invariant_def) 

298 

299 
lemma fun_rel_eq_invariant: 

300 
shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))" 

301 
by (auto simp add: invariant_def fun_rel_def) 

302 

303 
lemma invariant_same_args: 

304 
shows "invariant P x x \<equiv> P x" 

305 
using assms by (auto simp add: invariant_def) 

306 

53952  307 
lemma invariant_transfer [transfer_rule]: 
308 
assumes [transfer_rule]: "bi_unique A" 

309 
shows "((A ===> op=) ===> A ===> A ===> op=) Lifting.invariant Lifting.invariant" 

310 
unfolding invariant_def[abs_def] by transfer_prover 

311 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

312 
lemma UNIV_typedef_to_Quotient: 
47308  313 
assumes "type_definition Rep Abs UNIV" 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

314 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47308  315 
shows "Quotient (op =) Abs Rep T" 
316 
proof  

317 
interpret type_definition Rep Abs UNIV by fact 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

318 
from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

319 
by (fastforce intro!: QuotientI fun_eq_iff) 
47308  320 
qed 
321 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

322 
lemma UNIV_typedef_to_equivp: 
47308  323 
fixes Abs :: "'a \<Rightarrow> 'b" 
324 
and Rep :: "'b \<Rightarrow> 'a" 

325 
assumes "type_definition Rep Abs (UNIV::'a set)" 

326 
shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)" 

327 
by (rule identity_equivp) 

328 

47354  329 
lemma typedef_to_Quotient: 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

330 
assumes "type_definition Rep Abs S" 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

331 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47501  332 
shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T" 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

333 
proof  
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

334 
interpret type_definition Rep Abs S by fact 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

335 
from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

336 
by (auto intro!: QuotientI simp: invariant_def fun_eq_iff) 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

337 
qed 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

338 

87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

339 
lemma typedef_to_part_equivp: 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

340 
assumes "type_definition Rep Abs S" 
47501  341 
shows "part_equivp (invariant (\<lambda>x. x \<in> S))" 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

342 
proof (intro part_equivpI) 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

343 
interpret type_definition Rep Abs S by fact 
47501  344 
show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def) 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

345 
next 
47501  346 
show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def) 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

347 
next 
47501  348 
show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def) 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

349 
qed 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

350 

87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

351 
lemma open_typedef_to_Quotient: 
47308  352 
assumes "type_definition Rep Abs {x. P x}" 
47354  353 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47308  354 
shows "Quotient (invariant P) Abs Rep T" 
47651  355 
using typedef_to_Quotient [OF assms] by simp 
47308  356 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

357 
lemma open_typedef_to_part_equivp: 
47308  358 
assumes "type_definition Rep Abs {x. P x}" 
359 
shows "part_equivp (invariant P)" 

47651  360 
using typedef_to_part_equivp [OF assms] by simp 
47308  361 

47376  362 
text {* Generating transfer rules for quotients. *} 
363 

47537  364 
context 
365 
fixes R Abs Rep T 

366 
assumes 1: "Quotient R Abs Rep T" 

367 
begin 

47376  368 

47537  369 
lemma Quotient_right_unique: "right_unique T" 
370 
using 1 unfolding Quotient_alt_def right_unique_def by metis 

371 

372 
lemma Quotient_right_total: "right_total T" 

373 
using 1 unfolding Quotient_alt_def right_total_def by metis 

374 

375 
lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)" 

376 
using 1 unfolding Quotient_alt_def fun_rel_def by simp 

47376  377 

47538  378 
lemma Quotient_abs_induct: 
379 
assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x" 

380 
using 1 assms unfolding Quotient_def by metis 

381 

47537  382 
end 
383 

384 
text {* Generating transfer rules for total quotients. *} 

47376  385 

47537  386 
context 
387 
fixes R Abs Rep T 

388 
assumes 1: "Quotient R Abs Rep T" and 2: "reflp R" 

389 
begin 

47376  390 

47537  391 
lemma Quotient_bi_total: "bi_total T" 
392 
using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto 

393 

394 
lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs" 

395 
using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp 

396 

47575  397 
lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x" 
398 
using 1 2 assms unfolding Quotient_alt_def reflp_def by metis 

399 

47889
29212a4bb866
lifting package produces abs_eq_iff rules for total quotients
huffman
parents:
47777
diff
changeset

400 
lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y" 
29212a4bb866
lifting package produces abs_eq_iff rules for total quotients
huffman
parents:
47777
diff
changeset

401 
using Quotient_rel [OF 1] 2 unfolding reflp_def by simp 
29212a4bb866
lifting package produces abs_eq_iff rules for total quotients
huffman
parents:
47777
diff
changeset

402 

47537  403 
end 
47376  404 

47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

405 
text {* Generating transfer rules for a type defined with @{text "typedef"}. *} 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

406 

47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

407 
context 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

408 
fixes Rep Abs A T 
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

409 
assumes type: "type_definition Rep Abs A" 
47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

410 
assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)" 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

411 
begin 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

412 

51994  413 
lemma typedef_left_unique: "left_unique T" 
414 
unfolding left_unique_def T_def 

415 
by (simp add: type_definition.Rep_inject [OF type]) 

416 

47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

417 
lemma typedef_bi_unique: "bi_unique T" 
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

418 
unfolding bi_unique_def T_def 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

419 
by (simp add: type_definition.Rep_inject [OF type]) 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

420 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

421 
(* the following two theorems are here only for convinience *) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

422 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

423 
lemma typedef_right_unique: "right_unique T" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

424 
using T_def type Quotient_right_unique typedef_to_Quotient 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

425 
by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

426 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

427 
lemma typedef_right_total: "right_total T" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

428 
using T_def type Quotient_right_total typedef_to_Quotient 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

429 
by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

430 

47535
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset

431 
lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep" 
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset

432 
unfolding fun_rel_def T_def by simp 
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset

433 

47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

434 
end 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

435 

47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

436 
text {* Generating the correspondence rule for a constant defined with 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

437 
@{text "lift_definition"}. *} 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

438 

47351  439 
lemma Quotient_to_transfer: 
440 
assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c" 

441 
shows "T c c'" 

442 
using assms by (auto dest: Quotient_cr_rel) 

443 

47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

444 
text {* Proving reflexivity *} 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

445 

7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

446 
lemma Quotient_to_left_total: 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

447 
assumes q: "Quotient R Abs Rep T" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

448 
and r_R: "reflp R" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

449 
shows "left_total T" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

450 
using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE) 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

451 

55563
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

452 
lemma Quotient_composition_ge_eq: 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

453 
assumes "left_total T" 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

454 
assumes "R \<ge> op=" 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

455 
shows "(T OO R OO T\<inverse>\<inverse>) \<ge> op=" 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

456 
using assms unfolding left_total_def by fast 
51994  457 

55563
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

458 
lemma Quotient_composition_le_eq: 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

459 
assumes "left_unique T" 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

460 
assumes "R \<le> op=" 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

461 
shows "(T OO R OO T\<inverse>\<inverse>) \<le> op=" 
55604  462 
using assms unfolding left_unique_def by blast 
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

463 

52307  464 
lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)" 
465 
unfolding left_total_def OO_def by fast 

466 

467 
lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)" 

55604  468 
unfolding left_unique_def OO_def by blast 
52307  469 

55563
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

470 
lemma invariant_le_eq: 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

471 
"invariant P \<le> op=" unfolding invariant_def by blast 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

472 

a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

473 
lemma reflp_ge_eq: 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

474 
"reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

475 

a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

476 
lemma ge_eq_refl: 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

477 
"R \<ge> op= \<Longrightarrow> R x x" by blast 
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

478 

51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

479 
text {* Proving a parametrized correspondence relation *} 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

480 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

481 
definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

482 
"POS A B \<equiv> A \<le> B" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

483 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

484 
definition NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

485 
"NEG A B \<equiv> B \<le> A" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

486 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

487 
(* 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

488 
The following two rules are here because we don't have any proper 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

489 
leftunique ant lefttotal relations. Leftunique and lefttotal 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

490 
assumptions show up in distributivity rules for the function type. 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

491 
*) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

492 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

493 
lemma bi_unique_left_unique[transfer_rule]: "bi_unique R \<Longrightarrow> left_unique R" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

494 
unfolding bi_unique_def left_unique_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

495 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

496 
lemma bi_total_left_total[transfer_rule]: "bi_total R \<Longrightarrow> left_total R" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

497 
unfolding bi_total_def left_total_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

498 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

499 
lemma pos_OO_eq: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

500 
shows "POS (A OO op=) A" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

501 
unfolding POS_def OO_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

502 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

503 
lemma pos_eq_OO: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

504 
shows "POS (op= OO A) A" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

505 
unfolding POS_def OO_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

506 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

507 
lemma neg_OO_eq: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

508 
shows "NEG (A OO op=) A" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

509 
unfolding NEG_def OO_def by auto 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

510 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

511 
lemma neg_eq_OO: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

512 
shows "NEG (op= OO A) A" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

513 
unfolding NEG_def OO_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

514 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

515 
lemma POS_trans: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

516 
assumes "POS A B" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

517 
assumes "POS B C" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

518 
shows "POS A C" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

519 
using assms unfolding POS_def by auto 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

520 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

521 
lemma NEG_trans: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

522 
assumes "NEG A B" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

523 
assumes "NEG B C" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

524 
shows "NEG A C" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

525 
using assms unfolding NEG_def by auto 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

526 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

527 
lemma POS_NEG: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

528 
"POS A B \<equiv> NEG B A" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

529 
unfolding POS_def NEG_def by auto 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

530 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

531 
lemma NEG_POS: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

532 
"NEG A B \<equiv> POS B A" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

533 
unfolding POS_def NEG_def by auto 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

534 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

535 
lemma POS_pcr_rule: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

536 
assumes "POS (A OO B) C" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

537 
shows "POS (A OO B OO X) (C OO X)" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

538 
using assms unfolding POS_def OO_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

539 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

540 
lemma NEG_pcr_rule: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

541 
assumes "NEG (A OO B) C" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

542 
shows "NEG (A OO B OO X) (C OO X)" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

543 
using assms unfolding NEG_def OO_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

544 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

545 
lemma POS_apply: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

546 
assumes "POS R R'" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

547 
assumes "R f g" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

548 
shows "R' f g" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

549 
using assms unfolding POS_def by auto 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

550 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

551 
text {* Proving a parametrized correspondence relation *} 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

552 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

553 
lemma fun_mono: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

554 
assumes "A \<ge> C" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

555 
assumes "B \<le> D" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

556 
shows "(A ===> B) \<le> (C ===> D)" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

557 
using assms unfolding fun_rel_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

558 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

559 
lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

560 
unfolding OO_def fun_rel_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

561 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

562 
lemma functional_relation: "right_unique R \<Longrightarrow> left_total R \<Longrightarrow> \<forall>x. \<exists>!y. R x y" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

563 
unfolding right_unique_def left_total_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

564 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

565 
lemma functional_converse_relation: "left_unique R \<Longrightarrow> right_total R \<Longrightarrow> \<forall>y. \<exists>!x. R x y" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

566 
unfolding left_unique_def right_total_def by blast 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

567 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

568 
lemma neg_fun_distr1: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

569 
assumes 1: "left_unique R" "right_total R" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

570 
assumes 2: "right_unique R'" "left_total R'" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

571 
shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S')) " 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

572 
using functional_relation[OF 2] functional_converse_relation[OF 1] 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

573 
unfolding fun_rel_def OO_def 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

574 
apply clarify 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

575 
apply (subst all_comm) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

576 
apply (subst all_conj_distrib[symmetric]) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

577 
apply (intro choice) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

578 
by metis 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

579 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

580 
lemma neg_fun_distr2: 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

581 
assumes 1: "right_unique R'" "left_total R'" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

582 
assumes 2: "left_unique S'" "right_total S'" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

583 
shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S'))" 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

584 
using functional_converse_relation[OF 2] functional_relation[OF 1] 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

585 
unfolding fun_rel_def OO_def 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

586 
apply clarify 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

587 
apply (subst all_comm) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

588 
apply (subst all_conj_distrib[symmetric]) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

589 
apply (intro choice) 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

590 
by metis 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

591 

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

592 
subsection {* Domains *} 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

593 

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

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

595 
assumes "Domainp B = P" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

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

597 
assumes "(A ===> op=) P' P" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

598 
shows "Domainp (A OO B) = P'" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

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

600 
unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def fun_rel_def 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

601 
by (fast intro: fun_eq_iff) 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

602 

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

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

604 
assumes "Domainp B = P2" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

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

606 
assumes "(A ===> op=) P2' P2" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

607 
shows "Domainp (A OO B) = (inf P1 P2')" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

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

609 
by (fast intro: fun_eq_iff) 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

610 

53151  611 
definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool" 
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

612 
where "rel_pred_comp R P \<equiv> \<lambda>x. \<exists>y. R x y \<and> P y" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

613 

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

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

615 
assumes "Domainp B = P" 
53151  616 
shows "Domainp (A OO B) = (\<lambda>x. \<exists>y. A x y \<and> P y)" 
617 
using assms by blast 

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

618 

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

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

620 
assumes "bi_total B" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

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

622 
shows "Domainp (A OO B) = P" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

623 
using assms unfolding bi_total_def 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

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

625 

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

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

627 
assumes "Quotient R Abs Rep T" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

628 
shows "Domainp T = (\<lambda>x. R x x)" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

629 
by (simp add: Domainp_iff[abs_def] Quotient_cr_rel[OF assms]) 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

630 

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

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

632 
assumes "Quotient (Lifting.invariant P) Abs Rep T" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

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

634 
by (simp add: invariant_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms]) 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset

635 

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

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

637 

47308  638 
subsection {* ML setup *} 
639 

48891  640 
ML_file "Tools/Lifting/lifting_util.ML" 
47308  641 

48891  642 
ML_file "Tools/Lifting/lifting_info.ML" 
47308  643 
setup Lifting_Info.setup 
644 

51994  645 
lemmas [reflexivity_rule] = 
55563
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

646 
order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

647 
Quotient_composition_ge_eq 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

648 
left_total_eq left_unique_eq left_total_composition left_unique_composition 
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

649 
left_total_fun left_unique_fun 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

650 

84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

651 
(* setup for the function type *) 
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47698
diff
changeset

652 
declare fun_quotient[quot_map] 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

653 
declare fun_mono[relator_mono] 
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

654 
lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2 
47308  655 

48891  656 
ML_file "Tools/Lifting/lifting_term.ML" 
47308  657 

48891  658 
ML_file "Tools/Lifting/lifting_def.ML" 
47308  659 

48891  660 
ML_file "Tools/Lifting/lifting_setup.ML" 
47308  661 

55563
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55083
diff
changeset

662 
hide_const (open) invariant POS NEG 
47308  663 

664 
end 