1 (*<*)

     2 theory My_list_prefix

     3 imports List_Prefix

     4 begin

     5 (*>*)

     6 

     7 (* cmp:: 1:complete equal; 2:less; 3:greater; 4: len equal,but ele no equal *)

     8 fun cmp :: "'a list \<Rightarrow> 'a list \<Rightarrow> nat"

     9 where

    10   "cmp [] [] = 1" |                   

    11   "cmp [] (e#es) = 2" |

    12   "cmp (e#es) [] = 3" |

    13   "cmp (e#es) (a#as) = (let r = cmp es as in 

    14                             if (e = a) then r else 4)"

    15 

    16 (* list_com:: fetch the same ele of the same left order into a new list*) 

    17 fun list_com :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

    18 where 

    19   "list_com []  ys = []" |

    20   "list_com xs [] = []" |

    21   "list_com (x#xs) (y#ys) = (if x = y then x#(list_com xs ys) else [])"

    22 

    23 (* list_com_rev:: by the right order of list_com *)

    24 definition list_com_rev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "\<bullet>" 50)

    25 where

    26   "xs \<bullet> ys \<equiv> rev (list_com (rev xs) (rev ys))"

    27 

    28 (* list_diff:: list substract, once different return tailer *)

    29 fun list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

    30 where

    31   "list_diff []  xs = []" |

    32   "list_diff (x#xs) [] = x#xs" |

    33   "list_diff (x#xs) (y#ys) = (if x = y then list_diff xs ys else (x#xs))"

    34 

    35 (* list_diff_rev:: list substract with rev order*)

    36 definition list_diff_rev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "\<setminus>" 51)

    37 where

    38    "xs \<setminus> ys \<equiv> rev (list_diff (rev xs) (rev ys))"

    39 

    40 (* xs <= ys:: \<exists>zs. ys = xs @ zs *)

    41 (* no_junior:: xs is ys' tail,or equal *)

    42 definition no_junior  :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<preceq>" 50)

    43 where

    44   "xs \<preceq> ys \<equiv> rev xs \<le> rev ys"

    45 

    46 (* < :: xs <= ys \<and> xs \<noteq> ys *)

    47 (* is_ancestor:: xs is ys' tail, but no equal  *)

    48 definition is_ancestor :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<prec>" 50)

    49 where

    50   "xs \<prec> ys \<equiv> rev xs < rev ys"

    51 

    52 lemma list_com_diff [simp]: "(list_com xs  ys) @ (list_diff xs  ys) = xs" (is "?P xs ys")

    53   by (rule_tac P = ?P in cmp.induct, simp+)

    54 

    55 lemma list_com_diff_rev [simp]: "(xs \<setminus> ys) @ (xs \<bullet> ys) = xs"

    56   apply (simp only:list_com_rev_def list_diff_rev_def)

    57   by (fold rev_append, simp)

    58 

    59 lemma list_com_commute: "list_com xs ys = list_com ys xs" (is "?P xs ys")

    60   by (rule_tac P = ?P in cmp.induct, simp+)

    61 

    62 lemma list_com_ido: "xs \<le> ys \<longrightarrow> list_com xs ys = xs" (is "?P xs ys")

    63   by (rule_tac P = ?P in cmp.induct, auto+)

    64   

    65 lemma list_com_rev_ido [simp]: "xs \<preceq> ys \<Longrightarrow> xs \<bullet> ys = xs"

    66   by (cut_tac list_com_ido, auto simp: no_junior_def list_com_rev_def)

    67 

    68 lemma list_com_rev_commute [iff]: "(xs \<bullet> ys) = (ys \<bullet> xs)"

    69   by (simp only:list_com_rev_def list_com_commute)

    70 

    71 lemma list_com_rev_ido1 [simp]: "xs \<preceq> ys \<Longrightarrow> ys \<bullet> xs = xs"

    72   by simp

    73 

    74 lemma list_diff_le: "(list_diff xs ys = []) = (xs \<le> ys)" (is "?P xs ys")

    75   by (rule_tac P = ?P in cmp.induct, simp+)

    76   

    77 

    78 lemma list_diff_rev_le: "(xs \<setminus> ys = []) = (xs \<preceq> ys)"

    79   by (auto simp:list_diff_rev_def no_junior_def list_diff_le)

    80 

    81 lemma list_diff_lt: "(list_diff xs ys = [] \<and> list_diff ys xs \<noteq> []) = (xs < ys)" (is "?P xs ys")

    82   by (rule_tac P = ?P in cmp.induct, simp+)

    83 

    84 lemma list_diff_rev_lt: "(xs \<setminus> ys = [] \<and> ys \<setminus> xs \<noteq> []) = (xs \<prec> ys)"

    85   by (auto simp: list_diff_rev_def list_diff_lt is_ancestor_def)

    86 

    87 

    88 (* xs diff ys result not [] \<Longrightarrow> \<exists> e \<in> xs. a \<in> ys. e \<noteq> a *)

    89 lemma list_diff_neq: 

    90   "\<forall> e es a as. list_diff xs ys = (e#es) \<and> list_diff ys xs = (a#as) \<longrightarrow> e \<noteq> a" (is "?P xs ys")

    91   by (rule_tac P = ?P in cmp.induct, simp+)

    92 

    93 lemma list_diff_rev_neq_pre: "\<forall> e es a as. xs \<setminus> ys = rev (e#es) \<and> ys \<setminus> xs = rev (a#as) \<longrightarrow> e \<noteq> a"

    94   apply (simp only:list_diff_rev_def, clarify)

    95   apply (insert list_diff_neq, atomize)

    96   by (erule_tac x = "rev xs" in allE, erule_tac x = "rev ys" in allE, blast)

    97 

    98 lemma list_diff_rev_neq: "\<forall> e es a as. xs \<setminus> ys = es @ [e] \<and> ys \<setminus> xs = as @ [a] \<longrightarrow> e \<noteq> a"

    99   apply (rule_tac allI)+

   100   apply (insert list_diff_rev_neq_pre, atomize)

   101   apply (erule_tac x = "xs" in allE)

   102   apply (erule_tac x = "ys" in allE)

   103   apply (erule_tac x = "e" in allE)

   104   apply (erule_tac x = "rev es" in allE)

   105   apply (erule_tac x = "a" in allE)

   106   apply (erule_tac x = "rev as" in allE)

   107   by auto

   108 

   109 lemma list_com_self [simp]: "list_com zs zs = zs"

   110   by (induct_tac zs, simp+)

   111 

   112 lemma list_com_rev_self [simp]: "zs \<bullet> zs = zs"

   113   by (simp add:list_com_rev_def)

   114 

   115 lemma list_com_append [simp]: "(list_com (zs @ xs) (zs @ ys)) = (zs @ (list_com xs ys))"

   116   by (induct_tac zs, simp+)

   117 

   118 lemma list_inter_append [simp]: "((xs @ zs) \<bullet> (ys @ zs)) = ((xs \<bullet> ys) @ zs)"

   119   by (simp add:list_com_rev_def)

   120 

   121 lemma list_diff_djoin_pre: 

   122   "\<forall> e es a as. list_diff xs ys = e#es \<and>  list_diff ys xs = a#as \<longrightarrow> (\<forall> zs zs'. (list_diff (xs @ zs) (ys @ zs') = [e]@es@zs))" 

   123   (is "?P xs ys")

   124   by (rule_tac P = ?P in cmp.induct, simp+)

   125 

   126 lemma list_diff_djoin_rev_pre:

   127   "\<forall> e es a as. xs \<setminus> ys = rev (e#es) \<and>  ys \<setminus> xs = rev (a#as)  \<longrightarrow> (\<forall> zs zs'. ((zs @ xs) \<setminus> (zs' @ ys) = rev ([e]@es@rev zs)))"

   128   apply (simp only: list_diff_rev_def, clarify)

   129   apply (insert list_diff_djoin_pre, atomize)

   130   apply (erule_tac x = "rev xs" in allE)

   131   apply (erule_tac x = "rev ys" in allE)

   132   apply (erule_tac x = "e" in allE)

   133   apply (erule_tac x = "es" in allE)

   134   apply (erule_tac x = "a" in allE)

   135   apply (erule_tac x = "as" in allE)

   136   by simp

   137 

   138 lemma list_diff_djoin_rev:

   139   "xs \<setminus> ys = es @ [e] \<and> ys \<setminus> xs = as @ [a] \<Longrightarrow> zs @ xs \<setminus> zs' @ ys = zs @ es @ [e]"

   140   apply (insert list_diff_djoin_rev_pre [rule_format, simplified])

   141   apply (clarsimp, atomize)

   142   apply (erule_tac x = "xs" in allE)

   143   apply (erule_tac x = "ys" in allE)

   144   apply (erule_tac x = "rev es" in allE)

   145   apply (erule_tac x = "e" in allE)

   146   apply (erule_tac x = "rev as" in allE)

   147   apply (erule_tac x = "a" in allE)

   148   by auto

   149 

   150 lemmas list_diff_djoin_rev_simplified = conjI [THEN list_diff_djoin_rev, simp]

   151 

   152 lemmas list_diff_djoin = conjI [THEN list_diff_djoin_pre [rule_format], simp]

   153 

   154 lemma list_diff_ext_left [simp]: "(list_diff (zs @ xs) (zs @ ys) = (list_diff xs ys))"

   155   by (induct_tac zs, simp+)

   156 

   157 lemma list_diff_rev_ext_left [simp]: "((xs @ zs \<setminus> ys @ zs) = (xs \<setminus> ys))"

   158   by (auto simp: list_diff_rev_def)

   159 

   160 declare no_junior_def [simp]

   161 

   162 lemma no_juniorE: "\<lbrakk>xs \<preceq> ys; \<And> zs. ys = zs @ xs \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"

   163 proof -

   164   assume h: "xs \<preceq> ys"

   165     and h1: "\<And> zs. ys = zs @ xs \<Longrightarrow> R"

   166   show "R"

   167   proof -

   168     from h have "rev xs \<le> rev ys" by (simp)

   169     from this obtain zs where eq_rev: "rev ys = rev xs @ zs" by (auto simp:prefix_def)

   170     show R 

   171     proof(rule h1 [where zs = "rev zs"])

   172       from rev_rev_ident and eq_rev have "rev (rev (ys)) = rev zs @ rev (rev xs)"

   173 	by simp

   174       thus "ys = rev zs @ xs" by simp

   175     qed

   176   qed

   177 qed

   178 

   179 lemma no_juniorI: "\<lbrakk>ys = zs @ xs\<rbrakk> \<Longrightarrow> xs \<preceq> ys"

   180   by simp

   181 

   182 lemma no_junior_ident [simp]: "xs \<preceq> xs"

   183   by simp

   184 

   185 lemma no_junior_expand: "xs \<preceq> ys = ((xs \<prec> ys) \<or> xs = ys)"

   186   by (simp only:no_junior_def is_ancestor_def strict_prefix_def, blast)

   187 

   188 lemma no_junior_same_prefix: " e # \<tau> \<preceq> e' # \<tau>' \<Longrightarrow> \<tau> \<preceq> \<tau>'"

   189 apply (simp add:no_junior_def )

   190 apply (erule disjE, simp)

   191 apply (simp only:prefix_def)

   192 by (erule exE, rule_tac x = "[e] @ zs" in exI, auto)

   193 

   194 lemma no_junior_noteq: "\<lbrakk>\<tau> \<preceq> a # \<tau>'; \<tau> \<noteq> a # \<tau>'\<rbrakk> \<Longrightarrow> \<tau> \<preceq> \<tau>'"

   195 apply (erule no_juniorE)

   196 by (case_tac zs, simp+)

   197 

   198 lemma is_ancestor_app [simp]: "xs \<prec> ys \<Longrightarrow> xs \<prec> zs @ ys"

   199   by (auto simp:is_ancestor_def strict_prefix_def)

   200 

   201 lemma is_ancestor_cons [simp]: "xs \<prec> ys \<Longrightarrow> xs \<prec> a # ys"

   202   by (auto simp:is_ancestor_def strict_prefix_def)

   203 

   204 lemma no_junior_app [simp]: "xs \<preceq> ys \<Longrightarrow> xs \<preceq> zs @ ys"

   205   by simp

   206 

   207 lemma is_ancestor_no_junior [simp]: "xs \<prec> ys \<Longrightarrow> xs \<preceq> ys"

   208   by (simp add:is_ancestor_def)

   209 

   210 lemma is_ancestor_y [simp]: "ys \<prec> y#ys"

   211   by (simp add:is_ancestor_def strict_prefix_def)

   212 

   213 lemma no_junior_cons [simp]: "xs \<preceq> ys \<Longrightarrow> xs \<prec> (y#ys)"

   214   by (unfold no_junior_expand, auto)

   215 

   216 lemma no_junior_anti_sym: "\<lbrakk>xs \<preceq> ys; ys \<preceq> xs\<rbrakk> \<Longrightarrow> xs = ys"

   217   by simp

   218 

   219 declare no_junior_def [simp del]

   220 

   221 (* djoin:: xs and ys is not the other's tail, not equal either *)

   222 definition djoin :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<asymp>" 50)

   223 where

   224   "xs \<asymp> ys \<equiv> \<not> (xs \<preceq> ys \<or> ys \<preceq> xs)"

   225 

   226 (* dinj:: function f's returning list is not tailing when paras not equal *)

   227 definition dinj :: "('a \<Rightarrow> 'b list) \<Rightarrow> bool"

   228 where

   229   "dinj f \<equiv> (\<forall> a b. a \<noteq> b \<longrightarrow> f a \<asymp> f b)"

   230 

   231 

   232 (* list_cmp:: list comparison: one is other's prefix or no equal at some position *)

   233 lemma list_cmp: "xs \<le> ys \<or> ys \<le> xs \<or>  (\<exists> zs x y a b. xs = zs @ [a] @ x  \<and> ys = zs @ [b] @ y \<and> a \<noteq> b)"

   234 proof(cases "list_diff xs ys")

   235   assume " list_diff xs ys = []" with list_diff_le show ?thesis by blast

   236 next

   237   fix e es

   238   assume h: "list_diff xs ys = e # es"

   239   show ?thesis

   240   proof(cases "list_diff ys xs")

   241     assume " list_diff ys xs = []" with list_diff_le show ?thesis by blast

   242   next

   243     fix a as assume h1: "list_diff ys xs = (a # as)"

   244     have "xs = (list_com xs ys) @ [e] @ es \<and> ys = (list_com xs ys) @ [a] @ as \<and> e \<noteq> a"

   245       apply (simp, fold h1, fold h)

   246       apply (simp,subst list_com_commute, simp)

   247       apply (rule_tac list_diff_neq[rule_format])

   248       by (insert h1, insert h, blast)

   249     thus ?thesis by blast

   250   qed

   251 qed

   252 

   253 (* In fact, this is a case split *)

   254 lemma list_diff_ind: "\<lbrakk>list_diff xs ys = [] \<Longrightarrow> R; list_diff ys xs = [] \<Longrightarrow> R; 

   255                              \<And> e es a as. \<lbrakk>list_diff xs ys = e#es; list_diff ys xs = a#as; e \<noteq> a\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"

   256 proof -

   257   assume h1: "list_diff xs ys = [] \<Longrightarrow> R"

   258     and h2: "list_diff ys xs = [] \<Longrightarrow> R"

   259     and h3: "\<And> e es a as. \<lbrakk>list_diff xs ys = e#es; list_diff ys xs = a#as; e \<noteq> a\<rbrakk> \<Longrightarrow> R"

   260   show R

   261   proof(cases "list_diff xs ys")

   262     assume "list_diff xs ys = []" from h1 [OF this] show R .

   263   next

   264     fix e es

   265     assume he: "list_diff xs ys = e#es"

   266     show R

   267     proof(cases "list_diff ys xs")

   268       assume "list_diff ys xs = []" from h2 [OF this] show R .

   269     next

   270       fix a as

   271       assume ha: "list_diff ys xs = a#as" show R

   272       proof(rule h3 [OF he ha])

   273 	from list_diff_neq [rule_format, OF conjI [OF he ha ]]

   274 	show "e \<noteq> a" .

   275       qed

   276     qed

   277   qed

   278 qed

   279 

   280 lemma list_diff_rev_ind: 

   281   "\<lbrakk>xs \<setminus> ys = [] \<Longrightarrow> R; ys \<setminus> xs = [] \<Longrightarrow> R; \<And> e es a as. \<lbrakk>xs \<setminus> ys = es@[e]; ys \<setminus> xs = as@[a]; e \<noteq> a\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"

   282 proof -

   283   fix xs ys R

   284   assume h1: "xs \<setminus> ys = [] \<Longrightarrow> R"

   285     and h2: "ys \<setminus> xs = [] \<Longrightarrow> R"

   286     and h3: "\<And> e es a as. \<lbrakk>xs \<setminus> ys = es@[e]; ys \<setminus> xs = as@[a]; e \<noteq> a\<rbrakk> \<Longrightarrow> R"

   287   show R

   288   proof (rule list_diff_ind [where xs = "rev xs" and ys = "rev ys"])

   289     assume "list_diff (rev xs) (rev ys) = []" thus R by (auto intro:h1 simp:list_diff_rev_def)

   290   next

   291     assume "list_diff (rev ys) (rev xs) = []" thus R by (auto intro:h2 simp:list_diff_rev_def)

   292   next

   293     fix e es a as

   294     assume "list_diff (rev xs) (rev ys) = e # es"

   295       and "list_diff (rev ys) (rev xs) = a # as" 

   296       and " e \<noteq> a"

   297     thus R by (auto intro:h3 simp:list_diff_rev_def)

   298   qed

   299 qed

   300 

   301 lemma djoin_diff_iff: "(xs \<asymp> ys) = (\<exists> e es a as. list_diff (rev xs) (rev ys) = e#es \<and> list_diff (rev ys) (rev xs) = a#as \<and> a \<noteq> e)"

   302 proof (rule list_diff_ind [where xs = "rev xs" and ys = "rev ys"])

   303   assume "list_diff (rev xs) (rev ys) = []"

   304   hence "xs \<preceq> ys" by (unfold no_junior_def, simp add:list_diff_le)

   305   thus ?thesis 

   306     apply (auto simp:djoin_def no_junior_def)

   307     by (fold list_diff_le, simp)

   308 next

   309   assume "list_diff (rev ys) (rev xs) = []"

   310   hence "ys \<preceq> xs" by (unfold no_junior_def, simp add:list_diff_le)

   311   thus ?thesis 

   312     apply (auto simp:djoin_def no_junior_def)

   313     by (fold list_diff_le, simp)

   314 next

   315   fix e es a as

   316   assume he: "list_diff (rev xs) (rev ys) = e # es"

   317     and ha: "list_diff (rev ys) (rev xs) = a # as"

   318     and hn: "e \<noteq> a"

   319   show ?thesis

   320   proof

   321     from he ha hn

   322     show 

   323       "\<exists>e es a as. list_diff (rev xs) (rev ys) = e # es \<and> list_diff (rev ys) (rev xs) = a # as \<and> a \<noteq> e" 

   324       by blast

   325   next

   326     from he ha hn

   327     show "xs \<asymp> ys" 

   328       by (auto simp:djoin_def no_junior_def, fold list_diff_le, simp+)

   329   qed

   330 qed

   331 

   332 lemma djoin_diff_rev_iff: "(xs \<asymp> ys) = (\<exists> e es a as. xs \<setminus> ys = es@[e] \<and> ys \<setminus> xs = as@[a] \<and> a \<noteq> e)"

   333   apply (auto simp:djoin_diff_iff list_diff_rev_def)

   334   apply (rule_tac x = e in exI, safe)

   335   apply (rule_tac x = "rev es" in exI)

   336   apply (rule_tac injD[where f = rev], simp+)

   337   apply (rule_tac x = "a" in exI, safe)

   338   apply (rule_tac x = "rev as" in exI)

   339   apply (rule_tac injD[where f = rev], simp+)

   340   done

   341 

   342 lemma djoin_revE: "\<lbrakk>xs \<asymp> ys; \<And>e es a as. \<lbrakk>xs \<setminus> ys = es@[e]; ys \<setminus> xs = as@[a]; a \<noteq> e\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"

   343   by (unfold djoin_diff_rev_iff, blast)

   344 

   345 lemma djoin_append_left[simp, intro]: "xs \<asymp> ys \<Longrightarrow> (zs' @ xs) \<asymp> (zs @ ys)"

   346   by (auto simp:djoin_diff_iff intro:list_diff_djoin[simplified])

   347 

   348 lemma djoin_cons_left[simp]: "xs \<asymp> ys \<Longrightarrow> (e # xs) \<asymp> (a # ys)"

   349   by (drule_tac zs' = "[e]" and zs = "[a]" in djoin_append_left, simp)

   350 

   351 lemma djoin_simp_1 [simp]: "xs \<asymp> ys \<Longrightarrow> xs \<asymp> (zs @ ys)"

   352   by (drule_tac djoin_append_left [where zs' = "[]"], simp)

   353 

   354 lemma djoin_simp_2 [simp]: "xs \<asymp> ys \<Longrightarrow> (zs' @ xs) \<asymp> ys"

   355   by (drule_tac djoin_append_left [where zs = "[]"], simp)

   356 

   357 lemma djoin_append_right[simp]: "xs \<asymp> ys \<Longrightarrow> (xs @ zs) \<asymp> (ys @ zs)"

   358   by (simp add:djoin_diff_iff)

   359 

   360 lemma djoin_cons_append[simp]: "xs \<asymp> ys \<Longrightarrow> (x # xs) \<asymp> (zs @ ys)"

   361   by (subgoal_tac "[x] @ xs \<asymp> zs @ ys", simp, blast)

   362 

   363 lemma djoin_append_cons[simp]: "xs \<asymp> ys \<Longrightarrow> (zs @ xs) \<asymp> (y # ys)"

   364   by (subgoal_tac "zs @ xs \<asymp> [y] @ ys", simp, blast)

   365 

   366 lemma djoin_neq [simp]: "xs \<asymp> ys \<Longrightarrow> xs \<noteq> ys"

   367   by (simp only:djoin_diff_iff, clarsimp)

   368 

   369 lemma djoin_cons [simp]: "e \<noteq> a \<Longrightarrow> e # xs \<asymp> a # xs"

   370   by (unfold djoin_diff_iff, simp)

   371 

   372 lemma djoin_append_e [simp]: "e \<noteq> a \<Longrightarrow> (zs @ [e] @ xs) \<asymp> (zs' @ [a] @ xs)"

   373   by (unfold djoin_diff_iff, simp)

   374 

   375 lemma djoin_mono [simp]: "\<lbrakk>xs \<asymp> ys; xs \<preceq> xs'; ys \<preceq> ys'\<rbrakk> \<Longrightarrow> xs' \<asymp> ys'"

   376 proof(erule_tac djoin_revE,unfold djoin_diff_rev_iff)

   377   fix e es a as

   378   assume hx: "xs \<preceq> xs'"

   379     and hy: "ys \<preceq> ys'"

   380     and hmx: "xs \<setminus> ys = es @ [e]"

   381     and hmy: "ys \<setminus> xs = as @ [a]" 

   382     and neq: "a \<noteq> e"

   383   have "xs' \<setminus> ys' = ((xs' \<setminus> xs) @ es) @ [e] \<and> ys' \<setminus> xs' = ((ys' \<setminus> ys) @ as) @ [a] \<and> a \<noteq> e"

   384   proof -

   385     from hx have heqx: "(xs' \<setminus> xs) @ xs = xs'"

   386       by (cut_tac list_com_diff_rev [of xs' xs], subgoal_tac "xs' \<bullet> xs = xs", simp+)

   387     moreover from hy have heqy: "(ys' \<setminus> ys) @ ys = ys'" 

   388       by (cut_tac list_com_diff_rev [of ys' ys], subgoal_tac "ys' \<bullet> ys = ys", simp+)

   389     moreover from list_diff_djoin_rev_simplified [OF hmx hmy] 

   390     have "((xs' \<setminus> xs) @ xs) \<setminus>  ((ys' \<setminus> ys) @ ys) = (xs' \<setminus> xs) @ es @ [e]" by simp

   391     moreover from list_diff_djoin_rev_simplified [OF hmy hmx] 

   392     have "((ys' \<setminus> ys) @ ys) \<setminus>  ((xs' \<setminus> xs) @ xs) = (ys' \<setminus> ys) @ as @ [a]" by simp

   393     ultimately show ?thesis by (simp add:neq)

   394   qed

   395   thus "\<exists>e es a as. xs' \<setminus> ys' = es @ [e] \<and> ys' \<setminus> xs' = as @ [a] \<and> a \<noteq> e" by blast

   396 qed

   397 

   398 lemmas djoin_append_e_simplified [simp] = djoin_append_e [simplified]

   399 

   400 (*<*)

   401 end

   402 (*>*)