Theory "depGraphVtxCut"

Parents     systemAbstraction

Signature

Constant Type
before :α list # α list # α list -> bool
full_ass :((α |-> β) # γ -> bool) # (α -> bool) -> bool
in_ass_union :(α |-> β) # (α |-> β) # (α |-> β) -> bool
permutable :((α |-> β) # (α |-> β) -> bool) -> bool
replace_projected_dual :(α # β -> bool) # (α # γ -> bool) # α list # β list # γ list -> α list
replace_projected_single :(α # β -> bool) # α list # β list -> α list

Definitions

replace_projected_single_primitive_def
|- replace_projected_single =
   WFREC
     (@R.
        WF R ∧
        (∀as_1 as a_1 a P. P (a,a_1) ⇒ R (P,as,as_1) (P,a::as,a_1::as_1)) ∧
        ∀as_1 as a_1 a P. ¬P (a,a_1) ⇒ R (P,as,a_1::as_1) (P,a::as,a_1::as_1))
     (λreplace_projected_single a'.
        case a' of
          (P,[],as_1') => I []
        | (P,a::as,[]) => I []
        | (P,a::as,a_1::as_1) =>
            I
              (if P (a,a_1) then a::replace_projected_single (P,as,as_1)
               else replace_projected_single (P,as,a_1::as_1)))
replace_projected_dual_primitive_def
|- replace_projected_dual =
   WFREC
     (@R.
        WF R ∧
        (∀as_2 as_1 as a_2 P_2 a_1 a P_1.
           P_1 (a,a_1) ∧ P_2 (a,a_2) ⇒
           R (P_1,P_2,as,as_1,as_2) (P_1,P_2,a::as,a_1::as_1,a_2::as_2)) ∧
        (∀as_2 as_1 as a_2 P_2 a_1 a P_1.
           ¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ P_1 (a,a_1) ⇒
           R (P_1,P_2,as,as_1,a_2::as_2)
             (P_1,P_2,a::as,a_1::as_1,a_2::as_2)) ∧
        (∀as_2 as_1 as a_2 P_2 a_1 a P_1.
           ¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ ¬P_1 (a,a_1) ∧ P_2 (a,a_2) ⇒
           R (P_1,P_2,as,a_1::as_1,as_2)
             (P_1,P_2,a::as,a_1::as_1,a_2::as_2)) ∧
        ∀as_2 as_1 as a_2 P_2 a_1 a P_1.
          ¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ ¬P_1 (a,a_1) ∧ ¬P_2 (a,a_2) ⇒
          R (P_1,P_2,as,a_1::as_1,a_2::as_2)
            (P_1,P_2,a::as,a_1::as_1,a_2::as_2))
     (λreplace_projected_dual a'.
        case a' of
          (P_1,P_2,[],v5) => I []
        | (P_1,P_2,a::as,v14,[]) =>
            I (replace_projected_single (P_1,a::as,v14))
        | (P_1,P_2,a::as,[],a_2::as_2) =>
            I (replace_projected_single (P_2,a::as,a_2::as_2))
        | (P_1,P_2,a::as,a_1::as_1,a_2::as_2) =>
            I
              (if P_1 (a,a_1) ∧ P_2 (a,a_2) then
                 a::replace_projected_dual (P_1,P_2,as,as_1,as_2)
               else if P_1 (a,a_1) then
                 a::replace_projected_dual (P_1,P_2,as,as_1,a_2::as_2)
               else if P_2 (a,a_2) then
                 a::replace_projected_dual (P_1,P_2,as,a_1::as_1,as_2)
               else replace_projected_dual (P_1,P_2,as,a_1::as_1,a_2::as_2)))
full_ass_def
|- ∀PROB vs. full_ass (PROB,vs) ⇔ ∀a. a ∈ PROB ⇒ vs ⊆ FDOM (FST a)
permutable_def
|- ∀PROB.
     permutable PROB ⇔
     (∀s as' as'' as.
        as ∈ valid_plans PROB ∧ sublist as' as ∧ sublist as'' as ∧
        sat_precond_as (s,as') ∧ sat_precond_as (s,as'') ∧
        sat_precond_as (s,as) ⇒
        sat_precond_as
          (s,
           replace_projected_dual
             ((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,as',as''))) ∧
     full_ass (PROB,prob_dom PROB)
in_ass_union_def
|- ∀s s' s''.
     in_ass_union (s,s',s'') ⇔
     ∀x. x ∈ FDOM s'' ⇒ (s'' ' x = s ' x) ∨ (s'' ' x = s' ' x)
before_primitive_def
|- before =
   WFREC
     (@R.
        WF R ∧
        ∀t t'' t' h'' h h'.
          h' ≠ h ∧ ¬((h'' = h) ∧ h' ≠ h) ⇒
          R (h'::t',h''::t'',t) (h'::t',h''::t'',h::t))
     (λbefore a.
        case a of
          (v,[],v3) => ARB
        | ([],h''::t'',[]) => ARB
        | (h'''::t''',h''::t'',[]) => I F
        | ([],h''::t'',h::t) => I F
        | (h'::t',h''::t'',h::t) =>
            I
              (if h' = h then T
               else if (h'' = h) ∧ h' ≠ h then F
               else before (h'::t',h''::t'',t)))


Theorems

replace_projected_single_ind
|- ∀P'.
     (∀P a as a_1 as_1.
        (P (a,a_1) ⇒ P' (P,as,as_1)) ∧ (¬P (a,a_1) ⇒ P' (P,as,a_1::as_1)) ⇒
        P' (P,a::as,a_1::as_1)) ∧ (∀P as_1. P' (P,[],as_1)) ∧
     (∀P v4 v5. P' (P,v4::v5,[])) ⇒
     ∀v v1 v2. P' (v,v1,v2)
replace_projected_single_def
|- (∀as_1 as a_1 a P.
      replace_projected_single (P,a::as,a_1::as_1) =
      if P (a,a_1) then a::replace_projected_single (P,as,as_1)
      else replace_projected_single (P,as,a_1::as_1)) ∧
   (∀as_1 P. replace_projected_single (P,[],as_1) = []) ∧
   ∀v5 v4 P. replace_projected_single (P,v4::v5,[]) = []
replace_projected_dual_ind
|- ∀P.
     (∀P_1 P_2 a as a_1 as_1 a_2 as_2.
        (P_1 (a,a_1) ∧ P_2 (a,a_2) ⇒ P (P_1,P_2,as,as_1,as_2)) ∧
        (¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ P_1 (a,a_1) ⇒
         P (P_1,P_2,as,as_1,a_2::as_2)) ∧
        (¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ ¬P_1 (a,a_1) ∧ P_2 (a,a_2) ⇒
         P (P_1,P_2,as,a_1::as_1,as_2)) ∧
        (¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ ¬P_1 (a,a_1) ∧ ¬P_2 (a,a_2) ⇒
         P (P_1,P_2,as,a_1::as_1,a_2::as_2)) ⇒
        P (P_1,P_2,a::as,a_1::as_1,a_2::as_2)) ∧
     (∀P_1 P_2 as_1 as_2. P (P_1,P_2,[],as_1,as_2)) ∧
     (∀P_1 P_2 v6 v7 as_1. P (P_1,P_2,v6::v7,as_1,[])) ∧
     (∀P_1 P_2 v8 v9 v16 v17. P (P_1,P_2,v8::v9,[],v16::v17)) ⇒
     ∀v v1 v2 v3 v4. P (v,v1,v2,v3,v4)
replace_projected_dual_def
|- (∀as_2 as_1 as a_2 a_1 a P_2 P_1.
      replace_projected_dual (P_1,P_2,a::as,a_1::as_1,a_2::as_2) =
      if P_1 (a,a_1) ∧ P_2 (a,a_2) then
        a::replace_projected_dual (P_1,P_2,as,as_1,as_2)
      else if P_1 (a,a_1) then
        a::replace_projected_dual (P_1,P_2,as,as_1,a_2::as_2)
      else if P_2 (a,a_2) then
        a::replace_projected_dual (P_1,P_2,as,a_1::as_1,as_2)
      else replace_projected_dual (P_1,P_2,as,a_1::as_1,a_2::as_2)) ∧
   (∀as_2 as_1 P_2 P_1. replace_projected_dual (P_1,P_2,[],as_1,as_2) = []) ∧
   (∀v7 v6 as_1 P_2 P_1.
      replace_projected_dual (P_1,P_2,v6::v7,as_1,[]) =
      replace_projected_single (P_1,v6::v7,as_1)) ∧
   ∀v9 v8 v17 v16 P_2 P_1.
     replace_projected_dual (P_1,P_2,v8::v9,[],v16::v17) =
     replace_projected_single (P_2,v8::v9,v16::v17)
vtx_cut_main_lemma_1_1_1
|- ∀P as_1 as. LENGTH (replace_projected_single (P,as,as_1)) ≤ LENGTH as_1
vtx_cut_main_lemma_1_1
|- ∀P_1 P_2 as_1 as_2 as.
     LENGTH (replace_projected_dual (P_1,P_2,as,as_1,as_2)) ≤
     LENGTH as_1 + LENGTH as_2
vtx_cut_main_lemma_1_2_1
|- ∀P as' as. sublist (replace_projected_single (P,as,as')) as
vtx_cut_main_lemma_1_2
|- ∀P_1 P_2 as' as'' as.
     sublist (replace_projected_dual (P_1,P_2,as,as',as'')) as
vtx_cut_main_lemma_1_3
|- ∀P_1 P_2 as' as'' as.
     replace_projected_dual (P_1,P_2,as,as',as'') =
     replace_projected_dual (P_2,P_1,as,as'',as')
vtx_cut_main_lemma_xx_4_1
|- ∀as as'.
     sublist as' as ⇒
     (replace_projected_single ((λ(a_1,a_2). a_1 = a_2),as,as') = as')
vtx_cut_main_lemma_xx_1
|- ∀h h' as' as.
     h ≠ h' ∧ sublist (h'::as') as ⇒
     (replace_projected_dual
        ((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),h::as,h'::as',[h]) =
      h::h'::as')
vtx_cut_main_lemma_xx_2
|- ∀PROB s s' as.
     as ≠ [] ∧ full_ass (PROB,prob_dom PROB) ∧ as ∈ valid_plans PROB ∧
     s ∈ valid_states PROB ∧ s' ∈ valid_states PROB ∧ sat_precond_as (s,as) ∧
     sat_precond_as (s',as) ⇒
     (s = s')
vtx_cut_main_lemma_xx_3
|- ∀s s' s''. in_ass_union (s,s',s'') ⇔ in_ass_union (s',s,s'')
vtx_cut_main_lemma_xx_4_2
|- ∀h h' as as' as''.
     (replace_projected_single ((λ(a_1,a_2). a_1 = a_2),as,h::as') =
      h'::as'') ⇒
     (h = h')
vtx_cut_main_lemma_xx_4_3
|- ∀h h' h'' t as as' as''.
     (replace_projected_dual
        ((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,h'::as',
         h''::as'') =
      h::t) ⇒
     ∃as_dis as_new.
       (as = as_dis ⧺ [h] ⧺ as_new) ∧ ¬MEM h' as_dis ∧ ¬MEM h'' as_dis
vtx_cut_main_lemma_xx_4_4
|- ∀h h' h'' t as as' as''.
     (replace_projected_dual
        ((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,h'::as',
         h''::as'') =
      h::t) ⇒
     (h = h') ∨ (h = h'')
vtx_cut_main_lemma_xx_4
|- ∀h h' h'' t as as' as''.
     (replace_projected_dual
        ((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,h'::as',
         h''::as'') =
      h::t) ⇒
     (∃as_dis as_new.
        (as = as_dis ⧺ [h] ⧺ as_new) ∧ ¬MEM h' as_dis ∧ ¬MEM h'' as_dis) ∧
     ((h = h') ∨ (h = h''))
vtx_cut_main_lemma_xx_5
|- ∀h t as_dis as as' as''.
     ¬MEM h as_dis ∧
     (replace_projected_dual
        ((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as_dis ⧺ as,as',
         as'') =
      h::t) ⇒
     (replace_projected_dual
        ((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as_dis ⧺ as,as',
         as'') =
      replace_projected_dual
        ((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,as',as''))
vtx_cut_main_lemma_xx_6
|- ∀s s' h as as'.
     full_ass (PROB,prob_dom PROB) ∧ h::as ∈ valid_plans PROB ∧
     s ∈ valid_states PROB ∧ s' ∈ valid_states PROB ∧
     sat_precond_as (s,h::as) ∧ sat_precond_as (s',h::as') ⇒
     sat_precond_as (s,h::as')
vtx_cut_main_lemma_xx_8_1
|- ∀h' as as'.
     (replace_projected_single ((λ(a_1,a_2). a_1 = a_2),as,h'::as') = []) ⇒
     ¬MEM h' as
vtx_cut_main_lemma_xx_8
|- ∀h' h'' as as' as''.
     (replace_projected_dual
        ((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,h'::as',
         h''::as'') =
      []) ⇒
     ¬MEM h' as ∧ ¬MEM h'' as
vtx_cut_main_lemma_xx_9
|- ∀s. in_ass_union (s,s,s)
vtx_cut_main_lemma_xx_10
|- ∀s s'. in_ass_union (s,s',s')
before_ind
|- ∀P.
     (∀h' t' h'' t'' h t.
        (h' ≠ h ∧ ¬((h'' = h) ∧ h' ≠ h) ⇒ P (h'::t',h''::t'',t)) ⇒
        P (h'::t',h''::t'',h::t)) ∧ (∀h'' t'' h t. P ([],h''::t'',h::t)) ∧
     (∀h' t' h'' t''. P (h'::t',h''::t'',[])) ∧ (∀v7 v6. P (v7,[],v6)) ∧
     (∀v12 v13. P ([],v12::v13,[])) ⇒
     ∀v v1 v2. P (v,v1,v2)
before_def
|- (∀t'' t' t h'' h' h.
      before (h'::t',h''::t'',h::t) ⇔
      if h' = h then T
      else if (h'' = h) ∧ h' ≠ h then F
      else before (h'::t',h''::t'',t)) ∧
   (∀t'' t h'' h. before ([],h''::t'',h::t) ⇔ F) ∧
   ∀t'' t' h'' h'. before (h'::t',h''::t'',[]) ⇔ F
vtx_cut_main_lemma_xx
|- ∀PROB as' as'' as s.
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧ permutable PROB ∧
     sublist as' as ∧ sublist as'' as ∧ sat_precond_as (s,as') ∧
     sat_precond_as (s,as'') ∧ sat_precond_as (s,as) ⇒
     in_ass_union
       (exec_plan (s,as'),exec_plan (s,as''),
        exec_plan
          (s,
           replace_projected_dual
             ((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,as',as'')))