[isabelle] axiomatization



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.