src/Pure/thm.ML
 changeset 30554 73f8bd5f0af8 parent 30466 5f31e24937c5 child 30556 7be15917f3fa
1.1 --- a/src/Pure/thm.ML	Mon Mar 16 23:39:44 2009 +0100
1.2 +++ b/src/Pure/thm.ML	Mon Mar 16 23:52:30 2009 +0100
1.3 @@ -1247,12 +1247,17 @@
1.4            else (*normalize the new rule fully*)
1.5              Envir.norm_term env (Logic.list_implies (Bs, C)),
1.6          thy_ref = Theory.check_thy thy});
1.7 +
1.8 +    val (close, Hs, C) = Logic.assum_problems (~1, Bi);
1.9 +    val C' = close C;
1.10      fun addprfs [] _ = Seq.empty
1.11 -      | addprfs ((t, u) :: apairs) n = Seq.make (fn () => Seq.pull
1.12 +      | addprfs (H :: rest) n = Seq.make (fn () => Seq.pull
1.13            (Seq.mapp (newth n)
1.14 -            (Unify.unifiers (thy, Envir.empty maxidx, (t, u) :: tpairs))
1.15 -            (addprfs apairs (n + 1))))
1.16 -  in addprfs (Logic.assum_pairs (~1, Bi)) 1 end;
1.17 +            (if Term.could_unify (H, C) then
1.18 +              (Unify.unifiers (thy, Envir.empty maxidx, (close H, C') :: tpairs))
1.19 +             else Seq.empty)
1.20 +            (addprfs rest (n + 1))))
1.21 +  in addprfs Hs 1 end;
1.23  (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
1.24    Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
1.25 @@ -1520,24 +1525,37 @@
1.26       val env = Envir.empty(Int.max(rmax,smax));
1.27       val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
1.28       val dpairs = BBi :: (rtpairs@stpairs);
1.29 -     (*elim-resolution: try each assumption in turn.  Initially n=1*)
1.30 -     fun tryasms (_, _, _, []) = Seq.empty
1.31 -       | tryasms (A, As, n, (t,u)::apairs) =
1.32 -          (case Seq.pull(Unify.unifiers(thy, env, (t,u)::dpairs))  of
1.33 -              NONE                   => tryasms (A, As, n+1, apairs)
1.34 -            | cell as SOME((_,tpairs),_) =>
1.35 -                Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs)))
1.36 -                    (Seq.make(fn()=> cell),
1.37 -                     Seq.make(fn()=> Seq.pull (tryasms(A, As, n+1, apairs)))))
1.38 -     fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
1.39 -       | eres (A1::As) = tryasms(SOME A1, As, 1, Logic.assum_pairs(nlift+1,A1))
1.40 +
1.41 +     (*elim-resolution: try each assumption in turn*)
1.42 +     fun eres [] = raise THM ("bicompose: no premises", 0, [orule, state])
1.43 +       | eres (A1 :: As) =
1.44 +           let
1.45 +             val A = SOME A1;
1.46 +             val (close, Hs, C) = Logic.assum_problems (nlift + 1, A1);
1.47 +             val C' = close C;
1.48 +             fun tryasms [] _ = Seq.empty
1.49 +               | tryasms (H :: rest) n =
1.50 +                   if Term.could_unify (H, C) then
1.51 +                     let val H' = close H in
1.52 +                       (case Seq.pull (Unify.unifiers (thy, env, (H', C') :: dpairs)) of
1.53 +                         NONE => tryasms rest (n + 1)
1.54 +                       | cell as SOME ((_, tpairs), _) =>
1.55 +                           Seq.it_right (addth A (newAs (As, n, [BBi, (C', H')], tpairs)))
1.56 +                             (Seq.make (fn () => cell),
1.57 +                              Seq.make (fn () => Seq.pull (tryasms rest (n + 1)))))
1.58 +                     end
1.59 +                   else tryasms rest (n + 1);
1.60 +           in tryasms Hs 1 end;
1.61 +
1.62       (*ordinary resolution*)
1.63 -     fun res(NONE) = Seq.empty
1.64 -       | res(cell as SOME((_,tpairs),_)) =
1.65 -             Seq.it_right (addth NONE (newAs(rev rAs, 0, [BBi], tpairs)))
1.66 -                       (Seq.make (fn()=> cell), Seq.empty)
1.67 - in  if eres_flg then eres(rev rAs)
1.68 -     else res(Seq.pull(Unify.unifiers(thy, env, dpairs)))
1.69 +     fun res () =
1.70 +       (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of
1.71 +         NONE => Seq.empty
1.72 +       | cell as SOME ((_, tpairs), _) =>
1.73 +           Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
1.74 +             (Seq.make (fn () => cell), Seq.empty));
1.75 + in
1.76 +   if eres_flg then eres (rev rAs) else res ()
1.77   end;
1.78  end;