Email Gateway (Aug 18 2022 at 19:36): Email Gateway (Aug 18 2022 at 19:36):From: John Wickerson <jpw48@cam.ac.uk>
Hello Isabelle,
As part of a little separation logic theory I'm working on, I have the following axiomatisation of a star operator:
axiomatization
Star :: "assertion => assertion => assertion"
where star_comm: "Star p q = Star q p"
and star_assoc: "Star (Star p q) r = Star p (Star q r)"
and star_emp: "Star p Emp = p"
and emp_star: "Star Emp p = p"
I would now like to add a couple more properties of "star", such as:
and dist_conj: "Star p (Conj q r) ≤ Conj (Star p q) (Star p r)"
However, before I can use "≤" to compare assertions, I need "assertion :: order". I don't want to prove this (by giving a concrete definition for ≤), instead I want simply to assume this. How is this done?
Many thanks,
John
Email Gateway (Aug 18 2022 at 19:36):From: John Wickerson <jpw48@cam.ac.uk>
Ah, I worked it out. I replaced
typedecl assertion
with
typedecl assertion
arities assertion :: "order"
which seems to do the trick.
John
On 25 Apr 2012, at 13:51, John Wickerson wrote:
Hello Isabelle,
As part of a little separation logic theory I'm working on, I have the following axiomatisation of a star operator:
axiomatization
Star :: "assertion => assertion => assertion"
where star_comm: "Star p q = Star q p"
and star_assoc: "Star (Star p q) r = Star p (Star q r)"
and star_emp: "Star p Emp = p"
and emp_star: "Star Emp p = p"I would now like to add a couple more properties of "star", such as:
and dist_conj: "Star p (Conj q r) ≤ Conj (Star p q) (Star p r)"
However, before I can use "≤" to compare assertions, I need "assertion :: order". I don't want to prove this (by giving a concrete definition for ≤), instead I want simply to assume this. How is this done?
Many thanks,
John
Last updated: Apr 24 2024 at 16:18 UTC