src/HOL/Transfer.thy
 author huffman Fri Apr 27 14:07:31 2012 +0200 (2012-04-27) changeset 47789 71a526ee569a parent 47684 ead185e60b8c child 47924 4e951258204b permissions -rw-r--r--
implement transfer tactic with more scalable forward proof methods
 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@47789 45 text {* Explicit tag for relation membership allows for huffman@47789 46 backward proof methods. *} huffman@47325 47 huffman@47325 48 definition Rel :: "('a \ 'b \ bool) \ 'a \ 'b \ bool" huffman@47325 49 where "Rel r \ r" huffman@47325 50 huffman@47325 51 text {* Handling of meta-logic connectives *} huffman@47325 52 huffman@47325 53 definition transfer_forall where huffman@47325 54 "transfer_forall \ All" huffman@47325 55 huffman@47325 56 definition transfer_implies where huffman@47325 57 "transfer_implies \ op \" huffman@47325 58 huffman@47355 59 definition transfer_bforall :: "('a \ bool) \ ('a \ bool) \ bool" huffman@47355 60 where "transfer_bforall \ (\P Q. \x. P x \ Q x)" huffman@47355 61 huffman@47325 62 lemma transfer_forall_eq: "(\x. P x) \ Trueprop (transfer_forall (\x. P x))" huffman@47325 63 unfolding atomize_all transfer_forall_def .. huffman@47325 64 huffman@47325 65 lemma transfer_implies_eq: "(A \ B) \ Trueprop (transfer_implies A B)" huffman@47325 66 unfolding atomize_imp transfer_implies_def .. huffman@47325 67 huffman@47355 68 lemma transfer_bforall_unfold: huffman@47355 69 "Trueprop (transfer_bforall P (\x. Q x)) \ (\x. P x \ Q x)" huffman@47355 70 unfolding transfer_bforall_def atomize_imp atomize_all .. huffman@47355 71 huffman@47658 72 lemma transfer_start: "\P; Rel (op =) P Q\ \ Q" huffman@47325 73 unfolding Rel_def by simp huffman@47325 74 huffman@47658 75 lemma transfer_start': "\P; Rel (op \) P Q\ \ Q" huffman@47325 76 unfolding Rel_def by simp huffman@47325 77 huffman@47635 78 lemma transfer_prover_start: "\x = x'; Rel R x' y\ \ Rel R x y" huffman@47618 79 by simp huffman@47618 80 huffman@47325 81 lemma Rel_eq_refl: "Rel (op =) x x" huffman@47325 82 unfolding Rel_def .. huffman@47325 83 huffman@47789 84 lemma Rel_app: huffman@47523 85 assumes "Rel (A ===> B) f g" and "Rel A x y" huffman@47789 86 shows "Rel B (f x) (g y)" huffman@47789 87 using assms unfolding Rel_def fun_rel_def by fast huffman@47523 88 huffman@47789 89 lemma Rel_abs: huffman@47523 90 assumes "\x y. Rel A x y \ Rel B (f x) (g y)" huffman@47789 91 shows "Rel (A ===> B) (\x. f x) (\y. g y)" huffman@47789 92 using assms unfolding Rel_def fun_rel_def by fast huffman@47523 93 huffman@47325 94 use "Tools/transfer.ML" huffman@47325 95 huffman@47325 96 setup Transfer.setup huffman@47325 97 huffman@47503 98 declare fun_rel_eq [relator_eq] huffman@47503 99 huffman@47789 100 hide_const (open) Rel huffman@47325 101 huffman@47325 102 huffman@47325 103 subsection {* Predicates on relations, i.e. ``class constraints'' *} huffman@47325 104 huffman@47325 105 definition right_total :: "('a \ 'b \ bool) \ bool" huffman@47325 106 where "right_total R \ (\y. \x. R x y)" huffman@47325 107 huffman@47325 108 definition right_unique :: "('a \ 'b \ bool) \ bool" huffman@47325 109 where "right_unique R \ (\x y z. R x y \ R x z \ y = z)" huffman@47325 110 huffman@47325 111 definition bi_total :: "('a \ 'b \ bool) \ bool" huffman@47325 112 where "bi_total R \ (\x. \y. R x y) \ (\y. \x. R x y)" huffman@47325 113 huffman@47325 114 definition bi_unique :: "('a \ 'b \ bool) \ bool" huffman@47325 115 where "bi_unique R \ huffman@47325 116 (\x y z. R x y \ R x z \ y = z) \ huffman@47325 117 (\x y z. R x z \ R y z \ x = y)" huffman@47325 118 huffman@47325 119 lemma right_total_alt_def: huffman@47325 120 "right_total R \ ((R ===> op \) ===> op \) All All" huffman@47325 121 unfolding right_total_def fun_rel_def huffman@47325 122 apply (rule iffI, fast) huffman@47325 123 apply (rule allI) huffman@47325 124 apply (drule_tac x="\x. True" in spec) huffman@47325 125 apply (drule_tac x="\y. \x. R x y" in spec) huffman@47325 126 apply fast huffman@47325 127 done huffman@47325 128 huffman@47325 129 lemma right_unique_alt_def: huffman@47325 130 "right_unique R \ (R ===> R ===> op \) (op =) (op =)" huffman@47325 131 unfolding right_unique_def fun_rel_def by auto huffman@47325 132 huffman@47325 133 lemma bi_total_alt_def: huffman@47325 134 "bi_total R \ ((R ===> op =) ===> op =) All All" huffman@47325 135 unfolding bi_total_def fun_rel_def huffman@47325 136 apply (rule iffI, fast) huffman@47325 137 apply safe huffman@47325 138 apply (drule_tac x="\x. \y. R x y" in spec) huffman@47325 139 apply (drule_tac x="\y. True" in spec) huffman@47325 140 apply fast huffman@47325 141 apply (drule_tac x="\x. True" in spec) huffman@47325 142 apply (drule_tac x="\y. \x. R x y" in spec) huffman@47325 143 apply fast huffman@47325 144 done huffman@47325 145 huffman@47325 146 lemma bi_unique_alt_def: huffman@47325 147 "bi_unique R \ (R ===> R ===> op =) (op =) (op =)" huffman@47325 148 unfolding bi_unique_def fun_rel_def by auto huffman@47325 149 huffman@47660 150 text {* Properties are preserved by relation composition. *} huffman@47660 151 huffman@47660 152 lemma OO_def: "R OO S = (\x z. \y. R x y \ S y z)" huffman@47660 153 by auto huffman@47660 154 huffman@47660 155 lemma bi_total_OO: "\bi_total A; bi_total B\ \ bi_total (A OO B)" huffman@47660 156 unfolding bi_total_def OO_def by metis huffman@47660 157 huffman@47660 158 lemma bi_unique_OO: "\bi_unique A; bi_unique B\ \ bi_unique (A OO B)" huffman@47660 159 unfolding bi_unique_def OO_def by metis huffman@47660 160 huffman@47660 161 lemma right_total_OO: huffman@47660 162 "\right_total A; right_total B\ \ right_total (A OO B)" huffman@47660 163 unfolding right_total_def OO_def by metis huffman@47660 164 huffman@47660 165 lemma right_unique_OO: huffman@47660 166 "\right_unique A; right_unique B\ \ right_unique (A OO B)" huffman@47660 167 unfolding right_unique_def OO_def by metis huffman@47660 168 huffman@47325 169 huffman@47325 170 subsection {* Properties of relators *} huffman@47325 171 huffman@47325 172 lemma right_total_eq [transfer_rule]: "right_total (op =)" huffman@47325 173 unfolding right_total_def by simp huffman@47325 174 huffman@47325 175 lemma right_unique_eq [transfer_rule]: "right_unique (op =)" huffman@47325 176 unfolding right_unique_def by simp huffman@47325 177 huffman@47325 178 lemma bi_total_eq [transfer_rule]: "bi_total (op =)" huffman@47325 179 unfolding bi_total_def by simp huffman@47325 180 huffman@47325 181 lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)" huffman@47325 182 unfolding bi_unique_def by simp huffman@47325 183 huffman@47325 184 lemma right_total_fun [transfer_rule]: huffman@47325 185 "\right_unique A; right_total B\ \ right_total (A ===> B)" huffman@47325 186 unfolding right_total_def fun_rel_def huffman@47325 187 apply (rule allI, rename_tac g) huffman@47325 188 apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) huffman@47325 189 apply clarify huffman@47325 190 apply (subgoal_tac "(THE y. A x y) = y", simp) huffman@47325 191 apply (rule someI_ex) huffman@47325 192 apply (simp) huffman@47325 193 apply (rule the_equality) huffman@47325 194 apply assumption huffman@47325 195 apply (simp add: right_unique_def) huffman@47325 196 done huffman@47325 197 huffman@47325 198 lemma right_unique_fun [transfer_rule]: huffman@47325 199 "\right_total A; right_unique B\ \ right_unique (A ===> B)" huffman@47325 200 unfolding right_total_def right_unique_def fun_rel_def huffman@47325 201 by (clarify, rule ext, fast) huffman@47325 202 huffman@47325 203 lemma bi_total_fun [transfer_rule]: huffman@47325 204 "\bi_unique A; bi_total B\ \ bi_total (A ===> B)" huffman@47325 205 unfolding bi_total_def fun_rel_def huffman@47325 206 apply safe huffman@47325 207 apply (rename_tac f) huffman@47325 208 apply (rule_tac x="\y. SOME z. B (f (THE x. A x y)) z" in exI) huffman@47325 209 apply clarify huffman@47325 210 apply (subgoal_tac "(THE x. A x y) = x", simp) huffman@47325 211 apply (rule someI_ex) huffman@47325 212 apply (simp) huffman@47325 213 apply (rule the_equality) huffman@47325 214 apply assumption huffman@47325 215 apply (simp add: bi_unique_def) huffman@47325 216 apply (rename_tac g) huffman@47325 217 apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) huffman@47325 218 apply clarify huffman@47325 219 apply (subgoal_tac "(THE y. A x y) = y", simp) huffman@47325 220 apply (rule someI_ex) huffman@47325 221 apply (simp) huffman@47325 222 apply (rule the_equality) huffman@47325 223 apply assumption huffman@47325 224 apply (simp add: bi_unique_def) huffman@47325 225 done huffman@47325 226 huffman@47325 227 lemma bi_unique_fun [transfer_rule]: huffman@47325 228 "\bi_total A; bi_unique B\ \ bi_unique (A ===> B)" huffman@47325 229 unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff huffman@47325 230 by (safe, metis, fast) huffman@47325 231 huffman@47325 232 huffman@47635 233 subsection {* Transfer rules *} huffman@47325 234 huffman@47684 235 text {* Transfer rules using implication instead of equality on booleans. *} huffman@47684 236 huffman@47684 237 lemma eq_imp_transfer [transfer_rule]: huffman@47684 238 "right_unique A \ (A ===> A ===> op \) (op =) (op =)" huffman@47684 239 unfolding right_unique_alt_def . huffman@47684 240 huffman@47684 241 lemma forall_imp_transfer [transfer_rule]: huffman@47684 242 "right_total A \ ((A ===> op \) ===> op \) transfer_forall transfer_forall" huffman@47684 243 unfolding right_total_alt_def transfer_forall_def . huffman@47684 244 huffman@47636 245 lemma eq_transfer [transfer_rule]: huffman@47325 246 assumes "bi_unique A" huffman@47325 247 shows "(A ===> A ===> op =) (op =) (op =)" huffman@47325 248 using assms unfolding bi_unique_def fun_rel_def by auto huffman@47325 249 huffman@47636 250 lemma All_transfer [transfer_rule]: huffman@47325 251 assumes "bi_total A" huffman@47325 252 shows "((A ===> op =) ===> op =) All All" huffman@47325 253 using assms unfolding bi_total_def fun_rel_def by fast huffman@47325 254 huffman@47636 255 lemma Ex_transfer [transfer_rule]: huffman@47325 256 assumes "bi_total A" huffman@47325 257 shows "((A ===> op =) ===> op =) Ex Ex" huffman@47325 258 using assms unfolding bi_total_def fun_rel_def by fast huffman@47325 259 huffman@47636 260 lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If" huffman@47325 261 unfolding fun_rel_def by simp huffman@47325 262 huffman@47636 263 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" huffman@47612 264 unfolding fun_rel_def by simp huffman@47612 265 huffman@47636 266 lemma id_transfer [transfer_rule]: "(A ===> A) id id" huffman@47625 267 unfolding fun_rel_def by simp huffman@47625 268 huffman@47636 269 lemma comp_transfer [transfer_rule]: huffman@47325 270 "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \) (op \)" huffman@47325 271 unfolding fun_rel_def by simp huffman@47325 272 huffman@47636 273 lemma fun_upd_transfer [transfer_rule]: huffman@47325 274 assumes [transfer_rule]: "bi_unique A" huffman@47325 275 shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" huffman@47635 276 unfolding fun_upd_def [abs_def] by transfer_prover huffman@47325 277 huffman@47637 278 lemma nat_case_transfer [transfer_rule]: huffman@47637 279 "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case" huffman@47637 280 unfolding fun_rel_def by (simp split: nat.split) huffman@47627 281 huffman@47627 282 text {* Fallback rule for transferring universal quantifiers over huffman@47627 283 correspondence relations that are not bi-total, and do not have huffman@47627 284 custom transfer rules (e.g. relations between function types). *} huffman@47627 285 huffman@47637 286 lemma Domainp_iff: "Domainp T x \ (\y. T x y)" huffman@47637 287 by auto huffman@47637 288 huffman@47627 289 lemma Domainp_forall_transfer [transfer_rule]: huffman@47627 290 assumes "right_total A" huffman@47627 291 shows "((A ===> op =) ===> op =) huffman@47627 292 (transfer_bforall (Domainp A)) transfer_forall" huffman@47627 293 using assms unfolding right_total_def huffman@47627 294 unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff huffman@47627 295 by metis huffman@47627 296 huffman@47627 297 text {* Preferred rule for transferring universal quantifiers over huffman@47627 298 bi-total correspondence relations (later rules are tried first). *} huffman@47627 299 huffman@47636 300 lemma forall_transfer [transfer_rule]: huffman@47627 301 "bi_total A \ ((A ===> op =) ===> op =) transfer_forall transfer_forall" huffman@47636 302 unfolding transfer_forall_def by (rule All_transfer) huffman@47325 303 huffman@47325 304 end