Hello Sir,
I am trying to write the sigma_sets definition in isabelle. I tried
Hol_reln as following.
Hol_reln `(!sp st. {} IN sigma_sets sp st) /\
(!sp st a. a IN st ==> a IN sigma_sets sp st) /\
(!sp st a. a IN sigma_sets sp st ==> sp DIFF a IN sigma_sets sp st) /\
(!sp st A i. (A:num->'a->bool) i IN sigma_sets sp st ==>
BIGUNION {A i | i IN UNIV} IN sigma_sets sp st)`;
and it gives me unification failure. I guess it is different.
Regards
Qasim
Quoting Ramana Kumar <ram...@member.fsf.org>:
> Is this something different from what Hol_reln will give you?
>
> On Tue, Mar 10, 2015 at 6:33 PM, Muhammad Qasim <m_q...@encs.concordia.ca>
> wrote:
>
>> Hello Everyone,
>>
>> I saw an inductive_set definition in Isabelle. Is there a way to do
>> such definitions in HOL4?
>>
>> Thank you.
>>
>> Regards
>>
>> Qasim
>>
>>
>>
>> ------------------------------------------------------------------------------
>> Dive into the World of Parallel Programming The Go Parallel Website,
>> sponsored
>> by Intel and developed in partnership with Slashdot Media, is your hub for
>> all
>> things parallel software development, from weekly thought leadership blogs
>> to
>> news, videos, case studies, tutorials and more. Take a look and join the
>> conversation now. http://goparallel.sourceforge.net/
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
