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