Theory "acycSspace"

Parents     systemAbstraction   acyclicity

Signature

Constant Type
S :(α -> bool) -> (α |-> β) list -> ((α |-> β) # (α |-> β) -> bool) -> (α |-> β) -> num
sspace_DAG :((α |-> β) # (α |-> β) -> bool) -> (α |-> β) list -> bool
vars_change :((α |-> β) # (α |-> β)) list -> (α -> bool) -> (α |-> β) -> (α |-> β) list

Definitions

S_def
|- ∀vs lss PROB s.
     S vs lss PROB s =
     wlp (state_successors (prob_proj (PROB,vs)))
       (λs. problem_plan_bound (snapshot PROB s)) MAX (λx y. x + y + 1) s lss
vars_change_def
|- (∀a as vs s.
      vars_change (a::as) vs s =
      if DRESTRICT (state_succ s a) vs ≠ DRESTRICT s vs then
        state_succ s a::vars_change as vs (state_succ s a)
      else vars_change as vs (state_succ s a)) ∧
   ∀vs s. vars_change [] vs s = []
sspace_DAG_def
|- ∀PROB lss.
     sspace_DAG PROB lss ⇔
     (set lss = valid_states PROB) ∧
     top_sorted_abs (state_successors PROB) lss


Theorems

vars_change_cat
|- ∀s.
     vars_change (as1 ⧺ as2) vs s =
     vars_change as1 vs s ⧺ vars_change as2 vs (exec_plan (s,as1))
empty_change_no_change
|- ∀s.
     (vars_change as vs s = []) ⇒
     (DRESTRICT (exec_plan (s,as)) vs = DRESTRICT s vs)
zero_change_imp_all_effects_submap
|- ∀s s'.
     (vars_change as vs s = []) ∧ sat_precond_as (s,as) ∧ MEM a as ∧
     (DRESTRICT s vs = DRESTRICT s' vs) ⇒
     DRESTRICT (SND a) vs ⊑ DRESTRICT s' vs
zero_change_imp_all_preconds_submap
|- ∀s s'.
     (vars_change as vs s = []) ∧ sat_precond_as (s,as) ∧ MEM a as ∧
     (DRESTRICT s vs = DRESTRICT s' vs) ⇒
     DRESTRICT (FST a) vs ⊑ DRESTRICT s' vs
no_vs_change_valid_in_snapshot
|- as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ∧
   (vars_change as vs s = []) ⇒
   as ∈ valid_plans (snapshot PROB (DRESTRICT s vs))
no_vs_change_snapshot_s_vs_is_valid_bound_1_1_1
|- FINITE PROB ∧ (vars_change as vs s = []) ∧ sat_precond_as (s,as) ∧
   s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
   ∃as'.
     (exec_plan (DRESTRICT s (prob_dom (snapshot PROB (DRESTRICT s vs))),as) =
      exec_plan
        (DRESTRICT s (prob_dom (snapshot PROB (DRESTRICT s vs))),as')) ∧
     sublist as' as ∧
     LENGTH as' ≤ problem_plan_bound (snapshot PROB (DRESTRICT s vs))
no_vs_change_snapshot_s_vs_is_valid_bound_1_1
|- FINITE PROB ∧ (vars_change as vs s = []) ∧ sat_precond_as (s,as) ∧
   s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
   ∃as'.
     (exec_plan (DRESTRICT s (prob_dom (snapshot PROB (DRESTRICT s vs))),as) =
      exec_plan
        (DRESTRICT s (prob_dom (snapshot PROB (DRESTRICT s vs))),as')) ∧
     sublist as' as ∧ sat_precond_as (s,as') ∧
     LENGTH as' ≤ problem_plan_bound (snapshot PROB (DRESTRICT s vs))
no_vs_change_snapshot_s_vs_is_valid_bound_1
|- FINITE PROB ∧ (vars_change as vs s = []) ∧ no_effectless_act as ∧
   sat_precond_as (s,as) ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
   ∃as'.
     (DRESTRICT (exec_plan (s,as))
        (prob_dom (snapshot PROB (DRESTRICT s vs))) =
      DRESTRICT (exec_plan (s,as'))
        (prob_dom (snapshot PROB (DRESTRICT s vs)))) ∧ sublist as' as ∧
     LENGTH as' ≤ problem_plan_bound (snapshot PROB (DRESTRICT s vs))
no_vs_change_snapshot_s_vs_is_valid_bound
|- FINITE PROB ∧ (vars_change as vs s = []) ∧ no_effectless_act as ∧
   sat_precond_as (s,as) ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
   ∃as'.
     (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
     LENGTH as' ≤ problem_plan_bound (snapshot PROB (DRESTRICT s vs))
snapshot_bound_leq_S
|- problem_plan_bound (snapshot PROB (DRESTRICT s vs)) ≤
   S vs lss PROB (DRESTRICT s vs)
S_geq_S_succ_plus_ell
|- s ∈ valid_states PROB ∧
   top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧
   s' ∈ state_successors (prob_proj (PROB,vs)) s ∧
   (set lss = valid_states (prob_proj (PROB,vs))) ⇒
   problem_plan_bound (snapshot PROB (DRESTRICT s vs)) +
   S vs lss PROB (DRESTRICT s' vs) + 1 ≤ S vs lss PROB (DRESTRICT s vs)
vars_change_cons
|- ∀s s'.
     (vars_change as vs s = s'::ss) ⇒
     ∃as1 act as2.
       (as = as1 ⧺ act::as2) ∧ (vars_change as1 vs s = []) ∧
       (state_succ (exec_plan (s,as1)) act = s') ∧
       (vars_change as2 vs (state_succ (exec_plan (s,as1)) act) = ss)
vars_change_cons_2
|- ∀s s'. (vars_change as vs s = s'::ss) ⇒ DRESTRICT s' vs ≠ DRESTRICT s vs
S_bound_main_lemma_1_1_1
|- top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧ FINITE PROB ∧
   (set lss = valid_states (prob_proj (PROB,vs))) ∧ s ∈ valid_states PROB ∧
   as ∈ valid_plans PROB ∧ no_effectless_act as ∧ sat_precond_as (s,as) ⇒
   ∃as'.
     (exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as ∧
     LENGTH as' ≤ S vs lss PROB (DRESTRICT s vs)
S_bound_main_lemma_1_1
|- top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧ FINITE PROB ∧
   (set lss = valid_states (prob_proj (PROB,vs))) ∧ s ∈ valid_states PROB ∧
   as ∈ valid_plans PROB ⇒
   ∃as'.
     (exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as ∧
     LENGTH as' ≤ S vs lss PROB (DRESTRICT s vs)
S_bound_main_lemma_1
|- top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧ FINITE PROB ∧
   (set lss = valid_states (prob_proj (PROB,vs))) ∧ s ∈ valid_states PROB ∧
   as ∈ valid_plans PROB ⇒
   ∃as'.
     (exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as ∧
     LENGTH as' ≤
     MAX_SET {S vs lss PROB s' | s' | s' ∈ valid_states (prob_proj (PROB,vs))}
S_bound_main_lemma
|- top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧ FINITE PROB ∧
   (set lss = valid_states (prob_proj (PROB,vs))) ⇒
   problem_plan_bound PROB ≤
   MAX_SET {S vs lss PROB s' | s' | s' ∈ valid_states (prob_proj (PROB,vs))}
S_bound_main_lemma_1_1_thesis
|- FINITE PROB ∧ sspace_DAG (prob_proj (PROB,vs)) lss ∧
   s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
   ∃as'.
     (exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as ∧
     LENGTH as' ≤ S vs lss PROB (DRESTRICT s vs)
S_bound_main_lemma_thesis
|- FINITE PROB ∧ sspace_DAG (prob_proj (PROB,vs)) lss ⇒
   problem_plan_bound PROB ≤
   MAX_SET {S vs lss PROB s' | s' | s' ∈ valid_states (prob_proj (PROB,vs))}