src/HOLCF/Fixrec.thy
changeset 16221 879400e029bf
child 16229 77cae9c8e73e
equal deleted inserted replaced
16220:fd980649c4b2 16221:879400e029bf
       
     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 built-in 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