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