section ‹‹Extra_Pretty_Code_Examples› -- Setup for nicer output of ‹value›› theory Extra_Pretty_Code_Examples imports "HOL-Examples.Sqrt" Real_Impl.Real_Impl "HOL-Library.Code_Target_Numeral" Jordan_Normal_Form.Matrix_Impl begin text ‹Some setup that makes the output of the ‹value› command more readable if matrices and complex numbers are involved. It is not recommended to import this theory in theories that get included in actual developments (because of the changes to the code generation setup). It is meant for inclusion in example theories only.› lemma two_sqrt_irrat[simp]: "2 ∈ sqrt_irrat" using sqrt_prime_irrational[OF two_is_prime_nat] unfolding Rats_def sqrt_irrat_def image_def apply auto proof - (* Sledgehammer proof *) fix p :: rat assume "p * p = 2" hence f1: "(Ratreal p)⇧^{2}= real 2" by (metis Ratreal_def of_nat_numeral of_rat_numeral_eq power2_eq_square real_times_code) have "∀r. if 0 ≤ r then sqrt (r⇧^{2}) = r else r + sqrt (r⇧^{2}) = 0" by simp hence f2: "Ratreal p + sqrt ((Ratreal p)⇧^{2}) = 0" using f1 by (metis Ratreal_def Rats_def ‹sqrt (real 2) ∉ ℚ› range_eqI) have f3: "sqrt (real 2) + - 1 * sqrt ((Ratreal p)⇧^{2}) ≤ 0" using f1 by fastforce have f4: "0 ≤ sqrt (real 2) + - 1 * sqrt ((Ratreal p)⇧^{2})" using f1 by force have f5: "(- 1 * sqrt (real 2) = real_of_rat p) = (sqrt (real 2) + real_of_rat p = 0)" by linarith have "∀x0. - (x0::real) = - 1 * x0" by auto hence "sqrt (real 2) + real_of_rat p ≠ 0" using f5 by (metis (no_types) Rats_def Rats_minus_iff ‹sqrt (real 2) ∉ ℚ› range_eqI) thus False using f4 f3 f2 by simp qed (* Ensure that complex numbers with zero-imaginary part are rendered as reals *) lemma complex_number_code_post[code_post]: shows "Complex a 0 = complex_of_real a" and "complex_of_real 0 = 0" and "complex_of_real 1 = 1" and "complex_of_real (a/b) = complex_of_real a / complex_of_real b" and "complex_of_real (numeral n) = numeral n" and "complex_of_real (-r) = - complex_of_real r" using complex_eq_cancel_iff2 by auto (* Make real number implementation more readable *) lemma real_number_code_post[code_post]: shows "real_of (Abs_mini_alg (p, 0, b)) = real_of_rat p" and "real_of (Abs_mini_alg (p, q, 2)) = real_of_rat p + real_of_rat q * sqrt 2" and "sqrt 0 = 0" and "sqrt (real 0) = 0" and "x * (0::real) = 0" and "(0::real) * x = 0" and "(0::real) + x = x" and "x + (0::real) = x" and "(1::real) * x = x" and "x * (1::real) = x" by (auto simp add: eq_onp_same_args real_of.abs_eq) (* Hide IArray in output *) translations "x" ↽ "CONST IArray x" end