--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/MyFirst.thy	Mon Oct 06 11:17:46 2014 +0100
@@ -0,0 +1,110 @@
+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"
+
+lemma add_04: "add m (add n k) = add k (add m n)"
+apply(induct)
+apply(auto)
+oops
+
+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 n = 0" 
+
+(**
+fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where
+"count  "
+**)
+
+
+
+
+
+
+
+
+
+