Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] code_pred / inductive / lfp

view this post on Zulip Email Gateway (Feb 18 2025 at 09:22):

From: Tobias Nipkow <nipkow@in.tum.de>
I am trying to generate code from this inductive definition:

inductive nullable :: "(int * int list) list ⇒ int ⇒ bool"
for ps where
"⟦ mem ps (A, w); ∀s ∈ set w. nullable ps s⟧
⟹ nullable ps A"

where mem is the auxiliary definition

inductive mem :: "'a list ⇒ 'a ⇒ bool" where
"mem (x#xs) x" |
"mem xs y ⟹ mem (x#xs) y"

(I thought List.member does the job but that didn't work)

Back to nullable: this evaluation diverges:

values "{s. nullable [(1,[1, 0])] s}"

How can I fix this?

Alternatively, for my purposes it may be simpler to use the lfp-definition of
nullable. However, I can only find

HOL.nitpick_unfold(176):
nullable ≡ λps. lfp (λp x. ∃A w. x = A ∧ mem ps (A, w) ∧ (∀s∈set w. p s))

Is there no direct access to this def (not needing nitpick_unfold)? I seem to
remember it is hidden, but maybe there is a switch?

Tobias

smime.p7s

view this post on Zulip Email Gateway (Feb 18 2025 at 09:30):

From: Jan van Brügge <jan@vanbruegge.de>
Hi Tobias,

if you do declare [inductive_internals] before the definition of
nullable, the lfp definition will be available as "nullable_def"

Cheers,
Jan

Am 18.02.25 um 09:22 schrieb Tobias Nipkow:

I am trying to generate code from this inductive definition:

inductive nullable :: "(int * int list) list ⇒ int ⇒ bool"
for ps where
  "⟦ mem ps (A, w); ∀s ∈ set w. nullable ps s⟧
  ⟹ nullable ps A"

where mem is the auxiliary definition

inductive mem :: "'a list ⇒ 'a ⇒ bool" where
  "mem (x#xs) x" |
  "mem xs y ⟹ mem (x#xs) y"

(I thought List.member does the job but that didn't work)

Back to nullable: this evaluation diverges:

values "{s. nullable [(1,[1, 0])] s}"

How can I fix this?

Alternatively, for my purposes it may be simpler to use the
lfp-definition of nullable. However, I can only find

HOL.nitpick_unfold(176):
nullable ≡ λps. lfp (λp x. ∃A w. x = A ∧ mem ps (A, w) ∧ (∀s∈set w. p s))

Is there no direct access to this def (not needing nitpick_unfold)? I
seem to remember it is hidden, but maybe there is a switch?

Tobias

view this post on Zulip Email Gateway (Feb 18 2025 at 09:32):

From: Tobias Nipkow <nipkow@in.tum.de>
Thanks Jan, that's what I as looking for (and couldn't find in the Ref Man ...).

Tobias

On 18/02/2025 10:24, Jan van Brügge wrote:

Hi Tobias,

if you do declare [inductive_internals] before the definition of nullable, the
lfp definition will be available as "nullable_def"

Cheers,
Jan

Am 18.02.25 um 09:22 schrieb Tobias Nipkow:

I am trying to generate code from this inductive definition:

inductive nullable :: "(int * int list) list ⇒ int ⇒ bool"
for ps where
  "⟦ mem ps (A, w); ∀s ∈ set w. nullable ps s⟧
  ⟹ nullable ps A"

where mem is the auxiliary definition

inductive mem :: "'a list ⇒ 'a ⇒ bool" where
  "mem (x#xs) x" |
  "mem xs y ⟹ mem (x#xs) y"

(I thought List.member does the job but that didn't work)

Back to nullable: this evaluation diverges:

values "{s. nullable [(1,[1, 0])] s}"

How can I fix this?

Alternatively, for my purposes it may be simpler to use the lfp-definition of
nullable. However, I can only find

HOL.nitpick_unfold(176):
nullable ≡ λps. lfp (λp x. ∃A w. x = A ∧ mem ps (A, w) ∧ (∀s∈set w. p s))

Is there no direct access to this def (not needing nitpick_unfold)? I seem to
remember it is hidden, but maybe there is a switch?

Tobias

smime.p7s

view this post on Zulip Email Gateway (Feb 18 2025 at 19:44):

From: Tobias Nipkow <nipkow@in.tum.de>
A related question: I need to convert between fixpoints on predicates and on
sets and am using

lemma "mono P ⟹ lfp (λS. {x. P (λx. x ∈ S) x}) = {s. lfp (λp x. P p x) s}"

One direction of the proof is easy:

apply (simp add: lfp_fixpoint lfp_lowerbound)

but in the other direction I only have an ugly smt proof. Any clever
suggestions, including "transfer"?

Tobias

On 18/02/2025 10:24, Jan van Brügge wrote:

Hi Tobias,

if you do declare [inductive_internals] before the definition of nullable, the
lfp definition will be available as "nullable_def"

Cheers,
Jan

Am 18.02.25 um 09:22 schrieb Tobias Nipkow:

I am trying to generate code from this inductive definition:

inductive nullable :: "(int * int list) list ⇒ int ⇒ bool"
for ps where
  "⟦ mem ps (A, w); ∀s ∈ set w. nullable ps s⟧
  ⟹ nullable ps A"

where mem is the auxiliary definition

inductive mem :: "'a list ⇒ 'a ⇒ bool" where
  "mem (x#xs) x" |
  "mem xs y ⟹ mem (x#xs) y"

(I thought List.member does the job but that didn't work)

Back to nullable: this evaluation diverges:

values "{s. nullable [(1,[1, 0])] s}"

How can I fix this?

Alternatively, for my purposes it may be simpler to use the lfp-definition of
nullable. However, I can only find

HOL.nitpick_unfold(176):
nullable ≡ λps. lfp (λp x. ∃A w. x = A ∧ mem ps (A, w) ∧ (∀s∈set w. p s))

Is there no direct access to this def (not needing nitpick_unfold)? I seem to
remember it is hidden, but maybe there is a switch?

Tobias

smime.p7s

view this post on Zulip Email Gateway (Feb 18 2025 at 21:01):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
How about this:

lemma "{s. lfp (λp x. P p x) s} ⊆ lfp (λS. {x. P (λx. x ∈ S) x})"
    by (rule lfp_greatest)
     (simp add: less_eq_set_def lfp_lowerbound)

Stepan

On 18-Feb-25 8:44 PM, Tobias Nipkow wrote:

A related question: I need to convert between fixpoints on predicates
and on sets and am using

lemma "mono P ⟹ lfp (λS. {x. P (λx. x ∈ S) x}) = {s. lfp (λp x. P p x)
s}"

One direction of the proof is easy:

apply (simp add: lfp_fixpoint lfp_lowerbound)

but in the other direction I only have an ugly smt proof. Any clever
suggestions, including "transfer"?

Tobias

On 18/02/2025 10:24, Jan van Brügge wrote:

Hi Tobias,

if you do declare [inductive_internals] before the definition of
nullable, the lfp definition will be available as "nullable_def"

Cheers,
Jan

Am 18.02.25 um 09:22 schrieb Tobias Nipkow:

I am trying to generate code from this inductive definition:

inductive nullable :: "(int * int list) list ⇒ int ⇒ bool"
for ps where
  "⟦ mem ps (A, w); ∀s ∈ set w. nullable ps s⟧
  ⟹ nullable ps A"

where mem is the auxiliary definition

inductive mem :: "'a list ⇒ 'a ⇒ bool" where
  "mem (x#xs) x" |
  "mem xs y ⟹ mem (x#xs) y"

(I thought List.member does the job but that didn't work)

Back to nullable: this evaluation diverges:

values "{s. nullable [(1,[1, 0])] s}"

How can I fix this?

Alternatively, for my purposes it may be simpler to use the
lfp-definition of nullable. However, I can only find

HOL.nitpick_unfold(176):
nullable ≡ λps. lfp (λp x. ∃A w. x = A ∧ mem ps (A, w) ∧ (∀s∈set w.
p s))

Is there no direct access to this def (not needing nitpick_unfold)?
I seem to remember it is hidden, but maybe there is a switch?

Tobias

view this post on Zulip Email Gateway (Feb 18 2025 at 21:31):

From: Tobias Nipkow <nipkow@in.tum.de>
Cool!

Tobias

On 18/02/2025 22:01, Stepan Holub (via cl-isabelle-users Mailing List) wrote:

How about this:

lemma "{s. lfp (λp x. P p x) s} ⊆ lfp (λS. {x. P (λx. x ∈ S) x})"
    by (rule lfp_greatest)
     (simp add: less_eq_set_def lfp_lowerbound)

Stepan

On 18-Feb-25 8:44 PM, Tobias Nipkow wrote:

A related question: I need to convert between fixpoints on predicates and on
sets and am using

lemma "mono P ⟹ lfp (λS. {x. P (λx. x ∈ S) x}) = {s. lfp (λp x. P p x) s}"

One direction of the proof is easy:

apply (simp add: lfp_fixpoint lfp_lowerbound)

but in the other direction I only have an ugly smt proof. Any clever
suggestions, including "transfer"?

Tobias

On 18/02/2025 10:24, Jan van Brügge wrote:

Hi Tobias,

if you do declare [inductive_internals] before the definition of nullable,
the lfp definition will be available as "nullable_def"

Cheers,
Jan

Am 18.02.25 um 09:22 schrieb Tobias Nipkow:

I am trying to generate code from this inductive definition:

inductive nullable :: "(int * int list) list ⇒ int ⇒ bool"
for ps where
  "⟦ mem ps (A, w); ∀s ∈ set w. nullable ps s⟧
  ⟹ nullable ps A"

where mem is the auxiliary definition

inductive mem :: "'a list ⇒ 'a ⇒ bool" where
  "mem (x#xs) x" |
  "mem xs y ⟹ mem (x#xs) y"

(I thought List.member does the job but that didn't work)

Back to nullable: this evaluation diverges:

values "{s. nullable [(1,[1, 0])] s}"

How can I fix this?

Alternatively, for my purposes it may be simpler to use the lfp-definition
of nullable. However, I can only find

HOL.nitpick_unfold(176):
nullable ≡ λps. lfp (λp x. ∃A w. x = A ∧ mem ps (A, w) ∧ (∀s∈set w. p s))

Is there no direct access to this def (not needing nitpick_unfold)? I seem
to remember it is hidden, but maybe there is a switch?

Tobias

smime.p7s

Last updated: Mar 09 2025 at 12:28 UTC