Re: [isabelle] [isabelle-dev] Malformed YXML encoding



On Fri, 26 Aug 2011, Steve Wong wrote:

I'm trying to generate a proof goal from string using the following:

I am answering this on isabelle-users, because it is a perfectly normal user question. (Using ML alone does not mean it is relevant for isabelle-dev.)


fun generate x lthy =
   let
       val thy = Local_Theory.exit_global lthy
       val ctxt = ProofContext.init_global thy
   in

This is a bit odd. You can use lthy, which is called "auxiliary context" in local theory parlance directly as your context for the subsequent operations. A lthy: local_theory is a semantic subtype of ctxt: Proof.context, and the lthy naming convention is used whenever actual local theory operations follow, like the subsequent Specification.theorem_cmd.

       (Specification.theorem_cmd
            Thm.lemmaK NONE (K I)
            (Binding.name "", []) []

            (Element.Shows [(Attrib.empty_binding,
                             [(Syntax.string_of_term ctxt @{term "F"} ^ " =
" ^
                               Syntax.string_of_term ctxt @{term "G"}

, [])])]) x lthy)
   end

*** Malformed YXML encoding: multiple results
*** At command "verify_with"

Syntax.string_of_term turns internal formal entities (terms) into external text representation for user-consumption. For historic reasons the string type is used here, but it is in fact some kind of quasi-abstract datatype for marked-up document content. In general it is not allowed either to split text input that is passed in or paste together text that is passed out of the formal environment.

Working with string interfaces for formal entities was never robust, even 20 years ago, but now the fragility has become immediately apparent. When "generating" things, you should always use the regular non-text versions of tools and packages. (Sometines people forget to provide them, but for almost everything in the regular Isabelle distribution there is such a proper non-text version, taking directly typ and term values etc.)

Anyway, instead of Specification.theorem it is probably easier to use Proof.theorem, although you need to store the result yourself in the "after_qed" continuation.


	Makarius






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