Theory FactoredSystemLib
theory FactoredSystemLib
imports Main "HOL-Library.Finite_Map"
begin
section ‹Factored Systems Library›
text ‹This section contains definitions used in the factored system theory (FactoredSystem.thy) and in
other theories. ›
subsection ‹Semantics of Map Addition›
text ‹ Most importantly, we are redefining the map addition operator (`++`) to reflect HOL4
semantics which are left to right (ltr), rather than right-to-left as in Isabelle/HOL.
This means that given a finite map (`M = M1 ++ M2`) and a variable `v` which is in the domain of
both `M1` and `M2`, the lookup `M v` will yield `M1 v` in HOL4 but `M2 v` in Isabelle/HOL.
This behavior can be confirmed by looking at the definition of `fmap\_add` (`++f`,
Finite\_Map.thy:460)---which is lifted from `map\_add` (Map.thy:24)
@{const map_add} (infixl "++" 100) where
@{term "m1 ++ m2 = (λx. case m2 x of None ⇒ m1 x | Some y ⇒ Some y)"}
to finite sets---and the HOL4 definition of "FUNION` (finite\_mapScript.sml:770) which recurs
on `union\_lemma` (finite\_mapScript.sml:756)
!\^fmap g.
?union.
(FDOM union = FDOM f Union (g ` FDOM)) /\
(!x. FAPPLY union x = if x IN FDOM f then FAPPLY f x else FAPPLY g x)
The ltr semantics are also reflected in [Abdulaziz et al., Definition 2, p.9].
›
hide_const (open) Map.map_add
no_notation Map.map_add (infixl ‹++› 100)
definition fmap_add_ltr :: "('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap" (infixl ‹++› 100) where
"m1 ++ m2 ≡ m2 ++⇩f m1"
subsection ‹States, Actions and Problems.›
text ‹ Planning problems are typically formalized by considering possible states and the effect
of actions upon these states.
In this case we consider a world model in propositional logic: i.e. states are finite maps of
variables (with arbitrary type 'a) to boolean values and actions are pairs of states where the first
component specifies preconditions and the second component specifies effects (postconditions) of
applying the action to a given state. [Abdulaziz et al., Definition 2, p.9] ›
type_synonym ('a) state = "('a, bool) fmap"
type_synonym ('a) action = "('a state × 'a state)"
type_synonym ('a) problem = "('a state × 'a state) set"
text ‹ For a given action @{term "π = (p, e)"} the action domain @{term "𝒟(π)"} is the set of variables `v` where
a value is assigned to `v` in either `p` or `e`, i.e. `p v` or `e v` are defined. [Abdulaziz et al.,
Definition 2, p.9] ›
definition action_dom where
"action_dom s1 s2 ≡ (fmdom' s1 ∪ fmdom' s2)"
text ‹ Now, for a given problem (i.e. action set) @{term "δ"}, the problem domain @{term "𝒟(δ)"} is given by the
union of the action domains of all actions in @{term "δ"}. [Abdulaziz et al., Definition 3, p.9]
Moreover, the set of valid states @{term "U(δ)"} is given by the union over all states whose domain is equal
to the problem domain and the set of valid action sequences (or, valid plans) is given by the
Kleene closure of @{term "δ"}, i.e. @{term "δ_star = {π. set(π) ⊆ δ}"}. [Abdulaziz et al., Definition 3, p.9]
Ultimately, the effect of executing an action `a` on a state `s` is given by calculating the
succeding state. In general, the succeding state is either the preceding state---if the action does
not apply to the state, i.e. if the preconditions are not met---; or, the union of the effects of
the action application and the state. [Abdulaziz et al., Definition 3, p.9]
›
definition prob_dom where
"prob_dom prob ≡ ⋃ ((λ (s1, s2). action_dom s1 s2) ` prob)"
definition valid_states where
"valid_states prob ≡ {s. fmdom' s = prob_dom prob}"
definition valid_plans where
"valid_plans prob ≡ {as. set as ⊆ prob}"
definition state_succ where
"state_succ s a ≡ (if fst a ⊆⇩f s then (snd a ++ s) else s)"
end