# HG changeset patch
# User blanchet
# Date 1410773875 -7200
# Node ID d109244b89aa29d996d9e92d8034ce1c3cfdd795
# Parent  568fb4e382c913bcb432c8253fbb1cd412321248
tuned definition of 'size' function to get nicer properties

diff -r 568fb4e382c9 -r d109244b89aa src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 15 11:17:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 15 11:37:55 2014 +0200
@@ -145,6 +145,24 @@
       fun mk_size_of_arg t =
         mk_size_of_typ (fastype_of t) #>> (fn s => substCnatT (betapply (s, t)));
 
+      fun is_recursive_or_plain_case Ts =
+        exists (exists_subtype_in Cs) Ts orelse forall (not o exists_subtype_in As) Ts;
+
+      (* We want the size function to enjoy the following properties:
+
+         1. The size of a list should coincide with its length.
+         2. All the nonrecursive constructors of a type should have the same size.
+         3. Each constructor through which nested recursion takes place should count as at least
+            one in the generic size function.
+         4. The "size" function should be definable as "size_t (%_. 0) ... (%_. 0)", where "size_t"
+            is the generic function.
+
+         This justifies the somewhat convoluted logic ahead. *)
+
+      val base_case =
+        if forall (is_recursive_or_plain_case o binder_types) rec_arg_Ts then HOLogic.zero
+        else HOLogic.Suc_zero;
+
       fun mk_size_arg rec_arg_T size_o_maps =
         let
           val x_Ts = binder_types rec_arg_T;
@@ -155,7 +173,7 @@
             fold_map mk_size_of_arg xs size_o_maps
             |>> remove (op =) HOLogic.zero;
           val sum =
-            if null summands then HOLogic.zero
+            if null summands then base_case
             else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
         in
           (fold_rev Term.lambda (map substCnatT xs) sum, size_o_maps')