Theory MDL

theory MDL
  imports Interval Trace
begin

section ‹Formulas and Satisfiability›

declare [[typedef_overloaded]]

datatype ('a, 't :: timestamp) formula = Bool bool | Atom 'a | Neg "('a, 't) formula" |
  Bin "bool ⇒ bool ⇒ bool" "('a, 't) formula" "('a, 't) formula" |
  Prev "'t ℐ" "('a, 't) formula" | Next "'t ℐ" "('a, 't) formula" |
  Since "('a, 't) formula" "'t ℐ" "('a, 't) formula" |
  Until "('a, 't) formula" "'t ℐ" "('a, 't) formula" |
  MatchP "'t ℐ" "('a, 't) regex" | MatchF "'t ℐ" "('a, 't) regex"
  and ('a, 't) regex = Lookahead "('a, 't) formula" | Symbol "('a, 't) formula" |
  Plus "('a, 't) regex" "('a, 't) regex" | Times "('a, 't) regex" "('a, 't) regex" |
  Star "('a, 't) regex"

fun eps :: "('a, 't :: timestamp) regex ⇒ bool" where
  "eps (Lookahead phi) = True"
| "eps (Symbol phi) = False"
| "eps (Plus r s) = (eps r ∨ eps s)"
| "eps (Times r s) = (eps r ∧ eps s)"
| "eps (Star r) = True"

fun atms :: "('a, 't :: timestamp) regex ⇒ ('a, 't) formula set" where
  "atms (Lookahead phi) = {phi}"
| "atms (Symbol phi) = {phi}"
| "atms (Plus r s) = atms r ∪ atms s"
| "atms (Times r s) = atms r ∪ atms s"
| "atms (Star r) = atms r"

lemma size_atms[termination_simp]: "phi ∈ atms r ⟹ size phi < size r"
  by (induction r) auto

fun wf_fmla :: "('a, 't :: timestamp) formula ⇒ bool"
  and wf_regex :: "('a, 't) regex ⇒ bool" where
  "wf_fmla (Bool b) = True"
| "wf_fmla (Atom a) = True"
| "wf_fmla (Neg phi) = wf_fmla phi"
| "wf_fmla (Bin f phi psi) = (wf_fmla phi ∧ wf_fmla psi)"
| "wf_fmla (Prev I phi) = wf_fmla phi"
| "wf_fmla (Next I phi) = wf_fmla phi"
| "wf_fmla (Since phi I psi) = (wf_fmla phi ∧ wf_fmla psi)"
| "wf_fmla (Until phi I psi) = (wf_fmla phi ∧ wf_fmla psi)"
| "wf_fmla (MatchP I r) = (wf_regex r ∧ (∀phi ∈ atms r. wf_fmla phi))"
| "wf_fmla (MatchF I r) = (wf_regex r ∧ (∀phi ∈ atms r. wf_fmla phi))"
| "wf_regex (Lookahead phi) = False"
| "wf_regex (Symbol phi) = wf_fmla phi"
| "wf_regex (Plus r s) = (wf_regex r ∧ wf_regex s)"
| "wf_regex (Times r s) = (wf_regex s ∧ (¬eps s ∨ wf_regex r))"
| "wf_regex (Star r) = wf_regex r"

fun progress :: "('a, 't :: timestamp) formula ⇒ 't list ⇒ nat" where
  "progress (Bool b) ts = length ts"
| "progress (Atom a) ts = length ts"
| "progress (Neg phi) ts = progress phi ts"
| "progress (Bin f phi psi) ts = min (progress phi ts) (progress psi ts)"
| "progress (Prev I phi) ts = min (length ts) (Suc (progress phi ts))"
| "progress (Next I phi) ts = (case progress phi ts of 0 ⇒ 0 | Suc k ⇒ k)"
| "progress (Since phi I psi) ts = min (progress phi ts) (progress psi ts)"
| "progress (Until phi I psi) ts = (if length ts = 0 then 0 else
  (let k = min (length ts - 1) (min (progress phi ts) (progress psi ts)) in
   Min {j. 0 ≤ j ∧ j ≤ k ∧ memR (ts ! j) (ts ! k) I}))"
| "progress (MatchP I r) ts = Min ((λf. progress f ts) ` atms r)"
| "progress (MatchF I r) ts = (if length ts = 0 then 0 else
  (let k = min (length ts - 1) (Min ((λf. progress f ts) ` atms r)) in
   Min {j. 0 ≤ j ∧ j ≤ k ∧ memR (ts ! j) (ts ! k) I}))"

fun bounded_future_fmla :: "('a, 't :: timestamp) formula ⇒ bool"
  and bounded_future_regex :: "('a, 't) regex ⇒ bool" where
  "bounded_future_fmla (Bool b) ⟷ True"
| "bounded_future_fmla (Atom a) ⟷ True"
| "bounded_future_fmla (Neg phi) ⟷ bounded_future_fmla phi"
| "bounded_future_fmla (Bin f phi psi) ⟷ bounded_future_fmla phi ∧ bounded_future_fmla psi"
| "bounded_future_fmla (Prev I phi) ⟷ bounded_future_fmla phi"
| "bounded_future_fmla (Next I phi) ⟷ bounded_future_fmla phi"
| "bounded_future_fmla (Since phi I psi) ⟷ bounded_future_fmla phi ∧ bounded_future_fmla psi"
| "bounded_future_fmla (Until phi I psi) ⟷ bounded_future_fmla phi ∧ bounded_future_fmla psi ∧ right I ∈ tfin"
| "bounded_future_fmla (MatchP I r) ⟷ bounded_future_regex r"
| "bounded_future_fmla (MatchF I r) ⟷ bounded_future_regex r ∧ right I ∈ tfin"
| "bounded_future_regex (Lookahead phi) ⟷ bounded_future_fmla phi"
| "bounded_future_regex (Symbol phi) ⟷ bounded_future_fmla phi"
| "bounded_future_regex (Plus r s) ⟷ bounded_future_regex r ∧ bounded_future_regex s"
| "bounded_future_regex (Times r s) ⟷ bounded_future_regex r ∧ bounded_future_regex s"
| "bounded_future_regex (Star r) ⟷ bounded_future_regex r"

lemmas regex_induct[case_names Lookahead Symbol Plus Times Star, induct type: regex] =
  regex.induct[of "λ_. True", simplified]

definition "Once I φ ≡ Since (Bool True) I φ"
definition "Historically I φ ≡ Neg (Once I (Neg φ))"
definition "Eventually I φ ≡ Until (Bool True) I φ"
definition "Always I φ ≡ Neg (Eventually I (Neg φ))"

fun rderive :: "('a, 't :: timestamp) regex ⇒ ('a, 't) regex" where
  "rderive (Lookahead phi) = Lookahead (Bool False)"
| "rderive (Symbol phi) = Lookahead phi"
| "rderive (Plus r s) = Plus (rderive r) (rderive s)"
| "rderive (Times r s) = (if eps s then Plus (rderive r) (Times r (rderive s)) else Times r (rderive s))"
| "rderive (Star r) = Times (Star r) (rderive r)"

lemma atms_rderive: "phi ∈ atms (rderive r) ⟹ phi ∈ atms r ∨ phi = Bool False"
  by (induction r) (auto split: if_splits)

lemma size_formula_positive: "size (phi :: ('a, 't :: timestamp) formula) > 0"
  by (induction phi) auto

lemma size_regex_positive: "size (r :: ('a, 't :: timestamp) regex) > Suc 0"
  by (induction r) (auto intro: size_formula_positive)

lemma size_rderive[termination_simp]: "phi ∈ atms (rderive r) ⟹ size phi < size r"
  by (drule atms_rderive) (auto intro: size_atms size_regex_positive)

locale MDL =
  fixes σ :: "('a, 't :: timestamp) trace"
begin

fun sat :: "('a, 't) formula ⇒ nat ⇒ bool"
  and match :: "('a, 't) regex ⇒ (nat × nat) set" where
  "sat (Bool b) i = b"
| "sat (Atom a) i = (a ∈ Γ σ i)"
| "sat (Neg φ) i = (¬ sat φ i)"
| "sat (Bin f φ ψ) i = (f (sat φ i) (sat ψ i))"
| "sat (Prev I φ) i = (case i of 0 ⇒ False | Suc j ⇒ mem (τ σ j) (τ σ i) I ∧ sat φ j)"
| "sat (Next I φ) i = (mem (τ σ i) (τ σ (Suc i)) I ∧ sat φ (Suc i))"
| "sat (Since φ I ψ) i = (∃j≤i. mem (τ σ j) (τ σ i) I ∧ sat ψ j ∧ (∀k ∈ {j<..i}. sat φ k))"
| "sat (Until φ I ψ) i = (∃j≥i. mem (τ σ i) (τ σ j) I ∧ sat ψ j ∧ (∀k ∈ {i..<j}. sat φ k))"
| "sat (MatchP I r) i = (∃j≤i. mem (τ σ j) (τ σ i) I ∧ (j, Suc i) ∈ match r)"
| "sat (MatchF I r) i = (∃j≥i. mem (τ σ i) (τ σ j) I ∧ (i, Suc j) ∈ match r)"
| "match (Lookahead φ) = {(i, i) | i. sat φ i}"
| "match (Symbol φ) = {(i, Suc i) | i. sat φ i}"
| "match (Plus r s) = match r ∪ match s"
| "match (Times r s) = match r O match s"
| "match (Star r) = rtrancl (match r)"

lemma "sat (Prev I (Bool False)) i ⟷ sat (Bool False) i"
  "sat (Next I (Bool False)) i ⟷ sat (Bool False) i"
  "sat (Since φ I (Bool False)) i ⟷ sat (Bool False) i"
  "sat (Until φ I (Bool False)) i ⟷ sat (Bool False) i"
  apply (auto split: nat.splits)
  done

lemma prev_rewrite: "sat (Prev I φ) i ⟷ sat (MatchP I (Times (Symbol φ) (Symbol (Bool True)))) i"
  apply (auto split: nat.splits)
  subgoal for j
    by (fastforce intro: exI[of _ j])
  done

lemma next_rewrite: "sat (Next I φ) i ⟷ sat (MatchF I (Times (Symbol (Bool True)) (Symbol φ))) i"
  by (fastforce intro: exI[of _ "Suc i"])

lemma trancl_Base: "{(i, Suc i) |i. P i}* = {(i, j). i ≤ j ∧ (∀k∈{i..<j}. P k)}"
proof -
  have "(x, y) ∈ {(i, j). i ≤ j ∧ (∀k∈{i..<j}. P k)}"
    if "(x, y) ∈ {(i, Suc i) |i. P i}*" for x y
    using that by (induct rule: rtrancl_induct) (auto simp: less_Suc_eq)
  moreover have "(x, y) ∈ {(i, Suc i) |i. P i}*"
    if "(x, y) ∈ {(i, j). i ≤ j ∧ (∀k∈{i..<j}. P k)}" for x y
    using that unfolding mem_Collect_eq prod.case Ball_def
    by (induct y arbitrary: x)
       (auto 0 3 simp: le_Suc_eq intro: rtrancl_into_rtrancl[rotated])
  ultimately show ?thesis by blast
qed

lemma Ball_atLeastLessThan_reindex:
  "(∀k∈{j..<i}. P (Suc k)) = (∀k ∈ {j<..i}. P k)"
  by (auto simp: less_eq_Suc_le less_eq_nat.simps split: nat.splits)

lemma since_rewrite: "sat (Since φ I ψ) i ⟷ sat (MatchP I (Times (Symbol ψ) (Star (Symbol φ)))) i"
proof (rule iffI)
  assume "sat (Since φ I ψ) i"
  then obtain j where j_def: "j ≤ i" "mem (τ σ j) (τ σ i) I" "sat ψ j"
    "∀k ∈ {j..<i}. sat φ (Suc k)"
    by auto
  have "k ∈ {Suc j..<Suc i} ⟹ (k, Suc k) ∈ match (Symbol φ)" for k
    using j_def(4)
    by (cases k) auto
  then have "(Suc j, Suc i) ∈ (match (Symbol φ))*"
    using j_def(1) trancl_Base
    by auto
  then show "sat (MatchP I (Times (Symbol ψ) (Star (Symbol φ)))) i"
    using j_def(1,2,3)
    by auto
next
  assume "sat (MatchP I (Times (Symbol ψ) (Star (Symbol φ)))) i"
  then obtain j where j_def: "j ≤ i" "mem (τ σ j) (τ σ i) I" "(Suc j, Suc i) ∈ (match (Symbol φ))*" "sat ψ j"
    by auto
  have "⋀k. k ∈ {Suc j..<Suc i} ⟹ (k, Suc k) ∈ match (Symbol φ)"
    using j_def(3) trancl_Base[of "λk. (k, Suc k) ∈ match (Symbol φ)"]
    by simp
  then have "∀k ∈ {j..<i}. sat φ (Suc k)"
    by auto
  then show "sat (Since φ I ψ) i"
    using j_def(1,2,4) Ball_atLeastLessThan_reindex[of j i "sat φ"]
    by auto
qed

lemma until_rewrite: "sat (Until φ I ψ) i ⟷ sat (MatchF I (Times (Star (Symbol φ)) (Symbol ψ))) i"
proof (rule iffI)
  assume "sat (Until φ I ψ) i"
  then obtain j where j_def: "j ≥ i" "mem (τ σ i) (τ σ j) I" "sat ψ j"
    "∀k ∈ {i..<j}. sat φ k"
    by auto
  have "k ∈ {i..<j} ⟹ (k, Suc k) ∈ match (Symbol φ)" for k
    using j_def(4)
    by auto
  then have "(i, j) ∈ (match (Symbol φ))*"
    using j_def(1) trancl_Base
    by simp
  then show "sat (MatchF I (Times (Star (Symbol φ)) (Symbol ψ))) i"
    using j_def(1,2,3)
    by auto
next
  assume "sat (MatchF I (Times (Star (Symbol φ)) (Symbol ψ))) i"
  then obtain j where j_def: "j ≥ i" "mem (τ σ i) (τ σ j) I" "(i, j) ∈ (match (Symbol φ))*" "sat ψ j"
    by auto
  have "⋀k. k ∈ {i..<j} ⟹ (k, Suc k) ∈ match (Symbol φ)"
    using j_def(3) trancl_Base[of "λk. (k, Suc k) ∈ match (Symbol φ)"]
    by auto
  then have "∀k ∈ {i..<j}. sat φ k"
    by simp
  then show "sat (Until φ I ψ) i"
    using j_def(1,2,4)
    by auto
qed

lemma match_le: "(i, j) ∈ match r ⟹ i ≤ j"
proof (induction r arbitrary: i j)
  case (Times r s)
  then show ?case using order.trans by fastforce
next
  case (Star r)
  from Star.prems show ?case
    unfolding match.simps
    by (induct i j rule: rtrancl.induct) (force dest: Star.IH)+
qed auto

lemma match_Times: "(i, i + n) ∈ match (Times r s) ⟷
  (∃k ≤ n. (i, i + k) ∈ match r ∧ (i + k, i + n) ∈ match s)"
  using match_le by auto (metis le_iff_add nat_add_left_cancel_le)

lemma rtrancl_unfold: "(x, z) ∈ rtrancl R ⟹
  x = z ∨ (∃y. (x, y) ∈ R ∧ x ≠ y ∧ (y, z) ∈ rtrancl R)"
  by (induction x z rule: rtrancl.induct) auto

lemma rtrancl_unfold': "(x, z) ∈ rtrancl R ⟹
  x = z ∨ (∃y. (x, y) ∈ rtrancl R ∧ y ≠ z ∧ (y, z) ∈ R)"
  by (induction x z rule: rtrancl.induct) auto

lemma match_Star: "(i, i + Suc n) ∈ match (Star r) ⟷
  (∃k ≤ n. (i, i + 1 + k) ∈ match r ∧ (i + 1 + k, i + Suc n) ∈ match (Star r))"
proof (rule iffI)
  assume assms: "(i, i + Suc n) ∈ match (Star r)"
  obtain k where k_def: "(i, k) ∈ local.match r" "i ≤ k" "i ≠ k"
    "(k, i + Suc n) ∈ (local.match r)*"
    using rtrancl_unfold[OF assms[unfolded match.simps]] match_le by auto
  from k_def(4) have "(k, i + Suc n) ∈ match (Star r)"
    unfolding match.simps by simp
  then have k_le: "k ≤ i + Suc n"
    using match_le by blast
  from k_def(2,3) obtain k' where k'_def: "k = i + Suc k'"
    by (metis Suc_diff_Suc le_add_diff_inverse le_neq_implies_less)
  show "∃k ≤ n. (i, i + 1 + k) ∈ match r ∧ (i + 1 + k, i + Suc n) ∈ match (Star r)"
    using k_def k_le unfolding k'_def by auto
next
  assume assms: "∃k ≤ n. (i, i + 1 + k) ∈ match r ∧
    (i + 1 + k, i + Suc n) ∈ match (Star r)"
  then show "(i, i + Suc n) ∈ match (Star r)"
    by (induction n) auto
qed

lemma match_refl_eps: "(i, i) ∈ match r ⟹ eps r"
proof (induction r)
  case (Times r s)
  then show ?case
    using match_Times[where ?i=i and ?n=0]
    by auto
qed auto

lemma wf_regex_eps_match: "wf_regex r ⟹ eps r ⟹ (i, i) ∈ match r"
  by (induction r arbitrary: i) auto

lemma match_Star_unfold: "i < j ⟹ (i, j) ∈ match (Star r) ⟹ ∃k ∈ {i..<j}. (i, k) ∈ match (Star r) ∧ (k, j) ∈ match r"
  using rtrancl_unfold'[of i j "match r"] match_le[of _ j r] match_le[of i _ "Star r"]
  by auto (meson atLeastLessThan_iff order_le_less)

lemma match_rderive: "wf_regex r ⟹ i ≤ j ⟹ (i, Suc j) ∈ match r ⟷ (i, j) ∈ match (rderive r)"
proof (induction r arbitrary: i j)
  case (Times r1 r2)
  then show ?case
    using match_refl_eps[of "Suc j" r2] match_le[of _ "Suc j" r2]
    apply (auto)
          apply (metis le_Suc_eq relcomp.simps)
         apply (meson match_le relcomp.simps)
        apply (metis le_SucE relcomp.simps)
       apply (meson relcomp.relcompI wf_regex_eps_match)
      apply (meson match_le relcomp.simps)
     apply (metis le_SucE relcomp.simps)
    apply (meson match_le relcomp.simps)
    done
next
  case (Star r)
  then show ?case
    using match_Star_unfold[of i "Suc j" r]
    by auto (meson match_le rtrancl.simps)
qed auto

end

lemma atms_nonempty: "atms r ≠ {}"
  by (induction r) auto

lemma atms_finite: "finite (atms r)"
  by (induction r) auto

lemma progress_le_ts:
  assumes "⋀t. t ∈ set ts ⟹ t ∈ tfin"
  shows "progress phi ts ≤ length ts"
  using assms
proof (induction phi ts rule: progress.induct)
  case (8 phi I psi ts)
  have "ts ≠ [] ⟹ Min {j. j ≤ min (length ts - Suc 0) (min (progress phi ts) (progress psi ts)) ∧
    memR (ts ! j) (ts ! min (length ts - Suc 0) (min (progress phi ts) (progress psi ts))) I}
    ≤ length ts"
    apply (rule le_trans[OF Min_le[where ?x="min (length ts - Suc 0) (min (progress phi ts) (progress psi ts))"]])
      apply (auto simp: in_set_conv_nth intro!: memR_tfin_refl 8(3))
    apply (metis One_nat_def diff_less length_greater_0_conv less_numeral_extra(1) min.commute min.strict_coboundedI2)
    done
  then show ?case
    by auto
next
  case (9 I r ts)
  then show ?case
    using atms_nonempty[of r] atms_finite[of r]
    by auto (meson Min_le dual_order.trans finite_imageI image_iff)
next
  case (10 I r ts)
  have "ts ≠ [] ⟹ Min {j. j ≤ min (length ts - Suc 0) (MIN f∈atms r. progress f ts) ∧
    memR (ts ! j) (ts ! min (length ts - Suc 0) (MIN f∈atms r. progress f ts)) I}
    ≤ length ts"
    apply (rule le_trans[OF Min_le[where ?x="min (length ts - Suc 0) (Min ((λf. progress f ts) ` atms r))"]])
      apply (auto simp: in_set_conv_nth intro!: memR_tfin_refl 10(2))
    apply (metis One_nat_def diff_less length_greater_0_conv less_numeral_extra(1) min.commute min.strict_coboundedI2)
    done
  then show ?case
    by auto
qed (auto split: nat.splits)

end