adapted to new-style theories;
authorwenzelm
Sat Nov 03 18:42:00 2001 +0100 (2001-11-03)
changeset 120370282eacef4e7
parent 12036 49f6c49454c2
child 12038 343a9888e875
adapted to new-style theories;
src/HOLCF/domain/extender.ML
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/domain/extender.ML	Sat Nov 03 18:41:28 2001 +0100
     1.2 +++ b/src/HOLCF/domain/extender.ML	Sat Nov 03 18:42:00 2001 +0100
     1.3 @@ -1,17 +1,21 @@
     1.4  (*  Title:      HOLCF/domain/extender.ML
     1.5      ID:         $Id$
     1.6 -    Author:     David von Oheimb
     1.7 +    Author:     David von Oheimb and Markus Wenzel
     1.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  
    1.10 -Theory extender for domain section.
    1.11 +Theory extender for domain section, including new-style theory syntax.
    1.12  *)
    1.13  
    1.14 +signature DOMAIN_EXTENDER =
    1.15 +sig
    1.16 +  val add_domain: string *
    1.17 +      ((bstring * string list) * (string * mixfix * (bool * string * string) list) list) list
    1.18 +    -> theory -> theory
    1.19 +end;
    1.20  
    1.21 -structure Domain_Extender =
    1.22 +structure Domain_Extender: DOMAIN_EXTENDER =
    1.23  struct
    1.24  
    1.25 -local
    1.26 -
    1.27  open Domain_Library;
    1.28  
    1.29  (* ----- general testing and preprocessing of constructor list -------------- *)
    1.30 @@ -69,8 +73,6 @@
    1.31  
    1.32  (* ----- calls for building new thy and thms -------------------------------- *)
    1.33  
    1.34 -in
    1.35 -
    1.36    fun add_domain (comp_dnam,eqs''') thy''' = let
    1.37      val sg''' = sign_of thy''';
    1.38      val dtnvs = map ((fn (dname,vs) => 
    1.39 @@ -101,8 +103,44 @@
    1.40  	 )) cons') : cons list;
    1.41      val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
    1.42      val thy        = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
    1.43 -  in (foldl (fn (thy0,eq) => Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs)) 
    1.44 -                          |> Domain_Theorems.comp_theorems (comp_dnam, eqs) end;
    1.45 +    val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) =>
    1.46 +      Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
    1.47 +      |>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
    1.48 +in
    1.49 +  theorems_thy
    1.50 +  |> Theory.add_path (Sign.base_name comp_dnam)
    1.51 +  |> (#1 o (PureThy.add_thmss [(("rews", flat rewss @ take_rews), [])]))
    1.52 +  |> Theory.parent_path
    1.53 +end;
    1.54 +
    1.55 +
    1.56 +
    1.57 +(** outer syntax **)
    1.58 +
    1.59 +local structure P = OuterParse and K = OuterSyntax.Keyword in
    1.60 +
    1.61 +val dest_decl =
    1.62 +  P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
    1.63 +    P.name -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1;
    1.64  
    1.65 -end (* local *)
    1.66 -end (* struct *)
    1.67 +val cons_decl =
    1.68 +  P.name -- Scan.repeat dest_decl -- P.opt_mixfix --| P.marg_comment
    1.69 +  >> (fn ((c, ds), mx) => (c, mx, ds));
    1.70 +
    1.71 +val domain_decl = (P.type_args -- P.name >> Library.swap) -- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
    1.72 +val domains_decl =
    1.73 +  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.and_list1 domain_decl
    1.74 +  >> (fn (opt_name, doms) =>
    1.75 +      (case opt_name of None => space_implode "_" (map (#1 o #1) doms) | Some s => s, doms));
    1.76 +
    1.77 +val domainP =
    1.78 +  OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
    1.79 +    (domains_decl >> (Toplevel.theory o add_domain));
    1.80 +
    1.81 +
    1.82 +val _ = OuterSyntax.add_keywords ["lazy"];
    1.83 +val _ = OuterSyntax.add_parsers [domainP];
    1.84 +
    1.85 +end;
    1.86 +
    1.87 +end;
     2.1 --- a/src/HOLCF/domain/theorems.ML	Sat Nov 03 18:41:28 2001 +0100
     2.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Nov 03 18:42:00 2001 +0100
     2.3 @@ -94,7 +94,7 @@
     2.4  val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%:x_name === UU)) [
     2.5                             res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
     2.6                                  etac ssubst 1, rtac abs_strict 1];
     2.7 -val iso_rews = [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
     2.8 +val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
     2.9  
    2.10  local 
    2.11  val iso_swap = pg [] (dc_rep`%"x" === %:"y" ==> %:"x" === dc_abs`%"y") [
    2.12 @@ -263,7 +263,7 @@
    2.13      |   distincts ((c,leqs)::cs) = List.concat
    2.14  	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
    2.15  		    distincts cs;
    2.16 -    in distincts (cons~~distincts_le) end;
    2.17 +    in map standard (distincts (cons~~distincts_le)) end;
    2.18  
    2.19  local 
    2.20    fun pgterm rel con args = let
    2.21 @@ -327,7 +327,8 @@
    2.22  		("inverts" , inverts ),
    2.23  		("injects" , injects ),
    2.24  		("copy_rews", copy_rews)])))
    2.25 -       |> Theory.parent_path
    2.26 +       |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
    2.27 +                 dist_les @ dist_eqs @ copy_rews)
    2.28  end; (* let *)
    2.29  
    2.30  fun comp_theorems (comp_dnam, eqs: eq list) thy =
    2.31 @@ -336,7 +337,7 @@
    2.32  val conss  = map  snd        eqs;
    2.33  val comp_dname = Sign.full_name (sign_of thy) comp_dnam;
    2.34  
    2.35 -val d = writeln("Proving induction   properties of domain "^comp_dname^" ...");
    2.36 +val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
    2.37  val pg = pg' thy;
    2.38  
    2.39  (* ----- getting the composite axiom and definitions ------------------------ *)
    2.40 @@ -395,7 +396,7 @@
    2.41                                  asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1
    2.42                                                             ) cons) eqs)));
    2.43  in
    2.44 -val take_rews = atomize take_stricts @ take_0s @ atomize take_apps;
    2.45 +val take_rews = map standard (atomize take_stricts @ take_0s @ atomize take_apps);
    2.46  end; (* local *)
    2.47  
    2.48  local
    2.49 @@ -596,7 +597,7 @@
    2.50  		("finite_ind", [finite_ind]),
    2.51  		("ind"       , [ind       ]),
    2.52  		("coind"     , [coind     ])])))
    2.53 -       |> Theory.parent_path
    2.54 +       |> Theory.parent_path |> rpair take_rews
    2.55  end; (* let *)
    2.56  end; (* local *)
    2.57  end; (* struct *)