Theory "stateSpaceProduct"

Parents     systemAbstraction

Signature

Constant Type
PROD :(((α |-> β) -> bool) -> bool) -> ((α |-> β) -> bool) -> ((α |-> β) -> bool) -> bool
PRODf :(((α |-> β) -> bool) -> bool) -> ((α |-> β) -> bool) -> (α |-> β) -> bool
stateSpaceProduct :((α |-> β) -> bool) -> ((α |-> β) -> bool) -> (α |-> β) -> bool

Definitions

stateSpaceProduct_def
|- ∀ss1 ss2. stateSpaceProduct ss1 ss2 = IMAGE (λ(s1,s2). s1 ⊌ s2) (ss1 × ss2)
PROD_def
|- PROD =
   (λa0 a1 a2.
      ∀PROD'.
        (∀a0 a1 a2.
           (a0 = ∅) ∧ (a2 = a1) ∨
           (∃ss SS ss''.
              (a0 = ss INSERT SS) ∧ (a2 = stateSpaceProduct ss ss'') ∧
              ss ∉ SS ∧ PROD' SS a1 ss'') ⇒
           PROD' a0 a1 a2) ⇒
        PROD' a0 a1 a2)
PRODf_def
|- ∀s. FINITE s ⇒ ∀a. PROD s a (PRODf s a)


Theorems

stateSpaceProduct_comm_thm
|- ∀ss1 ss2 vs1 vs2.
     stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2 ⇒
     (stateSpaceProduct ss1 ss2 = stateSpaceProduct ss2 ss1)
stateSpaceProduct_assoc_thm
|- ∀ss1 ss2 ss3.
     stateSpaceProduct ss1 (stateSpaceProduct ss2 ss3) =
     stateSpaceProduct (stateSpaceProduct ss1 ss2) ss3
stateSpaceProduct_left_comm_thm
|- ∀ss1 ss2 ss3 vs1 vs2 vs3.
     stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ stateSpace ss3 vs3 ∧
     DISJOINT vs1 vs2 ∧ DISJOINT vs1 vs3 ⇒
     (stateSpaceProduct ss1 (stateSpaceProduct ss2 ss3) =
      stateSpaceProduct ss2 (stateSpaceProduct ss1 ss3))
invariantStateSpace_thm_7
|- ∀ss dom vs1 vs2.
     stateSpace ss dom ∧ dom ⊆ vs1 ∪ vs2 ⇒
     ss ⊆ stateSpaceProduct (ss_proj ss vs1) (ss_proj ss vs2)
invariantStateSpace_thm_8
|- ∀ss1 ss2 ss3 ss4.
     ss1 ⊆ ss3 ∧ ss2 ⊆ ss4 ⇒
     stateSpaceProduct ss1 ss2 ⊆ stateSpaceProduct ss3 ss4
invariantStateSpace_thm_10_1
|- ∀ss1 ss2 vs.
     stateSpaceProduct (ss_proj ss1 vs) (ss_proj ss2 vs) =
     ss_proj (stateSpaceProduct ss1 ss2) vs
invariantStateSpace_thm_11
|- ∀ss1 ss2 vs.
     stateSpaceProduct (ss_proj ss1 vs) (ss_proj ss2 vs) ⊆
     ss_proj (stateSpaceProduct ss1 ss2) vs
PROD_rules
|- (∀ss. PROD ∅ ss ss) ∧
   ∀ss SS ss' ss''.
     ss ∉ SS ∧ PROD SS ss' ss'' ⇒
     PROD (ss INSERT SS) ss' (stateSpaceProduct ss ss'')
PROD_ind
|- ∀PROD'.
     (∀ss. PROD' ∅ ss ss) ∧
     (∀ss SS ss' ss''.
        ss ∉ SS ∧ PROD' SS ss' ss'' ⇒
        PROD' (ss INSERT SS) ss' (stateSpaceProduct ss ss'')) ⇒
     ∀a0 a1 a2. PROD a0 a1 a2 ⇒ PROD' a0 a1 a2
PROD_strongind
|- ∀PROD'.
     (∀ss. PROD' ∅ ss ss) ∧
     (∀ss SS ss' ss''.
        ss ∉ SS ∧ PROD SS ss' ss'' ∧ PROD' SS ss' ss'' ⇒
        PROD' (ss INSERT SS) ss' (stateSpaceProduct ss ss'')) ⇒
     ∀a0 a1 a2. PROD a0 a1 a2 ⇒ PROD' a0 a1 a2
PROD_cases
|- ∀a0 a1 a2.
     PROD a0 a1 a2 ⇔
     (a0 = ∅) ∧ (a2 = a1) ∨
     ∃ss SS ss''.
       (a0 = ss INSERT SS) ∧ (a2 = stateSpaceProduct ss ss'') ∧ ss ∉ SS ∧
       PROD SS a1 ss''
PROD_empty
|- PROD ∅ a b ⇔ (a = b)
FINITE_PROD_result
|- ∀s. FINITE s ⇒ ∀a. ∃b. PROD s a b
PROD_FINITE
|- ∀s a b. PROD s a b ⇒ FINITE s
IN_INSERT_EXISTS
|- x ∈ s ⇔ ∃s0. (s = x INSERT s0) ∧ x ∉ s0
PROD_det
|- ∀s a b.
     PROD s a b ⇒
     (∀ss1 ss2.
        ss1 ∈ s ∧ ss2 ∈ s ∧ ss1 ≠ ss2 ⇒
        ∃vs1 vs2.
          stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2) ∧
     (∀ss. ss ∈ s ⇒ ∃vs. stateSpace ss vs) ⇒
     ∀c. PROD s a c ⇒ (b = c)
PRODf_EMPTY
|- PRODf ∅ a = a
PRODf_INSERT
|- ∀e s.
     FINITE s ∧ e ∉ s ∧ e ≠ ∅ ∧
     (∀ss1 ss2.
        ss1 ∈ s ∧ ss2 ∈ s ∧ ss1 ≠ ss2 ⇒
        ∃vs1 vs2.
          stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2) ∧
     (∀ss. ss ∈ s ⇒ ss ≠ ∅) ∧ (∃vse. stateSpace e vse) ∧
     (∀ss.
        ss ∈ s ⇒
        ∃vse vs. stateSpace e vse ∧ stateSpace ss vs ∧ DISJOINT vse vs) ⇒
     ∀a. PRODf (e INSERT s) a = stateSpaceProduct e (PRODf s a)
FINITE_stateSpaceProduct
|- ∀ss1 ss2. FINITE ss1 ∧ FINITE ss2 ⇒ FINITE (stateSpaceProduct ss1 ss2)
PRODf_FINITE
|- ∀s.
     FINITE s ⇒
     ∀e.
       e ∉ s ∧ e ≠ ∅ ∧ (∃vse. stateSpace e vse) ∧ (∀ss. ss ∈ s ⇒ ss ≠ ∅) ∧
       (∀ss1 ss2.
          ss1 ∈ s ∧ ss2 ∈ s ∧ ss1 ≠ ss2 ⇒
          ∃vs1 vs2.
            stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2) ∧
       (∀ss.
          ss ∈ s ⇒
          ∃vse vs. stateSpace e vse ∧ stateSpace ss vs ∧ DISJOINT vse vs) ∧
       FINITE e ∧ (∀ss. ss ∈ s ⇒ FINITE ss) ⇒
       FINITE (PRODf s e)
PRODf_FINITE'
|- ∀s e.
     FINITE s ∧ e ∉ s ∧ e ≠ ∅ ∧ (∃vse. stateSpace e vse) ∧
     (∀ss. ss ∈ s ⇒ ss ≠ ∅) ∧
     (∀ss1 ss2.
        ss1 ∈ s ∧ ss2 ∈ s ∧ ss1 ≠ ss2 ⇒
        ∃vs1 vs2.
          stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2) ∧
     (∀ss.
        ss ∈ s ⇒
        ∃vse vs. stateSpace e vse ∧ stateSpace ss vs ∧ DISJOINT vse vs) ∧
     FINITE e ∧ (∀ss. ss ∈ s ⇒ FINITE ss) ⇒
     FINITE (PRODf s e)
stateSpaceProduct_CARD
|- ∀ss1 ss2.
     FINITE ss1 ∧ FINITE ss2 ⇒
     CARD (stateSpaceProduct ss1 ss2) ≤ CARD ss1 * CARD ss2
PRODf_CARD
|- ∀s.
     FINITE s ⇒
     ∀e.
       e ∉ s ∧ e ≠ ∅ ∧ (∃vse. stateSpace e vse) ∧ (∀ss. ss ∈ s ⇒ ss ≠ ∅) ∧
       (∀ss1 ss2.
          ss1 ∈ s ∧ ss2 ∈ s ∧ ss1 ≠ ss2 ⇒
          ∃vs1 vs2.
            stateSpace ss1 vs1 ∧ stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2) ∧
       (∀ss.
          ss ∈ s ⇒
          ∃vse vs. stateSpace e vse ∧ stateSpace ss vs ∧ DISJOINT vse vs) ∧
       FINITE e ∧ (∀ss. ss ∈ s ⇒ FINITE ss) ⇒
       CARD (PRODf s e) ≤ Π CARD (e INSERT s)