theory intro_induction
imports Main
begin
thm nat.induct[of "P" "x"]
datatype my_nat = MyZero | MySuc nat
thm my_nat.induct
thm nat.induct (*library*)
(*example of notation*)
lemma "(2::nat)^4 = 16" by simp
(*3::nat zu sagen ist wichtig, damit alles als natÃ¼rlich zahl angenommen wird*)
(* typen anzeigen: declare[[show_types]]*)
lemma "\k::nat. 3^n - 1 = 2 * k"
apply(induction n)
apply(simp)
apply(simp)
(*try0 gibt presburger*)
by presburger
lemma "\k::nat. 3^n - 1 = 2 * k"
proof(induction n)
print_cases
case 0
have "(3::nat) ^ 0 - 1 = 2 * 0" by simp
from this show "\k::nat. 3 ^ 0 - 1 = 2 * k" by simp
next
case(Suc n)
--"Induction Hypothesis"
assume IH: "\k::nat. 3 ^ n - 1 = 2 * k"
have "(3::nat)^(Suc n) - 1 = 3*3^n - 1" by simp
also have "\ = (2+1)*3^n - 1" by simp
also have "\ = 2*3^n + 1*3^n - 1" by simp
also have "\ = 2*3^n + 3^n - 1" by simp
finally have fact1: "(3::nat)^(Suc n) - 1 = 2*3^n + 3^n - 1" by simp
from IH obtain k::nat where "3^n - 1 = 2*k" by blast
from this fact1 have "(3::nat)^(Suc n) - 1 = 2*3^n + 2*k" by simp
also have "\ = 2*(3^n + k)" by simp
finally have "(3::nat)^(Suc n) - 1 = 2*(3^n + k)" by simp
from this exI[where x="3^n + k"] have "\k'. (3::nat)^(Suc n) - 1 = 2*k'" by simp
from this show "\k::nat. 3 ^ (Suc n) - 1 = 2 * k" by simp
qed
fun find_fives :: "nat list \ nat list" where
"find_fives [] = []"
| "find_fives (x#xs) = (if x = 5 then 5 # find_fives xs else find_fives xs)"
lemma "find_fives l = [x\l . x = 5]"
proof(induction l)
case Nil
show "find_fives [] = [x\[] . x = 5]" by simp
next
case (Cons x xs)
assume IH: "find_fives xs = [x\xs . x = 5]"
from IH show "find_fives (x # xs) = [x\x # xs . x = 5]" by(simp)
qed
end