author wenzelm Tue Mar 13 13:31:26 2012 +0100 (2012-03-13) changeset 46898 1570b30ee040 parent 46897 ec793befc232 child 46899 58110c1e02bc
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
1.1 --- a/src/HOL/Finite_Set.thy	Tue Mar 13 12:51:52 2012 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Tue Mar 13 13:31:26 2012 +0100
1.3 @@ -22,7 +22,8 @@
1.4    assumes "P {}"
1.5      and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
1.6    shows "P F"
1.7 -using `finite F` proof induct
1.8 +using `finite F`
1.9 +proof induct
1.10    show "P {}" by fact
1.11    fix x F assume F: "finite F" and P: "P F"
1.12    show "P (insert x F)"
1.13 @@ -68,7 +69,8 @@
1.14  lemma finite_imp_nat_seg_image_inj_on:
1.15    assumes "finite A"
1.16    shows "\<exists>(n::nat) f. A = f ` {i. i < n} \<and> inj_on f {i. i < n}"
1.17 -using assms proof induct
1.18 +using assms
1.19 +proof induct
1.20    case empty
1.21    show ?case
1.22    proof
1.23 @@ -248,7 +250,8 @@
1.24  lemma finite_imageD:
1.25    assumes "finite (f ` A)" and "inj_on f A"
1.26    shows "finite A"
1.27 -using assms proof (induct "f ` A" arbitrary: A)
1.28 +using assms
1.29 +proof (induct "f ` A" arbitrary: A)
1.30    case empty then show ?case by simp
1.31  next
1.32    case (insert x B)
1.33 @@ -272,7 +275,8 @@
1.34  lemma finite_subset_image:
1.35    assumes "finite B"
1.36    shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
1.37 -using assms proof induct
1.38 +using assms
1.39 +proof induct
1.40    case empty then show ?case by simp
1.41  next
1.42    case insert then show ?case
1.43 @@ -413,7 +417,8 @@
1.44    assumes "\<And>x. P {x}"
1.45      and "\<And>x F. finite F \<Longrightarrow> F \<noteq> {} \<Longrightarrow> x \<notin> F \<Longrightarrow> P F  \<Longrightarrow> P (insert x F)"
1.46    shows "P F"
1.47 -using assms proof induct
1.48 +using assms
1.49 +proof induct
1.50    case empty then show ?case by simp
1.51  next
1.52    case (insert x F) then show ?case by cases auto
1.53 @@ -424,7 +429,8 @@
1.54    assumes empty: "P {}"
1.55      and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)"
1.56    shows "P F"
1.57 -using `finite F` `F \<subseteq> A` proof induct
1.58 +using `finite F` `F \<subseteq> A`
1.59 +proof induct
1.60    show "P {}" by fact
1.61  next
1.62    fix x F
1.63 @@ -486,8 +492,8 @@
1.65  end
1.67 -instance prod :: (finite, finite) finite proof
1.68 -qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
1.69 +instance prod :: (finite, finite) finite
1.70 +  by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
1.72  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
1.73    by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
1.74 @@ -506,24 +512,24 @@
1.75    qed
1.76  qed
1.78 -instance bool :: finite proof
1.79 -qed (simp add: UNIV_bool)
1.80 +instance bool :: finite
1.81 +  by default (simp add: UNIV_bool)
1.83  instance set :: (finite) finite
1.84    by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
1.86 -instance unit :: finite proof
1.87 -qed (simp add: UNIV_unit)
1.88 +instance unit :: finite
1.89 +  by default (simp add: UNIV_unit)
1.91 -instance sum :: (finite, finite) finite proof
1.92 -qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
1.93 +instance sum :: (finite, finite) finite
1.94 +  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
1.96  lemma finite_option_UNIV [simp]:
1.97    "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
1.98    by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
1.100 -instance option :: (finite) finite proof
1.101 -qed (simp add: UNIV_option_conv)
1.102 +instance option :: (finite) finite
1.103 +  by default (simp add: UNIV_option_conv)
1.106  subsection {* A basic fold functional for finite sets *}
1.107 @@ -830,9 +836,9 @@
1.108    assumes "finite A" and "a \<notin> A"
1.109    shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
1.110  proof -
1.111 -  interpret comp_fun_commute "%x y. (g x) * y" proof
1.112 -  qed (simp add: fun_eq_iff mult_ac)
1.113 -  show ?thesis using assms by (simp add: fold_image_def)
1.114 +  interpret comp_fun_commute "%x y. (g x) * y"
1.115 +    by default (simp add: fun_eq_iff mult_ac)
1.116 +  from assms show ?thesis by (simp add: fold_image_def)
1.117  qed
1.119  lemma fold_image_reindex:
1.120 @@ -1018,8 +1024,8 @@
1.121  context ab_semigroup_mult
1.122  begin
1.124 -lemma comp_fun_commute: "comp_fun_commute (op *)" proof
1.125 -qed (simp add: fun_eq_iff mult_ac)
1.126 +lemma comp_fun_commute: "comp_fun_commute (op *)"
1.127 +  by default (simp add: fun_eq_iff mult_ac)
1.129  lemma fold_graph_insert_swap:
1.130  assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
1.131 @@ -1104,8 +1110,8 @@
1.132  context ab_semigroup_idem_mult
1.133  begin
1.135 -lemma comp_fun_idem: "comp_fun_idem (op *)" proof
1.136 -qed (simp_all add: fun_eq_iff mult_left_commute)
1.137 +lemma comp_fun_idem: "comp_fun_idem (op *)"
1.138 +  by default (simp_all add: fun_eq_iff mult_left_commute)
1.140  lemma fold1_insert_idem [simp]:
1.141    assumes nonempty: "A \<noteq> {}" and A: "finite A"
1.142 @@ -1137,7 +1143,8 @@
1.143  lemma hom_fold1_commute:
1.144  assumes hom: "!!x y. h (x * y) = h x * h y"
1.145  and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
1.146 -using N proof (induct rule: finite_ne_induct)
1.147 +using N
1.148 +proof (induct rule: finite_ne_induct)
1.149    case singleton thus ?case by simp
1.150  next
1.151    case (insert n N)
1.152 @@ -1293,8 +1300,8 @@
1.153    assumes "finite A" and "x \<notin> A"
1.154    shows "F (insert x A) = F A \<circ> f x"
1.155  proof -
1.156 -  interpret comp_fun_commute f proof
1.157 -  qed (insert comp_fun_commute, simp add: fun_eq_iff)
1.158 +  interpret comp_fun_commute f
1.159 +    by default (insert comp_fun_commute, simp add: fun_eq_iff)
1.160    from fold_insert2 assms
1.161    have "\<And>s. fold f s (insert x A) = fold f (f x s) A" .
1.162    with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
1.163 @@ -1426,9 +1433,9 @@
1.164    assumes "finite A" and "x \<notin> A"
1.165    shows "F (insert x A) = g x * F A"
1.166  proof -
1.167 -  interpret comp_fun_commute "%x y. (g x) * y" proof
1.168 -  qed (simp add: ac_simps fun_eq_iff)
1.169 -  with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
1.170 +  interpret comp_fun_commute "%x y. (g x) * y"
1.171 +    by default (simp add: ac_simps fun_eq_iff)
1.172 +  from assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
1.173      by (simp add: fold_image_def)
1.174    with `finite A` show ?thesis by (simp add: eq_fold_g)
1.175  qed
1.176 @@ -1650,8 +1657,8 @@
1.177    assumes "finite A" and "x \<notin> A"
1.178    shows "F (insert x A) = fold (op *) x A"
1.179  proof -
1.180 -  interpret ab_semigroup_mult "op *" proof qed (simp_all add: ac_simps)
1.181 -  with assms show ?thesis by (simp add: eq_fold fold1_eq_fold)
1.182 +  interpret ab_semigroup_mult "op *" by default (simp_all add: ac_simps)
1.183 +  from assms show ?thesis by (simp add: eq_fold fold1_eq_fold)
1.184  qed
1.186  lemma insert [simp]:
1.187 @@ -1756,8 +1763,8 @@
1.188    assumes "finite A"
1.189    shows "F (insert a A) = fold (op *) a A"
1.190  proof -
1.191 -  interpret ab_semigroup_idem_mult "op *" proof qed (simp_all add: ac_simps)
1.192 -  with assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem)
1.193 +  interpret ab_semigroup_idem_mult "op *" by default (simp_all add: ac_simps)
1.194 +  from assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem)
1.195  qed
1.197  lemma insert_idem [simp]:
2.1 --- a/src/HOL/List.thy	Tue Mar 13 12:51:52 2012 +0100
2.2 +++ b/src/HOL/List.thy	Tue Mar 13 13:31:26 2012 +0100
2.3 @@ -4483,7 +4483,8 @@
2.4    shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
2.5  proof -
2.6    interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
2.7 -  with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
2.8 +  from assms show ?thesis
2.9 +    by (simp add: sorted_list_of_set_def fold_insert_remove)
2.10  qed
2.12  lemma sorted_list_of_set [simp]:
3.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Mar 13 12:51:52 2012 +0100
3.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Mar 13 13:31:26 2012 +0100
3.3 @@ -1689,7 +1689,7 @@
3.4  proof
3.5    assume ?l guess f' using `?l`[unfolded differentiable_def] .. note f' = this
3.6    then interpret bounded_linear f' by auto
3.7 -  thus ?r unfolding vector_derivative_def has_vector_derivative_def
3.8 +  show ?r unfolding vector_derivative_def has_vector_derivative_def
3.9      apply-apply(rule someI_ex,rule_tac x="f' 1" in exI)
3.10      using f' unfolding scaleR[THEN sym] by auto
3.11  next
4.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Mar 13 12:51:52 2012 +0100
4.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Mar 13 13:31:26 2012 +0100
4.3 @@ -197,7 +197,7 @@
4.4  next
4.5    fix A assume "A \<in> sets (M2 \<Otimes>\<^isub>M M1)"
4.6    interpret Q: pair_sigma_algebra M2 M1 by default
4.7 -  with Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets (M2 \<Otimes>\<^isub>M M1)`]
4.8 +  from Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets (M2 \<Otimes>\<^isub>M M1)`]
4.9    show "?f -` A \<inter> space ?P \<in> sets ?P" by simp
4.10  qed
4.12 @@ -221,7 +221,7 @@
4.13    assumes Q: "Q \<in> sets P" shows "(\<lambda>x. (x, y)) -` Q \<in> sets M1" (is "?cut Q \<in> sets M1")
4.14  proof -
4.15    interpret Q: pair_sigma_algebra M2 M1 by default
4.16 -  with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]
4.17 +  from Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]
4.18    show ?thesis by (simp add: vimage_compose[symmetric] comp_def)
4.19  qed
5.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 12:51:52 2012 +0100
5.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 13:31:26 2012 +0100
5.3 @@ -858,7 +858,7 @@
5.4  using assms proof induct
5.5    case empty
5.6    interpret finite_product_sigma_finite M "{}" by default auto
5.7 -  then show ?case by simp
5.8 +  show ?case by simp
5.9  next
5.10    case (insert i I)
5.11    note `finite I`[intro, simp]
6.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 12:51:52 2012 +0100
6.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 13:31:26 2012 +0100
6.3 @@ -502,7 +502,7 @@
6.4      fix A assume "A \<in> sets ?G"
6.5      with generatorE guess J X . note JX = this
6.6      interpret JK: finite_product_prob_space M J by default fact+
6.7 -    with JX show "\<mu>G A \<noteq> \<infinity>" by simp
6.8 +    from JX show "\<mu>G A \<noteq> \<infinity>" by simp
6.9    next
6.10      fix A assume A: "range A \<subseteq> sets ?G" "decseq A" "(\<Inter>i. A i) = {}"
6.11      then have "decseq (\<lambda>i. \<mu>G (A i))"
7.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 12:51:52 2012 +0100
7.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 13:31:26 2012 +0100
7.3 @@ -622,7 +622,7 @@
7.4    assumes "finite_random_variable M' X" shows "random_variable M' X"
7.5  proof -
7.6    interpret M': finite_sigma_algebra M' using assms by simp
7.7 -  then show "random_variable M' X" using assms by simp default
7.8 +  show "random_variable M' X" using assms by simp default
7.9  qed
7.11  lemma (in prob_space) distribution_finite_prob_space: