CODEWITHSUNDEEP
functiontypespartialisabelleproof
Montserrat Hermo
Montserrat Hermo

Reputation: 71

I have a problem in Isabelle related to 'Clash of types' that I am unable to solve. Could someone help me?

I would want to formalise a calculus in Isabelle. I started with this definitions:

type_synonym Signature = "string ⇀ nat"

type_synonym 'a Interpretation = "string ⇀ 'a list set"

datatype 'a Structure = Structure "Signature" "'a set" "'a Interpretation"

fun getNat :: "'a Structure ⇒ string ⇒ nat option" where "getNat (Structure sig _ _) w = sig w"

fun getModels :: "'a Structure ⇒ string ⇒ 'a list set option" where "getModels (Structure _ _ models) w = models w"

fun getDomain :: "'a Structure ⇒ 'a set" where "getDomain (Structure _ relations _) = relations"

I realised the functions need the types 'nat option' and 'set option'. I think this is because 'Signature' and 'Interpretation' are partial functions. However, when I try to define the next function, there is a problem that I cannot fix.

fun wfStructure :: "'a Structure  ⇒ bool " where 
"wfStructure Structure sig relations models = 
( 
    relations ≠ {} ) ∧ 
    (∀r. r ∈ dom(sig) ⟶ ( r ∈ dom(models)  ∧ 
                            (∀t. t ∈ (models r) ⟶ length(t) = (sig r)
                          )
    )
)"

Upvotes: 1

Views: 42

Answers (0)

Related Questions