huffman@48196
|
1 |
(* Title: HOL/Transfer.thy
|
huffman@48196
|
2 |
Author: Brian Huffman, TU Muenchen
|
kuncar@53093
|
3 |
Author: Ondrej Kuncar, TU Muenchen
|
huffman@48196
|
4 |
*)
|
huffman@48196
|
5 |
|
huffman@48196
|
6 |
header {* Generic theorem transfer using relations *}
|
huffman@48196
|
7 |
|
huffman@48196
|
8 |
theory Transfer
|
kuncar@57866
|
9 |
imports Hilbert_Choice Basic_BNFs BNF_FP_Base Metis Option
|
huffman@48196
|
10 |
begin
|
huffman@48196
|
11 |
|
kuncar@57866
|
12 |
(* We include Option here altough it's not needed here.
|
kuncar@57866
|
13 |
By doing this, we avoid a diamond problem for BNF and
|
kuncar@57866
|
14 |
FP sugar interpretation defined in this file. *)
|
kuncar@57866
|
15 |
|
huffman@48196
|
16 |
subsection {* Relator for function space *}
|
huffman@48196
|
17 |
|
kuncar@54148
|
18 |
locale lifting_syntax
|
kuncar@54148
|
19 |
begin
|
blanchet@57287
|
20 |
notation rel_fun (infixr "===>" 55)
|
kuncar@54148
|
21 |
notation map_fun (infixr "--->" 55)
|
kuncar@54148
|
22 |
end
|
kuncar@54148
|
23 |
|
kuncar@54148
|
24 |
context
|
kuncar@54148
|
25 |
begin
|
kuncar@54148
|
26 |
interpretation lifting_syntax .
|
kuncar@54148
|
27 |
|
blanchet@57287
|
28 |
lemma rel_funD2:
|
blanchet@57287
|
29 |
assumes "rel_fun A B f g" and "A x x"
|
kuncar@48952
|
30 |
shows "B (f x) (g x)"
|
blanchet@57287
|
31 |
using assms by (rule rel_funD)
|
kuncar@48952
|
32 |
|
blanchet@57287
|
33 |
lemma rel_funE:
|
blanchet@57287
|
34 |
assumes "rel_fun A B f g" and "A x y"
|
huffman@48196
|
35 |
obtains "B (f x) (g y)"
|
blanchet@57287
|
36 |
using assms by (simp add: rel_fun_def)
|
huffman@48196
|
37 |
|
blanchet@57287
|
38 |
lemmas rel_fun_eq = fun.rel_eq
|
huffman@48196
|
39 |
|
blanchet@57287
|
40 |
lemma rel_fun_eq_rel:
|
blanchet@57287
|
41 |
shows "rel_fun (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
|
blanchet@57287
|
42 |
by (simp add: rel_fun_def)
|
huffman@48196
|
43 |
|
huffman@48196
|
44 |
|
huffman@48196
|
45 |
subsection {* Transfer method *}
|
huffman@48196
|
46 |
|
huffman@48660
|
47 |
text {* Explicit tag for relation membership allows for
|
huffman@48660
|
48 |
backward proof methods. *}
|
huffman@48196
|
49 |
|
huffman@48196
|
50 |
definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
|
huffman@48196
|
51 |
where "Rel r \<equiv> r"
|
huffman@48196
|
52 |
|
huffman@50990
|
53 |
text {* Handling of equality relations *}
|
huffman@50990
|
54 |
|
huffman@50990
|
55 |
definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
|
huffman@50990
|
56 |
where "is_equality R \<longleftrightarrow> R = (op =)"
|
huffman@50990
|
57 |
|
kuncar@52574
|
58 |
lemma is_equality_eq: "is_equality (op =)"
|
kuncar@52574
|
59 |
unfolding is_equality_def by simp
|
kuncar@52574
|
60 |
|
huffman@53491
|
61 |
text {* Reverse implication for monotonicity rules *}
|
huffman@53491
|
62 |
|
huffman@53491
|
63 |
definition rev_implies where
|
huffman@53491
|
64 |
"rev_implies x y \<longleftrightarrow> (y \<longrightarrow> x)"
|
huffman@53491
|
65 |
|
huffman@48196
|
66 |
text {* Handling of meta-logic connectives *}
|
huffman@48196
|
67 |
|
huffman@48196
|
68 |
definition transfer_forall where
|
huffman@48196
|
69 |
"transfer_forall \<equiv> All"
|
huffman@48196
|
70 |
|
huffman@48196
|
71 |
definition transfer_implies where
|
huffman@48196
|
72 |
"transfer_implies \<equiv> op \<longrightarrow>"
|
huffman@48196
|
73 |
|
huffman@48213
|
74 |
definition transfer_bforall :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
|
huffman@48213
|
75 |
where "transfer_bforall \<equiv> (\<lambda>P Q. \<forall>x. P x \<longrightarrow> Q x)"
|
huffman@48213
|
76 |
|
huffman@48196
|
77 |
lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))"
|
huffman@48196
|
78 |
unfolding atomize_all transfer_forall_def ..
|
huffman@48196
|
79 |
|
huffman@48196
|
80 |
lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)"
|
huffman@48196
|
81 |
unfolding atomize_imp transfer_implies_def ..
|
huffman@48196
|
82 |
|
huffman@48213
|
83 |
lemma transfer_bforall_unfold:
|
huffman@48213
|
84 |
"Trueprop (transfer_bforall P (\<lambda>x. Q x)) \<equiv> (\<And>x. P x \<Longrightarrow> Q x)"
|
huffman@48213
|
85 |
unfolding transfer_bforall_def atomize_imp atomize_all ..
|
huffman@48213
|
86 |
|
huffman@48529
|
87 |
lemma transfer_start: "\<lbrakk>P; Rel (op =) P Q\<rbrakk> \<Longrightarrow> Q"
|
huffman@48196
|
88 |
unfolding Rel_def by simp
|
huffman@48196
|
89 |
|
huffman@48529
|
90 |
lemma transfer_start': "\<lbrakk>P; Rel (op \<longrightarrow>) P Q\<rbrakk> \<Longrightarrow> Q"
|
huffman@48196
|
91 |
unfolding Rel_def by simp
|
huffman@48196
|
92 |
|
huffman@48500
|
93 |
lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
|
huffman@48489
|
94 |
by simp
|
huffman@48489
|
95 |
|
huffman@53495
|
96 |
lemma untransfer_start: "\<lbrakk>Q; Rel (op =) P Q\<rbrakk> \<Longrightarrow> P"
|
huffman@53495
|
97 |
unfolding Rel_def by simp
|
huffman@53495
|
98 |
|
huffman@48196
|
99 |
lemma Rel_eq_refl: "Rel (op =) x x"
|
huffman@48196
|
100 |
unfolding Rel_def ..
|
huffman@48196
|
101 |
|
huffman@48660
|
102 |
lemma Rel_app:
|
huffman@48394
|
103 |
assumes "Rel (A ===> B) f g" and "Rel A x y"
|
huffman@48660
|
104 |
shows "Rel B (f x) (g y)"
|
blanchet@57287
|
105 |
using assms unfolding Rel_def rel_fun_def by fast
|
huffman@48394
|
106 |
|
huffman@48660
|
107 |
lemma Rel_abs:
|
huffman@48394
|
108 |
assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
|
huffman@48660
|
109 |
shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
|
blanchet@57287
|
110 |
using assms unfolding Rel_def rel_fun_def by fast
|
huffman@48394
|
111 |
|
huffman@48196
|
112 |
subsection {* Predicates on relations, i.e. ``class constraints'' *}
|
huffman@48196
|
113 |
|
kuncar@57860
|
114 |
definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
kuncar@57860
|
115 |
where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
|
kuncar@57860
|
116 |
|
kuncar@57860
|
117 |
definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
kuncar@57860
|
118 |
where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
|
kuncar@57860
|
119 |
|
huffman@48196
|
120 |
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
huffman@48196
|
121 |
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)"
|
huffman@48196
|
122 |
|
huffman@48196
|
123 |
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
huffman@48196
|
124 |
where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)"
|
huffman@48196
|
125 |
|
huffman@48196
|
126 |
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
huffman@48196
|
127 |
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)"
|
huffman@48196
|
128 |
|
huffman@48196
|
129 |
definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
huffman@48196
|
130 |
where "bi_unique R \<longleftrightarrow>
|
huffman@48196
|
131 |
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
|
huffman@48196
|
132 |
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
|
huffman@48196
|
133 |
|
kuncar@57860
|
134 |
lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
|
kuncar@57860
|
135 |
unfolding left_unique_def by blast
|
kuncar@57860
|
136 |
|
kuncar@57860
|
137 |
lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
|
kuncar@57860
|
138 |
unfolding left_unique_def by blast
|
kuncar@57860
|
139 |
|
kuncar@57860
|
140 |
lemma left_totalI:
|
kuncar@57860
|
141 |
"(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
|
kuncar@57860
|
142 |
unfolding left_total_def by blast
|
kuncar@57860
|
143 |
|
kuncar@57860
|
144 |
lemma left_totalE:
|
kuncar@57860
|
145 |
assumes "left_total R"
|
kuncar@57860
|
146 |
obtains "(\<And>x. \<exists>y. R x y)"
|
kuncar@57860
|
147 |
using assms unfolding left_total_def by blast
|
kuncar@57860
|
148 |
|
Andreas@55064
|
149 |
lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
|
Andreas@55064
|
150 |
by(simp add: bi_unique_def)
|
Andreas@55064
|
151 |
|
Andreas@55064
|
152 |
lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z"
|
Andreas@55064
|
153 |
by(simp add: bi_unique_def)
|
Andreas@55064
|
154 |
|
Andreas@55064
|
155 |
lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
|
blanchet@57427
|
156 |
unfolding right_unique_def by fast
|
Andreas@55064
|
157 |
|
Andreas@55064
|
158 |
lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
|
blanchet@57427
|
159 |
unfolding right_unique_def by fast
|
Andreas@55064
|
160 |
|
kuncar@57866
|
161 |
lemma right_total_alt_def2:
|
huffman@48196
|
162 |
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
|
blanchet@57287
|
163 |
unfolding right_total_def rel_fun_def
|
huffman@48196
|
164 |
apply (rule iffI, fast)
|
huffman@48196
|
165 |
apply (rule allI)
|
huffman@48196
|
166 |
apply (drule_tac x="\<lambda>x. True" in spec)
|
huffman@48196
|
167 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
|
huffman@48196
|
168 |
apply fast
|
huffman@48196
|
169 |
done
|
huffman@48196
|
170 |
|
kuncar@57866
|
171 |
lemma right_unique_alt_def2:
|
huffman@48196
|
172 |
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)"
|
blanchet@57287
|
173 |
unfolding right_unique_def rel_fun_def by auto
|
huffman@48196
|
174 |
|
kuncar@57866
|
175 |
lemma bi_total_alt_def2:
|
huffman@48196
|
176 |
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All"
|
blanchet@57287
|
177 |
unfolding bi_total_def rel_fun_def
|
huffman@48196
|
178 |
apply (rule iffI, fast)
|
huffman@48196
|
179 |
apply safe
|
huffman@48196
|
180 |
apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec)
|
huffman@48196
|
181 |
apply (drule_tac x="\<lambda>y. True" in spec)
|
huffman@48196
|
182 |
apply fast
|
huffman@48196
|
183 |
apply (drule_tac x="\<lambda>x. True" in spec)
|
huffman@48196
|
184 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
|
huffman@48196
|
185 |
apply fast
|
huffman@48196
|
186 |
done
|
huffman@48196
|
187 |
|
kuncar@57866
|
188 |
lemma bi_unique_alt_def2:
|
huffman@48196
|
189 |
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
|
blanchet@57287
|
190 |
unfolding bi_unique_def rel_fun_def by auto
|
huffman@48196
|
191 |
|
kuncar@57860
|
192 |
lemma [simp]:
|
kuncar@57860
|
193 |
shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
|
kuncar@57860
|
194 |
and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
|
kuncar@57860
|
195 |
by(auto simp add: left_unique_def right_unique_def)
|
kuncar@57860
|
196 |
|
kuncar@57860
|
197 |
lemma [simp]:
|
kuncar@57860
|
198 |
shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
|
kuncar@57860
|
199 |
and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
|
kuncar@57860
|
200 |
by(simp_all add: left_total_def right_total_def)
|
kuncar@57860
|
201 |
|
Andreas@55081
|
202 |
lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
|
Andreas@55081
|
203 |
by(auto simp add: bi_unique_def)
|
Andreas@55081
|
204 |
|
Andreas@55081
|
205 |
lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
|
Andreas@55081
|
206 |
by(auto simp add: bi_total_def)
|
Andreas@55081
|
207 |
|
kuncar@57866
|
208 |
lemma right_unique_alt_def: "right_unique R = (conversep R OO R \<le> op=)" unfolding right_unique_def by blast
|
kuncar@57866
|
209 |
lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \<le> op=)" unfolding left_unique_def by blast
|
kuncar@57866
|
210 |
|
kuncar@57866
|
211 |
lemma right_total_alt_def: "right_total R = (conversep R OO R \<ge> op=)" unfolding right_total_def by blast
|
kuncar@57866
|
212 |
lemma left_total_alt_def: "left_total R = (R OO conversep R \<ge> op=)" unfolding left_total_def by blast
|
kuncar@57866
|
213 |
|
kuncar@57866
|
214 |
lemma bi_total_alt_def: "bi_total A = (left_total A \<and> right_total A)"
|
kuncar@57860
|
215 |
unfolding left_total_def right_total_def bi_total_def by blast
|
kuncar@57860
|
216 |
|
kuncar@57866
|
217 |
lemma bi_unique_alt_def: "bi_unique A = (left_unique A \<and> right_unique A)"
|
kuncar@57860
|
218 |
unfolding left_unique_def right_unique_def bi_unique_def by blast
|
kuncar@57860
|
219 |
|
kuncar@57860
|
220 |
lemma bi_totalI: "left_total R \<Longrightarrow> right_total R \<Longrightarrow> bi_total R"
|
kuncar@57866
|
221 |
unfolding bi_total_alt_def ..
|
kuncar@57860
|
222 |
|
kuncar@57860
|
223 |
lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R"
|
kuncar@57866
|
224 |
unfolding bi_unique_alt_def ..
|
kuncar@57860
|
225 |
|
kuncar@57866
|
226 |
end
|
kuncar@57866
|
227 |
|
kuncar@57866
|
228 |
subsection {* Equality restricted by a predicate *}
|
kuncar@57866
|
229 |
|
kuncar@57866
|
230 |
definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
|
kuncar@57866
|
231 |
where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
|
kuncar@57866
|
232 |
|
kuncar@57866
|
233 |
lemma eq_onp_Grp: "eq_onp P = BNF_Util.Grp (Collect P) id"
|
kuncar@57866
|
234 |
unfolding eq_onp_def Grp_def by auto
|
kuncar@57866
|
235 |
|
kuncar@57866
|
236 |
lemma eq_onp_to_eq:
|
kuncar@57866
|
237 |
assumes "eq_onp P x y"
|
kuncar@57866
|
238 |
shows "x = y"
|
kuncar@57866
|
239 |
using assms by (simp add: eq_onp_def)
|
kuncar@57866
|
240 |
|
kuncar@57866
|
241 |
lemma eq_onp_same_args:
|
kuncar@57866
|
242 |
shows "eq_onp P x x = P x"
|
kuncar@57866
|
243 |
using assms by (auto simp add: eq_onp_def)
|
kuncar@57866
|
244 |
|
kuncar@57866
|
245 |
lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
|
kuncar@57866
|
246 |
by (metis mem_Collect_eq subset_eq)
|
kuncar@57866
|
247 |
|
kuncar@57866
|
248 |
ML_file "Tools/Transfer/transfer.ML"
|
kuncar@57866
|
249 |
setup Transfer.setup
|
kuncar@57866
|
250 |
declare refl [transfer_rule]
|
kuncar@57866
|
251 |
|
kuncar@57866
|
252 |
ML_file "Tools/Transfer/transfer_bnf.ML"
|
kuncar@57866
|
253 |
|
kuncar@57866
|
254 |
declare pred_fun_def [simp]
|
kuncar@57866
|
255 |
declare rel_fun_eq [relator_eq]
|
kuncar@57866
|
256 |
|
kuncar@57866
|
257 |
hide_const (open) Rel
|
kuncar@57866
|
258 |
|
kuncar@57866
|
259 |
context
|
kuncar@57866
|
260 |
begin
|
kuncar@57866
|
261 |
interpretation lifting_syntax .
|
kuncar@57866
|
262 |
|
kuncar@57866
|
263 |
text {* Handling of domains *}
|
kuncar@57866
|
264 |
|
kuncar@57866
|
265 |
lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
|
kuncar@57866
|
266 |
by auto
|
kuncar@57866
|
267 |
|
kuncar@57866
|
268 |
lemma Domaimp_refl[transfer_domain_rule]:
|
kuncar@57866
|
269 |
"Domainp T = Domainp T" ..
|
kuncar@57866
|
270 |
|
kuncar@57866
|
271 |
lemma Domainp_prod_fun_eq[relator_domain]:
|
kuncar@57866
|
272 |
"Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
|
kuncar@57866
|
273 |
by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
|
kuncar@57860
|
274 |
|
huffman@48531
|
275 |
text {* Properties are preserved by relation composition. *}
|
huffman@48531
|
276 |
|
huffman@48531
|
277 |
lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"
|
huffman@48531
|
278 |
by auto
|
huffman@48531
|
279 |
|
huffman@48531
|
280 |
lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)"
|
blanchet@57427
|
281 |
unfolding bi_total_def OO_def by fast
|
huffman@48531
|
282 |
|
huffman@48531
|
283 |
lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)"
|
blanchet@57427
|
284 |
unfolding bi_unique_def OO_def by blast
|
huffman@48531
|
285 |
|
huffman@48531
|
286 |
lemma right_total_OO:
|
huffman@48531
|
287 |
"\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)"
|
blanchet@57427
|
288 |
unfolding right_total_def OO_def by fast
|
huffman@48531
|
289 |
|
huffman@48531
|
290 |
lemma right_unique_OO:
|
huffman@48531
|
291 |
"\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)"
|
blanchet@57427
|
292 |
unfolding right_unique_def OO_def by fast
|
huffman@48531
|
293 |
|
kuncar@57860
|
294 |
lemma left_total_OO: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
|
kuncar@57860
|
295 |
unfolding left_total_def OO_def by fast
|
kuncar@57860
|
296 |
|
kuncar@57860
|
297 |
lemma left_unique_OO: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
|
kuncar@57860
|
298 |
unfolding left_unique_def OO_def by blast
|
kuncar@57860
|
299 |
|
huffman@48196
|
300 |
|
huffman@48196
|
301 |
subsection {* Properties of relators *}
|
huffman@48196
|
302 |
|
kuncar@57860
|
303 |
lemma left_total_eq[transfer_rule]: "left_total op="
|
kuncar@57860
|
304 |
unfolding left_total_def by blast
|
kuncar@57860
|
305 |
|
kuncar@57860
|
306 |
lemma left_unique_eq[transfer_rule]: "left_unique op="
|
kuncar@57860
|
307 |
unfolding left_unique_def by blast
|
kuncar@57860
|
308 |
|
kuncar@57860
|
309 |
lemma right_total_eq [transfer_rule]: "right_total op="
|
huffman@48196
|
310 |
unfolding right_total_def by simp
|
huffman@48196
|
311 |
|
kuncar@57860
|
312 |
lemma right_unique_eq [transfer_rule]: "right_unique op="
|
huffman@48196
|
313 |
unfolding right_unique_def by simp
|
huffman@48196
|
314 |
|
kuncar@57860
|
315 |
lemma bi_total_eq[transfer_rule]: "bi_total (op =)"
|
huffman@48196
|
316 |
unfolding bi_total_def by simp
|
huffman@48196
|
317 |
|
kuncar@57860
|
318 |
lemma bi_unique_eq[transfer_rule]: "bi_unique (op =)"
|
huffman@48196
|
319 |
unfolding bi_unique_def by simp
|
huffman@48196
|
320 |
|
kuncar@57860
|
321 |
lemma left_total_fun[transfer_rule]:
|
kuncar@57860
|
322 |
"\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
|
kuncar@57860
|
323 |
unfolding left_total_def rel_fun_def
|
kuncar@57860
|
324 |
apply (rule allI, rename_tac f)
|
kuncar@57860
|
325 |
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
|
kuncar@57860
|
326 |
apply clarify
|
kuncar@57860
|
327 |
apply (subgoal_tac "(THE x. A x y) = x", simp)
|
kuncar@57860
|
328 |
apply (rule someI_ex)
|
kuncar@57860
|
329 |
apply (simp)
|
kuncar@57860
|
330 |
apply (rule the_equality)
|
kuncar@57860
|
331 |
apply assumption
|
kuncar@57860
|
332 |
apply (simp add: left_unique_def)
|
kuncar@57860
|
333 |
done
|
kuncar@57860
|
334 |
|
kuncar@57860
|
335 |
lemma left_unique_fun[transfer_rule]:
|
kuncar@57860
|
336 |
"\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
|
kuncar@57860
|
337 |
unfolding left_total_def left_unique_def rel_fun_def
|
kuncar@57860
|
338 |
by (clarify, rule ext, fast)
|
kuncar@57860
|
339 |
|
huffman@48196
|
340 |
lemma right_total_fun [transfer_rule]:
|
huffman@48196
|
341 |
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
|
blanchet@57287
|
342 |
unfolding right_total_def rel_fun_def
|
huffman@48196
|
343 |
apply (rule allI, rename_tac g)
|
huffman@48196
|
344 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
|
huffman@48196
|
345 |
apply clarify
|
huffman@48196
|
346 |
apply (subgoal_tac "(THE y. A x y) = y", simp)
|
huffman@48196
|
347 |
apply (rule someI_ex)
|
huffman@48196
|
348 |
apply (simp)
|
huffman@48196
|
349 |
apply (rule the_equality)
|
huffman@48196
|
350 |
apply assumption
|
huffman@48196
|
351 |
apply (simp add: right_unique_def)
|
huffman@48196
|
352 |
done
|
huffman@48196
|
353 |
|
huffman@48196
|
354 |
lemma right_unique_fun [transfer_rule]:
|
huffman@48196
|
355 |
"\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
|
blanchet@57287
|
356 |
unfolding right_total_def right_unique_def rel_fun_def
|
huffman@48196
|
357 |
by (clarify, rule ext, fast)
|
huffman@48196
|
358 |
|
kuncar@57860
|
359 |
lemma bi_total_fun[transfer_rule]:
|
huffman@48196
|
360 |
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
|
kuncar@57866
|
361 |
unfolding bi_unique_alt_def bi_total_alt_def
|
kuncar@57860
|
362 |
by (blast intro: right_total_fun left_total_fun)
|
huffman@48196
|
363 |
|
kuncar@57860
|
364 |
lemma bi_unique_fun[transfer_rule]:
|
huffman@48196
|
365 |
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
|
kuncar@57866
|
366 |
unfolding bi_unique_alt_def bi_total_alt_def
|
kuncar@57860
|
367 |
by (blast intro: right_unique_fun left_unique_fun)
|
huffman@48196
|
368 |
|
huffman@48500
|
369 |
subsection {* Transfer rules *}
|
huffman@48196
|
370 |
|
kuncar@55089
|
371 |
lemma Domainp_forall_transfer [transfer_rule]:
|
kuncar@55089
|
372 |
assumes "right_total A"
|
kuncar@55089
|
373 |
shows "((A ===> op =) ===> op =)
|
kuncar@55089
|
374 |
(transfer_bforall (Domainp A)) transfer_forall"
|
kuncar@55089
|
375 |
using assms unfolding right_total_def
|
blanchet@57287
|
376 |
unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff
|
blanchet@57427
|
377 |
by fast
|
kuncar@55089
|
378 |
|
huffman@48555
|
379 |
text {* Transfer rules using implication instead of equality on booleans. *}
|
huffman@48555
|
380 |
|
huffman@53491
|
381 |
lemma transfer_forall_transfer [transfer_rule]:
|
huffman@53491
|
382 |
"bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
|
huffman@53491
|
383 |
"right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall"
|
huffman@53491
|
384 |
"right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall"
|
huffman@53491
|
385 |
"bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall"
|
huffman@53491
|
386 |
"bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
|
blanchet@57287
|
387 |
unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def
|
blanchet@57427
|
388 |
by fast+
|
huffman@53491
|
389 |
|
huffman@53491
|
390 |
lemma transfer_implies_transfer [transfer_rule]:
|
huffman@53491
|
391 |
"(op = ===> op = ===> op = ) transfer_implies transfer_implies"
|
huffman@53491
|
392 |
"(rev_implies ===> implies ===> implies ) transfer_implies transfer_implies"
|
huffman@53491
|
393 |
"(rev_implies ===> op = ===> implies ) transfer_implies transfer_implies"
|
huffman@53491
|
394 |
"(op = ===> implies ===> implies ) transfer_implies transfer_implies"
|
huffman@53491
|
395 |
"(op = ===> op = ===> implies ) transfer_implies transfer_implies"
|
huffman@53491
|
396 |
"(implies ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
|
huffman@53491
|
397 |
"(implies ===> op = ===> rev_implies) transfer_implies transfer_implies"
|
huffman@53491
|
398 |
"(op = ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
|
huffman@53491
|
399 |
"(op = ===> op = ===> rev_implies) transfer_implies transfer_implies"
|
blanchet@57287
|
400 |
unfolding transfer_implies_def rev_implies_def rel_fun_def by auto
|
huffman@53491
|
401 |
|
huffman@48555
|
402 |
lemma eq_imp_transfer [transfer_rule]:
|
huffman@48555
|
403 |
"right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
|
kuncar@57866
|
404 |
unfolding right_unique_alt_def2 .
|
huffman@48555
|
405 |
|
kuncar@57860
|
406 |
text {* Transfer rules using equality. *}
|
kuncar@57860
|
407 |
|
kuncar@57860
|
408 |
lemma left_unique_transfer [transfer_rule]:
|
kuncar@57860
|
409 |
assumes "right_total A"
|
kuncar@57860
|
410 |
assumes "right_total B"
|
kuncar@57860
|
411 |
assumes "bi_unique A"
|
kuncar@57860
|
412 |
shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
|
kuncar@57860
|
413 |
using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
|
kuncar@57860
|
414 |
by metis
|
kuncar@57860
|
415 |
|
huffman@48501
|
416 |
lemma eq_transfer [transfer_rule]:
|
huffman@48196
|
417 |
assumes "bi_unique A"
|
huffman@48196
|
418 |
shows "(A ===> A ===> op =) (op =) (op =)"
|
blanchet@57287
|
419 |
using assms unfolding bi_unique_def rel_fun_def by auto
|
huffman@48196
|
420 |
|
kuncar@53093
|
421 |
lemma right_total_Ex_transfer[transfer_rule]:
|
kuncar@53093
|
422 |
assumes "right_total A"
|
kuncar@53093
|
423 |
shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
|
blanchet@57287
|
424 |
using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def]
|
blanchet@57427
|
425 |
by fast
|
kuncar@53093
|
426 |
|
kuncar@53093
|
427 |
lemma right_total_All_transfer[transfer_rule]:
|
kuncar@53093
|
428 |
assumes "right_total A"
|
kuncar@53093
|
429 |
shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All"
|
blanchet@57287
|
430 |
using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
|
blanchet@57427
|
431 |
by fast
|
kuncar@53093
|
432 |
|
huffman@48501
|
433 |
lemma All_transfer [transfer_rule]:
|
huffman@48196
|
434 |
assumes "bi_total A"
|
huffman@48196
|
435 |
shows "((A ===> op =) ===> op =) All All"
|
blanchet@57287
|
436 |
using assms unfolding bi_total_def rel_fun_def by fast
|
huffman@48196
|
437 |
|
huffman@48501
|
438 |
lemma Ex_transfer [transfer_rule]:
|
huffman@48196
|
439 |
assumes "bi_total A"
|
huffman@48196
|
440 |
shows "((A ===> op =) ===> op =) Ex Ex"
|
blanchet@57287
|
441 |
using assms unfolding bi_total_def rel_fun_def by fast
|
huffman@48196
|
442 |
|
huffman@48501
|
443 |
lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
|
blanchet@57287
|
444 |
unfolding rel_fun_def by simp
|
huffman@48196
|
445 |
|
huffman@48501
|
446 |
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
|
blanchet@57287
|
447 |
unfolding rel_fun_def by simp
|
huffman@48475
|
448 |
|
huffman@48501
|
449 |
lemma id_transfer [transfer_rule]: "(A ===> A) id id"
|
blanchet@57287
|
450 |
unfolding rel_fun_def by simp
|
huffman@48496
|
451 |
|
huffman@48501
|
452 |
lemma comp_transfer [transfer_rule]:
|
huffman@48196
|
453 |
"((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
|
blanchet@57287
|
454 |
unfolding rel_fun_def by simp
|
huffman@48196
|
455 |
|
huffman@48501
|
456 |
lemma fun_upd_transfer [transfer_rule]:
|
huffman@48196
|
457 |
assumes [transfer_rule]: "bi_unique A"
|
huffman@48196
|
458 |
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
|
huffman@48500
|
459 |
unfolding fun_upd_def [abs_def] by transfer_prover
|
huffman@48196
|
460 |
|
blanchet@56757
|
461 |
lemma case_nat_transfer [transfer_rule]:
|
blanchet@56757
|
462 |
"(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat"
|
blanchet@57287
|
463 |
unfolding rel_fun_def by (simp split: nat.split)
|
huffman@48498
|
464 |
|
blanchet@56757
|
465 |
lemma rec_nat_transfer [transfer_rule]:
|
blanchet@56757
|
466 |
"(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat"
|
blanchet@57287
|
467 |
unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
|
huffman@48939
|
468 |
|
huffman@48939
|
469 |
lemma funpow_transfer [transfer_rule]:
|
huffman@48939
|
470 |
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
|
huffman@48939
|
471 |
unfolding funpow_def by transfer_prover
|
huffman@48939
|
472 |
|
kuncar@55089
|
473 |
lemma mono_transfer[transfer_rule]:
|
kuncar@55089
|
474 |
assumes [transfer_rule]: "bi_total A"
|
kuncar@55089
|
475 |
assumes [transfer_rule]: "(A ===> A ===> op=) op\<le> op\<le>"
|
kuncar@55089
|
476 |
assumes [transfer_rule]: "(B ===> B ===> op=) op\<le> op\<le>"
|
kuncar@55089
|
477 |
shows "((A ===> B) ===> op=) mono mono"
|
kuncar@55089
|
478 |
unfolding mono_def[abs_def] by transfer_prover
|
huffman@48498
|
479 |
|
kuncar@55089
|
480 |
lemma right_total_relcompp_transfer[transfer_rule]:
|
kuncar@55089
|
481 |
assumes [transfer_rule]: "right_total B"
|
kuncar@55089
|
482 |
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=)
|
kuncar@55089
|
483 |
(\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO"
|
kuncar@55089
|
484 |
unfolding OO_def[abs_def] by transfer_prover
|
kuncar@55089
|
485 |
|
kuncar@55089
|
486 |
lemma relcompp_transfer[transfer_rule]:
|
kuncar@55089
|
487 |
assumes [transfer_rule]: "bi_total B"
|
kuncar@55089
|
488 |
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO"
|
kuncar@55089
|
489 |
unfolding OO_def[abs_def] by transfer_prover
|
kuncar@55089
|
490 |
|
kuncar@55089
|
491 |
lemma right_total_Domainp_transfer[transfer_rule]:
|
kuncar@55089
|
492 |
assumes [transfer_rule]: "right_total B"
|
kuncar@55089
|
493 |
shows "((A ===> B ===> op=) ===> A ===> op=) (\<lambda>T x. \<exists>y\<in>Collect(Domainp B). T x y) Domainp"
|
kuncar@55089
|
494 |
apply(subst(2) Domainp_iff[abs_def]) by transfer_prover
|
kuncar@55089
|
495 |
|
kuncar@55089
|
496 |
lemma Domainp_transfer[transfer_rule]:
|
kuncar@55089
|
497 |
assumes [transfer_rule]: "bi_total B"
|
kuncar@55089
|
498 |
shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp"
|
kuncar@55089
|
499 |
unfolding Domainp_iff[abs_def] by transfer_prover
|
kuncar@55089
|
500 |
|
kuncar@55089
|
501 |
lemma reflp_transfer[transfer_rule]:
|
kuncar@55089
|
502 |
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp"
|
kuncar@55089
|
503 |
"right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp"
|
kuncar@55089
|
504 |
"right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
|
kuncar@55089
|
505 |
"bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
|
kuncar@55089
|
506 |
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
|
blanchet@57287
|
507 |
using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
|
kuncar@55089
|
508 |
by fast+
|
kuncar@55089
|
509 |
|
kuncar@55089
|
510 |
lemma right_unique_transfer [transfer_rule]:
|
kuncar@55089
|
511 |
assumes [transfer_rule]: "right_total A"
|
kuncar@55089
|
512 |
assumes [transfer_rule]: "right_total B"
|
kuncar@55089
|
513 |
assumes [transfer_rule]: "bi_unique B"
|
kuncar@55089
|
514 |
shows "((A ===> B ===> op=) ===> implies) right_unique right_unique"
|
blanchet@57287
|
515 |
using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
|
kuncar@55089
|
516 |
by metis
|
huffman@48196
|
517 |
|
kuncar@57866
|
518 |
lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
|
kuncar@57866
|
519 |
unfolding eq_onp_def rel_fun_def by auto
|
kuncar@57866
|
520 |
|
kuncar@57866
|
521 |
lemma rel_fun_eq_onp_rel:
|
kuncar@57866
|
522 |
shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
|
kuncar@57866
|
523 |
by (auto simp add: eq_onp_def rel_fun_def)
|
kuncar@57866
|
524 |
|
kuncar@57866
|
525 |
lemma eq_onp_transfer [transfer_rule]:
|
kuncar@57866
|
526 |
assumes [transfer_rule]: "bi_unique A"
|
kuncar@57866
|
527 |
shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
|
kuncar@57866
|
528 |
unfolding eq_onp_def[abs_def] by transfer_prover
|
kuncar@57866
|
529 |
|
huffman@48196
|
530 |
end
|
kuncar@54148
|
531 |
|
kuncar@54148
|
532 |
end
|