1.1 --- a/src/HOLCF/Fixrec.thy	Fri Nov 26 14:10:34 2010 -0800
     1.2 +++ b/src/HOLCF/Fixrec.thy	Fri Nov 26 15:11:08 2010 -0800
     1.3 @@ -26,10 +26,6 @@
     1.4    succeed :: "'a \<rightarrow> 'a match" where
     1.5    "succeed = (\<Lambda> x. Abs_match (sinr\<cdot>(up\<cdot>x)))"
     1.6  
     1.7 -definition
     1.8 -  match_case :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a match \<rightarrow> 'b::pcpo" where
     1.9 -  "match_case = (\<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_match m))"
    1.10 -
    1.11  lemma matchE [case_names bottom fail succeed, cases type: match]:
    1.12    "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = succeed\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    1.13  unfolding fail_def succeed_def
    1.14 @@ -52,40 +48,31 @@
    1.15    "succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x"
    1.16  by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject)
    1.17  
    1.18 -lemma match_case_simps [simp]:
    1.19 -  "match_case\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
    1.20 -  "match_case\<cdot>f\<cdot>r\<cdot>fail = f"
    1.21 -  "match_case\<cdot>f\<cdot>r\<cdot>(succeed\<cdot>x) = r\<cdot>x"
    1.22 -by (simp_all add: succeed_def fail_def match_case_def cont_Rep_match
    1.23 -                  cont2cont_LAM
    1.24 -                  cont_Abs_match Abs_match_inverse Rep_match_strict)
    1.25 -
    1.26 -translations
    1.27 -  "case m of XCONST fail \<Rightarrow> t1 | XCONST succeed\<cdot>x \<Rightarrow> t2"
    1.28 -    == "CONST match_case\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
    1.29 -
    1.30  subsubsection {* Run operator *}
    1.31  
    1.32  definition
    1.33    run :: "'a match \<rightarrow> 'a::pcpo" where
    1.34 -  "run = match_case\<cdot>\<bottom>\<cdot>ID"
    1.35 +  "run = (\<Lambda> m. sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)\<cdot>(Rep_match m))"
    1.36  
    1.37  text {* rewrite rules for run *}
    1.38  
    1.39  lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
    1.40 -by (simp add: run_def)
    1.41 +unfolding run_def
    1.42 +by (simp add: cont_Rep_match Rep_match_strict)
    1.43  
    1.44  lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
    1.45 -by (simp add: run_def)
    1.46 +unfolding run_def fail_def
    1.47 +by (simp add: cont_Rep_match Abs_match_inverse)
    1.48  
    1.49  lemma run_succeed [simp]: "run\<cdot>(succeed\<cdot>x) = x"
    1.50 -by (simp add: run_def)
    1.51 +unfolding run_def succeed_def
    1.52 +by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
    1.53  
    1.54  subsubsection {* Monad plus operator *}
    1.55  
    1.56  definition
    1.57    mplus :: "'a match \<rightarrow> 'a match \<rightarrow> 'a match" where
    1.58 -  "mplus = (\<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | succeed\<cdot>x \<Rightarrow> m1)"
    1.59 +  "mplus = (\<Lambda> m1 m2. sscase\<cdot>(\<Lambda> _. m2)\<cdot>(\<Lambda> _. m1)\<cdot>(Rep_match m1))"
    1.60  
    1.61  abbreviation
    1.62    mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match"  (infixr "+++" 65)  where
    1.63 @@ -93,14 +80,19 @@
    1.64  
    1.65  text {* rewrite rules for mplus *}
    1.66  
    1.67 +lemmas cont2cont_Rep_match = cont_Rep_match [THEN cont_compose]
    1.68 +
    1.69  lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
    1.70 -by (simp add: mplus_def)
    1.71 +unfolding mplus_def
    1.72 +by (simp add: cont2cont_Rep_match Rep_match_strict)
    1.73  
    1.74  lemma mplus_fail [simp]: "fail +++ m = m"
    1.75 -by (simp add: mplus_def)
    1.76 +unfolding mplus_def fail_def
    1.77 +by (simp add: cont2cont_Rep_match Abs_match_inverse)
    1.78  
    1.79  lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x"
    1.80 -by (simp add: mplus_def)
    1.81 +unfolding mplus_def succeed_def
    1.82 +by (simp add: cont2cont_Rep_match cont_Abs_match Abs_match_inverse)
    1.83  
    1.84  lemma mplus_fail2 [simp]: "m +++ fail = m"
    1.85  by (cases m, simp_all)

     2.1 --- a/src/HOLCF/ex/Pattern_Match.thy	Fri Nov 26 14:10:34 2010 -0800
     2.2 +++ b/src/HOLCF/ex/Pattern_Match.thy	Fri Nov 26 15:11:08 2010 -0800
     2.3 @@ -53,11 +53,24 @@
     2.4  
     2.5  lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
     2.6  
     2.7 +subsection {* Bind operator for match monad *}
     2.8 +
     2.9 +definition match_bind :: "'a match \<rightarrow> ('a \<rightarrow> 'b match) \<rightarrow> 'b match" where
    2.10 +  "match_bind = (\<Lambda> m k. sscase\<cdot>(\<Lambda> _. fail)\<cdot>(fup\<cdot>k)\<cdot>(Rep_match m))"
    2.11 +
    2.12 +lemma match_bind_simps [simp]:
    2.13 +  "match_bind\<cdot>\<bottom>\<cdot>k = \<bottom>"
    2.14 +  "match_bind\<cdot>fail\<cdot>k = fail"
    2.15 +  "match_bind\<cdot>(succeed\<cdot>x)\<cdot>k = k\<cdot>x"
    2.16 +unfolding match_bind_def fail_def succeed_def
    2.17 +by (simp_all add: cont2cont_Rep_match cont_Abs_match
    2.18 +  Rep_match_strict Abs_match_inverse)
    2.19 +
    2.20  subsection {* Case branch combinator *}
    2.21  
    2.22  definition
    2.23    branch :: "('a \<rightarrow> 'b match) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c match)" where
    2.24 -  "branch p \<equiv> \<Lambda> r x. match_case\<cdot>fail\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))\<cdot>(p\<cdot>x)"
    2.25 +  "branch p \<equiv> \<Lambda> r x. match_bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))"
    2.26  
    2.27  lemma branch_simps:
    2.28    "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
    2.29 @@ -72,7 +85,7 @@
    2.30  
    2.31  definition
    2.32    cases :: "'a match \<rightarrow> 'a::pcpo" where
    2.33 -  "cases = match_case\<cdot>\<bottom>\<cdot>ID"
    2.34 +  "cases = Fixrec.run"
    2.35  
    2.36  text {* rewrite rules for cases *}
    2.37  
    2.38 @@ -165,7 +178,7 @@
    2.39  definition
    2.40    cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
    2.41    "cpair_pat p1 p2 = (\<Lambda>(x, y).
    2.42 -    match_case\<cdot>fail\<cdot>(\<Lambda> a. match_case\<cdot>fail\<cdot>(\<Lambda> b. succeed\<cdot>(a, b))\<cdot>(p2\<cdot>y))\<cdot>(p1\<cdot>x))"
    2.43 +    match_bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. match_bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. succeed\<cdot>(a, b))))"
    2.44  
    2.45  definition
    2.46    spair_pat ::
    2.47 @@ -313,7 +326,7 @@
    2.48  
    2.49  definition
    2.50    as_pat :: "('a \<rightarrow> 'b match) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) match" where
    2.51 -  "as_pat p = (\<Lambda> x. match_case\<cdot>fail\<cdot>(\<Lambda> a. succeed\<cdot>(x, a))\<cdot>(p\<cdot>x))"
    2.52 +  "as_pat p = (\<Lambda> x. match_bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. succeed\<cdot>(x, a)))"
    2.53  
    2.54  definition
    2.55    lazy_pat :: "('a \<rightarrow> 'b::pcpo match) \<Rightarrow> ('a \<rightarrow> 'b match)" where
    2.56 @@ -544,7 +557,7 @@
    2.57            val (fun1, fun2, taken) = pat_lhs (pat, args);
    2.58            val defs = @{thm branch_def} :: pat_defs;
    2.59            val goal = mk_trp (mk_strict fun1);
    2.60 -          val rules = @{thms match_case_simps} @ case_rews;
    2.61 +          val rules = @{thms match_bind_simps} @ case_rews;
    2.62            val tacs = [simp_tac (beta_ss addsimps rules) 1];
    2.63          in prove thy defs goal (K tacs) end;
    2.64        fun pat_apps (i, (pat, (con, args))) =
    2.65 @@ -559,7 +572,7 @@
    2.66                val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
    2.67                val goal = Logic.list_implies (assms, concl);
    2.68                val defs = @{thm branch_def} :: pat_defs;
    2.69 -              val rules = @{thms match_case_simps} @ case_rews;
    2.70 +              val rules = @{thms match_bind_simps} @ case_rews;
    2.71                val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
    2.72              in prove thy defs goal (K tacs) end;
    2.73          in map_index pat_app spec end;