(* (C) Copyright Andreas Viktor Hess, DTU, 2015-2018 All Rights Reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: - Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. - Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. - Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (* Title: LazyIntruder.thy Author: Andreas Viktor Hess, DTU *) section {* Theory: The Lazy Intruder *} theory LazyIntruder imports StrandsAndConstraints IntruderDeduction InfiniteChains begin context intruder_model begin subsection {* Definition of the lazy intruder *} inductive_set LI_rel:: "((('fun,'var) strand \ (('fun,'var) subst)) \ ('fun,'var) strand \ (('fun,'var) subst)) set" and LI_rel' (infix "\" 50) and LI_rel_trancl (infix "\\<^sup>+" 50) and LI_rel_rtrancl (infix "\\<^sup>*" 50) where "A \ B \ (A,B) \ LI_rel" | "A \\<^sup>+ B \ (A,B) \ LI_rel\<^sup>+" | "A \\<^sup>* B \ (A,B) \ LI_rel\<^sup>*" | Compose: "\simple S; length X = arity f; public f\ \ (S@snd\Fun f X\#S',\) \ (S@(map Send X)@S',\)" | Unify: "\simple S; Fun f Y \ ik\<^sub>s\<^sub>t S; Some \ = mgu (Fun f X) (Fun f Y)\ \ (S@snd\Fun f X\#S',\) \ ((S@S') \\<^sub>s\<^sub>t \,\ \\<^sub>s \)" | Equality: "\simple S; Some \ = mgu t t'\ \ (S@t \ t'#S',\) \ ((S@S') \\<^sub>s\<^sub>t \,\ \\<^sub>s \)" lemma LI_rel_simps: assumes "simple S\<^sub>p\<^sub>r\<^sub>e" shows "(S\<^sub>p\<^sub>r\<^sub>e@snd\Fun f X\#S\<^sub>s\<^sub>u\<^sub>f, \) \ (S', \') \ (S' = S\<^sub>p\<^sub>r\<^sub>e@map Send X@S\<^sub>s\<^sub>u\<^sub>f \ \' = \ \ length X = arity f \ public f) \ (\\ Y. S' = (S\<^sub>p\<^sub>r\<^sub>e@S\<^sub>s\<^sub>u\<^sub>f \\<^sub>s\<^sub>t \) \ \' = \ \\<^sub>s \ \ Fun f Y \ ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \ Some \ = mgu (Fun f X) (Fun f Y))" (is "?A = (?B \ ?C)") proof assume ?A thus "?B \ ?C" proof cases case (Compose S'\<^sub>p\<^sub>r\<^sub>e X' f' S'\<^sub>s\<^sub>u\<^sub>f) hence "S'\<^sub>p\<^sub>r\<^sub>e = S\<^sub>p\<^sub>r\<^sub>e" "X' = X" "f' = f" "S'\<^sub>s\<^sub>u\<^sub>f = S\<^sub>s\<^sub>u\<^sub>f" using simple_fun_prefix_unique[OF Compose(1,4)] \simple S\<^sub>p\<^sub>r\<^sub>e\ by metis+ thus "?B \ ?C" using Compose by metis next case (Unify S'\<^sub>p\<^sub>r\<^sub>e f' Y \ X' S'\<^sub>s\<^sub>u\<^sub>f) hence "S'\<^sub>p\<^sub>r\<^sub>e = S\<^sub>p\<^sub>r\<^sub>e" "X' = X" "f' = f" "S'\<^sub>s\<^sub>u\<^sub>f = S\<^sub>s\<^sub>u\<^sub>f" using simple_fun_prefix_unique[OF Unify(1,4)] \simple S\<^sub>p\<^sub>r\<^sub>e\ by metis+ thus "?B \ ?C" using Unify by metis next case (Equality S'\<^sub>p\<^sub>r\<^sub>e \ t t' S'\<^sub>s\<^sub>u\<^sub>f) then obtain S where S: "S\<^sub>p\<^sub>r\<^sub>e = S'\<^sub>p\<^sub>r\<^sub>e@S \ S'\<^sub>p\<^sub>r\<^sub>e = S\<^sub>p\<^sub>r\<^sub>e@S" using append_eq_append_conv2 by blast have "S\<^sub>p\<^sub>r\<^sub>e \ S'\<^sub>p\<^sub>r\<^sub>e" using Equality by auto hence "S \ []" using S by auto then obtain x S' where "S = x#S'" by (metis hd_Cons_tl) hence "x = t \ t' \ x = snd\Fun f X\" "S\<^sub>p\<^sub>r\<^sub>e = S'\<^sub>p\<^sub>r\<^sub>e@x#S' \ S'\<^sub>p\<^sub>r\<^sub>e = S\<^sub>p\<^sub>r\<^sub>e@x#S'" using S Equality(1) by auto hence False using \simple S\<^sub>p\<^sub>r\<^sub>e\ \simple S'\<^sub>p\<^sub>r\<^sub>e\ S by auto thus "?B \ ?C" by rule qed next assume "?B \ ?C" thus ?A using \simple S\<^sub>p\<^sub>r\<^sub>e\ by (blast intro: Compose Unify) qed lemma LI_rel_lhs_unfold: assumes "(S\<^sub>1,\\<^sub>1) \ (S\<^sub>2,\\<^sub>2)" shows "(\S f X S'. simple S \ S\<^sub>1 = S@snd\Fun f X\#S') \ (\S t t' S'. simple S \ S\<^sub>1 = S@t \ t'#S')" using assms by (induct rule: LI_rel.induct) auto subsection {* Theorem: The lazy intruder terminates *} lemma LI_compose_measure_lt: "((S@(map Send X)@S',\\<^sub>1), (S@snd\Fun f X\#S',\\<^sub>2)) \ measure\<^sub>s\<^sub>t" using strand_FV_card_map_fun_eq[of S f X S'] strand_size_map_fun_lt(2)[of X f] by simp lemma LI_unify_measure_lt: assumes "Some \ = mgu (Fun f X) t" "FV t \ FV\<^sub>s\<^sub>t S" shows "(((S@S') \\<^sub>s\<^sub>t \,\\<^sub>1), (S@snd\Fun f X\#S',\\<^sub>2)) \ measure\<^sub>s\<^sub>t" proof (cases "\ = Var") assume "\ = Var" hence "(S@S') \\<^sub>s\<^sub>t \ = S@S'" by blast thus ?thesis using strand_FV_card_rm_fun_le[of S S' f X] by auto next assume "\ \ Var" then obtain v where "v \ FV (Fun f X) \ FV t" "elim \ v" using mgu_eliminates[OF assms(1)[symmetric]] by metis hence v_in: "v \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using assms(2) by auto have "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV (Fun f X) \ FV\<^sub>s\<^sub>t S" using assms(2) mgu_vars_bounded[OF assms(1)[symmetric]] by auto hence img_bound: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" by auto have finite_FV: "finite (FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))" by auto have "v \ FV\<^sub>s\<^sub>t ((S@snd\Fun f X\#S') \\<^sub>s\<^sub>t \)" using strand_FV_subst_subset_if_elim[OF \elim \ v\] v_in by metis hence v_not_in: "v \ FV\<^sub>s\<^sub>t ((S@S') \\<^sub>s\<^sub>t \)" by auto have "FV\<^sub>s\<^sub>t ((S@S') \\<^sub>s\<^sub>t \) \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using strand_subst_FV_bounded_if_img_bounded[OF img_bound] by simp hence "FV\<^sub>s\<^sub>t ((S@S') \\<^sub>s\<^sub>t \) \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using v_in v_not_in by blast hence "card (FV\<^sub>s\<^sub>t ((S@S') \\<^sub>s\<^sub>t \)) < card (FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S'))" using psubset_card_mono[OF finite_FV] by simp thus ?thesis by auto qed lemma LI_equality_measure_lt: assumes "Some \ = mgu t t'" shows "(((S@S') \\<^sub>s\<^sub>t \,\\<^sub>1), (S@t \ t'#S',\\<^sub>2)) \ measure\<^sub>s\<^sub>t" proof (cases "\ = Var") assume "\ = Var" hence "(S@S') \\<^sub>s\<^sub>t \ = S@S'" by blast thus ?thesis using strand_FV_card_rm_eq_le[of S S' t t'] by auto next assume "\ \ Var" then obtain v where "v \ FV t \ FV t'" "elim \ v" using mgu_eliminates[OF assms(1)[symmetric]] by metis hence v_in: "v \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" using assms by auto have "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV t \ FV t' \ FV\<^sub>s\<^sub>t S" using assms mgu_vars_bounded[OF assms(1)[symmetric]] by auto hence img_bound: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" by auto have finite_FV: "finite (FV\<^sub>s\<^sub>t (S@t \ t'#S'))" by auto have "v \ FV\<^sub>s\<^sub>t ((S@t \ t'#S') \\<^sub>s\<^sub>t \)" using strand_FV_subst_subset_if_elim[OF \elim \ v\] v_in by metis hence v_not_in: "v \ FV\<^sub>s\<^sub>t ((S@S') \\<^sub>s\<^sub>t \)" by auto have "FV\<^sub>s\<^sub>t ((S@S') \\<^sub>s\<^sub>t \) \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" using strand_subst_FV_bounded_if_img_bounded[OF img_bound] by simp hence "FV\<^sub>s\<^sub>t ((S@S') \\<^sub>s\<^sub>t \) \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" using v_in v_not_in by blast hence "card (FV\<^sub>s\<^sub>t ((S@S') \\<^sub>s\<^sub>t \)) < card (FV\<^sub>s\<^sub>t (S@t \ t'#S'))" using psubset_card_mono[OF finite_FV] by simp thus ?thesis by auto qed lemma LI_in_measure: "(S\<^sub>1,\\<^sub>1) \ (S\<^sub>2,\\<^sub>2) \ ((S\<^sub>2,\\<^sub>2),(S\<^sub>1,\\<^sub>1)) \ measure\<^sub>s\<^sub>t" proof (induction rule: LI_rel.induct) case (Compose S X f S' \) thus ?case using LI_compose_measure_lt[of S X S'] by metis next case (Unify S f Y \ X S' \) hence "FV (Fun f Y) \ FV\<^sub>s\<^sub>t S" using FV_snd_rcv_strand_subset(2)[of S] by fastforce thus ?case using LI_unify_measure_lt[OF Unify.hyps(3), of S S'] by metis qed (metis LI_equality_measure_lt) lemma LI_in_measure_trans: "(S\<^sub>1,\\<^sub>1) \\<^sup>+ (S\<^sub>2,\\<^sub>2) \ ((S\<^sub>2,\\<^sub>2),(S\<^sub>1,\\<^sub>1)) \ measure\<^sub>s\<^sub>t" apply (induction rule: trancl.induct, metis surjective_pairing LI_in_measure) by (metis (no_types, lifting) surjective_pairing LI_in_measure measure\<^sub>s\<^sub>t_trans trans_def) lemma LI_converse_wellfounded_trans: "wf ((LI_rel\<^sup>+)\)" proof - have "(LI_rel\<^sup>+)\ \ measure\<^sub>s\<^sub>t" using LI_in_measure_trans by auto thus ?thesis using measure\<^sub>s\<^sub>t_wellfounded wf_subset by metis qed lemma LI_acyclic_trans: "acyclic (LI_rel\<^sup>+)" using wf_acyclic[OF LI_converse_wellfounded_trans] acyclic_converse by metis lemma LI_acyclic: "acyclic LI_rel" using LI_acyclic_trans acyclic_subset by (simp add: acyclic_def) lemma LI_no_infinite_chain: "\(\f. \i. f i \\<^sup>+ f (Suc i))" proof - have "\(\f. \i. (f (Suc i), f i) \ (LI_rel\<^sup>+)\)" using wf_iff_no_infinite_down_chain LI_converse_wellfounded_trans by metis thus ?thesis by simp qed lemma LI_unify_finite: assumes "finite M" shows "finite {((S@snd\Fun f X\#S',\), ((S@S') \\<^sub>s\<^sub>t \,\ \\<^sub>s \)) | \ Y. simple S \ Fun f Y \ M \ Some \ = mgu (Fun f X) (Fun f Y)}" using assms proof (induction M rule: finite_induct) case (insert m M) thus ?case proof (cases m) case (Fun g Z) let ?a = "\\. ((S@snd\Fun f X\#S',\), ((S@S') \\<^sub>s\<^sub>t \,\ \\<^sub>s \))" let ?A = "\B. {?a \ | \ Y. simple S \ Fun f Y \ B \ Some \ = mgu (Fun f X) (Fun f Y)}" have "?A (insert m M) = (?A M) \ (?A {m})" by auto moreover have "finite (?A {m})" proof (cases "\\. Some \ = mgu (Fun f X) (Fun g Z)") case True then obtain \ where \: "Some \ = mgu (Fun f X) (Fun g Z)" by blast have A_m_eq: "\\'. ?a \' \ ?A {m} \ ?a \ = ?a \'" proof - fix \' assume "?a \' \ ?A {m}" hence "\\. Some \ = mgu (Fun f X) (Fun g Z) \ ?a \ = ?a \'" using \m = Fun g Z\ by auto thus "?a \ = ?a \'" by (metis \ option.inject) qed have "?A {m} = {} \ ?A {m} = {?a \}" proof (cases "simple S \ ?A {m} \ {}") case True hence "simple S" "?A {m} \ {}" by meson+ hence "?A {m} = {?a \ | \. Some \ = mgu (Fun f X) (Fun g Z)}" using \m = Fun g Z\ by auto hence "?a \ \ ?A {m}" using \ by auto show ?thesis proof (rule ccontr) assume "\(?A {m} = {} \ ?A {m} = {?a \})" then obtain B where B: "?A {m} = insert (?a \) B" "?a \ \ B" "B \ {}" using \?A {m} \ {}\ \?a \ \ ?A {m}\ by (metis (no_types, lifting) Set.set_insert) then obtain b where b: "?a \ \ b" "b \ B" by (metis (no_types, lifting) ex_in_conv) then obtain \' where \': "b = ?a \'" using B(1) by blast moreover have "?a \' \ ?A {m}" using B(1) b(2) \' by auto hence "?a \ = ?a \'" by (blast dest!: A_m_eq) ultimately show False using b(1) by simp qed qed auto thus ?thesis by (metis (no_types, lifting) finite.emptyI finite_insert) next case False hence "?A {m} = {}" using \m = Fun g Z\ by blast thus ?thesis by (metis finite.emptyI) qed ultimately show ?thesis using insert.IH by auto qed simp qed fastforce subsection {* Lemma: The lazy intruder preserves well-formedness *} lemma LI_preserves_trm_wf: assumes "(S,\) \\<^sup>* (S',\')" "\x \ set S. wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)" shows "\x \ set S'. wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)" proof - { fix S \ S' \' assume "(S,\) \ (S',\')" "\x \ set S. wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)" hence "\x \ set S'. wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)" proof (induction rule: LI_rel.induct) case (Compose S X f S' \) hence "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" and *: "\x. x \ set S \ wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)" "\x. x \ set S' \ wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)" by auto hence "\x. x \ set X \ wf\<^sub>t\<^sub>r\<^sub>m x" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto hence "\x. x \ set (map Send X) \ wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto thus ?case using * by auto next case (Unify S f Y \ X S' \) have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)" using Unify.prems(1) Unify.hyps(2) wf_trm_subterm[of _ "Fun f Y"] by (simp, force) hence "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" using mgu_wf_trm[OF Unify.hyps(3)[symmetric]] by simp { fix s assume "s \ set (S@S' \\<^sub>s\<^sub>t \)" hence "\s' \ set (S@S'). s = s' \\<^sub>s\<^sub>t\<^sub>p \ \ wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s') \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')" using Unify.prems(1) by auto moreover { fix s' assume "s = s' \\<^sub>s\<^sub>t\<^sub>p \" "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s')" "wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')" "s' \ set (S@S')" hence "trm\<^sub>s\<^sub>t\<^sub>p s = trm\<^sub>s\<^sub>t\<^sub>p s' \ (rm_vars (set (bvars\<^sub>s\<^sub>t\<^sub>p s')) \)" "trm_r\<^sub>s\<^sub>t\<^sub>p s = trm_r\<^sub>s\<^sub>t\<^sub>p s' \ (rm_vars (set (bvars\<^sub>s\<^sub>t\<^sub>p s')) \)" by (cases s'; auto)+ hence "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s)" "wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s)" by (simp_all add: wf_trm_subst \\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)\ \wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s')\ \wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')\) } ultimately have "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s) \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s)" by auto } thus ?case by simp next case (Equality S \ t t' S' \) hence "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" by simp_all hence "\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)" using mgu_wf_trm[OF Equality.hyps(2)[symmetric]] by simp { fix s assume "s \ set (S@S' \\<^sub>s\<^sub>t \)" hence "\s' \ set (S@S'). s = s' \\<^sub>s\<^sub>t\<^sub>p \ \ wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s') \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')" using Equality.prems(1) by auto moreover { fix s' assume "s = s' \\<^sub>s\<^sub>t\<^sub>p \" "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s')" "wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')" "s' \ set (S@S')" hence "trm\<^sub>s\<^sub>t\<^sub>p s = trm\<^sub>s\<^sub>t\<^sub>p s' \ (rm_vars (set (bvars\<^sub>s\<^sub>t\<^sub>p s')) \)" "trm_r\<^sub>s\<^sub>t\<^sub>p s = trm_r\<^sub>s\<^sub>t\<^sub>p s' \ (rm_vars (set (bvars\<^sub>s\<^sub>t\<^sub>p s')) \)" by (cases s'; auto)+ hence "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s)" "wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s)" by (simp_all add: wf_trm_subst \\v. wf\<^sub>t\<^sub>r\<^sub>m (\ v)\ \wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s')\ \wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')\) } ultimately have "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s) \ wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s)" by auto } thus ?case by simp qed } with assms show ?thesis by (induction rule: rtrancl_induct2) metis+ qed lemma LI_preserves_subst_wf_single: assumes "(S\<^sub>1,\\<^sub>1) \ (S\<^sub>2,\\<^sub>2)" "FV\<^sub>s\<^sub>t S\<^sub>1 \ bvars\<^sub>s\<^sub>t S\<^sub>1 = {}" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>1" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>1 \ vars\<^sub>s\<^sub>t S\<^sub>1 = {}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>1 \ bvars\<^sub>s\<^sub>t S\<^sub>1 = {}" shows "FV\<^sub>s\<^sub>t S\<^sub>2 \ bvars\<^sub>s\<^sub>t S\<^sub>2 = {}" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>2" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>2 \ vars\<^sub>s\<^sub>t S\<^sub>2 = {}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>2 \ bvars\<^sub>s\<^sub>t S\<^sub>2 = {}" using assms proof (induction rule: LI_rel.induct) case (Compose S X f S' \) { case 1 thus ?case using vars_st_snd_map by auto } { case 2 thus ?case using vars_st_snd_map by auto } { case 3 thus ?case using vars_st_snd_map by auto } { case 4 thus ?case using vars_st_snd_map by auto } next case (Unify S f Y \ X S' \) hence "FV (Fun f Y) \ FV\<^sub>s\<^sub>t S" using FV_subset_if_in_strand_ik'[OF trpI] by blast hence *: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] by fastforce have "FV\<^sub>s\<^sub>t (S@S') \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" "vars\<^sub>s\<^sub>t (S@S') \ vars\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" by auto hence **: "FV\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" "vars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) \ vars\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using strand_subst_FV_union_bound[of "S@S'" \] strand_subst_vars_union_bound[of "S@S'" \] * by blast+ have "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by (fact mgu_gives_wellformed_subst[OF Unify.hyps(3)[symmetric]]) { case 1 have "bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = bvars\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using bvars_subst_ident[of "S@S'" \] by auto thus ?case using 1 ** by blast } { case 2 hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using * by blast+ thus ?case by (metis wf_subst_compose[OF \wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ \wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\]) } { case 3 hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" using ** by blast moreover have "\v. v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ v \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using * by blast hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" using mgu_eliminates_dom[OF Unify.hyps(3)[symmetric], THEN strand_FV_subst_subset_if_elim, of _ "S@snd\Fun f X\#S'"] unfolding elim_def by auto moreover have "bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = bvars\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using bvars_subst_ident[of "S@S'" \] by auto hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" using 3(1) * by blast ultimately show ?case using ** * subst_dom_comp_subset[of \ \] vars\<^sub>s\<^sub>t_is_FV\<^sub>s\<^sub>t_bvars\<^sub>s\<^sub>t[of "S@S' \\<^sub>s\<^sub>t \"] by blast } { case 4 have ***: "bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = bvars\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using bvars_subst_ident[of "S@S'" \] by auto hence "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" using 4(1) * by blast thus ?case using subst_img_comp_subset[of \ \] 4(4) *** by blast } next case (Equality S \ t t' S' \) hence *: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] by fastforce have "FV\<^sub>s\<^sub>t (S@S') \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" "vars\<^sub>s\<^sub>t (S@S') \ vars\<^sub>s\<^sub>t (S@t \ t'#S')" by auto hence **: "FV\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" "vars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) \ vars\<^sub>s\<^sub>t (S@t \ t'#S')" using strand_subst_FV_union_bound[of "S@S'" \] strand_subst_vars_union_bound[of "S@S'" \] * by blast+ have "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \" by (fact mgu_gives_wellformed_subst[OF Equality.hyps(2)[symmetric]]) { case 1 have "bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = bvars\<^sub>s\<^sub>t (S@t \ t'#S')" using bvars_subst_ident[of "S@S'" \] by auto thus ?case using 1 ** by blast } { case 2 hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using * by blast+ thus ?case by (metis wf_subst_compose[OF \wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\ \wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\]) } { case 3 hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" using ** by blast moreover have "\v. v \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ v \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" using * by blast hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" using mgu_eliminates_dom[OF Equality.hyps(2)[symmetric], THEN strand_FV_subst_subset_if_elim, of _ "S@t \ t'#S'"] unfolding elim_def by auto moreover have "bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = bvars\<^sub>s\<^sub>t (S@t \ t'#S')" using bvars_subst_ident[of "S@S'" \] by auto hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" using 3(1) * by blast ultimately show ?case using ** * subst_dom_comp_subset[of \ \] vars\<^sub>s\<^sub>t_is_FV\<^sub>s\<^sub>t_bvars\<^sub>s\<^sub>t[of "S@S' \\<^sub>s\<^sub>t \"] by blast } { case 4 have ***: "bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = bvars\<^sub>s\<^sub>t (S@t \ t'#S')" using bvars_subst_ident[of "S@S'" \] by auto hence "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" using 4(1) * by blast thus ?case using subst_img_comp_subset[of \ \] 4(4) *** by blast } qed lemma LI_preserves_subst_wf: assumes "(S\<^sub>1,\\<^sub>1) \\<^sup>* (S\<^sub>2,\\<^sub>2)" "FV\<^sub>s\<^sub>t S\<^sub>1 \ bvars\<^sub>s\<^sub>t S\<^sub>1 = {}" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>1" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>1 \ vars\<^sub>s\<^sub>t S\<^sub>1 = {}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>1 \ bvars\<^sub>s\<^sub>t S\<^sub>1 = {}" shows "FV\<^sub>s\<^sub>t S\<^sub>2 \ bvars\<^sub>s\<^sub>t S\<^sub>2 = {}" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>2" and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>2 \ vars\<^sub>s\<^sub>t S\<^sub>2 = {}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \\<^sub>2 \ bvars\<^sub>s\<^sub>t S\<^sub>2 = {}" using assms proof (induction S\<^sub>2 \\<^sub>2 rule: rtrancl_induct2) case (step S\<^sub>i \\<^sub>i S\<^sub>j \\<^sub>j) { case 1 thus ?case using LI_preserves_subst_wf_single[OF \(S\<^sub>i,\\<^sub>i) \ (S\<^sub>j,\\<^sub>j)\] step.IH by metis } { case 2 thus ?case using LI_preserves_subst_wf_single[OF \(S\<^sub>i,\\<^sub>i) \ (S\<^sub>j,\\<^sub>j)\] step.IH by metis } { case 3 thus ?case using LI_preserves_subst_wf_single[OF \(S\<^sub>i,\\<^sub>i) \ (S\<^sub>j,\\<^sub>j)\] step.IH by metis } { case 4 thus ?case using LI_preserves_subst_wf_single[OF \(S\<^sub>i,\\<^sub>i) \ (S\<^sub>j,\\<^sub>j)\] step.IH by metis } qed metis lemma LI_preserves_wellformedness: "\(S\<^sub>1,\\<^sub>1) \\<^sup>* (S\<^sub>2,\\<^sub>2); wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1\ \ wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>2 \\<^sub>2" proof - assume "(S\<^sub>1,\\<^sub>1) \\<^sup>* (S\<^sub>2,\\<^sub>2)" have *: "\S\<^sub>i \\<^sub>i S\<^sub>j \\<^sub>j. \(S\<^sub>i, \\<^sub>i) \ (S\<^sub>j, \\<^sub>j); wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>i \\<^sub>i\ \ wf\<^sub>s\<^sub>t {} S\<^sub>j" proof - fix S\<^sub>i \\<^sub>i S\<^sub>j \\<^sub>j show "\(S\<^sub>i,\\<^sub>i) \ (S\<^sub>j,\\<^sub>j); wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>i \\<^sub>i\ \ wf\<^sub>s\<^sub>t {} S\<^sub>j" proof (induction rule: LI_rel.induct) case (Unify S f Y \ X S' \) have "FV (Fun f X) \ FV (Fun f Y) \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using Unify.hyps(2) by force hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] by (metis subset_trans) hence "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ bvars\<^sub>s\<^sub>t (S@snd\Fun f X\#S') = {}" using Unify.prems unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by blast thus ?case using wf_unify[OF _ trpI[OF Unify.hyps(2)] MGU_is_Unifier[OF mgu_gives_MGU], of "{}", OF _ Unify.hyps(3)[symmetric], of S'] Unify.prems(1) by auto next case (Equality S \ t t' S' \) have "FV t \ FV t' \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" using Equality.hyps(2) by force hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] by (metis subset_trans) hence "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ bvars\<^sub>s\<^sub>t (S@t \ t'#S') = {}" using Equality.prems unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by blast thus ?case using wf_equality[OF _ Equality.hyps(2)[symmetric], of "{}" S S'] Equality.prems(1) by auto qed (metis wf_send_compose wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def) qed from \(S\<^sub>1,\\<^sub>1) \\<^sup>* (S\<^sub>2,\\<^sub>2)\ show "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1 \ wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>2 \\<^sub>2" proof (induction rule: rtrancl_induct2) case (step S\<^sub>i \\<^sub>i S\<^sub>j \\<^sub>j) thus ?case using LI_preserves_subst_wf_single[OF \(S\<^sub>i,\\<^sub>i) \ (S\<^sub>j,\\<^sub>j)\] *[OF \(S\<^sub>i,\\<^sub>i) \ (S\<^sub>j,\\<^sub>j)\] by force qed simp qed subsection {* Theorem: Soundness of the lazy intruder *} lemma LI_soundness_single: assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1" "(S\<^sub>1,\\<^sub>1) \ (S\<^sub>2,\\<^sub>2)" "\ \\<^sub>c \S\<^sub>2,\\<^sub>2\" shows "\ \\<^sub>c \S\<^sub>1,\\<^sub>1\" using assms(2,1,3) proof (induction rule: LI_rel.induct) case (Compose S X f S' \) hence *: "\{}; S\\<^sub>c \" "\ik\<^sub>s\<^sub>t S; map Send X\\<^sub>c \" "\ik\<^sub>s\<^sub>t S; S'\\<^sub>c \" unfolding constr_sem_c_def by force+ have "ik\<^sub>s\<^sub>t S \set \ \\<^sub>c Fun f X \ \" using *(2) Compose.hyps(2) ComposeC[OF _ Compose.hyps(3), of "map (\x. x \ \) X"] unfolding subst_compose_def by force thus "\ \\<^sub>c \S@snd\Fun f X\#S',\\" using *(1,3) \\ \\<^sub>c \S@map Send X@S',\\\ by auto next case (Unify S f Y \ X S' \) have "(\ \\<^sub>s \) supports \" "\{}; S@S' \\<^sub>s\<^sub>t \\\<^sub>c \" using Unify.prems(2) unfolding constr_sem_c_def by metis+ then obtain \ where \: "\ \\<^sub>s \ \\<^sub>s \ = \" unfolding subst_compose_def by auto have \fun_id: "Fun f Y \ \ = Fun f Y" "Fun f X \ \ = Fun f X" using Unify.prems(1) trm_subst_ident[of "Fun f Y" \] FV_subset_if_in_strand_ik[of "Fun f Y" S] Unify.hyps(2) trpI[of "Fun f Y" "ik\<^sub>s\<^sub>t S"] FV_snd_rcv_strand_subset(2)[of S] strand_vars_split(1)[of S "snd\Fun f X\#S'"] unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def apply blast using Unify.prems(1) trm_subst_ident[of "Fun f X" \] unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by fastforce hence \\_disj: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using trm_subst_disj mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] apply (blast,blast) using Unify.prems(1) unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by blast hence \\_support: "\ supports \" "\ supports \" by (simp_all add: subst_support_comp_split[OF \(\ \\<^sub>s \) supports \\]) have "FV (Fun f X) \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" "FV (Fun f Y) \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using Unify.hyps(2) by force+ hence \_vars_bound: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@snd\Fun f X\#S')" using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] by blast have "\ik\<^sub>s\<^sub>t S; [snd\Fun f X\]\\<^sub>c \" proof - from Unify.hyps(2) have "Fun f Y \ \ \ ik\<^sub>s\<^sub>t S \set \" by blast hence "Fun f Y \ \ \ ik\<^sub>s\<^sub>t S \set \" using trp_subst_apply_subset_set[of \ "ik\<^sub>s\<^sub>t S"] by blast moreover have "Unifier \ (Fun f X) (Fun f Y)" by (fact MGU_is_Unifier[OF mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]]) ultimately have "Fun f X \ \ \ ik\<^sub>s\<^sub>t S \set \" using \ by (metis \fun_id subst_comp) thus ?thesis by simp qed have "\{}; S\\<^sub>c \" "\ik\<^sub>s\<^sub>t S; S'\\<^sub>c \" proof - have "(S@S' \\<^sub>s\<^sub>t \) \\<^sub>s\<^sub>t \ = S@S' \\<^sub>s\<^sub>t \" "(S@S') \\<^sub>s\<^sub>t \ = S@S'" proof - have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>s\<^sub>t (S@S') = {}" using Unify.prems(1) by auto hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" using \\_disj(2) strand_subst_vars_union_bound[of "S@S'" \] by blast thus "(S@S' \\<^sub>s\<^sub>t \) \\<^sub>s\<^sub>t \ = S@S' \\<^sub>s\<^sub>t \" "(S@S') \\<^sub>s\<^sub>t \ = S@S'" using strand_subst_comp \dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>s\<^sub>t (S@S') = {}\ by (blast,blast) qed moreover have "Idem \" by (fact mgu_gives_Idem[OF Unify.hyps(3)[symmetric]]) moreover have "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ bvars\<^sub>s\<^sub>t (S@S') = {}" "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ bvars\<^sub>s\<^sub>t (S@S') = {}" using wf_constr_bvars_disj[OF Unify.prems(1)] wf_constr_bvars_disj'[OF Unify.prems(1) \_vars_bound] by auto ultimately have "\{}; S@S'\\<^sub>c \" using \\{}; S@S' \\<^sub>s\<^sub>t \\\<^sub>c \\ \ strand_sem_subst[of \ "S@S' \\<^sub>s\<^sub>t \" "{}" "\ \\<^sub>s \"] strand_sem_subst'[of \ "S@S'" "{}" "\ \\<^sub>s \"] strand_sem_subst_Idem[of \ "S@S'" "{}" \] unfolding constr_sem_c_def by (metis subst_all_empty comp_assoc) thus "\{}; S\\<^sub>c \" "\ik\<^sub>s\<^sub>t S; S'\\<^sub>c \" by auto qed show "\ \\<^sub>c \S@snd\Fun f X\#S',\\" using \\_support(1) \\ik\<^sub>s\<^sub>t S; [snd\Fun f X\]\\<^sub>c \\ \\{}; S\\<^sub>c \\ \\ik\<^sub>s\<^sub>t S; S'\\<^sub>c \\ by auto next case (Equality S \ t t' S' \) have "(\ \\<^sub>s \) supports \" "\{}; S@S' \\<^sub>s\<^sub>t \\\<^sub>c \" using Equality.prems(2) unfolding constr_sem_c_def by metis+ then obtain \ where \: "\ \\<^sub>s \ \\<^sub>s \ = \" unfolding subst_compose_def by auto have "FV t \ vars\<^sub>s\<^sub>t (S@t \ t'#S')" "FV t' \ vars\<^sub>s\<^sub>t (S@t \ t'#S')" by auto moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>s\<^sub>t (S@t \ t'#S') = {}" using Equality.prems(1) unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by auto ultimately have \fun_id: "t \ \ = t" "t' \ \ = t'" using trm_subst_ident[of t \] trm_subst_ident[of t' \] by auto hence \\_disj: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ = {}" using trm_subst_disj mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] apply (blast,blast) using Equality.prems(1) unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by blast hence \\_support: "\ supports \" "\ supports \" by (simp_all add: subst_support_comp_split[OF \(\ \\<^sub>s \) supports \\]) have "FV t \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" "FV t' \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" by auto hence \_vars_bound: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@t \ t'#S')" using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] by blast have "\ik\<^sub>s\<^sub>t S; [t \ t']\\<^sub>c \" proof - have "t \ \ = t' \ \" using MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]] by metis hence "t \ (\ \\<^sub>s \) = t' \ (\ \\<^sub>s \)" by (metis \fun_id subst_comp) hence "t \ \ = t' \ \" by (metis \ subst_comp) thus ?thesis by simp qed have "\{}; S\\<^sub>c \" "\ik\<^sub>s\<^sub>t S; S'\\<^sub>c \" proof - have "(S@S' \\<^sub>s\<^sub>t \) \\<^sub>s\<^sub>t \ = S@S' \\<^sub>s\<^sub>t \" "(S@S') \\<^sub>s\<^sub>t \ = S@S'" proof - have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>s\<^sub>t (S@S') = {}" using Equality.prems(1) by auto hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@S') = {}" by blast hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" using \\_disj(2) strand_subst_FV_union_bound[of "S@S'" \] by blast thus "(S@S' \\<^sub>s\<^sub>t \) \\<^sub>s\<^sub>t \ = S@S' \\<^sub>s\<^sub>t \" "(S@S') \\<^sub>s\<^sub>t \ = S@S'" using strand_subst_comp \dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ vars\<^sub>s\<^sub>t (S@S') = {}\ by (blast,blast) qed moreover have "Idem \" by (fact mgu_gives_Idem[OF Equality.hyps(2)[symmetric]]) moreover have "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ bvars\<^sub>s\<^sub>t (S@S') = {}" "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ bvars\<^sub>s\<^sub>t (S@S' \\<^sub>s\<^sub>t \) = {}" "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \) \ bvars\<^sub>s\<^sub>t (S@S') = {}" using wf_constr_bvars_disj[OF Equality.prems(1)] wf_constr_bvars_disj'[OF Equality.prems(1) \_vars_bound] by auto ultimately have "\{}; S@S'\\<^sub>c \" using \\{}; S@S' \\<^sub>s\<^sub>t \\\<^sub>c \\ \ strand_sem_subst[of \ "S@S' \\<^sub>s\<^sub>t \" "{}" "\ \\<^sub>s \"] strand_sem_subst'[of \ "S@S'" "{}" "\ \\<^sub>s \"] strand_sem_subst_Idem[of \ "S@S'" "{}" \] unfolding constr_sem_c_def by (metis subst_all_empty comp_assoc) thus "\{}; S\\<^sub>c \" "\ik\<^sub>s\<^sub>t S; S'\\<^sub>c \" by auto qed show "\ \\<^sub>c \S@t \ t'#S',\\" using \\_support(1) \\ik\<^sub>s\<^sub>t S; [t \ t']\\<^sub>c \\ \\{}; S\\<^sub>c \\ \\ik\<^sub>s\<^sub>t S; S'\\<^sub>c \\ by auto qed theorem LI_soundness: assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1" "(S\<^sub>1,\\<^sub>1) \\<^sup>* (S\<^sub>2,\\<^sub>2)" "\ \\<^sub>c \S\<^sub>2, \\<^sub>2\" shows "\ \\<^sub>c \S\<^sub>1, \\<^sub>1\" using assms(2,1,3) proof (induction S\<^sub>2 \\<^sub>2 rule: rtrancl_induct2) case (step S\<^sub>i \\<^sub>i S\<^sub>j \\<^sub>j) thus ?case using LI_preserves_wellformedness[OF \(S\<^sub>1, \\<^sub>1) \\<^sup>* (S\<^sub>i, \\<^sub>i)\ \wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1\] LI_soundness_single[OF _ \(S\<^sub>i, \\<^sub>i) \ (S\<^sub>j, \\<^sub>j)\ \\ \\<^sub>c \S\<^sub>j, \\<^sub>j\\] step.IH[OF \wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1\] by metis qed metis subsection {* Theorem: Completeness of the lazy intruder *} lemma LI_completeness_single: assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1" "\ \\<^sub>c \S\<^sub>1, \\<^sub>1\" "\simple S\<^sub>1" shows "\S\<^sub>2 \\<^sub>2. (S\<^sub>1,\\<^sub>1) \ (S\<^sub>2,\\<^sub>2) \ (\ \\<^sub>c \S\<^sub>2, \\<^sub>2\)" using not_simple_elim[OF \\simple S\<^sub>1\] proof (* In this case S\<^sub>1 isn't simple because it contains an equality constraint, so we can simply proceed with the reduction by computing the MGU for the equation *) assume "\S' S'' t t'. S\<^sub>1 = S'@t \ t'#S'' \ simple S'" then obtain S t t' S' where S\<^sub>1: "S\<^sub>1 = S@t \ t'#S'" "simple S" by moura hence *: "wf\<^sub>s\<^sub>t {} S" "\ \\<^sub>c \S, \\<^sub>1\" "\\<^sub>1 supports \" "t \ \ = t' \ \" "FV t' \ FV\<^sub>s\<^sub>t S" using \\ \\<^sub>c \S\<^sub>1, \\<^sub>1\\ \wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1\ wf_eq_FV[of "{}" S t t' S'] FV_snd_rcv_strand_subset(5)[of S] by auto from * have "Unifier \ t t'" by simp then obtain \ where \: "Some \ = mgu t t'" "Idem \" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV t \ FV t'" using mgu_always_unifies mgu_gives_Idem mgu_vars_bounded by metis+ have "\ \\<^sub>\ \" using mgu_gives_MGU[OF \(1)[symmetric]] by (metis \Unifier \ t t'\) hence "\ supports \" using subst_support_if_mgt_Idem[OF _ \(2)] by metis hence "(\\<^sub>1 \\<^sub>s \) supports \" using subst_support_comp \\\<^sub>1 supports \\ by metis have "\{}; S@S' \\<^sub>s\<^sub>t \\\<^sub>c \" proof - have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t S\<^sub>1" using \(3) S\<^sub>1(1) by auto hence "\{}; S\<^sub>1 \\<^sub>s\<^sub>t \\\<^sub>c \" using \Idem \\ \\ \\<^sub>\ \\ \\ \\<^sub>c \S\<^sub>1, \\<^sub>1\\ strand_sem_subst wf_constr_bvars_disj'(1)[OF assms(1)] unfolding Idem_def constr_sem_c_def by (metis (no_types) subst_all_empty comp_assoc) thus "\{}; S@S' \\<^sub>s\<^sub>t \\\<^sub>c \" using S\<^sub>1(1) by force qed moreover have "(S@t \ t'#S', \\<^sub>1) \ (S@S' \\<^sub>s\<^sub>t \, \\<^sub>1 \\<^sub>s \)" using LI_rel.Equality[OF \simple S\ \(1)] S\<^sub>1 by metis ultimately show ?thesis using S\<^sub>1(1) \(\\<^sub>1 \\<^sub>s \) supports \\ by auto next (* In this case S\<^sub>1 isn't simple because it contains a deduction constraint for a composed term, so we must look at how this composed term is derived under the interpretation \ *) assume "\S' S'' f X. S\<^sub>1 = S'@snd\Fun f X\#S'' \ simple S'" with assms obtain S f X S' where S\<^sub>1: "S\<^sub>1 = S@snd\Fun f X\#S'" "simple S" using not_simple_elim[OF \\simple S\<^sub>1\] by metis hence "wf\<^sub>s\<^sub>t {} S" "\ \\<^sub>c \S, \\<^sub>1\" "\\<^sub>1 supports \" using \\ \\<^sub>c \S\<^sub>1, \\<^sub>1\\ \wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1\ by auto (* Lemma for a common subcase *) have fun_sat: "(\x. x \ set X \ ik\<^sub>s\<^sub>t S \set \ \\<^sub>c x \ \) \ \ \\<^sub>c \S@(map Send X)@S', \\<^sub>1\" proof - assume "\x. x \ set X \ ik\<^sub>s\<^sub>t S \set \ \\<^sub>c x \ \" hence "\x. x \ set X \ \ik\<^sub>s\<^sub>t S; [snd\x\]\\<^sub>c \" by simp hence "\ik\<^sub>s\<^sub>t S; map Send X\\<^sub>c \" using \\ \\<^sub>c \S\<^sub>1, \\<^sub>1\\ strand_sem_snd_map by metis moreover have "\ik\<^sub>s\<^sub>t (S@(map Send X)); S'\\<^sub>c \" using \\ \\<^sub>c \S\<^sub>1, \\<^sub>1\\ S\<^sub>1 by auto ultimately show ?thesis using \\ \\<^sub>c \S, \\<^sub>1\\ \\ \\<^sub>c \S\<^sub>1, \\<^sub>1\\ by force qed from S\<^sub>1 \\ \\<^sub>c \S\<^sub>1, \\<^sub>1\\ have "ik\<^sub>s\<^sub>t S \set \ \\<^sub>c Fun f X \ \" by auto thus ?thesis proof cases (* Case 1: \(f(X)) has been derived using the AxiomC rule.*) case AxiomC hence ex_t: "\t. t \ ik\<^sub>s\<^sub>t S \ Fun f X \ \ = t \ \" by auto show ?thesis proof (cases "\Y. Fun f Y \ ik\<^sub>s\<^sub>t S \ Fun f X \ \ \ Fun f Y \ \") (* Case 1.1: f(X) is equal to a variable in the intruder knowledge under \. Hence there must exists a deduction constraint in the simple prefix of the constraint in which this variable occurs/"is sent" for the first time. Since this variable itself cannot have been derived from the AxiomC rule (because it must be equal under the interpretation to f(X), which is by assumption not in the intruder knowledge under \) it must be the case that we can derive it using the ComposeC rule. Hence we can apply the Compose rule of the lazy intruder to f(X). *) case True have "\v. Var v \ ik\<^sub>s\<^sub>t S \ Fun f X \ \ = \ v" proof - obtain t where "t \ ik\<^sub>s\<^sub>t S" "Fun f X \ \ = t \ \" using ex_t by moura thus ?thesis using \\Y. Fun f Y \ ik\<^sub>s\<^sub>t S \ Fun f X \ \ \ Fun f Y \ \\ by (cases t) auto qed hence "\v \ vars2\<^sub>s\<^sub>t S. Fun f X \ \ = \ v" by (meson vars_subset_if_in_strand_ik2 trpI contra_subsetD trp_refl trp_var_is_FV) then obtain v S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f where S: "S = S\<^sub>p\<^sub>r\<^sub>e@snd\Var v\#S\<^sub>s\<^sub>u\<^sub>f" "Fun f X \ \ = \ v" "\(\w \ vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. Fun f X \ \ = \ w)" using \wf\<^sub>s\<^sub>t {} S\ wf_simple_strand_first_snd_var_split[OF _ \simple S\, of "Fun f X" \] by auto hence "\w. Var w \ ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \ \ v \ Var w \ \" by force moreover have "\Y. Fun f Y \ ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \ Fun f X \ \ \ Fun f Y \ \" using \\Y. Fun f Y \ ik\<^sub>s\<^sub>t S \ Fun f X \ \ \ Fun f Y \ \\ S(1) by (meson contra_subsetD ik_append_subset(1)) hence "\g Y. Fun g Y \ ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \ \ v \ Fun g Y \ \" using S(2) by simp ultimately have "\t \ ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. \ v \ t \ \" by (metis term.exhaust) hence "\ v \ (ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e) \set \" by auto have "ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \set \ \\<^sub>c \ v" using S\<^sub>1(1) S(1) \\ \\<^sub>c \S\<^sub>1, \\<^sub>1\\ by auto hence "ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \set \ \\<^sub>c Fun f X \ \" using \Fun f X \ \ = \ v\ by metis hence "length X = arity f" "public f" "\x. x \ set X \ ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \set \ \\<^sub>c x \ \" using \Fun f X \ \ = \ v\ \\ v \ ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \set \\ intruder_synth.simps[of "ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \set \" "\ v"] by auto hence *: "\x. x \ set X \ ik\<^sub>s\<^sub>t S \set \ \\<^sub>c x \ \" using S(1) by (auto intro: ideduct_synth_mono) hence "\ \\<^sub>c \S@(map Send X)@S', \\<^sub>1\" by (metis fun_sat) moreover have "(S@snd\Fun f X\#S', \\<^sub>1) \ (S@map Send X@S', \\<^sub>1)" by (metis LI_rel.Compose[OF \simple S\ \length X = arity f\ \public f\]) ultimately show ?thesis using S\<^sub>1 by auto next (* Case 1.2: \(f(X)) can be derived from an interpreted composed term in the intruder knowledge. Use the Unify rule on this composed term to further reduce the constraint. *) case False then obtain Y where t: "Fun f Y \ ik\<^sub>s\<^sub>t S" "Fun f X \ \ = Fun f Y \ \" by auto hence "FV (Fun f Y) \ FV\<^sub>s\<^sub>t S\<^sub>1" using S\<^sub>1(1) FV_subset_if_in_strand_ik'[OF trpI[OF t(1)]] FV_snd_rcv_strand_subset(2)[of S] by auto from t have "Unifier \ (Fun f X) (Fun f Y)" by simp then obtain \ where \: "Some \ = mgu (Fun f X) (Fun f Y)" "Idem \" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV (Fun f X) \ FV (Fun f Y)" using mgu_always_unifies mgu_gives_Idem mgu_vars_bounded by metis+ have "\ \\<^sub>\ \" using mgu_gives_MGU[OF \(1)[symmetric]] by (metis \Unifier \ (Fun f X) (Fun f Y)\) hence "\ supports \" using subst_support_if_mgt_Idem[OF _ \(2)] by metis hence "(\\<^sub>1 \\<^sub>s \) supports \" using subst_support_comp \\\<^sub>1 supports \\ by metis have "\{}; S@S' \\<^sub>s\<^sub>t \\\<^sub>c \" proof - have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \ \ FV\<^sub>s\<^sub>t S\<^sub>1" using \(3) S\<^sub>1(1) \FV (Fun f Y) \ FV\<^sub>s\<^sub>t S\<^sub>1\ by fastforce hence "\{}; S\<^sub>1 \\<^sub>s\<^sub>t \\\<^sub>c \" using \Idem \\ \\ \\<^sub>\ \\ \\ \\<^sub>c \S\<^sub>1, \\<^sub>1\\ strand_sem_subst wf_constr_bvars_disj'(1)[OF assms(1)] unfolding Idem_def constr_sem_c_def by (metis (no_types) subst_all_empty comp_assoc) thus "\{}; S@S' \\<^sub>s\<^sub>t \\\<^sub>c \" using S\<^sub>1(1) by force qed moreover have "(S@snd\Fun f X\#S', \\<^sub>1) \ (S@S' \\<^sub>s\<^sub>t \, \\<^sub>1 \\<^sub>s \)" using LI_rel.Unify[OF \simple S\ t(1) \(1)] S\<^sub>1 by metis ultimately show ?thesis using S\<^sub>1(1) \(\\<^sub>1 \\<^sub>s \) supports \\ by auto qed next (* Case 2: \(f(X)) has been derived using the ComposeC rule. Simply use the Compose rule of the lazy intruder to proceed with the reduction. *) case (ComposeC Y g) hence "f = g" "length X = arity f" "public f" and "\x. x \ set X \ ik\<^sub>s\<^sub>t S \set \ \\<^sub>c x \ \" by auto hence "\ \\<^sub>c \S@(map Send X)@S', \\<^sub>1\" using fun_sat by metis moreover have "(S\<^sub>1, \\<^sub>1) \ (S@(map Send X)@S', \\<^sub>1)" using S\<^sub>1 LI_rel.Compose[OF \simple S\ \length X = arity f\ \public f\] by metis ultimately show ?thesis by metis qed qed theorem LI_completeness: assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1" "\ \\<^sub>c \S\<^sub>1, \\<^sub>1\" shows "\S\<^sub>2 \\<^sub>2. (S\<^sub>1,\\<^sub>1) \\<^sup>* (S\<^sub>2,\\<^sub>2) \ simple S\<^sub>2 \ (\ \\<^sub>c \S\<^sub>2, \\<^sub>2\)" proof - let ?Stuck = "\S\<^sub>2 \\<^sub>2. \(\S\<^sub>3 \\<^sub>3. (S\<^sub>2,\\<^sub>2) \ (S\<^sub>3,\\<^sub>3) \ (\ \\<^sub>c \S\<^sub>3, \\<^sub>3\))" let ?SATConfs = "{(x,(S\<^sub>2,\\<^sub>2)) \ reachable LI_rel (S\<^sub>1,\\<^sub>1). \ \\<^sub>c \S\<^sub>2, \\<^sub>2\}" have simple_if_stuck: "\S\<^sub>2 \\<^sub>2. \(S\<^sub>1,\\<^sub>1) \\<^sup>+ (S\<^sub>2,\\<^sub>2); \ \\<^sub>c \S\<^sub>2, \\<^sub>2\; ?Stuck S\<^sub>2 \\<^sub>2\ \ simple S\<^sub>2" proof - fix S\<^sub>2 \\<^sub>2 assume "(S\<^sub>1,\\<^sub>1) \\<^sup>+ (S\<^sub>2,\\<^sub>2)" "\ \\<^sub>c \S\<^sub>2, \\<^sub>2\" "?Stuck S\<^sub>2 \\<^sub>2" show "simple S\<^sub>2" apply (rule ccontr) using \?Stuck S\<^sub>2 \\<^sub>2\ LI_completeness_single[OF _ \\ \\<^sub>c \S\<^sub>2, \\<^sub>2\\] trancl_into_rtrancl[OF \(S\<^sub>1,\\<^sub>1) \\<^sup>+ (S\<^sub>2,\\<^sub>2)\] LI_preserves_wellformedness[OF _ \wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1\, of S\<^sub>2 \\<^sub>2] by metis qed show ?thesis proof (cases "simple S\<^sub>1") case False hence "\S\<^sub>2 \\<^sub>2. (S\<^sub>1,\\<^sub>1) \ (S\<^sub>2,\\<^sub>2) \ (\ \\<^sub>c \S\<^sub>2, \\<^sub>2\)" by (metis LI_completeness_single[OF assms]) hence base: "\b. ((S\<^sub>1,\\<^sub>1),b) \ ?SATConfs" using reachable.Base[of "(S\<^sub>1,\\<^sub>1)" _ LI_rel] by blast { fix S \ S' \' assume "((S,\),(S',\')) \ ?SATConfs\<^sup>+" hence "(S,\) \\<^sup>+ (S',\') \ (\ \\<^sub>c \S', \'\)" by (induct rule: trancl_induct2) auto } hence *: "\S \ S' \'. ((S,\),(S',\')) \ ?SATConfs\<^sup>+ \ (S,\) \\<^sup>+ (S',\') \ (\ \\<^sub>c \S', \'\)" by blast have "\S\<^sub>2 \\<^sub>2. ((S\<^sub>1,\\<^sub>1),(S\<^sub>2,\\<^sub>2)) \ ?SATConfs\<^sup>+ \ ?Stuck S\<^sub>2 \\<^sub>2" proof (rule ccontr) assume "\(\S\<^sub>2 \\<^sub>2. ((S\<^sub>1,\\<^sub>1),(S\<^sub>2,\\<^sub>2)) \ ?SATConfs\<^sup>+ \ ?Stuck S\<^sub>2 \\<^sub>2)" hence sat_not_stuck: "\S\<^sub>2 \\<^sub>2. ((S\<^sub>1,\\<^sub>1),(S\<^sub>2,\\<^sub>2)) \ ?SATConfs\<^sup>+ \ \?Stuck S\<^sub>2 \\<^sub>2" by blast { fix a assume a: "((S\<^sub>1,\\<^sub>1),a) \ ?SATConfs\<^sup>+" { fix S\<^sub>2 \\<^sub>2 assume in_sat: "((S\<^sub>1,\\<^sub>1),(S\<^sub>2,\\<^sub>2)) \ ?SATConfs\<^sup>+" hence "\S\<^sub>3 \\<^sub>3. ((S\<^sub>2,\\<^sub>2),(S\<^sub>3,\\<^sub>3)) \ ?SATConfs" using * sat_not_stuck by blast hence "\S\<^sub>3 \\<^sub>3. (S\<^sub>2,\\<^sub>2) \ (S\<^sub>3,\\<^sub>3) \ ((S\<^sub>1,\\<^sub>1),(S\<^sub>3,\\<^sub>3)) \ ?SATConfs\<^sup>+" using trancl_into_trancl[OF in_sat] by blast } hence "\a. ((S\<^sub>1,\\<^sub>1),a) \ ?SATConfs\<^sup>+ \ \b. a \ b \ ((S\<^sub>1,\\<^sub>1),b) \ ?SATConfs\<^sup>+" by auto hence "\S' \'. a \ (S',\') \ ((S\<^sub>1,\\<^sub>1),(S',\')) \ ?SATConfs\<^sup>+" using a by auto then obtain S' \' where S'\': "a \ (S',\')" "((S\<^sub>1,\\<^sub>1),(S',\')) \ ?SATConfs\<^sup>+" by auto hence "\ \\<^sub>c \S', \'\" using * by blast moreover have "(S\<^sub>1, \\<^sub>1) \\<^sup>+ a" using a trancl_mono by blast ultimately have "(a,(S',\')) \ ?SATConfs" using S'\'(1) by fastforce hence "\b. (a,b) \ ?SATConfs \ ((S\<^sub>1,\\<^sub>1),b) \ ?SATConfs\<^sup>+" using S'\'(2) by blast } hence "\a. ((S\<^sub>1,\\<^sub>1),a) \ ?SATConfs\<^sup>+ \ (\b. (a,b) \ ?SATConfs)" by blast hence "\f. \i::nat. (f i, f (Suc i)) \ ?SATConfs" using infinite_chain_intro'[OF base] by blast moreover have "?SATConfs \ LI_rel\<^sup>+" by auto hence "\(\f. \i::nat. (f i, f (Suc i)) \ ?SATConfs)" using LI_no_infinite_chain infinite_chain_mono by blast ultimately show False by auto qed hence "\S\<^sub>2 \\<^sub>2. (S\<^sub>1, \\<^sub>1) \\<^sup>+ (S\<^sub>2, \\<^sub>2) \ simple S\<^sub>2 \ (\ \\<^sub>c \S\<^sub>2, \\<^sub>2\)" using simple_if_stuck * by blast thus ?thesis by (meson trancl_into_rtrancl) qed (blast intro: \\ \\<^sub>c \S\<^sub>1, \\<^sub>1\\) qed subsection {* Soundness and completeness as a single theorem *} corollary LI_soundness_and_completeness: assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1" shows "\ \\<^sub>c \S\<^sub>1, \\<^sub>1\ \ (\S\<^sub>2 \\<^sub>2. (S\<^sub>1,\\<^sub>1) \\<^sup>* (S\<^sub>2,\\<^sub>2) \ simple S\<^sub>2 \ (\ \\<^sub>c \S\<^sub>2, \\<^sub>2\))" using LI_soundness[OF \wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1\] LI_completeness[OF \wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \\<^sub>1\] by metis end end