Session MSO_Regex_Equivalence

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: "(xset xs. yset 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 "xset xs. yset 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 "xset xs. yset 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"
  by (auto simp add: conc_def)

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"
  by (simp_all add:conc_def)

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"
  by (simp add: hom_image_conc)

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 = {}"
  by (simp add: lang_pow_empty)

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)
  ultimately have "u@v : A ^^ (m+n)" by (simp add: lang_pow_add)
  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
  by (auto simp add: Cons_eq_append_conv)

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(auto simp add: Cons_eq_append_conv)
    apply(drule star_decom)
    apply(auto simp add: Cons_eq_append_conv)
    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"
  by(auto simp add: lQuot_def)

lemma lQuot_lists[simp]: "c : S  lQuot c (lists S) = lists S"
  by(auto simp add: lQuot_def)

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"
  by(auto simp add: rQuot_def)

lemma rQuot_lists[simp]: "c : S  rQuot c (lists S) = lists S"
  by(auto simp add: rQuot_def)

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"
  by(auto simp add: biQuot_def)

lemma biQuot_lists[simp]: "a : S  b : S  biQuot a b (lists S) = lists S"
  by(auto simp add: biQuot_def)

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  (mn. (A ^^ m) @@ B)"
proof (induct n)
  case 0 
  show "X = (A ^^ Suc 0) @@ X  (m0. (A ^^ m) @@ B)"
    using eq by simp
next
  case (Suc n)
  have ih: "X = (A ^^ Suc n) @@ X  (mn. (A ^^ m) @@ B)" by fact
  also have " = (A ^^ Suc n) @@ (A @@ X  B)  (mn. (A ^^ m) @@ B)" using eq by simp
  also have " = (A ^^ Suc (Suc n)) @@ X  ((A ^^ Suc n) @@ B)  (mn. (A ^^ m) @@ B)"
    by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm)
  also have " = (A ^^ Suc (Suc n)) @@ X  (mSuc n. (A ^^ m) @@ B)"
    by (auto simp add: atMost_Suc)
  finally show "X = (A ^^ Suc (Suc n)) @@ X  (mSuc 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)  (mn. B @@ (A ^^ m))"
proof (induct n)
  case 0 
  show "X = X @@ (A ^^ Suc 0)  (m0. B @@ (A ^^ m))"
    using eq by simp
next
  case (Suc n)
  have ih: "X = X @@ (A ^^ Suc n)  (mn. B @@ (A ^^ m))" by fact
  also have " = (X @@ A  B) @@ (A ^^ Suc n)  (mn. B @@ (A ^^ m))" using eq by simp
  also have " = X @@ (A ^^ Suc (Suc n))  (B @@ (A ^^ Suc n))  (mn. B @@ (A ^^ m))"
    by (simp add: conc_Un_distrib conc_assoc)
  also have " = X @@ (A ^^ Suc (Suc n))  (mSuc n. B @@ (A ^^ m))"
    by (auto simp add: atMost_Suc)
  finally show "X = X @@ (A ^^ Suc (Suc n))  (mSuc 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 = (rtoplevel_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 = (rtoplevel_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 = (rtoplevel_summands s. lang n r)"
  by (induct s) auto

lemma toplevel_summands_in_lang:
  "w  lang n s = (rtoplevel_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  {}" "rX. 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) = (stoplevel_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:
  "(atoplevel_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
   by (simp add: image_UN)
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)
qed (simp_all add: Let_def)


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 (simp add: takeWhile_takes_all)
  apply (simp add: takeWhile_takes_all)
  apply auto
  apply (metis (full_types) Suc_diff_le length_rev length_takeWhile_le take_Suc_Cons)
  apply (simp add: takeWhile_takes_all)
  apply (subst takeWhile_append2)
  apply auto
  apply (simp add: takeWhile_takes_all)
  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

fun rderiv_and_add where
  "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»)"

lemma invar_rderiv_and_add_init: "invar_rderiv_and_add as r (True, [«r»])"
  unfolding invar_rderiv_and_add_def by auto

lemma invar_rderiv_and_add_step: "invar_rderiv_and_add as r brs  fst brs 
  invar_rderiv_and_add as r (rderiv_and_add as brs)"
  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»»"
    by (simp add: ACI_norm_rderivs replicate_add rderivs_append)
  also have "«rderivs (replicate (m * i) as) r» = «r»" using assms
    by (simp add: rderivs_replicate_mult)
  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»"
  unfolding rderivs_append[symmetric] replicate_add[symmetric] by auto

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
  from while_option_rule[where P="invar_rderiv_and_add as r",
    OF invar_rderiv_and_add_step assms(2) invar_rderiv_and_add_init]
    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 
  from while_option_rule[where P="invar_rderiv_and_add as r",
    OF invar_rderiv_and_add_step assms invar_rderiv_and_add_init]
    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»"
    by (auto simp: invar_rderiv_and_add_def)
  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)»"
       unfolding replicate_add[symmetric] rderivs_append[symmetric] by (simp add: add.commute)
      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»" 
        unfolding rderivs_append[symmetric] replicate_add[symmetric] by (simp add: add.commute)
      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])
          (metis less_Suc_eq_le mod_less_divisor zero_less_Suc, simp add: add.commute)
      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_init invar_rderiv_and_add_step)
    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"]
    by (simp_all add: CoPr(1,3))
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 "xset 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. wlists (Σ 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') 
       (aset (σ 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') 
    (aset (σ 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 = (rtoplevel_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 = (rtoplevel_inters s. lang n r)"
  by (induct s) auto

lemma toplevel_inters_in_lang:
  "w  lang n s = (rtoplevel_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}))"
        by (simp add: Un_Diff)
  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}))"
        by (simp add: Un_Diff)
  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)
qed (simp_all add: inPlus_def Pluss_None)

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)
qed (simp_all add: inInter_def Inters_None)

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