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
have added further comments.

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
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
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.