apply transfer_prover after folding relator_eq
authortraytel
Mon Oct 24 16:53:32 2016 +0200 (2016-10-24)
changeset 64378e9eb0b99a44c
parent 64377 c1db9e3fe0e2
child 64379 71f42dcaa1df
apply transfer_prover after folding relator_eq
src/HOL/Library/BNF_Corec.thy
src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML
     1.1 --- a/src/HOL/Library/BNF_Corec.thy	Mon Oct 24 16:16:55 2016 +0200
     1.2 +++ b/src/HOL/Library/BNF_Corec.thy	Mon Oct 24 16:53:32 2016 +0200
     1.3 @@ -206,6 +206,10 @@
     1.4  ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML"
     1.5  ML_file "../Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
     1.6  
     1.7 +method_setup transfer_prover_eq = \<open>
     1.8 +  Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Tactics.transfer_prover_eq_tac)
     1.9 +\<close> "apply transfer_prover after folding relator_eq"
    1.10 +
    1.11  method_setup corec_unique = \<open>
    1.12    Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Unique_Sugar.corec_unique_tac)
    1.13  \<close> "prove uniqueness of corecursive equation"
     2.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML	Mon Oct 24 16:16:55 2016 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML	Mon Oct 24 16:53:32 2016 +0200
     2.3 @@ -8,6 +8,7 @@
     2.4  
     2.5  signature BNF_GFP_GREC_TACTICS =
     2.6  sig
     2.7 +  val transfer_prover_eq_tac: Proof.context -> int -> tactic
     2.8    val transfer_prover_add_tac: Proof.context -> thm list -> thm list -> int -> tactic
     2.9  
    2.10    val mk_algLam_algLam_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
    2.11 @@ -82,8 +83,12 @@
    2.12      rel_eqs ctxt;
    2.13  val context_transfer_rule_add = fold (snd oo Thm.proof_attributes [Transfer.transfer_add]);
    2.14  
    2.15 +fun transfer_prover_eq_tac ctxt =
    2.16 +  SELECT_GOAL (Local_Defs.fold_tac ctxt (Transfer.get_relator_eq ctxt)) THEN'
    2.17 +  Transfer.transfer_prover_tac ctxt;
    2.18 +
    2.19  fun transfer_prover_add_tac ctxt rel_eqs transfers =
    2.20 -  Transfer.transfer_prover_tac (ctxt
    2.21 +  transfer_prover_eq_tac (ctxt
    2.22      |> context_relator_eq_add rel_eqs
    2.23      |> context_transfer_rule_add transfers);
    2.24