# HG changeset patch
# User blanchet
# Date 1399220098 -7200
# Node ID 9df717fef2bbb85612732ef952f6735e0baf55e1
# Parent  691da43fbdd49e9ba1c524955cfb36bb5ab18367
renamed 'xxx_size' to 'size_xxx' for old datatype package

diff -r 691da43fbdd4 -r 9df717fef2bb NEWS
--- a/NEWS	Sun May 04 16:17:53 2014 +0200
+++ b/NEWS	Sun May 04 18:14:58 2014 +0200
@@ -306,8 +306,9 @@
   * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
     "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case").
     INCOMPATIBILITY.
-  * The generated constants "xxx_case" and "xxx_rec" have been renamed
-    "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
+  * The generated constants "xxx_case", "xxx_rec", and "xxx_size" have been
+    renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., "prod_case" ~>
+    "case_prod").
     INCOMPATIBILITY.
 
 * The types "'a list" and "'a option", their set and map functions, their
@@ -317,8 +318,6 @@
     Option.set ~> set_option
     Option.map ~> map_option
     option_rel ~> rel_option
-    list_size ~> size_list
-    option_size ~> size_option
   Renamed theorems:
     set_def ~> set_rec[abs_def]
     map_def ~> map_rec[abs_def]
@@ -6150,7 +6149,7 @@
 The "is_measure" predicate is logically meaningless (always true), and
 just guides the heuristic.  To find suitable measure functions, the
 termination prover sets up the goal "is_measure ?f" of the appropriate
-type and generates all solutions by prolog-style backwards proof using
+type and generates all solutions by Prolog-style backward proof using
 the declared rules.
 
 This setup also deals with rules like 
diff -r 691da43fbdd4 -r 9df717fef2bb src/Doc/Tutorial/Recdef/Nested1.thy
--- a/src/Doc/Tutorial/Recdef/Nested1.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/Doc/Tutorial/Recdef/Nested1.thy	Sun May 04 18:14:58 2014 +0200
@@ -21,9 +21,9 @@
 Remember that function @{term size} is defined for each \isacommand{datatype}.
 However, the definition does not succeed. Isabelle complains about an
 unproved termination condition
-@{prop[display]"t : set ts --> size t < Suc (term_list_size ts)"}
+@{prop[display]"t : set ts --> size t < Suc (size_term_list ts)"}
 where @{term set} returns the set of elements of a list
-and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
+and @{text"size_term_list :: term list \<Rightarrow> nat"} is an auxiliary
 function automatically defined by Isabelle
 (while processing the declaration of @{text term}).  Why does the
 recursive call of @{const trev} lead to this
@@ -31,7 +31,7 @@
 will apply @{const trev} only to elements of @{term ts}. Thus the 
 condition expresses that the size of the argument @{prop"t : set ts"} of any
 recursive call of @{const trev} is strictly less than @{term"size(App f ts)"},
-which equals @{term"Suc(term_list_size ts)"}.  We will now prove the termination condition and
+which equals @{term"Suc(size_term_list ts)"}.  We will now prove the termination condition and
 continue with our definition.  Below we return to the question of how
 \isacommand{recdef} knows about @{term map}.
 
diff -r 691da43fbdd4 -r 9df717fef2bb src/Doc/Tutorial/Recdef/Nested2.thy
--- a/src/Doc/Tutorial/Recdef/Nested2.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/Doc/Tutorial/Recdef/Nested2.thy	Sun May 04 18:14:58 2014 +0200
@@ -2,7 +2,7 @@
 theory Nested2 imports Nested0 begin
 (*>*)
 
-lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)"
+lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(size_term_list ts)"
 by(induct_tac ts, auto)
 (*<*)
 recdef trev "measure size"
@@ -55,7 +55,7 @@
 like @{term"map"}. For a start, if nothing were known about @{term"map"}, then
 @{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus
 \isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
-(term_list_size ts)"}, without any assumption about @{term"t"}.  Therefore
+(size_term_list ts)"}, without any assumption about @{term"t"}.  Therefore
 \isacommand{recdef} has been supplied with the congruence theorem
 @{thm[source]map_cong}:
 @{thm[display,margin=50]"map_cong"[no_vars]}
diff -r 691da43fbdd4 -r 9df717fef2bb src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy	Sun May 04 18:14:58 2014 +0200
@@ -195,22 +195,22 @@
 lemma size_bool[code]: "size (b\<Colon>bool) = 0"
   by (cases b) auto
 
-lemma nat_size[simp, code]: "size (n\<Colon>nat) = n"
+lemma size_nat[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)"
+lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (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)"
+lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
   by (rule ext) auto
 
 setup {*
-BNF_LFP_Size.register_size_global @{type_name sum} @{const_name sum_size} @{thms sum.size}
-  @{thms sum_size_o_map}
-#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name prod_size} @{thms prod.size}
-  @{thms prod_size_o_map}
+BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
+  @{thms size_sum_o_map}
+#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
+  @{thms size_prod_o_map}
 *}
 
 end
diff -r 691da43fbdd4 -r 9df717fef2bb src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/Code_Numeral.thy	Sun May 04 18:14:58 2014 +0200
@@ -810,10 +810,10 @@
   using assms by transfer blast
 
 lemma [simp, code]:
-  "natural_size = nat_of_natural"
+  "size_natural = nat_of_natural"
 proof (rule ext)
   fix n
-  show "natural_size n = nat_of_natural n"
+  show "size_natural n = nat_of_natural n"
     by (induct n) simp_all
 qed
 
diff -r 691da43fbdd4 -r 9df717fef2bb src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/Fun_Def.thy	Sun May 04 18:14:58 2014 +0200
@@ -168,8 +168,8 @@
   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"
+lemma size_prod_simp[termination_simp]:
+  "size_prod f g p = f (fst p) + g (snd p) + Suc 0"
 by (induct p) auto
 
 
diff -r 691da43fbdd4 -r 9df717fef2bb src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Sun May 04 18:14:58 2014 +0200
@@ -27,13 +27,10 @@
   "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
   by (auto intro: lazy_sequence_eqI)
 
-lemma lazy_sequence_size_eq:
-  "lazy_sequence_size f xq = Suc (size_list f (list_of_lazy_sequence xq))"
-  by (cases xq) simp
-
 lemma size_lazy_sequence_eq [code]:
+  "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
   "size (xq :: 'a lazy_sequence) = 0"
-  by (cases xq) simp
+  by (cases xq, simp)+
 
 lemma case_lazy_sequence [simp]:
   "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
@@ -75,11 +72,11 @@
   case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
   by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
 
-lemma lazy_sequence_size_code [code]:
-  "lazy_sequence_size s xq = (case yield xq of
+lemma size_lazy_sequence_code [code]:
+  "size_lazy_sequence s xq = (case yield xq of
     None \<Rightarrow> 1
-  | Some (x, xq') \<Rightarrow> Suc (s x + lazy_sequence_size s xq'))"
-  by (cases "list_of_lazy_sequence xq") (simp_all add: lazy_sequence_size_eq)
+  | Some (x, xq') \<Rightarrow> Suc (s x + size_lazy_sequence s xq'))"
+  by (cases "list_of_lazy_sequence xq") (simp_all add: size_lazy_sequence_eq)
 
 lemma equal_lazy_sequence_code [code]:
   "HOL.equal xq yq = (case (yield xq, yield yq) of
diff -r 691da43fbdd4 -r 9df717fef2bb src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/Library/IArray.thy	Sun May 04 18:14:58 2014 +0200
@@ -59,7 +59,7 @@
 by (cases as) simp
 
 lemma [code]:
-"iarray_size f as = Suc (size_list f (IArray.list_of as))"
+"size_iarray f as = Suc (size_list f (IArray.list_of as))"
 by (cases as) simp
 
 lemma [code]:
diff -r 691da43fbdd4 -r 9df717fef2bb src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/Library/refute.ML	Sun May 04 18:14:58 2014 +0200
@@ -2399,7 +2399,7 @@
                             end
                         end
                       val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index))
-                      (* sanity check: the size of 'IDT' should be 'idt_size' *)
+                      (* sanity check: the size of 'IDT' should be 'size_idt' *)
                       val _ =
                           if idt_size <> size_of_type ctxt (typs, []) IDT then
                             raise REFUTE ("IDT_recursion_interpreter",
diff -r 691da43fbdd4 -r 9df717fef2bb src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/Predicate.thy	Sun May 04 18:14:58 2014 +0200
@@ -498,7 +498,7 @@
   "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
 
 lemma [code]:
-  "pred_size f P = 0" by (cases P) simp
+  "size_pred f P = 0" by (cases P) simp
 
 primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
   "contained Empty Q \<longleftrightarrow> True"
diff -r 691da43fbdd4 -r 9df717fef2bb src/HOL/String.thy
--- a/src/HOL/String.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/String.thy	Sun May 04 18:14:58 2014 +0200
@@ -20,10 +20,9 @@
 qed
 
 lemma size_nibble [code, simp]:
-  "size (x::nibble) = 0" by (cases x) simp_all
-
-lemma nibble_size [code, simp]:
-  "nibble_size (x::nibble) = 0" by (cases x) simp_all
+  "size_nibble (x::nibble) = 0"
+  "size (x::nibble) = 0"
+  by (cases x, simp_all)+
 
 instantiation nibble :: enum
 begin
@@ -136,10 +135,9 @@
 qed
 
 lemma size_char [code, simp]:
-  "size (c::char) = 0" by (cases c) simp
-
-lemma char_size [code, simp]:
-  "char_size (c::char) = 0" by (cases c) simp
+  "size_char (c::char) = 0"
+  "size (c::char) = 0"
+  by (cases c, simp)+
 
 instantiation char :: enum
 begin
diff -r 691da43fbdd4 -r 9df717fef2bb src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/Tools/Function/size.ML	Sun May 04 18:14:58 2014 +0200
@@ -74,7 +74,7 @@
         val (((size_names, size_fns), def_names), def_names') =
           recTs1 |> map (fn T as Type (s, _) =>
             let
-              val s' = Long_Name.base_name s ^ "_size";
+              val s' = "size_" ^ Long_Name.base_name s;
               val s'' = Sign.full_bname thy s';
             in
               (s'',