# 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 \ 'a \ '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 \ 'a" +where + "foldR [] = un" +| "foldR (x#xs) = opr x (foldR xs)" + +fun foldL :: "'a list \ '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