# HG changeset patch
# User krauss
# Date 1176185960 -7200
# Node ID e40957ccf0e9cb9e9da2b359aa29b9c00d881918
# Parent  1fb7fb24c799a277e61cf0a780ce07c364ab3d82
added example for definitions in local contexts

diff -r 1fb7fb24c799 -r e40957ccf0e9 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Tue Apr 10 08:09:28 2007 +0200
+++ b/src/HOL/ex/Fundefs.thy	Tue Apr 10 08:19:20 2007 +0200
@@ -173,6 +173,41 @@
 thm evn_od.termination
 
 
+section {* Definitions in local contexts *}
+
+locale my_monoid = 
+fixes opr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  and un :: "'a"
+assumes assoc: "opr (opr x y) z = opr x (opr y z)"
+  and lunit: "opr un x = x"
+  and runit: "opr x un = x"
+
+
+context my_monoid
+begin
+
+fun foldR :: "'a list \<Rightarrow> 'a"
+where
+  "foldR [] = un"
+| "foldR (x#xs) = opr x (foldR xs)"
+
+fun foldL :: "'a list \<Rightarrow> 'a"
+where
+  "foldL [] = un"
+| "foldL [x] = x"
+| "foldL (x#y#ys) = foldL (opr x y # ys)" 
+
+thm foldL.simps
+
+lemma foldR_foldL: "foldR xs = foldL xs"
+by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc)
+
+thm foldR_foldL
+
+end
+
+thm my_monoid.foldL.simps
+thm my_monoid.foldR_foldL
 
 
 end