Theory "invariantsPlusOne"

Parents     stateSpaceProduct

Signature

Constant Type
invariant :α state -> bool
invariant_states :(α -> bool) -> α state -> bool

Definitions

invariant_def
|- ∀fm.
     invariant fm ⇔
     ∀x. x ∈ FDOM fm ∧ fm ' x ⇒ ∀x'. x ≠ x' ∧ x' ∈ FDOM fm ⇒ ¬fm ' x'
invariant_states_def
|- ∀vs. invariant_states vs = {fm | (FDOM fm = vs) ∧ invariant fm}


Theorems

invariant_lemma_2_1
|- ∀fm fm' x x'.
     invariant fm ∧ invariant fm' ∧ (FDOM fm = FDOM fm') ∧ x ∈ FDOM fm ∧
     fm ≠ fm' ∧ fm ' x ⇒
     ¬fm' ' x
invariant_lemma_2_2
|- ∀fm x s.
     invariant fm ∧ (FDOM fm = x INSERT s) ∧ ¬fm ' x ⇒ invariant (fm \\ x)
invariant_lemma_2_3
|- ∀fm x s. invariant fm ∧ (FDOM fm = s) ∧ x ∉ s ⇒ invariant (fm |+ (x,F))
invariant_lemma_2
|- ∀fm'' e vs.
     vs ≠ ∅ ∧ e ∉ vs ∧ invariant fm'' ∧ (FDOM fm'' = e INSERT vs) ∧ fm'' ' e ⇒
     ({fm | (FDOM fm = e INSERT vs) ∧ invariant fm} =
      fm'' INSERT
      IMAGE (λfm'. fm' |+ (e,F)) {fm | (FDOM fm = vs) ∧ invariant fm})
invariant_lemma_1
|- ∀vs.
     FINITE vs ⇒
     ∀e. e ∉ vs ⇒ ∃fm. invariant fm ∧ (FDOM fm = e INSERT vs) ∧ fm ' e
invariant_lemma_3
|- ∃fm fm'. ({fm | (FDOM fm = {e}) ∧ invariant fm} = {fm} ∪ {fm'}) ∧ fm ≠ fm'
invariant_lemma
|- ∀vs. FINITE vs ⇒ (CARD (invariant_states vs) = CARD vs + 1)
invariant_prob_reachable_states_thm_1
|- ∀vs. FINITE vs ⇒ ∃s. (FDOM s = vs) ∧ invariant s
invariant_prob_reachable_states_thm_2
|- ∀vs1 vs2.
     FINITE vs1 ∧ FINITE vs2 ∧ (invariant_states vs1 = invariant_states vs2) ⇒
     (vs1 = vs2)
invariantStateSpace_thm_3_1_1
|- ∀s vs. invariant s ⇒ invariant (DRESTRICT s vs)
invariantStateSpace_thm_3_1
|- ∀vs.
     FINITE vs ⇒
     ∀s.
       FDOM s ⊆ vs ∧ invariant s ⇒
       ∃s'.
         (FDOM s' = vs) ∧ invariant s' ∧ (DRESTRICT s' (FDOM s) = s) ∧
         ∀x. x ∈ FDOM s' DIFF FDOM s ⇒ ¬s' ' x
invariantStateSpace_thm_13
|- ∀vs. FINITE vs ⇒ invariant_states vs ≠ ∅
invariantStateSpace_DRESTRICT_SUBSET_thm
|- ∀s vs1 vs2.
     invariant (DRESTRICT s vs1) ∧ vs2 ⊆ vs1 ⇒ invariant (DRESTRICT s vs2)
invariant_states_stateSpace_thm
|- ∀vs. stateSpace (invariant_states vs) vs
invariantStateSpace_thm_10_2
|- ∀vs1 vs2. ss_proj (invariant_states vs1) (vs1 ∪ vs2) = invariant_states vs1
invariantStateSpace_thm_10_3
|- ∀vs VS.
     (∀vs1 vs2. vs2 ∈ vs INSERT VS ∧ vs1 ∈ vs INSERT VS ⇒ DISJOINT vs1 vs2) ⇒
     ∀ss1 ss2.
       ss1 ∈ IMAGE invariant_states (vs INSERT VS) ∧
       ss2 ∈ IMAGE invariant_states (vs INSERT VS) ⇒
       ∃vs1 vs2.
         vs1 ∈ vs INSERT VS ∧ stateSpace ss1 vs1 ∧ vs2 ∈ vs INSERT VS ∧
         stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2
invariantStateSpace_thm_10
|- ∀VS.
     FINITE VS ⇒
     (∀vs. vs ∈ VS ⇒ FINITE vs) ∧
     (∀vs1 vs2. vs1 ∈ VS ∧ vs2 ∈ VS ∧ vs1 ≠ vs2 ⇒ DISJOINT vs1 vs2) ⇒
     ∀vs vs2.
       FINITE vs ∧ (∀vs1. vs1 ∈ VS ⇒ DISJOINT vs vs1) ⇒
       (ss_proj (PRODf (IMAGE invariant_states VS) (invariant_states vs))
          (vs2 ∪ vs ∪ BIGUNION VS) =
        PRODf (IMAGE invariant_states VS) (invariant_states vs))
invariantStateSpace_CARD
|- ∀VS.
     FINITE VS ⇒
     ∀vs.
       FINITE vs ∧ vs ∉ VS ∧ (∀vs'. vs' ∈ VS ⇒ FINITE vs') ⇒
       (Π CARD (invariant_states vs INSERT IMAGE invariant_states VS) =
        Π (λvs. CARD vs + 1) (vs INSERT VS))