# HG changeset patch # User huffman # Date 1333485060 -7200 # Node ID ec6187036495467db663240db281598395df8eef # Parent ed2bad9b7c6a0ca5b56084b0c08b569acb75474c new transfer proof method diff -r ed2bad9b7c6a -r ec6187036495 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Apr 03 22:04:50 2012 +0200 +++ b/src/HOL/IsaMakefile Tue Apr 03 22:31:00 2012 +0200 @@ -306,6 +306,7 @@ Sledgehammer.thy \ SMT.thy \ String.thy \ + Transfer.thy \ Typerep.thy \ $(SRC)/Provers/Arith/assoc_fold.ML \ $(SRC)/Provers/Arith/cancel_numeral_factor.ML \ @@ -394,6 +395,7 @@ Tools/SMT/z3_proof_tools.ML \ Tools/string_code.ML \ Tools/string_syntax.ML \ + Tools/transfer.ML \ $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES) @$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main diff -r ed2bad9b7c6a -r ec6187036495 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Tue Apr 03 22:04:50 2012 +0200 +++ b/src/HOL/Lifting.thy Tue Apr 03 22:31:00 2012 +0200 @@ -6,7 +6,7 @@ header {* Lifting package *} theory Lifting -imports Plain Equiv_Relations +imports Plain Equiv_Relations Transfer keywords "print_quotmaps" "print_quotients" :: diag and "lift_definition" :: thy_goal and @@ -18,7 +18,7 @@ ("Tools/Lifting/lifting_setup.ML") begin -subsection {* Function map and function relation *} +subsection {* Function map *} notation map_fun (infixr "--->" 55) @@ -26,29 +26,6 @@ "(id ---> id) = id" by (simp add: fun_eq_iff) -definition - fun_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" (infixr "===>" 55) -where - "fun_rel R1 R2 = (\f g. \x y. R1 x y \ R2 (f x) (g y))" - -lemma fun_relI [intro]: - assumes "\x y. R1 x y \ R2 (f x) (g y)" - shows "(R1 ===> R2) f g" - using assms by (simp add: fun_rel_def) - -lemma fun_relE: - assumes "(R1 ===> R2) f g" and "R1 x y" - obtains "R2 (f x) (g y)" - using assms by (simp add: fun_rel_def) - -lemma fun_rel_eq: - shows "((op =) ===> (op =)) = (op =)" - by (auto simp add: fun_eq_iff elim: fun_relE) - -lemma fun_rel_eq_rel: - shows "((op =) ===> R) = (\f g. \x. R (f x) (g x))" - by (simp add: fun_rel_def) - subsection {* Quotient Predicate *} definition diff -r ed2bad9b7c6a -r ec6187036495 src/HOL/Tools/transfer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/transfer.ML Tue Apr 03 22:31:00 2012 +0200 @@ -0,0 +1,176 @@ +(* Title: HOL/Tools/transfer.ML + Author: Brian Huffman, TU Muenchen + +Generic theorem transfer method. +*) + +signature TRANSFER = +sig + val fo_conv: Proof.context -> conv + val prep_conv: conv + val transfer_add: attribute + val transfer_del: attribute + val transfer_tac: Proof.context -> int -> tactic + val correspondence_tac: Proof.context -> int -> tactic + val setup: theory -> theory +end + +structure Transfer : TRANSFER = +struct + +structure Data = Named_Thms +( + val name = @{binding transfer_raw} + val description = "raw correspondence rule for transfer method" +) + +(** Conversions **) + +val App_rule = Thm.symmetric @{thm App_def} +val Abs_rule = Thm.symmetric @{thm Abs_def} +val Rel_rule = Thm.symmetric @{thm Rel_def} + +fun dest_funcT cT = + (case Thm.dest_ctyp cT of [T, U] => (T, U) + | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], [])) + +fun App_conv ct = + let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct) + in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] App_rule end + +fun Abs_conv ct = + let val (cT, cU) = dest_funcT (Thm.ctyp_of_term ct) + in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Abs_rule end + +fun Rel_conv ct = + let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct) + val (cU, _) = dest_funcT cT' + in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end + +fun Trueprop_conv cv ct = + (case Thm.term_of ct of + Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct + | _ => raise CTERM ("Trueprop_conv", [ct])) + +(* Conversion to insert tags on every application and abstraction. *) +fun fo_conv ctxt ct = ( + Conv.combination_conv (fo_conv ctxt then_conv App_conv) (fo_conv ctxt) + else_conv + Conv.abs_conv (fo_conv o snd) ctxt then_conv Abs_conv + else_conv + Conv.all_conv) ct + +(* Conversion to preprocess a correspondence rule *) +fun prep_conv ct = ( + Conv.implies_conv Conv.all_conv prep_conv + else_conv + Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) + else_conv + Conv.all_conv) ct + +(* Conversion to prep a proof goal containing a correspondence rule *) +fun correspond_conv ctxt ct = ( + Conv.forall_conv (correspond_conv o snd) ctxt + else_conv + Conv.implies_conv Conv.all_conv (correspond_conv ctxt) + else_conv + Trueprop_conv + (Conv.combination_conv + (Conv.combination_conv Rel_conv (fo_conv ctxt)) (fo_conv ctxt)) + else_conv + Conv.all_conv) ct + + +(** Transfer proof method **) + +fun bnames (t $ u) = bnames t @ bnames u + | bnames (Abs (x,_,t)) = x :: bnames t + | bnames _ = [] + +fun rename [] t = (t, []) + | rename (x::xs) ((c as Const (@{const_name Abs}, _)) $ Abs (_, T, t)) = + let val (t', xs') = rename xs t + in (c $ Abs (x, T, t'), xs') end + | rename xs0 (t $ u) = + let val (t', xs1) = rename xs0 t + val (u', xs2) = rename xs1 u + in (t' $ u', xs2) end + | rename xs t = (t, xs) + +fun cert ctxt t = cterm_of (Proof_Context.theory_of ctxt) t + +fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y + +(* Tactic to correspond a value to itself *) +fun eq_tac ctxt = SUBGOAL (fn (t, i) => + let + val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t)) + val cT = ctyp_of (Proof_Context.theory_of ctxt) T + val rews = [@{thm fun_rel_eq [symmetric, THEN eq_reflection]}] + val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl} + val thm2 = Raw_Simplifier.rewrite_rule rews thm1 + in + rtac thm2 i + end handle Match => no_tac | TERM _ => no_tac) + +fun transfer_tac ctxt = SUBGOAL (fn (t, i) => + let + val bs = bnames t + val rules = Data.get ctxt + in + EVERY + [rewrite_goal_tac @{thms transfer_forall_eq transfer_implies_eq} i, + CONVERSION (Trueprop_conv (fo_conv ctxt)) i, + rtac @{thm transfer_start [rotated]} i, + REPEAT_ALL_NEW (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i + 1), + (* Alpha-rename bound variables in goal *) + SUBGOAL (fn (u, i) => + rtac @{thm equal_elim_rule1} i THEN + rtac (Thm.reflexive (cert ctxt (fst (rename bs u)))) i) i, + (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) + rewrite_goal_tac @{thms App_def Abs_def} i, + rewrite_goal_tac @{thms transfer_forall_eq [symmetric] transfer_implies_eq [symmetric]} i, + rtac @{thm _} i] + end) + +fun correspondence_tac ctxt i = + let + val rules = Data.get ctxt + in + EVERY + [CONVERSION (correspond_conv ctxt) i, + REPEAT_ALL_NEW + (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) i] + end + +val transfer_method = + Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_tac ctxt)) + +val correspondence_method = + Scan.succeed (fn ctxt => SIMPLE_METHOD' (correspondence_tac ctxt)) + +(* Attribute for correspondence rules *) + +val prep_rule = Conv.fconv_rule prep_conv + +val transfer_add = + Thm.declaration_attribute (Data.add_thm o prep_rule) + +val transfer_del = + Thm.declaration_attribute (Data.del_thm o prep_rule) + +val transfer_attribute = + Attrib.add_del transfer_add transfer_del + +(* Theory setup *) + +val setup = + Data.setup + #> Attrib.setup @{binding transfer_rule} transfer_attribute + "correspondence rule for transfer method" + #> Method.setup @{binding transfer} transfer_method + "generic theorem transfer method" + #> Method.setup @{binding correspondence} correspondence_method + "for proving correspondence rules" + +end diff -r ed2bad9b7c6a -r ec6187036495 src/HOL/Transfer.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Transfer.thy Tue Apr 03 22:31:00 2012 +0200 @@ -0,0 +1,240 @@ +(* Title: HOL/Transfer.thy + Author: Brian Huffman, TU Muenchen +*) + +header {* Generic theorem transfer using relations *} + +theory Transfer +imports Plain Hilbert_Choice +uses ("Tools/transfer.ML") +begin + +subsection {* Relator for function space *} + +definition + fun_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" (infixr "===>" 55) +where + "fun_rel A B = (\f g. \x y. A x y \ B (f x) (g y))" + +lemma fun_relI [intro]: + assumes "\x y. A x y \ B (f x) (g y)" + shows "(A ===> B) f g" + using assms by (simp add: fun_rel_def) + +lemma fun_relD: + assumes "(A ===> B) f g" and "A x y" + shows "B (f x) (g y)" + using assms by (simp add: fun_rel_def) + +lemma fun_relE: + assumes "(A ===> B) f g" and "A x y" + obtains "B (f x) (g y)" + using assms by (simp add: fun_rel_def) + +lemma fun_rel_eq: + shows "((op =) ===> (op =)) = (op =)" + by (auto simp add: fun_eq_iff elim: fun_relE) + +lemma fun_rel_eq_rel: + shows "((op =) ===> R) = (\f g. \x. R (f x) (g x))" + by (simp add: fun_rel_def) + + +subsection {* Transfer method *} + +text {* Explicit tags for application, abstraction, and relation +membership allow for backward proof methods. *} + +definition App :: "('a \ 'b) \ 'a \ 'b" + where "App f \ f" + +definition Abs :: "('a \ 'b) \ 'a \ 'b" + where "Abs f \ f" + +definition Rel :: "('a \ 'b \ bool) \ 'a \ 'b \ bool" + where "Rel r \ r" + +text {* Handling of meta-logic connectives *} + +definition transfer_forall where + "transfer_forall \ All" + +definition transfer_implies where + "transfer_implies \ op \" + +lemma transfer_forall_eq: "(\x. P x) \ Trueprop (transfer_forall (\x. P x))" + unfolding atomize_all transfer_forall_def .. + +lemma transfer_implies_eq: "(A \ B) \ Trueprop (transfer_implies A B)" + unfolding atomize_imp transfer_implies_def .. + +lemma transfer_start: "\Rel (op =) P Q; P\ \ Q" + unfolding Rel_def by simp + +lemma transfer_start': "\Rel (op \) P Q; P\ \ Q" + unfolding Rel_def by simp + +lemma Rel_eq_refl: "Rel (op =) x x" + unfolding Rel_def .. + +use "Tools/transfer.ML" + +setup Transfer.setup + +lemma Rel_App [transfer_raw]: + assumes "Rel (A ===> B) f g" and "Rel A x y" + shows "Rel B (App f x) (App g y)" + using assms unfolding Rel_def App_def fun_rel_def by fast + +lemma Rel_Abs [transfer_raw]: + assumes "\x y. Rel A x y \ Rel B (f x) (g y)" + shows "Rel (A ===> B) (Abs (\x. f x)) (Abs (\y. g y))" + using assms unfolding Rel_def Abs_def fun_rel_def by fast + +hide_const (open) App Abs Rel + + +subsection {* Predicates on relations, i.e. ``class constraints'' *} + +definition right_total :: "('a \ 'b \ bool) \ bool" + where "right_total R \ (\y. \x. R x y)" + +definition right_unique :: "('a \ 'b \ bool) \ bool" + where "right_unique R \ (\x y z. R x y \ R x z \ y = z)" + +definition bi_total :: "('a \ 'b \ bool) \ bool" + where "bi_total R \ (\x. \y. R x y) \ (\y. \x. R x y)" + +definition bi_unique :: "('a \ 'b \ bool) \ bool" + where "bi_unique R \ + (\x y z. R x y \ R x z \ y = z) \ + (\x y z. R x z \ R y z \ x = y)" + +lemma right_total_alt_def: + "right_total R \ ((R ===> op \) ===> op \) All All" + unfolding right_total_def fun_rel_def + apply (rule iffI, fast) + apply (rule allI) + apply (drule_tac x="\x. True" in spec) + apply (drule_tac x="\y. \x. R x y" in spec) + apply fast + done + +lemma right_unique_alt_def: + "right_unique R \ (R ===> R ===> op \) (op =) (op =)" + unfolding right_unique_def fun_rel_def by auto + +lemma bi_total_alt_def: + "bi_total R \ ((R ===> op =) ===> op =) All All" + unfolding bi_total_def fun_rel_def + apply (rule iffI, fast) + apply safe + apply (drule_tac x="\x. \y. R x y" in spec) + apply (drule_tac x="\y. True" in spec) + apply fast + apply (drule_tac x="\x. True" in spec) + apply (drule_tac x="\y. \x. R x y" in spec) + apply fast + done + +lemma bi_unique_alt_def: + "bi_unique R \ (R ===> R ===> op =) (op =) (op =)" + unfolding bi_unique_def fun_rel_def by auto + + +subsection {* Properties of relators *} + +lemma right_total_eq [transfer_rule]: "right_total (op =)" + unfolding right_total_def by simp + +lemma right_unique_eq [transfer_rule]: "right_unique (op =)" + unfolding right_unique_def by simp + +lemma bi_total_eq [transfer_rule]: "bi_total (op =)" + unfolding bi_total_def by simp + +lemma bi_unique_eq [transfer_rule]: "bi_unique (op =)" + unfolding bi_unique_def by simp + +lemma right_total_fun [transfer_rule]: + "\right_unique A; right_total B\ \ right_total (A ===> B)" + unfolding right_total_def fun_rel_def + apply (rule allI, rename_tac g) + apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) + apply clarify + apply (subgoal_tac "(THE y. A x y) = y", simp) + apply (rule someI_ex) + apply (simp) + apply (rule the_equality) + apply assumption + apply (simp add: right_unique_def) + done + +lemma right_unique_fun [transfer_rule]: + "\right_total A; right_unique B\ \ right_unique (A ===> B)" + unfolding right_total_def right_unique_def fun_rel_def + by (clarify, rule ext, fast) + +lemma bi_total_fun [transfer_rule]: + "\bi_unique A; bi_total B\ \ bi_total (A ===> B)" + unfolding bi_total_def fun_rel_def + apply safe + apply (rename_tac f) + apply (rule_tac x="\y. SOME z. B (f (THE x. A x y)) z" in exI) + apply clarify + apply (subgoal_tac "(THE x. A x y) = x", simp) + apply (rule someI_ex) + apply (simp) + apply (rule the_equality) + apply assumption + apply (simp add: bi_unique_def) + apply (rename_tac g) + apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) + apply clarify + apply (subgoal_tac "(THE y. A x y) = y", simp) + apply (rule someI_ex) + apply (simp) + apply (rule the_equality) + apply assumption + apply (simp add: bi_unique_def) + done + +lemma bi_unique_fun [transfer_rule]: + "\bi_total A; bi_unique B\ \ bi_unique (A ===> B)" + unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff + by (safe, metis, fast) + + +subsection {* Correspondence rules *} + +lemma eq_parametric [transfer_rule]: + assumes "bi_unique A" + shows "(A ===> A ===> op =) (op =) (op =)" + using assms unfolding bi_unique_def fun_rel_def by auto + +lemma All_parametric [transfer_rule]: + assumes "bi_total A" + shows "((A ===> op =) ===> op =) All All" + using assms unfolding bi_total_def fun_rel_def by fast + +lemma Ex_parametric [transfer_rule]: + assumes "bi_total A" + shows "((A ===> op =) ===> op =) Ex Ex" + using assms unfolding bi_total_def fun_rel_def by fast + +lemma If_parametric [transfer_rule]: "(op = ===> A ===> A ===> A) If If" + unfolding fun_rel_def by simp + +lemma comp_parametric [transfer_rule]: + "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \) (op \)" + unfolding fun_rel_def by simp + +lemma fun_upd_parametric [transfer_rule]: + assumes [transfer_rule]: "bi_unique A" + shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" + unfolding fun_upd_def [abs_def] by correspondence + +lemmas transfer_forall_parametric [transfer_rule] + = All_parametric [folded transfer_forall_def] + +end