chapter \<open>Exercise Sheet -- Week 12\<close>

theory Exercise12
  imports 
    Main
    "HOL-Computational_Algebra.Primes" 
    "HOL-Library.Code_Target_Numeral" 
(*    "Sqrt_Babylonian.Sqrt_Babylonian"  *)
begin

section \<open>Exercise 1 -- 5 points\<close>

definition "prime_nat = (prime :: nat \<Rightarrow> bool)" 

value (code) "prime_nat 100000007" 
(* takes too long: 
value (code) "prime_nat 10000000019" 
*)

text \<open>Let us define a faster primality test for some number \<open>n\<close>, where instead 
  of testing all divisors in @{term "{2 ..< n}"} only the divisors to the square-root
  of \<open>n\<close> should be tested.

  Luckily the archive of formal proofs (AFP) contains 
  an executable square-root-algorithm for integers and natural numbers in 
  @{theory Sqrt_Babylonian.Sqrt_Babylonian},
  that computes the floor of the square-root of a given number, cf.
  \<^url>\<open>https://www.isa-afp.org/entries/Sqrt_Babylonian.html\<close>\<close>

text \<open>Task 1 (4 points): download and extract the (complete) AFP, and invoke 
   @{verbatim \<open>isabelle jedit -d path/to/AFP/thys Exercise12.thy\<close>}. 
  Then activate the commented import-statement, the commented part below and remove the sorry.

  Remark: in @{verbatim \<open>path/to/AFP/thys\<close>} there is a \<^verbatim>\<open>ROOTS\<close>-file that
    includes all ROOT-files of all sessions in the AFP. So, you do not have
    to include all directories individually, but only one.\<close>

(*
definition prime_test :: "nat \<Rightarrow> bool" where
  "prime_test n = (1 < n \<and> (\<forall> x \<in> set [2 ..< Suc (nat (sqrt_nat_floor n))]. \<not> x dvd n))"  

lemma le_sqrt_nat_floor: "x * x \<le> n \<Longrightarrow> x \<le> nat (sqrt_nat_floor n)" 
  unfolding sqrt_nat_floor
  by (metis (mono_tags, lifting) le_nat_floor of_nat_0_le_iff of_nat_mono of_nat_mult real_sqrt_ge_0_iff sqrt_sqrt square_lesseq_square)

lemma sqrt_nat_floor_le: "n \<le> x * x \<Longrightarrow> nat (sqrt_nat_floor n) \<le> x" 
  unfolding sqrt_nat_floor
  by (metis floor_mono floor_of_nat nat_le_iff of_nat_0_le_iff of_nat_le_iff of_nat_mult real_sqrt_le_iff real_sqrt_mult sqrt_sqrt)


lemma [code]: "prime_nat n = prime_test n" 
proof (cases "n = 2")
  case True
  show ?thesis unfolding True by code_simp
next
  case False
  define s where "s = nat (sqrt_nat_floor n)" 
  show ?thesis
    unfolding prime_test_def set_upt prime_nat_def
    unfolding prime_nat_iff' s_def[symmetric]
  proof (rule conj_cong[OF refl], standard)
    assume n1: "1 < n" 
    with False have n2: "2 < n" by auto
    (* easy direction *)
    have "s \<le> n - 1" using n2
      by (intro sqrt_nat_floor_le[of n, folded s_def], cases n; cases "n - 1", auto)
    hence "Suc s \<le> n" using n1 by auto
    thus "(\<forall>x\<in>{2..<n}. \<not> x dvd n) \<Longrightarrow> (\<forall>x\<in>{2..<Suc s}. \<not> x dvd n)" by auto
    (* more difficult direction *)
    assume ndvd: "\<forall>x\<in>{2..<Suc s}. \<not> x dvd n" 
    show "\<forall>x\<in>{2..<n}. \<not> x dvd n" 
    proof
      fix x
      assume x: "x \<in> {2 ..< n}" 
      show "\<not> x dvd n" 
      proof
        assume "x dvd n" 
        then obtain y where n: "n = x * y" by auto
        show False sorry
      qed
    qed
  qed
qed    

value (code) "prime_nat 100000007" 
value (code) "prime_nat 10000000019" 
*)

text \<open>Task 2 (1 point): Write a \<^file>\<open>ROOT\<close> file for this Exercise, and generate 
  a document for this session. It is perfectly fine to use the @{system_option quick_and_dirty}
  option within the \<^file>\<open>ROOT\<close> file.\<close>


text \<open>Also specify the command line that is necessary to compile the document:
  
  \<^verbatim>\<open>isabelle build TODO\<close>\<close>




section \<open>Exercise 2 -- 5 points\<close>

hide_const inv

text \<open>Let us design some algebraic structures\<close>

text \<open>@{class plus} just fixes some constant \<open>(+)\<close>.\<close>
class semigroup = plus + 
  assumes plus_assoc: "x + (y + z) = (x + y) + z" 

text \<open>@{class zero} just fixes some constant 0.\<close>
class monoid = zero + semigroup + 
  assumes left_zero: "0 + x = x" 
    and right_zero: "x + 0 = x" 

class group = semigroup + zero + 
  fixes inv :: "'a \<Rightarrow> 'a" 
  assumes left_inv: "inv x + x = 0" 
    and gr_left_zero: "0 + x = x"  

context group (* perform reasoning for all groups *)
begin

text \<open>Task 1 -- 2 points\<close>


text \<open>Let us prove the right-variants of @{thm left_inv} and @{thm left_zero}.
  Consequently every group is a monoid.

  (either use equational reasoning manually or sledgehammer)\<close>

lemma gr_right_zero: "x + 0 = x" sorry
lemma right_inv: "x + inv x = 0" sorry

subclass monoid \<comment> \<open>hence all results for monoids will become available for groups as well\<close>
proof 
  oops (* complete this proof as well *)

end

text \<open>Task 2 -- 3 points\<close>

text \<open>Make lists an instance of @{class monoid} (using @{const append} and @{const Nil}) 
  and integers an instance of @{class group}.

  Note that the method to prove a class-instance starts with @{method intro_classes}.\<close>

instantiation list :: (type) monoid
begin
definition zero_list :: "'a list" where "zero_list = undefined"
definition plus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where "plus_list = undefined" 
instance sorry
end



text \<open>Note that after the class instantions the generic lemmas and syntax become available\<close>

(*
thm left_inv[of "5 :: int"]
thm right_inv[of "5 :: int"]
thm right_zero[of "''abc''"]

value "0 + ''abc'' + 0 + ''de''" 
*)

end