Theory "actionSeqProcess"

Parents     factoredSystem

Signature

Constant Type
no_effectless_act :(α # (β |-> γ)) list -> bool
rem_condless_act :(α |-> β) # ((α |-> β) # (α |-> β)) list # ((α |-> β) # (α |-> β)) list -> ((α |-> β) # (α |-> β)) list
rem_effectless_act :(α # (β |-> γ)) list -> (α # (β |-> γ)) list
rem_effectless_act_set :(α # (β |-> γ) -> bool) -> α # (β |-> γ) -> bool
sat_precond_as :(α |-> β) # ((α |-> β) # (α |-> β)) list -> bool
varset_action :(α # (β |-> γ)) # (β -> bool) -> bool

Definitions

sat_precond_as_primitive_def
|- sat_precond_as =
   WFREC (@R. WF R ∧ ∀as a s. R (state_succ s a,as) (s,a::as))
     (λsat_precond_as a'.
        case a' of
          (s,[]) => I T
        | (s,a::as) => I (FST a ⊑ s ∧ sat_precond_as (state_succ s a,as)))
rem_effectless_act_def
|- (∀a as.
      rem_effectless_act (a::as) =
      if FDOM (SND a) ≠ ∅ then a::rem_effectless_act as
      else rem_effectless_act as) ∧ (rem_effectless_act [] = [])
no_effectless_act_def
|- (∀a as.
      no_effectless_act (a::as) ⇔ FDOM (SND a) ≠ ∅ ∧ no_effectless_act as) ∧
   (no_effectless_act [] ⇔ T)
rem_condless_act_primitive_def
|- rem_condless_act =
   WFREC
     (@R.
        WF R ∧
        (∀as pfx_a s a.
           ¬(FST a ⊑ exec_plan (s,pfx_a)) ⇒ R (s,pfx_a,as) (s,pfx_a,a::as)) ∧
        ∀as pfx_a s a.
          FST a ⊑ exec_plan (s,pfx_a) ⇒ R (s,pfx_a ⧺ [a],as) (s,pfx_a,a::as))
     (λrem_condless_act a'.
        case a' of
          (s,pfx_a,[]) => I pfx_a
        | (s,pfx_a,a::as) =>
            I
              (if FST a ⊑ exec_plan (s,pfx_a) then
                 rem_condless_act (s,pfx_a ⧺ [a],as)
               else rem_condless_act (s,pfx_a,as)))
varset_action_def
|- ∀a varset. varset_action (a,varset) ⇔ FDOM (SND a) ⊆ varset
rem_effectless_act_set_def
|- ∀A. rem_effectless_act_set A = {a | a ∈ A ∧ FDOM (SND a) ≠ ∅}


Theorems

sat_precond_as_ind
|- ∀P.
     (∀s a as. P (state_succ s a,as) ⇒ P (s,a::as)) ∧ (∀s. P (s,[])) ⇒
     ∀v v1. P (v,v1)
sat_precond_as_def
|- (∀s as a.
      sat_precond_as (s,a::as) ⇔
      FST a ⊑ s ∧ sat_precond_as (state_succ s a,as)) ∧
   ∀s. sat_precond_as (s,[]) ⇔ T
sat_precond_as_pair
|- (sat_precond_as (s,(p,e)::as) ⇔
    p ⊑ s ∧ sat_precond_as (state_succ s (p,e),as)) ∧
   (sat_precond_as (s,[]) ⇔ T)
graph_plan_lemma_4
|- ∀s s' as vs P.
     (∀a. MEM a as ∧ P a ⇒ DISJOINT (FDOM (SND a)) vs) ∧
     sat_precond_as (s,as) ∧ sat_precond_as (s',FILTER (λa. ¬P a) as) ∧
     (DRESTRICT s vs = DRESTRICT s' vs) ⇒
     (DRESTRICT (exec_plan (s,as)) vs =
      DRESTRICT (exec_plan (s',FILTER (λa. ¬P a) as)) vs)
rem_condless_act_ind
|- ∀P.
     (∀s pfx_a a as.
        (¬(FST a ⊑ exec_plan (s,pfx_a)) ⇒ P (s,pfx_a,as)) ∧
        (FST a ⊑ exec_plan (s,pfx_a) ⇒ P (s,pfx_a ⧺ [a],as)) ⇒
        P (s,pfx_a,a::as)) ∧ (∀s pfx_a. P (s,pfx_a,[])) ⇒
     ∀v v1 v2. P (v,v1,v2)
rem_condless_act_def
|- (∀s pfx_a as a.
      rem_condless_act (s,pfx_a,a::as) =
      if FST a ⊑ exec_plan (s,pfx_a) then rem_condless_act (s,pfx_a ⧺ [a],as)
      else rem_condless_act (s,pfx_a,as)) ∧
   ∀s pfx_a. rem_condless_act (s,pfx_a,[]) = pfx_a
rem_condless_act_pair
|- (rem_condless_act (s,pfx_a,(p,e)::as) =
    if p ⊑ exec_plan (s,pfx_a) then rem_condless_act (s,pfx_a ⧺ [(p,e)],as)
    else rem_condless_act (s,pfx_a,as)) ∧
   (rem_condless_act (s,pfx_a,[]) = pfx_a)
graph_plan_lemma_7_1_1
|- ∀s h as pfx.
     exec_plan (s,rem_condless_act (s,h::pfx,as)) =
     exec_plan (state_succ s h,rem_condless_act (state_succ s h,pfx,as))
graph_plan_lemma_7_1
|- ∀as s. exec_plan (s,as) = exec_plan (s,rem_condless_act (s,[],as))
graph_plan_lemma_7_2_1_1
|- ∀h' pfx as s.
     rem_condless_act (s,h'::pfx,as) =
     h'::rem_condless_act (state_succ s h',pfx,as)
graph_plan_lemma_7_2_1
|- ∀h h' as as' s.
     h'::as' ≼ rem_condless_act (s,[h],as) ⇒
     as' ≼ rem_condless_act (state_succ s h,[],as) ∧ (h' = h)
graph_plan_lemma_7_2
|- ∀as s. sat_precond_as (s,rem_condless_act (s,[],as))
graph_plan_lemma_7_3
|- ∀as s. LENGTH (rem_condless_act (s,[],as)) ≤ LENGTH as
graph_plan_lemma_7_4
|- ∀as A s. set as ⊆ A ⇒ set (rem_condless_act (s,[],as)) ⊆ A
graph_plan_lemma_7_6
|- ∀as s P.
     LENGTH (FILTER P (rem_condless_act (s,[],as))) ≤ LENGTH (FILTER P as)
graph_plan_lemma_7_7
|- ∀s P as as2.
     EVERY P as ∧ EVERY P as2 ⇒ EVERY P (rem_condless_act (s,as2,as))
graph_plan_lemma_7_8
|- ∀s as. sublist (rem_condless_act (s,[],as)) as
graph_plan_lemma_7_10
|- ∀PROB as.
     as ∈ valid_plans PROB ⇒ rem_condless_act (s,[],as) ∈ valid_plans PROB
graph_plan_lemma_7
|- ∀as A s.
     (exec_plan (s,as) = exec_plan (s,rem_condless_act (s,[],as))) ∧
     sat_precond_as (s,rem_condless_act (s,[],as)) ∧
     LENGTH (rem_condless_act (s,[],as)) ≤ LENGTH as ∧
     (set as ⊆ A ⇒ set (rem_condless_act (s,[],as)) ⊆ A) ∧
     ∀P. LENGTH (FILTER P (rem_condless_act (s,[],as))) ≤ LENGTH (FILTER P as)
parent_children_lemma_1_1_1_10_1
|- ∀s1 s2 as. s1 ⊑ s2 ∧ sat_precond_as (s1,as) ⇒ sat_precond_as (s2,as)
submap_init_submap_exec
|- ∀s1 s2.
     s1 ⊑ s2 ∧ sat_precond_as (s1,as) ⇒ exec_plan (s1,as) ⊑ exec_plan (s2,as)
parent_children_lemma_1_1_1_10
|- ∀vs s as. sat_precond_as (DRESTRICT s vs,as) ⇒ sat_precond_as (s,as)
varset_action_pair
|- varset_action ((p,e),vs) ⇔ FDOM e ⊆ vs
graph_plan_lemma_14_2
|- ∀x y.
     (SND x = SND y) ⇒
     ((λa. varset_action (a,vs)) x ⇔ (λa. varset_action (a,vs)) y)
graph_plan_lemma_16_1
|- ∀s as. exec_plan (s,as) = exec_plan (s,rem_effectless_act as)
graph_plan_lemma_16_2
|- ∀as s. sat_precond_as (s,as) ⇒ sat_precond_as (s,rem_effectless_act as)
graph_plan_lemma_16_3
|- ∀as. LENGTH (rem_effectless_act as) ≤ LENGTH as
graph_plan_lemma_16_4
|- ∀A as. set as ⊆ A ⇒ set (rem_effectless_act as) ⊆ A
graph_plan_lemma_16_4'
|- ∀A as. as ∈ valid_plans A ⇒ rem_effectless_act as ∈ valid_plans A
graph_plan_lemma_16_5
|- ∀P as. LENGTH (FILTER P (rem_effectless_act as)) ≤ LENGTH (FILTER P as)
graph_plan_lemma_16_6
|- ∀as. no_effectless_act (rem_effectless_act as)
graph_plan_lemma_16_7
|- ∀as. no_effectless_act as ⇔ EVERY (λa. FDOM (SND a) ≠ ∅) as
graph_plan_lemma_16_8
|- ∀P as. EVERY P as ⇒ EVERY P (rem_effectless_act as)
graph_plan_lemma_16_9
|- ∀as. sublist (rem_effectless_act as) as
graph_plan_lemma_16_10
|- ∀as P. no_effectless_act as ⇒ no_effectless_act (FILTER P as)
graph_plan_lemma_16_11
|- ∀as1 as2. sublist as1 (rem_effectless_act as2) ⇒ sublist as1 as2
graph_plan_lemma_16_12
|- ∀as1 as2.
     no_effectless_act (as1 ⧺ as2) ⇔
     no_effectless_act as1 ∧ no_effectless_act as2
graph_plan_lemma_16_13
|- ∀as1 as2. sublist as1 as2 ∧ no_effectless_act as2 ⇒ no_effectless_act as1
graph_plan_lemma_16_14
|- ∀PROB as. exec_plan (s,as) = exec_plan (s,rem_effectless_act as)
graph_plan_lemma_16
|- ∀s A as.
     (exec_plan (s,as) = exec_plan (s,rem_effectless_act as)) ∧
     (sat_precond_as (s,as) ⇒ sat_precond_as (s,rem_effectless_act as)) ∧
     LENGTH (rem_effectless_act as) ≤ LENGTH as ∧
     (set as ⊆ A ⇒ set (rem_effectless_act as) ⊆ A) ∧
     no_effectless_act (rem_effectless_act as) ∧
     ∀P. LENGTH (FILTER P (rem_effectless_act as)) ≤ LENGTH (FILTER P as)
rem_effectless_act_subset_rem_effectless_act_set_thm
|- ∀as A. set as ⊆ A ⇒ set (rem_effectless_act as) ⊆ rem_effectless_act_set A
rem_effectless_act_set_no_empty_actions_thm
|- ∀A. rem_effectless_act_set A ⊆ {a | FDOM (SND a) ≠ ∅}
graph_plan_lemma_7_9
|- ∀s as.
     no_effectless_act as ⇒ no_effectless_act (rem_condless_act (s,[],as))
graph_plan_lemma_17
|- ∀as_1 as_2 as s.
     (as_1 ⧺ as_2 = as) ∧ sat_precond_as (s,as) ⇒
     sat_precond_as (s,as_1) ∧ sat_precond_as (exec_plan (s,as_1),as_2)
vtx_cut_main_lemma_1_1_1_1
|- ∀as.
     no_effectless_act as ∧ (∀x. FDOM (SND (f x)) ≠ ∅) ⇒
     EVERY (λa. f a ≠ (FEMPTY,FEMPTY)) as
vtx_cut_main_lemma_xx_7
|- ∀s as as'.
     sat_precond_as (s,as ⧺ as') ⇒ sat_precond_as (exec_plan (s,as),as')
child_parent_lemma_1_1_5
|- ∀PROB a vs.
     a ∈ PROB ∧ ¬varset_action (a,vs) ⇒
     ¬DISJOINT (FDOM (SND a)) (prob_dom PROB DIFF vs)
child_parent_lemma_xxx
|- ∀PROB a vs.
     varset_action (a,vs) ⇒ DISJOINT (FDOM (SND a)) (prob_dom PROB DIFF vs)
child_parent_lemma_xxxx
|- ∀PROB a vs.
     varset_action (a,prob_dom PROB DIFF vs) ⇒ DISJOINT (FDOM (SND a)) vs
child_parent_lemma_xxxxx
|- ∀PROB a vs.
     varset_action (a,vs) ∧ FDOM (SND a) ≠ ∅ ⇒ ¬DISJOINT (FDOM (SND a)) vs
child_parent_lemma_xxxxxx
|- ∀s a vs. varset_action (a,vs) ⇒ DISJOINT (FDOM (SND a)) (s DIFF vs)
child_parent_lemma_2_1_2_2
|- ∀PROB vs as s.
     EVERY (λa. varset_action (a,prob_dom PROB DIFF vs)) as ⇒
     (DRESTRICT s vs = DRESTRICT (exec_plan (s,as)) vs)
bound_child_parent_lemma_1_1_1_4_2_1
|- ∀as. no_effectless_act as ⇒ (FILTER (λa. FDOM (SND a) ≠ ∅) as = as)
parent_children_lemma_1_1_1_7_1
|- ∀a vs vs' vs''.
     varset_action (a,vs'' DIFF (vs' ∪ vs)) ⇒ varset_action (a,vs'' DIFF vs)
parent_children_lemma_1_1_1_12_2
|- ∀s vs vs' a.
     varset_action (a,s DIFF (vs ∪ vs')) ⇒ varset_action (a,s DIFF vs')
parent_children_main_lemma_1_1_10
|- ∀PROB as.
     as ∈ valid_plans PROB ⇒
     (FILTER (λa. varset_action (a,prob_dom PROB)) as = as)
parent_children_main_lemma_1_1_11_1
|- ∀a vs vs'. vs ⊆ vs' ∧ varset_action (a,vs) ⇒ varset_action (a,vs')
sat_precond_as_pfx
|- ∀s. sat_precond_as (s,as ⧺ as') ⇒ sat_precond_as (s,as)