Re: [PVS-Help] rewriting add_as_union

["Jerry James" <loganjerry@xxxxxxxxx>]

On Thu, May 8, 2008 at 5:58 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
> I'm trying to use the rewrite rule to get the following ([1]) to
> simplify:
>
>  [-1]  disjoint?(singleton(e!1), L!1)
>    |-------
>  [1]   fun(s!1, (union(singleton(e!1), L!1))) = s!1(e!1) o fun(s!1, L!1)
>
>  Rule? (rewrite "add_as_union" :dir RL)
>  No matching instance for add_as_union found.
>  No change on: (REWRITE "add_as_union" :DIR RL)
>  disjoint_compose.1 :
>
>  [-1]  disjoint?(singleton(e!1), L!1)
>    |-------
>  [1]   fun(s!1, (union(singleton(e!1), L!1))) = s!1(e!1) o fun(s!1, L!1)
>
> where 'add_as_union' is defined in the prelude to be:
>
>  add(x, a) = union(a, singleton(x))
>
> Is this problem due to the fact that the singleton and set definitions
> in my consequent are opposite to those in prelude? Is there anyway to
> use rewrite (or even rewrite-lemma) to get this to work? Thanks

Does rewriting with union_commutative help?
-- 
Jerry James
http://loganjerry.googlepages.com/