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
```