# Theory Degeneralization

```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
```