renamed 'xxx_size' to 'size_xxx' for old datatype package
authorblanchet
Sun May 04 18:14:58 2014 +0200 (2014-05-04)
changeset 568469df717fef2bb
parent 56845 691da43fbdd4
child 56847 3e369d8610c4
renamed 'xxx_size' to 'size_xxx' for old datatype package
NEWS
src/Doc/Tutorial/Recdef/Nested1.thy
src/Doc/Tutorial/Recdef/Nested2.thy
src/HOL/BNF_FP_Base.thy
src/HOL/Code_Numeral.thy
src/HOL/Fun_Def.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Library/IArray.thy
src/HOL/Library/refute.ML
src/HOL/Predicate.thy
src/HOL/String.thy
src/HOL/Tools/Function/size.ML
     1.1 --- a/NEWS	Sun May 04 16:17:53 2014 +0200
     1.2 +++ b/NEWS	Sun May 04 18:14:58 2014 +0200
     1.3 @@ -306,8 +306,9 @@
     1.4    * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
     1.5      "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case").
     1.6      INCOMPATIBILITY.
     1.7 -  * The generated constants "xxx_case" and "xxx_rec" have been renamed
     1.8 -    "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
     1.9 +  * The generated constants "xxx_case", "xxx_rec", and "xxx_size" have been
    1.10 +    renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., "prod_case" ~>
    1.11 +    "case_prod").
    1.12      INCOMPATIBILITY.
    1.13  
    1.14  * The types "'a list" and "'a option", their set and map functions, their
    1.15 @@ -317,8 +318,6 @@
    1.16      Option.set ~> set_option
    1.17      Option.map ~> map_option
    1.18      option_rel ~> rel_option
    1.19 -    list_size ~> size_list
    1.20 -    option_size ~> size_option
    1.21    Renamed theorems:
    1.22      set_def ~> set_rec[abs_def]
    1.23      map_def ~> map_rec[abs_def]
    1.24 @@ -6150,7 +6149,7 @@
    1.25  The "is_measure" predicate is logically meaningless (always true), and
    1.26  just guides the heuristic.  To find suitable measure functions, the
    1.27  termination prover sets up the goal "is_measure ?f" of the appropriate
    1.28 -type and generates all solutions by prolog-style backwards proof using
    1.29 +type and generates all solutions by Prolog-style backward proof using
    1.30  the declared rules.
    1.31  
    1.32  This setup also deals with rules like 
     2.1 --- a/src/Doc/Tutorial/Recdef/Nested1.thy	Sun May 04 16:17:53 2014 +0200
     2.2 +++ b/src/Doc/Tutorial/Recdef/Nested1.thy	Sun May 04 18:14:58 2014 +0200
     2.3 @@ -21,9 +21,9 @@
     2.4  Remember that function @{term size} is defined for each \isacommand{datatype}.
     2.5  However, the definition does not succeed. Isabelle complains about an
     2.6  unproved termination condition
     2.7 -@{prop[display]"t : set ts --> size t < Suc (term_list_size ts)"}
     2.8 +@{prop[display]"t : set ts --> size t < Suc (size_term_list ts)"}
     2.9  where @{term set} returns the set of elements of a list
    2.10 -and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
    2.11 +and @{text"size_term_list :: term list \<Rightarrow> nat"} is an auxiliary
    2.12  function automatically defined by Isabelle
    2.13  (while processing the declaration of @{text term}).  Why does the
    2.14  recursive call of @{const trev} lead to this
    2.15 @@ -31,7 +31,7 @@
    2.16  will apply @{const trev} only to elements of @{term ts}. Thus the 
    2.17  condition expresses that the size of the argument @{prop"t : set ts"} of any
    2.18  recursive call of @{const trev} is strictly less than @{term"size(App f ts)"},
    2.19 -which equals @{term"Suc(term_list_size ts)"}.  We will now prove the termination condition and
    2.20 +which equals @{term"Suc(size_term_list ts)"}.  We will now prove the termination condition and
    2.21  continue with our definition.  Below we return to the question of how
    2.22  \isacommand{recdef} knows about @{term map}.
    2.23  
     3.1 --- a/src/Doc/Tutorial/Recdef/Nested2.thy	Sun May 04 16:17:53 2014 +0200
     3.2 +++ b/src/Doc/Tutorial/Recdef/Nested2.thy	Sun May 04 18:14:58 2014 +0200
     3.3 @@ -2,7 +2,7 @@
     3.4  theory Nested2 imports Nested0 begin
     3.5  (*>*)
     3.6  
     3.7 -lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)"
     3.8 +lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(size_term_list ts)"
     3.9  by(induct_tac ts, auto)
    3.10  (*<*)
    3.11  recdef trev "measure size"
    3.12 @@ -55,7 +55,7 @@
    3.13  like @{term"map"}. For a start, if nothing were known about @{term"map"}, then
    3.14  @{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus
    3.15  \isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
    3.16 -(term_list_size ts)"}, without any assumption about @{term"t"}.  Therefore
    3.17 +(size_term_list ts)"}, without any assumption about @{term"t"}.  Therefore
    3.18  \isacommand{recdef} has been supplied with the congruence theorem
    3.19  @{thm[source]map_cong}:
    3.20  @{thm[display,margin=50]"map_cong"[no_vars]}
     4.1 --- a/src/HOL/BNF_FP_Base.thy	Sun May 04 16:17:53 2014 +0200
     4.2 +++ b/src/HOL/BNF_FP_Base.thy	Sun May 04 18:14:58 2014 +0200
     4.3 @@ -195,22 +195,22 @@
     4.4  lemma size_bool[code]: "size (b\<Colon>bool) = 0"
     4.5    by (cases b) auto
     4.6  
     4.7 -lemma nat_size[simp, code]: "size (n\<Colon>nat) = n"
     4.8 +lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
     4.9    by (induct n) simp_all
    4.10  
    4.11  declare prod.size[no_atp]
    4.12  
    4.13 -lemma sum_size_o_map: "sum_size g1 g2 \<circ> map_sum f1 f2 = sum_size (g1 \<circ> f1) (g2 \<circ> f2)"
    4.14 +lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
    4.15    by (rule ext) (case_tac x, auto)
    4.16  
    4.17 -lemma prod_size_o_map: "prod_size g1 g2 \<circ> map_prod f1 f2 = prod_size (g1 \<circ> f1) (g2 \<circ> f2)"
    4.18 +lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
    4.19    by (rule ext) auto
    4.20  
    4.21  setup {*
    4.22 -BNF_LFP_Size.register_size_global @{type_name sum} @{const_name sum_size} @{thms sum.size}
    4.23 -  @{thms sum_size_o_map}
    4.24 -#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name prod_size} @{thms prod.size}
    4.25 -  @{thms prod_size_o_map}
    4.26 +BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
    4.27 +  @{thms size_sum_o_map}
    4.28 +#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
    4.29 +  @{thms size_prod_o_map}
    4.30  *}
    4.31  
    4.32  end
     5.1 --- a/src/HOL/Code_Numeral.thy	Sun May 04 16:17:53 2014 +0200
     5.2 +++ b/src/HOL/Code_Numeral.thy	Sun May 04 18:14:58 2014 +0200
     5.3 @@ -810,10 +810,10 @@
     5.4    using assms by transfer blast
     5.5  
     5.6  lemma [simp, code]:
     5.7 -  "natural_size = nat_of_natural"
     5.8 +  "size_natural = nat_of_natural"
     5.9  proof (rule ext)
    5.10    fix n
    5.11 -  show "natural_size n = nat_of_natural n"
    5.12 +  show "size_natural n = nat_of_natural n"
    5.13      by (induct n) simp_all
    5.14  qed
    5.15  
     6.1 --- a/src/HOL/Fun_Def.thy	Sun May 04 16:17:53 2014 +0200
     6.2 +++ b/src/HOL/Fun_Def.thy	Sun May 04 18:14:58 2014 +0200
     6.3 @@ -168,8 +168,8 @@
     6.4    less_imp_le_nat[termination_simp]
     6.5    le_imp_less_Suc[termination_simp]
     6.6  
     6.7 -lemma prod_size_simp[termination_simp]:
     6.8 -  "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
     6.9 +lemma size_prod_simp[termination_simp]:
    6.10 +  "size_prod f g p = f (fst p) + g (snd p) + Suc 0"
    6.11  by (induct p) auto
    6.12  
    6.13  
     7.1 --- a/src/HOL/Lazy_Sequence.thy	Sun May 04 16:17:53 2014 +0200
     7.2 +++ b/src/HOL/Lazy_Sequence.thy	Sun May 04 18:14:58 2014 +0200
     7.3 @@ -27,13 +27,10 @@
     7.4    "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
     7.5    by (auto intro: lazy_sequence_eqI)
     7.6  
     7.7 -lemma lazy_sequence_size_eq:
     7.8 -  "lazy_sequence_size f xq = Suc (size_list f (list_of_lazy_sequence xq))"
     7.9 -  by (cases xq) simp
    7.10 -
    7.11  lemma size_lazy_sequence_eq [code]:
    7.12 +  "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
    7.13    "size (xq :: 'a lazy_sequence) = 0"
    7.14 -  by (cases xq) simp
    7.15 +  by (cases xq, simp)+
    7.16  
    7.17  lemma case_lazy_sequence [simp]:
    7.18    "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
    7.19 @@ -75,11 +72,11 @@
    7.20    case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
    7.21    by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
    7.22  
    7.23 -lemma lazy_sequence_size_code [code]:
    7.24 -  "lazy_sequence_size s xq = (case yield xq of
    7.25 +lemma size_lazy_sequence_code [code]:
    7.26 +  "size_lazy_sequence s xq = (case yield xq of
    7.27      None \<Rightarrow> 1
    7.28 -  | Some (x, xq') \<Rightarrow> Suc (s x + lazy_sequence_size s xq'))"
    7.29 -  by (cases "list_of_lazy_sequence xq") (simp_all add: lazy_sequence_size_eq)
    7.30 +  | Some (x, xq') \<Rightarrow> Suc (s x + size_lazy_sequence s xq'))"
    7.31 +  by (cases "list_of_lazy_sequence xq") (simp_all add: size_lazy_sequence_eq)
    7.32  
    7.33  lemma equal_lazy_sequence_code [code]:
    7.34    "HOL.equal xq yq = (case (yield xq, yield yq) of
     8.1 --- a/src/HOL/Library/IArray.thy	Sun May 04 16:17:53 2014 +0200
     8.2 +++ b/src/HOL/Library/IArray.thy	Sun May 04 18:14:58 2014 +0200
     8.3 @@ -59,7 +59,7 @@
     8.4  by (cases as) simp
     8.5  
     8.6  lemma [code]:
     8.7 -"iarray_size f as = Suc (size_list f (IArray.list_of as))"
     8.8 +"size_iarray f as = Suc (size_list f (IArray.list_of as))"
     8.9  by (cases as) simp
    8.10  
    8.11  lemma [code]:
     9.1 --- a/src/HOL/Library/refute.ML	Sun May 04 16:17:53 2014 +0200
     9.2 +++ b/src/HOL/Library/refute.ML	Sun May 04 18:14:58 2014 +0200
     9.3 @@ -2399,7 +2399,7 @@
     9.4                              end
     9.5                          end
     9.6                        val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index))
     9.7 -                      (* sanity check: the size of 'IDT' should be 'idt_size' *)
     9.8 +                      (* sanity check: the size of 'IDT' should be 'size_idt' *)
     9.9                        val _ =
    9.10                            if idt_size <> size_of_type ctxt (typs, []) IDT then
    9.11                              raise REFUTE ("IDT_recursion_interpreter",
    10.1 --- a/src/HOL/Predicate.thy	Sun May 04 16:17:53 2014 +0200
    10.2 +++ b/src/HOL/Predicate.thy	Sun May 04 18:14:58 2014 +0200
    10.3 @@ -498,7 +498,7 @@
    10.4    "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
    10.5  
    10.6  lemma [code]:
    10.7 -  "pred_size f P = 0" by (cases P) simp
    10.8 +  "size_pred f P = 0" by (cases P) simp
    10.9  
   10.10  primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
   10.11    "contained Empty Q \<longleftrightarrow> True"
    11.1 --- a/src/HOL/String.thy	Sun May 04 16:17:53 2014 +0200
    11.2 +++ b/src/HOL/String.thy	Sun May 04 18:14:58 2014 +0200
    11.3 @@ -20,10 +20,9 @@
    11.4  qed
    11.5  
    11.6  lemma size_nibble [code, simp]:
    11.7 -  "size (x::nibble) = 0" by (cases x) simp_all
    11.8 -
    11.9 -lemma nibble_size [code, simp]:
   11.10 -  "nibble_size (x::nibble) = 0" by (cases x) simp_all
   11.11 +  "size_nibble (x::nibble) = 0"
   11.12 +  "size (x::nibble) = 0"
   11.13 +  by (cases x, simp_all)+
   11.14  
   11.15  instantiation nibble :: enum
   11.16  begin
   11.17 @@ -136,10 +135,9 @@
   11.18  qed
   11.19  
   11.20  lemma size_char [code, simp]:
   11.21 -  "size (c::char) = 0" by (cases c) simp
   11.22 -
   11.23 -lemma char_size [code, simp]:
   11.24 -  "char_size (c::char) = 0" by (cases c) simp
   11.25 +  "size_char (c::char) = 0"
   11.26 +  "size (c::char) = 0"
   11.27 +  by (cases c, simp)+
   11.28  
   11.29  instantiation char :: enum
   11.30  begin
    12.1 --- a/src/HOL/Tools/Function/size.ML	Sun May 04 16:17:53 2014 +0200
    12.2 +++ b/src/HOL/Tools/Function/size.ML	Sun May 04 18:14:58 2014 +0200
    12.3 @@ -74,7 +74,7 @@
    12.4          val (((size_names, size_fns), def_names), def_names') =
    12.5            recTs1 |> map (fn T as Type (s, _) =>
    12.6              let
    12.7 -              val s' = Long_Name.base_name s ^ "_size";
    12.8 +              val s' = "size_" ^ Long_Name.base_name s;
    12.9                val s'' = Sign.full_bname thy s';
   12.10              in
   12.11                (s'',