move size hooks together, with new one preceding old one and sharing same theory data

--- a/src/HOL/BNF_LFP.thy	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/BNF_LFP.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -212,7 +212,35 @@
 ML_file "Tools/BNF/bnf_lfp.ML"
 ML_file "Tools/BNF/bnf_lfp_compat.ML"
 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
+
+
+subsection {* Size of a datatype value *}
+
 ML_file "Tools/BNF/bnf_lfp_size.ML"
+ML_file "Tools/Function/size.ML"
+setup Size.setup
+
+lemma size_bool[code]: "size (b\<Colon>bool) = 0"
+  by (cases b) auto
+
+lemma nat_size[simp, code]: "size (n\<Colon>nat) = n"
+  by (induct n) simp_all
+
+declare prod.size[no_atp]
+
+lemma sum_size_o_map: "sum_size g1 g2 \<circ> map_sum f1 f2 = sum_size (g1 \<circ> f1) (g2 \<circ> f2)"
+  by (rule ext) (case_tac x, auto)
+
+lemma prod_size_o_map: "prod_size g1 g2 \<circ> map_prod f1 f2 = prod_size (g1 \<circ> f1) (g2 \<circ> f2)"
+  by (rule ext) auto
+
+setup {*
+BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size}
+  @{thms sum_size_o_map}
+#> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size}
+  @{thms prod_size_o_map}
+*}
+
 
 hide_fact (open) id_transfer
 

--- a/src/HOL/Fun_Def.thy	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Fun_Def.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -111,7 +111,8 @@
   #> Function_Fun.setup
 *}
 
-subsection {* Measure Functions *}
+
+subsection {* Measure functions *}
 
 inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
 where is_measure_trivial: "is_measure f"
@@ -137,7 +138,7 @@
 setup Lexicographic_Order.setup
 
 
-subsection {* Congruence Rules *}
+subsection {* Congruence rules *}
 
 lemma let_cong [fundef_cong]:
   "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
@@ -156,22 +157,22 @@
   "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
   unfolding o_apply .
 
+
 subsection {* Simp rules for termination proofs *}
 
-lemma termination_basic_simps[termination_simp]:
-  "x < (y::nat) \<Longrightarrow> x < y + z"
-  "x < z \<Longrightarrow> x < y + z"
-  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
-  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
-  "x < y \<Longrightarrow> x \<le> (y::nat)"
-by arith+
-
-declare le_imp_less_Suc[termination_simp]
+declare
+  trans_less_add1[termination_simp]
+  trans_less_add2[termination_simp]
+  trans_le_add1[termination_simp]
+  trans_le_add2[termination_simp]
+  less_imp_le_nat[termination_simp]
+  le_imp_less_Suc[termination_simp]
 
 lemma prod_size_simp[termination_simp]:
   "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
 by (induct p) auto
 
+
 subsection {* Decomposition *}
 
 lemma less_by_empty:
@@ -185,7 +186,7 @@
 by (auto simp add: wf_comp_self[of R])
 
 
-subsection {* Reduction Pairs *}
+subsection {* Reduction pairs *}
 
 definition
   "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"

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

--- a/src/HOL/Library/IArray.thy	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Library/IArray.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -59,7 +59,7 @@
 by (cases as) simp
 
 lemma [code]:
-"iarray_size f as = Suc (list_size f (IArray.list_of as))"
+"iarray_size f as = Suc (size_list f (IArray.list_of as))"
 by (cases as) simp
 
 lemma [code]:

--- a/src/HOL/List.thy	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/List.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -3488,8 +3488,8 @@
   "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
   by (induct xs) (auto simp add: ac_simps)
 
-lemma (in monoid_add) list_size_conv_listsum:
-  "list_size f xs = listsum (map f xs) + size xs"
+lemma (in monoid_add) size_list_conv_listsum:
+  "size_list f xs = listsum (map f xs) + size xs"
   by (induct xs) auto
 
 lemma (in monoid_add) length_concat:
@@ -5945,28 +5945,28 @@
 
 subsection {* Size function *}
 
-lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
+lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (size_list f)"
 by (rule is_measure_trivial)
 
-lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
+lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (size_option f)"
 by (rule is_measure_trivial)
 
-lemma list_size_estimation[termination_simp]: 
-  "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
+lemma size_list_estimation[termination_simp]: 
+  "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < size_list f xs"
 by (induct xs) auto
 
-lemma list_size_estimation'[termination_simp]: 
-  "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
+lemma size_list_estimation'[termination_simp]: 
+  "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> size_list f xs"
 by (induct xs) auto
 
-lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
+lemma size_list_map[simp]: "size_list f (map g xs) = size_list (f o g) xs"
 by (induct xs) auto
 
-lemma list_size_append[simp]: "list_size f (xs @ ys) = list_size f xs + list_size f ys"
+lemma size_list_append[simp]: "size_list f (xs @ ys) = size_list f xs + size_list f ys"
 by (induct xs, auto)
 
-lemma list_size_pointwise[termination_simp]: 
-  "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
+lemma size_list_pointwise[termination_simp]: 
+  "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> size_list f xs \<le> size_list g xs"
 by (induct xs) force+
 
 
@@ -6757,7 +6757,7 @@
 
 lemma length_transfer [transfer_rule]:
   "(list_all2 A ===> op =) length length"
-  unfolding list_size_overloaded_def by transfer_prover
+  unfolding size_list_overloaded_def size_list_def by transfer_prover
 
 lemma rotate1_transfer [transfer_rule]:
   "(list_all2 A ===> list_all2 A) rotate1 rotate1"

--- a/src/HOL/Nitpick.thy	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Nitpick.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -113,9 +113,8 @@
 
 declare nat.case [nitpick_simp del]
 
-lemma list_size_simp [nitpick_simp]:
-"list_size f xs = (if xs = [] then 0
-                   else Suc (f (hd xs) + list_size f (tl xs)))"
+lemma size_list_simp [nitpick_simp]:
+"size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))"
 "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
 by (cases xs) auto
 
@@ -145,8 +144,9 @@
 definition Frac :: "int \<times> int \<Rightarrow> bool" where
 "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
 
-axiomatization Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
-           and Rep_Frac :: "'a \<Rightarrow> int \<times> int"
+axiomatization
+  Abs_Frac :: "int \<times> int \<Rightarrow> 'a" and
+  Rep_Frac :: "'a \<Rightarrow> int \<times> int"
 
 definition zero_frac :: 'a where
 "zero_frac \<equiv> Abs_Frac (0, 1)"
@@ -244,7 +244,7 @@
 hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
     prod_def refl'_def wf'_def card'_def setsum'_def
     fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
-    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
+    size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
     zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
     plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
     inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def

--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:27 2014 +0200
@@ -8,6 +8,7 @@
 signature BNF_LFP_SIZE =
 sig
   val register_size: string -> string -> thm list -> thm list -> theory -> theory
+  val lookup_size: theory -> string -> (string * (thm list * thm list)) option
 end;
 
 structure BNF_LFP_Size : BNF_LFP_SIZE =
@@ -33,7 +34,9 @@
 );
 
 fun register_size T_name size_name size_simps size_o_maps =
-  Data.map (Symtab.update_new (T_name, (size_name, (size_simps, size_o_maps))));
+  Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps))));
+
+val lookup_size = Symtab.lookup o Data.get;
 
 val zero_nat = @{const zero_class.zero (nat)};
 
@@ -224,8 +227,13 @@
 
       val maps0 = map map_of_bnf fp_bnfs;
 
+      (* This disables much of the functionality of the size extension within a locale. It is not
+         clear how to make the code below work with locales, given that interpretations are based on
+         theories. *)
+      val has_hyps = not (null (Thm.hyps_of (hd (hd rec_thmss))));
+
       val (rec_o_map_thmss, size_o_map_thmss) =
-        if live = 0 then
+        if has_hyps orelse live = 0 then
           `I (replicate nn [])
         else
           let
@@ -306,16 +314,19 @@
 
       val (_, thy4) = thy3
         |> fold_map4 (fn T_name => fn size_simps => fn rec_o_map_thms => fn size_o_map_thms =>
-            let val qualify = Binding.qualify true (Long_Name.base_name T_name) in
-              Global_Theory.note_thmss ""
-                ([((qualify (Binding.name rec_o_mapN), []), [(rec_o_map_thms, [])]),
-                  ((qualify (Binding.name sizeN),
-                     [Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute
-                        (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
-                   [(size_simps, [])]),
-                  ((qualify (Binding.name size_o_mapN), []), [(size_o_map_thms, [])])]
-                 |> filter_out (forall (null o fst) o snd))
-            end)
+            if has_hyps then
+              pair []
+            else
+              let val qualify = Binding.qualify true (Long_Name.base_name T_name) in
+                Global_Theory.note_thmss ""
+                  ([((qualify (Binding.name rec_o_mapN), []), [(rec_o_map_thms, [])]),
+                    ((qualify (Binding.name sizeN),
+                       [Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute
+                          (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
+                     [(size_simps, [])]),
+                    ((qualify (Binding.name size_o_mapN), []), [(size_o_map_thms, [])])]
+                   |> filter_out (forall (null o fst) o snd))
+              end)
           T_names (map2 append size_simpss overloaded_size_simpss) rec_o_map_thmss size_o_map_thmss
         ||> Spec_Rules.add_global Spec_Rules.Equational (size_consts, size_simps);
     in

--- a/src/HOL/Tools/Function/size.ML	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/Function/size.ML	Wed Apr 23 10:23:27 2014 +0200
@@ -6,23 +6,12 @@
 
 signature SIZE =
 sig
-  val size_thms: theory -> string -> thm list
   val setup: theory -> theory
 end;
 
 structure Size: SIZE =
 struct
 
-structure Data = Theory_Data
-(
-  type T = (string * thm list) Symtab.table;
-  val empty = Symtab.empty;
-  val extend = I
-  fun merge data = Symtab.merge (K true) data;
-);
-
-val lookup_size = Data.get #> Symtab.lookup;
-
 fun plus (t1, t2) = Const (@{const_name Groups.plus},
   HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
 
@@ -35,15 +24,13 @@
                map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT),
                  map (size_of_type' f g h) Ts))
          | NONE => NONE))
-  | size_of_type f g h (TFree (s, _)) = h s
+  | size_of_type _ _ h (TFree (s, _)) = h s
 and size_of_type' f g h T = (case size_of_type f g h T of
       NONE => Abs ("x", T, HOLogic.zero)
     | SOME t => t);
 
 fun is_poly thy (Datatype_Aux.DtType (name, dts)) =
-      (case lookup_size thy name of
-         NONE => false
-       | SOME _ => exists (is_poly thy) dts)
+      is_some (BNF_LFP_Size.lookup_size thy name) andalso exists (is_poly thy) dts
   | is_poly _ _ = true;
 
 fun constrs_of thy name =
@@ -66,7 +53,6 @@
       thy
     else
       let
-        val (rec_names1, rec_names2) = chop l rec_names;
         val recTs = Datatype_Aux.get_rec_types descr;
         val (recTs1, recTs2) = chop l recTs;
         val (_, (_, paramdts, _)) :: _ = descr;
@@ -82,8 +68,8 @@
         val param_size = AList.lookup op = param_size_fs;
 
         val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
-          map_filter (Option.map snd o lookup_size thy) |> flat;
-        val extra_size = Option.map fst o lookup_size thy;
+          map_filter (Option.map (fst o snd) o BNF_LFP_Size.lookup_size thy) |> flat;
+        val extra_size = Option.map fst o BNF_LFP_Size.lookup_size thy;
 
         val (((size_names, size_fns), def_names), def_names') =
           recTs1 |> map (fn T as Type (s, _) =>
@@ -160,7 +146,7 @@
             size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
         val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
 
-        fun mk_unfolded_size_eq tab size_ofp fs (p as (x, T), r) =
+        fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) =
           HOLogic.mk_eq (app fs r $ Free p,
             the (size_of_type tab extra_size size_ofp T) $ Free p);
 
@@ -181,7 +167,7 @@
           let
             val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
             val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts);
-            val ts = map_filter (fn (sT as (s, T), dt) =>
+            val ts = map_filter (fn (sT as (_, T), dt) =>
               Option.map (fn sz => sz $ Free sT)
                 (if p dt then size_of_type size_of extra_size size_ofp T
                  else NONE)) (tnames ~~ Ts ~~ cargs)
@@ -220,12 +206,13 @@
               [(size_eqns, [])])];
 
       in
-        Data.map (fold (Symtab.update_new o apsnd (rpair size_thms))
-          (new_type_names ~~ size_names)) thy''
+        fold2 (fn new_type_name => fn size_name =>
+            BNF_LFP_Size.register_size new_type_name size_name [] size_thms)
+          new_type_names size_names thy''
       end
   end;
 
-fun add_size_thms config (new_type_names as name :: _) thy =
+fun add_size_thms _ (new_type_names as name :: _) thy =
   let
     val info as {descr, ...} = Datatype_Data.the_info thy name;
     val prefix = space_implode "_" (map Long_Name.base_name new_type_names);
@@ -241,8 +228,6 @@
       |> Sign.restore_naming thy
   end;
 
-val size_thms = snd oo (the oo lookup_size);
-
 val setup = Datatype_Data.interpretation add_size_thms;
 
 end;

--- a/src/HOL/Wellfounded.thy	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -848,20 +848,6 @@
 done
 
 
-subsection {* size of a datatype value *}
-
-ML_file "Tools/Function/size.ML"
-setup Size.setup
-
-lemma size_bool [code]:
-  "size (b\<Colon>bool) = 0" by (cases b) auto
-
-lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
-  by (induct n) simp_all
-
-declare prod.size [no_atp]
-
-
 hide_const (open) acc accp
 
 end