src/HOLCF/Fixrec.thy
changeset 16460 72a08d509d62
parent 16417 9bc16273c2d4
child 16463 342d74ca8815
     1.1 --- a/src/HOLCF/Fixrec.thy	Fri Jun 17 18:36:25 2005 +0200
     1.2 +++ b/src/HOLCF/Fixrec.thy	Fri Jun 17 18:50:40 2005 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header "Package for defining recursive functions in HOLCF"
     1.5  
     1.6  theory Fixrec
     1.7 -imports Ssum One Up Fix
     1.8 +imports Ssum One Up Fix Tr
     1.9  uses ("fixrec_package.ML")
    1.10  begin
    1.11  
    1.12 @@ -111,6 +111,9 @@
    1.13  lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"
    1.14  by (simp add: mplus_def return_def)
    1.15  
    1.16 +lemma mplus_fail2 [simp]: "m +++ fail = m"
    1.17 +by (rule_tac p=m in maybeE, simp_all)
    1.18 +
    1.19  lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
    1.20  by (rule_tac p=x in maybeE, simp_all)
    1.21  
    1.22 @@ -125,6 +128,15 @@
    1.23    match_up :: "'a u \<rightarrow> 'a maybe"
    1.24    "match_up \<equiv> fup\<cdot>return"
    1.25  
    1.26 +  match_ONE :: "one \<rightarrow> unit maybe"
    1.27 +  "match_ONE \<equiv> flift1 (\<lambda>u. return\<cdot>())"
    1.28 +
    1.29 +  match_TT :: "tr \<rightarrow> unit maybe"
    1.30 +  "match_TT \<equiv> flift1 (\<lambda>b. if b then return\<cdot>() else fail)"
    1.31 +
    1.32 +  match_FF :: "tr \<rightarrow> unit maybe"
    1.33 +  "match_FF \<equiv> flift1 (\<lambda>b. if b then fail else return\<cdot>())"
    1.34 +
    1.35  lemma match_cpair_simps [simp]:
    1.36    "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
    1.37  by (simp add: match_cpair_def)
    1.38 @@ -134,6 +146,23 @@
    1.39    "match_up\<cdot>\<bottom> = \<bottom>"
    1.40  by (simp_all add: match_up_def)
    1.41  
    1.42 +lemma match_ONE_simps [simp]:
    1.43 +  "match_ONE\<cdot>ONE = return\<cdot>()"
    1.44 +  "match_ONE\<cdot>\<bottom> = \<bottom>"
    1.45 +by (simp_all add: ONE_def match_ONE_def)
    1.46 +
    1.47 +lemma match_TT_simps [simp]:
    1.48 +  "match_TT\<cdot>TT = return\<cdot>()"
    1.49 +  "match_TT\<cdot>FF = fail"
    1.50 +  "match_TT\<cdot>\<bottom> = \<bottom>"
    1.51 +by (simp_all add: TT_def FF_def match_TT_def)
    1.52 +
    1.53 +lemma match_FF_simps [simp]:
    1.54 +  "match_FF\<cdot>FF = return\<cdot>()"
    1.55 +  "match_FF\<cdot>TT = fail"
    1.56 +  "match_FF\<cdot>\<bottom> = \<bottom>"
    1.57 +by (simp_all add: TT_def FF_def match_FF_def)
    1.58 +
    1.59  subsection {* Mutual recursion *}
    1.60  
    1.61  text {*