From: George Zaff <ggzaff@gm...>  20130118 19:11:30
Attachments:
Message as HTML

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 
From: Hoang, Thai Son <htson@in...>  20130119 00:38:18

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 
From: George Zaff <ggzaff@gm...>  20130119 16:42:30
Attachments:
Message as HTML

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 > > 
From: Hoang, Thai Son <htson@in...>  20130121 09:53:01
Attachments:
Induction0.zip

Dear George, Attached is a development where I mimic the proof of induction. If you have any problem with the proving interface of Rodin, the following page from the Rodin Handbook will be quite useful. http://handbook.eventb.org/current/html/proving_perspective.html Cheers, Son On 19 Jan 2013, at 17:42, George Zaff <ggzaff@...<mailto:ggzaff@...>> wrote: 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. 