Theory MLTL_Properties

section ‹ Properties of MLTL ›
theory MLTL_Properties

imports MLTL_Encoding

begin

subsection ‹Useful Functions›

text ‹ We use the following function to assume that an MLTL formula is well-defined:
  i.e., that all intervals in the formula satisfy a is less than or equal to b ›
fun intervals_welldef:: "'a mltl  bool"
  where "intervals_welldef Truem = True"
  | "intervals_welldef Falsem = True"
  | "intervals_welldef (Propm (p)) = True"
  | "intervals_welldef (Notm φ) = intervals_welldef φ"
  | "intervals_welldef (φ Andm ψ) = (intervals_welldef φ  intervals_welldef ψ)"
  | "intervals_welldef (φ Orm ψ) = (intervals_welldef φ  intervals_welldef ψ)"
  | "intervals_welldef (Fm [a,b] φ)  = (a  b  intervals_welldef φ)"
  | "intervals_welldef (Gm [a,b] φ)  = (a  b  intervals_welldef φ)"
  | "intervals_welldef (φ Um [a,b] ψ) =
      (a  b  intervals_welldef φ  intervals_welldef ψ)"
  | "intervals_welldef (φ Rm [a,b] ψ) =
      (a  b  intervals_welldef φ  intervals_welldef ψ)"

subsection ‹Semantic Equivalence›
(* φ and ψ are sematically equivalent iff for all traces π, π |= φ ⟷ π |= ψ  *)
definition semantic_equiv:: "'a mltl  'a mltl  bool" ("_ m _" [80, 80] 80)
  where "φ m ψ  (π. π m φ = π m ψ)"

fun depth_mltl:: "'a mltl  nat"
  where "depth_mltl Truem = 0"
  | "depth_mltl Falsem = 0"
  | "depth_mltl Propm (p) = 0"
  | "depth_mltl (Notm φ) = 1 + depth_mltl φ"
  | "depth_mltl (φ Andm ψ) = 1 + max (depth_mltl φ) (depth_mltl ψ)"
  | "depth_mltl (φ Orm ψ) = 1 + max (depth_mltl φ) (depth_mltl ψ)"
  | "depth_mltl (Gm [a,b] φ) = 1 + depth_mltl φ"
  | "depth_mltl (Fm [a,b] φ) = 1 + depth_mltl φ"
  | "depth_mltl (φ Um [a,b] ψ) = 1 + max (depth_mltl φ) (depth_mltl ψ)"
  | "depth_mltl (φ Rm [a,b] ψ) = 1 + max (depth_mltl φ) (depth_mltl ψ)"

fun subformulas:: "'a mltl  'a mltl set"
  where "subformulas Truem = {}"
  | "subformulas Falsem = {}"
  | "subformulas Propm (p) = {}"
  | "subformulas (Notm φ) = {φ}  subformulas φ"
  | "subformulas (φ Andm ψ) = {φ, ψ}  subformulas φ  subformulas ψ"
  | "subformulas (φ Orm ψ) = {φ, ψ}  subformulas φ  subformulas ψ"
  | "subformulas (Gm [a,b] φ) = {φ}  subformulas φ"
  | "subformulas (Fm [a,b] φ) = {φ}  subformulas φ"
  | "subformulas (φ Um [a,b] ψ) = {φ, ψ}  subformulas φ  subformulas ψ"
  | "subformulas (φ Rm [a,b] ψ) = {φ, ψ}  subformulas φ  subformulas ψ"

subsection ‹Basic Properties›

lemma future_or_distribute:
  shows "Fm [a,b] (φ1 Orm φ2) m (Fm [a,b] φ1) Orm (Fm [a,b] φ2)"
  unfolding semantic_equiv_def by auto

lemma global_and_distribute:
  shows "Gm [a,b] (φ1 Andm φ2) m (Gm [a,b] φ1) Andm (Gm [a,b] φ2)"
  unfolding semantic_equiv_def
  unfolding semantics_mltl.simps by auto

lemma not_not_equiv:
  shows "φ m (Notm (Notm φ))"
  unfolding semantic_equiv_def by simp

lemma demorgan_and_or:
  shows "Notm (φ Andm ψ) m (Notm φ) Orm (Notm ψ)"
  unfolding semantic_equiv_def by simp

lemma demorgan_or_and:
  shows "semantic_equiv (Not_mltl (φ Orm ψ))
         (And_mltl (Notm φ) (Not_mltl ψ))"
  unfolding semantic_equiv_def by simp

lemma future_as_until:
  fixes a b::"nat"
  assumes "a  b"
  shows "(Fm [a,b] φ) m (Truem Um [a,b] φ)"
  unfolding semantic_equiv_def by auto

lemma globally_as_release:
  fixes a b::"nat"
  assumes "a  b"
  shows "(Gm [a,b] φ) m (Falsem Rm [a,b] φ)"
  unfolding semantic_equiv_def by auto

lemma until_or_distribute:
  fixes a b ::"nat"
  assumes "a  b"
  shows "φ Um [a,b] (α Orm β) m
         (φ Um [a,b] α) Orm (φ Um [a,b] β)"
  using assms semantics_mltl.simps unfolding semantic_equiv_def
  by auto

lemma until_and_distribute:
  fixes a b ::"nat"
  assumes "a  b"
  shows "(α Andm β) Um [a,b] φ m
         (α Um [a,b] φ) Andm (β Um [a,b] φ)"
  using assms unfolding semantic_equiv_def semantics_mltl.simps
  by (smt (verit) linorder_less_linear order_less_trans)

lemma release_or_distribute:
  fixes a b ::"nat"
  assumes "a  b"
  shows "(α Orm β) Rm [a,b] φ m
         (α Rm [a,b] φ) Orm (β Rm [a,b] φ)"
  using assms unfolding semantic_equiv_def semantics_mltl.simps
  by auto

lemma different_next_operators:
  shows "¬(Gm [1,1] φ m Fm [1,1] φ)"
  unfolding semantic_equiv_def semantics_mltl.simps
  by (metis le_numeral_extra(4) linordered_nonzero_semiring_class.zero_le_one list.size(3) not_one_less_zero)

subsection ‹Duality Properties›

lemma globally_future_dual:
  fixes a b::"nat"
  assumes "a  b"
  shows "(Gm [a,b] φ) m Notm (Fm [a,b] (Notm φ))"
  using assms unfolding semantic_equiv_def by auto

lemma future_globally_dual:
  fixes a b::"nat"
  assumes "a  b"
  shows "(Fm [a,b] φ) m Notm (Gm [a,b] (Notm φ))"
  using assms unfolding semantic_equiv_def by auto

text ‹ Proof altered from source material in the last case. ›
lemma release_until_dual1:
  fixes a b::"nat"
  assumes "π m (φ Rm [a,b] ψ)"
  shows "π m (Notm ((Notm φ) Um [a,b] (Notm ψ)))"
proof -
  have relase_unfold: "(a  b  (length π  a  (i::nat. (i  a  i  b)  ((semantics_mltl (drop i π) ψ)  (j. j  a  j  b-1  semantics_mltl (drop j π) φ  (k. a  k  k  j  semantics_mltl (drop k π) ψ))))))"
    using assms by auto
  {assume *: "length π  a"
    then have ?thesis
      by (simp add: assms)
  } moreover {assume **: "(i. (a  i  i  b)  semantics_mltl (drop i π) ψ)"
    then have "length π  a  (s. a  s  s  b  (semantics_mltl (drop s π) ψ  (t. t a  t  s-1  semantics_mltl (drop t π) φ)))"
      by auto
    then have ?thesis using assms
      using "**" linorder_not_less by auto
  } moreover {assume *: "length π > a  (i. (a  i  i  b)  ¬ (semantics_mltl (drop i π) ψ))"
    then obtain i where i_prop: "(a  i  i  b)" "¬ (semantics_mltl (drop i π) ψ)"
      by blast
    have "(i. (a  i  i  b)  (semantics_mltl (drop i π) ψ))
        semantics_mltl (drop i π) ψ"
      using i_prop(1) by blast
    then have h1: "¬ (i. (a  i  i  b) 
          semantics_mltl (drop i π) ψ)"
      using i_prop by blast
    have "(i. a  i  i  b 
          semantics_mltl (drop i π) ψ) 
          (ja. j  b - 1 
                  semantics_mltl (drop j π) φ 
                  (k. a  k  k  j 
                       semantics_mltl (drop k π) ψ))"
      using * relase_unfold by auto
    then have "(ja. j  b - 1 
                  semantics_mltl (drop j π) φ 
                  (k. a  k  k  j 
                       semantics_mltl (drop k π) ψ))"
      using * h1 by blast
   (*Deviates from proof after this point*)
   then have "j. a  j  j  b-1  (semantics_mltl (drop j π) φ  (k. a  k  k  j   semantics_mltl (drop k π) ψ))"
     using relase_unfold
     by metis
  (* Sledgehammer finds this *)
   then have "i. a  i  i  b 
        (semantics_mltl (drop i π) ψ 
        (j. a  j  j < i  semantics_mltl (drop j π) φ))"
     by (metis linorder_not_less)
   then have "i. (i  a  i  b)   (semantics_mltl (drop i π) ψ 
        ¬ (j. a  j  j < i  ¬ semantics_mltl (drop j π) φ))"
     by blast
   then have "i. (i  a  i  b)  ¬ (¬ semantics_mltl (drop i π) ψ 
        (j. a  j  j < i  ¬ semantics_mltl (drop j π) φ))"
     by blast
   then have "¬ ((i::nat. (i  a  i  b)  (¬ (semantics_mltl (drop i π) ψ)  (j. j  a  j<i  ¬ (semantics_mltl (drop j π ) φ)))))"
     by blast
   then have "¬ (a  b  length π > a  (i::nat. (i  a  i  b)  (¬ (semantics_mltl (drop i π) ψ)  (j. j  a  j<i  ¬ (semantics_mltl (drop j π ) φ)))))"
     using * by blast
   then have  ?thesis
     by auto
 }
  ultimately show ?thesis
    using linorder_not_less
    by (smt (verit) relase_unfold semantics_mltl.simps(4) semantics_mltl.simps(9))
qed

lemma release_until_dual2:
  fixes a b::"nat"
  assumes a_leq_b: "a  b"
  assumes "π m (Notm ((Notm φ) Um [a,b] (Notm ψ)))"
  shows "semantics_mltl π (φ Rm [a,b] ψ)"
proof -
  have unfold_not_until_not: " ¬ (a  b  length π > a  (i::nat. (i  a  i  b)  (¬ (semantics_mltl (drop i π) ψ)  (j. j  a  j<i  ¬ (semantics_mltl (drop j π ) φ)))))"
   using assms by auto
  have not_until_not_unfold: "(a  b  a < length π)  (π m (Notm ((Notm φ) Um [a,b] (Notm ψ))) 
    (i. a  i  i  b 
        semantics_mltl (drop i π) ψ 
        (j. a  j  j < i  semantics_mltl (drop j π) φ)))"
    by auto
  {assume *: "length π  a"
   then have ?thesis
     using assms semantics_mltl.simps(10)
     by blast
 } moreover {assume *: "s. (a  s  s  b)  semantics_mltl (drop s π) ψ"
   then have ?thesis
     by (simp add: assms(1))
 } moreover {assume *: "(a  b  a < length π)  (s. (a  s  s  b)  ¬ (semantics_mltl (drop s π) ψ))"
   then have not_until_not: "(i. a  i  i  b 
        semantics_mltl (drop i π) ψ 
        (j. a  j  j < i  semantics_mltl (drop j π) φ))"
     using not_until_not_unfold assms
     by blast
   have least_prop: "(s. (a  s  s  b)  f s π ψ 
        (k. a  k  k < s  ¬ (f k π ψ))
        )" if f_prop: "(s. (a  s  s  b)  f s π ψ)" for f::"nat  'a set list  'a mltl  bool"
   proof -
     have "q. q = (LEAST p. (a  p  p  b)  f p π ψ)"
       by simp
     then obtain q where q_prop: "q = (LEAST p. (a  p  p  b)  f p π ψ)"
       by auto
     then have least1: "(a  q  q  b)  f q π ψ"
       using f_prop
       by (smt (verit) LeastI)
     have least2: "(k. a  k  k < q  ¬ (f k π ψ))"
       using q_prop
       using least1 not_less_Least by fastforce
     show ?thesis using least1 least2 by blast
   qed
   have "i1. a  i1  i1  b  ¬ (semantics_mltl (drop i1 π) ψ)  (k. (a  k  k  i1-1)  (semantics_mltl (drop k π) ψ))"
     using * least_prop[of "λ s π ψ. ¬ (semantics_mltl (drop s π) ψ)"]
     by (metis add_diff_inverse_nat gr_implies_not0 le_imp_less_Suc less_one plus_1_eq_Suc unfold_not_until_not)
   then obtain i1 where i1_prop: "a  i1  i1  b  ¬ (semantics_mltl (drop i1 π) ψ)  (k. (a  k  k  i1-1)  (semantics_mltl (drop k π) ψ))"
     by auto

   have "semantics_mltl (drop i1 π) ψ 
        (ja. j < i1  semantics_mltl (drop j π) φ)"
     using not_until_not i1_prop by blast
   then have "(semantics_mltl (drop i1 π) ψ)  (t. a  t  t  i1-1  (semantics_mltl (drop t π) φ))"
     using * i1_prop
     using not_less_eq by fastforce
   then have "(t. a  t  t  i1-1  (semantics_mltl (drop t π) φ))"
     by (smt (verit, ccfv_threshold) "*" i1_prop less_imp_le_nat nle_le not_until_not order_le_less_trans)
   then obtain t where t_prop: "a  t  t  i1-1  semantics_mltl (drop t π) φ"
     by auto
   have "k. a  k  k  i1-1  (semantics_mltl (drop k π) ψ )"
     using i1_prop by blast
   then have "k. a  k  k  t  (semantics_mltl (drop k π) ψ )"
     using t_prop by auto
   then have "j. a  j  j  (b-1)  (semantics_mltl (drop j π) φ)
       (k. a  k k  j  (semantics_mltl (drop k π) ψ))"
     by (meson diff_le_mono i1_prop le_trans t_prop)
   then have ?thesis
     using semantics_mltl.simps(10) a_leq_b
     by blast
 }
  ultimately show  ?thesis
    using assms(1) linorder_not_less by blast
qed

lemma release_until_dual:
  fixes a b::"nat"
  assumes a_leq_b: "a  b"
  shows "(φ Rm [a,b] ψ) m (Notm ((Notm φ) Um [a,b] (Notm ψ)))"
  using release_until_dual1 release_until_dual2
  using assms unfolding semantic_equiv_def by metis

lemma until_release_dual:
  fixes a b::"nat"
  assumes a_leq_b: "a  b"
  shows "(φ Um [a,b] ψ) m (Notm ((Notm φ) Rm [a,b] (Notm ψ)))"
proof-
  have release_until_dual_alternate: "(Notm (φ Rm [a,b] ψ)) m ((Notm φ) Um [a,b] (Notm ψ))"
    using release_until_dual
    using assms semantics_mltl.simps(4) unfolding semantic_equiv_def by metis
  have not_not_until: "(φ Um [a,b] ψ) m ((Notm (Notm φ)) Um [a,b] (Notm (Notm ψ)))"
    using assms not_not_equiv using semantics_mltl.simps(9)
    by (simp add: semantic_equiv_def)
  have "(Notm ((Notm φ) Rm [a,b] (Notm ψ))) m ((Notm (Notm φ)) Um [a,b] (Notm (Notm ψ)))"
    using assms release_until_dual semantics_mltl.simps(4) unfolding semantic_equiv_def by metis
  then show ?thesis using not_not_until
    unfolding semantic_equiv_def
    by blast
qed

subsection "Additional Basic Properties"
lemma release_and_distribute:
  fixes a b ::"nat"
  assumes "a  b"
  shows "(φ Rm [a,b] (α Andm β)) m
         ((φ Rm [a,b] α) Andm (φ Rm [a,b] β))"
proof-
  let ?lhs = "(φ Rm [a,b] (α Andm β))"
  let ?rhs = "((φ Rm [a,b] α) Andm (φ Rm [a,b] β))"
  let ?neg = "Notm ((Notm φ) Um [a,b] (Notm (α Andm β)))"
  have eq_lhs: "semantic_equiv ?lhs ?neg"
    using until_release_dual release_until_dual until_or_distribute
    by (smt (verit) assms release_until_dual1 semantic_equiv_def)
  let ?neg1 = "Notm ((Notm φ) Um [a,b] ((Notm α) Orm (Notm β)))"
  have eq_neg1: "semantic_equiv ?neg ?neg1"
    unfolding semantic_equiv_def semantic_equiv_def by auto
  let ?neg2 = "Notm (((Notm φ) Um [a,b] (Not_mltl α)) Orm ((Notm φ) Um [a,b] (Not_mltl β)))"
  have eq_neg2: "semantic_equiv ?neg1 ?neg2"
    unfolding semantic_equiv_def by auto
  let ?neg3 = "((φ Rm [a,b] α) Andm (φ Rm [a,b] β))"
  have eq_neg3: "semantic_equiv ?neg2 ?neg3"
    unfolding semantic_equiv_def using assms
    by (metis release_until_dual1 release_until_dual2 semantics_mltl.simps(4) semantics_mltl.simps(5) semantics_mltl.simps(6))
  have eq_rhs: "semantic_equiv ?rhs ?neg"
    using eq_neg1 eq_neg2 eq_neg3
    by (meson semantic_equiv_def)
  show ?thesis using eq_rhs eq_lhs unfolding semantic_equiv_def by meson
qed

subsection ‹NNF Transformation and Properties ›
fun convert_nnf:: "'a mltl  'a mltl"
  where "convert_nnf Truem = Truem"
  | "convert_nnf Falsem = Falsem"
  | "convert_nnf Propm (p) = Propm (p)"
  | "convert_nnf (φ Andm ψ) = ((convert_nnf φ) Andm (convert_nnf ψ))"
  | "convert_nnf (φ Orm ψ) = ((convert_nnf φ) Orm (convert_nnf ψ))"
  | "convert_nnf (Fm [a,b] φ) = (Fm [a,b] (convert_nnf φ))"
  | "convert_nnf (Gm [a,b] φ) = (Gm [a,b] (convert_nnf φ))"
  | "convert_nnf (φ Um [a,b] ψ) = ((convert_nnf φ) Um [a,b] (convert_nnf ψ))"
  | "convert_nnf (φ Rm [a,b] ψ) = ((convert_nnf φ) Rm [a,b] (convert_nnf ψ))"
  (* Rewriting with logical duals *)
  | "convert_nnf (Notm Truem) = Falsem"
  | "convert_nnf (Notm Falsem) = Truem"
  | "convert_nnf (Notm Propm (p)) = (Notm Propm (p))"
  | "convert_nnf (Notm (Notm φ)) = convert_nnf φ"
  | "convert_nnf (Notm (φ Andm ψ)) = ((convert_nnf (Notm φ)) Orm (convert_nnf (Notm ψ)))"
  | "convert_nnf (Notm (φ Orm ψ)) = ((convert_nnf (Notm φ)) Andm (convert_nnf (Notm ψ)))"
  | "convert_nnf (Notm (Fm [a,b] φ)) = (Gm [a,b] (convert_nnf (Notm φ)))"
  | "convert_nnf (Notm (Gm [a,b] φ)) = (Fm [a,b] (convert_nnf (Notm φ)))"
  | "convert_nnf (Notm (φ Um [a,b] ψ)) = ((convert_nnf (Notm φ)) Rm [a,b] (convert_nnf (Notm ψ)))"
  | "convert_nnf (Notm (φ Rm [a,b] ψ)) = ((convert_nnf (Notm φ)) Um [a,b] (convert_nnf (Notm ψ)))"


lemma convert_nnf_preserves_semantics:
  assumes "intervals_welldef φ"
  shows "(π m (convert_nnf φ))  (π m φ)"
  using assms
proof (induct "depth_mltl φ" arbitrary:φ π rule:less_induct)
  case less
  then show ?case
  proof (cases φ)
    case True_mltl
    then show ?thesis by simp
  next
    case False_mltl
    then show ?thesis by simp
  next
    case (Prop_mltl x)
    then show ?thesis by simp
  next
    case (Not_mltl φ1)
    then have phi_is: "φ = Notm φ1"
      by auto
    then show ?thesis
    proof (cases φ1)
      case True_mltl
      then show ?thesis using Not_mltl
        by simp
    next
      case False_mltl
      then show ?thesis using Not_mltl
        by simp
    next
      case (Prop_mltl p)
      then show ?thesis using Not_mltl
        by simp
    next
      case (Not_mltl φ2)
      then show ?thesis using phi_is less
        by auto
    next
      case (And_mltl φ2 φ3)
      then show ?thesis using phi_is less
        by auto
    next
      case (Or_mltl φ2 φ3)
      then show ?thesis using phi_is less
        by auto
    next
      case (Future_mltl a b φ2)
      then have *: "a  b" using less(2)
        phi_is by simp
      have "semantics_mltl π (convert_nnf φ) = semantics_mltl π (Global_mltl a b (convert_nnf (Notm φ2)))"
        using Future_mltl phi_is by simp
      then have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a  b  (length π  a  (i::nat. (i  a  i  b)  semantics_mltl (drop i π) (convert_nnf (Notm φ2)))))"
        by auto
      have "intervals_welldef (Notm φ2)"
        using less(2) Future_mltl phi_is by simp
      then have "semantics_mltl (drop i π) (convert_nnf (Notm φ2)) =  semantics_mltl (drop i π) (Notm φ2)" for i
        using less(1)[of "Notm φ2" "(drop i π)"] phi_is Future_mltl
        by auto
      then have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (a  b  (length π  a  (i::nat. (i  a  i  b)  semantics_mltl (drop i π) (Notm φ2))))"
        using semantics_unfold by auto
      have "semantics_mltl π φ = (¬ (semantics_mltl π (Future_mltl a b φ2)))"
        using phi_is Future_mltl by simp
      then show ?thesis using semantics_unfold1 *
        by auto
    next
      case (Global_mltl a b φ2)
      then have *: "a  b" using less(2)
        phi_is by simp
      have "semantics_mltl π (convert_nnf φ) = semantics_mltl π (Future_mltl a b (convert_nnf (Notm φ2)))"
        using Global_mltl phi_is by simp
      then have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a  b  length π > a  (i::nat. (i  a  i  b)  semantics_mltl (drop i π) (convert_nnf (Notm φ2))))"
        by auto
      have "intervals_welldef (Notm φ2)"
        using less(2) Global_mltl phi_is by simp
      then have "semantics_mltl (drop i π) (convert_nnf (Notm φ2)) =  semantics_mltl (drop i π) (Notm φ2)" for i
        using less(1)[of "Notm φ2" "(drop i π)"] phi_is Global_mltl
        by auto
      then have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (a  b  length π > a  (i::nat. (i  a  i  b)  semantics_mltl (drop i π) (Notm φ2)))"
        using semantics_unfold by auto
       have "semantics_mltl π φ = (¬ (semantics_mltl π (Global_mltl a b φ2)))"
         using phi_is Global_mltl by simp
       then show ?thesis using semantics_unfold1 *
         by auto
    next
      case (Until_mltl φ2 a b φ3)
      then have *: "a  b" using less(2)
        phi_is by simp
      have "semantics_mltl π (convert_nnf φ) = semantics_mltl π (Release_mltl (convert_nnf (Notm φ2)) a b (convert_nnf (Notm φ3)))"
        using Until_mltl phi_is by simp
      then have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a  b  (length π  a  (i::nat. (i  a  i  b)  ((semantics_mltl (drop i π) (convert_nnf (Notm φ3)))))  (j. j  a  j  b-1  semantics_mltl (drop j π) (convert_nnf (Notm φ2))  (k. a  k  k  j  semantics_mltl (drop k π) (convert_nnf (Notm φ3))))))"
        by auto
      have phi3_ind_h: "semantics_mltl (drop i π) (convert_nnf (Notm φ3)) = semantics_mltl (drop i π) (Notm φ3)" for i
        using less(1)[of "Notm φ3" "(drop i π)"] phi_is Until_mltl
        using less.prems by force
      have phi2_ind_h: "semantics_mltl (drop i π) (convert_nnf (Notm φ2)) = semantics_mltl (drop i π) (Notm φ2)" for i
        using less(1)[of "Notm φ2" "(drop i π)"] phi_is Until_mltl
        using less.prems by force
      have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (length π  a  (i::nat. (i  a  i  b)  ((semantics_mltl (drop i π) (Notm φ3))))  (j. j  a  j  b-1  semantics_mltl (drop j π)  (Notm φ2)  (k. a  k  k  j  semantics_mltl (drop k π) (Notm φ3))))"
        using * phi3_ind_h phi2_ind_h semantics_unfold by auto
      have "semantics_mltl π φ = semantics_mltl π (Release_mltl (Notm φ2) a b (Notm φ3))"
        using Until_mltl phi_is until_release_dual[OF *]
        using semantics_mltl.simps(4)
        using semantic_equiv_def by blast
       then show ?thesis using semantics_unfold1 *
          by auto
    next
      case (Release_mltl φ2 a b φ3)
       then have *: "a  b" using less(2)
        phi_is by simp
      have "semantics_mltl π (convert_nnf φ) = semantics_mltl π (Until_mltl (convert_nnf (Notm φ2)) a b (convert_nnf (Notm φ3)))"
        using Release_mltl phi_is by simp
      then have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a  b  length π > a  (i::nat. (i  a  i  b)  (semantics_mltl (drop i π)  (convert_nnf (Notm φ3))  (j. j  a  j<i  semantics_mltl (drop j π )  (convert_nnf (Notm φ2))))))"
        by auto
      have phi3_ind_h: "semantics_mltl (drop i π) (convert_nnf (Notm φ3)) = semantics_mltl (drop i π) (Notm φ3)" for i
        using less(1)[of "Notm φ3" "(drop i π)"] phi_is Release_mltl
        using less.prems by force
      have phi2_ind_h: "semantics_mltl (drop i π) (convert_nnf (Notm φ2)) = semantics_mltl (drop i π) (Notm φ2)" for i
        using less(1)[of "Notm φ2" "(drop i π)"] phi_is Release_mltl
        using less.prems by force
      have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (length π > a  (i::nat. (i  a  i  b)  (semantics_mltl (drop i π) (Notm φ3)  (j. j  a  j<i  semantics_mltl (drop j π) (Notm φ2)))))"
        using * phi3_ind_h phi2_ind_h semantics_unfold by auto
      have "semantics_mltl π φ = semantics_mltl π (Until_mltl (Notm φ2) a b (Notm φ3))"
        using Release_mltl phi_is release_until_dual[OF *]
        using semantics_mltl.simps(4) unfolding semantic_equiv_def by metis
       then show ?thesis using semantics_unfold1 *
          by auto
    qed
  next
    case (And_mltl φ1 φ2)
    then show ?thesis using less by simp
  next
    case (Or_mltl φ1 φ2)
    then show ?thesis using less by simp
  next
    case (Future_mltl a b φ1)
    then have "intervals_welldef φ1"
      using less(2) by simp
    then have ind_h: "semantics_mltl (drop i π) (convert_nnf φ1) = semantics_mltl (drop i π)  φ1" for i
      using Future_mltl less(1)[of φ1 "(drop i π)"]
      by auto
    have unfold_future: "semantics_mltl π (convert_nnf (Future_mltl a b φ1)) = semantics_mltl π (Future_mltl a b (convert_nnf φ1))"
      by simp
    moreover then have unfold_future_semantics: "... = (a  b  length π > a  (i::nat. (i  a  i  b)  semantics_mltl (drop i π) (convert_nnf φ1)))"
      by simp
    moreover then have "... = (a  b  length π > a  (i::nat. (i  a  i  b)  semantics_mltl (drop i π) φ1))"
      using ind_h
      by auto
    ultimately show ?thesis using Future_mltl
      by simp
  next
    case (Global_mltl a b φ1)
    then have "intervals_welldef φ1"
      using less(2) by simp
    then have ind_h: "semantics_mltl (drop i π) (convert_nnf φ1) = semantics_mltl (drop i π)  φ1" for i
      using Global_mltl less(1)[of φ1 "(drop i π)"]
      by auto
    have unfold_future: "semantics_mltl π (convert_nnf (Global_mltl a b φ1)) = semantics_mltl π (Global_mltl a b (convert_nnf φ1))"
      by simp
    moreover then have unfold_future_semantics: "... = (a  b  (length π  a  (i::nat. (i  a  i  b)  semantics_mltl (drop i π) (convert_nnf φ1))))"
      by simp
    moreover then have "... = (a  b  (length π  a  (i::nat. (i  a  i  b)  semantics_mltl (drop i π) φ1)))"
      using ind_h
      by auto
    ultimately show ?thesis using Global_mltl
      by simp
  next
    case (Until_mltl φ1 a b φ2)
    then have *: "a  b" using less(2)
        Until_mltl by simp
    have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a  b  length π > a  (i::nat. (i  a  i  b)  (semantics_mltl (drop i π) (convert_nnf φ2)  (j. j  a  j<i  semantics_mltl (drop j π ) (convert_nnf φ1)))))"
        using Until_mltl by auto
      have phi3_ind_h: "semantics_mltl (drop i π) (convert_nnf φ1) = semantics_mltl (drop i π) φ1" for i
        using less(1)[of φ1 "(drop i π)"] Until_mltl less.prems
        by force
      have phi2_ind_h: "semantics_mltl (drop i π) (convert_nnf φ2) = semantics_mltl (drop i π) φ2" for i
        using less(1)[of φ2 "(drop i π)"] Until_mltl less.prems
        by force
      have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (length π > a  (i::nat. (i  a  i  b)  (semantics_mltl (drop i π) φ2  (j. j  a  j<i  semantics_mltl (drop j π ) φ1))))"
        using * phi3_ind_h phi2_ind_h semantics_unfold
        by auto
      then show ?thesis using semantics_unfold1 * Until_mltl
        by auto
  next
    case (Release_mltl φ1 a b φ2)
    then have *: "a  b" using less(2)
       Release_mltl by simp
    have semantics_unfold: "semantics_mltl π (convert_nnf φ) = (a  b  (length π  a  (i::nat. (i  a  i  b)  ((semantics_mltl (drop i π) (convert_nnf φ2))))  (j. j  a  j  b-1  semantics_mltl (drop j π) (convert_nnf φ1)  (k. a  k  k  j  semantics_mltl (drop k π) (convert_nnf φ2)))))"
       using Release_mltl by auto
    have phi3_ind_h: "semantics_mltl (drop i π) (convert_nnf φ1) = semantics_mltl (drop i π) φ1" for i
       using less(1)[of φ1 "(drop i π)"] Release_mltl less.prems
       by force
    have phi2_ind_h: "semantics_mltl (drop i π) (convert_nnf φ2) = semantics_mltl (drop i π) φ2" for i
       using less(1)[of φ2 "(drop i π)"] Release_mltl less.prems
       by force
    have semantics_unfold1: "semantics_mltl π (convert_nnf φ) = (length π  a  (i::nat. (i  a  i  b)  ((semantics_mltl (drop i π) φ2)))  (j. j  a  j  b-1  semantics_mltl (drop j π) φ1  (k. a  k  k  j  semantics_mltl (drop k π) φ2)))"
       using * phi3_ind_h phi2_ind_h semantics_unfold
       by auto
    then show ?thesis using semantics_unfold1 * Release_mltl
       by auto
  qed
qed

lemma convert_nnf_form_Not_Implies_Prop:
  assumes "Notm F = convert_nnf init_F"
  shows "p. F = Propm (p)"
  using assms
proof (induct "depth_mltl init_F" arbitrary: init_F rule: less_induct)
  case less
  then have ind_h1: "G. depth_mltl G < depth_mltl init_F 
    Not_mltl F = convert_nnf G  p. F = Prop_mltl p"
    by auto
  have not: "Not_mltl F = convert_nnf init_F" using less
    by auto
  then show ?case proof (cases init_F)
    case True_mltl
    then show ?thesis using ind_h1 not by auto
  next
    case False_mltl
    then show ?thesis using ind_h1 not by auto
  next
    case (Prop_mltl p)
    then show ?thesis using ind_h1 not by auto
  next
    case (Not_mltl φ)
    then have init_F_is: "init_F = Notm φ"
      by auto
    then show ?thesis  proof (cases φ)
      case True_mltl
      then show ?thesis using ind_h1 not init_F_is by auto
    next
      case False_mltl
      then show ?thesis using ind_h1 not init_F_is by auto
    next
      case (Prop_mltl p)
      then show ?thesis using ind_h1 not init_F_is by auto
    next
      case (Not_mltl φ)
      then have not_convert: "Not_mltl F = convert_nnf φ" using not init_F_is
        by auto
      have depth: "depth_mltl φ < depth_mltl init_F"
        using Not_mltl init_F_is by auto
      then show ?thesis using ind_h1[OF depth not_convert] by auto
    next
      case (And_mltl φ ψ)
      then show ?thesis using ind_h1 not init_F_is by auto
    next
      case (Or_mltl φ ψ)
      then show ?thesis using ind_h1 not init_F_is by auto
    next
      case (Future_mltl a b φ)
      then show ?thesis using ind_h1 not init_F_is by auto
    next
      case (Global_mltl a b φ)
      then show ?thesis using ind_h1 not init_F_is by auto
    next
      case (Until_mltl φ a b ψ)
      then show ?thesis using ind_h1 not init_F_is by auto
    next
      case (Release_mltl φ a b ψ)
      then show ?thesis using ind_h1 not init_F_is by auto
    qed
  next
    case (And_mltl φ ψ)
    then show ?thesis using ind_h1 not by auto
  next
    case (Or_mltl φ ψ)
    then show ?thesis using ind_h1 not by auto
  next
    case (Future_mltl a b φ)
    then show ?thesis using ind_h1 not by auto
  next
    case (Global_mltl a b φ)
    then show ?thesis using ind_h1 not by auto
  next
    case (Until_mltl φ a b ψ)
    then show ?thesis using ind_h1 not by auto
  next
    case (Release_mltl φ a b ψ)
    then show ?thesis using ind_h1 not by auto
  qed
qed

lemma convert_nnf_convert_nnf:
  shows "convert_nnf (convert_nnf F) = convert_nnf F"
proof (induction "depth_mltl F" arbitrary: F rule: less_induct)
  case less
  have not_case: "(F. depth_mltl F < Suc (depth_mltl G) 
               convert_nnf (convert_nnf F) = convert_nnf F) 
          F = Not_mltl G 
          convert_nnf (convert_nnf (Not_mltl G)) = convert_nnf (Not_mltl G)" for "G"
  proof -
    assume ind_h: "(F. depth_mltl F < Suc (depth_mltl G) 
               convert_nnf (convert_nnf F) = convert_nnf F)"
    assume F_is: "F = Not_mltl G"
    show ?thesis using less F_is apply (cases G) by simp_all
  qed
  show ?case using less apply (cases F) apply simp_all using not_case
    by auto
qed

lemma nnf_subformulas:
  assumes "F = convert_nnf init_F"
  assumes "G  subformulas F"
  shows " init_G. G = convert_nnf init_G"
  using assms proof (induct "depth_mltl init_F" arbitrary: init_F F G rule: less_induct)
  case less
  then show ?case proof (cases init_F)
    case True_mltl
    then show ?thesis using less by simp
  next
    case False_mltl
    then show ?thesis using less by simp
  next
    case (Prop_mltl p)
    then show ?thesis using less by simp
  next
    case (Not_mltl φ)
    then have init_is: "init_F = Notm φ"
      by auto
    then show ?thesis proof (cases φ)
      case True_mltl
      then show ?thesis using less init_is
        by auto
    next
      case False_mltl
      then show ?thesis using less init_is
        by auto
    next
      case (Prop_mltl p)
      then have "init_F = (Not_mltl Propm (p))"
        using init_is by auto
      then have "G = Prop_mltl p"
        using less by simp
      then have "G = convert_nnf Propm (p)"
        by auto
      then show ?thesis by blast
    next
      case (Not_mltl ψ)
      then have init_is2: "init_F = (Not_mltl (Not_mltl ψ))"
        using init_is by auto
      then have F_is: "F = convert_nnf ψ"
        using less by auto
      then show ?thesis using less.hyps[OF _ F_is] init_is2 less(3)
        by simp
    next
      case (And_mltl ψ1 ψ2)
        then have init_is2: "init_F = (Not_mltl (And_mltl ψ1 ψ2))"
        using init_is by auto
      then have F_is: "F = (Or_mltl (convert_nnf (Not_mltl ψ1)) (convert_nnf (Not_mltl ψ2)))"
        using less by auto
      have depth1: "depth_mltl (Not_mltl ψ1) < depth_mltl init_F"
        using init_is2
        by simp
      have depth2: "depth_mltl (Not_mltl ψ2) < depth_mltl init_F"
        using init_is2
        by simp
      have G_inset: "G  {(convert_nnf (Not_mltl ψ1)), (convert_nnf (Not_mltl ψ2))}
         subformulas (convert_nnf (Not_mltl ψ1))  subformulas (convert_nnf (Not_mltl ψ2))"
        using F_is less(3) by auto
      then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ1)"] less.hyps[OF depth2, of "convert_nnf (Not_mltl ψ2)"]
        G_inset by blast
    next
      case (Or_mltl ψ1 ψ2)
        then have init_is2: "init_F = (Not_mltl (Or_mltl ψ1 ψ2))"
        using init_is by auto
      then have F_is: "F = (And_mltl (convert_nnf (Not_mltl ψ1)) (convert_nnf (Not_mltl ψ2)))"
        using less by auto
      have depth1: "depth_mltl (Not_mltl ψ1) < depth_mltl init_F"
        using init_is2
        by simp
      have depth2: "depth_mltl (Not_mltl ψ2) < depth_mltl init_F"
        using init_is2
        by simp
      have G_inset: "G  {(convert_nnf (Not_mltl ψ1)), (convert_nnf (Not_mltl ψ2))}
         subformulas (convert_nnf (Not_mltl ψ1))  subformulas (convert_nnf (Not_mltl ψ2))"
        using F_is less(3) by auto
      then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ1)"] less.hyps[OF depth2, of "convert_nnf (Not_mltl ψ2)"]
        G_inset by blast
    next
      case (Future_mltl a b ψ)
      then have init_is2: "init_F = (Not_mltl (Future_mltl a b ψ))"
        using init_is by auto
      then have F_is: "F = (Global_mltl a b (convert_nnf (Not_mltl ψ)))"
        using less by auto
      have depth1: "depth_mltl (Not_mltl ψ) < depth_mltl init_F"
        using init_is2
        by simp
      have G_inset: "G  {(convert_nnf (Not_mltl ψ))}
         subformulas (convert_nnf (Not_mltl ψ))"
        using F_is less(3) by auto
      then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ)"]
        G_inset by blast
    next
      case (Global_mltl a b ψ)
      then have init_is2: "init_F = (Not_mltl (Global_mltl a b ψ))"
        using init_is by auto
      then have F_is: "F = (Future_mltl a b (convert_nnf (Not_mltl ψ)))"
        using less by auto
      have depth1: "depth_mltl (Not_mltl ψ) < depth_mltl init_F"
        using init_is2
        by simp
      have G_inset: "G  {(convert_nnf (Not_mltl ψ))}
         subformulas (convert_nnf (Not_mltl ψ))"
        using F_is less(3) by auto
      then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ)"]
        G_inset by blast
    next
      case (Until_mltl ψ1 a b ψ2)
     then have init_is2: "init_F = (Not_mltl (Until_mltl ψ1 a b ψ2))"
        using init_is by auto
      then have F_is: "F = (Release_mltl (convert_nnf (Not_mltl ψ1)) a b (convert_nnf (Not_mltl ψ2)))"
        using less by auto
      have depth1: "depth_mltl (Not_mltl ψ1) < depth_mltl init_F"
        using init_is2
        by simp
      have depth2: "depth_mltl (Not_mltl ψ2) < depth_mltl init_F"
        using init_is2
        by simp
      have G_inset: "G  {(convert_nnf (Not_mltl ψ1)), (convert_nnf (Not_mltl ψ2))}
         subformulas (convert_nnf (Not_mltl ψ1))  subformulas (convert_nnf (Not_mltl ψ2))"
        using F_is less(3) by auto
      then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ1)"] less.hyps[OF depth2, of "convert_nnf (Not_mltl ψ2)"]
        G_inset by blast
    next
      case (Release_mltl ψ1 a b ψ2)
     then have init_is2: "init_F = (Not_mltl (Release_mltl ψ1 a b ψ2))"
        using init_is by auto
      then have F_is: "F = (Until_mltl (convert_nnf (Not_mltl ψ1)) a b (convert_nnf (Not_mltl ψ2)))"
        using less by auto
      have depth1: "depth_mltl (Not_mltl ψ1) < depth_mltl init_F"
        using init_is2
        by simp
      have depth2: "depth_mltl (Not_mltl ψ2) < depth_mltl init_F"
        using init_is2
        by simp
      have G_inset: "G  {(convert_nnf (Not_mltl ψ1)), (convert_nnf (Not_mltl ψ2))}
         subformulas (convert_nnf (Not_mltl ψ1))  subformulas (convert_nnf (Not_mltl ψ2))"
        using F_is less(3) by auto
      then show ?thesis using less.hyps[OF depth1, of "convert_nnf (Not_mltl ψ1)"] less.hyps[OF depth2, of "convert_nnf (Not_mltl ψ2)"]
        G_inset by blast
    qed
  next
    case (And_mltl φ1 φ2)
    then have F_is: "F = And_mltl (convert_nnf φ1) (convert_nnf φ2)"
      using less by auto
    then have G_inset: "G  {(convert_nnf φ1), (convert_nnf φ2)}  subformulas (convert_nnf φ1) 
      subformulas (convert_nnf φ2)" using less(3) by simp
    have depth_phi1: "depth_mltl φ1 < depth_mltl init_F"
      using less And_mltl by simp
    have depth_phi2: "depth_mltl φ2 < depth_mltl init_F"
      using less And_mltl by simp
    then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ1"] using less.hyps[OF depth_phi2, of "convert_nnf φ2"]
        G_inset by blast
  next
    case (Or_mltl φ1 φ2)
    then have F_is: "F = Or_mltl (convert_nnf φ1) (convert_nnf φ2)"
      using less by auto
    then have G_inset: "G  {(convert_nnf φ1), (convert_nnf φ2)}  subformulas (convert_nnf φ1) 
      subformulas (convert_nnf φ2)" using less(3) by simp
    have depth_phi1: "depth_mltl φ1 < depth_mltl init_F"
      using less Or_mltl by simp
    have depth_phi2: "depth_mltl φ2 < depth_mltl init_F"
      using less Or_mltl by simp
    then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ1"] using less.hyps[OF depth_phi2, of "convert_nnf φ2"]
        G_inset by blast
  next
    case (Future_mltl a b φ)
    then have F_is: "F = Future_mltl a b (convert_nnf φ)"
      using less by auto
    then have G_inset: "G  {(convert_nnf φ)}  subformulas (convert_nnf φ)"
      using less(3) by simp
    have depth_phi1: "depth_mltl φ < depth_mltl init_F"
      using less Future_mltl by simp
    then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ"]
        G_inset by blast
  next
    case (Global_mltl a b φ)
    then have F_is: "F = Global_mltl a b (convert_nnf φ)"
      using less by auto
    then have G_inset: "G  {(convert_nnf φ)}  subformulas (convert_nnf φ)"
      using less(3) by simp
    have depth_phi1: "depth_mltl φ < depth_mltl init_F"
      using less Global_mltl by simp
    then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ"]
        G_inset by blast
  next
    case (Until_mltl φ1 a b φ2)
    then have F_is: "F = Until_mltl (convert_nnf φ1) a b (convert_nnf φ2)"
      using less by auto
    then have G_inset: "G  {(convert_nnf φ1), (convert_nnf φ2)}  subformulas (convert_nnf φ1) 
      subformulas (convert_nnf φ2)" using less(3) by simp
    have depth_phi1: "depth_mltl φ1 < depth_mltl init_F"
      using less Until_mltl by simp
    have depth_phi2: "depth_mltl φ2 < depth_mltl init_F"
      using less Until_mltl by simp
    then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ1"] using less.hyps[OF depth_phi2, of "convert_nnf φ2"]
        G_inset by blast
  next
    case (Release_mltl φ1 a b φ2)
     then have F_is: "F = Release_mltl (convert_nnf φ1) a b (convert_nnf φ2)"
      using less by auto
    then have G_inset: "G  {(convert_nnf φ1), (convert_nnf φ2)}  subformulas (convert_nnf φ1) 
      subformulas (convert_nnf φ2)" using less(3) by simp
    have depth_phi1: "depth_mltl φ1 < depth_mltl init_F"
      using less Release_mltl by simp
    have depth_phi2: "depth_mltl φ2 < depth_mltl init_F"
      using less Release_mltl by simp
    then show ?thesis using less.hyps[OF depth_phi1, of "convert_nnf φ1"] using less.hyps[OF depth_phi2, of "convert_nnf φ2"]
        G_inset by blast
  qed
qed


subsection ‹Computation Length and Properties›

fun complen_mltl:: "'a mltl  nat"
  where "complen_mltl Falsem = 1"
  | "complen_mltl Truem = 1"
  | "complen_mltl Propm (p) = 1"
  | "complen_mltl (Notm φ) = complen_mltl φ"
  | "complen_mltl (φ Andm ψ) = max (complen_mltl φ) (complen_mltl ψ)"
  | "complen_mltl (φ Orm ψ) = max (complen_mltl φ) (complen_mltl ψ)"
  | "complen_mltl (Gm [a,b] φ) = b + (complen_mltl φ)"
  | "complen_mltl (Fm [a,b] φ) = b + (complen_mltl φ)"
  | "complen_mltl (φ Rm [a,b] ψ) = b + (max ((complen_mltl φ)-1) (complen_mltl ψ))"
  | "complen_mltl (φ Um [a,b] ψ) = b + (max ((complen_mltl φ)-1) (complen_mltl ψ))"

lemma complen_geq_one: "complen_mltl F  1"
  apply (induct F) apply simp_all .

subsubsection ‹Capture (not (a <= b)) in an MLTL formula›
fun make_empty_trace:: "nat  'a set list"
  where "make_empty_trace 0 = []"
  | "make_empty_trace n = [{}]@ make_empty_trace (n-1)"

lemma length_make_empty_trace:
  shows "length (make_empty_trace n) = n"
proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then show ?case by auto
qed


lemma semantics_of_not_a_lteq_b:
  shows "(make_empty_trace (a+1)) m (Global_mltl a b Truem) = (a  b)"
  using length_make_empty_trace
  by simp

lemma semantics_of_not_a_lteq_b2:
  shows "(make_empty_trace (a+1)) m (Not_mltl (Global_mltl a b Truem)) = (¬ (a  b))"
  using semantics_of_not_a_lteq_b
  by simp

subsection ‹Custom Induction Rules›

text ‹ In some cases, it is sufficient to consider
 just a subset of MLTL operators when proving a property.
 We facilitate this with the following custom induction
 rules. ›

text ‹ In order to use the MLTL-induct rule,
  one must establish IntervalsWellDef, which
  states that the input formula is well-formed,
  and also prove PProp, which states that the
  property being established is not dependent on
  the syntax of the input formula but only on its
  semantics. ›
lemma MLTL_induct[case_names IntervalsWellDef PProp True False Prop Not And Until]:
  assumes IntervalsWellDef: "intervals_welldef F"
    and PProp: "( F G. ((π. semantics_mltl π F = semantics_mltl π G)  P F = P G))"
    and True: "P Truem"
    and False: "P Falsem"
    and Prop: " p. P Propm (p)"
    and Not: " F G. F = Notm G; P G  P F"
    and And: "F F1 F2.  F = F1 Andm F2;
        P F1; P F2  P F"
    and Until:"F F1 F2 a b.  F = F1 Um [a,b] F2;
        P F1; P F2  P F"
  shows "P F" using IntervalsWellDef
proof (induction F)
  case True_mltl
  then show ?case using True by simp
next
  case False_mltl
  then show ?case using False by simp
next
  case (Prop_mltl x)
  then show ?case using Prop by simp
next
  case (Not_mltl F1)
  then show ?case using Not by auto
next
  case (And_mltl F1 F2)
  then show ?case using And by auto
next
  case (Or_mltl F1 F2)
  have " π. semantics_mltl π (Or_mltl (Not_mltl (Not_mltl F1)) (Not_mltl (Not_mltl F2))) =
     semantics_mltl π (Or_mltl F1 F2)"
    using not_not_equiv
    by auto
  then have P1: "P (Or_mltl F1 F2) = P (Or_mltl (Not_mltl (Not_mltl F1)) (Not_mltl (Not_mltl F2)))"
    using PProp by blast
  have " π. semantics_mltl π (Not_mltl (And_mltl (Not_mltl F1) (Not_mltl F2))) =
    semantics_mltl π (Or_mltl (Not_mltl (Not_mltl F1)) (Not_mltl (Not_mltl F2)))"
    using demorgan_and_or[of "(Not_mltl F1)" "(Not_mltl F2)"]
    unfolding semantic_equiv_def by simp
  then have P2: "P (Not_mltl (And_mltl (Not_mltl F1) (Not_mltl F2))) = P (Or_mltl (Not_mltl (Not_mltl F1)) (Not_mltl (Not_mltl F2)))"
    using PProp by blast
  show ?case using P1 P2
    using And Not PProp
    using Or_mltl.IH(1) Or_mltl.IH(2) Or_mltl.prems by force
next
  case (Future_mltl a b F)
  then show ?case
    using future_as_until PProp IntervalsWellDef Until True
    unfolding semantic_equiv_def
    by (metis True Until intervals_welldef.simps(7))
next
  case (Global_mltl a b F)
  then show ?case using globally_future_dual Not PProp True Until future_as_until
    unfolding semantic_equiv_def
    by (metis intervals_welldef.simps(8))
next
  case (Until_mltl F1 a b F2)
  then show ?case using Until using intervals_welldef.simps(9)[of F1 a b F2]
    by blast
next
  case (Release_mltl F1 a b F2)
  have a_lt_b: "a  b" using Release_mltl(3) intervals_welldef.simps(10)[of F1 a b F2]
    by auto
  have PF: "P F1  P F2"
    using Release_mltl using intervals_welldef.simps(10)[of F1 a b F2]
    by blast
  have "P (Release_mltl F1 a b F2)  P (Not_mltl (Until_mltl (Not_mltl F1) a b (Not_mltl F2)))"
    using release_until_dual[OF a_lt_b, of F1 F2]  PProp
    unfolding semantic_equiv_def by metis
  then show ?case using Not
    using PF Until by force
qed

text ‹ In order to use the nnf-induct rule,
  one must establish that the input formula (i.e.
  the formula being inducted on) is in NNF format. ›
lemma nnf_induct[case_names nnf True False Prop And Or Final Global Until Release NotProp]:
  assumes nnf: "init_F. F = convert_nnf init_F"
    and True: "P Truem"
    and False: "P Falsem"
    and Prop: " p. P Propm (p)"
    and And: "F F1 F2.  F = F1 Andm F2;
        P F1; P F2  P F"
    and Or: "F F1 F2.  F = F1 Orm F2;
        P F1; P F2  P F"
    and Final: "F F1  a b.  F = Fm [a,b] F1;
        P F1  P F"
    and Global: "F F1  a b.  F = Gm [a,b] F1;
        P F1  P F"
    and Until: "F F1 F2  a b.  F = F1 Um [a,b] F2;
        P F1; P F2  P F"
    and Release: "F F1 F2 a b.  F = F1 Rm [a,b] F2;
        P F1; P F2  P F"
    and Not_Prop: " F p. F = Notm Propm (p)  P F"
  shows "P F" using nnf proof (induct F)
  case True_mltl
  then show ?case using True by auto
next
  case False_mltl
  then show ?case using False by auto
next
  case (Prop_mltl x)
  then show ?case using Prop by auto
next
  case (Not_mltl F)
  then show ?case using convert_nnf_form_Not_Implies_Prop Not_Prop by blast
next
  case (And_mltl F1 F2)
  then obtain init_F where init_F: "And_mltl F1 F2 = convert_nnf init_F"
    by auto
  then have "(init_F1. F1 = convert_nnf init_F1)  (init_F2. F2 = convert_nnf init_F2)"
    using nnf_subformulas[OF init_F] subformulas.simps(5) by blast
  then show ?case using And_mltl And by auto
next
  case (Or_mltl F1 F2)
  then obtain init_F where init_F: "Or_mltl F1 F2 = convert_nnf init_F"
    by auto
  then have "(init_F1. F1 = convert_nnf init_F1)  (init_F2. F2 = convert_nnf init_F2)"
    using nnf_subformulas[OF init_F] subformulas.simps(6) by blast
  then show ?case using Or_mltl Or by auto
next
  case (Future_mltl a b F)
  then obtain init_F where init_F: "Future_mltl a b F = convert_nnf init_F"
    by auto
  then have "(init_F1. F = convert_nnf init_F1)"
    using nnf_subformulas[OF init_F] subformulas.simps(8) by blast
  then show ?case using Future_mltl Final by auto
next
  case (Global_mltl a b F)
  then obtain init_F where init_F: "Global_mltl a b F = convert_nnf init_F"
    by auto
  then have "(init_F1. F = convert_nnf init_F1)"
    using nnf_subformulas[OF init_F] subformulas.simps(7) by blast
  then show ?case using Global_mltl Global by auto
next
  case (Until_mltl F1 a b F2)
  then obtain init_F where init_F: "Until_mltl F1 a b F2 = convert_nnf init_F"
    by auto
  then have "(init_F1. F1 = convert_nnf init_F1)  (init_F2. F2 = convert_nnf init_F2)"
    using nnf_subformulas[OF init_F] subformulas.simps(9) by blast
  then show ?case using Until_mltl Until by auto
next
  case (Release_mltl F1 a b F2)
  then obtain init_F where init_F: "Release_mltl F1 a b F2 = convert_nnf init_F"
    by auto
  then have "(init_F1. F1 = convert_nnf init_F1)  (init_F2. F2 = convert_nnf init_F2)"
    using nnf_subformulas[OF init_F] subformulas.simps(10) by blast
  then show ?case using Release_mltl Release by auto
qed

end