theory practical imports Main Real begin (* -------------------------------------------------------------- *) (* | PART 1: | *) (* | PROPOSITIONAL LOGIC | *) (* | AND QUANTIFIERS | *) (* -------------------------------------------------------------- *) (* --------------------------- *) (* | Problem 1 (2 marks): | *) (* --------------------------- *) lemma "(P \ Q) \ (P \ \Q) \ (P \ R)" oops (* --------------------------- *) (* | Problem 2 (2 marks): | *) (* --------------------------- *) lemma "(P \ Q) \ (R \ S) \ P \ R \ Q \ S" oops (* --------------------------- *) (* | Problem 3 (3 marks): | *) (* --------------------------- *) lemma "(\P \ \Q) \ \(P \ Q)" oops (* --------------------------- *) (* | Problem 4 (3 marks): | *) (* --------------------------- *) lemma "\ (\x. \ P x) \ (\x. P x)" oops (* --------------------------- *) (* | Problem 5 (5 marks): | *) (* --------------------------- *) lemma "\x. drunk x \ (\y. drunk y)" oops (* -------------------------------------------------------------- *) (* | PART 2: | *) (* | STRUCTURED PROOF AND | *) (* | POWERFUL REASONING TOOLS | *) (* -------------------------------------------------------------- *) (* From this point on you can use any of the following tactics: auto, simp, blast, fast, force, fastforce, presburger, algebra, unfold, induction. However, you are NOT allowed to use metis, meson and smt. *) (* --------------------------- *) (* | Problem 6 (3 marks): | *) (* --------------------------- *) (* Fill in the blanks in the following proof: *) lemma "\(\P. (\ y::int. \x::int. P x y) \ (\x. \y. P x y))" proof simp (* This step is given. Don't erase this, and don't try writing before this line. *) (* FILL THIS SPACE *) qed definition "R12 (x::int) y \ 12 dvd (x-y)" (* --------------------------- *) (* | Problem 7 (2 marks): | *) (* --------------------------- *) (* Fill in the blanks in the following proof: *) theorem reflR: "R12 x x" proof (unfold R12_def dvd_def) (* This step is given. Don't erase this, and don't try writing before this line. *) (* FILL THIS SPACE *) qed (* --------------------------- *) (* | Problem 8 (3 marks): | *) (* --------------------------- *) (* Fill in the blanks in the following proof: *) theorem symR: "R12 x y \ R12 y x" proof (unfold R12_def dvd_def, auto) (* This step is given. Don't erase this. *) fix k assume "(x - y) = 12 * k" (* This step is given. Don't erase this, don't try writing before this line. *) (* FILL THIS SPACE *) next fix k assume "(y - x) = 12 * k" (* This step is given. Don't change anything before this. *) (* FILL THIS SPACE *) qed (* --------------------------- *) (* | Problem 9 (3 marks): | *) (* --------------------------- *) (* Fill in the blanks in the following proof: *) theorem transR: "R12 x y \ R12 y z \ R12 x z" proof (unfold R12_def dvd_def, auto) (* This step is given. Don't change anything before this. *) (* FILL THIS SPACE *) qed (* you may find these equalities useful at some point. Do not erase this lemma *) lemma numeral_simps: "3 = Suc 2" "2 = Suc 1" "1 = Suc 0" by simp+ (* ---------------------------- *) (* | Problem 10 (2 marks): | *) (* ---------------------------- *) (* Define gauss_sum (1 pt) (the sum of all naturals from 1 to n) Do not modify the structure of the definition; only fill in the missing part. *) primrec gauss_sum :: "nat \ nat" where "gauss_sum (Suc n) = (* FILL THIS SPACE *)" | "gauss_sum 0 = (* FILL THIS SPACE *)" (* state theorem, prove (1 pt). *) theorem (* FILL THIS SPACE *) (* FILL THIS SPACE *) (* ---------------------------- *) (* | Problem 11 (2 marks): | *) (* ---------------------------- *) (* define sum_of_odds (1 pt), state theorem, prove (1 pt).*) primrec sum_of_odds :: "nat \ nat" where (* FILL THIS SPACE *) theorem (* FILL THIS SPACE *) (* FILL THIS SPACE *) (* ---------------------------- *) (* | Problem 12 (5 marks): | *) (* ---------------------------- *) primrec power_sum :: "nat \ nat \ nat" where "power_sum n (Suc m) = (power_sum n m) + (n - 1) * n^(Suc m)" | "power_sum n 0 = (n - 1)" theorem "n > 0 \ power_sum n m = n^(m+1) - 1" oops (* FILL THIS SPACE *) (* ---------------------------- *) (* | Problem 13 (5 marks): | *) (* ---------------------------- *) lemma "\x\X. \y\X. x = y \ card X \ 1" oops (* FILL THIS SPACE *) (* -------------------------------------------------------------- *) (* | PART 3: | *) (* | FORMALISING AND REASONING | *) (* | ABOUT GEOMETRIES USING LOCALES | *) (* -------------------------------------------------------------- *) (* From this point on you can also use metis and meson, but not smt. *) (* ---------------------------- *) (* | Problem 14 (2 marks): | *) (* ---------------------------- *) (* State formally the following axioms (first 3 are given; one point per each of the others): *) locale Simple_Geometry = fixes plane :: "'a set" fixes lines :: "('a set) set" assumes A1: "plane \ {}" and A2: "\l \ lines. l \ plane \ l \ {}" and A3: "\p \ plane. \q \ plane. \l \ lines. {p,q} \ l" and A4: (* FILL THIS SPACE: Two different lines intersect in no more than one point. *) and A5: (* FILL THIS SPACE: For every line L there is a point in the plane outside of L. *) (* --------------------------- *) (* | Problem 15 (1 point): | *) (* --------------------------- *) (* Formalise the statement: the set of lines is non-empty *) lemma (in Simple_Geometry) one_line_exists: (* FILL THIS SPACE: The set of lines is non-empty *) oops (* ---------------------------- *) (* | Problem 16 (2 marks): | *) (* ---------------------------- *) lemma (in Simple_Geometry) two_points_exist: "\p1 p2. p1 \ p2 \ {p1,p2} \ plane" oops (* ---------------------------- *) (* | Problem 17 (3 marks): | *) (* ---------------------------- *) lemma (in Simple_Geometry) three_points_exist: "\p1 p2 p3. distinct [p1,p2,p3] \ {p1,p2,p3} \ plane" oops (* ---------------------------- *) (* | Problem 18 (3 marks): | *) (* ---------------------------- *) (* REMEMVER THAT CARD OF INFINITE SETS IS 0! *) lemma (in Simple_Geometry) card_of_plane_greater: "finite plane \ card plane \ 3" oops (* ---------------------------- *) (* | Problem 19 (2 marks): | *) (* ---------------------------- *) (* GIVE THE SMALLEST MODEL! *) definition "plane_3 \ (* FILL THIS SPACE *)" definition "lines_3 \ (* FILL THIS SPACE *)" interpretation Simple_Geometry_smallest_model: Simple_Geometry plane_3 lines_3 apply standard oops (* ---------------------------- *) (* | Problem 20 (5 marks): | *) (* ---------------------------- *) lemma (in Simple_Geometry) how_to_produce_different_lines: assumes "l \ lines" "{a, b} \ l" "a \ b" "p \ l" "n \ lines" "{a, p} \ n" "m \ lines" "{b, p} \ m" shows "m \ n" oops (* ---------------------------- *) (* | Problem 21 (4 marks): | *) (* ---------------------------- *) lemma (in Simple_Geometry) how_to_produce_different_points: assumes "l \ lines" "{a, b} \ l" "a \ b" "p \ l" "n \ lines" "{a, p, c} \ n" "m \ lines" "{b, p, d} \ m" "p \ c" shows "c \ d" oops (* --------------------------- *) (* | Problem 22 (1 point): | *) (* --------------------------- *) (* 1 point: Formalise the following axiom: if a point p lies outside of a line l then there must exist at least one line m that passes through p, which does not intersect l *) locale Non_Projective_Geometry = Simple_Geometry + assumes parallels_Ex: (* FILL THIS SPACE *) (* ---------------------------- *) (* | Problem 23 (2 marks): | *) (* ---------------------------- *) (* Give a model of Non-Projective Geometry with cardinality 4. Show that it is indeed a model using the command "interpretation" *) (* FILL THIS SPACE *) (* ---------------------------- *) (* | Problem 24 (3 marks): | *) (* ---------------------------- *) (* Formalise and prove: "it is not true that every pair of lines intersect" *) lemma (in Non_Projective_Geometry) non_projective: (* fill this space *) oops (* The following are some auxiliary lemmas that may be useful. You don't need to use them if you don't want. *) lemma construct_set_of_card1: "card x = 1 \ \ p1. x = {p1}" by (metis One_nat_def card_eq_SucD) lemma construct_set_of_card2: "card x = 2 \ \ p1 p2 . distinct [p1,p2] \ x = {p1,p2}" by (metis card_eq_SucD distinct.simps(2) distinct_singleton list.set(1) list.set(2) numeral_2_eq_2) lemma construct_set_of_card3: "card x = 3 \ \ p1 p2 p3. distinct [p1,p2,p3] \ x = {p1,p2,p3}" by (metis card_eq_SucD distinct.simps(2) distinct_singleton list.set(1) list.set(2) numeral_3_eq_3) lemma construct_set_of_card4: "card x = 4 \ \ p1 p2 p3 p4. distinct [p1,p2,p3,p4] \ x = {p1,p2,p3,p4}" by (metis (no_types, lifting) card_eq_SucD construct_set_of_card3 Suc_numeral add_num_simps(1) add_num_simps(7) distinct.simps(2) empty_set list.set(2)) (* GIVEN *) locale Projective_Geometry = Simple_Geometry + assumes A6: "\l \ lines. \m \ lines. \p \ plane. p \ l \ p \ m" and A7: "\l \ lines. \x. card x = 3 \ x \ l" (* ---------------------------- *) (* | Problem 25 (3 marks): | *) (* ---------------------------- *) (* Prove this alternative to axiom A7 *) lemma (in Projective_Geometry) A7': "\l \ lines. \p1 p2 p3. {p1,p2,p3} \ plane \ distinct [p1,p2,p3] \ {p1,p2,p3} \ l" oops (* ---------------------------- *) (* | Problem 26 (3 marks): | *) (* ---------------------------- *) (* Prove yet another alternative to axiom A7 *) lemma (in Projective_Geometry) A7'': "l \ lines \ {p,q} \ l \ (\r \ plane. r \ {p,q} \ r \ l)" oops (* ---------------------------- *) (* | Problem 27 (5 marks): | *) (* ---------------------------- *) lemma (in Projective_Geometry) two_lines_per_point: "\p \ plane. \l \ lines. \m \ lines. l \ m \ p \ l \ m" oops (* ---------------------------- *) (* | Problem 28 (4 marks): | *) (* ---------------------------- *) lemma (in Projective_Geometry) external_line: "\p \ plane. \l \ lines. p \ l" oops (* ---------------------------- *) (* | Problem 29 (6 marks): | *) (* ---------------------------- *) lemma (in Projective_Geometry) three_lines_per_point: "\p \ plane. \l m n. distinct [l,m,n] \ {l,m,n} \ lines \ p \ l \ m \ n" oops (* ----------------------------- *) (* | Problem 30 (8 marks): | *) (* ----------------------------- *) lemma (in Projective_Geometry) at_least_seven_points: "\p1 p2 p3 p4 p5 p6 p7. distinct [p1,p2,p3,p4,p5,p6,p7] \ {p1,p2,p3,p4,p5,p6,p7} \ plane" oops (* ----------------------------- *) (* | Problem 31 (3 marks): | *) (* ----------------------------- *) (* Give a model of Projective Geometry with 7 points; use the command "interpretation" to prove that it is indeed a model. *) (* FILL THIS BLANK *) end