Re: [isabelle] Finite product simplification



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.