author | huffman |
Sat, 08 Jun 2013 19:40:19 -0700 | |
changeset 52354 | acb4f932dd24 |
parent 51956 | a4d81cdebf8b |
child 52358 | f4c4bcb0d564 |
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 |
|
52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
64 |
text {* Reverse implication for monotonicity rules *} |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
65 |
|
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
66 |
definition rev_implies where |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
67 |
"rev_implies x y \<longleftrightarrow> (y \<longrightarrow> x)" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
68 |
|
47325 | 69 |
text {* Handling of meta-logic connectives *} |
70 |
||
71 |
definition transfer_forall where |
|
72 |
"transfer_forall \<equiv> All" |
|
73 |
||
74 |
definition transfer_implies where |
|
75 |
"transfer_implies \<equiv> op \<longrightarrow>" |
|
76 |
||
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
77 |
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
|
78 |
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
|
79 |
|
47325 | 80 |
lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))" |
81 |
unfolding atomize_all transfer_forall_def .. |
|
82 |
||
83 |
lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)" |
|
84 |
unfolding atomize_imp transfer_implies_def .. |
|
85 |
||
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
86 |
lemma transfer_bforall_unfold: |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
87 |
"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
|
88 |
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
|
89 |
|
47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47637
diff
changeset
|
90 |
lemma transfer_start: "\<lbrakk>P; Rel (op =) P Q\<rbrakk> \<Longrightarrow> Q" |
47325 | 91 |
unfolding Rel_def by simp |
92 |
||
47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47637
diff
changeset
|
93 |
lemma transfer_start': "\<lbrakk>P; Rel (op \<longrightarrow>) P Q\<rbrakk> \<Longrightarrow> Q" |
47325 | 94 |
unfolding Rel_def by simp |
95 |
||
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
96 |
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
|
97 |
by simp |
1568dadd598a
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents:
47612
diff
changeset
|
98 |
|
47325 | 99 |
lemma Rel_eq_refl: "Rel (op =) x x" |
100 |
unfolding Rel_def .. |
|
101 |
||
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
102 |
lemma Rel_app: |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
103 |
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
|
104 |
shows "Rel B (f x) (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 |
|
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
107 |
lemma Rel_abs: |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
108 |
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
|
109 |
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
|
110 |
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
|
111 |
|
48891 | 112 |
ML_file "Tools/transfer.ML" |
47325 | 113 |
setup Transfer.setup |
114 |
||
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
115 |
declare refl [transfer_rule] |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
116 |
|
47503 | 117 |
declare fun_rel_eq [relator_eq] |
118 |
||
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
119 |
hide_const (open) Rel |
47325 | 120 |
|
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
|
121 |
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
|
122 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
123 |
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
|
124 |
"Domainp T = Domainp T" .. |
47325 | 125 |
|
126 |
subsection {* Predicates on relations, i.e. ``class constraints'' *} |
|
127 |
||
128 |
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
129 |
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)" |
|
130 |
||
131 |
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
132 |
where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)" |
|
133 |
||
134 |
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
135 |
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)" |
|
136 |
||
137 |
definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
138 |
where "bi_unique R \<longleftrightarrow> |
|
139 |
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and> |
|
140 |
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" |
|
141 |
||
142 |
lemma right_total_alt_def: |
|
143 |
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All" |
|
144 |
unfolding right_total_def fun_rel_def |
|
145 |
apply (rule iffI, fast) |
|
146 |
apply (rule allI) |
|
147 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
148 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
149 |
apply fast |
|
150 |
done |
|
151 |
||
152 |
lemma right_unique_alt_def: |
|
153 |
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)" |
|
154 |
unfolding right_unique_def fun_rel_def by auto |
|
155 |
||
156 |
lemma bi_total_alt_def: |
|
157 |
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All" |
|
158 |
unfolding bi_total_def fun_rel_def |
|
159 |
apply (rule iffI, fast) |
|
160 |
apply safe |
|
161 |
apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec) |
|
162 |
apply (drule_tac x="\<lambda>y. True" in spec) |
|
163 |
apply fast |
|
164 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
165 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
166 |
apply fast |
|
167 |
done |
|
168 |
||
169 |
lemma bi_unique_alt_def: |
|
170 |
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)" |
|
171 |
unfolding bi_unique_def fun_rel_def by auto |
|
172 |
||
47660 | 173 |
text {* Properties are preserved by relation composition. *} |
174 |
||
175 |
lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)" |
|
176 |
by auto |
|
177 |
||
178 |
lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)" |
|
179 |
unfolding bi_total_def OO_def by metis |
|
180 |
||
181 |
lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)" |
|
182 |
unfolding bi_unique_def OO_def by metis |
|
183 |
||
184 |
lemma right_total_OO: |
|
185 |
"\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)" |
|
186 |
unfolding right_total_def OO_def by metis |
|
187 |
||
188 |
lemma right_unique_OO: |
|
189 |
"\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)" |
|
190 |
unfolding right_unique_def OO_def by metis |
|
191 |
||
47325 | 192 |
|
193 |
subsection {* Properties of relators *} |
|
194 |
||
195 |
lemma right_total_eq [transfer_rule]: "right_total (op =)" |
|
196 |
unfolding right_total_def by simp |
|
197 |
||
198 |
lemma right_unique_eq [transfer_rule]: "right_unique (op =)" |
|
199 |
unfolding right_unique_def by simp |
|
200 |
||
201 |
lemma bi_total_eq [transfer_rule]: "bi_total (op =)" |
|
202 |
unfolding bi_total_def by simp |
|
203 |
||
204 |
lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)" |
|
205 |
unfolding bi_unique_def by simp |
|
206 |
||
207 |
lemma right_total_fun [transfer_rule]: |
|
208 |
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)" |
|
209 |
unfolding right_total_def fun_rel_def |
|
210 |
apply (rule allI, rename_tac g) |
|
211 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) |
|
212 |
apply clarify |
|
213 |
apply (subgoal_tac "(THE y. A x y) = y", simp) |
|
214 |
apply (rule someI_ex) |
|
215 |
apply (simp) |
|
216 |
apply (rule the_equality) |
|
217 |
apply assumption |
|
218 |
apply (simp add: right_unique_def) |
|
219 |
done |
|
220 |
||
221 |
lemma right_unique_fun [transfer_rule]: |
|
222 |
"\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)" |
|
223 |
unfolding right_total_def right_unique_def fun_rel_def |
|
224 |
by (clarify, rule ext, fast) |
|
225 |
||
226 |
lemma bi_total_fun [transfer_rule]: |
|
227 |
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)" |
|
228 |
unfolding bi_total_def fun_rel_def |
|
229 |
apply safe |
|
230 |
apply (rename_tac f) |
|
231 |
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI) |
|
232 |
apply clarify |
|
233 |
apply (subgoal_tac "(THE x. A x y) = x", simp) |
|
234 |
apply (rule someI_ex) |
|
235 |
apply (simp) |
|
236 |
apply (rule the_equality) |
|
237 |
apply assumption |
|
238 |
apply (simp add: bi_unique_def) |
|
239 |
apply (rename_tac g) |
|
240 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) |
|
241 |
apply clarify |
|
242 |
apply (subgoal_tac "(THE y. A x y) = y", simp) |
|
243 |
apply (rule someI_ex) |
|
244 |
apply (simp) |
|
245 |
apply (rule the_equality) |
|
246 |
apply assumption |
|
247 |
apply (simp add: bi_unique_def) |
|
248 |
done |
|
249 |
||
250 |
lemma bi_unique_fun [transfer_rule]: |
|
251 |
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)" |
|
252 |
unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff |
|
253 |
by (safe, metis, fast) |
|
254 |
||
255 |
||
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
256 |
subsection {* Transfer rules *} |
47325 | 257 |
|
47684 | 258 |
text {* Transfer rules using implication instead of equality on booleans. *} |
259 |
||
52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
260 |
lemma transfer_forall_transfer [transfer_rule]: |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
261 |
"bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
262 |
"right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
263 |
"right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
264 |
"bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
265 |
"bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
266 |
unfolding transfer_forall_def rev_implies_def fun_rel_def right_total_def bi_total_def |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
267 |
by metis+ |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
268 |
|
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
269 |
lemma transfer_implies_transfer [transfer_rule]: |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
270 |
"(op = ===> op = ===> op = ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
271 |
"(rev_implies ===> implies ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
272 |
"(rev_implies ===> op = ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
273 |
"(op = ===> implies ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
274 |
"(op = ===> op = ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
275 |
"(implies ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
276 |
"(implies ===> op = ===> rev_implies) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
277 |
"(op = ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
278 |
"(op = ===> op = ===> rev_implies) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
279 |
unfolding transfer_implies_def rev_implies_def fun_rel_def by auto |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
280 |
|
47684 | 281 |
lemma eq_imp_transfer [transfer_rule]: |
282 |
"right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)" |
|
283 |
unfolding right_unique_alt_def . |
|
284 |
||
47636 | 285 |
lemma eq_transfer [transfer_rule]: |
47325 | 286 |
assumes "bi_unique A" |
287 |
shows "(A ===> A ===> op =) (op =) (op =)" |
|
288 |
using assms unfolding bi_unique_def fun_rel_def by auto |
|
289 |
||
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
|
290 |
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
|
291 |
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
|
292 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
293 |
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
|
294 |
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
|
295 |
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
|
296 |
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
|
297 |
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
|
298 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
299 |
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
|
300 |
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
|
301 |
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
|
302 |
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
|
303 |
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
|
304 |
|
47636 | 305 |
lemma All_transfer [transfer_rule]: |
47325 | 306 |
assumes "bi_total A" |
307 |
shows "((A ===> op =) ===> op =) All All" |
|
308 |
using assms unfolding bi_total_def fun_rel_def by fast |
|
309 |
||
47636 | 310 |
lemma Ex_transfer [transfer_rule]: |
47325 | 311 |
assumes "bi_total A" |
312 |
shows "((A ===> op =) ===> op =) Ex Ex" |
|
313 |
using assms unfolding bi_total_def fun_rel_def by fast |
|
314 |
||
47636 | 315 |
lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If" |
47325 | 316 |
unfolding fun_rel_def by simp |
317 |
||
47636 | 318 |
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" |
47612 | 319 |
unfolding fun_rel_def by simp |
320 |
||
47636 | 321 |
lemma id_transfer [transfer_rule]: "(A ===> A) id id" |
47625 | 322 |
unfolding fun_rel_def by simp |
323 |
||
47636 | 324 |
lemma comp_transfer [transfer_rule]: |
47325 | 325 |
"((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)" |
326 |
unfolding fun_rel_def by simp |
|
327 |
||
47636 | 328 |
lemma fun_upd_transfer [transfer_rule]: |
47325 | 329 |
assumes [transfer_rule]: "bi_unique A" |
330 |
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" |
|
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
331 |
unfolding fun_upd_def [abs_def] by transfer_prover |
47325 | 332 |
|
47637 | 333 |
lemma nat_case_transfer [transfer_rule]: |
334 |
"(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case" |
|
335 |
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
|
336 |
|
47924 | 337 |
lemma nat_rec_transfer [transfer_rule]: |
338 |
"(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec" |
|
339 |
unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all) |
|
340 |
||
341 |
lemma funpow_transfer [transfer_rule]: |
|
342 |
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow" |
|
343 |
unfolding funpow_def by transfer_prover |
|
344 |
||
47627
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
345 |
lemma Domainp_forall_transfer [transfer_rule]: |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
346 |
assumes "right_total A" |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
347 |
shows "((A ===> op =) ===> op =) |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
348 |
(transfer_bforall (Domainp A)) transfer_forall" |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
349 |
using assms unfolding right_total_def |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
350 |
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
|
351 |
by metis |
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
352 |
|
47636 | 353 |
lemma forall_transfer [transfer_rule]: |
47627
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
354 |
"bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall" |
47636 | 355 |
unfolding transfer_forall_def by (rule All_transfer) |
47325 | 356 |
|
357 |
end |