Re: [isabelle] problem with class and sulocale declarations



Hi Viorel,

sorry for that problem.  Its technical source is rather obscure (c.f.
http://isabelle.in.tum.de/repos/isabelle/rev/95a41e6ef5a8).  Until the
next Isabelle release however we somehow have to live with it.  Since an
explicit annotation fails in your example, I would suggest an auxiliary
class with zero and one:

> class sup_a =
>   fixes sup_a :: "'a => 'a => 'a" (infixl "⊔1" 65)
> 
> class inf_a =
>   fixes inf_a :: "'a => 'a => 'a" (infixl "⊓1" 65)
> 
> class test = ord + times + one + sup_a + inf_a +
>   assumes a[simp]: "a = 1"
>   and b[simp]:"a = b"
>   and [simp]: "a ≤ b"
>   and [simp]: "¬ a < b"
> begin
> end
> 
> sublocale test <  testlattice!: lattice "op ≤" "op <" "op ⊓1" "op ⊔1"
>   apply unfold_locales
>   by simp_all
> 
> class zero_one = zero + one
> 
> class bounded = zero_one + test

The obscure problem is likely to occur if classes are combined with
different parameters which are not mentioned in the body of the class
declaration, e.g. by assume.

> 1. Why squnion and sqinter symbols are not defined in separate classes
> as most of the other symbols? This would make there reuse simpler.

The point is that inf and sup carry *no* syntax by default, so you are
free to use squnion and sqinter in syntax as you like; only by importing
Lattice_Syntax from the library this gets attached to inf and sup.

> 2. Why the proof for the above sublocale fails if I remove assumption b
> from test?
> assumption a should replace any element with 1.

a is not applied by the simplifier since it would loop: "a = 1 = 1 = 1 =
...".  You can apply it manually e.g. using apply (subst a).


Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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