Theory Extra_Pretty_Code_Examples

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