Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] term of partial_function body

Email Gateway (Aug 22 2022 at 16:52):

From: Walther Neuper <wneuper@ist.tugraz.at>
How get can one the term of the body from a function defined as
partial_function ?

Example: From a function definition like

partial_function (tailrec)
  solve_equation :: "bool ⇒ int ⇒ bool list "
where
  "solve_equation eq bdv = {eq, eq, eq}"

we get

val t as Const ("Scratch.solve_equation", T) = @{term solve_equation}
(* T = "bool ⇒ int ⇒ bool list" *)

while we also want

val Const ("Set.insert", _) $ Free ("eq", _) $
     (Const ("Set.insert", _) $ Free ("eq", _) $
       (Const ("Set.insert", _) $ Free ("eq", _) $
         Const ("Orderings.bot_class.bot", _))) = @{term "{eq, eq, eq}"}

from the definition by "partial_function".

Thanks in advance,
Walther

Email Gateway (Aug 22 2022 at 16:52):

From: Peter Lammich <lammich@in.tum.de>
\-------- Original Message --------
Subject: Re: [isabelle] term of partial_function body
From: Peter Lammich
To: Walther Neuper
CC:

There should be a theorem solve_equation.simps, and its rhs should be the
term you are looking for.

Peter

\-------- Original Message --------
Subject: [isabelle] term of partial_function body
From: Walther Neuper
To: cl-isabelle-users@lists.cam.ac.uk
CC:

How get can one the term of the body from a function defined as
partial_function ?

Example: From a function definition like

partial_function (tailrec)
solve_equation :: "bool ⇒ int ⇒ bool list "
where
"solve_equation eq bdv = {eq, eq, eq}"

we get

val t as Const ("Scratch.solve_equation", T) = @{term solve_equation}
(* T = "bool ⇒ int ⇒ bool list" *)

while we also want

val Const ("Set.insert", _) $ Free ("eq", _) $
(Const ("Set.insert", _) $ Free ("eq", _) $
(Const ("Set.insert", _) $ Free ("eq", _) $
Const ("Orderings.bot_class.bot", _))) = @{term "{eq, eq, eq}"}

from the definition by "partial_function".

Thanks in advance,
Walther

Email Gateway (Aug 22 2022 at 16:52):

From: Walther Neuper <wneuper@ist.tugraz.at>
On 2018-03-29 21:21, Peter Lammich wrote:

There should be a theorem solve_equation.simps, and its rhs should
be the term you are looking for.

Ahhh, there is all we need in Isabelle/ML (while a theorem cannot be not
found in Isabele/jEdit for good reasons).

Thanks a lot (saved much time for hacking context.ML) !

Peter

Walther

Last updated: Apr 26 2024 at 12:28 UTC