Theory Regex_Proof_System

(*<*)
theory Regex_Proof_System
imports Regex
begin
(*>*)

context begin

qualified inductive
  SAT :: "(nat ⇒ 'a ⇒ bool) ⇒ nat ⇒ nat ⇒ 'a Regex.regex ⇒ bool"
  for sat where
  STest: "i = j ⟹ sat i x ⟹ SAT sat i j (Regex.Test x)"
| SSkip: "j = i + n ⟹ SAT sat i j (Regex.Skip n)"
| SPlusL: "SAT sat i j r ⟹ SAT sat i j (Regex.Plus r s)"
| SPlusR: "SAT sat i j s ⟹ SAT sat i j (Regex.Plus r s)"
| STimes: "SAT sat i k r ⟹ SAT sat k j s ⟹ SAT sat i j (Regex.Times r s)"
| SStar_eps: "i = j ⟹ SAT sat i j (Regex.Star r)"
| SStar: "i < j ⟹ (∃zs. xs = i # zs @ [j]) ⟹
    ∀k ∈ {0 ..< length xs - 1}. xs ! k < xs ! (Suc k) ⟹
    ∀k ∈ {0 ..< length xs - 1}. SAT sat (xs ! k) (xs ! (Suc k)) r ⟹
    SAT sat i j (Regex.Star r)"

lemma SAT_mono[mono]:
  assumes "X ≤ Y"
  shows "SAT X ≤ SAT Y"
  unfolding le_fun_def le_bool_def
proof safe
  fix i j r
  assume "SAT X i j r"
  then show "SAT Y i j r"
    by (induct i j r rule: SAT.induct) (use assms in ‹auto 0 3 intro: SAT.intros›)
qed

abbreviation "rm S ≡ {(i, j) ∈ S. i < j}"

qualified inductive
  VIO :: "(nat ⇒ 'a ⇒ bool) ⇒ nat ⇒ nat ⇒ 'a Regex.regex ⇒ bool"
  for vio where
  VSkip: "j ≠ i + n ⟹ VIO vio i j (Regex.Skip n)"
| VTest: "i = j ⟹ vio i x ⟹ VIO vio i j (Regex.Test x)"
| VTest_neq: "i ≠ j ⟹ VIO vio i j (Regex.Test x)"
| VPlus: "VIO vio i j r ⟹ VIO vio i j s ⟹ VIO vio i j (Regex.Plus r s)"
| VTimes: "∀k ∈ {i .. j}. VIO vio i k r ∨ VIO vio k j s ⟹ VIO vio i j (Regex.Times r s)"
| VStar: "i < j ⟹ i ∈ S ⟹ j ∈ T ⟹ S ∪ T = {i .. j} ⟹ S ∩ T = {} ⟹
    ∀(s, t) ∈ rm (S × T). VIO vio s t r ⟹ VIO vio i j (Regex.Star r)"
| VStar_gt: "i > j ⟹ VIO vio i j (Regex.Star r)"

lemma VIO_mono[mono]:
  assumes "X ≤ Y"
  shows "VIO X ≤ VIO Y"
  unfolding le_fun_def le_bool_def
proof safe
  fix i j r
  assume "VIO X i j r"
  then show "VIO Y i j r"
    by (induct i j r rule: VIO.induct) (use assms in ‹auto 5 3 intro: VIO.intros›)
qed

inductive chain :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" for R :: "'a ⇒ 'a ⇒ bool" where
	chain_singleton: "chain R [x]"
| chain_cons: "chain R (y # xs) ⟹ R x y ⟹ chain R (x # y # xs)"

lemma
  chain_Nil[simp]: "¬ chain R []" and
  chain_not_Nil: "chain R xs ⟹ xs ≠ []"
  by (auto elim: chain.cases)

lemma chain_rtranclp: "chain R xs ⟹ R⇧*⇧* (hd xs) (last xs)"
  by (induct xs rule: chain.induct) auto

lemma chain_append:
  assumes "chain R xs" "chain R ys" "R (last xs) (hd ys)"
  shows "chain R (xs @ ys)"
  using assms
proof (induct xs arbitrary: ys rule: chain.induct)
  case (chain_singleton x)
  then show ?case by (cases ys) (auto intro: chain.intros)
qed (auto intro: chain.intros)

lemma tranclp_imp_exists_finite_chain_list:
  "R⇧+⇧+ x y ⟹ ∃xs. chain R (x # xs @ [y])"
proof (induct rule: tranclp.induct)
  case (r_into_trancl x y)
  then have "chain R (x # [] @ [y])"
    by (auto intro: chain.intros)
  then show ?case
    by blast
next
  case (trancl_into_trancl x y z)
  note rstar_xy = this(1) and ih = this(2) and r_yz = this(3)
  obtain xs where xs: "chain R (x # xs @ [y])" using ih by blast
  define ys where "ys = xs @ [y]"
  have "chain R (x # ys @ [z])"
    unfolding ys_def using r_yz chain_append[OF xs chain_singleton, of z] by auto
  then show ?case by blast
qed

lemma chain_pairwise:
  "chain R xs ⟹ Suc i < length xs ⟹ R (xs ! i) (xs ! Suc i)"
  by (induct xs arbitrary: i rule: chain.induct)
    (force simp: nth_Cons' not_le Suc_less_eq2 elim: chain.cases)+

lemma chain_sorted_remdups:
  "chain R xs ⟹ (⋀x y. R x y ⟹ x ≤ y) ⟹ sorted xs ∧ chain R (remdups xs)"
proof (induct xs rule: chain.induct)
  case (chain_cons y xs x)
  then show ?case
    using sorted_remdups[of xs] set_remdups[of xs] eq_iff[of y "hd (remdups xs)"]
    by (cases "remdups xs"; cases "y = hd (remdups xs)")
      (auto intro!: chain.intros intro: order_trans elim: chain.cases)
qed (auto intro: chain.intros)

lemma sorted_remdups: "sorted xs ⟹ sorted_wrt (<) (remdups xs)"
  by (induct xs) (auto dest: le_neq_trans)

lemma remdups_sorted_start_end:
  "sorted (i # xs @ [j]) ⟹ i ≠ j ⟹
  remdups (i # xs @ [j]) = i # remdups (removeAll j (removeAll i xs)) @ [j]"
  by (induct xs) auto

lemma tranclp_to_list:
  fixes R :: "'a :: linorder ⇒ 'a ⇒ bool"
  assumes "R⇧+⇧+ i j" "i ≠ j" "⋀x y. R x y ⟹ x ≤ y"
  obtains xs zs where "xs = i # zs @ [j]"
    "∀k ∈ {0 ..< length xs - 1}. xs ! k < xs ! (Suc k) ∧ R (xs ! k) (xs ! (Suc k))"
proof atomize_elim
  from ‹R⇧+⇧+ i j› obtain zs where "chain R (i # zs @ [j])"
    using tranclp_imp_exists_finite_chain_list by fast
  then have zs: "sorted (i # zs @ [j])" "chain R (remdups (i # zs @ [j]))"
    using chain_sorted_remdups assms(3) by blast+
  then have sorted_wrt: "sorted_wrt (<) (remdups (i # zs @ [j]))"
    using sorted_remdups by blast
  let ?zs = "remdups (removeAll j (removeAll i zs))"
  from zs sorted_wrt have "chain R (i # ?zs @ [j])" "sorted_wrt (<) (i # ?zs @ [j])"
    using remdups_sorted_start_end[of i zs j] assms(2) by auto
  then show "∃xs zs. xs = i # zs @ [j] ∧
    (∀k∈{0..<length xs - 1}. xs ! k < xs ! Suc k ∧ R (xs ! k) (xs ! Suc k))"
    by (subst ex_comm, unfold simp_thms, intro exI[of _ ?zs])
      (auto 0 3 dest: chain_pairwise simp del: remdups.simps
      simp: sorted_wrt_iff_nth_less)
qed


abbreviation match_rel where
  "match_rel test r xs k ≡ (xs ! k < xs ! (Suc k) ∧ Regex.match test r (xs ! k) (xs ! (Suc k)))"

lemma list_to_chain:
  "xs ≠ [] ⟹ ∀k ∈ {0 ..< length xs - 1}. R (xs ! k) (xs ! Suc k) ⟹ chain R xs"
proof (induct xs)
  case (Cons a xs)
  then show ?case
  proof (cases xs)
    case tail: (Cons b ys)
    with Cons(2,3) show ?thesis
      by (force intro!: chain.intros Cons(1)[unfolded tail])
  qed (auto intro: chain.intros)
qed simp

lemma match_rel_list_to_tranclp:
  "∃xs zs. xs = i # zs @ [j] ∧ (∀k ∈ {0 ..< length xs - 1}. match_rel test r xs k) ⟹ i ≠ j ⟹
  (Regex.match test r)⇧+⇧+ i j"
  using chain_rtranclp[OF list_to_chain, THEN rtranclpD, of "i # _ @ [j]" "Regex.match test r"]
  by fastforce

lemma completeness_SAT: 
  "∀x ∈ Regex.atms r. ∀i. test i x ⟶ sat i x ⟹ Regex.match test r i j ⟹ SAT sat i j r"
proof (induct r arbitrary: i j)
  case (Skip x)
  then show ?case
    by (auto intro: SAT.SSkip)
next
  case (Test x)
  then show ?case
    by (auto intro: SAT.STest)
next
  case (Plus r1 r2)
  then show ?case
    by (auto intro: SAT.SPlusL SPlusR)
next
  case (Times r1 r2)
  then obtain k where k_def: "k ∈ {i .. j} ∧ SAT sat i k r1 ∧ SAT sat k j r2"
    using match_le by fastforce
  then show ?case by (auto intro: SAT.STimes)
next
  case (Star r)
  then have "i = j ∨ (i ≠ j ∧ (Regex.match test r)⇧+⇧+ i j)"
    using rtranclpD[of "Regex.match test r" i j] tranclpD[of "Regex.match test r" i j]
    by auto
  moreover
  {
    assume i_eq_j: "i = j"
    then have "SAT sat i j (Regex.Star r)" by (auto intro: SAT.SStar_eps)
  }
  moreover
  {
    assume i_neq_j: "i ≠ j" and tranclp_ij: "(Regex.match test r)⇧+⇧+ i j"
    then have i_less: "i < j" using Star
      by (auto simp add: le_neq_implies_less match_rtranclp_le)
    then obtain xs and zs where xs_def: "xs = i # zs @ [j] ∧ (∀k ∈ {0 ..< length xs - 1}. xs ! k < xs ! (Suc k) ∧ Regex.match test r (xs ! k) (xs ! (Suc k)))"
      using tranclp_to_list[OF tranclp_ij i_neq_j match_le[of test r]] by auto
    then have "SAT sat i j (Regex.Star r)" using i_less Star
      by (auto intro: SAT.SStar)
  }
  ultimately show ?case by auto
qed

lemma completeness_VIO: 
  "∀x ∈ Regex.atms r. ∀i. ¬ test i x ⟶ vio i x ⟹ i ≤ j ⟹ ¬ Regex.match test r i j ⟹ VIO vio i j r"
proof (induct r arbitrary: i j)
  case (Skip x)
  then show ?case
    by (auto intro: VIO.VSkip)
next
  case (Test x)
  then show ?case
    by (auto intro: VIO.VTest VIO.VTest_neq)
next
  case (Plus r1 r2)
  then show ?case
    by (auto intro: VIO.VPlus)
next
  case (Times r1 r2)
  then have "∀k ∈ {i .. j}. VIO vio i k r1 ∨ VIO vio k j r2"
    by fastforce
  then show ?case
    by (auto intro: VIO.VTimes)
next
  case (Star r)
  define V where V_def: "V = {i .. j}"
  define S where S_def: "S = {k ∈ V. (Regex.match test r)⇧*⇧* i k} ∪ {i}"
  define T where T_def: "T = V - S"
  from S_def V_def have j_notin_S: "j ∉ S" using Star
    by auto
  from S_def have i_in_S: "i ∈ S"
    by auto
  then have j_in_T: "j ∈ T" using j_notin_S V_def T_def Star(3)
    by auto    
  from Star have nmatch_ij: "¬ (Regex.match test r)⇧*⇧* i j"
    by auto
  from S_def T_def V_def Star(3) have union_ST: "S ∪ T = {i .. j}"
    by auto
  from S_def T_def V_def Star(4) have inter_ST: "S ∩ T = {}"
    by auto
  with i_in_S j_in_T Star(3) have i_less_j: "i < j"
    using le_eq_less_or_eq by blast
  {
    assume not_viost: "¬ (∀(s,t) ∈ rm (S × T). VIO vio s t r)"
    then obtain s and t where st_def: "(s, t) ∈ rm (S × T) ∧ ¬ VIO vio s t r"
      by auto
    then have "Regex.match test r s t" using Star
      by auto
    then have "(Regex.match test r)⇧*⇧* i t" using st_def S_def
      by auto
    then have False using T_def st_def S_def
      by auto
  }
  then have no_path: "∀(s,t) ∈ rm (S × T). VIO vio s t r"
    by auto
  then show ?case
    by (auto intro: VIO.VStar[OF i_less_j i_in_S j_in_T union_ST inter_ST no_path])
qed

lemma soundness_SAT:
  "∀x ∈ Regex.atms r. ∀i. sat i x ⟶ test i x ⟹ SAT sat i j r ⟹ Regex.match test r i j"
proof(induct r arbitrary: i j)
  case (Skip x)
  then show ?case using SAT.simps[of sat i j "Regex.Skip x"]
    by auto
next
  case (Test x)
  then show ?case using SAT.simps[of sat i j "Regex.Test x"]
    by auto
next
  case (Plus r1 r2)
  then show ?case using SAT.simps[of sat i j "Regex.Plus r1 r2"]
    by auto
next
  case (Times r1 r2)
  then show ?case using SAT.simps[of sat i j "Regex.Times r1 r2"]
    by fastforce
next
  case (Star r)
  then show ?case
  proof(cases "i = j")
    case True
    then show ?thesis
      by auto
  next
    case False
    then obtain xs and zs where xs_form: "xs = i # zs @ [j]" and
      xs_props: "∀k ∈ {0 ..< length xs - 1}. xs ! k < xs ! (Suc k) ∧ SAT sat (xs ! k) (xs ! (Suc k)) r"
      using Star(3) SAT.simps[of sat i j "Regex.Star r"]
      by blast
    then have kmatch: "∀k ∈ {0 ..< length xs - 1}. Regex.match test r (xs ! k) (xs ! Suc k)"
      using Star
      by auto
    then have ex_lists: "∃xs zs. xs = i # zs @ [j] ∧
      (∀k ∈ {0 ..< length xs - 1}. xs ! k < xs ! (Suc k) ∧ Regex.match test r (xs ! k) (xs ! (Suc k)))"
      using xs_form xs_props by auto
    then have "(Regex.match test r)⇧+⇧+ i j"
      using match_rel_list_to_tranclp[OF ex_lists False] by auto
    then show ?thesis
      by auto
  qed
qed

lemma soundness_VIO:
"∀x ∈ Regex.atms r. ∀i. vio i x ⟶ ¬ test i x ⟹ i ≤ j ⟹ VIO vio i j r ⟹ ¬ Regex.match test r i j"
proof(induct r arbitrary: i j)
  case (Skip x)
  then show ?case using VIO.simps[of vio i j "Regex.Skip x"]
    by auto
next
  case (Test x)
  then show ?case using VIO.simps[of vio i j "Regex.Test x"]
    by auto
next
  case (Plus r1 r2)
  then show ?case using VIO.simps[of vio i j "Regex.Plus r1 r2"]
    by auto
next
  case (Times r1 r2)
  then have kvio: "∀k ∈ {i .. j}. VIO vio i k r1 ∨ VIO vio k j r2"
    using VIO.simps[of vio i j "Regex.Times r1 r2"]
    by auto
  have "∀k. Regex.match test r i k ∧ Regex.match test r k j ⟶ k ∈ {i .. j}"
    using match_le
    by auto
  then show ?case using Times kvio match_le[of test]
    unfolding Ball_def atLeastAtMost_iff match.simps regex.simps relcompp_apply
    by (metis Un_iff)
next
  case (Star r)
  then obtain S and T where S_def: "i ∈ S" and T_def: "j ∈ T" and
    ST_props: "S ∪ T = {i .. j} ∧ S ∩ T = {}" and
    st_vio: "∀(s,t) ∈ rm (S × T). VIO vio s t r"
    using Star(4) VIO.simps[of vio i j "Regex.Star r"]
    by auto
  then have nmatch_st: "∀(s,t) ∈ rm (S × T). ¬ Regex.match test r s t"
    using Star
    by auto
  from S_def T_def ST_props have i_neq_j: "i ≠ j"
    by auto
  {
    assume rtranclp_ij: "(Regex.match test r)⇧*⇧* i j"
    then have tranclp_ij: "(Regex.match test r)⇧+⇧+ i j"
      using rtranclpD[of "Regex.match test r" i j] i_neq_j
      by auto

    obtain xs and zs where xs_def: "xs = i # zs @ [j]" and
      xs_prop: "∀k ∈ {0 ..< length xs - 1}.  match_rel test r xs k"
      using tranclp_to_list[OF tranclp_ij i_neq_j match_le[of test r]]
      by auto

    with S_def T_def ST_props have "∃k ∈ {0 ..< length xs - 1}. (xs ! k) ∈ S ∧ (xs ! (Suc k)) ∈ T"
    proof (induction zs arbitrary: S T i j xs)
      case Nil
      then show ?case using S_def T_def xs_def
        by auto
    next
      case (Cons a zs')
      from Cons(2-6) have match: "Regex.match test r i a"
        by force
      show ?case
      proof (cases "a ∈ T")
        case True
        then have "xs ! 0 ∈ S ∧ xs ! Suc 0 ∈ T" using S_def Cons
          by (auto simp: xs_def)
        then show ?thesis using S_def Cons(1)[of _ _ _ _ xs] Cons(2-5)
          by force
      next
        case False
        from Cons(5,6) have "chain (<) (i # (a # zs') @ [j])"
          by (intro list_to_chain) auto
        then have "sorted (i # (a # zs') @ [j])"
          using chain_sorted_remdups[of "(<)" "i # (a # zs') @ [j]"]
          by auto
        then have "a ∈ {i .. j}"
          by auto
        with Cons(2-6) False have "∃k∈{0..<length (tl xs) - 1}. tl xs ! k ∈ {i ∈ S. a ≤ i} ∧ tl xs ! Suc k ∈ {i ∈ T. a ≤ i}"
          by (intro Cons(1)[of a _ j]) (auto dest: bspec[of _ _ "Suc _"])
        with Cons show ?thesis
          by (auto intro: bexI[of _ "Suc _"])
      qed
    qed
    then have False using nmatch_st xs_prop
      by auto
  }
  then show ?case
    by auto
qed

end

(*<*)
end
(*>*)