--- 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
--- 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}.
--- 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]}
--- 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
--- 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
--- 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
--- 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
--- 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]:
--- 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",
--- 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"
--- 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
--- 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'',