*To*: Diego Machado Dias <diegodias.m at gmail.com>*Subject*: Re: [isabelle] Apply rule: unexpected behaviour*From*: Peter Lammich <lammich at in.tum.de>*Date*: Mon, 14 Mar 2016 18:12:00 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAJA562uZPoRQ7gxsMDTKXCGD9Ua-HTa7dbDpwH+LaitvJVCd8w@mail.gmail.com>*References*: <56e5e182.4118c20a.67e02.0cc3SMTPIN_ADDED_MISSING@mx.google.com> <CAJA562uZPoRQ7gxsMDTKXCGD9Ua-HTa7dbDpwH+LaitvJVCd8w@mail.gmail.com>

Hi Diego, it's quite obvious what happened here: look at the theorem: thm Law_Frame_Monotonic_Refinement ?c â[?r] ?d â ?Yâ:?c â[?r] ?Yâ:?d it requires exactly (syntactically) the same ?Y on both sides. However, contrary to your comment in the theory file, the actual subgoal looks like: ({''oc''} â {''ot''})â:(ârâeâlây ?rx3 â â[true,trueâ] [idrel]) â[true] {''oc'', ''ot''}â:(ârâeâlây true â â[true,trueâ] [idrel]) Note the subtle difference between {''oc''} â {''ot''} and {''oc'', ''ot''}. The simp-call rewrites the {_}\<union>{_} to {_,_}, and then the rule works. Hope this helps, Peter p.s.: Isabelle sees {a,b} as "insert a (insert b {})", while it sees {a} \union {b} as "sup (insert a {}) (insert b {})". These are semantically equal, but cannot be unified syntactically. On Mo, 2016-03-14 at 14:28 +0000, Diego Machado Dias wrote: > Peter, > > > > > I didn't manage to reproduce the problem in a smaller theory. I am > sending you > a more accurate description of the context where the problem happens. > I hope > that clarifies the issue. > > > I am working around the problem using > > > apply (simp only: Un_insert_left sup_bot.left_neutral) > > > > Before applying the rule I want. The proof step above causes no > visible change > to the goal, but it makes it possible to apply the desired law. > > > Thanks for your help! > > > Diego Dias > > > > > > Regards, > Diego > > On 13 March 2016 at 21:54, Peter Lammich <lammich at in.tum.de> wrote: > Hi Diego > > > Can you post a small example to reproduce this behavior? > > Peter > > > -------- Originalnachricht -------- > Betreff: Re: [isabelle] Apply rule: unexpected behaviour > Von: Diego Machado Dias > An: hupel at in.tum.de > Cc: cl-isabelle-users at lists.cam.ac.uk > > > Hi Lars, > > The clash information I get is this: > "Lattices.sup_class.sup =/= > Set.insert". > > It understood that it has to do with the usage of > sets, but I will need to > find out > how this message can help me. Does this clash message > ring a bell for you? > > > Thanks for you help! > Diego > > > On 13 March 2016 at 18:59, Lars Hupel wrote: > > > Hi Diego, > > > > > Is there any way of extracting more information > from Isabelle about the > > > reason that causes the application of a rule to > fail? > > > > try this: > > > > using [[unify_trace_failure]] > > apply (rule ...) > > > > Then, you'll find the output like the following: > > > > Clash: Scratch.P =/= Scratch.Q > > > > Hope that helps. > > > > Cheers > > Lars > > > >

- Previous by Date: Re: [isabelle] Apply rule: unexpected behaviour
- Next by Date: [isabelle] isar-ref: simpset ~> Proof.context
- Previous by Thread: Re: [isabelle] Apply rule: unexpected behaviour
- Next by Thread: [isabelle] isar-ref: simpset ~> Proof.context
- Cl-isabelle-users March 2016 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