Re: [isabelle] Creating Theorems in ML



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

Attachment: signature.asc
Description: OpenPGP digital signature



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