Re: [isabelle] Creating Theorems in ML



Hi Florian,

Thank you for your e-mail.

I think you the issue you pointed out might be the cause of the problem. I managed to get something going by separating the process into multiple steps. Creating a locale and proving theorems at the same time, while referring to locale state seem to have caused some issues there.

In the end, Syntax.read_props was also helpful to create the props.

-- Reto

--

Reto Achermann
PhD Student, Systems Group, ETH Zurich



On 2019-03-07 15:44:02+01:00 Florian Haftmann wrote:

Hi Reto,

> Now, I'd like to use my own datatype in this lemma e.g.
>
> # datatype MyT = MyType string
> # lemma foobar : "MyType t ∈ st ⟹ A ⟹ (A⟹B) ⟹ (B⟹P) ⟹ P
>
> Which works well from within a Theory, but I want to create this lemma from my ML code using the datatype MyT  which has been defined in a Theory file.
>
>
> # Goal.prove ctxt vars asms prop auto_tac
> # where prop =  @{prop "MyType t ∈ st ⟹ A ⟹ (A⟹B) ⟹ (B⟹P) ⟹ P"}
>
> Which results in an error: Illegal fixed variable: "MyType"
>
> Is the use of the antiquotations @{prop } actually the right way to achieve this?

note that antiquotations are resolved *statically* when processing an
Isabelle/ML block, hence I guess the issue is that you make a reference
to a symbol which is not yet present when the Isabelle/ML is parsed.

I do not know what your application context is, but if you are plumbing
Isabelle/ML pieces in a theory file (which is usually a good starting
point for experimentation), it is sufficient to have the antiquotation
in question in a separate Isabelle/ML block.

Cheers,
        Florian




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