Re: [isabelle] problem with class and sulocale declarations

 Hi Florian,

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.
I managed to go forward using bot instead of zero. This is a good solution for me.

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).
I tried apply (subst a), but when using on "x = y" it only replace x to 1, and
I did not know how to replace y with 1. The second application of subst will
change again 1 to 1.

Best regards,


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