Theory "parentChildStructure"

Parents     systemAbstraction

Signature

Constant Type
as_proj_child :((α |-> β) # (α |-> γ)) list # (α -> bool) -> ((α |-> β) # (α |-> γ)) list
as_proj_parent :(α # (β |-> γ)) list # (β -> bool) -> (α # (β |-> γ)) list
child_parent_rel :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) -> bool
replace_projected :((α |-> β) # (α |-> γ)) list # ((α |-> β) # (α |-> γ)) list # ((α |-> β) # (α |-> γ)) list # (α -> bool) -> ((α |-> β) # (α |-> γ)) list
stitch :((α |-> β) # (α |-> γ)) list -> (α -> bool) -> ((α |-> β) # (α |-> γ)) list -> ((α |-> β) # (α |-> γ)) list

Definitions

child_parent_rel_def
|- ∀PROB vs.
     child_parent_rel (PROB,vs) ⇔ ¬dep_var_set (PROB,vs,prob_dom PROB DIFF vs)
as_proj_child_def
|- ∀as vs.
     as_proj_child (as,vs) =
     FILTER (λa. varset_action (a,vs) ∧ FDOM (SND a) ≠ ∅)
       (MAP (λa. (DRESTRICT (FST a) vs,SND a)) as)
as_proj_parent_def
|- ∀as vs.
     as_proj_parent (as,vs) =
     FILTER (λa. ¬varset_action (a,vs) ∧ FDOM (SND a) ≠ ∅) as
replace_projected_primitive_def
|- replace_projected =
   WFREC
     (@R.
        WF R ∧
        (∀as as' a' as'' vs a.
           ¬varset_action (a,vs) ⇒
           R (as'' ⧺ [a],a'::as',as,vs) (as'',a'::as',a::as,vs)) ∧
        (∀as as' as'' a' vs a.
           varset_action (a,vs) ∧ a' ≠ action_proj (a,vs) ⇒
           R (as'',a'::as',as,vs) (as'',a'::as',a::as,vs)) ∧
        ∀as as' as'' a' vs a.
          varset_action (a,vs) ∧ (a' = action_proj (a,vs)) ⇒
          R (as'' ⧺ [a],as',as,vs) (as'',a'::as',a::as,vs))
     (λreplace_projected a''.
        case a'' of
          (as'',[],as''',vs) =>
            I (as'' ⧺ FILTER (λa. ¬varset_action (a,vs)) as''')
        | (as'',a'::as',[],vs) => I as''
        | (as'',a'::as',a::as,vs) =>
            I
              (if varset_action (a,vs) then
                 if a' = action_proj (a,vs) then
                   replace_projected (as'' ⧺ [a],as',as,vs)
                 else replace_projected (as'',a'::as',as,vs)
               else replace_projected (as'' ⧺ [a],a'::as',as,vs)))


Theorems

child_parent_lemma_1_1_1
|- ∀a vs. varset_action (a,vs) ⇒ (DRESTRICT (SND a) vs = SND a)
child_parent_lemma_1_1_2
|- ∀PROB a vs.
     a ∈ PROB ∧ child_parent_rel (PROB,vs) ∧ FDOM (SND a) ≠ ∅ ⇒
     (varset_action (a,vs) ⇔ ¬varset_action (a,prob_dom PROB DIFF vs))
child_parent_lemma_1_4_1
|- ∀PROB a vs.
     child_parent_rel (PROB,vs) ∧ a ∈ PROB ∧
     ¬DISJOINT (FDOM (SND a)) (prob_dom PROB DIFF vs) ⇒
     DISJOINT (FDOM (SND a)) vs
child_parent_lemma_1_1
|- ∀PROB as vs.
     as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ⇒
     (as_proj_child (as,vs) = as_proj (as,vs))
graph_plan_lemma_3
|- ∀vs as.
     no_effectless_act as ⇒
     (LENGTH (FILTER (λa. varset_action (a,vs)) as) =
      LENGTH (as_proj_child (as,vs)))
graph_plan_lemma_18_1
|- ∀as vs.
     as_proj_child (as,vs) =
     FILTER (λa. varset_action (a,vs) ∧ FDOM (SND a) ≠ ∅)
       (MAP (λa. (DRESTRICT (FST a) vs,SND a)) as)
graph_plan_lemma_18
|- ∀as vs.
     as_proj_child (rem_effectless_act as,vs) =
     FILTER (λa. varset_action (a,vs))
       (MAP (λa. (DRESTRICT (FST a) vs,SND a)) (rem_effectless_act as))
child_parent_lemma_1_2_1_1
|- ∀PROB vs a.
     child_parent_rel (PROB,vs) ∧ a ∈ PROB ∧
     ¬DISJOINT (FDOM (SND a)) (prob_dom PROB DIFF vs) ⇒
     DISJOINT (FDOM (FST a)) vs
child_parent_lemma_1_2_1
|- ∀PROB vs a.
     child_parent_rel (PROB,vs) ∧ a ∈ PROB ∧
     varset_action (a,prob_dom PROB DIFF vs) ∧ FDOM (SND a) ≠ ∅ ⇒
     FDOM (FST a) ⊆ prob_dom PROB DIFF vs
child_parent_lemma_1_2
|- ∀PROB as vs.
     as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ⇒
     (as_proj_parent (as,vs) = as_proj (as,prob_dom PROB DIFF vs))
child_parent_lemma_1
|- ∀PROB as vs.
     as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ⇒
     (as_proj_child (as,vs) = as_proj (as,vs)) ∧
     (as_proj_parent (as,vs) = as_proj (as,prob_dom PROB DIFF vs))
child_parent_lemma_xx
|- ∀PROB a vs.
     child_parent_rel (PROB,vs) ∧ a ∈ PROB ∧ ¬varset_action (a,vs) ⇒
     DISJOINT (FDOM (SND a)) vs
child_parent_lemma_2_1_1_1_1_1
|- ∀PROB s as vs.
     as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ⇒
     (DRESTRICT s vs = DRESTRICT (exec_plan (s,as_proj_parent (as,vs))) vs)
child_parent_lemma_2_1_1_1_1
|- ∀PROB s s' as vs.
     as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ∧
     (DRESTRICT s vs = DRESTRICT (exec_plan (s,as)) vs) ⇒
     (DRESTRICT s vs = DRESTRICT (exec_plan (s,as_proj_parent (as,vs))) vs)
child_parent_lemma_2_1_1_1_3
|- ∀as vs.
     (∃a. MEM a as ∧ (λa. varset_action (a,vs)) a) ⇒
     LENGTH (FILTER (λa. varset_action (a,vs)) (as_proj_parent (as,vs))) <
     LENGTH (FILTER (λa. varset_action (a,vs)) as)
child_parent_lemma_2_1_1_1
|- ∀PROB s as vs.
     as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ∧
     (DRESTRICT s vs = DRESTRICT (exec_plan (s,as)) vs) ∧
     (∃a. MEM a as ∧ (λa. varset_action (a,vs)) a) ⇒
     (DRESTRICT (exec_plan (s,as)) vs =
      DRESTRICT (exec_plan (s,as_proj_parent (as,vs))) vs) ∧
     LENGTH (FILTER (λa. varset_action (a,vs)) (as_proj_parent (as,vs))) <
     LENGTH (FILTER (λa. varset_action (a,vs)) as)
child_parent_lemma_2_1_1_2
|- ∀PROB s as vs.
     as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ∧
     sat_precond_as (s,as) ⇒
     sat_precond_as (s,as_proj_parent (as,vs))
child_parent_lemma_2_1_2_1
|- ∀PROB vs as.
     child_parent_rel (PROB,vs) ∧ as ∈ valid_plans PROB ⇒
     (as_proj_parent (as,vs) =
      FILTER (λa. varset_action (a,prob_dom PROB DIFF vs) ∧ FDOM (SND a) ≠ ∅)
        as)
child_parent_lemma_2_1_2_4
|- ∀PROB as vs.
     as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ⇒
     (FILTER (λa. varset_action (a,prob_dom PROB DIFF vs) ∧ FDOM (SND a) ≠ ∅)
        as =
      FILTER (λa. ¬varset_action (a,vs) ∧ FDOM (SND a) ≠ ∅) as)
replace_projected_ind
|- ∀P.
     (∀as'' a' as' a as vs.
        (¬varset_action (a,vs) ⇒ P (as'' ⧺ [a],a'::as',as,vs)) ∧
        (varset_action (a,vs) ∧ a' ≠ action_proj (a,vs) ⇒
         P (as'',a'::as',as,vs)) ∧
        (varset_action (a,vs) ∧ (a' = action_proj (a,vs)) ⇒
         P (as'' ⧺ [a],as',as,vs)) ⇒
        P (as'',a'::as',a::as,vs)) ∧ (∀as'' as vs. P (as'',[],as,vs)) ∧
     (∀as'' v6 v7 vs. P (as'',v6::v7,[],vs)) ⇒
     ∀v v1 v2 v3. P (v,v1,v2,v3)
replace_projected_def
|- (∀vs as'' as' as a' a.
      replace_projected (as'',a'::as',a::as,vs) =
      if varset_action (a,vs) then
        if a' = action_proj (a,vs) then
          replace_projected (as'' ⧺ [a],as',as,vs)
        else replace_projected (as'',a'::as',as,vs)
      else replace_projected (as'' ⧺ [a],a'::as',as,vs)) ∧
   (∀vs as'' as.
      replace_projected (as'',[],as,vs) =
      as'' ⧺ FILTER (λa. ¬varset_action (a,vs)) as) ∧
   ∀vs v7 v6 as''. replace_projected (as'',v6::v7,[],vs) = as''
stitch_ind
|- ∀P.
     (∀a' as' vs a as.
        (¬varset_action (a,vs) ⇒ P (a'::as') vs as) ∧
        (varset_action (a,vs) ∧ a' ≠ action_proj (a,vs) ⇒ P (a'::as') vs as) ∧
        (varset_action (a,vs) ∧ (a' = action_proj (a,vs)) ⇒ P as' vs as) ⇒
        P (a'::as') vs (a::as)) ∧ (∀vs as. P [] vs as) ∧
     (∀a' as' vs. P (a'::as') vs []) ⇒
     ∀v v1 v2. P v v1 v2
stitch_def
|- (∀vs as' as a' a.
      stitch (a'::as') vs (a::as) =
      if varset_action (a,vs) then
        if a' = action_proj (a,vs) then a::stitch as' vs as
        else stitch (a'::as') vs as
      else a::stitch (a'::as') vs as) ∧
   (∀vs as. stitch [] vs as = FILTER (λa. ¬varset_action (a,vs)) as) ∧
   ∀vs as' a'. stitch (a'::as') vs [] = []
replace_projected_stitch
|- ∀as as' acc. replace_projected (acc,as',as,vs) = acc ⧺ stitch as' vs as
graph_plan_lemma_22_1
|- ∀as as' as'' vs s.
     set as ⊆ s ∧ set as'' ⊆ s ⇒ set (replace_projected (as'',as',as,vs)) ⊆ s
graph_plan_lemma_22_1'
|- ∀as as' as'' vs s.
     as ∈ valid_plans s ∧ as'' ∈ valid_plans s ⇒
     replace_projected (as'',as',as,vs) ∈ valid_plans s
graph_plan_lemma_22_2_1
|- ∀as as' as'' as''' as'''' vs.
     sublist (replace_projected (as'',as',as,vs)) as''' ⇒
     sublist (replace_projected (as'''' ⧺ as'',as',as,vs)) (as'''' ⧺ as''')
graph_plan_lemma_22_2
|- ∀as as' vs s. sublist (replace_projected ([],as',as,vs)) as
graph_plan_lemma_22_3_1
|- ∀as''' as'' as' as vs.
     replace_projected (as''' ⧺ as'',as',as,vs) =
     as''' ⧺ replace_projected (as'',as',as,vs)
graph_plan_lemma_22_3
|- ∀PROB vs as' as.
     no_effectless_act as ∧ as ∈ valid_plans PROB ⇒
     no_effectless_act (replace_projected ([],as',as,vs))
graph_plan_lemma_22_4
|- ∀PROB vs as as'.
     as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ∧
     no_effectless_act as ⇒
     replace_projected ([],as',as,vs) ∈ valid_plans PROB
bound_child_parent_lemma_1_1_1_2_1_1
|- ∀PROB as vs.
     no_effectless_act as ∧ child_parent_rel (PROB,vs) ∧
     as ∈ valid_plans PROB ⇒
     (as_proj (FILTER (λa. ¬varset_action (a,vs)) as,vs) = [])
bound_child_parent_lemma_1_1_1_2_1
|- ∀PROB as as' vs.
     no_effectless_act as ∧ child_parent_rel (PROB,vs) ∧
     as ∈ valid_plans PROB ∧ sublist as' (as_proj (as,vs)) ⇒
     (as' = as_proj (replace_projected ([],as',as,vs),vs))
bound_child_parent_lemma_1_1_1_2
|- ∀PROB s as vs as'.
     child_parent_rel (PROB,vs) ∧ s ∈ valid_states PROB ∧
     as ∈ valid_plans PROB ∧ sublist as' (as_proj (as,vs)) ∧
     no_effectless_act as ⇒
     (LENGTH as' =
      LENGTH
        (FILTER (λa. varset_action (a,vs))
           (replace_projected ([],as',as,vs))))
bound_child_parent_lemma_1_1_1_3_1_1
|- ∀PROB vs a s s'.
     child_parent_rel (PROB,vs) ∧ a ∈ PROB ∧ FDOM (SND a) ≠ ∅ ∧
     s ∈ valid_states PROB ∧ s' ∈ valid_states PROB ∧
     (DRESTRICT s (prob_dom PROB DIFF vs) =
      DRESTRICT s' (prob_dom PROB DIFF vs)) ∧ ¬varset_action (a,vs) ∧
     FST a ⊑ s ⇒
     FST a ⊑ s'
bound_child_parent_lemma_1_1_1_3_1
|- ∀PROB vs sa sc as as_c.
     sublist as_c (as_proj (as,vs)) ∧ sa ∈ valid_states PROB ∧
     sc ∈ valid_states PROB ∧ child_parent_rel (PROB,vs) ∧
     as ∈ valid_plans PROB ∧ no_effectless_act as ∧
     (DRESTRICT sa (prob_dom PROB DIFF vs) =
      DRESTRICT sc (prob_dom PROB DIFF vs)) ∧ sat_precond_as (sa,as) ∧
     sat_precond_as (sc,as_c) ⇒
     sat_precond_as (sc,replace_projected ([],as_c,as,vs))
bound_child_parent_lemma_1_1_1_3
|- ∀PROB s as vs as'.
     child_parent_rel (PROB,vs) ∧ s ∈ valid_states PROB ∧
     as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ∧
     sublist as' (as_proj (as,vs)) ∧ no_effectless_act as ∧
     sat_precond_as (s,as') ⇒
     (DRESTRICT (exec_plan (s,replace_projected ([],as',as,vs))) vs =
      exec_plan (DRESTRICT s vs,as'))
bound_child_parent_lemma_1_1_1_4_1_1
|- ∀PROB vs as_c as.
     child_parent_rel (PROB,vs) ∧ as ∈ valid_plans PROB ⇒
     (FILTER (λa. ¬varset_action (a,vs)) as =
      FILTER (λa. ¬varset_action (a,vs)) (replace_projected ([],as_c,as,vs)))
bound_child_parent_lemma_1_1_1_4_1_2
|- ∀PROB vs as.
     child_parent_rel (PROB,vs) ∧ no_effectless_act as ∧
     as ∈ valid_plans PROB ⇒
     (FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as =
      FILTER (λa. ¬varset_action (a,vs)) as)
bound_child_parent_lemma_1_1_1_4_1
|- ∀PROB vs as_c as.
     child_parent_rel (PROB,vs) ∧ no_effectless_act as ∧
     as ∈ valid_plans PROB ⇒
     (FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as =
      FILTER (λa. varset_action (a,prob_dom PROB DIFF vs))
        (replace_projected ([],as_c,as,vs)))
bound_child_parent_lemma_1_1_1_4_2
|- ∀PROB vs as.
     child_parent_rel (PROB,vs) ∧ as ∈ valid_plans PROB ∧
     no_effectless_act as ⇒
     (as_proj (as,prob_dom PROB DIFF vs) =
      FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as)
bound_child_parent_lemma_1_1_1_4_3
|- ∀PROB vs s as.
     child_parent_rel (PROB,vs) ∧ as ∈ valid_plans PROB ∧
     s ∈ valid_states PROB ∧ sat_precond_as (s,as) ∧ no_effectless_act as ⇒
     sat_precond_as
       (s,FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as)
bound_child_parent_lemma_1_1_1_4
|- ∀PROB vs s as_c as.
     child_parent_rel (PROB,vs) ∧ s ∈ valid_states PROB ∧
     as ∈ valid_plans PROB ∧ sublist as_c (as_proj (as,vs)) ∧
     sat_precond_as (s,as) ∧ sat_precond_as (s,as_c) ∧ no_effectless_act as ⇒
     (DRESTRICT (exec_plan (s,as)) (prob_dom PROB DIFF vs) =
      DRESTRICT (exec_plan (s,replace_projected ([],as_c,as,vs)))
        (prob_dom PROB DIFF vs)) ∧
     (FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as =
      FILTER (λa. varset_action (a,prob_dom PROB DIFF vs))
        (replace_projected ([],as_c,as,vs)))
bound_child_parent_lemma_1_1_1'
|- ∀PROB as vs s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     child_parent_rel (PROB,vs) ∧ sat_precond_as (s,as) ∧
     no_effectless_act as ⇒
     ∃as'.
       (exec_plan (s,as') = exec_plan (s,as)) ∧
       (LENGTH (FILTER (λa. varset_action (a,vs)) as') ≤
        problem_plan_bound (prob_proj (PROB,vs)) ∧
        (FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as' =
         FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as)) ∧
       sublist as' as ∧ no_effectless_act as' ∧ as' ∈ valid_plans PROB ∧
       sat_precond_as (s,as')
parent_children_lemma_1_1_1_11_5
|- ∀P P2 P3 vs.
     (∀a. P3 a ∧ P2 (action_proj (a,vs)) ⇒ (P a ⇔ P (action_proj (a,vs)))) ∧
     (∀a. P a ∧ P2 a ∧ P3 a ⇒ varset_action (a,vs)) ∧
     (∀a. P2 a ∧ P3 a ∧ ¬varset_action (a,vs) ⇒ DISJOINT (FDOM (SND a)) vs) ⇒
     ∀as' as''.
       sublist as' (as_proj (as'',vs)) ∧ EVERY P2 as' ∧ EVERY P2 as'' ∧
       EVERY P3 as'' ⇒
       (LENGTH (FILTER P (replace_projected ([],as',as'',vs))) =
        LENGTH (FILTER P as'))
bound_child_parent_lemma_1_1_1''
|- ∀PROB as as' vs s.
     child_parent_rel (PROB,vs) ∧ s ∈ valid_states PROB ∧
     no_effectless_act as ∧ sublist as' (as_proj (as,vs)) ∧
     as ∈ valid_plans PROB ∧
     (DRESTRICT (exec_plan (s,as)) vs = exec_plan (DRESTRICT s vs,as')) ∧
     sat_precond_as (s,as) ∧ sat_precond_as (s,as') ⇒
     (exec_plan (s,replace_projected ([],as',as,vs)) = exec_plan (s,as))