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



On 06/06/2014 11:15, Nils Jähnig wrote:
> 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.

This is not possible. As Dave pointed out, the problem goes away if in Main the
instantiation of "fun" on class complete_lattice is done in stages, where in a
first step one merely instantiates Sup and Inf.

@ Florian: any objections to that?

> 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?

What do you mean?

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

As Dave said, it is not your fault, the setup in Main is not fine-grained
enough. You can modify Complete_Lattice as follows to make it work, but your
theories will no longer work with the distribution: replace the block

instantiation "fun" :: (type, complete_lattice) complete_lattice
...
end

by the following:

instantiation "fun" :: (type, Inf) Inf
begin

definition
  "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"

lemma Inf_apply [simp, code]:
  "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
  by (simp add: Inf_fun_def)

instance ..

end

instantiation "fun" :: (type, Sup) Sup
begin

definition
  "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"

lemma Sup_apply [simp, code]:
  "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
  by (simp add: Sup_fun_def)

instance ..

end

instantiation "fun" :: (type, complete_lattice) complete_lattice
begin

instance proof
qed (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)

end

Tobias

PS Do not import individual theories that are part of Main (like
Complete_Partial_Order), start from Main instead. Otherwise you get some
fragment of Main with unpredictable behaviour.

> 
> 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.