author  wenzelm 
Fri, 13 May 2016 20:24:10 +0200  
changeset 63092  a949b2a5f51d 
parent 61799  4cf66f21b764 
child 63343  fb5d8a50c641 
permissions  rwrr 
47308  1 
(* Title: HOL/Lifting.thy 
2 
Author: Brian Huffman and Ondrej Kuncar 

3 
Author: Cezary Kaliszyk and Christian Urban 

4 
*) 

5 

60758  6 
section \<open>Lifting package\<close> 
47308  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 

60758  17 
subsection \<open>Function map\<close> 
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 

60758  27 
subsection \<open>Quotient Predicate\<close> 
47308  28 

29 
definition 

30 
"Quotient R Abs Rep T \<longleftrightarrow> 

58186  31 
(\<forall>a. Abs (Rep a) = a) \<and> 
47308  32 
(\<forall>a. R (Rep a) (Rep a)) \<and> 
33 
(\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and> 

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

35 

36 
lemma QuotientI: 

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

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

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

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

41 
shows "Quotient R Abs Rep T" 

42 
using assms unfolding Quotient_def by blast 

43 

47536  44 
context 
45 
fixes R Abs Rep T 

47308  46 
assumes a: "Quotient R Abs Rep T" 
47536  47 
begin 
48 

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

50 
using a unfolding Quotient_def 

47308  51 
by simp 
52 

47536  53 
lemma Quotient_rep_reflp: "R (Rep a) (Rep a)" 
54 
using a unfolding Quotient_def 

47308  55 
by blast 
56 

57 
lemma Quotient_rel: 

61799  58 
"R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" \<comment> \<open>orientation does not loop on rewriting\<close> 
47536  59 
using a unfolding Quotient_def 
47308  60 
by blast 
61 

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

65 

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

68 
by fast 

69 

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

71 
using a unfolding Quotient_def 

72 
by fast 

73 

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

75 
using a unfolding Quotient_def 

76 
by metis 

77 

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

47308  79 
using a unfolding Quotient_def 
80 
by blast 

81 

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

82 
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

83 
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

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

85 

58186  86 
lemma Quotient_rep_abs_fold_unmap: 
87 
assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' 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:
47936
diff
changeset

88 
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

89 
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

90 
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

91 
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

92 
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

93 

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

94 
lemma Quotient_Rep_eq: 
58186  95 
assumes "x' \<equiv> Abs 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:
47936
diff
changeset

96 
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

97 
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

98 

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

101 
by blast 

102 

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

103 
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

104 
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

105 
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

106 
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

107 
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

108 
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

109 
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

110 

47536  111 
lemma Quotient_symp: "symp R" 
47308  112 
using a unfolding Quotient_def using sympI by (metis (full_types)) 
113 

47536  114 
lemma Quotient_transp: "transp R" 
47308  115 
using a unfolding Quotient_def using transpI by (metis (full_types)) 
116 

47536  117 
lemma Quotient_part_equivp: "part_equivp R" 
118 
by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI) 

119 

120 
end 

47308  121 

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

58186  123 
unfolding Quotient_def by simp 
47308  124 

60758  125 
text \<open>TODO: Use one of these alternatives as the real definition.\<close> 
47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

126 

47308  127 
lemma Quotient_alt_def: 
128 
"Quotient R Abs Rep T \<longleftrightarrow> 

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

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

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

132 
apply safe 

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

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

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

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

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

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

139 
apply (rule QuotientI) 

140 
apply simp 

141 
apply metis 

142 
apply simp 

143 
apply (rule ext, rule ext, metis) 

144 
done 

145 

146 
lemma Quotient_alt_def2: 

147 
"Quotient R Abs Rep T \<longleftrightarrow> 

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

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

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

151 
unfolding Quotient_alt_def by (safe, metis+) 

152 

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

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

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

155 
(\<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

156 
(\<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

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

158 

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

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

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

161 
(\<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

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

163 

56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56519
diff
changeset

164 
lemma Quotient_alt_def5: 
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56519
diff
changeset

165 
"Quotient R Abs Rep T \<longleftrightarrow> 
57398  166 
T \<le> BNF_Def.Grp UNIV Abs \<and> BNF_Def.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>" 
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56519
diff
changeset

167 
unfolding Quotient_alt_def4 Grp_def by blast 
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56519
diff
changeset

168 

47308  169 
lemma fun_quotient: 
170 
assumes 1: "Quotient R1 abs1 rep1 T1" 

171 
assumes 2: "Quotient R2 abs2 rep2 T2" 

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

173 
using assms unfolding Quotient_alt_def2 

55945  174 
unfolding rel_fun_def fun_eq_iff map_fun_apply 
47308  175 
by (safe, metis+) 
176 

177 
lemma apply_rsp: 

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

179 
assumes q: "Quotient R1 Abs1 Rep1 T1" 

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

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

55945  182 
using a by (auto elim: rel_funE) 
47308  183 

184 
lemma apply_rsp': 

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

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

55945  187 
using a by (auto elim: rel_funE) 
47308  188 

189 
lemma apply_rsp'': 

190 
assumes "Quotient R Abs Rep T" 

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

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

193 
proof  

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

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

196 
qed 

197 

60758  198 
subsection \<open>Quotient composition\<close> 
47308  199 

200 
lemma Quotient_compose: 

201 
assumes 1: "Quotient R1 Abs1 Rep1 T1" 

202 
assumes 2: "Quotient R2 Abs2 Rep2 T2" 

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

51994  204 
using assms unfolding Quotient_alt_def4 by fastforce 
47308  205 

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

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

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

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

209 

60758  210 
subsection \<open>Respects predicate\<close> 
47544  211 

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

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

214 

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

216 
unfolding Respects_def by simp 

217 

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

218 
lemma UNIV_typedef_to_Quotient: 
47308  219 
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

220 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47308  221 
shows "Quotient (op =) Abs Rep T" 
222 
proof  

223 
interpret type_definition Rep Abs UNIV by fact 

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

225 
by (fastforce intro!: QuotientI fun_eq_iff) 
47308  226 
qed 
227 

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

228 
lemma UNIV_typedef_to_equivp: 
47308  229 
fixes Abs :: "'a \<Rightarrow> 'b" 
230 
and Rep :: "'b \<Rightarrow> 'a" 

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

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

233 
by (rule identity_equivp) 

234 

47354  235 
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

236 
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

237 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

238 
shows "Quotient (eq_onp (\<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

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

240 
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

241 
from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

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

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

244 

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

245 
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

246 
assumes "type_definition Rep Abs S" 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

247 
shows "part_equivp (eq_onp (\<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

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

249 
interpret type_definition Rep Abs S by fact 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

250 
show "\<exists>x. eq_onp (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: eq_onp_def) 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

251 
next 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

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

253 
next 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

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

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

256 

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

257 
lemma open_typedef_to_Quotient: 
47308  258 
assumes "type_definition Rep Abs {x. P x}" 
47354  259 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

260 
shows "Quotient (eq_onp P) Abs Rep T" 
47651  261 
using typedef_to_Quotient [OF assms] by simp 
47308  262 

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

263 
lemma open_typedef_to_part_equivp: 
47308  264 
assumes "type_definition Rep Abs {x. P x}" 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

265 
shows "part_equivp (eq_onp P)" 
47651  266 
using typedef_to_part_equivp [OF assms] by simp 
47308  267 

60229
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

268 
lemma type_definition_Quotient_not_empty: "Quotient (eq_onp P) Abs Rep T \<Longrightarrow> \<exists>x. P x" 
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

269 
unfolding eq_onp_def by (drule Quotient_rep_reflp) blast 
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

270 

4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

271 
lemma type_definition_Quotient_not_empty_witness: "Quotient (eq_onp P) Abs Rep T \<Longrightarrow> P (Rep undefined)" 
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

272 
unfolding eq_onp_def by (drule Quotient_rep_reflp) blast 
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

273 

4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

274 

60758  275 
text \<open>Generating transfer rules for quotients.\<close> 
47376  276 

47537  277 
context 
278 
fixes R Abs Rep T 

279 
assumes 1: "Quotient R Abs Rep T" 

280 
begin 

47376  281 

47537  282 
lemma Quotient_right_unique: "right_unique T" 
283 
using 1 unfolding Quotient_alt_def right_unique_def by metis 

284 

285 
lemma Quotient_right_total: "right_total T" 

286 
using 1 unfolding Quotient_alt_def right_total_def by metis 

287 

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

55945  289 
using 1 unfolding Quotient_alt_def rel_fun_def by simp 
47376  290 

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

293 
using 1 assms unfolding Quotient_def by metis 

294 

47537  295 
end 
296 

60758  297 
text \<open>Generating transfer rules for total quotients.\<close> 
47376  298 

47537  299 
context 
300 
fixes R Abs Rep T 

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

302 
begin 

47376  303 

56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56517
diff
changeset

304 
lemma Quotient_left_total: "left_total T" 
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56517
diff
changeset

305 
using 1 2 unfolding Quotient_alt_def left_total_def reflp_def by auto 
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56517
diff
changeset

306 

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

309 

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

55945  311 
using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp 
47537  312 

47575  313 
lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x" 
63092  314 
using 1 2 unfolding Quotient_alt_def reflp_def by metis 
47575  315 

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

316 
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

317 
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

318 

47537  319 
end 
47376  320 

61799  321 
text \<open>Generating transfer rules for a type defined with \<open>typedef\<close>.\<close> 
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

322 

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

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

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

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

326 
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

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

328 

51994  329 
lemma typedef_left_unique: "left_unique T" 
330 
unfolding left_unique_def T_def 

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

332 

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

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

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

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

336 

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

337 
(* 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

338 

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

339 
lemma typedef_right_unique: "right_unique T" 
58186  340 
using T_def type Quotient_right_unique typedef_to_Quotient 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

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

342 

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

343 
lemma typedef_right_total: "right_total T" 
58186  344 
using T_def type Quotient_right_total typedef_to_Quotient 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

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

346 

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

347 
lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep" 
55945  348 
unfolding rel_fun_def T_def by simp 
47535
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset

349 

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

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

351 

60758  352 
text \<open>Generating the correspondence rule for a constant defined with 
61799  353 
\<open>lift_definition\<close>.\<close> 
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

354 

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

357 
shows "T c c'" 

358 
using assms by (auto dest: Quotient_cr_rel) 

359 

60758  360 
text \<open>Proving reflexivity\<close> 
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

361 

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

362 
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

363 
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

364 
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

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

366 
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

367 

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

368 
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

369 
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

370 
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

371 
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

372 
using assms unfolding left_total_def by fast 
51994  373 

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

374 
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

375 
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

376 
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

377 
shows "(T OO R OO T\<inverse>\<inverse>) \<le> op=" 
55604  378 
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

379 

56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

380 
lemma eq_onp_le_eq: 
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

381 
"eq_onp P \<le> op=" unfolding eq_onp_def by blast 
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

382 

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

383 
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

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

385 

60758  386 
text \<open>Proving a parametrized correspondence relation\<close> 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

387 

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

388 
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

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

390 

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

391 
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

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

393 

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

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

395 
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

396 
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

397 

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

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

399 
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

400 
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

401 

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

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

403 
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

404 
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

405 

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

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

407 
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

408 
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

409 

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

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

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

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

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

414 
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

415 

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

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

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

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

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

420 
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

421 

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

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

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

424 
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

425 

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

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

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

428 
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

429 

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

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

431 
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

432 
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

433 
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

434 

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

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

436 
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

437 
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

438 
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

439 

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

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

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

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

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

444 
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

445 

60758  446 
text \<open>Proving a parametrized correspondence relation\<close> 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

447 

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

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

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

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

451 
shows "(A ===> B) \<le> (C ===> D)" 
55945  452 
using assms unfolding rel_fun_def by blast 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

453 

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

454 
lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))" 
55945  455 
unfolding OO_def rel_fun_def by blast 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

456 

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

457 
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

458 
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

459 

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

460 
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

461 
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

462 

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

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

464 
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

465 
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

466 
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

467 
using functional_relation[OF 2] functional_converse_relation[OF 1] 
55945  468 
unfolding rel_fun_def OO_def 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

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

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

471 
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

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

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

474 

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

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

476 
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

477 
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

478 
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

479 
using functional_converse_relation[OF 2] functional_relation[OF 1] 
55945  480 
unfolding rel_fun_def OO_def 
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset

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

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

483 
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

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

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

486 

60758  487 
subsection \<open>Domains\<close> 
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

488 

56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

489 
lemma composed_equiv_rel_eq_onp: 
55731
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55610
diff
changeset

490 
assumes "left_unique R" 
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55610
diff
changeset

491 
assumes "(R ===> op=) P P'" 
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55610
diff
changeset

492 
assumes "Domainp R = P''" 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

493 
shows "(R OO eq_onp P' OO R\<inverse>\<inverse>) = eq_onp (inf P'' P)" 
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

494 
using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def eq_onp_def 
55731
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55610
diff
changeset

495 
fun_eq_iff by blast 
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55610
diff
changeset

496 

56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

497 
lemma composed_equiv_rel_eq_eq_onp: 
55731
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55610
diff
changeset

498 
assumes "left_unique R" 
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55610
diff
changeset

499 
assumes "Domainp R = P" 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

500 
shows "(R OO op= OO R\<inverse>\<inverse>) = eq_onp P" 
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

501 
using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def eq_onp_def 
55731
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55610
diff
changeset

502 
fun_eq_iff is_equality_def by metis 
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55610
diff
changeset

503 

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

504 
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

505 
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

506 
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

507 
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

508 
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

509 
using assms 
58186  510 
unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def 
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

511 
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

512 

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

513 
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

514 
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

515 
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

516 
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

517 
shows "Domainp (A OO B) = (inf P1 P2')" 
55945  518 
using assms unfolding rel_fun_def Domainp_iff[abs_def] OO_def 
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

519 
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

520 

53151  521 
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

522 
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

523 

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

524 
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

525 
assumes "Domainp B = P" 
53151  526 
shows "Domainp (A OO B) = (\<lambda>x. \<exists>y. A x y \<and> P y)" 
527 
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

528 

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

529 
lemma pcr_Domainp_total: 
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56517
diff
changeset

530 
assumes "left_total B" 
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

531 
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

532 
shows "Domainp (A OO B) = P" 
58186  533 
using assms unfolding left_total_def 
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

534 
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

535 

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

536 
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

537 
assumes "Quotient R Abs Rep T" 
58186  538 
shows "Domainp T = (\<lambda>x. R x x)" 
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

539 
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

540 

56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

541 
lemma eq_onp_to_Domainp: 
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

542 
assumes "Quotient (eq_onp P) Abs Rep T" 
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

543 
shows "Domainp T = P" 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

544 
by (simp add: eq_onp_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms]) 
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

545 

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

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

547 

60229
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

548 
(* needed for lifting_def_code_dt.ML (moved from Lifting_Set) *) 
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

549 
lemma right_total_UNIV_transfer: 
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

550 
assumes "right_total A" 
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

551 
shows "(rel_set A) (Collect (Domainp A)) UNIV" 
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

552 
using assms unfolding right_total_def rel_set_def Domainp_iff by blast 
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

553 

60758  554 
subsection \<open>ML setup\<close> 
47308  555 

48891  556 
ML_file "Tools/Lifting/lifting_util.ML" 
47308  557 

57961  558 
named_theorems relator_eq_onp 
559 
"theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate" 

48891  560 
ML_file "Tools/Lifting/lifting_info.ML" 
47308  561 

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

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

563 
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

564 
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

565 
lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2 
47308  566 

56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
56519
diff
changeset

567 
ML_file "Tools/Lifting/lifting_bnf.ML" 
48891  568 
ML_file "Tools/Lifting/lifting_term.ML" 
569 
ML_file "Tools/Lifting/lifting_def.ML" 

570 
ML_file "Tools/Lifting/lifting_setup.ML" 

60229
4cd6462c1fda
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
kuncar
parents:
59726
diff
changeset

571 
ML_file "Tools/Lifting/lifting_def_code_dt.ML" 
58186  572 

61630  573 
lemma pred_prod_beta: "pred_prod P Q xy \<longleftrightarrow> P (fst xy) \<and> Q (snd xy)" 
574 
by(cases xy) simp 

575 

576 
lemma pred_prod_split: "P (pred_prod Q R xy) \<longleftrightarrow> (\<forall>x y. xy = (x, y) \<longrightarrow> P (Q x \<and> R y))" 

577 
by(cases xy) simp 

578 

56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

579 
hide_const (open) POS NEG 
47308  580 

581 
end 