# HG changeset patch # User wenzelm # Date 1622888997 -7200 # Node ID ce9529a616fd67077856db6456969b06e31933e7 # Parent da3405e5cd580a38bfad6d8a50b58647ca5319be misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a); diff -r da3405e5cd58 -r ce9529a616fd src/HOL/ex/Sqrt.thy --- a/src/HOL/ex/Sqrt.thy Fri Jun 04 23:55:35 2021 +0200 +++ b/src/HOL/ex/Sqrt.thy Sat Jun 05 12:29:57 2021 +0200 @@ -83,21 +83,16 @@ qed -text \Another old chestnut, which is a consequence of the irrationality of 2.\ +text \Another old chestnut, which is a consequence of the irrationality of \<^term>\sqrt 2\.\ lemma "\a b::real. a \ \ \ b \ \ \ a powr b \ \" (is "\a b. ?P a b") -proof cases - assume "sqrt 2 powr sqrt 2 \ \" - then have "?P (sqrt 2) (sqrt 2)" - by (metis sqrt_2_not_rat) +proof (cases "sqrt 2 powr sqrt 2 \ \") + case True + with sqrt_2_not_rat have "?P (sqrt 2) (sqrt 2)" by simp then show ?thesis by blast next - assume 1: "sqrt 2 powr sqrt 2 \ \" - have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2" - using powr_realpow [of _ 2] - by (simp add: powr_powr power2_eq_square [symmetric]) - then have "?P (sqrt 2 powr sqrt 2) (sqrt 2)" - by (metis 1 Rats_number_of sqrt_2_not_rat) + case False + with sqrt_2_not_rat powr_powr have "?P (sqrt 2 powr sqrt 2) (sqrt 2)" by simp then show ?thesis by blast qed