src/HOLCF/fixrec_package.ML

 (* extern_name is taken from domain/library.ML *)
 fun extern_name con = case Symbol.explode con of 
 		   ("o"::"p"::" "::rest) => implode rest
 		   | _ => con;
 
-(***************  This is the building functional **************)
-
-(* converts string proposition to a cterm *)
-fun all eqs thy = (let val sign = sign_of (thy) in 
-                  ((term_of o (Thm.read_cterm sign) o rpair propT) eqs) end);
-
 (* splits a cterm into the right and lefthand sides of equality *)
 fun dest_eqs (Const ("==", _)$lhs$rhs) = (lhs, rhs)
   | dest_eqs (Const ("Trueprop", _)$(Const ("op =", _)$lhs$rhs))    = (lhs,rhs)
   | dest_eqs t = sys_error (Sign.string_of_term (sign_of (the_context())) t);
 
-(* building fixpoint functional def for an equation with only 
-   variables as parameters *)
+(* these are helpful functions copied from HOLCF/domain/library.ML *)
+fun %: s = Free(s,dummyT);
+fun %%: s = Const(s,dummyT);
+infix 0 ==;  fun S ==  T = %%:"==" $ S $ T;
+infix 1 ===; fun S === T = %%:"op =" $ S $ T;
+infix 9 `  ; fun f ` x = %%:"Rep_CFun" $ f $ x;
+
+(* infers the type of a term *)
+fun infer t thy = #1 (Sign.infer_types (Sign.pp (sign_of thy)) (sign_of thy) (K NONE) (K NONE) [] true ([t],dummyT));
+
+(*************************************************************************)
+(************ fixed-point definitions and unfolding theorems *************)
+(*************************************************************************)
+
 fun func1 (lhs as Const(name,T), rhs) =
   let
     val basename = Sign.base_name name;
     val funcT = T ->> T;
     val functional = Const ("Cfun.Abs_CFun", (T --> T) --> funcT) $

   in
     (name, (basename^"_fixdef", equals T $ lhs $ rhs'))
   end
   | func1 t = sys_error "func1: not of correct form";
 
-(**************************************************************)
-(* these are helpful functions copied from HOLCF/domain/library.ML *)
-fun %: s = Free(s,dummyT);
-fun %%: s = Const(s,dummyT);
-infix 0 ==;  fun S ==  T = %%:"==" $ S $ T;
-infix 1 ===; fun S === T = %%:"op =" $ S $ T;
-infix 9 `  ; fun f`  x = %%:"Rep_CFun" $ f $ x;
-
-(* infers the type of a term *)
-fun infer t thy = #1 (Sign.infer_types (Sign.pp (sign_of thy)) (sign_of thy) (K NONE) (K NONE) [] true ([t],dummyT));
-
-(*****************************************************************)
-(* monadic notation and pattern matching *)
-(*****************************************************************)
+(*************************************************************************)
+(*********** monadic notation and pattern matching compilation ***********)
+(*************************************************************************)
 
 (* these 3 functions strip off parameters and destruct constructors *)
+(*
 fun strip_cpair (Const("Cfun.Rep_CFun",_) $
       (Const("Cfun.Rep_CFun",_) $ Const("Cprod.cpair",_) $ b) $ r) =
         b :: strip_cpair r
   | strip_cpair c = [c];
-
+*)
 fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(lambda v rhs);
 
 fun big_lambdas [] rhs = rhs
   | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
 

   | add_names (Abs(a,_,t), bs) = add_names(t,a ins_string bs)
   | add_names (_, bs) = bs;
 fun add_terms ts xs = foldr add_names xs ts;
 
 (* builds a monadic term for matching a constructor pattern *)
-fun pre_build (Const("Cfun.Rep_CFun",_)$f$(v as Free(n,T))) rhs vs taken =
+fun pre_build pat rhs vs taken =
+  case pat of
+    Const("Cfun.Rep_CFun",_)$f$(v as Free(n,T)) =>
       pre_build f rhs (v::vs) taken
-  | pre_build (Const("Cfun.Rep_CFun",_)$f$x) rhs vs taken =
+  | Const("Cfun.Rep_CFun",_)$f$x =>
       let val (rhs', v, taken') = pre_build x rhs [] taken;
-      in
-        pre_build f rhs' (v::vs) taken'
-      end
-  | pre_build (Const(c,T)) rhs vs taken =
+      in pre_build f rhs' (v::vs) taken' end
+  | Const(c,T) =>
       let
         val n = variant taken "v";
-        fun result_type (Type(_,[_,T])) (x::xs) = result_type T xs
+        fun result_type (Type("Cfun.->",[_,T])) (x::xs) = result_type T xs
           | result_type T _ = T;
         val v = Free(n, result_type T vs);
         val m = "match_"^(extern_name(NameSpace.base c));
         val k = lambda_tuple vs rhs;
       in
-        (%%:"bind"`(%%:m`v)`k, v, n::taken)
+        (%%:"Fixrec.bind"`(%%:m`v)`k, v, n::taken)
       end;
 
 (* builds a monadic term for matching a function definition pattern *)
 (* returns (name, arity, matcher) *)
-fun building (Const("Cfun.Rep_CFun", _)$f$(v as Free(n,T))) rhs vs taken =
+fun building pat rhs vs taken =
+  case pat of
+    Const("Cfun.Rep_CFun", _)$f$(v as Free(n,T)) =>
       building f rhs (v::vs) taken
-  | building (Const("Cfun.Rep_CFun", _)$f$x) rhs vs taken =
-      let
-        val (rhs', v, taken') = pre_build x rhs [] taken;
-      in
-        building f rhs' (v::vs) taken'
-      end
-  | building (c as Const(_,_)) rhs vs taken = (c, length vs, big_lambdas vs rhs)
-  | building _ _ _ _ = sys_error "function is not declared as constant in theory";
-
-fun match_eq thy f = 
-  let
-    val e = (all f thy);
-    val (lhs,rhs) = dest_eqs e;
-    val (Const(n,_), a, t) = building lhs (%%:"return"`rhs) [] (add_terms [e] []);
-  in
-    (n, a, t)
-  end;
+  | Const("Cfun.Rep_CFun", _)$f$x =>
+      let val (rhs', v, taken') = pre_build x rhs [] taken;
+      in building f rhs' (v::vs) taken' end
+  | Const(_,_) => (pat, length vs, big_lambdas vs rhs)
+  | _ => sys_error "function is not declared as constant in theory";
+
+fun match_eq eq = 
+  let
+    val (lhs,rhs) = dest_eqs eq;
+    val (Const(name,_), arity, term) =
+      building lhs (%%:"Fixrec.return"`rhs) [] (add_terms [eq] []);
+  in (name, arity, term) end;
 
 (* returns the sum (using +++) of the terms in ms *)
 (* also applies "run" to the result! *)
 fun fatbar arity ms =
   let

     val msum = foldr1 mplus (map (unLAM arity) ms);
   in
     reLAM arity (%%:"Fixrec.run"`msum)
   end;
 
-(***************************************************************)
-(*** Proving associated theorems ***)
-
-fun prove_thm thy unfold_thm x =
+fun unzip3 [] = ([],[],[])
+  | unzip3 ((x,y,z)::ts) =
+      let val (xs,ys,zs) = unzip3 ts
+      in (x::xs, y::ys, z::zs) end;
+
+(* this is the pattern-matching compiler function *)
+fun compile_pats eqs = 
+  let
+    val ((n::names),(a::arities),mats) = unzip3 (map match_eq eqs);
+    val cname = if forall (fn x => n=x) names then n
+          else sys_error "FIXREC: all equations must define the same function";
+    val arity = if forall (fn x => a=x) arities then a
+          else sys_error "FIXREC: all equations must have the same arity";
+    val rhs = fatbar arity mats;
+  in
+    HOLogic.mk_Trueprop (%%:cname === rhs)
+  end;
+
+(*************************************************************************)
+(********************** Proving associated theorems **********************)
+(*************************************************************************)
+
+fun prove_thm thy unfold_thm ct =
   let
     val ss = simpset_of thy;
-    val thm = prove_goalw thy [] x (fn _ => [SOLVE(stac unfold_thm 1 THEN simp_tac ss 1)])
-      handle _ => sys_error (x^" :: proof failed on this equation.");
+    val thm = prove_goalw_cterm [] ct
+      (fn _ => [SOLVE(stac unfold_thm 1 THEN simp_tac ss 1)])
+        handle _ => sys_error (string_of_cterm ct^" :: proof failed on this equation.");
   in thm end;
 
 (* this proves that each equation is a theorem *)
 fun prove_list thy unfold_thm [] = []
   | prove_list thy unfold_thm (x::xs) =

       , (basename^"_rews", rew_thms) ]
   in
     (#1 o PureThy.add_thmss (map Thm.no_attributes thmss)) thy'
   end;
 
-fun unzip3 [] = ([],[],[])
-  | unzip3 ((x,y,z)::ts) =
-      let val (xs,ys,zs) = unzip3 ts
-      in (x::xs, y::ys, z::zs) end;
-
-(* this is the main processing function *)
-fun pat_fun eqs thy = 
-  let
-    val ((n::names),(a::arities),mats) = unzip3 (map (match_eq thy) eqs);
-    val cname = if forall (fn x => n=x) names then n
-          else sys_error "PAT_FUN: all equations must define the same function";
-    val arity = if forall (fn x => a=x) arities then a
-          else sys_error "FIXREC: all equations must have the same arity";
-    val msum = fatbar arity mats;
-    val v = variant (add_term_names (msum,[])) "v";
-    val funcc = infer (HOLogic.mk_Trueprop (%%:cname === msum)) thy;
+(*************************************************************************)
+(************************* Main fixrec function **************************)
+(*************************************************************************)
+
+(* this calls the main processing function and then returns the new state *)
+fun add_fixrec strs thy =
+  let
+    val sg = sign_of thy;
+    val cts = map (Thm.read_cterm sg o rpair propT) strs;
+    val eqs = map term_of cts;
+    val funcc = infer (compile_pats eqs) thy;
+    val _ = print_cterm (cterm_of sg funcc);
     val (name', fixdef_name_term) = func1 (dest_eqs funcc);
     val (thy', [fixdef_thm]) =
       PureThy.add_defs_i false [Thm.no_attributes fixdef_name_term] thy;
-  in
-    make_simp name' eqs (cterm_of (sign_of thy') funcc) fixdef_thm thy'
-  end;
-
-(***************************************************************)
-
-(* this calls the main processing function and then returns the new state *)
-fun add_fixrec eqs = pat_fun eqs;
-
-(*****************************************************************)
-(*** Fixpat ***)
-
-(* like Term.strip_comb, but with continuous application *)
-fun strip_cdot u : term * term list =
-  let fun stripc (Const("Cfun.Rep_CFun",_)$f$t, ts) = stripc (f, t::ts)
-        | stripc x = x
-  in stripc(u,[]) end;
+    val ct = cterm_of (sign_of thy') funcc;
+  in
+    make_simp name' cts ct fixdef_thm thy'
+  end;
+
+(*************************************************************************)
+(******************************** Fixpat *********************************)
+(*************************************************************************)
 
 fun fix_pat name pat thy = 
   let
     val sign = sign_of thy;
-    val ct = Thm.read_cterm sign (pat, dummyT);
-    val (Const (f,_), args) = strip_cdot (term_of ct);
-    val unfold_thm = Goals.get_thm thy (f^"_unfold");
-    fun add_arg (arg,thm) = instantiate' [] [SOME arg] (thm RS cfun_fun_cong);
-    val unfold_thm' = foldl add_arg (freezeT unfold_thm) (map (cterm_of sign) args);
-    val thm = simplify (simpset_of thy) unfold_thm';
+    val t = term_of (Thm.read_cterm sign (pat, dummyT));
+    val T = fastype_of t;
+    val eq = HOLogic.mk_Trueprop (HOLogic.eq_const T $ t $ Var (("x",0),T));
+    fun head_const (Const ("Cfun.Rep_CFun",_) $ f $ t) = head_const f
+      | head_const (Const (c,_)) = c
+      | head_const _ = sys_error "FIXPAT: function is not declared as constant in theory";
+    val c = head_const t;
+    val unfold_thm = Goals.get_thm thy (c^"_unfold");
+    val thm = prove_goalw_cterm [] (cterm_of sign eq)
+          (fn _ => [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
+    val _ = print_thm thm;
   in
     (#1 o PureThy.add_thmss [Thm.no_attributes (name, [thm])]) thy
   end;
 
 fun add_fixpat (name,pat) = fix_pat name pat;
 
-(*****************************************************************)
-(*** Parsers ***)
+(*************************************************************************)
+(******************************** Parsers ********************************)
+(*************************************************************************)
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
-val fixrec_decl = Scan.repeat1 P.prop;
+val fixrec_decl = (*P.and_list1*) (Scan.repeat1 P.prop);
 
 (* this builds a parser for a new keyword, fixrec, whose functionality 
 is defined by add_fixrec *)
 val fixrecP =
   OuterSyntax.command "fixrec" "parser for fixrec functions" K.thy_decl