Hi Christian, > by the way, I noticed that sometimes [to_pred] yields undesirable > results (containing case-expressions), e.g., > > thm trancl_power[to_pred] > > results in > > (case ?p of (x, xa) ⇒ ?R^++ x xa) = > (∃n>0. case ?p of (x, xa) ⇒ (?R ^^ n) x xa) > > is this an inherent problem or could this be "repaired" by adding > appropriate [pred_set_conv] (I do not know how this workds in detail).
I do not know whether this is inherent (Stefan could know).
There are (at least) two solutions:
* [unfold prod_case_unfold]
* [of "(a, b)", unfold <some suitable rule>]
Note that internally prod_case is also used as »uncurry« combinator.
Hope this helps,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
