always expand equalities in the transfer relation in transfer_prover (cf. 0a7c97c76f46)
authorkuncar
Mon Oct 31 16:26:36 2016 +0100 (2016-10-31)
changeset 64434af5235830c16
parent 64433 d4829dc875fb
child 64435 c93b0e6131c3
always expand equalities in the transfer relation in transfer_prover (cf. 0a7c97c76f46)
src/HOL/Tools/Transfer/transfer.ML
     1.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Mon Oct 31 15:48:27 2016 +0100
     1.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Mon Oct 31 16:26:36 2016 +0100
     1.3 @@ -19,6 +19,8 @@
     1.4    val top_sweep_rewr_conv: thm list -> conv
     1.5  
     1.6    val prep_conv: conv
     1.7 +  val fold_relator_eqs_conv: Proof.context -> conv
     1.8 +  val unfold_relator_eqs_conv: Proof.context -> conv
     1.9    val get_transfer_raw: Proof.context -> thm list
    1.10    val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
    1.11    val get_relator_eq: Proof.context -> thm list
    1.12 @@ -231,6 +233,10 @@
    1.13        else_conv
    1.14        Conv.all_conv) ct
    1.15  
    1.16 +fun fold_relator_eqs_conv ctxt ct = (bottom_rewr_conv (get_relator_eq ctxt)) ct;
    1.17 +fun unfold_relator_eqs_conv ctxt ct = (top_rewr_conv (get_sym_relator_eq ctxt)) ct;
    1.18 +
    1.19 +
    1.20  (** Replacing explicit equalities with is_equality premises **)
    1.21  
    1.22  fun mk_is_equality t =
    1.23 @@ -278,7 +284,7 @@
    1.24            Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
    1.25        end
    1.26      val contracted_eq_thm =
    1.27 -      Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
    1.28 +      Conv.fconv_rule (transfer_rel_conv (fold_relator_eqs_conv ctxt)) thm
    1.29        handle CTERM _ => thm
    1.30    in
    1.31      gen_abstract_equalities ctxt dest contracted_eq_thm
    1.32 @@ -301,7 +307,7 @@
    1.33      fun transfer_rel_conv conv =
    1.34        Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv)))
    1.35      val contracted_eq_thm =
    1.36 -      Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
    1.37 +      Conv.fconv_rule (transfer_rel_conv (fold_relator_eqs_conv ctxt)) thm
    1.38    in
    1.39      gen_abstract_equalities ctxt dest contracted_eq_thm
    1.40    end
    1.41 @@ -654,13 +660,13 @@
    1.42    let
    1.43      val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
    1.44      val rule1 = transfer_rule_of_term ctxt false rhs
    1.45 -    val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])
    1.46 +    val expand_eqs_in_rel_conv = transfer_rel_conv (unfold_relator_eqs_conv ctxt)
    1.47    in
    1.48      EVERY
    1.49        [CONVERSION prep_conv i,
    1.50 +       CONVERSION expand_eqs_in_rel_conv i,
    1.51         resolve_tac ctxt @{thms transfer_prover_start} i,
    1.52 -       (resolve_tac ctxt [rule1] ORELSE'
    1.53 -         (CONVERSION expand_eq_in_rel THEN' resolve_tac ctxt [rule1])) (i + 1)]
    1.54 +       resolve_tac ctxt [rule1] (i + 1)]
    1.55    end);
    1.56  
    1.57  fun transfer_end_tac ctxt i =