section ‹Trace Theory› theory Traces imports "Basics/Word_Prefixes" begin locale traces = fixes ind :: "'item ⇒ 'item ⇒ bool" assumes independence_symmetric[sym]: "ind a b ⟹ ind b a" begin abbreviation Ind :: "'item set ⇒ 'item set ⇒ bool" where "Ind A B ≡ ∀ a ∈ A. ∀ b ∈ B. ind a b" inductive eq_swap :: "'item list ⇒ 'item list ⇒ bool" (infix "=⇩_{S}" 50) where swap: "ind a b ⟹ u @ [a] @ [b] @ v =⇩_{S}u @ [b] @ [a] @ v" declare eq_swap.intros[intro] declare eq_swap.cases[elim] lemma eq_swap_sym[sym]: "v =⇩_{S}w ⟹ w =⇩_{S}v" using independence_symmetric by auto lemma eq_swap_length[dest]: "w⇩_{1}=⇩_{S}w⇩_{2}⟹ length w⇩_{1}= length w⇩_{2}" by force lemma eq_swap_range[dest]: "w⇩_{1}=⇩_{S}w⇩_{2}⟹ set w⇩_{1}= set w⇩_{2}" by force lemma eq_swap_extend: assumes "w⇩_{1}=⇩_{S}w⇩_{2}" shows "u @ w⇩_{1}@ v =⇩_{S}u @ w⇩_{2}@ v" using assms proof induct case (swap a b u' v') have "u @ (u' @ [a] @ [b] @ v') @ v = (u @ u') @ [a] @ [b] @ (v' @ v)" by simp also have "… =⇩_{S}(u @ u') @ [b] @ [a] @ (v' @ v)" using swap by blast also have "… = u @ (u' @ [b] @ [a] @ v') @ v" by simp finally show ?case by this qed lemma eq_swap_remove1: assumes "w⇩_{1}=⇩_{S}w⇩_{2}" obtains (equal) "remove1 c w⇩_{1}= remove1 c w⇩_{2}" | (swap) "remove1 c w⇩_{1}=⇩_{S}remove1 c w⇩_{2}" using assms proof induct case (swap a b u v) have "c ∉ set (u @ [a] @ [b] @ v) ∨ c ∈ set u ∨ c ∉ set u ∧ c = a ∨ c ∉ set u ∧ c ≠ a ∧ c = b ∨ c ∉ set u ∧ c ≠ a ∧ c ≠ b ∧ c ∈ set v" by auto thus ?case proof (elim disjE) assume 0: "c ∉ set (u @ [a] @ [b] @ v)" have 1: "c ∉ set (u @ [b] @ [a] @ v)" using 0 by auto have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [a] @ [b] @ v" using remove1_idem 0 by this have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [b] @ [a] @ v" using remove1_idem 1 by this have 4: "remove1 c (u @ [a] @ [b] @ v) =⇩_{S}remove1 c (u @ [b] @ [a] @ v)" unfolding 2 3 using eq_swap.intros swap(1) by this show thesis using swap(3) 4 by this next assume 0: "c ∈ set u" have 2: "remove1 c (u @ [a] @ [b] @ v) = remove1 c u @ [a] @ [b] @ v" unfolding remove1_append using 0 by simp have 3: "remove1 c (u @ [b] @ [a] @ v) = remove1 c u @ [b] @ [a] @ v" unfolding remove1_append using 0 by simp have 4: "remove1 c (u @ [a] @ [b] @ v) =⇩_{S}remove1 c (u @ [b] @ [a] @ v)" unfolding 2 3 using eq_swap.intros swap(1) by this show thesis using swap(3) 4 by this next assume 0: "c ∉ set u ∧ c = a" have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [b] @ v" unfolding remove1_append using remove1_idem 0 by auto have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [b] @ v" unfolding remove1_append using remove1_idem 0 by auto have 4: "remove1 c (u @ [a] @ [b] @ v) = remove1 c (u @ [b] @ [a] @ v)" unfolding 2 3 by rule show thesis using swap(2) 4 by this next assume 0: "c ∉ set u ∧ c ≠ a ∧ c = b" have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [a] @ v" unfolding remove1_append using remove1_idem 0 by auto have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [a] @ v" unfolding remove1_append using remove1_idem 0 by auto have 4: "remove1 c (u @ [a] @ [b] @ v) = remove1 c (u @ [b] @ [a] @ v)" unfolding 2 3 by rule show thesis using swap(2) 4 by this next assume 0: "c ∉ set u ∧ c ≠ a ∧ c ≠ b ∧ c ∈ set v" have 2: "remove1 c (u @ [a] @ [b] @ v) = u @ [a] @ [b] @ remove1 c v" unfolding remove1_append using 0 by simp have 3: "remove1 c (u @ [b] @ [a] @ v) = u @ [b] @ [a] @ remove1 c v" unfolding remove1_append using 0 by simp have 4: "remove1 c (u @ [a] @ [b] @ v) =⇩_{S}remove1 c (u @ [b] @ [a] @ v)" unfolding 2 3 using eq_swap.intros swap(1) by this show ?thesis using swap(3) 4 by this qed qed lemma eq_swap_rev: assumes "w⇩_{1}=⇩_{S}w⇩_{2}" shows "rev w⇩_{1}=⇩_{S}rev w⇩_{2}" using assms proof induct case (swap a b u v) have 1: "rev v @ [a] @ [b] @ rev u =⇩_{S}rev v @ [b] @ [a] @ rev u" using swap by blast have 2: "rev v @ [b] @ [a] @ rev u =⇩_{S}rev v @ [a] @ [b] @ rev u" using 1 eq_swap_sym by blast show ?case using 2 by simp qed abbreviation eq_fin :: "'item list ⇒ 'item list ⇒ bool" (infix "=⇩_{F}" 50) where "eq_fin ≡ eq_swap⇧^{*}⇧^{*}" lemma eq_fin_symp[intro, sym]: "u =⇩_{F}v ⟹ v =⇩_{F}u" using eq_swap_sym sym_rtrancl[to_pred] unfolding symp_def by metis lemma eq_fin_length[dest]: "w⇩_{1}=⇩_{F}w⇩_{2}⟹ length w⇩_{1}= length w⇩_{2}" by (induct rule: rtranclp.induct, auto) lemma eq_fin_range[dest]: "w⇩_{1}=⇩_{F}w⇩_{2}⟹ set w⇩_{1}= set w⇩_{2}" by (induct rule: rtranclp.induct, auto) lemma eq_fin_remove1: assumes "w⇩_{1}=⇩_{F}w⇩_{2}" shows "remove1 c w⇩_{1}=⇩_{F}remove1 c w⇩_{2}" using assms proof induct case (base) show ?case by simp next case (step w⇩_{2}w⇩_{3}) show ?case using step(2) proof (cases rule: eq_swap_remove1[where ?c = c]) case equal show ?thesis using step equal by simp next case swap show ?thesis using step swap by auto qed qed lemma eq_fin_rev: assumes "w⇩_{1}=⇩_{F}w⇩_{2}" shows "rev w⇩_{1}=⇩_{F}rev w⇩_{2}" using assms by (induct, auto dest: eq_swap_rev) lemma eq_fin_concat_eq_fin_start: assumes "u @ v⇩_{1}=⇩_{F}u @ v⇩_{2}" shows "v⇩_{1}=⇩_{F}v⇩_{2}" using assms proof (induct u arbitrary: v⇩_{1}v⇩_{2}rule: rev_induct) case (Nil) show ?case using Nil by simp next case (snoc a u) have 1: "u @ [a] @ v⇩_{1}=⇩_{F}u @ [a] @ v⇩_{2}" using snoc(2) by simp have 2: "[a] @ v⇩_{1}=⇩_{F}[a] @ v⇩_{2}" using snoc(1) 1 by this show ?case using eq_fin_remove1[OF 2, of a] by simp qed lemma eq_fin_concat: "u @ w⇩_{1}@ v =⇩_{F}u @ w⇩_{2}@ v ⟷ w⇩_{1}=⇩_{F}w⇩_{2}" proof assume 0: "u @ w⇩_{1}@ v =⇩_{F}u @ w⇩_{2}@ v" have 1: "w⇩_{1}@ v =⇩_{F}w⇩_{2}@ v" using eq_fin_concat_eq_fin_start 0 by this have 2: "rev (w⇩_{1}@ v) =⇩_{F}rev (w⇩_{2}@ v)" using 1 by (blast dest: eq_fin_rev) have 3: "rev v @ rev w⇩_{1}=⇩_{F}rev v @ rev w⇩_{2}" using 2 by simp have 4: "rev w⇩_{1}=⇩_{F}rev w⇩_{2}" using eq_fin_concat_eq_fin_start 3 by this have 5: "rev (rev w⇩_{1}) =⇩_{F}rev (rev w⇩_{2})" using 4 by (blast dest: eq_fin_rev) show "w⇩_{1}=⇩_{F}w⇩_{2}" using 5 by simp next show "u @ w⇩_{1}@ v =⇩_{F}u @ w⇩_{2}@ v" if "w⇩_{1}=⇩_{F}w⇩_{2}" using that by (induct, auto dest: eq_swap_extend[of _ _ u v]) qed lemma eq_fin_concat_start[iff]: "w @ w⇩_{1}=⇩_{F}w @ w⇩_{2}⟷ w⇩_{1}=⇩_{F}w⇩_{2}" using eq_fin_concat[of "w" _ "[]"] by simp lemma eq_fin_concat_end[iff]: "w⇩_{1}@ w =⇩_{F}w⇩_{2}@ w ⟷ w⇩_{1}=⇩_{F}w⇩_{2}" using eq_fin_concat[of "[]" _ "w"] by simp lemma ind_eq_fin': assumes "Ind {a} (set v)" shows "[a] @ v =⇩_{F}v @ [a]" using assms proof (induct v) case (Nil) show ?case by simp next case (Cons b v) have 1: "Ind {a} (set v)" using Cons(2) by auto have 2: "ind a b" using Cons(2) by auto have "[a] @ b # v = [a] @ [b] @ v" by simp also have "… =⇩_{S}[b] @ [a] @ v" using eq_swap.intros[OF 2, of "[]"] by auto also have "… =⇩_{F}[b] @ v @ [a]" using Cons(1) 1 by blast also have "… = (b # v) @ [a]" by simp finally show ?case by this qed lemma ind_eq_fin[intro]: assumes "Ind (set u) (set v)" shows "u @ v =⇩_{F}v @ u" using assms proof (induct u) case (Nil) show ?case by simp next case (Cons a u) have 1: "Ind (set u) (set v)" using Cons(2) by auto have 2: "Ind {a} (set v)" using Cons(2) by auto have "(a # u) @ v = [a] @ u @ v" by simp also have "… =⇩_{F}[a] @ v @ u" using Cons(1) 1 by blast also have "… = ([a] @ v) @ u" by simp also have "… =⇩_{F}(v @ [a]) @ u" using ind_eq_fin' 2 by blast also have "… = v @ (a # u)" by simp finally show ?case by this qed definition le_fin :: "'item list ⇒ 'item list ⇒ bool" (infix "≼⇩_{F}" 50) where "w⇩_{1}≼⇩_{F}w⇩_{2}≡ ∃ v⇩_{1}. w⇩_{1}@ v⇩_{1}=⇩_{F}w⇩_{2}" lemma le_finI[intro 0]: assumes "w⇩_{1}@ v⇩_{1}=⇩_{F}w⇩_{2}" shows "w⇩_{1}≼⇩_{F}w⇩_{2}" using assms unfolding le_fin_def by auto lemma le_finE[elim 0]: assumes "w⇩_{1}≼⇩_{F}w⇩_{2}" obtains v⇩_{1}where "w⇩_{1}@ v⇩_{1}=⇩_{F}w⇩_{2}" using assms unfolding le_fin_def by auto lemma le_fin_empty[simp]: "[] ≼⇩_{F}w" by force lemma le_fin_trivial[intro]: "w⇩_{1}=⇩_{F}w⇩_{2}⟹ w⇩_{1}≼⇩_{F}w⇩_{2}" proof assume 1: "w⇩_{1}=⇩_{F}w⇩_{2}" show "w⇩_{1}@ [] =⇩_{F}w⇩_{2}" using 1 by simp qed lemma le_fin_length[dest]: "w⇩_{1}≼⇩_{F}w⇩_{2}⟹ length w⇩_{1}≤ length w⇩_{2}" by force lemma le_fin_range[dest]: "w⇩_{1}≼⇩_{F}w⇩_{2}⟹ set w⇩_{1}⊆ set w⇩_{2}" by force lemma eq_fin_alt_def: "w⇩_{1}=⇩_{F}w⇩_{2}⟷ w⇩_{1}≼⇩_{F}w⇩_{2}∧ w⇩_{2}≼⇩_{F}w⇩_{1}" proof show "w⇩_{1}≼⇩_{F}w⇩_{2}∧ w⇩_{2}≼⇩_{F}w⇩_{1}" if "w⇩_{1}=⇩_{F}w⇩_{2}" using that by blast next assume 0: "w⇩_{1}≼⇩_{F}w⇩_{2}∧ w⇩_{2}≼⇩_{F}w⇩_{1}" have 1: "w⇩_{1}≼⇩_{F}w⇩_{2}" "w⇩_{2}≼⇩_{F}w⇩_{1}" using 0 by auto have 10: "length w⇩_{1}= length w⇩_{2}" using 1 by force obtain v⇩_{1}v⇩_{2}where 2: "w⇩_{1}@ v⇩_{1}=⇩_{F}w⇩_{2}" "w⇩_{2}@ v⇩_{2}=⇩_{F}w⇩_{1}" using 1 by (elim le_finE) have 3: "length w⇩_{1}= length (w⇩_{1}@ v⇩_{1})" using 2 10 by force have 4: "w⇩_{1}= w⇩_{1}@ v⇩_{1}" using 3 by auto have 5: "length w⇩_{2}= length (w⇩_{2}@ v⇩_{2})" using 2 10 by force have 6: "w⇩_{2}= w⇩_{2}@ v⇩_{2}" using 5 by auto show "w⇩_{1}=⇩_{F}w⇩_{2}" using 4 6 2 by simp qed lemma le_fin_reflp[simp, intro]: "w ≼⇩_{F}w" by auto lemma le_fin_transp[intro, trans]: assumes "w⇩_{1}≼⇩_{F}w⇩_{2}" "w⇩_{2}≼⇩_{F}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}w⇩_{3}" proof - obtain v⇩_{1}where 1: "w⇩_{1}@ v⇩_{1}=⇩_{F}w⇩_{2}" using assms(1) by rule obtain v⇩_{2}where 2: "w⇩_{2}@ v⇩_{2}=⇩_{F}w⇩_{3}" using assms(2) by rule show ?thesis proof have "w⇩_{1}@ v⇩_{1}@ v⇩_{2}= (w⇩_{1}@ v⇩_{1}) @ v⇩_{2}" by simp also have "… =⇩_{F}w⇩_{2}@ v⇩_{2}" using 1 by blast also have "… =⇩_{F}w⇩_{3}" using 2 by blast finally show "w⇩_{1}@ v⇩_{1}@ v⇩_{2}=⇩_{F}w⇩_{3}" by this qed qed lemma eq_fin_le_fin_transp[intro, trans]: assumes "w⇩_{1}=⇩_{F}w⇩_{2}" "w⇩_{2}≼⇩_{F}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}w⇩_{3}" using assms by auto lemma le_fin_eq_fin_transp[intro, trans]: assumes "w⇩_{1}≼⇩_{F}w⇩_{2}" "w⇩_{2}=⇩_{F}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}w⇩_{3}" using assms by auto lemma prefix_le_fin_transp[intro, trans]: assumes "w⇩_{1}≤ w⇩_{2}" "w⇩_{2}≼⇩_{F}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}w⇩_{3}" proof - obtain v⇩_{1}where 1: "w⇩_{2}= w⇩_{1}@ v⇩_{1}" using assms(1) by rule obtain v⇩_{2}where 2: "w⇩_{2}@ v⇩_{2}=⇩_{F}w⇩_{3}" using assms(2) by rule show ?thesis proof show "w⇩_{1}@ v⇩_{1}@ v⇩_{2}=⇩_{F}w⇩_{3}" using 1 2 by simp qed qed lemma le_fin_prefix_transp[intro, trans]: assumes "w⇩_{1}≼⇩_{F}w⇩_{2}" "w⇩_{2}≤ w⇩_{3}" shows "w⇩_{1}≼⇩_{F}w⇩_{3}" proof - obtain v⇩_{1}where 1: "w⇩_{1}@ v⇩_{1}=⇩_{F}w⇩_{2}" using assms(1) by rule obtain v⇩_{2}where 2: "w⇩_{3}= w⇩_{2}@ v⇩_{2}" using assms(2) by rule show ?thesis proof have "w⇩_{1}@ v⇩_{1}@ v⇩_{2}= (w⇩_{1}@ v⇩_{1}) @ v⇩_{2}" by simp also have "… =⇩_{F}w⇩_{2}@ v⇩_{2}" using 1 by blast also have "… = w⇩_{3}" using 2 by simp finally show "w⇩_{1}@ v⇩_{1}@ v⇩_{2}=⇩_{F}w⇩_{3}" by this qed qed lemma prefix_eq_fin_transp[intro, trans]: assumes "w⇩_{1}≤ w⇩_{2}" "w⇩_{2}=⇩_{F}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}w⇩_{3}" using assms by auto lemma le_fin_concat_start[iff]: "w @ w⇩_{1}≼⇩_{F}w @ w⇩_{2}⟷ w⇩_{1}≼⇩_{F}w⇩_{2}" proof assume 0: "w @ w⇩_{1}≼⇩_{F}w @ w⇩_{2}" obtain v⇩_{1}where 1: "w @ w⇩_{1}@ v⇩_{1}=⇩_{F}w @ w⇩_{2}" using 0 by auto show "w⇩_{1}≼⇩_{F}w⇩_{2}" using 1 by auto next assume 0: "w⇩_{1}≼⇩_{F}w⇩_{2}" obtain v⇩_{1}where 1: "w⇩_{1}@ v⇩_{1}=⇩_{F}w⇩_{2}" using 0 by auto have 2: "(w @ w⇩_{1}) @ v⇩_{1}=⇩_{F}w @ w⇩_{2}" using 1 by auto show "w @ w⇩_{1}≼⇩_{F}w @ w⇩_{2}" using 2 by blast qed lemma le_fin_concat_end[dest]: assumes "w⇩_{1}≼⇩_{F}w⇩_{2}" shows "w⇩_{1}≼⇩_{F}w⇩_{2}@ w" proof - obtain v⇩_{1}where 1: "w⇩_{1}@ v⇩_{1}=⇩_{F}w⇩_{2}" using assms by rule show ?thesis proof have "w⇩_{1}@ v⇩_{1}@ w = (w⇩_{1}@ v⇩_{1}) @ w" by simp also have "… =⇩_{F}w⇩_{2}@ w" using 1 by blast finally show "w⇩_{1}@ v⇩_{1}@ w =⇩_{F}w⇩_{2}@ w" by this qed qed definition le_fininf :: "'item list ⇒ 'item stream ⇒ bool" (infix "≼⇩_{F}⇩_{I}" 50) where "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}≡ ∃ v⇩_{2}. v⇩_{2}≤⇩_{F}⇩_{I}w⇩_{2}∧ w⇩_{1}≼⇩_{F}v⇩_{2}" lemma le_fininfI[intro 0]: assumes "v⇩_{2}≤⇩_{F}⇩_{I}w⇩_{2}" "w⇩_{1}≼⇩_{F}v⇩_{2}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" using assms unfolding le_fininf_def by auto lemma le_fininfE[elim 0]: assumes "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" obtains v⇩_{2}where "v⇩_{2}≤⇩_{F}⇩_{I}w⇩_{2}" "w⇩_{1}≼⇩_{F}v⇩_{2}" using assms unfolding le_fininf_def by auto lemma le_fininf_empty[simp]: "[] ≼⇩_{F}⇩_{I}w" by force lemma le_fininf_range[dest]: "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}⟹ set w⇩_{1}⊆ sset w⇩_{2}" by force lemma eq_fin_le_fininf_transp[intro, trans]: assumes "w⇩_{1}=⇩_{F}w⇩_{2}" "w⇩_{2}≼⇩_{F}⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{3}" using assms by blast lemma le_fin_le_fininf_transp[intro, trans]: assumes "w⇩_{1}≼⇩_{F}w⇩_{2}" "w⇩_{2}≼⇩_{F}⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{3}" using assms by blast lemma prefix_le_fininf_transp[intro, trans]: assumes "w⇩_{1}≤ w⇩_{2}" "w⇩_{2}≼⇩_{F}⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{3}" using assms by auto lemma le_fin_prefix_fininf_transp[intro, trans]: assumes "w⇩_{1}≼⇩_{F}w⇩_{2}" "w⇩_{2}≤⇩_{F}⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{3}" using assms by auto lemma eq_fin_prefix_fininf_transp[intro, trans]: assumes "w⇩_{1}=⇩_{F}w⇩_{2}" "w⇩_{2}≤⇩_{F}⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{3}" using assms by auto lemma le_fininf_concat_start[iff]: "w @ w⇩_{1}≼⇩_{F}⇩_{I}w @- w⇩_{2}⟷ w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" proof assume 0: "w @ w⇩_{1}≼⇩_{F}⇩_{I}w @- w⇩_{2}" obtain v⇩_{2}where 1: "v⇩_{2}≤⇩_{F}⇩_{I}w @- w⇩_{2}" "w @ w⇩_{1}≼⇩_{F}v⇩_{2}" using 0 by rule have 2: "length w ≤ length v⇩_{2}" using 1(2) by force have 4: "w ≤ v⇩_{2}" using prefix_fininf_extend[OF 1(1) 2] by this obtain v⇩_{1}where 5: "v⇩_{2}= w @ v⇩_{1}" using 4 by rule show "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" proof show "v⇩_{1}≤⇩_{F}⇩_{I}w⇩_{2}" using 1(1) unfolding 5 by auto show "w⇩_{1}≼⇩_{F}v⇩_{1}" using 1(2) unfolding 5 by simp qed next assume 0: "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" obtain v⇩_{2}where 1: "v⇩_{2}≤⇩_{F}⇩_{I}w⇩_{2}" "w⇩_{1}≼⇩_{F}v⇩_{2}" using 0 by rule show "w @ w⇩_{1}≼⇩_{F}⇩_{I}w @- w⇩_{2}" proof show "w @ v⇩_{2}≤⇩_{F}⇩_{I}(w @- w⇩_{2})" using 1(1) by auto show "w @ w⇩_{1}≼⇩_{F}w @ v⇩_{2}" using 1(2) by auto qed qed lemma le_fininf_singleton[intro, simp]: "[shd v] ≼⇩_{F}⇩_{I}v" proof - have "[shd v] ≼⇩_{F}⇩_{I}shd v ## sdrop 1 v" by blast also have "… = v" by simp finally show ?thesis by this qed definition le_inf :: "'item stream ⇒ 'item stream ⇒ bool" (infix "≼⇩_{I}" 50) where "w⇩_{1}≼⇩_{I}w⇩_{2}≡ ∀ v⇩_{1}. v⇩_{1}≤⇩_{F}⇩_{I}w⇩_{1}⟶ v⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" lemma le_infI[intro 0]: assumes "⋀ v⇩_{1}. v⇩_{1}≤⇩_{F}⇩_{I}w⇩_{1}⟹ v⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" shows "w⇩_{1}≼⇩_{I}w⇩_{2}" using assms unfolding le_inf_def by auto lemma le_infE[elim 0]: assumes "w⇩_{1}≼⇩_{I}w⇩_{2}" "v⇩_{1}≤⇩_{F}⇩_{I}w⇩_{1}" obtains "v⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" using assms unfolding le_inf_def by auto lemma le_inf_range[dest]: assumes "w⇩_{1}≼⇩_{I}w⇩_{2}" shows "sset w⇩_{1}⊆ sset w⇩_{2}" proof fix a assume 1: "a ∈ sset w⇩_{1}" obtain i where 2: "a = w⇩_{1}!! i" using 1 by (metis imageE sset_range) have 3: "stake (Suc i) w⇩_{1}≤⇩_{F}⇩_{I}w⇩_{1}" by rule have 4: "stake (Suc i) w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" using assms 3 by rule have 5: "w⇩_{1}!! i ∈ set (stake (Suc i) w⇩_{1})" by (meson lessI set_stake_snth) show "a ∈ sset w⇩_{2}" unfolding 2 using 5 4 by fastforce qed lemma le_inf_reflp[simp, intro]: "w ≼⇩_{I}w" by auto lemma prefix_fininf_le_inf_transp[intro, trans]: assumes "w⇩_{1}≤⇩_{F}⇩_{I}w⇩_{2}" "w⇩_{2}≼⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{3}" using assms by blast lemma le_fininf_le_inf_transp[intro, trans]: assumes "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" "w⇩_{2}≼⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{3}" using assms by blast lemma le_inf_transp[intro, trans]: assumes "w⇩_{1}≼⇩_{I}w⇩_{2}" "w⇩_{2}≼⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{I}w⇩_{3}" using assms by blast lemma le_infI': assumes "⋀ k. ∃ v. v ≤⇩_{F}⇩_{I}w⇩_{1}∧ k < length v ∧ v ≼⇩_{F}⇩_{I}w⇩_{2}" shows "w⇩_{1}≼⇩_{I}w⇩_{2}" proof fix u assume 1: "u ≤⇩_{F}⇩_{I}w⇩_{1}" obtain v where 2: "v ≤⇩_{F}⇩_{I}w⇩_{1}" "length u < length v" "v ≼⇩_{F}⇩_{I}w⇩_{2}" using assms by auto have 3: "length u ≤ length v" using 2(2) by auto have 4: "u ≤ v" using prefix_fininf_length 1 2(1) 3 by this show "u ≼⇩_{F}⇩_{I}w⇩_{2}" using 4 2(3) by rule qed lemma le_infI_chain_left: assumes "chain w" "⋀ k. w k ≼⇩_{F}⇩_{I}v" shows "limit w ≼⇩_{I}v" proof (rule le_infI') fix k obtain l where 1: "k < length (w l)" using assms(1) by rule show "∃ va. va ≤⇩_{F}⇩_{I}limit w ∧ k < length va ∧ va ≼⇩_{F}⇩_{I}v" proof (intro exI conjI) show "w l ≤⇩_{F}⇩_{I}limit w" using chain_prefix_limit assms(1) by this show "k < length (w l)" using 1 by this show "w l ≼⇩_{F}⇩_{I}v" using assms(2) by this qed qed lemma le_infI_chain_right: assumes "chain w" "⋀ u. u ≤⇩_{F}⇩_{I}v ⟹ u ≼⇩_{F}w (l u)" shows "v ≼⇩_{I}limit w" proof fix u assume 1: "u ≤⇩_{F}⇩_{I}v" show "u ≼⇩_{F}⇩_{I}limit w" proof show "w (l u) ≤⇩_{F}⇩_{I}limit w" using chain_prefix_limit assms(1) by this show "u ≼⇩_{F}w (l u)" using assms(2) 1 by this qed qed lemma le_infI_chain_right': assumes "chain w" "⋀ k. stake k v ≼⇩_{F}w (l k)" shows "v ≼⇩_{I}limit w" proof (rule le_infI_chain_right) show "chain w" using assms(1) by this next fix u assume 1: "u ≤⇩_{F}⇩_{I}v" have 2: "stake (length u) v = u" using 1 by (simp add: prefix_fininf_def shift_eq) have 3: "stake (length u) v ≼⇩_{F}w (l (length u))" using assms(2) by this show "u ≼⇩_{F}w (l (length u))" using 3 unfolding 2 by this qed definition eq_inf :: "'item stream ⇒ 'item stream ⇒ bool" (infix "=⇩_{I}" 50) where "w⇩_{1}=⇩_{I}w⇩_{2}≡ w⇩_{1}≼⇩_{I}w⇩_{2}∧ w⇩_{2}≼⇩_{I}w⇩_{1}" lemma eq_infI[intro 0]: assumes "w⇩_{1}≼⇩_{I}w⇩_{2}" "w⇩_{2}≼⇩_{I}w⇩_{1}" shows "w⇩_{1}=⇩_{I}w⇩_{2}" using assms unfolding eq_inf_def by auto lemma eq_infE[elim 0]: assumes "w⇩_{1}=⇩_{I}w⇩_{2}" obtains "w⇩_{1}≼⇩_{I}w⇩_{2}" "w⇩_{2}≼⇩_{I}w⇩_{1}" using assms unfolding eq_inf_def by auto lemma eq_inf_range[dest]: "w⇩_{1}=⇩_{I}w⇩_{2}⟹ sset w⇩_{1}= sset w⇩_{2}" by force lemma eq_inf_reflp[simp, intro]: "w =⇩_{I}w" by auto lemma eq_inf_symp[intro]: "w⇩_{1}=⇩_{I}w⇩_{2}⟹ w⇩_{2}=⇩_{I}w⇩_{1}" by auto lemma eq_inf_transp[intro, trans]: assumes "w⇩_{1}=⇩_{I}w⇩_{2}" "w⇩_{2}=⇩_{I}w⇩_{3}" shows "w⇩_{1}=⇩_{I}w⇩_{3}" using assms by blast lemma le_fininf_eq_inf_transp[intro, trans]: assumes "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" "w⇩_{2}=⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{3}" using assms by blast lemma le_inf_eq_inf_transp[intro, trans]: assumes "w⇩_{1}≼⇩_{I}w⇩_{2}" "w⇩_{2}=⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{I}w⇩_{3}" using assms by blast lemma eq_inf_le_inf_transp[intro, trans]: assumes "w⇩_{1}=⇩_{I}w⇩_{2}" "w⇩_{2}≼⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{I}w⇩_{3}" using assms by blast lemma prefix_fininf_eq_inf_transp[intro, trans]: assumes "w⇩_{1}≤⇩_{F}⇩_{I}w⇩_{2}" "w⇩_{2}=⇩_{I}w⇩_{3}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{3}" using assms by blast lemma le_inf_concat_start[iff]: "w @- w⇩_{1}≼⇩_{I}w @- w⇩_{2}⟷ w⇩_{1}≼⇩_{I}w⇩_{2}" proof assume 1: "w @- w⇩_{1}≼⇩_{I}w @- w⇩_{2}" show "w⇩_{1}≼⇩_{I}w⇩_{2}" proof fix v⇩_{1}assume 2: "v⇩_{1}≤⇩_{F}⇩_{I}w⇩_{1}" have "w @ v⇩_{1}≤⇩_{F}⇩_{I}w @- w⇩_{1}" using 2 by auto also have "… ≼⇩_{I}w @- w⇩_{2}" using 1 by this finally show "v⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" by rule qed next assume 1: "w⇩_{1}≼⇩_{I}w⇩_{2}" show "w @- w⇩_{1}≼⇩_{I}w @- w⇩_{2}" proof fix v⇩_{1}assume 2: "v⇩_{1}≤⇩_{F}⇩_{I}w @- w⇩_{1}" then show "v⇩_{1}≼⇩_{F}⇩_{I}w @- w⇩_{2}" proof (cases rule: prefix_fininf_append) case (absorb) show ?thesis using absorb by auto next case (extend z) show ?thesis using 1 extend by auto qed qed qed lemma eq_fin_le_inf_concat_end[dest]: "w⇩_{1}=⇩_{F}w⇩_{2}⟹ w⇩_{1}@- w ≼⇩_{I}w⇩_{2}@- w" proof fix v⇩_{1}assume 1: "w⇩_{1}=⇩_{F}w⇩_{2}" "v⇩_{1}≤⇩_{F}⇩_{I}w⇩_{1}@- w" show "v⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}@- w" using 1(2) proof (cases rule: prefix_fininf_append) case (absorb) show ?thesis proof show "w⇩_{2}≤⇩_{F}⇩_{I}(w⇩_{2}@- w)" by auto show "v⇩_{1}≼⇩_{F}w⇩_{2}" using absorb 1(1) by auto qed next case (extend w') show ?thesis proof show "w⇩_{2}@ w' ≤⇩_{F}⇩_{I}(w⇩_{2}@- w)" using extend(2) by auto show "v⇩_{1}≼⇩_{F}w⇩_{2}@ w'" unfolding extend(1) using 1(1) by auto qed qed qed lemma eq_inf_concat_start[iff]: "w @- w⇩_{1}=⇩_{I}w @- w⇩_{2}⟷ w⇩_{1}=⇩_{I}w⇩_{2}" by blast lemma eq_inf_concat_end[dest]: "w⇩_{1}=⇩_{F}w⇩_{2}⟹ w⇩_{1}@- w =⇩_{I}w⇩_{2}@- w" proof - assume 0: "w⇩_{1}=⇩_{F}w⇩_{2}" have 1: "w⇩_{2}=⇩_{F}w⇩_{1}" using 0 by auto show "w⇩_{1}@- w =⇩_{I}w⇩_{2}@- w" using eq_fin_le_inf_concat_end[OF 0] eq_fin_le_inf_concat_end[OF 1] by auto qed lemma le_fininf_suffixI[intro]: assumes "w =⇩_{I}w⇩_{1}@- w⇩_{2}" shows "w⇩_{1}≼⇩_{F}⇩_{I}w" using assms by blast lemma le_fininf_suffixE[elim]: assumes "w⇩_{1}≼⇩_{F}⇩_{I}w" obtains w⇩_{2}where "w =⇩_{I}w⇩_{1}@- w⇩_{2}" proof - obtain v⇩_{2}where 1: "v⇩_{2}≤⇩_{F}⇩_{I}w" "w⇩_{1}≼⇩_{F}v⇩_{2}" using assms(1) by rule obtain u⇩_{1}where 2: "w⇩_{1}@ u⇩_{1}=⇩_{F}v⇩_{2}" using 1(2) by rule obtain v⇩_{2}' where 3: "w = v⇩_{2}@- v⇩_{2}'" using 1(1) by rule show ?thesis proof show "w =⇩_{I}w⇩_{1}@- u⇩_{1}@- v⇩_{2}'" unfolding 3 using 2 by fastforce qed qed lemma subsume_fin: assumes "u⇩_{1}≼⇩_{F}⇩_{I}w" "v⇩_{1}≼⇩_{F}⇩_{I}w" obtains w⇩_{1}where "u⇩_{1}≼⇩_{F}w⇩_{1}" "v⇩_{1}≼⇩_{F}w⇩_{1}" proof - obtain u⇩_{2}where 2: "u⇩_{2}≤⇩_{F}⇩_{I}w" "u⇩_{1}≼⇩_{F}u⇩_{2}" using assms(1) by rule obtain v⇩_{2}where 3: "v⇩_{2}≤⇩_{F}⇩_{I}w" "v⇩_{1}≼⇩_{F}v⇩_{2}" using assms(2) by rule show ?thesis proof (cases "length u⇩_{2}" "length v⇩_{2}" rule: le_cases) case le show ?thesis proof show "u⇩_{1}≼⇩_{F}v⇩_{2}" using 2(2) prefix_fininf_length[OF 2(1) 3(1) le] by auto show "v⇩_{1}≼⇩_{F}v⇩_{2}" using 3(2) by this qed next case ge show ?thesis proof show "u⇩_{1}≼⇩_{F}u⇩_{2}" using 2(2) by this show "v⇩_{1}≼⇩_{F}u⇩_{2}" using 3(2) prefix_fininf_length[OF 3(1) 2(1) ge] by auto qed qed qed lemma eq_fin_end: assumes "u⇩_{1}=⇩_{F}u⇩_{2}" "u⇩_{1}@ v⇩_{1}=⇩_{F}u⇩_{2}@ v⇩_{2}" shows "v⇩_{1}=⇩_{F}v⇩_{2}" proof - have "u⇩_{1}@ v⇩_{2}=⇩_{F}u⇩_{2}@ v⇩_{2}" using assms(1) by blast also have "… =⇩_{F}u⇩_{1}@ v⇩_{1}" using assms(2) by blast finally show ?thesis by blast qed definition indoc :: "'item ⇒ 'item list ⇒ bool" where "indoc a u ≡ ∃ u⇩_{1}u⇩_{2}. u = u⇩_{1}@ [a] @ u⇩_{2}∧ a ∉ set u⇩_{1}∧ Ind {a} (set u⇩_{1})" lemma indoc_set: "indoc a u ⟹ a ∈ set u" unfolding indoc_def by auto lemma indoc_appendI1[intro]: assumes "indoc a u" shows "indoc a (u @ v)" using assms unfolding indoc_def by force lemma indoc_appendI2[intro]: assumes "a ∉ set u" "Ind {a} (set u)" "indoc a v" shows "indoc a (u @ v)" proof - obtain v⇩_{1}v⇩_{2}where 1: "v = v⇩_{1}@ [a] @ v⇩_{2}" "a ∉ set v⇩_{1}" "Ind {a} (set v⇩_{1})" using assms(3) unfolding indoc_def by blast show ?thesis proof (unfold indoc_def, intro exI conjI) show "u @ v = (u @ v⇩_{1}) @ [a] @ v⇩_{2}" unfolding 1(1) by simp show "a ∉ set (u @ v⇩_{1})" using assms(1) 1(2) by auto show "Ind {a} (set (u @ v⇩_{1}))" using assms(2) 1(3) by auto qed qed lemma indoc_appendE[elim!]: assumes "indoc a (u @ v)" obtains (first) "a ∈ set u" "indoc a u" | (second) "a ∉ set u" "Ind {a} (set u)" "indoc a v" proof - obtain w⇩_{1}w⇩_{2}where 1: "u @ v = w⇩_{1}@ [a] @ w⇩_{2}" "a ∉ set w⇩_{1}" "Ind {a} (set w⇩_{1})" using assms unfolding indoc_def by blast show ?thesis proof (cases "a ∈ set u") case True obtain u⇩_{1}u⇩_{2}where 2: "u = u⇩_{1}@ [a] @ u⇩_{2}" "a ∉ set u⇩_{1}" using split_list_first[OF True] by auto have 3: "w⇩_{1}= u⇩_{1}" proof (rule split_list_first_unique) show "w⇩_{1}@ [a] @ w⇩_{2}= u⇩_{1}@ [a] @ u⇩_{2}@ v" using 1(1) unfolding 2(1) by simp show "a ∉ set w⇩_{1}" using 1(2) by auto show "a ∉ set u⇩_{1}" using 2(2) by this qed show ?thesis proof (rule first) show "a ∈ set u" using True by this show "indoc a u" proof (unfold indoc_def, intro exI conjI) show "u = u⇩_{1}@ [a] @ u⇩_{2}" using 2(1) by this show "a ∉ set u⇩_{1}" using 1(2) unfolding 3 by this show "Ind {a} (set u⇩_{1})" using 1(3) unfolding 3 by this qed qed next case False have 2: "a ∈ set v" using indoc_set assms False by fastforce obtain v⇩_{1}v⇩_{2}where 3: "v = v⇩_{1}@ [a] @ v⇩_{2}" "a ∉ set v⇩_{1}" using split_list_first[OF 2] by auto have 4: "w⇩_{1}= u @ v⇩_{1}" proof (rule split_list_first_unique) show "w⇩_{1}@ [a] @ w⇩_{2}= (u @ v⇩_{1}) @ [a] @ v⇩_{2}" using 1(1) unfolding 3(1) by simp show "a ∉ set w⇩_{1}" using 1(2) by auto show "a ∉ set (u @ v⇩_{1})" using False 3(2) by auto qed show ?thesis proof (rule second) show "a ∉ set u" using False by this show "Ind {a} (set u)" using 1(3) 4 by auto show "indoc a v" proof (unfold indoc_def, intro exI conjI) show "v = v⇩_{1}@ [a] @ v⇩_{2}" using 3(1) by this show "a ∉ set v⇩_{1}" using 1(2) unfolding 4 by auto show "Ind {a} (set v⇩_{1})" using 1(3) unfolding 4 by auto qed qed qed qed lemma indoc_single: "indoc a [b] ⟷ a = b" proof assume 1: "indoc a [b]" obtain u⇩_{1}u⇩_{2}where 2: "[b] = u⇩_{1}@ [a] @ u⇩_{2}" "Ind {a} (set u⇩_{1})" using 1 unfolding indoc_def by auto show "a = b" using 2(1) by (metis append_eq_Cons_conv append_is_Nil_conv list.distinct(2) list.inject) next assume 1: "a = b" show "indoc a [b]" unfolding indoc_def 1 proof (intro exI conjI) show "[b] = [] @ [b] @ []" by simp show "b ∉ set []" by simp show "Ind {b} (set [])" by simp qed qed lemma indoc_append[simp]: "indoc a (u @ v) ⟷ indoc a u ∨ a ∉ set u ∧ Ind {a} (set u) ∧ indoc a v" by blast lemma indoc_Nil[simp]: "indoc a [] ⟷ False" unfolding indoc_def by auto lemma indoc_Cons[simp]: "indoc a (b # v) ⟷ a = b ∨ a ≠ b ∧ ind a b ∧ indoc a v" proof - have "indoc a (b # v) ⟷ indoc a ([b] @ v)" by simp also have "… ⟷ indoc a [b] ∨ a ∉ set [b] ∧ Ind {a} (set [b]) ∧ indoc a v" unfolding indoc_append by rule also have "… ⟷ a = b ∨ a ≠ b ∧ ind a b ∧ indoc a v" unfolding indoc_single by simp finally show ?thesis by this qed lemma eq_swap_indoc: "u =⇩_{S}v ⟹ indoc c u ⟹ indoc c v" by auto lemma eq_fin_indoc: "u =⇩_{F}v ⟹ indoc c u ⟹ indoc c v" by (induct rule: rtranclp.induct, auto) lemma eq_fin_ind': assumes "[a] @ u =⇩_{F}u⇩_{1}@ [a] @ u⇩_{2}" "a ∉ set u⇩_{1}" shows "Ind {a} (set u⇩_{1})" proof - have 1: "indoc a ([a] @ u)" by simp have 2: "indoc a (u⇩_{1}@ [a] @ u⇩_{2})" using eq_fin_indoc assms(1) 1 by this show ?thesis using assms(2) 2 by blast qed lemma eq_fin_ind: assumes "u @ v =⇩_{F}v @ u" "set u ∩ set v = {}" shows "Ind (set u) (set v)" using assms proof (induct u) case Nil show ?case by simp next case (Cons a u) have 1: "Ind {a} (set v)" proof (rule eq_fin_ind') show "[a] @ u @ v =⇩_{F}v @ [a] @ u" using Cons(2) by simp show "a ∉ set v" using Cons(3) by simp qed have 2: "Ind (set [a]) (set v)" using 1 by simp have 4: "Ind (set u) (set v)" proof (rule Cons(1)) have "[a] @ u @ v = (a # u) @ v" by simp also have "… =⇩_{F}v @ a # u" using Cons(2) by this also have "… = (v @ [a]) @ u" by simp also have "… =⇩_{F}([a] @ v) @ u" using 2 by blast also have "… = [a] @ v @ u" by simp finally show "u @ v =⇩_{F}v @ u" by blast show "set u ∩ set v = {}" using Cons(3) by auto qed show ?case using 1 4 by auto qed lemma le_fin_member': assumes "[a] ≼⇩_{F}u @ v" "a ∈ set u" shows "[a] ≼⇩_{F}u" proof - obtain w where 1: "[a] @ w =⇩_{F}u @ v" using assms(1) by rule obtain u⇩_{1}u⇩_{2}where 2: "u = u⇩_{1}@ [a] @ u⇩_{2}" "a ∉ set u⇩_{1}" using split_list_first[OF assms(2)] by auto have 3: "Ind {a} (set u⇩_{1})" proof (rule eq_fin_ind') show "[a] @ w =⇩_{F}u⇩_{1}@ [a] @ u⇩_{2}@ v" using 1 unfolding 2(1) by simp show "a ∉ set u⇩_{1}" using 2(2) by this qed have 4: "Ind (set [a]) (set u⇩_{1})" using 3 by simp have "[a] ≤ [a] @ u⇩_{1}@ u⇩_{2}" by auto also have "… = ([a] @ u⇩_{1}) @ u⇩_{2}" by simp also have "… =⇩_{F}(u⇩_{1}@ [a]) @ u⇩_{2}" using 4 by blast also have "… = u" unfolding 2(1) by simp finally show ?thesis by this qed lemma le_fin_not_member': assumes "[a] ≼⇩_{F}u @ v" "a ∉ set u" shows "[a] ≼⇩_{F}v" proof - obtain w where 1: "[a] @ w =⇩_{F}u @ v" using assms(1) by rule have 3: "a ∈ set v" using assms by auto obtain v⇩_{1}v⇩_{2}where 4: "v = v⇩_{1}@ [a] @ v⇩_{2}" "a ∉ set v⇩_{1}" using split_list_first[OF 3] by auto have 5: "[a] @ w =⇩_{F}u @ v⇩_{1}@ [a] @ v⇩_{2}" using 1 unfolding 4(1) by this have 6: "Ind {a} (set (u @ v⇩_{1}))" proof (rule eq_fin_ind') show "[a] @ w =⇩_{F}(u @ v⇩_{1}) @ [a] @ v⇩_{2}" using 5 by simp show "a ∉ set (u @ v⇩_{1})" using assms(2) 4(2) by auto qed have 9: "Ind (set [a]) (set v⇩_{1})" using 6 by auto have "[a] ≤ [a] @ v⇩_{1}@ v⇩_{2}" by auto also have "… = ([a] @ v⇩_{1}) @ v⇩_{2}" by simp also have "… =⇩_{F}(v⇩_{1}@ [a]) @ v⇩_{2}" using 9 by blast also have "… = v⇩_{1}@ [a] @ v⇩_{2}" by simp also have "… = v" unfolding 4(1) by rule finally show ?thesis by this qed lemma le_fininf_not_member': assumes "[a] ≼⇩_{F}⇩_{I}u @- v" "a ∉ set u" shows "[a] ≼⇩_{F}⇩_{I}v" proof - obtain v⇩_{2}where 1: "v⇩_{2}≤⇩_{F}⇩_{I}u @- v" "[a] ≼⇩_{F}v⇩_{2}" using le_fininfE assms(1) by this show ?thesis using 1(1) proof (cases rule: prefix_fininf_append) case absorb have "[a] ≼⇩_{F}v⇩_{2}" using 1(2) by this also have "… ≤ u" using absorb by this finally have 2: "a ∈ set u" by force show ?thesis using assms(2) 2 by simp next case (extend z) have "[a] ≼⇩_{F}v⇩_{2}" using 1(2) by this also have "… = u @ z" using extend(1) by this finally have 2: "[a] ≼⇩_{F}u @ z" by this have "[a] ≼⇩_{F}z" using le_fin_not_member' 2 assms(2) by this also have "… ≤⇩_{F}⇩_{I}v" using extend(2) by this finally show ?thesis by this qed qed lemma le_fin_ind'': assumes "[a] ≼⇩_{F}w" "[b] ≼⇩_{F}w" "a ≠ b" shows "ind a b" proof - obtain u where 1: "[a] @ u =⇩_{F}w" using assms(1) by rule obtain v where 2: "[b] @ v =⇩_{F}w" using assms(2) by rule have 3: "[a] @ u =⇩_{F}[b] @ v" using 1 2[symmetric] by auto have 4: "a ∈ set v" using 3 assms(3) by (metis append_Cons append_Nil eq_fin_range list.set_intros(1) set_ConsD) obtain v⇩_{1}v⇩_{2}where 5: "v = v⇩_{1}@ [a] @ v⇩_{2}" "a ∉ set v⇩_{1}" using split_list_first[OF 4] by auto have 7: "Ind {a} (set ([b] @ v⇩_{1}))" proof (rule eq_fin_ind') show "[a] @ u =⇩_{F}([b] @ v⇩_{1}) @ [a] @ v⇩_{2}" using 3 unfolding 5(1) by simp show "a ∉ set ([b] @ v⇩_{1})" using assms(3) 5(2) by auto qed show ?thesis using 7 by auto qed lemma le_fin_ind': assumes "[a] ≼⇩_{F}w" "v ≼⇩_{F}w" "a ∉ set v" shows "Ind {a} (set v)" using assms proof (induct v arbitrary: w) case Nil show ?case by simp next case (Cons b v) have 1: "ind a b" proof (rule le_fin_ind'') show "[a] ≼⇩_{F}w" using Cons(2) by this show "[b] ≼⇩_{F}w" using Cons(3) by auto show "a ≠ b" using Cons(4) by auto qed obtain w' where 2: "[b] @ w' =⇩_{F}w" using Cons(3) by auto have 3: "Ind {a} (set v)" proof (rule Cons(1)) show "[a] ≼⇩_{F}w'" proof (rule le_fin_not_member') show "[a] ≼⇩_{F}[b] @ w'" using Cons(2) 2 by auto show "a ∉ set [b]" using Cons(4) by auto qed have "[b] @ v = b # v" by simp also have "… ≼⇩_{F}w" using Cons(3) by this also have "… =⇩_{F}[b] @ w'" using 2 by auto finally show "v ≼⇩_{F}w'" by blast show "a ∉ set v" using Cons(4) by auto qed show ?case using 1 3 by auto qed lemma le_fininf_ind'': assumes "[a] ≼⇩_{F}⇩_{I}w" "[b] ≼⇩_{F}⇩_{I}w" "a ≠ b" shows "ind a b" using subsume_fin le_fin_ind'' assms by metis lemma le_fininf_ind': assumes "[a] ≼⇩_{F}⇩_{I}w" "v ≼⇩_{F}⇩_{I}w" "a ∉ set v" shows "Ind {a} (set v)" using subsume_fin le_fin_ind' assms by metis lemma indoc_alt_def: "indoc a v ⟷ v =⇩_{F}[a] @ remove1 a v" proof assume 0: "indoc a v" obtain v⇩_{1}v⇩_{2}where 1: "v = v⇩_{1}@ [a] @ v⇩_{2}" "a ∉ set v⇩_{1}" "Ind {a} (set v⇩_{1})" using 0 unfolding indoc_def by blast have 2: "Ind (set [a]) (set v⇩_{1})" using 1(3) by simp have "v = v⇩_{1}@ [a] @ v⇩_{2}" using 1(1) by this also have "… = (v⇩_{1}@ [a]) @ v⇩_{2}" by simp also have "… =⇩_{F}([a] @ v⇩_{1}) @ v⇩_{2}" using 2 by blast also have "… = [a] @ v⇩_{1}@ v⇩_{2}" by simp also have "… = [a] @ remove1 a v" unfolding 1(1) remove1_append using 1(2) by auto finally show "v =⇩_{F}[a] @ remove1 a v" by this next assume 0: "v =⇩_{F}[a] @ remove1 a v" have 1: "indoc a ([a] @ remove1 a v)" by simp show "indoc a v" using eq_fin_indoc 0 1 by blast qed lemma levi_lemma: assumes "t @ u =⇩_{F}v @ w" obtains p r s q where "t =⇩_{F}p @ r" "u =⇩_{F}s @ q" "v =⇩_{F}p @ s" "w =⇩_{F}r @ q" "Ind (set r) (set s)" using assms proof (induct t arbitrary: thesis v w) case Nil show ?case proof (rule Nil(1)) show "[] =⇩_{F}[] @ []" by simp show "v =⇩_{F}[] @ v" by simp show "u =⇩_{F}v @ w" using Nil(2) by simp show "w =⇩_{F}[] @ w" by simp show "Ind (set []) (set v)" by simp qed next case (Cons a t') have 1: "[a] ≼⇩_{F}v @ w" using Cons(3) by blast show ?case proof (cases "a ∈ set v") case False have 2: "[a] ≼⇩_{F}w" using le_fin_not_member' 1 False by this obtain w' where 3: "w =⇩_{F}[a] @ w'" using 2 by blast have 4: "v ≼⇩_{F}v @ w" by auto have 5: "Ind (set [a]) (set v)" using le_fin_ind'[OF 1 4] False by simp have "[a] @ t' @ u = (a # t') @ u" by simp also have "… =⇩_{F}v @ w" using Cons(3) by this also have "… =⇩_{F}v @ [a] @ w'" using 3 by blast also have "… = (v @ [a]) @ w'" by simp also have "… =⇩_{F}([a] @ v) @ w'" using 5 by blast also have "… = [a] @ v @ w'" by simp finally have 6: "t' @ u =⇩_{F}v @ w'" by blast obtain p r' s q where 7: "t' =⇩_{F}p @ r'" "u =⇩_{F}s @ q" "v =⇩_{F}p @ s" "w' =⇩_{F}r' @ q" "Ind (set r') (set s)" using Cons(1)[OF _ 6] by this have 8: "set v = set p ∪ set s" using eq_fin_range 7(3) by auto have 9: "Ind (set [a]) (set p)" using 5 8 by auto have 10: "Ind (set [a]) (set s)" using 5 8 by auto show ?thesis proof (rule Cons(2)) have "a # t' = [a] @ t'" by simp also have "… =⇩_{F}[a] @ p @ r'" using 7(1) by blast also have "… = ([a] @ p) @ r'" by simp also have "… =⇩_{F}(p @ [a]) @ r'" using 9 by blast also have "… = p @ [a] @ r'" by simp finally show "a # t' =⇩_{F}p @ [a] @ r'" by this show "u =⇩_{F}s @ q" using 7(2) by this show "v =⇩_{F}p @ s" using 7(3) by this have "w =⇩_{F}[a] @ w'" using 3 by this also have "… =⇩_{F}[a] @ r' @ q" using 7(4) by blast also have "… = ([a] @ r') @ q" by simp finally show "w =⇩_{F}([a] @ r') @ q" by this show "Ind (set ([a] @ r')) (set s)" using 7(5) 10 by auto qed next case True have 2: "[a] ≼⇩_{F}v" using le_fin_member' 1 True by this obtain v' where 3: "v =⇩_{F}[a] @ v'" using 2 by blast have "[a] @ t' @ u = (a # t') @ u" by simp also have "… =⇩_{F}v @ w" using Cons(3) by this also have "… =⇩_{F}([a] @ v') @ w" using 3 by blast also have "… = [a] @ v' @ w" by simp finally have 4: "t' @ u =⇩_{F}v' @ w" by blast obtain p' r s q where 7: "t' =⇩_{F}p' @ r" "u =⇩_{F}s @ q" "v' =⇩_{F}p' @ s" "w =⇩_{F}r @ q" "Ind (set r) (set s)" using Cons(1)[OF _ 4] by this show ?thesis proof (rule Cons(2)) have "a # t' = [a] @ t'" by simp also have "… =⇩_{F}[a] @ p' @ r" using 7(1) by blast also have "… = ([a] @ p') @ r" by simp finally show "a # t' =⇩_{F}([a] @ p') @ r" by this show "u =⇩_{F}s @ q" using 7(2) by this have "v =⇩_{F}[a] @ v'" using 3 by this also have "… =⇩_{F}[a] @ p' @ s" using 7(3) by blast also have "… = ([a] @ p') @ s" by simp finally show "v =⇩_{F}([a] @ p') @ s" by this show "w =⇩_{F}r @ q" using 7(4) by this show "Ind (set r) (set s)" using 7(5) by this qed qed qed end end