src/HOLCF/Fixrec.thy
 author huffman Mon Nov 07 19:23:53 2005 +0100 (2005-11-07) changeset 18110 08ec4f1f116d parent 18097 d196d84c306f child 18112 dc1d6f588204 permissions -rw-r--r--
remove syntax for as-patterns
```     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 subsubsection {* Monadic bind operator *}
```
```    35
```
```    36 constdefs
```
```    37   bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
```
```    38   "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
```
```    39
```
```    40 syntax ">>=" :: "['a maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'b maybe" (infixl ">>=" 50)
```
```    41 translations "m >>= f" == "bind\<cdot>m\<cdot>f"
```
```    42
```
```    43 nonterminals
```
```    44   maybebind maybebinds
```
```    45
```
```    46 syntax
```
```    47   "_MBIND"  :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind"         ("(2_ <-/ _)" 10)
```
```    48   ""        :: "maybebind \<Rightarrow> maybebinds"                ("_")
```
```    49
```
```    50   "_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds"  ("_;/ _")
```
```    51   "_MDO"    :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe"     ("(do _;/ (_))" 10)
```
```    52
```
```    53 translations
```
```    54   "_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)"
```
```    55   "do (x,y) <- m; e" == "m >>= (LAM <x,y>. e)"
```
```    56   "do x <- m; e"            == "m >>= (LAM x. e)"
```
```    57
```
```    58 text {* monad laws *}
```
```    59
```
```    60 lemma bind_strict [simp]: "UU >>= f = UU"
```
```    61 by (simp add: bind_def)
```
```    62
```
```    63 lemma bind_fail [simp]: "fail >>= f = fail"
```
```    64 by (simp add: bind_def fail_def)
```
```    65
```
```    66 lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a"
```
```    67 by (simp add: bind_def return_def)
```
```    68
```
```    69 lemma right_unit [simp]: "m >>= return = m"
```
```    70 by (rule_tac p=m in maybeE, simp_all)
```
```    71
```
```    72 lemma bind_assoc [simp]:
```
```    73  "(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)"
```
```    74 by (rule_tac p=m in maybeE, simp_all)
```
```    75
```
```    76 subsubsection {* Run operator *}
```
```    77
```
```    78 constdefs
```
```    79   run:: "'a::pcpo maybe \<rightarrow> 'a"
```
```    80   "run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
```
```    81
```
```    82 text {* rewrite rules for run *}
```
```    83
```
```    84 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
```
```    85 by (simp add: run_def)
```
```    86
```
```    87 lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
```
```    88 by (simp add: run_def fail_def)
```
```    89
```
```    90 lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
```
```    91 by (simp add: run_def return_def)
```
```    92
```
```    93 subsubsection {* Monad plus operator *}
```
```    94
```
```    95 constdefs
```
```    96   mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
```
```    97   "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
```
```    98
```
```    99 syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65)
```
```   100 translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2"
```
```   101
```
```   102 text {* rewrite rules for mplus *}
```
```   103
```
```   104 lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
```
```   105 by (simp add: mplus_def)
```
```   106
```
```   107 lemma mplus_fail [simp]: "fail +++ m = m"
```
```   108 by (simp add: mplus_def fail_def)
```
```   109
```
```   110 lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"
```
```   111 by (simp add: mplus_def return_def)
```
```   112
```
```   113 lemma mplus_fail2 [simp]: "m +++ fail = m"
```
```   114 by (rule_tac p=m in maybeE, simp_all)
```
```   115
```
```   116 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
```
```   117 by (rule_tac p=x in maybeE, simp_all)
```
```   118
```
```   119 subsubsection {* Fatbar combinator *}
```
```   120
```
```   121 constdefs
```
```   122   fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)"
```
```   123   "fatbar \<equiv> \<Lambda> a b x. a\<cdot>x +++ b\<cdot>x"
```
```   124
```
```   125 syntax
```
```   126   "\<parallel>" :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)
```
```   127 translations
```
```   128   "m1 \<parallel> m2" == "fatbar\<cdot>m1\<cdot>m2"
```
```   129
```
```   130 lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
```
```   131 by (simp add: fatbar_def)
```
```   132
```
```   133 lemma fatbar2: "m\<cdot>x = fail \<Longrightarrow> (m \<parallel> ms)\<cdot>x = ms\<cdot>x"
```
```   134 by (simp add: fatbar_def)
```
```   135
```
```   136 lemma fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> (m \<parallel> ms)\<cdot>x = return\<cdot>y"
```
```   137 by (simp add: fatbar_def)
```
```   138
```
```   139 lemmas fatbar_simps = fatbar1 fatbar2 fatbar3
```
```   140
```
```   141 subsection {* Pattern combinators *}
```
```   142
```
```   143 types ('a,'b,'c) pattern = "'b \<rightarrow> 'a \<rightarrow> 'c maybe"
```
```   144
```
```   145 constdefs
```
```   146   wild_pat :: "('a, 'b, 'b) pattern"
```
```   147   "wild_pat \<equiv> \<Lambda> r a. return\<cdot>r"
```
```   148
```
```   149   var_pat :: "('a, 'a \<rightarrow> 'b, 'b) pattern"
```
```   150   "var_pat \<equiv> \<Lambda> r a. return\<cdot>(r\<cdot>a)"
```
```   151
```
```   152   as_pat :: "('a, 'b, 'c) pattern \<Rightarrow> ('a, 'a \<rightarrow> 'b, 'c) pattern"
```
```   153   "as_pat p \<equiv> \<Lambda> r a. p\<cdot>(r\<cdot>a)\<cdot>a"
```
```   154
```
```   155 lemma wild_pat [simp]: "wild_pat\<cdot>r\<cdot>a = return\<cdot>r"
```
```   156 by (simp add: wild_pat_def)
```
```   157
```
```   158 lemma var_pat [simp]: "var_pat\<cdot>r\<cdot>a = return\<cdot>(r\<cdot>a)"
```
```   159 by (simp add: var_pat_def)
```
```   160
```
```   161 lemma as_pat [simp]: "as_pat p\<cdot>r\<cdot>a = p\<cdot>(r\<cdot>a)\<cdot>a"
```
```   162 by (simp add: as_pat_def)
```
```   163
```
```   164 subsection {* Case syntax *}
```
```   165
```
```   166 nonterminals
```
```   167   Case_syn  Cases_syn
```
```   168
```
```   169 syntax
```
```   170   "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
```
```   171   "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 10)
```
```   172   ""            :: "Case_syn => Cases_syn"               ("_")
```
```   173   "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
```
```   174   "_as_pattern" :: "[idt, 'a] \<Rightarrow> 'a"                     (* infixr "as" 10 *)
```
```   175
```
```   176 syntax (xsymbols)
```
```   177   "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
```
```   178
```
```   179 syntax
```
```   180   "_match"   :: "'a \<Rightarrow> Case_syn" (* or Cases_syn *)
```
```   181   "_as"      :: "[pttrn, Case_syn] \<Rightarrow> Case_syn"
```
```   182   "_matches" :: "['a, Case_syn, 'a list] \<Rightarrow> Case_syn"
```
```   183   "_cons"    :: "['a, 'a list] \<Rightarrow> 'a list"
```
```   184   "_nil"     :: "'a list"
```
```   185
```
```   186 translations
```
```   187   "_Case_syntax x (_match m)"     == "run\<cdot>(m\<cdot>x)"
```
```   188   "_Case2 (_match c) (_match cs)" == "_match (c \<parallel> cs)"
```
```   189   "_Case1 dummy_pattern r"        == "_match (wild_pat\<cdot>r)"
```
```   190   "_as x (_match (p\<cdot>t))"          == "_match ((as_pat p)\<cdot>(\<Lambda> x. t))"
```
```   191   "_Case1 (_as_pattern x e) r"    == "_as x (_Case1 e r)"
```
```   192   "_Case1 x t"                    == "_match (var_pat\<cdot>(\<Lambda> x. t))"
```
```   193   "_Case1 (f\<cdot>e) r" == "_matches f (_Case1 e r) _nil"
```
```   194   "_matches (f\<cdot>e) (_match (p\<cdot>r)) ps" == "_matches f (_Case1 e r) (_cons p ps)"
```
```   195
```
```   196 lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>"
```
```   197 by (simp add: fatbar_def)
```
```   198
```
```   199 lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)"
```
```   200 by (simp add: fatbar_def)
```
```   201
```
```   202 lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
```
```   203 by (simp add: fatbar_def)
```
```   204
```
```   205 lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
```
```   206
```
```   207 subsection {* Pattern combinators for built-in types *}
```
```   208
```
```   209 constdefs
```
```   210   cpair_pat :: "_"
```
```   211   "cpair_pat p1 p2 \<equiv> \<Lambda> r1 \<langle>x1,x2\<rangle>. bind\<cdot>(p1\<cdot>r1\<cdot>x1)\<cdot>(\<Lambda> r2. p2\<cdot>r2\<cdot>x2)"
```
```   212
```
```   213   spair_pat :: "_"
```
```   214   "spair_pat p1 p2 \<equiv> \<Lambda> r (:x,y:). cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x,y\<rangle>"
```
```   215
```
```   216   sinl_pat :: "_"
```
```   217   "sinl_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x | sinr\<cdot>y \<Rightarrow> fail"
```
```   218
```
```   219   sinr_pat :: "_"
```
```   220   "sinr_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> fail | sinr\<cdot>y \<Rightarrow> p\<cdot>r\<cdot>y"
```
```   221
```
```   222   up_pat :: "_"
```
```   223   "up_pat p \<equiv> \<Lambda> r a. case a of up\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x"
```
```   224
```
```   225   Def_pat :: "'a::type \<Rightarrow> ('a lift, 'b, 'b) pattern"
```
```   226   "Def_pat x \<equiv> \<Lambda> r. FLIFT y. if x = y then return\<cdot>r else fail"
```
```   227
```
```   228   ONE_pat :: "_"
```
```   229   "ONE_pat \<equiv> \<Lambda> r ONE. return\<cdot>r"
```
```   230
```
```   231   TT_pat :: "(tr, _, _) pattern"
```
```   232   "TT_pat \<equiv> \<Lambda> r b. If b then return\<cdot>r else fail fi"
```
```   233
```
```   234   FF_pat :: "(tr, _, _) pattern"
```
```   235   "FF_pat \<equiv> \<Lambda> r b. If b then fail else return\<cdot>r fi"
```
```   236
```
```   237 translations
```
```   238   "_matches cpair (_match (p1\<cdot>r)) (_cons p2 _nil)"
```
```   239     == "_match ((cpair_pat p1 p2)\<cdot>r)"
```
```   240
```
```   241   "_matches spair (_match (p1\<cdot>r)) (_cons p2 _nil)"
```
```   242     == "_match ((spair_pat p1 p2)\<cdot>r)"
```
```   243
```
```   244 translations
```
```   245   "_matches sinl (_match (p1\<cdot>r)) _nil" == "_match ((sinl_pat p1)\<cdot>r)"
```
```   246   "_matches sinr (_match (p1\<cdot>r)) _nil" == "_match ((sinr_pat p1)\<cdot>r)"
```
```   247   "_matches up (_match (p1\<cdot>r)) _nil" == "_match ((up_pat p1)\<cdot>r)"
```
```   248
```
```   249 translations
```
```   250   "_Case1 (Def x) r" == "_match (Def_pat x\<cdot>r)"
```
```   251   "_Case1 ONE r" == "_match (ONE_pat\<cdot>r)"
```
```   252   "_Case1 TT r" == "_match (TT_pat\<cdot>r)"
```
```   253   "_Case1 FF r" == "_match (FF_pat\<cdot>r)"
```
```   254
```
```   255 lemma cpair_pat_simps [simp]:
```
```   256   "p1\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = \<bottom>"
```
```   257   "p1\<cdot>r\<cdot>x = fail \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = fail"
```
```   258   "p1\<cdot>r\<cdot>x = return\<cdot>r' \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = p2\<cdot>r'\<cdot>y"
```
```   259 by (simp_all add: cpair_pat_def)
```
```   260
```
```   261 lemma spair_pat_simps [simp]:
```
```   262   "spair_pat p1 p2\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   263   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> spair_pat p1 p2\<cdot>r\<cdot>(:x, y:) = cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x, y\<rangle>"
```
```   264 by (simp_all add: spair_pat_def)
```
```   265
```
```   266 lemma sinl_pat_simps [simp]:
```
```   267   "sinl_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   268   "x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = p\<cdot>r\<cdot>x"
```
```   269   "x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = fail"
```
```   270 by (simp_all add: sinl_pat_def)
```
```   271
```
```   272 lemma sinr_pat_simps [simp]:
```
```   273   "sinr_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   274   "x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
```
```   275   "x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = p\<cdot>r\<cdot>x"
```
```   276 by (simp_all add: sinr_pat_def)
```
```   277
```
```   278 lemma up_pat_simps [simp]:
```
```   279   "up_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   280   "up_pat p\<cdot>r\<cdot>(up\<cdot>x) = p\<cdot>r\<cdot>x"
```
```   281 by (simp_all add: up_pat_def)
```
```   282
```
```   283 lemma Def_pat_simps [simp]:
```
```   284   "Def_pat x\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   285   "Def_pat x\<cdot>r\<cdot>(Def x) = return\<cdot>r"
```
```   286   "x \<noteq> y \<Longrightarrow> Def_pat x\<cdot>r\<cdot>(Def y) = fail"
```
```   287 by (simp_all add: Def_pat_def)
```
```   288
```
```   289 lemma ONE_pat_simps [simp]:
```
```   290   "ONE_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   291   "ONE_pat\<cdot>r\<cdot>ONE = return\<cdot>r"
```
```   292 by (simp_all add: ONE_pat_def)
```
```   293
```
```   294 lemma TT_pat_simps [simp]:
```
```   295   "TT_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   296   "TT_pat\<cdot>r\<cdot>TT = return\<cdot>r"
```
```   297   "TT_pat\<cdot>r\<cdot>FF = fail"
```
```   298 by (simp_all add: TT_pat_def)
```
```   299
```
```   300 lemma FF_pat_simps [simp]:
```
```   301   "FF_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   302   "FF_pat\<cdot>r\<cdot>TT = fail"
```
```   303   "FF_pat\<cdot>r\<cdot>FF = return\<cdot>r"
```
```   304 by (simp_all add: FF_pat_def)
```
```   305
```
```   306 subsection {* Match functions for built-in types *}
```
```   307
```
```   308 defaultsort pcpo
```
```   309
```
```   310 constdefs
```
```   311   match_UU :: "'a \<rightarrow> unit maybe"
```
```   312   "match_UU \<equiv> \<Lambda> x. fail"
```
```   313
```
```   314   match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe"
```
```   315   "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
```
```   316
```
```   317   match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
```
```   318   "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
```
```   319
```
```   320   match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe"
```
```   321   "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
```
```   322
```
```   323   match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
```
```   324   "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
```
```   325
```
```   326   match_up :: "'a::cpo u \<rightarrow> 'a maybe"
```
```   327   "match_up \<equiv> fup\<cdot>return"
```
```   328
```
```   329   match_ONE :: "one \<rightarrow> unit maybe"
```
```   330   "match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()"
```
```   331
```
```   332   match_TT :: "tr \<rightarrow> unit maybe"
```
```   333   "match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
```
```   334
```
```   335   match_FF :: "tr \<rightarrow> unit maybe"
```
```   336   "match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
```
```   337
```
```   338 lemma match_UU_simps [simp]:
```
```   339   "match_UU\<cdot>x = fail"
```
```   340 by (simp add: match_UU_def)
```
```   341
```
```   342 lemma match_cpair_simps [simp]:
```
```   343   "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
```
```   344 by (simp add: match_cpair_def)
```
```   345
```
```   346 lemma match_spair_simps [simp]:
```
```   347   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>"
```
```   348   "match_spair\<cdot>\<bottom> = \<bottom>"
```
```   349 by (simp_all add: match_spair_def)
```
```   350
```
```   351 lemma match_sinl_simps [simp]:
```
```   352   "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x"
```
```   353   "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail"
```
```   354   "match_sinl\<cdot>\<bottom> = \<bottom>"
```
```   355 by (simp_all add: match_sinl_def)
```
```   356
```
```   357 lemma match_sinr_simps [simp]:
```
```   358   "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x"
```
```   359   "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail"
```
```   360   "match_sinr\<cdot>\<bottom> = \<bottom>"
```
```   361 by (simp_all add: match_sinr_def)
```
```   362
```
```   363 lemma match_up_simps [simp]:
```
```   364   "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
```
```   365   "match_up\<cdot>\<bottom> = \<bottom>"
```
```   366 by (simp_all add: match_up_def)
```
```   367
```
```   368 lemma match_ONE_simps [simp]:
```
```   369   "match_ONE\<cdot>ONE = return\<cdot>()"
```
```   370   "match_ONE\<cdot>\<bottom> = \<bottom>"
```
```   371 by (simp_all add: match_ONE_def)
```
```   372
```
```   373 lemma match_TT_simps [simp]:
```
```   374   "match_TT\<cdot>TT = return\<cdot>()"
```
```   375   "match_TT\<cdot>FF = fail"
```
```   376   "match_TT\<cdot>\<bottom> = \<bottom>"
```
```   377 by (simp_all add: match_TT_def)
```
```   378
```
```   379 lemma match_FF_simps [simp]:
```
```   380   "match_FF\<cdot>FF = return\<cdot>()"
```
```   381   "match_FF\<cdot>TT = fail"
```
```   382   "match_FF\<cdot>\<bottom> = \<bottom>"
```
```   383 by (simp_all add: match_FF_def)
```
```   384
```
```   385 subsection {* Mutual recursion *}
```
```   386
```
```   387 text {*
```
```   388   The following rules are used to prove unfolding theorems from
```
```   389   fixed-point definitions of mutually recursive functions.
```
```   390 *}
```
```   391
```
```   392 lemma cpair_equalI: "\<lbrakk>x \<equiv> cfst\<cdot>p; y \<equiv> csnd\<cdot>p\<rbrakk> \<Longrightarrow> <x,y> \<equiv> p"
```
```   393 by (simp add: surjective_pairing_Cprod2)
```
```   394
```
```   395 lemma cpair_eqD1: "<x,y> = <x',y'> \<Longrightarrow> x = x'"
```
```   396 by simp
```
```   397
```
```   398 lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
```
```   399 by simp
```
```   400
```
```   401 text {* lemma for proving rewrite rules *}
```
```   402
```
```   403 lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
```
```   404 by simp
```
```   405
```
```   406 ML {*
```
```   407 val cpair_equalI = thm "cpair_equalI";
```
```   408 val cpair_eqD1 = thm "cpair_eqD1";
```
```   409 val cpair_eqD2 = thm "cpair_eqD2";
```
```   410 val ssubst_lhs = thm "ssubst_lhs";
```
```   411 *}
```
```   412
```
```   413 subsection {* Initializing the fixrec package *}
```
```   414
```
```   415 use "fixrec_package.ML"
```
```   416
```
```   417 end
```