Theory "boundingAlgorithms"

Parents     acycSspace   acycDepGraph

Signature

Constant Type
N_gen :(((α |-> β) # (α |-> γ) -> bool) -> num) -> ((α |-> β) # (α |-> γ) -> bool) -> (α -> bool) -> (α -> bool) list -> num
N_gen_curried :(((α |-> β) # (α |-> γ) -> bool) -> num) -> ((α |-> β) # (α |-> γ) -> bool) -> (α -> bool) list -> (α -> bool) -> num
S_gen :(((α |-> β) # (α |-> β) -> bool) -> num) -> (α -> bool) -> (α |-> β) list -> ((α |-> β) # (α |-> β) -> bool) -> (α |-> β) -> num
hybrid_algo :(((α |-> β) # (α |-> β) -> bool) -> (α -> bool) list) -> (((α |-> β) # (α |-> β) -> bool) -> (α -> bool) # (α |-> β) list -> bool) -> ((α |-> β) # (α |-> β) -> bool) -> num
hybrid_algo_gen :(((α |-> β) # (α |-> β) -> bool) -> (α -> bool) list) -> (((α |-> β) # (α |-> β) -> bool) -> (α -> bool) # (α |-> β) list -> bool) -> ((α |-> β) # (α |-> β) -> bool) -> num

Definitions

N_gen_def
|- (∀b PROB vs vs' lvs.
      N_gen b PROB vs (vs'::lvs) =
      if dep_var_set (PROB,vs,vs') then
        b (prob_proj (PROB,vs)) * N_gen b PROB vs' lvs + N_gen b PROB vs lvs
      else N_gen b PROB vs lvs) ∧
   ∀b PROB vs. N_gen b PROB vs [] = b (prob_proj (PROB,vs))
N_gen_curried_def
|- ∀b PROB lvs vs. N_gen_curried b PROB lvs vs = N_gen b PROB vs lvs
hybrid_algo_def
|- ∀f1 f2 PROB.
     hybrid_algo f1 f2 PROB =
     if 2 ≤ LENGTH (f1 PROB) then
       SUM (MAP (N_curried PROB (f1 PROB)) (f1 PROB))
     else if f2 PROB ≠ ∅ then
       (let
          xx = CHOICE (f2 PROB)
        in
          MAX_SET
            {S (FST xx) (SND xx) PROB s' |
             s' |
             s' ∈ valid_states (prob_proj (PROB,FST xx))})
     else problem_plan_bound PROB
S_gen_def
|- ∀b vs lss PROB s.
     S_gen b vs lss PROB s =
     wlp (state_successors (prob_proj (PROB,vs))) (λs. b (snapshot PROB s))
       MAX (λx y. x + y + 1) s lss


Theorems

N_gen_is_wighted_longest_path
|- ∀vs.
     N_gen b PROB vs lvs =
     wlp (λvs1 vs2. dep_var_set (PROB,vs1,vs2)) (λvs. b (prob_proj (PROB,vs)))
       $+ $* vs lvs
N_gen_valid_thm_1
|- ∀b.
     (∀PROB'. problem_plan_bound PROB' ≤ b PROB') ⇒
     ∀lvs vs. N (PROB,vs,lvs) ≤ N_gen b PROB vs lvs
N_gen_valid_thm
|- ∀b.
     (∀PROB'. problem_plan_bound PROB' ≤ b PROB') ⇒
     ∀lvs.
       ALL_DISTINCT lvs ∧ disjoint_varset lvs ⇒
       ∀PROB.
         FINITE PROB ∧ (prob_dom PROB = BIGUNION (set lvs)) ∧
         top_sorted (PROB,lvs) ⇒
         problem_plan_bound PROB <
         SUM (MAP (λvs. N_gen b PROB vs lvs) lvs) + 1
N_super_gen_valid_thm_1
|- ∀b P.
     (∀PROB'. P PROB' ⇒ problem_plan_bound PROB' ≤ b PROB') ∧
     (∀PROB' vs'.
        vs' ∩ prob_dom PROB' ≠ ∅ ∧ P PROB' ⇒ P (prob_proj (PROB',vs'))) ⇒
     ∀PROB lvs vs.
       P PROB ∧ vs ∩ prob_dom PROB ≠ ∅ ∧
       EVERY (λvs. vs ∩ prob_dom PROB ≠ ∅) lvs ⇒
       N (PROB,vs,lvs) ≤ N_gen b PROB vs lvs
N_super_gen_valid_thm
|- ∀b P.
     (∀PROB'. P PROB' ⇒ problem_plan_bound PROB' ≤ b PROB') ∧
     (∀PROB' vs'.
        vs' ∩ prob_dom PROB' ≠ ∅ ∧ P PROB' ⇒ P (prob_proj (PROB',vs'))) ⇒
     ∀lvs.
       ALL_DISTINCT lvs ∧ disjoint_varset lvs ∧ lvs ≠ [] ⇒
       ∀PROB.
         P PROB ∧ FINITE PROB ∧ (prob_dom PROB = BIGUNION (set lvs)) ∧
         top_sorted (PROB,lvs) ∧ EVERY (λvs. vs ∩ prob_dom PROB ≠ ∅) lvs ⇒
         problem_plan_bound PROB <
         SUM (MAP (λvs. N_gen b PROB vs lvs) lvs) + 1
N_more_gen_valid_thm_1
|- ∀vs.
     problem_plan_bound (prob_proj (PROB,vs)) ≤ b (prob_proj (PROB,vs)) ∧
     (∀vs'.
        MEM vs' lvs ⇒
        problem_plan_bound (prob_proj (PROB,vs')) ≤
        b (prob_proj (PROB,vs'))) ⇒
     N_curried PROB lvs vs ≤ N_gen b PROB vs lvs
N_more_gen_valid_thm
|- (∀vs'.
      MEM vs' lvs ⇒
      problem_plan_bound (prob_proj (PROB,vs')) ≤ b (prob_proj (PROB,vs'))) ∧
   FINITE PROB ∧ dep_DAG PROB lvs ⇒
   problem_plan_bound PROB ≤ SUM (MAP (λvs. N_gen b PROB vs lvs) lvs)
N_gen_eq
|- ∀b1 b2 PROB vs lvs.
     (∀x. FINITE x ⇒ (b1 x = b2 x)) ∧ FINITE PROB ⇒
     (N_gen b1 PROB vs lvs = N_gen b2 PROB vs lvs)
N_gen_empty
|- (∀PROB'. b (prob_proj (PROB',∅)) = 0) ⇒ (N_gen b PROB ∅ lvs = 0)
N_gen_def_ITP2015
|- (∀PROB'. b (prob_proj (PROB',∅)) = 0) ⇒
   ∀PROB vs lvs.
     top_sorted (PROB,lvs) ⇒
     (N_gen b PROB vs lvs =
      b (prob_proj (PROB,vs)) *
      (SUM (MAP (λvs'. N_gen b PROB vs' lvs) (children (PROB,vs,lvs))) + 1))
N_curried_more_gen_valid_thm
|- (∀vs'.
      MEM vs' lvs ⇒
      problem_plan_bound (prob_proj (PROB,vs')) ≤ b (prob_proj (PROB,vs'))) ∧
   FINITE PROB ∧ dep_DAG PROB lvs ⇒
   problem_plan_bound PROB ≤ SUM (MAP (N_gen_curried b PROB lvs) lvs)
N_gen_curried_valid_thm
|- ∀b.
     (∀PROB'. problem_plan_bound PROB' ≤ b PROB') ∧ FINITE PROB ∧
     dep_DAG PROB lvs ⇒
     problem_plan_bound PROB ≤
     SUM (MAP (λvs. N_gen_curried b PROB lvs vs) lvs)
N_gen_curried_is_wighted_longest_path
|- ∀vs.
     N_gen_curried b PROB lvs vs =
     wlp (λvs1 vs2. dep_var_set (PROB,vs1,vs2)) (λvs. b (prob_proj (PROB,vs)))
       $+ $* vs lvs
N_gen_curried_CONG
|- ∀PROB1 PROB2 lvs1 lvs2 vs1 vs2 b1 b2.
     (PROB1 = PROB2) ∧ (lvs1 = lvs2) ∧ (vs1 = vs2) ∧
     (b1 (prob_proj (PROB1,vs1)) = b2 (prob_proj (PROB2,vs2))) ∧
     (∀vs.
        MEM vs lvs2 ⇒
        (b1 (prob_proj (PROB1,vs)) = b2 (prob_proj (PROB2,vs)))) ⇒
     (N_gen_curried b1 PROB1 lvs1 vs1 = N_gen_curried b2 PROB2 lvs2 vs2)
N_gen_curried_def_ITP2015
|- (∀PROB'. b (prob_proj (PROB',∅)) = 0) ⇒
   ∀PROB vs lvs.
     top_sorted_curried PROB lvs ⇒
     (N_gen_curried b PROB lvs vs =
      b (prob_proj (PROB,vs)) *
      (SUM (MAP (N_gen_curried b PROB lvs) (children_curried PROB lvs vs)) +
       1))
hybrid_algorithm_valid
|- FINITE PROB ∧ ALL_DISTINCT (f1 PROB) ∧ disjoint_varset (f1 PROB) ∧
   (prob_dom PROB = BIGUNION (set (f1 PROB))) ∧
   top_sorted_curried PROB (f1 PROB) ∧
   (∀vs lss.
      (vs,lss) ∈ f2 PROB ⇒
      top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧
      (set lss = valid_states (prob_proj (PROB,vs)))) ⇒
   problem_plan_bound PROB ≤ hybrid_algo f1 f2 PROB
hybrid_algorithm_valid_thesis
|- FINITE PROB ∧ dep_DAG PROB (f1 PROB) ∧
   (∀vs lss. (vs,lss) ∈ f2 PROB ⇒ sspace_DAG (prob_proj (PROB,vs)) lss) ⇒
   problem_plan_bound PROB ≤ hybrid_algo f1 f2 PROB
S_gen_ell_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_gen problem_plan_bound vs lss PROB (DRESTRICT s vs)
S_gen_ell_bound_main_lemma
|- FINITE PROB ∧ sspace_DAG (prob_proj (PROB,vs)) lss ⇒
   problem_plan_bound PROB ≤
   MAX_SET
     {S_gen problem_plan_bound vs lss PROB s' |
      s' |
      s' ∈ valid_states (prob_proj (PROB,vs))}
S_gen_bound_main_lemma_1
|- FINITE PROB ∧ (set lss = valid_states (prob_proj (PROB,vs))) ∧
   (∀s.
      MEM s lss ⇒
      problem_plan_bound (snapshot PROB s) ≤ b (snapshot PROB s)) ⇒
   MAX_SET
     {S_gen problem_plan_bound vs lss PROB s' |
      s' |
      s' ∈ valid_states (prob_proj (PROB,vs))} ≤
   MAX_SET
     {S_gen b vs lss PROB s' | s' | s' ∈ valid_states (prob_proj (PROB,vs))}
S_gen_bound_main_lemma
|- FINITE PROB ∧ sspace_DAG (prob_proj (PROB,vs)) lss ∧
   (∀s.
      MEM s lss ⇒
      problem_plan_bound (snapshot PROB s) ≤ b (snapshot PROB s)) ⇒
   problem_plan_bound PROB ≤
   MAX_SET
     {S_gen b vs lss PROB s' | s' | s' ∈ valid_states (prob_proj (PROB,vs))}
parent_children_main_lemma_N_gen_curried_thesis
|- ∀lvs PROB.
     FINITE PROB ∧ dep_DAG PROB lvs ⇒
     problem_plan_bound PROB <
     SUM (MAP (N_gen_curried problem_plan_bound PROB lvs) lvs) + 1
termination_goal_1_1
|- ∀PROB f1 x projPROB.
     (∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB) ∧ MEM x (f1 PROB) ∧
     FINITE PROB ∧
     (∃vs. MEM vs (f1 PROB) ∧ (projPROB = prob_proj (PROB,vs))) ⇒
     CARD (prob_dom projPROB) < CARD (prob_dom PROB)
termination_goal_1
|- ∀f1 PROB x projPROB.
     FINITE PROB ∧ (∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB) ∧
     MEM x (f1 PROB) ∧
     (∃vs. MEM vs (f1 PROB) ∧ (projPROB = prob_proj (PROB,vs))) ⇒
     CARD projPROB + CARD (prob_dom projPROB) <
     CARD PROB + CARD (prob_dom PROB)
termination_goal_2
|- ∀f2 f1 PROB p_1 p_2 snapshotPROB.
     FINITE PROB ∧ (∃vs. MEM vs (f1 PROB) ∧ ¬(vs ⊂ prob_dom PROB)) ∧
     (f2 PROB ≠ ∅ ∧
      ∀vs lss s. (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB) ∧
     ((p_1,p_2) = CHOICE (f2 PROB)) ∧
     (∃s. MEM s p_2 ∧ (snapshotPROB = snapshot PROB s)) ⇒
     CARD snapshotPROB + CARD (prob_dom snapshotPROB) <
     CARD PROB + CARD (prob_dom PROB)
hybrid_algo_gen_ind
|- ∀P.
     (∀f1 f2 PROB.
        (∀vs lss snapshotPROB.
           FINITE PROB ∧ ¬(∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB) ∧
           (f2 PROB ≠ ∅ ∧
            ∀vs lss s.
              (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB) ∧
           ((vs,lss) = CHOICE (f2 PROB)) ∧
           (∃s. MEM s lss ∧ (snapshotPROB = snapshot PROB s)) ⇒
           P f1 f2 snapshotPROB) ∧
        (∀lvs x projPROB.
           FINITE PROB ∧ (∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB) ∧
           (lvs = f1 PROB) ∧ MEM x lvs ∧
           (∃vs. MEM vs lvs ∧ (projPROB = prob_proj (PROB,vs))) ⇒
           P f1 f2 projPROB) ⇒
        P f1 f2 PROB) ⇒
     ∀v v1 v2. P v v1 v2
hybrid_algo_gen_def
|- ∀f2 f1 PROB.
     hybrid_algo_gen f1 f2 PROB =
     if FINITE PROB then
       if ∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB then
         (let
            lvs = f1 PROB
          in
            SUM
              (MAP
                 (N_gen_curried
                    (λprojPROB.
                       if
                         ∃vs. MEM vs lvs ∧ (projPROB = prob_proj (PROB,vs))
                       then
                         hybrid_algo_gen f1 f2 projPROB
                       else 0) PROB lvs) lvs))
       else if
         f2 PROB ≠ ∅ ∧
         ∀vs lss s. (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB
       then
         (let
            (vs,lss) = CHOICE (f2 PROB)
          in
            MAX_SET
              {S_gen
                 (λsnapshotPROB.
                    if ∃s. MEM s lss ∧ (snapshotPROB = snapshot PROB s) then
                      hybrid_algo_gen f1 f2 snapshotPROB
                    else 0) vs lss PROB s' |
               s' |
               s' ∈ valid_states (prob_proj (PROB,vs))})
       else problem_plan_bound PROB
     else 0
FINITE_PROB_hybrid_algo_gen_def
|- FINITE PROB ⇒
   (hybrid_algo_gen f1 f2 PROB =
    if ∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB then
      (let
         lvs = f1 PROB
       in
         SUM
           (MAP
              (N_gen_curried
                 (λprojPROB.
                    if ∃vs. MEM vs lvs ∧ (projPROB = prob_proj (PROB,vs)) then
                      hybrid_algo_gen f1 f2 projPROB
                    else 0) PROB lvs) lvs))
    else if
      f2 PROB ≠ ∅ ∧
      ∀vs lss s. (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB
    then
      (let
         (vs,lss) = CHOICE (f2 PROB)
       in
         MAX_SET
           {S_gen
              (λsnapshotPROB.
                 if ∃s. MEM s lss ∧ (snapshotPROB = snapshot PROB s) then
                   hybrid_algo_gen f1 f2 snapshotPROB
                 else 0) vs lss PROB s' |
            s' |
            s' ∈ valid_states (prob_proj (PROB,vs))})
    else problem_plan_bound PROB)
MAP_N_gen_remove_ite
|- ∀vs lss.
     (set lss = valid_states (prob_proj (PROB,vs))) ⇒
     (MAX_SET
        {S_gen
           (λsnapshotPROB.
              if ∃s''. MEM s'' lss ∧ (snapshotPROB = snapshot PROB s'') then
                hybrid_algo_gen f1 f2 snapshotPROB
              else 0) vs lss PROB s' |
         s' |
         s' ∈ valid_states (prob_proj (PROB,vs))} =
      MAX_SET
        {S_gen (hybrid_algo_gen f1 f2) vs lss PROB s' |
         s' |
         s' ∈ valid_states (prob_proj (PROB,vs))})
FINITE_no_ite_PROB_hybrid_algo_gen_def
|- FINITE PROB ∧
   (∀vs lss.
      (vs,lss) ∈ f2 PROB ⇒ (set lss = valid_states (prob_proj (PROB,vs)))) ⇒
   (hybrid_algo_gen f1 f2 PROB =
    if ∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB then
      (let
         lvs = f1 PROB
       in
         SUM (MAP (N_gen_curried (hybrid_algo_gen f1 f2) PROB lvs) lvs))
    else if
      f2 PROB ≠ ∅ ∧
      ∀vs lss s. (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB
    then
      (let
         (vs,lss) = CHOICE (f2 PROB)
       in
         MAX_SET
           {S_gen (hybrid_algo_gen f1 f2) vs lss PROB s' |
            s' |
            s' ∈ valid_states (prob_proj (PROB,vs))})
    else problem_plan_bound PROB)
FINITE_no_ite_PROB_hybrid_algo_gen_def_thesis
|- FINITE PROB ∧
   (∀vs lss. (vs,lss) ∈ f2 PROB ⇒ sspace_DAG (prob_proj (PROB,vs)) lss) ⇒
   (hybrid_algo_gen f1 f2 PROB =
    if ∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB then
      (let
         lvs = f1 PROB
       in
         SUM (MAP (N_gen_curried (hybrid_algo_gen f1 f2) PROB lvs) lvs))
    else if
      f2 PROB ≠ ∅ ∧
      ∀vs lss s. (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB
    then
      (let
         (vs,lss) = CHOICE (f2 PROB)
       in
         MAX_SET
           {S_gen (hybrid_algo_gen f1 f2) vs lss PROB s' |
            s' |
            s' ∈ valid_states (prob_proj (PROB,vs))})
    else problem_plan_bound PROB)
recursive_hybrid_algorithm_valid_thesis
|- ∀f1 f2 PROB.
     FINITE PROB ∧
     (∀PROB'.
        dep_DAG PROB' (f1 PROB') ∧
        ∀vs lss.
          (vs,lss) ∈ f2 PROB' ⇒ sspace_DAG (prob_proj (PROB',vs)) lss) ⇒
     problem_plan_bound PROB ≤ hybrid_algo_gen f1 f2 PROB