CS计算机代考程序代写 theory Practical

theory Practical
imports Main
begin

section \Part 1\

(* 1 mark *)
lemma disjunction_idempotence:
“A \ A \ A”
apply(rule iffI)
apply(erule disjE)
apply assumption+
apply(rule disjI1)
apply assumption
done

(* 1 mark *)
lemma conjunction_idempotence:
“A \ A \ A”
apply(rule iffI)
apply(erule conjE)
apply assumption
apply(rule conjI)
apply assumption+
done

(* 1 mark *)
lemma disjunction_to_conditional:
“(\ P \ R) \ (P \ R)”
apply(rule impI)+
apply(erule disjE)
apply(erule notE)
apply assumption+
done

(* 1 mark *)
lemma
“(\x. P x \ Q x) \ (\x. P x) \ (\x. Q x)”
apply(rule impI)
apply(rule conjI)
apply(erule exE)
apply(erule conjE)
apply (rule exI)
apply assumption
apply(erule exE)
apply(erule conjE)
apply(rule exI)
apply assumption
done

(* 1 mark *)
lemma
“(\ (\x. \P x) \ R) \ ((\x. \ P x) \ R)”
apply(rule impI)+
apply(erule disjE)
apply(erule notE)
apply assumption+
done

(* 2 marks *)
lemma
“(\x. P x) \ \ (\x. \ P x)”
apply(rule impI)
apply(rule notI)
apply(erule exE)
apply(erule_tac allE)
apply(erule notE)
apply assumption
done

(* 3 marks *)
text \Prove using ccontr\
lemma excluded_middle:
“P \ \ P”
apply (rule ccontr)
apply (rule_tac P = P in notE)
apply(rule notI)
apply(erule notE)
apply(rule disjI1)
apply assumption
apply (rule ccontr)
apply(erule notE)
apply(rule disjI2)
apply assumption
done

(* 3 marks *)
text \Prove using excluded middle\
lemma notnotD:
“\\ P \ P”
apply(rule disjE)
apply(rule excluded_middle)
apply assumption
apply(erule notE)
apply assumption
done

(* 3 marks *)
text \Prove using double-negation (rule notnotD)\
lemma classical:
“(\ P \ P) \ P”
apply(drule impI)
apply(rule notnotD)
apply(rule notI)
apply(erule impE)
apply assumption
apply(erule notE)
apply assumption
done

(* 3 marks *)
text \Prove using classical\
lemma ccontr:
“(\ P \ False) \ P”
apply(drule notI)
apply(rule classical)
apply(erule notE)
apply assumption
done

(* 3 marks *)
lemma
“(\ (\x. P x \ R x)) = (\x. \ P x \ \ R x)”
apply(rule iffI)
apply(rule ccontr)
apply(erule notE)
apply(rule allI)
apply(rule classical)
apply(erule notE)
apply(rule exI)
apply(rule conjI)

apply(rule notI)
apply(erule notE)
apply(rule disjI1)
apply assumption

apply(rule notI)
apply(erule notE)
apply(rule disjI2)
apply assumption

apply(rule notI)
apply(rule ccontr)
apply(erule exE)
apply(erule allE)

apply(erule notE)
apply(erule disjE)
apply(erule conjE)
apply(erule notE)
apply assumption
apply(erule conjE)
apply(erule notE)+
apply assumption
done

(* 3 marks *)
lemma
“(\x. P x \ R x) = (\((\x. \ P x) \ \ (\x. R x)))”
apply(rule iffI)
apply(rule notI)
apply(erule exE)
apply(erule conjE)
apply(erule notE)
apply(rule exI)
apply(erule allE)
apply(erule disjE)
apply(erule notE)
apply assumption+

apply(rule classical)
apply(erule notE)
apply(rule conjI)
apply(rule allI)
apply(rule notI)
apply(erule notE)
apply(rule exI)
apply(rule disjI1)
apply assumption
apply(rule notI)
apply(erule notE)
apply(erule exE)
apply(rule exI)
apply(rule disjI2)
apply assumption
done

section \Part 2.1\

locale partof =
fixes partof :: “‘region \ ‘region \ bool” (infix “\” 100)
begin

(* 1 mark *)
definition properpartof :: “‘region \ ‘region \ bool” (infix “\” 100) where
“x \ y \ x \ y \ x \ y”

(* 1 mark *)
definition overlaps :: “‘region \ ‘region \ bool” (infix “\” 100) where
“x \ y \ \z. z \ x \ z \ y”

definition disjoint :: “‘region \ ‘region \ bool” (infix “\” 100) where
“x \ y \ \ x \ y”

(* 1 mark *)
definition partialoverlap :: “‘region \ ‘region \ bool” (infix “~\” 100) where
“x ~\ y \ x \ y \ \x \ y \ \y \ x”

(* 1 mark *)
definition sumregions :: “‘region set \ ‘region \ bool” (“\ _ _” [100, 100] 100) where
“\ \ x \ (\y \ \. y \ x) \ (\y. y \ x \ (\z \ \. y \ z ))”

end

(* 1+1+1=3 marks *)
locale mereology = partof +
assumes A1: “\x y z. x \ y \ y \ z \ x \ z”
and A2: “\\. \ \ {} \ (\x. \ \ x)”
and A2′: “\\ x y. \ \ x \ \ \ y \(x = y)”
begin

section \Part 2.2\

(* 2 marks *)
theorem overlaps_sym:
“(x \ y) = (y \ x)”
apply (unfold overlaps_def)
oops

(* 1 mark *)
theorem in_sum_set_partof:
“undefined”
oops

(* 3 marks *)
theorem overlaps_refl:
“undefined”
oops

(* 1 mark *)
theorem all_has_partof:
“undefined”
oops

(* 2 marks *)
theorem partof_overlaps:
assumes “undefined”
shows “undefined”
oops

(* 1 mark *)
theorem sum_parts_eq:
“undefined”
oops

(* 2 marks *)
theorem sum_relation_is_same’:
assumes “\c. r y c \ c \ y”
and “\f. y \ f \ \g. r y g \ g \ f”
and “\ {y} x”
shows “\ {k. r y k} x”
oops

(* 1 mark *)
theorem overlap_has_partof_overlap:
assumes “undefined”
shows “undefined”
oops

(* 1 marks *)
theorem sum_parts_of_one_eq:
assumes “undefined”
shows “undefined”
oops

(* 5 marks *)
theorem both_partof_eq:
assumes “undefined”
shows “undefined”
oops

(* 4 marks *)
theorem sum_all_with_parts_overlapping:
assumes “undefined”
shows “undefined”
oops

(* 2 marks *)
theorem sum_one_is_self:
“undefined”
oops

(* 2 marks *)
theorem sum_all_with_parts_overlapping_self:
“undefined”
oops

(* 4 marks *)
theorem proper_have_nonoverlapping_proper:
assumes “undefined”
shows “undefined”
oops

(* 1 mark *)
sublocale parthood_partial_order: order “(\)” “(\)”
proof
show “\x y. x \ y = (x \ y \ \ y \ x)”
sorry
next
show “\x. x \ x”
sorry
next
show “\x y z. \x \ y; y \ z\ \ x \ z”
sorry
next
show “\x y. \x \ y; y \ x\ \ x = y”
sorry
qed

end

section \Part 2.3\

locale sphere =
fixes sphere :: “‘a \ bool”
begin

abbreviation AllSpheres :: “(‘a \ bool) \ bool” (binder “\\” 10) where
“\\x. P x \ \x. sphere x \ P x”

abbreviation ExSpheres :: “(‘a \ bool) \ bool” (binder “\\” 10) where
“\\x. P x \ \x. sphere x \ P x”

end

locale mereology_sphere = mereology partof + sphere sphere
for partof :: “‘region \ ‘region \ bool” (infix “\” 100)
and sphere :: “‘region \ bool”
begin

definition exttan :: “‘region \ ‘region \ bool” where
“exttan a b \ sphere a \ sphere b \ a \ b \ (\\x y. a \ x \ a \ y \ b \ x \ b \ y
\ x \ y \ y \ x)”

definition inttan :: “‘region \ ‘region \ bool” where
“inttan a b \ sphere a \ sphere b \ a \ b \ (\\x y. a \ x \ a \ y \ x \ b \ y \ b
\ x \ y \ y \ x)”

definition extdiam :: “‘region \ ‘region \ ‘region \ bool” where
“extdiam a b c \ exttan a c \ exttan b c
\ (\\x y. x \ c \ y \ c \ a \ x \ b \ y \ x \ y)”

definition intdiam :: “‘region \ ‘region \ ‘region \ bool” where
“intdiam a b c \ inttan a c \ inttan b c
\ (\\x y. x \ c \ y \ c \ exttan a x \ exttan b y \ x \ y)”

abbreviation properconcentric :: “‘region \ ‘region \ bool” where
“properconcentric a b \ a \ b
\ (\\x y. extdiam x y a \ inttan x b \ inttan y b \ intdiam x y b)”

definition concentric :: “‘region \ ‘region \ bool” (infix “\” 100) where
“a \ b \ sphere a \ sphere b \ (a = b \ properconcentric a b \ properconcentric b a)”

definition onboundary :: “‘region \ ‘region \ bool” where
“onboundary s r \ sphere s \ (\s’. s’ \ s \ s’ \ r \ \ s’ \ r)”

definition equidistant3 :: “‘region \ ‘region \ ‘region \ bool” where
“equidistant3 x y z \ \\z’. z’ \ z \ onboundary y z’ \ onboundary x z'”

definition betw :: “‘region \ ‘region \ ‘region \ bool” (“[_ _ _]” [100, 100, 100] 100) where
“[x y z] \ sphere x \ sphere z
\ (x \ y \ y \ z
\ (\x’ y’ z’ v w. x’ \ x \ y’ \ y \ z’ \ z
\ extdiam x’ y’ v \ extdiam v w y’ \ extdiam y’ z’ w))”

definition mid :: “‘region \ ‘region \ ‘region \ bool” where
“mid x y z \ [x y z] \ (\\y’. y’ \ y \ onboundary x y’ \ onboundary z y’)”

definition equidistant4 :: “‘region \ ‘region \ ‘region \ ‘region \ bool” (“_ _ \ _ _” [100, 100, 100, 100] 100) where
“x y \ z w \ \\u v. mid w u y \ mid x u v \ equidistant3 v z y”

definition oninterior :: “‘region \ ‘region \ bool” where
“oninterior s r \ \s’. s’ \ s \ s’ \ r”

definition nearer :: “‘region \ ‘region \ ‘region \ ‘region \ bool” where
“nearer w x y z \ \\x’. [w x x’] \ \ x \ x’ \ w x’ \ y z”

end

locale partial_region_geometry = mereology_sphere partof sphere
for partof :: “‘region \ ‘region \ bool” (infix “\” 100)
and sphere :: “‘region \ bool” +
assumes A4: “\x \ y; y \ z\ \ x \ z”
and A5: “\x y \ z w; x’ \ x\ \ x’ y \ z w”
and A6: “\sphere x; sphere y; \ x \ y\
\ \\s. \\z. oninterior z s = nearer x z x y”
and A7: “sphere x \ \\y. \ x \ y \ (\\z. oninterior z x = nearer x z x y)”
and A8: “x \ y = (\s. oninterior s x \ oninterior s y)”
and A9: “\\s. s \ r”
begin

(* 2 marks *)
thm equiv_def
theorem conc_equiv:
“equiv undefined undefined”
oops

(* 6 marks *)
theorem region_is_spherical_sum:
“undefined”
oops

(* 1 mark *)
theorem region_spherical_interior:
“undefined”
oops

(* 2 marks *)
theorem equal_interiors_equal_regions:
assumes “undefined”
shows “undefined”
oops

(* 2 marks *)
theorem proper_have_nonoverlapping_proper_sphere:
assumes “undefined”
shows “undefined”
oops

(* 4 marks *)
theorem not_sphere_spherical_parts_gt1:
assumes “undefined”
and “undefined”
shows “undefined”
oops

end

section \Part 3\

context mereology_sphere
begin

(* 3 marks *)
lemma
assumes T4: “\x y. \sphere x; sphere y\ \ x y \ y x”
and A9: “\\s. s \ r”
shows False
oops

(* 3 marks *)
definition equidistant3′ :: “‘region \ ‘region \ ‘region \ bool” where
“equidistant3′ x y z \ undefined”

no_notation equidistant4 (“_ _ \ _ _” [100, 100, 100, 100] 100)

definition equidistant4′ :: “‘region \ ‘region \ ‘region \ ‘region \ bool” (“_ _ \ _ _” [100, 100, 100, 100] 100) where
“x y \ z w \ \\u v. mid w u y \ mid x u v \ equidistant3′ v z y”

end

datatype two_reg = Left | Right | Both

(* 2 marks *)
definition tworeg_partof :: “two_reg \ two_reg \ bool” (infix “\” 100) where
“x \ y \ undefined”

(* 12 marks *)
interpretation mereology “(\)”
oops

end