From: Alexei I. <ale...@nc...> - 2011-03-16 21:02:27
|
Hi all, Regarding cardinality, may I suggest adding the following interactive rule: ∀ a, b · a ∈ ℙ(ℕ) ∧ b ⊆ a ∧ finite(a) ⇒ card(a ∖ b) = card(a) − card(b) This is a statement via which few other useful cardinality-related properties may be discharged. Regards, Alexei > -----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----- > > ------------------------------------------------------------------------------ > Colocation vs. Managed Hosting > A question and answer guide to determining the best fit > for your organization - today and in the future. > http://p.sf.net/sfu/internap-sfd2d > _______________________________________________ > Rodin-b-sharp-user mailing list > Rod...@li... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user |