tuned proofs
authornoschinl
Mon Mar 12 21:41:11 2012 +0100 (2012-03-12)
changeset 46884154dc6ec0041
parent 46883 eec472dae593
child 46885 48c82ef7d468
tuned proofs
src/HOL/Complete_Lattices.thy
src/HOL/Lattices.thy
src/HOL/Library/Cset.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/List.thy
src/HOL/Orderings.thy
src/HOL/Predicate.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Mon Mar 12 15:12:22 2012 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Mon Mar 12 21:41:11 2012 +0100
     1.3 @@ -591,20 +591,20 @@
     1.4    by (simp add: Sup_fun_def)
     1.5  
     1.6  instance proof
     1.7 -qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_lower INF_greatest SUP_upper SUP_least)
     1.8 +qed (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)
     1.9  
    1.10  end
    1.11  
    1.12  lemma INF_apply [simp]:
    1.13    "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
    1.14 -  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
    1.15 +  by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def)
    1.16  
    1.17  lemma SUP_apply [simp]:
    1.18    "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
    1.19 -  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
    1.20 +  by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def)
    1.21  
    1.22  instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
    1.23 -qed (auto simp add: inf_apply sup_apply Inf_apply Sup_apply INF_def SUP_def inf_Sup sup_Inf image_image)
    1.24 +qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf image_image)
    1.25  
    1.26  instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
    1.27  
    1.28 @@ -612,46 +612,46 @@
    1.29  subsection {* Complete lattice on unary and binary predicates *}
    1.30  
    1.31  lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
    1.32 -  by (simp add: INF_apply)
    1.33 +  by simp
    1.34  
    1.35  lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
    1.36 -  by (simp add: INF_apply)
    1.37 +  by simp
    1.38  
    1.39  lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
    1.40 -  by (auto simp add: INF_apply)
    1.41 +  by auto
    1.42  
    1.43  lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
    1.44 -  by (auto simp add: INF_apply)
    1.45 +  by auto
    1.46  
    1.47  lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
    1.48 -  by (auto simp add: INF_apply)
    1.49 +  by auto
    1.50  
    1.51  lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
    1.52 -  by (auto simp add: INF_apply)
    1.53 +  by auto
    1.54  
    1.55  lemma INF1_E: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
    1.56 -  by (auto simp add: INF_apply)
    1.57 +  by auto
    1.58  
    1.59  lemma INF2_E: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
    1.60 -  by (auto simp add: INF_apply)
    1.61 +  by auto
    1.62  
    1.63  lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
    1.64 -  by (simp add: SUP_apply)
    1.65 +  by simp
    1.66  
    1.67  lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
    1.68 -  by (simp add: SUP_apply)
    1.69 +  by simp
    1.70  
    1.71  lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
    1.72 -  by (auto simp add: SUP_apply)
    1.73 +  by auto
    1.74  
    1.75  lemma SUP2_I: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
    1.76 -  by (auto simp add: SUP_apply)
    1.77 +  by auto
    1.78  
    1.79  lemma SUP1_E: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R"
    1.80 -  by (auto simp add: SUP_apply)
    1.81 +  by auto
    1.82  
    1.83  lemma SUP2_E: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R"
    1.84 -  by (auto simp add: SUP_apply)
    1.85 +  by auto
    1.86  
    1.87  
    1.88  subsection {* Complete lattice on @{typ "_ set"} *}
     2.1 --- a/src/HOL/Lattices.thy	Mon Mar 12 15:12:22 2012 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Mon Mar 12 21:41:11 2012 +0100
     2.3 @@ -662,12 +662,12 @@
     2.4    by (simp add: sup_fun_def)
     2.5  
     2.6  instance proof
     2.7 -qed (simp_all add: le_fun_def inf_apply sup_apply)
     2.8 +qed (simp_all add: le_fun_def)
     2.9  
    2.10  end
    2.11  
    2.12  instance "fun" :: (type, distrib_lattice) distrib_lattice proof
    2.13 -qed (rule ext, simp add: sup_inf_distrib1 inf_apply sup_apply)
    2.14 +qed (rule ext, simp add: sup_inf_distrib1)
    2.15  
    2.16  instance "fun" :: (type, bounded_lattice) bounded_lattice ..
    2.17  
    2.18 @@ -700,7 +700,7 @@
    2.19  end
    2.20  
    2.21  instance "fun" :: (type, boolean_algebra) boolean_algebra proof
    2.22 -qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+
    2.23 +qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
    2.24  
    2.25  
    2.26  subsection {* Lattice on unary and binary predicates *}
     3.1 --- a/src/HOL/Library/Cset.thy	Mon Mar 12 15:12:22 2012 +0100
     3.2 +++ b/src/HOL/Library/Cset.thy	Mon Mar 12 21:41:11 2012 +0100
     3.3 @@ -175,10 +175,10 @@
     3.4  subsection {* Simplified simprules *}
     3.5  
     3.6  lemma empty_simp [simp]: "member Cset.empty = bot"
     3.7 -  by (simp add: fun_eq_iff bot_apply)
     3.8 +  by (simp add: fun_eq_iff)
     3.9  
    3.10  lemma UNIV_simp [simp]: "member Cset.UNIV = top"
    3.11 -  by (simp add: fun_eq_iff top_apply)
    3.12 +  by (simp add: fun_eq_iff)
    3.13  
    3.14  lemma is_empty_simp [simp]:
    3.15    "is_empty A \<longleftrightarrow> set_of A = {}"
    3.16 @@ -222,7 +222,7 @@
    3.17  
    3.18  lemma member_SUP [simp]:
    3.19    "member (SUPR A f) = SUPR A (member \<circ> f)"
    3.20 -  by (auto simp add: fun_eq_iff SUP_apply member_def, unfold SUP_def, auto)
    3.21 +  by (auto simp add: fun_eq_iff member_def, unfold SUP_def, auto)
    3.22  
    3.23  lemma member_bind [simp]:
    3.24    "member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> f)"
    3.25 @@ -247,14 +247,14 @@
    3.26   
    3.27  lemma bind_single [simp]:
    3.28    "A \<guillemotright>= single = A"
    3.29 -  by (simp add: Cset.set_eq_iff SUP_apply fun_eq_iff single_def member_def)
    3.30 +  by (simp add: Cset.set_eq_iff fun_eq_iff single_def member_def)
    3.31  
    3.32  lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
    3.33    by (auto simp add: Cset.set_eq_iff fun_eq_iff)
    3.34  
    3.35  lemma empty_bind [simp]:
    3.36    "Cset.empty \<guillemotright>= f = Cset.empty"
    3.37 -  by (simp add: Cset.set_eq_iff fun_eq_iff bot_apply)
    3.38 +  by (simp add: Cset.set_eq_iff fun_eq_iff )
    3.39  
    3.40  lemma member_of_pred [simp]:
    3.41    "member (of_pred P) = (\<lambda>x. x \<in> {x. Predicate.eval P x})"
    3.42 @@ -360,7 +360,7 @@
    3.43       Predicate.Empty \<Rightarrow> Cset.empty
    3.44     | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
    3.45     | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
    3.46 -  by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric])
    3.47 +  by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff eval_member [symmetric] member_def [symmetric])
    3.48  
    3.49  lemma of_seq_code [code]:
    3.50    "of_seq Predicate.Empty = Cset.empty"
     4.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Mar 12 15:12:22 2012 +0100
     4.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Mar 12 21:41:11 2012 +0100
     4.3 @@ -41,7 +41,7 @@
     4.4  
     4.5  lemma Diff[code_pred_inline]:
     4.6    "(A - B) = (%x. A x \<and> \<not> B x)"
     4.7 -  by (simp add: fun_eq_iff minus_apply)
     4.8 +  by (simp add: fun_eq_iff)
     4.9  
    4.10  lemma subset_eq[code_pred_inline]:
    4.11    "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
    4.12 @@ -232,4 +232,4 @@
    4.13  lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
    4.14  unfolding less_nat[symmetric] by auto
    4.15  
    4.16 -end
    4.17 \ No newline at end of file
    4.18 +end
     5.1 --- a/src/HOL/List.thy	Mon Mar 12 15:12:22 2012 +0100
     5.2 +++ b/src/HOL/List.thy	Mon Mar 12 21:41:11 2012 +0100
     5.3 @@ -4533,7 +4533,7 @@
     5.4    "listsp A (x # xs)"
     5.5  
     5.6  lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
     5.7 -by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
     5.8 +by (rule predicate1I, erule listsp.induct, blast+)
     5.9  
    5.10  lemmas lists_mono = listsp_mono [to_set]
    5.11  
     6.1 --- a/src/HOL/Orderings.thy	Mon Mar 12 15:12:22 2012 +0100
     6.2 +++ b/src/HOL/Orderings.thy	Mon Mar 12 21:41:11 2012 +0100
     6.3 @@ -1304,7 +1304,7 @@
     6.4    by (simp add: bot_fun_def)
     6.5  
     6.6  instance proof
     6.7 -qed (simp add: le_fun_def bot_apply)
     6.8 +qed (simp add: le_fun_def)
     6.9  
    6.10  end
    6.11  
    6.12 @@ -1320,7 +1320,7 @@
    6.13    by (simp add: top_fun_def)
    6.14  
    6.15  instance proof
    6.16 -qed (simp add: le_fun_def top_apply)
    6.17 +qed (simp add: le_fun_def)
    6.18  
    6.19  end
    6.20  
     7.1 --- a/src/HOL/Predicate.thy	Mon Mar 12 15:12:22 2012 +0100
     7.2 +++ b/src/HOL/Predicate.thy	Mon Mar 12 21:41:11 2012 +0100
     7.3 @@ -123,7 +123,7 @@
     7.4    by (simp add: minus_pred_def)
     7.5  
     7.6  instance proof
     7.7 -qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply INF_apply SUP_apply)
     7.8 +qed (auto intro!: pred_eqI)
     7.9  
    7.10  end
    7.11  
    7.12 @@ -143,7 +143,7 @@
    7.13  
    7.14  lemma bind_bind:
    7.15    "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
    7.16 -  by (rule pred_eqI) (auto simp add: SUP_apply)
    7.17 +  by (rule pred_eqI) auto
    7.18  
    7.19  lemma bind_single:
    7.20    "P \<guillemotright>= single = P"
    7.21 @@ -163,7 +163,7 @@
    7.22  
    7.23  lemma Sup_bind:
    7.24    "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
    7.25 -  by (rule pred_eqI) (auto simp add: SUP_apply)
    7.26 +  by (rule pred_eqI) auto
    7.27  
    7.28  lemma pred_iffI:
    7.29    assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
     8.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon Mar 12 15:12:22 2012 +0100
     8.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon Mar 12 21:41:11 2012 +0100
     8.3 @@ -1417,7 +1417,7 @@
     8.4  proof
     8.5    fix a
     8.6    have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
     8.7 -    by (auto simp: less_SUP_iff SUP_apply)
     8.8 +    by (auto simp: less_SUP_iff)
     8.9    then show "?sup -` {a<..} \<inter> space M \<in> sets M"
    8.10      using assms by auto
    8.11  qed
    8.12 @@ -1430,7 +1430,7 @@
    8.13  proof
    8.14    fix a
    8.15    have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
    8.16 -    by (auto simp: INF_less_iff INF_apply)
    8.17 +    by (auto simp: INF_less_iff)
    8.18    then show "?inf -` {..<a} \<inter> space M \<in> sets M"
    8.19      using assms by auto
    8.20  qed
     9.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Mon Mar 12 15:12:22 2012 +0100
     9.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Mon Mar 12 21:41:11 2012 +0100
     9.3 @@ -1044,7 +1044,7 @@
     9.4          with `a < 1` u_range[OF `x \<in> space M`]
     9.5          have "a * u x < 1 * u x"
     9.6            by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
     9.7 -        also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def SUP_apply)
     9.8 +        also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)
     9.9          finally obtain i where "a * u x < f i x" unfolding SUP_def
    9.10            by (auto simp add: less_Sup_iff)
    9.11          hence "a * u x \<le> f i x" by auto
    9.12 @@ -1115,7 +1115,7 @@
    9.13        using f by (auto intro!: SUP_upper2)
    9.14      ultimately show "integral\<^isup>S M g \<le> (SUP j. integral\<^isup>P M (f j))"
    9.15        by (intro  positive_integral_SUP_approx[OF f g _ g'])
    9.16 -         (auto simp: le_fun_def max_def SUP_apply)
    9.17 +         (auto simp: le_fun_def max_def)
    9.18    qed
    9.19  qed
    9.20  
    10.1 --- a/src/HOL/Relation.thy	Mon Mar 12 15:12:22 2012 +0100
    10.2 +++ b/src/HOL/Relation.thy	Mon Mar 12 21:41:11 2012 +0100
    10.3 @@ -96,40 +96,40 @@
    10.4    by (simp add: sup_fun_def)
    10.5  
    10.6  lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
    10.7 -  by (simp add: fun_eq_iff Inf_apply)
    10.8 +  by (simp add: fun_eq_iff)
    10.9  
   10.10  lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
   10.11 -  by (simp add: fun_eq_iff INF_apply)
   10.12 +  by (simp add: fun_eq_iff)
   10.13  
   10.14  lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (prod_case ` S) Collect)"
   10.15 -  by (simp add: fun_eq_iff Inf_apply INF_apply)
   10.16 +  by (simp add: fun_eq_iff)
   10.17  
   10.18  lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)"
   10.19 -  by (simp add: fun_eq_iff INF_apply)
   10.20 +  by (simp add: fun_eq_iff)
   10.21  
   10.22  lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> UNION S Collect)"
   10.23 -  by (simp add: fun_eq_iff Sup_apply)
   10.24 +  by (simp add: fun_eq_iff)
   10.25  
   10.26  lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
   10.27 -  by (simp add: fun_eq_iff SUP_apply)
   10.28 +  by (simp add: fun_eq_iff)
   10.29  
   10.30  lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)"
   10.31 -  by (simp add: fun_eq_iff Sup_apply SUP_apply)
   10.32 +  by (simp add: fun_eq_iff)
   10.33  
   10.34  lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
   10.35 -  by (simp add: fun_eq_iff SUP_apply)
   10.36 +  by (simp add: fun_eq_iff)
   10.37  
   10.38  lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
   10.39 -  by (simp add: INF_apply fun_eq_iff)
   10.40 +  by (simp add: fun_eq_iff)
   10.41  
   10.42  lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))"
   10.43 -  by (simp add: INF_apply fun_eq_iff)
   10.44 +  by (simp add: fun_eq_iff)
   10.45  
   10.46  lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   10.47 -  by (simp add: SUP_apply fun_eq_iff)
   10.48 +  by (simp add: fun_eq_iff)
   10.49  
   10.50  lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
   10.51 -  by (simp add: SUP_apply fun_eq_iff)
   10.52 +  by (simp add: fun_eq_iff)
   10.53  
   10.54  
   10.55  
   10.56 @@ -818,7 +818,7 @@
   10.57    by blast
   10.58  
   10.59  lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r"
   10.60 -  by (auto simp add: Field_def Domain_insert Range_insert)
   10.61 +  by (auto simp add: Field_def)
   10.62  
   10.63  lemma Domain_iff: "a \<in> Domain r \<longleftrightarrow> (\<exists>y. (a, y) \<in> r)"
   10.64    by blast
   10.65 @@ -884,10 +884,10 @@
   10.66    by auto
   10.67  
   10.68  lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)"
   10.69 -  by (induct set: finite) (auto simp add: Domain_insert)
   10.70 +  by (induct set: finite) auto
   10.71  
   10.72  lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)"
   10.73 -  by (induct set: finite) (auto simp add: Range_insert)
   10.74 +  by (induct set: finite) auto
   10.75  
   10.76  lemma finite_Field: "finite r \<Longrightarrow> finite (Field r)"
   10.77    by (simp add: Field_def finite_Domain finite_Range)