Re: [isabelle] axiomatization



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






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