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
value "add 2 3"
(**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"
sorry
lemma add_Suc: "add m (Suc n) = Suc (add m n)"
sorry
lemma add_comm: "add m n = add n m"
apply(induct m)
apply(simp add: add_zero)
apply(simp add: add_Suc)
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 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))"
(**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 "
**)
fun sum :: "nat \<Rightarrow> nat" where
"sum n = 0 + \<dots> + n"
(* prove n = n * (n + 1) div 2 *)