[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