theory Degeneralization imports Acceptance Sequence_Zip begin type_synonym 'a degen = "'a × nat" definition degen :: "'a pred gen ⇒ 'a degen pred" where "degen cs ≡ λ (a, k). k ≥ length cs ∨ (cs ! k) a" lemma degen_simps[iff]: "degen cs (a, k) ⟷ k ≥ length cs ∨ (cs ! k) a" unfolding degen_def by simp definition count :: "'a pred gen ⇒ 'a ⇒ nat ⇒ nat" where "count cs a k ≡ if k < length cs then if (cs ! k) a then Suc k mod length cs else k else if cs = [] then k else 0" lemma count_empty[simp]: "count [] a k = k" unfolding count_def by simp lemma count_nonempty[simp]: "cs ≠ [] ⟹ count cs a k < length cs" unfolding count_def by simp lemma count_constant_1: assumes "k < length cs" assumes "⋀ a. a ∈ set w ⟹ ¬ (cs ! k) a" shows "fold (count cs) w k = k" using assms unfolding count_def by (induct w) (auto) lemma count_constant_2: assumes "k < length cs" assumes "⋀ a. a ∈ set (w || k # scan (count cs) w k) ⟹ ¬ degen cs a" shows "fold (count cs) w k = k" using assms unfolding count_def by (induct w) (auto) lemma count_step: assumes "k < length cs" assumes "(cs ! k) a" shows "count cs a k = Suc k mod length cs" using assms unfolding count_def by simp lemma degen_skip_condition: assumes "k < length cs" assumes "infs (degen cs) (w ||| k ## sscan (count cs) w k)" obtains u a v where "w = u @- a ## v" "fold (count cs) u k = k" "(cs ! k) a" proof - have 1: "Collect (degen cs) ∩ sset (w ||| k ## sscan (count cs) w k) ≠ {}" using infs_any assms(2) by auto obtain ys x zs where 2: "w ||| k ## sscan (count cs) w k = ys @- x ## zs" "Collect (degen cs) ∩ set ys = {}" "x ∈ Collect (degen cs)" using split_stream_first 1 by this define u where "u ≡ stake (length ys) w" define a where "a ≡ w !! length ys" define v where "v ≡ sdrop (Suc (length ys)) w" have "ys = stake (length ys) (w ||| k ## sscan (count cs) w k)" using shift_eq 2(1) by auto also have "… = stake (length ys) w || stake (length ys) (k ## sscan (count cs) w k)" by simp also have "… = take (length ys) u || take (length ys) (k # scan (count cs) u k)" unfolding u_def using append_eq_conv_conj length_stake length_zip stream.sel using sscan_stake stake.simps(2) stake_Suc stake_szip take_stake by metis also have "… = take (length ys) (u || k # scan (count cs) u k)" using take_zip by rule also have "… = u || k # scan (count cs) u k" unfolding u_def by simp finally have 3: "ys = u || k # scan (count cs) u k" by this have "x = (w ||| k ## sscan (count cs) w k) !! length ys" unfolding 2(1) by simp also have "… = (w !! length ys, (k ## sscan (count cs) w k) !! length ys)" by simp also have "… = (a, fold (count cs) u k)" unfolding u_def a_def by simp finally have 4: "x = (a, fold (count cs) u k)" by this have 5: "fold (count cs) u k = k" using count_constant_2 assms(1) 2(2) unfolding 3 by blast show ?thesis proof show "w = u @- a ## v" unfolding u_def a_def v_def using id_stake_snth_sdrop by this show "fold (count cs) u k = k" using 5 by this show "(cs ! k) a" using assms(1) 2(3) unfolding 4 5 by simp qed qed lemma degen_skip_arbitrary: assumes "k < length cs" "l < length cs" assumes "infs (degen cs) (w ||| k ## sscan (count cs) w k)" obtains u v where "w = u @- v" "fold (count cs) u k = l" using assms proof (induct "nat ((int l - int k) mod length cs)" arbitrary: l thesis) case (0) have 1: "length cs > 0" using assms(1) by auto have 2: "(int l - int k) mod length cs = 0" using 0(1) 1 by (auto intro: antisym) have 3: "int l mod length cs = int k mod length cs" using mod_eq_dvd_iff 2 by force have 4: "k = l" using 0(3, 4) 3 by simp show ?case proof (rule 0(2)) show "w = [] @- w" by simp show "fold (count cs) [] k = l" using 4 by simp qed next case (Suc n) have 1: "length cs > 0" using assms(1) by auto define l' where "l' = nat ((int l - 1) mod length cs)" obtain u v where 2: "w = u @- v" "fold (count cs) u k = l'" proof (rule Suc(1)) have 2: "Suc n < length cs" using nat_less_iff Suc(2) 1 by simp have "n = nat (int n)" by simp also have "int n = (int (Suc n) - 1) mod length cs" using 2 by simp also have "… = (int l - int k - 1) mod length cs" using Suc(2) by (simp add: mod_simps) also have "… = (int l - 1 - int k) mod length cs" by (simp add: algebra_simps) also have "… = (int l' - int k) mod length cs" using l'_def 1 by (simp add: mod_simps) finally show "n = nat ((int l' - int k) mod length cs)" by this show "k < length cs" using Suc(4) by this show "l' < length cs" using nat_less_iff l'_def 1 by simp show "infs (degen cs) (w ||| k ## sscan (count cs) w k)" using Suc(6) by this qed have 3: "l' < length cs" using nat_less_iff l'_def 1 by simp have 4: "v ||| l' ## sscan (count cs) v l' = sdrop (length u) (w ||| k ## sscan (count cs) w k)" using 2 eq_scons eq_shift by (metis sdrop.simps(2) sdrop_simps sdrop_szip sscan_scons_snth sscan_sdrop stream.sel(2)) have 5: "infs (degen cs) (v ||| l' ## sscan (count cs) v l')" using Suc(6) unfolding 4 by blast obtain vu a vv where 6: "v = vu @- a ## vv" "fold (count cs) vu l' = l'" "(cs ! l') a" using degen_skip_condition 3 5 by this have "l = nat (int l)" by simp also have "int l = int l mod length cs" using Suc(5) by simp also have "… = int (Suc l') mod length cs" using l'_def 1 by (simp add: mod_simps) finally have 7: "l = Suc l' mod length cs" using nat_mod_as_int by metis show ?case proof (rule Suc(3)) show "w = (u @ vu @ [a]) @- vv" unfolding 2(1) 6(1) by simp show "fold (count cs) (u @ vu @ [a]) k = l" using 2(2) 3 6(2, 3) 7 count_step by simp qed qed lemma degen_skip_arbitrary_condition: assumes "l < length cs" assumes "infs (degen cs) (w ||| k ## sscan (count cs) w k)" obtains u a v where "w = u @- a ## v" "fold (count cs) u k = l" "(cs ! l) a" proof - have 0: "cs ≠ []" using assms(1) by auto have 1: "count cs (shd w) k < length cs" using 0 by simp have 2: "infs (degen cs) (stl w ||| count cs (shd w) k ## sscan (count cs) (stl w) (count cs (shd w) k))" using assms(2) by (metis alw.cases sscan.code stream.sel(2) szip.simps(2)) obtain u v where 3: "stl w = u @- v" "fold (count cs) u (count cs (shd w) k) = l" using degen_skip_arbitrary 1 assms(1) 2 by this have 4: "v ||| l ## sscan (count cs) v l = sdrop (length u) (stl w ||| count cs (shd w) k ## sscan (count cs) (stl w) (count cs (shd w) k))" using 3 eq_scons eq_shift by (metis sdrop.simps(2) sdrop_simps sdrop_szip sscan_scons_snth sscan_sdrop stream.sel(2)) have 5: "infs (degen cs) (v ||| l ## sscan (count cs) v l)" using 2 unfolding 4 by blast obtain vu a vv where 6: "v = vu @- a ## vv" "fold (count cs) vu l = l" "(cs ! l) a" using degen_skip_condition assms(1) 5 by this show ?thesis proof show "w = (shd w # u @ vu) @- a ## vv" using 3(1) 6(1) by (simp add: eq_scons) show "fold (count cs) (shd w # u @ vu) k = l" using 3(2) 6(2) by simp show "(cs ! l) a" using 6(3) by this qed qed lemma gen_degen_step: assumes "gen infs cs w" obtains u a v where "w = u @- a ## v" "degen cs (a, fold (count cs) u k)" proof (cases "k < length cs") case True have 1: "infs (cs ! k) w" using assms True by auto have 2: "{a. (cs ! k) a} ∩ sset w ≠ {}" using infs_any 1 by auto obtain u a v where 3: "w = u @- a ## v" "{a. (cs ! k) a} ∩ set u = {}" "a ∈ {a. (cs ! k) a}" using split_stream_first 2 by this have 4: "fold (count cs) u k = k" using count_constant_1 True 3(2) by auto show ?thesis using 3(1, 3) 4 that by simp next case False show ?thesis proof show "w = [] @- shd w ## stl w" by simp show "degen cs (shd w, fold (count cs) [] k)" using False by simp qed qed lemma degen_infs[iff]: "infs (degen cs) (w ||| k ## sscan (count cs) w k) ⟷ gen infs cs w" proof show "gen infs cs w" if "infs (degen cs) (w ||| k ## sscan (count cs) w k)" proof fix c assume 1: "c ∈ set cs" obtain l where 2: "c = cs ! l" "l < length cs" using in_set_conv_nth 1 by metis show "infs c w" using that unfolding 2(1) proof (coinduction arbitrary: w k rule: infs_coinduct_shift) case (infs w k) obtain u a v where 3: "w = u @- a ## v" "(cs ! l) a" using degen_skip_arbitrary_condition 2(2) infs by this let ?k = "fold (count cs) u k" let ?l = "fold (count cs) (u @ [a]) k" have 4: "a ## v ||| ?k ## sscan (count cs) (a ## v) ?k = sdrop (length u) (w ||| k ## sscan (count cs) w k)" using 3(1) eq_shift scons_eq by (metis sdrop_simps(1) sdrop_stl sdrop_szip sscan_scons_snth sscan_sdrop stream.sel(2)) have 5: "infs (degen cs) (a ## v ||| ?k ## sscan (count cs) (a ## v) ?k)" using infs unfolding 4 by blast show ?case proof (intro exI conjI bexI) show "w = (u @ [a]) @- v" "(cs ! l) a" "a ∈ set (u @ [a])" "v = v" using 3 by auto show "infs (degen cs) (v ||| ?l ## sscan (count cs) v ?l)" using 5 by simp qed qed qed show "infs (degen cs) (w ||| k ## sscan (count cs) w k)" if "gen infs cs w" using that proof (coinduction arbitrary: w k rule: infs_coinduct_shift) case (infs w k) obtain u a v where 1: "w = u @- a ## v" "degen cs (a, fold (count cs) u k)" using gen_degen_step infs by this let ?u = "u @ [a] || k # scan (count cs) u k" let ?l = "fold (count cs) (u @ [a]) k" show ?case proof (intro exI conjI bexI) have "w ||| k ## sscan (count cs) w k = (u @ [a]) @- v ||| k ## scan (count cs) u k @- ?l ## sscan (count cs) v ?l" unfolding 1(1) by simp also have "… = ?u @- (v ||| ?l ## sscan (count cs) v ?l)" by (metis length_Cons length_append_singleton scan_length shift.simps(2) szip_shift) finally show "w ||| k ## sscan (count cs) w k = ?u @- (v ||| ?l ## sscan (count cs) v ?l)" by this show "degen cs (a, fold (count cs) u k)" using 1(2) by this have "(a, fold (count cs) u k) = (last (u @ [a]), last (k # scan (count cs) u k))" unfolding scan_last by simp also have "… = last ?u" by (simp add: zip_eq_Nil_iff) also have "… ∈ set ?u" by (fastforce intro: last_in_set simp: zip_eq_Nil_iff) finally show "(a, fold (count cs) u k) ∈ set ?u" by this show "v ||| ?l ## sscan (count cs) v ?l = v ||| ?l ## sscan (count cs) v ?l" by rule show "gen infs cs v" using infs unfolding 1(1) by auto qed qed qed end