# Theory List_More

(* Author: Dmitry Traytel *)

theory List_More
imports Main "List-Index.List_Index" "HOL-Library.Multiset"
begin

subsection ‹Library Functions›

abbreviation "bool_product_lists n ≡ product_lists (replicate n [True, False])"

lemma in_set_bool_product_lists[simp]:
"bs ∈ set (bool_product_lists n) ⟷ length bs = n"
proof (induct n arbitrary: bs)
case (Suc n) thus ?case by (cases bs) auto
qed simp

text ‹More on sort and remdups›

lemma insort_min[simp]: "∀y ∈ set xs. x < y ⟹ insort x xs = x # xs"
by (induct xs) auto

lemma insort_max[simp]: "∀y ∈ set xs. x > y ⟹ insort x xs = xs @ [x]"
by (induct xs) auto

lemma insort_snoc[simp]: "∀z ∈ set xs. y > z ⟹
insort x (xs @ [y]) = (if x < y then insort x xs @ [y] else xs @ [y, x])"
by (induct xs) auto

declare set_insort_key[simp]

lemma insort_remdups[simp]: "⟦sorted xs; a ∉ set xs⟧ ⟹ insort a (remdups xs) = remdups (insort a xs)"
proof (induct xs)
case (Cons x xs) thus ?case by (cases xs) (auto)
qed simp

lemma remdups_insort[simp]: "a ∈ set xs ⟹ remdups (insort a xs) = remdups xs"
by (induct xs) auto

lemma sort_remdups[simp]: "sort (remdups xs) = remdups (sort xs)"
by (induct xs) auto

lemma sort_map_insort[simp]: "sorted xs ⟹ sort (map f (insort a xs)) = insort (f a) (sort (map f xs))"
by (induct xs) (auto simp: insort_left_comm)

lemma sort_map_sort[simp]: "sort (map f (sort xs)) = sort (map f xs)"
by (induct xs) auto

lemma remdups_append: "remdups (xs @ ys) = remdups (filter (λx. x ∉ set ys) xs) @ remdups ys"
by (induct xs) auto

lemma remdups_concat_map_remdups:
"remdups (concat (map f (remdups xs))) = remdups (concat (map f xs))"
by (induct xs) (auto simp: remdups_append filter_empty_conv)

(*remdups'*)

primrec remdups' where
"remdups' f [] = []"
| "remdups' f (x # xs) =
(case List.find (λy. f x = f y) xs of None ⇒ x # remdups' f xs | _ ⇒ remdups' f xs)"

lemma map_remdups'[simp]: "map f (remdups' f xs) = remdups (map f xs)"
by (induct xs) (auto split: option.splits simp add: find_Some_iff find_None_iff)

lemma remdups'_map[simp]: "remdups' f (map g xs) = map g (remdups' (f o g) xs)"
by (induct xs) (auto split: option.splits simp add: find_None_iff,
auto simp: find_Some_iff elim: imageI[OF nth_mem])

lemma map_apfst_remdups':
"map (f o fst) (remdups' snd xs) = map fst (remdups' snd (map (apfst f) xs))"
by (auto simp: comp_def)

lemma set_remdups'[simp]: "f  set (remdups' f xs) = f  set xs"
by (induct xs) (auto split: option.splits simp add: find_Some_iff)

lemma subset_remdups': "set (remdups' f xs) ⊆ set xs"
by (induct xs) (auto split: option.splits)

lemma find_append[simp]:
"List.find P (xs @ ys) = None = (List.find P xs = None ∧ List.find P ys = None)"
by (induct xs) auto

lemma subset_remdups'_append: "set (remdups' f (xs @ ys)) ⊆ set (remdups' f xs) ∪ set (remdups' f ys)"
by (induct xs arbitrary: ys) (auto split: option.splits)

lemmas mp_remdups' = subsetD[OF subset_remdups']
lemmas mp_remdups'_append = subsetD[OF subset_remdups'_append]

lemma inj_on_set_remdups'[simp]: "inj_on f (set (remdups' f xs))"
by (induct xs) (auto split: option.splits simp add: find_None_iff dest!: mp_remdups')

lemma distinct_remdups'[simp]: "distinct (map f (remdups' f xs))"
by (induct xs) (auto split: option.splits simp: find_None_iff)

lemma distinct_remdups'_strong: "(∀x∈set xs. ∀y∈set xs. g x = g y ⟶ f x = f y) ⟹
distinct (map g (remdups' f xs))"
proof (induct xs)
case (Cons x xs) thus ?case
by (auto split: option.splits) (fastforce simp: find_None_iff dest!: mp_remdups')
qed simp

lemma set_remdups'_strong:
"f  set (remdups' g xs) = f  set xs" if "∀x∈set xs. ∀y∈set xs. g x = g y ⟶ f x = f y"
using that proof (induction xs)
case Nil
then show ?case
by simp
next
case (Cons x xs)
then have "∀x∈set xs. ∀y∈set xs. g x = g y ⟶ f x = f y"
by (auto simp only: set_simps)
then have "f  set (remdups' g xs) = f  set xs"
by (rule Cons.IH)
then show ?case
by (auto simp add: find_Some_iff split: option.splits)
(metis Cons.prems image_eqI list.set_intros(1) list.set_intros(2) nth_mem)
qed

(*multisets only needed below*)
lemma multiset_concat_gen: "M + mset (concat xs) = fold (λx M. M + mset x) xs M"
by (induct xs arbitrary: M) (auto, metis union_assoc)

corollary multiset_concat: "mset (concat xs) = fold (λx M. M + mset x) xs {#}"
using multiset_concat_gen[of "{#}" xs] by simp

lemma fold_mset_insort[simp]: "fold (λx M. M + mset (f x)) (insort x xs) M =
fold (λx M. M + mset (f x)) xs (mset (f x) + M)"
by (induct xs arbitrary: M) (auto simp: ac_simps)

lemma fold_mset_sort[simp]:
"fold (λx M. M + mset (f x)) (sort xs) M = fold (λx M. M + mset (f x)) xs M"
by (induct xs arbitrary: M) (auto simp: ac_simps)

lemma multiset_concat_map_sort[simp]:
"mset (concat (map f (sort xs))) = mset (concat (map f xs))"
by (auto simp: multiset_concat fold_map o_def)

lemma sort_concat_map_sort[simp]: "sort (concat (map f (sort xs))) = sort (concat (map f xs))"
by (auto intro: properties_for_sort)

end


# Theory Pi_Regular_Set

(*  Author: Tobias Nipkow, Alex Krauss, Dmitriy Traytel  *)

section "Regular Sets"

(*<*)
theory Pi_Regular_Set
imports Main
begin
(*>*)

type_synonym 'a lang = "'a list set"

definition conc :: "'a lang ⇒ 'a lang ⇒ 'a lang" (infixr "@@" 75) where
"A @@ B = {xs@ys | xs ys. xs:A & ys:B}"

lemma [code]:
"A @@ B = (%(xs, ys). xs @ ys)  (A × B)"
unfolding conc_def by auto

overloading word_pow == "compow :: nat ⇒ 'a list ⇒ 'a list"
begin
primrec word_pow :: "nat ⇒ 'a list ⇒ 'a list" where
"word_pow 0 w = []" |
"word_pow (Suc n) w = w @ word_pow n w"
end

overloading lang_pow == "compow :: nat ⇒ 'a lang ⇒ 'a lang"
begin
primrec lang_pow :: "nat ⇒ 'a lang ⇒ 'a lang" where
"lang_pow 0 A = {[]}" |
"lang_pow (Suc n) A = A @@ (lang_pow n A)"
end

lemma word_pow_alt: "compow n w = concat (replicate n w)"
by (induct n) auto

definition star :: "'a lang ⇒ 'a lang" where
"star A = (⋃n. A ^^ n)"

subsection‹Concatenation of Languages›

lemma concI[simp,intro]: "u : A ⟹ v : B ⟹ u@v : A @@ B"

lemma concE[elim]:
assumes "w ∈ A @@ B"
obtains u v where "u ∈ A" "v ∈ B" "w = u@v"
using assms by (auto simp: conc_def)

lemma conc_mono: "A ⊆ C ⟹ B ⊆ D ⟹ A @@ B ⊆ C @@ D"
by (auto simp: conc_def)

lemma conc_empty[simp]: shows "{} @@ A = {}" and "A @@ {} = {}"
by auto

lemma conc_epsilon[simp]: shows "{[]} @@ A = A" and "A @@ {[]} = A"

lemma conc_assoc: "(A @@ B) @@ C = A @@ (B @@ C)"
by (auto elim!: concE) (simp only: append_assoc[symmetric] concI)

lemma conc_Un_distrib:
shows "A @@ (B ∪ C) = A @@ B ∪ A @@ C"
and   "(A ∪ B) @@ C = A @@ C ∪ B @@ C"
by auto

lemma conc_UNION_distrib:
shows "A @@ ⋃(M  I) = ⋃((%i. A @@ M i)  I)"
and   "⋃(M  I) @@ A = ⋃((%i. M i @@ A)  I)"
by auto

lemma hom_image_conc: "⟦⋀xs ys. f (xs @ ys) = f xs @ f ys⟧ ⟹ f  (A @@ B) = f  A @@ f  B"
unfolding conc_def by (auto simp: image_iff) metis

lemma map_image_conc[simp]: "map f  (A @@ B) = map f  A @@ map f  B"

lemma conc_subset_lists: "A ⊆ lists S ⟹ B ⊆ lists S ⟹ A @@ B ⊆ lists S"
by(fastforce simp: conc_def in_lists_conv_set)

subsection‹Iteration of Languages›

lemma lang_pow_add: "A ^^ (n + m) = A ^^ n @@ A ^^ m"
by (induct n) (auto simp: conc_assoc)

lemma lang_pow_simps: "(A ^^ Suc n) = (A ^^ n @@ A)"
using lang_pow_add[of n "Suc 0" A] by auto

lemma lang_pow_empty: "{} ^^ n = (if n = 0 then {[]} else {})"
by (induct n) auto

lemma lang_pow_empty_Suc[simp]: "({}::'a lang) ^^ Suc n = {}"

lemma conc_pow_comm:
shows "A @@ (A ^^ n) = (A ^^ n) @@ A"
by (induct n) (simp_all add: conc_assoc[symmetric])

lemma length_lang_pow_ub:
"ALL w : A. length w ≤ k ⟹ w : A^^n ⟹ length w ≤ k*n"
by(induct n arbitrary: w) (fastforce simp: conc_def)+

lemma length_lang_pow_lb:
"ALL w : A. length w ≥ k ⟹ w : A^^n ⟹ length w ≥ k*n"
by(induct n arbitrary: w) (fastforce simp: conc_def)+

lemma lang_pow_subset_lists: "A ⊆ lists S ⟹ A ^^ n ⊆ lists S"
by (induct n) (auto simp: conc_subset_lists)

lemma star_subset_lists: "A ⊆ lists S ⟹ star A ⊆ lists S"
unfolding star_def by(blast dest: lang_pow_subset_lists)

lemma star_if_lang_pow[simp]: "w : A ^^ n ⟹ w : star A"
by (auto simp: star_def)

lemma Nil_in_star[iff]: "[] : star A"
proof (rule star_if_lang_pow)
show "[] : A ^^ 0" by simp
qed

lemma star_if_lang[simp]: assumes "w : A" shows "w : star A"
proof (rule star_if_lang_pow)
show "w : A ^^ 1" using ‹w : A› by simp
qed

lemma append_in_starI[simp]:
assumes "u : star A" and "v : star A" shows "u@v : star A"
proof -
from ‹u : star A› obtain m where "u : A ^^ m" by (auto simp: star_def)
moreover
from ‹v : star A› obtain n where "v : A ^^ n" by (auto simp: star_def)
thus ?thesis by simp
qed

lemma conc_star_star: "star A @@ star A = star A"
by (auto simp: conc_def)

lemma conc_star_comm:
shows "A @@ star A = star A @@ A"
unfolding star_def conc_pow_comm conc_UNION_distrib
by simp

lemma star_induct[consumes 1, case_names Nil append, induct set: star]:
assumes "w : star A"
and "P []"
and step: "!!u v. u : A ⟹ v : star A ⟹ P v ⟹ P (u@v)"
shows "P w"
proof -
{ fix n have "w : A ^^ n ⟹ P w"
by (induct n arbitrary: w) (auto intro: ‹P []› step star_if_lang_pow) }
with ‹w : star A› show "P w" by (auto simp: star_def)
qed

lemma star_empty[simp]: "star {} = {[]}"
by (auto elim: star_induct)

lemma star_epsilon[simp]: "star {[]} = {[]}"
by (auto elim: star_induct)

lemma star_idemp[simp]: "star (star A) = star A"
by (auto elim: star_induct)

lemma star_unfold_left: "star A = A @@ star A ∪ {[]}" (is "?L = ?R")
proof
show "?L ⊆ ?R" by (rule, erule star_induct) auto
qed auto

lemma concat_in_star: "set ws ⊆ A ⟹ concat ws : star A"
by (induct ws) simp_all

lemma in_star_iff_concat:
"w : star A = (EX ws. set ws ⊆ A & w = concat ws & [] ∉ set ws)"
(is "_ = (EX ws. ?R w ws)")
proof
assume "w : star A" thus "EX ws. ?R w ws"
proof induct
case Nil have "?R [] []" by simp
thus ?case ..
next
case (append u v)
moreover
then obtain ws where "set ws ⊆ A ∧ v = concat ws ∧ [] ∉ set ws" by blast
ultimately have "?R (u@v) (if u = [] then ws else u#ws)" by auto
thus ?case ..
qed
next
assume "EX us. ?R w us" thus "w : star A"
by (auto simp: concat_in_star)
qed

lemma star_conv_concat: "star A = {concat ws|ws. set ws ⊆ A & [] ∉ set ws}"
by (fastforce simp: in_star_iff_concat)

lemma star_insert_eps[simp]: "star (insert [] A) = star(A)"
proof-
{ fix us
have "set us ⊆ insert [] A ⟹ EX vs. concat us = concat vs ∧ set vs ⊆ A"
(is "?P ⟹ EX vs. ?Q vs")
proof
let ?vs = "filter (%u. u ≠ []) us"
show "?P ⟹ ?Q ?vs" by (induct us) auto
qed
} thus ?thesis by (auto simp: star_conv_concat)
qed

lemma star_decom:
assumes a: "x ∈ star A" "x ≠ []"
shows "∃a b. x = a @ b ∧ a ≠ [] ∧ a ∈ A ∧ b ∈ star A"
using a by (induct rule: star_induct) (blast)+

lemma Ball_starI: "∀a ∈ set as. [a] ∈ A ⟹ as ∈ star A"
by (induct as rule: rev_induct) auto

lemma map_image_star[simp]: "map f  star A = star (map f  A)"
by (auto elim: star_induct) (auto elim: star_induct simp del: map_append simp: map_append[symmetric] intro!: imageI)

subsection ‹Left-Quotients of Languages›

definition lQuot :: "'a ⇒ 'a lang ⇒ 'a lang"
where "lQuot x A = { xs. x#xs ∈ A }"

definition lQuots :: "'a list ⇒ 'a lang ⇒ 'a lang"
where "lQuots xs A = { ys. xs @ ys ∈ A }"

abbreviation
lQuotss :: "'a list ⇒ 'a lang set ⇒ 'a lang"
where
"lQuotss s As ≡ ⋃ (lQuots s  As)"

lemma lQuot_empty[simp]:   "lQuot a {} = {}"
and lQuot_epsilon[simp]: "lQuot a {[]} = {}"
and lQuot_char[simp]:    "lQuot a {[b]} = (if a = b then {[]} else {})"
and lQuot_chars[simp]:   "lQuot a {[b] | b. P b} = (if P a then {[]} else {})"
and lQuot_union[simp]:   "lQuot a (A ∪ B) = lQuot a A ∪ lQuot a B"
and lQuot_inter[simp]:   "lQuot a (A ∩ B) = lQuot a A ∩ lQuot a B"
and lQuot_compl[simp]:   "lQuot a (-A) = - lQuot a A"
by (auto simp: lQuot_def)

lemma lQuot_conc_subset: "lQuot a A @@ B ⊆ lQuot a (A @@ B)" (is "?L ⊆ ?R")
proof
fix w assume "w ∈ ?L"
then obtain u v where "w = u @ v" "a # u ∈ A" "v ∈ B"
by (auto simp: lQuot_def)
then have "a # w ∈ A @@ B"
by (auto intro: concI[of "a # u", simplified])
thus "w ∈ ?R" by (auto simp: lQuot_def)
qed

lemma lQuot_conc [simp]: "lQuot c (A @@ B) = (lQuot c A) @@ B ∪ (if [] ∈ A then lQuot c B else {})"
unfolding lQuot_def conc_def

lemma lQuot_star [simp]: "lQuot c (star A) = (lQuot c A) @@ star A"
proof -
have incl: "[] ∈ A ⟹ lQuot c (star A) ⊆ (lQuot c A) @@ star A"
unfolding lQuot_def conc_def
apply(drule star_decom)
done

have "lQuot c (star A) = lQuot c (A @@ star A ∪ {[]})"
by (simp only: star_unfold_left[symmetric])
also have "... = lQuot c (A @@ star A)"
by (simp only: lQuot_union) (simp)
also have "... =  (lQuot c A) @@ (star A) ∪ (if [] ∈ A then lQuot c (star A) else {})"
by simp
also have "... =  (lQuot c A) @@ star A"
using incl by auto
finally show "lQuot c (star A) = (lQuot c A) @@ star A" .
qed

lemma lQuot_diff[simp]: "lQuot c (A - B) = lQuot c A - lQuot c B"

lemma lQuot_lists[simp]: "c : S ⟹ lQuot c (lists S) = lists S"

lemma lQuots_simps [simp]:
shows "lQuots [] A = A"
and   "lQuots (c # s) A = lQuots s (lQuot c A)"
and   "lQuots (s1 @ s2) A = lQuots s2 (lQuots s1 A)"
unfolding lQuots_def lQuot_def by auto

lemma lQuots_append[iff]: "v ∈ lQuots w A ⟷ w @ v ∈ A"
by (induct w arbitrary: v A) (auto simp add: lQuot_def)

subsection ‹Right-Quotients of Languages›

definition rQuot :: "'a ⇒ 'a lang ⇒ 'a lang"
where "rQuot x A = { xs. xs @ [x] ∈ A }"

definition rQuots :: "'a list ⇒ 'a lang ⇒ 'a lang"
where "rQuots xs A = { ys. ys @ rev xs ∈ A }"

abbreviation
rQuotss :: "'a list ⇒ 'a lang set ⇒ 'a lang"
where
"rQuotss s As ≡ ⋃ (rQuots s  As)"

lemma rQuot_rev_lQuot: "rQuot x A = rev  lQuot x (rev  A)"
unfolding rQuot_def lQuot_def by (auto simp: rev_swap[symmetric])

lemma rQuots_rev_lQuots: "rQuots x A = rev  lQuots x (rev  A)"
unfolding rQuots_def lQuots_def by (auto simp: rev_swap[symmetric])

lemma rQuot_empty[simp]:   "rQuot a {} = {}"
and rQuot_epsilon[simp]: "rQuot a {[]} = {}"
and rQuot_char[simp]:    "rQuot a {[b]} = (if a = b then {[]} else {})"
and rQuot_union[simp]:   "rQuot a (A ∪ B) = rQuot a A ∪ rQuot a B"
and rQuot_inter[simp]:   "rQuot a (A ∩ B) = rQuot a A ∩ rQuot a B"
and rQuot_compl[simp]:   "rQuot a (-A) = - rQuot a A"
by (auto simp: rQuot_def)

lemma lQuot_rQuot: "lQuot a (rQuot b A) = rQuot b (lQuot a A)"
unfolding lQuot_def rQuot_def by auto

lemma rQuot_lQuot: "rQuot a (lQuot b A) = lQuot b (rQuot a A)"
unfolding lQuot_def rQuot_def by auto

lemma rev_simp_invert: "(xs @ [x] = rev zs) = (zs = x # rev xs)"
by (induct zs) auto

lemma rev_append_invert: "(xs @ ys = rev zs) = (zs = rev ys @ rev xs)"
by (induct xs arbitrary: ys rule: rev_induct) auto

lemma image_rev_lists[simp]: "rev  lists S = lists S"
proof (intro set_eqI)
fix xs
show "xs ∈ rev  lists S ⟷ xs ∈ lists S"
proof (induct xs rule: rev_induct)
case (snoc x xs)
thus ?case by (auto intro!: image_eqI[of _ rev] simp: rev_simp_invert)
qed simp
qed

lemma image_rev_conc[simp]: "rev  (A @@ B) = rev  B @@ rev  A"
by auto (auto simp: rev_append[symmetric] simp del: rev_append)

lemma image_rev_star[simp]: "rev  star A = star (rev  A)"
by (auto elim: star_induct) (auto elim: star_induct simp: rev_append[symmetric] simp del: rev_append)

lemma rQuot_conc [simp]: "rQuot c (A @@ B) = A @@ (rQuot c B) ∪ (if [] ∈ B then rQuot c A else {})"
unfolding rQuot_rev_lQuot by (auto simp: image_image image_Un)

lemma rQuot_star [simp]: "rQuot c (star A) = star A @@ (rQuot c A)"
unfolding rQuot_rev_lQuot by (auto simp: image_image)

lemma rQuot_diff[simp]: "rQuot c (A - B) = rQuot c A - rQuot c B"

lemma rQuot_lists[simp]: "c : S ⟹ rQuot c (lists S) = lists S"

lemma rQuots_simps [simp]:
shows "rQuots [] A = A"
and   "rQuots (c # s) A = rQuots s (rQuot c A)"
and   "rQuots (s1 @ s2) A = rQuots s2 (rQuots s1 A)"
unfolding rQuots_def rQuot_def by auto

lemma rQuots_append[iff]: "v ∈ rQuots w A ⟷ v @ rev w ∈ A"
by (induct w arbitrary: v A) (auto simp add: rQuot_def)

subsection ‹Two-Sided-Quotients of Languages›

definition biQuot :: "'a ⇒ 'a ⇒ 'a lang ⇒ 'a lang"
where "biQuot x y A = { xs. x # xs @ [y] ∈ A }"

definition biQuots :: "'a list ⇒ 'a list ⇒ 'a lang ⇒ 'a lang"
where "biQuots xs ys A = { zs. xs @ zs @ rev ys ∈ A }"

abbreviation
biQuotss :: "'a list ⇒ 'a list ⇒ 'a lang set ⇒ 'a lang"
where
"biQuotss xs ys As ≡ ⋃ (biQuots xs ys  As)"

lemma biQuot_rQuot_lQuot: "biQuot x y A = rQuot y (lQuot x A)"
unfolding biQuot_def rQuot_def lQuot_def by auto

lemma biQuot_lQuot_rQuot: "biQuot x y A = lQuot x (rQuot y A)"
unfolding biQuot_def rQuot_def lQuot_def by auto

lemma biQuots_rQuots_lQuots: "biQuots x y A = rQuots y (lQuots x A)"
unfolding biQuots_def rQuots_def lQuots_def by auto

lemma biQuots_lQuots_rQuots: "biQuots x y A = lQuots x (rQuots y A)"
unfolding biQuots_def rQuots_def lQuots_def by auto

lemma biQuot_empty[simp]:   "biQuot a b {} = {}"
and biQuot_epsilon[simp]: "biQuot a b {[]} = {}"
and biQuot_char[simp]:    "biQuot a b {[c]} = {}"
and biQuot_union[simp]:   "biQuot a b (A ∪ B) = biQuot a b A ∪ biQuot a b B"
and biQuot_inter[simp]:   "biQuot a b (A ∩ B) = biQuot a b A ∩ biQuot a b B"
and biQuot_compl[simp]:   "biQuot a b (-A) = - biQuot a b A"
by (auto simp: biQuot_def)

lemma biQuot_conc [simp]: "biQuot a b (A @@ B) =
lQuot a A @@ rQuot b B ∪
(if [] ∈ A ∧ [] ∈ B then biQuot a b A ∪ biQuot a b B
else if [] ∈ A then biQuot a b B
else if [] ∈ B then biQuot a b A
else {})"
unfolding biQuot_rQuot_lQuot by auto

lemma biQuot_star [simp]: "biQuot a b (star A) = biQuot a b A ∪ lQuot a A @@ star A @@ rQuot b A"
unfolding biQuot_rQuot_lQuot by auto

lemma biQuot_diff[simp]: "biQuot a b (A - B) = biQuot a b A - biQuot a b B"

lemma biQuot_lists[simp]: "a : S ⟹ b : S ⟹ biQuot a b (lists S) = lists S"

lemma biQuots_simps [simp]:
shows "biQuots [] [] A = A"
and   "biQuots (a#as) (b#bs) A = biQuots as bs (biQuot a b A)"
and   "⟦length s1 = length t1; length s2 = length t2⟧ ⟹
biQuots (s1 @ s2) (t1 @ t2) A = biQuots s2 t2 (biQuots s1 t1 A)"
unfolding biQuots_def biQuot_def by auto

lemma biQuots_append[iff]: "v ∈ biQuots u w A ⟷ u @ v @ rev w ∈ A"
unfolding biQuots_def by auto

subsection ‹Arden's Lemma›

lemma arden_helper:
assumes eq: "X = A @@ X ∪ B"
shows "X = (A ^^ Suc n) @@ X ∪ (⋃m≤n. (A ^^ m) @@ B)"
proof (induct n)
case 0
show "X = (A ^^ Suc 0) @@ X ∪ (⋃m≤0. (A ^^ m) @@ B)"
using eq by simp
next
case (Suc n)
have ih: "X = (A ^^ Suc n) @@ X ∪ (⋃m≤n. (A ^^ m) @@ B)" by fact
also have "… = (A ^^ Suc n) @@ (A @@ X ∪ B) ∪ (⋃m≤n. (A ^^ m) @@ B)" using eq by simp
also have "… = (A ^^ Suc (Suc n)) @@ X ∪ ((A ^^ Suc n) @@ B) ∪ (⋃m≤n. (A ^^ m) @@ B)"
by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm)
also have "… = (A ^^ Suc (Suc n)) @@ X ∪ (⋃m≤Suc n. (A ^^ m) @@ B)"
finally show "X = (A ^^ Suc (Suc n)) @@ X ∪ (⋃m≤Suc n. (A ^^ m) @@ B)" .
qed

lemma Arden:
assumes "[] ∉ A"
shows "X = A @@ X ∪ B ⟷ X = star A @@ B"
proof
assume eq: "X = A @@ X ∪ B"
{ fix w assume "w : X"
let ?n = "size w"
from ‹[] ∉ A› have "ALL u : A. length u ≥ 1"
by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
hence "ALL u : A^^(?n+1). length u ≥ ?n+1"
by (metis length_lang_pow_lb nat_mult_1)
hence "ALL u : A^^(?n+1)@@X. length u ≥ ?n+1"
by(auto simp only: conc_def length_append)
hence "w ∉ A^^(?n+1)@@X" by auto
hence "w : star A @@ B" using ‹w : X› using arden_helper[OF eq, where n="?n"]
by (auto simp add: star_def conc_UNION_distrib)
} moreover
{ fix w assume "w : star A @@ B"
hence "EX n. w : A^^n @@ B" by(auto simp: conc_def star_def)
hence "w : X" using arden_helper[OF eq] by blast
} ultimately show "X = star A @@ B" by blast
next
assume eq: "X = star A @@ B"
have "star A = A @@ star A ∪ {[]}"
by (rule star_unfold_left)
then have "star A @@ B = (A @@ star A ∪ {[]}) @@ B"
by metis
also have "… = (A @@ star A) @@ B ∪ B"
unfolding conc_Un_distrib by simp
also have "… = A @@ (star A @@ B) ∪ B"
by (simp only: conc_assoc)
finally show "X = A @@ X ∪ B"
using eq by blast
qed

lemma reversed_arden_helper:
assumes eq: "X = X @@ A ∪ B"
shows "X = X @@ (A ^^ Suc n) ∪ (⋃m≤n. B @@ (A ^^ m))"
proof (induct n)
case 0
show "X = X @@ (A ^^ Suc 0) ∪ (⋃m≤0. B @@ (A ^^ m))"
using eq by simp
next
case (Suc n)
have ih: "X = X @@ (A ^^ Suc n) ∪ (⋃m≤n. B @@ (A ^^ m))" by fact
also have "… = (X @@ A ∪ B) @@ (A ^^ Suc n) ∪ (⋃m≤n. B @@ (A ^^ m))" using eq by simp
also have "… = X @@ (A ^^ Suc (Suc n)) ∪ (B @@ (A ^^ Suc n)) ∪ (⋃m≤n. B @@ (A ^^ m))"
also have "… = X @@ (A ^^ Suc (Suc n)) ∪ (⋃m≤Suc n. B @@ (A ^^ m))"
finally show "X = X @@ (A ^^ Suc (Suc n)) ∪ (⋃m≤Suc n. B @@ (A ^^ m))" .
qed

theorem reversed_Arden:
assumes nemp: "[] ∉ A"
shows "X = X @@ A ∪ B ⟷ X = B @@ star A"
proof
assume eq: "X = X @@ A ∪ B"
{ fix w assume "w : X"
let ?n = "size w"
from ‹[] ∉ A› have "ALL u : A. length u ≥ 1"
by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
hence "ALL u : A^^(?n+1). length u ≥ ?n+1"
by (metis length_lang_pow_lb nat_mult_1)
hence "ALL u : X @@ A^^(?n+1). length u ≥ ?n+1"
by(auto simp only: conc_def length_append)
hence "w ∉ X @@ A^^(?n+1)" by auto
hence "w : B @@ star A" using ‹w : X› using reversed_arden_helper[OF eq, where n="?n"]
by (auto simp add: star_def conc_UNION_distrib)
} moreover
{ fix w assume "w : B @@ star A"
hence "EX n. w : B @@ A^^n" by (auto simp: conc_def star_def)
hence "w : X" using reversed_arden_helper[OF eq] by blast
} ultimately show "X = B @@ star A" by blast
next
assume eq: "X = B @@ star A"
have "star A = {[]} ∪ star A @@ A"
unfolding conc_star_comm[symmetric]
by(metis Un_commute star_unfold_left)
then have "B @@ star A = B @@ ({[]} ∪ star A @@ A)"
by metis
also have "… = B ∪ B @@ (star A @@ A)"
unfolding conc_Un_distrib by simp
also have "… = B ∪ (B @@ star A) @@ A"
by (simp only: conc_assoc)
finally show "X = X @@ A ∪ B"
using eq by blast
qed

subsection ‹Lists of Fixed Length›

abbreviation listsN where "listsN n S ≡ {xs. xs ∈ lists S ∧ length xs = n}"

lemma tl_listsN: "A ⊆ listsN (n + 1) S ⟹ tl  A ⊆ listsN n S"
proof (intro image_subsetI)
fix xs assume "A ⊆ listsN (n + 1) S" "xs ∈ A"
thus "tl xs ∈ listsN n S" by (induct xs) auto
qed

lemma map_tl_listsN: "A ⊆ lists (listsN (n + 1) S) ⟹ map tl  A ⊆ lists (listsN n S)"
proof (intro image_subsetI)
fix xss assume "A ⊆ lists (listsN (n + 1) S)" "xss ∈ A"
hence "set xss ⊆ listsN (n + 1) S" by auto
hence "∀xs ∈ set xss. tl xs ∈ listsN n S" using tl_listsN[of "set xss" S n] by auto
thus "map tl xss ∈ lists (listsN n S)" by (induct xss) auto
qed

(*<*)
end
(*>*)


# Theory Pi_Regular_Exp

(* Author: Dmitriy Traytel *)

section ‹$\Pi$-Extended Regular Expressions›

(*<*)
theory Pi_Regular_Exp
imports Pi_Regular_Set "HOL-Library.List_Lexorder" "HOL-Library.Code_Target_Nat"
Deriving.Compare_Instances
begin
(*>*)
subsection ‹Syntax of regular expressions›

datatype 'a rexp =
Zero |
Full |
One |
Atom 'a |
Plus "('a rexp)" "('a rexp)" |
Times "('a rexp)" "('a rexp)" |
Star "('a rexp)" |
Not "('a rexp)" |
Inter "('a rexp)" "('a rexp)" |
Pr "('a rexp)"
derive linorder rexp

text ‹Lifting constructors to lists›

fun rexp_of_list where
"rexp_of_list OPERATION N [] = N"
| "rexp_of_list OPERATION N [x] = x"
| "rexp_of_list OPERATION N (x # xs) = OPERATION x (rexp_of_list OPERATION N xs)"

abbreviation "PLUS ≡ rexp_of_list Plus Zero"
abbreviation "TIMES ≡ rexp_of_list Times One"
abbreviation "INTERSECT ≡ rexp_of_list Inter Full"

lemma list_singleton_induct [case_names nil single cons]:
assumes nil: "P []"
assumes single: "⋀x. P [x]"
assumes cons: "⋀x y xs. P (y # xs) ⟹ P (x # (y # xs))"
shows "P xs"
using assms
proof (induct xs)
case (Cons x xs) thus ?case by (cases xs) auto
qed simp

subsection ‹ACI normalization›

fun toplevel_summands :: "'a rexp ⇒ 'a rexp set" where
"toplevel_summands (Plus r s) = toplevel_summands r ∪ toplevel_summands s"
| "toplevel_summands r = {r}"

abbreviation (input) "flatten LISTOP X ≡ LISTOP (sorted_list_of_set X)"

lemma toplevel_summands_nonempty[simp]:
"toplevel_summands r ≠ {}"
by (induct r) auto

lemma toplevel_summands_finite[simp]:
"finite (toplevel_summands r)"
by (induct r) auto

primrec ACI_norm :: "('a::linorder) rexp ⇒ 'a rexp"  ("«_»") where
"«Zero» = Zero"
| "«Full» = Full"
| "«One» = One"
| "«Atom a» = Atom a"
| "«Plus r s» = flatten PLUS (toplevel_summands (Plus «r» «s»))"
| "«Times r s» = Times «r» «s»"
| "«Star r» = Star «r»"
| "«Not r» = Not «r»"
| "«Inter r s» = Inter «r» «s»"
| "«Pr r» = Pr «r»"

lemma Plus_toplevel_summands:
"Plus r s ∈ toplevel_summands t ⟹ False"
by (induct t) auto

lemma toplevel_summands_not_Plus[simp]:
"(∀r s. x ≠ Plus r s) ⟹ toplevel_summands x = {x}"
by (induct x) auto

lemma toplevel_summands_PLUS_strong:
"⟦xs ≠ []; list_all (λx. ¬(∃r s. x = Plus r s)) xs⟧ ⟹ toplevel_summands (PLUS xs) = set xs"
by (induct xs rule: list_singleton_induct) auto

lemma toplevel_summands_flatten:
"⟦X ≠ {}; finite X; ∀x ∈ X. ¬(∃r s. x = Plus r s)⟧ ⟹ toplevel_summands (flatten PLUS X) = X"
using toplevel_summands_PLUS_strong[of "sorted_list_of_set X"]
unfolding list_all_iff by fastforce

lemma ACI_norm_Plus:
"«r» = Plus s t ⟹ ∃s t. r = Plus s t"
by (induct r) auto

lemma toplevel_summands_flatten_ACI_norm_image:
"toplevel_summands (flatten PLUS (ACI_norm  toplevel_summands r)) = ACI_norm  toplevel_summands r"
by (intro toplevel_summands_flatten) (auto dest!: ACI_norm_Plus intro: Plus_toplevel_summands)

lemma toplevel_summands_flatten_ACI_norm_image_Union:
"toplevel_summands (flatten PLUS (ACI_norm  toplevel_summands r ∪ ACI_norm  toplevel_summands s)) =
ACI_norm  toplevel_summands r ∪ ACI_norm  toplevel_summands s"
by (intro toplevel_summands_flatten) (auto dest!: ACI_norm_Plus[OF sym] intro: Plus_toplevel_summands)

lemma toplevel_summands_ACI_norm:
"toplevel_summands «r» = ACI_norm  toplevel_summands r"
by (induct r) (auto simp: toplevel_summands_flatten_ACI_norm_image_Union)

lemma ACI_norm_flatten:
"«r» = flatten PLUS (ACI_norm  toplevel_summands r)"
by (induct r) (auto simp: image_Un toplevel_summands_flatten_ACI_norm_image)

theorem ACI_norm_idem[simp]:
"««r»» = «r»"
proof (induct r)
case (Plus r s)
have "««Plus r s»» = «flatten PLUS (toplevel_summands «r» ∪ toplevel_summands «s»)»"
(is "_ = «flatten PLUS ?U»") by simp
also have "… = flatten PLUS (ACI_norm  toplevel_summands (flatten PLUS ?U))"
by (simp only: ACI_norm_flatten)
also have "toplevel_summands (flatten PLUS ?U) = ?U"
by (intro toplevel_summands_flatten) (auto intro: Plus_toplevel_summands)
also have "flatten PLUS (ACI_norm  ?U) = flatten PLUS (toplevel_summands «r» ∪ toplevel_summands «s»)"
by (simp only: image_Un toplevel_summands_ACI_norm[symmetric] Plus)
finally show ?case by simp
qed auto

fun ACI_nPlus :: "'a::linorder rexp ⇒ 'a rexp ⇒ 'a rexp"
where
"ACI_nPlus (Plus r1 r2) s = ACI_nPlus r1 (ACI_nPlus r2 s)"
| "ACI_nPlus r (Plus s1 s2) =
(if r = s1 then Plus s1 s2
else if r < s1 then Plus r (Plus s1 s2)
else Plus s1 (ACI_nPlus r s2))"
| "ACI_nPlus r s =
(if r = s then r
else if r < s then Plus r s
else Plus s r)"

fun ACI_norm_alt where
"ACI_norm_alt Zero = Zero"
| "ACI_norm_alt Full = Full"
| "ACI_norm_alt One = One"
| "ACI_norm_alt (Atom a) = Atom a"
| "ACI_norm_alt (Plus r s) = ACI_nPlus (ACI_norm_alt r) (ACI_norm_alt s)"
| "ACI_norm_alt (Times r s) = Times (ACI_norm_alt r) (ACI_norm_alt s)"
| "ACI_norm_alt (Star r) = Star (ACI_norm_alt r)"
| "ACI_norm_alt (Not r) = Not (ACI_norm_alt r)"
| "ACI_norm_alt (Inter r s) = Inter (ACI_norm_alt r) (ACI_norm_alt s)"
| "ACI_norm_alt (Pr r) = Pr (ACI_norm_alt r)"

lemma toplevel_summands_ACI_nPlus:
"toplevel_summands (ACI_nPlus r s) = toplevel_summands (Plus r s)"
by (induct r s rule: ACI_nPlus.induct) auto

lemma toplevel_summands_ACI_norm_alt:
"toplevel_summands (ACI_norm_alt r) = ACI_norm_alt  toplevel_summands r"
by (induct r) (auto simp: toplevel_summands_ACI_nPlus)

lemma ACI_norm_alt_Plus:
"ACI_norm_alt r = Plus s t ⟹ ∃s t. r = Plus s t"
by (induct r) auto

lemma toplevel_summands_flatten_ACI_norm_alt_image:
"toplevel_summands (flatten PLUS (ACI_norm_alt  toplevel_summands r)) = ACI_norm_alt  toplevel_summands r"
by (intro toplevel_summands_flatten) (auto dest!: ACI_norm_alt_Plus intro: Plus_toplevel_summands)

lemma ACI_norm_ACI_norm_alt: "«ACI_norm_alt r» = «r»"
proof (induction r)
case (Plus r s) show ?case
using ACI_norm_flatten [of "ACI_norm_alt (Plus r s)"] ACI_norm_flatten [of "Plus r s"]
by (auto simp: image_Un toplevel_summands_ACI_nPlus)
(metis Plus.IH toplevel_summands_ACI_norm)
qed auto

lemma ACI_nPlus_singleton_PLUS:
"⟦xs ≠ []; sorted xs; distinct xs; ∀x ∈ {x} ∪ set xs. ¬(∃r s. x = Plus r s)⟧ ⟹
ACI_nPlus x (PLUS xs) = (if x ∈ set xs then PLUS xs else PLUS (insort x xs))"
proof (induct xs rule: list_singleton_induct)
case (single y)
thus ?case
by (cases x y rule: linorder_cases) (induct x y rule: ACI_nPlus.induct, auto)+
next
case (cons y1 y2 ys) thus ?case by (cases x) (auto)
qed simp

lemma ACI_nPlus_PLUS:
"⟦xs1 ≠ []; xs2 ≠ []; ∀x ∈ set (xs1 @ xs2). ¬(∃r s. x = Plus r s); sorted xs2; distinct xs2⟧⟹
ACI_nPlus (PLUS xs1) (PLUS xs2) = flatten PLUS (set (xs1 @ xs2))"
proof (induct xs1 arbitrary: xs2 rule: list_singleton_induct)
case (single x1) thus ?case
apply (auto intro!: trans[OF ACI_nPlus_singleton_PLUS] simp: insert_absorb simp del: sorted_list_of_set_insert)
apply (metis finite_set finite_sorted_distinct_unique sorted_list_of_set)
apply (metis remdups_id_iff_distinct sorted_list_of_set_sort_remdups sorted_sort_id)
done
next
case (cons x11 x12 xs1) thus ?case
apply (simp del: sorted_list_of_set_insert)
apply (rule trans[OF ACI_nPlus_singleton_PLUS])
apply (auto simp del: sorted_list_of_set_insert simp add: insert_commute[of x11])
apply (auto simp only: Un_insert_left[of x11, symmetric] insert_absorb) []
apply (auto simp only: Un_insert_right[of _ x11, symmetric] insert_absorb) []
apply (auto simp add: insert_commute[of x12])
done
qed simp

lemma ACI_nPlus_flatten_PLUS:
"⟦X1 ≠ {}; X2 ≠ {}; finite X1; finite X2; ∀x ∈ X1 ∪ X2. ¬(∃r s. x = Plus r s)⟧⟹
ACI_nPlus (flatten PLUS X1) (flatten PLUS X2) = flatten PLUS (X1 ∪ X2)"
by (rule trans[OF ACI_nPlus_PLUS]) auto

lemma ACI_nPlus_ACI_norm[simp]: "ACI_nPlus «r» «s» = «Plus r s»"
using ACI_norm_flatten [of r] ACI_norm_flatten [of s] ACI_norm_flatten [of "Plus r s"]
apply (auto intro!: trans [OF ACI_nPlus_flatten_PLUS])
apply (auto simp: image_Un Un_assoc  intro!: trans [OF ACI_nPlus_flatten_PLUS])
apply (metis ACI_norm_Plus Plus_toplevel_summands)+
done

lemma ACI_norm_alt:
"ACI_norm_alt r = «r»"
by (induct r) auto

declare ACI_norm_alt[symmetric, code]

subsection ‹Finality›

primrec final :: "'a rexp ⇒ bool"
where
"final Zero = False"
| "final Full = True"
| "final One = True"
| "final (Atom _) = False"
| "final (Plus r s) = (final r ∨ final s)"
| "final (Times r s) = (final r ∧ final s)"
| "final (Star _) = True"
| "final (Not r) = (~ final r)"
| "final (Inter r1 r2) = (final r1 ∧ final r2)"
| "final (Pr r) = final r"

lemma toplevel_summands_final:
"final s = (∃r∈toplevel_summands s. final r)"
by (induct s) auto

lemma final_PLUS:
"final (PLUS xs) = (∃r ∈ set xs. final r)"
by (induct xs rule: list_singleton_induct) auto

theorem ACI_norm_final[simp]:
"final «r» = final r"
proof (induct r)
case (Plus r1 r2) thus ?case using toplevel_summands_final by (auto simp: final_PLUS)
qed auto

subsection ‹Wellformedness w.r.t. an alphabet›

locale alphabet =
fixes Σ :: "nat ⇒ 'a set" ("Σ _")
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
begin

primrec wf :: "nat ⇒ 'b rexp ⇒ bool"
where
"wf n Zero = True" |
"wf n Full = True" |
"wf n One = True" |
"wf n (Atom a) = (wf_atom n a)" |
"wf n (Plus r s) = (wf n r ∧ wf n s)" |
"wf n (Times r s) = (wf n r ∧ wf n s)" |
"wf n (Star r) = wf n r" |
"wf n (Not r) = wf n r" |
"wf n (Inter r s) = (wf n r ∧ wf n s)" |
"wf n (Pr r) = wf (n + 1) r"

primrec wf_word where
"wf_word n [] = True"
| "wf_word n (w # ws) = ((w ∈ Σ n) ∧ wf_word n ws)"

lemma wf_word_snoc[simp]: "wf_word n (ws @ [w]) = ((w ∈ Σ n) ∧ wf_word n ws)"
by (induct ws) auto

lemma wf_word_append[simp]: "wf_word n (ws @ vs) = (wf_word n ws ∧ wf_word n vs)"
by (induct ws arbitrary: vs) auto

lemma wf_word: "wf_word n w = (w ∈ lists (Σ n))"
by (induct w) auto

lemma toplevel_summands_wf:
"wf n s = (∀r∈toplevel_summands s. wf n r)"
by (induct s) auto

lemma wf_PLUS[simp]:
"wf n (PLUS xs) = (∀r ∈ set xs. wf n r)"
by (induct xs rule: list_singleton_induct) auto

lemma wf_TIMES[simp]:
"wf n (TIMES xs) = (∀r ∈ set xs. wf n r)"
by (induct xs rule: list_singleton_induct) auto

lemma wf_flatten_PLUS[simp]:
"finite X ⟹ wf n (flatten PLUS X) = (∀r ∈ X. wf n r)"
using wf_PLUS[of n "sorted_list_of_set X"] by fastforce

theorem ACI_norm_wf[simp]:
"wf n «r» = wf n r"
proof (induct r arbitrary: n)
case (Plus r1 r2) thus ?case
using toplevel_summands_wf[of n "«r1»"] toplevel_summands_wf[of n "«r2»"] by auto
qed auto

lemma wf_INTERSECT[simp]:
"wf n (INTERSECT xs) = (∀r ∈ set xs. wf n r)"
by (induct xs rule: list_singleton_induct) auto

lemma wf_flatten_INTERSECT[simp]:
"finite X ⟹ wf n (flatten INTERSECT X) = (∀r ∈ X. wf n r)"
using wf_INTERSECT[of n "sorted_list_of_set X"] by fastforce

end

subsection ‹Language›

locale project =
alphabet Σ wf_atom for Σ :: "nat ⇒ 'a set" and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool" +
fixes project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool"
assumes project: "⋀a. a ∈ Σ (Suc n) ⟹ project a ∈ Σ n"
begin

primrec lang :: "nat ⇒ 'b rexp => 'a lang" where
"lang n Zero = {}" |
"lang n Full = lists (Σ n)" |
"lang n One = {[]}" |
"lang n (Atom b) = {[x] | x. lookup b x ∧ x ∈ Σ n}" |
"lang n (Plus r s) = (lang n r) ∪ (lang n s)" |
"lang n (Times r s) = conc (lang n r) (lang n s)" |
"lang n (Star r) = star (lang n r)" |
"lang n (Not r) = lists (Σ n) - lang n r" |
"lang n (Inter r s) = (lang n r ∩ lang n s)" |
"lang n (Pr r) = map project  lang (n + 1) r"

lemma wf_word_map_project[simp]: "wf_word (Suc n) ws ⟹ wf_word n (map project ws)"
by (induct ws arbitrary: n) (auto intro: project)

lemma wf_lang_wf_word: "wf n r ⟹ ∀w ∈ lang n r. wf_word n w"
by (induct r arbitrary: n) (auto elim: rev_subsetD[OF _ conc_mono] star_induct intro: iffD2[OF wf_word])

lemma lang_subset_lists: "wf n r ⟹ lang n r ⊆ lists (Σ n)"
proof (induct r arbitrary: n)
case Pr thus ?case by (fastforce intro!: project)
qed (auto simp: conc_subset_lists star_subset_lists)

lemma toplevel_summands_lang:
"r ∈ toplevel_summands s ⟹ lang n r ⊆ lang n s"
by (induct s) auto

lemma toplevel_summands_lang_UN:
"lang n s = (⋃r∈toplevel_summands s. lang n r)"
by (induct s) auto

lemma toplevel_summands_in_lang:
"w ∈ lang n s = (∃r∈toplevel_summands s. w ∈ lang n r)"
by (induct s) auto

lemma lang_PLUS[simp]:
"lang n (PLUS xs) = (⋃r ∈ set xs. lang n r)"
by (induct xs rule: list_singleton_induct) auto

lemma lang_TIMES[simp]:
"lang n (TIMES xs) = foldr (@@) (map (lang n) xs) {[]}"
by (induct xs rule: list_singleton_induct) auto

lemma lang_flatten_PLUS:
"finite X ⟹ lang n (flatten PLUS X) = (⋃r ∈ X. lang n r)"
using lang_PLUS[of n "sorted_list_of_set X"] by fastforce

theorem ACI_norm_lang[simp]:
"lang n «r» = lang n r"
proof (induct r arbitrary: n)
case (Plus r1 r2)
moreover
from Plus[symmetric] have "lang n (Plus r1 r2) ⊆ lang n «Plus r1 r2»"
using toplevel_summands_in_lang[of _ n "«r1»"] toplevel_summands_in_lang[of _ n "«r2»"]
by auto
ultimately show ?case by (fastforce dest!: toplevel_summands_lang)
qed auto

lemma lang_final: "final r = ([] ∈ lang n r)"
using concI[of "[]" _ "[]"] by (induct r arbitrary: n) auto

lemma in_lang_INTERSECT:
"wf_word n w ⟹ w ∈ lang n (INTERSECT xs) = (∀r ∈ set xs. w ∈ lang n r)"
by (induct xs rule: list_singleton_induct) (auto simp: wf_word)

lemma lang_INTERSECT:
"lang n (INTERSECT xs) = (if xs = [] then lists (Σ n) else ⋂r ∈ set xs. lang n r)"
by (induct xs rule: list_singleton_induct) auto

lemma lang_flatten_INTERSECT[simp]:
assumes "finite X" "X ≠ {}" "∀r∈X. wf n r"
shows "w ∈ lang n (flatten INTERSECT X) = (∀r ∈ X. w ∈ lang n r)" (is "?L = ?R")
proof
assume ?L
thus ?R using in_lang_INTERSECT[OF bspec[OF wf_lang_wf_word[OF iffD2[OF wf_flatten_INTERSECT]]],
OF assms(1,3) ‹?L›, of "sorted_list_of_set X"] assms(1)
by auto
next
assume ?R
with assms show ?L by (intro iffD2[OF in_lang_INTERSECT]) (auto dest: wf_lang_wf_word)
qed

end

(*<*)
end
(*>*)


# Theory Pi_Derivatives

(* Author: Dmitriy Traytel *)

section ‹Derivatives of $\Pi$-Extended Regular Expressions›
(*<*)
theory Pi_Derivatives
imports Pi_Regular_Exp
begin
(*>*)

locale embed = project Σ wf_atom project lookup
for Σ :: "nat ⇒ 'a set"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool" +
fixes embed :: "'a ⇒ 'a list"
assumes embed: "⋀a. a ∈ Σ n ⟹ b ∈ set (embed a) = (b ∈ Σ (Suc n) ∧ project b = a)"
begin

subsection ‹Syntactic Derivatives›

primrec lderiv :: "'a ⇒ 'b rexp ⇒ 'b rexp" where
"lderiv _ Zero = Zero"
| "lderiv _ Full = Full"
| "lderiv _ One = Zero"
| "lderiv a (Atom b) = (if lookup b a then One else Zero)"
| "lderiv a (Plus r s) = Plus (lderiv a r) (lderiv a s)"
| "lderiv a (Times r s) =
(let r's = Times (lderiv a r) s
in if final r then Plus r's (lderiv a s) else r's)"
| "lderiv a (Star r) = Times (lderiv a r) (Star r)"
| "lderiv a (Not r) = Not (lderiv a r)"
| "lderiv a (Inter r s) = Inter (lderiv a r) (lderiv a s)"
| "lderiv a (Pr r) = Pr (PLUS (map (λa'. lderiv a' r) (embed a)))"

primrec lderivs where
"lderivs [] r = r"
| "lderivs (w#ws) r = lderivs ws (lderiv w r)"

subsection ‹Finiteness of ACI-Equivalent Derivatives›

lemma toplevel_summands_lderiv:
"toplevel_summands (lderiv as r) = (⋃s∈toplevel_summands r. toplevel_summands (lderiv as s))"
by (induct r) (auto simp: Let_def)

lemma lderivs_Zero[simp]: "lderivs xs Zero = Zero"
by (induct xs) auto

lemma lderivs_Full[simp]: "lderivs xs Full = Full"
by (induct xs) auto

lemma lderivs_One: "lderivs xs One ∈ {Zero, One}"
by (induct xs) auto

lemma lderivs_Atom: "lderivs xs (Atom as) ∈ {Zero, One, Atom as}"
proof (induct xs)
case (Cons x xs) thus ?case by (auto intro: insertE[OF lderivs_One])
qed simp

lemma lderivs_Plus: "lderivs xs (Plus r s) = Plus (lderivs xs r) (lderivs xs s)"
by (induct xs arbitrary: r s) auto

lemma lderivs_PLUS: "lderivs xs (PLUS ys) = PLUS (map (lderivs xs) ys)"
by (induct ys rule: list_singleton_induct) (auto simp: lderivs_Plus)

lemma toplevel_summands_lderivs_Times: "toplevel_summands (lderivs xs (Times r s)) ⊆
{Times (lderivs xs r) s} ∪
{r'. ∃ys zs. r' ∈ toplevel_summands (lderivs ys s) ∧ ys ≠ [] ∧ zs @ ys = xs}"
proof (induct xs arbitrary: r s)
case (Cons x xs)
thus ?case by (auto simp: Let_def lderivs_Plus) (fastforce intro: exI[of _ "x#xs"])+
qed simp

lemma toplevel_summands_lderivs_Star_nonempty:
"xs ≠ [] ⟹ toplevel_summands (lderivs xs (Star r)) ⊆
{Times (lderivs ys r) (Star r) | ys. ∃zs. ys ≠ [] ∧ zs @ ys = xs}"
proof (induct xs rule: length_induct)
case (1 xs)
then obtain y ys where "xs = y # ys" by (cases xs) auto
thus ?case using spec[OF 1(1)]
by (auto dest!: subsetD[OF toplevel_summands_lderivs_Times] intro: exI[of _ "y#ys"])
(auto elim!: impE dest!: meta_spec subsetD)
qed

lemma toplevel_summands_lderivs_Star:
"toplevel_summands (lderivs xs (Star r)) ⊆
{Star r} ∪ {Times (lderivs ys r) (Star r) | ys. ∃zs. ys ≠ [] ∧ zs @ ys = xs}"
by (cases "xs = []") (auto dest!: toplevel_summands_lderivs_Star_nonempty)

lemma ex_lderivs_Pr: "∃s. lderivs ass (Pr r) = Pr s"
by (induct ass arbitrary: r) auto

lemma toplevel_summands_PLUS:
"xs ≠ [] ⟹ toplevel_summands (PLUS (map f xs)) = (⋃r ∈ set xs. toplevel_summands (f r))"
by (induct xs rule: list_singleton_induct) simp_all

lemma lderiv_toplevel_summands_Zero:
"⟦lderivs xs (Pr r) = Pr s; toplevel_summands r = {Zero}⟧ ⟹ toplevel_summands s = {Zero}"
proof (induct xs arbitrary: r s)
case (Cons y ys)
from Cons.prems(1) have "toplevel_summands (PLUS (map (λa. lderiv a r) (embed y))) = {Zero}"
proof (cases "embed y = []")
case False
show ?thesis using Cons.prems(2) unfolding toplevel_summands_PLUS[OF False]
by (subst toplevel_summands_lderiv) (simp add: False)
qed simp
with Cons show ?case by simp
qed simp

lemma toplevel_summands_lderivs_Pr:
"⟦xs ≠ []; lderivs xs (Pr r) = Pr s⟧ ⟹
toplevel_summands s ⊆ {Zero} ∨ toplevel_summands s ⊆ (⋃xs. toplevel_summands (lderivs xs r))"
proof (induct xs arbitrary: r s)
case (Cons y ys) note * = this
show ?case
proof (cases "embed y = []")
case True with Cons show ?thesis by (cases "ys = []") (auto dest: lderiv_toplevel_summands_Zero)
next
case False
show ?thesis
proof (cases ys)
case Nil with * show ?thesis
by (auto simp: toplevel_summands_PLUS[OF False]) (metis lderivs.simps)
next
case (Cons z zs)
have "toplevel_summands s ⊆ {Zero} ∨ toplevel_summands s ⊆
(⋃xs. toplevel_summands (lderivs xs (PLUS (map (λa. lderiv a r) (embed y)))))" (is "_ ∨ ?B")
by (rule *(1)) (auto simp: Cons *(3)[symmetric])
thus ?thesis
proof
assume ?B
also have "… ⊆ (⋃xs. toplevel_summands (lderivs xs r))"
by (auto simp: lderivs_PLUS toplevel_summands_PLUS[OF False]) (metis lderivs.simps(2))
finally show ?thesis ..
qed blast
qed
qed
qed simp

lemma lderivs_Pr:
"{lderivs xs (Pr r) | xs. True} ⊆
{Pr s | s. toplevel_summands s ⊆ {Zero} ∨
toplevel_summands s ⊆ (⋃xs. toplevel_summands (lderivs xs r))}"
(is "?L ⊆?R")
proof (rule subsetI)
fix s assume "s ∈ ?L"
then obtain xs where "s = lderivs xs (Pr r)" by blast
moreover obtain t where "lderivs xs (Pr r) = Pr t" using ex_lderivs_Pr by blast
ultimately show "s ∈ ?R"
by (cases "xs = []") (auto dest!: toplevel_summands_lderivs_Pr elim!: allE[of _ "[]"])
qed

lemma ACI_norm_toplevel_summands_Zero: "toplevel_summands r ⊆ {Zero} ⟹ «r» = Zero"
by (subst ACI_norm_flatten) (auto dest: subset_singletonD)

lemma ACI_norm_lderivs_Pr:
"ACI_norm  {lderivs xs (Pr r) | xs. True} ⊆
{Pr Zero} ∪ {Pr «s» | s. toplevel_summands s ⊆ (⋃xs. toplevel_summands «lderivs xs r»)}"
proof (intro subset_trans[OF image_mono[OF lderivs_Pr]] subsetI,
elim imageE CollectE exE conjE disjE)
fix x x' s :: "'b rexp"
assume *: "x = «x'»" "x' = Pr s" and "toplevel_summands s ⊆ {Zero}"
hence "«Pr s» = Pr Zero" using ACI_norm_toplevel_summands_Zero by simp
thus "x ∈ {Pr Zero} ∪
{Pr «s» |s. toplevel_summands s ⊆ (⋃xs. toplevel_summands «lderivs xs r»)}"
unfolding * by blast
next
fix x x' s :: "'b rexp"
assume *: "x = «x'»" "x' = Pr s" and "toplevel_summands s ⊆ (⋃xs. toplevel_summands (lderivs xs r))"
hence "toplevel_summands «s» ⊆ (⋃xs. toplevel_summands «lderivs xs r»)"
by (fastforce simp: toplevel_summands_ACI_norm)
moreover have "x = Pr ««s»»" unfolding * ACI_norm_idem ACI_norm.simps(10) ..
ultimately show "x ∈ {Pr Zero} ∪
{Pr «s» |s. toplevel_summands s ⊆ (⋃xs. toplevel_summands «lderivs xs r»)}"
by blast
qed

lemma finite_ACI_norm_toplevel_summands: "finite B ⟹ finite {f «s» |s. toplevel_summands s ⊆ B}"
apply (elim finite_surj [OF iffD2 [OF finite_Pow_iff], of _ _ "f o flatten PLUS o image ACI_norm"])
apply (subst ACI_norm_flatten)
apply auto
done

lemma lderivs_Not: "lderivs xs (Not r) = Not (lderivs xs r)"
by (induct xs arbitrary: r) auto

lemma lderivs_Inter: "lderivs xs (Inter r s) = Inter (lderivs xs r) (lderivs xs s)"
by (induct xs arbitrary: r s) auto

theorem finite_lderivs: "finite {«lderivs xs r» | xs . True}"
proof (induct r)
case Zero show ?case by simp
next
case Full show ?case by simp
next
case One show ?case
by (rule finite_surj[of "{Zero, One}"]) (blast intro: insertE[OF lderivs_One])+
next
case (Atom as) show ?case
by (rule finite_surj[of "{Zero, One, Atom as}"]) (blast intro: insertE[OF lderivs_Atom])+
next
case (Plus r s)
show ?case by (auto simp: lderivs_Plus intro!: finite_surj[OF finite_cartesian_product[OF Plus]])
next
case (Times r s)
hence "finite (⋃ (toplevel_summands  {«lderivs xs s» | xs . True}))" by auto
moreover have "{«r'» |r'. ∃ys. r' ∈ toplevel_summands (lderivs ys s)} =
{r'. ∃ys. r' ∈ toplevel_summands «lderivs ys s»}"
unfolding toplevel_summands_ACI_norm by auto
ultimately have fin: "finite {«r'» |r'. ∃ys. r' ∈ toplevel_summands (lderivs ys s)}"
by (fastforce intro: finite_subset[of _ "⋃ (toplevel_summands  {«lderivs xs s» | xs . True})"])
let ?X = "λxs. {Times (lderivs ys r) s | ys. True} ∪ {r'. r' ∈ (⋃ys. toplevel_summands (lderivs ys s))}"
show ?case
proof (simp only: ACI_norm_flatten,
rule finite_surj[of "{X. ∃xs. X ⊆ ACI_norm  ?X xs}" _ "flatten PLUS"])
show "finite {X. ∃xs. X ⊆ ACI_norm  ?X xs}"
using fin by (fastforce simp: image_Un elim: finite_subset[rotated] intro: finite_surj[OF Times(1), of _ "λr. Times r «s»"])
qed (fastforce dest!: subsetD[OF toplevel_summands_lderivs_Times] intro!: imageI)
next
case (Star r)
let ?f = "λf r'. Times r' (Star (f r))"
let ?X = "{Star r} ∪ ?f id  {r'. r' ∈ {lderivs ys r|ys. True}}"
show ?case
proof (simp only: ACI_norm_flatten,
rule finite_surj[of "{X. X ⊆ ACI_norm  ?X}" _ "flatten PLUS"])
have *: "⋀X. ACI_norm  ?f (λx. x)  X = ?f ACI_norm  ACI_norm  X" by (auto simp: image_def)
show "finite {X. X ⊆ ACI_norm  ?X}"
by (rule finite_Collect_subsets)
(auto simp: * intro!: finite_imageI[of _ "?f ACI_norm"] intro: finite_subset[OF _ Star])
qed (fastforce dest!: subsetD[OF toplevel_summands_lderivs_Star] intro!: imageI)
next
case (Not r) thus ?case by (auto simp: lderivs_Not) (blast intro: finite_surj)
next
case (Inter r s)
show ?case by (auto simp: lderivs_Inter intro!: finite_surj[OF finite_cartesian_product[OF Inter]])
next
case (Pr r)
hence *: "finite (⋃ (toplevel_summands  {«lderivs xs r» | xs . True}))" by auto
have "finite (⋃xs. toplevel_summands «lderivs xs r»)" by (rule finite_subset[OF _ *]) auto
hence fin: "finite {Pr «s» |s. toplevel_summands s ⊆ (⋃xs. toplevel_summands «lderivs xs r»)}"
by (intro finite_ACI_norm_toplevel_summands)
have "{s. ∃xs. s = «lderivs xs (Pr r)»} = {«s»| s. ∃xs. s = lderivs xs (Pr r)}" by auto
thus ?case using finite_subset[OF ACI_norm_lderivs_Pr, of r] fin unfolding image_Collect by auto
qed

subsection ‹Wellformedness and language of derivatives›

lemma wf_lderiv[simp]: "wf n r ⟹ wf n (lderiv w r)"
by (induct r arbitrary: n w) (auto simp add: Let_def)

lemma wf_lderivs[simp]: "wf n r ⟹ wf n (lderivs ws r)"
by (induct ws arbitrary: r) (auto intro: wf_lderiv)

lemma lQuot_map_project:
assumes "as ∈ Σ n" "A ⊆ lists (Σ (Suc n))"
shows "lQuot as (map project  A) = map project  (⋃a ∈ set (embed as). lQuot a A)" (is "?L = ?R")
proof (intro equalityI image_subsetI subsetI)
fix xss assume "xss ∈ ?L"
with assms obtain zss
where zss: "zss ∈ A" "as # xss = map project zss"
unfolding lQuot_def by fastforce
hence "xss = map project (tl zss)" by auto
with zss assms(2) show "xss ∈ ?R" using embed[OF project, of _ n] unfolding lQuot_def by fastforce
next
fix xss assume "xss ∈ (⋃a ∈ set (embed as). lQuot a A)"
with assms(1) show "map project xss ∈ lQuot as (map project  A)" unfolding lQuot_def
by (fastforce intro!: rev_image_eqI simp: embed)
qed

lemma lang_lderiv: "⟦wf n r; w ∈ Σ n⟧ ⟹ lang n (lderiv w r) = lQuot w (lang n r)"
proof (induct r arbitrary: n w)
case (Pr r)
hence *: "wf (Suc n) r" "⋀w'. w' ∈ set (embed w) ⟹  w' ∈ Σ (Suc n)" by (auto simp: embed)
from Pr(1)[OF *] lQuot_map_project[OF Pr(3) lang_subset_lists[OF *(1)]] show ?case
by (auto simp: wf_lderiv[OF *(1)])
qed (auto simp: Let_def lang_final[symmetric])

lemma lang_lderivs: "⟦wf n r; wf_word n ws⟧ ⟹ lang n (lderivs ws r) = lQuots ws (lang n r)"
by (induct ws arbitrary: r) (auto simp: lang_lderiv)

corollary lderivs_final:
assumes "wf n r" "wf_word n ws"
shows "final (lderivs ws r) ⟷ ws ∈ lang n r"
using lang_lderivs[OF assms] lang_final[of "lderivs ws r" n] by auto

abbreviation "lderivs_set n r s ≡ {(«lderivs w r», «lderivs w s») | w. wf_word n w}"

subsection ‹Deriving preserves ACI-equivalence›

lemma ACI_norm_PLUS:
"list_all2 (λr s. «r» = «s») xs ys ⟹ «PLUS xs» = «PLUS ys»"
proof (induct rule: list_all2_induct)
case (Cons x xs y ys)
hence "length xs = length ys" by (elim list_all2_lengthD)
thus ?case using Cons by (induct xs ys rule: list_induct2) auto
qed simp

lemma toplevel_summands_ACI_norm_lderiv:
"(⋃a∈toplevel_summands r. toplevel_summands «lderiv as «a»») = toplevel_summands «lderiv as «r»»"
proof (induct r)
case (Plus r1 r2) thus ?case
unfolding toplevel_summands.simps toplevel_summands_ACI_norm
toplevel_summands_lderiv[of as "«Plus r1 r2»"] image_Un Union_Un_distrib
qed (auto simp: Let_def)

theorem ACI_norm_lderiv:
"«lderiv as «r»» = «lderiv as r»"
proof (induct r arbitrary: as)
case (Plus r1 r2) thus ?case
unfolding lderiv.simps ACI_norm_flatten[of "lderiv as «Plus r1 r2»"]
toplevel_summands_lderiv[of as "«Plus r1 r2»"] image_Un image_UN
by (auto simp: toplevel_summands_ACI_norm toplevel_summands_flatten_ACI_norm_image_Union)
(auto simp: toplevel_summands_ACI_norm[symmetric] toplevel_summands_ACI_norm_lderiv)
next
case (Pr r)
hence "list_all2 (λr s. «r» = «s»)
(map (λa. lderiv a «r») (embed as)) (map (λa. lderiv a r) (embed as))"
unfolding list_all2_map1 list_all2_map2 by (intro list_all2_refl)
thus ?case unfolding lderiv.simps ACI_norm.simps by (blast intro: ACI_norm_PLUS)

corollary lderiv_preserves: "«r» = «s» ⟹ «lderiv as r» = «lderiv as s»"
by (rule box_equals[OF _ ACI_norm_lderiv ACI_norm_lderiv]) (erule arg_cong)

lemma lderivs_snoc[simp]: "lderivs (ws @ [w]) r = (lderiv w (lderivs ws r))"
by (induct ws arbitrary: r) auto

theorem ACI_norm_lderivs:
"«lderivs ws «r»» = «lderivs ws r»"
proof (induct ws arbitrary: r rule: rev_induct)
case (snoc w ws) thus ?case
using ACI_norm_lderiv[of w "lderivs ws r"] ACI_norm_lderiv[of w "lderivs ws «r»"] by auto
qed simp

lemma lderivs_alt: "«lderivs w r» = fold (λa r. «lderiv a r») w «r»"
by (induct w arbitrary: r) (auto simp: ACI_norm_lderiv)

lemma finite_fold_lderiv: "finite {fold (λa r. «lderiv a r») w «s» |w. True}"
using finite_lderivs unfolding lderivs_alt .

end

(*<*)
end
(*>*)


# Theory Pi_Regular_Operators

(* Author: Dmitriy Traytel *)

section "Some Useful Regular Operators"

(*<*)
theory Pi_Regular_Operators
imports Pi_Derivatives "HOL-Library.While_Combinator"
begin
(*>*)

primrec REV :: "'a rexp ⇒ 'a rexp" where
"REV Zero = Zero"
| "REV Full = Full"
| "REV One = One"
| "REV (Atom a) = Atom a"
| "REV (Plus r s) = Plus (REV r) (REV s)"
| "REV (Times r s) = Times (REV s) (REV r)"
| "REV (Star r) = Star (REV r)"
| "REV (Not r) = Not (REV r)"
| "REV (Inter r s) = Inter (REV r) (REV s)"
| "REV (Pr r) = Pr (REV r)"

lemma REV_REV[simp]: "REV (REV r) = r"
by (induct r) auto

lemma final_REV[simp]: "final (REV r) = final r"
by (induct r) auto

lemma REV_PLUS: "REV (PLUS xs) = PLUS (map REV xs)"
by (induct xs rule: list_singleton_induct) auto

lemma (in alphabet) wf_REV[simp]: "wf n r ⟹ wf n (REV r)"
by (induct r arbitrary: n) auto

lemma (in project) lang_REV[simp]: "lang n (REV r) = rev  lang n r"
by (induct r arbitrary: n) (auto simp: image_image rev_map image_set_diff)

context embed
begin

primrec rderiv :: "'a ⇒ 'b rexp ⇒ 'b rexp" where
"rderiv _ Zero = Zero"
| "rderiv _ Full = Full"
| "rderiv _ One = Zero"
| "rderiv a (Atom b) = (if lookup b a then One else Zero)"
| "rderiv a (Plus r s) = Plus (rderiv a r) (rderiv a s)"
| "rderiv a (Times r s) =
(let rs' = Times r (rderiv a s)
in if final s then Plus rs' (rderiv a r) else rs')"
| "rderiv a (Star r) = Times (Star r) (rderiv a r)"
| "rderiv a (Not r) = Not (rderiv a r)"
| "rderiv a (Inter r s) = Inter (rderiv a r) (rderiv a s)"
| "rderiv a (Pr r) = Pr (PLUS (map (λa'. rderiv a' r) (embed a)))"

primrec rderivs where
"rderivs [] r = r"
| "rderivs (w#ws) r = rderivs ws (rderiv w r)"

lemma rderivs_snoc: "rderivs (ws @ [w]) r = rderiv w (rderivs ws r)"
by (induct ws arbitrary: r) auto

lemma rderivs_append: "rderivs (ws @ ws') r = rderivs ws' (rderivs ws r)"
by (induct ws arbitrary: r) auto

lemma rderiv_lderiv: "rderiv as r = REV (lderiv as (REV r))"
by (induct r arbitrary: as) (auto simp: Let_def o_def REV_PLUS)

lemma rderivs_lderivs: "rderivs w r = REV (lderivs w (REV r))"
by (induct w arbitrary: r) (auto simp: rderiv_lderiv)

lemma wf_rderiv[simp]: "wf n r ⟹ wf n (rderiv w r)"
unfolding rderiv_lderiv by (rule wf_REV[OF wf_lderiv[OF wf_REV]])

lemma wf_rderivs[simp]: "wf n r ⟹ wf n (rderivs ws r)"
unfolding rderivs_lderivs by (rule wf_REV[OF wf_lderivs[OF wf_REV]])

lemma lang_rderiv: "⟦wf n r; as ∈ Σ n⟧ ⟹ lang n (rderiv as r) = rQuot as (lang n r)"
unfolding rderiv_lderiv rQuot_rev_lQuot by (simp add: lang_lderiv)

lemma lang_rderivs: "⟦wf n r; wf_word n w⟧ ⟹ lang n (rderivs w r) = rQuots w (lang n r)"
unfolding rderivs_lderivs rQuots_rev_lQuots by (simp add: lang_lderivs)

corollary rderivs_final:
assumes "wf n r" "wf_word n w"
shows "final (rderivs w r) ⟷ rev w ∈ lang n r"
using lang_rderivs[OF assms] lang_final[of "rderivs w r" n] by auto

lemma toplevel_summands_REV[simp]: "toplevel_summands (REV r) = REV  toplevel_summands r"
by (induct r) auto

lemma ACI_norm_REV: "«REV «r»» = «REV r»"
proof (induct r)
case (Plus r s)
show ?case
using [[unfold_abs_def = false]]
unfolding REV.simps ACI_norm.simps Plus[symmetric] image_Un[symmetric]
toplevel_summands.simps(1) toplevel_summands_ACI_norm toplevel_summands_REV
unfolding toplevel_summands.simps(1)[symmetric] ACI_norm_flatten toplevel_summands_REV
unfolding ACI_norm_flatten[symmetric] toplevel_summands_ACI_norm
..
qed auto

lemma ACI_norm_rderiv: "«rderiv as «r»» = «rderiv as r»"
unfolding rderiv_lderiv by (metis ACI_norm_REV ACI_norm_lderiv)

lemma ACI_norm_rderivs: "«rderivs w «r»» = «rderivs w r»"
unfolding rderivs_lderivs by (metis ACI_norm_REV ACI_norm_lderivs)

theorem finite_rderivs: "finite {«rderivs xs r» | xs . True}"
unfolding rderivs_lderivs
by (subst ACI_norm_REV[symmetric]) (auto intro: finite_surj[OF finite_lderivs, of _ "λr. «REV r»"])

lemma lderiv_PLUS[simp]: "lderiv a (PLUS xs) = PLUS (map (lderiv a) xs)"
by (induct xs rule: list_singleton_induct) auto

lemma rderiv_PLUS[simp]: "rderiv a (PLUS xs) = PLUS (map (rderiv a) xs)"
by (induct xs rule: list_singleton_induct) auto

lemma lang_rderiv_lderiv: "lang n (rderiv a (lderiv b r)) = lang n (lderiv b (rderiv a r))"
by (induct r arbitrary: n a b) (auto simp: Let_def conc_assoc)

lemma lang_lderiv_rderiv: "lang n (lderiv a (rderiv b r)) = lang n (rderiv b (lderiv a r))"
by (induct r arbitrary: n a b) (auto simp: Let_def conc_assoc)

lemma lang_rderiv_lderivs[simp]: "⟦wf n r; wf_word n w; a ∈ Σ n⟧ ⟹
lang n (rderiv a (lderivs w r)) = lang n (lderivs w (rderiv a r))"
by (induct w arbitrary: n r)
(auto, auto simp: lang_lderivs lang_lderiv lang_rderiv lQuot_rQuot)

lemma lang_lderiv_rderivs[simp]: "⟦wf n r; wf_word n w; a ∈ Σ n⟧ ⟹
lang n (lderiv a (rderivs w r)) = lang n (rderivs w (lderiv a r))"
by (induct w arbitrary: n r)
(auto, auto simp: lang_rderivs lang_lderiv lang_rderiv lQuot_rQuot)
(*
primrec bideriv :: "'a ⇒ 'a ⇒ 'a rexp ⇒ 'a rexp" where
"bideriv _ _ Zero = Zero"
| "bideriv _ _ One = Zero"
| "bideriv a b (Atom c) = Zero"
| "bideriv a b (Plus r s) = Plus (bideriv a b r) (bideriv a b s)"
| "bideriv a b (Times r s) =
(let rs' = Times (lderiv a r) (rderiv b s)
in if final r ∧ final s then Plus (Plus rs' (bideriv a b r)) (bideriv a b s)
else if final r then Plus rs' (bideriv a b s)
else if final s then Plus rs' (bideriv a b r)
else rs')"
| "bideriv a b (Star r) = Plus (bideriv a b r) (TIMES [lderiv a r, Star r, rderiv b r])"
| "bideriv a b (Not r) = Not (bideriv a b r)"
| "bideriv a b (Inter r s) = Inter (bideriv a b r) (bideriv a b s)"
| "bideriv a b (Pr r) = Pr (PLUS (map (λb. PLUS (map (λa. bideriv a b r) (embed a))) (embed b)))"

lemma wf_bideriv[simp]: "wf n r ⟹ wf n (bideriv a b r)"
by (induct r arbitrary: n a b) (auto simp: maps_def Let_def)

lemma ACI_norm_bideriv_rderiv_lderiv: "«bideriv a b r» = «rderiv b (lderiv a r)»"
by (induct r arbitrary: a b)
(auto simp: Let_def maps_def o_def list_all2_map1 list_all2_map2 intro!: ACI_PLUS list_all2_refl)

lemma bideriv_rderiv_lderiv:
"lang n (bideriv a b r) = lang n (rderiv b (lderiv a r))"
by (induct r arbitrary: n a b) (auto simp: Let_def)

lemma lang_bideriv:
"⟦wf n r; a ∈ Σ n; b ∈ Σ n⟧ ⟹ lang n (bideriv a b r) = biQuot a b (lang n r)"
by (auto simp: bideriv_rderiv_lderiv lang_lderiv lang_rderiv biQuot_rQuot_lQuot)

lemma ACI_norm_bideriv: "«bideriv a b «r»» = «bideriv a b r»"
unfolding ACI_norm_bideriv_rderiv_lderiv by (metis ACI_norm_lderiv ACI_norm_rderiv)

fun biderivs where
"biderivs [] [] r = r"
| "biderivs as [] r = lderivs as r"
| "biderivs [] bs r = rderivs bs r"
| "biderivs (a#as) (b#bs) r = biderivs as bs (bideriv a b r)"

lemma biderivs_rderivs_lderivs: "⟦wf n r; wf_word n w1; wf_word n w2⟧ ⟹
lang n (biderivs w1 w2 r) = lang n (rderivs w2 (lderivs w1 r))"
by (induct arbitrary: r rule: biderivs.induct)
(auto simp: lang_rderivs lang_lderivs bideriv_rderiv_lderiv)

lemma lang_biderivs:
"⟦wf n r; wf_word n w1; wf_word n w2⟧ ⟹ lang n (biderivs w1 w2 r) = biQuots w1 w2 (lang n r)"
by (auto simp: biderivs_rderivs_lderivs lang_lderivs lang_rderivs biQuots_rQuots_lQuots)

lemma wf_biderivs[simp]: "wf n r ⟹ wf n (biderivs w1 w2 r)"
by (induct arbitrary: r rule: biderivs.induct) auto
*)
definition "biderivs w1 w2 = rderivs w2 o lderivs w1"

lemma lang_biderivs: "⟦wf n r; wf_word n w1; wf_word n w2⟧ ⟹
lang n (biderivs w1 w2 r) = biQuots w1 w2 (lang n r)"
unfolding biderivs_def by (auto simp: lang_rderivs lang_lderivs in_lists_conv_set)

lemma wf_biderivs[simp]: "wf n r ⟹ wf n (biderivs w1 w2 r)"
unfolding biderivs_def by simp

corollary biderivs_final:
assumes "wf n r" "wf_word n w1" "wf_word n w2"
shows "final (biderivs w1 w2 r) ⟷ w1 @ rev w2 ∈ lang n r"
using lang_biderivs[OF assms] lang_final[of "biderivs w1 w2 r" n] by auto

lemma ACI_norm_biderivs: "«biderivs w1 w2 «r»» = «biderivs w1 w2 r»"
unfolding biderivs_def by (metis ACI_norm_lderivs ACI_norm_rderivs o_apply)

lemma "finite {«biderivs w1 w2 r» | w1 w2 . True}"
proof -
have "{«biderivs w1 w2 r» | w1 w2 . True} =
(⋃s ∈ {«lderivs as r» | as . True}. {«rderivs bs s» | bs . True})"
unfolding biderivs_def by (fastforce simp: ACI_norm_rderivs)
also have "finite …" by (rule iffD2[OF finite_UN[OF finite_lderivs] ballI[OF finite_rderivs]])
finally show ?thesis .
qed

end

subsection ‹Quotioning by the same letter›

definition "fin_cut_same x xs = take (LEAST n. drop n xs = replicate (length xs - n) x) xs"

lemma fin_cut_same_Nil[simp]: "fin_cut_same x [] = []"
unfolding fin_cut_same_def by simp

lemma Least_fin_cut_same: "(LEAST n. drop n xs = replicate (length xs - n) y) =
length xs - length (takeWhile (λx. x = y) (rev xs))"
(is "Least ?P = ?min")
proof (rule Least_equality)
show "?P ?min" by (induct xs rule: rev_induct) (auto simp:  Suc_diff_le replicate_append_same)
next
fix m assume "?P m"
have "length xs - m ≤ length (takeWhile (λx. x = y) (rev xs))"
proof (intro length_takeWhile_less_P_nth)
fix i assume "i < length xs - m"
hence "rev xs ! i ∈ set (drop m xs)"
by (induct xs arbitrary: i rule: rev_induct) (auto simp: nth_Cons')
with ‹?P m› show "rev xs ! i = y" by simp
qed simp
thus "?min ≤ m" by linarith
qed

lemma takeWhile_takes_all: "length xs = m ⟹ m ≤ length (takeWhile P xs) ⟷ Ball (set xs) P"
by hypsubst_thin (induct xs, auto)

lemma fin_cut_same_Cons[simp]: "fin_cut_same x (y # xs) =
(if fin_cut_same x xs = [] then if x = y then [] else [y] else y # fin_cut_same x xs)"
unfolding fin_cut_same_def Least_fin_cut_same
apply auto
apply auto
apply (metis (full_types) Suc_diff_le length_rev length_takeWhile_le take_Suc_Cons)
apply (subst takeWhile_append2)
apply auto
apply auto
apply (metis (full_types) Suc_diff_le length_rev length_takeWhile_le take_Suc_Cons)
done

lemma fin_cut_same_singleton[simp]: "fin_cut_same x (xs @ [x]) = fin_cut_same x xs"
by (induct xs) auto

lemma fin_cut_same_replicate[simp]: "fin_cut_same x (xs @ replicate n x) = fin_cut_same x xs"
by (induct n arbitrary: xs)
(auto simp: replicate_append_same[symmetric] append_assoc[symmetric] simp del: append_assoc)

lemma fin_cut_sameE: "fin_cut_same x xs = ys ⟹ ∃m. xs = ys @ replicate m x"
apply (induct xs arbitrary: ys)
apply auto
apply (metis replicate_Suc)
apply metis
apply metis
done

definition "SAMEQUOT a A = {fin_cut_same a x @ replicate m a| x m. x ∈ A}"

lemma SAMEQUOT_mono: "A ⊆ B ⟹ SAMEQUOT a A ⊆ SAMEQUOT a B"
unfolding SAMEQUOT_def by auto

locale embed2 = embed Σ wf_atom project lookup embed
for Σ :: "nat ⇒ 'a set"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool"
and embed :: "'a ⇒ 'a list" +
fixes singleton :: "'a ⇒ 'b"
assumes wf_singleton[simp]: "a ∈ Σ n ⟹ wf_atom n (singleton a)"
assumes lookup_singleton[simp]: "lookup (singleton a) a' = (a = a')"
begin

lemma finite_rderivs_same: "finite {«rderivs (replicate m a) r» | m . True}"
by (auto intro: finite_subset[OF _ finite_rderivs])

lemma wf_word_replicate[simp]: "a ∈ Σ n ⟹ wf_word n (replicate m a)"
by (induct m) auto

lemma star_singleton[simp]: "star {[x]} = {replicate m x | m . True}"
proof (intro equalityI subsetI)
fix xs assume "xs ∈ star {[x]}"
thus "xs ∈ {replicate m x | m . True}" by (induct xs) (auto, metis replicate_Suc)
qed (auto intro: Ball_starI)

definition "samequot a r = Times (flatten PLUS {«rderivs (replicate m a) r» | m . True}) (Star (Atom (singleton a)))"

lemma wf_samequot: "⟦wf n r; a ∈ Σ n⟧ ⟹ wf n (samequot a r)"
unfolding samequot_def wf.simps wf_flatten_PLUS[OF finite_rderivs_same] by auto

lemma lang_samequot: "⟦wf n r; a ∈ Σ n⟧ ⟹
lang n (samequot a r) = SAMEQUOT a (lang n r)"
unfolding SAMEQUOT_def samequot_def lang.simps lang_flatten_PLUS[OF finite_rderivs_same]
apply (rule sym)
apply (auto simp: lang_rderivs)
apply (intro concI)
apply auto
apply (insert fin_cut_sameE[OF refl, of _ a])
apply (drule meta_spec)
apply (erule exE)
apply (intro exI conjI)
apply (rule refl)
apply (auto simp: lang_rderivs)
apply (erule subst)
apply assumption
apply (erule concE)
apply (auto simp: lang_rderivs)
apply (drule meta_spec)
apply (erule exE)
apply (intro exI conjI)
defer
apply assumption
unfolding fin_cut_same_replicate
apply (erule trans)
unfolding fin_cut_same_replicate
apply (rule refl)
done

"rderiv_and_add as (_ :: bool, rs) =
(let
r = «rderiv as (hd rs)»
in if r ∈ set rs then (False, rs) else (True, r # rs))"

definition "invar_rderiv_and_add as r brs ≡
(if fst brs then True else «rderiv as (hd (snd brs))» ∈ set (snd brs)) ∧
snd brs ≠ [] ∧ distinct (snd brs) ∧
(∀i < length (snd brs). snd brs ! i = «rderivs (replicate (length (snd brs) - 1 - i) as) r»)"

unfolding invar_rderiv_and_add_def by (cases brs) (auto simp:
Let_def nth_Cons' ACI_norm_rderiv rderivs_snoc[symmetric] neq_Nil_conv replicate_append_same)

lemma rderivs_replicate_mult: "⟦«rderivs (replicate i as) r» = «r»; i > 0⟧ ⟹
«rderivs (replicate (m * i) as) r» = «r»"
proof (induct m arbitrary: r)
case (Suc m)
hence "«rderivs (replicate (m * i) as) «rderivs (replicate i as) r»» = «r»"
by (auto simp: ACI_norm_rderivs)
thus ?case by (auto simp: ACI_norm_rderivs replicate_add rderivs_append)
qed simp

lemma rderivs_replicate_mult_rest:
assumes "«rderivs (replicate i as) r» = «r»" "k < i"
shows "«rderivs (replicate (m * i + k) as) r» = «rderivs (replicate k as) r»" (is "?L = ?R")
proof -
have "?L = «rderivs (replicate k as) «rderivs (replicate (m * i) as) r»»"
also have "«rderivs (replicate (m * i) as) r» = «r»" using assms
finally show ?thesis by (simp add: ACI_norm_rderivs)
qed

lemma rderivs_replicate_mod:
assumes "«rderivs (replicate i as) r» = «r»" "i > 0"
shows "«rderivs (replicate m as) r» = «rderivs (replicate (m mod i) as) r»" (is "?L = ?R")
by (subst div_mult_mod_eq[symmetric, of m i])
(intro rderivs_replicate_mult_rest[OF assms(1)] mod_less_divisor[OF assms(2)])

lemma rderivs_replicate_diff: "⟦«rderivs (replicate i as) r» = «rderivs (replicate j as) r»; i > j⟧ ⟹
«rderivs (replicate (i - j) as) (rderivs (replicate j as) r)» = «rderivs (replicate j as) r»"

lemma samequot_wf:
assumes "wf n r" "while_option fst (rderiv_and_add as) (True, [«r»]) = Some (b, rs)"
shows "wf n (PLUS rs)"
proof -
have "¬ b" using while_option_stop[OF assms(2)] by simp
have *: "invar_rderiv_and_add as r (b, rs)" by simp
thus "wf n (PLUS rs)" unfolding invar_rderiv_and_add_def wf_PLUS
by (auto simp: in_set_conv_nth wf_rderivs[OF assms(1)])
qed

lemma samequot_soundness:
assumes "while_option fst (rderiv_and_add as) (True, [«r»]) = Some (b, rs)"
shows "lang n (PLUS rs) = ⋃ (lang n  {«rderivs (replicate m as) r» | m. True})"
proof -
have "¬ b" using while_option_stop[OF assms] by simp
moreover
have *: "invar_rderiv_and_add as r (b, rs)" by simp
ultimately obtain i where i: "i < length rs" and "«rderivs (replicate (length rs - Suc i) as) r» =
«rderivs (replicate (Suc (length rs - Suc 0)) as) r»" (is "«rderivs ?x r» = _")
unfolding invar_rderiv_and_add_def by (auto simp: in_set_conv_nth hd_conv_nth ACI_norm_rderiv
rderivs_snoc[symmetric] replicate_append_same)
with * have "«rderivs ?x r» = «rderivs (replicate (length rs) as) r»"
with i have cyc: "«rderivs (replicate (Suc i) as) (rderivs ?x r)» = «rderivs ?x r»"
by (fastforce dest: rderivs_replicate_diff[OF sym])
{ fix m
have "∃i<length rs. rs ! i = «rderivs (replicate m as) r»"
proof (cases "m > length rs - Suc i")
case True
with i obtain m' where m: "m = m' + length rs - Suc i"
by atomize_elim (auto intro: exI[of _ "m - (length rs - Suc i)"])
with i have "«rderivs (replicate m as) r» = «rderivs (replicate m' as) (rderivs ?x r)»"
also from cyc have "… = «rderivs (replicate (m' mod (Suc i)) as) (rderivs ?x r)»"
by (elim rderivs_replicate_mod) simp
also from i have "… = «rderivs (replicate (m' mod (Suc i) + length rs - Suc i) as) r»"
also from m i have "… = «rderivs (replicate ((m - (length rs - Suc i)) mod (Suc i) + length rs - Suc i) as) r»"
by simp
also have "… = «rderivs (replicate (length rs - Suc (i - (m - (length rs - Suc i)) mod (Suc i))) as) r»"
by (subst Suc_diff_le[symmetric])
finally have "∃j < length rs. «rderivs (replicate m as) r» = «rderivs (replicate (length rs - Suc j) as) r»"
using i by (metis less_imp_diff_less)
with * show ?thesis unfolding invar_rderiv_and_add_def by auto
next
case False
with i have "∃j < length rs. m = length rs - Suc j"
by (induct m)
(metis diff_self_eq_0 gr_implies_not0 lessI nat.exhaust,
metis (no_types) One_nat_def Suc_diff_Suc diff_Suc_1 gr0_conv_Suc less_imp_diff_less
not_less_eq not_less_iff_gr_or_eq)
with * show ?thesis unfolding invar_rderiv_and_add_def by auto
qed
}
hence "⋃ (lang n  {«rderivs (replicate m as) r» |m. True}) ⊆ lang n (PLUS rs)"
by (fastforce simp: in_set_conv_nth intro!: bexI[rotated])
moreover from * have "lang n (PLUS rs) ⊆ ⋃ (lang n  {«rderivs (replicate m as) r» |m. True})"
unfolding invar_rderiv_and_add_def by (fastforce simp: in_set_conv_nth)
ultimately show "lang n (PLUS rs) = ⋃ (lang n  {«rderivs (replicate m as) r» |m. True})" by blast
qed

lemma length_subset_card: "⟦finite X; distinct (x # xs); set (x # xs) ⊆ X⟧ ⟹ length xs < card X"
by (metis card_mono distinct_card impossible_Cons not_le_imp_less order_trans)

lemma samequot_termination:
assumes "while_option fst (rderiv_and_add as) (True, [«r»]) = None" (is "?cl = None")
shows "False"
proof -
let ?D =  "{«rderivs (replicate m as) r» | m . True}"
let ?f = "λ(b, rs). card ?D + 1 - length rs + (if b then 1 else 0)"
have "∃st. ?cl = Some st"
apply (rule measure_while_option_Some[of "invar_rderiv_and_add as r" _ _ ?f])
apply (auto simp: invar_rderiv_and_add_def Let_def neq_Nil_conv in_set_conv_nth
intro!: diff_less_mono2 length_subset_card[OF finite_rderivs_same, simplified])
apply auto []
apply fastforce
apply (metis Suc_less_eq nth_Cons_Suc)
done
with assms show False by auto
qed

definition "samequot_exec a r =
Times (PLUS (snd (the (while_option fst (rderiv_and_add a) (True, [«r»]))))) (Star (Atom (singleton a)))"

lemma wf_samequot_exec: "⟦wf n r; as ∈ Σ n⟧ ⟹ wf n (samequot_exec as r)"
unfolding samequot_exec_def
by (cases "while_option fst (rderiv_and_add as) (True, [«r»])")
(auto dest: samequot_termination samequot_wf)

lemma samequot_exec_samequot: "lang n (samequot_exec as r) = lang n (samequot as r)"
unfolding samequot_exec_def samequot_def lang.simps lang_flatten_PLUS[OF finite_rderivs_same]
by (cases "while_option fst (rderiv_and_add as) (True, [«r»])")
(auto dest: samequot_termination dest!: samequot_soundness[of _ _ _ _ n] simp del: ACI_norm_lang)

lemma lang_samequot_exec:
"⟦wf n r; as ∈ Σ n⟧ ⟹ lang n (samequot_exec as r) = SAMEQUOT as (lang n r)"
unfolding samequot_exec_samequot by (rule lang_samequot)

end

subsection ‹Suffix and Prefix Languages›

definition Suffix :: "'a lang ⇒ 'a lang" where
"Suffix L = {w. ∃u. u @ w ∈ L}"

definition Prefix :: "'a lang ⇒ 'a lang" where
"Prefix L = {w. ∃u. w @ u ∈ L}"

lemma Prefix_Suffix: "Prefix L = rev  Suffix (rev  L)"
unfolding Prefix_def Suffix_def
by (auto simp: rev_append_invert
intro: image_eqI[of _ rev, OF rev_rev_ident[symmetric]]
image_eqI[of _ rev, OF rev_append[symmetric]])

definition Root :: "'a lang ⇒ 'a lang" where
"Root L = {x . ∃n > 0. x ^^ n ∈ L}"

definition Cycle :: "'a lang ⇒ 'a lang" where
"Cycle L = {u @ w | u w. w @ u ∈ L}"

context embed
begin

context
fixes n :: nat
begin

definition SUFFIX :: "'b rexp ⇒ 'b rexp" where
"SUFFIX r = flatten PLUS {«lderivs w r»| w. wf_word n w}"

lemma finite_lderivs_wf: "finite {«lderivs w r»| w. wf_word n w}"
by (auto intro: finite_subset[OF _ finite_lderivs])

definition PREFIX :: "'b rexp ⇒ 'b rexp" where
"PREFIX r = REV (SUFFIX (REV r))"

lemma wf_SUFFIX[simp]: "wf n r ⟹ wf n (SUFFIX r)"
unfolding SUFFIX_def by (intro iffD2[OF wf_flatten_PLUS[OF finite_lderivs_wf]]) auto

lemma lang_SUFFIX[simp]: "wf n r ⟹ lang n (SUFFIX r) = Suffix (lang n r)"
unfolding SUFFIX_def Suffix_def
using lang_flatten_PLUS[OF finite_lderivs_wf] lang_lderivs wf_lang_wf_word
by fastforce

lemma wf_PREFIX[simp]: "wf n r ⟹ wf n (PREFIX r)"
unfolding PREFIX_def by auto

lemma lang_PREFIX[simp]: "wf n r ⟹ lang n (PREFIX r) = Prefix (lang n r)"
unfolding PREFIX_def by (auto simp: Prefix_Suffix)

end

lemma take_drop_CycleI[intro!]: "x ∈ L ⟹ drop i x @ take i x ∈ Cycle L"
unfolding Cycle_def by fastforce

lemma take_drop_CycleI'[intro!]: "drop i x @ take i x ∈ L ⟹ x ∈ Cycle L"
by (drule take_drop_CycleI[of _ _ "length x - i"]) auto

end

(*<*)
end
(*>*)


# Theory Pi_Regular_Exp_Dual

(* Author: Dmitriy Traytel *)

section ‹$\Pi$-Extended Dual Regular Expressions›

(*<*)
theory Pi_Regular_Exp_Dual
imports Pi_Derivatives "HOL-Library.List_Lexorder" "HOL-Library.Code_Target_Nat"
begin
(*>*)
subsection ‹Syntax of regular expressions›

datatype 'a rexp_dual =
CoZero (co: bool) |
CoOne (co: bool) |
CoAtom (co: bool) 'a |
CoPlus (co: bool) "'a rexp_dual" "'a rexp_dual" |
CoTimes (co: bool) "'a rexp_dual" "'a rexp_dual" |
CoStar (co: bool) "'a rexp_dual" |
CoPr (co: bool) "'a rexp_dual"
derive linorder rexp_dual

abbreviation "CoPLUS_dual b ≡ rexp_of_list (CoPlus b) (CoZero b)"
abbreviation "bool_unop_dual b ≡ (if b then id else HOL.Not)"
abbreviation "bool_binop_dual b ≡ (if b then (∨) else (∧))"
abbreviation "set_binop_dual b ≡ (if b then (∪) else (∩))"

primrec final_dual :: "'a rexp_dual ⇒ bool"
where
"final_dual (CoZero b) = (¬ b)"
| "final_dual (CoOne b) = b"
| "final_dual (CoAtom b _) = (¬ b)"
| "final_dual (CoPlus b r s) = bool_binop_dual b (final_dual r) (final_dual s)"
| "final_dual (CoTimes b r s) = bool_binop_dual (¬ b) (final_dual r) (final_dual s)"
| "final_dual (CoStar b _) = b"
| "final_dual (CoPr _ r) = final_dual r"

context alphabet
begin

primrec wf_dual :: "nat ⇒ 'b rexp_dual ⇒ bool"
where
"wf_dual n (CoZero _) = True" |
"wf_dual n (CoOne _) = True" |
"wf_dual n (CoAtom _ a) = (wf_atom n a)" |
"wf_dual n (CoPlus _ r s) = (wf_dual n r ∧ wf_dual n s)" |
"wf_dual n (CoTimes _ r s) = (wf_dual n r ∧ wf_dual n s)" |
"wf_dual n (CoStar _ r) = wf_dual n r" |
"wf_dual n (CoPr _ r) = wf_dual (n + 1) r"

lemma wf_dual_PLUS_dual[simp]:
"wf_dual n (CoPLUS_dual b xs) = (∀r ∈ set xs. wf_dual n r)"
by (induct xs rule: list_singleton_induct) auto

abbreviation "set_unop_dual n b A ≡ if b then A else lists (Σ n) - A"

end

context project
begin

primrec lang_dual :: "nat ⇒ 'b rexp_dual => 'a lang" where
"lang_dual n (CoZero b) = set_unop_dual n b {}" |
"lang_dual n (CoOne b) = set_unop_dual n b {[]}" |
"lang_dual n (CoAtom b a) = set_unop_dual n b {[x] | x. lookup a x ∧ x ∈ Σ n}" |
"lang_dual n (CoPlus b r s) = set_binop_dual b (lang_dual n r) (lang_dual n s)" |
"lang_dual n (CoTimes b r s) = set_unop_dual n b
(set_unop_dual n b (lang_dual n r) @@ set_unop_dual n b (lang_dual n s))" |
"lang_dual n (CoStar b r) = set_unop_dual n b (star (set_unop_dual n b (lang_dual n r)))" |
"lang_dual n (CoPr b r) = set_unop_dual n b (map project  (set_unop_dual (n + 1) b (lang_dual (n + 1) r)))"

lemma wf_dual_lang_dual_wf_word: "wf_dual n r ⟹ ∀w ∈ lang_dual n r. wf_word n w"
by (induct r arbitrary: n) (auto elim: rev_subsetD[OF _ conc_mono] star_induct
intro: iffD2[OF wf_word] wf_word_map_project)

lemma lang_dual_subset_lists: "wf_dual n r ⟹ lang_dual n r ⊆ lists (Σ n)"
proof (induct r arbitrary: n)
case (CoPr b r) thus ?case by (cases b) (fastforce intro!: project)+
qed (auto simp: conc_subset_lists star_subset_lists)

lemma lang_dual_final_dual: "final_dual r = ([] ∈ lang_dual n r)"
by (induct r arbitrary: n) (auto intro: concI[of "[]" _ "[]", simplified])

lemma lang_dual_PLUS_dual[simp]:
"lang_dual n (CoPLUS_dual True xs) = (⋃r ∈ set xs. lang_dual n r)"
by (induct xs rule: list_singleton_induct) auto

lemma lang_dual_CoPLUS_dual[simp]:
"lang_dual n (CoPLUS_dual False xs) = (if xs = [] then lists (Σ n) else ⋂r ∈ set xs. lang_dual n r)"
by (induct xs rule: list_singleton_induct) auto

end

context embed
begin

primrec lderiv_dual :: "'a ⇒ 'b rexp_dual ⇒ 'b rexp_dual" where
"lderiv_dual _ (CoZero b) = (CoZero b)"
| "lderiv_dual _ (CoOne b) = (CoZero b)"
| "lderiv_dual a (CoAtom b c) = (if lookup c a then CoOne b else CoZero b)"
| "lderiv_dual a (CoPlus b r s) = CoPlus b (lderiv_dual a r) (lderiv_dual a s)"
| "lderiv_dual a (CoTimes b r s) =
(let r's = CoTimes b (lderiv_dual a r) s
in if bool_unop_dual b (final_dual r) then CoPlus b r's (lderiv_dual a s) else r's)"
| "lderiv_dual a (CoStar b r) = CoTimes b (lderiv_dual a r) (CoStar b r)"
| "lderiv_dual a (CoPr b r) = CoPr b (CoPLUS_dual b (map (λa'. lderiv_dual a' r) (embed a)))"

primrec lderivs_dual where
"lderivs_dual [] r = r"
| "lderivs_dual (w#ws) r = lderivs_dual ws (lderiv_dual w r)"

lemma wf_dual_lderiv_dual[simp]: "wf_dual n r ⟹ wf_dual n (lderiv_dual w r)"
by (induct r arbitrary: n w) (auto simp add: Let_def)

lemma wf_dual_lderivs_dual[simp]: "wf_dual n r ⟹ wf_dual n (lderivs_dual ws r)"
by (induct ws arbitrary: r) (auto intro: wf_dual_lderiv_dual)

lemma lang_dual_lderiv_dual: "⟦wf_dual n r; w ∈ Σ n⟧ ⟹
lang_dual n (lderiv_dual w r) = lQuot w (lang_dual n r)"
proof (induct r arbitrary: n w)
case (CoPr b r)
hence *: "wf_dual (Suc n) r" "⋀w'. w' ∈ set (embed w) ⟹  w' ∈ Σ (Suc n)" by (auto simp: embed)
then show ?case using lQuot_map_project[OF CoPr(3) lang_dual_subset_lists[OF *(1)]]
lQuot_map_project[OF CoPr(3) Diff_subset, of "lang_dual (n + 1) r"]
qed (auto 0 3 simp: Let_def lang_dual_final_dual[symmetric])

lemma lang_dual_lderivs_dual: "⟦wf_dual n r; wf_word n ws⟧ ⟹
lang_dual n (lderivs_dual ws r) = lQuots ws (lang_dual n r)"
by (induct ws arbitrary: r) (auto simp: lang_dual_lderiv_dual)

corollary lderivs_dual_final_dual:
assumes "wf_dual n r" "wf_word n ws"
shows "final_dual (lderivs_dual ws r) ⟷ ws ∈ lang_dual n r"
using lang_dual_lderivs_dual[OF assms] lang_dual_final_dual[of "lderivs_dual ws r" n] by auto

end

fun pnCoPlus :: "bool ⇒ 'a::linorder rexp_dual ⇒ 'a rexp_dual ⇒ 'a rexp_dual" where
"pnCoPlus b1 (CoZero b2) r = (if b1 = b2 then r else CoZero b2)"
| "pnCoPlus b1 r (CoZero b2) = (if b1 = b2 then r else CoZero b2)"
| "pnCoPlus b1 (CoPlus b2 r s) t =
(if b1 = b2 then pnCoPlus b2 r (pnCoPlus b2 s t) else CoPlus b1 (CoPlus b2 r s) t)"
| "pnCoPlus b1 r (CoPlus b2 s t) =
(if b1 = b2 then
(if r = s then (CoPlus b2 s t)
else if r ≤ s then CoPlus b2 r (CoPlus b2 s t)
else CoPlus b2 s (pnCoPlus b2 r t))
else CoPlus b1 r (CoPlus b2 s t))"
| "pnCoPlus b r s =
(if r = s then r
else if r ≤ s then CoPlus b r s
else CoPlus b s r)"

lemma (in alphabet) wf_dual_pnCoPlus[simp]: "⟦wf_dual n r; wf_dual n s⟧ ⟹ wf_dual n (pnCoPlus b r s)"
by (induct b r s rule: pnCoPlus.induct) auto

lemma (in project) lang_dual_pnCoPlus[simp]: "⟦wf_dual n r; wf_dual n s⟧ ⟹
lang_dual n (pnCoPlus b r s) = lang_dual n (CoPlus b r s)"
proof (induct b r s rule: pnCoPlus.induct)
case 1 thus ?case by (auto dest: lang_dual_subset_lists)
next
case "2_1" thus ?case by auto
next
case "2_2" thus ?case by auto
next
case "2_3" thus ?case by (auto dest: lang_dual_subset_lists)
next
case "2_4" thus ?case by (auto dest!: lang_dual_subset_lists dest:
subsetD[OF conc_subset_lists, unfolded in_lists_conv_set, rotated -1])
next
case "2_5" thus ?case by (auto dest!: lang_dual_subset_lists dest:
subsetD[OF star_subset_lists, unfolded in_lists_conv_set, rotated -1])
next
case "2_6" thus ?case by (auto 4 4 dest!: lang_dual_subset_lists intro: project)
next
case "3_1" thus ?case by auto
next
case "3_2" thus ?case by auto
next
case "3_3" thus ?case by auto
next
case "3_4" thus ?case by auto
next
case "3_5" thus ?case by auto
next
case "3_6" thus ?case by auto
next
case "4_1" thus ?case by auto
next
case "4_2" thus ?case by auto
next
case "4_3" thus ?case by auto
next
case "4_4" thus ?case by auto
next
case "4_5" thus ?case by auto
next
case "5_1" thus ?case by auto
next
case "5_2" thus ?case by auto
next
case "5_3" thus ?case by auto
next
case "5_4" thus ?case by auto
next
case "5_5" thus ?case by auto
next
case "5_6" thus ?case by auto
next
case "5_7" thus ?case by auto
next
case "5_8" thus ?case by auto
next
case "5_9" thus ?case by auto
next
case "5_10" thus ?case
by auto (metis (no_types, hide_lams) Cons_in_lists_iff Diff_iff imageI list.simps(8) list.simps(9) lists.Nil)+
next
case "5_11" thus ?case by auto
next
case "5_12" thus ?case by auto
next
case "5_13" thus ?case by auto
next
case "5_14" thus ?case by auto
next
case "5_15" thus ?case by auto
next
case "5_16" thus ?case by auto
next
case "5_17" thus ?case by auto
next
case "5_18" thus ?case by auto
next
case "5_19" thus ?case by (auto dest!: lang_dual_subset_lists dest:
subsetD[OF star_subset_lists, unfolded in_lists_conv_set, rotated -1])
next
case "5_20" thus ?case by auto
next
case "5_21" thus ?case by auto
next
case "5_22" thus ?case
by auto (metis (no_types, hide_lams) Cons_in_lists_iff Diff_iff imageI list.simps(8) list.simps(9) lists.Nil)+
next
case "5_23" thus ?case by auto
next
case "5_24" thus ?case by auto
next
case "5_25" thus ?case by auto
qed

fun pnCoTimes :: "bool ⇒ 'a::linorder rexp_dual ⇒ 'a rexp_dual ⇒ 'a rexp_dual" where
"pnCoTimes b1 (CoZero b2) r = (if b1 = b2 then CoZero b1 else CoTimes b1 (CoZero b2) r)"
| "pnCoTimes b1 (CoOne b2) r = (if b1 = b2 then r else CoTimes b1 (CoOne b2) r)"
| "pnCoTimes b1 (CoPlus b2 r s) t = (if b1 = b2 then pnCoPlus b2 (pnCoTimes b2 r t) (pnCoTimes b2 s t)
else CoTimes b1 (CoPlus b2 r s) t)"
| "pnCoTimes b r s = CoTimes b r s"

lemma (in alphabet) wf_dual_pnCoTimes[simp]: "⟦wf_dual n r; wf_dual n s⟧ ⟹ wf_dual n (pnCoTimes b r s)"
by (induct b r s rule: pnCoTimes.induct) auto

lemma (in project) lang_dual_pnCoTimes[simp]: "⟦wf_dual n r; wf_dual n s⟧ ⟹ lang_dual n (pnCoTimes b r s) = lang_dual n (CoTimes b r s)"
apply (induct b r s rule: pnCoTimes.induct)
apply (auto, auto dest!: lang_dual_subset_lists dest: project
subsetD[OF star_subset_lists, unfolded in_lists_conv_set, rotated -1]
subsetD[OF conc_subset_lists, unfolded in_lists_conv_set, rotated -1])
by (metis (full_types) Diff_iff conc_epsilon(1) double_diff empty_subsetI in_listsI insert_subset lists.Nil subset_refl)

fun pnCoPr :: "bool ⇒ 'a::linorder rexp_dual ⇒ 'a rexp_dual" where
"pnCoPr b1 (CoZero b2) = (if b1 = b2 then CoZero b2 else CoPr b1 (CoZero b2))"
| "pnCoPr b1 (CoOne b2) = (if b1 = b2 then CoOne b2 else CoPr b1 (CoOne b2))"
| "pnCoPr b1 (CoPlus b2 r s) = (if b1 = b2 then pnCoPlus b2 (pnCoPr b2 r) (pnCoPr b2 s)
else CoPr b1 (CoPlus b2 r s))"
| "pnCoPr b r = CoPr b r"

lemma (in alphabet) wf_dual_pnCoPr[simp]: "wf_dual (Suc n) r ⟹ wf_dual n (pnCoPr b r)"
by (induct b r rule: pnCoPr.induct) auto

lemma (in project) lang_dual_pnCoPr[simp]: "wf_dual (Suc n) r ⟹ lang_dual n (pnCoPr b r) = lang_dual n (CoPr b r)"
by (induct b r rule: pnCoPr.induct) auto

primrec pnorm_dual :: "'a::linorder rexp_dual ⇒ 'a rexp_dual" where
"pnorm_dual (CoZero b) = (CoZero b)"
| "pnorm_dual (CoOne b) = (CoOne b)"
| "pnorm_dual (CoAtom b a) = (CoAtom b a)"
| "pnorm_dual (CoPlus b r s) = pnCoPlus b (pnorm_dual r) (pnorm_dual s)"
| "pnorm_dual (CoTimes b r s) = pnCoTimes b (pnorm_dual r) s"
| "pnorm_dual (CoStar b r) = CoStar b r"
| "pnorm_dual (CoPr b r) = pnCoPr b (pnorm_dual r)"

lemma (in alphabet) wf_dual_pnorm_dual[simp]: "wf_dual n r ⟹ wf_dual n (pnorm_dual r)"
by (induct r arbitrary: n) auto

lemma (in project) lang_dual_pnorm_dual[simp]: "wf_dual n r ⟹ lang_dual n (pnorm_dual r) = lang_dual n r"
by (induct r arbitrary: n) auto

primrec CoNot where
"CoNot (CoZero b) = CoZero (¬ b)"
| "CoNot (CoOne b) = CoOne (¬ b)"
| "CoNot (CoAtom b a) = CoAtom (¬ b) a"
| "CoNot (CoPlus b r s) = CoPlus (¬ b) (CoNot r) (CoNot s)"
| "CoNot (CoTimes b r s) = CoTimes (¬ b) (CoNot r) (CoNot s)"
| "CoNot (CoStar b r) = CoStar (¬ b) (CoNot r)"
| "CoNot (CoPr b r) = CoPr (¬ b) (CoNot r)"

primrec rexp_dual_of where
"rexp_dual_of Zero = CoZero True"
| "rexp_dual_of Full = CoZero False"
| "rexp_dual_of One = CoOne True"
| "rexp_dual_of (Atom a) = CoAtom True a"
| "rexp_dual_of (Plus r s) = CoPlus True (rexp_dual_of r) (rexp_dual_of s)"
| "rexp_dual_of (Times r s) = CoTimes True (rexp_dual_of r) (rexp_dual_of s)"
| "rexp_dual_of (Star r) = CoStar True (rexp_dual_of r)"
| "rexp_dual_of (Not r) = CoNot (rexp_dual_of r)"
| "rexp_dual_of (Inter r s) = CoPlus False (rexp_dual_of r) (rexp_dual_of s)"
| "rexp_dual_of (Pr r) = CoPr True (rexp_dual_of r)"

lemma (in alphabet) wf_dual_CoNot[simp]: "wf_dual n r ⟹ wf_dual n (CoNot r)"
by (induct r arbitrary: n) auto

lemma (in project) lang_dual_CoNot[simp]: "wf_dual n r ⟹ lang_dual n (CoNot r) = lists (Σ n) - lang_dual n r"
apply (induct r arbitrary: n)
apply (auto dest!: lang_dual_subset_lists simp: double_diff intro!: project)
apply force
apply (metis (full_types) Diff_subset contra_subsetD in_listsD star_subset_lists)
done

lemma (in alphabet) wf_dual_rexp_dual_of[simp]: "wf n r ⟹ wf_dual n (rexp_dual_of r)"
by (induct r arbitrary: n) auto

lemma (in project) lang_dual_rexp_dual_of[simp]: "wf n r ⟹ lang_dual n (rexp_dual_of r) = lang n r"
by (induct r arbitrary: n) auto

end


# Theory Pi_Equivalence_Checking

(* Author: Dmitriy Traytel *)

section ‹Deciding Equivalence of $\Pi$-Extended Regular Expressions›

(*<*)
theory Pi_Equivalence_Checking
imports Pi_Regular_Exp "HOL-Library.While_Combinator" List_More
begin
(*>*)

lemma image2p_in_rel: "BNF_Greatest_Fixpoint.image2p f g (in_rel R) =  in_rel (map_prod f g  R)"
unfolding image2p_def fun_eq_iff by auto

lemma image2p_apply: "BNF_Greatest_Fixpoint.image2p f g R x y = (∃x' y'. R x' y' ∧ f x' = x ∧ g y' = y)"
unfolding image2p_def fun_eq_iff by auto

lemma rtrancl_fold_product:
shows "{((r, s), (f a r, f a s))| r s a. a ∈ A}^* =
{((r, s), (fold f w r, fold f w s))| r s w. w ∈ lists A}" (is "?L = ?R")
proof-
{ fix x :: "('a × 'a) × 'a × 'a"
obtain r s r' s' where x: "x = ((r, s), (r', s'))" by (cases x) auto
have "((r, s), (r', s')) ∈ ?L ⟹ ((r, s), (r', s')) ∈ ?R"
proof(induction rule: converse_rtrancl_induct2)
case refl show ?case by(force intro!: fold_simps(1)[symmetric])
next
case step thus ?case by(force intro!: fold_simps(2)[symmetric])
qed
with x have "x ∈ ?L ⟹ x ∈ ?R" by simp
} moreover
{ fix x :: "('a × 'a) × 'a × 'a"
obtain r s r' s' where x: "x = ((r, s), (r', s'))" by (cases x) auto
{ fix w have "∀x∈set w. x ∈ A ⟹ ((r, s), fold f w r, fold f w s) ∈ ?L"
proof(induction w rule: rev_induct)
case Nil show ?case by simp
next
case snoc thus ?case by (auto elim!: rtrancl_into_rtrancl)
qed
}
hence "((r, s), (r', s')) ∈ ?R ⟹ ((r, s), (r', s')) ∈ ?L" by auto
with x have "x ∈ ?R ⟹ x ∈ ?L" by simp
} ultimately show ?thesis by blast
qed

lemma in_fold_lQuot: "v ∈ fold lQuot w L ⟷ w @ v ∈ L"
by (induct w arbitrary: L) (simp_all add: lQuot_def)

lemma (in project) lang_eq_ext: "⟦wf n r; wf n s⟧ ⟹ (lang n r = lang n s) =
(∀w ∈ lists(Σ n). w ∈ lang n r ⟷ w ∈ lang n s)"
by (auto dest!: lang_subset_lists)

lemma (in project) lang_eq_ext_Nil_fold_Deriv:
fixes r s n
assumes WF: "wf n r" "wf n s"
defines "𝔅 ≡ {(fold lQuot w (lang n r), fold lQuot w (lang n s))| w. w∈lists (Σ n)}"
shows "lang n r = lang n s ⟷ (∀(K, L) ∈ 𝔅. [] ∈ K ⟷ [] ∈ L)"
unfolding lang_eq_ext[OF WF] 𝔅_def
by (subst (1 2) in_fold_lQuot[of "[]", simplified, symmetric]) auto

locale rexp_DA = project "set o σ" wf_atom project lookup
for σ :: "nat ⇒ 'a list"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool" +
fixes init :: "'b rexp ⇒ 's"
fixes delta :: "'a ⇒ 's ⇒ 's"
fixes final :: "'s ⇒ bool"
fixes wf_state :: "'s ⇒ bool"
fixes post :: "'s ⇒ 's"
fixes L :: "'s ⇒ 'a lang"
fixes n :: "nat"
assumes L_init[simp]: "wf n r ⟹ L (init r) = lang n r"
assumes L_delta[simp]: "⟦a ∈ set (σ n); wf_state s⟧ ⟹ L (delta a s) = lQuot a (L s)"
assumes final_iff_Nil[simp]: "final s ⟷ [] ∈ L s"
assumes L_wf_state[dest]: "wf_state s ⟹ L s ⊆ lists (set (σ n))"
assumes init_wf_state[simp]: "wf n r ⟹ wf_state (init r)"
assumes delta_wf_state[simp]: "⟦a ∈ set (σ n); wf_state s⟧ ⟹ wf_state (delta a s)"
assumes L_post[simp]: "wf_state s ⟹ L (post s) = L s"
assumes wf_state_post[simp]: "wf_state s ⟹ wf_state (post s)"
begin

lemma L_deltas[simp]: "⟦wf_word n w; wf_state s⟧ ⟹ L (fold delta w s) = fold lQuot w (L s)"
by (induction w arbitrary: s) auto

definition progression (infix "→" 60) where
"R → S = (∀s1 s2. R s1 s2 ⟶ wf_state s1 ∧ wf_state s2 ∧ final s1 = final s2 ∧
(∀x ∈ set (σ n). BNF_Greatest_Fixpoint.image2p post post S (post (delta x s1)) (post (delta x s2))))"

lemma SUPR_progression[intro!]: "∀n. ∃m. X n → Y m ⟹ (SUP n. X n) → (SUP n. Y n)"
unfolding progression_def image2p_def by fastforce

definition bisimulation where
"bisimulation R = R → R"

definition bisimulation_upto where
"bisimulation_upto R f = R → f R"

declare image2pI[intro!] image2pE[elim!]
lemmas bisim_def = bisimulation_def progression_def
lemmas bisim_upto_def = bisimulation_upto_def progression_def

definition compatible where
"compatible f = (mono f ∧ (∀R S. R → S ⟶ f R → f S))"

lemmas compat_def = compatible_def progression_def

lemma bisimulation_upto_bisimulation:
assumes "compatible f" "bisimulation_upto R f"
obtains S where "bisimulation S" "R ≤ S"
proof
{ fix n from assms have "(f^^n) R → (f^^Suc n) R"
by (induct n) (auto simp: bisimulation_upto_def compatible_def) }
then show "bisimulation (SUP n. (f^^n) R)"
unfolding bisimulation_def by (auto simp del: funpow.simps)
show "R ≤ (SUP n. (f^^n) R)" by (auto intro!: exI[of _ 0])
qed

lemma bisimulation_eqL: "bisimulation (λs1 s2. wf_state s1 ∧ wf_state s2 ∧ L s1 = L s2)"
unfolding bisim_def by (auto simp: lQuot_def)

lemma coinduction:
assumes bisim[unfolded bisim_def]: "bisimulation R" and
WF: "wf_state s1" "wf_state s2" and R: "R s1 s2"
shows "L s1 = L s2"
proof (rule set_eqI)
fix w
from R WF show "w ∈ L s1 ⟷ w ∈ L s2"
proof (induction w arbitrary: s1 s2)
case Nil then show ?case using bisim by simp
next
case (Cons a w s1 s2)
show ?case
proof cases
assume a: "a ∈ set (σ n)"
with ‹R s1 s2› obtain s1' s2' where "R s1' s2'" "wf_state s1'" "wf_state s2'" and
*[symmetric]: "post s1' = post (delta a s1)"  "post s2' = post (delta a s2)"
using bisim unfolding image2p_apply by blast
then have "w ∈ L (post (delta a s1)) ⟷ w ∈ L (post (delta a s2))"
unfolding * using Cons.IH[of s1' s2'] by simp
with a Cons.prems(2,3) show ?case by (simp add: lQuot_def)
next
assume "a ∉ set (σ n)"
thus ?case using Cons.prems bisim by force
qed
qed
qed

lemma coinduction_upto:
assumes "bisimulation_upto R f" and WF: "wf_state s1" "wf_state s2" and "R s1 s2" "compatible f"
shows "L s1 = L s2"
proof (rule bisimulation_upto_bisimulation[OF assms(5,1)])
fix S assume "R ≤ S"
assume "bisimulation S"
then show "L s1 = L s2"
proof (rule coinduction[OF _ WF])
from ‹R ≤ S› ‹R s1 s2› show "S s1 s2" by blast
qed
qed

fun test_invariant where
"test_invariant (ws, _ :: ('s × 's) list , _ :: 's rel) = (case ws of [] ⇒  False | (w::'a list,p,q)#_ ⇒ final p = final q)"
fun test where "test (ws, _ :: 's rel) = (case ws of [] ⇒  False | (p,q)#_ ⇒ final p = final q)"

fun step_invariant where "step_invariant (ws, ps, N) =
(let
(w, r, s) = hd ws;
ps' = (r, s) # ps;
succs = map (λa.
let r' = delta a r; s' = delta a s
in ((a # w, r', s'), (post r', post s'))) (σ n);
new = remdups' snd (filter (λ(_, rs). rs ∉ N) succs);
ws' = tl ws @ map fst new;
N' = set (map snd new) ∪ N
in (ws', ps', N'))"

fun step where "step (ws, N) =
(let
(r, s) = hd ws;
succs = map (λa.
let r' = delta a r; s' = delta a s
in ((r', s'), (post r', post s'))) (σ n);
new = remdups' snd (filter (λ(_, rs). rs ∉ N) succs)
in (tl ws @ map fst new, set (map snd new) ∪ N))"

definition closure_invariant where "closure_invariant = while_option test_invariant step_invariant"
definition closure where "closure = while_option test step"

definition invariant where
"invariant r s = (λ(ws, ps, N).
(r, s) ∈ snd  set ws ∪ set ps ∧
distinct (map snd ws @ ps) ∧
bij_betw (map_prod post post) (set (map snd ws @ ps)) N ∧
(∀(w, r', s') ∈ set ws. fold delta (rev w) r = r' ∧ fold delta (rev w) s = s' ∧
wf_word n (rev w) ∧ wf_state r' ∧ wf_state s') ∧
(∀(r', s') ∈ set ps. (∃w. fold delta w r = r' ∧ fold delta w s = s') ∧
wf_state r' ∧ wf_state s' ∧ (final r' ⟷ final s') ∧
(∀a∈set (σ n). (post (delta a r'), post (delta a s')) ∈ N)))"

lemma invariant_start:
"⟦wf_state r; wf_state s⟧ ⟹ invariant r s ([([], r, s)], [], {(post r, post s)})"
by (auto simp add: invariant_def bij_betw_def)

lemma step_invariant_mono:
assumes "step_invariant (ws, ps, N) = (ws', ps', N')"
shows "snd  set ws ∪ set ps ⊆ snd  set ws' ∪ set ps'"
using assms proof (intro subsetI, elim UnE)
fix x assume "x ∈ snd set ws"
with assms show "x ∈ snd  set ws' ∪ set ps'"
proof (cases "x = snd (hd ws)")
case False with ‹x ∈ image snd (set ws)› have "x ∈ snd  set (tl ws)" by (cases ws) auto
with assms show ?thesis by (auto split: prod.splits simp: Let_def)
qed (auto split: prod.splits simp: Let_def)
qed (auto split: prod.splits simp: Let_def)

lemma step_invatiant_unfold: "step_invariant (w # ws, ps, N) = (ws', ps', N') ⟹ (∃xs r s.
w = (xs, r, s) ∧ ps' = (r, s) # ps ∧
ws' = ws @ remdups' (map_prod post post o snd) (filter (λ(_, p). map_prod post post p ∉ N)
(map (λa. (a#xs, delta a r, delta a s)) (σ n))) ∧
N' = set (map (λa. (post (delta a r), post (delta a s))) (σ n)) ∪ N)"
by (auto split: prod.splits dest!: mp_remdups'
simp: Let_def filter_map set_n_lists image_Collect image_image comp_def)

lemma invariant: "invariant r s st ⟹ test_invariant st ⟹ invariant r s (step_invariant st)"
proof (unfold invariant_def, (split prod.splits)+, elim case_prodE conjE, clarify, intro allI impI conjI)
fix ws ps N ws' ps' N'
assume test_invariant: "test_invariant (ws, ps, N)"
and step_invariant: "step_invariant (ws, ps, N) = (ws', ps', N')"
and rs: "(r, s) ∈ snd  set ws ∪ set ps"
and distinct: "distinct (map snd ws @ ps)"
and bij: "bij_betw (map_prod post post) (set (map snd ws @ ps)) N"
and ws: "∀(w, r', s') ∈ set ws. fold delta (rev w) r = r' ∧ fold delta (rev w) s = s' ∧
wf_word n (rev w) ∧ wf_state r' ∧ wf_state s'"
(is "∀(w, r', s') ∈ set ws. ?ws w r' s'")
and ps: "∀(r', s') ∈ set ps. (∃w. fold delta w r = r' ∧ fold delta w s = s') ∧
wf_state r' ∧ wf_state s' ∧ (final r' ⟷ final s') ∧
(∀a∈set (σ n). (post (delta a r'), post (delta a s')) ∈ N)"
(is "∀(r, s) ∈ set ps. ?ps r s N")
from test_invariant obtain x xs where ws_Cons: "ws = x # xs" by (cases ws) auto
obtain w r' s' where x: "x = (w, r', s')" and ps': "ps' = (r', s') # ps"
and ws': "ws' = xs @ remdups' (map_prod post post o snd)
(filter (λ(_, p). map_prod post post p ∉ N)
(map (λa. (a # w, delta a r',  delta a s')) (σ n)))"
and N': "N' = (set (map (λa. (post (delta a r'), post (delta a s'))) (σ n)) - N) ∪ N"
using step_invatiant_unfold[OF step_invariant[unfolded ws_Cons]] by blast
hence ws'ps': "set (map snd ws' @ ps') =
set (remdups' (map_prod post post) (filter (λp. map_prod post post p ∉ N)
(map (λa. (delta a r',  delta a s')) (σ n)))) ∪ (set (map snd ws @ ps))"
unfolding ws' ps' ws_Cons x by (auto dest!: mp_remdups' simp: filter_map image_image image_Un o_def)
from rs step_invariant show "(r, s) ∈ snd  set ws' ∪ set ps'" by (blast dest: step_invariant_mono)
(*next*)
from distinct ps' ws' ws_Cons x bij show "distinct (map snd ws' @ ps')"
by (auto simp: bij_betw_def
intro!: imageI[of _ _ "map_prod post post"] distinct_remdups'_strong
map_prod_imageI[of _ _ _ post post]
dest!: mp_remdups'
elim: image_eqI[of _ snd, OF sym[OF snd_conv]])
(*next*)
from ps' ws' N' ws x bij show "bij_betw (map_prod post post) (set (map snd ws' @ ps')) N'"
unfolding ws'ps' N' by (intro bij_betw_combine[OF _ bij]) (auto simp: bij_betw_def map_prod_def)
(*next*)
from ws x ws_Cons have wr's': "?ws w r' s'" by auto
with ws ws_Cons show "∀(w, r', s') ∈ set ws'. ?ws w r' s'" unfolding ws'
by (auto dest!: mp_remdups' elim!: subsetD)
(*next*)
from ps wr's' test_invariant[unfolded ws_Cons x] show "∀(r', s') ∈ set ps'. ?ps r' s' N'" unfolding ps' N'
by (fastforce simp: image_Collect)
qed

lemma step_commute: "ws ≠ [] ⟹
(case step_invariant (ws, ps, N) of (ws', ps', N') ⇒ (map snd ws', N')) = step (map snd ws, N)"
apply (auto split: prod.splits)
apply (auto simp only: step_invariant.simps step.simps Let_def map_apfst_remdups' filter_map list.map_comp apfst_def map_prod_def snd_conv id_def)
apply (auto simp: filter_map comp_def map_tl hd_map)
apply (intro image_eqI, auto)+
done

lemma closure_invariant_closure:
"map_option (λ(ws, ps, N). (map snd ws, N)) (closure_invariant (ws, ps, N)) = closure (map snd ws, N)"
unfolding closure_invariant_def closure_def
by (rule trans[OF while_option_commute[of _ test _ _ "step"]])
(auto split: list.splits simp del: step_invariant.simps step.simps list.map simp: step_commute)

lemma
assumes result: "closure_invariant ([([], init r, init s)], [], {(post (init r), post (init s))}) =
Some(ws, ps, N)" (is "closure_invariant ([([], ?r, ?s)], _) = _")
and WF: "wf n r" "wf n s"
shows closure_invariant_sound: "ws = [] ⟹ lang n r = lang n s" and
counterexample: "ws ≠ [] ⟹ rev (fst (hd ws)) ∈ lang n r ⟷ rev (fst (hd ws)) ∉ lang n s"
proof -
from WF have wf_state: "wf_state ?r" "wf_state ?s" by simp_all
from invariant invariant_start[OF wf_state] have invariant_ps: "invariant ?r ?s (ws, ps, N)"
by (rule while_option_rule[OF _ result[unfolded closure_invariant_def]])
{ assume "ws = []"
with invariant_ps have "bisimulation (in_rel (set ps))" "(?r, ?s) ∈ set ps"
by (auto simp: bij_betw_def invariant_def bisimulation_def progression_def image2p_in_rel)
with wf_state have "L ?r = L ?s" by (auto dest: coinduction)
with WF show "lang n r = lang n s" by simp
}
{ assume "ws ≠ []"
then obtain w r' s' ws' where ws: "ws = (w, r', s') # ws'" by (cases ws) auto
with invariant_ps have "r' = fold delta (rev w) (init r)" "s' = fold delta (rev w) (init s)"
"wf_word n (rev w)" unfolding invariant_def by auto
moreover have "¬ test_invariant ((w, r', s') # ws', ps, N)"
by (rule while_option_stop[OF result[unfolded ws closure_invariant_def]])
ultimately have "rev (fst (hd ws)) ∈ L ?r ⟷ rev (fst (hd ws)) ∉ L ?s"
unfolding ws using wf_state by (simp add: in_fold_lQuot)
with WF show "rev (fst (hd ws)) ∈ lang n r ⟷ rev (fst (hd ws)) ∉ lang n s" by simp
}
qed

lemma closure_sound:
assumes result: "closure ([(init r, init s)], {(post (init r), post (init s))}) = Some ([], N)"
and WF: "wf n r" "wf n s"
shows "lang n r = lang n s"
using trans[OF closure_invariant_closure[of "[([], init r, init s)]", simplified] result]
by (auto dest: closure_invariant_sound[OF _ WF])

definition check_eqv where
"check_eqv r s =
(let r' = init r; s' = init s in (case closure ([(r', s')], {(post r', post s')}) of
Some ([], _) ⇒ True | _ ⇒ False))"

lemma check_eqv_sound:
assumes "check_eqv r s" and WF: "wf n r" "wf n s"
shows "lang n r = lang n s"
using closure_sound assms
by (auto simp: check_eqv_def Let_def split: option.splits list.splits)

definition counterexample where
"counterexample r s =
(let r' = init r; s' = init s in (case closure_invariant ([([], r', s')], [], {(post r', post s')}) of
Some((w,_,_) # _, _) ⇒ Some (rev w) | _ => None))"

lemma counterexample_sound:
assumes result: "counterexample r s = Some w"  and WF: "wf n r" "wf n s"
shows "w ∈ lang n r ⟷ w ∉ lang n s"
using assms unfolding counterexample_def Let_def
by (auto dest!: counterexample[of r s] split: option.splits list.splits)

text‹Auxiliary exacutable functions:›

definition reachable :: "'b rexp ⇒ 's set" where
"reachable s = snd (the (rtrancl_while (λ_. True) (λs. map (λa. post (delta a s)) (σ n)) (init s)))"

definition automaton :: "'b rexp ⇒ (('s * 'a) * 's) set" where
"automaton s =
snd (the
(let i = init s;
start = (([i], {post i}), {});
test_invariant = λ((ws, Z), A). ws ≠ [];
step_invariant = λ((ws, Z), A).
(let s = hd ws;
new_edges = map (λa. ((s, a), delta a s)) (σ n);
new = remdups (filter (λss. post ss ∉ Z) (map snd new_edges))
in ((new @ tl ws, post  set new ∪ Z), set new_edges ∪ A))
in while_option test_invariant step_invariant start))"

definition match :: "'b rexp ⇒ 'a list ⇒ bool" where
"match s w = final (fold delta w (init s))"

lemma match_correct: "⟦wf_word n w; wf n s⟧ ⟹ match s w ⟷ w ∈ lang n s"
unfolding match_def
by (induct w arbitrary: s) (auto simp: in_fold_lQuot lQuot_def)

end

locale rexp_DFA = rexp_DA σ wf_atom project lookup init delta final wf_state post L n
for σ :: "nat ⇒ 'a list"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool"
and init :: "'b rexp ⇒ 's"
and delta :: "'a ⇒ 's ⇒ 's"
and final :: "'s ⇒ bool"
and wf_state :: "'s ⇒ bool"
and post :: "'s ⇒ 's"
and L :: "'s ⇒ 'a lang"
and n :: nat +
assumes fin: "finite {fold delta w (init s) | w. True}"
begin

abbreviation "Reachable s ≡ {fold delta w (init s) | w. True}"

lemma closure_invariant_termination:
assumes WF: "wf n r" "wf n s"
and result: "closure_invariant ([([], init r, init s)], [], {(post (init r), post (init s))}) = None"
(is "closure_invariant ([([], ?r, ?s)], _) = None" is "?cl = None")
shows "False"
proof -
let ?D =  "post  Reachable r × post  Reachable s"
let ?X = "λps. ?D - map_prod post post  set ps"
let ?f = "λ(ws, ps, N). card (?X ps)"
have "∃st. ?cl = Some st" unfolding closure_invariant_def
proof (rule measure_while_option_Some[of "invariant ?r ?s" _ _ ?f], intro conjI)
fix st assume base: "invariant ?r ?s st" and "test_invariant st"
hence step: "invariant ?r ?s (step_invariant st)" by (rule invariant)
obtain ws ps N where st: "st = (ws, ps, N)" by (cases st) blast
hence "finite (?X ps)" by (blast intro: finite_cartesian_product fin)
moreover obtain ws' ps' N' where step_invariant: "step_invariant (ws, ps, N) = (ws', ps', N')"
by (cases "step_invariant (ws, ps, N)") blast
moreover
{ have "map_prod post post  set ps ⊆ ?D" using base[unfolded st invariant_def] by fast
moreover
have "map_prod post post  set ps' ⊆ ?D" using step[unfolded st step_invariant invariant_def]
by fast
moreover
{ have "distinct (map snd ws @ ps)" "inj_on (map_prod post post) (set (map snd ws @ ps))"
using base[unfolded st invariant_def] by (auto simp: bij_betw_def)
hence "distinct (map (map_prod post post) (map snd ws @ ps))" unfolding distinct_map ..
hence "map_prod post post  set ps ⊂ map_prod post post  set (snd (hd ws) # ps)"
using ‹test_invariant st› st by (cases ws) (simp_all, blast)
moreover have "map_prod post post  set ps' = map_prod post post  set (snd (hd ws) # ps)"
using step_invariant by (auto split: prod.splits)
ultimately have "map_prod post post  set ps ⊂ map_prod post post  set ps'" by simp
}
ultimately have "?X ps' ⊂ ?X ps" by (auto simp add: image_set simp del: set_map)
}
ultimately show "?f (step_invariant st) < ?f st" unfolding st step_invariant
using psubset_card_mono[of "?X ps" "?X ps'"] by simp
qed (auto simp add: invariant_start WF invariant)
then show False using result by auto
qed

lemma closure_termination:
assumes WF: "wf n r" "wf n s"
and result: "closure ([(init r, init s)], {(post (init r), post (init s))}) = None"
shows "False"
using trans[OF closure_invariant_closure[of "[([], init r, init s)]", simplified] result]
by (auto intro: closure_invariant_termination[OF WF])

lemma closure_invariant_complete:
assumes eq: "lang n r = lang n s"
and WF:  "wf n r" "wf n s"
shows "∃ps N. closure_invariant ([([], init r, init s)], [], {(post (init r), post (init s))}) =
Some([], ps, N)" (is "∃_ _. closure_invariant ([([], ?r, ?s)], _) = _" is "∃_ _. ?cl = _")
proof (cases ?cl)
case (Some st)
moreover obtain ws ps N where ws_ps_N: "st = (ws, ps, N)" by (cases st) blast
ultimately show ?thesis
proof (cases ws)
case (Cons wrs ws)
with Some obtain w where "counterexample r s = Some w" unfolding counterexample_def
by (cases wrs) (auto simp: ws_ps_N)
with eq counterexample_sound[OF _ WF] show ?thesis by blast
qed blast
qed (auto intro: closure_invariant_termination[OF WF])

lemma closure_complete:
assumes "lang n r = lang n s" "wf n r" "wf n s"
shows "∃N. closure ([(init r, init s)], {(post (init r), post (init s))}) = Some ([], N)"
using closure_invariant_complete[OF assms]
by (subst closure_invariant_closure[of "[([], init r, init s)]", simplified, symmetric]) auto

lemma check_eqv_complete:
assumes "lang n r = lang n s" "wf n r" "wf n s"
shows "check_eqv r s"
using closure_complete[OF assms] by (auto simp: check_eqv_def)

lemma counterexample_complete:
assumes "lang n r ≠ lang n s" and WF: "wf n r" "wf n s"
shows "∃w. counterexample r s = Some w"
using closure_invariant_sound[OF _ WF] closure_invariant_termination[OF WF] assms
by (fastforce simp: counterexample_def Let_def split: option.splits list.splits)

end

locale rexp_DA_no_post = rexp_DA σ wf_atom project lookup init delta final wf_state id L n
for σ :: "nat ⇒ 'a list"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool"
and init :: "'b rexp ⇒ 's"
and delta :: "'a ⇒ 's ⇒ 's"
and final :: "'s ⇒ bool"
and wf_state :: "'s ⇒ bool"
and L :: "'s ⇒ 'a lang"
and n :: nat
begin

lemma step_efficient[code]: "step (ws, N) =
(let
(r, s) = hd ws;
new = remdups (filter (λ(r,s). (r,s) ∉ N) (map (λa. (delta a r, delta a s)) (σ n)))
in (tl ws @ new, set new ∪ N))"
by (force simp: Let_def map_apfst_remdups' filter_map o_def split: prod.splits)

end

locale rexp_DFA_no_post = rexp_DFA σ wf_atom project lookup init delta final wf_state id L
for σ :: "nat ⇒ 'a list"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool"
and init :: "'b rexp ⇒ 's"
and delta :: "'a ⇒ 's ⇒ 's"
and final :: "'s ⇒ bool"
and wf_state :: "'s ⇒ bool"
and L :: "'s ⇒ 'a lang"
begin

sublocale rexp_DA_no_post by unfold_locales

end

locale rexp_DA_sim = project "set o σ" wf_atom project lookup
for σ :: "nat ⇒ 'a list"
and wf_atom :: "nat ⇒ 'b :: linorder ⇒ bool"
and project :: "'a ⇒ 'a"
and lookup :: "'b ⇒ 'a ⇒ bool" +
fixes init :: "'b rexp ⇒ 's"
fixes sim_delta :: "'s ⇒ 's list"
fixes final :: "'s ⇒ bool"
fixes wf_state :: "'s ⇒ bool"
fixes L :: "'s ⇒ 'a lang"
fixes post :: "'s ⇒ 's"
fixes n :: nat
assumes L_init[simp]: "wf n r ⟹ L (init r) = lang n r"
assumes final_iff_Nil[simp]: "final s ⟷ [] ∈ L s"
assumes L_wf_state[dest]: "wf_state s ⟹ L s ⊆ lists (set (σ n))"
assumes init_wf_state[simp]: "wf n r ⟹ wf_state (init r)"
assumes L_post[simp]: "wf_state s ⟹ L (post s) = L s"
assumes wf_state_post[simp]: "wf_state s ⟹ wf_state (post s)"
assumes L_sim_delta[simp]: "wf_state s ⟹ map L (sim_delta s) = map (λa. lQuot a (L s)) (σ n)"
assumes sim_delta_wf_state[simp]: "wf_state s ⟹ ∀s' ∈ set (sim_delta s). wf_state s'"
begin

definition "delta a s = sim_delta s ! index (σ n) a"

lemma length_sim_delta[simp]: "wf_state s ⟹ length (sim_delta s) = length (σ n)"
by (metis L_sim_delta length_map)

lemma L_delta[simp]: "⟦a ∈ set (σ n); wf_state s⟧ ⟹ L (delta a s) = lQuot a (L s)"
using L_sim_delta[of s] unfolding delta_def in_set_conv_nth
by (subst (asm) list_eq_iff_nth_eq) auto

lemma delta_wf_state[simp]: "⟦a ∈ set (σ n); wf_state s⟧ ⟹ wf_state (delta a s)"
unfolding delta_def by (auto intro: bspec[OF sim_delta_wf_state nth_mem])

sublocale rexp_DA σ wf_atom project lookup init delta final wf_state post L
by unfold_locales auto

sublocale rexp_DA_sim_no_post: rexp_DA_no_post σ wf_atom project lookup init delta final wf_state L
by unfold_locales auto

end

(*<*)
end
(*>*)


# Theory Init_Normalization

(* Author: Dmitriy Traytel *)

section "Initial Normalization of the Input"

(*<*)
theory Init_Normalization
imports Pi_Regular_Exp "HOL-Library.Simps_Case_Conv"
begin
(*>*)

fun toplevel_inters where
"toplevel_inters (Inter r s) = toplevel_inters r ∪ toplevel_inters s"
| "toplevel_inters r = {r}"

lemma toplevel_inters_nonempty[simp]:
"toplevel_inters r ≠ {}"
by (induct r) auto

lemma toplevel_inters_finite[simp]:
"finite (toplevel_inters r)"
by (induct r) auto

context alphabet
begin

lemma toplevel_inters_wf:
"wf n s = (∀r∈toplevel_inters s. wf n r)"
by (induct s) auto

end

context project
begin

lemma toplevel_inters_lang:
"r ∈ toplevel_inters s ⟹ lang n s ⊆ lang n r"
by (induct s) auto

lemma toplevel_inters_lang_INT:
"lang n s = (⋂r∈toplevel_inters s. lang n r)"
by (induct s) auto

lemma toplevel_inters_in_lang:
"w ∈ lang n s = (∀r∈toplevel_inters s. w ∈ lang n r)"
by (induct s) auto

lemma lang_flatten_INTERSECT_finite[simp]:
"finite X ⟹ w ∈ lang n (flatten INTERSECT X) =
(if X = {} then w ∈ lists (Σ n) else (∀r ∈ X. w ∈ lang n r))"
unfolding lang_INTERSECT by auto

end

fun merge_distinct where
"merge_distinct [] xs = xs"
| "merge_distinct xs [] = xs"
| "merge_distinct (a # xs) (b # ys) =
(if a = b then merge_distinct xs (b # ys)
else if a < b then a # merge_distinct xs (b # ys)
else b # merge_distinct (a # xs) ys)"

lemma set_merge_distinct[simp]: "set (merge_distinct xs ys) = set xs ∪ set ys"
by (induct xs ys rule: merge_distinct.induct) auto

lemma sorted_merge_distinct[simp]: "⟦sorted xs; sorted ys⟧ ⟹ sorted (merge_distinct xs ys)"
by (induct xs ys rule: merge_distinct.induct) (auto)

lemma distinct_merge_distinct[simp]: "⟦sorted xs; distinct xs; sorted ys; distinct ys⟧ ⟹
distinct (merge_distinct xs ys)"
by (induct xs ys rule: merge_distinct.induct) (auto)

lemma sorted_list_of_set_merge_distinct[simp]: "⟦sorted xs; distinct xs; sorted ys; distinct ys⟧ ⟹
merge_distinct xs ys = sorted_list_of_set (set xs ∪ set ys)"
by (auto intro: sorted_distinct_set_unique)

fun zip_with_option where
"zip_with_option f (Some a) (Some b) = Some (f a b)"
| "zip_with_option _ _ _ = None"

lemma zip_with_option_eq_Some[simp]:
"zip_with_option f x y = Some z ⟷ (∃a b. z = f a b ∧ x = Some a ∧ y = Some b)"
by (induct f x y rule: zip_with_option.induct) auto

fun Pluss where
"Pluss (Plus r s) = zip_with_option merge_distinct (Pluss r) (Pluss s)"
| "Pluss Zero = Some []"
| "Pluss Full = None"
| "Pluss r = Some [r]"

lemma Pluss_None[symmetric]: "Pluss r = None ⟷ Full ∈ toplevel_summands r"
by (induct r) auto

lemma Pluss_Some: "Pluss r = Some xs ⟷
(Full ∉ set xs ∧ xs = sorted_list_of_set (toplevel_summands r - {Zero}))"
proof (induct r arbitrary: xs)
case (Plus r s)
show ?case
proof safe
assume "Pluss (Plus r s) = Some xs"
then obtain a b where *: "Pluss r = Some a" "Pluss s = Some b" "xs = merge_distinct a b" by auto
with Plus(1)[of a] Plus(2)[of b]
show "xs = sorted_list_of_set (toplevel_summands (Plus r s) - {Zero})" by (simp add: Un_Diff)
assume "Full ∈ set xs" with Plus(1)[of a] Plus(2)[of b] * show False by (simp add: Pluss_None)
next
assume "Full ∉ set (sorted_list_of_set (toplevel_summands (Plus r s) - {Zero}))"
with Plus(1)[of "sorted_list_of_set (toplevel_summands r - {Zero})"]
Plus(2)[of "sorted_list_of_set (toplevel_summands s - {Zero})"]
show "Pluss (Plus r s) = Some (sorted_list_of_set (toplevel_summands (Plus r s) - {Zero}))"
qed
qed force+

fun Inters where
"Inters (Inter r s) = zip_with_option merge_distinct (Inters r) (Inters s)"
| "Inters Zero = None"
| "Inters Full = Some []"
| "Inters r = Some [r]"

lemma Inters_None[symmetric]: "Inters r = None ⟷ Zero ∈ toplevel_inters r"
by (induct r) auto

lemma Inters_Some: "Inters r = Some xs ⟷
(Zero ∉ set xs ∧ xs = sorted_list_of_set (toplevel_inters r - {Full}))"
proof (induct r arbitrary: xs)
case (Inter r s)
show ?case
proof safe
assume "Inters (Inter r s) = Some xs"
then obtain a b where *: "Inters r = Some a" "Inters s = Some b" "xs = merge_distinct a b" by auto
with Inter(1)[of a] Inter(2)[of b]
show "xs = sorted_list_of_set (toplevel_inters (Inter r s) - {Full})" by (simp add: Un_Diff)
assume "Zero ∈ set xs" with Inter(1)[of a] Inter(2)[of b] * show False by (simp add: Inters_None)
next
assume "Zero ∉ set (sorted_list_of_set (toplevel_inters (Inter r s) - {Full}))"
with Inter(1)[of "sorted_list_of_set (toplevel_inters r - {Full})"]
Inter(2)[of "sorted_list_of_set (toplevel_inters s - {Full})"]
show "Inters (Inter r s) = Some (sorted_list_of_set (toplevel_inters (Inter r s) - {Full}))"
qed
qed force+

definition inPlus where
"inPlus r s = (case Pluss (Plus r s) of None ⇒ Full | Some rs ⇒ PLUS rs)"

lemma inPlus_alt: "inPlus r s = (let X = toplevel_summands (Plus r s) - {Zero} in
flatten PLUS (if Full ∈ X then {Full} else X))"
proof (cases "Pluss r" "Pluss s" rule: option.exhaust[case_product option.exhaust])
case Some_Some then show ?thesis by (simp add: inPlus_def Pluss_None) (simp add: Pluss_Some Un_Diff)

fun inTimes where
"inTimes Zero _ = Zero"
| "inTimes _ Zero = Zero"
| "inTimes One r = r"
| "inTimes r One = r"
| "inTimes (Times r s) t = Times r (inTimes s t)"
| "inTimes r s = Times r s"

fun inStar where
"inStar Zero = One"
| "inStar Full = Full"
| "inStar One = One"
| "inStar (Star r) = Star r"
| "inStar r = Star r"

definition inInter where
"inInter r s = (case Inters (Inter r s) of None ⇒ Zero | Some rs ⇒ INTERSECT rs)"

lemma inInter_alt: "inInter r s = (let X = toplevel_inters (Inter r s) - {Full} in
flatten INTERSECT (if Zero ∈ X then {Zero} else X))"
proof (cases "Inters r" "Inters s" rule: option.exhaust[case_product option.exhaust])
case Some_Some then show ?thesis by (simp add: inInter_def Inters_None) (simp add: Inters_Some Un_Diff)

fun inNot where
"inNot Zero = Full"
| "inNot Full = Zero"
| "inNot (Not r) = r"
| "inNot (Plus r s) = Inter (inNot r) (inNot s)"
| "inNot (Inter r s) = Plus (inNot r) (inNot s)"
| "inNot r = Not r"

fun inPr where
"inPr Zero = Zero"
| "inPr One = One"
| "inPr (Plus r s) = Plus (inPr r) (inPr s)"
| "inPr r = Pr r"

primrec inorm where
"inorm Zero = Zero"
| "inorm Full = Full"
| "inorm One = One"
| "inorm (Atom a) = Atom a"
| "inorm (Plus r s) = Plus (inorm r) (inorm s)"
| "inorm (Times r s) = Times (inorm r) (inorm s)"
| "inorm (Star r) = inStar (inorm r)"
| "inorm (Not r) = inNot (inorm r)"
| "inorm (Inter r s) = inInter (inorm r) (inorm s)"
| "inorm (Pr r) = inPr (inorm r)"

context alphabet begin

lemma wf_inPlus[simp]: "⟦wf n r; wf n s⟧ ⟹ wf n (inPlus r s)"
by (subst (asm) (1 2) toplevel_summands_wf) (auto simp: inPlus_alt)

lemma wf_inTimes[simp]: "⟦wf n r; wf n s⟧ ⟹ wf n (inTimes r s)"
by (induct r s rule: inTimes.induct) auto

lemma wf_inStar[simp]: "wf n r ⟹ wf n (inStar r)"
by (induct r rule: inStar.induct) auto

lemma wf_inInter[simp]: "⟦wf n r; wf n s⟧ ⟹ wf n (inInter r s)"
by (subst (asm) (1 2) toplevel_inters_wf) (auto simp: inInter_alt)

lemma wf_inNot[simp]: "wf n r ⟹ wf n (inNot r)"
by (induct r rule: inNot.induct) auto

lemma wf_inPr[simp]: "wf (Suc n) r ⟹ wf n (inPr r)"
by (induct r rule: inPr.induct) auto

lemma wf_inorm[simp]: "wf n r ⟹ wf n (inorm r)"
by (induct r arbitrary: n) auto

end

context project begin

lemma lang_inPlus[simp]: "⟦wf n r; wf n s⟧ ⟹ lang n (inPlus r s) = lang n (Plus r s)"
by (auto 0 3 simp: inPlus_alt toplevel_summands_in_lang[of _ n r] toplevel_summands_in_lang[of _ n s]
dest: lang_subset_lists intro: bexI[of _ Full])

lemma lang_inTimes[simp]: "⟦wf n r; wf n s⟧ ⟹ lang n (inTimes r s) = lang n (Times r s)"
by (induct r s rule: inTimes.induct) (auto simp: conc_assoc)

lemma lang_inStar[simp]: "wf n r ⟹ lang n (inStar r) = lang n (Star r)"
by (induct r rule: inStar.induct)
(auto intro: star_if_lang dest: subsetD[OF star_subset_lists, rotated])

lemma Zero_toplevel_inters[dest]: "Zero ∈ toplevel_inters r ⟹ lang n r = {}"
by (metis lang.simps(1) subset_empty toplevel_inters_lang)

lemma toplevel_inters_Full: "⟦toplevel_inters r = {Full}; wf n r⟧ ⟹ lang n r = lists (Σ n)"
by (metis antisym lang.simps(2) subsetI toplevel_inters.simps(3) toplevel_inters_in_lang)

lemma toplevel_inters_subset_singleton[simp]: "toplevel_inters r ⊆ {s} ⟷ toplevel_inters r = {s}"
by (metis subset_refl subset_singletonD toplevel_inters_nonempty)

lemma lang_inInter[simp]: "⟦wf n r; wf n s⟧ ⟹ lang n (inInter r s) = lang n (Inter r s)"
using lang_subset_lists[of n, unfolded lang.simps(2)[symmetric]]
toplevel_inters_nonempty[of r] toplevel_inters_nonempty[of s]
apply (auto 0 2 simp: inInter_alt toplevel_inters_in_lang[of _ n r] toplevel_inters_in_lang[of _ n s]
toplevel_inters_wf[of n r] toplevel_inters_wf[of n s] Ball_def simp del: toplevel_inters_nonempty
dest!: toplevel_inters_Full[of _ n] split: if_splits)
by fastforce+

lemma lang_inNot[simp]: "wf n r ⟹ lang n (inNot r) = lang n (Not r)"
by (induct r rule: inNot.induct) (auto dest: lang_subset_lists)

lemma lang_inPr[simp]: "wf (Suc n) r ⟹ lang n (inPr r) = lang n (Pr r)"
by (induct r rule: inPr.induct) auto

lemma lang_inorm[simp]: "wf n r ⟹ lang n (inorm r) = lang n r"
by (induct r arbitrary: n) auto

end

(*<*)
end
(*>*)


# Theory PNormalization

(* Author: Dmitriy Traytel *)

section "Partial Derivatives-like Normalization"

(*<*)
theory PNormalization
imports Pi_Derivatives
begin
(*>*)

fun pnPlus :: "'a::linorder rexp ⇒ 'a rexp ⇒ 'a rexp" where
"pnPlus Zero r = r"
| "pnPlus r Zero = r"
(*<*)
(*
| "pnPlus Full r = Full"
| "pnPlus r Full = Full"
*)
(*>*)
| "pnPlus (Plus r s) t = pnPlus r (pnPlus s t)"
| "pnPlus r (Plus s t) =
(if r = s then (Plus s t)
else if r ≤ s then Plus r (Plus s t)
else Plus s (pnPlus r t))"
| "pnPlus r s =
(if r = s then r
else if r ≤ s then Plus r s
else Plus s r)"

lemma (in alphabet) wf_pnPlus[simp]: "⟦wf n r; wf n s⟧ ⟹ wf n (pnPlus r s)"
by (induct r s rule: pnPlus.induct) auto

lemma (in project) lang_pnPlus[simp]: "⟦wf n r; wf n s⟧ ⟹ lang n (pnPlus r s) = lang n (Plus r s)"
by (induct r s rule: pnPlus.induct) (auto dest!: lang_subset_lists dest: project
subsetD[OF star_subset_lists, unfolded in_lists_conv_set, rotated -1]
subsetD[OF conc_subset_lists, unfolded in_lists_conv_set, rotated -1])

fun pnTimes :: "'a::linorder rexp ⇒ 'a rexp ⇒ 'a rexp" where
"pnTimes Zero r = Zero"
| "pnTimes One r = r"
| "pnTimes (Plus r s) t = pnPlus (pnTimes r t) (pnTimes s t)"
| "pnTimes r s = Times r s"

lemma (in alphabet) wf_pnTimes[simp]: "⟦wf n r; wf n s⟧ ⟹ wf n (pnTimes r s)"
by (induct r s rule: pnTimes.induct) auto

lemma (in project) lang_pnTimes[simp]: "⟦wf n r; wf n s⟧ ⟹ lang n (pnTimes r s) = lang n (Times r s)"
by (induct r s rule: pnTimes.induct) auto

fun pnInter :: "'a::linorder rexp ⇒ 'a rexp ⇒ 'a rexp" where
"pnInter Zero r = Zero"
| "pnInter r Zero = Zero"
| "pnInter Full r = r"
| "pnInter r Full = r"
| "pnInter (Plus r s) t = pnPlus (pnInter r t) (pnInter s t)"
| "pnInter r (Plus s t) = pnPlus (pnInter r s) (pnInter r t)"
| "pnInter (Inter r s) t = pnInter r (pnInter s t)"
| "pnInter r (Inter s t) =
(if r = s then Inter s t
else if r ≤ s then Inter r (Inter s t)
else Inter s (pnInter r t))"
| "pnInter r s =
(if r = s then s
else if r ≤ s then Inter r s
else Inter s r)"

lemma (in alphabet) wf_pnInter[simp]: "⟦wf n r; wf n s⟧ ⟹ wf n (pnInter r s)"
by (induct r s rule: pnInter.induct) auto

lemma (in project) lang_pnInter[simp]: "⟦wf n r; wf n s⟧ ⟹ lang n (pnInter r s) = lang n (Inter r s)"
by (induct `