Email Gateway (Aug 22 2022 at 15:35): Email Gateway (Aug 22 2022 at 15:35):From: "Ali A. Noroozi" <aliasghar.noroozi@gmail.com>
Dear all,
I am trying to define valid quadruple ⊨ {P}c×c'{Q} of Hoare logic in
Isabelle/HOL, where c and c' are commands and P and Q are assertions.
Assertions are defined as :
type_synonym assn = "state × state ⇒ bool"
I have defined the valid quadruple as following:
definition
rel_hoare_valid :: "assn ⇒ com × com ⇒ assn ⇒ bool" ("⊨ {(1_)}/ (_)/
{(1_)}" 50)
where "⊨ {P}c×c'{Q} = ..."
... contains rest of the code, which is not relevant.
I know that the syntax annotation part
("⊨ {(1_)}/ (_)/ {(1_)}" 50)
is not correct, but I don't know how to fix it.
The error message is as following:
Type unification failed: Clash of types "_ set" and "_ × _"
Type error in application: incompatible operand type
Operator: rel_hoare_valid P :: com × com ⇒ ((char list ⇒ int) × (char
list ⇒ int) ⇒ bool) ⇒ bool
Operand: c × c' :: (??'a × ??'b) set
Can anyone help me correct the definition?
Email Gateway (Aug 22 2022 at 15:35):From: Tobias Nipkow <nipkow@in.tum.de>
It seems to me that your problem is the syntax for pairs: pairs are written
(c,c') not c×c'. The infix operator × produces the croos-product of two sets.
Tobias
smime.p7s
Last updated: Apr 19 2024 at 20:15 UTC