src/HOL/Transfer.thy
 author huffman Sun Apr 22 11:05:04 2012 +0200 (2012-04-22) changeset 47660 7a5c681c0265 parent 47658 7631f6f7873d child 47684 ead185e60b8c permissions -rw-r--r--
new example theory for quotient/transfer
 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@47658 78 lemma transfer_start: "\P; Rel (op =) P Q\ \ Q" huffman@47325 79 unfolding Rel_def by simp huffman@47325 80 huffman@47658 81 lemma transfer_start': "\P; Rel (op \) P Q\ \ Q" huffman@47325 82 unfolding Rel_def by simp huffman@47325 83 huffman@47635 84 lemma transfer_prover_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@47660 156 text {* Properties are preserved by relation composition. *} huffman@47660 157 huffman@47660 158 lemma OO_def: "R OO S = (\x z. \y. R x y \ S y z)" huffman@47660 159 by auto huffman@47660 160 huffman@47660 161 lemma bi_total_OO: "\bi_total A; bi_total B\ \ bi_total (A OO B)" huffman@47660 162 unfolding bi_total_def OO_def by metis huffman@47660 163 huffman@47660 164 lemma bi_unique_OO: "\bi_unique A; bi_unique B\ \ bi_unique (A OO B)" huffman@47660 165 unfolding bi_unique_def OO_def by metis huffman@47660 166 huffman@47660 167 lemma right_total_OO: huffman@47660 168 "\right_total A; right_total B\ \ right_total (A OO B)" huffman@47660 169 unfolding right_total_def OO_def by metis huffman@47660 170 huffman@47660 171 lemma right_unique_OO: huffman@47660 172 "\right_unique A; right_unique B\ \ right_unique (A OO B)" huffman@47660 173 unfolding right_unique_def OO_def by metis huffman@47660 174 huffman@47325 175 huffman@47325 176 subsection {* Properties of relators *} huffman@47325 177 huffman@47325 178 lemma right_total_eq [transfer_rule]: "right_total (op =)" huffman@47325 179 unfolding right_total_def by simp huffman@47325 180 huffman@47325 181 lemma right_unique_eq [transfer_rule]: "right_unique (op =)" huffman@47325 182 unfolding right_unique_def by simp huffman@47325 183 huffman@47325 184 lemma bi_total_eq [transfer_rule]: "bi_total (op =)" huffman@47325 185 unfolding bi_total_def by simp huffman@47325 186 huffman@47325 187 lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)" huffman@47325 188 unfolding bi_unique_def by simp huffman@47325 189 huffman@47325 190 lemma right_total_fun [transfer_rule]: huffman@47325 191 "\right_unique A; right_total B\ \ right_total (A ===> B)" huffman@47325 192 unfolding right_total_def fun_rel_def huffman@47325 193 apply (rule allI, rename_tac g) huffman@47325 194 apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) huffman@47325 195 apply clarify huffman@47325 196 apply (subgoal_tac "(THE y. A x y) = y", simp) huffman@47325 197 apply (rule someI_ex) huffman@47325 198 apply (simp) huffman@47325 199 apply (rule the_equality) huffman@47325 200 apply assumption huffman@47325 201 apply (simp add: right_unique_def) huffman@47325 202 done huffman@47325 203 huffman@47325 204 lemma right_unique_fun [transfer_rule]: huffman@47325 205 "\right_total A; right_unique B\ \ right_unique (A ===> B)" huffman@47325 206 unfolding right_total_def right_unique_def fun_rel_def huffman@47325 207 by (clarify, rule ext, fast) huffman@47325 208 huffman@47325 209 lemma bi_total_fun [transfer_rule]: huffman@47325 210 "\bi_unique A; bi_total B\ \ bi_total (A ===> B)" huffman@47325 211 unfolding bi_total_def fun_rel_def huffman@47325 212 apply safe huffman@47325 213 apply (rename_tac f) huffman@47325 214 apply (rule_tac x="\y. SOME z. B (f (THE x. A x y)) z" in exI) huffman@47325 215 apply clarify huffman@47325 216 apply (subgoal_tac "(THE x. A x y) = x", simp) huffman@47325 217 apply (rule someI_ex) huffman@47325 218 apply (simp) huffman@47325 219 apply (rule the_equality) huffman@47325 220 apply assumption huffman@47325 221 apply (simp add: bi_unique_def) huffman@47325 222 apply (rename_tac g) huffman@47325 223 apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) huffman@47325 224 apply clarify huffman@47325 225 apply (subgoal_tac "(THE y. A x y) = y", simp) huffman@47325 226 apply (rule someI_ex) huffman@47325 227 apply (simp) huffman@47325 228 apply (rule the_equality) huffman@47325 229 apply assumption huffman@47325 230 apply (simp add: bi_unique_def) huffman@47325 231 done huffman@47325 232 huffman@47325 233 lemma bi_unique_fun [transfer_rule]: huffman@47325 234 "\bi_total A; bi_unique B\ \ bi_unique (A ===> B)" huffman@47325 235 unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff huffman@47325 236 by (safe, metis, fast) huffman@47325 237 huffman@47325 238 huffman@47635 239 subsection {* Transfer rules *} huffman@47325 240 huffman@47636 241 lemma eq_transfer [transfer_rule]: huffman@47325 242 assumes "bi_unique A" huffman@47325 243 shows "(A ===> A ===> op =) (op =) (op =)" huffman@47325 244 using assms unfolding bi_unique_def fun_rel_def by auto huffman@47325 245 huffman@47636 246 lemma All_transfer [transfer_rule]: huffman@47325 247 assumes "bi_total A" huffman@47325 248 shows "((A ===> op =) ===> op =) All All" huffman@47325 249 using assms unfolding bi_total_def fun_rel_def by fast huffman@47325 250 huffman@47636 251 lemma Ex_transfer [transfer_rule]: huffman@47325 252 assumes "bi_total A" huffman@47325 253 shows "((A ===> op =) ===> op =) Ex Ex" huffman@47325 254 using assms unfolding bi_total_def fun_rel_def by fast huffman@47325 255 huffman@47636 256 lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If" huffman@47325 257 unfolding fun_rel_def by simp huffman@47325 258 huffman@47636 259 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" huffman@47612 260 unfolding fun_rel_def by simp huffman@47612 261 huffman@47636 262 lemma id_transfer [transfer_rule]: "(A ===> A) id id" huffman@47625 263 unfolding fun_rel_def by simp huffman@47625 264 huffman@47636 265 lemma comp_transfer [transfer_rule]: huffman@47325 266 "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \) (op \)" huffman@47325 267 unfolding fun_rel_def by simp huffman@47325 268 huffman@47636 269 lemma fun_upd_transfer [transfer_rule]: huffman@47325 270 assumes [transfer_rule]: "bi_unique A" huffman@47325 271 shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" huffman@47635 272 unfolding fun_upd_def [abs_def] by transfer_prover huffman@47325 273 huffman@47637 274 lemma nat_case_transfer [transfer_rule]: huffman@47637 275 "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case" huffman@47637 276 unfolding fun_rel_def by (simp split: nat.split) huffman@47627 277 huffman@47627 278 text {* Fallback rule for transferring universal quantifiers over huffman@47627 279 correspondence relations that are not bi-total, and do not have huffman@47627 280 custom transfer rules (e.g. relations between function types). *} huffman@47627 281 huffman@47637 282 lemma Domainp_iff: "Domainp T x \ (\y. T x y)" huffman@47637 283 by auto huffman@47637 284 huffman@47627 285 lemma Domainp_forall_transfer [transfer_rule]: huffman@47627 286 assumes "right_total A" huffman@47627 287 shows "((A ===> op =) ===> op =) huffman@47627 288 (transfer_bforall (Domainp A)) transfer_forall" huffman@47627 289 using assms unfolding right_total_def huffman@47627 290 unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff huffman@47627 291 by metis huffman@47627 292 huffman@47627 293 text {* Preferred rule for transferring universal quantifiers over huffman@47627 294 bi-total correspondence relations (later rules are tried first). *} huffman@47627 295 huffman@47636 296 lemma forall_transfer [transfer_rule]: huffman@47627 297 "bi_total A \ ((A ===> op =) ===> op =) transfer_forall transfer_forall" huffman@47636 298 unfolding transfer_forall_def by (rule All_transfer) huffman@47325 299 huffman@47658 300 text {* Transfer rules using implication instead of equality on booleans. *} huffman@47658 301 huffman@47658 302 lemma eq_imp_transfer [transfer_rule]: huffman@47658 303 "right_unique A \ (A ===> A ===> op \) (op =) (op =)" huffman@47658 304 unfolding right_unique_alt_def . huffman@47658 305 huffman@47658 306 lemma forall_imp_transfer [transfer_rule]: huffman@47658 307 "right_total A \ ((A ===> op \) ===> op \) transfer_forall transfer_forall" huffman@47658 308 unfolding right_total_alt_def transfer_forall_def . huffman@47658 309 huffman@47325 310 end