unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;
authorwenzelm
Wed May 29 16:12:05 2013 +0200 (2013-05-29)
changeset 522220fa3b456a267
parent 52221 4ffe819a9b11
child 52223 5bb6ae8acb87
unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Wed May 29 12:03:58 2013 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed May 29 16:12:05 2013 +0200
     1.3 @@ -1593,6 +1593,18 @@
     1.4    | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
     1.5  
     1.6  
     1.7 +(*unify types of schematic variables (non-lifted case)*)
     1.8 +fun unify_var_types thy (th1, th2) env =
     1.9 +  let
    1.10 +    fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types thy (T, U)) Us
    1.11 +      | unify_vars _ = I;
    1.12 +    val add_vars =
    1.13 +      full_prop_of #>
    1.14 +      fold_aterms (fn Var v => Vartab.insert_list (op =) v | _ => I);
    1.15 +    val vars = Vartab.empty |> add_vars th1 |> add_vars th2;
    1.16 +  in SOME (Vartab.fold (unify_vars o #2) vars env) end
    1.17 +  handle Pattern.Unif => NONE;
    1.18 +
    1.19  (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
    1.20    Unifies B with Bi, replacing subgoal i    (1 <= i <= n)
    1.21    If match then forbid instantiations in proof state
    1.22 @@ -1659,13 +1671,12 @@
    1.23            handle TERM _ =>
    1.24            raise THM("bicompose: 1st premise", 0, [orule])
    1.25         end;
    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  
    1.30       (*elim-resolution: try each assumption in turn*)
    1.31 -     fun eres [] = raise THM ("bicompose: no premises", 0, [orule, state])
    1.32 -       | eres (A1 :: As) =
    1.33 +     fun eres _ [] = raise THM ("bicompose: no premises", 0, [orule, state])
    1.34 +       | eres env (A1 :: As) =
    1.35             let
    1.36               val A = SOME A1;
    1.37               val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1);
    1.38 @@ -1685,14 +1696,18 @@
    1.39             in tryasms asms 1 end;
    1.40  
    1.41       (*ordinary resolution*)
    1.42 -     fun res () =
    1.43 +     fun res env =
    1.44         (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of
    1.45           NONE => Seq.empty
    1.46         | cell as SOME ((_, tpairs), _) =>
    1.47             Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
    1.48               (Seq.make (fn () => cell), Seq.empty));
    1.49 +
    1.50 +     val env0 = Envir.empty (Int.max (rmax, smax));
    1.51   in
    1.52 -   if eres_flg then eres (rev rAs) else res ()
    1.53 +   (case if lifted then SOME env0 else unify_var_types thy (state, orule) env0 of
    1.54 +     NONE => Seq.empty
    1.55 +   | SOME env => if eres_flg then eres env (rev rAs) else res env)
    1.56   end;
    1.57  end;
    1.58