theory TopologicalProps imports Main FactoredSystem ActionSeqProcess SetUtils begin section "Topological Properties" subsection "Basic Definitions and Properties" definition PLS_charles where "PLS_charles s as PROB ≡ {length as' | as'. (as' ∈ valid_plans PROB) ∧ (exec_plan s as' = exec_plan s as)}" definition MPLS_charles where "MPLS_charles PROB ≡ {Inf (PLS_charles (fst p) (snd p) PROB) | p. ((fst p) ∈ valid_states PROB) ∧ ((snd p) ∈ valid_plans PROB) }" ― ‹NOTE name shortened to 'problem\_plan\_bound\_charles'.› definition problem_plan_bound_charles where "problem_plan_bound_charles PROB ≡ Sup (MPLS_charles PROB)" ― ‹NOTE name shortened to 'PLS\_state'.› definition PLS_state_1 where "PLS_state_1 s as ≡ length ` {as'. (exec_plan s as' = exec_plan s as)}" ― ‹NOTE name shortened to 'MPLS\_stage\_1'.› definition MPLS_stage_1 where "MPLS_stage_1 PROB ≡ (λ (s, as). Inf (PLS_state_1 s as)) ` {(s, as). (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)} " ― ‹NOTE name shortened to 'problem\_plan\_bound\_stage\_1'.› definition problem_plan_bound_stage_1 where "problem_plan_bound_stage_1 PROB ≡ Sup (MPLS_stage_1 PROB)" for PROB :: "'a problem" ― ‹NOTE name shortened.› definition PLS where "PLS s as ≡ length ` {as'. (exec_plan s as' = exec_plan s as) ∧ (subseq as' as)}" ― ‹NOTE added lemma.› ― ‹NOTE proof finite PLS for use in 'proof in\_MPLS\_leq\_2\_pow\_n\_i'› lemma finite_PLS: "finite (PLS s as)" proof - let ?S = "{as'. (exec_plan s as' = exec_plan s as) ∧ (subseq as' as)}" let ?S1 = "length ` {as'. (exec_plan s as' = exec_plan s as) }" let ?S2 = "length ` {as'. (subseq as' as)}" let ?n = "length as + 1" have "finite ?S2" using bounded_nat_set_is_finite[where n = ?n and N = ?S2] by fastforce moreover have "length ` ?S ⊆ (?S1 ∩ ?S2)" by blast ultimately have "finite (length ` ?S)" using infinite_super by auto then show ?thesis unfolding PLS_def by blast qed ― ‹NOTE name shortened.› definition MPLS where "MPLS PROB ≡ (λ (s, as). Inf (PLS s as)) ` {(s, as). (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)} " ― ‹NOTE name shortened.› definition problem_plan_bound where "problem_plan_bound PROB ≡ Sup (MPLS PROB)" lemma expanded_problem_plan_bound_thm_1: fixes PROB shows " (problem_plan_bound PROB) = Sup ( (λ(s,as). Inf (PLS s as)) ` {(s, as). (s ∈ (valid_states PROB)) ∧ (as ∈ valid_plans PROB)} ) " unfolding problem_plan_bound_def MPLS_def by blast lemma expanded_problem_plan_bound_thm: fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set" shows " problem_plan_bound PROB = Sup ({Inf (PLS s as) | s as. (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB) }) " proof - { have "( {Inf (PLS s as) | s as. (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)} ) = ((λ(s, as). Inf (PLS s as)) ` {(s, as). (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB) }) " by fast also have "… = (λ(s, as). Inf (PLS s as)) ` ({s. fmdom' s = prob_dom PROB} × {as. set as ⊆ PROB}) " unfolding valid_states_def valid_plans_def by simp finally have " Sup ({Inf (PLS s as) | s as. (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)}) = Sup ( (λ(s, as). Inf (PLS s as)) ` ({s. fmdom' s = prob_dom PROB} × {as. set as ⊆ PROB}) ) " by argo } moreover have " problem_plan_bound PROB = Sup ((λ(s, as). Inf (PLS s as)) ` ({s. fmdom' s = prob_dom PROB} × {as. set as ⊆ PROB})) " unfolding problem_plan_bound_def MPLS_def valid_states_def valid_plans_def by fastforce ultimately show " problem_plan_bound PROB = Sup ({Inf (PLS s as) | s as. (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB) }) " by argo qed subsection "Recurrence Diameter" text ‹ The recurrence diameter---defined as the longest simple path in the digraph modelling the state space---provides a loose upper bound on the system diameter. [Abdulaziz et al., Definition 9, p.15] › ― ‹NOTE name shortened.› ― ‹NOTE 'fun' because of multiple defining equations, pattern matches.› fun valid_path where "valid_path Pi [] = True" | "valid_path Pi [s] = (s ∈ valid_states Pi)" | "valid_path Pi (s1 # s2 # rest) = ( (s1 ∈ valid_states Pi) ∧ (∃a. (a ∈ Pi) ∧ (exec_plan s1 [a] = s2)) ∧ (valid_path Pi (s2 # rest)) )" lemma valid_path_ITP2015: " (valid_path Pi [] ⟷ True) ∧ (valid_path Pi [s] ⟷ (s ∈ valid_states Pi)) ∧ (valid_path Pi (s1 # s2 # rest) ⟷ (s1 ∈ valid_states Pi) ∧ (∃a. (a ∈ Pi) ∧ (exec_plan s1 [a] = s2) ) ∧ (valid_path Pi (s2 # rest)) ) " using valid_states_def by simp ― ‹NOTE name shortened.› ― ‹NOTE second declaration skipped (declared twice in source).› definition RD where "RD Pi ≡ (Sup {length p - 1 | p. valid_path Pi p ∧ distinct p})" for Pi :: "'a problem" lemma in_PLS_leq_2_pow_n: fixes PROB :: "'a problem" and s :: "'a state" and as assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" shows "(∃x. (x ∈ PLS s as) ∧ (x ≤ (2 ^ card (prob_dom PROB)) - 1) )" proof - obtain as' where 1: "exec_plan s as = exec_plan s as'" "subseq as' as" "length as' ≤ 2 ^ card (prob_dom PROB) - 1" using assms main_lemma by blast let ?x="length as'" have "?x ∈ PLS s as" unfolding PLS_def using 1 by simp moreover have "?x ≤ 2 ^ card (prob_dom PROB) - 1" using 1(3) by blast ultimately show "(∃x. (x ∈ PLS s as) ∧ (x ≤ (2 ^ card (prob_dom PROB)) - 1) )" unfolding PLS_def by blast qed lemma in_MPLS_leq_2_pow_n: fixes PROB :: "'a problem" and x assumes "finite PROB" "(x ∈ MPLS PROB)" shows "(x ≤ 2 ^ card (prob_dom PROB) - 1)" proof - let ?mpls = "MPLS PROB" ― ‹NOTE obtain p = (s, as) where 'x = Inf (PLS s as)' from premise.› have "?mpls = (λ (s, as). Inf (PLS s as)) ` {(s, as). (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)} " using MPLS_def by blast then obtain s :: "('a, bool) fmap" and as :: "(('a, bool) fmap × ('a, bool) fmap) list" where obtain_s_as: "x ∈ ((λ (s, as). Inf (PLS s as)) ` {(s, as). (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)}) " using assms(2) by blast then have "x ∈ {Inf (PLS (fst p) (snd p)) | p. (fst p ∈ valid_states PROB) ∧ (snd p ∈ valid_plans PROB)}" using assms(1) obtain_s_as by auto then have "∃ p. x = Inf (PLS (fst p) (snd p)) ∧ (fst p ∈ valid_states PROB) ∧ (snd p ∈ valid_plans PROB)" by blast then obtain p :: "('a, bool) fmap × (('a, bool) fmap × ('a, bool) fmap) list" where obtain_p: "x = Inf (PLS (fst p) (snd p))" "(fst p ∈ valid_states PROB)" "(snd p ∈ valid_plans PROB)" by blast then have "fst p ∈ valid_states PROB" "snd p ∈ valid_plans PROB" using obtain_p by blast+ then obtain x' :: nat where obtain_x': "x' ∈ PLS (fst p) (snd p) ∧ x' ≤ 2 ^ card (prob_dom PROB) - 1" using assms(1) in_PLS_leq_2_pow_n[where s = "fst p" and as = "snd p"] by blast then have 1: "x' ≤ 2 ^ card (prob_dom PROB) - 1" "x' ∈ PLS (fst p) (snd p)" "x = Inf (PLS (fst p) (snd p))" "finite (PLS (fst p) (snd p))" using obtain_x' obtain_p finite_PLS by blast+ moreover have "x ≤ x'" using 1(2, 4) obtain_p(1) cInf_le_finite by blast ultimately show "(x ≤ 2 ^ card (prob_dom PROB) - 1)" by linarith qed lemma FINITE_MPLS: assumes "finite (Pi :: 'a problem)" shows "finite (MPLS Pi)" proof - have "∀x ∈ MPLS Pi. x ≤ 2 ^ card (prob_dom Pi) - 1" using assms in_MPLS_leq_2_pow_n by blast then show "finite (MPLS Pi)" using mems_le_finite[of "MPLS Pi" "2 ^ card (prob_dom Pi) - 1"] by blast qed ― ‹NOTE 'fun' because of multiple defining equations.› fun statelist' where "statelist' s [] = [s]" | "statelist' s (a # as) = (s # statelist' (state_succ s a) as)" lemma LENGTH_statelist': fixes as s shows "length (statelist' s as) = (length as + 1)" by (induction as arbitrary: s) auto lemma valid_path_statelist': fixes as and s :: "('a, 'b) fmap" assumes "(as ∈ valid_plans Pi)" "(s ∈ valid_states Pi)" shows "(valid_path Pi (statelist' s as))" using assms proof (induction as arbitrary: s Pi) case cons: (Cons a as) then have 1: "a ∈ Pi" "as ∈ valid_plans Pi" using valid_plan_valid_head valid_plan_valid_tail by metis+ then show ?case proof (cases as) case Nil { have "state_succ s a ∈ valid_states Pi" using 1 cons.prems(2) valid_action_valid_succ by blast then have "valid_path Pi [state_succ s a]" using 1 cons.prems(2) cons.IH by force moreover have "(∃aa. aa ∈ Pi ∧ exec_plan s [aa] = state_succ s a)" using 1(1) by fastforce ultimately have "valid_path Pi (statelist' s [a])" using cons.prems(2) by simp } then show ?thesis using Nil by blast next case (Cons b list) { have "s ∈ valid_states Pi" using cons.prems(2) by simp ― ‹TODO this step is inefficient (~5s).› then have "valid_path Pi (state_succ s a # statelist' (state_succ (state_succ s a) b) list)" using 1 cons.IH cons.prems(2) Cons lemma_1_i by fastforce moreover have "(∃aa b. (aa, b) ∈ Pi ∧ state_succ s (aa, b) = state_succ s a)" using 1(1) surjective_pairing by metis ultimately have "valid_path Pi (statelist' s (a # b # list))" using cons.prems(2) by auto } then show ?thesis using Cons by blast qed qed simp ― ‹TODO explicit proof.› lemma statelist'_exec_plan: fixes a s p assumes "(statelist' s as = p)" shows "(exec_plan s as = last p)" using assms apply(induction as arbitrary: s p) apply(auto) apply(cases "as") by (metis LENGTH_statelist' One_nat_def add_Suc_right list.size(3) nat.simps(3)) (metis (no_types) LENGTH_statelist' One_nat_def add_Suc_right list.size(3) nat.simps(3)) lemma statelist'_EQ_NIL: "statelist' s as ≠ []" by (cases as) auto ― ‹NOTE added lemma.› lemma statelist'_TAKE_i: assumes "Suc m ≤ length (a # as)" shows "m ≤ length as" using assms by (induction as arbitrary: a m) auto lemma statelist'_TAKE: fixes as s p assumes "(statelist' s as = p)" shows "(∀n. n ≤ length as ⟶ (exec_plan s (take n as)) = (p ! n))" using assms proof (induction as arbitrary: s p) case Nil { fix n assume P1: "n ≤ length []" then have "exec_plan s (take n []) = s" by simp moreover have "p ! 0 = s" using Nil.prems by force ultimately have "exec_plan s (take n []) = p ! n" using P1 by simp } then show ?case by blast next case (Cons a as) { fix n assume P2: "n ≤ length (a # as)" then have "exec_plan s (take n (a # as)) = p ! n" using Cons.prems proof (cases "n = 0") case False then obtain m where a: "n = Suc m" using not0_implies_Suc by presburger moreover have b: "statelist' s (a # as) ! n = statelist' (state_succ s a) as ! m" using a nth_Cons_Suc by simp moreover have c: "exec_plan s (take n (a # as)) = exec_plan (state_succ s a) (take m as)" using a by force moreover have "m ≤ length as" using a P2 statelist'_TAKE_i by simp moreover have "exec_plan (state_succ s a) (take m as) = statelist' (state_succ s a) as ! m" using calculation(2, 3, 4) Cons.IH by blast ultimately show ?thesis using Cons.prems by argo qed fastforce } then show ?case by blast qed lemma MPLS_nempty: fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set" assumes "finite PROB" shows "MPLS PROB ≠ {}" proof - let ?S="{(s, as). s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}" ― ‹NOTE type of 's' had to be fixed for 'valid\_states\_nempty'.› obtain s :: "('a, 'b) fmap" where "s ∈ valid_states PROB" using assms valid_states_nempty by blast moreover have "[] ∈ valid_plans PROB" using empty_plan_is_valid by auto ultimately have "(s, []) ∈ ?S" by blast then show ?thesis unfolding MPLS_def by blast qed theorem bound_main_lemma: fixes PROB :: "'a problem" assumes "finite PROB" shows "(problem_plan_bound PROB ≤ (2 ^ (card (prob_dom PROB))) - 1)" proof - have "MPLS PROB ≠ {}" using assms MPLS_nempty by auto moreover have "(∀x. x ∈ MPLS PROB ⟶ x ≤ 2 ^ card (prob_dom PROB) - 1)" using assms in_MPLS_leq_2_pow_n by blast ultimately show ?thesis unfolding problem_plan_bound_def using cSup_least by blast qed ― ‹NOTE types in premise had to be fixed to be able to match `valid\_as\_valid\_exec`.› lemma bound_child_parent_card_state_set_cons: fixes P f assumes "(∀(PROB :: 'a problem) as (s :: 'a state). (P PROB) ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB) ) )" shows "(∀PROB s as. (P PROB) ∧ (as ∈ valid_plans PROB) ∧ (s ∈ (valid_states PROB)) ⟶ (∃x. (x ∈ PLS s as) ∧ (x < f PROB) ) )" proof - { fix PROB :: "'a problem" and as and s :: "'a state" assume P1: "(P PROB)" "(as ∈ valid_plans PROB)" "(s ∈ valid_states PROB)" "(∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB) )" have "(exec_plan s as ∈ valid_states PROB)" using assms P1 valid_as_valid_exec by blast then have "(P PROB) ∧ (as ∈ valid_plans PROB) ∧ (s ∈ (valid_states PROB)) ⟶ (∃x. (x ∈ PLS s as) ∧ (x < f PROB) ) " unfolding PLS_def using P1 by force } then show "(∀PROB s as. (P PROB) ∧ (as ∈ valid_plans PROB) ∧ (s ∈ (valid_states PROB)) ⟶ (∃x. (x ∈ PLS s as) ∧ (x < f PROB) ) )" using assms by simp qed ― ‹NOTE types of premise had to be fixed to be able to use lemma `bound\_child\_parent\_card\_state\_set\_cons`.› lemma bound_on_all_plans_bounds_MPLS: fixes P f assumes "(∀(PROB :: 'a problem) as (s :: 'a state). (P PROB) ∧ (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB) ) )" shows "(∀PROB x. P PROB ⟶ (x ∈ MPLS(PROB)) ⟶ (x < f PROB) )" proof - { fix PROB :: "'a problem" and as and s :: "'a state" assume "(P PROB)" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "(∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB) )" then have "(∃x. x ∈ PLS s as ∧ x < f PROB)" using assms(1) bound_child_parent_card_state_set_cons[where P = P and f = f] by presburger } note 1 = this { fix PROB x assume P1: "P PROB" "x ∈ MPLS PROB" ― ‹TODO refactor 'x\_in\_MPLS\_if' and use here.› then obtain s as where a: "x = Inf (PLS s as)" "s ∈ valid_states PROB" "as ∈ valid_plans PROB" unfolding MPLS_def by auto moreover have "(∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB) )" using P1(1) assms calculation(2, 3) by blast ultimately obtain x' where "x' ∈ PLS s as" "x' < f PROB" using P1 1 by blast then have "x < f PROB" using a(1) mem_lt_imp_MIN_lt by fastforce } then show ?thesis by blast qed lemma bound_child_parent_card_state_set_cons_finite: fixes P f assumes "(∀PROB as s. P PROB ∧ finite PROB ∧ as ∈ (valid_plans PROB) ∧ s ∈ (valid_states PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ subseq as' as ∧ length as' < f(PROB) ) )" shows "(∀PROB s as. P PROB ∧ finite PROB ∧ as ∈ (valid_plans PROB) ∧ (s ∈ (valid_states PROB)) ⟶ (∃x. (x ∈ PLS s as) ∧ x < f PROB) )" proof - { fix PROB s as assume "P PROB" "finite PROB" "as ∈ (valid_plans PROB)" "s ∈ (valid_states PROB)" " (∃as'. (exec_plan s as = exec_plan s as') ∧ subseq as' as ∧ length as' < f PROB )" (* NOTE[1] moreover have "exec_plan s as ∈ valid_states PROB" using calculation valid_as_valid_exec by blast *) then obtain as' where "(exec_plan s as = exec_plan s as')" "subseq as' as" "length as' < f PROB" by blast moreover have "length as' ∈ PLS s as" unfolding PLS_def using calculation by fastforce ultimately have "(∃x. (x ∈ PLS s as) ∧ x < f PROB)" by blast } then show "(∀PROB s as. P PROB ∧ finite PROB ∧ as ∈ (valid_plans PROB) ∧ (s ∈ (valid_states PROB)) ⟶ (∃x. (x ∈ PLS s as) ∧ x < f PROB) )" using assms by auto qed lemma bound_on_all_plans_bounds_MPLS_finite: fixes P f assumes "(∀PROB as s. P PROB ∧ finite PROB ∧ s ∈ (valid_states PROB) ∧ as ∈ (valid_plans PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ subseq as' as ∧ length as' < f(PROB) ) )" shows "(∀PROB x. P PROB ∧ finite PROB ⟶ (x ∈ MPLS PROB) ⟶ x < f PROB )" proof - { fix PROB x assume P1: "P PROB" "finite PROB" "x ∈ MPLS PROB" ― ‹TODO refactor 'x\_in\_MPLS\_if' and use here.› then obtain s as where a: "x = Inf (PLS s as)" "s ∈ valid_states PROB" "as ∈ valid_plans PROB" unfolding MPLS_def by auto moreover have "(∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB) )" using P1(1, 2) assms calculation(2, 3) by blast moreover obtain x' where "x' ∈ PLS s as" "x' < f PROB" using PLS_def calculation(4) by fastforce then have "x < f PROB" using a(1) mem_lt_imp_MIN_lt by fastforce } then show ?thesis using assms by blast qed lemma bound_on_all_plans_bounds_problem_plan_bound: fixes P f assumes "(∀PROB as s. (P PROB) ∧ finite PROB ∧ (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB) ) )" shows "(∀PROB. (P PROB) ∧ finite PROB ⟶ (problem_plan_bound PROB < f PROB) )" proof - have 1: "∀PROB x. P PROB ∧ finite PROB ⟶ x ∈ MPLS PROB ⟶ x < f PROB " using assms bound_on_all_plans_bounds_MPLS_finite by blast { fix PROB x assume "P PROB ∧ finite PROB ⟶ x ∈ MPLS PROB ⟶ x < f PROB " then have "∀PROB. P PROB ∧ finite PROB ⟶ problem_plan_bound PROB < f PROB " unfolding problem_plan_bound_def using 1 bound_child_parent_not_eq_last_diff_paths 1 MPLS_nempty by metis then have "∀PROB. P PROB ∧ finite PROB ⟶ problem_plan_bound PROB < f PROB " using MPLS_nempty by blast } then show "(∀PROB. (P PROB) ∧ finite PROB ⟶ (problem_plan_bound PROB < f PROB) )" using 1 by blast qed lemma bound_child_parent_card_state_set_cons_thesis: assumes "finite PROB" "(∀as s. as ∈ (valid_plans PROB) ∧ s ∈ (valid_states PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ subseq as' as ∧ length as' < k ) )" "as ∈ (valid_plans PROB)" "(s ∈ (valid_states PROB))" shows "(∃x. (x ∈ PLS s as) ∧ x < k)" unfolding PLS_def using assms by fastforce ― ‹NOTE added lemma.› ― ‹TODO refactor/move up.› lemma x_in_MPLS_if: fixes x PROB assumes "x ∈ MPLS PROB" shows "∃s as. s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧ x = Inf (PLS s as)" using assms unfolding MPLS_def by fast lemma bound_on_all_plans_bounds_MPLS_thesis: assumes "finite PROB" "(∀as s. (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < k) ) )" "(x ∈ MPLS PROB)" shows "(x < k)" proof - obtain s as where 1: "s ∈ valid_states PROB" "as ∈ valid_plans PROB" "x = Inf (PLS s as)" using assms(3) x_in_MPLS_if by blast then obtain x' :: nat where "x' ∈ PLS s as" "x' < k" using assms(1, 2) bound_child_parent_card_state_set_cons_thesis by blast then have "Inf (PLS s as) < k" using mem_lt_imp_MIN_lt by blast then show "x < k" using 1 by simp qed ― ‹NOTE added lemma.› lemma bounded_MPLS_contains_supremum: fixes PROB assumes "finite PROB" "(∃k. ∀x ∈ MPLS PROB. x < k)" shows "Sup (MPLS PROB) ∈ MPLS PROB" proof - obtain k where "∀x ∈ MPLS PROB. x < k" using assms(2) by blast moreover have "finite (MPLS PROB)" using assms(2) finite_nat_set_iff_bounded by presburger moreover have "MPLS PROB ≠ {}" using assms(1) MPLS_nempty by auto ultimately show "Sup (MPLS PROB) ∈ MPLS PROB" unfolding Sup_nat_def by simp qed lemma bound_on_all_plans_bounds_problem_plan_bound_thesis': assumes "finite PROB" "(∀as s. s ∈ (valid_states PROB) ∧ as ∈ (valid_plans PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ subseq as' as ∧ length as' < k ) )" shows "problem_plan_bound PROB < k" proof - have 1: "∀x ∈ MPLS PROB. x < k" using assms(1, 2) bound_on_all_plans_bounds_MPLS_thesis by blast then have "Sup (MPLS PROB) ∈ MPLS PROB" using assms(1) bounded_MPLS_contains_supremum by auto then have "Sup (MPLS PROB) < k" using 1 by blast then show ?thesis unfolding problem_plan_bound_def by simp qed lemma bound_on_all_plans_bounds_problem_plan_bound_thesis: assumes "finite PROB" "(∀as s. (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' ≤ k) ) )" shows "(problem_plan_bound PROB ≤ k)" proof - have 1: "∀x∈MPLS PROB. x < k + 1" using assms(1, 2) bound_on_all_plans_bounds_MPLS_thesis[where k = "k + 1"] Suc_eq_plus1 less_Suc_eq_le by metis then have "Sup (MPLS PROB) ∈ MPLS PROB" using assms(1) bounded_MPLS_contains_supremum by fast then show "(problem_plan_bound PROB ≤ k)" unfolding problem_plan_bound_def using 1 by fastforce qed lemma bound_on_all_plans_bounds_problem_plan_bound_: fixes P f PROB assumes "(∀PROB' as s. finite PROB ∧ (P PROB') ∧ (s ∈ valid_states PROB') ∧ (as ∈ valid_plans PROB') ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB') ) )" "(P PROB)" "finite PROB" shows "(problem_plan_bound PROB < f PROB)" unfolding problem_plan_bound_def MPLS_def using assms bound_on_all_plans_bounds_problem_plan_bound_thesis' expanded_problem_plan_bound_thm_1 by metis lemma S_VALID_AS_VALID_IMP_MIN_IN_PLS: fixes PROB s as assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" shows "(Inf (PLS s as) ∈ (MPLS PROB))" unfolding MPLS_def using assms by fast ― ‹NOTE type of `s` had to be fixed (type mismatch in goal).› ― ‹NOTE premises rewritten to implications for proof set up.› lemma problem_plan_bound_ge_min_pls: fixes PROB :: "'a problem" and s :: "'a state" and as k assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "(problem_plan_bound PROB ≤ k)" shows "(Inf (PLS s as) ≤ problem_plan_bound PROB)" proof - have "Inf (PLS s as) ∈ MPLS PROB" using assms(2, 3) S_VALID_AS_VALID_IMP_MIN_IN_PLS by blast moreover have "finite (MPLS PROB)" using assms(1) FINITE_MPLS by blast ultimately have "Inf (PLS s as) ≤ Sup (MPLS PROB)" using le_cSup_finite by blast then show ?thesis unfolding problem_plan_bound_def by simp qed lemma PLS_NEMPTY: fixes s as shows "PLS s as ≠ {}" unfolding PLS_def by blast lemma PLS_nempty_and_has_min: fixes s as shows "(∃x. (x ∈ PLS s as) ∧ (x = Inf (PLS s as)))" proof - have "PLS s as ≠ {}" using PLS_NEMPTY by blast then have "Inf (PLS s as) ∈ PLS s as" unfolding Inf_nat_def using LeastI_ex Max_in finite_PLS by metis then show ?thesis by blast qed lemma PLS_works: fixes x s as assumes "(x ∈ PLS s as)" shows"(∃as'. (exec_plan s as = exec_plan s as') ∧ (length as' = x) ∧ (subseq as' as) )" using assms unfolding PLS_def by (smt imageE mem_Collect_eq) ― ‹NOTE type of `s` had to be fixed (type mismatch in goal).› lemma problem_plan_bound_works: fixes PROB :: "'a problem" and as and s :: "'a state" assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" shows "(∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' ≤ problem_plan_bound PROB) )" proof - have "problem_plan_bound PROB ≤ 2 ^ card (prob_dom PROB) - 1" using assms(1) bound_main_lemma by blast then have 1: "Inf (PLS s as) ≤ problem_plan_bound PROB" using assms(1, 2, 3) problem_plan_bound_ge_min_pls by blast then have "∃x. x ∈ PLS s as ∧ x = Inf (PLS s as)" using PLS_nempty_and_has_min by blast then have "Inf (PLS s as) ∈ (PLS s as)" by blast then obtain as' where 2: "exec_plan s as = exec_plan s as'" "length as' = Inf (PLS s as)" "subseq as' as" using PLS_works by blast then have "length as' ≤ problem_plan_bound PROB" using 1 by argo then show "(∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' ≤ problem_plan_bound PROB) )" using 2(1) 2(3) by blast qed ― ‹NOTE name shortened.› definition MPLS_s where "MPLS_s PROB s ≡ (λ (s, as). Inf (PLS s as)) ` {(s, as) | as. as ∈ valid_plans PROB}" ― ‹NOTE type of `PROB` had to be fixed (type mismatch in goal).› lemma bound_main_lemma_s_3: fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set" and s shows "MPLS_s PROB s ≠ {}" proof - ― ‹TODO @{term "(s, []) ∈ {}"} could be refactored (this is used in 'MPLS\_nempty' too).› have "[] ∈ valid_plans PROB" using empty_plan_is_valid by blast then have "(s, []) ∈ {(s, as). as ∈ valid_plans PROB}" by simp then show "MPLS_s PROB s ≠ {}" unfolding MPLS_s_def by blast qed ― ‹NOTE name shortened.› definition problem_plan_bound_s where "problem_plan_bound_s PROB s = Sup (MPLS_s PROB s)" ― ‹NOTE removed typing from assumption due to matching problems in later proofs.› lemma bound_on_all_plans_bounds_PLS_s: fixes P f assumes "(∀PROB as s. finite PROB ∧ (P PROB) ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB s) ) )" shows "(∀PROB s as. finite PROB ∧ (P PROB) ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB) ⟶ (∃x. (x ∈ PLS s as) ∧ (x < f PROB s) ) )" using assms unfolding PLS_def by fastforce ― ‹NOTE added lemma.› lemma bound_on_all_plans_bounds_MPLS_s_i: fixes PROB s x assumes "s ∈ valid_states PROB" "x ∈ MPLS_s PROB s" shows "∃as. x = Inf (PLS s as) ∧ as ∈ valid_plans PROB" proof - let ?S="{(s, as) | as. as ∈ valid_plans PROB}" obtain x' where 1: "x' ∈ ?S" "x = (λ (s, as). Inf (PLS s as)) x'" using assms unfolding MPLS_s_def by blast let ?as="snd x'" let ?s="fst x'" have "?as ∈ valid_plans PROB" using 1(1) by auto moreover have "?s = s" using 1(1) by fastforce moreover have "x = Inf (PLS ?s ?as)" using 1(2) by (simp add: case_prod_unfold) ultimately show ?thesis by blast qed lemma bound_on_all_plans_bounds_MPLS_s: fixes P f assumes "(∀PROB as s. finite PROB ∧ (P PROB) ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB s) ) )" shows "(∀PROB x s. finite PROB ∧ (P PROB) ∧ (s ∈ valid_states PROB) ⟶ (x ∈ MPLS_s PROB s) ⟶ (x < f PROB s) )" using assms unfolding MPLS_def proof - have 1: "∀PROB s as. finite PROB ∧ P PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⟶ (∃x. x ∈ PLS s as ∧ x < f PROB s)" using bound_on_all_plans_bounds_PLS_s[OF assms] . { fix PROB x and s :: "('a, 'b) fmap" assume P1: "finite PROB" "(P PROB)" "(s ∈ valid_states PROB)" { assume "(x ∈ MPLS_s PROB s)" then obtain as where i: "x = Inf (PLS s as)" "as ∈ valid_plans PROB" using P1 bound_on_all_plans_bounds_MPLS_s_i by blast then obtain x' where "x' ∈ PLS s as" "x' < f PROB s" using P1 i 1 by blast then have "x < f PROB s" using mem_lt_imp_MIN_lt i(1) by blast } then have "(x ∈ MPLS_s PROB s) ⟶ (x < f PROB s)" by blast } then show ?thesis by blast qed ― ‹NOTE added lemma.› lemma Sup_MPLS_s_lt_if: fixes PROB s k assumes "(∀x∈MPLS_s PROB s. x < k)" shows "Sup (MPLS_s PROB s) < k" proof - have "MPLS_s PROB s ≠ {}" using bound_main_lemma_s_3 by fast then have "Sup (MPLS_s PROB s) ∈ MPLS_s PROB s" using assms Sup_nat_def bounded_nat_set_is_finite by force then show "Sup (MPLS_s PROB s) < k" using assms by blast qed ― ‹NOTE type of `P` had to be fixed (type mismatch in goal).› lemma bound_child_parent_lemma_s_2: fixes PROB :: "'a problem" and P :: "'a problem ⇒ bool" and s f assumes "(∀(PROB :: 'a problem) as s. finite PROB ∧ (P PROB) ∧ (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB s) ) )" shows "( finite PROB ∧ (P PROB) ∧ (s ∈ valid_states PROB) ⟶ problem_plan_bound_s PROB s < f PROB s )" proof - ― ‹NOTE manual instantiation is required (automation fails otherwise).› have "∀(PROB :: 'a problem) x s. finite PROB ∧ P PROB ∧ s ∈ valid_states PROB ⟶ x ∈ MPLS_s PROB s ⟶ x < f PROB s " using assms bound_on_all_plans_bounds_MPLS_s[of P f] by simp then show "finite PROB ∧ (P PROB) ∧ (s ∈ valid_states PROB) ⟶ (problem_plan_bound_s PROB s < f PROB s)" unfolding problem_plan_bound_s_def using Sup_MPLS_s_lt_if problem_plan_bound_s_def by metis qed theorem bound_main_lemma_reachability_s: fixes PROB :: "'a problem" and s assumes "finite PROB" "s ∈ valid_states PROB" shows "(problem_plan_bound_s PROB s < card (reachable_s PROB s))" proof - ― ‹NOTE derive premise for MP of 'bound\_child\_parent\_lemma\_s\_2'.› ― ‹NOTE type of `s` had to be fixed (warning in assumption declaration).› { fix PROB :: "'a problem" and s :: "'a state" and as assume P1: "finite PROB" "s ∈ valid_states PROB" "as ∈ valid_plans PROB" then obtain as' where a: "exec_plan s as = exec_plan s as'" "subseq as' as" "length as' ≤ card (reachable_s PROB s) - 1" using P1 main_lemma_reachability_s by blast then have "length as' < card (reachable_s PROB s)" using P1(1, 2) card_reachable_s_non_zero by fastforce then have "(∃as'. exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' < card (reachable_s PROB s)) " using a by blast } then have " finite PROB ∧ True ∧ s ∈ valid_states PROB ⟶ problem_plan_bound_s PROB s < card (reachable_s PROB s) " using bound_child_parent_lemma_s_2[where PROB = PROB and P = "λ_. True" and s = s and f = "λPROB s. card (reachable_s PROB s)"] by blast then show ?thesis using assms(1, 2) by blast qed lemma problem_plan_bound_s_LESS_EQ_problem_plan_bound_thm: fixes PROB :: "'a problem" and s :: "'a state" assumes "finite PROB" "(s ∈ valid_states PROB)" shows "(problem_plan_bound_s PROB s < problem_plan_bound PROB + 1)" proof - { fix PROB :: "'a problem" and s :: "'a state" and as assume "finite PROB" "s ∈ valid_states PROB" "as ∈ valid_plans PROB" then obtain as' where a: "exec_plan s as = exec_plan s as'" "subseq as' as" "length as' ≤ problem_plan_bound PROB" using problem_plan_bound_works by blast then have "length as' < problem_plan_bound PROB + 1" by linarith then have "∃as'. exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' ≤ problem_plan_bound PROB + 1 " using a by fastforce } ― ‹TODO unsure why a proof is needed at all here.› then have "∀(PROB :: 'a problem) as s. finite PROB ∧ True ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⟶ (∃as'. exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' < problem_plan_bound PROB + 1) " by (metis Suc_eq_plus1 problem_plan_bound_works le_imp_less_Suc) then show "(problem_plan_bound_s PROB s < problem_plan_bound PROB + 1)" using assms bound_child_parent_lemma_s_2[where PROB = PROB and s = s and P = "λ_. True" and f = "λPROB s. problem_plan_bound PROB + 1"] by fast qed ― ‹NOTE lemma `bound\_main\_lemma\_s\_1` skipped (this is being equivalently redeclared later).› lemma AS_VALID_MPLS_VALID: fixes PROB as assumes "(as ∈ valid_plans PROB)" shows "(Inf (PLS s as) ∈ MPLS_s PROB s)" using assms unfolding MPLS_s_def by fast ― ‹NOTE moved up because it's used in the following lemma.› ― ‹NOTE type of `s` had to be fixed for 'in\_PLS\_leq\_2\_pow\_n'.› lemma bound_main_lemma_s_1: fixes PROB :: "'a problem" and s :: "'a state" and x assumes "finite PROB" "s ∈ (valid_states PROB)" "x ∈ MPLS_s PROB s" shows "(x ≤ (2 ^ card (prob_dom PROB)) - 1)" proof - obtain as :: "(('a, bool) fmap × ('a, bool) fmap) list" where "as ∈ valid_plans PROB" using empty_plan_is_valid by blast then obtain x where 1: "x ∈ PLS s as" "x ≤ 2 ^ card (prob_dom PROB) - 1" using assms in_PLS_leq_2_pow_n by blast then have "Inf (PLS s as) ≤ 2 ^ card (prob_dom PROB) - 1" using mem_le_imp_MIN_le[where s = "PLS s as" and k = "2 ^ card (prob_dom PROB) - 1"] by blast then have "x ≤ 2 ^ card (prob_dom PROB) - 1" using assms(3) 1 by blast ― ‹TODO unsure why a proof is needed here (typing problem?).› then show ?thesis using assms(1, 2, 3) S_VALID_AS_VALID_IMP_MIN_IN_PLS bound_on_all_plans_bounds_MPLS_s_i in_MPLS_leq_2_pow_n by metis qed lemma problem_plan_bound_s_ge_min_pls: fixes PROB :: "'a problem" and as k s assumes "finite PROB" "s ∈ (valid_states PROB)" "as ∈ (valid_plans PROB)" "problem_plan_bound_s PROB s ≤ k" shows "(Inf (PLS s as) ≤ problem_plan_bound_s PROB s)" proof - have "∀x∈MPLS_s PROB s. x ≤ 2 ^ card (prob_dom PROB) - 1" using assms(1, 2) bound_main_lemma_s_1 by blast then have 1: "finite (MPLS_s PROB s)" using mems_le_finite[where s = "MPLS_s PROB s" and k = "2 ^ card (prob_dom PROB) - 1"] by blast then have "MPLS_s PROB s ≠ {}" using bound_main_lemma_s_3 by fast then have "Inf (PLS s as) ∈ MPLS_s PROB s" using assms AS_VALID_MPLS_VALID by blast then show "(Inf (PLS s as) ≤ problem_plan_bound_s PROB s)" unfolding problem_plan_bound_s_def using 1 le_cSup_finite by blast qed theorem bound_main_lemma_s: fixes PROB :: "'a problem" and s assumes "finite PROB" "(s ∈ valid_states PROB)" shows "(problem_plan_bound_s PROB s ≤ 2 ^ (card (prob_dom PROB)) - 1)" proof - have 1: "∀x∈MPLS_s PROB s. x ≤ 2 ^ card (prob_dom PROB) - 1" using assms bound_main_lemma_s_1 by metis then have "MPLS_s PROB s ≠ {}" using bound_main_lemma_s_3 by fast then have "Sup (MPLS_s PROB s) ≤ 2 ^ card (prob_dom PROB) - 1" using 1 bound_main_lemma_2[where s = "MPLS_s PROB s" and k = "2 ^ card (prob_dom PROB) - 1"] by blast then show "problem_plan_bound_s PROB s ≤ 2 ^ card (prob_dom PROB) - 1" unfolding problem_plan_bound_s_def by blast qed lemma problem_plan_bound_s_works: fixes PROB :: "'a problem" and as s assumes "finite PROB" "(as ∈ valid_plans PROB)" "(s ∈ valid_states PROB)" shows "(∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' ≤ problem_plan_bound_s PROB s) )" proof - have "problem_plan_bound_s PROB s ≤ 2 ^ card (prob_dom PROB) - 1" using assms(1, 3) bound_main_lemma_s by blast then have 1: "Inf (PLS s as) ≤ problem_plan_bound_s PROB s" using assms problem_plan_bound_s_ge_min_pls[of PROB s as " 2 ^ card (prob_dom PROB) - 1"] by blast then obtain x where obtain_x: "x ∈ PLS s as ∧ x = Inf (PLS s as)" using PLS_nempty_and_has_min by blast then have "∃as'. exec_plan s as = exec_plan s as' ∧ length as' = Inf (PLS s as) ∧ subseq as' as" using PLS_works[where s = s and as = as and x = "Inf (PLS s as)"] obtain_x by fastforce then show "(∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' ≤ problem_plan_bound_s PROB s) )" using 1 by metis qed ― ‹NOTE skipped second declaration (declared twice in source).› lemma PLS_def_ITP2015: fixes s as shows "PLS s as = {length as' | as'. (exec_plan s as' = exec_plan s as) ∧ (subseq as' as)}" using PLS_def by blast ― ‹NOTE Set comprehension had to be rewritten to image (there is no pattern matching in the part left of the pipe symbol).› lemma expanded_problem_plan_bound_charles_thm: fixes PROB :: "'a problem" shows " problem_plan_bound_charles PROB = Sup ( { Inf (PLS_charles (fst p) (snd p) PROB) | p. (fst p ∈ valid_states PROB) ∧ (snd p ∈ valid_plans PROB)}) " unfolding problem_plan_bound_charles_def MPLS_charles_def by blast lemma bound_main_lemma_charles_3: fixes PROB :: "'a problem" assumes "finite PROB" shows "MPLS_charles PROB ≠ {}" proof - have 1: "[] ∈ valid_plans PROB" using empty_plan_is_valid by auto then obtain s :: "'a state" where obtain_s: "s ∈ valid_states PROB" using assms valid_states_nempty by auto then have "Inf (PLS_charles s [] PROB) ∈ MPLS_charles PROB" unfolding MPLS_charles_def using 1 by auto then show "MPLS_charles PROB ≠ {}" by blast qed lemma in_PLS_charles_leq_2_pow_n: fixes PROB :: "'a problem" and s as assumes "finite PROB" "s ∈ valid_states PROB" "as ∈ valid_plans PROB" shows "(∃x. (x ∈ PLS_charles s as PROB) ∧ (x ≤ 2 ^ card (prob_dom PROB) - 1)) " proof - obtain as' where 1: "exec_plan s as = exec_plan s as'" "subseq as' as" "length as' ≤ 2 ^ card (prob_dom PROB) - 1" using assms main_lemma by blast then have "as' ∈ valid_plans PROB" using assms(3) sublist_valid_plan by blast then have "length as' ∈ PLS_charles s as PROB" unfolding PLS_charles_def using 1 by auto then show ?thesis using 1(3) by fast qed ― ‹NOTE added lemma.› ― ‹NOTE this lemma retrieves `s`, `as` for a given @{term "x ∈ MPLS_charles PROB"} and characterizes it as the minimum of 'PLS\_charles s as PROB'.› lemma x_in_MPLS_charles_then: fixes PROB s as assumes "x ∈ MPLS_charles PROB" shows "∃s as. s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧ x = Inf (PLS_charles s as PROB) " proof - have "∃p ∈ {p. (fst p) ∈ valid_states PROB ∧ (snd p) ∈ valid_plans PROB}. x = Inf (PLS_charles (fst p) (snd p) PROB)" using MPLS_charles_def assms by fast then obtain p where 1: "p ∈ {p. (fst p) ∈ valid_states PROB ∧ (snd p) ∈ valid_plans PROB}" "x = Inf (PLS_charles (fst p) (snd p) PROB)" by blast then have "fst p ∈ valid_states PROB" "snd p ∈ valid_plans PROB" by blast+ then show ?thesis using 1 by fast qed lemma in_MPLS_charles_leq_2_pow_n: fixes PROB :: "'a problem" and x assumes "finite PROB" "x ∈ MPLS_charles PROB" shows "x ≤ 2 ^ card (prob_dom PROB) - 1" proof - obtain s as where 1: "s ∈ valid_states PROB" "as ∈ valid_plans PROB" "x = Inf (PLS_charles s as PROB)" using assms(2) x_in_MPLS_charles_then by blast then obtain x' where 2: "x' ∈ PLS_charles s as PROB""x' ≤ 2 ^ card (prob_dom PROB) - 1" using assms(1) in_PLS_charles_leq_2_pow_n by blast then have "x ≤ x'" using 1(3) mem_le_imp_MIN_le by blast then show ?thesis using 1 2 by linarith qed lemma bound_main_lemma_charles: fixes PROB :: "'a problem" assumes "finite PROB" shows "problem_plan_bound_charles PROB ≤ 2 ^ (card (prob_dom PROB)) - 1" proof - have 1: "∀x∈MPLS_charles PROB. x ≤ 2 ^ (card (prob_dom PROB)) - 1" using assms in_MPLS_charles_leq_2_pow_n by blast then have "MPLS_charles PROB ≠ {}" using assms bound_main_lemma_charles_3 by blast then have "Sup (MPLS_charles PROB) ≤ 2 ^ (card (prob_dom PROB)) - 1" using 1 bound_main_lemma_2 by meson then show ?thesis using problem_plan_bound_charles_def by metis qed lemma bound_on_all_plans_bounds_PLS_charles: fixes P and f assumes "∀(PROB :: 'a problem) as s. (P PROB) ∧ finite PROB ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as)∧ (length as' < f PROB)) " shows "(∀PROB s as. (P PROB) ∧ finite PROB ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB) ⟶ (∃x. (x ∈ PLS_charles s as PROB) ∧ (x < f PROB))) " proof - { ― ‹NOTE type for 's' had to be fixed (type mismatch in first proof step.› fix PROB :: "'a problem" and as and s :: "'a state" assume P: "P PROB" "finite PROB" "as ∈ valid_plans PROB" "s ∈ valid_states PROB" "(∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB) )" then obtain as' where 1: "(exec_plan s as = exec_plan s as')" "(subseq as' as)" "(length as' < f PROB)" using P(5) by blast then have 2: "as' ∈ valid_plans PROB" using P(3) sublist_valid_plan by blast let ?x = "length as'" have "?x ∈ PLS_charles s as PROB" unfolding PLS_charles_def using 1 2 by auto then have "∃x. x ∈ PLS_charles s as PROB ∧ x < f PROB" using 1 2 by blast } then show ?thesis using assms by auto qed ― ‹NOTE added lemma (refactored from `bound\_on\_all\_plans\_bounds\_MPLS\_charles`).› lemma bound_on_all_plans_bounds_MPLS_charles_i: assumes "∀(PROB :: 'a problem) s as. (P PROB) ∧ finite PROB ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB)) " shows "∀(PROB :: 'a problem) s as. P PROB ∧ finite PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⟶ Inf {n. n ∈ PLS_charles s as PROB} < f PROB " proof - { fix PROB :: "'a problem" and s as have "P PROB ∧ finite PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⟶ (∃x. x ∈ PLS_charles s as PROB ∧ x < f PROB) " using assms bound_on_all_plans_bounds_PLS_charles[of P f] by blast then have " P PROB ∧ finite PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⟶ Inf {n. n ∈ PLS_charles s as PROB} < f PROB " using mem_lt_imp_MIN_lt CollectI by metis } then show ?thesis by blast qed lemma bound_on_all_plans_bounds_MPLS_charles: fixes P f assumes "(∀(PROB :: 'a problem) as s. (P PROB) ∧ finite PROB ∧ (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB) ) )" shows "(∀PROB x. (P PROB) ∧ finite PROB ⟶ (x ∈ MPLS_charles PROB) ⟶ (x < f PROB) )" proof - have 1: "∀(PROB :: 'a problem) s as. P PROB ∧ finite PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⟶ Inf {n. n ∈ PLS_charles s as PROB} < f PROB " using assms bound_on_all_plans_bounds_MPLS_charles_i by blast moreover { fix PROB :: "'a problem" and x assume P1: "(P PROB)" "finite PROB" "x ∈ MPLS_charles PROB" then obtain s as where a: "as ∈ valid_plans PROB" "s ∈ valid_states PROB" "x = Inf (PLS_charles s as PROB)" using x_in_MPLS_charles_then by blast then have "Inf {n. n ∈ PLS_charles s as PROB} < f PROB" using 1 P1 by blast then have "x < f PROB" using a by simp } ultimately show ?thesis by blast qed ― ‹NOTE added lemma (refactored from 'bound\_on\_all\_plans\_bounds\_problem\_plan\_bound\_charles').› lemma bound_on_all_plans_bounds_problem_plan_bound_charles_i: fixes PROB :: "'a problem" assumes "finite PROB" "∀x ∈ MPLS_charles PROB. x < k" shows "Sup (MPLS_charles PROB) ∈ MPLS_charles PROB" proof - have 1: "MPLS_charles PROB ≠ {}" using assms(1) bound_main_lemma_charles_3 by auto then have "finite (MPLS_charles PROB)" using assms(2) finite_nat_set_iff_bounded by blast then show ?thesis unfolding Sup_nat_def using 1 by simp qed lemma bound_on_all_plans_bounds_problem_plan_bound_charles: fixes P f assumes "(∀(PROB :: 'a problem) as s. (P PROB) ∧ finite PROB ∧ (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB) ⟶ (∃as'. (exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB))) " shows "(∀PROB. (P PROB) ∧ finite PROB ⟶ (problem_plan_bound_charles PROB < f PROB)) " proof - have 1: "∀PROB x. P PROB ∧ finite PROB ⟶ x ∈ MPLS_charles PROB ⟶ x < f PROB" using assms bound_on_all_plans_bounds_MPLS_charles by blast moreover { fix PROB assume P: "P PROB" "finite PROB" moreover have 2: "∀x. x ∈ MPLS_charles PROB ⟶ x < f PROB" using 1 P by blast moreover { fix x assume P1: "x ∈ MPLS_charles PROB" moreover have "x < f PROB" using P(1, 2) P1 1 by presburger moreover have "MPLS_charles PROB ≠ {}" using P1 by blast moreover have "Sup (MPLS_charles PROB) < f PROB" using calculation(3) 2 bound_child_parent_not_eq_last_diff_paths[of "MPLS_charles PROB" "f PROB"] by blast ultimately have "(problem_plan_bound_charles PROB < f PROB)" unfolding problem_plan_bound_charles_def by blast } moreover have "Sup (MPLS_charles PROB) ∈ MPLS_charles PROB" using P(2) 2 bound_on_all_plans_bounds_problem_plan_bound_charles_i by blast ultimately have "problem_plan_bound_charles PROB < f PROB" unfolding problem_plan_bound_charles_def by blast } ultimately show ?thesis by blast qed subsection "The Relation between Diameter, Sublist Diameter and Recurrence Diameter Bounds." text ‹ The goal of this subsection is to verify the relation between diameter, sublist diameter and recurrence diameter bounds given by HOL4 Theorem 1, i.e. @{term "𝖽(δ) ≤ 𝗅(δ) ∧ 𝗅(δ) ≤ 𝗋𝖽(δ)"} where @{term "𝖽(δ)"}, @{term "𝗅(δ)"} and @{term "𝗋𝖽(δ)"} denote the diameter, sublist diameter and recurrence diameter bounds. [Abdualaziz et al., p.20] The relevant lemmas are `sublistD\_bounds\_D` and `RD\_bounds\_sublistD` which culminate in theorem `sublistD\_bounds\_D\_and\_RD\_bounds\_sublistD`. › lemma sublistD_bounds_D: fixes PROB :: "'a problem" assumes "finite PROB" shows "problem_plan_bound_charles PROB ≤ problem_plan_bound PROB" proof - ― ‹NOTE obtain the premise needed for MP of 'bound\_on\_all\_plans\_bounds\_problem\_plan\_bound\_charles'.› { fix PROB :: "'a problem" and s :: "'a state" and as assume P: "finite PROB" "s ∈ valid_states PROB" "as ∈ valid_plans PROB" then have "∃as'. exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' ≤ problem_plan_bound PROB " using problem_plan_bound_works by blast then have "∃as'. exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' < problem_plan_bound PROB + 1 " by force } then have "problem_plan_bound_charles PROB < problem_plan_bound PROB + 1" using assms bound_on_all_plans_bounds_problem_plan_bound_charles[where f = "λPROB. problem_plan_bound PROB + 1" and P = "λ_. True"] by blast then show ?thesis by simp qed ― ‹NOTE added lemma (this was adapted from pred\_setScript.sml:4887 with exlusion of the premise for the empty set since `Max {}` is undefined in Isabelle/HOL.)› lemma MAX_SET_ELIM': fixes P Q assumes "finite P" "P ≠ {}" "(∀x. (∀y. y ∈ P ⟶ y ≤ x) ∧ x ∈ P ⟶ R x)" shows "R (Max P)" using assms by force ― ‹NOTE added lemma.› ― ‹NOTE adapted from pred\_setScript.sml:4895 (premise `finite P` was added).› lemma MIN_SET_ELIM': fixes P Q assumes "finite P" "P ≠ {}" "∀x. (∀y. y ∈ P ⟶ x ≤ y) ∧ x ∈ P ⟶ Q x" shows "Q (Min P)" proof - let ?x="Min P" have "Min P ∈ P" using Min_in[OF assms(1) assms(2)] by simp moreover { fix y assume P: "y ∈ P" then have "?x ≤ y" using Min.coboundedI[OF assms(1)] by blast then have "Q ?x" using P assms by auto } ultimately show ?thesis by blast qed ― ‹NOTE added lemma (refactored from `RD\_bounds\_sublistD`).› lemma RD_bounds_sublistD_i_a: fixes Pi :: "'a problem" assumes "finite Pi" shows "finite {length p - 1 |p. valid_path Pi p ∧ distinct p}" proof - { let ?ss="{length p - 1 |p. valid_path Pi p ∧ distinct p}" let ?ss'="{p. valid_path Pi p ∧ distinct p}" have 1: "?ss = (λx. length x - 1) ` ?ss'" by blast { ― ‹NOTE type of `valid\_states Pi` had to be asserted to match `FINITE\_valid\_states`.› let ?S="{p. distinct p ∧ set p ⊆ (valid_states Pi :: 'a state set)}" { from assms have "finite (valid_states Pi :: 'a state set)" using FINITE_valid_states[of Pi] by simp then have "finite ?S" using FINITE_ALL_DISTINCT_LISTS by blast } moreover { { fix x assume "x ∈ ?ss'" then have "x ∈ ?S" proof (induction x) case (Cons a x) then have a: "valid_path Pi (a # x)" "distinct (a # x)" by blast+ moreover { fix x' assume P: "x' ∈ set (a # x)" then have "x' ∈ valid_states Pi" proof (cases "x") case Nil from a(1) Nil have "a ∈ valid_states Pi" by simp moreover from P Nil have "x' = a" by force ultimately show ?thesis by simp next case (Cons a' list) { { from Cons.prems have "valid_path Pi (a # x)" by simp then have "a ∈ valid_states Pi" "valid_path Pi (a' # list)" using Cons by fastforce+ } note a = this moreover { from Cons.prems have "distinct (a # x)" by blast then have "distinct (a' # list)" using Cons by simp } ultimately have "(a' # list) ∈ ?ss'" by blast then have "(a' # list) ∈ ?S" using Cons Cons.IH by argo } then show ?thesis using P a(1) local.Cons set_ConsD by fastforce qed } ultimately show ?case by blast qed simp } then have "?ss' ⊆ ?S" by blast } ultimately have "finite ?ss'" using rev_finite_subset by auto } note 2 = this from 1 2 have "finite ?ss" using finite_imageI by auto } then show ?thesis by blast qed ― ‹NOTE added lemma (refactored from `RD\_bounds\_sublistD`).› lemma RD_bounds_sublistD_i_b: fixes Pi :: "'a problem" shows "{length p - 1 |p. valid_path Pi p ∧ distinct p} ≠ {}" proof - let ?Q="{length p - 1 |p. valid_path Pi p ∧ distinct p}" let ?Q'="{p. valid_path Pi p ∧ distinct p}" { have "valid_path Pi []" by simp moreover have "distinct []" by simp ultimately have "[] ∈ ?Q'" by simp } note 1 = this have "?Q = (λp. length p - 1) ` ?Q'" by blast then have "length [] - 1 ∈ ?Q" using 1 by (metis (mono_tags, lifting) image_iff list.size(3)) then show ?thesis by blast qed ― ‹NOTE added lemma (refactored from `RD\_bounds\_sublistD`).› lemma RD_bounds_sublistD_i_c: fixes Pi :: "'a problem" and as :: "(('a, bool) fmap × ('a, bool) fmap) list" and x and s :: "('a, bool) fmap" assumes "s ∈ valid_states Pi" "as ∈ valid_plans Pi" "(∀y. y ∈ {length p - 1 |p. valid_path Pi p ∧ distinct p} ⟶ y ≤ x)" "x ∈ {length p - 1 |p. valid_path Pi p ∧ distinct p}" shows "Min (PLS s as) ≤ Max {length p - 1 |p. valid_path Pi p ∧ distinct p}" proof - let ?P="(PLS s as)" let ?Q="{length p - 1 |p. valid_path Pi p ∧ distinct p}" from assms(4) obtain p where 1: "x = length p - 1" "valid_path Pi p" "distinct p" by blast { fix p' assume "valid_path Pi p'" "distinct p'" then obtain y where "y ∈ ?Q" "y = length p' - 1" by blast ― ‹NOTE we cannot infer @{term "length p' - 1 ≤ length p - 1"} since `length p' = 0` might be true.› then have a: "length p' - 1 ≤ length p - 1" using assms(3) 1(1) by meson } note 2 = this { from finite_PLS PLS_NEMPTY have "finite (PLS s as)" "PLS s as ≠ {}" by blast+ moreover { fix n assume P: "(∀y. y ∈ PLS s as ⟶ n ≤ y)" "n ∈ PLS s as" from P(2) obtain as' where i: "n = length as'" "exec_plan s as' = exec_plan s as" "subseq as' as" unfolding PLS_def by blast let ?p'="statelist' s as'" { have "length as' = length ?p' - 1" by (simp add: LENGTH_statelist') ― ‹MARKER (topologicalPropsScript.sml:195)› have "1 + (length p - 1) = length p - 1 + 1" by presburger ― ‹MARKER (topologicalPropsScript.sml:200)› { from assms(2) i(3) sublist_valid_plan have "as' ∈ valid_plans Pi" by blast then have "valid_path Pi ?p'" using assms(1) valid_path_statelist' by auto } moreover { { assume C: "¬distinct ?p'" ― ‹NOTE renamed variable `drop` to `drop'` to avoid shadowing of the function by the same name in Isabelle/HOL.› then obtain rs pfx drop' tail where C_1: "?p' = pfx @ [rs] @ drop' @ [rs] @ tail" using not_distinct_decomp[OF C] by fast let ?pfxn="length pfx" have C_2: "?p' ! ?pfxn = rs" by (simp add: C_1) from LENGTH_statelist' have C_3: "length as' + 1 = length ?p'" by metis then have "?pfxn ≤ length as'" using C_1 by fastforce then have C_4: "exec_plan s (take ?pfxn as') = rs" using C_2 statelist'_TAKE by blast let ?prsd = "length (pfx @ [rs] @ drop')" let ?ap1 = "take ?pfxn as'" ― ‹MARKER (topologicalPropsScript.sml:215)› from C_1 have C_5: "?p' ! ?prsd = rs" by (metis append_Cons length_append nth_append_length nth_append_length_plus) from C_1 C_3 have C_6: "?prsd ≤ length as'" by simp then have C_7: "exec_plan s (take ?prsd as') = rs" using C_5 statelist'_TAKE by auto let ?ap2="take ?prsd as'" let ?asfx="drop ?prsd as'" have C_8: "as' = ?ap2 @ ?asfx" by force then have "exec_plan s as' = exec_plan (exec_plan s ?ap2) ?asfx" using exec_plan_Append by metis then have C_9: "exec_plan s as' = exec_plan s (?ap1 @ ?asfx)" using C_4 C_7 exec_plan_Append by metis from C_6 have C_10: "(length ?ap1 = ?pfxn) ∧ (length ?ap2 = ?prsd)" by fastforce then have C_11: "length (?ap1 @ ?asfx) < length (?ap2 @ ?asfx)" by auto { from C_10 have "?pfxn + length ?asfx = length (?ap1 @ ?asfx)" by simp from C_9 i(2) have C_12: "exec_plan s (?ap1 @ ?asfx) = exec_plan s as" by argo { { { have "prefix ?ap1 ?ap2" by (metis (no_types) length_append prefix_def take_add) then have "subseq ?ap1 ?ap2" using isPREFIX_sublist by blast } moreover have "sublist ?asfx ?asfx" using sublist_refl by blast ultimately have "subseq (?ap1 @ ?asfx) as'" using C_8 subseq_append by metis } moreover from i(3) have "subseq as' as" by simp ultimately have "subseq (?ap1 @ ?asfx) as" using sublist_trans by blast } then have "length (?ap1 @ ?asfx) ∈ PLS s as" unfolding PLS_def using C_12 by blast } then have False using P(1) i(1) C_10 by auto } hence "distinct ?p'" by auto } ultimately have "length ?p' - 1 ≤ length p - 1" using 2 by blast } note ii = this { from i(1) have "n + 1 = length ?p'" using LENGTH_statelist'[symmetric] by blast also have "… ≤ 1 + (length p - 1)" using ii by linarith finally have "n ≤ length p - 1" by fastforce } then have "n ≤ length p - 1" by blast } ultimately have "Min ?P ≤ length p - 1" using MIN_SET_ELIM'[where P="?P" and Q="λx. x ≤ length p - 1"] by blast } note 3 = this { have "length p - 1 ≤ Max {length p - 1 |p. valid_path Pi p ∧ distinct p}" using assms(3, 4) 1(1) by (smt Max.coboundedI bdd_aboveI bdd_above_nat) moreover have "Min (PLS s as) ≤ length p - 1" using 3 by blast ultimately have "Min (PLS s as) ≤ Max {length p - 1 |p. valid_path Pi p ∧ distinct p}" by linarith } then show ?thesis by blast qed ― ‹NOTE added lemma (refactored from `RD\_bounds\_sublistD`).› lemma RD_bounds_sublistD_i: fixes Pi :: "'a problem" and x assumes "finite Pi" "(∀y. y ∈ MPLS Pi ⟶ y ≤ x)" "x ∈ MPLS Pi" shows "x ≤ Max {length p - 1 |p. valid_path Pi p ∧ distinct p}" proof - { let ?P="MPLS Pi" let ?Q="{length p - 1 |p. valid_path Pi p ∧ distinct p}" from assms(3) obtain s as where 1: "s ∈ valid_states Pi" "as ∈ valid_plans Pi" "x = Inf (PLS s as)" unfolding MPLS_def by fast have "x ≤ Max ?Q" proof - text ‹ Show that `x` is not only the infimum but also the minimum of `PLS s as`.› { have "finite (PLS s as)" using finite_PLS by auto moreover have "PLS s as ≠ {}" using PLS_NEMPTY by auto ultimately have a: "Inf (PLS s as) = Min (PLS s as)" using cInf_eq_Min[of "PLS s as"] by blast from 1(3) a have "x = Min (PLS s as)" by blast } note a = this { let ?limit="Min (PLS s as)" from assms(1) have a: "finite ?Q" using RD_bounds_sublistD_i_a by blast have b: "?Q ≠ {}" using RD_bounds_sublistD_i_b by fast from 1(1, 2) have c: "∀x. (∀y. y ∈ ?Q ⟶ y ≤ x) ∧ x ∈ ?Q ⟶ ?limit ≤ Max ?Q" using RD_bounds_sublistD_i_c by blast have "?limit ≤ Max ?Q" using MAX_SET_ELIM'[where P="?Q" and R="λx. ?limit ≤ Max ?Q", OF a b c] by blast } note b = this from a b show "x ≤ Max ?Q" by blast qed } then show ?thesis using assms unfolding MPLS_def by blast qed ― ‹NOTE type of `Pi` had to be fixed for use of `FINITE\_valid\_states`.› lemma RD_bounds_sublistD: fixes Pi :: "'a problem" assumes "finite Pi" shows "problem_plan_bound Pi ≤ RD Pi" proof - let ?P="MPLS Pi" let ?Q="{length p - 1 |p. valid_path Pi p ∧ distinct p}" { from assms have 1: "finite ?P" using FINITE_MPLS by blast from assms have 2: "?P ≠ {}" using MPLS_nempty by blast from assms have 3: "∀x. (∀y. y ∈ ?P ⟶ y ≤ x) ∧ x ∈ ?P ⟶ x ≤ Max ?Q" using RD_bounds_sublistD_i by blast have "Max ?P ≤ Max ?Q" using MAX_SET_ELIM'[OF 1 2 3] by blast } then show ?thesis unfolding problem_plan_bound_def RD_def Sup_nat_def using RD_bounds_sublistD_i_b by auto qed ― ‹NOTE type for `PROB` had to be fixed in order to be able to match `sublistD\_bounds\_D`.› theorem sublistD_bounds_D_and_RD_bounds_sublistD: fixes PROB :: "'a problem" assumes "finite PROB" shows " problem_plan_bound_charles PROB ≤ problem_plan_bound PROB ∧ problem_plan_bound PROB ≤ RD PROB " using assms sublistD_bounds_D RD_bounds_sublistD by auto ― ‹NOTE type of `PROB` had to be fixed for MP of lemmas.› lemma empty_problem_bound: fixes PROB :: "'a problem" assumes "(prob_dom PROB = {})" shows "(problem_plan_bound PROB = 0)" proof - { fix PROB' and as :: "(('a, 'b) fmap × ('a, 'b) fmap) list" and s :: "('a, 'b) fmap" assume "finite PROB" "prob_dom PROB' = {}" "s ∈ valid_states PROB'" "as ∈ valid_plans PROB'" then have "exec_plan s [] = exec_plan s as" using empty_prob_dom_imp_empty_plan_always_good by blast then have "(∃as'. exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' < 1)" by force } then show ?thesis using bound_on_all_plans_bounds_problem_plan_bound_[where P="λP. prob_dom P = {}" and f="λP. 1", of PROB] using assms empty_prob_dom_finite by blast qed lemma problem_plan_bound_works': fixes PROB :: "'a problem" and as s assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB<