src/HOLCF/Fixrec.thy
author huffman
Mon Nov 07 19:23:53 2005 +0100 (2005-11-07)
changeset 18110 08ec4f1f116d
parent 18097 d196d84c306f
child 18112 dc1d6f588204
permissions -rw-r--r--
remove syntax for as-patterns
     1 (*  Title:      HOLCF/Fixrec.thy
     2     ID:         $Id$
     3     Author:     Amber Telfer and Brian Huffman
     4 *)
     5 
     6 header "Package for defining recursive functions in HOLCF"
     7 
     8 theory Fixrec
     9 imports Sprod Ssum Up One Tr Fix
    10 uses ("fixrec_package.ML")
    11 begin
    12 
    13 subsection {* Maybe monad type *}
    14 
    15 defaultsort cpo
    16 
    17 types 'a maybe = "one ++ 'a u"
    18 
    19 constdefs
    20   fail :: "'a maybe"
    21   "fail \<equiv> sinl\<cdot>ONE"
    22 
    23   return :: "'a \<rightarrow> 'a maybe"
    24   "return \<equiv> sinr oo up"
    25 
    26 lemma maybeE:
    27   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    28 apply (unfold fail_def return_def)
    29 apply (rule_tac p=p in ssumE, simp)
    30 apply (rule_tac p=x in oneE, simp, simp)
    31 apply (rule_tac p=y in upE, simp, simp)
    32 done
    33 
    34 subsubsection {* Monadic bind operator *}
    35 
    36 constdefs
    37   bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
    38   "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
    39 
    40 syntax ">>=" :: "['a maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'b maybe" (infixl ">>=" 50)
    41 translations "m >>= f" == "bind\<cdot>m\<cdot>f"
    42 
    43 nonterminals
    44   maybebind maybebinds
    45 
    46 syntax 
    47   "_MBIND"  :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind"         ("(2_ <-/ _)" 10)
    48   ""        :: "maybebind \<Rightarrow> maybebinds"                ("_")
    49 
    50   "_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds"  ("_;/ _")
    51   "_MDO"    :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe"     ("(do _;/ (_))" 10)
    52 
    53 translations
    54   "_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)"
    55   "do (x,y) <- m; e" == "m >>= (LAM <x,y>. e)" 
    56   "do x <- m; e"            == "m >>= (LAM x. e)"
    57 
    58 text {* monad laws *}
    59 
    60 lemma bind_strict [simp]: "UU >>= f = UU"
    61 by (simp add: bind_def)
    62 
    63 lemma bind_fail [simp]: "fail >>= f = fail"
    64 by (simp add: bind_def fail_def)
    65 
    66 lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a"
    67 by (simp add: bind_def return_def)
    68 
    69 lemma right_unit [simp]: "m >>= return = m"
    70 by (rule_tac p=m in maybeE, simp_all)
    71 
    72 lemma bind_assoc [simp]:
    73  "(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)"
    74 by (rule_tac p=m in maybeE, simp_all)
    75 
    76 subsubsection {* Run operator *}
    77 
    78 constdefs
    79   run:: "'a::pcpo maybe \<rightarrow> 'a"
    80   "run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
    81 
    82 text {* rewrite rules for run *}
    83 
    84 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
    85 by (simp add: run_def)
    86 
    87 lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
    88 by (simp add: run_def fail_def)
    89 
    90 lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
    91 by (simp add: run_def return_def)
    92 
    93 subsubsection {* Monad plus operator *}
    94 
    95 constdefs
    96   mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
    97   "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
    98 
    99 syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65)
   100 translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2"
   101 
   102 text {* rewrite rules for mplus *}
   103 
   104 lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
   105 by (simp add: mplus_def)
   106 
   107 lemma mplus_fail [simp]: "fail +++ m = m"
   108 by (simp add: mplus_def fail_def)
   109 
   110 lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"
   111 by (simp add: mplus_def return_def)
   112 
   113 lemma mplus_fail2 [simp]: "m +++ fail = m"
   114 by (rule_tac p=m in maybeE, simp_all)
   115 
   116 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
   117 by (rule_tac p=x in maybeE, simp_all)
   118 
   119 subsubsection {* Fatbar combinator *}
   120 
   121 constdefs
   122   fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)"
   123   "fatbar \<equiv> \<Lambda> a b x. a\<cdot>x +++ b\<cdot>x"
   124 
   125 syntax
   126   "\<parallel>" :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)
   127 translations
   128   "m1 \<parallel> m2" == "fatbar\<cdot>m1\<cdot>m2"
   129 
   130 lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
   131 by (simp add: fatbar_def)
   132 
   133 lemma fatbar2: "m\<cdot>x = fail \<Longrightarrow> (m \<parallel> ms)\<cdot>x = ms\<cdot>x"
   134 by (simp add: fatbar_def)
   135 
   136 lemma fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> (m \<parallel> ms)\<cdot>x = return\<cdot>y"
   137 by (simp add: fatbar_def)
   138 
   139 lemmas fatbar_simps = fatbar1 fatbar2 fatbar3
   140 
   141 subsection {* Pattern combinators *}
   142 
   143 types ('a,'b,'c) pattern = "'b \<rightarrow> 'a \<rightarrow> 'c maybe"
   144 
   145 constdefs
   146   wild_pat :: "('a, 'b, 'b) pattern"
   147   "wild_pat \<equiv> \<Lambda> r a. return\<cdot>r"
   148 
   149   var_pat :: "('a, 'a \<rightarrow> 'b, 'b) pattern"
   150   "var_pat \<equiv> \<Lambda> r a. return\<cdot>(r\<cdot>a)"
   151 
   152   as_pat :: "('a, 'b, 'c) pattern \<Rightarrow> ('a, 'a \<rightarrow> 'b, 'c) pattern"
   153   "as_pat p \<equiv> \<Lambda> r a. p\<cdot>(r\<cdot>a)\<cdot>a"
   154 
   155 lemma wild_pat [simp]: "wild_pat\<cdot>r\<cdot>a = return\<cdot>r"
   156 by (simp add: wild_pat_def)
   157 
   158 lemma var_pat [simp]: "var_pat\<cdot>r\<cdot>a = return\<cdot>(r\<cdot>a)"
   159 by (simp add: var_pat_def)
   160 
   161 lemma as_pat [simp]: "as_pat p\<cdot>r\<cdot>a = p\<cdot>(r\<cdot>a)\<cdot>a"
   162 by (simp add: as_pat_def)
   163 
   164 subsection {* Case syntax *}
   165 
   166 nonterminals
   167   Case_syn  Cases_syn
   168 
   169 syntax
   170   "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
   171   "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 10)
   172   ""            :: "Case_syn => Cases_syn"               ("_")
   173   "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
   174   "_as_pattern" :: "[idt, 'a] \<Rightarrow> 'a"                     (* infixr "as" 10 *)
   175 
   176 syntax (xsymbols)
   177   "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
   178 
   179 syntax
   180   "_match"   :: "'a \<Rightarrow> Case_syn" (* or Cases_syn *)
   181   "_as"      :: "[pttrn, Case_syn] \<Rightarrow> Case_syn"
   182   "_matches" :: "['a, Case_syn, 'a list] \<Rightarrow> Case_syn"
   183   "_cons"    :: "['a, 'a list] \<Rightarrow> 'a list"
   184   "_nil"     :: "'a list"
   185 
   186 translations
   187   "_Case_syntax x (_match m)"     == "run\<cdot>(m\<cdot>x)"
   188   "_Case2 (_match c) (_match cs)" == "_match (c \<parallel> cs)"
   189   "_Case1 dummy_pattern r"        == "_match (wild_pat\<cdot>r)"
   190   "_as x (_match (p\<cdot>t))"          == "_match ((as_pat p)\<cdot>(\<Lambda> x. t))"
   191   "_Case1 (_as_pattern x e) r"    == "_as x (_Case1 e r)"
   192   "_Case1 x t"                    == "_match (var_pat\<cdot>(\<Lambda> x. t))"
   193   "_Case1 (f\<cdot>e) r" == "_matches f (_Case1 e r) _nil"
   194   "_matches (f\<cdot>e) (_match (p\<cdot>r)) ps" == "_matches f (_Case1 e r) (_cons p ps)"
   195 
   196 lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>"
   197 by (simp add: fatbar_def)
   198 
   199 lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)"
   200 by (simp add: fatbar_def)
   201 
   202 lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
   203 by (simp add: fatbar_def)
   204 
   205 lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
   206 
   207 subsection {* Pattern combinators for built-in types *}
   208 
   209 constdefs
   210   cpair_pat :: "_"
   211   "cpair_pat p1 p2 \<equiv> \<Lambda> r1 \<langle>x1,x2\<rangle>. bind\<cdot>(p1\<cdot>r1\<cdot>x1)\<cdot>(\<Lambda> r2. p2\<cdot>r2\<cdot>x2)"
   212 
   213   spair_pat :: "_"
   214   "spair_pat p1 p2 \<equiv> \<Lambda> r (:x,y:). cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x,y\<rangle>"
   215 
   216   sinl_pat :: "_"
   217   "sinl_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x | sinr\<cdot>y \<Rightarrow> fail"
   218 
   219   sinr_pat :: "_"
   220   "sinr_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> fail | sinr\<cdot>y \<Rightarrow> p\<cdot>r\<cdot>y"
   221 
   222   up_pat :: "_"
   223   "up_pat p \<equiv> \<Lambda> r a. case a of up\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x"
   224 
   225   Def_pat :: "'a::type \<Rightarrow> ('a lift, 'b, 'b) pattern"
   226   "Def_pat x \<equiv> \<Lambda> r. FLIFT y. if x = y then return\<cdot>r else fail"
   227 
   228   ONE_pat :: "_"
   229   "ONE_pat \<equiv> \<Lambda> r ONE. return\<cdot>r"
   230 
   231   TT_pat :: "(tr, _, _) pattern"
   232   "TT_pat \<equiv> \<Lambda> r b. If b then return\<cdot>r else fail fi"
   233 
   234   FF_pat :: "(tr, _, _) pattern"
   235   "FF_pat \<equiv> \<Lambda> r b. If b then fail else return\<cdot>r fi"
   236 
   237 translations
   238   "_matches cpair (_match (p1\<cdot>r)) (_cons p2 _nil)"
   239     == "_match ((cpair_pat p1 p2)\<cdot>r)"
   240 
   241   "_matches spair (_match (p1\<cdot>r)) (_cons p2 _nil)"
   242     == "_match ((spair_pat p1 p2)\<cdot>r)"
   243 
   244 translations
   245   "_matches sinl (_match (p1\<cdot>r)) _nil" == "_match ((sinl_pat p1)\<cdot>r)"
   246   "_matches sinr (_match (p1\<cdot>r)) _nil" == "_match ((sinr_pat p1)\<cdot>r)"
   247   "_matches up (_match (p1\<cdot>r)) _nil" == "_match ((up_pat p1)\<cdot>r)"
   248 
   249 translations
   250   "_Case1 (Def x) r" == "_match (Def_pat x\<cdot>r)"
   251   "_Case1 ONE r" == "_match (ONE_pat\<cdot>r)"
   252   "_Case1 TT r" == "_match (TT_pat\<cdot>r)"
   253   "_Case1 FF r" == "_match (FF_pat\<cdot>r)"
   254 
   255 lemma cpair_pat_simps [simp]:
   256   "p1\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = \<bottom>"
   257   "p1\<cdot>r\<cdot>x = fail \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = fail"
   258   "p1\<cdot>r\<cdot>x = return\<cdot>r' \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = p2\<cdot>r'\<cdot>y"
   259 by (simp_all add: cpair_pat_def)
   260 
   261 lemma spair_pat_simps [simp]:
   262   "spair_pat p1 p2\<cdot>r\<cdot>\<bottom> = \<bottom>"
   263   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> spair_pat p1 p2\<cdot>r\<cdot>(:x, y:) = cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x, y\<rangle>"
   264 by (simp_all add: spair_pat_def)
   265 
   266 lemma sinl_pat_simps [simp]:
   267   "sinl_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
   268   "x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = p\<cdot>r\<cdot>x"
   269   "x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = fail"
   270 by (simp_all add: sinl_pat_def)
   271 
   272 lemma sinr_pat_simps [simp]:
   273   "sinr_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
   274   "x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
   275   "x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = p\<cdot>r\<cdot>x"
   276 by (simp_all add: sinr_pat_def)
   277 
   278 lemma up_pat_simps [simp]:
   279   "up_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
   280   "up_pat p\<cdot>r\<cdot>(up\<cdot>x) = p\<cdot>r\<cdot>x"
   281 by (simp_all add: up_pat_def)
   282 
   283 lemma Def_pat_simps [simp]:
   284   "Def_pat x\<cdot>r\<cdot>\<bottom> = \<bottom>"
   285   "Def_pat x\<cdot>r\<cdot>(Def x) = return\<cdot>r"
   286   "x \<noteq> y \<Longrightarrow> Def_pat x\<cdot>r\<cdot>(Def y) = fail"
   287 by (simp_all add: Def_pat_def)
   288 
   289 lemma ONE_pat_simps [simp]:
   290   "ONE_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
   291   "ONE_pat\<cdot>r\<cdot>ONE = return\<cdot>r"
   292 by (simp_all add: ONE_pat_def)
   293 
   294 lemma TT_pat_simps [simp]:
   295   "TT_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
   296   "TT_pat\<cdot>r\<cdot>TT = return\<cdot>r"
   297   "TT_pat\<cdot>r\<cdot>FF = fail"
   298 by (simp_all add: TT_pat_def)
   299 
   300 lemma FF_pat_simps [simp]:
   301   "FF_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
   302   "FF_pat\<cdot>r\<cdot>TT = fail"
   303   "FF_pat\<cdot>r\<cdot>FF = return\<cdot>r"
   304 by (simp_all add: FF_pat_def)
   305 
   306 subsection {* Match functions for built-in types *}
   307 
   308 defaultsort pcpo
   309 
   310 constdefs
   311   match_UU :: "'a \<rightarrow> unit maybe"
   312   "match_UU \<equiv> \<Lambda> x. fail"
   313 
   314   match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe"
   315   "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   316 
   317   match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
   318   "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   319 
   320   match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe"
   321   "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
   322 
   323   match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
   324   "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
   325 
   326   match_up :: "'a::cpo u \<rightarrow> 'a maybe"
   327   "match_up \<equiv> fup\<cdot>return"
   328 
   329   match_ONE :: "one \<rightarrow> unit maybe"
   330   "match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()"
   331  
   332   match_TT :: "tr \<rightarrow> unit maybe"
   333   "match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
   334  
   335   match_FF :: "tr \<rightarrow> unit maybe"
   336   "match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
   337 
   338 lemma match_UU_simps [simp]:
   339   "match_UU\<cdot>x = fail"
   340 by (simp add: match_UU_def)
   341 
   342 lemma match_cpair_simps [simp]:
   343   "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
   344 by (simp add: match_cpair_def)
   345 
   346 lemma match_spair_simps [simp]:
   347   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>"
   348   "match_spair\<cdot>\<bottom> = \<bottom>"
   349 by (simp_all add: match_spair_def)
   350 
   351 lemma match_sinl_simps [simp]:
   352   "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x"
   353   "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail"
   354   "match_sinl\<cdot>\<bottom> = \<bottom>"
   355 by (simp_all add: match_sinl_def)
   356 
   357 lemma match_sinr_simps [simp]:
   358   "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x"
   359   "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail"
   360   "match_sinr\<cdot>\<bottom> = \<bottom>"
   361 by (simp_all add: match_sinr_def)
   362 
   363 lemma match_up_simps [simp]:
   364   "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
   365   "match_up\<cdot>\<bottom> = \<bottom>"
   366 by (simp_all add: match_up_def)
   367 
   368 lemma match_ONE_simps [simp]:
   369   "match_ONE\<cdot>ONE = return\<cdot>()"
   370   "match_ONE\<cdot>\<bottom> = \<bottom>"
   371 by (simp_all add: match_ONE_def)
   372 
   373 lemma match_TT_simps [simp]:
   374   "match_TT\<cdot>TT = return\<cdot>()"
   375   "match_TT\<cdot>FF = fail"
   376   "match_TT\<cdot>\<bottom> = \<bottom>"
   377 by (simp_all add: match_TT_def)
   378 
   379 lemma match_FF_simps [simp]:
   380   "match_FF\<cdot>FF = return\<cdot>()"
   381   "match_FF\<cdot>TT = fail"
   382   "match_FF\<cdot>\<bottom> = \<bottom>"
   383 by (simp_all add: match_FF_def)
   384 
   385 subsection {* Mutual recursion *}
   386 
   387 text {*
   388   The following rules are used to prove unfolding theorems from
   389   fixed-point definitions of mutually recursive functions.
   390 *}
   391 
   392 lemma cpair_equalI: "\<lbrakk>x \<equiv> cfst\<cdot>p; y \<equiv> csnd\<cdot>p\<rbrakk> \<Longrightarrow> <x,y> \<equiv> p"
   393 by (simp add: surjective_pairing_Cprod2)
   394 
   395 lemma cpair_eqD1: "<x,y> = <x',y'> \<Longrightarrow> x = x'"
   396 by simp
   397 
   398 lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
   399 by simp
   400 
   401 text {* lemma for proving rewrite rules *}
   402 
   403 lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
   404 by simp
   405 
   406 ML {*
   407 val cpair_equalI = thm "cpair_equalI";
   408 val cpair_eqD1 = thm "cpair_eqD1";
   409 val cpair_eqD2 = thm "cpair_eqD2";
   410 val ssubst_lhs = thm "ssubst_lhs";
   411 *}
   412 
   413 subsection {* Initializing the fixrec package *}
   414 
   415 use "fixrec_package.ML"
   416 
   417 end