16221

1 
(* Title: HOLCF/Fixrec.thy


2 
ID: $Id$


3 
Author: Amber Telfer and Brian Huffman


4 
*)


5 


6 
header "Package for defining recursive functions in HOLCF"


7 


8 
theory Fixrec


9 
imports Ssum One Up Fix


10 
(* files ("fixrec_package.ML") *)


11 
begin


12 


13 
subsection {* Maybe monad type *}


14 


15 
types 'a maybe = "one ++ 'a u"


16 


17 
constdefs


18 
fail :: "'a maybe"


19 
"fail \<equiv> sinl\<cdot>ONE"


20 


21 
return :: "'a \<rightarrow> 'a maybe"


22 
"return \<equiv> sinr oo up"


23 


24 
lemma maybeE:


25 
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"


26 
apply (unfold fail_def return_def)


27 
apply (rule_tac p=p in ssumE, simp)


28 
apply (rule_tac p=x in oneE, simp, simp)


29 
apply (rule_tac p=y in upE1, simp, simp)


30 
done


31 


32 
subsection {* Monadic bind operator *}


33 


34 
constdefs


35 
bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"


36 
"bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"


37 


38 
syntax


39 
"_bind" :: "'a maybe \<Rightarrow> ('a \<rightarrow> 'b maybe) \<Rightarrow> 'b maybe"


40 
("(_ >>= _)" [50, 51] 50)


41 


42 
translations "m >>= k" == "bind\<cdot>m\<cdot>k"


43 


44 
nonterminals


45 
maybebind maybebinds


46 


47 
syntax


48 
"_MBIND" :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind" ("(2_ </ _)" 10)


49 
"" :: "maybebind \<Rightarrow> maybebinds" ("_")


50 


51 
"_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds" ("_;/ _")


52 
"_MDO" :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe" ("(do _;/ (_))" 10)


53 


54 
translations


55 
"_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)"


56 
"do (x,y) < m; e" == "m >>= (LAM <x,y>. e)"


57 
"do x < m; e" == "m >>= (LAM x. e)"


58 


59 
text {* monad laws *}


60 


61 
lemma bind_strict [simp]: "UU >>= f = UU"


62 
by (simp add: bind_def)


63 


64 
lemma bind_fail [simp]: "fail >>= f = fail"


65 
by (simp add: bind_def fail_def)


66 


67 
lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a"


68 
by (simp add: bind_def return_def)


69 


70 
lemma right_unit [simp]: "m >>= return = m"


71 
by (rule_tac p=m in maybeE, simp_all)


72 


73 
lemma bind_assoc [simp]:


74 
"(do a < m; b < k\<cdot>a; h\<cdot>b) = (do b < (do a < m; k\<cdot>a); h\<cdot>b)"


75 
by (rule_tac p=m in maybeE, simp_all)


76 


77 
subsection {* Run operator *}


78 


79 
constdefs


80 
run:: "'a maybe \<rightarrow> 'a"


81 
"run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"


82 


83 
text {* rewrite rules for run *}


84 


85 
lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"


86 
by (simp add: run_def)


87 


88 
lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"


89 
by (simp add: run_def fail_def)


90 


91 
lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"


92 
by (simp add: run_def return_def)


93 


94 
subsection {* Monad plus operator *}


95 


96 
constdefs


97 
mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"


98 
"mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"


99 


100 
syntax "+++" :: "'a maybe \<Rightarrow> 'a maybe \<Rightarrow> 'a maybe" (infixr 65)


101 
translations "x +++ y" == "mplus\<cdot>x\<cdot>y"


102 


103 
text {* rewrite rules for mplus *}


104 


105 
lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"


106 
by (simp add: mplus_def)


107 


108 
lemma mplus_fail [simp]: "fail +++ m = m"


109 
by (simp add: mplus_def fail_def)


110 


111 
lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"


112 
by (simp add: mplus_def return_def)


113 


114 
lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"


115 
by (rule_tac p=x in maybeE, simp_all)


116 


117 
subsection {* Match functions for builtin types *}


118 


119 
text {* Currently the package only supports lazy constructors *}


120 


121 
constdefs


122 
match_cpair :: "'a \<times> 'b \<rightarrow> ('a \<times> 'b) maybe"


123 
"match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"


124 


125 
match_up :: "'a u \<rightarrow> 'a maybe"


126 
"match_up \<equiv> fup\<cdot>return"


127 


128 
lemma match_cpair_simps [simp]:


129 
"match_cpair\<cdot><x,y> = return\<cdot><x,y>"


130 
by (simp add: match_cpair_def)


131 


132 
lemma match_up_simps [simp]:


133 
"match_up\<cdot>(up\<cdot>x) = return\<cdot>x"


134 
"match_up\<cdot>\<bottom> = \<bottom>"


135 
by (simp_all add: match_up_def)


136 


137 


138 
subsection {* Intitializing the fixrec package *}


139 


140 
(* use "fixrec_package.ML" *)


141 


142 
end
