# HG changeset patch
# User wenzelm
# Date 1004809320 -3600
# Node ID 0282eacef4e7b8f46e1957cf00514bdace717698
# Parent  49f6c49454c210e615ade3919f066f3e95ea10bc
adapted to new-style theories;

diff -r 49f6c49454c2 -r 0282eacef4e7 src/HOLCF/domain/extender.ML
--- a/src/HOLCF/domain/extender.ML	Sat Nov 03 18:41:28 2001 +0100
+++ b/src/HOLCF/domain/extender.ML	Sat Nov 03 18:42:00 2001 +0100
@@ -1,17 +1,21 @@
 (*  Title:      HOLCF/domain/extender.ML
     ID:         $Id$
-    Author:     David von Oheimb
+    Author:     David von Oheimb and Markus Wenzel
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Theory extender for domain section.
+Theory extender for domain section, including new-style theory syntax.
 *)
 
+signature DOMAIN_EXTENDER =
+sig
+  val add_domain: string *
+      ((bstring * string list) * (string * mixfix * (bool * string * string) list) list) list
+    -> theory -> theory
+end;
 
-structure Domain_Extender =
+structure Domain_Extender: DOMAIN_EXTENDER =
 struct
 
-local
-
 open Domain_Library;
 
 (* ----- general testing and preprocessing of constructor list -------------- *)
@@ -69,8 +73,6 @@
 
 (* ----- calls for building new thy and thms -------------------------------- *)
 
-in
-
   fun add_domain (comp_dnam,eqs''') thy''' = let
     val sg''' = sign_of thy''';
     val dtnvs = map ((fn (dname,vs) => 
@@ -101,8 +103,44 @@
 	 )) cons') : cons list;
     val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
     val thy        = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
-  in (foldl (fn (thy0,eq) => Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs)) 
-                          |> Domain_Theorems.comp_theorems (comp_dnam, eqs) end;
+    val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) =>
+      Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
+      |>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+in
+  theorems_thy
+  |> Theory.add_path (Sign.base_name comp_dnam)
+  |> (#1 o (PureThy.add_thmss [(("rews", flat rewss @ take_rews), [])]))
+  |> Theory.parent_path
+end;
+
+
+
+(** outer syntax **)
+
+local structure P = OuterParse and K = OuterSyntax.Keyword in
+
+val dest_decl =
+  P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
+    P.name -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1;
 
-end (* local *)
-end (* struct *)
+val cons_decl =
+  P.name -- Scan.repeat dest_decl -- P.opt_mixfix --| P.marg_comment
+  >> (fn ((c, ds), mx) => (c, mx, ds));
+
+val domain_decl = (P.type_args -- P.name >> Library.swap) -- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+val domains_decl =
+  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
+  >> (fn (opt_name, doms) =>
+      (case opt_name of None => space_implode "_" (map (#1 o #1) doms) | Some s => s, doms));
+
+val domainP =
+  OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
+    (domains_decl >> (Toplevel.theory o add_domain));
+
+
+val _ = OuterSyntax.add_keywords ["lazy"];
+val _ = OuterSyntax.add_parsers [domainP];
+
+end;
+
+end;
diff -r 49f6c49454c2 -r 0282eacef4e7 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Sat Nov 03 18:41:28 2001 +0100
+++ b/src/HOLCF/domain/theorems.ML	Sat Nov 03 18:42:00 2001 +0100
@@ -94,7 +94,7 @@
 val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%:x_name === UU)) [
                            res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
                                 etac ssubst 1, rtac abs_strict 1];
-val iso_rews = [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
+val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
 
 local 
 val iso_swap = pg [] (dc_rep`%"x" === %:"y" ==> %:"x" === dc_abs`%"y") [
@@ -263,7 +263,7 @@
     |   distincts ((c,leqs)::cs) = List.concat
 	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
 		    distincts cs;
-    in distincts (cons~~distincts_le) end;
+    in map standard (distincts (cons~~distincts_le)) end;
 
 local 
   fun pgterm rel con args = let
@@ -327,7 +327,8 @@
 		("inverts" , inverts ),
 		("injects" , injects ),
 		("copy_rews", copy_rews)])))
-       |> Theory.parent_path
+       |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
+                 dist_les @ dist_eqs @ copy_rews)
 end; (* let *)
 
 fun comp_theorems (comp_dnam, eqs: eq list) thy =
@@ -336,7 +337,7 @@
 val conss  = map  snd        eqs;
 val comp_dname = Sign.full_name (sign_of thy) comp_dnam;
 
-val d = writeln("Proving induction   properties of domain "^comp_dname^" ...");
+val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
 val pg = pg' thy;
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
@@ -395,7 +396,7 @@
                                 asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1
                                                            ) cons) eqs)));
 in
-val take_rews = atomize take_stricts @ take_0s @ atomize take_apps;
+val take_rews = map standard (atomize take_stricts @ take_0s @ atomize take_apps);
 end; (* local *)
 
 local
@@ -596,7 +597,7 @@
 		("finite_ind", [finite_ind]),
 		("ind"       , [ind       ]),
 		("coind"     , [coind     ])])))
-       |> Theory.parent_path
+       |> Theory.parent_path |> rpair take_rews
 end; (* let *)
 end; (* local *)
 end; (* struct *)