1.1 --- a/src/HOL/BNF_LFP.thy	Wed Apr 23 10:23:26 2014 +0200
     1.2 +++ b/src/HOL/BNF_LFP.thy	Wed Apr 23 10:23:27 2014 +0200
     1.3 @@ -212,7 +212,35 @@
     1.4  ML_file "Tools/BNF/bnf_lfp.ML"
     1.5  ML_file "Tools/BNF/bnf_lfp_compat.ML"
     1.6  ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
     1.7 +
     1.8 +
     1.9 +subsection {* Size of a datatype value *}
    1.10 +
    1.11  ML_file "Tools/BNF/bnf_lfp_size.ML"
    1.12 +ML_file "Tools/Function/size.ML"
    1.13 +setup Size.setup
    1.14 +
    1.15 +lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    1.16 +  by (cases b) auto
    1.17 +
    1.18 +lemma nat_size[simp, code]: "size (n\<Colon>nat) = n"
    1.19 +  by (induct n) simp_all
    1.20 +
    1.21 +declare prod.size[no_atp]
    1.22 +
    1.23 +lemma sum_size_o_map: "sum_size g1 g2 \<circ> map_sum f1 f2 = sum_size (g1 \<circ> f1) (g2 \<circ> f2)"
    1.24 +  by (rule ext) (case_tac x, auto)
    1.25 +
    1.26 +lemma prod_size_o_map: "prod_size g1 g2 \<circ> map_prod f1 f2 = prod_size (g1 \<circ> f1) (g2 \<circ> f2)"
    1.27 +  by (rule ext) auto
    1.28 +
    1.29 +setup {*
    1.30 +BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size}
    1.31 +  @{thms sum_size_o_map}
    1.32 +#> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size}
    1.33 +  @{thms prod_size_o_map}
    1.34 +*}
    1.35 +
    1.36  
    1.37  hide_fact (open) id_transfer
    1.38  

     2.1 --- a/src/HOL/Fun_Def.thy	Wed Apr 23 10:23:26 2014 +0200
     2.2 +++ b/src/HOL/Fun_Def.thy	Wed Apr 23 10:23:27 2014 +0200
     2.3 @@ -111,7 +111,8 @@
     2.4    #> Function_Fun.setup
     2.5  *}
     2.6  
     2.7 -subsection {* Measure Functions *}
     2.8 +
     2.9 +subsection {* Measure functions *}
    2.10  
    2.11  inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
    2.12  where is_measure_trivial: "is_measure f"
    2.13 @@ -137,7 +138,7 @@
    2.14  setup Lexicographic_Order.setup
    2.15  
    2.16  
    2.17 -subsection {* Congruence Rules *}
    2.18 +subsection {* Congruence rules *}
    2.19  
    2.20  lemma let_cong [fundef_cong]:
    2.21    "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
    2.22 @@ -156,22 +157,22 @@
    2.23    "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
    2.24    unfolding o_apply .
    2.25  
    2.26 +
    2.27  subsection {* Simp rules for termination proofs *}
    2.28  
    2.29 -lemma termination_basic_simps[termination_simp]:
    2.30 -  "x < (y::nat) \<Longrightarrow> x < y + z"
    2.31 -  "x < z \<Longrightarrow> x < y + z"
    2.32 -  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
    2.33 -  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
    2.34 -  "x < y \<Longrightarrow> x \<le> (y::nat)"
    2.35 -by arith+
    2.36 -
    2.37 -declare le_imp_less_Suc[termination_simp]
    2.38 +declare
    2.39 +  trans_less_add1[termination_simp]
    2.40 +  trans_less_add2[termination_simp]
    2.41 +  trans_le_add1[termination_simp]
    2.42 +  trans_le_add2[termination_simp]
    2.43 +  less_imp_le_nat[termination_simp]
    2.44 +  le_imp_less_Suc[termination_simp]
    2.45  
    2.46  lemma prod_size_simp[termination_simp]:
    2.47    "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
    2.48  by (induct p) auto
    2.49  
    2.50 +
    2.51  subsection {* Decomposition *}
    2.52  
    2.53  lemma less_by_empty:
    2.54 @@ -185,7 +186,7 @@
    2.55  by (auto simp add: wf_comp_self[of R])
    2.56  
    2.57  
    2.58 -subsection {* Reduction Pairs *}
    2.59 +subsection {* Reduction pairs *}
    2.60  
    2.61  definition
    2.62    "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"

     3.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Apr 23 10:23:26 2014 +0200
     3.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Apr 23 10:23:27 2014 +0200
     3.3 @@ -28,7 +28,7 @@
     3.4    by (auto intro: lazy_sequence_eqI)
     3.5  
     3.6  lemma lazy_sequence_size_eq:
     3.7 -  "lazy_sequence_size f xq = Suc (list_size f (list_of_lazy_sequence xq))"
     3.8 +  "lazy_sequence_size f xq = Suc (size_list f (list_of_lazy_sequence xq))"
     3.9    by (cases xq) simp
    3.10  
    3.11  lemma size_lazy_sequence_eq [code]:

     4.1 --- a/src/HOL/Library/IArray.thy	Wed Apr 23 10:23:26 2014 +0200
     4.2 +++ b/src/HOL/Library/IArray.thy	Wed Apr 23 10:23:27 2014 +0200
     4.3 @@ -59,7 +59,7 @@
     4.4  by (cases as) simp
     4.5  
     4.6  lemma [code]:
     4.7 -"iarray_size f as = Suc (list_size f (IArray.list_of as))"
     4.8 +"iarray_size f as = Suc (size_list f (IArray.list_of as))"
     4.9  by (cases as) simp
    4.10  
    4.11  lemma [code]:

     5.1 --- a/src/HOL/List.thy	Wed Apr 23 10:23:26 2014 +0200
     5.2 +++ b/src/HOL/List.thy	Wed Apr 23 10:23:27 2014 +0200
     5.3 @@ -3488,8 +3488,8 @@
     5.4    "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
     5.5    by (induct xs) (auto simp add: ac_simps)
     5.6  
     5.7 -lemma (in monoid_add) list_size_conv_listsum:
     5.8 -  "list_size f xs = listsum (map f xs) + size xs"
     5.9 +lemma (in monoid_add) size_list_conv_listsum:
    5.10 +  "size_list f xs = listsum (map f xs) + size xs"
    5.11    by (induct xs) auto
    5.12  
    5.13  lemma (in monoid_add) length_concat:
    5.14 @@ -5945,28 +5945,28 @@
    5.15  
    5.16  subsection {* Size function *}
    5.17  
    5.18 -lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
    5.19 +lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (size_list f)"
    5.20  by (rule is_measure_trivial)
    5.21  
    5.22 -lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
    5.23 +lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (size_option f)"
    5.24  by (rule is_measure_trivial)
    5.25  
    5.26 -lemma list_size_estimation[termination_simp]: 
    5.27 -  "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
    5.28 +lemma size_list_estimation[termination_simp]: 
    5.29 +  "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < size_list f xs"
    5.30  by (induct xs) auto
    5.31  
    5.32 -lemma list_size_estimation'[termination_simp]: 
    5.33 -  "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
    5.34 +lemma size_list_estimation'[termination_simp]: 
    5.35 +  "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> size_list f xs"
    5.36  by (induct xs) auto
    5.37  
    5.38 -lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
    5.39 +lemma size_list_map[simp]: "size_list f (map g xs) = size_list (f o g) xs"
    5.40  by (induct xs) auto
    5.41  
    5.42 -lemma list_size_append[simp]: "list_size f (xs @ ys) = list_size f xs + list_size f ys"
    5.43 +lemma size_list_append[simp]: "size_list f (xs @ ys) = size_list f xs + size_list f ys"
    5.44  by (induct xs, auto)
    5.45  
    5.46 -lemma list_size_pointwise[termination_simp]: 
    5.47 -  "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
    5.48 +lemma size_list_pointwise[termination_simp]: 
    5.49 +  "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> size_list f xs \<le> size_list g xs"
    5.50  by (induct xs) force+
    5.51  
    5.52  
    5.53 @@ -6757,7 +6757,7 @@
    5.54  
    5.55  lemma length_transfer [transfer_rule]:
    5.56    "(list_all2 A ===> op =) length length"
    5.57 -  unfolding list_size_overloaded_def by transfer_prover
    5.58 +  unfolding size_list_overloaded_def size_list_def by transfer_prover
    5.59  
    5.60  lemma rotate1_transfer [transfer_rule]:
    5.61    "(list_all2 A ===> list_all2 A) rotate1 rotate1"

     6.1 --- a/src/HOL/Nitpick.thy	Wed Apr 23 10:23:26 2014 +0200
     6.2 +++ b/src/HOL/Nitpick.thy	Wed Apr 23 10:23:27 2014 +0200
     6.3 @@ -113,9 +113,8 @@
     6.4  
     6.5  declare nat.case [nitpick_simp del]
     6.6  
     6.7 -lemma list_size_simp [nitpick_simp]:
     6.8 -"list_size f xs = (if xs = [] then 0
     6.9 -                   else Suc (f (hd xs) + list_size f (tl xs)))"
    6.10 +lemma size_list_simp [nitpick_simp]:
    6.11 +"size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))"
    6.12  "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
    6.13  by (cases xs) auto
    6.14  
    6.15 @@ -145,8 +144,9 @@
    6.16  definition Frac :: "int \<times> int \<Rightarrow> bool" where
    6.17  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
    6.18  
    6.19 -axiomatization Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
    6.20 -           and Rep_Frac :: "'a \<Rightarrow> int \<times> int"
    6.21 +axiomatization
    6.22 +  Abs_Frac :: "int \<times> int \<Rightarrow> 'a" and
    6.23 +  Rep_Frac :: "'a \<Rightarrow> int \<times> int"
    6.24  
    6.25  definition zero_frac :: 'a where
    6.26  "zero_frac \<equiv> Abs_Frac (0, 1)"
    6.27 @@ -244,7 +244,7 @@
    6.28  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
    6.29      prod_def refl'_def wf'_def card'_def setsum'_def
    6.30      fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
    6.31 -    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    6.32 +    size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    6.33      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    6.34      plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    6.35      inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def

     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:26 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:27 2014 +0200
     7.3 @@ -8,6 +8,7 @@
     7.4  signature BNF_LFP_SIZE =
     7.5  sig
     7.6    val register_size: string -> string -> thm list -> thm list -> theory -> theory
     7.7 +  val lookup_size: theory -> string -> (string * (thm list * thm list)) option
     7.8  end;
     7.9  
    7.10  structure BNF_LFP_Size : BNF_LFP_SIZE =
    7.11 @@ -33,7 +34,9 @@
    7.12  );
    7.13  
    7.14  fun register_size T_name size_name size_simps size_o_maps =
    7.15 -  Data.map (Symtab.update_new (T_name, (size_name, (size_simps, size_o_maps))));
    7.16 +  Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps))));
    7.17 +
    7.18 +val lookup_size = Symtab.lookup o Data.get;
    7.19  
    7.20  val zero_nat = @{const zero_class.zero (nat)};
    7.21  
    7.22 @@ -224,8 +227,13 @@
    7.23  
    7.24        val maps0 = map map_of_bnf fp_bnfs;
    7.25  
    7.26 +      (* This disables much of the functionality of the size extension within a locale. It is not
    7.27 +         clear how to make the code below work with locales, given that interpretations are based on
    7.28 +         theories. *)
    7.29 +      val has_hyps = not (null (Thm.hyps_of (hd (hd rec_thmss))));
    7.30 +
    7.31        val (rec_o_map_thmss, size_o_map_thmss) =
    7.32 -        if live = 0 then
    7.33 +        if has_hyps orelse live = 0 then
    7.34            `I (replicate nn [])
    7.35          else
    7.36            let
    7.37 @@ -306,16 +314,19 @@
    7.38  
    7.39        val (_, thy4) = thy3
    7.40          |> fold_map4 (fn T_name => fn size_simps => fn rec_o_map_thms => fn size_o_map_thms =>
    7.41 -            let val qualify = Binding.qualify true (Long_Name.base_name T_name) in
    7.42 -              Global_Theory.note_thmss ""
    7.43 -                ([((qualify (Binding.name rec_o_mapN), []), [(rec_o_map_thms, [])]),
    7.44 -                  ((qualify (Binding.name sizeN),
    7.45 -                     [Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute
    7.46 -                        (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
    7.47 -                   [(size_simps, [])]),
    7.48 -                  ((qualify (Binding.name size_o_mapN), []), [(size_o_map_thms, [])])]
    7.49 -                 |> filter_out (forall (null o fst) o snd))
    7.50 -            end)
    7.51 +            if has_hyps then
    7.52 +              pair []
    7.53 +            else
    7.54 +              let val qualify = Binding.qualify true (Long_Name.base_name T_name) in
    7.55 +                Global_Theory.note_thmss ""
    7.56 +                  ([((qualify (Binding.name rec_o_mapN), []), [(rec_o_map_thms, [])]),
    7.57 +                    ((qualify (Binding.name sizeN),
    7.58 +                       [Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute
    7.59 +                          (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
    7.60 +                     [(size_simps, [])]),
    7.61 +                    ((qualify (Binding.name size_o_mapN), []), [(size_o_map_thms, [])])]
    7.62 +                   |> filter_out (forall (null o fst) o snd))
    7.63 +              end)
    7.64            T_names (map2 append size_simpss overloaded_size_simpss) rec_o_map_thmss size_o_map_thmss
    7.65          ||> Spec_Rules.add_global Spec_Rules.Equational (size_consts, size_simps);
    7.66      in

     8.1 --- a/src/HOL/Tools/Function/size.ML	Wed Apr 23 10:23:26 2014 +0200
     8.2 +++ b/src/HOL/Tools/Function/size.ML	Wed Apr 23 10:23:27 2014 +0200
     8.3 @@ -6,23 +6,12 @@
     8.4  
     8.5  signature SIZE =
     8.6  sig
     8.7 -  val size_thms: theory -> string -> thm list
     8.8    val setup: theory -> theory
     8.9  end;
    8.10  
    8.11  structure Size: SIZE =
    8.12  struct
    8.13  
    8.14 -structure Data = Theory_Data
    8.15 -(
    8.16 -  type T = (string * thm list) Symtab.table;
    8.17 -  val empty = Symtab.empty;
    8.18 -  val extend = I
    8.19 -  fun merge data = Symtab.merge (K true) data;
    8.20 -);
    8.21 -
    8.22 -val lookup_size = Data.get #> Symtab.lookup;
    8.23 -
    8.24  fun plus (t1, t2) = Const (@{const_name Groups.plus},
    8.25    HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
    8.26  
    8.27 @@ -35,15 +24,13 @@
    8.28                 map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT),
    8.29                   map (size_of_type' f g h) Ts))
    8.30           | NONE => NONE))
    8.31 -  | size_of_type f g h (TFree (s, _)) = h s
    8.32 +  | size_of_type _ _ h (TFree (s, _)) = h s
    8.33  and size_of_type' f g h T = (case size_of_type f g h T of
    8.34        NONE => Abs ("x", T, HOLogic.zero)
    8.35      | SOME t => t);
    8.36  
    8.37  fun is_poly thy (Datatype_Aux.DtType (name, dts)) =
    8.38 -      (case lookup_size thy name of
    8.39 -         NONE => false
    8.40 -       | SOME _ => exists (is_poly thy) dts)
    8.41 +      is_some (BNF_LFP_Size.lookup_size thy name) andalso exists (is_poly thy) dts
    8.42    | is_poly _ _ = true;
    8.43  
    8.44  fun constrs_of thy name =
    8.45 @@ -66,7 +53,6 @@
    8.46        thy
    8.47      else
    8.48        let
    8.49 -        val (rec_names1, rec_names2) = chop l rec_names;
    8.50          val recTs = Datatype_Aux.get_rec_types descr;
    8.51          val (recTs1, recTs2) = chop l recTs;
    8.52          val (_, (_, paramdts, _)) :: _ = descr;
    8.53 @@ -82,8 +68,8 @@
    8.54          val param_size = AList.lookup op = param_size_fs;
    8.55  
    8.56          val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
    8.57 -          map_filter (Option.map snd o lookup_size thy) |> flat;
    8.58 -        val extra_size = Option.map fst o lookup_size thy;
    8.59 +          map_filter (Option.map (fst o snd) o BNF_LFP_Size.lookup_size thy) |> flat;
    8.60 +        val extra_size = Option.map fst o BNF_LFP_Size.lookup_size thy;
    8.61  
    8.62          val (((size_names, size_fns), def_names), def_names') =
    8.63            recTs1 |> map (fn T as Type (s, _) =>
    8.64 @@ -160,7 +146,7 @@
    8.65              size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
    8.66          val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
    8.67  
    8.68 -        fun mk_unfolded_size_eq tab size_ofp fs (p as (x, T), r) =
    8.69 +        fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) =
    8.70            HOLogic.mk_eq (app fs r $ Free p,
    8.71              the (size_of_type tab extra_size size_ofp T) $ Free p);
    8.72  
    8.73 @@ -181,7 +167,7 @@
    8.74            let
    8.75              val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
    8.76              val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts);
    8.77 -            val ts = map_filter (fn (sT as (s, T), dt) =>
    8.78 +            val ts = map_filter (fn (sT as (_, T), dt) =>
    8.79                Option.map (fn sz => sz $ Free sT)
    8.80                  (if p dt then size_of_type size_of extra_size size_ofp T
    8.81                   else NONE)) (tnames ~~ Ts ~~ cargs)
    8.82 @@ -220,12 +206,13 @@
    8.83                [(size_eqns, [])])];
    8.84  
    8.85        in
    8.86 -        Data.map (fold (Symtab.update_new o apsnd (rpair size_thms))
    8.87 -          (new_type_names ~~ size_names)) thy''
    8.88 +        fold2 (fn new_type_name => fn size_name =>
    8.89 +            BNF_LFP_Size.register_size new_type_name size_name [] size_thms)
    8.90 +          new_type_names size_names thy''
    8.91        end
    8.92    end;
    8.93  
    8.94 -fun add_size_thms config (new_type_names as name :: _) thy =
    8.95 +fun add_size_thms _ (new_type_names as name :: _) thy =
    8.96    let
    8.97      val info as {descr, ...} = Datatype_Data.the_info thy name;
    8.98      val prefix = space_implode "_" (map Long_Name.base_name new_type_names);
    8.99 @@ -241,8 +228,6 @@
   8.100        |> Sign.restore_naming thy
   8.101    end;
   8.102  
   8.103 -val size_thms = snd oo (the oo lookup_size);
   8.104 -
   8.105  val setup = Datatype_Data.interpretation add_size_thms;
   8.106  
   8.107  end;

     9.1 --- a/src/HOL/Wellfounded.thy	Wed Apr 23 10:23:26 2014 +0200
     9.2 +++ b/src/HOL/Wellfounded.thy	Wed Apr 23 10:23:27 2014 +0200
     9.3 @@ -848,20 +848,6 @@
     9.4  done
     9.5  
     9.6  
     9.7 -subsection {* size of a datatype value *}
     9.8 -
     9.9 -ML_file "Tools/Function/size.ML"
    9.10 -setup Size.setup
    9.11 -
    9.12 -lemma size_bool [code]:
    9.13 -  "size (b\<Colon>bool) = 0" by (cases b) auto
    9.14 -
    9.15 -lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
    9.16 -  by (induct n) simp_all
    9.17 -
    9.18 -declare prod.size [no_atp]
    9.19 -
    9.20 -
    9.21  hide_const (open) acc accp
    9.22  
    9.23  end