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.22  
    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;
    1.79