src/HOLCF/Fixrec.thy
author huffman
Sun Nov 06 00:35:24 2005 +0100 (2005-11-06)
changeset 18096 574aa0487069
parent 18094 404f298220af
child 18097 d196d84c306f
permissions -rw-r--r--
use consts for infix syntax
     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 Sprod Ssum Up One Tr Fix
    10 uses ("fixrec_package.ML")
    11 begin
    12 
    13 subsection {* Maybe monad type *}
    14 
    15 defaultsort cpo
    16 
    17 types 'a maybe = "one ++ 'a u"
    18 
    19 constdefs
    20   fail :: "'a maybe"
    21   "fail \<equiv> sinl\<cdot>ONE"
    22 
    23   return :: "'a \<rightarrow> 'a maybe"
    24   "return \<equiv> sinr oo up"
    25 
    26 lemma maybeE:
    27   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    28 apply (unfold fail_def return_def)
    29 apply (rule_tac p=p in ssumE, simp)
    30 apply (rule_tac p=x in oneE, simp, simp)
    31 apply (rule_tac p=y in upE, simp, simp)
    32 done
    33 
    34 subsection {* Monadic bind operator *}
    35 
    36 consts
    37   bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" (infixl ">>=" 50)
    38 defs
    39   bind_def: "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
    40 
    41 nonterminals
    42   maybebind maybebinds
    43 
    44 syntax 
    45   "_MBIND"  :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind"         ("(2_ <-/ _)" 10)
    46   ""        :: "maybebind \<Rightarrow> maybebinds"                ("_")
    47 
    48   "_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds"  ("_;/ _")
    49   "_MDO"    :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe"     ("(do _;/ (_))" 10)
    50 
    51 translations
    52   "_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)"
    53   "do (x,y) <- m; e" == "m >>= (LAM <x,y>. e)" 
    54   "do x <- m; e"            == "m >>= (LAM x. e)"
    55 
    56 text {* monad laws *}
    57 
    58 lemma bind_strict [simp]: "UU >>= f = UU"
    59 by (simp add: bind_def)
    60 
    61 lemma bind_fail [simp]: "fail >>= f = fail"
    62 by (simp add: bind_def fail_def)
    63 
    64 lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a"
    65 by (simp add: bind_def return_def)
    66 
    67 lemma right_unit [simp]: "m >>= return = m"
    68 by (rule_tac p=m in maybeE, simp_all)
    69 
    70 lemma bind_assoc [simp]:
    71  "(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)"
    72 by (rule_tac p=m in maybeE, simp_all)
    73 
    74 subsection {* Run operator *}
    75 
    76 constdefs
    77   run:: "'a::pcpo maybe \<rightarrow> 'a"
    78   "run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
    79 
    80 text {* rewrite rules for run *}
    81 
    82 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
    83 by (simp add: run_def)
    84 
    85 lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
    86 by (simp add: run_def fail_def)
    87 
    88 lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
    89 by (simp add: run_def return_def)
    90 
    91 subsection {* Monad plus operator *}
    92 
    93 consts
    94   mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" (infixr "+++" 65)
    95 defs
    96   mplus_def: "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
    97 
    98 text {* rewrite rules for mplus *}
    99 
   100 lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
   101 by (simp add: mplus_def)
   102 
   103 lemma mplus_fail [simp]: "fail +++ m = m"
   104 by (simp add: mplus_def fail_def)
   105 
   106 lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"
   107 by (simp add: mplus_def return_def)
   108 
   109 lemma mplus_fail2 [simp]: "m +++ fail = m"
   110 by (rule_tac p=m in maybeE, simp_all)
   111 
   112 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
   113 by (rule_tac p=x in maybeE, simp_all)
   114 
   115 subsection {* Match functions for built-in types *}
   116 
   117 defaultsort pcpo
   118 
   119 constdefs
   120   match_UU :: "'a \<rightarrow> unit maybe"
   121   "match_UU \<equiv> \<Lambda> x. fail"
   122 
   123   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>)"
   125 
   126   match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
   127   "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   128 
   129   match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe"
   130   "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
   131 
   132   match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
   133   "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
   134 
   135   match_up :: "'a::cpo u \<rightarrow> 'a maybe"
   136   "match_up \<equiv> fup\<cdot>return"
   137 
   138   match_ONE :: "one \<rightarrow> unit maybe"
   139   "match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()"
   140  
   141   match_TT :: "tr \<rightarrow> unit maybe"
   142   "match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
   143  
   144   match_FF :: "tr \<rightarrow> unit maybe"
   145   "match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
   146 
   147 lemma match_UU_simps [simp]:
   148   "match_UU\<cdot>x = fail"
   149 by (simp add: match_UU_def)
   150 
   151 lemma match_cpair_simps [simp]:
   152   "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
   153 by (simp add: match_cpair_def)
   154 
   155 lemma match_spair_simps [simp]:
   156   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>"
   157   "match_spair\<cdot>\<bottom> = \<bottom>"
   158 by (simp_all add: match_spair_def)
   159 
   160 lemma match_sinl_simps [simp]:
   161   "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x"
   162   "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail"
   163   "match_sinl\<cdot>\<bottom> = \<bottom>"
   164 by (simp_all add: match_sinl_def)
   165 
   166 lemma match_sinr_simps [simp]:
   167   "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x"
   168   "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail"
   169   "match_sinr\<cdot>\<bottom> = \<bottom>"
   170 by (simp_all add: match_sinr_def)
   171 
   172 lemma match_up_simps [simp]:
   173   "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
   174   "match_up\<cdot>\<bottom> = \<bottom>"
   175 by (simp_all add: match_up_def)
   176 
   177 lemma match_ONE_simps [simp]:
   178   "match_ONE\<cdot>ONE = return\<cdot>()"
   179   "match_ONE\<cdot>\<bottom> = \<bottom>"
   180 by (simp_all add: match_ONE_def)
   181 
   182 lemma match_TT_simps [simp]:
   183   "match_TT\<cdot>TT = return\<cdot>()"
   184   "match_TT\<cdot>FF = fail"
   185   "match_TT\<cdot>\<bottom> = \<bottom>"
   186 by (simp_all add: match_TT_def)
   187 
   188 lemma match_FF_simps [simp]:
   189   "match_FF\<cdot>FF = return\<cdot>()"
   190   "match_FF\<cdot>TT = fail"
   191   "match_FF\<cdot>\<bottom> = \<bottom>"
   192 by (simp_all add: match_FF_def)
   193 
   194 subsection {* Mutual recursion *}
   195 
   196 text {*
   197   The following rules are used to prove unfolding theorems from
   198   fixed-point definitions of mutually recursive functions.
   199 *}
   200 
   201 lemma cpair_equalI: "\<lbrakk>x \<equiv> cfst\<cdot>p; y \<equiv> csnd\<cdot>p\<rbrakk> \<Longrightarrow> <x,y> \<equiv> p"
   202 by (simp add: surjective_pairing_Cprod2)
   203 
   204 lemma cpair_eqD1: "<x,y> = <x',y'> \<Longrightarrow> x = x'"
   205 by simp
   206 
   207 lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
   208 by simp
   209 
   210 text {* lemma for proving rewrite rules *}
   211 
   212 lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
   213 by simp
   214 
   215 ML {*
   216 val cpair_equalI = thm "cpair_equalI";
   217 val cpair_eqD1 = thm "cpair_eqD1";
   218 val cpair_eqD2 = thm "cpair_eqD2";
   219 val ssubst_lhs = thm "ssubst_lhs";
   220 *}
   221 
   222 subsection {* Initializing the fixrec package *}
   223 
   224 use "fixrec_package.ML"
   225 
   226 end