New theory with lemmas for the fixrec package
authorhuffman
Sat Jun 04 00:22:08 2005 +0200 (2005-06-04)
changeset 16221879400e029bf
parent 16220 fd980649c4b2
child 16222 613183ac1fa0
New theory with lemmas for the fixrec package
src/HOLCF/Fixrec.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/Fixrec.thy	Sat Jun 04 00:22:08 2005 +0200
     1.3 @@ -0,0 +1,142 @@
     1.4 +(*  Title:      HOLCF/Fixrec.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Amber Telfer and Brian Huffman
     1.7 +*)
     1.8 +
     1.9 +header "Package for defining recursive functions in HOLCF"
    1.10 +
    1.11 +theory Fixrec
    1.12 +imports Ssum One Up Fix
    1.13 +(* files ("fixrec_package.ML") *)
    1.14 +begin
    1.15 +
    1.16 +subsection {* Maybe monad type *}
    1.17 +
    1.18 +types 'a maybe = "one ++ 'a u"
    1.19 +
    1.20 +constdefs
    1.21 +  fail :: "'a maybe"
    1.22 +  "fail \<equiv> sinl\<cdot>ONE"
    1.23 +
    1.24 +  return :: "'a \<rightarrow> 'a maybe"
    1.25 +  "return \<equiv> sinr oo up"
    1.26 +
    1.27 +lemma maybeE:
    1.28 +  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    1.29 +apply (unfold fail_def return_def)
    1.30 +apply (rule_tac p=p in ssumE, simp)
    1.31 +apply (rule_tac p=x in oneE, simp, simp)
    1.32 +apply (rule_tac p=y in upE1, simp, simp)
    1.33 +done
    1.34 +
    1.35 +subsection {* Monadic bind operator *}
    1.36 +
    1.37 +constdefs
    1.38 +  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
    1.39 +  "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
    1.40 +
    1.41 +syntax
    1.42 +  "_bind" :: "'a maybe \<Rightarrow> ('a \<rightarrow> 'b maybe) \<Rightarrow> 'b maybe"
    1.43 +    ("(_ >>= _)" [50, 51] 50)
    1.44 +
    1.45 +translations "m >>= k" == "bind\<cdot>m\<cdot>k"
    1.46 +
    1.47 +nonterminals
    1.48 +  maybebind maybebinds
    1.49 +
    1.50 +syntax 
    1.51 +  "_MBIND"  :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind"         ("(2_ <-/ _)" 10)
    1.52 +  ""        :: "maybebind \<Rightarrow> maybebinds"                ("_")
    1.53 +
    1.54 +  "_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds"  ("_;/ _")
    1.55 +  "_MDO"    :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe"     ("(do _;/ (_))" 10)
    1.56 +
    1.57 +translations
    1.58 +  "_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)"
    1.59 +  "do (x,y) <- m; e" == "m >>= (LAM <x,y>. e)" 
    1.60 +  "do x <- m; e"            == "m >>= (LAM x. e)"
    1.61 +
    1.62 +text {* monad laws *}
    1.63 +
    1.64 +lemma bind_strict [simp]: "UU >>= f = UU"
    1.65 +by (simp add: bind_def)
    1.66 +
    1.67 +lemma bind_fail [simp]: "fail >>= f = fail"
    1.68 +by (simp add: bind_def fail_def)
    1.69 +
    1.70 +lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a"
    1.71 +by (simp add: bind_def return_def)
    1.72 +
    1.73 +lemma right_unit [simp]: "m >>= return = m"
    1.74 +by (rule_tac p=m in maybeE, simp_all)
    1.75 +
    1.76 +lemma bind_assoc [simp]:
    1.77 + "(do a <- m; b <- k\<cdot>a; h\<cdot>b) = (do b <- (do a <- m; k\<cdot>a); h\<cdot>b)"
    1.78 +by (rule_tac p=m in maybeE, simp_all)
    1.79 +
    1.80 +subsection {* Run operator *}
    1.81 +
    1.82 +constdefs
    1.83 +  run:: "'a maybe \<rightarrow> 'a"
    1.84 +  "run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
    1.85 +
    1.86 +text {* rewrite rules for run *}
    1.87 +
    1.88 +lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
    1.89 +by (simp add: run_def)
    1.90 +
    1.91 +lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
    1.92 +by (simp add: run_def fail_def)
    1.93 +
    1.94 +lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
    1.95 +by (simp add: run_def return_def)
    1.96 +
    1.97 +subsection {* Monad plus operator *}
    1.98 +
    1.99 +constdefs
   1.100 +  mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
   1.101 +  "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
   1.102 +
   1.103 +syntax "+++" :: "'a maybe \<Rightarrow> 'a maybe \<Rightarrow> 'a maybe" (infixr 65)
   1.104 +translations "x +++ y" == "mplus\<cdot>x\<cdot>y"
   1.105 +
   1.106 +text {* rewrite rules for mplus *}
   1.107 +
   1.108 +lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
   1.109 +by (simp add: mplus_def)
   1.110 +
   1.111 +lemma mplus_fail [simp]: "fail +++ m = m"
   1.112 +by (simp add: mplus_def fail_def)
   1.113 +
   1.114 +lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"
   1.115 +by (simp add: mplus_def return_def)
   1.116 +
   1.117 +lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
   1.118 +by (rule_tac p=x in maybeE, simp_all)
   1.119 +
   1.120 +subsection {* Match functions for built-in types *}
   1.121 +
   1.122 +text {* Currently the package only supports lazy constructors *}
   1.123 +
   1.124 +constdefs
   1.125 +  match_cpair :: "'a \<times> 'b \<rightarrow> ('a \<times> 'b) maybe"
   1.126 +  "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   1.127 +
   1.128 +  match_up :: "'a u \<rightarrow> 'a maybe"
   1.129 +  "match_up \<equiv> fup\<cdot>return"
   1.130 +
   1.131 +lemma match_cpair_simps [simp]:
   1.132 +  "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
   1.133 +by (simp add: match_cpair_def)
   1.134 +
   1.135 +lemma match_up_simps [simp]:
   1.136 +  "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
   1.137 +  "match_up\<cdot>\<bottom> = \<bottom>"
   1.138 +by (simp_all add: match_up_def)
   1.139 +
   1.140 +
   1.141 +subsection {* Intitializing the fixrec package *}
   1.142 +
   1.143 +(* use "fixrec_package.ML" *)
   1.144 +
   1.145 +end