diff -r 893f0314a88b -r fff2b8d356a5 thys/#MyFirst.thy#
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/#MyFirst.thy#	Tue Oct 07 12:33:27 2014 +0100
@@ -0,0 +1,198 @@
+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 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)"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"
+apply(induct n)
+apply(auto)
+done
+lemma add_zero: "add n 0 = n"
+apply(induct n)
+apply(auto)
+done
+lemma add_Suc: "add m (Suc n) = Suc (add m n)"
+apply(induct m)
+apply(metis add.simps(1))
+apply(auto)
+done
+
+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  *)
+
+
+
+
+
+
+
+
+
+
+