Re: [isabelle] Problem with unfolding definitions while instantiating class



Hello Dave,


thanks for the information! I was suspecting this, but was not sure.

Is there any way to re-define Sup_fun for ccpos?
When there is no definition at all, I am asked to give a definition (e.g.
when I instantiate Sup with nat). I would like to override definitions in
the same way.

And is it just me not understanding the type classes or overloading, or is
it really strange that definitions of one type class use definitions of
another (stronger!) type class?

I would also be grateful for explanations why it doesn't work, or why I am
trying in a wrong direction.


Thanks in advance
Nils




2014-06-06 0:10 GMT+02:00 David Cock <davec at cse.unsw.edu.au>:

> Nils,
>   Your problem in the first instance is that Sup_fun is only defined where
> the result type is a complete lattice.  Try:
>
> declare [[show_sorts = true]]
> thm Sup_fun_def
>
> Sup_fun_def won't unfold, as you're assuming that the result type is in
> class ccpo, not complete_lattice.  This is a bit of a nuisance, as the
> definition of Sup_fun only really needs the result type to be in class Sup.
>
> Dave
>
>
> On 05/06/14 00:40, Nils Jähnig wrote:
>
>> Dear Isabelle Users,
>>
>>
>> I am trying to instantiate a class, and can not see how to unfold the
>> predefined fixed definitions.
>> My question is: how do I figure out the right rules or definition names?
>>
>>
>> I'll use two example to explain:
>>
>> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>> -
>> - - - - -
>>
>> Example 1
>>
>> theory fun_ccpo
>> imports Complete_Partial_Order
>> begin
>>
>> instantiation "fun" :: (type, ccpo) ccpo
>> begin
>> instance
>> apply(intro_classes)
>> (* First subgoal:
>>   1. ⋀A x. chain op ≤ A ⟹ x ∈ A ⟹ x ≤ ⨆A
>>   *)
>> (* I found those two definition and can unfold them*)
>> apply(unfold chain_def)[]
>> apply(unfold le_fun_def)[]
>> (* but I am not able to find the right Sup definition
>> neither do I know how to overwrite the Sup definition *)
>> thm Sup_fun_def
>> (* Those don't work *)
>> apply(unfold Sup_fun_def)
>> apply(simp add: Sup_fun_def)
>> sorry
>>
>> end
>> end
>>
>>
>> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>> -
>> - - - - -
>> Example 2, uses HOLCF
>>
>> theory fun_pcpo
>> imports Fun_Cpo
>> begin
>>
>> datatype nat_bot = N nat | Bot
>>
>> instantiation nat_bot :: pcpo
>> begin
>> definition "below_nat_bot a b == a=b ∨ a=Bot"
>> instance
>> apply(default)
>> apply(unfold below_nat_bot_def, simp)[]
>> apply(unfold below_nat_bot_def, auto)[]
>> apply(unfold below_nat_bot_def, auto)[]
>> (* First Subgoal
>>   1. ⋀S. chain S ⟹ ∃x. range S <<| x
>> *)
>> (* How do i unfold chain, range and <<| *)
>> thm chain_def
>> thm is_lub_def
>> sorry
>>
>> end
>> end
>> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>> -
>> - - - - -
>>
>>
>> Thanks for any help
>> Nils
>>
>>
>
>



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