theory Practical imports Main begin (***************************First-order logic*************************************) (*1 mark*) lemma "A\A \ A" oops (*1 mark*) lemma "(P\R)\(\P\R)" oops (*1 mark*) lemma "(P\Q\R)\P\Q\R" oops (*3 marks*) lemma "\\P \ \P" oops (*4 marks*) lemma "(P\R)\(\(\P\ \R))" oops (*1 mark*) lemma "(\ x . F x) \ (\ x . G x ) \ (\ x . F x \ G x )" oops (*1 mark*) lemma "(\ x y. R x y) \ (\ x . R x x )" oops (*3 marks*) lemma "(\x. P x)\(\x.\P x)" oops (*3 marks*) lemma "(\x. \ (P x \ Q x)) \ \(\x. \P x \ Q x)" oops (*3 marks*) lemma "\Bob. (drunk Bob \ (\y. drunk y))" oops (*4 marks*) lemma "\ (\ barber . man barber \ (\ x . man x \ \shaves x x \ shaves barber x ))" oops locale incidence = fixes incidence_points_on_sections :: "'point \ 'section \ bool" (infix " \\<^sub>p\<^sub>o\<^sub>i\<^sub>n\<^sub>t " 80) fixes region_to_section :: "'region \ 'section" assumes section_nonempty: (*Write here your axiom stating that every section has a point incident to it*) (*2 marks*) and section_uniqueness: (*Write here your axiom stating that two sections are the same if the same points are incident to each*) (*2 marks*) begin definition isPartOf ::"'section \ 'section \ bool" (infix "isPartOf" 80) where (*write your formalisation of definition D1 here*) (*1 mark*) definition inclusion ::"'region \ 'section \ bool"(infix "isIncludedIn" 80) where (*write your formalisation of definition D2 here*) (*1 mark*) definition overlaps ::"'region \ 'section \ bool"(infix "overlaps" 80) where (*write your formalisation of definition D3 here*) (*1 mark*) lemma region_overlaps_itself: "R overlaps (region_to_section R)" (*Write your structured proof here*) (*2 marks*) oops (*Formalise and prove that isPartOf is reflexive, transitive and antisymmetric*) (*3 marks*) lemma isPartOf_reflexive: (*Formalise and prove that isPartOf is reflexive here*) oops lemma isPartOf_transitive: (*Formalise and prove that isPartOf is transitive here*) oops lemma isPartOf_antisymmetric: (*Formalise and prove that isPartOf is antisymmetric here*) oops end locale section_bundles = incidence incidence_points_on_sections region_to_section for incidence_points_on_sections :: "'point \ 'section \ bool" and region_to_section :: "'region \ 'section" + fixes crossing :: "'region \ 'section \ bool" (infix "crosses" 80) and incidence_sections_on_bundles :: "'section \ 'bundle \ bool" (infix "\\<^sub>s\<^sub>e\<^sub>c\<^sub>t\<^sub>i\<^sub>o\<^sub>n" 80) assumes SC1: (*Write your formalisation of Axiom SC1 here*) (*1 mark*) and SI1: (*Write your formalisation of Axiom SI1 here*) (*1 mark*) begin definition atLeastAsRestrictiveAs :: "'section \ 'bundle \ 'section \ bool" where (*Write your formalisation of atLeastAsRestrictiveAs here*) (*1 mark*) notation atLeastAsRestrictiveAs ("_ \\<^sub>_ _" [80, 80, 80] 80) (*Formalise and prove that atLeastAsRestrictiveAs is reflexive, transitive and antisymmetric*) (*2 marks*) (*Kulik and Eschenbach say 'The relation \ is reflexive, transitive and antisymmetric for a given sector bundle.' So, do they mean, given that the sections under consideration are in the bundle? This is what we assume for reflexivity.*) lemma atLeastAsRestrictiveAs_reflexive: assumes "s \\<^sub>s\<^sub>e\<^sub>c\<^sub>t\<^sub>i\<^sub>o\<^sub>n b" shows "s \\<^sub>b s" (*Add your proof here*) oops lemma atLeastAsRestrictiveAs_transitive: (*Formalise and prove that atLeastAsRestrictiveAs is transitive*) oops lemma atLeastAsRestrictiveAs_antisymmetric: (*Formalise and prove that atLeastAsRestrictiveAs is antisymmetric*)) oops end locale comparison = section_bundles incidence_points_on_sections region_to_section crossing incidence_sections_on_bundles for incidence_points_on_sections :: "'point \ 'section \ bool" (infix "\\<^sub>p\<^sub>o\<^sub>i\<^sub>n\<^sub>t" 80) and region_to_section :: "'region \ 'section" and crossing :: "'region \ 'section \ bool" (infix "crosses" 80) and incidence_sections_on_bundles :: "'section \ 'bundle \ bool" (infix "\\<^sub>s\<^sub>e\<^sub>c\<^sub>t\<^sub>i\<^sub>o\<^sub>n" 80)+ assumes SB2:(*Write your formalisation of Axiom SB2 here*) (*1 mark*) begin lemma T1:(*Write your formalisation and proof of Theorem T1 here*) (*1 mark*) lemma T2:(*Write your formalisation and proof of Theorem T2 here*) (*1 mark*) definition isCore (infix "isCoreOf" 80) where "s isCoreOf b = (s \\<^sub>s\<^sub>e\<^sub>c\<^sub>t\<^sub>i\<^sub>o\<^sub>n b \ (\s'. s' \\<^sub>s\<^sub>e\<^sub>c\<^sub>t\<^sub>i\<^sub>o\<^sub>n b \ s \\<^sub>b s'))" definition (*Write your definition of hull here*) (*1 mark*) end locale crossing_sector = comparison incidence_points_on_sections region_to_section crossing incidence_sections_on_bundles for incidence_points_on_sections :: "'point \ 'section \ bool" (infix "\\<^sub>p\<^sub>o\<^sub>i\<^sub>n\<^sub>t" 80) and region_to_section :: "'region \ 'section" and crossing :: "'region \ 'section \ bool" (infix "crosses" 80) and incidence_sections_on_bundles :: "'section \ 'bundle \ bool" (infix "\\<^sub>s\<^sub>e\<^sub>c\<^sub>t\<^sub>i\<^sub>o\<^sub>n" 80) + assumes SC2: (*Write your formalisation of Axiom SC2 here*) (*1 mark*) begin lemma overlaps_core: (*Write your formalisation and structured proof of the remark `If a region overlaps the core of a section bundle then it overlaps every section of the section bundle'*) (*4 marks*) lemma crosses_hull: (*Write your formalisation and structured proof of the remark `If a region crosses the hull of a section bundle then it crosses every sector of the section bundle'*) (*4 marks*) lemma not_overlap_hull: (*Write your formalisation and structured proof of the remark `If a region does not overlap the hull of a section bundle, it does not overlap any of its sections'*) (*4 marks*) definition overlapsAsMuchAs :: "'region \ 'bundle \ 'region \ bool" where "overlapsAsMuchAs R b R' == (\s. s \\<^sub>s\<^sub>e\<^sub>c\<^sub>t\<^sub>i\<^sub>o\<^sub>n b \ R' overlaps s \ R overlaps s)" notation overlapsAsMuchAs ("_ \\<^sub>o\<^sub>v\<^sub>e\<^sub>r\<^sub>l\<^sub>a\<^sub>p\<^sub>s \<^sub>_ _" [80, 80, 80] 80) definition eq_overlapsAsMuchAs :: "'region \ 'bundle \ 'region \ bool" where "eq_overlapsAsMuchAs R b R' == R \\<^sub>o\<^sub>v\<^sub>e\<^sub>r\<^sub>l\<^sub>a\<^sub>p\<^sub>s \<^sub>b R' \ R' \\<^sub>o\<^sub>v\<^sub>e\<^sub>r\<^sub>l\<^sub>a\<^sub>p\<^sub>s \<^sub>b R" notation eq_overlapsAsMuchAs ("_ \\<^sub>o\<^sub>v\<^sub>e\<^sub>r\<^sub>l\<^sub>a\<^sub>p\<^sub>s \<^sub>_ _" [80, 80, 80] 80) abbreviation rev_overlapsAsMuchAs :: "'region \ 'bundle \ 'region \ bool" ("_ \\<^sub>o\<^sub>v\<^sub>e\<^sub>r\<^sub>l\<^sub>a\<^sub>p\<^sub>s \<^sub>_ _" [80, 80, 80] 80) where"rev_overlapsAsMuchAs R b R' == overlapsAsMuchAs R' b R" definition more_overlapsAsMuchAs :: "'region \ 'bundle \ 'region \ bool" where "more_overlapsAsMuchAs R b R' == R \\<^sub>o\<^sub>v\<^sub>e\<^sub>r\<^sub>l\<^sub>a\<^sub>p\<^sub>s \<^sub>b R' \ \(R' \\<^sub>o\<^sub>v\<^sub>e\<^sub>r\<^sub>l\<^sub>a\<^sub>p\<^sub>s \<^sub>b R)" notation more_overlapsAsMuchAs ("_ >\<^sub>o\<^sub>v\<^sub>e\<^sub>r\<^sub>l\<^sub>a\<^sub>p\<^sub>s \<^sub>_ _" [80, 80, 80] 80) abbreviation less_overlapsAsMuchAs :: "'region \ 'bundle \ 'region \ bool" ("_ <\<^sub>o\<^sub>v\<^sub>e\<^sub>r\<^sub>l\<^sub>a\<^sub>p\<^sub>s \<^sub>_ _" [80, 80, 80] 80) where"less_overlapsAsMuchAs R b R' == more_overlapsAsMuchAs R' b R" (*Formalise and prove that overlapsAsMuchAs is reflexive and transitive*) (*2 marks*) lemma overlapsAsMuchAs_reflexive: (*Write your formalisation and proof that overlapsAsMuchAs is reflexive here*) lemma overlapsAsMuchAs_transitive: (*Write your formalisation and proof that overlapsAsMuchAs is transitive here*) lemma T3: (*Write your formalisation and structured proof of Theorem T3 here. You must attempt to formalise Kulik et al.'s reasoning*) (*11 marks*) (*In under 200 words, compare and contrast the mechanical proof that you produced with the pen-and-paper proof by Kulik et al.\. In particular, indicate any reasoning, proof parts, and/or useful lemmas that you had to make explicit during the mechanisation but may have been glossed over or assumed by the pen-and-paper proof. Also highlight any inaccuracies in their language or notation. Note any parts where you had to diverge from their reasoning, and why. Write your answer in a comment here.*) (*4 marks*) lemma T4: (*Write your formalisation and proof of Theorem T4 here*) (*1 mark*) lemma T5: (*Write your formalisation and structured proof of Theorem T5 here. You must show it follows from T4*) (*3 marks*) (********************Challenge problem****************************************) definition crosses_isIncludedIn (*Write your definition of the relation ci here. Kulik et al. say `If a region crosses or is included in a section we write ci'.*) (*2 marks*) definition crosses_isIncludedInAsMuchAs (*Write your definition of `crosses or is included in as much as' here*) (*2 marks*) definition belongsAsMuchAs (*Write your definition of `belongs as much as here: definition D8 in the paper.*) (*2 marks*) (*Formalise and write structured proofs of Theorems T6-T8 for both crossesIncludedInAsMuchAs and belongsAsMuchAs*) (*14 marks*) lemma T6_crosses_isIncludedInAsMuchAs: lemma T6_belongsAsMuchAs: lemma T7_crosses_isIncludedInAsMuchAs: lemma T7_belongsAsMuchAs: lemma T8_crosses_isIncludedInAsMuchAs: lemma T8_belongsAsMuchAs: end end