src/HOL/Transfer.thy
 author huffman Fri Apr 20 15:49:45 2012 +0200 (2012-04-20) changeset 47627 2b1d3eda59eb parent 47625 10cfaf771687 child 47635 ebb79474262c permissions -rw-r--r--
add secondary transfer rule for universal quantifiers on non-bi-total relations
 huffman@47325 1 (* Title: HOL/Transfer.thy huffman@47325 2 Author: Brian Huffman, TU Muenchen huffman@47325 3 *) huffman@47325 4 huffman@47325 5 header {* Generic theorem transfer using relations *} huffman@47325 6 huffman@47325 7 theory Transfer huffman@47325 8 imports Plain Hilbert_Choice huffman@47325 9 uses ("Tools/transfer.ML") huffman@47325 10 begin huffman@47325 11 huffman@47325 12 subsection {* Relator for function space *} huffman@47325 13 huffman@47325 14 definition huffman@47325 15 fun_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" (infixr "===>" 55) huffman@47325 16 where huffman@47325 17 "fun_rel A B = (\f g. \x y. A x y \ B (f x) (g y))" huffman@47325 18 huffman@47325 19 lemma fun_relI [intro]: huffman@47325 20 assumes "\x y. A x y \ B (f x) (g y)" huffman@47325 21 shows "(A ===> B) f g" huffman@47325 22 using assms by (simp add: fun_rel_def) huffman@47325 23 huffman@47325 24 lemma fun_relD: huffman@47325 25 assumes "(A ===> B) f g" and "A x y" huffman@47325 26 shows "B (f x) (g y)" huffman@47325 27 using assms by (simp add: fun_rel_def) huffman@47325 28 huffman@47325 29 lemma fun_relE: huffman@47325 30 assumes "(A ===> B) f g" and "A x y" huffman@47325 31 obtains "B (f x) (g y)" huffman@47325 32 using assms by (simp add: fun_rel_def) huffman@47325 33 huffman@47325 34 lemma fun_rel_eq: huffman@47325 35 shows "((op =) ===> (op =)) = (op =)" huffman@47325 36 by (auto simp add: fun_eq_iff elim: fun_relE) huffman@47325 37 huffman@47325 38 lemma fun_rel_eq_rel: huffman@47325 39 shows "((op =) ===> R) = (\f g. \x. R (f x) (g x))" huffman@47325 40 by (simp add: fun_rel_def) huffman@47325 41 huffman@47325 42 huffman@47325 43 subsection {* Transfer method *} huffman@47325 44 huffman@47325 45 text {* Explicit tags for application, abstraction, and relation huffman@47325 46 membership allow for backward proof methods. *} huffman@47325 47 huffman@47325 48 definition App :: "('a \ 'b) \ 'a \ 'b" huffman@47325 49 where "App f \ f" huffman@47325 50 huffman@47325 51 definition Abs :: "('a \ 'b) \ 'a \ 'b" huffman@47325 52 where "Abs f \ f" huffman@47325 53 huffman@47325 54 definition Rel :: "('a \ 'b \ bool) \ 'a \ 'b \ bool" huffman@47325 55 where "Rel r \ r" huffman@47325 56 huffman@47325 57 text {* Handling of meta-logic connectives *} huffman@47325 58 huffman@47325 59 definition transfer_forall where huffman@47325 60 "transfer_forall \ All" huffman@47325 61 huffman@47325 62 definition transfer_implies where huffman@47325 63 "transfer_implies \ op \" huffman@47325 64 huffman@47355 65 definition transfer_bforall :: "('a \ bool) \ ('a \ bool) \ bool" huffman@47355 66 where "transfer_bforall \ (\P Q. \x. P x \ Q x)" huffman@47355 67 huffman@47325 68 lemma transfer_forall_eq: "(\x. P x) \ Trueprop (transfer_forall (\x. P x))" huffman@47325 69 unfolding atomize_all transfer_forall_def .. huffman@47325 70 huffman@47325 71 lemma transfer_implies_eq: "(A \ B) \ Trueprop (transfer_implies A B)" huffman@47325 72 unfolding atomize_imp transfer_implies_def .. huffman@47325 73 huffman@47355 74 lemma transfer_bforall_unfold: huffman@47355 75 "Trueprop (transfer_bforall P (\x. Q x)) \ (\x. P x \ Q x)" huffman@47355 76 unfolding transfer_bforall_def atomize_imp atomize_all .. huffman@47355 77 huffman@47325 78 lemma transfer_start: "\Rel (op =) P Q; P\ \ Q" huffman@47325 79 unfolding Rel_def by simp huffman@47325 80 huffman@47325 81 lemma transfer_start': "\Rel (op \) P Q; P\ \ Q" huffman@47325 82 unfolding Rel_def by simp huffman@47325 83 huffman@47618 84 lemma correspondence_start: "\x = x'; Rel R x' y\ \ Rel R x y" huffman@47618 85 by simp huffman@47618 86 huffman@47325 87 lemma Rel_eq_refl: "Rel (op =) x x" huffman@47325 88 unfolding Rel_def .. huffman@47325 89 huffman@47523 90 lemma Rel_App: huffman@47523 91 assumes "Rel (A ===> B) f g" and "Rel A x y" huffman@47523 92 shows "Rel B (App f x) (App g y)" huffman@47523 93 using assms unfolding Rel_def App_def fun_rel_def by fast huffman@47523 94 huffman@47523 95 lemma Rel_Abs: huffman@47523 96 assumes "\x y. Rel A x y \ Rel B (f x) (g y)" huffman@47523 97 shows "Rel (A ===> B) (Abs (\x. f x)) (Abs (\y. g y))" huffman@47523 98 using assms unfolding Rel_def Abs_def fun_rel_def by fast huffman@47523 99 huffman@47325 100 use "Tools/transfer.ML" huffman@47325 101 huffman@47325 102 setup Transfer.setup huffman@47325 103 huffman@47503 104 declare fun_rel_eq [relator_eq] huffman@47503 105 huffman@47325 106 hide_const (open) App Abs Rel huffman@47325 107 huffman@47325 108 huffman@47325 109 subsection {* Predicates on relations, i.e. ``class constraints'' *} huffman@47325 110 huffman@47325 111 definition right_total :: "('a \ 'b \ bool) \ bool" huffman@47325 112 where "right_total R \ (\y. \x. R x y)" huffman@47325 113 huffman@47325 114 definition right_unique :: "('a \ 'b \ bool) \ bool" huffman@47325 115 where "right_unique R \ (\x y z. R x y \ R x z \ y = z)" huffman@47325 116 huffman@47325 117 definition bi_total :: "('a \ 'b \ bool) \ bool" huffman@47325 118 where "bi_total R \ (\x. \y. R x y) \ (\y. \x. R x y)" huffman@47325 119 huffman@47325 120 definition bi_unique :: "('a \ 'b \ bool) \ bool" huffman@47325 121 where "bi_unique R \ huffman@47325 122 (\x y z. R x y \ R x z \ y = z) \ huffman@47325 123 (\x y z. R x z \ R y z \ x = y)" huffman@47325 124 huffman@47325 125 lemma right_total_alt_def: huffman@47325 126 "right_total R \ ((R ===> op \) ===> op \) All All" huffman@47325 127 unfolding right_total_def fun_rel_def huffman@47325 128 apply (rule iffI, fast) huffman@47325 129 apply (rule allI) huffman@47325 130 apply (drule_tac x="\x. True" in spec) huffman@47325 131 apply (drule_tac x="\y. \x. R x y" in spec) huffman@47325 132 apply fast huffman@47325 133 done huffman@47325 134 huffman@47325 135 lemma right_unique_alt_def: huffman@47325 136 "right_unique R \ (R ===> R ===> op \) (op =) (op =)" huffman@47325 137 unfolding right_unique_def fun_rel_def by auto huffman@47325 138 huffman@47325 139 lemma bi_total_alt_def: huffman@47325 140 "bi_total R \ ((R ===> op =) ===> op =) All All" huffman@47325 141 unfolding bi_total_def fun_rel_def huffman@47325 142 apply (rule iffI, fast) huffman@47325 143 apply safe huffman@47325 144 apply (drule_tac x="\x. \y. R x y" in spec) huffman@47325 145 apply (drule_tac x="\y. True" in spec) huffman@47325 146 apply fast huffman@47325 147 apply (drule_tac x="\x. True" in spec) huffman@47325 148 apply (drule_tac x="\y. \x. R x y" in spec) huffman@47325 149 apply fast huffman@47325 150 done huffman@47325 151 huffman@47325 152 lemma bi_unique_alt_def: huffman@47325 153 "bi_unique R \ (R ===> R ===> op =) (op =) (op =)" huffman@47325 154 unfolding bi_unique_def fun_rel_def by auto huffman@47325 155 huffman@47325 156 huffman@47325 157 subsection {* Properties of relators *} huffman@47325 158 huffman@47325 159 lemma right_total_eq [transfer_rule]: "right_total (op =)" huffman@47325 160 unfolding right_total_def by simp huffman@47325 161 huffman@47325 162 lemma right_unique_eq [transfer_rule]: "right_unique (op =)" huffman@47325 163 unfolding right_unique_def by simp huffman@47325 164 huffman@47325 165 lemma bi_total_eq [transfer_rule]: "bi_total (op =)" huffman@47325 166 unfolding bi_total_def by simp huffman@47325 167 huffman@47325 168 lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)" huffman@47325 169 unfolding bi_unique_def by simp huffman@47325 170 huffman@47325 171 lemma right_total_fun [transfer_rule]: huffman@47325 172 "\right_unique A; right_total B\ \ right_total (A ===> B)" huffman@47325 173 unfolding right_total_def fun_rel_def huffman@47325 174 apply (rule allI, rename_tac g) huffman@47325 175 apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) huffman@47325 176 apply clarify huffman@47325 177 apply (subgoal_tac "(THE y. A x y) = y", simp) huffman@47325 178 apply (rule someI_ex) huffman@47325 179 apply (simp) huffman@47325 180 apply (rule the_equality) huffman@47325 181 apply assumption huffman@47325 182 apply (simp add: right_unique_def) huffman@47325 183 done huffman@47325 184 huffman@47325 185 lemma right_unique_fun [transfer_rule]: huffman@47325 186 "\right_total A; right_unique B\ \ right_unique (A ===> B)" huffman@47325 187 unfolding right_total_def right_unique_def fun_rel_def huffman@47325 188 by (clarify, rule ext, fast) huffman@47325 189 huffman@47325 190 lemma bi_total_fun [transfer_rule]: huffman@47325 191 "\bi_unique A; bi_total B\ \ bi_total (A ===> B)" huffman@47325 192 unfolding bi_total_def fun_rel_def huffman@47325 193 apply safe huffman@47325 194 apply (rename_tac f) huffman@47325 195 apply (rule_tac x="\y. SOME z. B (f (THE x. A x y)) z" in exI) huffman@47325 196 apply clarify huffman@47325 197 apply (subgoal_tac "(THE x. A x y) = x", simp) huffman@47325 198 apply (rule someI_ex) huffman@47325 199 apply (simp) huffman@47325 200 apply (rule the_equality) huffman@47325 201 apply assumption huffman@47325 202 apply (simp add: bi_unique_def) huffman@47325 203 apply (rename_tac g) huffman@47325 204 apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) huffman@47325 205 apply clarify huffman@47325 206 apply (subgoal_tac "(THE y. A x y) = y", simp) huffman@47325 207 apply (rule someI_ex) huffman@47325 208 apply (simp) huffman@47325 209 apply (rule the_equality) huffman@47325 210 apply assumption huffman@47325 211 apply (simp add: bi_unique_def) huffman@47325 212 done huffman@47325 213 huffman@47325 214 lemma bi_unique_fun [transfer_rule]: huffman@47325 215 "\bi_total A; bi_unique B\ \ bi_unique (A ===> B)" huffman@47325 216 unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff huffman@47325 217 by (safe, metis, fast) huffman@47325 218 huffman@47325 219 huffman@47325 220 subsection {* Correspondence rules *} huffman@47325 221 huffman@47325 222 lemma eq_parametric [transfer_rule]: huffman@47325 223 assumes "bi_unique A" huffman@47325 224 shows "(A ===> A ===> op =) (op =) (op =)" huffman@47325 225 using assms unfolding bi_unique_def fun_rel_def by auto huffman@47325 226 huffman@47325 227 lemma All_parametric [transfer_rule]: huffman@47325 228 assumes "bi_total A" huffman@47325 229 shows "((A ===> op =) ===> op =) All All" huffman@47325 230 using assms unfolding bi_total_def fun_rel_def by fast huffman@47325 231 huffman@47325 232 lemma Ex_parametric [transfer_rule]: huffman@47325 233 assumes "bi_total A" huffman@47325 234 shows "((A ===> op =) ===> op =) Ex Ex" huffman@47325 235 using assms unfolding bi_total_def fun_rel_def by fast huffman@47325 236 huffman@47325 237 lemma If_parametric [transfer_rule]: "(op = ===> A ===> A ===> A) If If" huffman@47325 238 unfolding fun_rel_def by simp huffman@47325 239 huffman@47612 240 lemma Let_parametric [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" huffman@47612 241 unfolding fun_rel_def by simp huffman@47612 242 huffman@47625 243 lemma id_parametric [transfer_rule]: "(A ===> A) id id" huffman@47625 244 unfolding fun_rel_def by simp huffman@47625 245 huffman@47325 246 lemma comp_parametric [transfer_rule]: huffman@47325 247 "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \) (op \)" huffman@47325 248 unfolding fun_rel_def by simp huffman@47325 249 huffman@47325 250 lemma fun_upd_parametric [transfer_rule]: huffman@47325 251 assumes [transfer_rule]: "bi_unique A" huffman@47325 252 shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" huffman@47325 253 unfolding fun_upd_def [abs_def] by correspondence huffman@47325 254 huffman@47627 255 lemma Domainp_iff: "Domainp T x \ (\y. T x y)" huffman@47627 256 by auto huffman@47627 257 huffman@47627 258 text {* Fallback rule for transferring universal quantifiers over huffman@47627 259 correspondence relations that are not bi-total, and do not have huffman@47627 260 custom transfer rules (e.g. relations between function types). *} huffman@47627 261 huffman@47627 262 lemma Domainp_forall_transfer [transfer_rule]: huffman@47627 263 assumes "right_total A" huffman@47627 264 shows "((A ===> op =) ===> op =) huffman@47627 265 (transfer_bforall (Domainp A)) transfer_forall" huffman@47627 266 using assms unfolding right_total_def huffman@47627 267 unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff huffman@47627 268 by metis huffman@47627 269 huffman@47627 270 text {* Preferred rule for transferring universal quantifiers over huffman@47627 271 bi-total correspondence relations (later rules are tried first). *} huffman@47627 272 huffman@47627 273 lemma transfer_forall_parametric [transfer_rule]: huffman@47627 274 "bi_total A \ ((A ===> op =) ===> op =) transfer_forall transfer_forall" huffman@47627 275 unfolding transfer_forall_def by (rule All_parametric) huffman@47325 276 huffman@47325 277 end