[SOLVED] 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 (ruleexI)
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 innotE)
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