substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
authorwenzelm
Mon Mar 16 23:52:30 2009 +0100 (2009-03-16)
changeset 3055473f8bd5f0af8
parent 30553 0709fda91b06
child 30555 5925cd6671d5
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
src/Pure/logic.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/logic.ML	Mon Mar 16 23:39:44 2009 +0100
     1.2 +++ b/src/Pure/logic.ML	Mon Mar 16 23:52:30 2009 +0100
     1.3 @@ -65,6 +65,7 @@
     1.4    val flatten_params: int -> term -> term
     1.5    val list_rename_params: string list * term -> term
     1.6    val assum_pairs: int * term -> (term*term)list
     1.7 +  val assum_problems: int * term -> (term -> term) * term list * term
     1.8    val varifyT: typ -> typ
     1.9    val unvarifyT: typ -> typ
    1.10    val varify: term -> term
    1.11 @@ -462,6 +463,13 @@
    1.12    in  pairrev (Hs,[])
    1.13    end;
    1.14  
    1.15 +fun assum_problems (nasms, A) =
    1.16 +  let
    1.17 +    val (params, A') = strip_assums_all ([], A)
    1.18 +    val (Hs, B) = strip_assums_imp (nasms, [], A')
    1.19 +    fun abspar t = rlist_abs (params, t)
    1.20 +  in (abspar, rev Hs, B) end;
    1.21 +
    1.22  
    1.23  (* global schematic variables *)
    1.24  
     2.1 --- a/src/Pure/thm.ML	Mon Mar 16 23:39:44 2009 +0100
     2.2 +++ b/src/Pure/thm.ML	Mon Mar 16 23:52:30 2009 +0100
     2.3 @@ -1247,12 +1247,17 @@
     2.4            else (*normalize the new rule fully*)
     2.5              Envir.norm_term env (Logic.list_implies (Bs, C)),
     2.6          thy_ref = Theory.check_thy thy});
     2.7 +
     2.8 +    val (close, Hs, C) = Logic.assum_problems (~1, Bi);
     2.9 +    val C' = close C;
    2.10      fun addprfs [] _ = Seq.empty
    2.11 -      | addprfs ((t, u) :: apairs) n = Seq.make (fn () => Seq.pull
    2.12 +      | addprfs (H :: rest) n = Seq.make (fn () => Seq.pull
    2.13            (Seq.mapp (newth n)
    2.14 -            (Unify.unifiers (thy, Envir.empty maxidx, (t, u) :: tpairs))
    2.15 -            (addprfs apairs (n + 1))))
    2.16 -  in addprfs (Logic.assum_pairs (~1, Bi)) 1 end;
    2.17 +            (if Term.could_unify (H, C) then
    2.18 +              (Unify.unifiers (thy, Envir.empty maxidx, (close H, C') :: tpairs))
    2.19 +             else Seq.empty)
    2.20 +            (addprfs rest (n + 1))))
    2.21 +  in addprfs Hs 1 end;
    2.22  
    2.23  (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
    2.24    Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
    2.25 @@ -1520,24 +1525,37 @@
    2.26       val env = Envir.empty(Int.max(rmax,smax));
    2.27       val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
    2.28       val dpairs = BBi :: (rtpairs@stpairs);
    2.29 -     (*elim-resolution: try each assumption in turn.  Initially n=1*)
    2.30 -     fun tryasms (_, _, _, []) = Seq.empty
    2.31 -       | tryasms (A, As, n, (t,u)::apairs) =
    2.32 -          (case Seq.pull(Unify.unifiers(thy, env, (t,u)::dpairs))  of
    2.33 -              NONE                   => tryasms (A, As, n+1, apairs)
    2.34 -            | cell as SOME((_,tpairs),_) =>
    2.35 -                Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs)))
    2.36 -                    (Seq.make(fn()=> cell),
    2.37 -                     Seq.make(fn()=> Seq.pull (tryasms(A, As, n+1, apairs)))))
    2.38 -     fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
    2.39 -       | eres (A1::As) = tryasms(SOME A1, As, 1, Logic.assum_pairs(nlift+1,A1))
    2.40 +
    2.41 +     (*elim-resolution: try each assumption in turn*)
    2.42 +     fun eres [] = raise THM ("bicompose: no premises", 0, [orule, state])
    2.43 +       | eres (A1 :: As) =
    2.44 +           let
    2.45 +             val A = SOME A1;
    2.46 +             val (close, Hs, C) = Logic.assum_problems (nlift + 1, A1);
    2.47 +             val C' = close C;
    2.48 +             fun tryasms [] _ = Seq.empty
    2.49 +               | tryasms (H :: rest) n =
    2.50 +                   if Term.could_unify (H, C) then
    2.51 +                     let val H' = close H in
    2.52 +                       (case Seq.pull (Unify.unifiers (thy, env, (H', C') :: dpairs)) of
    2.53 +                         NONE => tryasms rest (n + 1)
    2.54 +                       | cell as SOME ((_, tpairs), _) =>
    2.55 +                           Seq.it_right (addth A (newAs (As, n, [BBi, (C', H')], tpairs)))
    2.56 +                             (Seq.make (fn () => cell),
    2.57 +                              Seq.make (fn () => Seq.pull (tryasms rest (n + 1)))))
    2.58 +                     end
    2.59 +                   else tryasms rest (n + 1);
    2.60 +           in tryasms Hs 1 end;
    2.61 +
    2.62       (*ordinary resolution*)
    2.63 -     fun res(NONE) = Seq.empty
    2.64 -       | res(cell as SOME((_,tpairs),_)) =
    2.65 -             Seq.it_right (addth NONE (newAs(rev rAs, 0, [BBi], tpairs)))
    2.66 -                       (Seq.make (fn()=> cell), Seq.empty)
    2.67 - in  if eres_flg then eres(rev rAs)
    2.68 -     else res(Seq.pull(Unify.unifiers(thy, env, dpairs)))
    2.69 +     fun res () =
    2.70 +       (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of
    2.71 +         NONE => Seq.empty
    2.72 +       | cell as SOME ((_, tpairs), _) =>
    2.73 +           Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
    2.74 +             (Seq.make (fn () => cell), Seq.empty));
    2.75 + in
    2.76 +   if eres_flg then eres (rev rAs) else res ()
    2.77   end;
    2.78  end;
    2.79