On 08/03/2011 12:34 PM, Lawrence Paulson wrote:
Many thanks for your analysis. It looks like an interaction involving "fix" and
bound variables.
Not too fast :-)
We must now peel off the various layers of Isar (recall that "show" is
just a normal refinement step), to get closer to the problem. The
attached theory exposes the same issue in a bare-bones HOL, using plain
rule application. Note that after the "apply (rule R)", the two
arguments of P have been "over-unified", which makes the following
assumption step fail. Using the alpha-equivalent rule R2, the same works
nicely.
The same can be done in low-level ML, using just "rtac", which suggests
that the error is somewhere in the underlying Thm.biresolution etc. So
far, I have not looked any further...
I could reproduce the same behaviour in Isabelle 2005, so the issue has
been around for a while... possibly much longer.
Alex
theory Odd_Failure
imports HOL
begin
typedecl nat
consts
P :: "nat \<Rightarrow> nat \<Rightarrow> bool"
Q :: "nat \<Rightarrow> bool"
lemma R: (* triggers the error *)
fixes s t :: nat assumes "P s t"
shows "\<forall>(s::nat) (t::nat). Q t" sorry
lemma R2: (* works as expected, with (unused) bound variable renamed. *)
fixes s t :: nat assumes "P s t"
shows "\<forall>(s'::nat) (t::nat). Q t" sorry
(* both rules are alpha-equivalent: *)
ML {*
(op aconv o pairself prop_of) (@{thm R}, @{thm R2})
*}
lemma "\<And>(a::nat) (b::nat). P a b \<Longrightarrow> \<forall>(c::nat)
(c::nat). Q c"
apply (rule R) (* wrong step here *)
(*apply assumption*) (* fails here *)
oops
text {* The same thing in ML without any Isar management: *}
ML {*
let
val goal = @{cprop "\<And>(a::nat) (b::nat). P a b \<Longrightarrow>
\<forall>(c::nat) (c::nat). Q c"}
val rule = @{thm R}
val st = Goal.init goal
in
st |> rtac rule 1 |> Seq.hd
end
*}
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
