Theory Computation_Checks

(*  Title:      HOL/Computational_Algebra/Computation_Checks.thy
    Author:     Florian Haftmann, TU Muenchen
*)

section ‹Computation checks›

theory Computation_Checks
imports Primes Polynomial_Factorial "HOL-Library.Discrete_Functions" "HOL-Library.Code_Target_Numeral"
begin

text ‹
  @{lemma ‹floor_sqrt 16476148165462159 = 128359449› by eval}
›

text ‹
  @{lemma ‹prime (97 :: nat)› by simp}
›

text ‹
  @{lemma ‹prime (97 :: int)› by simp}
›

text ‹
  @{lemma ‹prime (9973 :: nat)› by eval}
›

text ‹
  @{lemma ‹prime (9973 :: int)› by eval}
›

text ‹
  @{lemma ‹Gcd {[:1, 2, 3:], [:2, 3, (4 :: int):]} = 1› by eval}
›

text ‹
  @{lemma ‹Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]› by eval}
›

end