# HG changeset patch # User kuncar # Date 1444347477 -7200 # Node ID 46af4f577c7e20ba8b5a7edc4084b81b8e3e5526 # Parent 3933c0d7edc9d71e9c3a405eff321fb808d62acf new methods for debugging transfer and transfer_prover diff -r 3933c0d7edc9 -r 46af4f577c7e src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Fri Oct 09 01:37:57 2015 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Fri Oct 09 01:37:57 2015 +0200 @@ -43,7 +43,11 @@ val transfer_rule_of_term: Proof.context -> bool -> term -> thm val transfer_rule_of_lhs: Proof.context -> term -> thm val eq_tac: Proof.context -> int -> tactic + val transfer_start_tac: bool -> Proof.context -> int -> tactic + val transfer_prover_start_tac: Proof.context -> int -> tactic val transfer_step_tac: Proof.context -> int -> tactic + val transfer_end_tac: Proof.context -> int -> tactic + val transfer_prover_end_tac: Proof.context -> int -> tactic val transfer_tac: bool -> Proof.context -> int -> tactic val transfer_prover_tac: Proof.context -> int -> tactic val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic @@ -635,52 +639,84 @@ REPEAT_ALL_NEW (resolve_tac ctxt (get_transfer_raw ctxt)) THEN_ALL_NEW (DETERM o eq_rules_tac ctxt (get_relator_eq_raw ctxt)) -fun transfer_tac equiv ctxt i = - let - val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} - val start_rule = - if equiv then @{thm transfer_start} else @{thm transfer_start'} - val rules = get_transfer_raw ctxt - val eq_rules = get_relator_eq_raw ctxt - (* allow unsolved subgoals only for standard transfer method, not for transfer' *) - val end_tac = if equiv then K all_tac else K no_tac - val err_msg = "Transfer failed to convert goal to an object-logic formula" - fun main_tac (t, i) = - resolve_tac ctxt [start_rule] i THEN - (resolve_tac ctxt [transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t)] - THEN_ALL_NEW - (SOLVED' - (REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW - (DETERM o eq_rules_tac ctxt eq_rules)) - ORELSE' end_tac)) (i + 1) - handle TERM (_, ts) => raise TERM (err_msg, ts) - in - EVERY - [rewrite_goal_tac ctxt pre_simps i THEN - SUBGOAL main_tac i, - (* FIXME: rewrite_goal_tac does unwanted eta-contraction *) - rewrite_goal_tac ctxt post_simps i, - Goal.norm_hhf_tac ctxt i] - end +fun transfer_start_tac equiv ctxt i = + let + val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} + val start_rule = + if equiv then @{thm transfer_start} else @{thm transfer_start'} + val err_msg = "Transfer failed to convert goal to an object-logic formula" + fun main_tac (t, i) = + resolve_tac ctxt [start_rule] i THEN + (resolve_tac ctxt [transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t)]) (i + 1) + handle TERM (_, ts) => raise TERM (err_msg, ts) + in + EVERY + [rewrite_goal_tac ctxt pre_simps i THEN + SUBGOAL main_tac i] + end; -fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) => +fun transfer_prover_start_tac ctxt = SUBGOAL (fn (t, i) => let val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t val rule1 = transfer_rule_of_term ctxt false rhs - val rules = get_transfer_raw ctxt - val eq_rules = get_relator_eq_raw ctxt val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}]) in EVERY [CONVERSION prep_conv i, resolve_tac ctxt @{thms transfer_prover_start} i, - ((resolve_tac ctxt [rule1] ORELSE' - (CONVERSION expand_eq_in_rel THEN' resolve_tac ctxt [rule1])) - THEN_ALL_NEW - (REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW - (DETERM o eq_rules_tac ctxt eq_rules))) (i + 1), - resolve_tac ctxt @{thms refl} i] - end) + (resolve_tac ctxt [rule1] ORELSE' + (CONVERSION expand_eq_in_rel THEN' resolve_tac ctxt [rule1])) (i + 1)] + end); + +fun transfer_end_tac ctxt i = + let + val post_simps = @{thms transfer_forall_eq [symmetric] + transfer_implies_eq [symmetric] transfer_bforall_unfold} + in + EVERY [rewrite_goal_tac ctxt post_simps i, + Goal.norm_hhf_tac ctxt i] + end; + +fun transfer_prover_end_tac ctxt i = resolve_tac ctxt @{thms refl} i + +local + infix 1 THEN_ALL_BUT_FIRST_NEW + fun (tac1 THEN_ALL_BUT_FIRST_NEW tac2) i st = + st |> (tac1 i THEN (fn st' => + Seq.INTERVAL tac2 (i + 1) (i + Thm.nprems_of st' - Thm.nprems_of st) st')); +in + fun transfer_tac equiv ctxt i = + let + val rules = get_transfer_raw ctxt + val eq_rules = get_relator_eq_raw ctxt + (* allow unsolved subgoals only for standard transfer method, not for transfer' *) + val end_tac = if equiv then K all_tac else K no_tac + + fun transfer_search_tac i = + (SOLVED' + (REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW + (DETERM o eq_rules_tac ctxt eq_rules)) + ORELSE' end_tac) i + in + (transfer_start_tac equiv ctxt + THEN_ALL_BUT_FIRST_NEW transfer_search_tac + THEN' transfer_end_tac ctxt) i + end + + fun transfer_prover_tac ctxt i = + let + val rules = get_transfer_raw ctxt + val eq_rules = get_relator_eq_raw ctxt + + fun transfer_prover_search_tac i = + (REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW + (DETERM o eq_rules_tac ctxt eq_rules)) i + in + (transfer_prover_start_tac ctxt + THEN_ALL_BUT_FIRST_NEW transfer_prover_search_tac + THEN' transfer_prover_end_tac ctxt) i + end +end; (** Transfer attribute **) @@ -766,10 +802,21 @@ val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon) |-- Scan.repeat free) [] +val reverse_prems = fn _ => PRIMITIVE (fn thm => fold_rev (fn i => Thm.permute_prems i 1) + (0 upto Thm.nprems_of thm - 1) thm); + +fun transfer_start_method equiv : (Proof.context -> Proof.method) context_parser = + fixing >> (fn vs => fn ctxt => + SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_start_tac equiv ctxt + THEN' reverse_prems)); + fun transfer_method equiv : (Proof.context -> Proof.method) context_parser = fixing >> (fn vs => fn ctxt => SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt)) +val transfer_prover_start_method : (Proof.context -> Proof.method) context_parser = + Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_start_tac ctxt THEN' reverse_prems)) + val transfer_prover_method : (Proof.context -> Proof.method) context_parser = Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt)) @@ -887,11 +934,25 @@ "abstract theorem transferred to raw theorem using transfer rules" #> Global_Theory.add_thms_dynamic (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get) + #> Method.setup @{binding transfer_start} (transfer_start_method true) + "firtst step in the transfer algorithm (for debugging transfer)" + #> Method.setup @{binding transfer_start'} (transfer_start_method false) + "firtst step in the transfer algorithm (for debugging transfer)" + #> Method.setup @{binding transfer_prover_start} transfer_prover_start_method + "firtst step in the transfer_prover algorithm (for debugging transfer_prover)" + #> Method.setup @{binding transfer_step} + (Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_step_tac ctxt))) + "step in the search for transfer rules (for debugging transfer and transfer_prover)" + #> Method.setup @{binding transfer_end} + (Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_end_tac ctxt))) + "last step in the transfer algorithm (for debugging transfer)" + #> Method.setup @{binding transfer_prover_end} + (Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_end_tac ctxt))) + "last step in the transfer_prover algorithm (for debugging transfer_prover)" #> 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") - end