src/HOLCF/Fixrec.thy
changeset 16776 a3899ac14a1c
parent 16758 c32334d98fcd
child 16779 ac1dc3d4746a
equal deleted inserted replaced
16775:c1b87ef4a1c3 16776:a3899ac14a1c
     9 imports Sprod Ssum Up One Tr Fix
     9 imports Sprod Ssum Up One Tr Fix
    10 uses ("fixrec_package.ML")
    10 uses ("fixrec_package.ML")
    11 begin
    11 begin
    12 
    12 
    13 subsection {* Maybe monad type *}
    13 subsection {* Maybe monad type *}
       
    14 
       
    15 defaultsort cpo
    14 
    16 
    15 types 'a maybe = "one ++ 'a u"
    17 types 'a maybe = "one ++ 'a u"
    16 
    18 
    17 constdefs
    19 constdefs
    18   fail :: "'a maybe"
    20   fail :: "'a maybe"
    75 by (rule_tac p=m in maybeE, simp_all)
    77 by (rule_tac p=m in maybeE, simp_all)
    76 
    78 
    77 subsection {* Run operator *}
    79 subsection {* Run operator *}
    78 
    80 
    79 constdefs
    81 constdefs
    80   run:: "'a maybe \<rightarrow> 'a"
    82   run:: "'a::pcpo maybe \<rightarrow> 'a"
    81   "run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
    83   "run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
    82 
    84 
    83 text {* rewrite rules for run *}
    85 text {* rewrite rules for run *}
    84 
    86 
    85 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
    87 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
   117 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
   119 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
   118 by (rule_tac p=x in maybeE, simp_all)
   120 by (rule_tac p=x in maybeE, simp_all)
   119 
   121 
   120 subsection {* Match functions for built-in types *}
   122 subsection {* Match functions for built-in types *}
   121 
   123 
   122 constdefs
   124 defaultsort pcpo
   123   match_cpair :: "'a \<times> 'b \<rightarrow> ('a \<times> 'b) maybe"
   125 
       
   126 constdefs
       
   127   match_UU :: "'a \<rightarrow> unit maybe"
       
   128   "match_UU \<equiv> \<Lambda> x. fail"
       
   129 
       
   130   match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe"
   124   "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   131   "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   125 
   132 
   126   match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
   133   match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
   127   "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   134   "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   128 
   135 
   130   "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
   137   "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
   131 
   138 
   132   match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
   139   match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
   133   "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
   140   "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
   134 
   141 
   135   match_up :: "'a u \<rightarrow> 'a maybe"
   142   match_up :: "'a::cpo u \<rightarrow> 'a maybe"
   136   "match_up \<equiv> fup\<cdot>return"
   143   "match_up \<equiv> fup\<cdot>return"
   137 
   144 
   138   match_ONE :: "one \<rightarrow> unit maybe"
   145   match_ONE :: "one \<rightarrow> unit maybe"
   139   "match_ONE \<equiv> flift1 (\<lambda>u. return\<cdot>())"
   146   "match_ONE \<equiv> flift1 (\<lambda>u. return\<cdot>())"
   140 
   147 
   141   match_TT :: "tr \<rightarrow> unit maybe"
   148   match_TT :: "tr \<rightarrow> unit maybe"
   142   "match_TT \<equiv> flift1 (\<lambda>b. if b then return\<cdot>() else fail)"
   149   "match_TT \<equiv> flift1 (\<lambda>b. if b then return\<cdot>() else fail)"
   143 
   150 
   144   match_FF :: "tr \<rightarrow> unit maybe"
   151   match_FF :: "tr \<rightarrow> unit maybe"
   145   "match_FF \<equiv> flift1 (\<lambda>b. if b then fail else return\<cdot>())"
   152   "match_FF \<equiv> flift1 (\<lambda>b. if b then fail else return\<cdot>())"
       
   153 
       
   154 lemma match_UU_simps [simp]:
       
   155   "match_UU\<cdot>x = fail"
       
   156 by (simp add: match_UU_def)
   146 
   157 
   147 lemma match_cpair_simps [simp]:
   158 lemma match_cpair_simps [simp]:
   148   "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
   159   "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
   149 by (simp add: match_cpair_def)
   160 by (simp add: match_cpair_def)
   150 
   161