adapted primrec/datatype to Isar;
authorwenzelm
Wed Nov 14 18:46:30 2001 +0100 (2001-11-14)
changeset 12183c10cea75dd56
parent 12182 3f820a21dcc1
child 12184 f4aaa2647fd2
adapted primrec/datatype to Isar;
src/ZF/Datatype.ML
src/ZF/Datatype.thy
src/ZF/Inductive.thy
src/ZF/ROOT.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
src/ZF/thy_syntax.ML
     1.1 --- a/src/ZF/Datatype.ML	Wed Nov 14 18:46:07 2001 +0100
     1.2 +++ b/src/ZF/Datatype.ML	Wed Nov 14 18:46:30 2001 +0100
     1.3 @@ -22,11 +22,12 @@
     1.4  
     1.5  
     1.6  structure Data_Package = 
     1.7 -    Add_datatype_def_Fun
     1.8 -      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
     1.9 -       and Su=Standard_Sum
    1.10 -       and Ind_Package = Ind_Package
    1.11 -       and Datatype_Arg = Data_Arg);
    1.12 +  Add_datatype_def_Fun
    1.13 +   (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    1.14 +    and Su=Standard_Sum
    1.15 +    and Ind_Package = Ind_Package
    1.16 +    and Datatype_Arg = Data_Arg
    1.17 +    val coind = false);
    1.18  
    1.19  
    1.20  (*Typechecking rules for most codatatypes involving quniv*)
    1.21 @@ -42,10 +43,12 @@
    1.22    end;
    1.23  
    1.24  structure CoData_Package = 
    1.25 -    Add_datatype_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
    1.26 -                          and Su=Quine_Sum
    1.27 -                          and Ind_Package = CoInd_Package
    1.28 -                          and Datatype_Arg = CoData_Arg);
    1.29 +  Add_datatype_def_Fun
    1.30 +   (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
    1.31 +    and Su=Quine_Sum
    1.32 +    and Ind_Package = CoInd_Package
    1.33 +    and Datatype_Arg = CoData_Arg
    1.34 +    val coind = true);
    1.35  
    1.36  
    1.37  
     2.1 --- a/src/ZF/Datatype.thy	Wed Nov 14 18:46:07 2001 +0100
     2.2 +++ b/src/ZF/Datatype.thy	Wed Nov 14 18:46:30 2001 +0100
     2.3 @@ -7,7 +7,8 @@
     2.4  *)
     2.5  
     2.6  theory Datatype = Inductive + Univ + QUniv
     2.7 -  files "Tools/datatype_package.ML":
     2.8 +  files
     2.9 +    "Tools/datatype_package.ML"
    2.10 +    "Tools/numeral_syntax.ML":  (*belongs to theory Bin*)
    2.11  
    2.12  end
    2.13 -
     3.1 --- a/src/ZF/Inductive.thy	Wed Nov 14 18:46:07 2001 +0100
     3.2 +++ b/src/ZF/Inductive.thy	Wed Nov 14 18:46:30 2001 +0100
     3.3 @@ -8,6 +8,7 @@
     3.4  
     3.5  theory Inductive = Fixedpt + mono
     3.6    files
     3.7 +    "ind_syntax.ML"
     3.8      "Tools/cartprod.ML"
     3.9      "Tools/ind_cases.ML"
    3.10      "Tools/inductive_package.ML"
     4.1 --- a/src/ZF/ROOT.ML	Wed Nov 14 18:46:07 2001 +0100
     4.2 +++ b/src/ZF/ROOT.ML	Wed Nov 14 18:46:30 2001 +0100
     4.3 @@ -21,14 +21,7 @@
     4.4  use "~~/src/Provers/Arith/cancel_numerals.ML";
     4.5  use "~~/src/Provers/Arith/combine_numerals.ML";
     4.6  
     4.7 -use_thy "mono";
     4.8 -use "ind_syntax.ML";
     4.9 -use_thy "Datatype";
    4.10 -
    4.11 -use     "Tools/numeral_syntax.ML";
    4.12 -(*the all-in-one theory*)
    4.13  with_path "Integ" use_thy "Main";
    4.14 -
    4.15  simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
    4.16  
    4.17  print_depth 8;
     5.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Nov 14 18:46:07 2001 +0100
     5.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Nov 14 18:46:30 2001 +0100
     5.3 @@ -12,7 +12,6 @@
     5.4  Products are used only to derive "streamlined" induction rules for relations
     5.5  *)
     5.6  
     5.7 -
     5.8  type datatype_result =
     5.9     {con_defs   : thm list,             (*definitions made in thy*)
    5.10      case_eqns  : thm list,             (*equations for case operator*)
    5.11 @@ -21,53 +20,40 @@
    5.12      free_SEs   : thm list,             (*freeness destruct rules*)
    5.13      mk_free    : string -> thm};       (*function to make freeness theorems*)
    5.14  
    5.15 -
    5.16  signature DATATYPE_ARG =
    5.17 -  sig
    5.18 +sig
    5.19    val intrs : thm list
    5.20    val elims : thm list
    5.21 -  end;
    5.22 -
    5.23 +end;
    5.24  
    5.25  (*Functor's result signature*)
    5.26  signature DATATYPE_PACKAGE =
    5.27  sig
    5.28 -
    5.29    (*Insert definitions for the recursive sets, which
    5.30       must *already* be declared as constants in parent theory!*)
    5.31 -  val add_datatype_i:
    5.32 -      term * term list * Ind_Syntax.constructor_spec list list *
    5.33 -      thm list * thm list * thm list
    5.34 -      -> theory -> theory * inductive_result * datatype_result
    5.35 -
    5.36 -  val add_datatype:
    5.37 -      string * string list *
    5.38 -      (string * string list * mixfix) list list *
    5.39 -      thm list * thm list * thm list
    5.40 -      -> theory -> theory * inductive_result * datatype_result
    5.41 -
    5.42 +  val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
    5.43 +    thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
    5.44 +  val add_datatype_x: string * string list -> (string * string list * mixfix) list list ->
    5.45 +    thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
    5.46 +  val add_datatype: string * string list -> (string * string list * mixfix) list list ->
    5.47 +    (xstring * Args.src list) list * (xstring * Args.src list) list *
    5.48 +    (xstring * Args.src list) list -> theory -> theory * inductive_result * datatype_result
    5.49  end;
    5.50  
    5.51 -
    5.52 -(*Declares functions to add fixedpoint/constructor defs to a theory.
    5.53 -  Recursive sets must *already* be declared as constants.*)
    5.54  functor Add_datatype_def_Fun
    5.55 -    (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
    5.56 -           and Ind_Package : INDUCTIVE_PACKAGE
    5.57 -           and Datatype_Arg : DATATYPE_ARG)
    5.58 - : DATATYPE_PACKAGE =
    5.59 + (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
    5.60 +  and Ind_Package : INDUCTIVE_PACKAGE
    5.61 +  and Datatype_Arg : DATATYPE_ARG
    5.62 +  val coind : bool): DATATYPE_PACKAGE =
    5.63  struct
    5.64  
    5.65 +(*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *)
    5.66  
    5.67 -(*con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
    5.68 -fun add_datatype_i (dom_sum, rec_tms, con_ty_lists,
    5.69 -                    monos, type_intrs, type_elims) thy =
    5.70 +fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
    5.71   let
    5.72 -  open BasisLibrary
    5.73    val dummy = (*has essential ancestors?*)
    5.74      Theory.requires thy "Datatype" "(co)datatype definitions";
    5.75  
    5.76 -
    5.77    val rec_names = map (#1 o dest_Const o head_of) rec_tms
    5.78    val rec_base_names = map Sign.base_name rec_names
    5.79    val big_rec_base_name = space_implode "_" rec_base_names
    5.80 @@ -80,9 +66,7 @@
    5.81    val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists);
    5.82  
    5.83    val dummy =
    5.84 -        writeln ((if (#1 (dest_Const Fp.oper) = "Fixedpt.lfp") then "Datatype"
    5.85 -                  else "Codatatype")
    5.86 -                 ^ " definition " ^ big_rec_name)
    5.87 +    writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ big_rec_name);
    5.88  
    5.89    val case_varname = "f";                (*name for case variables*)
    5.90  
    5.91 @@ -238,8 +222,7 @@
    5.92  
    5.93    (* Build the new theory *)
    5.94  
    5.95 -  val need_recursor =
    5.96 -      (#1 (dest_Const Fp.oper) = "Fixedpt.lfp" andalso recursor_typ <> case_typ);
    5.97 +  val need_recursor = (not coind andalso recursor_typ <> case_typ);
    5.98  
    5.99    fun add_recursor thy =
   5.100        if need_recursor then
   5.101 @@ -387,17 +370,11 @@
   5.102   in
   5.103    (*Updating theory components: simprules and datatype info*)
   5.104    (thy1 |> Theory.add_path big_rec_base_name
   5.105 -        |> (#1 o PureThy.add_thmss [(("simps", simps),
   5.106 -                               [Simplifier.simp_add_global])])
   5.107 -        |> (#1 o PureThy.add_thmss [(("", intrs),
   5.108 -                                (*not "intrs" to avoid the warning that they
   5.109 -                                  are already stored by the inductive package*)
   5.110 -                               [Classical.safe_intro_global])])
   5.111 -        |> DatatypesData.put
   5.112 -            (Symtab.update
   5.113 -             ((big_rec_name, dt_info), DatatypesData.get thy1))
   5.114 -        |> ConstructorsData.put
   5.115 -             (foldr Symtab.update (con_pairs, ConstructorsData.get thy1))
   5.116 +        |> (#1 o PureThy.add_thmss
   5.117 +         [(("simps", simps), [Simplifier.simp_add_global]),
   5.118 +          (("", intrs), [Classical.safe_intro_global])])
   5.119 +        |> DatatypesData.map (fn tab => Symtab.update ((big_rec_name, dt_info), tab))
   5.120 +        |> ConstructorsData.map (fn tab => foldr Symtab.update (con_pairs, tab))
   5.121          |> Theory.parent_path,
   5.122     ind_result,
   5.123     {con_defs = con_defs,
   5.124 @@ -409,20 +386,52 @@
   5.125    end;
   5.126  
   5.127  
   5.128 -fun add_datatype (sdom, srec_tms, scon_ty_lists,
   5.129 -                  monos, type_intrs, type_elims) thy =
   5.130 -  let val sign = sign_of thy
   5.131 -      val read_i = Sign.simple_read_term sign Ind_Syntax.iT
   5.132 -      val rec_tms = map read_i srec_tms
   5.133 -      val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
   5.134 -      val dom_sum =
   5.135 -          if sdom = "" then
   5.136 -              Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp")
   5.137 -                                     (rec_tms, con_ty_lists)
   5.138 -          else read_i sdom
   5.139 -  in
   5.140 -      add_datatype_i (dom_sum, rec_tms, con_ty_lists,
   5.141 -                      monos, type_intrs, type_elims) thy
   5.142 -  end
   5.143 +fun add_datatype_x (sdom, srec_tms) scon_ty_lists (monos, type_intrs, type_elims) thy =
   5.144 +  let
   5.145 +    val sign = sign_of thy;
   5.146 +    val read_i = Sign.simple_read_term sign Ind_Syntax.iT;
   5.147 +    val rec_tms = map read_i srec_tms;
   5.148 +    val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
   5.149 +    val dom_sum =
   5.150 +      if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
   5.151 +      else read_i sdom;
   5.152 +  in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end;
   5.153 +
   5.154 +fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
   5.155 +  let
   5.156 +    val (thy', ((monos, type_intrs), type_elims)) = thy
   5.157 +      |> IsarThy.apply_theorems raw_monos
   5.158 +      |>>> IsarThy.apply_theorems raw_type_intrs
   5.159 +      |>>> IsarThy.apply_theorems raw_type_elims;
   5.160 +  in add_datatype_x (sdom, srec_tms) scon_ty_lists (monos, type_intrs, type_elims) thy' end;
   5.161 +
   5.162 +
   5.163 +(* outer syntax *)
   5.164 +
   5.165 +local structure P = OuterParse and K = OuterSyntax.Keyword in
   5.166 +
   5.167 +fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
   5.168 +  #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
   5.169 +
   5.170 +val con_decl =
   5.171 +  P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
   5.172 +  >> P.triple1;
   5.173 +
   5.174 +val datatype_decl =
   5.175 +  (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
   5.176 +  P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
   5.177 +  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   5.178 +  Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   5.179 +  Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1 --| P.marg_comment) []
   5.180 +  >> (Toplevel.theory o mk_datatype);
   5.181 +
   5.182 +val coind_prefix = if coind then "co" else "";
   5.183 +
   5.184 +val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype")
   5.185 +  ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
   5.186 +
   5.187 +val _ = OuterSyntax.add_parsers [inductiveP];
   5.188  
   5.189  end;
   5.190 +
   5.191 +end;
     6.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Nov 14 18:46:07 2001 +0100
     6.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Nov 14 18:46:30 2001 +0100
     6.3 @@ -47,6 +47,7 @@
     6.4      (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU val coind: bool)
     6.5   : INDUCTIVE_PACKAGE =
     6.6  struct
     6.7 +
     6.8  open Logic Ind_Syntax;
     6.9  
    6.10  
    6.11 @@ -522,28 +523,27 @@
    6.12                    |> standard
    6.13       and mutual_induct = CP.remove_split mutual_induct_fsplit
    6.14  
    6.15 -     val induct_att =
    6.16 -       (case rec_names of [name] => [InductAttrib.induct_set_global name] | _ => []);
    6.17 -     val (thy', [induct', mutual_induct']) =
    6.18 -        thy |> PureThy.add_thms [(("induct", induct), induct_att),
    6.19 -          (("mutual_induct", mutual_induct), [])];
    6.20 +     val (thy', [induct', mutual_induct']) = thy |>
    6.21 +       PureThy.add_thms [(("induct", induct), [InductAttrib.induct_set_global big_rec_name]),
    6.22 +         (("mutual_induct", mutual_induct), [])];
    6.23      in (thy', induct', mutual_induct')
    6.24      end;  (*of induction_rules*)
    6.25  
    6.26    val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
    6.27  
    6.28    val (thy2, induct, mutual_induct) =
    6.29 -      if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then induction_rules raw_induct thy1
    6.30 +      if not coind then induction_rules raw_induct thy1
    6.31        else (thy1, raw_induct, TrueI)
    6.32    and defs = big_rec_def :: part_rec_defs
    6.33  
    6.34  
    6.35    val (thy3, ([bnd_mono', dom_subset', elim'], [defs', intrs'])) =
    6.36      thy2
    6.37 +    |> IndCases.declare big_rec_name make_cases
    6.38      |> PureThy.add_thms
    6.39        [(("bnd_mono", bnd_mono), []),
    6.40         (("dom_subset", dom_subset), []),
    6.41 -       (("cases", elim), [InductAttrib.cases_set_global ""])]
    6.42 +       (("cases", elim), [InductAttrib.cases_set_global big_rec_name])]
    6.43      |>>> (PureThy.add_thmss o map Thm.no_attributes)
    6.44          [("defs", defs),
    6.45           ("intros", intrs)];
     7.1 --- a/src/ZF/Tools/primrec_package.ML	Wed Nov 14 18:46:07 2001 +0100
     7.2 +++ b/src/ZF/Tools/primrec_package.ML	Wed Nov 14 18:46:30 2001 +0100
     7.3 @@ -9,13 +9,20 @@
     7.4  
     7.5  signature PRIMREC_PACKAGE =
     7.6  sig
     7.7 -  val add_primrec_i : (string * term) list -> theory -> theory * thm list
     7.8 -  val add_primrec   : (string * string) list -> theory -> theory * thm list
     7.9 +  val quiet_mode: bool ref
    7.10 +  val add_primrec: ((bstring * string) * Args.src list) list -> theory -> theory * thm list
    7.11 +  val add_primrec_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
    7.12  end;
    7.13  
    7.14  structure PrimrecPackage : PRIMREC_PACKAGE =
    7.15  struct
    7.16  
    7.17 +(* messages *)
    7.18 +
    7.19 +val quiet_mode = ref false;
    7.20 +fun message s = if ! quiet_mode then () else writeln s;
    7.21 +
    7.22 +
    7.23  exception RecError of string;
    7.24  
    7.25  (*Remove outer Trueprop and equality sign*)
    7.26 @@ -26,24 +33,25 @@
    7.27  fun primrec_eq_err sign s eq =
    7.28    primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq);
    7.29  
    7.30 +
    7.31  (* preprocessing of equations *)
    7.32  
    7.33  (*rec_fn_opt records equations already noted for this function*)
    7.34 -fun process_eqn thy (eq, rec_fn_opt) = 
    7.35 +fun process_eqn thy (eq, rec_fn_opt) =
    7.36    let
    7.37 -    val (lhs, rhs) = 
    7.38 -	if null (term_vars eq) then
    7.39 -	    dest_eqn eq handle _ => raise RecError "not a proper equation"
    7.40 -	else raise RecError "illegal schematic variable(s)";
    7.41 +    val (lhs, rhs) =
    7.42 +        if null (term_vars eq) then
    7.43 +            dest_eqn eq handle _ => raise RecError "not a proper equation"
    7.44 +        else raise RecError "illegal schematic variable(s)";
    7.45  
    7.46      val (recfun, args) = strip_comb lhs;
    7.47 -    val (fname, ftype) = dest_Const recfun handle _ => 
    7.48 +    val (fname, ftype) = dest_Const recfun handle _ =>
    7.49        raise RecError "function is not declared as constant in theory";
    7.50  
    7.51      val (ls_frees, rest)  = take_prefix is_Free args;
    7.52      val (middle, rs_frees) = take_suffix is_Free rest;
    7.53  
    7.54 -    val (constr, cargs_frees) = 
    7.55 +    val (constr, cargs_frees) =
    7.56        if null middle then raise RecError "constructor missing"
    7.57        else strip_comb (hd middle);
    7.58      val (cname, _) = dest_Const constr
    7.59 @@ -52,9 +60,9 @@
    7.60        handle _ =>
    7.61        raise RecError "cannot determine datatype associated with function"
    7.62  
    7.63 -    val (ls, cargs, rs) = (map dest_Free ls_frees, 
    7.64 -			   map dest_Free cargs_frees, 
    7.65 -			   map dest_Free rs_frees)
    7.66 +    val (ls, cargs, rs) = (map dest_Free ls_frees,
    7.67 +                           map dest_Free cargs_frees,
    7.68 +                           map dest_Free rs_frees)
    7.69        handle _ => raise RecError "illegal argument in pattern";
    7.70      val lfrees = ls @ rs @ cargs;
    7.71  
    7.72 @@ -63,31 +71,31 @@
    7.73      val new_eqn = (cname, (rhs, cargs, eq))
    7.74  
    7.75    in
    7.76 -    if not (null (duplicates lfrees)) then 
    7.77 -      raise RecError "repeated variable name in pattern" 
    7.78 +    if not (null (duplicates lfrees)) then
    7.79 +      raise RecError "repeated variable name in pattern"
    7.80      else if not ((map dest_Free (term_frees rhs)) subset lfrees) then
    7.81        raise RecError "extra variables on rhs"
    7.82 -    else if length middle > 1 then 
    7.83 +    else if length middle > 1 then
    7.84        raise RecError "more than one non-variable in pattern"
    7.85      else case rec_fn_opt of
    7.86          None => Some (fname, ftype, ls, rs, con_info, [new_eqn])
    7.87 -      | Some (fname', _, ls', rs', con_info': constructor_info, eqns) => 
    7.88 -	  if is_some (assoc (eqns, cname)) then
    7.89 -	    raise RecError "constructor already occurred as pattern"
    7.90 -	  else if (ls <> ls') orelse (rs <> rs') then
    7.91 -	    raise RecError "non-recursive arguments are inconsistent"
    7.92 -	  else if #big_rec_name con_info <> #big_rec_name con_info' then
    7.93 -	     raise RecError ("Mixed datatypes for function " ^ fname)
    7.94 -	  else if fname <> fname' then
    7.95 -	     raise RecError ("inconsistent functions for datatype " ^ 
    7.96 -			     #big_rec_name con_info)
    7.97 -	  else Some (fname, ftype, ls, rs, con_info, new_eqn::eqns)
    7.98 +      | Some (fname', _, ls', rs', con_info': constructor_info, eqns) =>
    7.99 +          if is_some (assoc (eqns, cname)) then
   7.100 +            raise RecError "constructor already occurred as pattern"
   7.101 +          else if (ls <> ls') orelse (rs <> rs') then
   7.102 +            raise RecError "non-recursive arguments are inconsistent"
   7.103 +          else if #big_rec_name con_info <> #big_rec_name con_info' then
   7.104 +             raise RecError ("Mixed datatypes for function " ^ fname)
   7.105 +          else if fname <> fname' then
   7.106 +             raise RecError ("inconsistent functions for datatype " ^
   7.107 +                             #big_rec_name con_info)
   7.108 +          else Some (fname, ftype, ls, rs, con_info, new_eqn::eqns)
   7.109    end
   7.110    handle RecError s => primrec_eq_err (sign_of thy) s eq;
   7.111  
   7.112  
   7.113  (*Instantiates a recursor equation with constructor arguments*)
   7.114 -fun inst_recursor ((_ $ constr, rhs), cargs') = 
   7.115 +fun inst_recursor ((_ $ constr, rhs), cargs') =
   7.116      subst_atomic (#2 (strip_comb constr) ~~ map Free cargs') rhs;
   7.117  
   7.118  
   7.119 @@ -111,27 +119,27 @@
   7.120      (*Translate rec equations into function arguments suitable for recursor.
   7.121        Missing cases are replaced by 0 and all cases are put into order.*)
   7.122      fun add_case ((cname, recursor_pair), cases) =
   7.123 -      let val (rhs, recursor_rhs, eq) = 
   7.124 -	    case assoc (eqns, cname) of
   7.125 -		None => (warning ("no equation for constructor " ^ cname ^
   7.126 -				  "\nin definition of function " ^ fname);
   7.127 -			 (Const ("0", Ind_Syntax.iT), 
   7.128 -			  #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
   7.129 -	      | Some (rhs, cargs', eq) =>
   7.130 -		    (rhs, inst_recursor (recursor_pair, cargs'), eq)
   7.131 -	  val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
   7.132 -	  val abs = foldr absterm (allowed_terms, rhs)
   7.133 -      in 
   7.134 +      let val (rhs, recursor_rhs, eq) =
   7.135 +            case assoc (eqns, cname) of
   7.136 +                None => (warning ("no equation for constructor " ^ cname ^
   7.137 +                                  "\nin definition of function " ^ fname);
   7.138 +                         (Const ("0", Ind_Syntax.iT),
   7.139 +                          #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
   7.140 +              | Some (rhs, cargs', eq) =>
   7.141 +                    (rhs, inst_recursor (recursor_pair, cargs'), eq)
   7.142 +          val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
   7.143 +          val abs = foldr absterm (allowed_terms, rhs)
   7.144 +      in
   7.145            if !Ind_Syntax.trace then
   7.146 -	      writeln ("recursor_rhs = " ^ 
   7.147 -		       Sign.string_of_term (sign_of thy) recursor_rhs ^
   7.148 -		       "\nabs = " ^ Sign.string_of_term (sign_of thy) abs)
   7.149 +              writeln ("recursor_rhs = " ^
   7.150 +                       Sign.string_of_term (sign_of thy) recursor_rhs ^
   7.151 +                       "\nabs = " ^ Sign.string_of_term (sign_of thy) abs)
   7.152            else();
   7.153 -	  if Logic.occs (fconst, abs) then 
   7.154 -	      primrec_eq_err (sign_of thy) 
   7.155 -	           ("illegal recursive occurrences of " ^ fname)
   7.156 -		   eq
   7.157 -	  else abs :: cases
   7.158 +          if Logic.occs (fconst, abs) then
   7.159 +              primrec_eq_err (sign_of thy)
   7.160 +                   ("illegal recursive occurrences of " ^ fname)
   7.161 +                   eq
   7.162 +          else abs :: cases
   7.163        end
   7.164  
   7.165      val recursor = head_of (#1 (hd recursor_pairs))
   7.166 @@ -140,58 +148,68 @@
   7.167  
   7.168      (*the recursive argument*)
   7.169      val rec_arg = Free (variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
   7.170 -			Ind_Syntax.iT)
   7.171 +                        Ind_Syntax.iT)
   7.172  
   7.173      val def_tm = Logic.mk_equals
   7.174 -	            (subst_bound (rec_arg, fabs),
   7.175 -		     list_comb (recursor,
   7.176 -				foldr add_case (cnames ~~ recursor_pairs, []))
   7.177 -		     $ rec_arg)
   7.178 +                    (subst_bound (rec_arg, fabs),
   7.179 +                     list_comb (recursor,
   7.180 +                                foldr add_case (cnames ~~ recursor_pairs, []))
   7.181 +                     $ rec_arg)
   7.182  
   7.183    in
   7.184        if !Ind_Syntax.trace then
   7.185 -	    writeln ("primrec def:\n" ^ 
   7.186 -		     Sign.string_of_term (sign_of thy) def_tm)
   7.187 +            writeln ("primrec def:\n" ^
   7.188 +                     Sign.string_of_term (sign_of thy) def_tm)
   7.189        else();
   7.190        (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
   7.191         def_tm)
   7.192    end;
   7.193  
   7.194  
   7.195 -
   7.196  (* prepare functions needed for definitions *)
   7.197  
   7.198 -(*Each equation is paired with an optional name, which is "_" (ML wildcard)
   7.199 -  if omitted.*)
   7.200 -fun add_primrec_i recursion_eqns thy =
   7.201 +fun add_primrec_i args thy =
   7.202    let
   7.203 -    val Some (fname, ftype, ls, rs, con_info, eqns) = 
   7.204 -	foldr (process_eqn thy) (map snd recursion_eqns, None);
   7.205 -    val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns) 
   7.206 -    val (thy', [def_thm]) = thy |> Theory.add_path (Sign.base_name (#1 def))
   7.207 -                   |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]
   7.208 +    val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args);
   7.209 +    val Some (fname, ftype, ls, rs, con_info, eqns) =
   7.210 +      foldr (process_eqn thy) (eqn_terms, None);
   7.211 +    val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
   7.212 +
   7.213 +    val (thy1, [def_thm]) = thy
   7.214 +      |> Theory.add_path (Sign.base_name (#1 def))
   7.215 +      |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
   7.216 +
   7.217      val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
   7.218 -    val char_thms = 
   7.219 -	(if !Ind_Syntax.trace then	(* FIXME message / quiet_mode (!?) *)
   7.220 -	     writeln ("Proving equations for primrec function " ^ fname)
   7.221 -	 else ();
   7.222 -	 map (fn (_,t) =>
   7.223 -	      prove_goalw_cterm rewrites
   7.224 -		(Ind_Syntax.traceIt "next primrec equation = "
   7.225 -		 (cterm_of (sign_of thy') t))
   7.226 -	      (fn _ => [rtac refl 1]))
   7.227 -	 recursion_eqns);
   7.228 -    val simps = char_thms;
   7.229 -    val thy'' = thy' 
   7.230 -      |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
   7.231 -      |> (#1 o PureThy.add_thms (map (rpair [])
   7.232 -         (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ simps))))
   7.233 +    val eqn_thms =
   7.234 +      (message ("Proving equations for primrec function " ^ fname);
   7.235 +      map (fn t => prove_goalw_cterm rewrites
   7.236 +        (Ind_Syntax.traceIt "next primrec equation = " (cterm_of (sign_of thy1) t))
   7.237 +        (fn _ => [rtac refl 1])) eqn_terms);
   7.238 +
   7.239 +    val (thy2, eqn_thms') = thy1 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
   7.240 +    val thy3 = thy2
   7.241 +      |> (#1 o PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])])
   7.242        |> Theory.parent_path;
   7.243 -  in
   7.244 -    (thy'', char_thms)
   7.245 -  end;
   7.246 +  in (thy3, eqn_thms') end;
   7.247 +
   7.248 +fun add_primrec args thy =
   7.249 +  add_primrec_i (map (fn ((name, s), srcs) =>
   7.250 +    ((name, Sign.simple_read_term (sign_of thy) propT s), map (Attrib.global_attribute thy) srcs))
   7.251 +    args) thy;
   7.252 +
   7.253 +
   7.254 +(* outer syntax *)
   7.255  
   7.256 -fun add_primrec eqns thy =
   7.257 -  add_primrec_i (map (apsnd (Sign.simple_read_term (sign_of thy) propT)) eqns) thy;
   7.258 +local structure P = OuterParse and K = OuterSyntax.Keyword in
   7.259 +
   7.260 +val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment);
   7.261 +
   7.262 +val primrecP =
   7.263 +  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
   7.264 +    (primrec_decl >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
   7.265 +
   7.266 +val _ = OuterSyntax.add_parsers [primrecP];
   7.267  
   7.268  end;
   7.269 +
   7.270 +end;
     8.1 --- a/src/ZF/thy_syntax.ML	Wed Nov 14 18:46:07 2001 +0100
     8.2 +++ b/src/ZF/thy_syntax.ML	Wed Nov 14 18:46:30 2001 +0100
     8.3 @@ -10,19 +10,18 @@
     8.4  
     8.5  open ThyParse;
     8.6  
     8.7 -(*ML identifiers for introduction rules.*)
     8.8 -fun mk_intr_name suffix s =  
     8.9 +fun mk_bind suffix s =
    8.10      if ThmDatabase.is_ml_identifier s then
    8.11 -	"op " ^ s ^ suffix  (*the "op" cancels any infix status*)
    8.12 +        "op " ^ s ^ suffix  (*the "op" cancels any infix status*)
    8.13      else "_";               (*bad name, don't try to bind*)
    8.14  
    8.15  
    8.16  (*For lists of theorems.  Either a string (an ML list expression) or else
    8.17    a list of identifiers.*)
    8.18 -fun optlist s = 
    8.19 -    optional (s $$-- 
    8.20 -	      (string >> unenclose
    8.21 -	       || list1 (name>>unenclose) >> mk_list)) 
    8.22 +fun optlist s =
    8.23 +    optional (s $$--
    8.24 +              (string >> unenclose
    8.25 +               || list1 (name>>unenclose) >> mk_list))
    8.26      "[]";
    8.27  
    8.28  (*Skipping initial blanks, find the first identifier*)  (* FIXME slightly broken! *)
    8.29 @@ -33,42 +32,43 @@
    8.30          (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
    8.31      |> #1;
    8.32  
    8.33 -(*(Co)Inductive definitions theory section."*)
    8.34 +
    8.35 +(* (Co)Inductive definitions *)
    8.36 +
    8.37  fun inductive_decl coind =
    8.38 -  let  
    8.39 -    fun mk_params ((((((recs, sdom_sum), ipairs), 
    8.40 +  let
    8.41 +    fun mk_params ((((((recs, sdom_sum), ipairs),
    8.42                        monos), con_defs), type_intrs), type_elims) =
    8.43 -      let val big_rec_name = space_implode "_" 
    8.44 +      let val big_rec_name = space_implode "_"
    8.45                             (map (scan_to_id o unenclose) recs)
    8.46            and srec_tms = mk_list recs
    8.47            and sintrs   =
    8.48              mk_big_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) ipairs)
    8.49 -          and inames   = mk_list (map (mk_intr_name "" o fst) ipairs)
    8.50 +          and inames   = mk_list (map (mk_bind "" o fst) ipairs)
    8.51        in
    8.52 -	 ";\n\n\
    8.53 -	 \local\n\
    8.54 -	 \val (thy, {defs, intrs, elim, mk_cases, \
    8.55 -		    \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
    8.56 -	 \  " ^
    8.57 -	 (if coind then "Co" else "") ^ 
    8.58 -	 "Ind_Package.add_inductive_x (" ^  srec_tms ^ ", " ^ sdom_sum ^ ") " ^
    8.59 -	  sintrs ^ " (" ^ monos ^ ", " ^ con_defs ^ ", " ^ 
    8.60 -	  type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
    8.61 -	 \in\n\
    8.62 -	 \structure " ^ big_rec_name ^ " =\n\
    8.63 -	 \struct\n\
    8.64 -	 \  val defs = defs\n\
    8.65 -	 \  val bnd_mono = bnd_mono\n\
    8.66 -	 \  val dom_subset = dom_subset\n\
    8.67 -	 \  val intrs = intrs\n\
    8.68 -	 \  val elim = elim\n\
    8.69 -	 \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
    8.70 -	 \  val mutual_induct = mutual_induct\n\
    8.71 -	 \  val mk_cases = mk_cases\n\
    8.72 -	 \  val " ^ inames ^ " = intrs\n\
    8.73 -	 \end;\n\
    8.74 -	 \val thy = thy;\nend;\n\
    8.75 -	 \val thy = thy\n"
    8.76 +         ";\n\n\
    8.77 +         \local\n\
    8.78 +         \val (thy, {defs, intrs, elim, mk_cases, \
    8.79 +                    \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
    8.80 +         \  " ^
    8.81 +         (if coind then "Co" else "") ^
    8.82 +         "Ind_Package.add_inductive_x (" ^  srec_tms ^ ", " ^ sdom_sum ^ ") " ^ sintrs ^
    8.83 +           " (" ^ monos ^ ", " ^ con_defs ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
    8.84 +         \in\n\
    8.85 +         \structure " ^ big_rec_name ^ " =\n\
    8.86 +         \struct\n\
    8.87 +         \  val defs = defs\n\
    8.88 +         \  val bnd_mono = bnd_mono\n\
    8.89 +         \  val dom_subset = dom_subset\n\
    8.90 +         \  val intrs = intrs\n\
    8.91 +         \  val elim = elim\n\
    8.92 +         \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
    8.93 +         \  val mutual_induct = mutual_induct\n\
    8.94 +         \  val mk_cases = mk_cases\n\
    8.95 +         \  val " ^ inames ^ " = intrs\n\
    8.96 +         \end;\n\
    8.97 +         \val thy = thy;\nend;\n\
    8.98 +         \val thy = thy\n"
    8.99        end
   8.100      val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
   8.101      val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
   8.102 @@ -78,54 +78,53 @@
   8.103    end;
   8.104  
   8.105  
   8.106 -(*Datatype definitions theory section.   co is true for codatatypes*)
   8.107 +(* Datatype definitions *)
   8.108 +
   8.109  fun datatype_decl coind =
   8.110    let
   8.111 -    (*generate strings*)
   8.112      fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
   8.113      val mk_data = mk_list o map mk_const o snd
   8.114      val mk_scons = mk_big_list o map mk_data
   8.115      fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
   8.116        let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs
   8.117 -	  val big_rec_name = space_implode "_" rec_names
   8.118 -	  and srec_tms = mk_list (map fst rec_pairs)
   8.119 -	  and scons    = mk_scons rec_pairs
   8.120 -	  val con_names = flat (map (map (unenclose o #1 o #1) o snd)
   8.121 -				rec_pairs)
   8.122 -          val inames = mk_list (map (mk_intr_name "_I") con_names)
   8.123 +          val big_rec_name = space_implode "_" rec_names
   8.124 +          and srec_tms = mk_list (map fst rec_pairs)
   8.125 +          and scons    = mk_scons rec_pairs
   8.126 +          val con_names = flat (map (map (unenclose o #1 o #1) o snd)
   8.127 +                                rec_pairs)
   8.128 +          val inames = mk_list (map (mk_bind "_I") con_names)
   8.129        in
   8.130 -	 ";\n\n\
   8.131 -	 \local\n\
   8.132 -	 \val (thy,\n\
   8.133 +         ";\n\n\
   8.134 +         \local\n\
   8.135 +         \val (thy,\n\
   8.136           \     {defs, intrs, elim, mk_cases, \
   8.137 -		    \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
   8.138 +                    \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
   8.139           \     {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\
   8.140 -	 \  " ^
   8.141 -	 (if coind then "Co" else "") ^ 
   8.142 -	 "Data_Package.add_datatype (" ^  sdom ^ ", " ^ srec_tms ^ ", " ^
   8.143 -	  scons ^ ", " ^ monos ^ ", " ^ 
   8.144 -	  type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
   8.145 -	 \in\n\
   8.146 -	 \structure " ^ big_rec_name ^ " =\n\
   8.147 -	 \struct\n\
   8.148 -	 \  val defs = defs\n\
   8.149 -	 \  val bnd_mono = bnd_mono\n\
   8.150 -	 \  val dom_subset = dom_subset\n\
   8.151 -	 \  val intrs = intrs\n\
   8.152 -	 \  val elim = elim\n\
   8.153 -	 \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
   8.154 -	 \  val mutual_induct = mutual_induct\n\
   8.155 -	 \  val mk_cases = mk_cases\n\
   8.156 -	 \  val con_defs = con_defs\n\
   8.157 -	 \  val case_eqns = case_eqns\n\
   8.158 -	 \  val recursor_eqns = recursor_eqns\n\
   8.159 -	 \  val free_iffs = free_iffs\n\
   8.160 -	 \  val free_SEs = free_SEs\n\
   8.161 -	 \  val mk_free = mk_free\n\
   8.162 -	 \  val " ^ inames ^ " = intrs;\n\
   8.163 -	 \end;\n\
   8.164 -	 \val thy = thy;\nend;\n\
   8.165 -	 \val thy = thy\n"
   8.166 +         \  " ^
   8.167 +         (if coind then "Co" else "") ^
   8.168 +         "Data_Package.add_datatype_x (" ^  sdom ^ ", " ^ srec_tms ^ ") " ^ scons ^
   8.169 +           " (" ^ monos ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
   8.170 +         \in\n\
   8.171 +         \structure " ^ big_rec_name ^ " =\n\
   8.172 +         \struct\n\
   8.173 +         \  val defs = defs\n\
   8.174 +         \  val bnd_mono = bnd_mono\n\
   8.175 +         \  val dom_subset = dom_subset\n\
   8.176 +         \  val intrs = intrs\n\
   8.177 +         \  val elim = elim\n\
   8.178 +         \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
   8.179 +         \  val mutual_induct = mutual_induct\n\
   8.180 +         \  val mk_cases = mk_cases\n\
   8.181 +         \  val con_defs = con_defs\n\
   8.182 +         \  val case_eqns = case_eqns\n\
   8.183 +         \  val recursor_eqns = recursor_eqns\n\
   8.184 +         \  val free_iffs = free_iffs\n\
   8.185 +         \  val free_SEs = free_SEs\n\
   8.186 +         \  val mk_free = mk_free\n\
   8.187 +         \  val " ^ inames ^ " = intrs;\n\
   8.188 +         \end;\n\
   8.189 +         \val thy = thy;\nend;\n\
   8.190 +         \val thy = thy\n"
   8.191        end
   8.192      val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
   8.193      val construct = name -- string_list -- opt_mixfix;
   8.194 @@ -136,6 +135,7 @@
   8.195  end;
   8.196  
   8.197  
   8.198 +
   8.199  (** rep_datatype **)
   8.200  
   8.201  fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) =
   8.202 @@ -143,27 +143,25 @@
   8.203    mk_list case_eqns ^ " " ^ mk_list recursor_eqns;
   8.204  
   8.205  val rep_datatype_decl =
   8.206 -  (("elim" $$-- ident) -- 
   8.207 +  (("elim" $$-- ident) --
   8.208     ("induct" $$-- ident) --
   8.209 -   ("case_eqns" $$-- list1 ident) -- 
   8.210 +   ("case_eqns" $$-- list1 ident) --
   8.211     optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string;
   8.212  
   8.213  
   8.214 +
   8.215  (** primrec **)
   8.216  
   8.217  fun mk_primrec_decl eqns =
   8.218 -  let val names = map fst eqns
   8.219 -  in
   8.220 -    ";\nval (thy, " ^ mk_list names ^
   8.221 -    ") = PrimrecPackage.add_primrec " ^
   8.222 -      mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
   8.223 +  let val binds = map (mk_bind "" o fst) eqns in
   8.224 +    ";\nval (thy, " ^ mk_list binds ^ ") = PrimrecPackage.add_primrec " ^
   8.225 +      mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
   8.226      \val thy = thy\n"
   8.227    end;
   8.228  
   8.229  (* either names and axioms or just axioms *)
   8.230 -val primrec_decl = 
   8.231 -    ((repeat1 ((ident -- string) || (string >> pair "_")))) >> mk_primrec_decl;
   8.232 -
   8.233 +val primrec_decl =
   8.234 +    ((repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
   8.235  
   8.236  
   8.237