author | kuncar |
Mon, 13 May 2013 13:59:04 +0200 | |
changeset 51956 | a4d81cdebf8b |
parent 51374 | 84d01fd733cf |
child 51994 | 82cc2aeb7d13 |
permissions | -rw-r--r-- |
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 |
47308 | 12 |
"print_quotmaps" "print_quotients" :: diag and |
13 |
"lift_definition" :: thy_goal and |
|
14 |
"setup_lifting" :: thy_decl |
|
15 |
begin |
|
16 |
||
47325 | 17 |
subsection {* Function map *} |
47308 | 18 |
|
19 |
notation map_fun (infixr "--->" 55) |
|
20 |
||
21 |
lemma map_fun_id: |
|
22 |
"(id ---> id) = id" |
|
23 |
by (simp add: fun_eq_iff) |
|
24 |
||
25 |
subsection {* Quotient Predicate *} |
|
26 |
||
27 |
definition |
|
28 |
"Quotient R Abs Rep T \<longleftrightarrow> |
|
29 |
(\<forall>a. Abs (Rep a) = a) \<and> |
|
30 |
(\<forall>a. R (Rep a) (Rep a)) \<and> |
|
31 |
(\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and> |
|
32 |
T = (\<lambda>x y. R x x \<and> Abs x = y)" |
|
33 |
||
34 |
lemma QuotientI: |
|
35 |
assumes "\<And>a. Abs (Rep a) = a" |
|
36 |
and "\<And>a. R (Rep a) (Rep a)" |
|
37 |
and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s" |
|
38 |
and "T = (\<lambda>x y. R x x \<and> Abs x = y)" |
|
39 |
shows "Quotient R Abs Rep T" |
|
40 |
using assms unfolding Quotient_def by blast |
|
41 |
||
47536 | 42 |
context |
43 |
fixes R Abs Rep T |
|
47308 | 44 |
assumes a: "Quotient R Abs Rep T" |
47536 | 45 |
begin |
46 |
||
47 |
lemma Quotient_abs_rep: "Abs (Rep a) = a" |
|
48 |
using a unfolding Quotient_def |
|
47308 | 49 |
by simp |
50 |
||
47536 | 51 |
lemma Quotient_rep_reflp: "R (Rep a) (Rep a)" |
52 |
using a unfolding Quotient_def |
|
47308 | 53 |
by blast |
54 |
||
55 |
lemma Quotient_rel: |
|
47536 | 56 |
"R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *} |
57 |
using a unfolding Quotient_def |
|
47308 | 58 |
by blast |
59 |
||
47536 | 60 |
lemma Quotient_cr_rel: "T = (\<lambda>x y. R x x \<and> Abs x = y)" |
47308 | 61 |
using a unfolding Quotient_def |
62 |
by blast |
|
63 |
||
47536 | 64 |
lemma Quotient_refl1: "R r s \<Longrightarrow> R r r" |
65 |
using a unfolding Quotient_def |
|
66 |
by fast |
|
67 |
||
68 |
lemma Quotient_refl2: "R r s \<Longrightarrow> R s s" |
|
69 |
using a unfolding Quotient_def |
|
70 |
by fast |
|
71 |
||
72 |
lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b" |
|
73 |
using a unfolding Quotient_def |
|
74 |
by metis |
|
75 |
||
76 |
lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r" |
|
47308 | 77 |
using a unfolding Quotient_def |
78 |
by blast |
|
79 |
||
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
|
80 |
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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
have "R (Rep x') x" using assms(1-2) 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
|
85 |
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
|
86 |
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
|
87 |
|
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 |
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
|
89 |
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
|
90 |
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
|
91 |
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 |
|
47536 | 93 |
lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s" |
94 |
using a unfolding Quotient_def |
|
95 |
by blast |
|
96 |
||
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
|
97 |
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
|
98 |
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
|
99 |
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
|
100 |
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
|
101 |
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
|
102 |
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
|
103 |
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
|
104 |
|
47536 | 105 |
lemma Quotient_symp: "symp R" |
47308 | 106 |
using a unfolding Quotient_def using sympI by (metis (full_types)) |
107 |
||
47536 | 108 |
lemma Quotient_transp: "transp R" |
47308 | 109 |
using a unfolding Quotient_def using transpI by (metis (full_types)) |
110 |
||
47536 | 111 |
lemma Quotient_part_equivp: "part_equivp R" |
112 |
by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI) |
|
113 |
||
114 |
end |
|
47308 | 115 |
|
116 |
lemma identity_quotient: "Quotient (op =) id id (op =)" |
|
117 |
unfolding Quotient_def by simp |
|
118 |
||
47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset
|
119 |
text {* TODO: Use one of these alternatives as the real definition. *} |
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset
|
120 |
|
47308 | 121 |
lemma Quotient_alt_def: |
122 |
"Quotient R Abs Rep T \<longleftrightarrow> |
|
123 |
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> |
|
124 |
(\<forall>b. T (Rep b) b) \<and> |
|
125 |
(\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)" |
|
126 |
apply safe |
|
127 |
apply (simp (no_asm_use) only: Quotient_def, fast) |
|
128 |
apply (simp (no_asm_use) only: Quotient_def, fast) |
|
129 |
apply (simp (no_asm_use) only: Quotient_def, fast) |
|
130 |
apply (simp (no_asm_use) only: Quotient_def, fast) |
|
131 |
apply (simp (no_asm_use) only: Quotient_def, fast) |
|
132 |
apply (simp (no_asm_use) only: Quotient_def, fast) |
|
133 |
apply (rule QuotientI) |
|
134 |
apply simp |
|
135 |
apply metis |
|
136 |
apply simp |
|
137 |
apply (rule ext, rule ext, metis) |
|
138 |
done |
|
139 |
||
140 |
lemma Quotient_alt_def2: |
|
141 |
"Quotient R Abs Rep T \<longleftrightarrow> |
|
142 |
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> |
|
143 |
(\<forall>b. T (Rep b) b) \<and> |
|
144 |
(\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))" |
|
145 |
unfolding Quotient_alt_def by (safe, metis+) |
|
146 |
||
47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset
|
147 |
lemma Quotient_alt_def3: |
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset
|
148 |
"Quotient R Abs Rep T \<longleftrightarrow> |
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset
|
149 |
(\<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
|
150 |
(\<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
|
151 |
unfolding Quotient_alt_def2 by (safe, metis+) |
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset
|
152 |
|
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset
|
153 |
lemma Quotient_alt_def4: |
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> R = T OO conversep T" |
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset
|
156 |
unfolding Quotient_alt_def3 fun_eq_iff by auto |
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset
|
157 |
|
47308 | 158 |
lemma fun_quotient: |
159 |
assumes 1: "Quotient R1 abs1 rep1 T1" |
|
160 |
assumes 2: "Quotient R2 abs2 rep2 T2" |
|
161 |
shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)" |
|
162 |
using assms unfolding Quotient_alt_def2 |
|
163 |
unfolding fun_rel_def fun_eq_iff map_fun_apply |
|
164 |
by (safe, metis+) |
|
165 |
||
166 |
lemma apply_rsp: |
|
167 |
fixes f g::"'a \<Rightarrow> 'c" |
|
168 |
assumes q: "Quotient R1 Abs1 Rep1 T1" |
|
169 |
and a: "(R1 ===> R2) f g" "R1 x y" |
|
170 |
shows "R2 (f x) (g y)" |
|
171 |
using a by (auto elim: fun_relE) |
|
172 |
||
173 |
lemma apply_rsp': |
|
174 |
assumes a: "(R1 ===> R2) f g" "R1 x y" |
|
175 |
shows "R2 (f x) (g y)" |
|
176 |
using a by (auto elim: fun_relE) |
|
177 |
||
178 |
lemma apply_rsp'': |
|
179 |
assumes "Quotient R Abs Rep T" |
|
180 |
and "(R ===> S) f f" |
|
181 |
shows "S (f (Rep x)) (f (Rep x))" |
|
182 |
proof - |
|
183 |
from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp) |
|
184 |
then show ?thesis using assms(2) by (auto intro: apply_rsp') |
|
185 |
qed |
|
186 |
||
187 |
subsection {* Quotient composition *} |
|
188 |
||
189 |
lemma Quotient_compose: |
|
190 |
assumes 1: "Quotient R1 Abs1 Rep1 T1" |
|
191 |
assumes 2: "Quotient R2 Abs2 Rep2 T2" |
|
192 |
shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)" |
|
47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset
|
193 |
using assms unfolding Quotient_alt_def4 by (auto intro!: ext) |
47308 | 194 |
|
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset
|
195 |
lemma equivp_reflp2: |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset
|
196 |
"equivp R \<Longrightarrow> reflp R" |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset
|
197 |
by (erule equivpE) |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset
|
198 |
|
47544 | 199 |
subsection {* Respects predicate *} |
200 |
||
201 |
definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set" |
|
202 |
where "Respects R = {x. R x x}" |
|
203 |
||
204 |
lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x" |
|
205 |
unfolding Respects_def by simp |
|
206 |
||
47308 | 207 |
subsection {* Invariant *} |
208 |
||
209 |
definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
210 |
where "invariant R = (\<lambda>x y. R x \<and> x = y)" |
|
211 |
||
212 |
lemma invariant_to_eq: |
|
213 |
assumes "invariant P x y" |
|
214 |
shows "x = y" |
|
215 |
using assms by (simp add: invariant_def) |
|
216 |
||
217 |
lemma fun_rel_eq_invariant: |
|
218 |
shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))" |
|
219 |
by (auto simp add: invariant_def fun_rel_def) |
|
220 |
||
221 |
lemma invariant_same_args: |
|
222 |
shows "invariant P x x \<equiv> P x" |
|
223 |
using assms by (auto simp add: invariant_def) |
|
224 |
||
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
225 |
lemma UNIV_typedef_to_Quotient: |
47308 | 226 |
assumes "type_definition Rep Abs UNIV" |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
227 |
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |
47308 | 228 |
shows "Quotient (op =) Abs Rep T" |
229 |
proof - |
|
230 |
interpret type_definition Rep Abs UNIV by fact |
|
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
231 |
from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
232 |
by (fastforce intro!: QuotientI fun_eq_iff) |
47308 | 233 |
qed |
234 |
||
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
235 |
lemma UNIV_typedef_to_equivp: |
47308 | 236 |
fixes Abs :: "'a \<Rightarrow> 'b" |
237 |
and Rep :: "'b \<Rightarrow> 'a" |
|
238 |
assumes "type_definition Rep Abs (UNIV::'a set)" |
|
239 |
shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)" |
|
240 |
by (rule identity_equivp) |
|
241 |
||
47354 | 242 |
lemma typedef_to_Quotient: |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
243 |
assumes "type_definition Rep Abs S" |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
244 |
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |
47501 | 245 |
shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T" |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
246 |
proof - |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
247 |
interpret type_definition Rep Abs S by fact |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
248 |
from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
249 |
by (auto intro!: QuotientI simp: invariant_def fun_eq_iff) |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
250 |
qed |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
251 |
|
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
252 |
lemma typedef_to_part_equivp: |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
253 |
assumes "type_definition Rep Abs S" |
47501 | 254 |
shows "part_equivp (invariant (\<lambda>x. x \<in> S))" |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
255 |
proof (intro part_equivpI) |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
256 |
interpret type_definition Rep Abs S by fact |
47501 | 257 |
show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def) |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
258 |
next |
47501 | 259 |
show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def) |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
260 |
next |
47501 | 261 |
show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def) |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
262 |
qed |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
263 |
|
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
264 |
lemma open_typedef_to_Quotient: |
47308 | 265 |
assumes "type_definition Rep Abs {x. P x}" |
47354 | 266 |
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |
47308 | 267 |
shows "Quotient (invariant P) Abs Rep T" |
47651 | 268 |
using typedef_to_Quotient [OF assms] by simp |
47308 | 269 |
|
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset
|
270 |
lemma open_typedef_to_part_equivp: |
47308 | 271 |
assumes "type_definition Rep Abs {x. P x}" |
272 |
shows "part_equivp (invariant P)" |
|
47651 | 273 |
using typedef_to_part_equivp [OF assms] by simp |
47308 | 274 |
|
47376 | 275 |
text {* Generating transfer rules for quotients. *} |
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 =)" |
|
289 |
using 1 unfolding Quotient_alt_def fun_rel_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 |
||
297 |
text {* Generating transfer rules for total quotients. *} |
|
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 |
|
47537 | 304 |
lemma Quotient_bi_total: "bi_total T" |
305 |
using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto |
|
306 |
||
307 |
lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs" |
|
308 |
using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp |
|
309 |
||
47575 | 310 |
lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x" |
311 |
using 1 2 assms unfolding Quotient_alt_def reflp_def by metis |
|
312 |
||
47889
29212a4bb866
lifting package produces abs_eq_iff rules for total quotients
huffman
parents:
47777
diff
changeset
|
313 |
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
|
314 |
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
|
315 |
|
47537 | 316 |
end |
47376 | 317 |
|
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset
|
318 |
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
|
319 |
|
47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset
|
320 |
context |
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset
|
321 |
fixes Rep Abs A T |
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset
|
322 |
assumes type: "type_definition Rep Abs A" |
47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset
|
323 |
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
|
324 |
begin |
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset
|
325 |
|
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset
|
326 |
lemma typedef_bi_unique: "bi_unique T" |
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset
|
327 |
unfolding bi_unique_def T_def |
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset
|
328 |
by (simp add: type_definition.Rep_inject [OF type]) |
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset
|
329 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
330 |
(* 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
|
331 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
332 |
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
|
333 |
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
|
334 |
by blast |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
335 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
336 |
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
|
337 |
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
|
338 |
by blast |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
339 |
|
47535
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset
|
340 |
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
|
341 |
unfolding fun_rel_def T_def by simp |
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset
|
342 |
|
47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset
|
343 |
end |
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset
|
344 |
|
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset
|
345 |
text {* Generating the correspondence rule for a constant defined with |
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset
|
346 |
@{text "lift_definition"}. *} |
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset
|
347 |
|
47351 | 348 |
lemma Quotient_to_transfer: |
349 |
assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c" |
|
350 |
shows "T c c'" |
|
351 |
using assms by (auto dest: Quotient_cr_rel) |
|
352 |
||
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
353 |
text {* Proving reflexivity *} |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
354 |
|
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
355 |
definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
356 |
where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)" |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
357 |
|
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
358 |
lemma left_totalI: |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
359 |
"(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R" |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
360 |
unfolding left_total_def by blast |
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 left_totalE: |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
363 |
assumes "left_total R" |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
364 |
obtains "(\<And>x. \<exists>y. R x y)" |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
365 |
using assms unfolding left_total_def by blast |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
366 |
|
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
367 |
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
|
368 |
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
|
369 |
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
|
370 |
shows "left_total T" |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
371 |
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
|
372 |
|
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
373 |
lemma reflp_Quotient_composition: |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
374 |
assumes lt_R1: "left_total R1" |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
375 |
and r_R2: "reflp R2" |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
376 |
shows "reflp (R1 OO R2 OO R1\<inverse>\<inverse>)" |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
377 |
using assms |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
378 |
proof - |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
379 |
{ |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
380 |
fix x |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
381 |
from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
382 |
moreover then have "R1\<inverse>\<inverse> y x" by simp |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
383 |
moreover have "R2 y y" using r_R2 by (auto elim: reflpE) |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
384 |
ultimately have "(R1 OO R2 OO R1\<inverse>\<inverse>) x x" by auto |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
385 |
} |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
386 |
then show ?thesis by (auto intro: reflpI) |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
387 |
qed |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
388 |
|
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
389 |
lemma reflp_equality: "reflp (op =)" |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
390 |
by (auto intro: reflpI) |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset
|
391 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
392 |
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
|
393 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
394 |
lemma eq_OO: "op= OO R = R" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
395 |
unfolding OO_def by metis |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
396 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
397 |
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
|
398 |
"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
|
399 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
400 |
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
|
401 |
"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
|
402 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
403 |
definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
404 |
where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" |
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 |
(* |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
407 |
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
|
408 |
left-unique ant left-total relations. Left-unique and left-total |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
409 |
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
|
410 |
*) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
411 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
412 |
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
|
413 |
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
|
414 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
415 |
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
|
416 |
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
|
417 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
418 |
lemma pos_OO_eq: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
419 |
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
|
420 |
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
|
421 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
422 |
lemma pos_eq_OO: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
423 |
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
|
424 |
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
|
425 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
426 |
lemma neg_OO_eq: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
427 |
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
|
428 |
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
|
429 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
430 |
lemma neg_eq_OO: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
431 |
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
|
432 |
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
|
433 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
434 |
lemma POS_trans: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
435 |
assumes "POS A B" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
436 |
assumes "POS B C" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
437 |
shows "POS A C" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
438 |
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
|
439 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
440 |
lemma NEG_trans: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
441 |
assumes "NEG A B" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
442 |
assumes "NEG B C" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
443 |
shows "NEG A C" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
444 |
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
|
445 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
446 |
lemma POS_NEG: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
447 |
"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
|
448 |
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
|
449 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
450 |
lemma NEG_POS: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
451 |
"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
|
452 |
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
|
453 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
454 |
lemma POS_pcr_rule: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
455 |
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
|
456 |
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
|
457 |
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
|
458 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
459 |
lemma NEG_pcr_rule: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
460 |
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
|
461 |
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
|
462 |
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
|
463 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
464 |
lemma POS_apply: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
465 |
assumes "POS R R'" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
466 |
assumes "R f g" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
467 |
shows "R' f g" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
468 |
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
|
469 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
470 |
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
|
471 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
472 |
lemma fun_mono: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
473 |
assumes "A \<ge> C" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
474 |
assumes "B \<le> D" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
475 |
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
|
476 |
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
|
477 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
478 |
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
|
479 |
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
|
480 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
481 |
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
|
482 |
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
|
483 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
484 |
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
|
485 |
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
|
486 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
487 |
lemma neg_fun_distr1: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
488 |
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
|
489 |
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
|
490 |
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
|
491 |
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
|
492 |
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
|
493 |
apply clarify |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
494 |
apply (subst all_comm) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
495 |
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
|
496 |
apply (intro choice) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
497 |
by metis |
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 neg_fun_distr2: |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
500 |
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
|
501 |
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
|
502 |
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
|
503 |
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
|
504 |
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
|
505 |
apply clarify |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
506 |
apply (subst all_comm) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
507 |
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
|
508 |
apply (intro choice) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
509 |
by metis |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
510 |
|
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 |
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
|
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_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
|
514 |
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
|
515 |
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
|
516 |
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
|
517 |
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
|
518 |
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
|
519 |
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
|
520 |
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
|
521 |
|
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 |
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
|
523 |
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
|
524 |
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
|
525 |
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
|
526 |
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
|
527 |
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
|
528 |
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
|
529 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
530 |
definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool" (infixr "OP" 75) |
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 |
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
|
532 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
533 |
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
|
534 |
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
|
535 |
shows "Domainp (A OO B) = (A OP 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
|
536 |
using assms unfolding rel_pred_comp_def by blast |
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 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
538 |
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
|
539 |
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
|
540 |
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
|
541 |
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
|
542 |
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
|
543 |
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
|
544 |
|
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 |
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
|
546 |
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
|
547 |
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
|
548 |
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
|
549 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
550 |
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
|
551 |
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
|
552 |
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
|
553 |
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
|
554 |
|
47308 | 555 |
subsection {* ML setup *} |
556 |
||
48891 | 557 |
ML_file "Tools/Lifting/lifting_util.ML" |
47308 | 558 |
|
48891 | 559 |
ML_file "Tools/Lifting/lifting_info.ML" |
47308 | 560 |
setup Lifting_Info.setup |
561 |
||
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
562 |
lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
563 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
564 |
(* setup for the function type *) |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47698
diff
changeset
|
565 |
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
|
566 |
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
|
567 |
lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2 |
47308 | 568 |
|
48891 | 569 |
ML_file "Tools/Lifting/lifting_term.ML" |
47308 | 570 |
|
48891 | 571 |
ML_file "Tools/Lifting/lifting_def.ML" |
47308 | 572 |
|
48891 | 573 |
ML_file "Tools/Lifting/lifting_setup.ML" |
47308 | 574 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51112
diff
changeset
|
575 |
hide_const (open) invariant POS NEG |
47308 | 576 |
|
577 |
end |