[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.