*To*: cl-isabelle-users at lists.cam.ac.uk, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] problem with class and sulocale declarations*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Wed, 08 Sep 2010 15:16:28 +0300*In-reply-to*: <4C8776A9.1060204@informatik.tu-muenchen.de>*References*: <4C873677.6010001@abo.fi> <4C873BA2.6030603@informatik.tu-muenchen.de> <4C874E4B.5090207@abo.fi> <4C8776A9.1060204@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.8) Gecko/20100802 Thunderbird/3.1.2

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

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 did not know how to replace y with 1. The second application of subst will change again 1 to 1. Best regards, Viorel

**Follow-Ups**:**Re: [isabelle] problem with class and sulocale declarations***From:*Florian Haftmann

**References**:**[isabelle] problem with class and sulocale declarations***From:*Viorel Preoteasa

**Re: [isabelle] problem with class and sulocale declarations***From:*Florian Haftmann

**Re: [isabelle] problem with class and sulocale declarations***From:*Viorel Preoteasa

**Re: [isabelle] problem with class and sulocale declarations***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] problem with class and sulocale declarations
- Next by Date: Re: [isabelle] problem with class and sulocale declarations
- Previous by Thread: Re: [isabelle] problem with class and sulocale declarations
- Next by Thread: Re: [isabelle] problem with class and sulocale declarations
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list