# Theory List_Prefixes

section ‹List Prefixes› theory List_Prefixes imports "HOL-Library.Prefix_Order" begin lemmas [intro] = prefixI strict_prefixI[folded less_eq_list_def] lemmas [elim] = prefixE strict_prefixE[folded less_eq_list_def] lemmas [intro?] = take_is_prefix[folded less_eq_list_def] hide_const (open) Sublist.prefix Sublist.suffix lemma prefix_finI_item[intro!]: assumes "a = b" "u ≤ v" shows "a # u ≤ b # v" using assms by force lemma prefix_finE_item[elim!]: assumes "a # u ≤ b # v" obtains "a = b" "u ≤ v" using assms by force lemma prefix_fin_append[intro]: "u ≤ u @ v" by auto lemma pprefix_fin_length[dest]: assumes "u < v" shows "length u < length v" proof - obtain a w where 1: "v = u @ a # w" using assms by rule show ?thesis unfolding 1 by simp qed end

# Theory List_Extensions

section ‹Lists› theory List_Extensions imports "HOL-Library.Sublist" begin declare remove1_idem[simp] lemma nth_append_simps[simp]: "i < length xs ⟹ (xs @ ys) ! i = xs ! i" "i ≥ length xs ⟹ (xs @ ys) ! i = ys ! (i - length xs)" unfolding nth_append by simp+ notation zip (infixr "||" 51) abbreviation "project A ≡ filter (λ a. a ∈ A)" abbreviation "select s w ≡ nths w s" lemma map_plus[simp]: "map (plus n) [i ..< j] = [i + n ..< j + n]" proof (induct n) case 0 show ?case by simp next case (Suc n) have "map (plus (Suc n)) [i ..< j] = map (Suc ∘ plus n) [i ..< j]" by simp also have "… = (map Suc ∘ map (plus n)) [i ..< j]" by simp also have "… = map Suc (map (plus n) [i ..< j])" by simp also have "… = map Suc [i + n ..< j + n]" unfolding Suc by simp also have "… = [Suc (i + n) ..< Suc (j + n)]" unfolding map_Suc_upt by simp also have "… = [i + Suc n ..< j + Suc n]" by simp finally show ?case by this qed lemma singleton_list_lengthE[elim]: assumes "length xs = 1" obtains x where "xs = [x]" proof - have 0: "length xs = Suc 0" using assms by simp obtain y ys where 1: "xs = y # ys" "length ys = 0" using 0 Suc_length_conv by metis show ?thesis using that 1 by blast qed lemma singleton_hd_last: "length xs = 1 ⟹ hd xs = last xs" by fastforce lemma set_subsetI[intro]: assumes "⋀ i. i < length xs ⟹ xs ! i ∈ S" shows "set xs ⊆ S" proof fix x assume 0: "x ∈ set xs" obtain i where 1: "i < length xs" "x = xs ! i" using 0 unfolding in_set_conv_nth by blast show "x ∈ S" using assms(1) 1 by auto qed lemma hd_take[simp]: assumes "n ≠ 0" "xs ≠ []" shows "hd (take n xs) = hd xs" proof - have 1: "take n xs ≠ []" using assms by simp have 2: "0 < n" using assms by simp have "hd (take n xs) = take n xs ! 0" using hd_conv_nth[OF 1] by this also have "… = xs ! 0" using nth_take[OF 2] by this also have "… = hd xs" using hd_conv_nth[OF assms(2)] by simp finally show ?thesis by this qed lemma hd_drop[simp]: assumes "n < length xs" shows "hd (drop n xs) = xs ! n" using hd_drop_conv_nth assms by this lemma last_take[simp]: assumes "n < length xs" shows "last (take (Suc n) xs) = xs ! n" using assms proof (induct xs arbitrary: n) case (Nil) show ?case using Nil by simp next case (Cons x xs) show ?case using Cons by (auto) (metis Suc_less_eq Suc_pred) qed lemma split_list_first_unique: assumes "u⇩_{1}@ [a] @ u⇩_{2}= v⇩_{1}@ [a] @ v⇩_{2}" "a ∉ set u⇩_{1}" "a ∉ set v⇩_{1}" shows "u⇩_{1}= v⇩_{1}" proof - obtain w where "u⇩_{1}= v⇩_{1}@ w ∧ w @ [a] @ u⇩_{2}= [a] @ v⇩_{2}∨ u⇩_{1}@ w = v⇩_{1}∧ [a] @ u⇩_{2}= w @ [a] @ v⇩_{2}" using assms(1) append_eq_append_conv2 by blast thus ?thesis using assms(2, 3) by (auto) (metis hd_append2 list.sel(1) list.set_sel(1))+ qed end

# Theory Word_Prefixes

section ‹Finite Prefixes of Infinite Sequences› theory Word_Prefixes imports List_Prefixes "../Extensions/List_Extensions" Transition_Systems_and_Automata.Sequence begin definition prefix_fininf :: "'a list ⇒ 'a stream ⇒ bool" (infix "≤⇩_{F}⇩_{I}" 50) where "u ≤⇩_{F}⇩_{I}v ≡ ∃ w. u @- w = v" lemma prefix_fininfI[intro]: assumes "u @- w = v" shows "u ≤⇩_{F}⇩_{I}v" using assms unfolding prefix_fininf_def by auto lemma prefix_fininfE[elim]: assumes "u ≤⇩_{F}⇩_{I}v" obtains w where "v = u @- w" using assms unfolding prefix_fininf_def by auto lemma prefix_fininfI_empty[intro!]: "[] ≤⇩_{F}⇩_{I}w" by force lemma prefix_fininfI_item[intro!]: assumes "a = b" "u ≤⇩_{F}⇩_{I}v" shows "a # u ≤⇩_{F}⇩_{I}b ## v" using assms by force lemma prefix_fininfE_item[elim!]: assumes "a # u ≤⇩_{F}⇩_{I}b ## v" obtains "a = b" "u ≤⇩_{F}⇩_{I}v" using assms by force lemma prefix_fininf_item[simp]: "a # u ≤⇩_{F}⇩_{I}a ## v ⟷ u ≤⇩_{F}⇩_{I}v" by force lemma prefix_fininf_list[simp]: "w @ u ≤⇩_{F}⇩_{I}w @- v ⟷ u ≤⇩_{F}⇩_{I}v" by (induct w, auto) lemma prefix_fininf_conc[intro]: "u ≤⇩_{F}⇩_{I}u @- v" by auto lemma prefix_fininf_prefix[intro]: "stake k w ≤⇩_{F}⇩_{I}w" using stake_sdrop by blast lemma prefix_fininf_set_range[dest]: "u ≤⇩_{F}⇩_{I}v ⟹ set u ⊆ sset v" by auto lemma prefix_fininf_absorb: assumes "u ≤⇩_{F}⇩_{I}v @- w" "length u ≤ length v" shows "u ≤ v" proof - obtain x where 1: "u @- x = v @- w" using assms(1) by auto have "u ≤ u @ stake (length v - length u) x" by rule also have "… = stake (length v) (u @- x)" using assms(2) by (simp add: stake_shift) also have "… = stake (length v) (v @- w)" unfolding 1 by rule also have "… = v" using eq_shift by blast finally show ?thesis by this qed lemma prefix_fininf_extend: assumes "u ≤⇩_{F}⇩_{I}v @- w" "length v ≤ length u" shows "v ≤ u" proof - obtain x where 1: "u @- x = v @- w" using assms(1) by auto have "v ≤ v @ stake (length u - length v) w" by rule also have "… = stake (length u) (v @- w)" using assms(2) by (simp add: stake_shift) also have "… = stake (length u) (u @- x)" unfolding 1 by rule also have "… = u" using eq_shift by blast finally show ?thesis by this qed lemma prefix_fininf_length: assumes "u ≤⇩_{F}⇩_{I}w" "v ≤⇩_{F}⇩_{I}w" "length u ≤ length v" shows "u ≤ v" proof - obtain u' v' where 1: "w = u @- u'" "w = v @- v'" using assms(1, 2) by blast+ have "u = stake (length u) (u @- u')" using shift_eq by blast also have "… = stake (length u) w" unfolding 1(1) by rule also have "… = stake (length u) (v @- v')" unfolding 1(2) by rule also have "… = take (length u) v" using assms by (simp add: min.absorb2 stake_append) also have "… ≤ v" by rule finally show ?thesis by this qed lemma prefix_fininf_append: assumes "u ≤⇩_{F}⇩_{I}v @- w" obtains (absorb) "u ≤ v" | (extend) z where "u = v @ z" "z ≤⇩_{F}⇩_{I}w" proof (cases "length u" "length v" rule: le_cases) case le obtain x where 1: "u @- x = v @- w" using assms(1) by auto show ?thesis proof (rule absorb) have "u ≤ u @ stake (length v - length u) x" by rule also have "… = stake (length v) (u @- x)" using le by (simp add: stake_shift) also have "… = stake (length v) (v @- w)" unfolding 1 by rule also have "… = v" using eq_shift by blast finally show "u ≤ v" by this qed next case ge obtain x where 1: "u @- x = v @- w" using assms(1) by auto show ?thesis proof (rule extend) have "u = stake (length u) (u @- x)" using shift_eq by auto also have "… = stake (length u) (v @- w)" unfolding 1 by rule also have "… = v @ stake (length u - length v) w" using ge by (simp add: stake_shift) finally show "u = v @ stake (length u - length v) w" by this show "stake (length u - length v) w ≤⇩_{F}⇩_{I}w" by rule qed qed lemma prefix_fin_prefix_fininf_trans[trans, intro]: "u ≤ v ⟹ v ≤⇩_{F}⇩_{I}w ⟹ u ≤⇩_{F}⇩_{I}w" by (metis Prefix_Order.prefixE prefix_fininf_def shift_append) lemma prefix_finE_nth: assumes "u ≤ v" "i < length u" shows "u ! i = v ! i" proof - obtain w where 1: "v = u @ w" using assms(1) by auto show ?thesis unfolding 1 using assms(2) by (simp add: nth_append) qed lemma prefix_fininfI_nth: assumes "⋀ i. i < length u ⟹ u ! i = w !! i" shows "u ≤⇩_{F}⇩_{I}w" proof (rule prefix_fininfI) show "u @- sdrop (length u) w = w" by (simp add: assms list_eq_iff_nth_eq shift_eq) qed definition chain :: "(nat ⇒ 'a list) ⇒ bool" where "chain w ≡ mono w ∧ (∀ k. ∃ l. k < length (w l))" definition limit :: "(nat ⇒ 'a list) ⇒ 'a stream" where "limit w ≡ smap (λ k. w (SOME l. k < length (w l)) ! k) nats" lemma chainI[intro?]: assumes "mono w" assumes "⋀ k. ∃ l. k < length (w l)" shows "chain w" using assms unfolding chain_def by auto lemma chainD_mono[dest?]: assumes "chain w" shows "mono w" using assms unfolding chain_def by auto lemma chainE_length[elim?]: assumes "chain w" obtains l where "k < length (w l)" using assms unfolding chain_def by auto lemma chain_prefix_limit: assumes "chain w" shows "w k ≤⇩_{F}⇩_{I}limit w" proof (rule prefix_fininfI_nth) fix i assume 1: "i < length (w k)" have 2: "mono w" "⋀ k. ∃ l. k < length (w l)" using chainD_mono chainE_length assms by blast+ have 3: "i < length (w (SOME l. i < length (w l)))" using someI_ex 2(2) by this show "w k ! i = limit w !! i" proof (cases "k" "SOME l. i < length (w l)" rule: le_cases) case (le) have 4: "w k ≤ w (SOME l. i < length (w l))" using monoD 2(1) le by this show ?thesis unfolding limit_def using prefix_finE_nth 4 1 by auto next case (ge) have 4: "w (SOME l. i < length (w l)) ≤ w k" using monoD 2(1) ge by this show ?thesis unfolding limit_def using prefix_finE_nth 4 3 by auto qed qed lemma chain_construct_1: assumes "P 0 x⇩_{0}" "⋀ k x. P k x ⟹ ∃ x'. P (Suc k) x' ∧ f x ≤ f x'" assumes "⋀ k x. P k x ⟹ k ≤ length (f x)" obtains Q where "⋀ k. P k (Q k)" "chain (f ∘ Q)" proof - obtain x' where 1: "P 0 x⇩_{0}" "⋀ k x. P k x ⟹ P (Suc k) (x' k x) ∧ f x ≤ f (x' k x)" using assms(1, 2) by metis define Q where "Q ≡ rec_nat x⇩_{0}x'" have [simp]: "Q 0 = x⇩_{0}" "⋀ k. Q (Suc k) = x' k (Q k)" unfolding Q_def by simp+ have 2: "⋀ k. P k (Q k)" proof - fix k show "P k (Q k)" using 1 by (induct k, auto) qed show ?thesis proof (intro that chainI monoI, unfold comp_apply) fix k show "P k (Q k)" using 2 by this next fix x y :: nat assume "x ≤ y" thus "f (Q x) ≤ f (Q y)" proof (induct "y - x" arbitrary: x y) case 0 show ?case using 0 by simp next case (Suc k) have "f (Q x) ≤ f (Q (Suc x))" using 1(2) 2 by auto also have "… ≤ f (Q y)" using Suc(2) by (intro Suc(1), auto) finally show ?case by this qed next fix k have 3: "P (Suc k) (Q (Suc k))" using 2 by this have 4: "Suc k ≤ length (f (Q (Suc k)))" using assms(3) 3 by this have 5: "k < length (f (Q (Suc k)))" using 4 by auto show "∃ l. k < length (f (Q l))" using 5 by blast qed qed lemma chain_construct_2: assumes "P 0 x⇩_{0}" "⋀ k x. P k x ⟹ ∃ x'. P (Suc k) x' ∧ f x ≤ f x' ∧ g x ≤ g x'" assumes "⋀ k x. P k x ⟹ k ≤ length (f x)" "⋀ k x. P k x ⟹ k ≤ length (g x)" obtains Q where "⋀ k. P k (Q k)" "chain (f ∘ Q)" "chain (g ∘ Q)" proof - obtain x' where 1: "P 0 x⇩_{0}" "⋀ k x. P k x ⟹ P (Suc k) (x' k x) ∧ f x ≤ f (x' k x) ∧ g x ≤ g (x' k x)" using assms(1, 2) by metis define Q where "Q ≡ rec_nat x⇩_{0}x'" have [simp]: "Q 0 = x⇩_{0}" "⋀ k. Q (Suc k) = x' k (Q k)" unfolding Q_def by simp+ have 2: "⋀ k. P k (Q k)" proof - fix k show "P k (Q k)" using 1 by (induct k, auto) qed show ?thesis proof (intro that chainI monoI, unfold comp_apply) fix k show "P k (Q k)" using 2 by this next fix x y :: nat assume "x ≤ y" thus "f (Q x) ≤ f (Q y)" proof (induct "y - x" arbitrary: x y) case 0 show ?case using 0 by simp next case (Suc k) have "f (Q x) ≤ f (Q (Suc x))" using 1(2) 2 by auto also have "… ≤ f (Q y)" using Suc(2) by (intro Suc(1), auto) finally show ?case by this qed next fix k have 3: "P (Suc k) (Q (Suc k))" using 2 by this have 4: "Suc k ≤ length (f (Q (Suc k)))" using assms(3) 3 by this have 5: "k < length (f (Q (Suc k)))" using 4 by auto show "∃ l. k < length (f (Q l))" using 5 by blast next fix x y :: nat assume "x ≤ y" thus "g (Q x) ≤ g (Q y)" proof (induct "y - x" arbitrary: x y) case 0 show ?case using 0 by simp next case (Suc k) have "g (Q x) ≤ g (Q (Suc x))" using 1(2) 2 by auto also have "… ≤ g (Q y)" using Suc(2) by (intro Suc(1), auto) finally show ?case by this qed next fix k have 3: "P (Suc k) (Q (Suc k))" using 2 by this have 4: "Suc k ≤ length (g (Q (Suc k)))" using assms(4) 3 by this have 5: "k < length (g (Q (Suc k)))" using 4 by auto show "∃ l. k < length (g (Q l))" using 5 by blast qed qed lemma chain_construct_2': assumes "P 0 u⇩_{0}v⇩_{0}" "⋀ k u v. P k u v ⟹ ∃ u' v'. P (Suc k) u' v' ∧ u ≤ u' ∧ v ≤ v'" assumes "⋀ k u v. P k u v ⟹ k ≤ length u" "⋀ k u v. P k u v ⟹ k ≤ length v" obtains u v where "⋀ k. P k (u k) (v k)" "chain u" "chain v" proof - obtain Q where 1: "⋀ k. (case_prod ∘ P) k (Q k)" "chain (fst ∘ Q)" "chain (snd ∘ Q)" proof (rule chain_construct_2) show "∃ x'. (case_prod ∘ P) (Suc k) x' ∧ fst x ≤ fst x' ∧ snd x ≤ snd x'" if "(case_prod ∘ P) k x" for k x using assms that by auto show "(case_prod ∘ P) 0 (u⇩_{0}, v⇩_{0})" using assms by auto show "k ≤ length (fst x)" if "(case_prod ∘ P) k x" for k x using assms that by auto show "k ≤ length (snd x)" if "(case_prod ∘ P) k x" for k x using assms that by auto qed rule show ?thesis proof show "P k ((fst ∘ Q) k) ((snd ∘ Q) k)" for k using 1(1) by (auto simp: prod.case_eq_if) show "chain (fst ∘ Q)" "chain (snd ∘ Q)" using 1(2, 3) by this qed qed end

# Theory Set_Extensions

section ‹Sets› theory Set_Extensions imports "HOL-Library.Infinite_Set" begin declare finite_subset[intro] lemma set_not_emptyI[intro 0]: "x ∈ S ⟹ S ≠ {}" by auto lemma sets_empty_iffI[intro 0]: assumes "⋀ a. a ∈ A ⟹ ∃ b. b ∈ B" assumes "⋀ b. b ∈ B ⟹ ∃ a. a ∈ A" shows "A = {} ⟷ B = {}" using assms by auto lemma disjointI[intro 0]: assumes "⋀ x. x ∈ A ⟹ x ∈ B ⟹ False" shows "A ∩ B = {}" using assms by auto lemma range_subsetI[intro 0]: assumes "⋀ x. f x ∈ S" shows "range f ⊆ S" using assms by blast lemma finite_imageI_range: assumes "finite (range f)" shows "finite (f ` A)" using finite_subset image_mono subset_UNIV assms by metis lemma inf_img_fin_domE': assumes "infinite A" assumes "finite (f ` A)" obtains y where "y ∈ f ` A" "infinite (A ∩ f -` {y})" proof (rule ccontr) assume 1: "¬ thesis" have 2: "finite (⋃ y ∈ f ` A. A ∩ f -` {y})" proof (rule finite_UN_I) show "finite (f ` A)" using assms(2) by this show "⋀ y. y ∈ f ` A ⟹ finite (A ∩ f -` {y})" using that 1 by blast qed have 3: "A ⊆ (⋃ y ∈ f ` A. A ∩ f -` {y})" by blast show False using assms(1) 2 3 by blast qed lemma vimage_singleton[simp]: "f -` {y} = {x. f x = y}" unfolding vimage_def by simp lemma these_alt_def: "Option.these S = Some -` S" unfolding Option.these_def by force lemma the_vimage_subset: "the -` {a} ⊆ {None, Some a}" by auto lemma finite_induct_reverse[consumes 1, case_names remove]: assumes "finite S" assumes "⋀ S. finite S ⟹ (⋀ x. x ∈ S ⟹ P (S - {x})) ⟹ P S" shows "P S" using assms(1) proof (induct rule: finite_psubset_induct) case (psubset S) show ?case proof (rule assms(2)) show "finite S" using psubset(1) by this next fix x assume 0: "x ∈ S" show "P (S - {x})" proof (rule psubset(2)) show "S - {x} ⊂ S" using 0 by auto qed qed qed lemma zero_not_in_Suc_image[simp]: "0 ∉ Suc ` A" by auto lemma Collect_split_Suc: "¬ P 0 ⟹ {i. P i} = Suc ` {i. P (Suc i)}" "P 0 ⟹ {i. P i} = {0} ∪ Suc ` {i. P (Suc i)}" proof - assume "¬ P 0" thus "{i. P i} = Suc ` {i. P (Suc i)}" by (auto, metis image_eqI mem_Collect_eq nat.exhaust) next assume "P 0" thus "{i. P i} = {0} ∪ Suc ` {i. P (Suc i)}" by (auto, metis imageI mem_Collect_eq not0_implies_Suc) qed lemma Collect_subsume[simp]: assumes "⋀ x. x ∈ A ⟹ P x" shows "{x ∈ A. P x} = A" using assms unfolding simp_implies_def by auto lemma Max_ge': assumes "finite A" "A ≠ {}" assumes "b ∈ A" "a ≤ b" shows "a ≤ Max A" using assms Max_ge_iff by auto abbreviation "least A ≡ LEAST k. k ∈ A" lemma least_contains[intro?, simp]: fixes A :: "'a :: wellorder set" assumes "k ∈ A" shows "least A ∈ A" using assms by (metis LeastI) lemma least_contains'[intro?, simp]: fixes A :: "'a :: wellorder set" assumes "A ≠ {}" shows "least A ∈ A" using assms by (metis LeastI equals0I) lemma least_least[intro?, simp]: fixes A :: "'a :: wellorder set" assumes "k ∈ A" shows "least A ≤ k" using assms by (metis Least_le) lemma least_unique: fixes A :: "'a :: wellorder set" assumes "k ∈ A" "k ≤ least A" shows "k = least A" using assms by (metis Least_le antisym) lemma least_not_less: fixes A :: "'a :: wellorder set" assumes "k < least A" shows "k ∉ A" using assms by (metis not_less_Least) lemma leastI2_order[simp]: fixes A :: "'a :: wellorder set" assumes "A ≠ {}" "⋀ k. k ∈ A ⟹ (⋀ l. l ∈ A ⟹ k ≤ l) ⟹ P k" shows "P (least A)" proof (rule LeastI2_order) show "least A ∈ A" using assms(1) by rule next fix k assume 1: "k ∈ A" show "least A ≤ k" using 1 by rule next fix k assume 1: "k ∈ A" "∀ l. l ∈ A ⟶ k ≤ l" show "P k" using assms(2) 1 by auto qed lemma least_singleton[simp]: fixes a :: "'a :: wellorder" shows "least {a} = a" by (metis insert_not_empty least_contains' singletonD) lemma least_image[simp]: fixes f :: "'a :: wellorder ⇒ 'b :: wellorder" assumes "A ≠ {}" "⋀ k l. k ∈ A ⟹ l ∈ A ⟹ k ≤ l ⟹ f k ≤ f l" shows "least (f ` A) = f (least A)" proof (rule leastI2_order) show "A ≠ {}" using assms(1) by this next fix k assume 1: "k ∈ A" "⋀ i. i ∈ A ⟹ k ≤ i" show "least (f ` A) = f k" proof (rule leastI2_order) show "f ` A ≠ {}" using assms(1) by simp next fix l assume 2: "l ∈ f ` A" "⋀ i. i ∈ f ` A ⟹ l ≤ i" show "l = f k" using assms(2) 1 2 by force qed qed lemma least_le: fixes A B :: "'a :: wellorder set" assumes "B ≠ {}" assumes "⋀ i. i ≤ least A ⟹ i ≤ least B ⟹ i ∈ B ⟹ i ∈ A" shows "least A ≤ least B" proof (rule ccontr) assume 1: "¬ least A ≤ least B" have 2: "least B ∈ A" using assms(1, 2) 1 by simp have 3: "least A ≤ least B" using 2 by rule show False using 1 3 by rule qed lemma least_eq: fixes A B :: "'a :: wellorder set" assumes "A ≠ {}" "B ≠ {}" assumes "⋀ i. i ≤ least A ⟹ i ≤ least B ⟹ i ∈ A ⟷ i ∈ B" shows "least A = least B" using assms by (auto intro: antisym least_le) lemma least_Suc[simp]: assumes "A ≠ {}" shows "least (Suc ` A) = Suc (least A)" proof (rule antisym) obtain k where 10: "k ∈ A" using assms by blast have 11: "Suc k ∈ Suc ` A" using 10 by auto have 20: "least A ∈ A" using 10 LeastI by metis have 21: "least (Suc ` A) ∈ Suc ` A" using 11 LeastI by metis have 30: "⋀ l. l ∈ A ⟹ least A ≤ l" using 10 Least_le by metis have 31: "⋀ l. l ∈ Suc ` A ⟹ least (Suc ` A) ≤ l" using 11 Least_le by metis show "least (Suc ` A) ≤ Suc (least A)" using 20 31 by auto show "Suc (least A) ≤ least (Suc ` A)" using 21 30 by auto qed lemma least_Suc_diff[simp]: "Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})" proof (cases "A = {}") case True show ?thesis unfolding True by simp next case False have "Suc ` A - {least (Suc ` A)} = Suc ` A - {Suc (least A)}" using False by simp also have "… = Suc ` A - Suc ` {least A}" by simp also have "… = Suc ` (A - {least A})" by blast finally show ?thesis by this qed lemma Max_diff_least[simp]: fixes A :: "'a :: wellorder set" assumes "finite A" "A - {least A} ≠ {}" shows "Max (A - {least A}) = Max A" proof - have 1: "least A ∈ A" using assms(2) by auto obtain a where 2: "a ∈ A - {least A}" using assms(2) by blast have "Max A = Max (insert (least A) (A - {least A}))" using insert_absorb 1 by force also have "… = max (least A) (Max (A - {least A}))" proof (rule Max_insert) show "finite (A - {least A})" using assms(1) by auto show "A - {least A} ≠ {}" using assms(2) by this qed also have "… = Max (A - {least A})" proof (rule max_absorb2, rule Max_ge') show "finite (A - {least A})" using assms(1) by auto show "A - {least A} ≠ {}" using assms(2) by this show "a ∈ A - {least A}" using 2 by this show "least A ≤ a" using 2 by simp qed finally show ?thesis by rule qed lemma nat_set_card_equality_less: fixes A :: "nat set" assumes "x ∈ A" "y ∈ A" "card {z ∈ A. z < x} = card {z ∈ A. z < y}" shows "x = y" proof (cases x y rule: linorder_cases) case less have 0: "finite {z ∈ A. z < y}" by simp have 1: "{z ∈ A. z < x} ⊂ {z ∈ A. z < y}" using assms(1, 2) less by force have 2: "card {z ∈ A. z < x} < card {z ∈ A. z < y}" using psubset_card_mono 0 1 by this show ?thesis using assms(3) 2 by simp next case equal show ?thesis using equal by this next case greater have 0: "finite {z ∈ A. z < x}" by simp have 1: "{z ∈ A. z < y} ⊂ {z ∈ A. z < x}" using assms(1, 2) greater by force have 2: "card {z ∈ A. z < y} < card {z ∈ A. z < x}" using psubset_card_mono 0 1 by this show ?thesis using assms(3) 2 by simp qed lemma nat_set_card_equality_le: fixes A :: "nat set" assumes "x ∈ A" "y ∈ A" "card {z ∈ A. z ≤ x} = card {z ∈ A. z ≤ y}" shows "x = y" proof (cases x y rule: linorder_cases) case less have 0: "finite {z ∈ A. z ≤ y}" by simp have 1: "{z ∈ A. z ≤ x} ⊂ {z ∈ A. z ≤ y}" using assms(1, 2) less by force have 2: "card {z ∈ A. z ≤ x} < card {z ∈ A. z ≤ y}" using psubset_card_mono 0 1 by this show ?thesis using assms(3) 2 by simp next case equal show ?thesis using equal by this next case greater have 0: "finite {z ∈ A. z ≤ x}" by simp have 1: "{z ∈ A. z ≤ y} ⊂ {z ∈ A. z ≤ x}" using assms(1, 2) greater by force have 2: "card {z ∈ A. z ≤ y} < card {z ∈ A. z ≤ x}" using psubset_card_mono 0 1 by this show ?thesis using assms(3) 2 by simp qed lemma nat_set_card_mono[simp]: fixes A :: "nat set" assumes "x ∈ A" shows "card {z ∈ A. z < x} < card {z ∈ A. z < y} ⟷ x < y" proof assume 1: "card {z ∈ A. z < x} < card {z ∈ A. z < y}" show "x < y" proof (rule ccontr) assume 2: "¬ x < y" have 3: "card {z ∈ A. z < y} ≤ card {z ∈ A. z < x}" using 2 by (auto intro: card_mono) show "False" using 1 3 by simp qed next assume 1: "x < y" show "card {z ∈ A. z < x} < card {z ∈ A. z < y}" proof (intro psubset_card_mono psubsetI) show "finite {z ∈ A. z < y}" by simp show "{z ∈ A. z < x} ⊆ {z ∈ A. z < y}" using 1 by auto show "{z ∈ A. z < x} ≠ {z ∈ A. z < y}" using assms 1 by blast qed qed lemma card_one[elim]: assumes "card A = 1" obtains a where "A = {a}" using assms by (metis One_nat_def card_Suc_eq) lemma image_alt_def: "f ` A = {f x |x. x ∈ A}" by auto lemma supset_mono_inductive[mono]: assumes "⋀ x. x ∈ B ⟶ x ∈ C" shows "A ⊆ B ⟶ A ⊆ C" using assms by auto lemma Collect_mono_inductive[mono]: assumes "⋀ x. P x ⟶ Q x" shows "x ∈ {x. P x} ⟶ x ∈ {x. Q x}" using assms by auto lemma image_union_split: assumes "f ` (A ∪ B) = g ` C" obtains D E where "f ` A = g ` D" "f ` B = g ` E" "D ⊆ C" "E ⊆ C" using assms unfolding image_Un by (metis (erased, lifting) inf_sup_ord(3) inf_sup_ord(4) subset_imageE) lemma image_insert_split: assumes "inj g" "f ` insert a B = g ` C" obtains d E where "f a = g d" "f ` B = g ` E" "d ∈ C" "E ⊆ C" proof - have 1: "f ` ({a} ∪ B) = g ` C" using assms(2) by simp obtain D E where 2: "f ` {a} = g ` D" "f ` B = g ` E" "D ⊆ C" "E ⊆ C" using image_union_split 1 by this obtain d where 3: "D = {d}" using assms(1) 2(1) by (auto, metis (erased, hide_lams) imageE image_empty image_insert inj_image_eq_iff singletonI) show ?thesis using that 2 unfolding 3 by simp qed end

# Theory Basic_Extensions

section ‹Basics› theory Basic_Extensions imports "HOL-Library.Infinite_Set" begin subsection ‹Types› type_synonym 'a step = "'a ⇒ 'a" subsection ‹Rules› declare less_imp_le[dest, simp] declare le_funI[intro] declare le_funE[elim] declare le_funD[dest] lemma IdI'[intro]: assumes "x = y" shows "(x, y) ∈ Id" using assms by auto lemma (in order) order_le_cases: assumes "x ≤ y" obtains (eq) "x = y" | (lt) "x < y" using assms le_less by auto lemma (in linorder) linorder_cases': obtains (le) "x ≤ y" | (gt) "x > y" by force lemma monoI_comp[intro]: assumes "mono f" "mono g" shows "mono (f ∘ g)" using assms by (intro monoI, auto dest: monoD) lemma strict_monoI_comp[intro]: assumes "strict_mono f" "strict_mono g" shows "strict_mono (f ∘ g)" using assms by (intro strict_monoI, auto dest: strict_monoD) lemma eq_le_absorb[simp]: fixes x y :: "'a :: order" shows "x = y ∧ x ≤ y ⟷ x = y" "x ≤ y ∧ x = y ⟷ x = y" by auto lemma INFM_Suc[simp]: "(∃⇩_{∞}i. P (Suc i)) ⟷ (∃⇩_{∞}i. P i)" unfolding INFM_nat using Suc_lessE less_Suc_eq by metis lemma INFM_plus[simp]: "(∃⇩_{∞}i. P (i + n :: nat)) ⟷ (∃⇩_{∞}i. P i)" proof (induct n) case 0 show ?case by simp next case (Suc n) have "(∃⇩_{∞}i. P (i + Suc n)) ⟷ (∃⇩_{∞}i. P (Suc i + n))" by simp also have "… ⟷ (∃⇩_{∞}i. P (i + n))" using INFM_Suc by this also have "… ⟷ (∃⇩_{∞}i. P i)" using Suc by this finally show ?case by this qed lemma INFM_minus[simp]: "(∃⇩_{∞}i. P (i - n :: nat)) ⟷ (∃⇩_{∞}i. P i)" proof (induct n) case 0 show ?case by simp next case (Suc n) have "(∃⇩_{∞}i. P (i - Suc n)) ⟷ (∃⇩_{∞}i. P (Suc i - Suc n))" using INFM_Suc by meson also have "… ⟷ (∃⇩_{∞}i. P (i - n))" by simp also have "… ⟷ (∃⇩_{∞}i. P i)" using Suc by this finally show ?case by this qed subsection ‹Constants› definition const :: "'a ⇒ 'b ⇒ 'a" where "const x ≡ λ _. x" definition const2 :: "'a ⇒ 'b ⇒ 'c ⇒ 'a" where "const2 x ≡ λ _ _. x" definition const3 :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'a" where "const3 x ≡ λ _ _ _. x" definition const4 :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'a" where "const4 x ≡ λ _ _ _ _. x" definition const5 :: "'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ 'a" where "const5 x ≡ λ _ _ _ _ _. x" lemma const_apply[simp]: "const x y = x" unfolding const_def by rule lemma const2_apply[simp]: "const2 x y z = x" unfolding const2_def by rule lemma const3_apply[simp]: "const3 x y z u = x" unfolding const3_def by rule lemma const4_apply[simp]: "const4 x y z u v = x" unfolding const4_def by rule lemma const5_apply[simp]: "const5 x y z u v w = x" unfolding const5_def by rule definition zip_fun :: "('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ 'a ⇒ 'b × 'c" (infixr "∥" 51) where "f ∥ g ≡ λ x. (f x, g x)" lemma zip_fun_simps[simp]: "(f ∥ g) x = (f x, g x)" "fst ∘ (f ∥ g) = f" "snd ∘ (f ∥ g) = g" "fst ∘ h ∥ snd ∘ h = h" "fst ` range (f ∥ g) = range f" "snd ` range (f ∥ g) = range g" unfolding zip_fun_def by force+ lemma zip_fun_eq[dest]: assumes "f ∥ g = h ∥ i" shows "f = h" "g = i" using assms unfolding zip_fun_def by (auto dest: fun_cong) lemma zip_fun_range_subset[intro, simp]: "range (f ∥ g) ⊆ range f × range g" unfolding zip_fun_def by blast lemma zip_fun_range_finite[elim]: assumes "finite (range (f ∥ g))" obtains "finite (range f)" "finite (range g)" proof show "finite (range f)" using finite_imageI [OF assms(1), of fst] by (simp add: image_image) show "finite (range g)" using finite_imageI [OF assms(1), of snd] by (simp add: image_image) qed lemma zip_fun_split: obtains f g where "h = f ∥ g" proof show "h = fst ∘ h ∥ snd ∘ h" by simp qed abbreviation "None_None ≡ (None, None)" abbreviation "None_Some ≡ λ (y). (None, Some y)" abbreviation "Some_None ≡ λ (x). (Some x, None)" abbreviation "Some_Some ≡ λ (x, y). (Some x, Some y)" abbreviation "None_None_None ≡ (None, None, None)" abbreviation "None_None_Some ≡ λ (z). (None, None, Some z)" abbreviation "None_Some_None ≡ λ (y). (None, Some y, None)" abbreviation "None_Some_Some ≡ λ (y, z). (None, Some y, Some z)" abbreviation "Some_None_None ≡ λ (x). (Some x, None, None)" abbreviation "Some_None_Some ≡ λ (x, z). (Some x, None, Some z)" abbreviation "Some_Some_None ≡ λ (x, y). (Some x, Some y, None)" abbreviation "Some_Some_Some ≡ λ (x, y, z). (Some x, Some y, Some z)" lemma inj_Some2[simp, intro]: "inj None_Some" "inj Some_None" "inj Some_Some" by (rule injI, force)+ lemma inj_Some3[simp, intro]: "inj None_None_Some" "inj None_Some_None" "inj None_Some_Some" "inj Some_None_None" "inj Some_None_Some" "inj Some_Some_None" "inj Some_Some_Some" by (rule injI, force)+ definition swap :: "'a × 'b ⇒ 'b × 'a" where "swap x ≡ (snd x, fst x)" lemma swap_simps[simp]: "swap (a, b) = (b, a)" unfolding swap_def by simp lemma swap_inj[intro, simp]: "inj swap" by (rule injI, auto) lemma swap_surj[intro, simp]: "surj swap" by (rule surjI[where ?f = swap], auto) lemma swap_bij[intro, simp]: "bij swap" by (rule bijI, auto) definition push :: "('a × 'b) × 'c ⇒ 'a × 'b × 'c" where "push x ≡ (fst (fst x), snd (fst x), snd x)" definition pull :: "'a × 'b × 'c ⇒ ('a × 'b) × 'c" where "pull x ≡ ((fst x, fst (snd x)), snd (snd x))" lemma push_simps[simp]: "push ((x, y), z) = (x, y, z)" unfolding push_def by simp lemma pull_simps[simp]: "pull (x, y, z) = ((x, y), z)" unfolding pull_def by simp definition label :: "'vertex × 'label × 'vertex ⇒ 'label" where "label ≡ fst ∘ snd" lemma label_select[simp]: "label (p, a, q) = a" unfolding label_def by simp subsection ‹Theorems for @term{curry} and @term{split}› lemma curry_split[simp]: "curry ∘ case_prod = id" by auto lemma split_curry[simp]: "case_prod ∘ curry = id" by auto lemma curry_le[simp]: "curry f ≤ curry g ⟷ f ≤ g" unfolding le_fun_def by force lemma split_le[simp]: "case_prod f ≤ case_prod g ⟷ f ≤ g" unfolding le_fun_def by force lemma mono_curry_left[simp]: "mono (curry ∘ h) ⟷ mono h" unfolding mono_def by fastforce lemma mono_split_left[simp]: "mono (case_prod ∘ h) ⟷ mono h" unfolding mono_def by fastforce lemma mono_curry_right[simp]: "mono (h ∘ curry) ⟷ mono h" unfolding mono_def split_le[symmetric] by bestsimp lemma mono_split_right[simp]: "mono (h ∘ case_prod) ⟷ mono h" unfolding mono_def curry_le[symmetric] by bestsimp lemma Collect_curry[simp]: "{x. P (curry x)} = case_prod ` {x. P x}" using image_Collect by fastforce lemma Collect_split[simp]: "{x. P (case_prod x)} = curry ` {x. P x}" using image_Collect by force lemma gfp_split_curry[simp]: "gfp (case_prod ∘ f ∘ curry) = case_prod (gfp f)" proof - have "gfp (case_prod ∘ f ∘ curry) = Sup {u. u ≤ case_prod (f (curry u))}" unfolding gfp_def by simp also have "… = Sup {u. curry u ≤ curry (case_prod (f (curry u)))}" unfolding curry_le by simp also have "… = Sup {u. curry u ≤ f (curry u)}" by simp also have "… = Sup (case_prod ` {u. u ≤ f u})" unfolding Collect_curry[of "λ u. u ≤ f u"] by simp also have "… = case_prod (Sup {u. u ≤ f u})" by (force simp add: image_comp) also have "… = case_prod (gfp f)" unfolding gfp_def by simp finally show ?thesis by this qed lemma gfp_curry_split[simp]: "gfp (curry ∘ f ∘ case_prod) = curry (gfp f)" proof - have "gfp (curry ∘ f ∘ case_prod) = Sup {u. u ≤ curry (f (case_prod u))}" unfolding gfp_def by simp also have "… = Sup {u. case_prod u ≤ case_prod (curry (f (case_prod u)))}" unfolding split_le by simp also have "… = Sup {u. case_prod u ≤ f (case_prod u)}" by simp also have "… = Sup (curry ` {u. u ≤ f u})" unfolding Collect_split[of "λ u. u ≤ f u"] by simp also have "… = curry (Sup {u. u ≤ f u})" by (force simp add: image_comp) also have "… = curry (gfp f)" unfolding gfp_def by simp finally show ?thesis by this qed lemma not_someI: assumes "⋀ x. P x ⟹ False" shows "¬ P (SOME x. P x)" using assms by blast lemma some_ccontr: assumes "(⋀ x. ¬ P x) ⟹ False" shows "P (SOME x. P x)" using assms someI_ex ccontr by metis end

# Theory Relation_Extensions

section ‹Relations› theory Relation_Extensions imports Basic_Extensions begin abbreviation rev_lex_prod (infixr "<*rlex*>" 80) where "r⇩_{1}<*rlex*> r⇩_{2}≡ inv_image (r⇩_{2}<*lex*> r⇩_{1}) swap" lemmas sym_rtranclp[intro] = sym_rtrancl[to_pred] definition liftablep :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool" where "liftablep r f ≡ ∀ x y. r x y ⟶ r (f x) (f y)" lemma liftablepI[intro]: assumes "⋀ x y. r x y ⟹ r (f x) (f y)" shows "liftablep r f" using assms unfolding liftablep_def by simp lemma liftablepE[elim]: assumes "liftablep r f" assumes "r x y" obtains "r (f x) (f y)" using assms unfolding liftablep_def by simp lemma liftablep_rtranclp: assumes "liftablep r f" shows "liftablep r⇧^{*}⇧^{*}f" proof fix x y assume "r⇧^{*}⇧^{*}x y" thus "r⇧^{*}⇧^{*}(f x) (f y)" using assms by (induct rule: rtranclp_induct, force+) qed definition confluentp :: "('a ⇒ 'a ⇒ bool) ⇒ bool" where "confluentp r ≡ ∀ x y1 y2. r⇧^{*}⇧^{*}x y1 ⟶ r⇧^{*}⇧^{*}x y2 ⟶ (∃ z. r⇧^{*}⇧^{*}y1 z ∧ r⇧^{*}⇧^{*}y2 z)" lemma confluentpI[intro]: assumes "⋀ x y1 y2. r⇧^{*}⇧^{*}x y1 ⟹ r⇧^{*}⇧^{*}x y2 ⟹ ∃ z. r⇧^{*}⇧^{*}y1 z ∧ r⇧^{*}⇧^{*}y2 z" shows "confluentp r" using assms unfolding confluentp_def by simp lemma confluentpE[elim]: assumes "confluentp r" assumes "r⇧^{*}⇧^{*}x y1" "r⇧^{*}⇧^{*}x y2" obtains z where "r⇧^{*}⇧^{*}y1 z" "r⇧^{*}⇧^{*}y2 z" using assms unfolding confluentp_def by blast lemma confluentpI'[intro]: assumes "⋀ x y1 y2. r⇧^{*}⇧^{*}x y1 ⟹ r x y2 ⟹ ∃ z. r⇧^{*}⇧^{*}y1 z ∧ r⇧^{*}⇧^{*}y2 z" shows "confluentp r" proof fix x y1 y2 assume "r⇧^{*}⇧^{*}x y1" "r⇧^{*}⇧^{*}x y2" thus "∃ z. r⇧^{*}⇧^{*}y1 z ∧ r⇧^{*}⇧^{*}y2 z" using assms by (induct rule: rtranclp_induct, force+) qed lemma transclp_eq_implies_confluent_imp: assumes "r1⇧^{*}⇧^{*}= r2⇧^{*}⇧^{*}" assumes "confluentp r1" shows "confluentp r2" using assms by force lemma transclp_eq_implies_confluent_eq: assumes "r1⇧^{*}⇧^{*}= r2⇧^{*}⇧^{*}" shows "confluentp r1 ⟷ confluentp r2" using assms transclp_eq_implies_confluent_imp by metis definition diamondp :: "('a ⇒ 'a ⇒ bool) ⇒ bool" where "diamondp r ≡ ∀ x y1 y2. r x y1 ⟶ r x y2 ⟶ (∃ z. r y1 z ∧ r y2 z)" lemma diamondpI[intro]: assumes "⋀ x y1 y2. r x y1 ⟹ r x y2 ⟹ ∃ z. r y1 z ∧ r y2 z" shows "diamondp r" using assms unfolding diamondp_def by simp lemma diamondpE[elim]: assumes "diamondp r" assumes "r x y1" "r x y2" obtains z where "r y1 z" "r y2 z" using assms unfolding diamondp_def by blast lemma diamondp_implies_confluentp: assumes "diamondp r" shows "confluentp r" proof (rule confluentpI') fix x y1 y2 assume "r⇧^{*}⇧^{*}x y1" "r x y2" hence "∃ z. r y1 z ∧ r⇧^{*}⇧^{*}y2 z" using assms by (induct rule: rtranclp_induct, force+) thus "∃ z. r⇧^{*}⇧^{*}y1 z ∧ r⇧^{*}⇧^{*}y2 z" by blast qed locale wellfounded_relation = fixes R :: "'a ⇒ 'a ⇒ bool" assumes wellfounded: "wfP R" end

# Theory Transition_System_Extensions

section ‹Transition Systems› theory Transition_System_Extensions imports "Basics/Word_Prefixes" "Extensions/Set_Extensions" "Extensions/Relation_Extensions" Transition_Systems_and_Automata.Transition_System Transition_Systems_and_Automata.Transition_System_Extra Transition_Systems_and_Automata.Transition_System_Construction begin context transition_system_initial begin definition cycles :: "'state ⇒ 'transition list set" where "cycles p ≡ {w. path w p ∧ target w p = p}" lemma cyclesI[intro!]: assumes "path w p" "target w p = p" shows "w ∈ cycles p" using assms unfolding cycles_def by auto lemma cyclesE[elim!]: assumes "w ∈ cycles p" obtains "path w p" "target w p = p" using assms unfolding cycles_def by auto inductive_set executable :: "'transition set" where executable: "p ∈ nodes ⟹ enabled a p ⟹ a ∈ executable" lemma executableI_step[intro!]: assumes "p ∈ nodes" "enabled a p" shows "a ∈ executable" using executable assms by this lemma executableI_words_fin[intro!]: assumes "p ∈ nodes" "path w p" shows "set w ⊆ executable" using assms by (induct w arbitrary: p, auto del: subsetI) lemma executableE[elim?]: assumes "a ∈ executable" obtains p where "p ∈ nodes" "enabled a p" using assms by induct auto end locale transition_system_interpreted = transition_system ex en for ex :: "'action ⇒ 'state ⇒ 'state" and en :: "'action ⇒ 'state ⇒ bool" and int :: "'state ⇒ 'interpretation" begin definition visible :: "'action set" where "visible ≡ {a. ∃ q. en a q ∧ int q ≠ int (ex a q)}" lemma visibleI[intro]: assumes "en a q" "int q ≠ int (ex a q)" shows "a ∈ visible" using assms unfolding visible_def by auto lemma visibleE[elim]: assumes "a ∈ visible" obtains q where "en a q" "int q ≠ int (ex a q)" using assms unfolding visible_def by auto abbreviation "invisible ≡ - visible" lemma execute_fin_word_invisible: assumes "path w p" "set w ⊆ invisible" shows "int (target w p) = int p" using assms by (induct w arbitrary: p rule: list.induct, auto) lemma execute_inf_word_invisible: assumes "run w p" "k ≤ l" "⋀ i. k ≤ i ⟹ i < l ⟹ w !! i ∉ visible" shows "int ((p ## trace w p) !! k) = int ((p ## trace w p) !! l)" proof - have "(p ## trace w p) !! l = target (stake l w) p" by simp also have "stake l w = stake k w @ stake (l - k) (sdrop k w)" using assms(2) by simp also have "target … p = target (stake (l - k) (sdrop k w)) (target (stake k w) p)" unfolding fold_append comp_apply by rule also have "int … = int (target (stake k w) p)" proof (rule execute_fin_word_invisible) have "w = stake l w @- sdrop l w" by simp also have "stake l w = stake k w @ stake (l - k) (sdrop k w)" using assms(2) by simp finally have 1: "run (stake k w @- stake (l - k) (sdrop k w) @- sdrop l w) p" unfolding shift_append using assms(1) by simp show "path (stake (l - k) (sdrop k w)) (target (stake k w) p)" using 1 by auto show "set (stake (l - k) (sdrop k w)) ⊆ invisible" using assms(3) by (auto simp: set_stake_snth) qed also have "… = int ((p ## trace w p) !! k)" by simp finally show ?thesis by rule qed end locale transition_system_complete = transition_system_initial ex en init + transition_system_interpreted ex en int for ex :: "'action ⇒ 'state ⇒ 'state" and en :: "'action ⇒ 'state ⇒ bool" and init :: "'state ⇒ bool" and int :: "'state ⇒ 'interpretation" begin definition language :: "'interpretation stream set" where "language ≡ {smap int (p ## trace w p) |p w. init p ∧ run w p}" lemma languageI[intro!]: assumes "w = smap int (p ## trace v p)" "init p" "run v p" shows "w ∈ language" using assms unfolding language_def by auto lemma languageE[elim!]: assumes "w ∈ language" obtains p v where "w = smap int (p ## trace v p)" "init p" "run v p" using assms unfolding language_def by auto end locale transition_system_finite_nodes = transition_system_initial ex en init for ex :: "'action ⇒ 'state ⇒ 'state" and en :: "'action ⇒ 'state ⇒ bool" and init :: "'state ⇒ bool" + assumes reachable_finite: "finite nodes" locale transition_system_cut = transition_system_finite_nodes ex en init for ex :: "'action ⇒ 'state ⇒ 'state" and en :: "'action ⇒ 'state ⇒ bool" and init :: "'state ⇒ bool" + fixes cuts :: "'action set" assumes cycles_cut: "p ∈ nodes ⟹ w ∈ cycles p ⟹ w ≠ [] ⟹ set w ∩ cuts ≠ {}" begin inductive scut :: "'state ⇒ 'state ⇒ bool" where scut: "p ∈ nodes ⟹ en a p ⟹ a ∉ cuts ⟹ scut p (ex a p)" declare scut.intros[intro!] declare scut.cases[elim!] lemma scut_reachable: assumes "scut p q" shows "p ∈ nodes" "q ∈ nodes" using assms by auto lemma scut_trancl: assumes "scut⇧^{+}⇧^{+}p q" obtains w where "path w p" "target w p = q" "set w ∩ cuts = {}" "w ≠ []" using assms proof (induct arbitrary: thesis) case (base q) show ?case using base by force next case (step q r) obtain w where 1: "path w p" "target w p = q" "set w ∩ cuts = {}" "w ≠ []" using step(3) by this obtain a where 2: "en a q" "a ∉ cuts" "ex a q = r" using step(2) by auto show ?case proof (rule step(4)) show "path (w @ [a]) p" using 1 2 by auto show "target (w @ [a]) p = r" using 1 2 by auto show "set (w @ [a]) ∩ cuts = {}" using 1 2 by auto show "w @ [a] ≠ []" by auto qed qed sublocale wellfounded_relation "scut¯¯" proof (unfold_locales, intro finite_acyclic_wf_converse[to_pred] acyclicI[to_pred], safe) have 1: "{(p, q). scut p q} ⊆ nodes × nodes" using scut_reachable by blast have 2: "finite (nodes × nodes)" using finite_cartesian_product reachable_finite by blast show "finite {(p, q). scut p q}" using 1 2 by blast next fix p assume 1: "scut⇧^{+}⇧^{+}p p" have 2: "p ∈ nodes" using 1 tranclE[to_pred] scut_reachable by metis obtain w where 3: "path w p" "target w p = p" "set w ∩ cuts = {}" "w ≠ []" using scut_trancl 1 by this have 4: "w ∈ cycles p" using 3(1, 2) by auto have 5: "set w ∩ cuts ≠ {}" using cycles_cut 2 4 3(4) by this show "False" using 3(3) 5 by simp qed lemma no_cut_scut: assumes "p ∈ nodes" "en a p" "a ∉ cuts" shows "scut¯¯ (ex a p) p" using assms by auto end locale transition_system_sticky = transition_system_complete ex en init int + transition_system_cut ex en init sticky for ex :: "'action ⇒ 'state ⇒ 'state" and en :: "'action ⇒ 'state ⇒ bool" and init :: "'state ⇒ bool" and int :: "'state ⇒ 'interpretation" and sticky :: "'action set" + assumes executable_visible_sticky: "executable ∩ visible ⊆ sticky" end

# Theory Traces

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

# Theory Transition_System_Traces

section ‹Transition Systems and Trace Theory› theory Transition_System_Traces imports Transition_System_Extensions Traces begin lemma (in transition_system) words_infI_construct[rule_format, intro?]: assumes "∀ v. v ≤⇩_{F}⇩_{I}w ⟶ path v p" shows "run w p" using assms by coinduct auto lemma (in transition_system) words_infI_construct': assumes "⋀ k. ∃ v. v ≤⇩_{F}⇩_{I}w ∧ k < length v ∧ path v p" shows "run w p" proof fix u assume 1: "u ≤⇩_{F}⇩_{I}w" obtain v where 2: "v ≤⇩_{F}⇩_{I}w" "length u < length v" "path v p" using assms(1) by auto have 3: "length u ≤ length v" using 2(2) by simp have 4: "u ≤ v" using prefix_fininf_length 1 2(1) 3 by this show "path u p" using 4 2(3) by auto qed lemma (in transition_system) words_infI_construct_chain[intro]: assumes "chain w" "⋀ k. path (w k) p" shows "run (limit w) p" proof (rule words_infI_construct') fix k obtain l where 1: "k < length (w l)" using assms(1) by rule show "∃ v. v ≤⇩_{F}⇩_{I}limit w ∧ k < length v ∧ path v p" 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 "path (w l) p" using assms(2) by this qed qed lemma (in transition_system) words_fin_blocked: assumes "⋀ w. path w p ⟹ A ∩ set w = {} ⟹ A ∩ {a. enabled a (target w p)} ⊆ A ∩ {a. enabled a p}" assumes "path w p" "A ∩ {a. enabled a p} ∩ set w = {}" shows "A ∩ set w = {}" using assms by (induct w rule: rev_induct, auto) locale transition_system_traces = transition_system ex en + traces ind for ex :: "'action ⇒ 'state ⇒ 'state" and en :: "'action ⇒ 'state ⇒ bool" and ind :: "'action ⇒ 'action ⇒ bool" + assumes en: "ind a b ⟹ en a p ⟹ en b p ⟷ en b (ex a p)" assumes ex: "ind a b ⟹ en a p ⟹ en b p ⟹ ex b (ex a p) = ex a (ex b p)" begin lemma diamond_bottom: assumes "ind a b" assumes "en a p" "en b p" shows "en a (ex b p)" "en b (ex a p)" "ex b (ex a p) = ex a (ex b p)" using assms independence_symmetric en ex by metis+ lemma diamond_right: assumes "ind a b" assumes "en a p" "en b (ex a p)" shows "en a (ex b p)" "en b p" "ex b (ex a p) = ex a (ex b p)" using assms independence_symmetric en ex by metis+ lemma diamond_left: assumes "ind a b" assumes "en a (ex b p)" "en b p" shows "en a p" "en b (ex a p)" "ex b (ex a p) = ex a (ex b p)" using assms independence_symmetric en ex by metis+ lemma eq_swap_word: assumes "w⇩_{1}=⇩_{S}w⇩_{2}" "path w⇩_{1}p" shows "path w⇩_{2}p" using assms diamond_right by (induct, auto) lemma eq_fin_word: assumes "w⇩_{1}=⇩_{F}w⇩_{2}" "path w⇩_{1}p" shows "path w⇩_{2}p" using assms eq_swap_word by (induct, auto) lemma le_fin_word: assumes "w⇩_{1}≼⇩_{F}w⇩_{2}" "path w⇩_{2}p" shows "path w⇩_{1}p" using assms eq_fin_word by blast lemma le_fininf_word: assumes "w⇩_{1}≼⇩_{F}⇩_{I}w⇩_{2}" "run w⇩_{2}p" shows "path w⇩_{1}p" using assms le_fin_word by blast lemma le_inf_word: assumes "w⇩_{2}≼⇩_{I}w⇩_{1}" "run w⇩_{1}p" shows "run w⇩_{2}p" using assms le_fininf_word by (blast intro: words_infI_construct) lemma eq_inf_word: assumes "w⇩_{1}=⇩_{I}w⇩_{2}" "run w⇩_{1}p" shows "run w⇩_{2}p" using assms le_inf_word by auto lemma eq_swap_execute: assumes "path w⇩_{1}p" "w⇩_{1}=⇩_{S}w⇩_{2}" shows "fold ex w⇩_{1}p = fold ex w⇩_{2}p" using assms(2, 1) diamond_right by (induct, auto) lemma eq_fin_execute: assumes "path w⇩_{1}p" "w⇩_{1}=⇩_{F}w⇩_{2}" shows "fold ex w⇩_{1}p = fold ex w⇩_{2}p" using assms(2, 1) eq_fin_word eq_swap_execute by (induct, auto) lemma diamond_fin_word_step: assumes "Ind {a} (set v)" "en a p" "path v p" shows "path v (ex a p)" using diamond_bottom assms by (induct v arbitrary: p, auto, metis) lemma diamond_inf_word_step: assumes "Ind {a} (sset w)" "en a p" "run w p" shows "run w (ex a p)" using diamond_fin_word_step assms by (fast intro: words_infI_construct) lemma diamond_fin_word_inf_word: assumes "Ind (set v) (sset w)" "path v p" "run w p" shows "run w (fold ex v p)" using diamond_inf_word_step assms by (induct v arbitrary: p, auto) lemma diamond_fin_word_inf_word': assumes "Ind (set v) (sset w)" "path (u @ v) p" "run (u @- w) p" shows "run (u @- v @- w) p" using assms diamond_fin_word_inf_word by auto end end

# Theory Functions

section ‹Functions› theory Functions imports "../Extensions/Set_Extensions" begin locale bounded_function = fixes A :: "'a set" fixes B :: "'b set" fixes f :: "'a ⇒ 'b" assumes wellformed[intro?, simp]: "x ∈ A ⟹ f x ∈ B" locale bounded_function_pair = f: bounded_function A B f + g: bounded_function B A g for A :: "'a set" and B :: "'b set" and f :: "'a ⇒ 'b" and g :: "'b ⇒ 'a" locale injection = bounded_function_pair + assumes left_inverse[simp]: "x ∈ A ⟹ g (f x) = x" begin lemma inj_on[intro]: "inj_on f A" using inj_onI left_inverse by metis lemma injective_on: assumes "x ∈ A" "y ∈ A" "f x = f y" shows "x = y" using assms left_inverse by metis end locale injective = bounded_function + assumes injection: "∃ g. injection A B f g" begin definition "g ≡ SOME g. injection A B f g" sublocale injection A B f g unfolding g_def using someI_ex[OF injection] by this end locale surjection = bounded_function_pair + assumes right_inverse[simp]: "y ∈ B ⟹ f (g y) = y" begin lemma image_superset[intro]: "f ` A ⊇ B" using g.wellformed image_iff right_inverse subsetI by metis lemma image_eq[simp]: "f ` A = B" using image_superset by auto end locale surjective = bounded_function + assumes surjection: "∃ g. surjection A B f g" begin definition "g ≡ SOME g. surjection A B f g" sublocale surjection A B f g unfolding g_def using someI_ex[OF surjection] by this end locale bijection = injection + surjection lemma inj_on_bijection: assumes "inj_on f A" shows "bijection A (f ` A) f (inv_into A f)" proof show "⋀ x. x ∈ A ⟹ f x ∈ f ` A" using imageI by this show "⋀ y. y ∈ f ` A ⟹ inv_into A f y ∈ A" using inv_into_into by this show "⋀ x. x ∈ A ⟹ inv_into A f (f x) = x" using inv_into_f_f assms by this show "⋀ y. y ∈ f ` A ⟹ f (inv_into A f y) = y" using f_inv_into_f by this qed end

# Theory ENat_Extensions

section ‹Extended Natural Numbers› theory ENat_Extensions imports Coinductive.Coinductive_Nat begin declare eSuc_enat[simp] declare iadd_Suc[simp] iadd_Suc_right[simp] declare enat_0[simp] enat_1[simp] one_eSuc[simp] declare enat_0_iff[iff] enat_1_iff[iff] declare Suc_ile_eq[iff] lemma enat_Suc0[simp]: "enat (Suc 0) = eSuc 0" by (metis One_nat_def one_eSuc one_enat_def) lemma le_epred[iff]: "l < epred k ⟷ eSuc l < k" by (metis eSuc_le_iff epred_eSuc epred_le_epredI less_le_not_le not_le) lemma eq_infI[intro]: assumes "⋀ n. enat n ≤ m" shows "m = ∞" using assms by (metis enat_less_imp_le enat_ord_simps(5) less_le_not_le) end

# Theory CCPO_Extensions

section ‹Chain-Complete Partial Orders› theory CCPO_Extensions imports "HOL-Library.Complete_Partial_Order2" ENat_Extensions Set_Extensions begin lemma chain_split[dest]: assumes "Complete_Partial_Order.chain ord C" "x ∈ C" shows "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}" proof - have 1: "⋀ y. y ∈ C ⟹ ord x y ∨ ord y x" using chainD assms by this show ?thesis using 1 by blast qed lemma infinite_chain_below[dest]: assumes "Complete_Partial_Order.chain ord C" "infinite C" "x ∈ C" assumes "finite {y ∈ C. ord x y}" shows "infinite {y ∈ C. ord y x}" proof - have 1: "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}" using assms(1, 3) by rule show ?thesis using finite_Un assms(2, 4) 1 by (metis (poly_guards_query)) qed lemma infinite_chain_above[dest]: assumes "Complete_Partial_Order.chain ord C" "infinite C" "x ∈ C" assumes "finite {y ∈ C. ord y x}" shows "infinite {y ∈ C. ord x y}" proof - have 1: "C = {y ∈ C. ord x y} ∪ {y ∈ C. ord y x}" using assms(1, 3) by rule show ?thesis using finite_Un assms(2, 4) 1 by (metis (poly_guards_query)) qed lemma (in ccpo) ccpo_Sup_upper_inv: assumes "Complete_Partial_Order.chain less_eq C" "x > ⨆ C" shows "x ∉ C" using assms ccpo_Sup_upper by fastforce lemma (in ccpo) ccpo_Sup_least_inv: assumes "Complete_Partial_Order.chain less_eq C" "⨆ C > x" obtains y where "y ∈ C" "¬ y ≤ x" using assms ccpo_Sup_least that by fastforce lemma ccpo_Sup_least_inv': fixes C :: "'a :: {ccpo, linorder} set" assumes "Complete_Partial_Order.chain less_eq C" "⨆ C > x" obtains y where "y ∈ C" "y > x" proof - obtain y where 1: "y ∈ C" "¬ y ≤ x" using ccpo_Sup_least_inv assms by this show ?thesis using that 1 by simp qed lemma mcont2mcont_lessThan[THEN lfp.mcont2mcont, simp, cont_intro]: shows mcont_lessThan: "mcont Sup less_eq Sup less_eq (lessThan :: 'a :: {ccpo, linorder} ⇒ 'a set)" proof show "monotone less_eq less_eq (lessThan :: 'a ⇒ 'a set)" by (rule, auto) show "cont Sup less_eq Sup less_eq (lessThan :: 'a ⇒ 'a set)" proof fix C :: "'a set" assume 1: "Complete_Partial_Order.chain less_eq C" show "{..< ⨆ C} = ⋃ (lessThan ` C)" proof (intro equalityI subsetI) fix A assume 2: "A ∈ {..< ⨆ C}" obtain B where 3: "B ∈ C" "B > A" using ccpo_Sup_least_inv' 1 2 by blast show "A ∈ ⋃ (lessThan ` C)" using 3 by auto next fix A assume 2: "A ∈ ⋃ (lessThan ` C)" show "A ∈ {..< ⨆ C}" using ccpo_Sup_upper 2 by force qed qed qed class esize = fixes esize :: "'a ⇒ enat" class esize_order = esize + order + assumes esize_finite[dest]: "esize x ≠ ∞ ⟹ finite {y. y ≤ x}" assumes esize_mono[intro]: "x ≤ y ⟹ esize x ≤ esize y" assumes esize_strict_mono[intro]: "esize x ≠ ∞ ⟹ x < y ⟹ esize x < esize y" begin lemma infinite_chain_eSuc_esize[dest]: assumes "Complete_Partial_Order.chain less_eq C" "infinite C" "x ∈ C" obtains y where "y ∈ C" "esize y ≥ eSuc (esize x)" proof (cases "esize x") case (enat k) have 1: "finite {y ∈ C. y ≤ x}" using esize_finite enat by simp have 2: "infinite {y ∈ C. y ≥ x}" using assms 1 by rule have 3: "{y ∈ C. y > x} = {y ∈ C. y ≥ x} - {x}" by auto have 4: "infinite {y ∈ C. y > x}" using 2 unfolding 3 by simp obtain y where 5: "y ∈ C" "y > x" using 4 by auto have 6: "esize y > esize x" using esize_strict_mono enat 5(2) by blast show ?thesis using that 5(1) 6 ileI1 by simp next case (infinity) show ?thesis using that infinity assms(3) by simp qed lemma infinite_chain_arbitrary_esize[dest]: assumes "Complete_Partial_Order.chain less_eq C" "infinite C" obtains x where "x ∈ C" "esize x ≥ enat n" proof (induct n arbitrary: thesis) case 0 show ?case using assms(2) 0 by force next case (Suc n) obtain x where 1: "x ∈ C" "esize x ≥ enat n" using Suc(1) by blast obtain y where 2: "y ∈ C" "esize y ≥ eSuc (esize x)" using assms 1(1) by rule show ?case using gfp.leq_trans Suc(2) 1(2) 2 by fastforce qed end class esize_ccpo = esize_order + ccpo begin lemma esize_cont[dest]: assumes "Complete_Partial_Order.chain less_eq C" "C ≠ {}" shows "esize (⨆ C) = ⨆ (esize ` C)" proof (cases "finite C") case False have 1: "esize (⨆ C) = ∞" proof fix n obtain A where 1: "A ∈ C" "esize A ≥ enat n" using assms(1) False by rule have 2: "A ≤ ⨆ C" using ccpo_Sup_upper assms(1) 1(1) by this have "enat n ≤ esize A" using 1(2) by this also have "… ≤ esize (⨆ C)" using 2 by rule finally show "enat n ≤ esize (⨆ C)" by this qed have 2: "(⨆ A ∈ C. esize A) = ∞" proof fix n obtain A where 1: "A ∈ C" "esize A ≥ enat n" using assms(1) False by rule show "enat n ≤ (⨆ A ∈ C. esize A)" using SUP_upper2 1 by this qed show ?thesis using 1 2 by simp next case True have 1: "esize (⨆ C) = (⨆ x ∈ C. esize x)" proof (intro order_class.order.antisym SUP_upper SUP_least esize_mono) show "⨆ C ∈ C" using in_chain_finite assms(1) True assms(2) by this show "⋀ x. x ∈ C ⟹ x ≤ ⨆ C" using ccpo_Sup_upper assms(1) by this qed show ?thesis using 1 by simp qed lemma esize_mcont: "mcont Sup less_eq Sup less_eq esize" by (blast intro: mcontI monotoneI contI) lemmas mcont2mcont_esize = esize_mcont[THEN lfp.mcont2mcont, simp, cont_intro] end end

# Theory ESet_Extensions

section ‹Sets and Extended Natural Numbers› theory ESet_Extensions imports "../Basics/Functions" Basic_Extensions CCPO_Extensions begin lemma card_lessThan_enat[simp]: "card {..< enat k} = card {..< k}" proof - have 1: "{..< enat k} = enat ` {..< k}" unfolding lessThan_def image_Collect using enat_iless by force have "card {..< enat k} = card (enat ` {..< k})" unfolding 1 by rule also have "… = card {..< k}" using card_image inj_enat by metis finally show ?thesis by this qed lemma card_atMost_enat[simp]: "card {.. enat k} = card {.. k}" proof - have 1: "{.. enat k} = enat ` {.. k}" unfolding atMost_def image_Collect using enat_ile by force have "card {.. enat k} = card (enat ` {.. k})" unfolding 1 by rule also have "… = card {.. k}" using card_image inj_enat by metis finally show ?thesis by this qed lemma enat_Collect: assumes "∞ ∉ A" shows "{i. enat i ∈ A} = the_enat ` A" using assms by (safe, force) (metis enat_the_enat) lemma Collect_lessThan: "{i. enat i < n} = the_enat ` {..< n}" proof - have 1: "∞ ∉ {..< n}" by simp have "{i. enat i < n} = {i. enat i ∈ {..< n}}" by simp also have "… = the_enat ` {..< n}" using enat_Collect 1 by this finally show ?thesis by this qed instantiation set :: (type) esize_ccpo begin function esize_set where "finite A ⟹ esize A = enat (card A)" | "infinite A ⟹ esize A = ∞" by auto termination by lexicographic_order lemma esize_iff_empty[iff]: "esize A = 0 ⟷ A = {}" by (cases "finite A", auto) lemma esize_iff_infinite[iff]: "esize A = ∞ ⟷ infinite A" by force lemma esize_singleton[simp]: "esize {a} = eSuc 0" by simp lemma esize_infinite_enat[dest, simp]: "infinite A ⟹ enat k < esize A" by force instance proof fix A :: "'a set" assume 1: "esize A ≠ ∞" show "finite {B. B ⊆ A}" using 1 by simp next fix A B :: "'a set" assume 1: "A ⊆ B" show "esize A ≤ esize B" proof (cases "finite B") case False show ?thesis using False by auto next case True have 2: "finite A" using True 1 by auto show ?thesis using card_mono True 1 2 by auto qed next fix A B :: "'a set" assume 1: "esize A ≠ ∞" "A ⊂ B" show "esize A < esize B" using psubset_card_mono 1 by (cases "finite B", auto) qed end lemma esize_image[simp, intro]: assumes "inj_on f A" shows "esize (f ` A) = esize A" using card_image finite_imageD assms by (cases "finite A", auto) lemma esize_insert1[simp]: "a ∉ A ⟹ esize (insert a A) = eSuc (esize A)" by (cases "finite A", force+) lemma esize_insert2[simp]: "a ∈ A ⟹ esize (insert a A) = esize A" using insert_absorb by metis lemma esize_remove1[simp]: "a ∉ A ⟹ esize (A - {a}) = esize A" by (cases "finite A", force+) lemma esize_remove2[simp]: "a ∈ A ⟹ esize (A - {a}) = epred (esize A)" by (cases "finite A", force+) lemma esize_union_disjoint[simp]: assumes "A ∩ B = {}" shows "esize (A ∪ B) = esize A + esize B" proof (cases "finite (A ∪ B)") case True show ?thesis using card_Un_disjoint assms True by auto next case False show ?thesis using False by (cases "finite A", auto) qed lemma esize_lessThan[simp]: "esize {..< n} = n" proof (cases n) case (enat k) have 1: "finite {..< n}" unfolding enat by (metis finite_lessThan_enat_iff not_enat_eq) show ?thesis using 1 unfolding enat by simp next case (infinity) have 1: "infinite {..< n}" unfolding infinity using infinite_lessThan_infty by simp show ?thesis using 1 unfolding infinity by simp qed lemma esize_atMost[simp]: "esize {.. n} = eSuc n" proof (cases n) case (enat k) have 1: "finite {.. n}" unfolding enat by (metis atMost_iff finite_enat_bounded) show ?thesis using 1 unfolding enat by simp next case (infinity) have 1: "infinite {.. n}" unfolding infinity by (metis atMost_iff enat_ord_code(3) infinite_lessThan_infty infinite_super subsetI) show ?thesis using 1 unfolding infinity by simp qed lemma least_eSuc[simp]: assumes "A ≠ {}" shows "least (eSuc ` A) = eSuc (least A)" proof (rule antisym) obtain k where 10: "k ∈ A" using assms by blast have 11: "eSuc k ∈ eSuc ` A" using 10 by auto have 20: "least A ∈ A" using 10 LeastI by metis have 21: "least (eSuc ` A) ∈ eSuc ` A" using 11 LeastI by metis have 30: "⋀ l. l ∈ A ⟹ least A ≤ l" using 10 Least_le by metis have 31: "⋀ l. l ∈ eSuc ` A ⟹ least (eSuc ` A) ≤ l" using 11 Least_le by metis show "least (eSuc ` A) ≤ eSuc (least A)" using 20 31 by auto show "eSuc (least A) ≤ least (eSuc ` A)" using 21 30 by auto qed lemma Inf_enat_eSuc[simp]: "⨅ (eSuc ` A) = eSuc (⨅ A)" unfolding Inf_enat_def by simp definition lift :: "nat set ⇒ nat set" where "lift A ≡ insert 0 (Suc ` A)" lemma liftI_0[intro, simp]: "0 ∈ lift A" unfolding lift_def by auto lemma liftI_Suc[intro]: "a ∈ A ⟹ Suc a ∈ lift A" unfolding lift_def by auto lemma liftE[elim]: assumes "b ∈ lift A" obtains (0) "b = 0" | (Suc) a where "b = Suc a" "a ∈ A" using assms unfolding lift_def by auto lemma lift_esize[simp]: "esize (lift A) = eSuc (esize A)" unfolding lift_def by auto lemma lift_least[simp]: "least (lift A) = 0" unfolding lift_def by auto primrec nth_least :: "'a set ⇒ nat ⇒ 'a :: wellorder" where "nth_least A 0 = least A" | "nth_least A (Suc n) = nth_least (A - {least A}) n" lemma nth_least_wellformed[intro?, simp]: assumes "enat n < esize A" shows "nth_least A n ∈ A" using assms proof (induct n arbitrary: A) case 0 show ?case using 0 by simp next case (Suc n) have 1: "A ≠ {}" using Suc(2) by auto have 2: "enat n < esize (A - {least A})" using Suc(2) 1 by simp have 3: "nth_least (A - {least A}) n ∈ A - {least A}" using Suc(1) 2 by this show ?case using 3 by simp qed lemma card_wellformed[intro?, simp]: fixes k :: "'a :: wellorder" assumes "k ∈ A" shows "enat (card {i ∈ A. i < k}) < esize A" proof (cases "finite A") case False show ?thesis using False by simp next case True have 1: "esize {i ∈ A. i < k} < esize A" using True assms by fastforce show ?thesis using True 1 by simp qed lemma nth_least_strict_mono: assumes "enat l < esize A" "k < l" shows "nth_least A k < nth_least A l" using assms proof (induct k arbitrary: A l) case 0 obtain l' where 1: "l = Suc l'" using 0(2) by (metis gr0_conv_Suc) have 2: "A ≠ {}" using 0(1) by auto have 3: "enat l' < esize (A - {least A})" using 0(1) 2 unfolding 1 by simp have 4: "nth_least (A - {least A}) l' ∈ A - {least A}" using 3 by rule show ?case using 1 4 by (auto intro: le_neq_trans) next case (Suc k) obtain l' where 1: "l = Suc l'" using Suc(3) by (metis Suc_lessE) have 2: "A ≠ {}" using Suc(2) by auto show ?case using Suc 2 unfolding 1 by simp qed lemma nth_least_mono[intro, simp]: assumes "enat l < esize A" "k ≤ l" shows "nth_least A k ≤ nth_least A l" using nth_least_strict_mono le_less assms by metis lemma card_nth_least[simp]: assumes "enat n < esize A" shows "card {k ∈ A. k < nth_least A n} = n" using assms proof (induct n arbitrary: A) case 0 have 1: "{k ∈ A. k < least A} = {}" using least_not_less by auto show ?case using nth_least.simps(1) card.empty 1 by metis next case (Suc n) have 1: "A ≠ {}" using Suc(2) by auto have 2: "enat n < esize (A - {least A})" using Suc(2) 1 by simp have 3: "nth_least A 0 < nth_least A (Suc n)" using nth_least_strict_mono Suc(2) by blast have 4: "{k ∈ A. k < nth_least A (Suc n)} = {least A} ∪ {k ∈ A - {least A}. k < nth_least (A - {least A}) n}" using 1 3 by auto have 5: "card {k ∈ A - {least A}. k < nth_least (A - {least A}) n} = n" using Suc(1) 2 by this have 6: "finite {k ∈ A - {least A}. k < nth_least (A - {least A}) n}" using 5 Collect_empty_eq card.infinite infinite_imp_nonempty least_not_less nth_least.simps(1) by (metis (no_types, lifting)) have "card {k ∈ A. k < nth_least A (Suc n)} = card ({least A} ∪ {k ∈ A - {least A}. k < nth_least (A - {least A}) n})" using 4 by simp also have "… = card {least A} + card {k ∈ A - {least A}. k < nth_least (A - {least A}) n}" using 6 by simp also have "… = Suc n" using 5 by simp finally show ?case by this qed lemma card_nth_least_le[simp]: assumes "enat n < esize A" shows "card {k ∈ A. k ≤ nth_least A n} = Suc n" proof - have 1: "{k ∈ A. k ≤ nth_least A n} = {nth_least A n} ∪ {k ∈ A. k < nth_least A n}" using assms by auto have 2: "card {k ∈ A. k < nth_least A n} = n" using assms by simp have 3: "finite {k ∈ A. k < nth_least A n}" using 2 Collect_empty_eq card.infinite infinite_imp_nonempty least_not_less nth_least.simps(1) by (metis (no_types, lifting)) have "card {k ∈ A. k ≤ nth_least A n} = card ({nth_least A n} ∪ {k ∈ A. k < nth_least A n})" unfolding 1 by rule also have "… = card {nth_least A n} + card {k ∈ A. k < nth_least A n}" using 3 by simp also have "… = Suc n" using assms by simp finally show ?thesis by this qed lemma nth_least_card: fixes k :: nat assumes "k ∈ A" shows "nth_least A (card {i ∈ A. i < k}) = k" proof (rule nat_set_card_equality_less) have 1: "enat (card {l ∈ A. l < k}) < esize A" proof (cases "finite A") case False show ?thesis using False by simp next case True have 1: "{l ∈ A. l < k} ⊂ A" using assms by blast have 2: "card {l ∈ A. l < k} < card A" using psubset_card_mono True 1 by this show ?thesis using True 2 by simp qed show "nth_least A (card {l ∈ A. l < k}) ∈ A" using 1 by rule show "k ∈ A" using assms by this show "card {z ∈ A. z < nth_least A (card {i ∈ A. i < k})} = card {z ∈ A. z < k}" using 1 by simp qed interpretation nth_least: bounded_function_pair "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}" using nth_least_wellformed card_wellformed by (unfold_locales, blast+) interpretation nth_least: injection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}" using card_nth_least by (unfold_locales, blast) interpretation nth_least: surjection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}" for A :: "nat set" using nth_least_card by (unfold_locales, blast) interpretation nth_least: bijection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}" for A :: "nat set" by unfold_locales lemma nth_least_strict_mono_inverse: fixes A :: "nat set" assumes "enat k < esize A" "enat l < esize A" "nth_least A k < nth_least A l" shows "k < l" using assms by (metis not_less_iff_gr_or_eq nth_least_strict_mono) lemma nth_least_less_card_less: fixes k :: nat shows "enat n < esize A ∧ nth_least A n < k ⟷ n < card {i ∈ A. i < k}" proof safe assume 1: "enat n < esize A" "nth_least A n < k" have 2: "nth_least A n ∈ A" using 1(1) by rule have "n = card {i ∈ A. i < nth_least A n}" using 1 by simp also have "… < card {i ∈ A. i < k}" using 1(2) 2 by simp finally show "n < card {i ∈ A. i < k}" by this next assume 1: "n < card {i ∈ A. i < k}" have "enat n < enat (card {i ∈ A. i < k})" using 1 by simp also have "… = esize {i ∈ A. i < k}" by simp also have "… ≤ esize A" by blast finally show 2: "enat n < esize A" by this have 3: "n = card {i ∈ A. i < nth_least A n}" using 2 by simp have 4: "card {i ∈ A. i < nth_least A n} < card {i ∈ A. i < k}" using 1 2 by simp have 5: "nth_least A n ∈ A" using 2 by rule show "nth_least A n < k" using 4 5 by simp qed lemma nth_least_less_esize_less: "enat n < esize A ∧ enat (nth_least A n) < k ⟷ enat n < esize {i ∈ A. enat i < k}" using nth_least_less_card_less by (cases k, simp+) lemma nth_least_le: assumes "enat n < esize A" shows "n ≤ nth_least A n" using assms proof (induct n) case 0 show ?case using 0 by simp next case (Suc n) have "n ≤ nth_least A n" using Suc by (metis Suc_ile_eq less_imp_le) also have "… < nth_least A (Suc n)" using nth_least_strict_mono Suc(2) by blast finally show ?case by simp qed lemma nth_least_eq: assumes "enat n < esize A" "enat n < esize B" assumes "⋀ i. i ≤ nth_least A n ⟹ i ≤ nth_least B n ⟹ i ∈ A ⟷ i ∈ B" shows "nth_least A n = nth_least B n" using assms proof (induct n arbitrary: A B) case 0 have 1: "least A = least B" proof (rule least_eq) show "A ≠ {}" using 0(1) by simp show "B ≠ {}" using 0(2) by simp next fix i assume 2: "i ≤ least A" "i ≤ least B" show "i ∈ A ⟷ i ∈ B" using 0(3) 2 unfolding nth_least.simps by this qed show ?case using 1 by simp next case (Suc n) have 1: "A ≠ {}" "B ≠ {}" using Suc(2, 3) by auto have 2: "least A = least B" proof (rule least_eq) show "A ≠ {}" using 1(1) by this show "B ≠ {}" using 1(2) by this next fix i assume 3: "i ≤ least A" "i ≤ least B" have 4: "nth_least A 0 ≤ nth_least A (Suc n)" using Suc(2) by blast have 5: "nth_least B 0 ≤ nth_least B (Suc n)" using Suc(3) by blast have 6: "i ≤ nth_least A (Suc n)" "i ≤ nth_least B (Suc n)" using 3 4 5 by auto show "i ∈ A ⟷ i ∈ B" using Suc(4) 6 by this qed have 3: "nth_least (A - {least A}) n = nth_least (B - {least B}) n" proof (rule Suc(1)) show "enat n < esize (A - {least A})" using Suc(2) 1(1) by simp show "enat n < esize (B - {least B})" using Suc(3) 1(2) by simp next fix i assume 3: "i ≤ nth_least (A - {least A}) n" "i ≤ nth_least (B - {least B}) n" have 4: "i ≤ nth_least A (Suc n)" "i ≤ nth_least B (Suc n)" using 3 by simp+ have 5: "i ∈ A ⟷ i ∈ B" using Suc(4) 4 by this show "i ∈ A - {least A} ⟷ i ∈ B - {least B}" using 2 5 by auto qed show ?case using 3 by simp qed lemma nth_least_restrict[simp]: assumes "enat i < esize {i ∈ s. enat i < k}" shows "nth_least {i ∈ s. enat i < k} i = nth_least s i" proof (rule nth_least_eq) show "enat i < esize {i ∈ s. enat i < k}" using assms by this show "enat i < esize s" using nth_least_less_esize_less assms by auto next fix l assume 1: "l ≤ nth_least {i ∈ s. enat i < k} i" have 2: "nth_least {i ∈ s. enat i < k} i ∈ {i ∈ s. enat i < k}" using assms by rule have "enat l ≤ enat (nth_least {i ∈ s. enat i < k} i)" using 1 by simp also have "… < k" using 2 by simp finally show "l ∈ {i ∈ s. enat i < k} ⟷ l ∈ s" by auto qed lemma least_nth_least[simp]: assumes "A ≠ {}" "⋀ i. i ∈ A ⟹ enat i < esize B" shows "least (nth_least B ` A) = nth_least B (least A)" using assms by simp lemma nth_least_nth_least[simp]: assumes "enat n < esize A" "⋀ i. i ∈ A ⟹ enat i < esize B" shows "nth_least B (nth_least A n) = nth_least (nth_least B ` A) n" using assms proof (induct n arbitrary: A) case 0 show ?case using 0 by simp next case (Suc n) have 1: "A ≠ {}" using Suc(2) by auto have 2: "nth_least B ` (A - {least A}) = nth_least B ` A - nth_least B ` {least A}" proof (rule inj_on_image_set_diff) show "inj_on (nth_least B) {i. enat i < esize B}" using nth_least.inj_on by this show "A - {least A} ⊆ {i. enat i < esize B}" using Suc(3) by blast show "{least A} ⊆ {i. enat i < esize B}" using Suc(3) 1 by force qed have "nth_least B (nth_least A (Suc n)) = nth_least B (nth_least (A - {least A}) n)" by simp also have "… = nth_least (nth_least B ` (A - {least A})) n" using Suc 1 by force also have "… = nth_least (nth_least B ` A - nth_least B ` {least A}) n" unfolding 2 by rule also have "… = nth_least (nth_least B ` A - {nth_least B (least A)}) n" by simp also have "… = nth_least (nth_least B ` A - {least (nth_least B ` A)}) n" using Suc(3) 1 by auto also have "… = nth_least (nth_least B ` A) (Suc n)" by simp finally show ?case by this qed lemma nth_least_Max[simp]: assumes "finite A" "A ≠ {}" shows "nth_least A (card A - 1) = Max A" using assms proof (induct "card A - 1" arbitrary: A) case 0 have 1: "card A = 1" using 0 by (metis One_nat_def Suc_diff_1 card_gt_0_iff) obtain a where 2: "A = {a}" using 1 by rule show ?case unfolding 2 by (simp del: insert_iff) next case (Suc n) have 1: "least A ∈ A" using Suc(4) by rule have 2: "card (A - {least A}) = Suc n" using Suc(2, 3) 1 by simp have 3: "A - {least A} ≠ {}" using 2 Suc(3) by fastforce have "nth_least A (card A - 1) = nth_least A (Suc n)" unfolding Suc(2) by rule also have "… = nth_least (A - {least A}) n" by simp also have "… = nth_least (A - {least A}) (card (A - {least A}) - 1)" unfolding 2 by simp also have "… = Max (A - {least A})" proof (rule Suc(1)) show "n = card (A - {least A}) - 1" unfolding 2 by simp show "finite (A - {least A})" using Suc(3) by simp show "A - {least A} ≠ {}" using 3 by this qed also have "… = Max A" using Suc(3) 3 by simp finally show ?case by this qed lemma nth_least_le_Max: assumes "finite A" "A ≠ {}" "enat n < esize A" shows "nth_least A n ≤ Max A" proof - have "nth_least A n ≤ nth_least A (card A - 1)" proof (rule nth_least_mono) show "enat (card A - 1) < esize A" by (metis Suc_diff_1 Suc_ile_eq assms(1) assms(2) card_eq_0_iff esize_set.simps(1) not_gr0 order_refl) show "n ≤ card A - 1" by (metis Suc_diff_1 Suc_leI antisym_conv assms(1) assms(3) enat_ord_simps(2) esize_set.simps(1) le_less neq_iff not_gr0) qed also have "… = Max A" using nth_least_Max assms(1, 2) by this finally show ?thesis by this qed lemma nth_least_not_contains: fixes k :: nat assumes "enat (Suc n) < esize A" "nth_least A n < k" "k < nth_least A (Suc n)" shows "k ∉ A" proof assume 1: "k ∈ A" have 2: "nth_least A (card {i ∈ A. i < k}) = k" using nth_least.right_inverse 1 by this have 3: "n < card {i ∈ A. i < k}" proof (rule nth_least_strict_mono_inverse) show "enat n < esize A" using assms(1) by auto show "enat (card {i ∈ A. i < k}) < esize A" using nth_least.g.wellformed 1 by simp show "nth_least A n < nth_least A (card {i ∈ A. i < k})" using assms(2) 2 by simp qed have 4: "card {i ∈ A. i < k} < Suc n" proof (rule nth_least_strict_mono_inverse) show "enat (card {i ∈ A. i < k}) < esize A" using nth_least.g.wellformed 1 by simp show "enat (Suc n) < esize A" using assms(1) by this show "nth_least A (card {i ∈ A. i < k}) < nth_least A (Suc n)" using assms(3) 2 by simp qed show "False" using 3 4 by auto qed lemma nth_least_Suc[simp]: assumes "enat n < esize A" shows "nth_least (Suc ` A) n = Suc (nth_least A n)" using assms proof (induct n arbitrary: A) case (0) have 1: "A ≠ {}" using 0 by auto show ?case using 1 by simp next case (Suc n) have 1: "enat n < esize (A - {least A})" proof - have 2: "A ≠ {}" using Suc(2) by auto have 3: "least A ∈ A" using LeastI 2 by fast have 4: "A = insert (least A) A" using 3 by auto have "eSuc (enat n) = enat (Suc n)" by simp also have "… < esize A" using Suc(2) by this also have "… = esize (insert (least A) A)" using 4 by simp also have "… = eSuc (esize (A - {least A}))" using 3 2 by simp finally show ?thesis using Extended_Nat.eSuc_mono by metis qed have "nth_least (Suc ` A) (Suc n) = nth_least (Suc ` A - {least (Suc ` A)}) n" by simp also have "… = nth_least (Suc ` (A - {least A})) n" by simp also have "… = Suc (nth_least (A - {least A}) n)" using Suc(1) 1 by this also have "… = Suc (nth_least A (Suc n))" by simp finally show ?case by this qed lemma nth_least_lift[simp]: "nth_least (lift A) 0 = 0" "enat n < esize A ⟹ nth_least (lift A) (Suc n) = Suc (nth_least A n)" unfolding lift_def by simp+ lemma nth_least_list_card[simp]: assumes "enat n ≤ esize A" shows "card {k ∈ A. k < nth_least (lift A) n} = n" using less_Suc_eq_le assms by (cases n, auto simp del: nth_least.simps) end

# Theory Coinductive_List_Extensions

section ‹Coinductive Lists› theory Coinductive_List_Extensions imports Coinductive.Coinductive_List Coinductive.Coinductive_List_Prefix Coinductive.Coinductive_Stream "../Extensions/List_Extensions" "../Extensions/ESet_Extensions" begin hide_const (open) Sublist.prefix hide_const (open) Sublist.suffix declare list_of_lappend[simp] declare lnth_lappend1[simp] declare lnth_lappend2[simp] declare lprefix_llength_le[dest] declare Sup_llist_def[simp] declare length_list_of[simp] declare llast_linfinite[simp] declare lnth_ltake[simp] declare lappend_assoc[simp] declare lprefix_lappend[simp] lemma lprefix_lSup_revert: "lSup = Sup" "lprefix = less_eq" by auto lemma admissible_lprefixI[cont_intro]: assumes "mcont lub ord lSup lprefix f" assumes "mcont lub ord lSup lprefix g" shows "ccpo.admissible lub ord (λ x. lprefix (f x) (g x))" using ccpo_class.admissible_leI assms unfolding lprefix_lSup_revert by this lemma llist_lift_admissible: assumes "ccpo.admissible lSup lprefix P" assumes "⋀ u. u ≤ v ⟹ lfinite u ⟹ P u" shows "P v" using assms by (metis LNil_lprefix le_llist_conv_lprefix lfinite.simps llist_gen_induct) abbreviation "linfinite w ≡ ¬ lfinite w" notation LNil ("<>") notation LCons (infixr "%" 65) notation lzip (infixr "¦¦" 51) notation lappend (infixr "$" 65) notation lnth (infixl "?!" 100) syntax "_llist" :: "args ⇒ 'a llist" ("<_>") translations "<a, x>" ⇌ "a % <x>" "<a>" ⇌ "a % <>" lemma eq_LNil_conv_lnull[simp]: "w = <> ⟷ lnull w" by auto lemma Collect_lnull[simp]: "{w. lnull w} = {<>}" by auto lemma inj_on_ltake: "inj_on (λ k. ltake k w) {.. llength w