From: <kimmo.varpaaniemi@ko...>  20130120 09:39:07

Hello, See the theorem "thm_Wiki_trick" in the EventB context "Results" in the EventB project "PowersOfTwo" that is available in the archive http://sourceforge.net/p/rodinbsharp/bugs/_discuss/thread/8454803b/9bdc/attachment/PowersOfTwo.zip where all proof obligations have got discharged as indicated by the EventB 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 <htson@...> wrote: > > > Dear George, > > Here is the wiki page for an example of performing a proof by induction > > http://wiki.eventb.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@...<mailto: > > ggzaff@...>> > > wrote: > > > > Hi all, > > > > Im new to Rodin/eventb 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<http://ASP.NET>;, MVC, AJAX, Knockout.js, Web > > API and > > much more. Get web development skills now with LearnDevNow  > > 350+ hours of stepbystep video tutorials by Microsoft MVPs and experts. > > SALE $99.99 this month only  learn more at: > > > > http://p.sf.net/sfu/learnmore_122812_______________________________________________ > > Rodinbsharpuser mailing list > > Rodinbsharpuser@... > > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > > > > > >  > 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 stepbystep video tutorials by Microsoft > MVPs and experts. SALE $99.99 this month only  learn more at: > http://p.sf.net/sfu/learnmore_122912 > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 