Added overloaded function `size' for all datatypes.
authornipkow
Fri May 23 09:17:26 1997 +0200 (1997-05-23)
changeset 3308da002cef7090
parent 3307 a106a557d704
child 3309 992a25b24d0d
Added overloaded function `size' for all datatypes.
src/HOL/Arith.thy
src/HOL/NatDef.ML
src/HOL/datatype.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/Arith.thy	Thu May 22 18:29:17 1997 +0200
     1.2 +++ b/src/HOL/Arith.thy	Fri May 23 09:17:26 1997 +0200
     1.3 @@ -14,6 +14,8 @@
     1.4  consts
     1.5    pred      :: nat => nat
     1.6    div, mod  :: [nat, nat] => nat  (infixl 70)
     1.7 +  (* size of a datatype value; overloaded *)
     1.8 +  size      :: 'a => nat
     1.9  
    1.10  defs
    1.11    pred_def  "pred(m) == case m of 0 => 0 | Suc n => n"
     2.1 --- a/src/HOL/NatDef.ML	Thu May 22 18:29:17 1997 +0200
     2.2 +++ b/src/HOL/NatDef.ML	Fri May 23 09:17:26 1997 +0200
     2.3 @@ -701,6 +701,8 @@
     2.4  
     2.5  
     2.6  (* add function nat_add_primrec *) 
     2.7 -val (_, nat_add_primrec) = Datatype.add_datatype
     2.8 -([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([], "nat")], NoSyn)]) HOL.thy;
     2.9 +val (_, nat_add_primrec, _) = Datatype.add_datatype
    2.10 +([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([],
    2.11 +"nat")], NoSyn)]) (add_thyname "Arith" HOL.thy);
    2.12 +(* pretend Arith is part of the basic theory to fool package *)
    2.13  
     3.1 --- a/src/HOL/datatype.ML	Thu May 22 18:29:17 1997 +0200
     3.2 +++ b/src/HOL/datatype.ML	Fri May 23 09:17:26 1997 +0200
     3.3 @@ -143,8 +143,7 @@
     3.4  in
     3.5    fun add_datatype (typevars, tname, cons_list') thy = 
     3.6      let
     3.7 -      val dummy = if length cons_list' < dtK then ()
     3.8 -                  else require_thy thy "Nat" "datatype definitions";
     3.9 +      val dummy = require_thy thy "Arith" "datatype definitions";
    3.10        
    3.11        fun typid(dtRek(_,id)) = id
    3.12          | typid(dtVar s) = implode (tl (explode s))
    3.13 @@ -344,6 +343,19 @@
    3.14        val rules_rec = rec_rules 1 cons_list
    3.15  
    3.16  (* -------------------------------------------------------------------- *)
    3.17 +(* The size function                                                    *) 
    3.18 +
    3.19 +      fun size_eqn(_,name,types,vns,_) =
    3.20 +        let fun sum((T,vn)::args) =
    3.21 +                  if is_dtRek T then "size(" ^ vn ^ ") + " ^ sum(args)
    3.22 +                  else sum args
    3.23 +              | sum [] = "1"
    3.24 +            val rhs = if exists is_dtRek types then sum(types~~vns) else "0"
    3.25 +        in ("", "size(" ^ C_exp name vns ^ ") = " ^ rhs) end;
    3.26 +
    3.27 +      val size_eqns  = map size_eqn cons_list;
    3.28 +
    3.29 +(* -------------------------------------------------------------------- *)
    3.30        val consts = 
    3.31          map const_type cons_list
    3.32          @ (if num_of_cons < dtK then []
    3.33 @@ -413,7 +425,7 @@
    3.34             |> add_arities arities
    3.35             |> add_consts consts
    3.36             |> add_trrules xrules
    3.37 -           |> add_axioms rules, add_primrec)
    3.38 +           |> add_axioms rules, add_primrec, size_eqns)
    3.39      end
    3.40  
    3.41  (*Check if the (induction) variable occurs among the premises, which
     4.1 --- a/src/HOL/thy_syntax.ML	Thu May 22 18:29:17 1997 +0200
     4.2 +++ b/src/HOL/thy_syntax.ML	Fri May 23 09:17:26 1997 +0200
     4.3 @@ -118,9 +118,9 @@
     4.4  
     4.5    (*generate string for calling add_datatype and build_record*)
     4.6    fun mk_params ((ts, tname), cons) =
     4.7 -   ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
     4.8 +   ("val (thy," ^ tname ^ "_add_primrec," ^ tname ^ "_size_eqns) = Datatype.add_datatype\n"
     4.9      ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
    4.10 -    \val thy = thy"
    4.11 +    \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
    4.12      ,
    4.13      "structure " ^ tname ^ " =\n\
    4.14      \struct\n\
    4.15 @@ -147,7 +147,12 @@
    4.16      \val dummy = AddIffs " ^ tname ^ ".inject;\n\
    4.17      \val dummy = " ^
    4.18        (if length cons < dtK then "AddIffs " else "Addsimps ") ^
    4.19 -      tname ^ ".distinct;");
    4.20 +      tname ^ ".distinct;\n\
    4.21 +    \val dummy = Addsimps(map (fn (_,eqn) =>\n\
    4.22 +    \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
    4.23 +                     "] eqn (fn _ => [Simp_tac 1]))\n" ^
    4.24 +    tname^"_size_eqns)\n"
    4.25 +   );
    4.26  
    4.27    (*parsers*)
    4.28    val tvars = type_args >> map (cat "dtVar");