added [simp]
authornipkow
Thu Jun 12 18:47:16 2014 +0200 (2014-06-12)
changeset 572478191ccf6a1bd
parent 57235 b0b9a10e4bf4
child 57248 5496011859eb
added [simp]
src/HOL/Enum.thy
src/HOL/List.thy
src/HOL/String.thy
     1.1 --- a/src/HOL/Enum.thy	Thu Jun 12 15:47:36 2014 +0200
     1.2 +++ b/src/HOL/Enum.thy	Thu Jun 12 18:47:16 2014 +0200
     1.3 @@ -447,7 +447,7 @@
     1.4  
     1.5   
     1.6  instance by default
     1.7 -  (simp_all add: enum_prod_def product_list_set distinct_product
     1.8 +  (simp_all add: enum_prod_def distinct_product
     1.9      enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
    1.10  
    1.11  end
     2.1 --- a/src/HOL/List.thy	Thu Jun 12 15:47:36 2014 +0200
     2.2 +++ b/src/HOL/List.thy	Thu Jun 12 18:47:16 2014 +0200
     2.3 @@ -2711,7 +2711,7 @@
     2.4  
     2.5  subsubsection {* @{const List.product} and @{const product_lists} *}
     2.6  
     2.7 -lemma product_list_set:
     2.8 +lemma set_product[simp]:
     2.9    "set (List.product xs ys) = set xs \<times> set ys"
    2.10    by (induct xs) auto
    2.11  
    2.12 @@ -3332,10 +3332,8 @@
    2.13  qed (auto simp: dec_def)
    2.14  
    2.15  lemma distinct_product:
    2.16 -  assumes "distinct xs" and "distinct ys"
    2.17 -  shows "distinct (List.product xs ys)"
    2.18 -  using assms by (induct xs)
    2.19 -    (auto intro: inj_onI simp add: product_list_set distinct_map)
    2.20 +  "distinct xs \<Longrightarrow> distinct ys \<Longrightarrow> distinct (List.product xs ys)"
    2.21 +by (induct xs) (auto intro: inj_onI simp add: distinct_map)
    2.22  
    2.23  lemma distinct_product_lists:
    2.24    assumes "\<forall>xs \<in> set xss. distinct xs"
     3.1 --- a/src/HOL/String.thy	Thu Jun 12 15:47:36 2014 +0200
     3.2 +++ b/src/HOL/String.thy	Thu Jun 12 18:47:16 2014 +0200
     3.3 @@ -224,7 +224,7 @@
     3.4  
     3.5  instance proof
     3.6    show UNIV: "UNIV = set (Enum.enum :: char list)"
     3.7 -    by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
     3.8 +    by (simp add: enum_char_product_enum_nibble UNIV_char enum_UNIV)
     3.9    show "distinct (Enum.enum :: char list)"
    3.10      by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
    3.11    show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"