author | kuncar |
Mon, 13 May 2013 13:59:04 +0200 | |
changeset 51956 | a4d81cdebf8b |
parent 51955 | 04d9381bebff |
child 52354 | acb4f932dd24 |
permissions | -rw-r--r-- |
47325 | 1 |
(* Title: HOL/Transfer.thy |
2 |
Author: Brian Huffman, TU Muenchen |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
3 |
Author: Ondrej Kuncar, TU Muenchen |
47325 | 4 |
*) |
5 |
||
6 |
header {* Generic theorem transfer using relations *} |
|
7 |
||
8 |
theory Transfer |
|
51112 | 9 |
imports Hilbert_Choice |
47325 | 10 |
begin |
11 |
||
12 |
subsection {* Relator for function space *} |
|
13 |
||
14 |
definition |
|
15 |
fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55) |
|
16 |
where |
|
17 |
"fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))" |
|
18 |
||
19 |
lemma fun_relI [intro]: |
|
20 |
assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)" |
|
21 |
shows "(A ===> B) f g" |
|
22 |
using assms by (simp add: fun_rel_def) |
|
23 |
||
24 |
lemma fun_relD: |
|
25 |
assumes "(A ===> B) f g" and "A x y" |
|
26 |
shows "B (f x) (g y)" |
|
27 |
using assms by (simp add: fun_rel_def) |
|
28 |
||
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47924
diff
changeset
|
29 |
lemma fun_relD2: |
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47924
diff
changeset
|
30 |
assumes "(A ===> B) f g" and "A 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:
47924
diff
changeset
|
31 |
shows "B (f x) (g 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:
47924
diff
changeset
|
32 |
using assms unfolding fun_rel_def 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:
47924
diff
changeset
|
33 |
|
47325 | 34 |
lemma fun_relE: |
35 |
assumes "(A ===> B) f g" and "A x y" |
|
36 |
obtains "B (f x) (g y)" |
|
37 |
using assms by (simp add: fun_rel_def) |
|
38 |
||
39 |
lemma fun_rel_eq: |
|
40 |
shows "((op =) ===> (op =)) = (op =)" |
|
41 |
by (auto simp add: fun_eq_iff elim: fun_relE) |
|
42 |
||
43 |
lemma fun_rel_eq_rel: |
|
44 |
shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))" |
|
45 |
by (simp add: fun_rel_def) |
|
46 |
||
47 |
||
48 |
subsection {* Transfer method *} |
|
49 |
||
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
50 |
text {* Explicit tag for relation membership allows for |
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
51 |
backward proof methods. *} |
47325 | 52 |
|
53 |
definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
|
54 |
where "Rel r \<equiv> r" |
|
55 |
||
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
56 |
text {* Handling of equality relations *} |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
57 |
|
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
58 |
definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
59 |
where "is_equality R \<longleftrightarrow> R = (op =)" |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
60 |
|
51437
8739f8abbecb
fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset
|
61 |
lemma is_equality_eq: "is_equality (op =)" |
8739f8abbecb
fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset
|
62 |
unfolding is_equality_def by simp |
8739f8abbecb
fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset
|
63 |
|
47325 | 64 |
text {* Handling of meta-logic connectives *} |
65 |
||
66 |
definition transfer_forall where |
|
67 |
"transfer_forall \<equiv> All" |
|
68 |
||
69 |
definition transfer_implies where |
|
70 |
"transfer_implies \<equiv> op \<longrightarrow>" |
|
71 |
||
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
72 |
definition transfer_bforall :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
73 |
where "transfer_bforall \<equiv> (\<lambda>P Q. \<forall>x. P x \<longrightarrow> Q x)" |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
74 |
|
47325 | 75 |
lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))" |
76 |
unfolding atomize_all transfer_forall_def .. |
|
77 |
||
78 |
lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)" |
|
79 |
unfolding atomize_imp transfer_implies_def .. |
|
80 |
||
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
81 |
lemma transfer_bforall_unfold: |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
82 |
"Trueprop (transfer_bforall P (\<lambda>x. Q x)) \<equiv> (\<And>x. P x \<Longrightarrow> Q x)" |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
83 |
unfolding transfer_bforall_def atomize_imp atomize_all .. |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
84 |
|
47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47637
diff
changeset
|
85 |
lemma transfer_start: "\<lbrakk>P; Rel (op =) P Q\<rbrakk> \<Longrightarrow> Q" |
47325 | 86 |
unfolding Rel_def by simp |
87 |
||
47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47637
diff
changeset
|
88 |
lemma transfer_start': "\<lbrakk>P; Rel (op \<longrightarrow>) P Q\<rbrakk> \<Longrightarrow> Q" |
47325 | 89 |
unfolding Rel_def by simp |
90 |
||
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
91 |
lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y" |
47618
1568dadd598a
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents:
47612
diff
changeset
|
92 |
by simp |
1568dadd598a
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents:
47612
diff
changeset
|
93 |
|
47325 | 94 |
lemma Rel_eq_refl: "Rel (op =) x x" |
95 |
unfolding Rel_def .. |
|
96 |
||
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
97 |
lemma Rel_app: |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
98 |
assumes "Rel (A ===> B) f g" and "Rel A x y" |
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
99 |
shows "Rel B (f x) (g y)" |
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
100 |
using assms unfolding Rel_def fun_rel_def by fast |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
101 |
|
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
102 |
lemma Rel_abs: |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
103 |
assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)" |
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
104 |
shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)" |
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
105 |
using assms unfolding Rel_def fun_rel_def by fast |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
106 |
|
48891 | 107 |
ML_file "Tools/transfer.ML" |
47325 | 108 |
setup Transfer.setup |
109 |
||
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
110 |
declare refl [transfer_rule] |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
111 |
|
47503 | 112 |
declare fun_rel_eq [relator_eq] |
113 |
||
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
114 |
hide_const (open) Rel |
47325 | 115 |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
116 |
text {* Handling of domains *} |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
117 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
118 |
lemma Domaimp_refl[transfer_domain_rule]: |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
119 |
"Domainp T = Domainp T" .. |
47325 | 120 |
|
121 |
subsection {* Predicates on relations, i.e. ``class constraints'' *} |
|
122 |
||
123 |
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
124 |
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)" |
|
125 |
||
126 |
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
127 |
where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)" |
|
128 |
||
129 |
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
130 |
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)" |
|
131 |
||
132 |
definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
133 |
where "bi_unique R \<longleftrightarrow> |
|
134 |
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and> |
|
135 |
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" |
|
136 |
||
137 |
lemma right_total_alt_def: |
|
138 |
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All" |
|
139 |
unfolding right_total_def fun_rel_def |
|
140 |
apply (rule iffI, fast) |
|
141 |
apply (rule allI) |
|
142 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
143 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
144 |
apply fast |
|
145 |
done |
|
146 |
||
147 |
lemma right_unique_alt_def: |
|
148 |
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)" |
|
149 |
unfolding right_unique_def fun_rel_def by auto |
|
150 |
||
151 |
lemma bi_total_alt_def: |
|
152 |
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All" |
|
153 |
unfolding bi_total_def fun_rel_def |
|
154 |
apply (rule iffI, fast) |
|
155 |
apply safe |
|
156 |
apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec) |
|
157 |
apply (drule_tac x="\<lambda>y. True" in spec) |
|
158 |
apply fast |
|
159 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
160 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
161 |
apply fast |
|
162 |
done |
|
163 |
||
164 |
lemma bi_unique_alt_def: |
|
165 |
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)" |
|
166 |
unfolding bi_unique_def fun_rel_def by auto |
|
167 |
||
47660 | 168 |
text {* Properties are preserved by relation composition. *} |
169 |
||
170 |
lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)" |
|
171 |
by auto |
|
172 |
||
173 |
lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)" |
|
174 |
unfolding bi_total_def OO_def by metis |
|
175 |
||
176 |
lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)" |
|
177 |
unfolding bi_unique_def OO_def by metis |
|
178 |
||
179 |
lemma right_total_OO: |
|
180 |
"\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)" |
|
181 |
unfolding right_total_def OO_def by metis |
|
182 |
||
183 |
lemma right_unique_OO: |
|
184 |
"\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)" |
|
185 |
unfolding right_unique_def OO_def by metis |
|
186 |
||
47325 | 187 |
|
188 |
subsection {* Properties of relators *} |
|
189 |
||
190 |
lemma right_total_eq [transfer_rule]: "right_total (op =)" |
|
191 |
unfolding right_total_def by simp |
|
192 |
||
193 |
lemma right_unique_eq [transfer_rule]: "right_unique (op =)" |
|
194 |
unfolding right_unique_def by simp |
|
195 |
||
196 |
lemma bi_total_eq [transfer_rule]: "bi_total (op =)" |
|
197 |
unfolding bi_total_def by simp |
|
198 |
||
199 |
lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)" |
|
200 |
unfolding bi_unique_def by simp |
|
201 |
||
202 |
lemma right_total_fun [transfer_rule]: |
|
203 |
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)" |
|
204 |
unfolding right_total_def fun_rel_def |
|
205 |
apply (rule allI, rename_tac g) |
|
206 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) |
|
207 |
apply clarify |
|
208 |
apply (subgoal_tac "(THE y. A x y) = y", simp) |
|
209 |
apply (rule someI_ex) |
|
210 |
apply (simp) |
|
211 |
apply (rule the_equality) |
|
212 |
apply assumption |
|
213 |
apply (simp add: right_unique_def) |
|
214 |
done |
|
215 |
||
216 |
lemma right_unique_fun [transfer_rule]: |
|
217 |
"\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)" |
|
218 |
unfolding right_total_def right_unique_def fun_rel_def |
|
219 |
by (clarify, rule ext, fast) |
|
220 |
||
221 |
lemma bi_total_fun [transfer_rule]: |
|
222 |
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)" |
|
223 |
unfolding bi_total_def fun_rel_def |
|
224 |
apply safe |
|
225 |
apply (rename_tac f) |
|
226 |
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI) |
|
227 |
apply clarify |
|
228 |
apply (subgoal_tac "(THE x. A x y) = x", simp) |
|
229 |
apply (rule someI_ex) |
|
230 |
apply (simp) |
|
231 |
apply (rule the_equality) |
|
232 |
apply assumption |
|
233 |
apply (simp add: bi_unique_def) |
|
234 |
apply (rename_tac g) |
|
235 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) |
|
236 |
apply clarify |
|
237 |
apply (subgoal_tac "(THE y. A x y) = y", simp) |
|
238 |
apply (rule someI_ex) |
|
239 |
apply (simp) |
|
240 |
apply (rule the_equality) |
|
241 |
apply assumption |
|
242 |
apply (simp add: bi_unique_def) |
|
243 |
done |
|
244 |
||
245 |
lemma bi_unique_fun [transfer_rule]: |
|
246 |
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)" |
|
247 |
unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff |
|
248 |
by (safe, metis, fast) |
|
249 |
||
250 |
||
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
251 |
subsection {* Transfer rules *} |
47325 | 252 |
|
47684 | 253 |
text {* Transfer rules using implication instead of equality on booleans. *} |
254 |
||
255 |
lemma eq_imp_transfer [transfer_rule]: |
|
256 |
"right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)" |
|
257 |
unfolding right_unique_alt_def . |
|
258 |
||
259 |
lemma forall_imp_transfer [transfer_rule]: |
|
260 |
"right_total A \<Longrightarrow> ((A ===> op \<longrightarrow>) ===> op \<longrightarrow>) transfer_forall transfer_forall" |
|
261 |
unfolding right_total_alt_def transfer_forall_def . |
|
262 |
||
47636 | 263 |
lemma eq_transfer [transfer_rule]: |
47325 | 264 |
assumes "bi_unique A" |
265 |
shows "(A ===> A ===> op =) (op =) (op =)" |
|
266 |
using assms unfolding bi_unique_def fun_rel_def by auto |
|
267 |
||
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
268 |
lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
269 |
by auto |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
270 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
271 |
lemma right_total_Ex_transfer[transfer_rule]: |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
272 |
assumes "right_total A" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
273 |
shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
274 |
using assms unfolding right_total_def Bex_def fun_rel_def Domainp_iff[abs_def] |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
275 |
by blast |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
276 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
277 |
lemma right_total_All_transfer[transfer_rule]: |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
278 |
assumes "right_total A" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
279 |
shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
280 |
using assms unfolding right_total_def Ball_def fun_rel_def Domainp_iff[abs_def] |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
281 |
by blast |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
282 |
|
47636 | 283 |
lemma All_transfer [transfer_rule]: |
47325 | 284 |
assumes "bi_total A" |
285 |
shows "((A ===> op =) ===> op =) All All" |
|
286 |
using assms unfolding bi_total_def fun_rel_def by fast |
|
287 |
||
47636 | 288 |
lemma Ex_transfer [transfer_rule]: |
47325 | 289 |
assumes "bi_total A" |
290 |
shows "((A ===> op =) ===> op =) Ex Ex" |
|
291 |
using assms unfolding bi_total_def fun_rel_def by fast |
|
292 |
||
47636 | 293 |
lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If" |
47325 | 294 |
unfolding fun_rel_def by simp |
295 |
||
47636 | 296 |
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" |
47612 | 297 |
unfolding fun_rel_def by simp |
298 |
||
47636 | 299 |
lemma id_transfer [transfer_rule]: "(A ===> A) id id" |
47625 | 300 |
unfolding fun_rel_def by simp |
301 |
||
47636 | 302 |
lemma comp_transfer [transfer_rule]: |
47325 | 303 |
"((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)" |
304 |
unfolding fun_rel_def by simp |
|
305 |
||
47636 | 306 |
lemma fun_upd_transfer [transfer_rule]: |
47325 | 307 |
assumes [transfer_rule]: "bi_unique A" |
308 |
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" |
|
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
309 |
unfolding fun_upd_def [abs_def] by transfer_prover |
47325 | 310 |
|
47637 | 311 |
lemma nat_case_transfer [transfer_rule]: |
312 |
"(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case" |
|
313 |
unfolding fun_rel_def by (simp split: nat.split) |
|
47627
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
314 |
|
47924 | 315 |
lemma nat_rec_transfer [transfer_rule]: |
316 |
"(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec" |
|
317 |
unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all) |
|
318 |
||
319 |
lemma funpow_transfer [transfer_rule]: |
|
320 |
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow" |
|
321 |
unfolding funpow_def by transfer_prover |
|
322 |
||
47627
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
323 |
lemma Domainp_forall_transfer [transfer_rule]: |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
324 |
assumes "right_total A" |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
325 |
shows "((A ===> op =) ===> op =) |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
326 |
(transfer_bforall (Domainp A)) transfer_forall" |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
327 |
using assms unfolding right_total_def |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
328 |
unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
329 |
by metis |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
330 |
|
47636 | 331 |
lemma forall_transfer [transfer_rule]: |
47627
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
332 |
"bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall" |
47636 | 333 |
unfolding transfer_forall_def by (rule All_transfer) |
47325 | 334 |
|
335 |
end |