src/HOL/Transfer.thy
 author kuncar Mon May 13 12:13:24 2013 +0200 (2013-05-13) changeset 51955 04d9381bebff parent 51437 8739f8abbecb child 51956 a4d81cdebf8b permissions -rw-r--r--
try to detect assumptions of transfer rules that are in a shape of a transfer rule
 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 ``` haftmann@51112 ` 8` ```imports Hilbert_Choice ``` huffman@47325 ` 9` ```begin ``` huffman@47325 ` 10` huffman@47325 ` 11` ```subsection {* Relator for function space *} ``` huffman@47325 ` 12` huffman@47325 ` 13` ```definition ``` huffman@47325 ` 14` ``` fun_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" (infixr "===>" 55) ``` huffman@47325 ` 15` ```where ``` huffman@47325 ` 16` ``` "fun_rel A B = (\f g. \x y. A x y \ B (f x) (g y))" ``` huffman@47325 ` 17` huffman@47325 ` 18` ```lemma fun_relI [intro]: ``` huffman@47325 ` 19` ``` assumes "\x y. A x y \ B (f x) (g y)" ``` huffman@47325 ` 20` ``` shows "(A ===> B) f g" ``` huffman@47325 ` 21` ``` using assms by (simp add: fun_rel_def) ``` huffman@47325 ` 22` huffman@47325 ` 23` ```lemma fun_relD: ``` huffman@47325 ` 24` ``` assumes "(A ===> B) f g" and "A x y" ``` huffman@47325 ` 25` ``` shows "B (f x) (g y)" ``` huffman@47325 ` 26` ``` using assms by (simp add: fun_rel_def) ``` huffman@47325 ` 27` kuncar@47937 ` 28` ```lemma fun_relD2: ``` kuncar@47937 ` 29` ``` assumes "(A ===> B) f g" and "A x x" ``` kuncar@47937 ` 30` ``` shows "B (f x) (g x)" ``` kuncar@47937 ` 31` ``` using assms unfolding fun_rel_def by auto ``` kuncar@47937 ` 32` huffman@47325 ` 33` ```lemma fun_relE: ``` huffman@47325 ` 34` ``` assumes "(A ===> B) f g" and "A x y" ``` huffman@47325 ` 35` ``` obtains "B (f x) (g y)" ``` huffman@47325 ` 36` ``` using assms by (simp add: fun_rel_def) ``` huffman@47325 ` 37` huffman@47325 ` 38` ```lemma fun_rel_eq: ``` huffman@47325 ` 39` ``` shows "((op =) ===> (op =)) = (op =)" ``` huffman@47325 ` 40` ``` by (auto simp add: fun_eq_iff elim: fun_relE) ``` huffman@47325 ` 41` huffman@47325 ` 42` ```lemma fun_rel_eq_rel: ``` huffman@47325 ` 43` ``` shows "((op =) ===> R) = (\f g. \x. R (f x) (g x))" ``` huffman@47325 ` 44` ``` by (simp add: fun_rel_def) ``` huffman@47325 ` 45` huffman@47325 ` 46` huffman@47325 ` 47` ```subsection {* Transfer method *} ``` huffman@47325 ` 48` huffman@47789 ` 49` ```text {* Explicit tag for relation membership allows for ``` huffman@47789 ` 50` ``` backward proof methods. *} ``` huffman@47325 ` 51` huffman@47325 ` 52` ```definition Rel :: "('a \ 'b \ bool) \ 'a \ 'b \ bool" ``` huffman@47325 ` 53` ``` where "Rel r \ r" ``` huffman@47325 ` 54` huffman@49975 ` 55` ```text {* Handling of equality relations *} ``` huffman@49975 ` 56` huffman@49975 ` 57` ```definition is_equality :: "('a \ 'a \ bool) \ bool" ``` huffman@49975 ` 58` ``` where "is_equality R \ R = (op =)" ``` huffman@49975 ` 59` kuncar@51437 ` 60` ```lemma is_equality_eq: "is_equality (op =)" ``` kuncar@51437 ` 61` ``` unfolding is_equality_def by simp ``` kuncar@51437 ` 62` huffman@47325 ` 63` ```text {* Handling of meta-logic connectives *} ``` huffman@47325 ` 64` huffman@47325 ` 65` ```definition transfer_forall where ``` huffman@47325 ` 66` ``` "transfer_forall \ All" ``` huffman@47325 ` 67` huffman@47325 ` 68` ```definition transfer_implies where ``` huffman@47325 ` 69` ``` "transfer_implies \ op \" ``` huffman@47325 ` 70` huffman@47355 ` 71` ```definition transfer_bforall :: "('a \ bool) \ ('a \ bool) \ bool" ``` huffman@47355 ` 72` ``` where "transfer_bforall \ (\P Q. \x. P x \ Q x)" ``` huffman@47355 ` 73` huffman@47325 ` 74` ```lemma transfer_forall_eq: "(\x. P x) \ Trueprop (transfer_forall (\x. P x))" ``` huffman@47325 ` 75` ``` unfolding atomize_all transfer_forall_def .. ``` huffman@47325 ` 76` huffman@47325 ` 77` ```lemma transfer_implies_eq: "(A \ B) \ Trueprop (transfer_implies A B)" ``` huffman@47325 ` 78` ``` unfolding atomize_imp transfer_implies_def .. ``` huffman@47325 ` 79` huffman@47355 ` 80` ```lemma transfer_bforall_unfold: ``` huffman@47355 ` 81` ``` "Trueprop (transfer_bforall P (\x. Q x)) \ (\x. P x \ Q x)" ``` huffman@47355 ` 82` ``` unfolding transfer_bforall_def atomize_imp atomize_all .. ``` huffman@47355 ` 83` huffman@47658 ` 84` ```lemma transfer_start: "\P; Rel (op =) P Q\ \ Q" ``` huffman@47325 ` 85` ``` unfolding Rel_def by simp ``` huffman@47325 ` 86` huffman@47658 ` 87` ```lemma transfer_start': "\P; Rel (op \) P Q\ \ Q" ``` huffman@47325 ` 88` ``` unfolding Rel_def by simp ``` huffman@47325 ` 89` huffman@47635 ` 90` ```lemma transfer_prover_start: "\x = x'; Rel R x' y\ \ Rel R x y" ``` huffman@47618 ` 91` ``` by simp ``` huffman@47618 ` 92` huffman@47325 ` 93` ```lemma Rel_eq_refl: "Rel (op =) x x" ``` huffman@47325 ` 94` ``` unfolding Rel_def .. ``` huffman@47325 ` 95` huffman@47789 ` 96` ```lemma Rel_app: ``` huffman@47523 ` 97` ``` assumes "Rel (A ===> B) f g" and "Rel A x y" ``` huffman@47789 ` 98` ``` shows "Rel B (f x) (g y)" ``` huffman@47789 ` 99` ``` using assms unfolding Rel_def fun_rel_def by fast ``` huffman@47523 ` 100` huffman@47789 ` 101` ```lemma Rel_abs: ``` huffman@47523 ` 102` ``` assumes "\x y. Rel A x y \ Rel B (f x) (g y)" ``` huffman@47789 ` 103` ``` shows "Rel (A ===> B) (\x. f x) (\y. g y)" ``` huffman@47789 ` 104` ``` using assms unfolding Rel_def fun_rel_def by fast ``` huffman@47523 ` 105` kuncar@51955 ` 106` ```text {* Handling of domains *} ``` kuncar@51955 ` 107` kuncar@51955 ` 108` ```definition DOM :: "('a => 'b => bool) => ('a => bool) => bool" where "DOM T R \ Domainp T = R" ``` kuncar@51955 ` 109` wenzelm@48891 ` 110` ```ML_file "Tools/transfer.ML" ``` huffman@47325 ` 111` ```setup Transfer.setup ``` huffman@47325 ` 112` huffman@49975 ` 113` ```declare refl [transfer_rule] ``` huffman@49975 ` 114` huffman@47503 ` 115` ```declare fun_rel_eq [relator_eq] ``` huffman@47503 ` 116` huffman@47789 ` 117` ```hide_const (open) Rel ``` huffman@47325 ` 118` huffman@47325 ` 119` huffman@47325 ` 120` ```subsection {* Predicates on relations, i.e. ``class constraints'' *} ``` huffman@47325 ` 121` huffman@47325 ` 122` ```definition right_total :: "('a \ 'b \ bool) \ bool" ``` huffman@47325 ` 123` ``` where "right_total R \ (\y. \x. R x y)" ``` huffman@47325 ` 124` huffman@47325 ` 125` ```definition right_unique :: "('a \ 'b \ bool) \ bool" ``` huffman@47325 ` 126` ``` where "right_unique R \ (\x y z. R x y \ R x z \ y = z)" ``` huffman@47325 ` 127` huffman@47325 ` 128` ```definition bi_total :: "('a \ 'b \ bool) \ bool" ``` huffman@47325 ` 129` ``` where "bi_total R \ (\x. \y. R x y) \ (\y. \x. R x y)" ``` huffman@47325 ` 130` huffman@47325 ` 131` ```definition bi_unique :: "('a \ 'b \ bool) \ bool" ``` huffman@47325 ` 132` ``` where "bi_unique R \ ``` huffman@47325 ` 133` ``` (\x y z. R x y \ R x z \ y = z) \ ``` huffman@47325 ` 134` ``` (\x y z. R x z \ R y z \ x = y)" ``` huffman@47325 ` 135` huffman@47325 ` 136` ```lemma right_total_alt_def: ``` huffman@47325 ` 137` ``` "right_total R \ ((R ===> op \) ===> op \) All All" ``` huffman@47325 ` 138` ``` unfolding right_total_def fun_rel_def ``` huffman@47325 ` 139` ``` apply (rule iffI, fast) ``` huffman@47325 ` 140` ``` apply (rule allI) ``` 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 right_unique_alt_def: ``` huffman@47325 ` 147` ``` "right_unique R \ (R ===> R ===> op \) (op =) (op =)" ``` huffman@47325 ` 148` ``` unfolding right_unique_def fun_rel_def by auto ``` huffman@47325 ` 149` huffman@47325 ` 150` ```lemma bi_total_alt_def: ``` huffman@47325 ` 151` ``` "bi_total R \ ((R ===> op =) ===> op =) All All" ``` huffman@47325 ` 152` ``` unfolding bi_total_def fun_rel_def ``` huffman@47325 ` 153` ``` apply (rule iffI, fast) ``` huffman@47325 ` 154` ``` apply safe ``` huffman@47325 ` 155` ``` apply (drule_tac x="\x. \y. R x y" in spec) ``` huffman@47325 ` 156` ``` apply (drule_tac x="\y. True" in spec) ``` huffman@47325 ` 157` ``` apply fast ``` huffman@47325 ` 158` ``` apply (drule_tac x="\x. True" in spec) ``` huffman@47325 ` 159` ``` apply (drule_tac x="\y. \x. R x y" in spec) ``` huffman@47325 ` 160` ``` apply fast ``` huffman@47325 ` 161` ``` done ``` huffman@47325 ` 162` huffman@47325 ` 163` ```lemma bi_unique_alt_def: ``` huffman@47325 ` 164` ``` "bi_unique R \ (R ===> R ===> op =) (op =) (op =)" ``` huffman@47325 ` 165` ``` unfolding bi_unique_def fun_rel_def by auto ``` huffman@47325 ` 166` huffman@47660 ` 167` ```text {* Properties are preserved by relation composition. *} ``` huffman@47660 ` 168` huffman@47660 ` 169` ```lemma OO_def: "R OO S = (\x z. \y. R x y \ S y z)" ``` huffman@47660 ` 170` ``` by auto ``` huffman@47660 ` 171` huffman@47660 ` 172` ```lemma bi_total_OO: "\bi_total A; bi_total B\ \ bi_total (A OO B)" ``` huffman@47660 ` 173` ``` unfolding bi_total_def OO_def by metis ``` huffman@47660 ` 174` huffman@47660 ` 175` ```lemma bi_unique_OO: "\bi_unique A; bi_unique B\ \ bi_unique (A OO B)" ``` huffman@47660 ` 176` ``` unfolding bi_unique_def OO_def by metis ``` huffman@47660 ` 177` huffman@47660 ` 178` ```lemma right_total_OO: ``` huffman@47660 ` 179` ``` "\right_total A; right_total B\ \ right_total (A OO B)" ``` huffman@47660 ` 180` ``` unfolding right_total_def OO_def by metis ``` huffman@47660 ` 181` huffman@47660 ` 182` ```lemma right_unique_OO: ``` huffman@47660 ` 183` ``` "\right_unique A; right_unique B\ \ right_unique (A OO B)" ``` huffman@47660 ` 184` ``` unfolding right_unique_def OO_def by metis ``` huffman@47660 ` 185` huffman@47325 ` 186` huffman@47325 ` 187` ```subsection {* Properties of relators *} ``` huffman@47325 ` 188` huffman@47325 ` 189` ```lemma right_total_eq [transfer_rule]: "right_total (op =)" ``` huffman@47325 ` 190` ``` unfolding right_total_def by simp ``` huffman@47325 ` 191` huffman@47325 ` 192` ```lemma right_unique_eq [transfer_rule]: "right_unique (op =)" ``` huffman@47325 ` 193` ``` unfolding right_unique_def by simp ``` huffman@47325 ` 194` huffman@47325 ` 195` ```lemma bi_total_eq [transfer_rule]: "bi_total (op =)" ``` huffman@47325 ` 196` ``` unfolding bi_total_def by simp ``` huffman@47325 ` 197` huffman@47325 ` 198` ```lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)" ``` huffman@47325 ` 199` ``` unfolding bi_unique_def by simp ``` huffman@47325 ` 200` huffman@47325 ` 201` ```lemma right_total_fun [transfer_rule]: ``` huffman@47325 ` 202` ``` "\right_unique A; right_total B\ \ right_total (A ===> B)" ``` huffman@47325 ` 203` ``` unfolding right_total_def fun_rel_def ``` huffman@47325 ` 204` ``` apply (rule allI, rename_tac g) ``` huffman@47325 ` 205` ``` apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) ``` huffman@47325 ` 206` ``` apply clarify ``` huffman@47325 ` 207` ``` apply (subgoal_tac "(THE y. A x y) = y", simp) ``` huffman@47325 ` 208` ``` apply (rule someI_ex) ``` huffman@47325 ` 209` ``` apply (simp) ``` huffman@47325 ` 210` ``` apply (rule the_equality) ``` huffman@47325 ` 211` ``` apply assumption ``` huffman@47325 ` 212` ``` apply (simp add: right_unique_def) ``` huffman@47325 ` 213` ``` done ``` huffman@47325 ` 214` huffman@47325 ` 215` ```lemma right_unique_fun [transfer_rule]: ``` huffman@47325 ` 216` ``` "\right_total A; right_unique B\ \ right_unique (A ===> B)" ``` huffman@47325 ` 217` ``` unfolding right_total_def right_unique_def fun_rel_def ``` huffman@47325 ` 218` ``` by (clarify, rule ext, fast) ``` huffman@47325 ` 219` huffman@47325 ` 220` ```lemma bi_total_fun [transfer_rule]: ``` huffman@47325 ` 221` ``` "\bi_unique A; bi_total B\ \ bi_total (A ===> B)" ``` huffman@47325 ` 222` ``` unfolding bi_total_def fun_rel_def ``` huffman@47325 ` 223` ``` apply safe ``` huffman@47325 ` 224` ``` apply (rename_tac f) ``` huffman@47325 ` 225` ``` apply (rule_tac x="\y. SOME z. B (f (THE x. A x y)) z" in exI) ``` huffman@47325 ` 226` ``` apply clarify ``` huffman@47325 ` 227` ``` apply (subgoal_tac "(THE x. A x y) = x", simp) ``` huffman@47325 ` 228` ``` apply (rule someI_ex) ``` huffman@47325 ` 229` ``` apply (simp) ``` huffman@47325 ` 230` ``` apply (rule the_equality) ``` huffman@47325 ` 231` ``` apply assumption ``` huffman@47325 ` 232` ``` apply (simp add: bi_unique_def) ``` huffman@47325 ` 233` ``` apply (rename_tac g) ``` huffman@47325 ` 234` ``` apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) ``` huffman@47325 ` 235` ``` apply clarify ``` huffman@47325 ` 236` ``` apply (subgoal_tac "(THE y. A x y) = y", simp) ``` huffman@47325 ` 237` ``` apply (rule someI_ex) ``` huffman@47325 ` 238` ``` apply (simp) ``` huffman@47325 ` 239` ``` apply (rule the_equality) ``` huffman@47325 ` 240` ``` apply assumption ``` huffman@47325 ` 241` ``` apply (simp add: bi_unique_def) ``` huffman@47325 ` 242` ``` done ``` huffman@47325 ` 243` huffman@47325 ` 244` ```lemma bi_unique_fun [transfer_rule]: ``` huffman@47325 ` 245` ``` "\bi_total A; bi_unique B\ \ bi_unique (A ===> B)" ``` huffman@47325 ` 246` ``` unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff ``` huffman@47325 ` 247` ``` by (safe, metis, fast) ``` huffman@47325 ` 248` huffman@47325 ` 249` huffman@47635 ` 250` ```subsection {* Transfer rules *} ``` huffman@47325 ` 251` huffman@47684 ` 252` ```text {* Transfer rules using implication instead of equality on booleans. *} ``` huffman@47684 ` 253` huffman@47684 ` 254` ```lemma eq_imp_transfer [transfer_rule]: ``` huffman@47684 ` 255` ``` "right_unique A \ (A ===> A ===> op \) (op =) (op =)" ``` huffman@47684 ` 256` ``` unfolding right_unique_alt_def . ``` huffman@47684 ` 257` huffman@47684 ` 258` ```lemma forall_imp_transfer [transfer_rule]: ``` huffman@47684 ` 259` ``` "right_total A \ ((A ===> op \) ===> op \) transfer_forall transfer_forall" ``` huffman@47684 ` 260` ``` unfolding right_total_alt_def transfer_forall_def . ``` huffman@47684 ` 261` huffman@47636 ` 262` ```lemma eq_transfer [transfer_rule]: ``` huffman@47325 ` 263` ``` assumes "bi_unique A" ``` huffman@47325 ` 264` ``` shows "(A ===> A ===> op =) (op =) (op =)" ``` huffman@47325 ` 265` ``` using assms unfolding bi_unique_def fun_rel_def by auto ``` huffman@47325 ` 266` huffman@47636 ` 267` ```lemma All_transfer [transfer_rule]: ``` huffman@47325 ` 268` ``` assumes "bi_total A" ``` huffman@47325 ` 269` ``` shows "((A ===> op =) ===> op =) All All" ``` huffman@47325 ` 270` ``` using assms unfolding bi_total_def fun_rel_def by fast ``` huffman@47325 ` 271` huffman@47636 ` 272` ```lemma Ex_transfer [transfer_rule]: ``` huffman@47325 ` 273` ``` assumes "bi_total A" ``` huffman@47325 ` 274` ``` shows "((A ===> op =) ===> op =) Ex Ex" ``` huffman@47325 ` 275` ``` using assms unfolding bi_total_def fun_rel_def by fast ``` huffman@47325 ` 276` huffman@47636 ` 277` ```lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If" ``` huffman@47325 ` 278` ``` unfolding fun_rel_def by simp ``` huffman@47325 ` 279` huffman@47636 ` 280` ```lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" ``` huffman@47612 ` 281` ``` unfolding fun_rel_def by simp ``` huffman@47612 ` 282` huffman@47636 ` 283` ```lemma id_transfer [transfer_rule]: "(A ===> A) id id" ``` huffman@47625 ` 284` ``` unfolding fun_rel_def by simp ``` huffman@47625 ` 285` huffman@47636 ` 286` ```lemma comp_transfer [transfer_rule]: ``` huffman@47325 ` 287` ``` "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \) (op \)" ``` huffman@47325 ` 288` ``` unfolding fun_rel_def by simp ``` huffman@47325 ` 289` huffman@47636 ` 290` ```lemma fun_upd_transfer [transfer_rule]: ``` huffman@47325 ` 291` ``` assumes [transfer_rule]: "bi_unique A" ``` huffman@47325 ` 292` ``` shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" ``` huffman@47635 ` 293` ``` unfolding fun_upd_def [abs_def] by transfer_prover ``` huffman@47325 ` 294` huffman@47637 ` 295` ```lemma nat_case_transfer [transfer_rule]: ``` huffman@47637 ` 296` ``` "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case" ``` huffman@47637 ` 297` ``` unfolding fun_rel_def by (simp split: nat.split) ``` huffman@47627 ` 298` huffman@47924 ` 299` ```lemma nat_rec_transfer [transfer_rule]: ``` huffman@47924 ` 300` ``` "(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec" ``` huffman@47924 ` 301` ``` unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all) ``` huffman@47924 ` 302` huffman@47924 ` 303` ```lemma funpow_transfer [transfer_rule]: ``` huffman@47924 ` 304` ``` "(op = ===> (A ===> A) ===> (A ===> A)) compow compow" ``` huffman@47924 ` 305` ``` unfolding funpow_def by transfer_prover ``` huffman@47924 ` 306` huffman@47627 ` 307` ```text {* Fallback rule for transferring universal quantifiers over ``` huffman@47627 ` 308` ``` correspondence relations that are not bi-total, and do not have ``` huffman@47627 ` 309` ``` custom transfer rules (e.g. relations between function types). *} ``` huffman@47627 ` 310` huffman@47637 ` 311` ```lemma Domainp_iff: "Domainp T x \ (\y. T x y)" ``` huffman@47637 ` 312` ``` by auto ``` huffman@47637 ` 313` huffman@47627 ` 314` ```lemma Domainp_forall_transfer [transfer_rule]: ``` huffman@47627 ` 315` ``` assumes "right_total A" ``` huffman@47627 ` 316` ``` shows "((A ===> op =) ===> op =) ``` huffman@47627 ` 317` ``` (transfer_bforall (Domainp A)) transfer_forall" ``` huffman@47627 ` 318` ``` using assms unfolding right_total_def ``` huffman@47627 ` 319` ``` unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff ``` huffman@47627 ` 320` ``` by metis ``` huffman@47627 ` 321` huffman@47627 ` 322` ```text {* Preferred rule for transferring universal quantifiers over ``` huffman@47627 ` 323` ``` bi-total correspondence relations (later rules are tried first). *} ``` huffman@47627 ` 324` huffman@47636 ` 325` ```lemma forall_transfer [transfer_rule]: ``` huffman@47627 ` 326` ``` "bi_total A \ ((A ===> op =) ===> op =) transfer_forall transfer_forall" ``` huffman@47636 ` 327` ``` unfolding transfer_forall_def by (rule All_transfer) ``` huffman@47325 ` 328` huffman@47325 ` 329` ```end ```