# [isabelle] learning isabelle

Hi,

`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.
`
Regards,
Ruben
(* Title: Stuff.thy
Author: Ruben Zilibowitz
2008
*)
header {* Stuff *}
theory Stuff imports Main begin
consts
factorial :: "nat \<Rightarrow> nat"
primrec
"factorial 0 = 1"
"factorial (Suc n) = (Suc n) * (factorial n)"
lemma positive_factorial [simp]: "factorial n \<ge> 1"
apply (induct_tac n)
apply auto
done
lemma [simp]: "factorial n \<le> factorial (n+1)"
apply (induct_tac n)
apply auto
done

`lemma [simp]: "\<forall> n. n > (0::nat) \<Longrightarrow> n \<le>
``factorial n"
` apply (induct_tac n)
apply auto
done
lemma [simp]: "n = 0 \<Longrightarrow> n \<le> factorial n" by simp
lemma my_lemma [simp]: "n \<le> factorial n"
apply (case_tac n)
apply auto
done
end

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