theory MyFirst

imports Main

begin

datatype 'a list = Nil | Cons 'a "'a list"

fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

"app Nil ys = ys" |

"app (Cons x xs) ys = Cons x (app xs ys)"

fun rev :: "'a list \<Rightarrow> 'a list" where

"rev Nil = Nil" |

"rev (Cons x xs) = app (rev xs) (Cons x Nil)"

value "rev(Cons True (Cons False Nil))"

value "1 + (2::nat)"

value "1 + (2::int)"

value "1 - (2::nat)"

value "1 - (2::int)"

lemma app_Nil2 [simp]: "app xs Nil = xs"

apply(induction xs)

apply(auto)

done

lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"

apply(induction xs)

apply(auto)

done

lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"

apply (induction xs)

apply (auto)

done

theorem rev_rev [simp]: "rev(rev xs) = xs"

apply (induction xs)

apply (auto)

done

fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

"add 0 n = n" |

"add (Suc m) n = Suc(add m n)"

lemma add_02: "add m 0 = m"

apply(induction m)

apply(auto)

done

(**commutative-associative**)

lemma add_04: "add m (add n k) = add (add m n) k"

apply(induct m)

apply(simp_all)

done

lemma add_zero: "add n 0 = n"

lemma add_Suc: "add m (Suc n) = Suc (add m n)"

lemma add_comm: "add m n = add n m"

apply(induct m)

apply(simp add: add_zero)

apply(simp add: add_Suc)

done

lemma add_odd: "add m (add n k) = add k (add m n)"

apply(subst add_04)

apply(subst (2) add_comm)

apply(simp)

done

fun dub :: "nat \<Rightarrow> nat" where

"dub 0 = 0" |

"dub m = add m m"

lemma dub_01: "dub 0 = 0"

apply(induct)

apply(auto)

done

lemma dub_02: "dub m = add m m"

apply(induction m)

apply(auto)

done

value "dub 2"

fun trip :: "nat \<Rightarrow> nat" where

"trip 0 = 0" |

"trip m = add m (add m m)"

lemma trip_01: "trip 0 = 0"

apply(induct)

apply(auto)

done

lemma trip_02: "trip m = add m (add m m)"

apply(induction m)

apply(auto)

done

value "trip 1"

value "trip 2"

fun sum :: "nat \<Rightarrow> nat" where

  "sum 0 = 0"

| "sum (Suc n) = (Suc n) + sum n"

function sum1 :: "nat \<Rightarrow> nat" where

  "sum1 0 = 0"

| "n \<noteq> 0 \<Longrightarrow> sum1 n = n + sum1 (n - 1)"

apply(auto)

done

termination sum1

by (smt2 "termination" diff_less less_than_iff not_gr0 wf_less_than zero_neq_one)

lemma "sum n = sum1 n"

apply(induct n)

apply(auto)

done

lemma "sum n = (\<Sum>i \<le> n. i)"

apply(induct n)

apply(simp_all)

done

fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

"mull 0 0 = 0" |

"mull m 0 = 0" |

"mull m 1 = m" | 

(**"mull m (1::nat) = m" | **)

(**"mull m (suc(0)) = m" | **)

"mull m n = mull m (n-(1::nat))" 

apply(pat_completeness)

apply(auto)

done

  "mull 0 n = 0"

| "mull (Suc m) n = add n (mull m n)" 

lemma test: "mull m n = m * n"

sorry

fun poww :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

  "poww 0 n = 1"

| "poww (Suc m) n = mull n (poww m n)" 

"mull 0 0 = 0" |

"mull m 0 = 0" |

(**"mull m 1 = m" | **)

(**"mull m (1::nat) = m" | **)

(**"mull m (suc(0)) = m" | **)

"mull m n = mull m (n-(1::nat))" 

(**Define a function that counts the

number of occurrences of an element in a list **)

(**

fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where

"count  "

**)

(* prove n = n * (n + 1) div 2  *)