Theory Rewriting

(*
    Author:   Salomon Sickert
    Author:   Benedikt Seidl
    Author:   Alexander Schimpf (original entry: CAVA/LTL_Rewrite.thy)
    License:  BSD
*)

section ‹Rewrite Rules for LTL Simplification›

theory Rewriting
imports
  LTL "HOL-Library.Extended_Nat"
begin

text ‹This theory provides rewrite rules for the simplification of LTL formulas. It supports:
  \begin{itemize}
    \item Constants Removal
    \item @{const Next_ltln}-Normalisation
    \item Modal Simplification (based on pure eventual, pure universal, or suspendable formulas)
    \item Syntactic Implication Checking
  \end{itemize}
  It reuses parts of LTL\_Rewrite.thy (CAVA, LTL\_TO\_GBA). Furthermore, some rules were taken from
  cite"DBLP:conf/cav/SomenziB00" and cite"DBLP:conf/tacas/BabiakKRS12". All functions are defined for @{type ltln}.›



subsection ‹Constant Eliminating Constructors›

definition mk_and
where
  "mk_and x y  case x of falsen  falsen | truen  y | _  (case y of falsen  falsen | truen  x | _  x andn y)"

definition mk_or
where
  "mk_or x y  case x of falsen  y | truen  truen | _  (case y of truen  truen | falsen  x | _  x orn y)"

fun remove_strong_ops
where
  "remove_strong_ops (x Un y) = remove_strong_ops y"
| "remove_strong_ops (x Mn y) = x andn y"
| "remove_strong_ops (x orn y) = remove_strong_ops x orn remove_strong_ops y"
| "remove_strong_ops x = x"

fun remove_weak_ops
where
  "remove_weak_ops (x Rn y) = remove_weak_ops y"
| "remove_weak_ops (x Wn y) = x orn y"
| "remove_weak_ops (x andn y) = remove_weak_ops x andn remove_weak_ops y"
| "remove_weak_ops x = x"

definition mk_finally
where
  "mk_finally x  case x of truen  truen | falsen  falsen | _  Fn (remove_strong_ops x)"

definition mk_globally
where
  "mk_globally x  case x of truen  truen | falsen  falsen | _  Gn (remove_weak_ops x)"

definition mk_until
where
  "mk_until x y  case x of falsen  y
    | truen  mk_finally y
    | _  (case y of truen  truen | falsen  falsen | _  x Un y)"

definition mk_release
where
  "mk_release x y  case x of truen  y
    | falsen  mk_globally y
    | _  (case y of truen  truen | falsen  falsen | _  x Rn y)"

definition mk_weak_until
where
  "mk_weak_until x y  case y of truen  truen
    | falsen  mk_globally x
    | _  (case x of truen  truen | falsen  y | _  x Wn y)"

definition mk_strong_release
where
  "mk_strong_release x y  case y of falsen  falsen
    | truen  mk_finally x
    | _  (case x of truen  y | falsen  falsen | _  x Mn y)"

definition mk_next
where
  "mk_next x  case x of truen  truen | falsen  falsen | _  Xn x"

definition mk_next_pow ("Xn''")
where
  "mk_next_pow n x  case x of truen  truen | falsen  falsen | _  (Next_ltln ^^ n) x"



lemma mk_and_semantics [simp]:
  "w n mk_and x y  w n x andn y"
  unfolding mk_and_def by (cases x; cases y; simp)

lemma mk_or_semantics [simp]:
  "w n mk_or x y  w n x orn y"
  unfolding mk_or_def by (cases x; cases y; simp)

lemma remove_strong_ops_sound [simp]:
  "w n Fn (remove_strong_ops y)  w n Fn y"
  by (induction y arbitrary: w) (auto; force)+

lemma remove_weak_ops_sound [simp]:
  "w n Gn (remove_weak_ops y)  w n Gn y"
  by (induction y arbitrary: w) (auto; force)+

lemma mk_finally_semantics [simp]:
  "w n mk_finally x  w n Fn x"
  by (simp add: mk_finally_def del: semantics_ltln.simps(8,9) remove_strong_ops.simps split: ltln.splits)

lemma mk_globally_semantics [simp]:
  "w n mk_globally x  w n Gn x"
  by (simp add: mk_globally_def del: semantics_ltln.simps(8,9) remove_weak_ops.simps split: ltln.splits)

lemma mk_until_semantics [simp]:
  "w n mk_until x y  w n x Un y"
proof (cases x)
  case (True_ltln)
    show ?thesis
      unfolding True_ltln mk_until_def
      by (cases y) auto
next
  case (False_ltln)
    thus ?thesis
      by (force simp: mk_until_def)
qed (cases y; force simp: mk_until_def)+

lemma mk_release_semantics [simp]:
  "w n mk_release x y  w n x Rn y"
proof (cases x)
  case (False_ltln)
    thus ?thesis
      unfolding False_ltln mk_release_def
      by (cases y) auto
next
  case (True_ltln)
    thus ?thesis
      by (force simp: mk_release_def)
qed (cases y; force simp: mk_release_def)+

lemma mk_weak_until_semantics [simp]:
  "w n mk_weak_until x y  w n x Wn y"
proof (cases y)
  case (False_ltln)
    thus ?thesis
      unfolding False_ltln mk_weak_until_def
      by (cases x) auto
next
  case (True_ltln)
    thus ?thesis
      by (force simp: mk_weak_until_def)
qed (cases x; force simp: mk_weak_until_def)+

lemma mk_strong_release_semantics [simp]:
  "w n mk_strong_release x y  w n x Mn y"
proof (cases y)
  case (True_ltln)
    show ?thesis
      unfolding True_ltln mk_strong_release_def
      by (cases x) auto
next
  case (False_ltln)
    thus ?thesis
      by (force simp: mk_strong_release_def)
qed (cases x; force simp: mk_strong_release_def)+

lemma mk_next_semantics [simp]:
  "w n mk_next x  w n Xn x"
  unfolding mk_next_def by (cases x; auto)

lemma mk_next_pow_semantics [simp]:
  "w n mk_next_pow i x  suffix i w n x"
  by (induction i arbitrary: w; cases x)
     (auto simp: mk_next_pow_def)

lemma mk_next_pow_simp [simp, code_unfold]:
  "mk_next_pow 0 x = x"
  "mk_next_pow 1 x = mk_next x"
  by (cases x; simp add: mk_next_pow_def mk_next_def)+



subsection ‹Constant Propagation›

fun is_constant :: "'a ltln  bool"
where
  "is_constant truen = True"
| "is_constant falsen = True"
| "is_constant _ = False"

lemma is_constant_constructorsI:
  "is_constant x  is_constant y  is_constant (mk_and x y)"
  "¬is_constant x  ¬is_constant y  ¬is_constant (mk_and x y)"
  "is_constant x  is_constant y  is_constant (mk_or x y)"
  "¬is_constant x  ¬is_constant y  ¬is_constant (mk_or x y)"
  "is_constant x   is_constant (mk_finally x)"
  "¬is_constant x   ¬is_constant (mk_finally x)"
  "is_constant x  is_constant (mk_globally x)"
  "¬is_constant x   ¬is_constant (mk_globally x)"
  "is_constant x  is_constant (mk_until y x)"
  "¬is_constant x  ¬is_constant (mk_until y x)"
  "is_constant x  is_constant (mk_release y x)"
  "¬is_constant x  ¬is_constant (mk_release y x)"
  "is_constant x  is_constant y  is_constant (mk_weak_until x y)"
  "¬is_constant x  ¬is_constant y  ¬is_constant (mk_weak_until x y)"
  "is_constant x  is_constant y  is_constant (mk_strong_release x y)"
  "¬is_constant x  ¬is_constant y  ¬is_constant (mk_strong_release x y)"
  "is_constant x  is_constant (mk_next x)"
  "¬is_constant x  ¬is_constant (mk_next x)"
  "is_constant x  is_constant (mk_next_pow n x)"
  by (cases x; cases y; simp add: mk_and_def mk_or_def mk_finally_def mk_globally_def mk_until_def mk_release_def mk_weak_until_def mk_strong_release_def mk_next_def mk_next_pow_def)+

lemma is_constant_constructors_simps:
  "mk_next_pow n x = falsen  x = falsen"
  "mk_next_pow n x = truen  x = truen"
  "is_constant (mk_next_pow n x)  is_constant x"
  by (induction n) (cases x; simp add: mk_next_pow_def)+

lemma is_constant_constructors_simps2:
  "is_constant (mk_and x y)  (x = truen  y = truen  x = falsen  y = falsen)"
  "is_constant (mk_or x y)  (x = falsen  y = falsen  x = truen  y = truen)"
  "is_constant (mk_finally x)  is_constant x"
  "is_constant (mk_globally x)  is_constant x"
  "is_constant (mk_until y x)  is_constant x"
  "is_constant (mk_release y x)  is_constant x"
  "is_constant (mk_next x)  is_constant x"
  by ((cases x; cases y; simp add: mk_and_def),
      (cases x; cases y; simp add: mk_or_def),
      (meson is_constant_constructorsI)+)

lemma is_constant_constructors_simps3:
  "is_constant (mk_weak_until x y)  (x = falsen  y = falsen  x = truen  y = truen)"
  "is_constant (mk_strong_release x y)  (x = truen  y = truen  x = falsen  y = falsen)"
  by (cases x; cases y; simp add: mk_weak_until_def mk_strong_release_def is_constant_constructors_simps2)+

lemma is_constant_semantics:
  "is_constant φ  ((w. w n φ)  ¬(w. w n φ))"
  by (cases φ) auto

lemma until_constant_simp:
  "is_constant ψ  w n φ Un ψ  w n ψ"
  by (cases ψ) auto

lemma release_constant_simp:
  "is_constant ψ  w n φ Rn ψ  w n ψ"
  by (cases ψ) auto

lemma mk_next_pow_dist:
  "mk_next_pow (i + j) φ = mk_next_pow i (mk_next_pow j φ)"
  by (cases j; simp) (cases φ; simp add: mk_next_pow_def funpow_add; simp add: funpow_swap1)

lemma mk_next_pow_until:
  "suffix (min i j) w n (mk_next_pow (i - j) φ) Un (mk_next_pow (j - i) ψ)  w n (mk_next_pow i φ) Un (mk_next_pow j ψ)"
  by (simp add: mk_next_pow_dist min_def add.commute)

lemma mk_next_pow_release:
  "suffix (min i j) w n (mk_next_pow (i - j) φ) Rn (mk_next_pow (j - i) ψ)  w n (mk_next_pow i φ) Rn (mk_next_pow j ψ)"
  by (simp add: mk_next_pow_dist min_def add.commute)

subsection ‹X-Normalisation›

text ‹The following rewrite functions pulls the X-operator up in the syntax tree. This preprocessing
  step enables the removal of X-operators in front of suspendable formulas. Furthermore constants are
  removed as far as possible.›

fun the_enat_0 :: "enat  nat"
where
  "the_enat_0 i = i"
| "the_enat_0  = 0"

lemma the_enat_0_simp [simp]:
  "the_enat_0 0 = 0"
  "the_enat_0 1 = 1"
  by (simp add: zero_enat_def one_enat_def)+

fun combine :: "('a ltln  'a ltln  'a ltln)  ('a ltln * enat)  ('a ltln * enat)  ('a ltln * enat)"
where
  "combine binop (φ, i) (ψ, j) = (
    let
      χ = binop (mk_next_pow (the_enat_0 (i - j)) φ) (mk_next_pow (the_enat_0 (j - i)) ψ)
    in
      (χ, if is_constant χ then  else min i j))"

lemma fst_combine:
  "fst (combine binop (φ, i) (ψ, j)) = binop (mk_next_pow (the_enat_0 (i - j)) φ) (mk_next_pow (the_enat_0 (j - i)) ψ)"
  unfolding combine.simps by (meson fstI)

abbreviation to_ltln :: "('a ltln * enat)  'a ltln"
where
  "to_ltln x  mk_next_pow (the_enat_0 (snd x)) (fst x)"

fun rewrite_X_enat :: "'a ltln  ('a ltln * enat)"
where
  "rewrite_X_enat truen = (truen, )"
| "rewrite_X_enat falsen = (falsen, )"
| "rewrite_X_enat propn(a) = (propn(a), 0)"
| "rewrite_X_enat npropn(a) = (npropn(a), 0)"
| "rewrite_X_enat (φ andn ψ) = combine mk_and (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (φ orn ψ) = combine mk_or (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (φ Un ψ) = combine mk_until (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (φ Rn ψ) = combine mk_release (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (φ Wn ψ) = combine mk_weak_until (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (φ Mn ψ) = combine mk_strong_release (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (Xn φ) = (λ(φ, n). (φ, eSuc n)) (rewrite_X_enat φ)"

definition
  "rewrite_X φ = to_ltln (rewrite_X_enat φ)"

lemma combine_infinity_invariant:
  assumes "i =   is_constant x"
  assumes "j =   is_constant y"
  shows "combine mk_and (x, i) (y, j) = (z, k)  (k =   is_constant z)"
    and "combine mk_or (x, i) (y, j) = (z, k)  (k =   is_constant z)"
    and "combine mk_until (x, i) (y, j) = (z, k)  (k =   is_constant z)"
    and "combine mk_release (x, i) (y, j) = (z, k)  (k =   is_constant z)"
    and "combine mk_weak_until (x, i) (y, j) = (z, k)  (k =   is_constant z)"
    and "combine mk_strong_release (x, i) (y, j) = (z, k)  (k =   is_constant z)"
  by (cases i; cases j; simp add: assms Let_def; force intro: is_constant_constructorsI)+

lemma combine_and_or_semantics:
  assumes "i =   is_constant φ"
  assumes "j =   is_constant ψ"
  shows "w n to_ltln (combine mk_and (φ, i) (ψ, j))  w n to_ltln (φ, i) andn to_ltln (ψ, j)"
    and "w n to_ltln (combine mk_or (φ, i) (ψ, j))  w n to_ltln (φ, i) orn to_ltln (ψ, j)"
  by ((cases i; cases j; simp add: min_def is_constant_constructors_simps is_constant_constructors_simps2 assms),
      (cases ψ; insert assms; auto),
      (cases φ; insert assms; auto),
      (blast elim!: is_constant.elims))+

lemma combine_until_release_semantics:
  assumes "i =   is_constant φ"
  assumes "j =   is_constant ψ"
  shows "w n to_ltln (combine mk_until (φ, i) (ψ, j))  w n to_ltln (φ, i) Un to_ltln (ψ, j)"
    and "w n to_ltln (combine mk_release (φ, i) (ψ, j))  w n to_ltln (φ, i) Rn to_ltln (ψ, j)"
  by ((cases i; cases j; simp add: is_constant_constructors_simps is_constant_constructors_simps2
       until_constant_simp release_constant_simp mk_next_pow_until mk_next_pow_release del: semantics_ltln.simps),
      (blast dest: is_constant_semantics),
      (cases ψ; simp add: assms),
      (cases φ; insert assms; auto simp: add.commute))+

(* TODO this proof is a bit slow and could be optimized *)
lemma combine_weak_until_strong_release_semantics:
  assumes "i =   is_constant φ"
  assumes "j =   is_constant ψ"
  shows "w n to_ltln (combine mk_weak_until (φ, i) (ψ, j))  w n to_ltln (φ, i) Wn to_ltln (ψ, j)"
    and "w n to_ltln (combine mk_strong_release (φ, i) (ψ, j))  w n to_ltln (φ, i) Mn to_ltln (ψ, j)"
  by ((cases i; cases j; simp add: min_def is_constant_constructors_simps is_constant_constructors_simps3 del: semantics_ltln.simps),
      (cases φ; simp add: assms),
      (cases ψ; insert assms; auto simp: add.commute))+



lemma rewrite_X_enat_infinity_invariant:
  "snd (rewrite_X_enat φ) =   is_constant (fst (rewrite_X_enat φ))"
proof (induction φ)
  case (And_ltln φ ψ)
    thus ?case
      by (simp add: combine_infinity_invariant[OF And_ltln(1,2), unfolded prod.collapse])
next
  case (Or_ltln φ ψ)
    thus ?case
      by (simp add: combine_infinity_invariant[OF Or_ltln(1,2), unfolded prod.collapse])
next
  case (Until_ltln φ ψ)
    thus ?case
      by (simp add: combine_infinity_invariant[OF Until_ltln(1,2), unfolded prod.collapse])
next
  case (Release_ltln φ ψ)
    thus ?case
      by (simp add: combine_infinity_invariant[OF Release_ltln(1,2), unfolded prod.collapse])
next
  case (WeakUntil_ltln φ ψ)
    thus ?case
      by (simp add: combine_infinity_invariant[OF WeakUntil_ltln(1,2), unfolded prod.collapse])
next
  case (StrongRelease_ltln φ ψ)
    thus ?case
      by (simp add: combine_infinity_invariant[OF StrongRelease_ltln(1,2), unfolded prod.collapse])
next
  case (Next_ltln φ)
    thus ?case
      by (simp add: split_def) (metis eSuc_infinity eSuc_inject)
qed auto

lemma rewrite_X_enat_correct:
  "w n φ  w n to_ltln (rewrite_X_enat φ)"
proof (induction φ arbitrary: w)
  case (And_ltln φ ψ)
    thus ?case
      using combine_and_or_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant] by fastforce
next
  case (Or_ltln φ ψ)
    thus ?case
      using combine_and_or_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant] by fastforce
next
  case (Until_ltln φ ψ)
    thus ?case
      unfolding rewrite_X_enat.simps combine_until_release_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant, unfolded prod.collapse] by fastforce
next
  case (Release_ltln φ ψ)
    thus ?case
      unfolding rewrite_X_enat.simps combine_until_release_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant, unfolded prod.collapse] by fastforce
next
  case (WeakUntil_ltln φ ψ)
    thus ?case
      unfolding rewrite_X_enat.simps combine_weak_until_strong_release_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant, unfolded prod.collapse] by fastforce
next
  case (StrongRelease_ltln φ ψ)
    thus ?case
      unfolding rewrite_X_enat.simps combine_weak_until_strong_release_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant, unfolded prod.collapse] by fastforce
next
  case (Next_ltln φ)
  moreover
    have " w n to_ltln (rewrite_X_enat (Xn φ))  suffix 1 w n to_ltln (rewrite_X_enat φ)"
      by (simp add: split_def; cases "snd (rewrite_X_enat φ)  ")
         (auto simp: eSuc_def, auto simp: rewrite_X_enat_infinity_invariant eSuc_def dest: is_constant_semantics)
    ultimately
    show ?case
       using semantics_ltln.simps(7) by blast
qed auto

lemma rewrite_X_sound [simp]:
  "w n rewrite_X φ  w n φ"
  using rewrite_X_enat_correct unfolding rewrite_X_def Let_def by auto

subsection ‹Pure Eventual, Pure Universal, and Suspendable Formulas›

fun pure_eventual :: "'a ltln  bool"
where
  "pure_eventual truen = True"
| "pure_eventual falsen = True"
| "pure_eventual (μ andn μ') = (pure_eventual μ  pure_eventual μ')"
| "pure_eventual (μ orn μ') = (pure_eventual μ  pure_eventual μ')"
| "pure_eventual (μ Un μ') = (μ = truen  pure_eventual μ')"
| "pure_eventual (μ Rn μ') = (pure_eventual μ  pure_eventual μ')"
| "pure_eventual (μ Wn μ') = (pure_eventual μ  pure_eventual μ')"
| "pure_eventual (μ Mn μ') = (pure_eventual μ  pure_eventual μ'  μ' = truen)"
| "pure_eventual (Xn μ) = pure_eventual μ"
| "pure_eventual _ = False"

fun pure_universal :: "'a ltln  bool"
where
  "pure_universal truen = True"
| "pure_universal falsen = True"
| "pure_universal (ν andn ν') = (pure_universal ν  pure_universal ν')"
| "pure_universal (ν orn ν') = (pure_universal ν  pure_universal ν')"
| "pure_universal (ν Un ν') = (pure_universal ν  pure_universal ν')"
| "pure_universal (ν Rn ν') = (ν = falsen  pure_universal ν')"
| "pure_universal (ν Wn ν') = (pure_universal ν  pure_universal ν'  ν' = falsen)"
| "pure_universal (ν Mn ν') = (pure_universal ν  pure_universal ν')"
| "pure_universal (Xn ν) = pure_universal ν"
| "pure_universal _ = False"

fun suspendable :: "'a ltln  bool"
where
  "suspendable truen = True"
| "suspendable falsen = True"
| "suspendable (ξ andn ξ') = (suspendable ξ  suspendable ξ')"
| "suspendable (ξ orn ξ') = (suspendable ξ  suspendable ξ')"
| "suspendable (φ Un ξ) = (φ = truen  pure_universal ξ  suspendable ξ)"
| "suspendable (φ Rn ξ) = (φ = falsen  pure_eventual ξ  suspendable ξ)"
| "suspendable (φ Wn ξ) = (suspendable φ  suspendable ξ  pure_eventual φ  ξ = falsen)"
| "suspendable (φ Mn ξ) = (suspendable φ  suspendable ξ  pure_universal φ  ξ = truen)"
| "suspendable (Xn ξ) = suspendable ξ"
| "suspendable _ = False"

lemma pure_eventual_left_append:
  "pure_eventual μ  w n μ  (u  w) n μ"
proof (induction μ arbitrary: u w)
  case (Until_ltln μ μ')
    moreover
    then obtain i where "suffix i w n μ'"
      by auto
    hence "μ = truen  ?case"
      by simp (metis suffix_conc_length suffix_suffix)
    moreover
    have "pure_eventual μ'  (u  w) n μ'"
      by (metis suffix i w n μ' Until_ltln(2) prefix_suffix)
    hence "pure_eventual μ'  ?case"
      by force
    ultimately
    show ?case
      by fastforce
next
  case (Release_ltln μ μ')
    thus ?case
      by (cases "i. suffix i w n μ'"; simp_all)
         (metis linear suffix_conc_snd gr0I not_less0 prefix_suffix suffix_0)+
next
  case (WeakUntil_ltln μ μ')
    thus ?case
      by (cases "i. suffix i w n μ'"; simp_all)
         (metis zero_le le0 nat_le_linear prefix_suffix suffix_0 suffix_conc_length suffix_conc_snd suffix_subseq_join)+
next
  case (StrongRelease_ltln μ μ')
    moreover
    then obtain i where "suffix i w n μ andn μ'"
      by auto
    hence "μ' = truen  ?case"
      by simp (metis suffix_conc_length suffix_suffix)
    moreover
    have "pure_eventual μ  pure_eventual μ'  (u  w) n μ andn μ'"
      by (metis suffix i w n μ andn μ' calculation(1) calculation(2) prefix_suffix semantics_ltln.simps(5))
    hence "pure_eventual μ  pure_eventual μ'  ?case"
      by force
    ultimately
    show ?case
      by fastforce
qed (auto, metis diff_zero le_0_eq not_less_eq_eq suffix_conc_length suffix_conc_snd word_split)

lemma pure_universal_suffix_closed:
  "pure_universal ν  (u  w) n ν  w n ν"
proof (induction ν arbitrary: u w)
  case (Until_ltln ν ν')
    hence "i. suffix i (u  w) n ν'  (j<i. suffix j (u  w) n ν)"
      using semantics_ltln.simps(8) by blast
    thus ?case
      by simp (metis Until_ltln(1-3) le_0_eq le_eq_less_or_eq le_less_linear prefix_suffix pure_universal.simps(5) suffix_conc_fst suffix_conc_snd)
next
  case (Release_ltln ν ν')
    moreover
    hence "i. suffix i (u  w) n ν'  (j<i. suffix j (u  w) n ν)"
      by simp
    ultimately
    show ?case
      by simp (metis semantics_ltln.simps(2) not_less0 prefix_suffix suffix_0 suffix_conc_length suffix_suffix)
next
  case (WeakUntil_ltln ν ν')
    moreover
    hence "i. suffix i (u  w) n ν  (ji. suffix j (u  w) n ν')"
      by simp
    ultimately
    show ?case
      by simp (metis (full_types) le_antisym prefix_suffix semantics_ltln.simps(2) suffix_0 suffix_conc_length suffix_suffix zero_le)
next
  case (StrongRelease_ltln ν ν')
    hence "i. suffix i (u  w) n ν  (ji. suffix j (u  w) n ν')"
      using semantics_ltln.simps(11) by blast
    thus ?case
      by simp (metis StrongRelease_ltln(1-3) diff_is_0_eq nat_le_linear prefix_conc_length prefix_suffix pure_universal.simps(8) subsequence_length suffix_conc_snd suffix_subseq_join)
next
  case (Next_ltln μ)
    thus ?case
      by (metis prefix_suffix pure_universal.simps(9) semantics_ltln.simps(7) semiring_normalization_rules(24) suffix_conc_length suffix_suffix)
qed auto

lemma suspendable_prefix_invariant:
  "suspendable ξ  (u  w) n ξ  w n ξ"
proof (induction ξ arbitrary: u w)
  case (Until_ltln ξ ξ')
    show ?case
    proof (cases "suspendable ξ'")
      case False
        hence "ξ = truen" and "pure_universal ξ'"
          using Until_ltln by simp+
        thus ?thesis
          by (simp; metis (no_types) linear pure_universal_suffix_closed suffix_conc_fst suffix_conc_length suffix_conc_snd suffix_suffix)
    qed (simp; metis Until_ltln(2) not_less0 prefix_suffix)
next
  case (Release_ltln ξ ξ')
    show ?case
    proof (cases "suspendable ξ'")
      case False
        hence "ξ = falsen" and "pure_eventual ξ'"
          using Release_ltln by simp+
        thus ?thesis
          by (simp; metis (no_types) le_iff_add add_diff_cancel_left' linear pure_eventual_left_append suffix_0 suffix_conc_fst suffix_conc_snd)
    qed (simp; metis Release_ltln(2) not_less0 prefix_suffix)
next
  case (WeakUntil_ltln ξ ξ')
    show ?case
    proof (cases "suspendable ξ  suspendable ξ'")
      case False
        hence "ξ' = falsen" and "pure_eventual ξ"
          using WeakUntil_ltln by simp+
        thus ?thesis
          by (simp; metis (no_types) le_iff_add add_diff_cancel_left' linear pure_eventual_left_append suffix_0 suffix_conc_fst suffix_conc_snd)
      qed (simp; metis (full_types) WeakUntil_ltln.IH prefix_suffix)
next
  case (StrongRelease_ltln ξ ξ')
    show ?case
    proof (cases "suspendable ξ  suspendable ξ'")
      case False
        hence "ξ' = truen" and "pure_universal ξ"
          using StrongRelease_ltln by simp+
        thus ?thesis
          by (simp; metis (no_types) linear pure_universal_suffix_closed suffix_conc_fst suffix_conc_length suffix_conc_snd suffix_suffix)
    qed (simp; metis (full_types) StrongRelease_ltln.IH(1) StrongRelease_ltln.IH(2) prefix_suffix)
qed (simp_all, metis prefix_suffix)

theorem pure_eventual_until_simp:
  assumes "pure_eventual μ"
  shows "w n φ Un μ  w n μ"
proof -
  have "i. suffix i w n μ  w n μ"
    using pure_eventual_left_append[OF assms] prefix_suffix by metis
  thus ?thesis
    by force
qed

theorem pure_universal_release_simp:
  assumes "pure_universal ν"
  shows "w n φ Rn ν  w n ν"
proof -
  have "i. w n ν  suffix i w n ν"
    using pure_universal_suffix_closed[OF assms] prefix_suffix by metis
  thus ?thesis
    by force
qed

theorem pure_universal_weak_until_simp:
  assumes "pure_universal φ" and "pure_universal ψ"
  shows "w n φ Wn ψ  w n φ orn ψ"
proof -
  have "i. w n φ  suffix i w n φ" and "i. w n ψ  suffix i w n ψ"
    using assms pure_universal_suffix_closed prefix_suffix by metis+
  thus ?thesis
    by force
qed

theorem pure_eventual_strong_release_simp:
  assumes "pure_eventual φ" and "pure_eventual ψ"
  shows "w n φ Mn ψ  w n φ andn ψ"
proof -
  have "i. suffix i w n φ  w n φ" and "i. suffix i w n ψ  w n ψ"
    using assms pure_eventual_left_append prefix_suffix by metis+
  thus ?thesis
    by force
qed


theorem suspendable_formula_simp:
  assumes "suspendable ξ"
  shows "w n Xn ξ  w n ξ" (is ?t1)
    and "w n φ Un ξ  w n ξ" (is ?t2)
    and "w n φ Rn ξ  w n ξ" (is ?t3)
proof -
  have "i. suffix i w n ξ  w n ξ"
    using suspendable_prefix_invariant[OF assms] prefix_suffix by metis
  thus ?t1 ?t2 ?t3
    by force+
qed

theorem suspendable_formula_simp2:
  assumes "suspendable φ" and "suspendable ψ"
  shows "w n φ Wn ψ  w n φ orn ψ" (is ?t1)
    and "w n φ Mn ψ  w n φ andn ψ" (is ?t2)
proof -
  have "i. suffix i w n φ  w n φ" and "i. suffix i w n ψ  w n ψ"
    using assms suspendable_prefix_invariant prefix_suffix by metis+
  thus ?t1 ?t2
    by force+
qed

fun rewrite_modal :: "'a ltln  'a ltln"
where
  "rewrite_modal truen = truen"
| "rewrite_modal falsen = falsen"
| "rewrite_modal (φ andn ψ) = (rewrite_modal φ andn rewrite_modal ψ)"
| "rewrite_modal (φ orn ψ) = (rewrite_modal φ orn rewrite_modal ψ)"
| "rewrite_modal (φ Un ψ) = (if pure_eventual ψ  suspendable ψ then rewrite_modal ψ else (rewrite_modal φ Un rewrite_modal ψ))"
| "rewrite_modal (φ Rn ψ) = (if pure_universal ψ  suspendable ψ then rewrite_modal ψ else (rewrite_modal φ Rn rewrite_modal ψ))"
| "rewrite_modal (φ Wn ψ) = (if pure_universal φ  pure_universal ψ  suspendable φ  suspendable ψ then (rewrite_modal φ orn rewrite_modal ψ) else (rewrite_modal φ Wn rewrite_modal ψ))"
| "rewrite_modal (φ Mn ψ) = (if pure_eventual φ  pure_eventual ψ  suspendable φ  suspendable ψ then (rewrite_modal φ andn rewrite_modal ψ) else (rewrite_modal φ Mn rewrite_modal ψ))"
| "rewrite_modal (Xn φ) = (if suspendable φ then rewrite_modal φ else Xn (rewrite_modal φ))"
| "rewrite_modal φ = φ"

lemma rewrite_modal_sound [simp]:
  "w n rewrite_modal φ  w n φ"
proof (induction φ arbitrary: w)
  case (Until_ltln φ ψ)
    thus ?case
      apply (cases "pure_eventual ψ  suspendable ψ")
      apply (insert pure_eventual_until_simp[of ψ] suspendable_formula_simp[of ψ])
      apply fastforce+
      done
next
  case (Release_ltln φ ψ)
    thus ?case
      apply (cases "pure_universal ψ  suspendable ψ")
      apply (insert pure_universal_release_simp[of ψ] suspendable_formula_simp[of ψ])
      apply fastforce+
      done
next
  case (WeakUntil_ltln φ ψ)
    thus ?case
      apply (cases "pure_universal φ  pure_universal ψ  suspendable φ  suspendable ψ")
      apply (insert pure_universal_weak_until_simp[of φ ψ] suspendable_formula_simp2[of φ ψ])
      apply fastforce+
      done
next
  case (StrongRelease_ltln φ ψ)
    thus ?case
      apply (cases "pure_eventual φ  pure_eventual ψ  suspendable φ  suspendable ψ")
      apply (insert pure_eventual_strong_release_simp[of φ ψ] suspendable_formula_simp2[of φ ψ])
      apply fastforce+
      done
next
  case (Next_ltln φ)
    thus ?case
      apply (cases "suspendable φ")
      apply (insert suspendable_formula_simp[of φ])
      apply fastforce+
      done
qed auto

lemma rewrite_modal_size:
  "size (rewrite_modal φ)  size φ"
  by (induction φ) auto

subsection ‹Syntactical Implication Based Simplification›

inductive syntactical_implies :: "'a ltln  'a ltln  bool" ("_ s _" [80, 80])
where
  "_ s truen"
| "falsen s _"
| "φ = φ  φ s φ"

| "φ s χ  (φ andn ψ) s χ"
| "ψ s χ  (φ andn ψ) s χ"
| "φ s ψ  φ s χ  φ s (ψ andn χ)"

| "φ s ψ  φ s (ψ orn χ)"
| "φ s χ  φ s (ψ orn χ)"
| "φ s χ  ψ s χ  (φ orn ψ) s χ"

| "φ s χ  φ s (ψ Un χ)"
| "φ s χ  ψ s χ  (φ Un ψ) s χ"
| "φ s χ  ψ s ν  (φ Un ψ) s (χ Un ν)"

| "χ s φ  (ψ Rn χ) s φ"
| "χ s φ  χ s ψ  χ s (φ Rn ψ)"
| "φ s χ  ψ s ν  (φ Rn ψ) s (χ Rn ν)"

| "(falsen Rn φ) s ψ  (falsen Rn φ) s Xn ψ"
| "φ s (truen Un ψ)  (Xn φ) s (truen Un ψ)"
| "φ s ψ  (Xn φ) s (Xn ψ)"

lemma syntactical_implies_correct:
  "φ s ψ  w n φ  w n ψ"
  by (induction arbitrary: w rule: syntactical_implies.induct; auto; force)

fun rewrite_syn_imp
where
  "rewrite_syn_imp (φ andn ψ) = (
    if φ s ψ then
      rewrite_syn_imp φ
    else if ψ s φ then
      rewrite_syn_imp ψ
    else if φ s (notn ψ)  ψ s (notn φ) then
      falsen
    else
      mk_and (rewrite_syn_imp φ) (rewrite_syn_imp ψ))"
| "rewrite_syn_imp (φ orn ψ) = (
    if φ s ψ then
      rewrite_syn_imp ψ
    else if ψ s φ then
      rewrite_syn_imp φ
    else if (notn φ) s ψ  (notn ψ) s φ then
      truen
    else
      mk_or (rewrite_syn_imp φ) (rewrite_syn_imp ψ))"
| "rewrite_syn_imp (φ Un ψ) = (
    if φ s ψ then
      rewrite_syn_imp ψ
    else if (notn φ) s ψ then
      mk_finally (rewrite_syn_imp ψ)
    else
      mk_until (rewrite_syn_imp φ) (rewrite_syn_imp ψ))"
| "rewrite_syn_imp (φ Rn ψ) = (
    if ψ s φ then
      rewrite_syn_imp ψ
    else if ψ s (notn φ) then
      mk_globally (rewrite_syn_imp ψ)
    else
      mk_release (rewrite_syn_imp φ) (rewrite_syn_imp ψ))"
| "rewrite_syn_imp (Xn φ) = mk_next (rewrite_syn_imp φ)"
| "rewrite_syn_imp φ = φ"

lemma rewrite_syn_imp_sound:
  "w n rewrite_syn_imp φ  w n φ"
proof (induction φ arbitrary: w)
  case And_ltln
    thus ?case
      by (simp add: Let_def; metis syntactical_implies_correct notn_semantics)
next
  case (Or_ltln φ ψ)
    moreover
    have "(notn φ) s ψ  w. w n φ orn ψ"
      by (auto intro: syntactical_implies_correct[of "notn φ"])
    moreover
    have "(notn ψ) s φ  w. w n φ orn ψ"
      by (auto intro: syntactical_implies_correct[of "notn ψ"])
    ultimately
    show ?case
      by (auto intro: syntactical_implies_correct)
next
  case (Until_ltln φ ψ)
    moreover
    have "φ s ψ  ?case"
      by (force simp add: Until_ltln dest: syntactical_implies_correct)
    moreover
    {
      assume A: "(notn φ) s ψ" and B: "¬ φ s ψ"
      hence [simp]: "rewrite_syn_imp (φ Un ψ) = mk_finally (rewrite_syn_imp ψ)"
        by simp
      {
        assume "i. suffix i w n ψ"
        moreover
        define i where "i  LEAST i. suffix i w n ψ"
        ultimately
        have "j < i. ¬suffix j w n ψ" and "suffix i w n ψ"
          by (blast dest: not_less_Least , metis LeastI i. suffix i w n ψ i_def)
        hence "j < i. suffix j w n φ" and "suffix i w n ψ"
          using syntactical_implies_correct[OF A] by auto
      }
      hence ?case
        by (simp del: rewrite_syn_imp.simps; unfold Until_ltln(2)) blast
    }
    ultimately
    show ?case
      by fastforce
next
  case (Release_ltln φ ψ)
    moreover
    have "ψ s φ  ?case"
      by (force simp add: Release_ltln dest: syntactical_implies_correct)
    moreover
    {
      assume A: "ψ s (notn φ)" and B: "¬ ψ s φ"
      hence [simp]: "rewrite_syn_imp (φ Rn ψ) = mk_globally (rewrite_syn_imp ψ)"
        by simp
      {
        assume "i. ¬suffix i w n ψ"
        moreover
        define i where "i  LEAST i. ¬suffix i w n ψ"
        ultimately
        have "j < i. suffix j w n ψ" and "¬ suffix i w n ψ"
          by (blast dest: not_less_Least , metis LeastI i. ¬suffix i w n ψ i_def)
        hence "j < i. ¬suffix j w n φ" and "¬ suffix i w n ψ"
          using syntactical_implies_correct[OF A] by auto
      }
      hence ?case
        by (simp del: rewrite_syn_imp.simps; unfold Release_ltln(2)) blast
    }
    ultimately
    show ?case
      by fastforce
qed auto

subsection ‹Iterated Rewriting›

fun iterate
where
  "iterate f x 0 = x"
| "iterate f x (Suc n) = (let x' = f x in if x = x' then x else iterate f x' n)"

definition
  "rewrite_iter_fast φ  iterate (rewrite_modal o rewrite_X) φ (size φ)"

definition
  "rewrite_iter_slow φ  iterate (rewrite_syn_imp o rewrite_modal o rewrite_X) φ (size φ)"

text ‹The rewriting functions defined in the previous subsections can be used as-is. However, in the
  most cases one wants to iterate these rules until the formula cannot be simplified further.
  @{const rewrite_iter_fast} pulls X operators up in the syntax tree and the uses the
  "modal" simplification rules. @{const rewrite_iter_slow} additionally tries to simplify the
  formula using syntactic implication checking.›

lemma iterate_sound:
  assumes "φ. w n f φ  w n φ"
  shows "w n iterate f φ n  w n φ"
  by (induction n arbitrary: φ; simp add: assms Let_def)

theorem rewrite_iter_fast_sound [simp]:
  "w n rewrite_iter_fast φ  w n φ"
  using iterate_sound[of _ "rewrite_modal o rewrite_X"]
  unfolding comp_def rewrite_modal_sound rewrite_X_sound rewrite_iter_fast_def
  by blast

theorem rewrite_iter_slow_sound [simp]:
  "w n rewrite_iter_slow φ  w n φ"
  using iterate_sound[of _ "rewrite_syn_imp o rewrite_modal o rewrite_X"]
  unfolding comp_def rewrite_modal_sound rewrite_X_sound rewrite_syn_imp_sound rewrite_iter_slow_def
  by blast

subsection ‹Preservation of atoms›

lemma iterate_atoms:
  assumes
    "φ. atoms_ltln (f φ)  atoms_ltln φ"
  shows
    "atoms_ltln (iterate f φ n)  atoms_ltln φ"
  by (induction n arbitrary: φ) (auto, metis (mono_tags, lifting) assms in_mono)

lemma rewrite_modal_atoms:
  "atoms_ltln (rewrite_modal φ)  atoms_ltln φ"
  by (induction φ) auto

lemma mk_and_atoms:
  "atoms_ltln (mk_and φ ψ)  atoms_ltln φ  atoms_ltln ψ"
  by (auto simp: mk_and_def split: ltln.splits)

lemma mk_or_atoms:
  "atoms_ltln (mk_or φ ψ)  atoms_ltln φ  atoms_ltln ψ"
  by (auto simp: mk_or_def split: ltln.splits)

lemma remove_strong_ops_atoms:
  "atoms_ltln (remove_strong_ops φ)  atoms_ltln φ"
  by (induction φ) auto

lemma remove_weak_ops_atoms:
  "atoms_ltln (remove_weak_ops φ)  atoms_ltln φ"
  by (induction φ) auto

lemma mk_finally_atoms:
  "atoms_ltln (mk_finally φ)  atoms_ltln φ"
  by (auto simp: mk_finally_def split: ltln.splits) (insert remove_strong_ops_atoms, fast+)

lemma mk_globally_atoms:
  "atoms_ltln (mk_globally φ)  atoms_ltln φ"
  by (auto simp: mk_globally_def split: ltln.splits) (insert remove_weak_ops_atoms, fast+)

lemma mk_until_atoms:
  "atoms_ltln (mk_until φ ψ)  atoms_ltln φ  atoms_ltln ψ"
  by (auto simp: mk_until_def split: ltln.splits) (insert mk_finally_atoms, fastforce+)

lemma mk_release_atoms:
  "atoms_ltln (mk_release φ ψ)  atoms_ltln φ  atoms_ltln ψ"
  by (auto simp: mk_release_def split: ltln.splits) (insert mk_globally_atoms, fastforce+)

lemma mk_weak_until_atoms:
  "atoms_ltln (mk_weak_until φ ψ)  atoms_ltln φ  atoms_ltln ψ"
  by (auto simp: mk_weak_until_def split: ltln.splits) (insert mk_globally_atoms, fastforce+)

lemma mk_strong_release_atoms:
  "atoms_ltln (mk_strong_release φ ψ)  atoms_ltln φ  atoms_ltln ψ"
  by (auto simp: mk_strong_release_def split: ltln.splits) (insert mk_finally_atoms, fastforce+)

lemma mk_next_atoms:
  "atoms_ltln (mk_next φ) = atoms_ltln φ"
  by (auto simp: mk_next_def split: ltln.splits)

lemma mk_next_pow_atoms:
  "atoms_ltln (mk_next_pow n φ) = atoms_ltln φ"
  by (induction n) (auto simp: mk_next_pow_def split: ltln.splits)

lemma combine_atoms:
  assumes
    "φ ψ. atoms_ltln (f φ ψ)  atoms_ltln φ  atoms_ltln ψ"
  shows
    "atoms_ltln (fst (combine f x y))  atoms_ltln (fst x)  atoms_ltln (fst y)"
  by (metis assms fst_combine mk_next_pow_atoms prod.collapse)

lemmas combine_mk_atoms =
  combine_atoms[OF mk_and_atoms]
  combine_atoms[OF mk_or_atoms]
  combine_atoms[OF mk_until_atoms]
  combine_atoms[OF mk_release_atoms]
  combine_atoms[OF mk_weak_until_atoms]
  combine_atoms[OF mk_strong_release_atoms]

lemma rewrite_X_enat_atoms:
  "atoms_ltln (fst (rewrite_X_enat φ))  atoms_ltln φ"
  by (induction φ) (simp_all add: case_prod_beta, insert combine_mk_atoms, fast+)

lemma rewrite_X_atoms:
  "atoms_ltln (rewrite_X φ)  atoms_ltln φ"
  by (induction φ) (simp_all add: rewrite_X_def mk_next_pow_atoms case_prod_beta, insert combine_mk_atoms, fast+)

lemma rewrite_syn_imp_atoms:
  "atoms_ltln (rewrite_syn_imp φ)  atoms_ltln φ"
proof (induction φ)
  case (And_ltln φ1 φ2)
  then show ?case
    using mk_and_atoms by simp fast
next
  case (Or_ltln φ1 φ2)
  then show ?case
    using mk_or_atoms by simp fast
next
  case (Next_ltln φ)
  then show ?case
    using mk_next_atoms by simp fast
next
  case (Until_ltln φ1 φ2)
  then show ?case
    using mk_finally_atoms mk_until_atoms by simp fast
next
  case (Release_ltln φ1 φ2)
  then show ?case
    using mk_globally_atoms mk_release_atoms by simp fast
qed simp_all

lemma rewrite_iter_fast_atoms:
  "atoms_ltln (rewrite_iter_fast φ)  atoms_ltln φ"
proof -
  have 1: "φ. atoms_ltln (rewrite_modal (rewrite_X φ))  atoms_ltln φ"
    using rewrite_modal_atoms rewrite_X_atoms by force

  show ?thesis
    by (simp add: rewrite_iter_fast_def 1 iterate_atoms)
qed

lemma rewrite_iter_slow_atoms:
  "atoms_ltln (rewrite_iter_slow φ)  atoms_ltln φ"
proof -
  have 1: "φ. atoms_ltln (rewrite_syn_imp (rewrite_modal (rewrite_X φ)))  atoms_ltln φ"
    using rewrite_syn_imp_atoms rewrite_modal_atoms rewrite_X_atoms by force

  show ?thesis
    by (simp add: rewrite_iter_slow_def 1 iterate_atoms)
qed

subsection ‹Simplifier›

text ‹We now define a convenience wrapper for the rewriting engine›

datatype mode = Nop | Fast | Slow

fun simplify :: "mode  'a ltln  'a ltln"
where
  "simplify Nop = id"
| "simplify Fast = rewrite_iter_fast"
| "simplify Slow = rewrite_iter_slow"

theorem simplify_correct:
  "w n simplify m φ  w n φ"
  by (cases m) simp+

lemma simplify_atoms:
  "atoms_ltln (simplify m φ)  atoms_ltln φ"
  by (cases m) (insert rewrite_iter_fast_atoms rewrite_iter_slow_atoms, fastforce+)

subsection ‹Code Generation›

code_pred syntactical_implies .

export_code simplify checking

lemma "rewrite_iter_fast (Fn (Gn (Xn propn(''a'')))) = (Fn (Gn propn(''a'')))"
  by eval

lemma "rewrite_iter_fast (Xn propn(''a'') Un (Xn npropn(''a''))) = Xn (propn(''a'') Un npropn(''a''))"
  by eval

lemma "rewrite_iter_slow (Xn propn(''a'') Un (Xn npropn(''a''))) = Xn (Fn npropn(''a''))"
  by eval

end