theory PlaceAffordanceTheory imports Complex_Main begin declare [[show_types]] --{*This theory is a specification of place reference systems by Simon Scheider, January 2014*} --{*Basic types*} typedecl Action typedecl A --{* affordances *} typedecl Referent typedecl Focus typedecl Space typedecl Time type_synonym A' = "A + Action" type_synonym A'Type = "A' => bool" type_synonym AType = "A => bool" type_synonym Involvement = "Referent => A' => bool" type_synonym Place = "A'Type \ Involvement \ Involvement \ Referent" type_synonym ReferentType = "Referent => bool" consts --{*Affordance and action semi-lattice*} join :: "A => A => A" join' :: "Action => Action => Action" n::A --{*neutral element*} n'::Action --{*Participation*} agentOf :: Involvement objectOf :: Involvement productOf :: Involvement toolOf :: Involvement resourceOf :: Involvement supports :: Involvement performedAt :: "A' => Focus => bool" purpose :: "A' => A'" inv_profile :: "Involvement => A => ReferentType" --{*Referent types*} Vehicle :: "Referent => bool" --{*Space and Time*} wheref :: "Focus => Space" when :: "Focus => Time" leqt :: "Focus => Focus => bool" --{*Affordance Types (Primitive)*} Standing :: A'Type Placing :: A'Type Sitting :: A'Type Walking :: A'Type Climbing :: A'Type Seeing :: A'Type Hearing :: A'Type Talking :: A'Type Writing :: A'Type Showing :: A'Type Giving :: A'Type Receiving :: A'Type Manufacturing :: A'Type Cultivation :: A'Type --{*Axiomatization*} --{*temporal order *} axiomatization where totality: "ALL (x::Focus) (y::Focus). leqt x y \ leqt y x" and transitivity: "leqt x y & leqt y z --> leqt x z" definition eqt :: "Focus => Focus => bool" where "eqt x y == leqt x y & leqt y x" --{*antisymmetry*} --{*join semi-lattice on affordances and activities*} --{*least upper bound def*} fun lub :: "A list => A" where "lub [] = n" | "lub (Cons s' s) = join (lub s) s'" --{*non-compound affordances*} definition primAff :: "A => bool" where "primAff a == (ALL a' a''. join a' a'' = a --> a' = a & a''= a)" fun lub' :: "Action list => Action" where "lub' [] = n'" | "lub' (Cons s' s) = join' (lub' s) s'" --{*non-compound activities*} definition primAct :: "Action => bool" where "primAct a == (ALL a' a''. join' a' a'' = a --> a' = a & a''= a)" axiomatization where associativity: "join (join x y) z = join x (join y z)" and commutativity: "join x y = join y x" and idempotency: "join x x = x" and neutralelement : "join n x = x" and atomicity: "ALL (a::A). EX (as::A list). (lub as = a & (ALL a'. a': set as --> primAff a'))" --{* propagation of activity joins*} axiomatization where inversein: "ALL r (x::A) (y::A) (p::Involvement). p r (Inl x) --> p r (Inl (join x y))" and inverseinh2: "ALL f (x::A) (y::A). performedAt (Inl x) f --> performedAt (Inl (join x y)) f" and inversein': "ALL r (x::Action) (y::Action) (p::Involvement). p r (Inr x) --> p r (Inr (join' x y))" and inverseinh2': "ALL f (x::Action) (y::Action). performedAt (Inr x) f --> performedAt (Inr (join' x y)) f" --{*involvement profile for affordances (= dummy participant)*} axiomatization where inv: "ALL x (a::A) (inv::Involvement). (inv_profile inv) a x \ inv x (Inl a)" --{*activity kinds*} definition AK ::"A'Type set" where "AK == {Standing,Placing,Sitting,Walking,Climbing,Seeing,Hearing,Talking,Writing,Showing,Giving,Receiving,Manufacturing,Cultivation}" axiomatization excl where --{*... are conjunctively exhaustive on non-compound affordances and actions*} "ALL (a::A). primAff a--> (EX ak1. ak1:AK & ak1 (Inl a))" "ALL (a::Action). primAct a--> (EX ak1. ak1:AK & ak1 (Inr a))" --{* activity correspondence*} definition corresp :: "A => Action => bool" where "corresp a a' == (ALL (inv::Involvement) r. inv r (Inr a') \ inv r (Inl a)) & (ALL ak. ak:AK \ (ak (Inl a) \ ak (Inr a'))) & (ALL f. performedAt (Inr a') f \ performedAt (Inl a) f)" --{*Some defined types of activities*} definition Prompting ::A'Type where "Prompting a == ~(a = purpose a) & (ALL b. objectOf b a \ (agentOf b (purpose a)))" definition Supported :: A'Type where "Supported a == EX x. supports x a" definition Speechact:: A'Type where "Speechact a == (Showing a \ Talking a \ Writing a)" axiomatization affordancekinds where axiom1: "ALL (x::A'). (EX y. agentOf y x)" and axiom2: "ALL (x::A'). (EX y. performedAt x y)" and axiom3: "(Standing x \ Sitting x \ Walking x \ Climbing x \ Placing x) --> Supported x" and axiom44: "Placing a --> (EX y. objectOf y a)" and axiom4: "Seeing x --> (EX y. objectOf y x)" and axiom5: "Manufacturing a --> (EX x y z. productOf x a & resourceOf y a & toolOf z a)" and axiom6: "Cultivation a --> (EX x z. objectOf x a & toolOf z a)" and axiom8: "(Speechact a --> Prompting a) & (Giving a --> Prompting a)" and axiom10: "Talking a --> Hearing (purpose a) " and axiom11: "Showing a --> Seeing (purpose a)" and axiom12: "Writing a --> Seeing (purpose a)" and axiom13: "Giving a --> Receiving (purpose a)" and axiom14: "Giving a --> (EX y. resourceOf y a)" and axiom15: "Giving a & resourceOf y a --> resourceOf y (purpose a)" --{*Defined relations on activities*} definition covers :: "A' => A' => bool" where "covers b a == ALL x. performedAt a x --> performedAt b x" definition coincident :: "A' => A' => bool" where "coincident a b == covers a b \ covers b a" definition overlap :: "A' => A' => bool" where "overlap a b == (EX x. performedAt a x & performedAt b x)" definition endof :: "A' => Focus set" where "endof a == {e.((performedAt a e) & (ALL x. performedAt a x --> leqt x e))}" definition startof :: "A' => Focus set" where "startof a == {e. ((performedAt a e) & (ALL x. performedAt a x --> leqt e x))}" definition during :: "A' => A'=> bool" where "during a b == ALL x. performedAt a x --> (EX y. eqt x y & performedAt b y)" definition simultaneous :: "A' => A' => bool" where "simultaneous a b == during a b & during b a" definition concat :: "A' => A' => bool" where "concat a b == ( endof a = startof b)" definition coagentive :: "A' => A' => bool" where "coagentive a b == ALL x. agentOf x a \ agentOf x b" definition sequence :: "A' => A' => bool" where "sequence x y == coagentive x y & concat x y" definition coobjective :: "A' => A' => bool" where "coobjective a b == ALL x. objectOf x a \ objectOf x b" definition endures :: "A' => A' => bool" where "endures y x == (EX z. objectOf z x & agentOf z y)" --{*Compounds of affordances *} definition Combination :: "A => A => A => bool" where "Combination a x y == ~(x=y) & a = join x y" definition Simult :: "A => A => A => bool" where "Simult a x y == Combination a x y & simultaneous (Inl x) (Inl y)" definition Bitask :: "A => A => A => bool" where "Bitask a x y == Combination a x y & coincident (Inl x) (Inl y) & coagentive (Inl x) (Inl y)" --{*Complex involvements with things*} definition Sighting :: A'Type where "Sighting a == EX x y a'. Bitask a' x y & Inl a' = a & Seeing (Inl x) & Supported (Inl y)" definition BeingExposed :: "A' => A' =>bool" where "BeingExposed a x == endures a x & simultaneous x a & Supported a" definition BeingSightedFrom :: "A' => Referent => bool" where "BeingSightedFrom a r == EX x. BeingExposed a x & Sighting x & supports r x" definition ShelterFrom :: "A' => A'Type => bool" where "ShelterFrom a t == ~(EX a'. t a' & BeingExposed a a')" definition ShelterFromSight :: "A' => Referent => bool" where "ShelterFromSight a r == ShelterFrom a (% s. Sighting s & supports r s)" definition Accessing :: "A' => A' => A' => bool" where "Accessing x y z == Standing x & Walking y & Standing z & sequence x y & sequence y z " definition AccessableFrom :: "Referent => A' => bool" where "AccessableFrom r x == (EX y z. Accessing x y z & supports r z)" --{*Complex involvements with people*} --{*Transactions*} definition Transaction :: "A => A => A => bool" where "Transaction a x y == Simult a x y & (EX x' x'' y' y''. Giving (Inl x') & purpose (Inl x') = (Inl y') & Supported (Inl x'') & Supported (Inl y'') & Bitask x x' x'' & Bitask y y' y'')" definition TradingWith :: "A => Referent => Referent => Referent=> bool" where "TradingWith a ag1 ag2 ob == (EX x x1 x2 y y1 y2. resourceOf ob (Inl y1) & join x y = a & Transaction x x1 x2 & Transaction y y1 y2 & agentOf ag1 (Inl x1) & objectOf ag1 (Inl y1) & agentOf ag2 (Inl y1) & objectOf ag2 (Inl x1))" --{*Conversations *} definition Speech :: "A => A => A => bool" where "Speech a x y == Simult a x y & (EX x' x'' y' y''. Speechact (Inl x') & purpose (Inl x') = (Inl y') & Supported (Inl x'') & Supported (Inl y'') & Bitask x x' x'' & Bitask y y' y'')" definition Conversation :: "A=>Referent=>Referent=>bool" where "Conversation a ag1 ag2 == (EX x x1 x2 y y1 y2. join x y = a & Speech x x1 x2 & Speech y y1 y2 & agentOf ag1 (Inl x1) & objectOf ag1 (Inl y1) & agentOf ag2 (Inl y1) & objectOf ag2 (Inl x1))" definition Listening :: "A => A =>bool" where "Listening a b == Talking (Inl b) & purpose (Inl b) = (Inl a)" definition Watching :: "A =>A =>bool" where "Watching a b == Showing (Inl b) & purpose (Inl b) = (Inl a)" definition Reading :: "A => A => bool" where "Reading a b == Writing (Inl b) & purpose (Inl b) = (Inl a)" definition Marketing :: "A => Referent => Referent => bool" where "Marketing a ag2 ob == (EX ag1 x y. a = join x y & Conversation x ag1 ag2 & TradingWith y ag1 ag2 ob)" --{*Place construction, Locatum and locator, in*} definition Locator :: "Place => Referent" where "Locator p == snd (snd (snd p))" definition Locatuminv :: "Place => Involvement" where "Locatuminv p == fst (snd p)" definition Locatorinv :: "Place => Involvement" where "Locatorinv p == fst (snd (snd p))" definition Aftype :: "Place => A'Type" where "Aftype p == fst p" definition Af'type :: "Place => AType" where "Af'type p == (\x. (fst p) (Inl x))" definition Locatorinv' :: "Place => Referent => A => bool" where "Locatorinv' p == (\x y. Locatorinv p x (Inl y))" definition GroundedIn :: "Place => A => bool" where "GroundedIn p a == ((Aftype p) (Inl a) & (EX locatum .(Locatuminv p) locatum (Inl a) & (Locatorinv p) (Locator p) (Inl a)))" definition locatedAt :: "Place => Space => bool" where "locatedAt p s == (EX a x. GroundedIn p a & performedAt (Inl a) x & wheref x = s)" definition in_place :: "Referent => Place => Time=> bool" where "in_place r p t == EX a a' f. GroundedIn p a & corresp a a' & (Locatuminv p) r (Inr a') & performedAt (Inr a') f & when f = t" definition equipment :: "Referent => Place => bool" where "equipment z p == EX (inv::Involvement) a. GroundedIn p a & inv z (Inl a)" --{*Types of places*} definition StoringPlace :: "Place => bool" where "StoringPlace p == (Aftype p) = Placing & (Locatuminv p)= objectOf & (Locatorinv p) = supports" definition PlaceofSight :: "Place => bool" where "PlaceofSight p == (Aftype p) = (Sighting) & (Locatuminv p)= agentOf & (Locatorinv p) = objectOf" definition ShelterFromSightPlace :: "Place => bool" where "ShelterFromSightPlace p == ((Aftype p) = (% a . ShelterFromSight a (Locator p)) & (Locatuminv p)= agentOf & (Locatorinv p) = (% x y. ShelterFromSight y x))" definition Manufacture :: "Place => bool" where "Manufacture p == (Aftype p) = Manufacturing & (Locatuminv p)= agentOf & (Locatorinv p) = toolOf" definition Cropland :: "Place => bool" where "Cropland p == (Aftype p) = Cultivation & (Locatuminv p)= agentOf & (Locatorinv p) = objectOf" definition Station :: "Place => bool" where "Station p == Vehicle (Locator p) & (Aftype p) = (%a . AccessableFrom (Locator p) a) & (Locatuminv p)= agentOf & (Locatorinv p) = AccessableFrom" definition Market :: "Place => bool" where "Market p == (Af'type p) = (%a . (EX ob. Marketing a (Locator p) ob)) & (Locatuminv p)= agentOf & (Locatorinv' p) = (% r a. (EX ob. Marketing a r ob)) " --{* Theorems and models*} lemma induct2: "lub ([])= n" apply (simp ) done lemma induct3: "lub (Cons ax []) = ax" apply simp apply(insert neutralelement, assumption) done lemma lubexistence: "ALL (a::A). EX (as::A list). (lub as = a)" apply (rule allI, rule exI) apply (insert induct3, assumption) done --{* Simple Model*} consts a1::A a2::A r::Referent ob::Referent su::Referent f::Focus s::Space t::Time definition p:: Place where "p == (Sighting, agentOf, objectOf, ob)" definition a:: A where "a == join a1 a2" axiomatization where 1: "Seeing (Inl a1)" and 11: "Standing (Inl a2)" and 12: "supports su (Inl a2)" and 13: "objectOf ob (Inl a1)" and 2: "agentOf r (Inl a1)" and 21: "agentOf r (Inl a2)" and 22: "ALL ag a. agentOf ag (Inl a) --> r = ag " and 3: "purpose (Inl a1) = (Inl a1)" and 33: "purpose (Inl a2) = (Inl a2)" and 4: "performedAt (Inl a1) f" and 44: "performedAt (Inl a2) f" and 45: "ALL x\Focus. f = x " and 5: "wheref f = s" and 6: "when f = t" and 7: "leqt f f" and 8: "a1 ~= a2" lemma helper1: "Aftype (p) = Sighting" apply (simp add: Aftype_def, simp add:p_def) done lemma helper2: "Locatuminv (p) = agentOf" apply (simp add: Locatuminv_def, simp add:p_def) done lemma helper3: "Locatorinv (p) = objectOf" apply (simp add: Locatorinv_def, simp add:p_def) done lemma helper4: "Locator (p) = ob" apply (simp add: Locator_def, simp add:p_def) done lemma sight1: "performedAt (Inl a1) x = performedAt (Inl a2) x" apply (insert 45) apply (insert 4, insert 44) apply (drule_tac ?x =x in spec) apply (auto) done lemma sight2: "coincident (Inl a1) (Inl a2)" apply (simp add:coincident_def, simp add:covers_def) apply (insert sight1, simp) done lemma sight3: "coagentive (Inl a1) (Inl a2)" apply (simp add: coagentive_def, rule allI) apply (insert 2, insert 21) apply (insert 22) apply (drule_tac ?x =x in spec) apply (blast) done lemma sight4: "Combination a a1 a2" apply (insert 8, simp add:Combination_def, simp add:a_def) done lemma sighta: "Sighting (Inl a)" apply (insert 1, insert 11) apply (simp add: a_def, simp add: Sighting_def) apply (rule exI, rule exI, rule conjI) apply (simp add: Bitask_def) apply (insert sight2, insert sight3, insert sight4, simp add:a_def) apply auto apply (insert axiom3, simp) done lemma aa: "agentOf r (Inl a)" apply (insert 2, simp add:a_def) apply (insert inversein, drule spec, drule spec, drule spec, drule spec) apply (erule mp, simp) done lemma ac: "objectOf ob (Inl a)" apply (insert 13, simp add:a_def) apply (insert inversein, drule spec, drule spec, drule spec, drule spec) apply (erule mp, simp) done lemma ab: "performedAt (Inl a) f" apply (insert 4, simp add:a_def) apply (insert inversein, drule spec, drule spec, drule spec, drule spec) apply (erule mp, simp) done lemma Gr: "GroundedIn p a" apply (insert sighta) apply (insert aa) apply (insert ac) apply (insert helper1) apply (insert helper2) apply (insert helper3) apply (insert helper4) apply (simp add: p_def) apply (simp add: GroundedIn_def) apply (rule exI, simp) done lemma la: "locatedAt p s" apply (simp add: locatedAt_def) apply (rule exI, rule conjI) apply (insert Gr, simp) apply (insert ab) apply (insert 5) apply (rule exI, rule conjI, simp, simp) done lemma main: "PlaceofSight p" apply (simp add:PlaceofSight_def, rule conjI) apply (insert helper1, simp add:p_def) apply (rule conjI) apply (insert helper2, simp add:p_def) apply (insert helper3, simp add:p_def) done end