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