From: Matthias S. <Mat...@in...> - 2011-03-16 20:51:06
|
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Hi again, my personal impression is that support for card (question 1, 2, and 4) and for non-linear arithmetic (question 3) is poor. Therefore I tend to avoid them. But this is just my impression, and maybe somebody on the list can help you better than me. If you have to use card or non-linear arithmetic, you can search the wiki for available rules: http://wiki.event-b.org/index.php/All_Rewrite_Rules http://wiki.event-b.org/index.php/Inference_Rules The AtelierB provers can also prove some facts about them, but it is hard to predict which ones. If my students are frustrated because of such issues, I allow them to introduce axioms. (I insist on reviewing their axioms.) Or course, as already pointed out on some other mailing list: axioms are evil. - -Matthias Joachim Breitner schrieb: > Hello, > > I have progressed sufficiently far with my Rodin project and now want to > proof termination. My variant involves multiplication (to simulate a > lexicographic ordering) and cardinality – both areas where Rodin does > not seem to be very strong. For example, I am not able to proof this > obligation (which is simple transitivity of < with <=): > > hyps: finite(ran(fan)) >  finite(V) >  card(V)≤card(V)∗(1+card(V) − card(ran(fan))) >  0<card(V) > goal: 0<card(V)∗(1+card(V) − card(ran(fan))) > > This is part of a work-around to hopefully be able to prove this – maybe > it is possible to obtain it directly? > >  0≤card(V) − card(ran(fan)) >  0<card(V) > goal: 0<card(V)∗(1+card(V) − card(ran(fan))) > > > I am basically looking for rules such as > A * C < B * C <=> A < B (if C > 0) > and > 0 < A & 0 < B ==> 0 < A * B > > > And while I am at it, is there a way to reason about cardinality of > images and domains of total and injective functions? Things like > f : A --> B ==> card(ran(f)) <= card(dom(f)) > and f : A >+> B ==> card(ran(f)) = card(dom(f)) > > I had to add an axiom to my context stating something that would follow > from the other axioms if I could express this in Rodin. > > Thanks in advance, > Joachim > > > -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFNgSKxczhznXSdWggRAtQuAJsF+cdehbO9s3o3WXsgD7UWaPud2gCfd7B5 OWla/QeMc2cCwJ7vrwuWEfg= =4qfS -----END PGP SIGNATURE----- |