# HG changeset patch # User wenzelm # Date 1378240252 -7200 # Node ID e93772b451ef595c21e339e133b4a4a5aec161af # Parent 7a41ec2cc522ceda02fe9edd86171c28737c4c96# Parent 344587a4d5cdea32f346ffa498b475ad8d121b1e merged diff -r 7a41ec2cc522 -r e93772b451ef src/Doc/IsarRef/Proof.thy --- a/src/Doc/IsarRef/Proof.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/Doc/IsarRef/Proof.thy Tue Sep 03 22:30:52 2013 +0200 @@ -1195,7 +1195,7 @@ later. @{rail " - @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) +) ')') + @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')') ; caseref: nameref attributes? ; diff -r 7a41ec2cc522 -r e93772b451ef src/Doc/ROOT --- a/src/Doc/ROOT Tue Sep 03 22:12:48 2013 +0200 +++ b/src/Doc/ROOT Tue Sep 03 22:30:52 2013 +0200 @@ -284,6 +284,8 @@ session Tutorial (doc) in "Tutorial" = HOL + options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] + theories [threads = 1] + "ToyList/ToyList_Test" theories [thy_output_indent = 5] "ToyList/ToyList" "Ifexpr/Ifexpr" diff -r 7a41ec2cc522 -r e93772b451ef src/Doc/Tutorial/ToyList/ToyList.thy --- a/src/Doc/Tutorial/ToyList/ToyList.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/Doc/Tutorial/ToyList/ToyList.thy Tue Sep 03 22:30:52 2013 +0200 @@ -2,18 +2,6 @@ imports Datatype begin -(*<*) -ML {* (* FIXME somewhat non-standard, fragile *) - let - val texts = - map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode) - ["ToyList1", "ToyList2"]; - val trs = Outer_Syntax.parse Position.start (implode texts); - val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel; - in @{assert} (Toplevel.is_toplevel end_state) end; -*} -(*>*) - text{*\noindent HOL already has a predefined theory of lists called @{text List} --- @{text ToyList} is merely a small fragment of it chosen as an example. In diff -r 7a41ec2cc522 -r e93772b451ef src/Doc/Tutorial/ToyList/ToyList_Test.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy Tue Sep 03 22:30:52 2013 +0200 @@ -0,0 +1,16 @@ +theory ToyList_Test +imports Datatype +begin + +ML {* (* FIXME somewhat non-standard, fragile *) + let + val texts = + map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode) + ["ToyList1", "ToyList2"]; + val trs = Outer_Syntax.parse Position.start (implode texts); + val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel; + in @{assert} (Toplevel.is_toplevel end_state) end; +*} + +end + diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Tue Sep 03 22:30:52 2013 +0200 @@ -3637,11 +3637,11 @@ assume cunit:"c \ Units G" have "b \ inv c = a \ c \ inv c" by (simp add: b) - also with ccarr acarr cunit + also from ccarr acarr cunit have "\ = a \ (c \ inv c)" by (fast intro: m_assoc) - also with ccarr cunit + also from ccarr cunit have "\ = a \ \" by (simp add: Units_r_inv) - also with acarr + also from acarr have "\ = a" by simp finally have "a = b \ inv c" by simp with ccarr cunit diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Tue Sep 03 22:30:52 2013 +0200 @@ -423,9 +423,9 @@ case False hence "x = flat (stl s) !! (y - length (shd s))" by (metis less(2,3) flat_snth) moreover - { from less(2) have "length (shd s) > 0" by (cases s) simp_all - moreover with False have "y > 0" by (cases y) simp_all - ultimately have "y - length (shd s) < y" by simp + { from less(2) have *: "length (shd s) > 0" by (cases s) simp_all + with False have "y > 0" by (cases y) simp_all + with * have "y - length (shd s) < y" by simp } moreover have "\xs \ sset (stl s). xs \ []" using less(2) by (cases s) auto ultimately have "\n m'. x = stl s !! n ! m' \ m' < length (stl s !! n)" by (intro less(1)) auto diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Tue Sep 03 22:30:52 2013 +0200 @@ -898,11 +898,10 @@ proof (intro multiset_eqI, transfer fixing: f) fix x :: 'a and M1 M2 :: "'b \ nat" assume "M1 \ multiset" "M2 \ multiset" - moreover hence "setsum M1 {a. f a = x \ 0 < M1 a} = setsum M1 {a. f a = x \ 0 < M1 a + M2 a}" "setsum M2 {a. f a = x \ 0 < M2 a} = setsum M2 {a. f a = x \ 0 < M1 a + M2 a}" by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left) - ultimately show "(\a | f a = x \ 0 < M1 a + M2 a. M1 a + M2 a) = + then show "(\a | f a = x \ 0 < M1 a + M2 a. M1 a + M2 a) = setsum M1 {a. f a = x \ 0 < M1 a} + setsum M2 {a. f a = x \ 0 < M2 a}" by (auto simp: setsum.distrib[symmetric]) diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Big_Operators.thy Tue Sep 03 22:30:52 2013 +0200 @@ -46,7 +46,7 @@ proof - from `x \ A` obtain B where A: "A = insert x B" and "x \ B" by (auto dest: mk_disjoint_insert) - moreover from `finite A` this have "finite B" by simp + moreover from `finite A` A have "finite B" by simp ultimately show ?thesis by simp qed diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Complete_Lattices.thy Tue Sep 03 22:30:52 2013 +0200 @@ -250,7 +250,7 @@ shows "\A \ u" proof - from `A \ {}` obtain v where "v \ A" by blast - moreover with assms have "v \ u" by blast + moreover from `v \ A` assms(1) have "v \ u" by blast ultimately show ?thesis by (rule Inf_lower2) qed @@ -260,7 +260,7 @@ shows "u \ \A" proof - from `A \ {}` obtain v where "v \ A" by blast - moreover with assms have "u \ v" by blast + moreover from `v \ A` assms(1) have "u \ v" by blast ultimately show ?thesis by (rule Sup_upper2) qed diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Complex.thy --- a/src/HOL/Complex.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Complex.thy Tue Sep 03 22:30:52 2013 +0200 @@ -707,11 +707,11 @@ unfolding d_def by simp moreover from a assms have "cos a = cos x" and "sin a = sin x" by (simp_all add: complex_eq_iff) - hence "cos d = 1" unfolding d_def cos_diff by simp - moreover hence "sin d = 0" by (rule cos_one_sin_zero) + hence cos: "cos d = 1" unfolding d_def cos_diff by simp + moreover from cos have "sin d = 0" by (rule cos_one_sin_zero) ultimately have "d = 0" unfolding sin_zero_iff even_mult_two_ex - by (safe, auto simp add: numeral_2_eq_2 less_Suc_eq) + by (auto simp add: numeral_2_eq_2 less_Suc_eq) thus "a = x" unfolding d_def by simp qed (simp add: assms del: Re_sgn Im_sgn) with `z \ 0` show "arg z = x" diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Decision_Procs/Commutative_Ring_Complete.thy --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Tue Sep 03 22:30:52 2013 +0200 @@ -138,7 +138,6 @@ by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) moreover note 6 Y0 - moreover ultimately have ?case by (simp add: mkPinj_cn) } moreover { assume "x>y" hence "EX d. x = d + y" by arith @@ -286,7 +285,6 @@ from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False) moreover note 6 - moreover ultimately have ?case by (simp add: mkPinj_cn) } moreover { assume "x > y" hence "EX d. x = d + y" by arith diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 03 22:30:52 2013 +0200 @@ -2168,7 +2168,6 @@ by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - moreover {assume c: "?c = 0" and d: "?d>0" from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff) from d have d': "2*?d \ 0" by simp @@ -2314,7 +2313,6 @@ by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - moreover {assume c: "?c = 0" and d: "?d>0" from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff) from d have d': "2*?d \ 0" by simp diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Sep 03 22:30:52 2013 +0200 @@ -1314,7 +1314,7 @@ head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']] have ?case by simp} moreover - {moreover assume nz: "n = 0" + { assume nz: "n = 0" from polymul_degreen[OF norm(5,4), where m="0"] polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0 norm(5,6) degree_npolyhCN[OF norm(6)] diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Deriv.thy Tue Sep 03 22:30:52 2013 +0200 @@ -416,10 +416,10 @@ proof fix h show "F h = 0" proof (rule ccontr) - assume "F h \ 0" - moreover from this have h: "h \ 0" + assume **: "F h \ 0" + then have h: "h \ 0" by (clarsimp simp add: F.zero) - ultimately have "0 < ?r h" + with ** have "0 < ?r h" by (simp add: divide_pos_pos) from LIM_D [OF * this] obtain s where s: "0 < s" and r: "\x. x \ 0 \ norm x < s \ ?r x < ?r h" by auto @@ -528,11 +528,11 @@ lemma differentiable_def: "(f::real \ real) differentiable x in s \ (\D. DERIV f x : s :> D)" proof safe assume "f differentiable x in s" - then obtain f' where "FDERIV f x : s :> f'" + then obtain f' where *: "FDERIV f x : s :> f'" unfolding isDiff_def by auto - moreover then obtain c where "f' = (\x. x * c)" + then obtain c where "f' = (\x. x * c)" by (metis real_bounded_linear FDERIV_bounded_linear) - ultimately show "\D. DERIV f x : s :> D" + with * show "\D. DERIV f x : s :> D" unfolding deriv_fderiv by auto qed (auto simp: isDiff_def deriv_fderiv) @@ -730,8 +730,8 @@ DERIV f x :> u \ DERIV g y :> v" unfolding DERIV_iff2 proof (rule filterlim_cong) - assume "eventually (\x. f x = g x) (nhds x)" - moreover then have "f x = g x" by (auto simp: eventually_nhds) + assume *: "eventually (\x. f x = g x) (nhds x)" + moreover from * have "f x = g x" by (auto simp: eventually_nhds) moreover assume "x = y" "u = v" ultimately show "eventually (\xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)" by (auto simp: eventually_at_filter elim: eventually_elim1) @@ -1319,7 +1319,8 @@ and fd: "\x. a < x \ x < b \ f differentiable x" and gc: "\x. a \ x \ x \ b \ isCont g x" and gd: "\x. a < x \ x < b \ g differentiable x" - shows "\g'c f'c c. DERIV g c :> g'c \ DERIV f c :> f'c \ a < c \ c < b \ ((f b - f a) * g'c) = ((g b - g a) * f'c)" + shows "\g'c f'c c. + DERIV g c :> g'c \ DERIV f c :> f'c \ a < c \ c < b \ ((f b - f a) * g'c) = ((g b - g a) * f'c)" proof - let ?h = "\x. (f b - f a)*(g x) - (g b - g a)*(f x)" from assms have "a < b" by simp @@ -1348,7 +1349,7 @@ { from cdef have "?h b - ?h a = (b - a) * l" by auto - also with leq have "\ = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp + also from leq have "\ = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp } moreover @@ -1458,14 +1459,15 @@ using `isCont g 0` g by (auto intro: DERIV_isCont simp: le_less) ultimately have "\c. 0 < c \ c < x \ (f x - f 0) * g' c = (g x - g 0) * f' c" using f g `x < a` by (intro GMVT') auto - then guess c .. + then obtain c where *: "0 < c" "c < x" "(f x - f 0) * g' c = (g x - g 0) * f' c" + by blast moreover - with g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c" + from * g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c" by (simp add: field_simps) ultimately show "\y. 0 < y \ y < x \ f x / g x = f' y / g' y" using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c]) qed - then guess \ .. + then obtain \ where "\x\{0 <..< a}. 0 < \ x \ \ x < x \ f x / g x = f' (\ x) / g' (\ x)" .. then have \: "eventually (\x. 0 < \ x \ \ x < x \ f x / g x = f' (\ x) / g' (\ x)) (at_right 0)" unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def) moreover @@ -1581,9 +1583,10 @@ have "\y. t < y \ y < a \ (g a - g t) * f' y = (f a - f t) * g' y" using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+ - then guess y .. - from this - have [arith]: "t < y" "y < a" and D_eq: "(f t - f a) / (g t - g a) = f' y / g' y" + then obtain y where [arith]: "t < y" "y < a" + and D_eq0: "(g a - g t) * f' y = (f a - f t) * g' y" + by blast + from D_eq0 have D_eq: "(f t - f a) / (g t - g a) = f' y / g' y" using `g a < g t` g'_neq_0[of y] by (auto simp add: field_simps) have *: "f t / g t - x = ((f t - f a) / (g t - g a) - x) * (1 - g a / g t) + (f a - x * g a) / g t" diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Divides.thy Tue Sep 03 22:30:52 2013 +0200 @@ -742,11 +742,11 @@ apply (subst less_iff_Suc_add) apply (auto simp add: add_mult_distrib) done - from `n \ 0` assms have "fst qr = fst qr'" + from `n \ 0` assms have *: "fst qr = fst qr'" by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym) - moreover from this assms have "snd qr = snd qr'" + with assms have "snd qr = snd qr'" by (simp add: divmod_nat_rel_def) - ultimately show ?thesis by (cases qr, cases qr') simp + with * show ?thesis by (cases qr, cases qr') simp qed text {* diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Fields.thy --- a/src/HOL/Fields.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Fields.thy Tue Sep 03 22:30:52 2013 +0200 @@ -919,8 +919,8 @@ assume notless: "~ (0 < x)" have "~ (1 < inverse x)" proof - assume "1 < inverse x" - also with notless have "... \ 0" by simp + assume *: "1 < inverse x" + also from notless and * have "... \ 0" by simp also have "... < 1" by (rule zero_less_one) finally show False by auto qed diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Finite_Set.thy Tue Sep 03 22:30:52 2013 +0200 @@ -1103,7 +1103,7 @@ proof - from `x \ A` obtain B where A: "A = insert x B" and "x \ B" by (auto dest: mk_disjoint_insert) - moreover from `finite A` this have "finite B" by simp + moreover from `finite A` A have "finite B" by simp ultimately show ?thesis by simp qed diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Imperative_HOL/Legacy_Mrec.thy --- a/src/HOL/Imperative_HOL/Legacy_Mrec.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Imperative_HOL/Legacy_Mrec.thy Tue Sep 03 22:30:52 2013 +0200 @@ -118,7 +118,7 @@ proof (cases "mrec b h1") case (Some result) then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastforce - moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))" + moreover from mrec_rec have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))" apply (intro 1(2)) apply (auto simp add: Inr Inl') done diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Sep 03 22:30:52 2013 +0200 @@ -469,12 +469,12 @@ assume pivot: "l \ p \ p \ r" assume i_outer: "i < l \ r < i" from partition_outer_remains [OF part True] i_outer - have "Array.get h a !i = Array.get h1 a ! i" by fastforce + have 2: "Array.get h a !i = Array.get h1 a ! i" by fastforce moreover - with 1(1) [OF True pivot qs1] pivot i_outer - have "Array.get h1 a ! i = Array.get h2 a ! i" by auto + from 1(1) [OF True pivot qs1] pivot i_outer 2 + have 3: "Array.get h1 a ! i = Array.get h2 a ! i" by auto moreover - with qs2 1(2) [of p h2 h' ret2] True pivot i_outer + from qs2 1(2) [of p h2 h' ret2] True pivot i_outer 3 have "Array.get h2 a ! i = Array.get h' a ! i" by auto ultimately have "Array.get h a ! i= Array.get h' a ! i" by simp } @@ -604,9 +604,9 @@ shows "success (f \= g) h" using assms(1) proof (rule success_effectE) fix h' r - assume "effect f h h' r" - moreover with assms(2) have "success (g r) h'" . - ultimately show "success (f \= g) h" by (rule success_bind_effectI) + assume *: "effect f h h' r" + with assms(2) have "success (g r) h'" . + with * show "success (f \= g) h" by (rule success_bind_effectI) qed lemma success_partitionI: diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Imperative_HOL/ex/Sublist.thy --- a/src/HOL/Imperative_HOL/ex/Sublist.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Tue Sep 03 22:30:52 2013 +0200 @@ -490,7 +490,6 @@ moreover from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys" by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) - moreover ultimately show ?thesis by (simp add: multiset_of_append) qed diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Induct/Common_Patterns.thy --- a/src/HOL/Induct/Common_Patterns.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Induct/Common_Patterns.thy Tue Sep 03 22:30:52 2013 +0200 @@ -388,19 +388,18 @@ refl: "star r x x" | step: "r x y \ star r y z \ star r x z" -text{* Underscores are replaced by the default name hyps: *} +text {* Underscores are replaced by the default name hyps: *} -lemmas star_induct = star.induct[case_names base step[r _ IH]] +lemmas star_induct = star.induct [case_names base step[r _ IH]] lemma "star r x y \ star r y z \ star r x z" -proof(induct rule: star_induct) -print_cases - case base thus ?case . +proof (induct rule: star_induct) print_cases + case base + then show ?case . next - case (step a b c) - from step.prems have "star r b z" by(rule step.IH) - from step.r this show ?case by(rule star.step) + case (step a b c) print_facts + from step.prems have "star r b z" by (rule step.IH) + with step.r show ?case by (rule star.step) qed - end \ No newline at end of file diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Library/ContNotDenum.thy --- a/src/HOL/Library/ContNotDenum.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Library/ContNotDenum.thy Tue Sep 03 22:30:52 2013 +0200 @@ -323,64 +323,46 @@ lemma closed_subset_ex: fixes c::real - assumes alb: "a < b" - shows - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" -proof - - { - assume clb: "c < b" - { - assume cla: "c < a" - from alb cla clb have "c \ closed_int a b" by (unfold closed_int_def, auto) - with alb have - "a < b \ closed_int a b \ closed_int a b \ c \ closed_int a b" - by auto - hence - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" - by auto - } - moreover - { - assume ncla: "\(c < a)" - with clb have cdef: "a \ c \ c < b" by simp - obtain ka where kadef: "ka = (c + b)/2" by blast + assumes "a < b" + shows "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ closed_int ka kb" +proof (cases "c < b") + case True + show ?thesis + proof (cases "c < a") + case True + with `a < b` `c < b` have "c \ closed_int a b" + unfolding closed_int_def by auto + with `a < b` show ?thesis by auto + next + case False + then have "a \ c" by simp + def ka \ "(c + b)/2" - from kadef clb have kalb: "ka < b" by auto - moreover from kadef cdef have kagc: "ka > c" by simp - ultimately have "c\(closed_int ka b)" by (unfold closed_int_def, auto) - moreover from cdef kagc have "ka \ a" by simp - hence "closed_int ka b \ closed_int a b" by (unfold closed_int_def, auto) - ultimately have - "ka < b \ closed_int ka b \ closed_int a b \ c \ closed_int ka b" - using kalb by auto - hence - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" - by auto - - } + from ka_def `c < b` have kalb: "ka < b" by auto + moreover from ka_def `c < b` have kagc: "ka > c" by simp + ultimately have "c\(closed_int ka b)" by (unfold closed_int_def, auto) + moreover from `a \ c` kagc have "ka \ a" by simp + hence "closed_int ka b \ closed_int a b" by (unfold closed_int_def, auto) ultimately have - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" - by (rule case_split) - } - moreover - { - assume "\ (c < b)" - hence cgeb: "c \ b" by simp + "ka < b \ closed_int ka b \ closed_int a b \ c \ closed_int ka b" + using kalb by auto + then show ?thesis + by auto + qed +next + case False + then have "c \ b" by simp - obtain kb where kbdef: "kb = (a + b)/2" by blast - with alb have kblb: "kb < b" by auto - with kbdef cgeb have "a < kb \ kb < c" by auto - moreover hence "c \ (closed_int a kb)" by (unfold closed_int_def, auto) - moreover from kblb have - "closed_int a kb \ closed_int a b" by (unfold closed_int_def, auto) - ultimately have - "a < kb \ closed_int a kb \ closed_int a b \ c\closed_int a kb" - by simp - hence - "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" - by auto - } - ultimately show ?thesis by (rule case_split) + def kb \ "(a + b)/2" + with `a < b` have "kb < b" by auto + with kb_def `c \ b` have "a < kb" "kb < c" by auto + from `kb < c` have c: "c \ closed_int a kb" + unfolding closed_int_def by auto + with `kb < b` have "closed_int a kb \ closed_int a b" + unfolding closed_int_def by auto + with `a < kb` c have "a < kb \ closed_int a kb \ closed_int a b \ c \ closed_int a kb" + by simp + then show ?thesis by auto qed subsection {* newInt: Interval generation *} diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Library/Countable_Set.thy --- a/src/HOL/Library/Countable_Set.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Library/Countable_Set.thy Tue Sep 03 22:30:52 2013 +0200 @@ -55,7 +55,8 @@ assumes "countable S" "infinite S" obtains e :: "'a \ nat" where "bij_betw e S UNIV" proof - - from `countable S`[THEN countableE] guess f . + obtain f :: "'a \ nat" where "inj_on f S" + using `countable S` by (rule countableE) then have "bij_betw f S (f`S)" unfolding bij_betw_def by simp moreover @@ -169,9 +170,12 @@ "countable I \ (\i. i \ I \ countable (A i)) \ countable (SIGMA i : I. A i)" by (intro countableI'[of "\(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def) -lemma countable_image[intro, simp]: assumes A: "countable A" shows "countable (f`A)" +lemma countable_image[intro, simp]: + assumes "countable A" + shows "countable (f`A)" proof - - from A guess g by (rule countableE) + obtain g :: "'a \ nat" where "inj_on g A" + using assms by (rule countableE) moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \ A" by (auto intro: inj_on_inv_into inv_into_into) ultimately show ?thesis diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Library/Extended_Real.thy Tue Sep 03 22:30:52 2013 +0200 @@ -146,11 +146,11 @@ "-\ + -\ = -(\::ereal)" proof - case (goal1 P x) - moreover then obtain a b where "x = (a, b)" by (cases x) auto - ultimately show P + then obtain a b where "x = (a, b)" by (cases x) auto + with goal1 show P by (cases rule: ereal2_cases[of a b]) auto qed auto -termination proof qed (rule wf_empty) +termination by default (rule wf_empty) lemma Infty_neq_0[simp]: "(\::ereal) \ 0" "0 \ (\::ereal)" @@ -234,8 +234,8 @@ | " -\ < (\::ereal) \ True" proof - case (goal1 P x) - moreover then obtain a b where "x = (a,b)" by (cases x) auto - ultimately show P by (cases rule: ereal2_cases[of a b]) auto + then obtain a b where "x = (a,b)" by (cases x) auto + with goal1 show P by (cases rule: ereal2_cases[of a b]) auto qed simp_all termination by (relation "{}") simp @@ -496,8 +496,8 @@ "-(\::ereal) * -\ = \" proof - case (goal1 P x) - moreover then obtain a b where "x = (a, b)" by (cases x) auto - ultimately show P by (cases rule: ereal2_cases[of a b]) auto + then obtain a b where "x = (a, b)" by (cases x) auto + with goal1 show P by (cases rule: ereal2_cases[of a b]) auto qed simp_all termination by (relation "{}") simp @@ -1338,9 +1338,9 @@ next { assume "c = \" have ?thesis proof cases - assume "\i. f i = 0" - moreover then have "range f = {0}" by auto - ultimately show "c * SUPR UNIV f \ y" using * + assume **: "\i. f i = 0" + then have "range f = {0}" by auto + with ** show "c * SUPR UNIV f \ y" using * by (auto simp: SUP_def min_max.sup_absorb1) next assume "\ (\i. f i = 0)" @@ -1368,7 +1368,8 @@ next case (real r) with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)" by auto - moreover from assms[of n] guess i .. + moreover obtain i where "i \ A" "ereal (real n) \ f i" + using assms .. ultimately show ?thesis by (auto intro!: bexI[of _ i]) qed @@ -1383,11 +1384,12 @@ proof fix n ::nat have "\x\A. Sup A - 1 / ereal (real n) < x" using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def) - then guess x .. + then obtain x where "x \ A" "Sup A - 1 / ereal (real n) < x" .. then show "\x. x \ A \ Sup A < x + 1 / ereal (real n)" by (auto intro!: exI[of _ x] simp: ereal_minus_less_iff) qed - from choice[OF this] guess f .. note f = this + from choice[OF this] obtain f :: "nat \ ereal" + where f: "\x. f x \ A \ Sup A < f x + 1 / ereal (real x)" .. have "SUPR UNIV f = Sup A" proof (rule SUP_eqI) fix i show "f i \ Sup A" using f @@ -1417,9 +1419,9 @@ from `A \ {}` obtain x where "x \ A" by auto show ?thesis proof cases - assume "\ \ A" - moreover then have "\ \ Sup A" by (intro complete_lattice_class.Sup_upper) - ultimately show ?thesis by (auto intro!: exI[of _ "\x. \"]) + assume *: "\ \ A" + then have "\ \ Sup A" by (intro complete_lattice_class.Sup_upper) + with * show ?thesis by (auto intro!: exI[of _ "\x. \"]) next assume "\ \ A" have "\x\A. 0 \ x" @@ -1433,10 +1435,12 @@ then show False using `x \ A` `\ \ A` PInf by(cases x) auto qed - from choice[OF this] guess f .. note f = this + from choice[OF this] obtain f :: "nat \ ereal" + where f: "\z. f z \ A \ x + ereal (real z) \ f z" .. have "SUPR UNIV f = \" proof (rule SUP_PInfty) - fix n :: nat show "\i\UNIV. ereal (real n) \ f i" + fix n :: nat + show "\i\UNIV. ereal (real n) \ f i" using f[THEN spec, of n] `0 \ x` by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n]) qed @@ -1489,10 +1493,13 @@ fixes A :: "ereal set" assumes "A \ {}" and "\a\ \ \" shows "Inf ((\x. a - x) ` A) = a - Sup A" proof - - { fix x have "-a - -x = -(a - x)" using assms by (cases x) auto } - moreover then have "(\x. -a - x)`uminus`A = uminus ` (\x. a - x) ` A" + { + fix x + have "-a - -x = -(a - x)" using assms by (cases x) auto + } note * = this + then have "(\x. -a - x)`uminus`A = uminus ` (\x. a - x) ` A" by (auto simp: image_image) - ultimately show ?thesis + with * show ?thesis using Sup_ereal_cminus[of "uminus ` A" "-a"] assms by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq) qed @@ -1606,9 +1613,9 @@ unfolding open_ereal_generated proof (induct rule: generate_topology.induct) case (Int A B) - moreover then obtain x z where "\ \ A \ {ereal x <..} \ A" "\ \ B \ {ereal z <..} \ B" - by auto - ultimately show ?case + then obtain x z where "\ \ A \ {ereal x <..} \ A" "\ \ B \ {ereal z <..} \ B" + by auto + with Int show ?case by (intro exI[of _ "max x z"]) fastforce next { fix x have "x \ \ \ \t. x \ ereal t" by (cases x) auto } @@ -1621,9 +1628,9 @@ unfolding open_ereal_generated proof (induct rule: generate_topology.induct) case (Int A B) - moreover then obtain x z where "-\ \ A \ {..< ereal x} \ A" "-\ \ B \ {..< ereal z} \ B" - by auto - ultimately show ?case + then obtain x z where "-\ \ A \ {..< ereal x} \ A" "-\ \ B \ {..< ereal z} \ B" + by auto + with Int show ?case by (intro exI[of _ "min x z"]) fastforce next { fix x have "x \ - \ \ \t. ereal t \ x" by (cases x) auto } @@ -1711,8 +1718,9 @@ fixes S :: "ereal set" assumes "open S" "x \ S" and x: "\x\ \ \" obtains a b where "a < x" "x < b" "{a <..< b} \ S" -proof- - guess e using ereal_open_cont_interval[OF assms] . +proof - + obtain e where "0 < e" "{x - e<.. S" + using assms by (rule ereal_open_cont_interval) with that[of "x-e" "x+e"] ereal_between[OF x, of e] show thesis by auto qed @@ -1759,8 +1767,9 @@ lemma tendsto_MInfty: "(f ---> -\) F \ (\r. eventually (\x. f x < ereal r) F)" unfolding tendsto_def proof safe - fix S :: "ereal set" assume "open S" "-\ \ S" - from open_MInfty[OF this] guess B .. note B = this + fix S :: "ereal set" + assume "open S" "-\ \ S" + from open_MInfty[OF this] obtain B where "{.. S" .. moreover assume "\r::real. eventually (\z. f z < r) F" then have "eventually (\z. f z \ {..< B}) F" by auto @@ -1775,7 +1784,7 @@ unfolding tendsto_PInfty eventually_sequentially proof safe fix r assume "\r. \N. \n\N. ereal r \ f n" - from this[rule_format, of "r+1"] guess N .. + then obtain N where "\n\N. ereal (r + 1) \ f n" by blast moreover have "ereal r < ereal (r + 1)" by auto ultimately show "\N. \n\N. ereal r < f n" by (blast intro: less_le_trans) @@ -1785,7 +1794,7 @@ unfolding tendsto_MInfty eventually_sequentially proof safe fix r assume "\r. \N. \n\N. f n \ ereal r" - from this[rule_format, of "r - 1"] guess N .. + then obtain N where "\n\N. f n \ ereal (r - 1)" by blast moreover have "ereal (r - 1) < ereal r" by auto ultimately show "\N. \n\N. f n < ereal r" by (blast intro: le_less_trans) diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Library/FinFun.thy --- a/src/HOL/Library/FinFun.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Library/FinFun.thy Tue Sep 03 22:30:52 2013 +0200 @@ -960,7 +960,7 @@ { fix g' a b show "Abs_finfun (g \ op $ g'(a $:= b)) = (Abs_finfun (g \ op $ g'))(a $:= g b)" proof - obtain y where y: "y \ finfun" and g': "g' = Abs_finfun y" by(cases g') - moreover hence "(g \ op $ g') \ finfun" by(simp add: finfun_left_compose) + moreover from g' have "(g \ op $ g') \ finfun" by(simp add: finfun_left_compose) moreover have "g \ y(a := b) = (g \ y)(a := g b)" by(auto) ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def) qed } diff -r 7a41ec2cc522 -r e93772b451ef src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Tue Sep 03 22:12:48 2013 +0200 +++ b/src/HOL/Library/Float.thy Tue Sep 03 22:30:52 2013 +0200 @@ -44,7 +44,7 @@ lemma zero_float[simp]: "0 \ float" by (auto simp: float_def) lemma one_float[simp]: "1 \ float" by (intro floatI[of 1 0]) simp -lemma numeral_float[simp]: "numeral i \ float" by (intro floatI[of "numeral i" 0]) simp +lemma numeral_float[simp]: "numeral i \ float" by (intro floatI[of "numeral i" 0]) simp lemma neg_numeral_float[simp]: "neg_numeral i \ float" by (intro floatI[of "neg_numeral i" 0]) simp lemma real_of_int_float[simp]: "real (x :: int) \ float" by (intro floatI[of x 0]) simp lemma real_of_nat_float[simp]: "real (x :: nat) \ float" by (intro floatI[of x 0]) simp @@ -175,7 +175,7 @@ lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n" by (induct n) simp_all -lemma fixes x y::float +lemma fixes x y::float shows real_of_float_min: "real (min x y) = min (real x) (real y)" and real_of_float_max: "real (max x y) = max (real x) (real y)" by (simp_all add: min_def max_def) @@ -197,7 +197,7 @@ then show "\c. a < c \ c < b" apply (intro exI[of _ "(a + b) * Float 1 -1"]) apply transfer - apply (simp add: powr_neg_numeral) + apply (simp add: powr_neg_numeral) done qed @@ -222,14 +222,14 @@ plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float) done -lemma transfer_numeral [transfer_rule]: +lemma transfer_numeral [transfer_rule]: "fun_rel (op =) pcr_float (numeral :: _ \