theory ActionSeqProcess imports Main "HOL-Library.Sublist" FactoredSystemLib FactoredSystem FSSublist begin section "Action Sequence Process" text ‹ This section defines the preconditions satisfied predicate for action sequences and shows relations between the execution of action sequnences and their projections some. The preconditions satisfied predicate (`sat\_precond\_as`) states that in each recursion step, the given state and the next action are compatible, i.e. the actions preconditions are met by the state. This is used as premise to propositions on projections of action sequences to avoid that an invalid unprojected sequence is suddenly valid after projection. [Abdulaziz et al., p.13] › ― ‹NOTE curried.› ― ‹NOTE 'fun' because of multiple defining equations.› fun sat_precond_as where "sat_precond_as s [] = True" | "sat_precond_as s (a # as) = (fst a ⊆⇩_{f}s ∧ sat_precond_as (state_succ s a) as)" ― ‹NOTE added lemma.› lemma sat_precond_as_pair: "sat_precond_as s ((p, e) # as) = (p ⊆⇩_{f}s ∧ sat_precond_as (state_succ s (p, e)) as)" by simp ― ‹NOTE 'fun' because of multiple defining equations.› fun rem_effectless_act where "rem_effectless_act [] = []" | "rem_effectless_act (a # as) = (if fmdom' (snd a) ≠ {} then (a # rem_effectless_act as) else rem_effectless_act as )" ― ‹NOTE 'fun' because of multiple defining equations.› fun no_effectless_act where "no_effectless_act [] = True" | "no_effectless_act (a # as) = ((fmdom' (snd a) ≠ {}) ∧ no_effectless_act as)" lemma graph_plan_lemma_4: fixes s s' as vs P assumes "(∀a. (ListMem a as ∧ P a) ⟶ ((fmdom' (snd a) ∩ vs) = {}))" "sat_precond_as s as" "sat_precond_as s' (filter (λa. ¬(P a)) as)" "(fmrestrict_set vs s = fmrestrict_set vs s')" shows " (fmrestrict_set vs (exec_plan s as) = fmrestrict_set vs (exec_plan s' (filter (λ a. ¬(P a)) as))) " using assms unfolding exec_plan.simps proof(induction as arbitrary: s s' vs P) case (Cons a as) then have 1: "fst a ⊆⇩_{f}s" "sat_precond_as (state_succ s a) as" by auto then have 2: "∀a'. ListMem a' as ∧ P a' ⟶ fmdom' (snd a') ∩ vs = {}" by (simp add: Cons.prems(1) insert) then show ?case proof (cases "P a") case True { then have "filter (λa. ¬(P a)) (a # as) = filter (λa. ¬(P a)) as" by simp then have "sat_precond_as s' (filter (λa. ¬(P a)) as)" using Cons.prems(3) True by argo } note a = this { then have "ListMem a (a # as)" using elem by fast then have "(fmdom' (snd a) ∩ vs) = {}" using Cons.prems(1) True by blast then have "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s" using disj_imp_eq_proj_exec[symmetric] by fast } then show ?thesis unfolding exec_plan.simps using Cons.prems(4) 1(2) 2 True a Cons.IH[where s="state_succ s a" and s'=s'] by fastforce next case False { have "filter (λa. ¬(P a)) (a # as) = a # filter (λa. ¬(P a)) as" using False by auto then have "fst a ⊆⇩_{f}s'" "sat_precond_as (state_succ s' a) (filter (λa. ¬(P a)) as)" using Cons.prems(3) False by force+ } note b = this then have "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs (state_succ s' a)" using proj_eq_proj_exec_eq using Cons.prems(4) 1(1) by blast then show ?thesis unfolding exec_plan.simps using 1(2) 2 False b Cons.IH[where s="state_succ s a" and s'="state_succ s' a"] by force qed qed simp ― ‹NOTE curried instead of triples.› ― ‹NOTE 'fun' because of multiple defining equations.› fun rem_condless_act where "rem_condless_act s pfx_a [] = pfx_a" | "rem_condless_act s pfx_a (a # as) = (if fst a ⊆⇩_{f}exec_plan s pfx_a then rem_condless_act s (pfx_a @ [a]) as else rem_condless_act s pfx_a as )" lemma rem_condless_act_pair: " rem_condless_act s pfx_a ((p, e) # as) = (if p ⊆⇩_{f}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)" by simp+ lemma exec_remcondless_cons: fixes s h as pfx shows " 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) " by (induction as arbitrary: s h pfx) auto lemma rem_condless_valid_1: fixes as s shows "(exec_plan s as = exec_plan s (rem_condless_act s [] as))" by (induction as arbitrary: s) (auto simp add: exec_remcondless_cons FDOM_state_succ state_succ_def) lemma rem_condless_act_cons: fixes h' pfx as s shows "(rem_condless_act s (h' # pfx) as) = (h' # rem_condless_act (state_succ s h') pfx as)" by (induction as arbitrary: h' pfx s) auto lemma rem_condless_act_cons_prefix: fixes h h' as as' s assumes "prefix (h' # as') (rem_condless_act s [h] as)" shows "( (prefix as' (rem_condless_act (state_succ s h) [] as)) ∧ h' = h )" using assms proof (induction as arbitrary: h h' as' s) case Nil then have "rem_condless_act s [h] [] = [h]" by simp then have 1: "as' = []" using Nil.prems by simp then have "rem_condless_act (state_succ s h) [] [] = []" by simp then have 2: "prefix as' (rem_condless_act (state_succ s h) [] [])" using 1 by simp then have "h = h'" using Nil.prems by force then show ?case using 2 by blast next case (Cons a as) { have "rem_condless_act s [h] (a # as) = h # rem_condless_act (state_succ s h) [] (a # as)" using rem_condless_act_cons by fast then have "h = h'" using Cons.prems by simp } moreover { obtain l where "(h' # as') @ l = (h # rem_condless_act (state_succ s h) [] (a # as))" using Cons.prems rem_condless_act_cons prefixE by metis then have "prefix (as' @ l) (rem_condless_act (state_succ s h) [] (a # as))" by simp then have "prefix as' (rem_condless_act (state_succ s h) [] (a # as))" using append_prefixD by blast } ultimately show ?case by fastforce qed lemma rem_condless_valid_2: fixes as s shows "sat_precond_as s (rem_condless_act s [] as)" by (induction as arbitrary: s) (auto simp: rem_condless_act_cons) lemma rem_condless_valid_3: fixes as s shows "length (rem_condless_act s [] as) ≤ length as" by (induction as arbitrary: s) (auto simp: rem_condless_act_cons le_SucI) lemma rem_condless_valid_4: fixes as A s assumes "(set as ⊆ A)" shows "(set (rem_condless_act s [] as) ⊆ A)" using assms by (induction as arbitrary: A s) (auto simp: rem_condless_act_cons) lemma rem_condless_valid_6: fixes as s P shows "length (filter P (rem_condless_act s [] as)) ≤ length (filter P as)" proof (induction as arbitrary: P s) case (Cons a as) then show ?case by (simp add: rem_condless_act_cons le_SucI) qed simp lemma rem_condless_valid_7: fixes s P as as2 assumes "(list_all P as ∧ list_all P as2)" shows "list_all P (rem_condless_act s as2 as)" using assms by (induction as arbitrary: P s as2) auto lemma rem_condless_valid_8: fixes s as shows "subseq (rem_condless_act s [] as) as" by (induction as arbitrary: s) (auto simp: sublist_cons_4 rem_condless_act_cons) lemma rem_condless_valid_10: fixes PROB as assumes "as ∈ (valid_plans PROB)" shows "(rem_condless_act s [] as ∈ valid_plans PROB)" using assms valid_plans_def rem_condless_valid_1 rem_condless_valid_4 by blast lemma rem_condless_valid: fixes as A s assumes "(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))" shows "(∀P. (length (filter P (rem_condless_act s [] as)) ≤ length (filter P as)))" using rem_condless_valid_1 rem_condless_valid_2 rem_condless_valid_3 rem_condless_valid_6 rem_condless_valid_4 by fast ― ‹NOTE type of `as` had to be fixed for lemma submap\_imp\_state\_succ\_submap.› lemma submap_sat_precond_submap: fixes as :: "'a action list" assumes "(s1 ⊆⇩_{f}s2)" "(sat_precond_as s1 as)" shows "(sat_precond_as s2 as)" using assms proof (induction as arbitrary: s1 s2) case (Cons a as) { have "fst a ⊆⇩_{f}s1" using Cons.prems(2) by simp then have "fst a ⊆⇩_{f}s2" using Cons.prems(1) submap_imp_state_succ_submap_a by blast } note 1 = this { have 2: "fst a ⊆⇩_{f}s1" "sat_precond_as (state_succ s1 a) as" using Cons.prems(2) by simp+ then have "state_succ s1 a ⊆⇩_{f}state_succ s2 a" using Cons.prems(1) submap_imp_state_succ_submap by blast then have 3: "sat_precond_as (state_succ s2 a) as" using 2(2) Cons.IH by blast } then show ?case using 1 by auto qed auto ― ‹NOTE added lemma.› lemma submap_init_submap_exec_i: fixes s1 s2 assumes "(s1 ⊆⇩_{f}s2)" "(sat_precond_as s1 (a # as))" shows "state_succ s1 a ⊆⇩_{f}state_succ s2 a" using assms proof (cases "fst a ⊆⇩_{f}s1") case true: True then show ?thesis proof (cases "fst a ⊆⇩_{f}s2") case True then show ?thesis unfolding state_succ_def using assms submap_imp_state_succ_submap_b state_succ_def true by auto next case False then show ?thesis using assms submap_imp_state_succ_submap_a true by blast qed next case false: False then show ?thesis proof (cases "fst a ⊆⇩_{f}s2") case True then show ?thesis using assms false by auto next case False then show ?thesis unfolding state_succ_def using false assms by simp qed qed lemma submap_init_submap_exec: fixes s1 s2 assumes "(s1 ⊆⇩_{f}s2)" "(sat_precond_as s1 as)" shows "(exec_plan s1 as ⊆⇩_{f}exec_plan s2 as)" using assms proof (induction as arbitrary: s1 s2) case (Cons a as) have "state_succ s1 a ⊆⇩_{f}state_succ s2 a" using Cons.prems submap_init_submap_exec_i by blast moreover have "sat_precond_as (state_succ s1 a) as" using Cons.prems(2) by simp ultimately have "exec_plan (state_succ s1 a) as ⊆⇩_{f}exec_plan (state_succ s2 a) as" using Cons.IH by blast then show ?case by simp qed simp ― ‹NOTE type of `as` had to be fixed for `submap\_sat\_precond\_submap`.› lemma sat_precond_drest_sat_precond: fixes vs s and as :: "'a action list" assumes "sat_precond_as (fmrestrict_set vs s) as" shows "(sat_precond_as s as)" proof - have "fmrestrict_set vs s ⊆⇩_{f}s" by simp then show "(sat_precond_as s as)" using assms submap_sat_precond_submap by blast qed ― ‹NOTE name shortened to 'varset\_action'.› definition varset_action where "varset_action a varset ≡ (fmdom' (snd a) ⊆ varset)" for a :: "'a action" lemma varset_action_pair: "(varset_action (p, e) vs) = (fmdom' e ⊆ vs)" unfolding varset_action_def by auto lemma eq_effect_eq_vset: fixes x y assumes "(snd x = snd y)" shows "((λa. varset_action a vs) x = (λa. varset_action a vs) y)" unfolding varset_action_def using assms by presburger lemma rem_effectless_works_1: fixes s as shows "(exec_plan s as = exec_plan s (rem_effectless_act as))" by (induction as arbitrary: s) (auto simp: empty_eff_exec_eq) lemma rem_effectless_works_2: fixes as s assumes "(sat_precond_as s as)" shows "(sat_precond_as s (rem_effectless_act as))" using assms by (induction as arbitrary: s) (auto simp: empty_eff_exec_eq) lemma rem_effectless_works_3: fixes as shows "length (rem_effectless_act as) ≤ length as" by (induction as) auto lemma rem_effectless_works_4: fixes A as assumes "(set as ⊆ A)" shows "(set (rem_effectless_act as) ⊆ A)" using assms by (induction as arbitrary: A) auto lemma rem_effectless_works_4': fixes A as assumes "(as ∈ valid_plans A)" shows "(rem_effectless_act as ∈ valid_plans A)" using assms by (induction as arbitrary: A) (auto simp: valid_plans_def) ― ‹NOTE added lemma.› lemma rem_effectless_works_5_i: shows "subseq (rem_effectless_act as) as" by (induction as) auto lemma rem_effectless_works_5: fixes P as shows "length (filter P (rem_effectless_act as)) ≤ length (filter P as)" using rem_effectless_works_5_i sublist_imp_len_filter_le by blast lemma rem_effectless_works_6: fixes as shows "no_effectless_act (rem_effectless_act as)" by (induction as) auto lemma rem_effectless_works_7: fixes as shows "no_effectless_act as = list_all (λa. fmdom' (snd a) ≠ {}) as" by (induction as) auto lemma rem_effectless_works_8: fixes P as assumes "(list_all P as)" shows "list_all P (rem_effectless_act as)" using assms by (induction as arbitrary: P) auto ― ‹TODO move and replace `rem\_effectless\_works\_5\_i`.› lemma rem_effectless_works_9: fixes as shows "subseq (rem_effectless_act as) as" by (induction as) auto lemma rem_effectless_works_10: fixes as P assumes "(no_effectless_act as)" shows "(no_effectless_act (filter P as))" using assms by (auto simp: rem_effectless_works_7) (metis Ball_set filter_set member_filter) lemma rem_effectless_works_11: fixes as1 as2 assumes "subseq as1 (rem_effectless_act as2)" shows "(subseq as1 as2)" using assms rem_effectless_works_9 sublist_trans by blast lemma rem_effectless_works_12: fixes as1 as2 shows "(no_effectless_act (as1 @ as2)) = (no_effectless_act as1 ∧ no_effectless_act(as2))" by (induction as1) auto ― ‹TODO refactor into 'List\_Utils.thy'.› lemma rem_effectless_works_13_i: fixes x l assumes "ListMem x l" "list_all P l" shows "P x" using assms proof (induction l) case (insert x xs y) have 1: "P y" using insert.prems list.pred_inject by simp then have 2: "list_all P l" using assms(2) list.pred_inject by force then show ?case using 1 proof (cases "y = x") case False then show ?thesis using insert 2 by fastforce qed simp qed simp lemma rem_effectless_works_13: fixes as1 as2 assumes "(subseq as1 as2)" "(no_effectless_act as2)" shows "(no_effectless_act as1)" using assms proof (induction as1 arbitrary: as2) case (Cons a as1) { have "subseq as1 as2" using Cons.prems(1) sublist_CONS1_E by metis then have "no_effectless_act as1" using Cons.prems(2) Cons.IH by blast } moreover { have "list_all (λa. fmdom' (snd a) ≠ {}) as2" using Cons.prems(2) rem_effectless_works_7 by blast moreover have "ListMem a as2" using Cons.prems(1) sublist_MEM by fast ultimately have "fmdom' (snd a) ≠ {}" using rem_effectless_works_13_i by fastforce } ultimately show ?case by simp qed simp lemma rem_effectless_works_14: fixes PROB as shows "exec_plan s as = exec_plan s (rem_effectless_act as)" using rem_effectless_works_1 by blast lemma rem_effectless_works: fixes s A as assumes "(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))" shows "(∀P. length (filter P (rem_effectless_act as)) ≤ length (filter P as))" using assms rem_effectless_works_5 by blast ― ‹NOTE name shortened.› definition rem_effectless_act_set where "rem_effectless_act_set A ≡ {a ∈ A. fmdom' (snd a) ≠ {}}" lemma rem_effectless_act_subset_rem_effectless_act_set_thm: fixes as A assumes "(set as ⊆ A)" shows "(set (rem_effectless_act as) ⊆ rem_effectless_act_set A)" unfolding rem_effectless_act_set_def using assms by (induction as) auto lemma rem_effectless_act_set_no_empty_actions_thm: fixes A shows "rem_effectless_act_set A ⊆ {a. fmdom' (snd a) ≠ {}}" unfolding rem_effectless_act_set_def by blast ― ‹NOTE proof required additional lemmas 'rem\_effectless\_works\_7' and 'rem\_condless\_valid\_7'.› lemma rem_condless_valid_9: fixes s as assumes "no_effectless_act as" shows "no_effectless_act (rem_condless_act s [] as)" using assms proof (induction as arbitrary: s) case (Cons a as) then show ?case using Cons proof (cases " fst a ⊆⇩_{f}exec_plan s []") case True then have "rem_condless_act s [] (a # as) = a # rem_condless_act (state_succ s a) [] as" using rem_condless_act_cons by fastforce moreover { have "fmdom' (snd a) ≠ {}" "no_effectless_act as" using Cons.prems by simp+ then have "no_effectless_act (rem_condless_act (state_succ s a) [] as)" using Cons.IH by blast } moreover have "no_effectless_act [a]" using Cons.prems by simp ultimately show ?thesis using rem_effectless_works_12 by force qed simp qed simp lemma graph_plan_lemma_17: fixes as_1 as_2 as s assumes "(as_1 @ as_2 = as)" "(sat_precond_as s as)" shows "((sat_precond_as s as_1) ∧ sat_precond_as (exec_plan s as_1) as_2)" using assms proof (induction as arbitrary: as_1 as_2 s) case (Cons a as) then show ?case proof(cases "as_1") case Nil then show ?thesis using Cons.prems(1, 2) by auto next case (Cons a list) then show ?thesis using Cons.prems(1, 2) Cons.IH hd_append2 list.distinct(1) list.sel(1, 3) tl_append2 by auto qed qed auto lemma nempty_eff_every_nempty_act: fixes as assumes "(no_effectless_act as)" "(∀x. ¬(fmdom' (snd (f x)) = {}))" shows "(list_all (λa. ¬(f a = (fmempty, fmempty))) as)" using assms proof (induction as arbitrary: f) case (Cons a as) then show ?case using fmdom'_empty snd_conv by (metis (mono_tags, lifting) Ball_set) qed simp lemma empty_replace_proj_dual7: fixes s as as' assumes "sat_precond_as s (as @ as')" shows "sat_precond_as (exec_plan s as) as'" using assms by (induction as arbitrary: as' s) auto lemma not_vset_not_disj_eff_prod_dom_diff: fixes PROB a vs assumes "(a ∈ PROB)" "(¬varset_action a vs)" shows "¬((fmdom' (snd a) ∩ ((prob_dom PROB) - vs)) = {})" proof - have 1: "fmdom' (snd a) ≠ {}" using assms(2) varset_action_def by blast { have "fmdom' (snd a) ⊆ prob_dom PROB" using assms(1) FDOM_eff_subset_prob_dom_pair by metis then have " fmdom' (snd a) ∩ (prob_dom PROB - vs) = (fmdom' (snd a)) - (fmdom' (snd a) ∩ vs)" using Diff_Int_distrib by blast } note 2 = this then show ?thesis using 1 2 proof (cases "fmdom' (snd a) ∩ vs = {}") case False { have "¬(fmdom' (snd a) ⊆ vs)" using assms(2) varset_action_def by fast then have "(fmdom' (snd a) ∩ vs ≠ fmdom' (snd a))" by auto then have "(fmdom' (snd a) ∩ vs) ⊂ fmdom' (snd a)" by blast } then show ?thesis using 2 by auto qed force qed lemma vset_disj_dom_eff_diff: fixes PROB a vs assumes "(varset_action a vs)" shows "(((fmdom' (snd a)) ∩ (prob_dom PROB - vs)) = {})" using assms unfolding varset_action_def by auto lemma vset_diff_disj_eff_vs: fixes PROB a vs assumes "(varset_action a (prob_dom PROB - vs))" shows "(((fmdom' (snd a)) ∩ vs) = {})" using assms unfolding varset_action_def by blast lemma vset_nempty_efff_not_disj_eff_vs: fixes PROB a vs assumes "(varset_action a vs)" "(fmdom' (snd a) ≠ {})" shows "¬((fmdom' (snd a) ∩ vs)) = {}" using assms unfolding varset_action_def by auto lemma vset_disj_eff_diff: fixes s a vs assumes "(varset_action a vs)" shows "((fmdom' (snd a) ∩ (s - vs)) = {})" proof - have 1: "fmdom' (snd a) ⊆ vs" using assms by (simp add: varset_action_def) moreover { have "fmdom' (snd a) ∩ (s - vs) = (fmdom' (snd a) ∩ s) - (fmdom' (snd a) ∩ vs)" using Diff_Int_distrib by fast also have " … = (fmdom' (snd a) ∩ s) - (fmdom' (snd a))" using 1 by auto finally have "fmdom' (snd a) ∩ (s - vs) = {}" by simp } ultimately show ?thesis by blast qed ― ‹NOTE added lemma.› lemma list_all_list_mem: fixes P and l :: "'a list" shows "list_all P l ⟷ (∀e. ListMem e l ⟶ P e)" proof - { assume P1: "list_all P l" { fix e assume P11: "ListMem e l" then have "P e" using P1 P11 proof (induction l arbitrary: P) case (insert x xs y) then show ?case proof (cases "y = x") case False then have "list_all P xs" "ListMem x xs" using insert.prems(1) insert.hyps by fastforce+ then show ?thesis using insert.IH by blast qed simp qed simp } } moreover { assume P2: "(∀e. ListMem e l ⟶ P e)" then have "list_all P l" proof(induction l arbitrary: P) case (Cons a l) { have "∀e. ListMem e l ⟶ P e" using Cons.prems insert by fast then have "list_all P l" using Cons.IH by blast } moreover have "P a" using Cons.prems elem by fast ultimately show ?case by simp qed simp } ultimately show ?thesis by blast qed lemma every_vset_imp_drestrict_exec_eq: fixes PROB vs as s assumes "(list_all (λa. varset_action a ((prob_dom PROB) - vs)) as)" shows "(fmrestrict_set vs s = fmrestrict_set vs (exec_plan s as))" proof - have 1: "∀e. ListMem e as ⟶ varset_action e ((prob_dom PROB) - vs)" using assms list_all_list_mem by metis { fix a assume "ListMem a as" then have "varset_action a (prob_dom PROB - vs)" using 1 by blast then have "disjnt (fmdom' (snd a)) vs" unfolding disjnt_def using vset_diff_disj_eff_vs by blast } then have "list_all (λa. disjnt (fmdom' (snd a)) vs) as" using list_all_list_mem by blast then have "list_all (λa. disjnt (fmdom' (snd a)) vs) (rem_condless_act s [] as)" by (simp add: rem_condless_valid_7) then have "exec_plan s as = exec_plan s (rem_condless_act s [] as)" using rem_condless_valid_1 by blast then have"sat_precond_as s (rem_condless_act s [] as)" using rem_condless_valid_2 by blast then have "sat_precond_as s [a←as . ¬ varset_action a (prob_dom PROB - vs)]" by (simp add: 1 ListMem_iff) then have "fmrestrict_set vs s = fmrestrict_set vs s" by simp then have " fmrestrict_set vs (exec_plan s as) = fmrestrict_set vs (exec_plan s [a←as . ¬ varset_action a (prob_dom PROB - vs)]) " using 1 graph_plan_lemma_4[where s = s and s' = s and as = "rem_condless_act s [] as" and vs = vs and P = "λa. varset_action a (prob_dom PROB - vs)" ] filter_empty_every_not vset_diff_disj_eff_vs 1disjoint_effects_no_effects exec_plan.simps(1) fmdom'_restrict_set_precise list_all_list_mem by smt then have "list_all (λa. varset_action a (prob_dom PROB - vs)) (rem_condless_act s [] as)" using assms(1) rem_condless_valid_7 list.pred_inject(1) by blast then have "filter (λa. ¬(varset_action a (prob_dom PROB - vs))) (rem_condless_act s [] as) = []" using filter_empty_every_not by fastforce then have " sat_precond_as s (filter (λa. ¬(varset_action a (prob_dom PROB - vs))) (rem_condless_act s []as)) " by fastforce then show ?thesis using 1 vset_diff_disj_eff_vs disjoint_effects_no_effects fmdom'_restrict_set_precise by metis qed lemma no_effectless_act_works: fixes as assumes "(no_effectless_act as)" shows "(filter (λa. ¬(fmdom' (snd a) = {})) as = as)" using assms by (simp add: Ball_set rem_effectless_works_7) lemma varset_act_diff_un_imp_varset_diff: fixes a vs vs' vs'' assumes "(varset_action a (vs'' - (vs' ∪ vs)))" shows "(varset_action a (vs'' - vs))" using assms unfolding varset_action_def by blast lemma vset_diff_union_vset_diff: fixes s vs vs' a assumes "(varset_action a (s - (vs ∪ vs')))" shows "(varset_action a (s - vs'))" using assms unfolding varset_action_def by blast lemma valid_filter_vset_dom_idempot: fixes PROB as assumes "(as ∈ valid_plans PROB)" shows "(filter (λa. varset_action a (prob_dom PROB)) as = as)" using assms proof (induction as) case (Cons a as) { have "as ∈ valid_plans PROB" using Cons.prems valid_plan_valid_tail by fast then have "(filter (λa. varset_action a (prob_dom PROB)) as = as)" using Cons.IH by blast } moreover { have "a ∈ PROB" using Cons.prems valid_plan_valid_head by fast then have "varset_action a (prob_dom PROB)" unfolding varset_action_def using FDOM_eff_subset_prob_dom_pair by metis } ultimately show ?case by simp qed fastforce lemma n_replace_proj_le_n_as_1: fixes a vs vs' assumes "(vs ⊆ vs')" "(varset_action a vs)" shows "(varset_action a vs')" using assms unfolding varset_action_def by simp lemma sat_precond_as_pfx: fixes s assumes "(sat_precond_as s (as @ as'))" shows "(sat_precond_as s as)" using assms proof (induction as arbitrary: s as') case (Cons a as) have "fst a ⊆⇩_{f}s" using Cons.prems by fastforce moreover have "sat_precond_as (state_succ s a) (as @ as')" using Cons.prems by simp ultimately show ?case using Cons.IH sat_precond_as.simps(2) by blast qed simp end