# HG changeset patch
# User fahadausaf <fahad.ausaf@icloud.com>
# Date 1412703809 -3600
# Node ID a2a7f65f538a14a3fb3b2128b1a7363faa4b760f
# Parent  789ade899a53a3c8616dab23697e9d09f5e929ee
lemma

diff -r 789ade899a53 -r a2a7f65f538a thys/CountSnoc.thy
--- a/thys/CountSnoc.thy	Tue Oct 07 16:17:23 2014 +0100
+++ b/thys/CountSnoc.thy	Tue Oct 07 18:43:29 2014 +0100
@@ -22,6 +22,11 @@
 value "count_list (1::nat) [1,1,1]"
 value "count_list (1::nat) [2,2,2]"
 value "count_list (2::nat) [2,2,1]"
+
+lemma count1: "count_list n(xs @ ys) = count_list n xs + count_list n ys"
+apply(induct xs)
+apply(auto)
+ 
  
 
 
diff -r 789ade899a53 -r a2a7f65f538a thys/CountSnoc.thy.orig
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/CountSnoc.thy.orig	Tue Oct 07 18:43:29 2014 +0100
@@ -0,0 +1,39 @@
+theory CountSnoc
+imports Main
+begin
+
+datatype 'a myList = Nil | Cons 'a "'a myList"
+
+fun app_list :: "'a myList \<Rightarrow> 'a myList \<Rightarrow> 'a myList" where
+"app_list Nil ys = ys" |
+"app_list (Cons x xs) ys = Cons x (app_list xs ys)"
+
+fun rev_list :: "'a myList \<Rightarrow> 'a myList" where
+"rev_list Nil = Nil" |
+"rev_list (Cons x xs) = app_list (rev_list xs) (Cons x Nil)"
+
+(*
+fun count_list :: "'a \<Rightarrow> 'a myList \<Rightarrow> nat" where
+"count_list x [] = 0" |
+"count_list x (y#xs) = (
+  if x = y then Suc(count_list x xs) 
+  else count_list x xs)"
+*)
+
+fun count_list :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
+"count_list x [] = 0" |
+"count_list x (y#xs) = (
+  if x = y then Suc(count_list x xs) 
+  else count_list x xs)"
+
+<<<<<<< local
+value "count_list 1 [1,1,0]"
+value "count_list 1 [2,2,2]"
+value "count_list 2 [2,2,1]"
+=======
+value "count_list (1::nat) [1,1,1]"
+value "count_list (1::nat) [2,2,2]"
+value "count_list (2::nat) [2,2,1]"
+>>>>>>> other
+ 
+
diff -r 789ade899a53 -r a2a7f65f538a thys/CountSnoc.thy~
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/CountSnoc.thy~	Tue Oct 07 18:43:29 2014 +0100
@@ -0,0 +1,29 @@
+theory CountSnoc
+imports Main
+begin
+
+
+datatype 'a myList = Nil | Cons 'a "'a myList"
+
+fun app_list :: "'a myList \<Rightarrow> 'a myList \<Rightarrow> 'a myList" where
+"app_list Nil ys = ys" |
+"app_list (Cons x xs) ys = Cons x (app_list xs ys)"
+
+fun rev_list :: "'a myList \<Rightarrow> 'a myList" where
+"rev_list Nil = Nil" |
+"rev_list (Cons x xs) = app_list (rev_list xs) (Cons x Nil)"
+
+fun count_list :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
+"count_list x [] = 0" |
+"count_list x (y#xs) = (
+  if x = y then Suc(count_list x xs) 
+  else count_list x xs)"
+
+value "count_list (1::nat) [1,1,1]"
+value "count_list (1::nat) [2,2,2]"
+value "count_list (2::nat) [2,2,1]"
+ 
+
+
+
+