Re: [isabelle] problem with class and sulocale declarations
I managed to go forward using bot instead of zero. This is a good
solution for me.
sublocale test< testlattice!: lattice "op ≤" "op<" "op ⊓1" "op ⊔1"
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 tried apply (subst a), but when using on "x = y" it only replace x to
2. Why the proof for the above sublocale fails if I remove assumption b
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 did not know how to replace y with 1. The second application of subst will
change again 1 to 1.
This archive was generated by a fusion of
Pipermail (Mailman edition) and