author | blanchet |
Mon, 20 Jan 2014 20:42:43 +0100 | |
changeset 55084 | 8ee9aabb2bca |
parent 53952 | b2781a3ce958 |
child 55415 | 05f5fdb8d093 |
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 |
|
55084 | 9 |
imports Hilbert_Choice Basic_BNFs |
47325 | 10 |
begin |
11 |
||
12 |
subsection {* Relator for function space *} |
|
13 |
||
53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
14 |
locale lifting_syntax |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
15 |
begin |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
16 |
notation fun_rel (infixr "===>" 55) |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
17 |
notation map_fun (infixr "--->" 55) |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
18 |
end |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
19 |
|
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
20 |
context |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
21 |
begin |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
22 |
interpretation lifting_syntax . |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
23 |
|
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
|
24 |
lemma fun_relD2: |
55084 | 25 |
assumes "fun_rel A B f g" and "A x x" |
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47924
diff
changeset
|
26 |
shows "B (f x) (g x)" |
55084 | 27 |
using assms by (rule fun_relD) |
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
|
28 |
|
47325 | 29 |
lemma fun_relE: |
55084 | 30 |
assumes "fun_rel A B f g" and "A x y" |
47325 | 31 |
obtains "B (f x) (g y)" |
32 |
using assms by (simp add: fun_rel_def) |
|
33 |
||
55084 | 34 |
lemmas fun_rel_eq = fun.rel_eq |
47325 | 35 |
|
36 |
lemma fun_rel_eq_rel: |
|
55084 | 37 |
shows "fun_rel (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))" |
47325 | 38 |
by (simp add: fun_rel_def) |
39 |
||
40 |
||
41 |
subsection {* Transfer method *} |
|
42 |
||
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
43 |
text {* Explicit tag for relation membership allows for |
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
44 |
backward proof methods. *} |
47325 | 45 |
|
46 |
definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
|
47 |
where "Rel r \<equiv> r" |
|
48 |
||
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
49 |
text {* Handling of equality relations *} |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
50 |
|
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
51 |
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
|
52 |
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
|
53 |
|
51437
8739f8abbecb
fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset
|
54 |
lemma is_equality_eq: "is_equality (op =)" |
8739f8abbecb
fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset
|
55 |
unfolding is_equality_def by simp |
8739f8abbecb
fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents:
51112
diff
changeset
|
56 |
|
52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
57 |
text {* Reverse implication for monotonicity rules *} |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
58 |
|
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
59 |
definition rev_implies where |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
60 |
"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
|
61 |
|
47325 | 62 |
text {* Handling of meta-logic connectives *} |
63 |
||
64 |
definition transfer_forall where |
|
65 |
"transfer_forall \<equiv> All" |
|
66 |
||
67 |
definition transfer_implies where |
|
68 |
"transfer_implies \<equiv> op \<longrightarrow>" |
|
69 |
||
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
70 |
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
|
71 |
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
|
72 |
|
47325 | 73 |
lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))" |
74 |
unfolding atomize_all transfer_forall_def .. |
|
75 |
||
76 |
lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)" |
|
77 |
unfolding atomize_imp transfer_implies_def .. |
|
78 |
||
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
79 |
lemma transfer_bforall_unfold: |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
80 |
"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
|
81 |
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
|
82 |
|
47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47637
diff
changeset
|
83 |
lemma transfer_start: "\<lbrakk>P; Rel (op =) P Q\<rbrakk> \<Longrightarrow> Q" |
47325 | 84 |
unfolding Rel_def by simp |
85 |
||
47658
7631f6f7873d
enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents:
47637
diff
changeset
|
86 |
lemma transfer_start': "\<lbrakk>P; Rel (op \<longrightarrow>) P Q\<rbrakk> \<Longrightarrow> Q" |
47325 | 87 |
unfolding Rel_def by simp |
88 |
||
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
89 |
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
|
90 |
by simp |
1568dadd598a
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents:
47612
diff
changeset
|
91 |
|
52358
f4c4bcb0d564
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents:
52354
diff
changeset
|
92 |
lemma untransfer_start: "\<lbrakk>Q; Rel (op =) P Q\<rbrakk> \<Longrightarrow> P" |
f4c4bcb0d564
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents:
52354
diff
changeset
|
93 |
unfolding Rel_def by simp |
f4c4bcb0d564
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents:
52354
diff
changeset
|
94 |
|
47325 | 95 |
lemma Rel_eq_refl: "Rel (op =) x x" |
96 |
unfolding Rel_def .. |
|
97 |
||
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
98 |
lemma Rel_app: |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
99 |
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
|
100 |
shows "Rel B (f x) (g y)" |
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
101 |
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
|
102 |
|
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
103 |
lemma Rel_abs: |
47523
1bf0e92c1ca0
make transfer method more deterministic by using SOLVED' on some subgoals
huffman
parents:
47503
diff
changeset
|
104 |
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
|
105 |
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
|
106 |
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
|
107 |
|
53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
108 |
end |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
109 |
|
48891 | 110 |
ML_file "Tools/transfer.ML" |
47325 | 111 |
setup Transfer.setup |
112 |
||
49975
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
113 |
declare refl [transfer_rule] |
faf4afed009f
transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents:
48891
diff
changeset
|
114 |
|
47503 | 115 |
declare fun_rel_eq [relator_eq] |
116 |
||
47789
71a526ee569a
implement transfer tactic with more scalable forward proof methods
huffman
parents:
47684
diff
changeset
|
117 |
hide_const (open) Rel |
47325 | 118 |
|
53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
119 |
context |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
120 |
begin |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
121 |
interpretation lifting_syntax . |
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
122 |
|
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
|
123 |
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
|
124 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
125 |
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
|
126 |
"Domainp T = Domainp T" .. |
47325 | 127 |
|
128 |
subsection {* Predicates on relations, i.e. ``class constraints'' *} |
|
129 |
||
130 |
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
131 |
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)" |
|
132 |
||
133 |
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
134 |
where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)" |
|
135 |
||
136 |
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
137 |
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)" |
|
138 |
||
139 |
definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
140 |
where "bi_unique R \<longleftrightarrow> |
|
141 |
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and> |
|
142 |
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" |
|
143 |
||
53927 | 144 |
lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z" |
145 |
by(simp add: bi_unique_def) |
|
146 |
||
147 |
lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z" |
|
148 |
by(simp add: bi_unique_def) |
|
149 |
||
150 |
lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A" |
|
151 |
unfolding right_unique_def by blast |
|
152 |
||
153 |
lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z" |
|
154 |
unfolding right_unique_def by blast |
|
155 |
||
47325 | 156 |
lemma right_total_alt_def: |
157 |
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All" |
|
158 |
unfolding right_total_def fun_rel_def |
|
159 |
apply (rule iffI, fast) |
|
160 |
apply (rule allI) |
|
161 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
162 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
163 |
apply fast |
|
164 |
done |
|
165 |
||
166 |
lemma right_unique_alt_def: |
|
167 |
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)" |
|
168 |
unfolding right_unique_def fun_rel_def by auto |
|
169 |
||
170 |
lemma bi_total_alt_def: |
|
171 |
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All" |
|
172 |
unfolding bi_total_def fun_rel_def |
|
173 |
apply (rule iffI, fast) |
|
174 |
apply safe |
|
175 |
apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec) |
|
176 |
apply (drule_tac x="\<lambda>y. True" in spec) |
|
177 |
apply fast |
|
178 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
179 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
180 |
apply fast |
|
181 |
done |
|
182 |
||
183 |
lemma bi_unique_alt_def: |
|
184 |
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)" |
|
185 |
unfolding bi_unique_def fun_rel_def by auto |
|
186 |
||
53944 | 187 |
lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R" |
188 |
by(auto simp add: bi_unique_def) |
|
189 |
||
190 |
lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R" |
|
191 |
by(auto simp add: bi_total_def) |
|
192 |
||
47660 | 193 |
text {* Properties are preserved by relation composition. *} |
194 |
||
195 |
lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)" |
|
196 |
by auto |
|
197 |
||
198 |
lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)" |
|
199 |
unfolding bi_total_def OO_def by metis |
|
200 |
||
201 |
lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)" |
|
202 |
unfolding bi_unique_def OO_def by metis |
|
203 |
||
204 |
lemma right_total_OO: |
|
205 |
"\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)" |
|
206 |
unfolding right_total_def OO_def by metis |
|
207 |
||
208 |
lemma right_unique_OO: |
|
209 |
"\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)" |
|
210 |
unfolding right_unique_def OO_def by metis |
|
211 |
||
47325 | 212 |
|
213 |
subsection {* Properties of relators *} |
|
214 |
||
215 |
lemma right_total_eq [transfer_rule]: "right_total (op =)" |
|
216 |
unfolding right_total_def by simp |
|
217 |
||
218 |
lemma right_unique_eq [transfer_rule]: "right_unique (op =)" |
|
219 |
unfolding right_unique_def by simp |
|
220 |
||
221 |
lemma bi_total_eq [transfer_rule]: "bi_total (op =)" |
|
222 |
unfolding bi_total_def by simp |
|
223 |
||
224 |
lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)" |
|
225 |
unfolding bi_unique_def by simp |
|
226 |
||
227 |
lemma right_total_fun [transfer_rule]: |
|
228 |
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)" |
|
229 |
unfolding right_total_def fun_rel_def |
|
230 |
apply (rule allI, rename_tac g) |
|
231 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) |
|
232 |
apply clarify |
|
233 |
apply (subgoal_tac "(THE y. A x y) = y", simp) |
|
234 |
apply (rule someI_ex) |
|
235 |
apply (simp) |
|
236 |
apply (rule the_equality) |
|
237 |
apply assumption |
|
238 |
apply (simp add: right_unique_def) |
|
239 |
done |
|
240 |
||
241 |
lemma right_unique_fun [transfer_rule]: |
|
242 |
"\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)" |
|
243 |
unfolding right_total_def right_unique_def fun_rel_def |
|
244 |
by (clarify, rule ext, fast) |
|
245 |
||
246 |
lemma bi_total_fun [transfer_rule]: |
|
247 |
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)" |
|
248 |
unfolding bi_total_def fun_rel_def |
|
249 |
apply safe |
|
250 |
apply (rename_tac f) |
|
251 |
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI) |
|
252 |
apply clarify |
|
253 |
apply (subgoal_tac "(THE x. A x y) = x", simp) |
|
254 |
apply (rule someI_ex) |
|
255 |
apply (simp) |
|
256 |
apply (rule the_equality) |
|
257 |
apply assumption |
|
258 |
apply (simp add: bi_unique_def) |
|
259 |
apply (rename_tac g) |
|
260 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) |
|
261 |
apply clarify |
|
262 |
apply (subgoal_tac "(THE y. A x y) = y", simp) |
|
263 |
apply (rule someI_ex) |
|
264 |
apply (simp) |
|
265 |
apply (rule the_equality) |
|
266 |
apply assumption |
|
267 |
apply (simp add: bi_unique_def) |
|
268 |
done |
|
269 |
||
270 |
lemma bi_unique_fun [transfer_rule]: |
|
271 |
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)" |
|
272 |
unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff |
|
273 |
by (safe, metis, fast) |
|
274 |
||
275 |
||
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
276 |
subsection {* Transfer rules *} |
47325 | 277 |
|
53952 | 278 |
lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)" |
279 |
by auto |
|
280 |
||
281 |
lemma Domainp_forall_transfer [transfer_rule]: |
|
282 |
assumes "right_total A" |
|
283 |
shows "((A ===> op =) ===> op =) |
|
284 |
(transfer_bforall (Domainp A)) transfer_forall" |
|
285 |
using assms unfolding right_total_def |
|
286 |
unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff |
|
287 |
by metis |
|
288 |
||
47684 | 289 |
text {* Transfer rules using implication instead of equality on booleans. *} |
290 |
||
52354
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
291 |
lemma transfer_forall_transfer [transfer_rule]: |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
292 |
"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
|
293 |
"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
|
294 |
"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
|
295 |
"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
|
296 |
"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
|
297 |
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
|
298 |
by metis+ |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
299 |
|
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
300 |
lemma transfer_implies_transfer [transfer_rule]: |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
301 |
"(op = ===> op = ===> op = ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
302 |
"(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
|
303 |
"(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
|
304 |
"(op = ===> implies ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
305 |
"(op = ===> op = ===> implies ) transfer_implies transfer_implies" |
acb4f932dd24
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents:
51956
diff
changeset
|
306 |
"(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
|
307 |
"(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
|
308 |
"(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
|
309 |
"(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
|
310 |
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
|
311 |
|
47684 | 312 |
lemma eq_imp_transfer [transfer_rule]: |
313 |
"right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)" |
|
314 |
unfolding right_unique_alt_def . |
|
315 |
||
47636 | 316 |
lemma eq_transfer [transfer_rule]: |
47325 | 317 |
assumes "bi_unique A" |
318 |
shows "(A ===> A ===> op =) (op =) (op =)" |
|
319 |
using assms unfolding bi_unique_def fun_rel_def by auto |
|
320 |
||
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
|
321 |
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
|
322 |
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
|
323 |
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
|
324 |
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
|
325 |
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
|
326 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51955
diff
changeset
|
327 |
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
|
328 |
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
|
329 |
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
|
330 |
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
|
331 |
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
|
332 |
|
47636 | 333 |
lemma All_transfer [transfer_rule]: |
47325 | 334 |
assumes "bi_total A" |
335 |
shows "((A ===> op =) ===> op =) All All" |
|
336 |
using assms unfolding bi_total_def fun_rel_def by fast |
|
337 |
||
47636 | 338 |
lemma Ex_transfer [transfer_rule]: |
47325 | 339 |
assumes "bi_total A" |
340 |
shows "((A ===> op =) ===> op =) Ex Ex" |
|
341 |
using assms unfolding bi_total_def fun_rel_def by fast |
|
342 |
||
47636 | 343 |
lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If" |
47325 | 344 |
unfolding fun_rel_def by simp |
345 |
||
47636 | 346 |
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" |
47612 | 347 |
unfolding fun_rel_def by simp |
348 |
||
47636 | 349 |
lemma id_transfer [transfer_rule]: "(A ===> A) id id" |
47625 | 350 |
unfolding fun_rel_def by simp |
351 |
||
47636 | 352 |
lemma comp_transfer [transfer_rule]: |
47325 | 353 |
"((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)" |
354 |
unfolding fun_rel_def by simp |
|
355 |
||
47636 | 356 |
lemma fun_upd_transfer [transfer_rule]: |
47325 | 357 |
assumes [transfer_rule]: "bi_unique A" |
358 |
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" |
|
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47627
diff
changeset
|
359 |
unfolding fun_upd_def [abs_def] by transfer_prover |
47325 | 360 |
|
47637 | 361 |
lemma nat_case_transfer [transfer_rule]: |
362 |
"(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case" |
|
363 |
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
|
364 |
|
47924 | 365 |
lemma nat_rec_transfer [transfer_rule]: |
366 |
"(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec" |
|
367 |
unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all) |
|
368 |
||
369 |
lemma funpow_transfer [transfer_rule]: |
|
370 |
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow" |
|
371 |
unfolding funpow_def by transfer_prover |
|
372 |
||
53952 | 373 |
lemma mono_transfer[transfer_rule]: |
374 |
assumes [transfer_rule]: "bi_total A" |
|
375 |
assumes [transfer_rule]: "(A ===> A ===> op=) op\<le> op\<le>" |
|
376 |
assumes [transfer_rule]: "(B ===> B ===> op=) op\<le> op\<le>" |
|
377 |
shows "((A ===> B) ===> op=) mono mono" |
|
378 |
unfolding mono_def[abs_def] by transfer_prover |
|
379 |
||
380 |
lemma right_total_relcompp_transfer[transfer_rule]: |
|
381 |
assumes [transfer_rule]: "right_total B" |
|
382 |
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) |
|
383 |
(\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO" |
|
384 |
unfolding OO_def[abs_def] by transfer_prover |
|
385 |
||
386 |
lemma relcompp_transfer[transfer_rule]: |
|
387 |
assumes [transfer_rule]: "bi_total B" |
|
388 |
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO" |
|
389 |
unfolding OO_def[abs_def] by transfer_prover |
|
47627
2b1d3eda59eb
add secondary transfer rule for universal quantifiers on non-bi-total relations
huffman
parents:
47625
diff
changeset
|
390 |
|
53952 | 391 |
lemma right_total_Domainp_transfer[transfer_rule]: |
392 |
assumes [transfer_rule]: "right_total B" |
|
393 |
shows "((A ===> B ===> op=) ===> A ===> op=) (\<lambda>T x. \<exists>y\<in>Collect(Domainp B). T x y) Domainp" |
|
394 |
apply(subst(2) Domainp_iff[abs_def]) by transfer_prover |
|
395 |
||
396 |
lemma Domainp_transfer[transfer_rule]: |
|
397 |
assumes [transfer_rule]: "bi_total B" |
|
398 |
shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp" |
|
399 |
unfolding Domainp_iff[abs_def] by transfer_prover |
|
400 |
||
401 |
lemma reflp_transfer[transfer_rule]: |
|
402 |
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp" |
|
403 |
"right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp" |
|
404 |
"right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp" |
|
405 |
"bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp" |
|
406 |
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp" |
|
407 |
using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def fun_rel_def |
|
408 |
by fast+ |
|
409 |
||
410 |
lemma right_unique_transfer [transfer_rule]: |
|
411 |
assumes [transfer_rule]: "right_total A" |
|
412 |
assumes [transfer_rule]: "right_total B" |
|
413 |
assumes [transfer_rule]: "bi_unique B" |
|
414 |
shows "((A ===> B ===> op=) ===> implies) right_unique right_unique" |
|
415 |
using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def |
|
416 |
by metis |
|
47325 | 417 |
|
418 |
end |
|
53011
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
419 |
|
aeee0a4be6cf
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents:
52358
diff
changeset
|
420 |
end |