Stream: Isabelle/ML

Topic: Parsing lemma in Isar assumes/shows syntax

Sólrún Einarsdóttir (Aug 27 2024 at 13:29):

I've been parsing lemma statements from strings, using Syntax.read_prop, and I would like to also be able to parse lemma statements in the Isar assumes/shows syntax, for example the string

' fixes t :: "'a tree" and t' :: "'b tree"
  assumes "acomplete t" "size t ≤ size t'" shows "height t ≤ height t'" '

Is there a function similar to Syntax.read_prop that supports this syntax, that I can use to parse this string into a term?

Yutaka Nagashima (Sep 02 2024 at 18:23):

Sólrún Einarsdóttir said:

I've been parsing lemma statements from strings, using Syntax.read_prop, and I would like to also be able to parse lemma statements in the Isar assumes/shows syntax, for example the string

' fixes t :: "'a tree" and t' :: "'b tree"
  assumes "acomplete t" "size t ≤ size t'" shows "height t ≤ height t'" '

Is there a function similar to Syntax.read_prop that supports this syntax, that I can use to parse this string into a term?

Goal.prove might be useful? But it gives you a thm.

Yutaka Nagashima (Sep 02 2024 at 18:26):

Proof.theorem if you want to work on Proof.state?

Last updated: Dec 21 2024 at 16:20 UTC