Up to index of Isabelle/HOL/IsarTut

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