diff -r 5b01f7c233f8 -r a33d3040bf7e thys/MyFirst.thy
--- a/thys/MyFirst.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,189 +0,0 @@
-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"
-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  *)
-
-
-
-
-
-
-
-
-
-
-