# Theory FactoredSystemLib

theory FactoredSystemLib imports Main "HOL-Library.Finite_Map" begin section ‹Factored Systems Library› text ‹This section contains definitions used in the factored system theory (FactoredSystem.thy) and in other theories. › subsection ‹Semantics of Map Addition› text ‹ Most importantly, we are redefining the map addition operator (`++`) to reflect HOL4 semantics which are left to right (ltr), rather than right-to-left as in Isabelle/HOL. This means that given a finite map (`M = M1 ++ M2`) and a variable `v` which is in the domain of both `M1` and `M2`, the lookup `M v` will yield `M1 v` in HOL4 but `M2 v` in Isabelle/HOL. This behavior can be confirmed by looking at the definition of `fmap\_add` (`++f`, Finite\_Map.thy:460)---which is lifted from `map\_add` (Map.thy:24) @{const map_add} (infixl "++" 100) where @{term "m1 ++ m2 = (λx. case m2 x of None ⇒ m1 x | Some y ⇒ Some y)"} to finite sets---and the HOL4 definition of "FUNION` (finite\_mapScript.sml:770) which recurs on `union\_lemma` (finite\_mapScript.sml:756) !\^fmap g. ?union. (FDOM union = FDOM f Union (g ` FDOM)) /\ (!x. FAPPLY union x = if x IN FDOM f then FAPPLY f x else FAPPLY g x) The ltr semantics are also reflected in [Abdulaziz et al., Definition 2, p.9]. › ― ‹NOTE hide `Map.map\_add` to free the operator symbol `++` and redefine it to reflect HOL4 map addition semantics.› hide_const (open) Map.map_add no_notation Map.map_add (infixl "++" 100) definition fmap_add_ltr :: "('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap" (infixl "++" 100) where "m1 ++ m2 ≡ m2 ++⇩_{f}m1" subsection ‹States, Actions and Problems.› text ‹ Planning problems are typically formalized by considering possible states and the effect of actions upon these states. In this case we consider a world model in propositional logic: i.e. states are finite maps of variables (with arbitrary type 'a) to boolean values and actions are pairs of states where the first component specifies preconditions and the second component specifies effects (postconditions) of applying the action to a given state. [Abdulaziz et al., Definition 2, p.9] › type_synonym ('a) state = "('a, bool) fmap" type_synonym ('a) action = "('a state × 'a state)" type_synonym ('a) problem = "('a state × 'a state) set" text ‹ For a given action @{term "π = (p, e)"} the action domain @{term "𝒟(π)"} is the set of variables `v` where a value is assigned to `v` in either `p` or `e`, i.e. `p v` or `e v` are defined. [Abdulaziz et al., Definition 2, p.9] › definition action_dom where "action_dom s1 s2 ≡ (fmdom' s1 ∪ fmdom' s2)" ― ‹NOTE lemma `action\_dom\_pair` action\_dom a = FDOM (FST a) Union ((SND a) ` FDOM) was removed because the curried definition of `action\_dom` in the translation makes it redundant.› text ‹ Now, for a given problem (i.e. action set) @{term "δ"}, the problem domain @{term "𝒟(δ)"} is given by the union of the action domains of all actions in @{term "δ"}. [Abdulaziz et al., Definition 3, p.9] Moreover, the set of valid states @{term "U(δ)"} is given by the union over all states whose domain is equal to the problem domain and the set of valid action sequences (or, valid plans) is given by the Kleene closure of @{term "δ"}, i.e. @{term "δ_star = {π. set(π) ⊆ δ}"}. [Abdulaziz et al., Definition 3, p.9] Ultimately, the effect of executing an action `a` on a state `s` is given by calculating the succeding state. In general, the succeding state is either the preceding state---if the action does not apply to the state, i.e. if the preconditions are not met---; or, the union of the effects of the action application and the state. [Abdulaziz et al., Definition 3, p.9] › ― ‹NOTE name shortened to 'prob\_dom'.› ― ‹NOTE lambda added to convert problem pairs to arguments of 'action\_dom'.› definition prob_dom where "prob_dom prob ≡ ⋃ ((λ (s1, s2). action_dom s1 s2) ` prob)" definition valid_states where "valid_states prob ≡ {s. fmdom' s = prob_dom prob}" definition valid_plans where "valid_plans prob ≡ {as. set as ⊆ prob}" definition state_succ where "state_succ s a ≡ (if fst a ⊆⇩_{f}s then (snd a ++ s) else s)" end

# Theory ListUtils

theory ListUtils imports Main "HOL-Library.Sublist" begin ― ‹TODO assure translations * 'sublist' --> 'subseq' * list\_frag l l' --> sublist l' l (switch operands!)› lemma len_ge_0: fixes l shows "length l ≥ 0" by simp lemma len_gt_pref_is_pref: fixes l l1 l2 assumes "(length l2 > length l1)" "(prefix l1 l)" "(prefix l2 l)" shows "(prefix l1 l2)" using assms proof (induction l2 arbitrary: l1 l) case Nil then have "¬(length [] > length l1)" by simp then show ?case using Nil by blast next case (Cons a l2) then show ?case proof(induction l1 arbitrary: l) case Nil then show ?case using Nil_prefix by blast next case (Cons b l1) then show ?case proof(cases l) case Nil then have "¬(prefix (a # l2) l)" by simp then show ?thesis using Cons.prems(4) by simp next case (Cons c l) then have 1: "length l2 > length l1" using Cons.prems(2) by fastforce then show ?thesis using Cons proof(cases l) case Nil then have "l1 = [c]" "l2 = [c]" using Cons.prems(3, 4) local.Cons 1 by fastforce+ then show ?thesis using 1 by auto next case (Cons d l') { thm len_ge_0 have "length l1 ≥ 0" by simp then have "length l2 > 0" using 1 by force then have "l2 ≠ []" using 1 by blast } then have "length (a # l1) ≤ length (b # l2)" using 1 le_eq_less_or_eq by simp then show ?thesis using Cons.prems(3, 4) prefix_length_prefix by fastforce qed qed qed qed lemma nempty_list_append_length_add: fixes l1 l2 l3 assumes "l2 ≠ []" shows "length (l1 @ l3) < length (l1 @ l2 @l3)" using assms by (induction l2) auto lemma append_filter: fixes f1 :: "'a ⇒ bool" and f2 as1 as2 and p :: "'a list" assumes "(as1 @ as2 = filter f1 (map f2 p))" shows "(∃p_1 p_2. (p_1 @ p_2 = p) ∧ (as1 = filter f1 (map f2 p_1)) ∧ (as2 = filter f1 (map f2 p_2)) )" using assms proof (induction p arbitrary: f1 f2 as1 as2) case Nil from Nil have 1: "as1 @ as2 = []" by force then have 2: "as1 = []" "as2 = []" by blast+ let ?p1="[]" let ?p2="[]" from 1 2 have "?p1 @ ?p2 = []" "as1 = (filter f1 (map f2 ?p1))" "as2 = (filter f1 (map f2 ?p2))" subgoal by blast subgoal using 2(1) by simp subgoal using 2(2) by simp done then show ?case by fast next case cons: (Cons a p) then show ?case proof (cases "as1") case Nil from cons.prems Nil have 1: "as2 = filter f1 (map f2 (a # p))" by simp let ?p1="[]" let ?p2="a # p" have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)" subgoal by simp subgoal using Nil by simp subgoal using 1 by auto done then show ?thesis by blast next case (Cons a' p') then show ?thesis proof (cases "¬f1 (f2 a)") case True hence "filter f1 (map f2 (a # p)) = filter f1 (map f2 p)" by fastforce hence "as1 @ as2 = filter f1 (map f2 p)" using cons.prems by argo then obtain p1 p2 where a: "p1 @ p2 = p" "as1 = filter f1 (map f2 p1)" "as2 = filter f1 (map f2 p2)" using cons.IH by meson let ?p1="a # p1" let ?p2="p2" have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)" subgoal using a(1) by fastforce subgoal using True a(2) by auto subgoal using a(3) by blast done then show ?thesis by blast next case False hence "filter f1 (map f2 (a # p)) = f2 a # filter f1 (map f2 p)" by fastforce then have 1: "a' = f2 a" "p' @ as2 = filter f1 (map f2 p)" "as1 = a' # p'" using cons.prems Cons by fastforce+ then obtain p1 p2 where 2: "p1 @ p2 = p" "p' = filter f1 (map f2 p1)" "as2 = filter f1 (map f2 p2)" using cons.IH by meson let ?p1="a # p1" let ?p2="p2" have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)" subgoal using 2(1) by simp subgoal using False 1(1, 3) 2(2) by force subgoal using 2(3) by blast done then show ?thesis by blast qed qed qed ― ‹NOTE types of `f1` and `p` had to be fixed for `append\_eq\_as\_proj\_1`.› lemma append_eq_as_proj_1: fixes f1 :: "'a ⇒ bool" and f2 as1 as2 as3 and p :: "'a list" assumes "(as1 @ as2 @ as3 = filter f1 (map f2 p))" shows "(∃p_1 p_2 p_3. (p_1 @ p_2 @ p_3 = p) ∧ (as1 = filter f1 (map f2 p_1)) ∧ (as2 = filter f1 (map f2 p_2)) ∧ (as3 = filter f1 (map f2 p_3)) )" proof - from assms obtain p_1 p_2 where 1: "(p_1 @ p_2 = p)" "(as1 = filter f1 (map f2 p_1))" "(as2 @ as3 = filter f1 (map f2 p_2))" using append_filter[of as1 "(as2 @ as3)"] by meson moreover from 1 obtain p_a p_b where "(p_a @ p_b = p_2)" "(as2 = filter f1 (map f2 p_a))" "(as3 = filter f1 (map f2 p_b))" using append_filter[where p=p_2] by meson ultimately show ?thesis by blast qed lemma filter_empty_every_not: "⋀P l. (filter (λx. P x) l = []) = list_all (λx. ¬P x) l" proof - fix P l show "(filter (λx. P x) l = []) = list_all (λx. ¬P x) l" apply(induction l) apply(auto) done qed ― ‹NOTE added lemma (listScript.sml:810).› lemma MEM_SPLIT: fixes x l assumes "¬ListMem x l" shows "∀l1 l2. l ≠ l1 @ [x] @ l2" proof - { assume C: "¬(∀l1 l2. l ≠ l1 @ [x] @ l2)" then have "∃l1 l2. l = l1 @ [x] @ l2" by blast then obtain l1 l2 where 1: "l = l1 @ [x] @ l2" by blast from assms have 2: "(∀xs. l ≠ x # xs) ∧ (∀xs. (∀y. l ≠ y # xs) ∨ ¬ ListMem x xs)" using ListMem_iff by fastforce then have False proof (cases l1) case Nil let ?xs="l2" from 1 Nil have "l = [x] @ ?xs" by blast then show ?thesis using 2 by simp next case (Cons a list) { let ?y="a" let ?xs="list @ [x] @ l2" from 1 Cons have "l = ?y # ?xs" by simp moreover have "ListMem x ?xs" by (simp add: ListMem_iff) ultimately have "∃xs. ∃y. l = y # xs ∧ ListMem x xs" by blast then have "¬(∀xs. (∀y. l ≠ y # xs) ∨ ¬ ListMem x xs)" by presburger } then show ?thesis using 2 by auto qed } then show ?thesis by blast qed ― ‹NOTE added lemma (listScript.sml:2784)› lemma APPEND_EQ_APPEND_MID: fixes l1 l2 m1 m2 e shows "(l1 @ [e] @ l2 = m1 @ m2) ⟷ (∃l. (m1 = l1 @ [e] @ l) ∧ (l2 = l @ m2)) ∨ (∃l. (l1 = m1 @ l) ∧ (m2 = l @ [e] @ l2))" proof (induction "l1" arbitrary: m1) case Nil then show ?case by (simp; metis Cons_eq_append_conv)+ next case (Cons a l1) then show ?case by (cases m1; simp; blast) qed ― ‹NOTE variable `P` was removed (redundant).› lemma LIST_FRAG_DICHOTOMY: fixes l la x lb assumes "sublist l (la @ [x] @ lb)" "¬ListMem x l" shows "sublist l la ∨ sublist l lb" proof - { from assms(1) obtain pfx sfx where 1: "pfx @ l @ sfx = la @ [x] @ lb" unfolding sublist_def by force from assms(2) have 2: "∀l1 l2. l ≠ l1 @ [x] @ l2" using MEM_SPLIT[OF assms(2)] by blast from 1 consider (a) "(∃lc. pfx = la @ [x] @ lc ∧ lb = lc @ l @ sfx)" | (b) "(∃lc. la = pfx @ lc ∧ l @ sfx = lc @ [x] @ lb)" using APPEND_EQ_APPEND_MID[of la x lb pfx "l @ sfx"] by presburger then have "∃pfx' sfx. (pfx' @ l @ sfx = la) ∨ (pfx'@ l @ sfx = lb)" proof (cases) case a ― ‹NOTE `lc` is `l'` in original proof.› then obtain lc where a: "pfx = la @ [x] @ lc" "lb = lc @ l @ sfx" by blast then show ?thesis by blast next case b then obtain lc where i: "la = pfx @ lc" "l @ sfx = lc @ [x] @ lb" by blast then show ?thesis using 2 by (metis APPEND_EQ_APPEND_MID) qed } then show ?thesis unfolding sublist_def by blast qed lemma LIST_FRAG_DICHOTOMY_2: fixes l la x lb P assumes "sublist l (la @ [x] @ lb) " "¬P x" "list_all P l" shows "sublist l la ∨ sublist l lb" proof - { assume "¬P x" "list_all P l" then have "¬ListMem x l" proof (induction l arbitrary: x P) case Nil then show ?case using ListMem_iff by force next case (Cons a l) { have "list_all P l" using Cons.prems(2) by simp then have "¬ListMem x l" using Cons.prems(1) Cons.IH by blast } moreover { have "P a" using Cons.prems(2) by simp then have "a ≠ x" using Cons.prems(1) by meson } ultimately show ?case using Cons.prems(1, 2) ListMem_iff list.pred_set by metis qed } then have "¬ListMem x l" using assms(2, 3) by fast then show ?thesis using assms(1) LIST_FRAG_DICHOTOMY by metis qed lemma frag_len_filter_le: fixes P l' l assumes "sublist l' l" shows "length (filter P l') ≤ length (filter P l)" proof - obtain ps ss where "l = ps @ l' @ ss" using assms sublist_def by blast then have 1: "length (filter P l) = length (filter P ps) + length (filter P l') + length (filter P ss)" by force then have "length (filter P ps) ≥ 0" "length (filter P ss) ≥ 0" by blast+ then show ?thesis using 1 by linarith qed end

# Theory FSSublist

(* * cf. planning/hol/sublistScript *) theory FSSublist imports Main "HOL-Library.Sublist" ListUtils begin text ‹ This file is a port of the original HOL4 source file sublistScript.sml. › section "Factored System Sublist" subsection "Sublist Characterization" text ‹ We take a look at the characterization of sublists. As a precursor, we are replacing the original definition of `sublist` in HOL4 (sublistScript.sml:10) with the semantically equivalent `subseq` of Isabelle/HOL's to be able to use the associated theorems and automation. In HOL4 `sublist` is defined as (sublist [] l1 = T) /\ (sublist (h::t) [] = F) /\ (sublist (x::l1) (y::l2) = (x = y) /\ sublist l1 l2 \/ sublist (x::l1) l2) [Abdulaziz et al., HOL4 Definition 10, p.19]. Whereas `subseq` (Sublist.tyh:927) is defined as an abbrevation of `list\_emb` with the predicate @{term "λ x y. x = y"}, i.e. @{term "subseq xs ys ≡ list_emb (=) xs ys"} `list\_emb` itself is defined as an inductive predicate. However, an equivalent function definition is provided in `list\_emb\_code` (Sublist.thy:784) which is very close to `sublist` in HOL4. The correctness of the equivalence claim is shown below by the technical lemma `sublist\_HOL4\_equiv\_subseq` (where the HOL4 definition of `sublist` is renamed to `sublist\_HOL4`). › ― ‹NOTE added definition› fun sublist_HOL4 where "sublist_HOL4 [] l1 = True" | "(sublist_HOL4 (h # t) [] = False)" | "(sublist_HOL4 (x # l1) (y # l2) = ((x = y) ∧ sublist_HOL4 l1 l2 ∨ sublist_HOL4 (x # l1) l2))" ― ‹NOTE added lemma› lemma sublist_HOL4_equiv_subseq: fixes l1 l2 shows "sublist_HOL4 l1 l2 ⟷ subseq l1 l2" proof - have "subseq l1 l2 = list_emb (λx y. x = y) l1 l2" by blast moreover { have "sublist_HOL4 l1 l2 ⟷ list_emb (λx y. x = y) l1 l2" proof (induction rule: sublist_HOL4.induct) case (3 x l1 y l2) then show "sublist_HOL4 (x # l1) (y # l2) ⟷ list_emb (λx y. x = y) (x # l1) (y # l2)" proof (cases "x = y") case True then show ?thesis using "3.IH"(1, 2) by (metis sublist_HOL4.simps(3) subseq_Cons' subseq_Cons2_iff) next case False then show ?thesis using "3.IH"(2) by force qed qed simp+ } ultimately show ?thesis by blast qed text ‹ Likewise as with `sublist` and `subseq`, the HOL4 definition of `list\_frag` (list\_utilsScript.sml:207) has a an Isabelle/HOL counterpart in `sublist` (Sublist.thy:1124). The equivalence claim is proven in the technical lemma `list\_frag\_HOL4\_equiv\_sublist`. Note that `sublist` reverses the argument order of `list\_frag`. Other than that, both definitions are syntactically identical. › definition list_frag_HOL4 where "list_frag_HOL4 l frag ≡ ∃pfx sfx. pfx @ frag @ sfx = l" lemma list_frag_HOL4_equiv_sublist: shows "list_frag_HOL4 l l' ⟷ sublist l' l" unfolding list_frag_HOL4_def sublist_def by blast text ‹ Given these equivalences, occurences of `sublist` and `list\_frag` in the original HOL4 source are now always translated directly to `subseq` and `sublist` respectively. The remainer of this subsection is concerned with characterizations of `sublist`/ `subseq`. › lemma sublist_EQNS: "subseq [] l = True" "subseq (h # t) [] = False" by auto lemma sublist_refl: "subseq l l" by auto lemma sublist_cons: assumes "subseq l1 l2" shows "subseq l1 (h # l2)" using assms by blast lemma sublist_NIL: "subseq l1 [] = (l1 = [])" by fastforce lemma sublist_trans: fixes l1 l2 assumes "subseq l1 l2" "subseq l2 l3" shows "subseq l1 l3" using assms by force ― ‹NOTE can be solved directly with 'list\_emb\_length'.› lemma sublist_length: fixes l l' assumes "subseq l l'" shows "length l ≤ length l'" using assms list_emb_length by blast ― ‹NOTE can be solved directly with subseq\_Cons'.› lemma sublist_CONS1_E: fixes l1 l2 assumes "subseq (h # l1) l2" shows "subseq l1 l2" using assms subseq_Cons' by metis lemma sublist_equal_lengths: fixes l1 l2 assumes "subseq l1 l2" "(length l1 = length l2)" shows "(l1 = l2)" using assms subseq_same_length by blast ― ‹NOTE can be solved directly with 'subseq\_order.antisym'.› lemma sublist_antisym: assumes "subseq l1 l2" "subseq l2 l1" shows "(l1 = l2)" using assms subseq_order.antisym by blast lemma sublist_append_back: fixes l1 l2 shows "subseq l1 (l2 @ l1)" by blast ― ‹NOTE can be solved directly with 'subseq\_rev\_drop\_many'.› lemma sublist_snoc: fixes l1 l2 assumes "subseq l1 l2" shows "subseq l1 (l2 @ [h])" using assms subseq_rev_drop_many by blast lemma sublist_append_front: fixes l1 l2 shows "subseq l1 (l1 @ l2)" by fast lemma append_sublist_1: assumes "subseq (l1 @ l2) l" shows "subseq l1 l ∧ subseq l2 l" using assms sublist_append_back sublist_append_front sublist_trans by blast ― ‹NOTE added lemma (eventually wasn't needed in the remaining proofs).› lemma sublist_prefix: shows "subseq (h # l1) l2 ⟹ ∃l2a l2b. l2 = l2a @ [h] @ l2b ∧ ¬ListMem h l2a" proof (induction l2 arbitrary: h l1) ― ‹NOTE l2 cannot be empty when @{term "(h # l1)"} isn't.› case Nil have "¬(subseq (h # l1) [])" by simp then show ?case using Nil.prems by blast next case (Cons a l2) then show ?case proof (cases "a = h") ― ‹NOTE If a = h then a trivial solution exists in l2a = [] and l2b = l2.› case True then show "∃ l2a l2b. (Cons a l2) = l2a @ [h] @ l2b ∧ ¬ListMem h l2a" using ListMem_iff by force next case False have "subseq (h # l1) l2" using Cons.prems False subseq_Cons2_neq by force then obtain l2a l2b where "l2 = l2a @ [h] @ l2b" "¬ListMem h l2a" using Cons.IH Cons.prems by meson moreover have "a # l2 = (a # l2a) @ [h] @ l2b" using calculation(1) by simp moreover have "¬(ListMem h (a # l2a))" using False calculation(2) ListMem.simps by fastforce ultimately show ?thesis by blast qed qed ― ‹NOTE added lemma (eventually wasn't needed in the remaining proofs).› lemma sublist_skip: fixes l1 l2 h l1' assumes "l1 = (h # l1')" "l2 = l2a @ [h] @ l2b" "subseq l1 l2" "¬(ListMem h l2a)" shows "subseq l1 (h # l2b)" using assms proof (induction l2a arbitrary: l1 l2 h l1') case Nil then have "l2 = h # l2b" by fastforce then show ?case using Nil.prems(3) by blast next case (Cons a l2a) have "a ≠ h" using Cons.prems(4) ListMem.simps by fast then have "subseq l1 (l2a @ [h] @ l2b)" using Cons.prems(1, 2, 3) subseq_Cons2_neq by force moreover have "¬ListMem h l2a" using Cons.prems(4) insert by metis ultimately have "subseq l1 (h # l2b)" using Cons.IH Cons.prems by meson then show ?case by simp qed ― ‹NOTE added lemma (eventually wasn't needed in the remaining proofs).› lemma sublist_split_trans: fixes l1 l2 h l1' assumes "l1 = (h # l1')" "l2 = l2a @ [h] @ l2b" "subseq l1 l2" "¬(ListMem h l2a)" shows "subseq l1' l2b" proof - have "subseq (h # l1') (h # l2b)" using assms sublist_skip by metis then show ?thesis using subseq_Cons2' by metis qed lemma sublist_cons_exists: shows " subseq (h # l1) l2 ⟷ (∃l2a l2b. (l2 = l2a @ [h] @ l2b) ∧ ¬ListMem h l2a ∧ subseq l1 l2b) " proof - ― ‹NOTE show both directions of the equivalence in pure proof blocks.› { have "subseq (h # l1) l2 ⟹ (∃l2a l2b. (l2 = l2a @ [h] @ l2b) ∧ ¬ListMem h l2a ∧ subseq l1 l2b)" proof (induction l2 arbitrary: h l1) case (Cons a l2) show ?case proof (cases "a = h") case True ― ‹NOTE This case has a trivial solution in '?l2a = []', '?l2b = l2'.› let ?l2a="[]" have "(a # l2) = ?l2a @ [h] @ l2" using True by auto moreover have "¬(ListMem h ?l2a)" using ListMem_iff by force moreover have "subseq l1 l2" using Cons.prems True by simp ultimately show ?thesis by blast next case False have 1: "subseq (h # l1) l2" using Cons.prems False subseq_Cons2_neq by metis then obtain l2a l2b where "l2 = l2a @ [h] @ l2b" "¬ListMem h l2a" using Cons.IH Cons.prems by meson moreover have "a # l2 = (a # l2a) @ [h] @ l2b" using calculation(1) by simp moreover have "¬(ListMem h (a # l2a))" using False calculation(2) ListMem.simps by fastforce ultimately show ?thesis using 1 sublist_split_trans by metis qed qed simp } moreover { assume "∃l2a l2b. (l2 = l2a @ [h] @ l2b) ∧ ¬ListMem h l2a ∧ subseq l1 l2b" then have "subseq (h # l1) l2" by auto } ultimately show ?thesis by argo qed lemma sublist_append_exists: fixes l1 l2 shows "subseq (l1 @ l2) l3 ⟹ ∃l3a l3b. (l3 = l3a @ l3b) ∧ subseq l1 l3a ∧ subseq l2 l3b" using list_emb_appendD by fast ― ‹NOTE can be solved directly with 'list\_emb\_append\_mono'.› lemma sublist_append_both_I: assumes "subseq a b" "subseq c d" shows "subseq (a @ c) (b @ d)" using assms list_emb_append_mono by blast lemma sublist_append: assumes "subseq l1 l1'" "subseq l2 l2'" shows "subseq (l1 @ l2) (l1' @ l2')" using assms sublist_append_both_I by blast lemma sublist_append2: assumes "subseq l1 l2" shows "subseq l1 (l2 @ l3)" using assms sublist_append[of "l1" "l2" "[]" "l3"] by fast lemma append_sublist: shows "subseq (l1 @ l2 @ l3) l ⟹ subseq (l1 @ l3) l" proof (induction l) case Nil then show ?case using sublist_NIL by fastforce next case (Cons a l) then show ?case proof (cases l1) case Nil then show ?thesis using Cons.prems append_sublist_1 by auto next case (Cons a list) then show ?thesis using Cons.prems subseq_append' subseq_order.dual_order.trans by blast qed qed lemma sublist_subset: assumes "subseq l1 l2" shows "set l1 ⊆ set l2" using assms set_nths_subset subseq_conv_nths by metis lemma sublist_filter: fixes P l shows "subseq (filter P l) l" using subseq_filter_left by blast lemma sublist_cons_2: fixes l1 l2 h shows "(subseq (h # l1) (h # l2) ⟷ (subseq l1 l2))" by fastforce lemma sublist_every: fixes l1 l2 P assumes "(subseq l1 l2 ∧ list_all P l2)" shows "list_all P l1" by (metis (full_types) Ball_set assms list_emb_set) lemma sublist_SING_MEM: "subseq [h] l ⟷ ListMem h l" using ListMem_iff subseq_singleton_left by metis ― ‹NOTE renamed due to previous declaration of `sublist\_append\_exists\_2.› lemma sublist_append_exists_2: fixes l1 l2 l3 assumes "subseq (h # l1) l2" shows "(∃l3 l4. (l2 = l3 @ [h] @ l4) ∧ (subseq l1 l4))" using assms sublist_cons_exists by metis lemma sublist_append_4: fixes l l1 l2 h assumes "(subseq (h # l) (l1 @ [h] @ l2))" "(list_all (λx. ¬(h = x)) l1)" shows "subseq l l2" using assms proof (induction l1) qed auto lemma sublist_append_5: fixes l l1 l2 h assumes "(subseq (h # l) (l1 @ l2))" "(list_all (λx. ¬(h = x)) l1)" shows "subseq (h # l) l2" using assms proof (induction l1) qed auto lemma sublist_append_6: fixes l l1 l2 h assumes "(subseq (h # l) (l1 @ l2))" "(¬(ListMem h l1))" shows "subseq (h # l) l2" using assms proof (induction l1) case (Cons a l1) then show ?case by (simp add: ListMem_iff) qed simp lemma sublist_MEM: fixes h l1 l2 shows "subseq (h # l1) l2 ⟹ ListMem h l2" proof (induction l2) next case (Cons a l2) then show ?case using elem insert subseq_Cons2_neq by metis qed simp lemma sublist_cons_4: fixes l h l' shows "subseq l l' ⟹ subseq l (h # l')" using sublist_cons by blast subsection "Main Theorems" theorem sublist_imp_len_filter_le: fixes P l l' assumes "subseq l' l" shows "length (filter P l') ≤ length (filter P l)" using assms by (simp add: sublist_length) ― ‹TODO showcase (non-trivial proof translation/ obscurity).› theorem list_with_three_types_shorten_type2: fixes P1 P2 P3 k1 f PProbs PProbl s l assumes "(PProbs s)" "(PProbl l)" "(∀l s. (PProbs s) ∧ (PProbl l) ∧ (list_all P1 l) ⟶ (∃l'. (f s l' = f s l) ∧ (length (filter P2 l') ≤ k1) ∧ (length (filter P3 l') ≤ length (filter P3 l)) ∧ (list_all P1 l') ∧ (subseq l' l) ) )" "(∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2))" "(∀s l. (PProbs s) ∧ (PProbl l) ⟶ (PProbs (f s l)))" "(∀l1 l2. (subseq l1 l2) ∧ (PProbl l2) ⟶ (PProbl l1))" "(∀l1 l2. PProbl (l1 @ l2) ⟷ (PProbl l1 ∧ PProbl l2))" shows "(∃l'. (f s l' = f s l) ∧ (length (filter P3 l') ≤ length (filter P3 l)) ∧ (∀l''. (sublist l'' l') ∧ (list_all P1 l'') ⟶ (length (filter P2 l'') ≤ k1) ) ∧ (subseq l' l) )" using assms proof (induction "filter (λx. ¬P1 x) l" arbitrary: P1 P2 P3 k1 f PProbs PProbl s l) case Nil then have "list_all (λx. P1 x) l" using Nil(1) filter_empty_every_not[of "λx. ¬P1 x" l] by presburger then obtain l' where 1: "(f s l' = f s l)" "length (filter P2 l') ≤ k1" "length (filter P3 l') ≤ length (filter P3 l)" "list_all P1 l'" "subseq l' l" using Nil.prems(1, 2, 3) by blast moreover { fix l'' assume "sublist l'' l'" "list_all P1 l''" then have "subseq l'' l'" by blast ― ‹NOTE original proof uses `frag\_len\_filter\_le` which however requires the fact `sublist l' ?l`. Unfortunately, this could not be derived in Isabelle/HOL.› then have "length (filter P2 l'') ≤ length (filter P2 l')" using sublist_imp_len_filter_le by blast then have "length (filter P2 l'') ≤ k1" using 1 by linarith } ultimately show ?case by blast next case (Cons a x) ― ‹NOTE The proof of the induction step basically consists of construction a list `?l'=l'' @ [a] @ l'''` where `l''` and `l'''` are lists obtained from certain specifications of the induction hypothesis.› then obtain l1 l2 where 2: "l = l1 @ a # l2" "(∀u∈set l1. P1 u)" "¬ P1 a ∧ x = [x←l2 . ¬ P1 x]" using Cons(2) filter_eq_Cons_iff[of "λx. ¬P1 x"] by metis then have 3: "PProbl l2" using Cons.prems(2, 6) 2(1) sublist_append_back by blast ― ‹NOTE Use the induction hypothesis to obtain a specific `l'''`.› { have "x = filter (λx. ¬P1 x) l2" using 2(3) by blast moreover have "PProbs (f (f s l1) [a])" using Cons.prems(1, 2, 5, 6, 7) 2(1) elem sublist_SING_MEM by metis moreover have "∀l s. PProbs s ∧ PProbl l ∧ list_all P1 l ⟶ (∃l'. f s l' = f s l ∧ length (filter P2 l') ≤ k1 ∧ length (filter P3 l') ≤ length (filter P3 l) ∧ list_all P1 l' ∧ subseq l' l)" using Cons.prems(3) by blast moreover have "∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2)" "∀s l. PProbs s ∧ PProbl l ⟶ PProbs (f s l)" "∀l1 l2. subseq l1 l2 ∧ PProbl l2 ⟶ PProbl l1" "∀l1 l2. PProbl (l1 @ l2) = (PProbl l1 ∧ PProbl l2)" using Cons.prems(4, 5, 6, 7) by blast+ ultimately have "∃l'. f (f (f s l1) [a]) l' = f (f (f s l1) [a]) l2 ∧ length (filter P3 l') ≤ length (filter P3 l2) ∧ (∀l''. sublist l'' l' ∧ list_all P1 l'' ⟶ length (filter P2 l'') ≤ k1) ∧ subseq l' l2" using 3 Cons(1)[of P1 l2, where s="(f (f s l1) [a])"] by blast } then obtain l''' where 4: "f (f (f s l1) [a]) l''' = f (f (f s l1) [a]) l2" "length (filter P3 l''') ≤ length (filter P3 l2)" "(∀l''. sublist l'' l''' ∧ list_all P1 l'' ⟶ length (filter P2 l'') ≤ k1) ∧ subseq l''' l2" by blast then have "f s (l1 @ [a] @ l''') = f s (l1 @ [a] @ l2)" using Cons.prems(4) by auto then have "subseq l''' l2" using 4(3) by blast ― ‹NOTE Use the induction hypothesis to obtain a specific `l''`.› { have "∀l s. PProbs s ∧ PProbl l1 ∧ list_all P1 l1 ⟶ (∃l''. f s l'' = f s l1 ∧ length (filter P2 l'') ≤ k1 ∧ length (filter P3 l'') ≤ length (filter P3 l1) ∧ list_all P1 l'' ∧ subseq l'' l1)" using Cons.prems(3) by blast then have "∃l''. f s l'' = f s l1 ∧ length (filter P2 l'') ≤ k1 ∧ length (filter P3 l'') ≤ length (filter P3 l1) ∧ list_all P1 l'' ∧ subseq l'' l1" using Cons.prems(1, 2, 7) 2(1, 2) by (metis Ball_set) } then obtain l'' where 5: "f s l'' = f s l1" "length (filter P2 l'') ≤ k1" "length (filter P3 l'') ≤ length (filter P3 l1)" "list_all P1 l'' ∧ subseq l'' l1" by blast text ‹ Proof the proposition by providing the witness @{term "l'=(l'' @ [a] @ l''')"}. › let ?l'="(l'' @ [a] @ l''') " { have "∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2)" by (simp add: Cons.prems(4)) text ‹ Rewrite and show the goal.› have "f s ?l' = f s (l1 @ [a] @ l2) ⟷ f s (l'' @ (a # l''')) = f s (l1 @ (a # l2))" by simp also have "… ⟷ f (f (f s l1) [a]) l''' = f (f (f s l1) [a]) l2" by (metis Cons.prems(4) ‹f s l'' = f s l1› calculation) finally have "f s ?l' = f s (l1 @ [a] @ l2)" using 4(1) by blast } moreover { have " length (filter P3 ?l') ≤ length (filter P3 (l1 @ [a] @ l2)) ⟷ (length (filter P3 l'') + 1 + length (filter P3 l''') ≤ length (filter P3 l1) + 1 + length (filter P3 l2))" by force then have " length (filter P3 ?l') ≤ length (filter P3 (l1 @ [a] @ l2)) ⟷ length (filter P3 l'') + length (filter P3 l''') ≤ length (filter P3 l1) + length (filter P3 l2)" by linarith then have "length (filter P3 ?l') ≤ length (filter P3 (l1 @ [a] @ l2))" using 4(2) ‹length (filter P3 l'') ≤ length (filter P3 l1)› add_mono_thms_linordered_semiring(1) by blast } moreover { fix l'''' assume P: "sublist l'''' ?l'" "list_all P1 l''''" have "list_all P1 l1" using 2(2) Ball_set by blast consider (i) "sublist l'''' l''" | (ii) "sublist l'''' l'''" using P(1, 2) 2(3) LIST_FRAG_DICHOTOMY_2 by metis then have "length (filter P2 l'''') ≤ k1" proof (cases) case i then have "length (filter P2 l'''') ≤ length (filter P2 l'')" using frag_len_filter_le by blast then show ?thesis using 5(2) order_trans by blast next case ii then show ?thesis using 4(3) P(2) by blast qed } ― ‹NOTE the following two steps seem to be necessary to convince Isabelle that the split @{term "l = l1 @ a # l2"} matches the split `(l1 @ [a] @ l2` and the previous proof steps therefore is prove the goal.› moreover { have "subseq ?l' (l1 @ [a] @ l2)" by (simp add: FSSublist.sublist_append ‹list_all P1 l'' ∧ subseq l'' l1› ‹subseq l''' l2›) } moreover have "l = l1 @ [a] @ l2" using 2 by force ultimately show ?case by blast qed lemma isPREFIX_sublist: fixes x y assumes "prefix x y" shows "subseq x y" using assms prefix_order.dual_order.antisym by blast end

# Theory HoArithUtils

theory HoArithUtils imports Main begin lemma general_theorem: fixes P f and l :: nat assumes "(∀p. P p ∧ f p > l ⟶ (∃p'. P p' ∧ f p' < f p))" shows "(∀p. P p ⟶ (∃p'. P p' ∧ f p' ≤ l))" proof- have "∀p. (n = f p) ∧ P p ⟶ (∃p'. P p' ∧ f p' ≤ l)" for n apply(rule Nat.nat_less_induct[where ?P = "%n. ∀p. (n = f p) ∧ P p ⟶ (∃p'. P p' ∧ f p' ≤ l)"]) by (metis assms not_less) then show ?thesis by auto qed end

# Theory FmapUtils

theory FmapUtils imports "HOL-Library.Finite_Map" FactoredSystemLib begin ― ‹TODO A lemma 'fmrestrict\_set\_twice\_eq' 'fmrestrict\_set ?vs (fmrestrict\_set ?vs ?f) = fmrestrict\_set ?vs ?f' to replace the recurring proofs steps using 'by (simp add: fmfilter\_alt\_defs(4))' would make sense.› ― ‹NOTE hide the '++' operator from 'Map' to prevent warnings.› hide_const (open) Map.map_add no_notation Map.map_add (infixl "++" 100) ― ‹TODO more explicit proof.› lemma IN_FDOM_DRESTRICT_DIFF: fixes vs v f assumes "¬(v ∈ vs)" "fmdom' f ⊆ fdom" "v ∈ fmdom' f" shows "v ∈ fmdom' (fmrestrict_set (fdom - vs) f)" using assms by (metis DiffI Int_def Int_iff Set.filter_def fmdom'_filter fmfilter_alt_defs(4) inf.order_iff) lemma disj_dom_drest_fupdate_eq: " disjnt (fmdom' x) vs ⟹ (fmrestrict_set vs s = fmrestrict_set vs (x ++ s)) " proof - fix vs s x assume P: "disjnt (fmdom' x) vs" moreover have 1: "∀x''. (x'' ∈ vs) ⟶ (fmlookup (x ++ s) x'' = fmlookup s x'')" by (metis calculation disjnt_iff fmap_add_ltr_def fmdom'_notD fmdom_notI fmlookup_add) moreover { fix x'' have "fmlookup (fmrestrict_set vs s) x'' = fmlookup (fmrestrict_set vs (x ++ s)) x''" apply(cases "x'' ∉ fmdom' x") apply(cases "x'' ∉ vs") apply(auto simp add: "1") done } ultimately show "(fmrestrict_set vs s = fmrestrict_set vs (x ++ s))" using fmap_ext by blast qed ― ‹TODO refactor into 'FmapUtils.thy'.› lemma graph_plan_card_state_set: fixes PROB vs assumes "finite vs" shows "card (fmdom' (fmrestrict_set vs s)) ≤ card vs" proof - let ?vs' = "fmdom' (fmrestrict_set vs s)" have "?vs' ⊆ vs" using fmdom'_restrict_set by metis moreover have "card ?vs' ≤ card vs" using assms calculation card_mono by blast ultimately show ?thesis by blast qed lemma exec_drest_5: fixes x vs assumes "fmdom' x ⊆ vs" shows "(fmrestrict_set vs x = x)" proof - ― ‹TODO refactor and make into ISAR proof.› { fix v have "fmlookup (fmrestrict_set vs x) v = fmlookup x v" apply(cases "v ∈ fmdom' x") subgoal using assms by auto subgoal by (simp add: fmdom'_notD) done then have "fmlookup (fmrestrict_set vs x) v = fmlookup x v" by fast } moreover have "fmlookup (fmrestrict_set vs x) = fmlookup x" using calculation fmap_ext by auto ultimately show ?thesis using fmlookup_inject by blast qed lemma graph_plan_lemma_5: fixes s s' vs assumes "(fmrestrict_set (fmdom' s - vs) s = fmrestrict_set (fmdom' s' - vs) s')" "(fmrestrict_set vs s = fmrestrict_set vs s')" shows "(s = s')" proof - have "∀x. fmlookup s x = fmlookup s' x" using assms(1, 2) fmdom'_notD fminusI fmlookup_restrict_set Diff_iff by metis then show ?thesis using fmap_ext by blast qed lemma drest_smap_drest_smap_drest: fixes x s vs shows "fmrestrict_set vs x ⊆⇩_{f}s ⟷ fmrestrict_set vs x ⊆⇩_{f}fmrestrict_set vs s" proof - ― ‹TODO this could be refactored into standalone lemma since it's very common in proofs.› have 1: "fmlookup (fmrestrict_set vs s) ⊆⇩_{m}fmlookup s" by (metis fmdom'.rep_eq fmdom'_notI fmlookup_restrict_set map_le_def) moreover { assume P1: "fmrestrict_set vs x ⊆⇩_{f}s" moreover have 2: "fmlookup (fmrestrict_set vs x) ⊆⇩_{m}fmlookup s" using P1 fmsubset.rep_eq by blast { fix v assume "v ∈ fmdom' (fmrestrict_set vs x)" then have "fmlookup (fmrestrict_set vs x) v = fmlookup (fmrestrict_set vs s) v" by (metis (full_types) "2" domIff fmdom'_notI fmlookup_restrict_set map_le_def) } ultimately have "fmrestrict_set vs x ⊆⇩_{f}fmrestrict_set vs s" unfolding fmsubset.rep_eq by (simp add: map_le_def) } moreover { assume P2: "fmrestrict_set vs x ⊆⇩_{f}fmrestrict_set vs s" moreover have "fmrestrict_set vs s ⊆⇩_{f}s" using 1 fmsubset.rep_eq by blast ultimately have "fmrestrict_set vs x ⊆⇩_{f}s" using fmsubset.rep_eq map_le_trans by blast } ultimately show ?thesis by blast qed lemma sat_precond_as_proj_1: fixes s s' vs x assumes "fmrestrict_set vs s = fmrestrict_set vs s'" shows "fmrestrict_set vs x ⊆⇩_{f}s ⟷ fmrestrict_set vs x ⊆⇩_{f}s'" using assms drest_smap_drest_smap_drest by metis lemma sat_precond_as_proj_4: fixes fm1 fm2 vs assumes "fm2 ⊆⇩_{f}fm1" shows "(fmrestrict_set vs fm2 ⊆⇩_{f}fm1)" using assms fmpred_restrict_set fmsubset_alt_def by metis lemma sublist_as_proj_eq_as_1: fixes x s vs assumes "(x ⊆⇩_{f}fmrestrict_set vs s)" shows "(x ⊆⇩_{f}s)" using assms by (meson fmsubset.rep_eq fmsubset_alt_def fmsubset_pred drest_smap_drest_smap_drest map_le_refl) lemma limited_dom_neq_restricted_neq: assumes "fmdom' f1 ⊆ vs" "f1 ++ f2 ≠ f2" shows "fmrestrict_set vs (f1 ++ f2) ≠ fmrestrict_set vs f2" proof - { assume C: "fmrestrict_set vs (f1 ++ f2) = fmrestrict_set vs f2" then have "∀x ∈ fmdom' (fmrestrict_set vs (f1 ++ f2)). fmlookup (fmrestrict_set vs (f1 ++ f2)) x = fmlookup (fmrestrict_set vs f2) x" by simp obtain v where a: "v ∈ fmdom' f1" "fmlookup (f1 ++ f2) v ≠ fmlookup f2 v" using assms(2) by (metis fmap_add_ltr_def fmap_ext fmdom'_notD fmdom_notI fmlookup_add) then have b: "v ∈ vs" using assms(1) by blast moreover { have "fmdom' (fmrestrict_set vs (f1 ++ f2)) = vs ∩ fmdom' (f1 ++ f2)" by (simp add: fmdom'_alt_def fmfilter_alt_defs(4)) then have "v ∈ fmdom' (fmrestrict_set vs (f1 ++ f2))" using C a b by fastforce } then have False by (metis C a(2) calculation fmlookup_restrict_set) } then show ?thesis by auto qed lemma fmlookup_fmrestrict_set_dom: "⋀vs s. dom (fmlookup (fmrestrict_set vs s)) = vs ∩ (fmdom' s)" by (auto simp add: fmdom'_restrict_set_precise) end

# Theory FactoredSystem

theory FactoredSystem imports Main "HOL-Library.Finite_Map" "HOL-Library.Sublist" FSSublist FactoredSystemLib ListUtils HoArithUtils FmapUtils begin section "Factored System" ― ‹NOTE hide the '++' operator from 'Map' to prevent warnings.› hide_const (open) Map.map_add no_notation Map.map_add (infixl "++" 100) subsection "Semantics of Plan Execution" text ‹ This section aims at characterizing the semantics of executing plans---i.e. sequences of actions---on a given initial state. The semantics of action execution were previously introduced via the notion of succeding state (`state\_succ`). Plan execution (`exec\_plan`) extends this notion to sequences of actions by calculating the succeding state from the given state and action pair and then recursively executing the remaining actions on the succeding state. [Abdulaziz et al., HOL4 Definition 3, p.9] › lemma state_succ_pair: "state_succ s (p, e) = (if (p ⊆⇩_{f}s) then (e ++ s) else s)" by (simp add: state_succ_def) ― ‹NOTE shortened to 'exec\_plan'› ― ‹NOTE using 'fun' because of multiple definining equations.› ― ‹NOTE first argument was curried.› fun exec_plan where "exec_plan s [] = s" | "exec_plan s (a # as) = exec_plan (state_succ s a) as" lemma exec_plan_Append: fixes as_a as_b s shows "exec_plan s (as_a @ as_b) = exec_plan (exec_plan s as_a) as_b" by (induction as_a arbitrary: s as_b) auto text ‹ Plan execution effectively eliminates cycles: i.e., if a given plan `as` may be partitioned into plans `as1`, `as2` and `as3`, s.t. the sequential execution of `as1` and `as2` yields the same state, `as2` may be skipped during plan execution. › lemma cycle_removal_lemma: fixes as1 as2 as3 assumes "(exec_plan s (as1 @ as2) = exec_plan s as1)" shows "(exec_plan s (as1 @ as2 @ as3) = exec_plan s (as1 @ as3))" using assms exec_plan_Append by metis subsubsection "Characterization of the Set of Possible States" text ‹ To show the construction principle of the set of possible states---in lemma `construction\_of\_all\_possible\_states\_lemma`---the following ancillary proves of finite map properties are required. Most importantly, in lemma `fmupd\_fmrestrict\_subset` we show how finite mappings `s` with domain @{term "{v} ∪ X"} and `s v = (Some x)` are constructed from their restrictions to `X` via update, i.e. s = fmupd v x (fmrestrict\_set X s) This is used in lemma `construction\_of\_all\_possible\_states\_lemma` to show that the set of possible states for variables @{term "{v} ∪ X"} is constructed inductively from the set of all possible states for variables `X` via update on point @{term "v ∉ X"}. › ― ‹NOTE added lemma.› lemma empty_domain_fmap_set: "{s. fmdom' s = {}} = {fmempty}" proof - let ?A = "{s. fmdom' s = {}}" let ?B = "{fmempty}" fix s show ?thesis proof(rule ccontr) assume C: "?A ≠ ?B" then show False proof - { assume C1: "?A ⊂ ?B" have "?A = {}" using C1 by force then have False using fmdom'_empty by blast } moreover { assume C2: "¬(?A ⊂ ?B)" then have "fmdom' fmempty = {}" by auto moreover have "fmempty ∈ ?A" by auto moreover have "?A ≠ {}" using calculation(2) by blast moreover have "∀a∈?A.a∉?B" by (metis (mono_tags, lifting) C Collect_cong calculation(1) fmrestrict_set_dom fmrestrict_set_null singleton_conv) moreover have "fmempty ∈ ?B" by auto moreover have "∃a∈?A.a∈?B" by simp moreover have "¬(∀a∈?A.a∉?B)" by simp ultimately have False by blast } ultimately show False by fastforce qed qed qed ― ‹NOTE added lemma.› lemma possible_states_set_ii_a: fixes s x v assumes "(v ∈ fmdom' s)" shows "(fmdom' ((λs. fmupd v x s) s) = fmdom' s)" using assms insert_absorb by auto ― ‹NOTE added lemma.› lemma possible_states_set_ii_b: fixes s x v assumes "(v ∉ fmdom' s)" shows "(fmdom' ((λs. fmupd v x s) s) = fmdom' s ∪ {v})" by auto ― ‹NOTE added lemma.› lemma fmap_neq: fixes s :: "('a, bool) fmap" and s' :: "('a, bool) fmap" assumes "(fmdom' s = fmdom' s')" shows "((s ≠ s') ⟷ (∃v∈(fmdom' s). fmlookup s v ≠ fmlookup s' v))" using assms fmap_ext fmdom'_notD by metis ― ‹NOTE added lemma.› lemma fmdom'_fmsubset_restrict_set: fixes X1 X2 and s :: "('a, bool) fmap" assumes "X1 ⊆ X2" "fmdom' s = X2" shows "fmdom' (fmrestrict_set X1 s) = X1" using assms by (metis (no_types, lifting) antisym_conv fmdom'_notD fmdom'_notI fmlookup_restrict_set rev_subsetD subsetI) ― ‹NOTE added lemma.› lemma fmsubset_restrict_set: fixes X1 X2 and s :: "'a state" assumes "X1 ⊆ X2" "s ∈ {s. fmdom' s = X2}" shows "fmrestrict_set X1 s ∈ {s. fmdom' s = X1}" using assms fmdom'_fmsubset_restrict_set by blast ― ‹NOTE added lemma.› lemma fmupd_fmsubset_restrict_set: fixes X v x and s :: "'a state" assumes "s ∈ {s. fmdom' s = insert v X}" "fmlookup s v = Some x" shows "s = fmupd v x (fmrestrict_set X s)" proof - ― ‹Show that domains of 's' and 'fmupd v x (fmrestrict\_set X s)' are identical.› have 1: "fmdom' s = insert v X" using assms(1) by simp { have "X ⊆ insert v X" by auto then have "fmdom' (fmrestrict_set X s) = X" using 1 fmdom'_fmsubset_restrict_set by metis then have "fmdom' (fmupd v x (fmrestrict_set X s)) = insert v X" using assms(1) fmdom'_fmupd by auto } note 2 = this moreover { fix w ― ‹Show case for undefined variables (where lookup yields 'None').› { assume "w ∉ insert v X" then have "w ∉ fmdom' s" "w ∉ fmdom' (fmupd v x (fmrestrict_set X s))" using 1 2 by argo+ then have "fmlookup s w = fmlookup (fmupd v x (fmrestrict_set X s)) w" using fmdom'_notD by metis } ― ‹Show case for defined variables (where lookup yields 'Some y').› moreover { assume "w ∈ insert v X" then have "w ∈ fmdom' s" "w ∈ fmdom' (fmupd v x (fmrestrict_set X s))" using 1 2 by argo+ then have "fmlookup s w = fmlookup (fmupd v x (fmrestrict_set X s)) w" by (cases "w = v") (auto simp add: assms calculation) } ultimately have "fmlookup s w = fmlookup (fmupd v x (fmrestrict_set X s)) w" by blast } then show ?thesis using fmap_ext by blast qed lemma construction_of_all_possible_states_lemma: fixes v X assumes "(v ∉ X)" shows "({s. fmdom' s = insert v X} = ((λs. fmupd v True s) ` {s. fmdom' s = X}) ∪ ((λs. fmupd v False s) ` {s. fmdom' s = X}) )" proof - fix v X let ?A = "{s :: 'a state. fmdom' s = insert v X}" let ?B = " ((λs. fmupd v True s) ` {s :: 'a state. fmdom' s = X}) ∪ ((λs. fmupd v False s) ` {s :: 'a state. fmdom' s = X}) " text ‹Show the goal by mutual inclusion. The inclusion @{term "?B ⊆ ?A"} is trivial and can be solved by automation. For the complimentary proof @{term "?A ⊆ ?B"} however we need to do more work. In our case we choose a proof by contradiction and show that an @{term "s ∈ ?A"} which is not also in '?B' cannot exist.› { have "?A ⊆ ?B" proof(rule ccontr) assume C: "¬(?A ⊆ ?B)" moreover have "∃s∈?A. s∉?B" using C by auto moreover obtain s where obtain_s: "s∈?A ∧ s∉?B" using calculation by auto moreover have "s∉?B" using obtain_s by auto moreover have "fmdom' s = X ∪ {v}" using obtain_s by auto moreover have "∀s'∈?B. fmdom' s' = X ∪ {v}" by auto moreover have "(s ∉ ((λs. fmupd v True s) ` {s. fmdom' s = X}))" "(s ∉ ((λs. fmupd v False s) ` {s. fmdom' s = X}))" using obtain_s by blast+ text ‹ Show that every state @{term "s ∈ ?A"} has been constructed from another state with domain 'X'. › moreover { fix s :: "'a state" assume 1: "s ∈ {s :: 'a state. fmdom' s = insert v X}" then have "fmrestrict_set X s ∈ {s :: 'a state. fmdom' s = X}" using subset_insertI fmsubset_restrict_set by metis moreover { assume "fmlookup s v = Some True" then have "s = fmupd v True (fmrestrict_set X s)" using 1 fmupd_fmsubset_restrict_set by metis } moreover { assume "fmlookup s v = Some False" then have "s = fmupd v False (fmrestrict_set X s)" using 1 fmupd_fmsubset_restrict_set by fastforce } moreover have "fmlookup s v ≠ None" using 1 fmdom'_notI by fastforce ultimately have " (s ∈ ((λs. fmupd v True s) ` {s. fmdom' s = X})) ∨ (s ∈ ((λs. fmupd v False s) ` {s. fmdom' s = X})) " by force } ultimately show False by meson qed } moreover have "?B ⊆ ?A" by force ultimately show "?A = ?B" by blast qed text ‹ Another important property of the state set is cardinality, i.e. the number of distinct states which can be modelled using a given finite variable set. As lemma `card\_of\_set\_of\_all\_possible\_states` shows, for a finite variable set `X`, the number of possible states is `2 \^ card X`, i.e. the number of assigning two discrete values to `card X` slots as known from combinatorics. Again, some additional properties of finite maps had to be proven. Pivotally, in lemma `updates\_disjoint`, it is shown that the image of updating a set of states with domain `X` on a point @{term "x ∉ X"} with either `True` or `False` yields two distinct sets of states with domain @{term "{x} ∪ X"}. › ― ‹NOTE goal has to stay implication otherwise induction rule won't watch.› lemma FINITE_states: fixes X :: "'a set" shows "finite X ⟹ finite {(s :: 'a state). fmdom' s = X}" proof (induction rule: finite.induct) case emptyI then have "{s. fmdom' s = {}} = {fmempty}" by (simp add: empty_domain_fmap_set) then show ?case by (simp add: ‹{s. fmdom' s = {}} = {fmempty}›) next case (insertI A a) assume P1: "finite A" and P2: "finite {s. fmdom' s = A}" then show ?case proof (cases "a ∈ A") case True then show ?thesis using insertI.IH insert_Diff by fastforce next case False then show ?thesis proof - have "finite ( ((λs. fmupd a True s) ` {s. fmdom' s = A}) ∪ ((λs. fmupd a False s) ` {s. fmdom' s = A}))" using False construction_of_all_possible_states_lemma insertI.IH by blast then show ?thesis using False construction_of_all_possible_states_lemma by fastforce qed qed qed ― ‹NOTE added lemma.› lemma bool_update_effect: fixes s X x v b assumes "finite X" "s ∈ {s :: 'a state. fmdom' s = X}" "x ∈ X" "x ≠ v" shows "fmlookup ((λs :: 'a state. fmupd v b s) s) x = fmlookup s x" using assms fmupd_lookup by auto ― ‹NOTE added lemma.› lemma bool_update_inj: fixes X :: "'a set" and v b assumes "finite X" "v ∉ X" shows "inj_on (λs. fmupd v b s) {s :: 'a state. fmdom' s = X}" proof - let ?f = "λs :: 'a state. fmupd v b s" { fix s1 s2 :: "'a state" assume "s1 ∈ {s :: 'a state. fmdom' s = X}" "s2 ∈ {s :: 'a state. fmdom' s = X}" "?f s1 = ?f s2" moreover { have "∀x∈X. x ≠ v ⟶ fmlookup (?f s1) x = fmlookup s1 x" "∀x∈X. x ≠ v ⟶ fmlookup (?f s2) x = fmlookup s2 x" by simp+ then have "∀x∈X. x ≠ v ⟶ fmlookup s1 x = fmlookup s2 x" using calculation(3) by auto } moreover have "fmlookup s1 v = fmlookup s2 v" using calculation ‹v ∉ X› by force ultimately have "s1 = s2" using fmap_neq by fastforce } then show "inj_on (λs. fmupd v b s) {s :: 'a state. fmdom' s = X}" using inj_onI by blast qed ― ‹NOTE added lemma.› lemma card_update: fixes X v b assumes "finite (X :: 'a set)" "v ∉ X" shows " card ((λs. fmupd v b s) ` {s :: 'a state. fmdom' s = X}) = card {s :: 'a state. fmdom' s = X} " proof - have "inj_on (λs. fmupd v b s) {s :: 'a state. fmdom' s = X}" using assms bool_update_inj by fast then show "card ((λs. fmupd v b s) ` {s :: 'a state. fmdom' s = X}) = card {s :: 'a state. fmdom' s = X}" using card_image by blast qed ― ‹NOTE added lemma.› lemma updates_disjoint: fixes X x assumes "finite X" "x ∉ X" shows " ((λs. fmupd x True s) ` {s. fmdom' s = X}) ∩ ((λs. fmupd x False s) ` {s. fmdom' s = X}) = {} " proof - let ?A = "((λs. fmupd x True s) ` {s. fmdom' s = X})" let ?B = "((λs. fmupd x False s) ` {s. fmdom' s = X})" { assume C: "¬(∀a∈?A. ∀b∈?B. a ≠ b)" then have "∀a∈?A. ∀b∈?B. fmlookup a x ≠ fmlookup b x" by simp then have "∀a∈?A. ∀b∈?B. a ≠ b" by blast then have False using C by blast } then show "?A ∩ ?B = {}" using disjoint_iff_not_equal by blast qed lemma card_of_set_of_all_possible_states: fixes X :: "'a set" assumes "finite X" shows "card {(s :: 'a state). fmdom' s = X} = 2 ^ (card X)" using assms proof (induction X) case empty then have 1: "{s :: 'a state. fmdom' s = {}} = {fmempty}" using empty_domain_fmap_set by simp then have "card {fmempty} = 1" using is_singleton_altdef by blast then have "2^(card {}) = 1" by auto then show ?case using 1 by auto next case (insert x F) then show ?case ― ‹TODO refactor and simplify proof further.› proof (cases "x ∈ F") case True then show ?thesis using insert.hyps(2) by blast next case False then have " {s :: 'a state. fmdom' s = insert x F} = (λs. fmupd x True s) ` {s. fmdom' s = F} ∪ (λs. fmupd x False s) ` {s. fmdom' s = F} " using False construction_of_all_possible_states_lemma by metis then have 2: " card ({s :: 'a state. fmdom' s = insert x F}) = card ((λs. fmupd x True s) ` {s. fmdom' s = F} ∪ (λs. fmupd x False s) ` {s. fmdom' s = F}) " by argo then have 3: "2^(card (insert x F)) = 2 * 2^(card F)" using False insert.hyps(1) by simp then have "card ((λs. fmupd x True s) ` {s. fmdom' s = F}) = 2^(card F)" "card ((λs. fmupd x False s) ` {s. fmdom' s = F}) = 2^(card F)" using False card_update insert.IH insert.hyps(1) by metis+ moreover have " ((λs. fmupd x True s) ` {s. fmdom' s = F}) ∩ ((λs. fmupd x False s) ` {s. fmdom' s = F}) = {} " using False insert.hyps(1) updates_disjoint by metis moreover have "card ( ((λs. fmupd x True s) ` {s. fmdom' s = F}) ∪ ((λs. fmupd x False s) ` {s. fmdom' s = F}) ) = card (((λs. fmupd x True s) ` {s. fmdom' s = F})) + card ((λs. fmupd x False s) ` {s. fmdom' s = F}) " using calculation card_Un_disjoint card.infinite power_eq_0_iff rel_simps(76) by metis then have "card ( ((λs. fmupd x True s) ` {s. fmdom' s = F}) ∪ ((λs. fmupd x False s) ` {s. fmdom' s = F}) ) = 2 * (2^(card F))" using calculation(1, 2) by presburger then have "card ( ((λs. fmupd x True s) ` {s. fmdom' s = F}) ∪ ((λs. fmupd x False s) ` {s. fmdom' s = F}) ) = 2^(card (insert x F))" using insert.IH 3 by metis then show ?thesis using "2" by argo qed qed subsubsection "State Lists and State Sets" ― ‹NOTE using fun because of two defining equations.› ― ‹NOTE paired argument replaced by currying.› fun state_list where "state_list s [] = [s]" | "state_list s (a # as) = s # state_list (state_succ s a) as" lemma empty_state_list_lemma: fixes as s shows "¬([] = state_list s as)" proof (induction as) qed auto lemma state_list_length_non_zero: fixes as s shows "¬(0 = length (state_list s as))" proof (induction as) qed auto lemma state_list_length_lemma: fixes as s shows "length as = length (state_list s as) - 1" proof (induction as arbitrary: s) next case (Cons a as) have "length (state_list s (Cons a as)) - 1 = length (state_list (state_succ s a) as)" by auto ― ‹TODO unwrap metis proof.› then show "length (Cons a as) = length (state_list s (Cons a as)) - 1" by (metis Cons.IH Suc_diff_1 empty_state_list_lemma length_Cons length_greater_0_conv) qed simp lemma state_list_length_lemma_2: fixes as s shows "(length (state_list s as)) = (length as + 1)" proof (induction as arbitrary: s) qed auto ― ‹NOTE using fun because of multiple defining equations.› ― ‹NOTE name shortened to 'state\_def'› fun state_set where "state_set [] = {}" | "state_set (s # ss) = insert [s] (Cons s ` (state_set ss))" lemma state_set_thm: fixes s1 shows "s1 ∈ state_set s2 ⟷ prefix s1 s2 ∧ s1 ≠ []" proof - ― ‹NOTE Show equivalence by proving both directions. Left-to-right is trivial. Right-to-Left primarily involves exploiting the prefix premise, induction hypothesis and `state\_set` definition.› have "s1 ∈ state_set s2 ⟹ prefix s1 s2 ∧ s1 ≠ []" by (induction s2 arbitrary: s1) auto moreover { assume P: "prefix s1 s2" "s1 ≠ []" then have "s1 ∈ state_set s2" proof (induction s2 arbitrary: s1) case (Cons a s2) obtain s1' where 1: "s1 = a # s1'" "prefix s1' s2" using Cons.prems(1, 2) prefix_Cons by metis then show ?case proof (cases "s1' = []") case True then show ?thesis using 1 by force next case False then have "s1' ∈ state_set s2" using 1 False Cons.IH by blast then show ?thesis using 1 by fastforce qed qed simp } ultimately show "s1 ∈ state_set s2 ⟷ prefix s1 s2 ∧ s1 ≠ []" by blast qed lemma state_set_finite: fixes X shows "finite (state_set X)" by (induction X) auto lemma LENGTH_state_set: fixes X e assumes "e ∈ state_set X" shows "length e ≤ length X" using assms by (induction X arbitrary: e) auto lemma lemma_temp: fixes x s as h assumes "x ∈ state_set (state_list s as)" shows "length (h # state_list s as) > length x" using assms LENGTH_state_set le_imp_less_Suc by force lemma NIL_NOTIN_stateset: fixes X shows "[] ∉ state_set X" by (induction X) auto ― ‹NOTE added lemma.› lemma state_set_card_i: fixes X a shows "[a] ∉ (Cons a ` state_set X)" by (induction X) auto ― ‹NOTE added lemma.› lemma state_set_card_ii: fixes X a shows "card (Cons a ` state_set X) = card (state_set X)" proof - have "inj_on (Cons a) (state_set X)" by simp then show ?thesis using card_image by blast qed ― ‹NOTE added lemma.› lemma state_set_card_iii: fixes X a shows "card (state_set (a # X)) = 1 + card (state_set X)" proof - have "card (state_set (a # X)) = card (insert [a] (Cons a ` state_set X))" by auto ― ‹TODO unwrap this metis step.› also have "… = 1 + card (Cons a ` state_set X)" using state_set_card_i by (metis Suc_eq_plus1_left card_insert_disjoint finite_imageI state_set_finite) also have"… = 1 + card (state_set X)" using state_set_card_ii by metis finally show "card (state_set (a # X)) = 1 + card (state_set X)" by blast qed lemma state_set_card: fixes X shows "card (state_set X) = length X" proof (induction X) case (Cons a X) then have "card (state_set (a # X)) = 1 + card (state_set X)" using state_set_card_iii by fast then show ?case using Cons by fastforce qed auto subsubsection "Properties of Domain Changes During Plan Execution" lemma FDOM_state_succ: assumes "fmdom' (snd a) ⊆ fmdom' s" shows "(fmdom' (state_succ s a) = fmdom' s)" unfolding state_succ_def fmap_add_ltr_def using assms by force lemma FDOM_state_succ_subset: "fmdom' (state_succ s a) ⊆ (fmdom' s ∪ fmdom' (snd a))" unfolding state_succ_def fmap_add_ltr_def by simp ― ‹NOTE definition `qispl\_then` removed (was not being used).› lemma FDOM_eff_subset_FDOM_valid_states: fixes p e s assumes "(p, e) ∈ PROB" "(s ∈ valid_states PROB)" shows "(fmdom' e ⊆ fmdom' s)" proof - { have "fmdom' e ⊆ action_dom p e" unfolding action_dom_def by blast also have "… ⊆ prob_dom PROB" unfolding action_dom_def prob_dom_def using assms(1) by blast finally have "fmdom' e ⊆ fmdom' s" using assms by (auto simp: valid_states_def) } then show "fmdom' e ⊆ fmdom' s" by simp qed lemma FDOM_eff_subset_FDOM_valid_states_pair: fixes a s assumes "a ∈ PROB" "s ∈ valid_states PROB" shows "fmdom' (snd a) ⊆ fmdom' s" proof - { have "fmdom' (snd a) ⊆ (λ(s1, s2). action_dom s1 s2) a" unfolding action_dom_def using case_prod_beta by fastforce also have "… ⊆ prob_dom PROB" using assms(1) prob_dom_def Sup_upper by fast finally have "fmdom' (snd a) ⊆ fmdom' s" using assms(2) valid_states_def by fast } then show ?thesis by simp qed lemma FDOM_pre_subset_FDOM_valid_states: fixes p e s assumes "(p, e) ∈ PROB" "s ∈ valid_states PROB" shows "fmdom' p ⊆ fmdom' s" proof - { have "fmdom' p ⊆ (λ(s1, s2). action_dom s1 s2) (p, e)" using action_dom_def by fast also have "… ⊆ prob_dom PROB" using assms(1) by (simp add: Sup_upper pair_imageI prob_dom_def) finally have "fmdom' p ⊆ fmdom' s" using assms(2) valid_states_def by fast } then show ?thesis by simp qed lemma FDOM_pre_subset_FDOM_valid_states_pair: fixes a s assumes "a ∈ PROB" "s ∈ valid_states PROB" shows "fmdom' (fst a) ⊆ fmdom' s" proof - { have "fmdom' (fst a) ⊆ (λ(s1, s2). action_dom s1 s2) a" using action_dom_def by force also have "… ⊆ prob_dom PROB" using assms(1) by (simp add: Sup_upper pair_imageI prob_dom_def) finally have "fmdom' (fst a) ⊆ fmdom' s" using assms(2) valid_states_def by fast } then show ?thesis by simp qed ― ‹TODO unwrap the simp proof.› lemma action_dom_subset_valid_states_FDOM: fixes p e s assumes "(p, e) ∈ PROB" "s ∈ valid_states PROB" shows "action_dom p e ⊆ fmdom' s" using assms by (simp add: Sup_upper pair_imageI prob_dom_def valid_states_def) ― ‹TODO unwrap the metis proof.› lemma FDOM_eff_subset_prob_dom: fixes p e assumes "(p, e) ∈ PROB" shows "fmdom' e ⊆ prob_dom PROB" using assms by (metis Sup_upper Un_subset_iff action_dom_def pair_imageI prob_dom_def) lemma FDOM_eff_subset_prob_dom_pair: fixes a assumes "a ∈ PROB" shows "fmdom' (snd a) ⊆ prob_dom PROB" using assms(1) FDOM_eff_subset_prob_dom surjective_pairing by metis ― ‹TODO unwrap metis proof.› lemma FDOM_pre_subset_prob_dom: fixes p e assumes "(p, e) ∈ PROB" shows "fmdom' p ⊆ prob_dom PROB" using assms by (metis (no_types) Sup_upper Un_subset_iff action_dom_def pair_imageI prob_dom_def) lemma FDOM_pre_subset_prob_dom_pair: fixes a assumes "a ∈ PROB" shows "fmdom' (fst a) ⊆ prob_dom PROB" using assms FDOM_pre_subset_prob_dom surjective_pairing by metis subsubsection "Properties of Valid Plans" lemma valid_plan_valid_head: assumes "(h # as ∈ valid_plans PROB)" shows "h ∈ PROB" using assms valid_plans_def by force lemma valid_plan_valid_tail: assumes "(h # as ∈ valid_plans PROB)" shows "(as ∈ valid_plans PROB)" using assms by (simp add: valid_plans_def) ― ‹TODO unwrap simp proof.› lemma valid_plan_pre_subset_prob_dom_pair: assumes "as ∈ valid_plans PROB" shows "(∀a. ListMem a as ⟶ fmdom' (fst a) ⊆ (prob_dom PROB))" unfolding valid_plans_def using assms by (simp add: FDOM_pre_subset_prob_dom_pair ListMem_iff rev_subsetD valid_plans_def) lemma valid_append_valid_suff: assumes "as1 @ as2 ∈ (valid_plans PROB)" shows "as2 ∈ (valid_plans PROB)" using assms by (simp add: valid_plans_def) lemma valid_append_valid_pref: assumes "as1 @ as2 ∈ (valid_plans PROB)" shows "as1 ∈ (valid_plans PROB)" using assms by (simp add: valid_plans_def) lemma valid_pref_suff_valid_append: assumes "as1 ∈ (valid_plans PROB)" "as2 ∈ (valid_plans PROB)" shows "(as1 @ as2) ∈ (valid_plans PROB)" using assms by (simp add: valid_plans_def) ― ‹NOTE showcase (case split seems necessary for MP of IH but the original proof does not need it).› lemma MEM_statelist_FDOM: fixes PROB h as s0 assumes "s0 ∈ (valid_states PROB)" "as ∈ (valid_plans PROB)" "ListMem h (state_list s0 as)" shows "(fmdom' h = fmdom' s0)" using assms proof (induction as arbitrary: PROB h s0) case Nil have "h = s0" using Nil.prems(3) ListMem_iff by force then show ?case by simp next case (Cons a as) then show ?case ― ‹NOTE This case split seems necessary to be able to infer 'ListMem h (state\_list (state\_succ s0 a) as)' which is required in order to apply MP to the induction hypothesis.› proof (cases "h = s0") case False ― ‹TODO proof steps could be refactored into auxillary lemmas.› { have "a ∈ PROB" using Cons.prems(2) valid_plan_valid_head by fast then have "fmdom' (snd a) ⊆ fmdom' s0" using Cons.prems(1) FDOM_eff_subset_FDOM_valid_states_pair by blast then have "fmdom' (state_succ s0 a) = fmdom' s0" using FDOM_state_succ[of _ s0] Cons.prems(1) valid_states_def by presburger } note 1 = this { have "fmdom' s0 = prob_dom PROB" using Cons.prems(1) valid_states_def by fast then have "state_succ s0 a ∈ valid_states PROB" unfolding valid_states_def using 1 by force } note 2 = this { have "ListMem h (state_list (state_succ s0 a) as)" using Cons.prems(3) False by (simp add: ListMem_iff) } note 3 = this { have "as ∈ valid_plans PROB" using Cons.prems(2) valid_plan_valid_tail by fast then have "fmdom' h = fmdom' (state_succ s0 a)" using 1 2 3 Cons.IH[of "state_succ s0 a"] by blast } then show ?thesis using 1 by argo qed simp qed ― ‹TODO unwrap metis proof.› lemma MEM_statelist_valid_state: fixes PROB h as s0 assumes "s0 ∈ valid_states PROB" "as ∈ valid_plans PROB" "ListMem h (state_list s0 as)" shows "(h ∈ valid_states PROB)" using assms by (metis MEM_statelist_FDOM mem_Collect_eq valid_states_def) ― ‹TODO refactor (characterization lemma for 'state\_succ').› ― ‹TODO unwrap metis proof.› ― ‹NOTE added lemma.› lemma lemma_1_i: fixes s a PROB assumes "s ∈ valid_states PROB" "a ∈ PROB" shows "state_succ s a ∈ valid_states PROB" using assms by (metis FDOM_eff_subset_FDOM_valid_states_pair FDOM_state_succ mem_Collect_eq valid_states_def) ― ‹TODO unwrap smt proof.› ― ‹NOTE added lemma.› lemma lemma_1_ii: "last ` ((#) s ` state_set (state_list (state_succ s a) as)) = last ` state_set (state_list (state_succ s a) as)" by (smt NIL_NOTIN_stateset image_cong image_image last_ConsR) lemma lemma_1: fixes as :: "(('a, 'b) fmap × ('a, 'b) fmap) list" and PPROB assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" shows "((last ` (state_set (state_list s as))) ⊆ valid_states PROB)" using assms proof (induction as arbitrary: s PROB) ― ‹NOTE Base case simplifies to @{term "{s} ⊆ valid_states PROB"} which itself follows directly from 1st assumption.› case (Cons a as) text ‹ Split the 'insert' term produced by @{term "state_set (state_list s (a # as))"} and proof inclusion in 'valid\_states PROB' for both parts. › { ― ‹NOTE Inclusion of the first subset follows from the induction premise by simplification. The inclusion of the second subset is shown by applying the induction hypothesis to `state\_succ s a` and some elementary set simplifications.› have "last [s] ∈ valid_states PROB" using Cons.prems(1) by simp moreover { { have "a ∈ PROB" using Cons.prems(2) valid_plan_valid_head by fast then have "state_succ s a ∈ valid_states PROB" using Cons.prems(1) lemma_1_i by blast } moreover have "as ∈ valid_plans PROB" using Cons.prems(2) valid_plan_valid_tail by fast then have "(last ` state_set (state_list (state_succ s a) as)) ⊆ valid_states PROB" using calculation Cons.IH[of "state_succ s a"] by presburger then have "(last ` ((#) s ` state_set (state_list (state_succ s a) as))) ⊆ valid_states PROB" using lemma_1_ii by metis } ultimately have "(last ` insert [s] ((#) s ` state_set (state_list (state_succ s a) as))) ⊆ valid_states PROB" by simp } then show ?case by fastforce qed auto ― ‹TODO unwrap metis proof.› lemma len_in_state_set_le_max_len: fixes as x PROB assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "¬(as = [])" "(x ∈ state_set (state_list s as))" shows "(length x ≤ (Suc (length as)))" using assms by (metis LENGTH_state_set Suc_eq_plus1_left add.commute state_list_length_lemma_2) lemma card_state_set_cons: fixes as s h shows " (card (state_set (state_list s (h # as))) = Suc (card (state_set (state_list (state_succ s h) as)))) " by (metis length_Cons state_list.simps(2) state_set_card) lemma card_state_set: fixes as s shows "(Suc (length as)) = card (state_set (state_list s as))" by (simp add: state_list_length_lemma_2 state_set_card) lemma neq_mems_state_set_neq_len: fixes as x y s assumes "x ∈ state_set (state_list s as)" "(y ∈ state_set (state_list s as))" "¬(x = y)" shows "¬(length x = length y)" proof - have "x ≠ []" "prefix x (state_list s as)" using assms(1) state_set_thm by blast+ moreover have "y ≠ []" "prefix y (state_list s as)" using assms(2) state_set_thm by blast+ ultimately show ?thesis using assms(3) append_eq_append_conv prefixE by metis qed ― ‹NOTE added definition (imported from pred\_setScript.sml:1562).› definition inj :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ bool" where "inj f A B ≡ (∀x ∈ A. f x ∈ B) ∧ inj_on f A" ― ‹NOTE added lemma; refactored from `not\_eq\_last\_diff\_paths`.› lemma not_eq_last_diff_paths_i: fixes s as PROB assumes "s ∈ valid_states PROB" "as ∈ valid_plans PROB" "x ∈ state_set (state_list s as)" shows "last x ∈ valid_states PROB" proof - have "last x ∈ last ` (state_set (state_list s as))" using assms(3) by simp then show ?thesis using assms(1, 2) lemma_1 by blast qed lemma not_eq_last_diff_paths_ii: assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "¬(inj (last) (state_set (state_list s as)) (valid_states PROB))" shows "∃l1. ∃l2. l1 ∈ state_set (state_list s as) ∧ l2 ∈ state_set (state_list s as) ∧ last l1 = last l2 ∧ l1 ≠ l2 " proof - let ?S="state_set (state_list s as)" have 1: "¬(∀x∈?S. last x ∈ valid_states PROB) = False" using assms(1, 2) not_eq_last_diff_paths_i by blast { have "(¬(inj (last) ?S (valid_states PROB))) = (¬((∀x∈?S. ∀y∈?S. last x = last y ⟶ x = y)))" unfolding inj_def inj_on_def using 1 by blast then have " (¬(inj (last) ?S (valid_states PROB))) = (∃x. ∃y. x∈?S ∧ y∈?S ∧ last x = last y ∧ x ≠ y) " using assms(3) by blast } then show ?thesis using assms(3) by blast qed lemma not_eq_last_diff_paths: fixes as PROB s assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "¬(inj (last) (state_set (state_list s as)) (valid_states PROB))" shows "(∃slist_1 slist_2. (slist_1 ∈ state_set (state_list s as)) ∧ (slist_2 ∈ state_set (state_list s as)) ∧ ((last slist_1) = (last slist_2)) ∧ ¬(length slist_1 = length slist_2)) " proof - obtain l1 l2 where " l1 ∈ state_set (state_list s as) ∧ l2 ∈ state_set (state_list s as) ∧ last l1 = last l2 ∧ l1 ≠ l2 " using assms(1, 2, 3) not_eq_last_diff_paths_ii by blast then show ?thesis using neq_mems_state_set_neq_len by blast qed ― ‹NOTE this lemma was removed due to being redundant and being shadowed later on: lemma empty\_list\_nin\_state\_set› lemma nempty_sl_in_state_set: fixes sl assumes "sl ≠ []" shows "sl ∈ state_set sl" using assms state_set_thm by auto lemma empty_list_nin_state_set: fixes h slist as assumes "(h # slist) ∈ state_set (state_list s as)" shows "(h = s)" using assms by (induction as) auto lemma cons_in_state_set_2: fixes s slist h t assumes "(slist ≠ [])" "((s # slist) ∈ state_set (state_list s (h # t)))" shows "(slist ∈ state_set (state_list (state_succ s h) t))" using assms by (induction slist) auto ― ‹TODO move up and replace 'FactoredSystem.lemma\_1\_i'?› lemma valid_action_valid_succ: assumes "h ∈ PROB" "s ∈ valid_states PROB" shows "(state_succ s h) ∈ valid_states PROB" using assms lemma_1_i by blast lemma in_state_set_imp_eq_exec_prefix: fixes slist as PROB s assumes "(as ≠ [])" "(slist ≠ [])" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "(slist ∈ state_set (state_list s as))" shows "(∃as'. (prefix as' as) ∧ (exec_plan s as' = last slist) ∧ (length slist = Suc (length as')))" using assms proof (induction slist arbitrary: as s PROB) case cons_1: (Cons a slist) have 1: "s # slist ∈ state_set (state_list s as)" using cons_1.prems(5) empty_list_nin_state_set by auto then show ?case using cons_1 proof (cases as) case cons_2: (Cons a' R⇩_{a}⇩_{s}) then have a: "state_succ s a' ∈ valid_states PROB" using cons_1.prems(3, 4) valid_action_valid_succ valid_plan_valid_head by metis then have b: "R⇩_{a}⇩_{s}∈ valid_plans PROB" using cons_1.prems(4) cons_2 valid_plan_valid_tail by fast then show ?thesis proof (cases slist) case Nil then show ?thesis using cons_1.prems(5) empty_list_nin_state_set by auto next case cons_3: (Cons a'' R⇩_{s}⇩_{l}⇩_{i}⇩_{s}⇩_{t}) then have i: "a'' # R⇩_{s}⇩_{l}⇩_{i}⇩_{s}⇩_{t}∈ state_set (state_list (state_succ s a') R⇩_{a}⇩_{s})" using 1 cons_2 cons_in_state_set_2 by blast then show ?thesis proof (cases R⇩_{a}⇩_{s}) case Nil then show ?thesis using i cons_2 cons_3 by auto next case (Cons a''' R⇩_{a}⇩_{s}') then obtain as' where "prefix as' (a''' # R⇩_{a}⇩_{s}')" "exec_plan (state_succ s a') as' = last slist" "length slist = Suc (length as')" using cons_1.IH[of "a''' # R⇩_{a}⇩_{s}'" "state_succ s a'" PROB] using i a b cons_3 by blast then show ?thesis using Cons_prefix_Cons cons_2 cons_3 exec_plan.simps(2) last.simps length_Cons list.distinct(1) local.Cons by metis qed qed qed auto qed auto lemma eq_last_state_imp_append_nempty_as: fixes as PROB slist_1 slist_2 assumes "(as ≠ [])" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "(slist_1 ≠ [])" "(slist_2 ≠ [])" "(slist_1 ∈ state_set (state_list s as))" "(slist_2 ∈ state_set (state_list s as))" "¬(length slist_1 = length slist_2)" "(last slist_1 = last slist_2)" shows "(∃as1 as2 as3. (as1 @ as2 @ as3 = as) ∧ (exec_plan s (as1 @ as2) = exec_plan s as1) ∧ ¬(as2 = []) )" proof - obtain as_1 where 1: "(prefix as_1 as)" "(exec_plan s as_1 = last slist_1)" "length slist_1 = Suc (length as_1)" using assms(1, 2, 3, 4, 6) in_state_set_imp_eq_exec_prefix by blast obtain as_2 where 2: "(prefix as_2 as)" "(exec_plan s as_2 = last slist_2)" "(length slist_2) = Suc (length as_2)" using assms(1, 2, 3, 5, 7) in_state_set_imp_eq_exec_prefix by blast then have "length as_1 ≠ length as_2" using assms(8) 1(3) 2(3) by fastforce then consider (i) "length as_1 < length as_2" | (ii) "length as_1 > length as_2" by force then show ?thesis proof (cases) case i then have "prefix as_1 as_2" using 1(1) 2(1) len_gt_pref_is_pref by blast then obtain a where a1: "as_2 = as_1 @ a" using prefixE by blast then obtain b where b1: "as = as_2 @ b" using prefixE 2(1) by blast let ?as1="as_1" let ?as2="a" let ?as3="b" have "as = ?as1 @ ?as2 @ ?as3" using a1 b1 by simp moreover have "exec_plan s (?as1 @ ?as2) = exec_plan s ?as1" using 1(2) 2(2) a1 assms(9) by auto moreover have "?as2 ≠ []" using i a1 by simp ultimately show ?thesis by blast next case ii then have "prefix as_2 as_1" using 1(1) 2(1) len_gt_pref_is_pref by blast then obtain a where a2: "as_1 = as_2 @ a" using prefixE by blast then obtain b where b2: "as = as_1 @ b" using prefixE 1(1) by blast let ?as1="as_2" let ?as2="a" let ?as3="b" have "as = ?as1 @ ?as2 @ ?as3" using a2 b2 by simp moreover have "exec_plan s (?as1 @ ?as2) = exec_plan s ?as1" using 1(2) 2(2) a2 assms(9) by auto moreover have "?as2 ≠ []" using ii a2 by simp ultimately show ?thesis by blast qed qed lemma FINITE_prob_dom: assumes "finite PROB" shows "finite (prob_dom PROB)" proof - { fix x assume P2: "x ∈ PROB" then have 1: "(λ(s1, s2). action_dom s1 s2) x = fmdom' (fst x) ∪ fmdom' (snd x)" by (simp add: action_dom_def case_prod_beta') then have 2: "finite (fset (fmdom (fst x)))" "finite (fset (fmdom (snd x)))" by auto then have 3: "fset (fmdom (fst x)) = fmdom' (fst x)" "fset (fmdom (snd x)) = fmdom' (snd x)" by (auto simp add: fmdom'_alt_def) then have "finite (fmdom' (fst x))" using 2 by auto then have "finite (fmdom' (snd x))" using 2 3 by auto then have "finite ((λ(s1, s2). action_dom s1 s2) x)" using 1 2 3 by simp } then show "finite (prob_dom PROB)" unfolding prob_dom_def using assms by blast qed lemma CARD_valid_states: assumes "finite (PROB :: 'a problem)" shows "(card (valid_states PROB :: 'a state set) = 2 ^ card (prob_dom PROB))" proof - have 1: "finite (prob_dom PROB)" using assms FINITE_prob_dom by blast have"(card (valid_states PROB :: 'a state set)) = card {s :: 'a state. fmdom' s = prob_dom PROB}" unfolding valid_states_def by simp also have "... = 2 ^ (card (prob_dom PROB))" using 1 card_of_set_of_all_possible_states by blast finally show ?thesis by blast qed ― ‹NOTE type of 'valid\_states PROB' has to be asserted to match 'FINITE\_states' in the proof.› lemma FINITE_valid_states: fixes PROB :: "'a problem" shows "finite PROB ⟹ finite ((valid_states PROB) :: 'a state set)" proof (induction PROB rule: finite.induct) case emptyI then have "valid_states {} = {fmempty}" unfolding valid_states_def prob_dom_def using empty_domain_fmap_set by force then show ?case by(subst ‹valid_states {} = {fmempty}›) auto next case (insertI A a) { then have "finite (insert a A)" by blast then have "finite (prob_dom (insert a A))" using FINITE_prob_dom by blast then have "finite {s :: 'a state. fmdom' s = prob_dom (insert a A)}" using FINITE_states by blast } then show ?case unfolding valid_states_def by simp qed ― ‹NOTE type of 'PROB' had to be fixed for use of 'FINITE\_valid\_states'.› lemma lemma_2: fixes PROB :: "'a problem" and as :: "('a action) list" and s :: "'a state" assumes "finite PROB" "s ∈ (valid_states PROB)" "(as ∈ valid_plans PROB)" "((length as) > (2 ^ (card (fmdom' s)) - 1))" shows "(∃as1 as2 as3. (as1 @ as2 @ as3 = as) ∧ (exec_plan s (as1 @ as2) = exec_plan s as1) ∧ ¬(as2 = []) )" proof - have "Suc (length as) > 2^(card (fmdom' s))" using assms(4) by linarith then have 1: "card (state_set (state_list s as)) > 2^card (fmdom' s)" using card_state_set[symmetric] by metis { ― ‹NOTE type of 'valid\_states PROB' had to be asserted to match 'FINITE\_valid\_states'.› have 2: "finite (prob_dom PROB)" "finite ((valid_states PROB) :: 'a state set)" using assms(1) FINITE_prob_dom FINITE_valid_states by blast+ have 3: "fmdom' s = prob_dom PROB" using assms(2) valid_states_def by fast then have "card ((valid_states PROB) :: 'a state set) = 2^card (fmdom' s)" using assms(1) CARD_valid_states by auto then have 4: "card (state_set (state_list (s :: 'a state) as)) > card ((valid_states PROB) :: 'a state set)" unfolding valid_states_def using 1 2(1) 3 card_of_set_of_all_possible_states[of "prob_dom PROB"] by argo ― ‹TODO refactor into lemma.› { let ?S="state_set (state_list (s :: 'a state) as)" let ?T="valid_states PROB :: 'a state set" assume C2: "inj_on last ?S" ― ‹TODO unwrap the metis step or refactor into lemma.› have a: "?T ⊆ last ` ?S" using C2 by (metis "2"(2) "4" assms(2) assms(3) card_image card_mono lemma_1 not_less) have "finite (state_set (state_list s as))" using state_set_finite by auto then have "card (last ` ?S) = card ?S" using C2 inj_on_iff_eq_card by blast also have "… > card ?T" using 4 by blast then have "∃x. x ∈ (last ` ?S) ∧ x ∉ ?T" using C2 a assms(2) assms(3) calculation lemma_1 by fastforce } note 5 = this moreover { assume C: "inj last (state_set (state_list (s :: 'a state) as)) (valid_states PROB)" then have "inj_on last (state_set (state_list (s :: 'a state) as))" using C inj_def by blast then obtain x where "x ∈ last ` (state_set (state_list s as)) ∧ x ∉ valid_states PROB" using 5 by presburger then have "¬(∀x∈state_set (state_list s as). last x ∈ valid_states PROB)" by blast then have "¬inj last (state_set (state_list (s :: 'a state) as)) (valid_states PROB)" using inj_def by metis then have False using C by simp } ultimately have "¬inj last (state_set (state_list (s :: 'a state) as)) (valid_states PROB)" unfolding inj_def by blast } then obtain slist_1 slist_2 where 6: "slist_1 ∈ state_set (state_list s as)" "slist_2 ∈ state_set (state_list s as)" "(last slist_1 = last slist_2)" "length slist_1 ≠ length slist_2" using assms(2, 3) not_eq_last_diff_paths by blast then show ?thesis proof (cases as) case Nil text ‹ 4th assumption is violated in the 'Nil' case. › then have "¬(2 ^ card (fmdom' s) - 1 < length as)" using Nil by simp then show ?thesis using assms(4) by blast next case (Cons a list) then have "as ≠ []" by simp moreover have "slist_1 ≠ []" "slist_2 ≠ []" using 6(1, 2) NIL_NOTIN_stateset by blast+ ultimately show ?thesis using assms(2, 3) 6(1, 2, 3, 4) eq_last_state_imp_append_nempty_as by fastforce qed qed lemma lemma_2_prob_dom: fixes PROB and as :: "('a action) list" and s :: "'a state" assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "(length as > (2 ^ (card (prob_dom PROB))) - 1)" shows "(∃as1 as2 as3. (as1 @ as2 @ as3 = as) ∧ (exec_plan s (as1 @ as2) = exec_plan s as1) ∧ ¬(as2 = []) )" proof - have "prob_dom PROB = fmdom' s" using assms(2) valid_states_def by fast then have "2 ^ card (fmdom' s) - 1 < length as" using assms(4) by argo then show ?thesis using assms(1, 2, 3) lemma_2 by blast qed ― ‹NOTE type for `s` had to be fixed (type mismatch in obtain statement).› ― ‹NOTE type for `as1`, `as2` and `as3` had to be fixed (due type mismatch on `as1` in `cycle\_removal\_lemma`)› lemma lemma_3: fixes PROB :: "'a problem" and s :: "'a state" assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "(length as > (2 ^ (card (prob_dom PROB)) - 1))" shows "(∃as'. (exec_plan s as = exec_plan s as') ∧ (length as' < length as) ∧ (subseq as' as) )" proof - have "prob_dom PROB = fmdom' s" using assms(2) valid_states_def by fast then have "2 ^ card (fmdom' s) - 1 < length as" using assms(4) by argo then obtain as1 as2 as3 :: "'a action list" where 1: "as1 @ as2 @ as3 = as" "exec_plan s (as1 @ as2) = exec_plan s as1" "as2 ≠ []" using assms(1, 2, 3) lemma_2 by metis have 2: "exec_plan s (as1 @ as3) = exec_plan s (as1 @ as2 @ as3)" using 1 cycle_removal_lemma by fastforce let ?as' = "as1 @ as3" have "exec_plan s as = exec_plan s ?as'" using 1 2 by auto moreover have "length ?as' < length as" using 1 nempty_list_append_length_add by blast moreover have "subseq ?as' as" using 1 subseq_append' by blast ultimately show "(∃as'. (exec_plan s as = exec_plan s as') ∧ (length as' < length as) ∧ (subseq as' as))" by blast qed ― ‹TODO unwrap meson step.› lemma sublist_valid_is_valid: fixes as' as PROB assumes "(as ∈ valid_plans PROB)" "(subseq as' as)" shows "as' ∈ valid_plans PROB" using assms by (simp add: valid_plans_def) (meson dual_order.trans fset_of_list_subset sublist_subset) ― ‹NOTE type of 's' had to be fixed (type mismatch in goal).› theorem main_lemma: fixes PROB :: "'a problem" and as s 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' ≤ (2 ^ (card (prob_dom PROB))) - 1) )" proof (cases "length as ≤ (2 ^ (card (prob_dom PROB))) - 1") case True then have "exec_plan s as = exec_plan s as" by simp then have "subseq as as" by auto then have "length as ≤ (2^(card (prob_dom PROB)) - 1)" using True by auto then show ?thesis by blast next case False then have "length as > (2 ^ (card (prob_dom PROB))) - 1" using False by auto then obtain as' where 1: "exec_plan s as = exec_plan s as'" "length as' < length as" "subseq as' as" using assms lemma_3 by blast { fix p assume "exec_plan s as = exec_plan s p" "subseq p as" "2 ^ card (prob_dom PROB) - 1 < length p" then have "(∃p'. (exec_plan s as = exec_plan s p' ∧ subseq p' as) ∧ length p' < length p)" using assms(1, 2, 3) lemma_3 sublist_valid_is_valid by fastforce } then have "∀p. exec_plan s as = exec_plan s p ∧ subseq p as ⟶ (∃p'. (exec_plan s as = exec_plan s p' ∧ subseq p' as) ∧ length p' ≤ 2 ^ card (prob_dom PROB) - 1)" using general_theorem[where P = "λ(as'' :: 'a action list). (exec_plan s as = exec_plan s as'') ∧ subseq as'' as" and l = "(2 ^ (card (prob_dom (PROB ::'a problem)))) - 1" and f = length] by blast then obtain p' where "exec_plan s as = exec_plan s p'" "subseq p' as" "length p' ≤ 2 ^ card (prob_dom PROB) - 1" by blast then show ?thesis using sublist_refl by blast qed subsection "Reachable States" ― ‹NOTE shortened to 'reachable\_s'› definition reachable_s where "reachable_s PROB s ≡ {exec_plan s as | as. as ∈ valid_plans PROB}" ― ‹NOTE types for `s` and `PROB` had to be fixed (type mismatch in goal).› lemma valid_as_valid_exec: fixes as and s :: "'a state" and PROB :: "'a problem" assumes "(as ∈ valid_plans PROB)" "(s ∈ valid_states PROB)" shows "(exec_plan s as ∈ valid_states PROB)" using assms proof (induction as arbitrary: s PROB) case (Cons a as) then have "a ∈ PROB" using valid_plan_valid_head by metis then have "state_succ s a ∈ valid_states PROB" using Cons.prems(2) valid_action_valid_succ by blast moreover have "as ∈ valid_plans PROB" using Cons.prems(1) valid_plan_valid_tail by fast ultimately show ?case using Cons.IH by force qed simp lemma exec_plan_fdom_subset: fixes as s PROB assumes "(as ∈ valid_plans PROB)" shows "(fmdom' (exec_plan s as) ⊆ (fmdom' s ∪ prob_dom PROB))" using assms proof (induction as arbitrary: s PROB) case (Cons a as) have "as ∈ valid_plans PROB" using Cons.prems valid_plan_valid_tail by fast then have "fmdom' (exec_plan (state_succ s a) as) ⊆ fmdom' (state_succ s a) ∪ prob_dom PROB" using Cons.IH[of _ "state_succ s a"] by simp ― ‹TODO unwrap metis proofs.› moreover have "fmdom' s ∪ fmdom' (snd a) ∪ prob_dom PROB = fmdom' s ∪ prob_dom PROB" by (metis Cons.prems FDOM_eff_subset_prob_dom_pair sup_absorb2 sup_assoc valid_plan_valid_head) ultimately show ?case by (metis (no_types, lifting) FDOM_state_succ_subset exec_plan.simps(2) order_refl subset_trans sup.mono) qed simp ― ‹NOTE added lemma.› lemma reachable_s_finite_thm_1_a: fixes s and PROB :: "'a problem" assumes "(s :: 'a state) ∈ valid_states PROB" shows "(∀l∈reachable_s PROB s. l∈valid_states PROB)" proof - have 1: "∀l∈reachable_s PROB s. ∃as. l = exec_plan s as ∧ as ∈ valid_plans PROB" using reachable_s_def by fastforce { fix l assume P1: "l ∈ reachable_s PROB s" ― ‹NOTE type for 's' and 'as' had to be fixed due to type mismatch in obtain statement.› then obtain as :: "'a action list" where a: "l = exec_plan s as ∧ as ∈ valid_plans PROB" using 1 by blast then have "exec_plan s as ∈ valid_states PROB" using assms a valid_as_valid_exec by blast then have "l ∈ valid_states PROB" using a by simp } then show "∀l ∈ reachable_s PROB s. l ∈ valid_states PROB" by blast qed lemma reachable_s_finite_thm_1: assumes "((s :: 'a state) ∈ valid_states PROB)" shows "(reachable_s PROB s ⊆ valid_states PROB)" using assms reachable_s_finite_thm_1_a by blast ― ‹NOTE second declaration skipped (this is declared twice in the source; see above)› ― ‹NOTE type for `s` had to be fixed (type mismatch in goal).› lemma reachable_s_finite_thm: fixes s :: "'a state" assumes "finite (PROB :: 'a problem)" "(s ∈ valid_states PROB)" shows "finite (reachable_s PROB s)" using assms by (meson FINITE_valid_states reachable_s_finite_thm_1 rev_finite_subset) lemma empty_plan_is_valid: "[] ∈ (valid_plans PROB)" by (simp add: valid_plans_def) lemma valid_head_and_tail_valid_plan: assumes "(h ∈ PROB)" "(as ∈ valid_plans PROB)" shows "((h # as) ∈ valid_plans PROB)" using assms by (auto simp: valid_plans_def) ― ‹TODO refactor› ― ‹NOTE added lemma› lemma lemma_1_reachability_s_i: fixes PROB s assumes "s ∈ valid_states PROB" shows "s ∈ reachable_s PROB s" proof - have "[] ∈ valid_plans PROB" using empty_plan_is_valid by blast then show ?thesis unfolding reachable_s_def by force qed ― ‹NOTE types for 'PROB' and 's' had to be fixed (type mismatch in goal).› lemma lemma_1_reachability_s: fixes PROB :: "'a problem" and s :: "'a state" and as assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" shows "((last ` state_set (state_list s as)) ⊆ (reachable_s PROB s))" using assms proof(induction as arbitrary: PROB s) case Nil then have "(last ` state_set (state_list s [])) = {s}" by force then show ?case unfolding reachable_s_def using empty_plan_is_valid by force next case cons: (Cons a as) let ?S="last ` state_set (state_list s (a # as))" { let ?as="[]" have "last [s] = exec_plan s ?as" by simp moreover have "?as ∈ valid_plans PROB" using empty_plan_is_valid by auto ultimately have "∃as. (last [s] = exec_plan s as) ∧ as ∈ valid_plans PROB" by blast } note 1 = this { fix x assume P: "x ∈ ?S" then consider (a) "x = last [s]" | (b) "x ∈ last ` ((#) s ` state_set (state_list (state_succ s a) as))" by auto then have "x ∈ reachable_s PROB s" proof (cases) case a then have "x = s" by simp then show ?thesis using cons.prems(1) P lemma_1_reachability_s_i by blast next case b then obtain x'' where i: "x'' ∈ state_set (state_list (state_succ s a) as)" "x = last (s # x'')" by blast then show ?thesis proof (cases "x''") case Nil then have "x = s" using i by fastforce then show ?thesis using cons.prems(1) lemma_1_reachability_s_i by blast next case (Cons a' list) then obtain x' where a: "last (a' # list) = last x'" "x' ∈ state_set (state_list (state_succ s a) as)" using i(1) by blast { have "state_succ s a ∈ valid_states PROB" using cons.prems(1, 2) valid_action_valid_succ valid_plan_valid_head by metis moreover have "as ∈ valid_plans PROB" using cons.prems(2) valid_plan_valid_tail by fast ultimately have "last ` state_set (state_list (state_succ s a) as) ⊆ reachable_s PROB (state_succ s a)" using cons.IH[of "state_succ s a"] by auto then have "∃as'. last (a' # list) = exec_plan (state_succ s a) as' ∧ (as' ∈ (valid_plans PROB))" unfolding state_set.simps state_list.simps reachable_s_def using i(1) Cons by blast } then obtain as' where b: "last (a' # list) = exec_plan (state_succ s a) as'" "(as' ∈ (valid_plans PROB))" by blast then have "x = exec_plan (state_succ s a) as'" using i(2) Cons a(1) by auto then show ?thesis unfolding reachable_s_def using cons.prems(2) b(2) by (metis (mono_tags, lifting) exec_plan.simps(2) mem_Collect_eq valid_head_and_tail_valid_plan valid_plan_valid_head) qed qed } then show ?case by blast qed ― ‹NOTE types for `PROB` and `s` had to be fixed for use of `lemma\_1\_reachability\_s`.› lemma not_eq_last_diff_paths_reachability_s: fixes PROB :: "'a problem" and s :: "'a state" and as assumes "s ∈ valid_states PROB" "as ∈ valid_plans PROB" "¬(inj last (state_set (state_list s as)) (reachable_s PROB s))" shows "(∃slist_1 slist_2. slist_1 ∈ state_set (state_list s as) ∧ slist_2 ∈ state_set (state_list s as) ∧ (last slist_1 = last slist_2) ∧ ¬(length slist_1 = length slist_2) )" proof - { fix x assume P1: "x ∈ state_set (state_list s as)" have a: "last ` state_set (state_list s as) ⊆ reachable_s PROB s" using assms(1, 2) lemma_1_reachability_s by fast then have "∀as PROB. s ∈ (valid_states PROB) ∧ as ∈ (valid_plans PROB) ⟶ (last ` (state_set (state_list s as)) ⊆ reachable_s PROB s)" using lemma_1_reachability_s by fast then have "last x ∈ valid_states PROB" using assms(1, 2) P1 lemma_1 by fast then have "last x ∈ reachable_s PROB s" using P1 a by fast } note 1 = this text ‹ Show the goal by disproving the contradiction. › { assume C: "(∀slist_1 slist_2. (slist_1 ∈ state_set (state_list s as) ∧ slist_2 ∈ state_set (state_list s as) ∧ (last slist_1 = last slist_2)) ⟶ (length slist_1 = length slist_2))" moreover { fix slist_1 slist_2 assume C1: "slist_1 ∈ state_set (state_list s as)" "slist_2 ∈ state_set (state_list s as)" "(last slist_1 = last slist_2)" moreover have i: "(length slist_1 = length slist_2)" using C1 C by blast moreover have "slist_1 = slist_2" using C1(1, 2) i neq_mems_state_set_neq_len by auto ultimately have "inj_on last (state_set (state_list s as))" unfolding inj_on_def using C neq_mems_state_set_neq_len by blast then have False using 1 inj_def assms(3) by blast } ultimately have False by (metis empty_state_list_lemma nempty_sl_in_state_set) } then show ?thesis by blast qed ― ‹NOTE added lemma ( translation of `PHP` in pred\_setScript.sml:3155).› lemma lemma_2_reachability_s_i: fixes f :: "'a ⇒ 'b" and s t assumes "finite t" "card t < card s" shows "¬(inj f s t)" proof - { assume C: "inj f s t" then have 1: "(∀x∈s. f x ∈ t)" "inj_on f s" unfolding inj_def by blast+ moreover { have "f ` s ⊆ t" using 1 by fast then have "card (f ` s) ≤ card t" using assms(1) card_mono by auto } moreover have "card (f ` s) = card s" using 1 card_image by fast ultimately have False using assms(2) by linarith } then show ?thesis by blast qed lemma lemma_2_reachability_s: fixes PROB :: "'a problem" and as s assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "(length as > card (reachable_s PROB s) - 1)" shows "(∃as1 as2 as3. (as1 @ as2 @ as3 = as) ∧ (exec_plan s (as1 @ as2) = exec_plan s as1) ∧ ¬(as2 = []))" proof - { have "Suc (length as) > card (reachable_s PROB s)" using assms(4) by fastforce then have "card (state_set (state_list s as)) > card (reachable_s PROB s)" using card_state_set by metis } note 1 = this { have "finite (reachable_s PROB s)" using assms(1, 2) reachable_s_finite_thm by blast then have "¬(inj last (state_set (state_list s as)) (reachable_s PROB s))" using assms(4) 1 lemma_2_reachability_s_i by blast } note 2 = this obtain slist_1 slist_2 where 3: "slist_1 ∈ state_set (state_list s as)" "slist_2 ∈ state_set (state_list s as)" "(last slist_1 = last slist_2)" "length slist_1 ≠ length slist_2" using assms(2, 3) 2 not_eq_last_diff_paths_reachability_s by blast then show ?thesis using assms proof(cases as) case (Cons a list) then show ?thesis using assms(2, 3) 3 eq_last_state_imp_append_nempty_as state_set_thm list.distinct(1) by metis qed force qed lemma lemma_3_reachability_s: fixes as and PROB :: "'a problem" and s assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "(length as > (card (reachable_s PROB s) - 1))" shows "(∃as'. (exec_plan s as = exec_plan s as') ∧ (length as' < length as) ∧ (subseq as' as) )" proof - obtain as1 as2 as3 :: "'a action list" where 1: "(as1 @ as2 @ as3 = as)" "(exec_plan s (as1 @ as2) = exec_plan s as1)" "~(as2=[])" using assms lemma_2_reachability_s by metis then have "(exec_plan s (as1 @ as2) = exec_plan s as1)" using 1 by blast then have 2: "exec_plan s (as1 @ as3) = exec_plan s (as1 @ as2 @ as3)" using 1 cycle_removal_lemma by fastforce let ?as' = "as1 @ as3" have 3: "exec_plan s as = exec_plan s ?as'" using 1 2 by argo then have "as2 ≠ []" using 1 by blast then have 4: "length ?as' < length as" using nempty_list_append_length_add 1 by blast then have "subseq ?as' as" using 1 subseq_append' by blast then show ?thesis using 3 4 by blast qed ― ‹NOTE type for `as` had to be fixed (type mismatch in goal).› lemma main_lemma_reachability_s: 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' ≤ (card (reachable_s PROB s) - 1)))" proof (cases "length as ≤ card (reachable_s PROB s) - 1") case False let ?as' = "as" have "length as > card (reachable_s PROB s) - 1" using False by simp { fix p assume P: "exec_plan s as = exec_plan s p" "subseq p as" "card (reachable_s PROB s) - 1 < length p" moreover have "p ∈ valid_plans PROB" using assms(3) P(2) sublist_valid_is_valid by blast ultimately obtain as' where 1: "exec_plan s p = exec_plan s as'" "length as' < length p" "subseq as' p" using assms lemma_3_reachability_s by blast then have "exec_plan s as = exec_plan s as'" using P by presburger moreover have "subseq as' as" using P 1 sublist_trans by blast ultimately have "(∃p'. (exec_plan s as = exec_plan s p' ∧ subseq p' as) ∧ length p' < length p)" using 1 by blast } then have "∀p. exec_plan s as = exec_plan s p ∧ subseq p as ⟶ (∃p'. (exec_plan s as = exec_plan s p' ∧ subseq p' as) ∧ length p' ≤ card (reachable_s PROB s) - 1)" using general_theorem[of "λas''. (exec_plan s as = exec_plan s as'') ∧ subseq as'' as" "(card (reachable_s (PROB :: 'a problem) (s :: 'a state)) - 1)" length] by blast then show ?thesis by blast qed blast lemma reachable_s_non_empty: "¬(reachable_s PROB s = {})" using empty_plan_is_valid reachable_s_def by blast lemma card_reachable_s_non_zero: fixes s assumes "finite (PROB :: 'a problem)" "(s ∈ valid_states PROB)" shows "(0 < card (reachable_s PROB s))" using assms by (simp add: card_gt_0_iff reachable_s_finite_thm reachable_s_non_empty) lemma exec_fdom_empty_prob: fixes s assumes "(prob_dom PROB = {})" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" shows "(exec_plan s as = fmempty)" proof - have "fmdom' s = {}" using assms(1, 2) by (simp add: valid_states_def) then show "exec_plan s as = fmempty" using assms(1, 3) by (metis exec_plan_fdom_subset fmrestrict_set_dom fmrestrict_set_null subset_empty sup_bot.left_neutral) qed ― ‹NOTE types for `PROB` and `s` had to be fixed (type mismatch in goal).› lemma reachable_s_empty_prob: fixes PROB :: "'a problem" and s :: "'a state" assumes "(prob_dom PROB = {})" "(s ∈ valid_states PROB)" shows "((reachable_s PROB s) ⊆ {fmempty})" proof - { fix x assume P1: "x ∈ reachable_s PROB s" then obtain as :: "'a action list" where a: "as ∈ valid_plans PROB" "x = exec_plan s as" using reachable_s_def by blast then have "as ∈ valid_plans PROB" "x = exec_plan s as" using a by auto then have "x = fmempty" using assms(1, 2) exec_fdom_empty_prob by blast } then show "((reachable_s PROB s) ⊆ {fmempty})" by blast qed ― ‹NOTE this is semantically equivalent to `sublist\_valid\_is\_valid`.› ― ‹NOTE Renamed to 'sublist\_valid\_plan\_alt' because another lemma by the same name is declared later.› lemma sublist_valid_plan__alt: assumes "(as1 ∈ valid_plans PROB)" "(subseq as2 as1)" shows "(as2 ∈ valid_plans PROB)" using assms by (auto simp add: sublist_valid_is_valid) lemma fmsubset_eq: assumes "s1 ⊆⇩_{f}s2" shows "(∀a. a |∈| fmdom s1 ⟶ fmlookup s1 a = fmlookup s2 a)" using assms by (metis (mono_tags, lifting) domIff fmdom_notI fmsubset.rep_eq map_le_def) ― ‹NOTE added lemma.› ― ‹TODO refactor/move into 'FmapUtils.thy'.› lemma submap_imp_state_succ_submap_a: assumes "s1 ⊆⇩_{f}s2" "s2 ⊆⇩_{f}s3" shows "s1 ⊆⇩_{f}s3" using assms fmsubset.rep_eq map_le_trans by blast ― ‹NOTE added lemma.› ― ‹TODO refactor into FmapUtils?› lemma submap_imp_state_succ_submap_b: assumes "s1 ⊆⇩_{f}s2" shows "(s0 ++ s1) ⊆⇩_{f}(s0 ++ s2)" proof - { assume C: "¬((s0 ++ s1) ⊆⇩_{f}(s0 ++ s2))" then have 1: "(s0 ++ s1) = (s1 ++⇩_{f}s0)" using fmap_add_ltr_def by blast then have 2: "(s0 ++ s2) = (s2 ++⇩_{f}s0)" using fmap_add_ltr_def by auto then obtain a where 3: "a |∈| fmdom (s1 ++⇩_{f}s0) ∧ fmlookup (s1 ++⇩_{f}s0) ≠ fmlookup (s2 ++⇩_{f}s0)" using C 1 2 fmsubset.rep_eq domIff fmdom_notD map_le_def by (metis (no_types, lifting)) then have False using assms(1) C proof (cases "a |∈| fmdom s1") case True moreover have "fmlookup s1 a = fmlookup s2 a" by (meson assms(1) calculation fmsubset_eq) moreover have "fmlookup (s0 ++⇩_{f}s1) a = fmlookup s1 a" by (simp add: True) moreover have "a |∈| fmdom s2" using True calculation(2) fmdom_notD by fastforce moreover have "fmlookup (s0 ++⇩_{f}s2) a = fmlookup s2 a" by (simp add: calculation(4)) moreover have "fmlookup (s0 ++⇩_{f}s1) a = fmlookup (s0 ++⇩_{f}s2) a" using calculation(2, 3, 5) by auto ultimately show ?thesis by (smt "1" "2" C assms domIff fmlookup_add fmsubset.rep_eq map_le_def) next case False moreover have "fmlookup (s0 ++⇩_{f}s1) a = fmlookup s0 a" by (auto simp add: False) ultimately show ?thesis proof (cases "a |∈| fmdom s0") case True have "a |∉| fmdom (s1 ++⇩_{f}s0)" by (smt "1" "2" C UnE assms dom_map_add fmadd.rep_eq fmsubset.rep_eq map_add_def map_add_dom_app_simps(1) map_le_def) then show ?thesis using 3 by blast next case False then have "a |∉| fmdom (s1 ++⇩_{f}s0)" using ‹fmlookup (s0 ++⇩_{f}s1) a = fmlookup s0 a› by force then show ?thesis using 3 by blast qed qed } then show ?thesis by blast qed ― ‹NOTE type for `a` had to be fixed (type mismatch in goal).› lemma submap_imp_state_succ_submap: fixes a :: "'a action" and s1 s2 assumes "(fst a ⊆⇩_{f}s1)" "(s1 ⊆⇩_{f}s2)" shows "(state_succ s1 a ⊆⇩_{f}state_succ s2 a)" proof - have 1: "state_succ s1 a = (snd a ++ s1)" using assms(1) by (simp add: state_succ_def) then have "fst a ⊆⇩_{f}s2" using assms(1, 2) submap_imp_state_succ_submap_a by auto then have 2: "state_succ s2 a = (snd a ++ s2)" using 1 state_succ_def by metis then have "snd a ++ s1 ⊆⇩_{f}snd a ++ s2" using assms(2) submap_imp_state_succ_submap_b by fast then show ?thesis using 1 2 by argo qed ― ‹NOTE types for `a`, `s1` and `s2` had to be fixed (type mismatch in goal).› lemma pred_dom_subset_succ_submap: fixes a :: "'a action" and s1 s2 :: "'a state" assumes "(fmdom' (fst a) ⊆ fmdom' s1)" "(s1 ⊆⇩_{f}s2)" shows "(state_succ s1 a ⊆⇩_{f}state_succ s2 a)" using assms unfolding state_succ_def proof (auto) assume P1: "fmdom' (fst a) ⊆ fmdom' s1" "s1 ⊆⇩_{f}s2" "fst a ⊆⇩_{f}s1" "fst a ⊆⇩_{f}s2" then show "snd a ++ s1 ⊆⇩_{f}snd a ++ s2" using submap_imp_state_succ_submap_b by fast next assume P2: "fmdom' (fst a) ⊆ fmdom' s1" "s1 ⊆⇩_{f}s2" "fst a ⊆⇩_{f}s1" "¬ fst a ⊆⇩_{f}s2" then show "snd a ++ s1 ⊆⇩_{f}s2" using submap_imp_state_succ_submap_a by blast next assume P3: "fmdom' (fst a) ⊆ fmdom' s1" "s1 ⊆⇩_{f}s2" "¬ fst a ⊆⇩_{f}s1" "fst a ⊆⇩_{f}s2" { have a: "fmlookup s1 ⊆⇩_{m}fmlookup s2" using P3(2) fmsubset.rep_eq by blast { have "¬(fmlookup (fst a) ⊆⇩_{m}fmlookup s1)" using P3(3) fmsubset.rep_eq by blast then have "∃v ∈ dom (fmlookup (fst a)). fmlookup (fst a) v ≠ fmlookup s1 v" using map_le_def by fast } then obtain v where b: "v ∈ dom (fmlookup (fst a))" "fmlookup (fst a) v ≠ fmlookup s1 v" by blast then have "fmlookup (fst a) v ≠ fmlookup s2 v" using assms(1) a contra_subsetD fmdom'.rep_eq map_le_def by metis then have "¬(fst a ⊆⇩_{f}s2)" using b fmsubset.rep_eq map_le_def by metis } then show "s1 ⊆⇩_{f}snd a ++ s2" using P3(4) by simp qed ― ‹NOTE added lemma.› ― ‹TODO refactor.› lemma valid_as_submap_init_submap_exec_i: fixes s a shows "fmdom' s ⊆ fmdom' (state_succ s a)" proof (cases "fst a ⊆⇩_{f}s") case True then have "state_succ s a = s ++⇩_{f}(snd a)" unfolding state_succ_def using fmap_add_ltr_def by auto then have "fmdom' (state_succ s a) = fmdom' s ∪ fmdom' (snd a)" using fmdom'_add by simp then show ?thesis by simp next case False then show ?thesis unfolding state_succ_def by simp qed ― ‹NOTE types for `s1` and `s2` had to be fixed in order to apply `pred\_dom\_subset\_succ\_submap`.› lemma valid_as_submap_init_submap_exec: fixes s1 s2 :: "'a state" assumes "(s1 ⊆⇩_{f}s2) " "(∀a. ListMem a as ⟶ (fmdom' (fst a) ⊆ fmdom' s1))" shows "(exec_plan s1 as ⊆⇩_{f}exec_plan s2 as)" using assms proof (induction as arbitrary: s1 s2) case (Cons a as) { have "ListMem a (a # as)" using elem by fast then have "fmdom' (fst a) ⊆ fmdom' s1" using Cons.prems(2) by blast then have "state_succ s1 a ⊆⇩_{f}state_succ s2 a" using Cons.prems(1) pred_dom_subset_succ_submap by fast } note 1 = this { fix b assume "ListMem b as" then have "ListMem b (a # as)" using insert by fast then have a: "fmdom' (fst b) ⊆ fmdom' s1" using Cons.prems(2) by blast then have "fmdom' s1 ⊆ fmdom' (state_succ s1 a)" using valid_as_submap_init_submap_exec_i by metis then have "fmdom' (fst b) ⊆ fmdom' (state_succ s1 a)" using a by simp } then show ?case using 1 Cons.IH[of "(state_succ s1 a)" "(state_succ s2 a)"] by fastforce qed auto lemma valid_plan_mems: assumes "(as ∈ valid_plans PROB)" "(ListMem a as)" shows "a ∈ PROB" using assms ListMem_iff in_set_conv_decomp valid_append_valid_suff valid_plan_valid_head by (metis) ― ‹NOTE typing moved into 'fixes' due to type mismatches when using lemma.› ― ‹NOTE showcase (this can't be used due to type problems when the type is specified within proposition.› lemma valid_states_nempty: fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set" assumes "finite PROB" shows "∃s. s ∈ (valid_states PROB)" unfolding valid_states_def using fmchoice'[OF FINITE_prob_dom[OF assms], where Q = "λ_ _. True"] by auto lemma empty_prob_dom_single_val_state: assumes "(prob_dom PROB = {})" shows "(∃s. valid_states PROB = {s})" proof - { assume C: "¬(∃s. valid_states PROB = {s})" then have "valid_states PROB = {s. fmdom' s = {}}" using assms by (simp add: valid_states_def) then have "∃s. valid_states PROB = {s}" using empty_domain_fmap_set by blast then have False using C by blast } then show ?thesis by blast qed lemma empty_prob_dom_imp_empty_plan_always_good: fixes PROB s assumes "(prob_dom PROB = {})" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" shows "(exec_plan s [] = exec_plan s as)" using assms empty_plan_is_valid exec_fdom_empty_prob by fastforce lemma empty_prob_dom: fixes PROB assumes "(prob_dom PROB = {})" shows "(PROB = {(fmempty, fmempty)} ∨ PROB = {})" using assms proof (cases "PROB = {}") case False have "⋃((λ(s1, s2). fmdom' s1 ∪ fmdom' s2) ` PROB) = {}" using assms by (simp add: prob_dom_def action_dom_def) then have 1:"∀a∈PROB. (λ(s1, s2). fmdom' s1 ∪ fmdom' s2) a = {}" using Union_empty_conv by auto { fix a assume P1: "a∈PROB" then have "(λ(s1, s2). fmdom' s1 ∪ fmdom' s2) a = {}" using 1 by simp then have a: "fmdom' (fst a) = {}" "fmdom' (snd a) = {}" by auto+ then have b: "fst a = fmempty" using fmrestrict_set_dom fmrestrict_set_null by metis then have "snd a = fmempty" using a(2) fmrestrict_set_dom fmrestrict_set_null by metis then have "a = (fmempty, fmempty)" using b surjective_pairing by metis } then have "PROB = {(fmempty, fmempty)}" using False by blast then show ?thesis by blast qed simp lemma empty_prob_dom_finite: fixes PROB :: "'a problem" assumes "prob_dom PROB = {}" shows "finite PROB" proof - consider (i) "PROB = {(fmempty, fmempty)}" | (ii) "PROB = {}" using assms empty_prob_dom by auto then show ?thesis by (cases) auto qed ― ‹NOTE type for `a` had to be fixed (type mismatch in goal).› lemma disj_imp_eq_proj_exec: fixes a :: "('a, 'b) fmap × ('a, 'b) fmap" and vs s assumes "(fmdom' (snd a) ∩ vs) = {}" shows "(fmrestrict_set vs s = fmrestrict_set vs (state_succ s a))" proof - have "disjnt (fmdom' (snd a)) vs" using assms disjnt_def by fast then show ?thesis using disj_dom_drest_fupdate_eq state_succ_pair surjective_pairing by metis qed lemma no_change_vs_eff_submap: fixes a vs s assumes "(fmrestrict_set vs s = fmrestrict_set vs (state_succ s a))" "(fst a ⊆⇩_{f}s)" shows "(fmrestrict_set vs (snd a) ⊆⇩_{f}(fmrestrict_set vs s))" proof - { fix x assume P3: "x ∈ dom (fmlookup (fmrestrict_set vs (snd a)))" then have "(fmlookup (fmrestrict_set vs (snd a))) x = (fmlookup (fmrestrict_set vs s)) x" proof (cases "fmlookup (fmrestrict_set vs (snd a)) x") case None then show ?thesis using P3 by blast next case (Some y) then have "fmrestrict_set vs s = fmrestrict_set vs (s ++⇩_{f}snd a)" using assms by (simp add: state_succ_def fmap_add_ltr_def) then have "fmlookup (fmrestrict_set vs s) = fmlookup (fmrestrict_set vs (s ++⇩_{f}snd a))" by auto then have 1: " fmlookup (fmrestrict_set vs s) x = (if x ∈ vs then fmlookup (s ++⇩_{f}snd a) x else None) " using fmlookup_restrict_set by metis then show ?thesis proof (cases "x ∈ vs") case True then have "fmlookup (fmrestrict_set vs s) x = fmlookup (s ++⇩_{f}snd a) x" using True 1 by auto then show ?thesis using Some fmadd.rep_eq fmlookup_restrict_set map_add_Some_iff by (metis (mono_tags, lifting)) next case False then have 1: "fmlookup (fmrestrict_set vs s) x = None" using False "1" by auto then show ?thesis using 1 False by auto qed qed } then have "(fmlookup (fmrestrict_set vs (snd a)) ⊆⇩_{m}fmlookup (fmrestrict_set vs s))" using map_le_def by blast then show ?thesis using fmsubset.rep_eq by blast qed ― ‹NOTE type of `a` had to be fixed.› lemma sat_precond_as_proj_3: fixes s and a :: "('a, 'b) fmap × ('a, 'b) fmap" and vs assumes "(fmdom' (fmrestrict_set vs (snd a)) = {})" shows "((fmrestrict_set vs (state_succ s a)) = (fmrestrict_set vs s))" proof - have "fmdom' (fmrestrict_set vs (fmrestrict_set vs (snd a))) = {}" using assms fmrestrict_set_dom fmrestrict_set_empty fmrestrict_set_null by metis { fix x assume C: "x ∈ fmdom' (snd a) ∧ x ∈ vs" then have a: "x ∈ fmdom' (snd a)" "x ∈ vs" using C by blast+ then have "fmlookup (snd a) x ≠ None" using fmdom'_notI by metis then have "fmlookup (fmrestrict_set vs (snd a)) x ≠ None" using a(2) by force then have "x ∈ fmdom' (fmrestrict_set vs (snd a))" using fmdom'_notD by metis then have "fmdom' (fmrestrict_set vs (snd a)) ≠ {}" by blast then have False using assms by blast } then have "∀x. ¬(x ∈ fmdom' (snd a) ∧ x ∈ vs)" by blast then have 1: "fmdom' (snd a) ∩ vs = {}" by blast have "disjnt (fmdom' (snd a)) vs" using 1 disjnt_def by blast then show ?thesis using 1 disj_imp_eq_proj_exec by metis qed ― ‹NOTE type for `a` had to be fixed (type mismatch in goal).› ― ‹TODO showcase (quick win with simp).› lemma proj_eq_proj_exec_eq: fixes s s' vs and a :: "('a, 'b) fmap × ('a, 'b) fmap" and a' assumes "((fmrestrict_set vs s) = (fmrestrict_set vs s'))" "((fst a ⊆⇩_{f}s) = (fst a' ⊆⇩_{f}s'))" "(fmrestrict_set vs (snd a) = fmrestrict_set vs (snd a'))" shows "(fmrestrict_set vs (state_succ s a) = fmrestrict_set vs (state_succ s' a'))" using assms by (simp add: fmap_add_ltr_def state_succ_def) lemma empty_eff_exec_eq: fixes s a assumes "(fmdom' (snd a) = {})" shows "(state_succ s a = s)" using assms unfolding state_succ_def fmap_add_ltr_def by (metis fmadd_empty(2) fmrestrict_set_dom fmrestrict_set_null) lemma exec_as_proj_valid_2: fixes a assumes "a ∈ PROB" shows "(action_dom (fst a) (snd a) ⊆ prob_dom PROB)" using assms by (simp add: FDOM_eff_subset_prob_dom_pair FDOM_pre_subset_prob_dom_pair action_dom_def) lemma valid_filter_valid_as: assumes "(as ∈ valid_plans PROB)" shows "(filter P as ∈ valid_plans PROB)" using assms by(auto simp: valid_plans_def) lemma sublist_valid_plan: assumes "(subseq as' as)" "(as ∈ valid_plans PROB)" shows "(as' ∈ valid_plans PROB)" using assms by (auto simp: valid_plans_def) (meson fset_mp fset_of_list_elem sublist_subset subsetCE) lemma prob_subset_dom_subset: assumes "PROB1 ⊆ PROB2" shows "(prob_dom PROB1 ⊆ prob_dom PROB2)" using assms by (auto simp add: prob_dom_def) lemma state_succ_valid_act_disjoint: assumes "(a ∈ PROB)" "(vs ∩ (prob_dom PROB) = {})" shows "(fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s)" using assms by (smt FDOM_eff_subset_prob_dom_pair disj_imp_eq_proj_exec inf.absorb1 inf_bot_right inf_commute inf_left_commute ) lemma exec_valid_as_disjoint: fixes s assumes "(vs ∩ (prob_dom PROB) = {})" "(as ∈ valid_plans PROB)" shows "(fmrestrict_set vs (exec_plan s as) = fmrestrict_set vs s)" using assms proof (induction as arbitrary: s vs PROB) case (Cons a as) then show ?case by (metis exec_plan.simps(2) state_succ_valid_act_disjoint valid_plan_valid_head valid_plan_valid_tail) qed simp definition state_successors where "state_successors PROB s ≡ ((state_succ s ` PROB) - {s})" subsection "State Spaces" definition stateSpace where "stateSpace ss vs ≡ (∀s. s ∈ ss ⟶ (fmdom' s = vs))" lemma EQ_SS_DOM: assumes "¬(ss = {})" "(stateSpace ss vs1)" "(stateSpace ss vs2)" shows "(vs1 = vs2)" using assms by (auto simp: stateSpace_def) ― ‹NOTE Name 'dom' changed to 'domain' because of name clash with 'Map.dom'.› lemma FINITE_SS: fixes ss :: "('a, bool) fmap set" assumes "¬(ss = {})" "(stateSpace ss domain)" shows "finite ss" proof - have 1: "stateSpace ss domain = (∀s. s ∈ ss ⟶ (fmdom' s = domain))" by (simp add: stateSpace_def) { fix s assume P1: "s ∈ ss" have "fmdom' s = domain" using assms 1 P1 by blast then have "s ∈ {s. fmdom' s = domain}" by auto } then have 2: "ss ⊆ {s. fmdom' s = domain}" by blast ― ‹TODO add lemma (finite (fmdom' s))› then have "finite domain" using 1 assms by fastforce then have "finite {s :: 'a state. fmdom' s = domain}" using FINITE_states by blast then show ?thesis using 2 finite_subset by auto qed lemma disjoint_effects_no_effects: fixes s assumes "(∀a. ListMem a as ⟶ (fmdom' (fmrestrict_set vs (snd a)) = {}))" shows "(fmrestrict_set vs (exec_plan s as) = (fmrestrict_set vs s))" using assms proof (induction as arbitrary: s vs) case (Cons a as) then have "ListMem a (a # as)" using elem by fast then have "fmdom' (fmrestrict_set vs (snd a)) = {}" using Cons.prems(1) by blast then have "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s" using sat_precond_as_proj_3 by blast then show ?case by (simp add: Cons.IH Cons.prems insert) qed auto subsection "Needed Asses" ― ‹NOTE name shortened.› definition action_needed_vars where "action_needed_vars a s ≡ {v. (v ∈ fmdom' s) ∧ (v ∈ fmdom' (fst a)) ∧ (fmlookup (fst a) v = fmlookup s v)}" ― ‹NOTE name shortened to 'action\_needed\_asses'.› definition action_needed_asses where "action_needed_asses a s ≡ fmrestrict_set (action_needed_vars a s) s" ― ‹NOTE type for 'a' had to be fixed (type mismatch in goal).› lemma act_needed_asses_submap_succ_submap: fixes a s1 s2 assumes "(action_needed_asses a s2 ⊆⇩_{f}action_needed_asses a s1)" "(s1 ⊆⇩_{f}s2)" shows "(state_succ s1 a ⊆⇩_{f}state_succ s2 a)" using assms unfolding state_succ_def proof (auto) assume P1: "action_needed_asses a s2 ⊆⇩_{f}action_needed_asses a s1" "s1 ⊆⇩_{f}s2" "fst a ⊆⇩_{f}s1" "fst a ⊆⇩_{f}s2" then show "snd a ++ s1 ⊆⇩_{f}snd a ++ s2" using submap_imp_state_succ_submap_b by blast next assume P2: "action_needed_asses a s2 ⊆⇩_{f}action_needed_asses a s1" "s1 ⊆⇩_{f}s2" "fst a ⊆⇩_{f}s1" "¬ fst a ⊆⇩_{f}s2" then show "snd a ++ s1 ⊆⇩_{f}s2" using submap_imp_state_succ_submap_a by blast next assume P3: "action_needed_asses a s2 ⊆⇩_{f}action_needed_asses a s1" "s1 ⊆⇩_{f}s2" "¬ fst a ⊆⇩_{f}s1" "fst a ⊆⇩_{f}s2" let ?vs1="{v ∈ fmdom' s1. v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup s1 v}" let ?vs2="{v ∈ fmdom' s2. v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup s2 v}" let ?f="fmrestrict_set ?vs1 s1" let ?g="fmrestrict_set ?vs2 s2" have 1: "fmdom' ?f = ?vs1" "fmdom' ?g = ?vs2" unfolding action_needed_asses_def action_needed_vars_def fmdom'_restrict_set_precise by blast+ have 2: "fmlookup ?g ⊆⇩_{m}fmlookup ?f" using P3(1) unfolding action_needed_asses_def action_needed_vars_def using fmsubset.rep_eq by blast { { fix v assume P3_1: "v ∈ fmdom' ?g" then have "v ∈ fmdom' s2" "v ∈ fmdom' (fst a)" "fmlookup (fst a) v = fmlookup s2 v" using 1 by simp+ then have "fmlookup (fst a) v = fmlookup ?g v" by simp then have "fmlookup (fst a) v = fmlookup ?f v" using 2 by (metis (mono_tags, lifting) P3_1 domIff fmdom'_notI map_le_def) } then have i: "fmlookup (fst a) ⊆⇩_{m}fmlookup ?f" using P3(4) 1(2) by (smt domIff fmdom'_notD fmsubset.rep_eq map_le_def mem_Collect_eq) { fix v assume P3_2: "v ∈ dom (fmlookup (fst a))" then have "fmlookup (fst a) v = fmlookup ?f v" using i by (meson domIff fmdom'_notI map_le_def) then have "v ∈ ?vs1" using P3_2 1(1) by (metis (no_types, lifting) domIff fmdom'_notD) then have "fmlookup (fst a) v = fmlookup s1 v" by blast } then have "fst a ⊆⇩_{f}s1" by (simp add: map_le_def fmsubset.rep_eq) } then show "s1 ⊆⇩_{f}snd a ++ s2" using P3(3) by simp qed ― ‹NOTE added lemma.› ― ‹TODO refactor.› lemma as_needed_asses_submap_exec_i: fixes a s assumes "v ∈ fmdom' (action_needed_asses a s)" shows " fmlookup (action_needed_asses a s) v = fmlookup s v ∧ fmlookup (action_needed_asses a s) v = fmlookup (fst a) v" using assms unfolding action_needed_asses_def action_needed_vars_def using fmdom'_notI fmlookup_restrict_set by (smt mem_Collect_eq) ― ‹NOTE added lemma.› ― ‹TODO refactor.› lemma as_needed_asses_submap_exec_ii: fixes f g v assumes "v ∈ fmdom' f" "f ⊆⇩_{f}g" shows "fmlookup f v = fmlookup g v" using assms by (meson fmdom'_notI fmdom_notD fmsubset_eq) ― ‹NOTE added lemma.› ― ‹TODO refactor.› lemma as_needed_asses_submap_exec_iii: fixes f g v shows " fmdom' (action_needed_asses a s) = {v ∈ fmdom' s. v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup s v}" unfolding action_needed_asses_def action_needed_vars_def by (simp add: Set.filter_def fmfilter_alt_defs(4)) ― ‹NOTE added lemma.› lemma as_needed_asses_submap_exec_iv: fixes f a v assumes "v ∈ fmdom' (action_needed_asses a s)" shows " fmlookup (action_needed_asses a s) v = fmlookup s v ∧ fmlookup (action_needed_asses a s) v = fmlookup (fst a) v ∧ fmlookup (fst a) v = fmlookup s v" using assms proof - have 1: "v ∈ {v ∈ fmdom' s. v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup s v}" using assms as_needed_asses_submap_exec_iii by metis then have 2: "fmlookup (action_needed_asses a s) v = fmlookup s v" unfolding action_needed_asses_def action_needed_vars_def by force moreover have 3: "fmlookup (action_needed_asses a s) v = fmlookup (fst a) v" using 1 2 by simp moreover have "fmlookup (fst a) v = fmlookup s v" using 2 3 by argo ultimately show ?thesis by blast qed ― ‹NOTE added lemma.› ― ‹TODO refactor (into Fmap\_Utils.thy).› lemma as_needed_asses_submap_exec_v: fixes f g v assumes "v ∈ fmdom' f" "f ⊆⇩_{f}g" shows "v ∈ fmdom' g" proof - obtain b where 1: "fmlookup f v = b" "b ≠ None" using assms(1) by (meson fmdom'_notI) then have "fmlookup g v = b" using as_needed_asses_submap_exec_ii[OF assms] by argo then show ?thesis using 1 fmdom'_notD by fastforce qed ― ‹NOTE added lemma.› ― ‹TODO refactor.› lemma as_needed_asses_submap_exec_vi: fixes a s1 s2 v assumes "v ∈ fmdom' (action_needed_asses a s1)" "(action_needed_asses a s1) ⊆⇩_{f}(action_needed_asses a s2)" shows "(fmlookup (action_needed_asses a s1) v) = fmlookup (fst a) v ∧ (fmlookup (action_needed_asses a s2) v) = fmlookup (fst a) v ∧ fmlookup s1 v = fmlookup (fst a) v ∧ fmlookup s2 v = fmlookup (fst a) v" using assms proof - have 1: "fmlookup (action_needed_asses a s1) v = fmlookup s1 v" "fmlookup (action_needed_asses a s1) v = fmlookup (fst a) v" "fmlookup (fst a) v = fmlookup s1 v" using as_needed_asses_submap_exec_iv[OF assms(1)] by blast+ moreover { have "fmlookup (action_needed_asses a s1) v = fmlookup (action_needed_asses a s2) v" using as_needed_asses_submap_exec_ii[OF assms] by simp then have "fmlookup (action_needed_asses a s2) v = fmlookup (fst a) v" using 1(2) by argo } note 2 = this moreover { have "v ∈ fmdom' (action_needed_asses a s2)" using as_needed_asses_submap_exec_v[OF assms] by simp then have "fmlookup s2 v = fmlookup (action_needed_asses a s2) v" using as_needed_asses_submap_exec_i by metis also have "… = fmlookup (fst a) v" using 2 by simp finally have "fmlookup s2 v = fmlookup (fst a) v" by simp } ultimately show ?thesis by argo qed ― ‹TODO refactor.› ― ‹NOTE added lemma.› lemma as_needed_asses_submap_exec_vii: fixes f g v assumes "∀v ∈ fmdom' f. fmlookup f v = fmlookup g v" shows "f ⊆⇩_{f}g" proof - { fix v assume a: "v ∈ fmdom' f" then have "v ∈ dom (fmlookup f)" by simp moreover have "fmlookup f v = fmlookup g v" using assms a by blast ultimately have "v ∈ dom (fmlookup f) ⟶ fmlookup f v = fmlookup g v" by blast } then have "fmlookup f ⊆⇩_{m}fmlookup g" by (simp add: map_le_def) then show ?thesis by (simp add: fmsubset.rep_eq) qed ― ‹TODO refactor.› ― ‹NOTE added lemma.› lemma as_needed_asses_submap_exec_viii: fixes f g v assumes "f ⊆⇩_{f}g" shows "∀v ∈ fmdom' f. fmlookup f v = fmlookup g v" proof - have 1: "fmlookup f ⊆⇩_{m}fmlookup g" using assms by (simp add: fmsubset.rep_eq) { fix v assume "v ∈ fmdom' f" then have "v ∈ dom (fmlookup f)" by simp then have "fmlookup f v = fmlookup g v" using 1 map_le_def by metis } then show ?thesis by blast qed ― ‹NOTE added lemma.› lemma as_needed_asses_submap_exec_viii': fixes f g v assumes "f ⊆⇩_{f}g" shows "fmdom' f ⊆ fmdom' g" using assms as_needed_asses_submap_exec_v subsetI by metis ― ‹NOTE added lemma.› ― ‹TODO refactor.› lemma as_needed_asses_submap_exec_ix: fixes f g shows "f ⊆⇩_{f}g = (∀v ∈ fmdom' f. fmlookup f v = fmlookup g v)" using as_needed_asses_submap_exec_vii as_needed_asses_submap_exec_viii by metis ― ‹NOTE added lemma.› lemma as_needed_asses_submap_exec_x: fixes f a v assumes "v ∈ fmdom' (action_needed_asses a f)" shows "v ∈ fmdom' (fst a) ∧ v ∈ fmdom' f ∧ fmlookup (fst a) v = fmlookup f v" using assms unfolding action_needed_asses_def action_needed_vars_def using as_needed_asses_submap_exec_i assms by (metis fmdom'_notD fmdom'_notI) ― ‹NOTE added lemma.› ― ‹TODO refactor.› lemma as_needed_asses_submap_exec_xi: fixes v a f g assumes "v ∈ fmdom' (action_needed_asses a (f ++ g))" "v ∈ fmdom' f" shows " fmlookup (action_needed_asses a (f ++ g)) v = fmlookup f v ∧ fmlookup (action_needed_asses a (f ++ g)) v = fmlookup (fst a) v" proof - have 1: "v ∈ {v ∈ fmdom' (f ++ g). v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup (f ++ g) v}" using as_needed_asses_submap_exec_x[OF assms(1)] by blast { have "v |∈| fmdom f" using assms(2) by (meson fmdom'_notI fmdom_notD) then have "fmlookup (f ++ g) v = fmlookup f v" unfolding fmap_add_ltr_def fmlookup_add by simp } note 2 = this { have "fmlookup (action_needed_asses a (f ++ g)) v = fmlookup (f ++ g) v" unfolding action_needed_asses_def action_needed_vars_def using 1 by force then have "fmlookup (action_needed_asses a (f ++ g)) v = fmlookup f v" using 2 by simp } note 3 = this moreover { have "fmlookup (fst a) v = fmlookup (f ++ g) v" using 1 by simp also have "… = fmlookup f v" using 2 by simp also have "… = fmlookup (action_needed_asses a (f ++ g)) v" using 3 by simp finally have "fmlookup (action_needed_asses a (f ++ g)) v = fmlookup (fst a) v" by simp } ultimately show ?thesis by blast qed ― ‹NOTE added lemma.› ― ‹TODO refactor (into Fmap\_Utils.thy).› lemma as_needed_asses_submap_exec_xii: fixes f g v assumes "v ∈ fmdom' f" shows "fmlookup (f ++ g) v = fmlookup f v" proof - have "v |∈| fmdom f" using assms(1) fmdom'_notI fmdom_notD by metis then show ?thesis unfolding fmap_add_ltr_def using fmlookup_add by force qed ― ‹NOTE added lemma.› lemma as_needed_asses_submap_exec_xii': fixes f g v assumes "v ∉ fmdom' f" "v ∈ fmdom' g" shows "fmlookup (f ++ g) v = fmlookup g v" proof - have "¬(v |∈| fmdom f)" using assms(1) fmdom'_notI fmdom_notD by fastforce moreover have "v |∈| fmdom g" using assms(2) fmdom'_notI fmdom_notD by metis ultimately show ?thesis unfolding fmap_add_ltr_def using fmlookup_add by simp qed ― ‹NOTE showcase.› lemma as_needed_asses_submap_exec: fixes s1 s2 assumes "(s1 ⊆⇩_{f}s2)" "(∀a. ListMem a as ⟶ (action_needed_asses a s2 ⊆⇩_{f}action_needed_asses a s1))" shows "(exec_plan s1 as ⊆⇩_{f}exec_plan s2 as)" using assms proof (induction as arbitrary: s1 s2) case (Cons a as) ― ‹Proof the premises of the induction hypothesis for 'state\_succ s1 a' and 'state\_succ s2 a'.› { then have "action_needed_asses a s2 ⊆⇩_{f}action_needed_asses a s1" using Cons.prems(2) elem by metis then have "state_succ s1 a ⊆⇩_{f}state_succ s2 a" using Cons.prems(1) act_needed_asses_submap_succ_submap by blast } note 1 = this moreover { fix a' assume P: "ListMem a' as" ― ‹Show the goal by rule 'as\_needed\_asses\_submap\_exec\_ix'.› let ?f="action_needed_asses a' (state_succ s2 a)" let ?g="action_needed_asses a' (state_succ s1 a)" { fix v assume P_1: "v ∈ fmdom' ?f" then have "fmlookup ?f v = fmlookup ?g v" unfolding state_succ_def text ‹ Split cases on the if-then branches introduced by the definition of 'state\_succ'.› proof (auto) assume P_1_1: "v ∈ fmdom' (action_needed_asses a' (snd a ++ s2))" "fst a ⊆⇩_{f}s2" "fst a ⊆⇩_{f}s1" have i: "action_needed_asses a' s2 ⊆⇩_{f}action_needed_asses a' s1" using Cons.prems(2) P insert by fast then show " fmlookup (action_needed_asses a' (snd a ++ s2)) v = fmlookup (action_needed_asses a' (snd a ++ s1)) v" proof (cases "v ∈ fmdom' ?g") case true: True then have A: "v ∈ fmdom' (fst a') ∧ v ∈ fmdom' (snd a ++ s1) ∧ fmlookup (fst a') v = fmlookup (snd a ++ s1) v" using as_needed_asses_submap_exec_x[OF true] unfolding state_succ_def using P_1_1(3) by simp then have B: "v ∈ fmdom' (fst a') ∧ v ∈ fmdom' (snd a ++ s2) ∧ fmlookup (fst a') v = fmlookup (snd a ++ s2) v" using as_needed_asses_submap_exec_x[OF P_1] unfolding state_succ_def using P_1_1(2) by simp then show ?thesis proof (cases "v ∈ fmdom' (snd a)") case True then have I: "fmlookup (snd a ++ s2) v = fmlookup (snd a) v" "fmlookup (snd a ++ s1) v = fmlookup (snd a) v" using as_needed_asses_submap_exec_xii by fast+ moreover { have "fmlookup ?f v = fmlookup (snd a ++ s2) v" using as_needed_asses_submap_exec_iv[OF P_1] unfolding state_succ_def using P_1_1(2) by presburger then have "fmlookup ?f v = fmlookup (snd a) v" using I(1) by argo } moreover { have "fmlookup ?g v = fmlookup (snd a ++ s1) v" using as_needed_asses_submap_exec_iv[OF true] unfolding state_succ_def using P_1_1(3) by presburger then have "fmlookup ?g v = fmlookup (snd a) v" using I(2) by argo } ultimately show ?thesis unfolding state_succ_def using P_1_1(2, 3) by presburger next case False then have I: "v ∈ fmdom' s1" "v ∈ fmdom' s2" using A B unfolding fmap_add_ltr_def fmdom'_add by blast+ { have "fmlookup ?g v = fmlookup (snd a ++ s1) v" using as_needed_asses_submap_exec_iv[OF true] unfolding state_succ_def using P_1_1(3) by presburger then have "fmlookup ?g v = fmlookup s1 v" using as_needed_asses_submap_exec_xii'[OF False I(1)] by simp moreover { have "fmlookup (snd a ++ s1) v = fmlookup s1 v" using as_needed_asses_submap_exec_xii'[OF False I(1)] by simp moreover from ‹fmlookup (snd a ++ s1) v = fmlookup s1 v› have "fmlookup (fst a') v = fmlookup s1 v" using A(1) by argo ultimately have "fmlookup (action_needed_asses a' s1) v = fmlookup s1 v" using A(1) I(1) unfolding action_needed_asses_def action_needed_vars_def fmlookup_restrict_set by simp } ultimately have "fmlookup ?g v = fmlookup (action_needed_asses a' s1) v" by argo } note II = this { have "fmlookup ?f v = fmlookup (snd a ++ s2) v" using as_needed_asses_submap_exec_iv[OF P_1] unfolding state_succ_def using P_1_1(2) by presburger moreover from ‹fmlookup ?f v = fmlookup (snd a ++ s2) v› have α: "fmlookup ?f v = fmlookup s2 v" using as_needed_asses_submap_exec_xii'[OF False I(2)] by argo ultimately have "fmlookup (snd a ++ s2) v = fmlookup s2 v" by argo moreover { from ‹fmlookup (snd a ++ s2) v = fmlookup s2 v› have "fmlookup (fst a') v = fmlookup s2 v" using B(1) by argo then have "fmlookup (action_needed_asses a' s2) v = fmlookup s2 v" using B(1) I(2) unfolding action_needed_asses_def action_needed_vars_def fmlookup_restrict_set by simp } ultimately have "fmlookup ?f v = fmlookup (action_needed_asses a' s2) v" using α by argo } note III = this { have "v ∈ fmdom' (action_needed_asses a' s2)" proof - have "fmlookup (fst a') v = fmlookup s1 v" by (simp add: A False I(1) as_needed_asses_submap_exec_xii') then show ?thesis by (simp add: A Cons.prems(1) I(1, 2) as_needed_asses_submap_exec_ii as_needed_asses_submap_exec_iii) qed then have " fmlookup (action_needed_asses a' s2) v = fmlookup (action_needed_asses a' s1) v" using i as_needed_asses_submap_exec_ix[of "action_needed_asses a' s2" "action_needed_asses a' s1"] by blast } note IV = this { have "fmlookup ?f v = fmlookup (action_needed_asses a' s2) v" using III by simp also have "… = fmlookup (action_needed_asses a' s1) v" using IV by simp finally have "… = fmlookup ?g v" using II by simp } then show ?thesis unfolding action_needed_asses_def action_needed_vars_def state_succ_def using P_1_1 A B by simp qed next case false: False have A: "v ∈ fmdom' (fst a') ∧ v ∈ fmdom' (snd a ++ s2) ∧ fmlookup (fst a') v = fmlookup (snd a ++ s2) v" using as_needed_asses_submap_exec_x[OF P_1] unfolding state_succ_def using P_1_1(2) by simp from false have B: "¬(v ∈ fmdom' (snd a ++ s1)) ∨ ¬(fmlookup (fst a') v = fmlookup (snd a ++ s1) v)" by (simp add: A P_1_1(3) as_needed_asses_submap_exec_iii state_succ_def) then show ?thesis proof (cases "v ∈ fmdom' (snd a)") case True then have I: "v ∈ fmdom' (snd a ++ s1)" unfolding fmap_add_ltr_def fmdom'_add by simp { from True have "fmlookup (snd a ++ s2) v = fmlookup (snd a) v" "fmlookup (snd a ++ s1) v = fmlookup (snd a) v" using as_needed_asses_submap_exec_xii by fast+ then have "fmlookup (snd a ++ s1) v = fmlookup (snd a ++ s2) v" by auto also have " … = fmlookup (fst a') v" using A by simp finally have "fmlookup (snd a ++ s1) v = fmlookup (fst a') v" by simp } then show ?thesis using B I by presburger next case False then have I: "v ∈ fmdom' s2" using A unfolding fmap_add_ltr_def fmdom'_add by blast { from P_1 have "fmlookup ?f v ≠ None" by (meson fmdom'_notI) moreover from false have "fmlookup ?g v = None" by (simp add: fmdom'_notD) ultimately have "fmlookup ?f v ≠ fmlookup ?g v" by simp } moreover { { from P_1_1(2) have "state_succ s2 a = snd a ++ s2" unfolding state_succ_def by simp moreover from ‹state_succ s2 a = snd a ++ s2› have "fmlookup (state_succ s2 a) v = fmlookup s2 v" using as_needed_asses_submap_exec_xii'[OF False I] by simp ultimately have "fmlookup ?f v = fmlookup (action_needed_asses a' s2) v" unfolding action_needed_asses_def action_needed_vars_def by (simp add: A I) } note I = this moreover { from P_1_1(3) have "state_succ s1 a = snd a ++ s1" unfolding state_succ_def by simp moreover from ‹state_succ s1 a = snd a ++ s1› False have "fmlookup (state_succ s1 a) v = fmlookup s1 v" unfolding fmap_add_ltr_def using fmlookup_add by (simp add: fmdom'_alt_def fmember.rep_eq) ultimately have "fmlookup ?g v = fmlookup (action_needed_asses a' s1) v" unfolding action_needed_asses_def action_needed_vars_def using FDOM_state_succ_subset by auto } moreover { have "v ∈ fmdom' (action_needed_asses a' s2)" proof - have "v ∈ fmdom' s2 ∪ fmdom' (snd a)" by (metis (no_types) A FDOM_state_succ_subset P_1_1(2) state_succ_def subsetCE) then show ?thesis by (simp add: A False as_needed_asses_submap_exec_iii as_needed_asses_submap_exec_xii') qed then have " fmlookup (action_needed_asses a' s2) v = fmlookup (action_needed_asses a' s1) v" using i as_needed_asses_submap_exec_ix[of "action_needed_asses a' s2" "action_needed_asses a' s1"] by blast } ultimately have "fmlookup ?f v = fmlookup ?g v" by simp } ultimately show ?thesis by simp qed qed next assume P2: "v ∈ fmdom' (action_needed_asses a' (snd a ++ s2))" "fst a ⊆⇩_{f}s2" "¬ fst a ⊆⇩_{f}s1" then show " fmlookup (action_needed_asses a' (snd a ++ s2)) v = fmlookup (action_needed_asses a' s1) v" proof - obtain aa :: "('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ 'a" where "∀x0 x1. (∃v2. v2 ∈ fmdom' x1 ∧ fmlookup x1 v2 ≠ fmlookup x0 v2) = (aa x0 x1 ∈ fmdom' x1 ∧ fmlookup x1 (aa x0 x1) ≠ fmlookup x0 (aa x0 x1))" by moura then have f1: "∀f fa. aa fa f ∈ fmdom' f ∧ fmlookup f (aa fa f) ≠ fmlookup fa (aa fa f) ∨ f ⊆⇩_{f}fa" by (meson as_needed_asses_submap_exec_vii) then have f2: "aa s1 (fst a) ∈ fmdom' (fst a) ∧ fmlookup (fst a) (aa s1 (fst a)) ≠ fmlookup s1 (aa s1 (fst a))" using P2(3) by blast then have "aa s1 (fst a) ∈ fmdom' s2" by (metis (full_types) P2(2) as_needed_asses_submap_exec_v) then have "aa s1 (fst a) ∈ fmdom' (action_needed_asses a s2)" using f2 by (simp add: P2(2) as_needed_asses_submap_exec_iii as_needed_asses_submap_exec_viii) then show ?thesis using f1 by (metis (no_types) Cons.prems(2) P2(3) as_needed_asses_submap_exec_vi elem) qed next assume P3: "v ∈ fmdom' (action_needed_asses a' s2)" "¬ fst a ⊆⇩_{f}s2" "fst a ⊆⇩_{f}s1" then show " fmlookup (action_needed_asses a' s2) v = fmlookup (action_needed_asses a' (snd a ++ s1)) v" using Cons.prems(1) submap_imp_state_succ_submap_a by blast next assume P4: "v ∈ fmdom' (action_needed_asses a' s2)" "¬ fst a ⊆⇩_{f}s2" "¬ fst a ⊆⇩_{f}s1" then show " fmlookup (action_needed_asses a' s2) v = fmlookup (action_needed_asses a' s1) v" by (simp add: Cons.prems(2) P as_needed_asses_submap_exec_ii insert) qed } then have a: "?f ⊆⇩_{f}?g" using as_needed_asses_submap_exec_ix by blast } note 2 = this then show ?case unfolding exec_plan.simps using Cons.IH[of "state_succ s1 a" "state_succ s2 a", OF 1] by blast qed simp ― ‹NOTE name shortened.› definition system_needed_vars where "system_needed_vars PROB s ≡ (⋃{action_needed_vars a s | a. a ∈ PROB})" ― ‹NOTE name shortened.› definition system_needed_asses where "system_needed_asses PROB s ≡ (fmrestrict_set (system_needed_vars PROB s) s)" lemma action_needed_vars_subset_sys_needed_vars_subset: assumes "(a ∈ PROB)" shows "(action_needed_vars a s ⊆ system_needed_vars PROB s)" using assms by (auto simp: system_needed_vars_def) (metis surjective_pairing) lemma action_needed_asses_submap_sys_needed_asses: assumes "(a ∈ PROB)" shows "(action_needed_asses a s ⊆⇩_{f}system_needed_asses PROB s)" proof - have "action_needed_asses a s = fmrestrict_set (action_needed_vars a s) s" unfolding action_needed_asses_def by simp then have "system_needed_asses PROB s = (fmrestrict_set (system_needed_vars PROB s) s)" unfolding system_needed_asses_def by simp then have 1: "action_needed_vars a s ⊆ system_needed_vars PROB s" unfolding action_needed_vars_subset_sys_needed_vars_subset using assms action_needed_vars_subset_sys_needed_vars_subset by fast { fix x assume P1: "x ∈ dom (fmlookup (fmrestrict_set (action_needed_vars a s) s))" then have a: "fmlookup (fmrestrict_set (action_needed_vars a s) s) x = fmlookup s x" by (auto simp: fmdom'_restrict_set_precise) then have "fmlookup (fmrestrict_set (system_needed_vars PROB s) s) x = fmlookup s x" using 1 contra_subsetD by fastforce then have " fmlookup (fmrestrict_set (action_needed_vars a s) s) x = fmlookup (fmrestrict_set (system_needed_vars PROB s) s) x " using a by argo } then have " fmlookup (fmrestrict_set (action_needed_vars a s) s) ⊆⇩_{m}fmlookup (fmrestrict_set (system_needed_vars PROB s) s) " using map_le_def by blast then show "(action_needed_asses a s ⊆⇩_{f}system_needed_asses PROB s)" by (simp add: fmsubset.rep_eq action_needed_asses_def system_needed_asses_def) qed lemma system_needed_asses_include_action_needed_asses_1: assumes "(a ∈ PROB)" shows "(action_needed_vars a (fmrestrict_set (system_needed_vars PROB s) s) = action_needed_vars a s)" proof - let ?A="{v ∈ fmdom' (fmrestrict_set (system_needed_vars PROB s) s). v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup (fmrestrict_set (system_needed_vars PROB s) s) v}" let ?B="{v ∈ fmdom' s. v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup s v}" { fix v assume "v ∈ ?A" then have i: "v ∈ fmdom' (fmrestrict_set (system_needed_vars PROB s) s)" "v ∈ fmdom' (fst a)" "fmlookup (fst a) v = fmlookup (fmrestrict_set (system_needed_vars PROB s) s) v" by blast+ then have "v ∈ fmdom' s" by (simp add: fmdom'_restrict_set_precise) moreover have "fmlookup (fst a) v = fmlookup s v" using i(2, 3) fmdom'_notI by force ultimately have "v ∈ ?B" using i by blast } then have 1: "?A ⊆ ?B" by blast { fix v assume P: "v ∈ ?B" then have ii: "v ∈ fmdom' s" "v ∈ fmdom' (fst a)" "fmlookup (fst a) v = fmlookup s v" by blast+ moreover { have "∃s'. v ∈ s' ∧ (∃a. (s' = action_needed_vars a s) ∧ a ∈ PROB)" unfolding action_needed_vars_def using assms P action_needed_vars_def by metis then obtain s' where α: "v ∈ s'" "(∃a. (s' = action_needed_vars a s) ∧ a ∈ PROB)" by blast moreover obtain a' where "s' = action_needed_vars a' s" "a' ∈ PROB" using α by blast ultimately have "v ∈ fmdom' (fmrestrict_set (system_needed_vars PROB s) s)" unfolding fmdom'_restrict_set_precise using action_needed_vars_subset_sys_needed_vars_subset ii(1) by blast } note iii = this moreover have "fmlookup (fst a) v = fmlookup (fmrestrict_set (system_needed_vars PROB s) s) v" using ii(3) iii fmdom'_notI by force ultimately have "v ∈ ?A" by blast } then have "?B ⊆ ?A" by blast then show ?thesis unfolding action_needed_vars_def using 1 by blast qed ― ‹NOTE added lemma.› ― ‹TODO refactor (proven elsewhere?).› lemma system_needed_asses_include_action_needed_asses_i: fixes A B f assumes "A ⊆ B" shows "fmrestrict_set A (fmrestrict_set B f) = fmrestrict_set A f" proof - { let ?f'="fmrestrict_set A f" let ?f''="fmrestrict_set A (fmrestrict_set B f)" assume C: "?f'' ≠ ?f'" then obtain v where 1: "fmlookup ?f'' v ≠ fmlookup ?f' v" by (meson fmap_ext) then have False proof (cases "v ∈ A") case True have "fmlookup ?f'' v = fmlookup (fmrestrict_set B f) v" using True fmlookup_restrict_set by simp moreover have "fmlookup (fmrestrict_set B f) v = fmlookup ?f' v" using True assms(1) by auto ultimately show ?thesis using 1 by argo next case False then have "fmlookup ?f' v = None" "fmlookup ?f'' v = None" using fmlookup_restrict_set by auto+ then show ?thesis using 1 by argo qed } then show ?thesis by blast qed lemma system_needed_asses_include_action_needed_asses: assumes "(a ∈ PROB)" shows "(action_needed_asses a (system_needed_asses PROB s) = action_needed_asses a s)" proof - { have " action_needed_vars a s ⊆ system_needed_vars PROB s" using action_needed_vars_subset_sys_needed_vars_subset[OF assms] by simp then have " fmrestrict_set (action_needed_vars a s) (fmrestrict_set (system_needed_vars PROB s) s) = fmrestrict_set (action_needed_vars a s) s" using system_needed_asses_include_action_needed_asses_i by fast } moreover { have "action_needed_vars a (fmrestrict_set (system_needed_vars PROB s) s) = action_needed_vars a s" using system_needed_asses_include_action_needed_asses_1[OF assms] by simp then have "fmrestrict_set (action_needed_vars a (fmrestrict_set (system_needed_vars PROB s) s)) (fmrestrict_set (system_needed_vars PROB s) s) = fmrestrict_set (action_needed_vars a s) s ⟷ fmrestrict_set (action_needed_vars a s) (fmrestrict_set (system_needed_vars PROB s) s) = fmrestrict_set (action_needed_vars a s) s" by simp } ultimately show ?thesis unfolding action_needed_asses_def system_needed_asses_def by simp qed lemma system_needed_asses_submap: "system_needed_asses PROB s ⊆⇩_{f}s" proof - { fix x assume P: "x∈ dom (fmlookup (system_needed_asses PROB s))" then have "system_needed_asses PROB s = (fmrestrict_set (system_needed_vars PROB s) s)" by (simp add: system_needed_asses_def) then have "fmlookup (system_needed_asses PROB s) x = fmlookup s x" using P by (auto simp: fmdom'_restrict_set_precise) } then have "fmlookup (system_needed_asses PROB s) ⊆⇩_{m}fmlookup s" using map_le_def by blast then show ?thesis using fmsubset.rep_eq by fast qed lemma as_works_from_system_needed_asses: assumes "(as ∈ valid_plans PROB)" shows "(exec_plan (system_needed_asses PROB s) as ⊆⇩_{f}exec_plan s as)" using assms by (metis action_needed_asses_def as_needed_asses_submap_exec fmsubset_restrict_set_mono system_needed_asses_def system_needed_asses_include_action_needed_asses system_needed_asses_include_action_needed_asses_1 system_needed_asses_submap valid_plan_mems ) end

# Theory ActionSeqProcess

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