beta-eta-contract, to respect "first_order_match"'s specification;
authorblanchet
Fri Jun 11 17:07:27 2010 +0200 (2010-06-11)
changeset 37398e194213451c9
parent 37397 18000f9d783e
child 37399 34f080a12063
beta-eta-contract, to respect "first_order_match"'s specification;
Sledgehammer's Skolem cache sometimes failed without the contraction
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/Tools/meson.ML	Fri Jun 11 17:05:11 2010 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri Jun 11 17:07:27 2010 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  sig
     1.5    val trace: bool Unsynchronized.ref
     1.6    val term_pair_of: indexname * (typ * 'a) -> term * 'a
     1.7 -  val first_order_resolve: thm -> thm -> thm
     1.8    val flexflex_first_order: thm -> thm
     1.9    val size_of_subgoals: thm -> int
    1.10    val too_many_clauses: Proof.context option -> term -> bool
    1.11 @@ -98,11 +97,14 @@
    1.12        let val thy = theory_of_thm thA
    1.13            val tmA = concl_of thA
    1.14            val Const("==>",_) $ tmB $ _ = prop_of thB
    1.15 -          val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
    1.16 +          val tenv =
    1.17 +            Pattern.first_order_match thy
    1.18 +                (pairself Envir.beta_eta_contract (tmB, tmA))
    1.19 +                (Vartab.empty, Vartab.empty) |> snd
    1.20            val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    1.21        in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
    1.22      SOME th => th
    1.23 -  | NONE => raise THM ("first_order_resolve", 0, [thA, thB]));
    1.24 +  | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
    1.25  
    1.26  fun flexflex_first_order th =
    1.27    case (tpairs_of th) of
    1.28 @@ -316,9 +318,11 @@
    1.29      exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
    1.30  
    1.31  fun apply_skolem_ths (th, rls) =
    1.32 -  let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
    1.33 -        | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
    1.34 -  in  tryall rls  end;
    1.35 +  let
    1.36 +    fun tryall [] = raise THM ("apply_skolem_ths", 0, th::rls)
    1.37 +      | tryall (rl :: rls) =
    1.38 +        first_order_resolve th rl handle THM _ => tryall rls
    1.39 +  in tryall rls end
    1.40  
    1.41  (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
    1.42    Strips universal quantifiers and breaks up conjunctions.