src/HOLCF/Fixrec.thy
changeset 16551 7abf8a713613
parent 16463 342d74ca8815
child 16754 1b979f8b7e8e
     1.1 --- a/src/HOLCF/Fixrec.thy	Thu Jun 23 19:40:03 2005 +0200
     1.2 +++ b/src/HOLCF/Fixrec.thy	Thu Jun 23 21:17:26 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 Tr
     1.8 +imports Sprod Ssum Up One Tr Fix
     1.9  uses ("fixrec_package.ML")
    1.10  begin
    1.11  
    1.12 @@ -119,12 +119,19 @@
    1.13  
    1.14  subsection {* Match functions for built-in types *}
    1.15  
    1.16 -text {* Currently the package only supports lazy constructors *}
    1.17 -
    1.18  constdefs
    1.19    match_cpair :: "'a \<times> 'b \<rightarrow> ('a \<times> 'b) maybe"
    1.20    "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
    1.21  
    1.22 +  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
    1.23 +  "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
    1.24 +
    1.25 +  match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe"
    1.26 +  "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
    1.27 +
    1.28 +  match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
    1.29 +  "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
    1.30 +
    1.31    match_up :: "'a u \<rightarrow> 'a maybe"
    1.32    "match_up \<equiv> fup\<cdot>return"
    1.33  
    1.34 @@ -141,6 +148,23 @@
    1.35    "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
    1.36  by (simp add: match_cpair_def)
    1.37  
    1.38 +lemma match_spair_simps [simp]:
    1.39 +  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>"
    1.40 +  "match_spair\<cdot>\<bottom> = \<bottom>"
    1.41 +by (simp_all add: match_spair_def)
    1.42 +
    1.43 +lemma match_sinl_simps [simp]:
    1.44 +  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x"
    1.45 +  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail"
    1.46 +  "match_sinl\<cdot>\<bottom> = \<bottom>"
    1.47 +by (simp_all add: match_sinl_def)
    1.48 +
    1.49 +lemma match_sinr_simps [simp]:
    1.50 +  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x"
    1.51 +  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail"
    1.52 +  "match_sinr\<cdot>\<bottom> = \<bottom>"
    1.53 +by (simp_all add: match_sinr_def)
    1.54 +
    1.55  lemma match_up_simps [simp]:
    1.56    "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
    1.57    "match_up\<cdot>\<bottom> = \<bottom>"