--- a/src/HOL/Enum.thy Thu Jun 12 15:47:36 2014 +0200
+++ b/src/HOL/Enum.thy Thu Jun 12 18:47:16 2014 +0200
@@ -447,7 +447,7 @@
instance by default
- (simp_all add: enum_prod_def product_list_set distinct_product
+ (simp_all add: enum_prod_def distinct_product
enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
end
--- a/src/HOL/List.thy Thu Jun 12 15:47:36 2014 +0200
+++ b/src/HOL/List.thy Thu Jun 12 18:47:16 2014 +0200
@@ -2711,7 +2711,7 @@
subsubsection {* @{const List.product} and @{const product_lists} *}
-lemma product_list_set:
+lemma set_product[simp]:
"set (List.product xs ys) = set xs \<times> set ys"
by (induct xs) auto
@@ -3332,10 +3332,8 @@
qed (auto simp: dec_def)
lemma distinct_product:
- assumes "distinct xs" and "distinct ys"
- shows "distinct (List.product xs ys)"
- using assms by (induct xs)
- (auto intro: inj_onI simp add: product_list_set distinct_map)
+ "distinct xs \<Longrightarrow> distinct ys \<Longrightarrow> distinct (List.product xs ys)"
+by (induct xs) (auto intro: inj_onI simp add: distinct_map)
lemma distinct_product_lists:
assumes "\<forall>xs \<in> set xss. distinct xs"
--- a/src/HOL/String.thy Thu Jun 12 15:47:36 2014 +0200
+++ b/src/HOL/String.thy Thu Jun 12 18:47:16 2014 +0200
@@ -224,7 +224,7 @@
instance proof
show UNIV: "UNIV = set (Enum.enum :: char list)"
- by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
+ by (simp add: enum_char_product_enum_nibble UNIV_char enum_UNIV)
show "distinct (Enum.enum :: char list)"
by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"