Theory "factoredSystem"

Parents     sublist   set_utils   fmap_utils   HO_arith_utils

Signature

Constant Type
action_dom :(α |-> β) # (α |-> γ) -> α -> bool
action_needed_asses :(α |-> β) # γ -> (α |-> β) -> (α |-> β)
action_needed_vars :(α |-> β) # γ -> (α |-> β) -> α -> bool
exec_plan :(α |-> β) # ((α |-> β) # (α |-> β)) list -> (α |-> β)
prob_dom :((α |-> β) # (α |-> γ) -> bool) -> α -> bool
reachable_s :((α |-> β) # (α |-> β) -> bool) -> (α |-> β) -> (α |-> β) -> bool
stateSpace :((α |-> β) -> bool) -> (α -> bool) -> bool
state_list :(α |-> β) # ((α |-> β) # (α |-> β)) list -> (α |-> β) list
state_set :α list -> α list -> bool
state_succ :(α |-> β) -> (α |-> β) # (α |-> β) -> (α |-> β)
state_successors :((α |-> β) # (α |-> β) -> bool) -> (α |-> β) -> (α |-> β) -> bool
system_needed_asses :((α |-> β) # γ -> bool) -> (α |-> β) -> (α |-> β)
system_needed_vars :((α |-> β) # γ -> bool) -> (α |-> β) -> α -> bool
valid_plans :(α -> bool) -> α list -> bool
valid_states :((α |-> γ) # (α |-> δ) -> bool) -> (α |-> β) -> bool

Definitions

action_dom_def
|- ∀s1 s2. action_dom (s1,s2) = FDOM s1 ∪ FDOM s2
prob_dom_def
|- ∀PROB. prob_dom PROB = BIGUNION (IMAGE action_dom PROB)
valid_states_def
|- ∀PROB. valid_states PROB = {s | FDOM s = prob_dom PROB}
valid_plans_def
|- ∀PROB. valid_plans PROB = {as | set as ⊆ PROB}
state_succ_def
|- ∀s a. state_succ s a = if FST a ⊑ s then SND a ⊌ s else s
exec_plan_primitive_def
|- exec_plan =
   WFREC (@R. WF R ∧ ∀as a s. R (state_succ s a,as) (s,a::as))
     (λexec_plan a'.
        case a' of
          (s,[]) => I s
        | (s,a::as) => I (exec_plan (state_succ s a,as)))
state_list_primitive_def
|- state_list =
   WFREC (@R. WF R ∧ ∀as a s. R (state_succ s a,as) (s,a::as))
     (λstate_list a'.
        case a' of
          (s,[]) => I [s]
        | (s,a::as) => I (s::state_list (state_succ s a,as)))
state_set_def
|- (∀s ss. state_set (s::ss) = [s] INSERT IMAGE (CONS s) (state_set ss)) ∧
   (state_set [] = ∅)
reachable_s_def
|- ∀PROB s. reachable_s PROB s = {exec_plan (s,as) | as ∈ valid_plans PROB}
state_successors_def
|- ∀PROB s. state_successors PROB s = IMAGE (state_succ s) PROB DIFF {s}
stateSpace_def
|- ∀ss vs. stateSpace ss vs ⇔ ∀s. s ∈ ss ⇒ (FDOM s = vs)
action_needed_vars_def
|- ∀a s.
     action_needed_vars a s =
     {v | v ∈ FDOM s ∧ v ∈ FDOM (FST a) ∧ (FST a ' v = s ' v)}
action_needed_asses_def
|- ∀a s. action_needed_asses a s = DRESTRICT s (action_needed_vars a s)
system_needed_vars_def
|- ∀PROB s.
     system_needed_vars PROB s = BIGUNION {action_needed_vars a s | a ∈ PROB}
system_needed_asses_def
|- ∀PROB s.
     system_needed_asses PROB s = DRESTRICT s (system_needed_vars PROB s)


Theorems

graph_plan_lemma_22_4_1
|- as ∈ valid_plans PROB ⇒ FILTER P as ∈ valid_plans PROB
graph_plan_lemma_10_2
|- ∀a. a ∈ PROB ⇒ action_dom a ⊆ prob_dom PROB
graph_plan_lemma_16_1_1
|- ∀s a. (FDOM (SND a) = ∅) ⇒ (state_succ s a = s)
graph_plan_lemma_4_1
|- ∀s s' vs a a'.
     (DRESTRICT s vs = DRESTRICT s' vs) ∧ (FST a ⊑ s ⇔ FST a' ⊑ s') ∧
     (DRESTRICT (SND a) vs = DRESTRICT (SND a') vs) ⇒
     (DRESTRICT (state_succ s a) vs = DRESTRICT (state_succ s' a') vs)
graph_plan_lemma_12_3
|- ∀s a vs.
     (FDOM (DRESTRICT (SND a) vs) = ∅) ⇒
     (DRESTRICT (state_succ s a) vs = DRESTRICT s vs)
no_change_vs_eff_submap
|- ∀a vs s.
     (DRESTRICT s vs = DRESTRICT (state_succ s a) vs) ∧ FST a ⊑ s ⇒
     DRESTRICT (SND a) vs ⊑ DRESTRICT s vs
graph_plan_lemma_1_2
|- ∀a vs s.
     DISJOINT (FDOM (SND a)) vs ⇒
     (DRESTRICT s vs = DRESTRICT (state_succ s a) vs)
empty_prob_dom_finite
|- (prob_dom PROB = ∅) ⇒ FINITE PROB
empty_prob_dom
|- (prob_dom PROB = ∅) ⇒ (PROB = {(FEMPTY,FEMPTY)}) ∨ (PROB = ∅)
empty_prob_dom_imp_empty_plan_always_good
|- ∀PROB s.
     (prob_dom PROB = ∅) ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     (exec_plan (s,[]) = exec_plan (s,as))
empty_prob_dom_single_val_state
|- (prob_dom PROB = ∅) ⇒ ∃s. valid_states PROB = {s}
valid_states_nempty
|- FINITE PROB ⇒ ∃s. s ∈ valid_states PROB
valid_plan_mems
|- as ∈ valid_plans PROB ∧ MEM a as ⇒ a ∈ PROB
valid_as_submap_init_submap_exec
|- ∀s1 s2.
     s1 ⊑ s2 ∧ (∀a. MEM a as ⇒ FDOM (FST a) ⊆ FDOM s1) ⇒
     exec_plan (s1,as) ⊑ exec_plan (s2,as)
pred_dom_subset_succ_submap
|- ∀a s1 s2.
     FDOM (FST a) ⊆ FDOM s1 ∧ s1 ⊑ s2 ⇒ state_succ s1 a ⊑ state_succ s2 a
parent_children_lemma_1_1_1_10_1_1
|- ∀a s1 s2. FST a ⊑ s1 ∧ s1 ⊑ s2 ⇒ state_succ s1 a ⊑ state_succ s2 a
action_dom_pair
|- action_dom a = FDOM (FST a) ∪ FDOM (SND a)
state_succ_pair
|- state_succ s (p,e) = if p ⊑ s then e ⊌ s else s
exec_plan_ind
|- ∀P.
     (∀s a as. P (state_succ s a,as) ⇒ P (s,a::as)) ∧ (∀s. P (s,[])) ⇒
     ∀v v1. P (v,v1)
exec_plan_def
|- (∀s as a. exec_plan (s,a::as) = exec_plan (state_succ s a,as)) ∧
   ∀s. exec_plan (s,[]) = s
exec_plan_Append
|- ∀as_a as_b s.
     exec_plan (s,as_a ⧺ as_b) = exec_plan (exec_plan (s,as_a),as_b)
cycle_removal_lemma
|- ∀s as1 as2 as3.
     (exec_plan (s,as1 ⧺ as2) = exec_plan (s,as1)) ⇒
     (exec_plan (s,as1 ⧺ as2 ⧺ as3) = exec_plan (s,as1 ⧺ as3))
construction_of_all_possible_states_lemma
|- ∀e X.
     e ∉ X ⇒
     ({s | FDOM s = e INSERT X} =
      IMAGE (λs. s |+ (e,T)) {s | FDOM s = X} ∪
      IMAGE (λs. s |+ (e,F)) {s | FDOM s = X})
FINITE_states
|- ∀X. FINITE X ⇒ FINITE {s | FDOM s = X}
card_of_set_of_all_possible_states
|- ∀X. FINITE X ⇒ (CARD {s | FDOM s = X} = 2 ** CARD X)
state_list_ind
|- ∀P.
     (∀s a as. P (state_succ s a,as) ⇒ P (s,a::as)) ∧ (∀s. P (s,[])) ⇒
     ∀v v1. P (v,v1)
state_list_def
|- (∀s as a. state_list (s,a::as) = s::state_list (state_succ s a,as)) ∧
   ∀s. state_list (s,[]) = [s]
empty_state_list_lemma
|- ∀as s. [] ≠ state_list (s,as)
state_list_length_non_zero
|- ∀as s. 0 ≠ LENGTH (state_list (s,as))
state_list_length_lemma
|- ∀as s. LENGTH as = LENGTH (state_list (s,as)) − 1
state_list_length_lemma_2
|- ∀as s. LENGTH (state_list (s,as)) = LENGTH as + 1
state_set_thm
|- ∀s1. s1 ∈ state_set s2 ⇔ s1 ≼ s2 ∧ s1 ≠ []
state_set_finite
|- ∀X. FINITE (state_set X)
LENGTH_state_set
|- ∀X e. e ∈ state_set X ⇒ LENGTH e ≤ LENGTH X
lemma_temp
|- ∀x s as h.
     x ∈ state_set (state_list (s,as)) ⇒
     LENGTH (h::state_list (s,as)) > LENGTH x
NIL_NOTIN_stateset
|- ∀X. [] ∉ state_set X
state_set_card
|- ∀X. CARD (state_set X) = LENGTH X
FDOM_state_succ
|- FDOM (SND a) ⊆ FDOM s ⇒ (FDOM (state_succ s a) = FDOM s)
FDOM_state_succ_subset
|- FDOM (state_succ s a) ⊆ FDOM s ∪ FDOM (SND a)
FDOM_eff_subset_FDOM_valid_states
|- ∀p e s. (p,e) ∈ PROB ∧ s ∈ valid_states PROB ⇒ FDOM e ⊆ FDOM s
FDOM_eff_subset_FDOM_valid_states_pair
|- ∀a s. a ∈ PROB ∧ s ∈ valid_states PROB ⇒ FDOM (SND a) ⊆ FDOM s
FDOM_pre_subset_FDOM_valid_states
|- ∀p e s. (p,e) ∈ PROB ∧ s ∈ valid_states PROB ⇒ FDOM p ⊆ FDOM s
FDOM_pre_subset_FDOM_valid_states_pair
|- ∀a s. a ∈ PROB ∧ s ∈ valid_states PROB ⇒ FDOM (FST a) ⊆ FDOM s
action_dom_subset_valid_states_FDOM
|- ∀p e s. (p,e) ∈ PROB ∧ s ∈ valid_states PROB ⇒ action_dom (p,e) ⊆ FDOM s
FDOM_eff_subset_prob_dom
|- ∀p e. (p,e) ∈ PROB ⇒ FDOM e ⊆ prob_dom PROB
FDOM_eff_subset_prob_dom_pair
|- ∀a. a ∈ PROB ⇒ FDOM (SND a) ⊆ prob_dom PROB
FDOM_pre_subset_prob_dom
|- ∀p e. (p,e) ∈ PROB ⇒ FDOM p ⊆ prob_dom PROB
FDOM_pre_subset_prob_dom_pair
|- ∀a. a ∈ PROB ⇒ FDOM (FST a) ⊆ prob_dom PROB
valid_plan_valid_head
|- h::as ∈ valid_plans PROB ⇒ h ∈ PROB
valid_plan_valid_tail
|- h::as ∈ valid_plans PROB ⇒ as ∈ valid_plans PROB
valid_plan_pre_subset_prob_dom_pair
|- as ∈ valid_plans PROB ⇒ ∀a. MEM a as ⇒ FDOM (FST a) ⊆ prob_dom PROB
valid_append_valid_suff
|- as1 ⧺ as2 ∈ valid_plans PROB ⇒ as2 ∈ valid_plans PROB
valid_append_valid_pref
|- as1 ⧺ as2 ∈ valid_plans PROB ⇒ as1 ∈ valid_plans PROB
valid_pref_suff_valid_append
|- as1 ∈ valid_plans PROB ∧ as2 ∈ valid_plans PROB ⇒
   as1 ⧺ as2 ∈ valid_plans PROB
MEM_statelist_FDOM
|- ∀PROB h as s0.
     s0 ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     MEM h (state_list (s0,as)) ⇒
     h ∈ valid_states PROB
lemma_1
|- ∀as PROB.
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     IMAGE LAST (state_set (state_list (s,as))) ⊆ valid_states PROB
lemma_2_1_1_1
|- ∀as x PROB.
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧ as ≠ [] ⇒
     x ∈ state_set (state_list (s,as)) ⇒
     LENGTH x ≤ SUC (LENGTH as)
lemma_2_1_1
|- ∀as s h.
     CARD (state_set (state_list (s,h::as))) =
     SUC (CARD (state_set (state_list (state_succ s h,as))))
lemma_2_1
|- ∀as s. SUC (LENGTH as) = CARD (state_set (state_list (s,as)))
lemma_2_2_1
|- ∀as x y s.
     x ∈ state_set (state_list (s,as)) ∧ y ∈ state_set (state_list (s,as)) ∧
     x ≠ y ⇒
     LENGTH x ≠ LENGTH y
lemma_2_2
|- ∀as PROB s.
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     ¬INJ LAST (state_set (state_list (s,as))) (valid_states PROB) ⇒
     ∃slist_1 slist_2.
       slist_1 ∈ state_set (state_list (s,as)) ∧
       slist_2 ∈ state_set (state_list (s,as)) ∧
       (LAST slist_1 = LAST slist_2) ∧ LENGTH slist_1 ≠ LENGTH slist_2
lemma_2_3_1_1
|- ∀sl. [] ∉ state_set sl
lemma_2_3_1_2_1
|- ∀sl. sl ≠ [] ⇒ sl ∈ state_set sl
lemma_2_3_1_2
|- ∀s slist h t.
     slist ≠ [] ∧ s::slist ∈ state_set (state_list (s,h::t)) ⇒
     slist ∈ state_set (state_list (state_succ s h,t))
valid_action_valid_succ
|- h ∈ PROB ∧ s ∈ valid_states PROB ⇒ state_succ s h ∈ valid_states PROB
lemma_2_3_1_thm
|- ∀slist as PROB s.
     as ≠ [] ∧ slist ≠ [] ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     slist ∈ state_set (state_list (s,as)) ⇒
     ∃as'.
       as' ≼ as ∧ (exec_plan (s,as') = LAST slist) ∧
       (LENGTH slist = SUC (LENGTH as'))
FINITE_prob_dom
|- FINITE PROB ⇒ FINITE (prob_dom PROB)
CARD_valid_states
|- FINITE PROB ⇒ (CARD (valid_states PROB) = 2 ** CARD (prob_dom PROB))
FINITE_valid_states
|- FINITE PROB ⇒ FINITE (valid_states PROB)
lemma_2
|- ∀PROB as s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     LENGTH as > 2 ** CARD (FDOM s) − 1 ⇒
     ∃as1 as2 as3.
       (as1 ⧺ as2 ⧺ as3 = as) ∧
       (exec_plan (s,as1 ⧺ as2) = exec_plan (s,as1)) ∧ as2 ≠ []
lemma_2_prob_dom
|- ∀PROB as s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     LENGTH as > 2 ** CARD (prob_dom PROB) − 1 ⇒
     ∃as1 as2 as3.
       (as1 ⧺ as2 ⧺ as3 = as) ∧
       (exec_plan (s,as1 ⧺ as2) = exec_plan (s,as1)) ∧ as2 ≠ []
lemma_3
|- ∀as PROB s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     LENGTH as > 2 ** CARD (prob_dom PROB) − 1 ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ LENGTH as' < LENGTH as ∧
       sublist as' as
sublist_valid_is_valid
|- ∀as' as PROB.
     as ∈ valid_plans PROB ∧ sublist as' as ⇒ as' ∈ valid_plans PROB
main_lemma
|- ∀PROB as s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
       LENGTH as' ≤ 2 ** CARD (prob_dom PROB) − 1
graph_plan_lemma_6_1
|- ∀as s PROB.
     as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
     exec_plan (s,as) ∈ valid_states PROB
exec_plan_fdom_subset
|- ∀as s PROB.
     as ∈ valid_plans PROB ⇒ FDOM (exec_plan (s,as)) ⊆ FDOM s ∪ prob_dom PROB
reachable_s_finite_thm_1
|- s ∈ valid_states PROB ⇒ reachable_s PROB s ⊆ valid_states PROB
reachable_s_finite_thm
|- ∀s. FINITE PROB ∧ s ∈ valid_states PROB ⇒ FINITE (reachable_s PROB s)
empty_plan_is_valid
|- [] ∈ valid_plans PROB
valid_head_and_tail_valid_plan
|- h ∈ PROB ∧ as ∈ valid_plans PROB ⇒ h::as ∈ valid_plans PROB
lemma_1_reachability_s
|- ∀PROB s as.
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     IMAGE LAST (state_set (state_list (s,as))) ⊆ reachable_s PROB s
lemma_2_2_reachability_s
|- ∀as PROB s.
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     ¬INJ LAST (state_set (state_list (s,as))) (reachable_s PROB s) ⇒
     ∃slist_1 slist_2.
       slist_1 ∈ state_set (state_list (s,as)) ∧
       slist_2 ∈ state_set (state_list (s,as)) ∧
       (LAST slist_1 = LAST slist_2) ∧ LENGTH slist_1 ≠ LENGTH slist_2
lemma_2_reachability_s
|- ∀PROB as s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     LENGTH as > CARD (reachable_s PROB s) − 1 ⇒
     ∃as1 as2 as3.
       (as1 ⧺ as2 ⧺ as3 = as) ∧
       (exec_plan (s,as1 ⧺ as2) = exec_plan (s,as1)) ∧ as2 ≠ []
lemma_3_reachability_s
|- ∀as PROB s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     LENGTH as > CARD (reachable_s PROB s) − 1 ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ LENGTH as' < LENGTH as ∧
       sublist as' as
main_lemma_reachability_s
|- ∀PROB as s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
       LENGTH as' ≤ CARD (reachable_s PROB s) − 1
reachable_s_non_empty
|- reachable_s PROB s ≠ ∅
card_reachable_s_non_zero
|- ∀s. FINITE PROB ∧ s ∈ valid_states PROB ⇒ 0 < CARD (reachable_s PROB s)
exec_fdom_empty_prob
|- ∀s.
     (prob_dom PROB = ∅) ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     (exec_plan (s,as) = FEMPTY)
reachable_s_empty_prob
|- ∀PROB s.
     (prob_dom PROB = ∅) ∧ s ∈ valid_states PROB ⇒
     reachable_s PROB s ⊆ {FEMPTY}
sublist_valid_plan
|- sublist as' as ∧ as ∈ valid_plans PROB ⇒ as' ∈ valid_plans PROB
prob_subset_dom_subset
|- PROB1 ⊆ PROB2 ⇒ prob_dom PROB1 ⊆ prob_dom PROB2
state_succ_valid_act_disjoint
|- a ∈ PROB ∧ DISJOINT vs (prob_dom PROB) ⇒
   (DRESTRICT (state_succ s a) vs = DRESTRICT s vs)
exec_valid_as_disjoint
|- ∀s.
     DISJOINT vs (prob_dom PROB) ∧ as ∈ valid_plans PROB ⇒
     (DRESTRICT (exec_plan (s,as)) vs = DRESTRICT s vs)
EQ_SS_DOM
|- ss ≠ ∅ ∧ stateSpace ss vs1 ∧ stateSpace ss vs2 ⇒ (vs1 = vs2)
FINITE_SS
|- ∀ss. ss ≠ ∅ ∧ stateSpace ss dom ⇒ FINITE ss
disjoint_effects_no_effects
|- ∀s.
     (∀a. MEM a as ⇒ (FDOM (DRESTRICT (SND a) vs) = ∅)) ⇒
     (DRESTRICT (exec_plan (s,as)) vs = DRESTRICT s vs)
act_needed_asses_submap_succ_submap
|- ∀a s1 s2.
     action_needed_asses a s2 ⊑ action_needed_asses a s1 ∧ s1 ⊑ s2 ⇒
     state_succ s1 a ⊑ state_succ s2 a
as_needed_asses_submap_exec
|- ∀s1 s2.
     s1 ⊑ s2 ∧
     (∀a. MEM a as ⇒ action_needed_asses a s2 ⊑ action_needed_asses a s1) ⇒
     exec_plan (s1,as) ⊑ exec_plan (s2,as)
action_needed_vars_subset_sys_needed_vars_subset
|- a ∈ PROB ⇒ action_needed_vars a s ⊆ system_needed_vars PROB s
action_needed_asses_submap_sys_needed_asses
|- a ∈ PROB ⇒ action_needed_asses a s ⊑ system_needed_asses PROB s
system_needed_asses_include_action_needed_asses_1
|- a ∈ PROB ⇒
   (action_needed_vars a (DRESTRICT s (system_needed_vars PROB s)) =
    action_needed_vars a s)
system_needed_asses_include_action_needed_asses
|- a ∈ PROB ⇒
   (action_needed_asses a (system_needed_asses PROB s) =
    action_needed_asses a s)
system_needed_asses_submap
|- system_needed_asses PROB s ⊑ s
as_works_from_system_needed_asses
|- as ∈ valid_plans PROB ⇒
   exec_plan (system_needed_asses PROB s,as) ⊑ exec_plan (s,as)