Re: [isabelle] Finite product simplification



Lets assume we have a cong rule of the form:

  [| A = B ; !!x. x : B =simp=> f x = g x |] ==> OP A f = OP B g

The =simp=> tells the simplifier to simplify x : B before it is used.
When ==>
is used this does not happen. 
 
Recently there was a discussion about the usage of =simp=> = :

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00069.html
 

 - Johannes

Am Dienstag, den 26.08.2014, 10:43 +0100 schrieb Holden Lee:
> Thanks, this works - what's the difference between ==> and =simp=>?
> 
> 
> -Holden
> 
> 
> 
> 2014-08-26 9:46 GMT+01:00 Johannes Hölzl <hoelzl at in.tum.de>:
>         I'm not sure but you might try an even stronger form of your
>         cong rule:
>         
>         lemma (in comm_monoid) finprod_cong2':
>           "[| A = B; !!i. i ∈ B =simp=> f i = g i ; g ∈ B -> carrier
>         G|] ==>
>            finprod G f A = finprod G g B"
>         
>         
>         then i : {x. P x /\ Q x} is rewritten into P i /\ Q i when
>         applying the
>         congruence rule.
>         
>         I don't know what simp_if is but I don't think you need
>         if_splits and
>         simp_if.
>         
>          - Johannes
>         
>         Am Donnerstag, den 21.08.2014, 10:14 +0100 schrieb Holden Lee:
>         > I need to be able to do something like this automatically:
>         >
>         > lemma (in comm_monoid) finprod_exp:
>         >   "⟦A={x. P x ∧ Q x}; finite A; a∈A→carrier G⟧⟹finprod G
>         (λx. if P x then
>         >     a x else b x) A = finprod G a A"
>         > using[[simp_trace, simp_trace_depth_limit=10]]
>         > apply (auto cong: finprod_cong2' simp add:simp_if
>         split:if_splits)
>         >
>         > Looking at the simp trace, it appears to fail during the
>         congruence, when
>         > it fails to show "a∈A→carrier G" even when this was given as
>         a hypothesis.
>         > (Note that apply (intro finprod_cong2') apply (auto...)
>         works, but this is
>         > not good enough for applications because simp doesn't call
>         intro.)
>         >
>         > Here finprod_cong2' is just finprod_cong' in a different
>         (hopefully better)
>         > order:
>         >
>         > lemma (in comm_monoid) finprod_cong2':
>         >   "[| A = B;
>         >       !!i. i ∈ B ==> f i = g i ; g ∈ B -> carrier G|] ==>
>         finprod G f A =
>         > finprod G g B"
>         >  apply (auto cong: finprod_cong')
>         > done
>         >
>         > What gives?
>         >
>         > Thanks,
>         > Holden
>         
>         
>         
> 
> 






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