# HG changeset patch # User huffman # Date 1117837328 -7200 # Node ID 879400e029bfaa67fde024185902d489ae8b8d1b # Parent fd980649c4b2c3b988c8097b0d852384f32e1cf0 New theory with lemmas for the fixrec package diff -r fd980649c4b2 -r 879400e029bf src/HOLCF/Fixrec.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Fixrec.thy Sat Jun 04 00:22:08 2005 +0200 @@ -0,0 +1,142 @@ +(* Title: HOLCF/Fixrec.thy + ID: $Id$ + Author: Amber Telfer and Brian Huffman +*) + +header "Package for defining recursive functions in HOLCF" + +theory Fixrec +imports Ssum One Up Fix +(* files ("fixrec_package.ML") *) +begin + +subsection {* Maybe monad type *} + +types 'a maybe = "one ++ 'a u" + +constdefs + fail :: "'a maybe" + "fail \ sinl\ONE" + + return :: "'a \ 'a maybe" + "return \ sinr oo up" + +lemma maybeE: + "\p = \ \ Q; p = fail \ Q; \x. p = return\x \ Q\ \ Q" +apply (unfold fail_def return_def) +apply (rule_tac p=p in ssumE, simp) +apply (rule_tac p=x in oneE, simp, simp) +apply (rule_tac p=y in upE1, simp, simp) +done + +subsection {* Monadic bind operator *} + +constdefs + bind :: "'a maybe \ ('a \ 'b maybe) \ 'b maybe" + "bind \ \ m f. sscase\sinl\(fup\f)\m" + +syntax + "_bind" :: "'a maybe \ ('a \ 'b maybe) \ 'b maybe" + ("(_ >>= _)" [50, 51] 50) + +translations "m >>= k" == "bind\m\k" + +nonterminals + maybebind maybebinds + +syntax + "_MBIND" :: "pttrn \ 'a maybe \ maybebind" ("(2_ <-/ _)" 10) + "" :: "maybebind \ maybebinds" ("_") + + "_MBINDS" :: "[maybebind, maybebinds] \ maybebinds" ("_;/ _") + "_MDO" :: "[maybebinds, 'a maybe] \ 'a maybe" ("(do _;/ (_))" 10) + +translations + "_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)" + "do (x,y) <- m; e" == "m >>= (LAM . e)" + "do x <- m; e" == "m >>= (LAM x. e)" + +text {* monad laws *} + +lemma bind_strict [simp]: "UU >>= f = UU" +by (simp add: bind_def) + +lemma bind_fail [simp]: "fail >>= f = fail" +by (simp add: bind_def fail_def) + +lemma left_unit [simp]: "(return\a) >>= k = k\a" +by (simp add: bind_def return_def) + +lemma right_unit [simp]: "m >>= return = m" +by (rule_tac p=m in maybeE, simp_all) + +lemma bind_assoc [simp]: + "(do a <- m; b <- k\a; h\b) = (do b <- (do a <- m; k\a); h\b)" +by (rule_tac p=m in maybeE, simp_all) + +subsection {* Run operator *} + +constdefs + run:: "'a maybe \ 'a" + "run \ sscase\\\(fup\ID)" + +text {* rewrite rules for run *} + +lemma run_strict [simp]: "run\\ = \" +by (simp add: run_def) + +lemma run_fail [simp]: "run\fail = \" +by (simp add: run_def fail_def) + +lemma run_return [simp]: "run\(return\x) = x" +by (simp add: run_def return_def) + +subsection {* Monad plus operator *} + +constdefs + mplus :: "'a maybe \ 'a maybe \ 'a maybe" + "mplus \ \ m1 m2. sscase\(\ x. m2)\(fup\return)\m1" + +syntax "+++" :: "'a maybe \ 'a maybe \ 'a maybe" (infixr 65) +translations "x +++ y" == "mplus\x\y" + +text {* rewrite rules for mplus *} + +lemma mplus_strict [simp]: "\ +++ m = \" +by (simp add: mplus_def) + +lemma mplus_fail [simp]: "fail +++ m = m" +by (simp add: mplus_def fail_def) + +lemma mplus_return [simp]: "return\x +++ m = return\x" +by (simp add: mplus_def return_def) + +lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)" +by (rule_tac p=x in maybeE, simp_all) + +subsection {* Match functions for built-in types *} + +text {* Currently the package only supports lazy constructors *} + +constdefs + match_cpair :: "'a \ 'b \ ('a \ 'b) maybe" + "match_cpair \ csplit\(\ x y. return\)" + + match_up :: "'a u \ 'a maybe" + "match_up \ fup\return" + +lemma match_cpair_simps [simp]: + "match_cpair\ = return\" +by (simp add: match_cpair_def) + +lemma match_up_simps [simp]: + "match_up\(up\x) = return\x" + "match_up\\ = \" +by (simp_all add: match_up_def) + + +subsection {* Intitializing the fixrec package *} + +(* use "fixrec_package.ML" *) + +end