Theory Regular_Algebra_Models

(* Title:      Regular Algebras
   Author:     Simon Foster, Georg Struth
   Maintainer: Simon Foster <s.foster at york.ac.uk>
               Georg Struth <g.struth at sheffield.ac.uk>               
*)

section ‹Models of Regular Algebra›

theory Regular_Algebra_Models
  imports Regular_Algebras Kleene_Algebra.Kleene_Algebra_Models
begin

subsection ‹Language Model of Salomaa Algebra›

abbreviation w_length :: "'a list  nat" ( "|_|")
  where "|x|  length x"

definition l_ewp :: "'a lan  bool" where
  "l_ewp X  {[]}  X"

interpretation lan_kozen: K2_algebra "(+)" "(⋅)" "1 :: 'a lan" 0 "(⊆)" "(⊂)" "star" ..

interpretation lan_boffa: B1_algebra "(+)" "(⋅)" "1 :: 'a lan" 0 "(⊆)" "(⊂)" "star" ..

lemma length_lang_pow_lb:
  assumes "xX. |x|  k" "x  X^n" 
  shows "|x|  k*n"
using assms proof (induct n arbitrary: x)
  case 0 thus ?case by auto
next
  case (Suc n) 
  note hyp = this
  thus ?case
  proof -
    have "x  XSuc n ( y z. x = y@z  y  X  z  Xn)"
      by (simp add:c_prod_def times_list_def)
    also from hyp have "...  ( y z. x = y@z  |y|  k  |z|  k*n)"
      by auto
    also have "...  ( y z. x = y@z  |y|  k  |z|  k*n  ( |x| = |y| + |z| ))"
      by force
    also have "...  ( y z. x = y@z  |y|  k  |z|  k*n  ( |x|  (n + 1) * k ))"
      by (auto, metis add_mono mult.commute, force)
    finally show ?thesis
      by (metis Suc_eq_plus1 hyp(3) mult.commute)
  qed
qed

lemma l_prod_elim: "wX  Y  (u v. w = u@v  uX  vY)"
  by (simp add: c_prod_def times_list_def)

lemma power_minor_var: 
  assumes "wX. k|w|"
  shows "wXSuc n. n*k|w|"
  using assms
  apply (auto simp add: l_prod_elim)
  using length_lang_pow_lb trans_le_add2
  by (simp add: length_lang_pow_lb trans_le_add2 mult.commute)
 
lemma power_lb: "(wX. k|w| )  (w. wXSuc n n*k|w| )"
  by (metis power_minor_var)

lemma prod_lb: 
  " (wX. m  length w); (wY. n  length w)   (w(XY). (m+n)  length w)"
  by (metis l_prod_elim add_le_mono length_append) 

lemma suicide_aux_l: 
  " (wY. 0length w); (wXSuc n. n  length w)   (wXSuc n Y. n  length w)"
  apply (auto simp: l_prod_elim)
  apply (drule_tac x="ua @ va" in bspec)
  apply (auto simp add: l_prod_elim)
done

lemma suicide_aux_r: 
  " (wY. 0length w); (wXSuc n. n  length w)   (wY  XSuc n. n  length w)"
  by (auto, metis (full_types) le0 plus_nat.add_0 prod_lb)

lemma word_suicide_l: 
  assumes "¬ l_ewp X" "Y  {}"  
  shows "(wY. n. wXSuc n Y)"
proof -
  have  "vY. 0length v" 
    by (metis le0)
  from assms have "vX. 1length v"
    by (simp add: l_ewp_def, metis le_0_eq length_0_conv not_less_eq_eq)
  hence "wY. n. wXSuc n Y"
    by (metis nat_mult_1_right power_lb suicide_aux_l le0 Suc_n_not_le_n)
  thus ?thesis by metis
qed 

lemma word_suicide_r: 
  assumes "¬ l_ewp X" "Y  {}"  
  shows "(wY. n. wY  XSuc n)"
proof -
  have  "vY. 0length v" 
    by (metis le0)
  from assms have "vX. 1length v"
    by (simp add: l_ewp_def, metis le_0_eq length_0_conv not_less_eq_eq)
  hence "wY. n. wY  XSuc n ⇖"
    by (metis nat_mult_1_right power_lb suicide_aux_r le0 Suc_n_not_le_n)
  thus ?thesis by metis
qed 

lemma word_suicide_lang_l: " ¬ l_ewp X; Y  {}    n. ¬ (Y  XSuc n Y)"
  by (metis Set.set_eqI empty_iff in_mono word_suicide_l)

lemma word_suicide_lang_r: " ¬ l_ewp X; Y  {}    n. ¬ (Y  Y  XSuc n)"
  by (metis Set.set_eqI empty_iff in_mono word_suicide_r)

text ‹These duality results cannot be relocated easily›

context K1_algebra
begin

lemma power_dual_transfer [simp]: 
  "power.power (1::'a) (⊙) x n = xn⇖"
  by (induct n, simp_all, metis opp_mult_def power_commutes)

lemma aarden_aux_l:
  "y  x  y + z  y   xSuc n y + x  z"
  using dual.aarden_aux[of "y" "x" "z" "n"]
  by (auto simp add:opp_mult_def)

end

lemma arden_l: 
  assumes "¬ l_ewp y" "x = yx + z" 
  shows "x = y  z"
proof (rule antisym)
  show one: "y  z  x"
    by (metis assms(2) join_semilattice_class.add_comm left_near_kleene_algebra_class.star_inductl_eq)
  show "x  y  z"
  proof (cases "x = 0")
    show "x = 0  x  yz"  
      by simp
    assume assms': "x  0"
    have " n. x  ySuc n x + y  z"
      by (metis assms(2) kleene_algebra_class.aarden_aux_l subsetI)
    moreover then have " w n. w  x  w  ySuc n x  w  y  z"
      by (force simp: plus_set_def)
    ultimately show "x  y  z"
      by (metis (full_types) all_not_in_conv assms(1) subsetI word_suicide_l)
  qed
qed

lemma arden_r: 
  assumes "¬ l_ewp y" "x = x  y + z" 
  shows "x = z  y"
proof (rule antisym)
  show one: "z  y  x"
    by (metis assms(2) join.sup_commute kleene_algebra_class.star_inductr_var order_refl)
  show "x  z  y"
  proof (cases "x = 0")
    show "x = 0  x  z  y"  
      by simp
    assume assms': "x  0"
    have " n. x  x  ySuc n+ z  y"
      by (metis assms(2) kleene_algebra_class.aarden_aux subsetI)
    moreover then have " w n. w  x  w  x  ySuc n w  z  y"
      by (force simp: plus_set_def)
    ultimately show "x  z  y"
      by (metis (full_types) all_not_in_conv assms(1) subsetI word_suicide_r)
  qed
qed

text ‹The following two facts provide counterexamples to Arden's rule if the empty word property is not considered.›

lemma arden_l_counter: " (x::'a lan) (y::'a lan) (z::'a lan). x = y  x + z  x  y  z"
proof -
  have one: "(0::'a lan) + 1  1 = 1"
    by (metis ab_near_semiring_one_class.mult_onel kleene_algebra_class.dual.add_zerol)
  have two: "(1::'a lan)  1  0"
  proof -
    have "x1. (0::'a list set)  x1"
      by auto
    hence "(1::'a list set)  0"
      by (metis kleene_algebra_class.dual.annir kleene_algebra_class.dual.mult.right_neutral)
    thus "(1::'a list set)  1  0"
      by simp
  qed
  show ?thesis using one and two
    by (metis kleene_algebra_class.dual.add_zerol kleene_algebra_class.dual.add_zeror)
qed

lemma arden_r_counter: " (x::'a lan) (y::'a lan) (z::'a lan). x = x  y + z  x  z  y"
proof -
  have one: "(0::'a lan) + 1  1 = 1"
    by (metis ab_near_semiring_one_class.mult_onel kleene_algebra_class.dual.add_zerol)
  have two: "(1::'a lan)  0  1"
  proof -
    have "x1. (0::'a list set)  x1"
      by auto
    hence "(1::'a list set)  0"
      by (metis kleene_algebra_class.dual.annir kleene_algebra_class.dual.mult.right_neutral)
    thus "(1::'a list set)  0  1"
      by simp
  qed
  show ?thesis using one and two
    by (metis kleene_algebra_class.dual.add_zerol kleene_algebra_class.dual.add_zeror)
qed

interpretation lan_salomaa_l: Sl_algebra "(+)" "(⋅)" "1 :: 'a lan" 0 "(⊆)" "(⊂)" "star" "l_ewp"
proof
  fix x y z :: "'a lan"
  show "(1 + x) = x"
    by (metis kleene_algebra_class.dual.star2)
  show "l_ewp x = (y. x = 1 + y  ¬ l_ewp y)"
    by (simp add:l_ewp_def one_set_def one_list_def plus_set_def, metis insertCI mk_disjoint_insert)
  show "1 + x  x = x"
    by (metis kleene_algebra_class.star_unfoldl_eq)
  show "¬ l_ewp y  x = y  x + z  x = y  z"
    by (metis arden_l)
qed

interpretation lan_salomaa_r: Sr_algebra "(+)" "(⋅)" "1 :: 'a lan" 0 "(⊆)" "(⊂)" "star" "l_ewp"
proof
  fix x y z :: "'a lan"
  show "1 + x  x = x"
    by (metis kleene_algebra_class.star_unfoldr_eq)
  show "¬ l_ewp y  x = x  y + z  x = z  y"
    by (metis arden_r)
qed

subsection ‹Regular Language Model of Salomaa Algebra›

notation
  Atom ("_") and
  Plus (infixl "+r" 65) and
  Times (infixl "r" 70) and
  Star ("_r" [101] 100) and
  Zero ("0r") and
  One ("1r")

fun rexp_ewp :: "'a rexp  bool" where
  "rexp_ewp 0r = False" |
  "rexp_ewp 1r = True" |
  "rexp_ewp a = False" |
  "rexp_ewp (s +r t) = (rexp_ewp s  rexp_ewp t)" |
  "rexp_ewp (s r t) = (rexp_ewp s  rexp_ewp t)" |
  "rexp_ewp (sr) = True"

abbreviation "ro(s)  (if (rexp_ewp s) then 1r else 0r)"

lift_definition r_ewp :: "'a reg_lan  bool" is "l_ewp" .

lift_definition r_lang :: "'a rexp  'a reg_lan"  is "lang"
  by (simp)

abbreviation r_sim :: "'a rexp  'a rexp  bool" (infix "" 50) where
  "p  q  r_lang p = r_lang q"

declare Rep_reg_lan [simp]
declare Rep_reg_lan_inverse [simp]
declare Abs_reg_lan_inverse [simp]

lemma rexp_ewp_l_ewp: "l_ewp (lang x) = rexp_ewp x"
proof (induct x)
  case (Star x) thus ?case
    by (simp, metis lan_salomaa_l.EWP left_near_kleene_algebra_class.star_plus_one)
qed (simp_all add:l_ewp_def zero_set_def one_set_def one_list_def plus_set_def c_prod_def times_list_def)

theorem regexp_ewp:
  defines P_def: "P(t)   t'. t  ro(t) +r t'  ro(t') = 0r"
  shows "P t"
proof (induct t)
  show "P(0r)"
    by (simp add:P_def r_lang_def, rule_tac x="0r" in exI, simp)
next
  fix a
  show "P(a)"
    by (simp add:P_def r_lang_def, rule_tac x="a" in exI, simp)
next
  show "P(1r)"
    by (simp add:P_def r_lang_def, rule_tac x="0r" in exI, simp)
next
  fix t1 t2
  assume "P(t1)" "P(t2)"
  then obtain t1' t2' 
    where "t1  ro(t1) +r t1'" "ro(t1') = 0r"
          "t2  ro(t2) +r t2'" "ro(t2') = 0r"
    by (metis assms rexp.distinct(1))
  thus "P(t1 +r t2)"
    apply (subst P_def, transfer)
    apply (rule_tac x="t1' +r t2'" in exI)
    apply clarsimp
    by (metis (no_types, lifting) add.left_commute join.sup_assoc join.sup_left_idem rexp.distinct(2))
 next
  fix t1 t2
  assume "P(t1)" "P(t2)"
  then obtain t1' t2' 
    where t1: "t1  ro(t1) +r t1'" "ro(t1') = 0r" and
          t2: "t2  ro(t2) +r t2'" "ro(t2') = 0r"
      by (metis assms rexp.distinct(1))
  thus "P(t1 r t2)"
  proof -
    let ?t' = "ro(t1) r t2' +r t1' r ro(t2) +r t1' r t2'"
    from t1 t2 have r1: "ro(?t') = 0r"
      by (auto)
    from t1 t2 have "t1 r t2  (ro(t1) +r t1') r (ro(t2) +r t2')" (is "?l  ?r")
      by (transfer, simp)
    also have "?r  ro(t1) r ro(t2) +r ro(t1) r t2' +r t1' r ro(t2) +r t1' r t2'" (is "?l  ?r")
      apply (transfer, unfold lang.simps)
      apply (simp only: distrib_right' semiring_class.distrib_left)
      apply (metis (opaque_lifting, no_types) join_semilattice_class.add_comm semiring_class.combine_common_factor)
    done
    also have "?r  ro(t1 r t2) +r ro(t1) r t2' +r t1' r ro(t2) +r t1' r t2'" (is "?l  ?r")
      by (transfer, simp)
    also have "?r  ro(t1 r t2) +r ?t'"
      apply (transfer, unfold lang.simps)
      apply (metis (mono_tags) join_semilattice_class.add_assoc')
    done
    finally show ?thesis using r1
      apply (unfold P_def)
      apply (rule_tac x="?t'" in exI, simp)
    done
  qed
next
  fix s
  assume assm:"P s"
  then obtain s' where r1: "s  ro(s) +r s'" "ro(s') = 0r"
    by (metis assms rexp.distinct(1))
  thus "P (sr)"
  proof -
    let ?t' = "s' r (s')r"
    have r2: "ro(?t') = 0r"
      by (metis r1(2) rexp.distinct(1) rexp_ewp.simps(5))
    from assm r1 have "(ro(s) +r s')r  (s')r" (is "?l  ?r")
      by (transfer, auto)
    also have "?r  1r +r s' r (s')r" (is "?l  ?r")
      by (transfer, auto)
    also have "?r  ro(sr) +r ?t'"
      by (metis (full_types) rexp_ewp.simps(6))
    finally show ?thesis
      by (metis assms lang.simps(6) r1(1) r2 r_lang.abs_eq r_lang.rep_eq)
  qed
qed

instantiation reg_lan :: (type) Sr_algebra
begin

lift_definition ewp_reg_lan :: "'a reg_lan  bool" is "l_ewp" .

instance proof
  fix x :: "'a reg_lan"
  show "(1 + x) = x"
    by (metis kleene_algebra_class.dual.star2)
next
  fix x :: "'a reg_lan"
  show "1 + x  x = x"
    by (metis kleene_algebra_class.star_unfoldr_eq)
next
  fix x :: "'a reg_lan"
  show "ewp x = (y. x = 1 + y  ¬ ewp y)"
  proof -
    obtain t where "r_lang t = x"
      by (transfer, auto)
    moreover obtain t' where "t  ro(t) +r t'" "ro(t') = 0r"
      by (metis regexp_ewp)
    ultimately show ?thesis
      apply (transfer, auto)
      apply (metis (full_types) lang.simps(2) rexp.distinct(1) rexp_ewp_l_ewp)
      apply (metis lan_salomaa_l.EWP)
    done
  qed
next
  fix x y z :: "'a reg_lan"
  show " ¬ ewp y; x = x  y + z   x = z  y"
    by (transfer, metis lan_salomaa_r.Ar)
qed
end

instantiation reg_lan :: (type) Sl_algebra
begin

instance proof
  fix x :: "'a reg_lan"
  show "1 + x  x = x"
    by (metis left_pre_kleene_algebra_class.star_unfoldl_eq)
next
  fix x y z :: "'a reg_lan"
  show " ¬ ewp y; x = y  x + z   x = y  z"
    by (transfer, metis lan_salomaa_l.Al)
qed
end

instance reg_lan :: (type) S_algebra ..

theorem arden_regexp_l: 
  assumes "ro(y) = 0r" "x  y r x +r z" 
  shows "x  yr r z"
  using assms
  by (transfer, metis arden_l lang.simps(4) lang.simps(5) lang.simps(6) rexp.distinct(1) rexp_ewp_l_ewp)

theorem arden_regexp_r: 
  assumes "ro(y) = 0r" "x  x r y +r z" 
  shows "x  z r yr"
  using assms
  by transfer (metis lan_salomaa_r.Ar lang.simps(4) lang.simps(5) lang.simps(6) rexp.distinct(1) rexp_ewp_l_ewp)

end