Theory RegSet_of_nat_DA

(*  Author:     Tobias Nipkow
    Copyright   1998 TUM

To generate a regular expression, the alphabet must be finite.
regexp needs to be supplied with an 'a list for a unique order

add_Atom d i j r a = (if d a i = j then Union r (Atom a) else r)
atoms d i j as = foldl (add_Atom d i j) Empty as

regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as)
                        else atoms d i j as
*)

section "From deterministic automata to regular sets"

theory RegSet_of_nat_DA
imports "Regular-Sets.Regular_Set" DA
begin

type_synonym 'a nat_next = "'a ⇒ nat ⇒ nat"

abbreviation
  deltas :: "'a nat_next ⇒ 'a list ⇒ nat ⇒ nat" where
  "deltas ≡ foldl2"

primrec trace :: "'a nat_next ⇒ nat ⇒ 'a list ⇒ nat list"  where
"trace d i [] = []" |
"trace d i (x#xs) = d x i # trace d (d x i) xs"

(* conversion a la Warshall *)

primrec regset :: "'a nat_next ⇒ nat ⇒ nat ⇒ nat ⇒ 'a list set" where
"regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j}
                          else {[a] | a. d a i = j})" |
"regset d i j (Suc k) =
  regset d i j k ∪
  (regset d i k k) @@ (star(regset d k k k)) @@ (regset d k j k)"

definition
 regset_of_DA :: "('a,nat)da ⇒ nat ⇒ 'a list set" where
"regset_of_DA A k = (⋃j∈{j. j<k ∧ fin A j}. regset (next A) (start A) j k)"

definition
 bounded :: "'a nat_next ⇒ nat ⇒ bool" where
"bounded d k = (∀n. n < k ⟶ (∀x. d x n < k))"

declare
  in_set_butlast_appendI[simp,intro] less_SucI[simp] image_eqI[simp]

(* Lists *)

lemma butlast_empty[iff]:
  "(butlast xs = []) = (case xs of [] ⇒ True | y#ys ⇒ ys=[])"
by (cases xs) simp_all

lemma in_set_butlast_concatI:
 "x ∈ set(butlast xs) ⟹ xs ∈ set xss ⟹ x ∈ set(butlast(concat xss))"
  by (metis concat.simps(2) concat_append in_set_butlast_appendI split_list_first)

(* Regular sets *)

(* The main lemma:
   how to decompose a trace into a prefix, a list of loops and a suffix.
*)
lemma decompose:
  "k ∈ set(trace d i xs) ⟹ 
    ∃pref mids suf.
      xs = pref @ concat mids @ suf ∧
      deltas d pref i = k ∧ (∀n∈set(butlast(trace d i pref)). n ≠ k) ∧
      (∀mid∈set mids. (deltas d mid k = k) ∧
                      (∀n∈set(butlast(trace d k mid)). n ≠ k)) ∧
      (∀n∈set(butlast(trace d k suf)). n ≠ k)"
proof (induction "xs" arbitrary: i)
  case Nil
  then show ?case
    by simp
next
  case (Cons a as)
  then consider "d a i = k" | "k ∈ set (trace d (d a i) as)" "d a i ≠ k"
    by auto
  then
  show ?case 
  proof cases
    case 1
    then show ?thesis
      apply (intro exI [where x = "[a]"], simp)
      apply (cases "k ∈ set(trace d (d a i) as)")
      using Cons.IH append.assoc concat.simps(2) set_ConsD apply metis
      by (metis Nil_is_append_conv append_Nil concat.simps(1) in_set_butlastD
          in_set_conv_decomp list.distinct(1))
  next
    case 2
    with Cons.IH [OF 2(1)] show ?thesis
      apply clarify
      subgoal for pref mids suf
        apply (rule exI [where x = "a#pref"])
        apply (rule exI [where x = mids])
        apply (rule exI [where x = suf])
        apply auto
        done
      done
  qed
qed

lemma length_trace[simp]: "⋀i. length(trace d i xs) = length xs"
by (induct "xs") simp_all

lemma deltas_append[simp]:
  "⋀i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)"
by (induct "xs") simp_all

lemma trace_append[simp]:
  "⋀i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys"
by (induct "xs") simp_all

lemma trace_concat[simp]:
 "(∀xs ∈ set xss. deltas d xs i = i) ⟹
  trace d i (concat xss) = concat (map (trace d i) xss)"
by (induct "xss") simp_all

lemma trace_is_Nil[simp]: "⋀i. (trace d i xs = []) = (xs = [])"
by (case_tac "xs") simp_all

lemma trace_is_Cons_conv[simp]:
 "(trace d i xs = n#ns) =
  (case xs of [] ⇒ False | y#ys ⇒ n = d y i ∧ ns = trace d n ys)"
by (auto simp: split: list.splits)

lemma set_trace_conv:
 "⋀i. set(trace d i xs) =
  (if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))"
  by (induct "xs") (simp_all add: insert_commute)

lemma deltas_concat[simp]:
 "(∀mid∈set mids. deltas d mid k = k) ⟹ deltas d (concat mids) k = k"
by (induct mids) simp_all

lemma lem: "[| n < Suc k; n ≠ k |] ==> n < k"
by arith

lemma regset_spec:
  "xs ∈ regset d i j k ⟷
   ((∀n∈set(butlast(trace d i xs)). n < k) ∧ deltas d xs i = j)"
proof (induction k arbitrary: i j xs)
  case 0
  then show ?case by (force split: list.split)
next
  case (Suc k)
  show ?case
  proof
    assume xs: "xs ∈ regset d i j (Suc k)"
    have *: "⋀ys. ys ∈ star (regset d k k k)
       ⟹ (∀m∈set (butlast (trace d k ys)). m < Suc k) ∧ deltas d ys k = k"
      by (erule star_induct; simp add: Suc set_trace_conv butlast_append ball_Un)
    show "(∀n∈set (butlast (trace d i xs)). n < Suc k) ∧ deltas d xs i = j"
      using xs Suc 
      apply (simp add: conc_def)
      apply (elim disjE exE conjE; simp add: set_trace_conv butlast_append ball_Un * Suc)
      done
  next
    assume §: "(∀n∈set (butlast (trace d i xs)). n < Suc k) ∧ deltas d xs i = j"
    show "xs ∈ regset d i j (Suc k)"
    proof (cases "k ∈ set(butlast(trace d i xs))")
      case True
      then obtain pref mids suf 
        where xs: "pref @ concat mids @ suf = xs"
          and k: "deltas d pref i = k"
          and "∀n∈set (butlast (trace d i pref)). n ≠ k"
          and 2: "⋀mid. mid∈set mids ⟹ 
                     deltas d mid k = k ∧ (∀n∈set (butlast (trace d k mid)). n ≠ k)"
          and 3: "∀n∈set (butlast (trace d k suf)). n ≠ k"
        by (auto dest!: in_set_butlastD decompose)
      then have 4: "∀n∈set (butlast (trace d i pref)). n < k"
        by (metis "§" in_set_butlast_appendI lem trace_append xs)
      have 1: "set mids ⊆ regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)"
        using xs k 2 
        apply (clarsimp simp: subset_iff Suc)
        using § by (force intro: lem in_set_butlast_concatI)
      have "∃xs ys. concat mids @ suf = xs @ ys ∧ xs ∈ star (regset d k k k) ∧ ys ∈ regset d k j k"
        using § 
        apply (simp add: Suc 4 k xs)
        using 1 2 3 concat_in_star
        by (metis deltas_append deltas_concat in_set_butlast_appendI k linorder_neqE_nat
            not_less_eq trace_append xs)
      with "4" Suc k xs
      show ?thesis
        by (fastforce simp add: conc_def)
    next
      case False
      with Suc § show ?thesis
        by (auto simp add: conc_def less_Suc_eq)
    qed
  qed
qed

lemma trace_below:
 "bounded d k ⟹ ∀i. i < k ⟶ (∀n∈set(trace d i xs). n < k)"
  unfolding bounded_def
  by (induct "xs") force+

lemma regset_below:
 "⟦bounded d k; i < k; j < k⟧ ⟹ regset d i j k = {xs. deltas d xs i = j}"
  by (force simp add: regset_spec dest: trace_below in_set_butlastD)

lemma deltas_below:
 "⋀i. bounded d k ⟹ i < k ⟹ deltas d w i < k"
  unfolding bounded_def
  by (induct w) force+

lemma regset_DA_equiv:
 "⟦bounded (next A) k; start A < k; j < k⟧ ⟹ (w ∈ regset_of_DA A k) = accepts A w"
  unfolding regset_of_DA_def
  by (simp cong: conj_cong add: regset_below deltas_below accepts_def delta_def)

end