[isabelle] Handling of invalid type variable names on ML level



Hi,

I am not sure the following situation should be considered a bug or not,
since it occurs only when using Isabelle incorrectly. But I feel that it
probably indicates that invalid input is not detected in time, and it may
lead to very hard to understand problems (starting from a typo). So I just
explain the problem and leave it to the Isabelle-experts to decide whether
it indicates a real problem or not.

The problem is exhibited by the theory below. But in a nutshell, we have
the following situation:

   - It is possible to prove a theorem with a type variable called *a* (not
   *'a*). I understand that I should not do that, of course. But there is
   no error when proving the theorem.
   - Then, if we try to use OF with that theorem, we get unexpected
   failures. But only if *a* is the name of a fixed variable (not type
   variable).

I guess that type variable *a* should probably just be rejected when trying
to prove the theorem. But even if not, it is surprising that the existence
of a fixed variable *a* makes a difference since I would have assumed that
free variables and free type variables have completely independent name
spaces.


theory Test
  imports Main
begin

lemma x: fixes c :: int assumes "c = d" shows "True" ..

context fixes a :: int begin

ML {*
val ctx = @{context}
val T = TFree(("a"),@{sort type}) (* Note the incorrect "a" instead of "'a"
*)
val l = Free(("l"),T)
val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (l,l)) (* prop = "l=l" *)
fun tac {context=ctx, ...} = ALLGOALS (simp_tac ctx)
val thm = Goal.prove ctx ["l"] [] prop tac (* proving prop *)
val _ = @{thm x} OF [thm] (* Fails with "no unifiers". But succeeds if
"fixes a" above is "fixes b" *)
*}

Best wishes,
Dominique.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.