Stream: Beginner Questions

Topic: Defining the range in a locale based on a record

Atie Bastan (Dec 06 2024 at 05:10):

Hi all,

I am using the combination of record and locale to prove some lemmas. To do so, I have a record with a field that maps (nat x 'a x 'b) => (nat x 'b), let's call it next, and another field that keeps track of all the inserted ('b)s in another field as a ('b list), let's call it List.
My problem is in the locale when I am trying to define the range of next. I tried different combinations for it, for example, set (nat set A x set (List A)). But Isabelle finds my definition a clash of types and says:

Type unification failed: Clash of types "_ set" and "_ list"

Type error in application: incompatible operand type

I borrowed this use of record and locale from :
https://www.isa-afp.org/sessions/finite_automata_hf/#Finite_Automata_HF.html#Finite_Automata_HF.nfa_def|fact

Mathias Fleury (Dec 06 2024 at 05:56):

My crystal ball says that you are using your List field wrong, sometimes a list and sometimes as a set. Isabelle does not allow mixing

Mathias Fleury (Dec 06 2024 at 05:57):

(x ∈ set (List q), not x ∈ List q)

Mathias Fleury (Dec 06 2024 at 05:58):

But: without code, without any precise information, how do you expect any help?

Atie Bastan (Dec 06 2024 at 06:02):

You are right. This is the whole thing:

record ('a, 'b) pda =
                states :: "nat set"
                init   :: "nat set"
                final  :: "nat set"
                nxt    :: "nat ⇒ 'a ⇒ 'b ⇒ (nat × 'b list) set"
                eps    :: "(nat × nat) set"
                stack  :: "'b list"


locale pda =
  fixes P :: "('a, 'b) pda"
  assumes init: "init P ⊆ states P"
      and final: "final P ⊆ states P"
      and nxt:   "⋀q a b. q ∈ states P ⟹ ((nxt P) q a b) ⊆ set (states P × set (stack P))"
      and finite: "finite (states P)"

Mathias Fleury (Dec 06 2024 at 06:05):

As the error message, you nxt statement does not type

Mathias Fleury (Dec 06 2024 at 06:07):

Is this what you want?

locale pda =
  fixes P :: "('a, 'b) pda"
  assumes init: "init P ⊆ states P"
      and final: "final P ⊆ states P"
      and nxt:   "⋀q a b. q ∈ states P ⟹ fst ` ((nxt P) q a b) ⊆  (states P)"
      and nxt':   "⋀q a b. q ∈ states P ⟹ q' ∈ snd ` ((nxt P) q a b) ⟹ set q' ⊆ set (stack P)"
      and finite: "finite (states P)"

Atie Bastan (Dec 06 2024 at 16:28):

Thank you.

Atie Bastan (Dec 10 2024 at 02:44):

Mathias Fleury said:

As the error message, you nxt statement does not type

I want to check my understanding here: nxt doesn't have a type of its own, and whenever I want to construct/define something based on it, I need to decompose it into its first and second elements and define them appropriately.

Is this correct?

Mathias Fleury (Dec 10 2024 at 05:47):

nxt has a type: nxt :: "nat ⇒ 'a ⇒ 'b ⇒ (nat × 'b list) set"

Mathias Fleury (Dec 10 2024 at 05:48):

and your assumptions must be typable w.r.t. that type

Mathias Fleury (Dec 10 2024 at 05:48):

and ((nxt P) q a b) ⊆ set (states P × set (stack P)) does not do it, because ⊆ does not type in the expression

Mathias Fleury (Dec 10 2024 at 05:51):

So I tried to guess what you are trying to write: you want the ⊆ to apply pointwise in the pair. This is not a usage of ⊆ that is possible in Isabelle (and not a usage I have never heard in math either). Hence I split the pair.

Mathias Fleury (Dec 10 2024 at 05:52):

But, splitting is not needed. It is just needed here because the operator you would need does not exist, but you could also define a pairwise subset and use that instead

Atie Bastan (Dec 11 2024 at 05:05):

thank you.

Last updated: Dec 21 2024 at 16:20 UTC