47325
|
1 |
(* Title: HOL/Transfer.thy
|
|
2 |
Author: Brian Huffman, TU Muenchen
|
|
3 |
*)
|
|
4 |
|
|
5 |
header {* Generic theorem transfer using relations *}
|
|
6 |
|
|
7 |
theory Transfer
|
|
8 |
imports Plain Hilbert_Choice
|
|
9 |
uses ("Tools/transfer.ML")
|
|
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 |
|
|
29 |
lemma fun_relE:
|
|
30 |
assumes "(A ===> B) f g" and "A x y"
|
|
31 |
obtains "B (f x) (g y)"
|
|
32 |
using assms by (simp add: fun_rel_def)
|
|
33 |
|
|
34 |
lemma fun_rel_eq:
|
|
35 |
shows "((op =) ===> (op =)) = (op =)"
|
|
36 |
by (auto simp add: fun_eq_iff elim: fun_relE)
|
|
37 |
|
|
38 |
lemma fun_rel_eq_rel:
|
|
39 |
shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
|
|
40 |
by (simp add: fun_rel_def)
|
|
41 |
|
|
42 |
|
|
43 |
subsection {* Transfer method *}
|
|
44 |
|
|
45 |
text {* Explicit tags for application, abstraction, and relation
|
|
46 |
membership allow for backward proof methods. *}
|
|
47 |
|
|
48 |
definition App :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
|
|
49 |
where "App f \<equiv> f"
|
|
50 |
|
|
51 |
definition Abs :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
|
|
52 |
where "Abs f \<equiv> f"
|
|
53 |
|
|
54 |
definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
|
|
55 |
where "Rel r \<equiv> r"
|
|
56 |
|
|
57 |
text {* Handling of meta-logic connectives *}
|
|
58 |
|
|
59 |
definition transfer_forall where
|
|
60 |
"transfer_forall \<equiv> All"
|
|
61 |
|
|
62 |
definition transfer_implies where
|
|
63 |
"transfer_implies \<equiv> op \<longrightarrow>"
|
|
64 |
|
|
65 |
lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))"
|
|
66 |
unfolding atomize_all transfer_forall_def ..
|
|
67 |
|
|
68 |
lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)"
|
|
69 |
unfolding atomize_imp transfer_implies_def ..
|
|
70 |
|
|
71 |
lemma transfer_start: "\<lbrakk>Rel (op =) P Q; P\<rbrakk> \<Longrightarrow> Q"
|
|
72 |
unfolding Rel_def by simp
|
|
73 |
|
|
74 |
lemma transfer_start': "\<lbrakk>Rel (op \<longrightarrow>) P Q; P\<rbrakk> \<Longrightarrow> Q"
|
|
75 |
unfolding Rel_def by simp
|
|
76 |
|
|
77 |
lemma Rel_eq_refl: "Rel (op =) x x"
|
|
78 |
unfolding Rel_def ..
|
|
79 |
|
|
80 |
use "Tools/transfer.ML"
|
|
81 |
|
|
82 |
setup Transfer.setup
|
|
83 |
|
|
84 |
lemma Rel_App [transfer_raw]:
|
|
85 |
assumes "Rel (A ===> B) f g" and "Rel A x y"
|
|
86 |
shows "Rel B (App f x) (App g y)"
|
|
87 |
using assms unfolding Rel_def App_def fun_rel_def by fast
|
|
88 |
|
|
89 |
lemma Rel_Abs [transfer_raw]:
|
|
90 |
assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
|
|
91 |
shows "Rel (A ===> B) (Abs (\<lambda>x. f x)) (Abs (\<lambda>y. g y))"
|
|
92 |
using assms unfolding Rel_def Abs_def fun_rel_def by fast
|
|
93 |
|
|
94 |
hide_const (open) App Abs Rel
|
|
95 |
|
|
96 |
|
|
97 |
subsection {* Predicates on relations, i.e. ``class constraints'' *}
|
|
98 |
|
|
99 |
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
|
100 |
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)"
|
|
101 |
|
|
102 |
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
|
103 |
where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)"
|
|
104 |
|
|
105 |
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
|
106 |
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)"
|
|
107 |
|
|
108 |
definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
|
|
109 |
where "bi_unique R \<longleftrightarrow>
|
|
110 |
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
|
|
111 |
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
|
|
112 |
|
|
113 |
lemma right_total_alt_def:
|
|
114 |
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
|
|
115 |
unfolding right_total_def fun_rel_def
|
|
116 |
apply (rule iffI, fast)
|
|
117 |
apply (rule allI)
|
|
118 |
apply (drule_tac x="\<lambda>x. True" in spec)
|
|
119 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
|
|
120 |
apply fast
|
|
121 |
done
|
|
122 |
|
|
123 |
lemma right_unique_alt_def:
|
|
124 |
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)"
|
|
125 |
unfolding right_unique_def fun_rel_def by auto
|
|
126 |
|
|
127 |
lemma bi_total_alt_def:
|
|
128 |
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All"
|
|
129 |
unfolding bi_total_def fun_rel_def
|
|
130 |
apply (rule iffI, fast)
|
|
131 |
apply safe
|
|
132 |
apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec)
|
|
133 |
apply (drule_tac x="\<lambda>y. True" in spec)
|
|
134 |
apply fast
|
|
135 |
apply (drule_tac x="\<lambda>x. True" in spec)
|
|
136 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
|
|
137 |
apply fast
|
|
138 |
done
|
|
139 |
|
|
140 |
lemma bi_unique_alt_def:
|
|
141 |
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
|
|
142 |
unfolding bi_unique_def fun_rel_def by auto
|
|
143 |
|
|
144 |
|
|
145 |
subsection {* Properties of relators *}
|
|
146 |
|
|
147 |
lemma right_total_eq [transfer_rule]: "right_total (op =)"
|
|
148 |
unfolding right_total_def by simp
|
|
149 |
|
|
150 |
lemma right_unique_eq [transfer_rule]: "right_unique (op =)"
|
|
151 |
unfolding right_unique_def by simp
|
|
152 |
|
|
153 |
lemma bi_total_eq [transfer_rule]: "bi_total (op =)"
|
|
154 |
unfolding bi_total_def by simp
|
|
155 |
|
|
156 |
lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)"
|
|
157 |
unfolding bi_unique_def by simp
|
|
158 |
|
|
159 |
lemma right_total_fun [transfer_rule]:
|
|
160 |
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
|
|
161 |
unfolding right_total_def fun_rel_def
|
|
162 |
apply (rule allI, rename_tac g)
|
|
163 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
|
|
164 |
apply clarify
|
|
165 |
apply (subgoal_tac "(THE y. A x y) = y", simp)
|
|
166 |
apply (rule someI_ex)
|
|
167 |
apply (simp)
|
|
168 |
apply (rule the_equality)
|
|
169 |
apply assumption
|
|
170 |
apply (simp add: right_unique_def)
|
|
171 |
done
|
|
172 |
|
|
173 |
lemma right_unique_fun [transfer_rule]:
|
|
174 |
"\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
|
|
175 |
unfolding right_total_def right_unique_def fun_rel_def
|
|
176 |
by (clarify, rule ext, fast)
|
|
177 |
|
|
178 |
lemma bi_total_fun [transfer_rule]:
|
|
179 |
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
|
|
180 |
unfolding bi_total_def fun_rel_def
|
|
181 |
apply safe
|
|
182 |
apply (rename_tac f)
|
|
183 |
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
|
|
184 |
apply clarify
|
|
185 |
apply (subgoal_tac "(THE x. A x y) = x", simp)
|
|
186 |
apply (rule someI_ex)
|
|
187 |
apply (simp)
|
|
188 |
apply (rule the_equality)
|
|
189 |
apply assumption
|
|
190 |
apply (simp add: bi_unique_def)
|
|
191 |
apply (rename_tac g)
|
|
192 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
|
|
193 |
apply clarify
|
|
194 |
apply (subgoal_tac "(THE y. A x y) = y", simp)
|
|
195 |
apply (rule someI_ex)
|
|
196 |
apply (simp)
|
|
197 |
apply (rule the_equality)
|
|
198 |
apply assumption
|
|
199 |
apply (simp add: bi_unique_def)
|
|
200 |
done
|
|
201 |
|
|
202 |
lemma bi_unique_fun [transfer_rule]:
|
|
203 |
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
|
|
204 |
unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff
|
|
205 |
by (safe, metis, fast)
|
|
206 |
|
|
207 |
|
|
208 |
subsection {* Correspondence rules *}
|
|
209 |
|
|
210 |
lemma eq_parametric [transfer_rule]:
|
|
211 |
assumes "bi_unique A"
|
|
212 |
shows "(A ===> A ===> op =) (op =) (op =)"
|
|
213 |
using assms unfolding bi_unique_def fun_rel_def by auto
|
|
214 |
|
|
215 |
lemma All_parametric [transfer_rule]:
|
|
216 |
assumes "bi_total A"
|
|
217 |
shows "((A ===> op =) ===> op =) All All"
|
|
218 |
using assms unfolding bi_total_def fun_rel_def by fast
|
|
219 |
|
|
220 |
lemma Ex_parametric [transfer_rule]:
|
|
221 |
assumes "bi_total A"
|
|
222 |
shows "((A ===> op =) ===> op =) Ex Ex"
|
|
223 |
using assms unfolding bi_total_def fun_rel_def by fast
|
|
224 |
|
|
225 |
lemma If_parametric [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
|
|
226 |
unfolding fun_rel_def by simp
|
|
227 |
|
|
228 |
lemma comp_parametric [transfer_rule]:
|
|
229 |
"((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
|
|
230 |
unfolding fun_rel_def by simp
|
|
231 |
|
|
232 |
lemma fun_upd_parametric [transfer_rule]:
|
|
233 |
assumes [transfer_rule]: "bi_unique A"
|
|
234 |
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
|
|
235 |
unfolding fun_upd_def [abs_def] by correspondence
|
|
236 |
|
|
237 |
lemmas transfer_forall_parametric [transfer_rule]
|
|
238 |
= All_parametric [folded transfer_forall_def]
|
|
239 |
|
|
240 |
end
|