Theory FactoredSystemLib

theory FactoredSystemLib
  imports Main "HOL-Library.Finite_Map"

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.
       (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].

― ‹NOTE hide `\_add` to free the operator symbol `++` and redefine it to reflect HOL4 map 
addition semantics.›
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)"

― ‹NOTE lemma `action\_dom\_pair`

  action\_dom a = FDOM (FST a) Union ((SND a) ` FDOM)

was removed because the curried definition of `action\_dom` in the translation makes it redundant.›

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]

― ‹NOTE name shortened to 'prob\_dom'.›
― ‹NOTE lambda added to convert problem pairs to arguments of 'action\_dom'.›
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)"