# HG changeset patch # User fahadausaf <fahad.ausaf@icloud.com> # Date 1412590666 -3600 # Node ID 5c6f9325327f5cdc49c9c59b05a3c7e2f72345ec # Parent 62fe79ee27264872f7dd9d3fe68aba249a89c526 calculator diff -r 62fe79ee2726 -r 5c6f9325327f thys/MyFirst.thy --- /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 " +**) + + + + + + + + + +