Atie Bastan (Dec 06 2024 at 05:10): 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)"
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)"
Thank you.
Atie Bastan (Dec 10 2024 at 02:44):Mathias Fleury said:
As the error message, you
nxtstatement 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: Nov 04 2025 at 08:30 UTC