src/HOLCF/Fixrec.thy
changeset 16401 57c35ede00b9
parent 16229 77cae9c8e73e
child 16417 9bc16273c2d4
     1.1 --- a/src/HOLCF/Fixrec.thy	Wed Jun 15 14:59:25 2005 +0200
     1.2 +++ b/src/HOLCF/Fixrec.thy	Wed Jun 15 20:50:38 2005 +0200
     1.3 @@ -134,6 +134,27 @@
     1.4    "match_up\<cdot>\<bottom> = \<bottom>"
     1.5  by (simp_all add: match_up_def)
     1.6  
     1.7 +subsection {* Mutual recursion *}
     1.8 +
     1.9 +text {*
    1.10 +  The following rules are used to prove unfolding theorems from
    1.11 +  fixed-point definitions of mutually recursive functions.
    1.12 +*}
    1.13 +
    1.14 +lemma cpair_equalI: "\<lbrakk>x \<equiv> cfst\<cdot>p; y \<equiv> csnd\<cdot>p\<rbrakk> \<Longrightarrow> <x,y> \<equiv> p"
    1.15 +by (simp add: surjective_pairing_Cprod2)
    1.16 +
    1.17 +lemma cpair_eqD1: "<x,y> = <x',y'> \<Longrightarrow> x = x'"
    1.18 +by simp
    1.19 +
    1.20 +lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
    1.21 +by simp
    1.22 +
    1.23 +ML {*
    1.24 +val cpair_equalI = thm "cpair_equalI";
    1.25 +val cpair_eqD1 = thm "cpair_eqD1";
    1.26 +val cpair_eqD2 = thm "cpair_eqD2";
    1.27 +*}
    1.28  
    1.29  subsection {* Intitializing the fixrec package *}
    1.30