prefer existing beta_eta_conversion;
authorwenzelm
Thu May 30 16:11:14 2013 +0200 (2013-05-30)
changeset 522396a6033fa507c
parent 52238 d84ff5a93764
child 52240 066c2ff17f7c
prefer existing beta_eta_conversion;
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/eqsubst.ML
     1.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Thu May 30 15:51:55 2013 +0200
     1.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu May 30 16:11:14 2013 +0200
     1.3 @@ -7,11 +7,6 @@
     1.4  
     1.5  signature RW_INST =
     1.6  sig
     1.7 -
     1.8 -  val beta_eta_contract : thm -> thm
     1.9 -
    1.10 -  (* Rewrite: give it instantiation infromation, a rule, and the
    1.11 -  target thm, and it will return the rewritten target thm *)
    1.12    val rw : Proof.context ->
    1.13        ((indexname * (sort * typ)) list *  (* type var instantiations *)
    1.14         (indexname * (typ * term)) list)  (* schematic var instantiations *)
    1.15 @@ -28,15 +23,6 @@
    1.16  structure RWInst : RW_INST =
    1.17  struct
    1.18  
    1.19 -
    1.20 -(* beta-eta contract the theorem *)
    1.21 -fun beta_eta_contract thm =
    1.22 -    let
    1.23 -      val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    1.24 -      val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    1.25 -    in thm3 end;
    1.26 -
    1.27 -
    1.28  (* Given a list of variables that were bound, and a that has been
    1.29  instantiated with free variable placeholders for the bound vars, it
    1.30  creates an abstracted version of the theorem, with local bound vars as
    1.31 @@ -234,7 +220,7 @@
    1.32            rule_inst |> Thm.instantiate ([], cterm_renamings)
    1.33                      |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
    1.34        val specific_tgt_rule =
    1.35 -          beta_eta_contract
    1.36 +          Conv.fconv_rule Drule.beta_eta_conversion
    1.37              (Thm.combination couter_inst abstract_rule_inst);
    1.38  
    1.39        (* create an instantiated version of the target thm *)
    1.40 @@ -245,7 +231,7 @@
    1.41        val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
    1.42  
    1.43      in
    1.44 -      (beta_eta_contract tgt_th_inst)
    1.45 +      Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst
    1.46          |> Thm.equal_elim specific_tgt_rule
    1.47          |> Drule.implies_intr_list cprems
    1.48          |> Drule.forall_intr_list frees_of_fixed_vars
     2.1 --- a/src/Tools/eqsubst.ML	Thu May 30 15:51:55 2013 +0200
     2.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 16:11:14 2013 +0200
     2.3 @@ -247,7 +247,7 @@
     2.4  fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
     2.5    RWInst.rw ctxt m rule conclthm
     2.6    |> IsaND.unfix_frees cfvs
     2.7 -  |> RWInst.beta_eta_contract
     2.8 +  |> Conv.fconv_rule Drule.beta_eta_conversion
     2.9    |> (fn r => Tactic.rtac r i st);
    2.10  
    2.11  (* substitute within the conclusion of goal i of gth, using a meta
    2.12 @@ -327,7 +327,7 @@
    2.13        |> (Seq.hd o prune_params_tac)
    2.14        |> Thm.permute_prems 0 ~1 (* put old asm first *)
    2.15        |> IsaND.unfix_frees cfvs (* unfix any global params *)
    2.16 -      |> RWInst.beta_eta_contract; (* normal form *)
    2.17 +      |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
    2.18    in
    2.19      (* ~j because new asm starts at back, thus we subtract 1 *)
    2.20      Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))