Re: [isabelle] Same proof state, different metis behaviour



Hi Joachim,

> consider this theory, which uses Nominal2

Could you specify precisely which version of Nominal2 and of Isabelle you're using? I'm using the latest of both and get this error from Nominal2:

*** Error (line 251 of "/Users/blanchet/misc/nominal2/Nominal/nominal_dt_alpha.ML"):
*** Type error in function application.
***    Function: Inductive.add_inductive_i :
***       inductive_flags ->
***       ((binding * typ) * mixfix) list ->
***       (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory -> inductive_result * local_theory
***    Argument: {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = ..., ...} :
***       {coind: bool,
***        no_ind: bool, no_elim: bool, verbose: bool, alt_name: binding, fork_mono: bool, skip_mono: bool, quiet_mode: bool}
***    Reason:
***    Can't unify {coind: bool, no_ind: bool, no_elim: bool, verbose: bool, alt_name: binding, skip_mono: bool, quiet_mode: bool}
***       to {coind: bool,
***           no_ind: bool, no_elim: bool, verbose: bool, alt_name: binding, fork_mono: bool, skip_mono: bool, quiet_mode: bool}
***       (Different number of fields)
*** 
*** At command "use" (line 27 of "/Users/blanchet/misc/nominal2/Nominal/Nominal2.thy")

> Nevertheless, in the first lemma, metis finds the proof sufficiently
> fast, while in the second, it does not find any proof. As this is
> probably not the intended behavior I was told to report that here.

That certainly sounds strange. Are the goals really identical, or is one using metaequality and the other object-level equality?

Jasmin






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