Re: [isabelle] Apply rule: unexpected behaviour



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
>                 >
> 
> 






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