src/HOLCF/Fixrec.thy
changeset 31008 b8f4e351b5bf
parent 30914 ceeb5f2eac75
child 31095 b79d140f6d0b
     1.1 --- a/src/HOLCF/Fixrec.thy	Mon Apr 27 07:26:17 2009 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Mon Apr 27 19:44:30 2009 -0700
     1.3 @@ -520,8 +520,9 @@
     1.4    "match_FF = (\<Lambda> x k. If x then fail else k fi)"
     1.5  
     1.6  lemma match_UU_simps [simp]:
     1.7 -  "match_UU\<cdot>x\<cdot>k = (if x = \<bottom> then \<bottom> else fail)"
     1.8 -by (simp add: match_UU_def)
     1.9 +  "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
    1.10 +  "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
    1.11 +by (simp_all add: match_UU_def)
    1.12  
    1.13  lemma match_cpair_simps [simp]:
    1.14    "match_cpair\<cdot>\<langle>x, y\<rangle>\<cdot>k = k\<cdot>x\<cdot>y"
    1.15 @@ -603,7 +604,8 @@
    1.16        (@{const_name cpair}, @{const_name match_cpair}),
    1.17        (@{const_name ONE}, @{const_name match_ONE}),
    1.18        (@{const_name TT}, @{const_name match_TT}),
    1.19 -      (@{const_name FF}, @{const_name match_FF}) ]
    1.20 +      (@{const_name FF}, @{const_name match_FF}),
    1.21 +      (@{const_name UU}, @{const_name match_UU}) ]
    1.22  *}
    1.23  
    1.24  hide (open) const return bind fail run cases