Re: [isabelle] Problems with auto (at ML level)



On Thu, 10 Sep 2009, Burkhart Wolff wrote:

I found a somewhat strange difference in the behaviour of auto_tac
between an ISAR-level execution and an ML-level execution:

apply(auto intro: abs_cases )
done

In contrast:
ML{* fun auto_solver thms {prems: Thm.thm list, context: Proof.context}  =
                  auto_tac ((local_claset_of context) addIs thms,
                                     local_simpset_of context)*}


apply(tactic "(auto_solver (thms\"abs_cases\")){prems=[], context= @{context}}")

looks as if "auto intro!: abs_cases" has been fired; backtracking is reduced to just choosing
the first match and getting stuck.

The problem here is that the old operators addIs (and simular) prefer rules from right to left, while Isar declarations work in textual order from left to right. Thus the internal priorities of the rules come out differently.

Your example works, if auto_solver is defined like this:

ML {*
  fun auto_solver thms {prems: Thm.thm list, context: Proof.context} =
    auto_tac (local_claset_of context addIs (rev thms),
      local_simpset_of context)
*}

Here (rev thms) does the trick.


	Makarius





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