Theory BasicTypes

Up to index of Isabelle/HOL/IsarTut

theory BasicTypes = Main:
theory BasicTypes = Main:

text {* Beginning section 2.5. *}

consts sum:: "nat => nat"
primrec
"sum 0 = 0"
"sum (Suc n) = Suc n + sum n"

lemma "sum n + sum n = n*(Suc n)" by (induct n, auto)

text {* Hey, that wasn't so bad!

Hmm, here comes one written as a rule. *}

lemma "[| ~ m<n ; m < n+1 |] ==> m = n" by auto

lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))" by arith

text {* Wow, arith had to think about that for a while.
I would too: I'm not even sure what it means. *}

lemma "n*n = n --> n=0 | n=1" (is "?P n --> ?Q n" is "?R n")
proof (induct n)
  show "?R 0" by simp
  fix n assume "?R n" show "?R (Suc n)" by (cases n, auto)
qed

text {* This seems to answer the question of how you handle
proving an implication by showing that the premis is false
in some cases and the conclusion true in others.  Get it down
to the cases and let auto deal with the inference rules. *}

end


  
  






lemma

  sum n + sum n = n * Suc n

lemma

  [| ¬ m < n; m < n + 1 |] ==> m = n

lemma

  min i (max j (k * k)) = max (min (k * k) i) (min i j)

lemma

  n * n = n --> n = 0 | n = 1