# HG changeset patch # User wenzelm # Date 1331641886 -3600 # Node ID 1570b30ee040d2ccd55ca22185642297917a018c # Parent ec793befc232c68f63427ac3059cac7ce3b6bfba tuned proofs -- eliminated pointless chaining of facts after 'interpret'; diff -r ec793befc232 -r 1570b30ee040 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Mar 13 12:51:52 2012 +0100 +++ b/src/HOL/Finite_Set.thy Tue Mar 13 13:31:26 2012 +0100 @@ -22,7 +22,8 @@ assumes "P {}" and insert: "\x F. finite F \ x \ F \ P F \ P (insert x F)" shows "P F" -using `finite F` proof induct +using `finite F` +proof induct show "P {}" by fact fix x F assume F: "finite F" and P: "P F" show "P (insert x F)" @@ -68,7 +69,8 @@ lemma finite_imp_nat_seg_image_inj_on: assumes "finite A" shows "\(n::nat) f. A = f ` {i. i < n} \ inj_on f {i. i < n}" -using assms proof induct +using assms +proof induct case empty show ?case proof @@ -248,7 +250,8 @@ lemma finite_imageD: assumes "finite (f ` A)" and "inj_on f A" shows "finite A" -using assms proof (induct "f ` A" arbitrary: A) +using assms +proof (induct "f ` A" arbitrary: A) case empty then show ?case by simp next case (insert x B) @@ -272,7 +275,8 @@ lemma finite_subset_image: assumes "finite B" shows "B \ f ` A \ \C\A. finite C \ B = f ` C" -using assms proof induct +using assms +proof induct case empty then show ?case by simp next case insert then show ?case @@ -413,7 +417,8 @@ assumes "\x. P {x}" and "\x F. finite F \ F \ {} \ x \ F \ P F \ P (insert x F)" shows "P F" -using assms proof induct +using assms +proof induct case empty then show ?case by simp next case (insert x F) then show ?case by cases auto @@ -424,7 +429,8 @@ assumes empty: "P {}" and insert: "\a F. finite F \ a \ A \ a \ F \ P F \ P (insert a F)" shows "P F" -using `finite F` `F \ A` proof induct +using `finite F` `F \ A` +proof induct show "P {}" by fact next fix x F @@ -486,8 +492,8 @@ end -instance prod :: (finite, finite) finite proof -qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) +instance prod :: (finite, finite) finite + by default (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) @@ -506,24 +512,24 @@ qed qed -instance bool :: finite proof -qed (simp add: UNIV_bool) +instance bool :: finite + by default (simp add: UNIV_bool) instance set :: (finite) finite by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite) -instance unit :: finite proof -qed (simp add: UNIV_unit) +instance unit :: finite + by default (simp add: UNIV_unit) -instance sum :: (finite, finite) finite proof -qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) +instance sum :: (finite, finite) finite + by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) lemma finite_option_UNIV [simp]: "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)" by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some) -instance option :: (finite) finite proof -qed (simp add: UNIV_option_conv) +instance option :: (finite) finite + by default (simp add: UNIV_option_conv) subsection {* A basic fold functional for finite sets *} @@ -830,9 +836,9 @@ assumes "finite A" and "a \ A" shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)" proof - - interpret comp_fun_commute "%x y. (g x) * y" proof - qed (simp add: fun_eq_iff mult_ac) - show ?thesis using assms by (simp add: fold_image_def) + interpret comp_fun_commute "%x y. (g x) * y" + by default (simp add: fun_eq_iff mult_ac) + from assms show ?thesis by (simp add: fold_image_def) qed lemma fold_image_reindex: @@ -1018,8 +1024,8 @@ context ab_semigroup_mult begin -lemma comp_fun_commute: "comp_fun_commute (op *)" proof -qed (simp add: fun_eq_iff mult_ac) +lemma comp_fun_commute: "comp_fun_commute (op *)" + by default (simp add: fun_eq_iff mult_ac) lemma fold_graph_insert_swap: assumes fold: "fold_graph times (b::'a) A y" and "b \ A" @@ -1104,8 +1110,8 @@ context ab_semigroup_idem_mult begin -lemma comp_fun_idem: "comp_fun_idem (op *)" proof -qed (simp_all add: fun_eq_iff mult_left_commute) +lemma comp_fun_idem: "comp_fun_idem (op *)" + by default (simp_all add: fun_eq_iff mult_left_commute) lemma fold1_insert_idem [simp]: assumes nonempty: "A \ {}" and A: "finite A" @@ -1137,7 +1143,8 @@ lemma hom_fold1_commute: assumes hom: "!!x y. h (x * y) = h x * h y" and N: "finite N" "N \ {}" shows "h (fold1 times N) = fold1 times (h ` N)" -using N proof (induct rule: finite_ne_induct) +using N +proof (induct rule: finite_ne_induct) case singleton thus ?case by simp next case (insert n N) @@ -1293,8 +1300,8 @@ assumes "finite A" and "x \ A" shows "F (insert x A) = F A \ f x" proof - - interpret comp_fun_commute f proof - qed (insert comp_fun_commute, simp add: fun_eq_iff) + interpret comp_fun_commute f + by default (insert comp_fun_commute, simp add: fun_eq_iff) from fold_insert2 assms have "\s. fold f s (insert x A) = fold f (f x s) A" . with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff) @@ -1426,9 +1433,9 @@ assumes "finite A" and "x \ A" shows "F (insert x A) = g x * F A" proof - - interpret comp_fun_commute "%x y. (g x) * y" proof - qed (simp add: ac_simps fun_eq_iff) - with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A" + interpret comp_fun_commute "%x y. (g x) * y" + by default (simp add: ac_simps fun_eq_iff) + from assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A" by (simp add: fold_image_def) with `finite A` show ?thesis by (simp add: eq_fold_g) qed @@ -1650,8 +1657,8 @@ assumes "finite A" and "x \ A" shows "F (insert x A) = fold (op *) x A" proof - - interpret ab_semigroup_mult "op *" proof qed (simp_all add: ac_simps) - with assms show ?thesis by (simp add: eq_fold fold1_eq_fold) + interpret ab_semigroup_mult "op *" by default (simp_all add: ac_simps) + from assms show ?thesis by (simp add: eq_fold fold1_eq_fold) qed lemma insert [simp]: @@ -1756,8 +1763,8 @@ assumes "finite A" shows "F (insert a A) = fold (op *) a A" proof - - interpret ab_semigroup_idem_mult "op *" proof qed (simp_all add: ac_simps) - with assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem) + interpret ab_semigroup_idem_mult "op *" by default (simp_all add: ac_simps) + from assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem) qed lemma insert_idem [simp]: diff -r ec793befc232 -r 1570b30ee040 src/HOL/List.thy --- a/src/HOL/List.thy Tue Mar 13 12:51:52 2012 +0100 +++ b/src/HOL/List.thy Tue Mar 13 13:31:26 2012 +0100 @@ -4483,7 +4483,8 @@ shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))" proof - interpret comp_fun_commute insort by (fact comp_fun_commute_insort) - with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove) + from assms show ?thesis + by (simp add: sorted_list_of_set_def fold_insert_remove) qed lemma sorted_list_of_set [simp]: diff -r ec793befc232 -r 1570b30ee040 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Mar 13 12:51:52 2012 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Mar 13 13:31:26 2012 +0100 @@ -1689,7 +1689,7 @@ proof assume ?l guess f' using `?l`[unfolded differentiable_def] .. note f' = this then interpret bounded_linear f' by auto - thus ?r unfolding vector_derivative_def has_vector_derivative_def + show ?r unfolding vector_derivative_def has_vector_derivative_def apply-apply(rule someI_ex,rule_tac x="f' 1" in exI) using f' unfolding scaleR[THEN sym] by auto next diff -r ec793befc232 -r 1570b30ee040 src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Tue Mar 13 12:51:52 2012 +0100 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Mar 13 13:31:26 2012 +0100 @@ -197,7 +197,7 @@ next fix A assume "A \ sets (M2 \\<^isub>M M1)" interpret Q: pair_sigma_algebra M2 M1 by default - with Q.sets_pair_sigma_algebra_swap[OF `A \ sets (M2 \\<^isub>M M1)`] + from Q.sets_pair_sigma_algebra_swap[OF `A \ sets (M2 \\<^isub>M M1)`] show "?f -` A \ space ?P \ sets ?P" by simp qed @@ -221,7 +221,7 @@ assumes Q: "Q \ sets P" shows "(\x. (x, y)) -` Q \ sets M1" (is "?cut Q \ sets M1") proof - interpret Q: pair_sigma_algebra M2 M1 by default - with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y] + from Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y] show ?thesis by (simp add: vimage_compose[symmetric] comp_def) qed diff -r ec793befc232 -r 1570b30ee040 src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Tue Mar 13 12:51:52 2012 +0100 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Mar 13 13:31:26 2012 +0100 @@ -858,7 +858,7 @@ using assms proof induct case empty interpret finite_product_sigma_finite M "{}" by default auto - then show ?case by simp + show ?case by simp next case (insert i I) note `finite I`[intro, simp] diff -r ec793befc232 -r 1570b30ee040 src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Mar 13 12:51:52 2012 +0100 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Mar 13 13:31:26 2012 +0100 @@ -502,7 +502,7 @@ fix A assume "A \ sets ?G" with generatorE guess J X . note JX = this interpret JK: finite_product_prob_space M J by default fact+ - with JX show "\G A \ \" by simp + from JX show "\G A \ \" by simp next fix A assume A: "range A \ sets ?G" "decseq A" "(\i. A i) = {}" then have "decseq (\i. \G (A i))" diff -r ec793befc232 -r 1570b30ee040 src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Tue Mar 13 12:51:52 2012 +0100 +++ b/src/HOL/Probability/Probability_Measure.thy Tue Mar 13 13:31:26 2012 +0100 @@ -622,7 +622,7 @@ assumes "finite_random_variable M' X" shows "random_variable M' X" proof - interpret M': finite_sigma_algebra M' using assms by simp - then show "random_variable M' X" using assms by simp default + show "random_variable M' X" using assms by simp default qed lemma (in prob_space) distribution_finite_prob_space: