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