# Re: [isabelle] learning isabelle

```Hi Ruben,

> I'm still learning Isabelle. I'm trying to prove the lemma named
> "my_lemma" at the bottom of this file but can't. If someone could give
> me a hint that would be great.

The issue is that you have first to do induction and then case
distinction on the induction variable.  See attached theory, to which I

Hope this helps
Florian

--

PGP available:
http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de.pgp
```
```theory Fac
imports Main
begin

primrec factorial :: "nat \<Rightarrow> nat" where
-- "observe new primrec syntax"
"factorial 0 = 1"
| "factorial (Suc n) = (Suc n) * (factorial n)"

lemma positive_factorial [simp]: "factorial n \<ge> Suc 0"
-- {*
1 bad on lhs of simp rule, since 1 unfolds to Suc 0
under simplification by default
*}
apply (induct n)
apply auto
done

lemma [simp]: "\<forall> n. n > (0::nat) \<Longrightarrow> n \<le> factorial n"
-- {*
This is not what you probably have meant: it says
"if all natural numbers are greater than 0, then n is less or
equal factorial n" -- of course thats trivially true.
*}
apply auto
done

lemma my_lemma [simp]: "n \<le> factorial n"
proof (induct n)
case 0 then show ?case by simp
next
case (Suc n) then show ?case by (cases n) simp_all
qed

-- "in apply style"
lemma my_lemma' [simp]: "n \<le> factorial n"
apply (induct n)
apply simp
apply (case_tac n)
apply auto
done
```
```begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:289 - 17300
note;quoted-printable:PGP available: =
=0D=0A=
http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
nformatik_tu_muenchen_de.pgp=0D=0A=

x-mozilla-html:FALSE
url:http://www4.in.tum.de/~haftmann
version:2.1
end:vcard

```

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.