--- a/src/HOL/Finite_Set.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Finite_Set.thy Sun Sep 13 22:56:52 2015 +0200
@@ -573,7 +573,7 @@
end
instance prod :: (finite, finite) finite
- by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
+ by standard (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
lemma inj_graph: "inj (%f. {(x, y). y = f x})"
by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
@@ -593,16 +593,16 @@
qed
instance bool :: finite
- by default (simp add: UNIV_bool)
+ by standard (simp add: UNIV_bool)
instance set :: (finite) finite
- by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
+ by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
instance unit :: finite
- by default (simp add: UNIV_unit)
+ by standard (simp add: UNIV_unit)
instance sum :: (finite, finite) finite
- by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
+ by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
subsection \<open>A basic fold functional for finite sets\<close>
@@ -967,7 +967,7 @@
"comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')"
proof -
interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
- show ?thesis by default (auto simp: fun_eq_iff)
+ show ?thesis by standard (auto simp: fun_eq_iff)
qed
lemma Set_filter_fold:
@@ -988,7 +988,7 @@
shows "image f A = fold (\<lambda>k A. Set.insert (f k) A) {} A"
using assms
proof -
- interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" by default auto
+ interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" by standard auto
show ?thesis using assms by (induct A) auto
qed
@@ -997,7 +997,7 @@
shows "Ball A P = fold (\<lambda>k s. s \<and> P k) True A"
using assms
proof -
- interpret comp_fun_commute "\<lambda>k s. s \<and> P k" by default auto
+ interpret comp_fun_commute "\<lambda>k s. s \<and> P k" by standard auto
show ?thesis using assms by (induct A) auto
qed
@@ -1006,7 +1006,7 @@
shows "Bex A P = fold (\<lambda>k s. s \<or> P k) False A"
using assms
proof -
- interpret comp_fun_commute "\<lambda>k s. s \<or> P k" by default auto
+ interpret comp_fun_commute "\<lambda>k s. s \<or> P k" by standard auto
show ?thesis using assms by (induct A) auto
qed
@@ -1027,14 +1027,14 @@
assumes "finite B"
shows "(\<Union>y\<in>B. {(x, y)}) \<union> A = fold (\<lambda>y. Set.insert (x, y)) A B"
proof -
- interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" by default auto
+ interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" by standard auto
show ?thesis using assms by (induct B arbitrary: A) simp_all
qed
lemma comp_fun_commute_product_fold:
assumes "finite B"
shows "comp_fun_commute (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B)"
-by default (auto simp: fold_union_pair[symmetric] assms)
+ by standard (auto simp: fold_union_pair[symmetric] assms)
lemma product_fold:
assumes "finite A"
@@ -1122,18 +1122,16 @@
begin
interpretation fold?: comp_fun_commute f
- by default (insert comp_fun_commute, simp add: fun_eq_iff)
+ by standard (insert comp_fun_commute, simp add: fun_eq_iff)
definition F :: "'a set \<Rightarrow> 'b"
where
eq_fold: "F A = fold f z A"
-lemma empty [simp]:
- "F {} = z"
+lemma empty [simp]:"F {} = z"
by (simp add: eq_fold)
-lemma infinite [simp]:
- "\<not> finite A \<Longrightarrow> F A = z"
+lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F A = z"
by (simp add: eq_fold)
lemma insert [simp]:
@@ -1172,7 +1170,7 @@
declare insert [simp del]
interpretation fold?: comp_fun_idem f
- by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
+ by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
lemma insert_idem [simp]:
assumes "finite A"
@@ -1202,7 +1200,7 @@
where
"folding.F (\<lambda>_. Suc) 0 = card"
proof -
- show "folding (\<lambda>_. Suc)" by default rule
+ show "folding (\<lambda>_. Suc)" by standard rule
then interpret card!: folding "\<lambda>_. Suc" 0 .
from card_def show "folding.F (\<lambda>_. Suc) 0 = card" by rule
qed