# HG changeset patch
# User fahadausaf <fahad.ausaf@icloud.com>
# Date 1413188423 -3600
# Node ID 2345ba5b42648e2b80729a5f18fe6bd399306508
# Parent  d3831bf423f2357cba1ef43f223aca74b94b270e
Proof Automation

diff -r d3831bf423f2 -r 2345ba5b4264 thys/#MyTree.thy#
--- a/thys/#MyTree.thy#	Fri Oct 10 18:45:10 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-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 d3831bf423f2 -r 2345ba5b4264 thys/MyInduction.thy
--- a/thys/MyInduction.thy	Fri Oct 10 18:45:10 2014 +0100
+++ b/thys/MyInduction.thy	Mon Oct 13 09:20:23 2014 +0100
@@ -1,3 +1,19 @@
 theory MyInduction
 imports Main
 begin
+
+fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"itrev [] ys = ys" |
+"itrev (x#xs) ys = itrev xs (x#ys)"
+
+lemma "itrev xs [] = rev xs"
+apply(induction xs)
+apply(auto)
+oops
+
+lemma "itrev xs ys = rev xs @ ys"
+apply(induction xs arbitrary: ys)
+apply auto
+done
+
+
diff -r d3831bf423f2 -r 2345ba5b4264 thys/MySimplification.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/MySimplification.thy	Mon Oct 13 09:20:23 2014 +0100
@@ -0,0 +1,3 @@
+theory MySimplification
+imports Main
+begin
diff -r d3831bf423f2 -r 2345ba5b4264 thys/MyTree.thy
--- a/thys/MyTree.thy	Fri Oct 10 18:45:10 2014 +0100
+++ b/thys/MyTree.thy	Mon Oct 13 09:20:23 2014 +0100
@@ -1,3 +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 d3831bf423f2 -r 2345ba5b4264 thys/ProofAutomation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/ProofAutomation.thy	Mon Oct 13 09:20:23 2014 +0100
@@ -0,0 +1,36 @@
+theory ProofAutomation
+imports Main
+begin
+
+lemma "\<forall>x. \<exists>y. x = y"
+by auto
+
+lemma "A \<subseteq> B \<inter> C \<Longrightarrow> A \<subseteq> B \<union> C"
+by auto
+
+lemma "\<lbrakk> \<forall> xs \<in> A. \<exists> ys. xs = ys @ ys; us \<in> A \<rbrakk> \<Longrightarrow> \<exists>n. length us = n+n"
+by fastforce
+
+lemma "\<lbrakk>xs @ ys = ys @ xs; length xs = length ys \<rbrakk> \<Longrightarrow> xs = ys"
+by auto
+
+lemma "\<lbrakk> (a::nat) \<le> x + b; 2*x < c\<rbrakk> \<Longrightarrow> 2*a + 1 \<le> 2*b + c"
+by arith
+
+lemma "\<lbrakk> (a::nat) \<le> b; b \<le> c; c \<le> d; d \<le> e \<rbrakk> \<Longrightarrow> a \<le> e"
+by (blast intro: le_trans)
+
+lemma "Suc(Suc(Suc a)) \<le> b \<Longrightarrow> a \<le> b"
+by(blast dest: Suc_leD)
+
+inductive ev :: "nat \<Rightarrow> bool" where
+ev0: "ev 0" |
+evSS: "ev n \<Longrightarrow> ev (n + 2)"
+
+fun even :: "nat \<Rightarrow> bool" where
+"even 0 = True" |
+"even (Suc 0) = False" |
+"even (Suc(Suc n)) = even n"
+
+lemma "ev m \<Longrightarrow> even m"
+