src/HOLCF/Fixrec.thy
 author huffman Thu Jun 23 21:17:26 2005 +0200 (2005-06-23) changeset 16551 7abf8a713613 parent 16463 342d74ca8815 child 16754 1b979f8b7e8e permissions -rw-r--r--
added match functions for spair, sinl, sinr
```     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 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_fail2 [simp]: "m +++ fail = m"
```
```   115 by (rule_tac p=m in maybeE, simp_all)
```
```   116
```
```   117 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
```
```   118 by (rule_tac p=x in maybeE, simp_all)
```
```   119
```
```   120 subsection {* Match functions for built-in types *}
```
```   121
```
```   122 constdefs
```
```   123   match_cpair :: "'a \<times> 'b \<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 u \<rightarrow> 'a maybe"
```
```   136   "match_up \<equiv> fup\<cdot>return"
```
```   137
```
```   138   match_ONE :: "one \<rightarrow> unit maybe"
```
```   139   "match_ONE \<equiv> flift1 (\<lambda>u. return\<cdot>())"
```
```   140
```
```   141   match_TT :: "tr \<rightarrow> unit maybe"
```
```   142   "match_TT \<equiv> flift1 (\<lambda>b. if b then return\<cdot>() else fail)"
```
```   143
```
```   144   match_FF :: "tr \<rightarrow> unit maybe"
```
```   145   "match_FF \<equiv> flift1 (\<lambda>b. if b then fail else return\<cdot>())"
```
```   146
```
```   147 lemma match_cpair_simps [simp]:
```
```   148   "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
```
```   149 by (simp add: match_cpair_def)
```
```   150
```
```   151 lemma match_spair_simps [simp]:
```
```   152   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>"
```
```   153   "match_spair\<cdot>\<bottom> = \<bottom>"
```
```   154 by (simp_all add: match_spair_def)
```
```   155
```
```   156 lemma match_sinl_simps [simp]:
```
```   157   "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x"
```
```   158   "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail"
```
```   159   "match_sinl\<cdot>\<bottom> = \<bottom>"
```
```   160 by (simp_all add: match_sinl_def)
```
```   161
```
```   162 lemma match_sinr_simps [simp]:
```
```   163   "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x"
```
```   164   "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail"
```
```   165   "match_sinr\<cdot>\<bottom> = \<bottom>"
```
```   166 by (simp_all add: match_sinr_def)
```
```   167
```
```   168 lemma match_up_simps [simp]:
```
```   169   "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
```
```   170   "match_up\<cdot>\<bottom> = \<bottom>"
```
```   171 by (simp_all add: match_up_def)
```
```   172
```
```   173 lemma match_ONE_simps [simp]:
```
```   174   "match_ONE\<cdot>ONE = return\<cdot>()"
```
```   175   "match_ONE\<cdot>\<bottom> = \<bottom>"
```
```   176 by (simp_all add: ONE_def match_ONE_def)
```
```   177
```
```   178 lemma match_TT_simps [simp]:
```
```   179   "match_TT\<cdot>TT = return\<cdot>()"
```
```   180   "match_TT\<cdot>FF = fail"
```
```   181   "match_TT\<cdot>\<bottom> = \<bottom>"
```
```   182 by (simp_all add: TT_def FF_def match_TT_def)
```
```   183
```
```   184 lemma match_FF_simps [simp]:
```
```   185   "match_FF\<cdot>FF = return\<cdot>()"
```
```   186   "match_FF\<cdot>TT = fail"
```
```   187   "match_FF\<cdot>\<bottom> = \<bottom>"
```
```   188 by (simp_all add: TT_def FF_def match_FF_def)
```
```   189
```
```   190 subsection {* Mutual recursion *}
```
```   191
```
```   192 text {*
```
```   193   The following rules are used to prove unfolding theorems from
```
```   194   fixed-point definitions of mutually recursive functions.
```
```   195 *}
```
```   196
```
```   197 lemma cpair_equalI: "\<lbrakk>x \<equiv> cfst\<cdot>p; y \<equiv> csnd\<cdot>p\<rbrakk> \<Longrightarrow> <x,y> \<equiv> p"
```
```   198 by (simp add: surjective_pairing_Cprod2)
```
```   199
```
```   200 lemma cpair_eqD1: "<x,y> = <x',y'> \<Longrightarrow> x = x'"
```
```   201 by simp
```
```   202
```
```   203 lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
```
```   204 by simp
```
```   205
```
```   206 text {* lemma for proving rewrite rules *}
```
```   207
```
```   208 lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
```
```   209 by simp
```
```   210
```
```   211 ML {*
```
```   212 val cpair_equalI = thm "cpair_equalI";
```
```   213 val cpair_eqD1 = thm "cpair_eqD1";
```
```   214 val cpair_eqD2 = thm "cpair_eqD2";
```
```   215 val ssubst_lhs = thm "ssubst_lhs";
```
```   216 *}
```
```   217
```
```   218 subsection {* Intitializing the fixrec package *}
```
```   219
```
```   220 use "fixrec_package.ML"
```
```   221
```
```   222 end
```