# HG changeset patch
# User huffman
# Date 1119035971 -7200
# Node ID e6b431cb8e0c5874f32e2b0b2f5ea26596379d88
# Parent  72a08d509d625e10e25a9f43b2b3d7d08dccb603
support theorem names and attributes for fixrec equations; also make them into simp rules by default, like primrec does

diff -r 72a08d509d62 -r e6b431cb8e0c src/HOLCF/fixrec_package.ML
--- a/src/HOLCF/fixrec_package.ML	Fri Jun 17 18:50:40 2005 +0200
+++ b/src/HOLCF/fixrec_package.ML	Fri Jun 17 21:19:31 2005 +0200
@@ -7,7 +7,7 @@
 
 signature FIXREC_PACKAGE =
 sig
-  val add_fixrec: string list list -> theory -> theory
+  val add_fixrec: ((string * Attrib.src list) * string) list list -> theory -> theory
   val add_fixpat: ((string * Attrib.src list) * string) list -> theory -> theory
 end;
 
@@ -31,9 +31,13 @@
 
 (* 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 (Const ("Trueprop", _)$(Const ("op =", _)$lhs$rhs)) = (lhs,rhs)
   | dest_eqs t = sys_error (Sign.string_of_term (sign_of (the_context())) t);
 
+(* similar to Thm.head_of, but for continuous application *)
+fun chead_of (Const("Cfun.Rep_CFun",_)$f$t) = chead_of f
+  | chead_of u = u;
+
 (* these are helpful functions copied from HOLCF/domain/library.ML *)
 fun %: s = Free(s,dummyT);
 fun %%: s = Const(s,dummyT);
@@ -98,19 +102,19 @@
           (fn _ => [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
                     simp_tac (simpset_of thy') 1]);
     val ctuple_induct_thm =
-          (space_implode "_" names ^ "_induct", [ctuple_fixdef_thm RS def_fix_ind]);
+          (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind);
     
     fun unfolds [] thm = []
-      | unfolds (n::[]) thm = [(n^"_unfold", [thm])]
+      | unfolds (n::[]) thm = [(n^"_unfold", thm)]
       | unfolds (n::ns) thm = let
           val thmL = thm RS cpair_eqD1;
           val thmR = thm RS cpair_eqD2;
-        in (n^"_unfold", [thmL]) :: unfolds ns thmR end;
-    val unfold_thmss = unfolds names ctuple_unfold_thm;
-    val thmss = ctuple_induct_thm :: unfold_thmss;
-    val (thy'', _) = PureThy.add_thmss (map Thm.no_attributes thmss) thy';
+        in (n^"_unfold", thmL) :: unfolds ns thmR end;
+    val unfold_thms = unfolds names ctuple_unfold_thm;
+    val thms = ctuple_induct_thm :: unfold_thms;
+    val (thy'', _) = PureThy.add_thms (map Thm.no_attributes thms) thy';
   in
-    (thy'', names, fixdef_thms, List.concat (map snd unfold_thmss))
+    (thy'', names, fixdef_thms, map snd unfold_thms)
   end;
 
 (*************************************************************************)
@@ -201,25 +205,29 @@
 (********************** Proving associated theorems **********************)
 (*************************************************************************)
 
-fun prove_rew thy unfold_thm ct =
+fun prove_simp thy unfold_thm t =
   let
     val ss = simpset_of thy;
+    val ct = cterm_of thy t;
     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_rews thy (unfold_thm,cts) = map (prove_rew thy unfold_thm) cts;
+fun prove_simps thy (unfold_thm,ts) = map (prove_simp thy unfold_thm) ts;
 
 (* proves the pattern matching equations as theorems, using unfold *)
-fun make_simps names unfold_thms ctss thy = 
+fun make_simps cnames unfold_thms namess attss tss thy = 
   let
-    val thm_names = map (fn name => name^"_rews") names;
-    val rew_thmss = ListPair.map (prove_rews thy) (unfold_thms, ctss);
-    val thmss = ListPair.zip (thm_names, rew_thmss);
+    val thm_names = map (fn name => name^"_simps") cnames;
+    val rew_thmss = map (prove_simps thy) (unfold_thms ~~ tss);
+    val thms = (List.concat namess ~~ List.concat rew_thmss) ~~ List.concat attss;
+    val (thy',_) = PureThy.add_thms thms thy;
+    val thmss = thm_names ~~ rew_thmss;
+    val simp_attribute = rpair [Simplifier.simp_add_global];
   in
-    (#1 o PureThy.add_thmss (map Thm.no_attributes thmss)) thy
+    (#1 o PureThy.add_thmss (map simp_attribute thmss)) thy'
   end;
 
 (*************************************************************************)
@@ -227,15 +235,17 @@
 (*************************************************************************)
 
 (* this calls the main processing function and then returns the new state *)
-fun add_fixrec strss thy =
+fun add_fixrec blocks thy =
   let
     val sg = sign_of thy;
-    val ctss = map (map (Thm.read_cterm sg o rpair propT)) strss;
-    val tss = map (map term_of) ctss;
-    val ts' = map (fn ts => infer sg (compile_pats ts)) tss;
-    val (thy', names, fixdef_thms, unfold_thms) = add_fixdefs ts' thy;
+    fun split_list2 xss = split_list (map split_list xss);
+    val ((namess, srcsss), strss) = apfst split_list2 (split_list2 blocks);
+    val attss = map (map (map (Attrib.global_attribute thy))) srcsss;
+    val tss = map (map (term_of o Thm.read_cterm sg o rpair propT)) strss;
+    val ts' = map (infer sg o compile_pats) tss;
+    val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs ts' thy;
   in
-    make_simps names unfold_thms ctss thy'
+    make_simps cnames unfold_thms namess attss tss thy'
   end;
 
 (*************************************************************************)
@@ -248,11 +258,9 @@
     val t = term_of (Thm.read_cterm sg (pat, dummyT));
     val T = fastype_of t;
     val eq = mk_trp (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 cname = case chead_of t of Const(c,_) => c | _ =>
+              sys_error "FIXPAT: function is not declared as constant in theory";
+    val unfold_thm = Goals.get_thm thy (cname^"_unfold");
     val rew = prove_goalw_cterm [] (cterm_of sg eq)
           (fn _ => [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   in rew end;
@@ -261,8 +269,8 @@
   let
     val ((names, srcss), strings) = apfst ListPair.unzip (ListPair.unzip pats);
     val atts = map (map (Attrib.global_attribute thy)) srcss;
-    val rews = map (fix_pat thy) strings;
-    val (thy', _) = PureThy.add_thms ((names ~~ rews) ~~ atts) thy;
+    val simps = map (fix_pat thy) strings;
+    val (thy', _) = PureThy.add_thms ((names ~~ simps) ~~ atts) thy;
   in thy' end;
 
 (*************************************************************************)
@@ -271,7 +279,7 @@
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
-val fixrec_decl = P.and_list1 (Scan.repeat1 P.prop);
+val fixrec_decl = P.and_list1 (Scan.repeat1 (P.opt_thm_name ":" -- P.prop));
 
 (* this builds a parser for a new keyword, fixrec, whose functionality 
 is defined by add_fixrec *)
@@ -283,8 +291,7 @@
 val _ = OuterSyntax.add_parsers [fixrecP];
 
 (* fixpat parser *)
-(*val fixpat_decl = P.name -- P.prop;*)
-val fixpat_decl = Scan.repeat1 (P.thm_name ":" -- P.prop);
+val fixpat_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
 
 val fixpatP =
   OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl