src/HOLCF/Fixrec.thy
 author huffman Mon May 11 08:28:09 2009 -0700 (2009-05-11) changeset 31095 b79d140f6d0b parent 31008 b8f4e351b5bf child 31738 7b9b9ba532ca permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
```     1 (*  Title:      HOLCF/Fixrec.thy
```
```     2     Author:     Amber Telfer and Brian Huffman
```
```     3 *)
```
```     4
```
```     5 header "Package for defining recursive functions in HOLCF"
```
```     6
```
```     7 theory Fixrec
```
```     8 imports Sprod Ssum Up One Tr Fix
```
```     9 uses ("Tools/fixrec_package.ML")
```
```    10 begin
```
```    11
```
```    12 subsection {* Maybe monad type *}
```
```    13
```
```    14 defaultsort cpo
```
```    15
```
```    16 pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set"
```
```    17 by simp_all
```
```    18
```
```    19 definition
```
```    20   fail :: "'a maybe" where
```
```    21   "fail = Abs_maybe (sinl\<cdot>ONE)"
```
```    22
```
```    23 definition
```
```    24   return :: "'a \<rightarrow> 'a maybe" where
```
```    25   "return = (\<Lambda> x. Abs_maybe (sinr\<cdot>(up\<cdot>x)))"
```
```    26
```
```    27 definition
```
```    28   maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo" where
```
```    29   "maybe_when = (\<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_maybe m))"
```
```    30
```
```    31 lemma maybeE:
```
```    32   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
```
```    33 apply (unfold fail_def return_def)
```
```    34 apply (cases p, rename_tac r)
```
```    35 apply (rule_tac p=r in ssumE, simp add: Abs_maybe_strict)
```
```    36 apply (rule_tac p=x in oneE, simp, simp)
```
```    37 apply (rule_tac p=y in upE, simp, simp add: cont_Abs_maybe)
```
```    38 done
```
```    39
```
```    40 lemma return_defined [simp]: "return\<cdot>x \<noteq> \<bottom>"
```
```    41 by (simp add: return_def cont_Abs_maybe Abs_maybe_defined)
```
```    42
```
```    43 lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
```
```    44 by (simp add: fail_def Abs_maybe_defined)
```
```    45
```
```    46 lemma return_eq [simp]: "(return\<cdot>x = return\<cdot>y) = (x = y)"
```
```    47 by (simp add: return_def cont_Abs_maybe Abs_maybe_inject)
```
```    48
```
```    49 lemma return_neq_fail [simp]:
```
```    50   "return\<cdot>x \<noteq> fail" "fail \<noteq> return\<cdot>x"
```
```    51 by (simp_all add: return_def fail_def cont_Abs_maybe Abs_maybe_inject)
```
```    52
```
```    53 lemma maybe_when_rews [simp]:
```
```    54   "maybe_when\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```    55   "maybe_when\<cdot>f\<cdot>r\<cdot>fail = f"
```
```    56   "maybe_when\<cdot>f\<cdot>r\<cdot>(return\<cdot>x) = r\<cdot>x"
```
```    57 by (simp_all add: return_def fail_def maybe_when_def cont_Rep_maybe
```
```    58                   cont2cont_LAM
```
```    59                   cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
```
```    60
```
```    61 translations
```
```    62   "case m of XCONST fail \<Rightarrow> t1 | XCONST return\<cdot>x \<Rightarrow> t2"
```
```    63     == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
```
```    64
```
```    65
```
```    66 subsubsection {* Monadic bind operator *}
```
```    67
```
```    68 definition
```
```    69   bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" where
```
```    70   "bind = (\<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x)"
```
```    71
```
```    72 text {* monad laws *}
```
```    73
```
```    74 lemma bind_strict [simp]: "bind\<cdot>\<bottom>\<cdot>f = \<bottom>"
```
```    75 by (simp add: bind_def)
```
```    76
```
```    77 lemma bind_fail [simp]: "bind\<cdot>fail\<cdot>f = fail"
```
```    78 by (simp add: bind_def)
```
```    79
```
```    80 lemma left_unit [simp]: "bind\<cdot>(return\<cdot>a)\<cdot>k = k\<cdot>a"
```
```    81 by (simp add: bind_def)
```
```    82
```
```    83 lemma right_unit [simp]: "bind\<cdot>m\<cdot>return = m"
```
```    84 by (rule_tac p=m in maybeE, simp_all)
```
```    85
```
```    86 lemma bind_assoc:
```
```    87  "bind\<cdot>(bind\<cdot>m\<cdot>k)\<cdot>h = bind\<cdot>m\<cdot>(\<Lambda> a. bind\<cdot>(k\<cdot>a)\<cdot>h)"
```
```    88 by (rule_tac p=m in maybeE, simp_all)
```
```    89
```
```    90 subsubsection {* Run operator *}
```
```    91
```
```    92 definition
```
```    93   run :: "'a maybe \<rightarrow> 'a::pcpo" where
```
```    94   "run = maybe_when\<cdot>\<bottom>\<cdot>ID"
```
```    95
```
```    96 text {* rewrite rules for run *}
```
```    97
```
```    98 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
```
```    99 by (simp add: run_def)
```
```   100
```
```   101 lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
```
```   102 by (simp add: run_def)
```
```   103
```
```   104 lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
```
```   105 by (simp add: run_def)
```
```   106
```
```   107 subsubsection {* Monad plus operator *}
```
```   108
```
```   109 definition
```
```   110   mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" where
```
```   111   "mplus = (\<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | return\<cdot>x \<Rightarrow> m1)"
```
```   112
```
```   113 abbreviation
```
```   114   mplus_syn :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe"  (infixr "+++" 65)  where
```
```   115   "m1 +++ m2 == mplus\<cdot>m1\<cdot>m2"
```
```   116
```
```   117 text {* rewrite rules for mplus *}
```
```   118
```
```   119 lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
```
```   120 by (simp add: mplus_def)
```
```   121
```
```   122 lemma mplus_fail [simp]: "fail +++ m = m"
```
```   123 by (simp add: mplus_def)
```
```   124
```
```   125 lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"
```
```   126 by (simp add: mplus_def)
```
```   127
```
```   128 lemma mplus_fail2 [simp]: "m +++ fail = m"
```
```   129 by (rule_tac p=m in maybeE, simp_all)
```
```   130
```
```   131 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
```
```   132 by (rule_tac p=x in maybeE, simp_all)
```
```   133
```
```   134 subsubsection {* Fatbar combinator *}
```
```   135
```
```   136 definition
```
```   137   fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)" where
```
```   138   "fatbar = (\<Lambda> a b x. a\<cdot>x +++ b\<cdot>x)"
```
```   139
```
```   140 abbreviation
```
```   141   fatbar_syn :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)  where
```
```   142   "m1 \<parallel> m2 == fatbar\<cdot>m1\<cdot>m2"
```
```   143
```
```   144 lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
```
```   145 by (simp add: fatbar_def)
```
```   146
```
```   147 lemma fatbar2: "m\<cdot>x = fail \<Longrightarrow> (m \<parallel> ms)\<cdot>x = ms\<cdot>x"
```
```   148 by (simp add: fatbar_def)
```
```   149
```
```   150 lemma fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> (m \<parallel> ms)\<cdot>x = return\<cdot>y"
```
```   151 by (simp add: fatbar_def)
```
```   152
```
```   153 lemmas fatbar_simps = fatbar1 fatbar2 fatbar3
```
```   154
```
```   155 lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>"
```
```   156 by (simp add: fatbar_def)
```
```   157
```
```   158 lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)"
```
```   159 by (simp add: fatbar_def)
```
```   160
```
```   161 lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
```
```   162 by (simp add: fatbar_def)
```
```   163
```
```   164 lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
```
```   165
```
```   166 subsection {* Case branch combinator *}
```
```   167
```
```   168 definition
```
```   169   branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)" where
```
```   170   "branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))"
```
```   171
```
```   172 lemma branch_rews:
```
```   173   "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
```
```   174   "p\<cdot>x = fail \<Longrightarrow> branch p\<cdot>r\<cdot>x = fail"
```
```   175   "p\<cdot>x = return\<cdot>y \<Longrightarrow> branch p\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>y)"
```
```   176 by (simp_all add: branch_def)
```
```   177
```
```   178 lemma branch_return [simp]: "branch return\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>x)"
```
```   179 by (simp add: branch_def)
```
```   180
```
```   181 subsubsection {* Cases operator *}
```
```   182
```
```   183 definition
```
```   184   cases :: "'a maybe \<rightarrow> 'a::pcpo" where
```
```   185   "cases = maybe_when\<cdot>\<bottom>\<cdot>ID"
```
```   186
```
```   187 text {* rewrite rules for cases *}
```
```   188
```
```   189 lemma cases_strict [simp]: "cases\<cdot>\<bottom> = \<bottom>"
```
```   190 by (simp add: cases_def)
```
```   191
```
```   192 lemma cases_fail [simp]: "cases\<cdot>fail = \<bottom>"
```
```   193 by (simp add: cases_def)
```
```   194
```
```   195 lemma cases_return [simp]: "cases\<cdot>(return\<cdot>x) = x"
```
```   196 by (simp add: cases_def)
```
```   197
```
```   198 subsection {* Case syntax *}
```
```   199
```
```   200 nonterminals
```
```   201   Case_syn  Cases_syn
```
```   202
```
```   203 syntax
```
```   204   "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
```
```   205   "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 10)
```
```   206   ""            :: "Case_syn => Cases_syn"               ("_")
```
```   207   "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
```
```   208
```
```   209 syntax (xsymbols)
```
```   210   "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
```
```   211
```
```   212 translations
```
```   213   "_Case_syntax x ms" == "CONST Fixrec.cases\<cdot>(ms\<cdot>x)"
```
```   214   "_Case2 m ms" == "m \<parallel> ms"
```
```   215
```
```   216 text {* Parsing Case expressions *}
```
```   217
```
```   218 syntax
```
```   219   "_pat" :: "'a"
```
```   220   "_variable" :: "'a"
```
```   221   "_noargs" :: "'a"
```
```   222
```
```   223 translations
```
```   224   "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_variable p r)"
```
```   225   "_variable (_args x y) r" => "CONST csplit\<cdot>(_variable x (_variable y r))"
```
```   226   "_variable _noargs r" => "CONST unit_when\<cdot>r"
```
```   227
```
```   228 parse_translation {*
```
```   229 (* rewrites (_pat x) => (return) *)
```
```   230 (* rewrites (_variable x t) => (Abs_CFun (%x. t)) *)
```
```   231   [("_pat", K (Syntax.const "Fixrec.return")),
```
```   232    mk_binder_tr ("_variable", "Abs_CFun")];
```
```   233 *}
```
```   234
```
```   235 text {* Printing Case expressions *}
```
```   236
```
```   237 syntax
```
```   238   "_match" :: "'a"
```
```   239
```
```   240 print_translation {*
```
```   241   let
```
```   242     fun dest_LAM (Const (@{const_syntax Rep_CFun},_) \$ Const (@{const_syntax unit_when},_) \$ t) =
```
```   243           (Syntax.const "_noargs", t)
```
```   244     |   dest_LAM (Const (@{const_syntax Rep_CFun},_) \$ Const (@{const_syntax csplit},_) \$ t) =
```
```   245           let
```
```   246             val (v1, t1) = dest_LAM t;
```
```   247             val (v2, t2) = dest_LAM t1;
```
```   248           in (Syntax.const "_args" \$ v1 \$ v2, t2) end
```
```   249     |   dest_LAM (Const (@{const_syntax Abs_CFun},_) \$ t) =
```
```   250           let
```
```   251             val abs = case t of Abs abs => abs
```
```   252                 | _ => ("x", dummyT, incr_boundvars 1 t \$ Bound 0);
```
```   253             val (x, t') = atomic_abs_tr' abs;
```
```   254           in (Syntax.const "_variable" \$ x, t') end
```
```   255     |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
```
```   256
```
```   257     fun Case1_tr' [Const(@{const_syntax branch},_) \$ p, r] =
```
```   258           let val (v, t) = dest_LAM r;
```
```   259           in Syntax.const "_Case1" \$ (Syntax.const "_match" \$ p \$ v) \$ t end;
```
```   260
```
```   261   in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
```
```   262 *}
```
```   263
```
```   264 translations
```
```   265   "x" <= "_match Fixrec.return (_variable x)"
```
```   266
```
```   267
```
```   268 subsection {* Pattern combinators for data constructors *}
```
```   269
```
```   270 types ('a, 'b) pat = "'a \<rightarrow> 'b maybe"
```
```   271
```
```   272 definition
```
```   273   cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
```
```   274   "cpair_pat p1 p2 = (\<Lambda>\<langle>x, y\<rangle>.
```
```   275     bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>)))"
```
```   276
```
```   277 definition
```
```   278   spair_pat ::
```
```   279   "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat" where
```
```   280   "spair_pat p1 p2 = (\<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>)"
```
```   281
```
```   282 definition
```
```   283   sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
```
```   284   "sinl_pat p = sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
```
```   285
```
```   286 definition
```
```   287   sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
```
```   288   "sinr_pat p = sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
```
```   289
```
```   290 definition
```
```   291   up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat" where
```
```   292   "up_pat p = fup\<cdot>p"
```
```   293
```
```   294 definition
```
```   295   TT_pat :: "(tr, unit) pat" where
```
```   296   "TT_pat = (\<Lambda> b. If b then return\<cdot>() else fail fi)"
```
```   297
```
```   298 definition
```
```   299   FF_pat :: "(tr, unit) pat" where
```
```   300   "FF_pat = (\<Lambda> b. If b then fail else return\<cdot>() fi)"
```
```   301
```
```   302 definition
```
```   303   ONE_pat :: "(one, unit) pat" where
```
```   304   "ONE_pat = (\<Lambda> ONE. return\<cdot>())"
```
```   305
```
```   306 text {* Parse translations (patterns) *}
```
```   307 translations
```
```   308   "_pat (XCONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
```
```   309   "_pat (XCONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
```
```   310   "_pat (XCONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
```
```   311   "_pat (XCONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
```
```   312   "_pat (XCONST up\<cdot>x)" => "CONST up_pat (_pat x)"
```
```   313   "_pat (XCONST TT)" => "CONST TT_pat"
```
```   314   "_pat (XCONST FF)" => "CONST FF_pat"
```
```   315   "_pat (XCONST ONE)" => "CONST ONE_pat"
```
```   316
```
```   317 text {* CONST version is also needed for constructors with special syntax *}
```
```   318 translations
```
```   319   "_pat (CONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
```
```   320   "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
```
```   321
```
```   322 text {* Parse translations (variables) *}
```
```   323 translations
```
```   324   "_variable (XCONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
```
```   325   "_variable (XCONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
```
```   326   "_variable (XCONST sinl\<cdot>x) r" => "_variable x r"
```
```   327   "_variable (XCONST sinr\<cdot>x) r" => "_variable x r"
```
```   328   "_variable (XCONST up\<cdot>x) r" => "_variable x r"
```
```   329   "_variable (XCONST TT) r" => "_variable _noargs r"
```
```   330   "_variable (XCONST FF) r" => "_variable _noargs r"
```
```   331   "_variable (XCONST ONE) r" => "_variable _noargs r"
```
```   332
```
```   333 translations
```
```   334   "_variable (CONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
```
```   335   "_variable (CONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
```
```   336
```
```   337 text {* Print translations *}
```
```   338 translations
```
```   339   "CONST cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
```
```   340       <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)"
```
```   341   "CONST spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
```
```   342       <= "_match (CONST spair_pat p1 p2) (_args v1 v2)"
```
```   343   "CONST sinl\<cdot>(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1"
```
```   344   "CONST sinr\<cdot>(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1"
```
```   345   "CONST up\<cdot>(_match p1 v1)" <= "_match (CONST up_pat p1) v1"
```
```   346   "CONST TT" <= "_match (CONST TT_pat) _noargs"
```
```   347   "CONST FF" <= "_match (CONST FF_pat) _noargs"
```
```   348   "CONST ONE" <= "_match (CONST ONE_pat) _noargs"
```
```   349
```
```   350 lemma cpair_pat1:
```
```   351   "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
```
```   352 apply (simp add: branch_def cpair_pat_def)
```
```   353 apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
```
```   354 done
```
```   355
```
```   356 lemma cpair_pat2:
```
```   357   "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = fail"
```
```   358 apply (simp add: branch_def cpair_pat_def)
```
```   359 apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
```
```   360 done
```
```   361
```
```   362 lemma cpair_pat3:
```
```   363   "branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow>
```
```   364    branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = branch q\<cdot>s\<cdot>y"
```
```   365 apply (simp add: branch_def cpair_pat_def)
```
```   366 apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
```
```   367 apply (rule_tac p="q\<cdot>y" in maybeE, simp_all)
```
```   368 done
```
```   369
```
```   370 lemmas cpair_pat [simp] =
```
```   371   cpair_pat1 cpair_pat2 cpair_pat3
```
```   372
```
```   373 lemma spair_pat [simp]:
```
```   374   "branch (spair_pat p1 p2)\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   375   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk>
```
```   376      \<Longrightarrow> branch (spair_pat p1 p2)\<cdot>r\<cdot>(:x, y:) =
```
```   377          branch (cpair_pat p1 p2)\<cdot>r\<cdot>\<langle>x, y\<rangle>"
```
```   378 by (simp_all add: branch_def spair_pat_def)
```
```   379
```
```   380 lemma sinl_pat [simp]:
```
```   381   "branch (sinl_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   382   "x \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = branch p\<cdot>r\<cdot>x"
```
```   383   "y \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = fail"
```
```   384 by (simp_all add: branch_def sinl_pat_def)
```
```   385
```
```   386 lemma sinr_pat [simp]:
```
```   387   "branch (sinr_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   388   "x \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
```
```   389   "y \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = branch p\<cdot>r\<cdot>y"
```
```   390 by (simp_all add: branch_def sinr_pat_def)
```
```   391
```
```   392 lemma up_pat [simp]:
```
```   393   "branch (up_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
```
```   394   "branch (up_pat p)\<cdot>r\<cdot>(up\<cdot>x) = branch p\<cdot>r\<cdot>x"
```
```   395 by (simp_all add: branch_def up_pat_def)
```
```   396
```
```   397 lemma TT_pat [simp]:
```
```   398   "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
```
```   399   "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = return\<cdot>r"
```
```   400   "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = fail"
```
```   401 by (simp_all add: branch_def TT_pat_def)
```
```   402
```
```   403 lemma FF_pat [simp]:
```
```   404   "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
```
```   405   "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = fail"
```
```   406   "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = return\<cdot>r"
```
```   407 by (simp_all add: branch_def FF_pat_def)
```
```   408
```
```   409 lemma ONE_pat [simp]:
```
```   410   "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
```
```   411   "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>ONE = return\<cdot>r"
```
```   412 by (simp_all add: branch_def ONE_pat_def)
```
```   413
```
```   414
```
```   415 subsection {* Wildcards, as-patterns, and lazy patterns *}
```
```   416
```
```   417 syntax
```
```   418   "_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10)
```
```   419   "_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000)
```
```   420
```
```   421 definition
```
```   422   wild_pat :: "'a \<rightarrow> unit maybe" where
```
```   423   "wild_pat = (\<Lambda> x. return\<cdot>())"
```
```   424
```
```   425 definition
```
```   426   as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" where
```
```   427   "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>))"
```
```   428
```
```   429 definition
```
```   430   lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
```
```   431   "lazy_pat p = (\<Lambda> x. return\<cdot>(cases\<cdot>(p\<cdot>x)))"
```
```   432
```
```   433 text {* Parse translations (patterns) *}
```
```   434 translations
```
```   435   "_pat _" => "CONST wild_pat"
```
```   436   "_pat (_as_pat x y)" => "CONST as_pat (_pat y)"
```
```   437   "_pat (_lazy_pat x)" => "CONST lazy_pat (_pat x)"
```
```   438
```
```   439 text {* Parse translations (variables) *}
```
```   440 translations
```
```   441   "_variable _ r" => "_variable _noargs r"
```
```   442   "_variable (_as_pat x y) r" => "_variable (_args x y) r"
```
```   443   "_variable (_lazy_pat x) r" => "_variable x r"
```
```   444
```
```   445 text {* Print translations *}
```
```   446 translations
```
```   447   "_" <= "_match (CONST wild_pat) _noargs"
```
```   448   "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_variable x) v)"
```
```   449   "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
```
```   450
```
```   451 text {* Lazy patterns in lambda abstractions *}
```
```   452 translations
```
```   453   "_cabs (_lazy_pat p) r" == "CONST Fixrec.cases oo (_Case1 (_lazy_pat p) r)"
```
```   454
```
```   455 lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
```
```   456 by (simp add: branch_def wild_pat_def)
```
```   457
```
```   458 lemma as_pat [simp]:
```
```   459   "branch (as_pat p)\<cdot>(csplit\<cdot>r)\<cdot>x = branch p\<cdot>(r\<cdot>x)\<cdot>x"
```
```   460 apply (simp add: branch_def as_pat_def)
```
```   461 apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
```
```   462 done
```
```   463
```
```   464 lemma lazy_pat [simp]:
```
```   465   "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>\<bottom>)"
```
```   466   "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>\<bottom>)"
```
```   467   "branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>s"
```
```   468 apply (simp_all add: branch_def lazy_pat_def)
```
```   469 apply (rule_tac [!] p="p\<cdot>x" in maybeE, simp_all)
```
```   470 done
```
```   471
```
```   472
```
```   473 subsection {* Match functions for built-in types *}
```
```   474
```
```   475 defaultsort pcpo
```
```   476
```
```   477 definition
```
```   478   match_UU :: "'a \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
```
```   479 where
```
```   480   "match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
```
```   481
```
```   482 definition
```
```   483   match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
```
```   484 where
```
```   485   "match_cpair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
```
```   486
```
```   487 definition
```
```   488   match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
```
```   489 where
```
```   490   "match_spair = (\<Lambda> x k. ssplit\<cdot>k\<cdot>x)"
```
```   491
```
```   492 definition
```
```   493   match_sinl :: "'a \<oplus> 'b \<rightarrow> ('a \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
```
```   494 where
```
```   495   "match_sinl = (\<Lambda> x k. sscase\<cdot>k\<cdot>(\<Lambda> b. fail)\<cdot>x)"
```
```   496
```
```   497 definition
```
```   498   match_sinr :: "'a \<oplus> 'b \<rightarrow> ('b \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
```
```   499 where
```
```   500   "match_sinr = (\<Lambda> x k. sscase\<cdot>(\<Lambda> a. fail)\<cdot>k\<cdot>x)"
```
```   501
```
```   502 definition
```
```   503   match_up :: "'a::cpo u \<rightarrow> ('a \<rightarrow> 'c maybe) \<rightarrow> 'c maybe"
```
```   504 where
```
```   505   "match_up = (\<Lambda> x k. fup\<cdot>k\<cdot>x)"
```
```   506
```
```   507 definition
```
```   508   match_ONE :: "one \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
```
```   509 where
```
```   510   "match_ONE = (\<Lambda> ONE k. k)"
```
```   511
```
```   512 definition
```
```   513   match_TT :: "tr \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
```
```   514 where
```
```   515   "match_TT = (\<Lambda> x k. If x then k else fail fi)"
```
```   516
```
```   517 definition
```
```   518   match_FF :: "tr \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
```
```   519 where
```
```   520   "match_FF = (\<Lambda> x k. If x then fail else k fi)"
```
```   521
```
```   522 lemma match_UU_simps [simp]:
```
```   523   "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
```
```   524   "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
```
```   525 by (simp_all add: match_UU_def)
```
```   526
```
```   527 lemma match_cpair_simps [simp]:
```
```   528   "match_cpair\<cdot>\<langle>x, y\<rangle>\<cdot>k = k\<cdot>x\<cdot>y"
```
```   529 by (simp add: match_cpair_def)
```
```   530
```
```   531 lemma match_spair_simps [simp]:
```
```   532   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x, y:)\<cdot>k = k\<cdot>x\<cdot>y"
```
```   533   "match_spair\<cdot>\<bottom>\<cdot>k = \<bottom>"
```
```   534 by (simp_all add: match_spair_def)
```
```   535
```
```   536 lemma match_sinl_simps [simp]:
```
```   537   "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x)\<cdot>k = k\<cdot>x"
```
```   538   "y \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>y)\<cdot>k = fail"
```
```   539   "match_sinl\<cdot>\<bottom>\<cdot>k = \<bottom>"
```
```   540 by (simp_all add: match_sinl_def)
```
```   541
```
```   542 lemma match_sinr_simps [simp]:
```
```   543   "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x)\<cdot>k = fail"
```
```   544   "y \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>y)\<cdot>k = k\<cdot>y"
```
```   545   "match_sinr\<cdot>\<bottom>\<cdot>k = \<bottom>"
```
```   546 by (simp_all add: match_sinr_def)
```
```   547
```
```   548 lemma match_up_simps [simp]:
```
```   549   "match_up\<cdot>(up\<cdot>x)\<cdot>k = k\<cdot>x"
```
```   550   "match_up\<cdot>\<bottom>\<cdot>k = \<bottom>"
```
```   551 by (simp_all add: match_up_def)
```
```   552
```
```   553 lemma match_ONE_simps [simp]:
```
```   554   "match_ONE\<cdot>ONE\<cdot>k = k"
```
```   555   "match_ONE\<cdot>\<bottom>\<cdot>k = \<bottom>"
```
```   556 by (simp_all add: match_ONE_def)
```
```   557
```
```   558 lemma match_TT_simps [simp]:
```
```   559   "match_TT\<cdot>TT\<cdot>k = k"
```
```   560   "match_TT\<cdot>FF\<cdot>k = fail"
```
```   561   "match_TT\<cdot>\<bottom>\<cdot>k = \<bottom>"
```
```   562 by (simp_all add: match_TT_def)
```
```   563
```
```   564 lemma match_FF_simps [simp]:
```
```   565   "match_FF\<cdot>FF\<cdot>k = k"
```
```   566   "match_FF\<cdot>TT\<cdot>k = fail"
```
```   567   "match_FF\<cdot>\<bottom>\<cdot>k = \<bottom>"
```
```   568 by (simp_all add: match_FF_def)
```
```   569
```
```   570 subsection {* Mutual recursion *}
```
```   571
```
```   572 text {*
```
```   573   The following rules are used to prove unfolding theorems from
```
```   574   fixed-point definitions of mutually recursive functions.
```
```   575 *}
```
```   576
```
```   577 lemma Pair_equalI: "\<lbrakk>x \<equiv> fst p; y \<equiv> snd p\<rbrakk> \<Longrightarrow> (x, y) \<equiv> p"
```
```   578 by simp
```
```   579
```
```   580 lemma Pair_eqD1: "(x, y) = (x', y') \<Longrightarrow> x = x'"
```
```   581 by simp
```
```   582
```
```   583 lemma Pair_eqD2: "(x, y) = (x', y') \<Longrightarrow> y = y'"
```
```   584 by simp
```
```   585
```
```   586 lemma def_cont_fix_eq:
```
```   587   "\<lbrakk>f \<equiv> fix\<cdot>(Abs_CFun F); cont F\<rbrakk> \<Longrightarrow> f = F f"
```
```   588 by (simp, subst fix_eq, simp)
```
```   589
```
```   590 lemma def_cont_fix_ind:
```
```   591   "\<lbrakk>f \<equiv> fix\<cdot>(Abs_CFun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
```
```   592 by (simp add: fix_ind)
```
```   593
```
```   594 text {* lemma for proving rewrite rules *}
```
```   595
```
```   596 lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
```
```   597 by simp
```
```   598
```
```   599
```
```   600 subsection {* Initializing the fixrec package *}
```
```   601
```
```   602 use "Tools/fixrec_package.ML"
```
```   603
```
```   604 setup {* FixrecPackage.setup *}
```
```   605
```
```   606 setup {*
```
```   607   FixrecPackage.add_matchers
```
```   608     [ (@{const_name up}, @{const_name match_up}),
```
```   609       (@{const_name sinl}, @{const_name match_sinl}),
```
```   610       (@{const_name sinr}, @{const_name match_sinr}),
```
```   611       (@{const_name spair}, @{const_name match_spair}),
```
```   612       (@{const_name cpair}, @{const_name match_cpair}),
```
```   613       (@{const_name ONE}, @{const_name match_ONE}),
```
```   614       (@{const_name TT}, @{const_name match_TT}),
```
```   615       (@{const_name FF}, @{const_name match_FF}),
```
```   616       (@{const_name UU}, @{const_name match_UU}) ]
```
```   617 *}
```
```   618
```
```   619 hide (open) const return bind fail run cases
```
```   620
```
```   621 end
```