# HG changeset patch
# User fahadausaf <fahad.ausaf@icloud.com>
# Date 1412963110 -3600
# Node ID d3831bf423f2357cba1ef43f223aca74b94b270e
# Parent  378077bab5d24e367c65bf6552d932cc6f19665c
trees

diff -r 378077bab5d2 -r d3831bf423f2 thys/#MyTree.thy#
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/#MyTree.thy#	Fri Oct 10 18:45:10 2014 +0100
@@ -0,0 +1,42 @@
+theory MyTree
+imports Main
+begin
+
+datatype 
+  'a tree = Tip | 
+  Node " 'a tree" 'a " 'a tree"
+
+fun mirror :: " 'a tree \<Rightarrow> 'a tree" where
+  "mirror Tip = Tip" |
+  "mirror (Node l a r) = Node (mirror r) a (mirror l)"
+
+lemma "mirror(mirror t) = t"
+  apply(induction t)
+  apply(auto)
+  done
+
+datatype 'a option = None | Some 'a
+
+fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
+  "lookup [] x = None" |
+  "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
+
+definition sq :: "nat \<Rightarrow> nat" where
+  "sq n = n * n"
+ 
+abbreviation sq' :: "nat \<Rightarrow> nat" where
+  "sq' n \<equiv> n * n"
+
+fun div2 :: "nat \<Rightarrow> nat" where
+  "div2 0 = 0" |
+  "div2 (Suc 0) = 0" |
+  "div2 (Suc(Suc n)) = Suc(div2 n)"
+
+lemma "div2(n) = n div 2"
+apply(induction n rule: div2.induct)
+apply(auto)
+done
+
+value "div2 8"
+
+
diff -r 378077bab5d2 -r d3831bf423f2 thys/MyInduction.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/MyInduction.thy	Fri Oct 10 18:45:10 2014 +0100
@@ -0,0 +1,3 @@
+theory MyInduction
+imports Main
+begin
diff -r 378077bab5d2 -r d3831bf423f2 thys/MyTree.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/MyTree.thy	Fri Oct 10 18:45:10 2014 +0100
@@ -0,0 +1,3 @@
+theory MyTree
+imports Main
+begin