## rodin-b-sharp-user

 Re: [Rodin-b-sharp-user] Induction in proof From: - 2013-01-20 09:39:07 ```Hello, See the theorem "thm_Wiki_trick" in the Event-B context "Results" in the Event-B project "PowersOfTwo" that is available in the archive http://sourceforge.net/p/rodin-b-sharp/bugs/_discuss/thread/8454803b/9bdc/attachment/PowersOfTwo.zip where all proof obligations have got discharged as indicated by the Event-B Explorer view in Rodin Platform. All items in the "Axioms" section are theorems indeed, so the proofs are at least as convincing as Rodin Platform. As indicated by the name of the project, the same section contains some theorems about powers of two. I created the project almost two years ago as a reaction to discussions where provability of such properties in Rodin Platform had been questioned. With best regards, Kimmo Varpaaniemi George Zaff [ggzaff@...] kirjoitti: > Thanks that is very helpful. > > I have another question relating to induction: Out of interest, I was > wondering whether it is possible to prove the axiom of induction on natural > numbers using Rodin? Ive looked at the proof on the Wikipedia article: > > https://en.wikipedia.org/wiki/Mathematical_induction#Proof_of_mathematical_induction > > However, I have been unable to carry out the proof in Rodin. > > > Thanks, > George > > > On Sat, Jan 19, 2013 at 12:38 AM, Hoang, Thai Son wrote: > > > Dear George, > > Here is the wiki page for an example of performing a proof by induction > > http://wiki.event-b.org/index.php/Induction_proof > > In your case, for proving axm18, you can instantiate s in axm11 with {a | > > a'fromNat(toNat(a))=a}. > > Cheers, > > Son > > On 18 Jan 2013, at 20:11, George Zaff > ggzaff@...>> > > wrote: > > > > Hi all, > > > > Im new to Rodin/event-b and have been exploring the interactive proof > > system. I found myself stuck while trying to apply induction. > > > > In the following, I define a set of natural numbers, mappings to/from this > > set into the builtin set of natural numbers and show that it defines the > > same set. However, when attempting to show that the mappings are > > isomorphic, axm18 and amx20 below, I am not sure how to proceed. Their > > proofs require the induction hypothesis. > > > > CONTEXT > > Nat : > > SETS > > Nat : > > CONSTANTS > > zero : > > suc : > > toNat : > > fromNat : > > S : > > AXIOMS > > axm1: zero  Nat not theorem : > > axm2: suc  Nat  Nat not theorem : > > axm3: toNat    Nat not theorem : > > axm4: toNat(0) = zero not theorem : > > axm5: n · n   Ò toNat(n + 1) = suc(toNat(n)) not theorem : > > axm6: toNat(1) = suc(zero) theorem : > > axm7: fromNat  Nat   not theorem : > > axm8: fromNat(zero) = 0 not theorem : > > axm9: n · n  Nat Ò fromNat(suc(n)) = fromNat(n) + 1 not > > theorem : > > axm10: fromNat(suc(zero)) = 1 theorem : > > axm11: s · s   ' 0  s ' ( n · n  s Ò n + 1  s) Ò   s > > not theorem : > > axm12: n · n   Ò n = 0 ( ( m · m   ' n = m + 1) theorem : > > axm13: S = { n # n   ' ( x · x  Nat ' n = fromNat(x)) } not > > theorem : > > axm14: S   theorem : > > axm15: 0  S theorem : > > axm16: s · s  S Ò s + 1  S theorem : > > axm17:   S theorem : > > axm18: n · n   Ò fromNat(toNat(n)) = n theorem : > > axm19: x · x  Nat Ò x = zero ( ( y · y  Nat ' x = suc(y)) > > not theorem : > > axm20: x · x  Nat Ò toNat(fromNat(x)) = x theorem : > > END > > > > > > A second small query I have is whether there is support for a type of all > > sets? E.g. it is possible to write something of the form: > > A , B , f , a , a' · A  SET ' B  SET ' f  A  B ' a  A ' a'  A ' a > > = a' Ò f(a) = f(a') > > > > Thanks, > > George > > > > ------------------------------------------------------------------------------ > > Master HTML5, CSS3, ASP.NET;, MVC, AJAX, Knockout.js, Web > > API and > > much more. Get web development skills now with LearnDevNow - > > 350+ hours of step-by-step video tutorials by Microsoft MVPs and experts. > > SALE \$99.99 this month only -- learn more at: > > > > http://p.sf.net/sfu/learnmore_122812_______________________________________________ > > Rodin-b-sharp-user mailing list > > Rodin-b-sharp-user@... > > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > > > > > > ------------------------------------------------------------------------------ > Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, > MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current > with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft > MVPs and experts. SALE \$99.99 this month only -- learn more at: > http://p.sf.net/sfu/learnmore_122912 > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > ```