# HG changeset patch # User huffman # Date 1335034353 -7200 # Node ID 7631f6f7873d6c96b1bdd71dfa7defce0c711a81 # Parent 1ba213363d0c24eaf261426e3fcf316ffb2741bc enable variant of transfer method that proves an implication instead of an equivalence diff -r 1ba213363d0c -r 7631f6f7873d src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Thu Apr 19 19:36:24 2012 +0200 +++ b/src/HOL/Tools/transfer.ML Sat Apr 21 20:52:33 2012 +0200 @@ -11,7 +11,7 @@ val get_relator_eq: Proof.context -> thm list val transfer_add: attribute val transfer_del: attribute - val transfer_tac: Proof.context -> int -> tactic + val transfer_tac: bool -> Proof.context -> int -> tactic val transfer_prover_tac: Proof.context -> int -> tactic val setup: theory -> theory val abs_tac: int -> tactic @@ -132,18 +132,20 @@ rtac rule i end handle TERM _ => no_tac) -fun transfer_tac ctxt = SUBGOAL (fn (t, i) => +fun transfer_tac equiv ctxt = SUBGOAL (fn (t, i) => let val rules = Data.get ctxt val app_tac = rtac @{thm Rel_App} + val start_rule = + if equiv then @{thm transfer_start} else @{thm transfer_start'} 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 (app_tac ORELSE' abs_tac ORELSE' atac + rtac start_rule i, + SOLVED' (REPEAT_ALL_NEW (app_tac ORELSE' abs_tac ORELSE' atac ORELSE' SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)) - ORELSE' eq_tac ctxt) (i + 1), + ORELSE' eq_tac ctxt)) (i + 1), (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) rewrite_goal_tac post_simps i, rtac @{thm _} i] @@ -168,9 +170,9 @@ val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon) |-- Scan.repeat free) [] -val transfer_method : (Proof.context -> Method.method) context_parser = +fun transfer_method equiv : (Proof.context -> Method.method) context_parser = fixing >> (fn vs => fn ctxt => - SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac ctxt)) + SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt)) val transfer_prover_method : (Proof.context -> Method.method) context_parser = Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt)) @@ -195,7 +197,9 @@ #> Relator_Eq.setup #> Attrib.setup @{binding transfer_rule} transfer_attribute "transfer rule for transfer method" - #> Method.setup @{binding transfer} transfer_method + #> Method.setup @{binding transfer} (transfer_method true) + "generic theorem transfer method" + #> Method.setup @{binding transfer'} (transfer_method false) "generic theorem transfer method" #> Method.setup @{binding transfer_prover} transfer_prover_method "for proving transfer rules" diff -r 1ba213363d0c -r 7631f6f7873d src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Thu Apr 19 19:36:24 2012 +0200 +++ b/src/HOL/Transfer.thy Sat Apr 21 20:52:33 2012 +0200 @@ -75,10 +75,10 @@ "Trueprop (transfer_bforall P (\x. Q x)) \ (\x. P x \ Q x)" unfolding transfer_bforall_def atomize_imp atomize_all .. -lemma transfer_start: "\Rel (op =) P Q; P\ \ Q" +lemma transfer_start: "\P; Rel (op =) P Q\ \ Q" unfolding Rel_def by simp -lemma transfer_start': "\Rel (op \) P Q; P\ \ Q" +lemma transfer_start': "\P; Rel (op \) P Q\ \ Q" unfolding Rel_def by simp lemma transfer_prover_start: "\x = x'; Rel R x' y\ \ Rel R x y" @@ -278,4 +278,14 @@ "bi_total A \ ((A ===> op =) ===> op =) transfer_forall transfer_forall" unfolding transfer_forall_def by (rule All_transfer) +text {* Transfer rules using implication instead of equality on booleans. *} + +lemma eq_imp_transfer [transfer_rule]: + "right_unique A \ (A ===> A ===> op \) (op =) (op =)" + unfolding right_unique_alt_def . + +lemma forall_imp_transfer [transfer_rule]: + "right_total A \ ((A ===> op \) ===> op \) transfer_forall transfer_forall" + unfolding right_total_alt_def transfer_forall_def . + end