[isabelle] Fw: term of partial_function body





-------- 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 at 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




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