author | huffman |
Wed, 04 Apr 2012 16:03:01 +0200 | |
changeset 47355 | 3d9d98e0f1a4 |
parent 47325 | ec6187036495 |
child 47503 | cb44d09d9d22 |
permissions | -rw-r--r-- |
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 |
||
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
65 |
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
|
66 |
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
|
67 |
|
47325 | 68 |
lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))" |
69 |
unfolding atomize_all transfer_forall_def .. |
|
70 |
||
71 |
lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)" |
|
72 |
unfolding atomize_imp transfer_implies_def .. |
|
73 |
||
47355
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
74 |
lemma transfer_bforall_unfold: |
3d9d98e0f1a4
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents:
47325
diff
changeset
|
75 |
"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
|
76 |
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
|
77 |
|
47325 | 78 |
lemma transfer_start: "\<lbrakk>Rel (op =) P Q; P\<rbrakk> \<Longrightarrow> Q" |
79 |
unfolding Rel_def by simp |
|
80 |
||
81 |
lemma transfer_start': "\<lbrakk>Rel (op \<longrightarrow>) P Q; P\<rbrakk> \<Longrightarrow> Q" |
|
82 |
unfolding Rel_def by simp |
|
83 |
||
84 |
lemma Rel_eq_refl: "Rel (op =) x x" |
|
85 |
unfolding Rel_def .. |
|
86 |
||
87 |
use "Tools/transfer.ML" |
|
88 |
||
89 |
setup Transfer.setup |
|
90 |
||
91 |
lemma Rel_App [transfer_raw]: |
|
92 |
assumes "Rel (A ===> B) f g" and "Rel A x y" |
|
93 |
shows "Rel B (App f x) (App g y)" |
|
94 |
using assms unfolding Rel_def App_def fun_rel_def by fast |
|
95 |
||
96 |
lemma Rel_Abs [transfer_raw]: |
|
97 |
assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)" |
|
98 |
shows "Rel (A ===> B) (Abs (\<lambda>x. f x)) (Abs (\<lambda>y. g y))" |
|
99 |
using assms unfolding Rel_def Abs_def fun_rel_def by fast |
|
100 |
||
101 |
hide_const (open) App Abs Rel |
|
102 |
||
103 |
||
104 |
subsection {* Predicates on relations, i.e. ``class constraints'' *} |
|
105 |
||
106 |
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
107 |
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)" |
|
108 |
||
109 |
definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
110 |
where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)" |
|
111 |
||
112 |
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
113 |
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)" |
|
114 |
||
115 |
definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
|
116 |
where "bi_unique R \<longleftrightarrow> |
|
117 |
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and> |
|
118 |
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)" |
|
119 |
||
120 |
lemma right_total_alt_def: |
|
121 |
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All" |
|
122 |
unfolding right_total_def fun_rel_def |
|
123 |
apply (rule iffI, fast) |
|
124 |
apply (rule allI) |
|
125 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
126 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
127 |
apply fast |
|
128 |
done |
|
129 |
||
130 |
lemma right_unique_alt_def: |
|
131 |
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)" |
|
132 |
unfolding right_unique_def fun_rel_def by auto |
|
133 |
||
134 |
lemma bi_total_alt_def: |
|
135 |
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All" |
|
136 |
unfolding bi_total_def fun_rel_def |
|
137 |
apply (rule iffI, fast) |
|
138 |
apply safe |
|
139 |
apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec) |
|
140 |
apply (drule_tac x="\<lambda>y. True" in spec) |
|
141 |
apply fast |
|
142 |
apply (drule_tac x="\<lambda>x. True" in spec) |
|
143 |
apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec) |
|
144 |
apply fast |
|
145 |
done |
|
146 |
||
147 |
lemma bi_unique_alt_def: |
|
148 |
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)" |
|
149 |
unfolding bi_unique_def fun_rel_def by auto |
|
150 |
||
151 |
||
152 |
subsection {* Properties of relators *} |
|
153 |
||
154 |
lemma right_total_eq [transfer_rule]: "right_total (op =)" |
|
155 |
unfolding right_total_def by simp |
|
156 |
||
157 |
lemma right_unique_eq [transfer_rule]: "right_unique (op =)" |
|
158 |
unfolding right_unique_def by simp |
|
159 |
||
160 |
lemma bi_total_eq [transfer_rule]: "bi_total (op =)" |
|
161 |
unfolding bi_total_def by simp |
|
162 |
||
163 |
lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)" |
|
164 |
unfolding bi_unique_def by simp |
|
165 |
||
166 |
lemma right_total_fun [transfer_rule]: |
|
167 |
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)" |
|
168 |
unfolding right_total_def fun_rel_def |
|
169 |
apply (rule allI, rename_tac g) |
|
170 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) |
|
171 |
apply clarify |
|
172 |
apply (subgoal_tac "(THE y. A x y) = y", simp) |
|
173 |
apply (rule someI_ex) |
|
174 |
apply (simp) |
|
175 |
apply (rule the_equality) |
|
176 |
apply assumption |
|
177 |
apply (simp add: right_unique_def) |
|
178 |
done |
|
179 |
||
180 |
lemma right_unique_fun [transfer_rule]: |
|
181 |
"\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)" |
|
182 |
unfolding right_total_def right_unique_def fun_rel_def |
|
183 |
by (clarify, rule ext, fast) |
|
184 |
||
185 |
lemma bi_total_fun [transfer_rule]: |
|
186 |
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)" |
|
187 |
unfolding bi_total_def fun_rel_def |
|
188 |
apply safe |
|
189 |
apply (rename_tac f) |
|
190 |
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI) |
|
191 |
apply clarify |
|
192 |
apply (subgoal_tac "(THE x. A x y) = x", simp) |
|
193 |
apply (rule someI_ex) |
|
194 |
apply (simp) |
|
195 |
apply (rule the_equality) |
|
196 |
apply assumption |
|
197 |
apply (simp add: bi_unique_def) |
|
198 |
apply (rename_tac g) |
|
199 |
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI) |
|
200 |
apply clarify |
|
201 |
apply (subgoal_tac "(THE y. A x y) = y", simp) |
|
202 |
apply (rule someI_ex) |
|
203 |
apply (simp) |
|
204 |
apply (rule the_equality) |
|
205 |
apply assumption |
|
206 |
apply (simp add: bi_unique_def) |
|
207 |
done |
|
208 |
||
209 |
lemma bi_unique_fun [transfer_rule]: |
|
210 |
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)" |
|
211 |
unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff |
|
212 |
by (safe, metis, fast) |
|
213 |
||
214 |
||
215 |
subsection {* Correspondence rules *} |
|
216 |
||
217 |
lemma eq_parametric [transfer_rule]: |
|
218 |
assumes "bi_unique A" |
|
219 |
shows "(A ===> A ===> op =) (op =) (op =)" |
|
220 |
using assms unfolding bi_unique_def fun_rel_def by auto |
|
221 |
||
222 |
lemma All_parametric [transfer_rule]: |
|
223 |
assumes "bi_total A" |
|
224 |
shows "((A ===> op =) ===> op =) All All" |
|
225 |
using assms unfolding bi_total_def fun_rel_def by fast |
|
226 |
||
227 |
lemma Ex_parametric [transfer_rule]: |
|
228 |
assumes "bi_total A" |
|
229 |
shows "((A ===> op =) ===> op =) Ex Ex" |
|
230 |
using assms unfolding bi_total_def fun_rel_def by fast |
|
231 |
||
232 |
lemma If_parametric [transfer_rule]: "(op = ===> A ===> A ===> A) If If" |
|
233 |
unfolding fun_rel_def by simp |
|
234 |
||
235 |
lemma comp_parametric [transfer_rule]: |
|
236 |
"((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)" |
|
237 |
unfolding fun_rel_def by simp |
|
238 |
||
239 |
lemma fun_upd_parametric [transfer_rule]: |
|
240 |
assumes [transfer_rule]: "bi_unique A" |
|
241 |
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" |
|
242 |
unfolding fun_upd_def [abs_def] by correspondence |
|
243 |
||
244 |
lemmas transfer_forall_parametric [transfer_rule] |
|
245 |
= All_parametric [folded transfer_forall_def] |
|
246 |
||
247 |
end |