Theory WEST_Algorithms

section ‹ Key algorithms for WEST ›

theory WEST_Algorithms

imports Mission_Time_LTL.MLTL_Properties

begin

subsection ‹Custom Types›

datatype WEST_bit = Zero | One | S
type_synonym state = "nat set"
type_synonym trace = "nat set list"
type_synonym state_regex = "WEST_bit list"
type_synonym trace_regex = "WEST_bit list list"
type_synonym WEST_regex = "WEST_bit list list list"

subsection ‹Trace Regular Expressions›

fun WEST_get_bit:: "trace_regex ⇒ nat ⇒ nat ⇒ WEST_bit"
  where "WEST_get_bit regex timestep var = (
  if timestep ≥ length regex then S
  else let regex_index = regex ! timestep in
  if var ≥ length regex_index then S
  else regex_index ! var
  )"

text ‹ Returns the state at time i, list of variable states ›
fun WEST_get_state:: "trace_regex ⇒ nat ⇒ nat ⇒ state_regex"
  where "WEST_get_state regex time num_vars = (
  if time ≥ length regex then (map (λ k. S) [0 ..< num_vars])
  else regex ! time
  )"


text ‹ Checks if one state of a trace matches one timeslice of a WEST regex ›
definition match_timestep:: "nat set ⇒ state_regex ⇒ bool"
  where "match_timestep state regex_state = (∀ x::nat. x < length regex_state ⟶ (
  ((regex_state ! x = One) ⟶ x ∈ state) ∧
  ((regex_state ! x = Zero) ⟶ x ∉ state)))"

fun trim_reversed_regex:: "trace_regex ⇒ trace_regex"
  where "trim_reversed_regex [] = []"
  | "trim_reversed_regex (h#t) = (if (∀i<length h. (h!i) = S)
  then (trim_reversed_regex t) else (h#t))"

fun trim_regex:: "trace_regex ⇒ trace_regex"
  where "trim_regex regex = rev (trim_reversed_regex (rev regex))"

definition match_regex:: "nat set list ⇒ trace_regex ⇒ bool"
  where "match_regex trace regex =  ((∀ time<length regex.
  (match_timestep (trace ! time) (regex ! time)))
  ∧(length trace ≥ length regex))"

definition match:: "nat set list ⇒ WEST_regex ⇒ bool"
  where "match trace regex_list = (∃ i. i < length regex_list ∧
  (match_regex trace (regex_list ! i)))"

lemma match_example:
  shows "match [{0::nat,1}, {1}, {0}]
  [
    [[Zero,Zero]],
    [[S,S], [S,One]]
  ] = True"
proof-
  let ?regexList = "[[[Zero,Zero]],[[S,S], [S,One]]]"
  let ?trace = "[{0::nat,1}, {1}, {0}]"
  have "(match_regex ?trace (?regexList!1))"
    unfolding match_regex_def
    by (simp add: match_timestep_def nth_Cons')
  then show ?thesis
    by (metis One_nat_def add.commute le_imp_less_Suc le_numeral_extra(4) list.size(3) list.size(4) match_def plus_1_eq_Suc)
qed


definition regex_equiv:: "WEST_regex ⇒ WEST_regex ⇒ bool"
  where "regex_equiv rl1 rl2 = (
  ∀ π::nat set list. (match π rl1) ⟷ (match π rl2))"


lemma "(regex_equiv [[[S,S]]]
  [[[S,One]],
    [[One,S]],
    [[Zero,Zero]]]) = True"
proof -
  have d1: "match π [[[S, One]], [[One, S]], [[Zero, Zero]]]" if match: "match π [[[S, S]]]" for π
  proof -
    have match_ss: "match_regex π [[S, S]]"
      using match unfolding match_def
      by (metis One_nat_def length_Cons less_one list.size(3) nth_Cons_0)
    {assume *: "¬ (match_regex π [[S, One]]) ∧ ¬ (match_regex π [[One, S]])"
      have "match_regex π [[Zero, Zero]]"
        using match_ss unfolding match_regex_def
        by (smt (verit) "*" One_nat_def WEST_bit.simps(2) length_Cons less_2_cases less_one list.size(3) match_regex_def match_timestep_def nth_Cons_0 nth_Cons_Suc numeral_2_eq_2)
    }
    then show ?thesis
      unfolding match_def
      by (metis length_Cons less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc)
  qed
  have d2: "match π [[[S, S]]]" if match: "match π [[[S, One]], [[One, S]], [[Zero, Zero]]]" for π
  proof -
    {assume *: "match_regex π [[S, One]]"
      then have "match_regex π [[S, S]]"
        unfolding  match_regex_def
        by (smt (verit, ccfv_SIG) One_nat_def WEST_bit.simps(4) length_Cons less_2_cases less_one list.size(3) match_timestep_def nth_Cons_0 nth_Cons_Suc numeral_2_eq_2)
      then have "match π [[[S, S]]]"
        unfolding match_def by simp
    } moreover {assume *: "match_regex π [[One, S]]"
      then have "match_regex π [[S, S]]"
        unfolding  match_regex_def
        by (smt (verit, ccfv_SIG) One_nat_def WEST_bit.simps(4) length_Cons less_2_cases less_one list.size(3) match_timestep_def nth_Cons_0 nth_Cons_Suc numeral_2_eq_2)
      then have "match π [[[S, S]]]"
        unfolding match_def by simp
    } moreover {assume *: "match_regex π [[Zero, Zero]]"
      then have "match_regex π [[S, S]]"
        unfolding  match_regex_def
        by (smt (verit) One_nat_def WEST_bit.distinct(5) length_Cons less_2_cases_iff less_one list.size(3) match_timestep_def nth_Cons_0 nth_Cons_Suc numeral_2_eq_2)
      then have "match π [[[S, S]]]"
        unfolding match_def by simp
    }
    ultimately show ?thesis using match unfolding regex_equiv_def
      by (smt (verit, del_insts) length_Cons less_Suc_eq_0_disj match_def nth_Cons_0 nth_Cons_Suc)
  qed
  show ?thesis using d1 d2
    unfolding regex_equiv_def by metis
qed


subsection ‹ WEST Operations ›

subsubsection ‹ AND ›


fun WEST_and_bitwise::"WEST_bit ⇒
                       WEST_bit ⇒
                       WEST_bit option"
  where "WEST_and_bitwise b One = (if b = Zero then None else Some One)"
  | "WEST_and_bitwise b Zero = (if b = One then None else Some Zero)"
  | "WEST_and_bitwise b S = Some b"



fun WEST_and_state:: "state_regex ⇒ state_regex ⇒ state_regex option"
  where "WEST_and_state [] [] = Some []"
  | "WEST_and_state (h1#t1) (h2#t2) =
  (case WEST_and_bitwise h1 h2 of
    None ⇒ None
    | Some b ⇒ (case WEST_and_state t1 t2 of
                  None ⇒ None
                  | Some L ⇒ Some (b#L)))"
  | "WEST_and_state _ _ = None"



fun WEST_and_trace:: "trace_regex ⇒ trace_regex ⇒ trace_regex option"
  where "WEST_and_trace trace [] = Some trace"
  | "WEST_and_trace [] trace = Some trace"
  | "WEST_and_trace (h1#t1) (h2#t2) =
  (case WEST_and_state h1 h2 of
    None ⇒ None
    | Some state ⇒ (case WEST_and_trace t1 t2 of
                      None ⇒ None
                      | Some trace ⇒ Some (state#trace)))"


fun WEST_and_helper:: "trace_regex ⇒ WEST_regex ⇒ WEST_regex"
  where "WEST_and_helper trace [] = []"
  | "WEST_and_helper trace (t#traces) =
  (case WEST_and_trace trace t of
    None ⇒ WEST_and_helper trace traces
    | Some res ⇒ res#(WEST_and_helper trace traces))"


fun WEST_and:: "WEST_regex ⇒ WEST_regex ⇒ WEST_regex"
  where "WEST_and traceList [] = []"
  | "WEST_and [] traceList = []"
  | "WEST_and (trace#traceList1) traceList2 =
  (case WEST_and_helper trace traceList2 of
    [] ⇒ WEST_and traceList1 traceList2
    | traceList ⇒ traceList@(WEST_and traceList1 traceList2))"

subsubsection ‹Simp›

paragraph ‹Bitwise simplification operation›

fun WEST_simp_bitwise:: "WEST_bit ⇒ WEST_bit ⇒ WEST_bit"
  where "WEST_simp_bitwise b S = S"
  | "WEST_simp_bitwise b Zero = (if b = Zero then Zero else S)"
  | "WEST_simp_bitwise b One = (if b = One then One else S)"

fun WEST_simp_state:: "state_regex ⇒ state_regex ⇒ state_regex"
  where "WEST_simp_state s1 s2 = (
  map (λ k. WEST_simp_bitwise (s1 ! k) (s2 ! k)) [0 ..< (length s1)])"


fun WEST_simp_trace:: "trace_regex ⇒ trace_regex ⇒ nat => trace_regex"
  where "WEST_simp_trace trace1 trace2 num_vars = (
  map (λ k. (WEST_simp_state (WEST_get_state trace1 k num_vars) (WEST_get_state trace2 k num_vars)))
  [0 ..< (Max {(length trace1), (length trace2)})])"


paragraph ‹ Helper functions for defining WEST-simp ›

fun count_nonS_trace:: "state_regex ⇒ nat"
  where "count_nonS_trace [] = 0"
  | "count_nonS_trace (h#t) = (if (h ≠ S) then (1 + (count_nonS_trace t)) else (count_nonS_trace t))"

fun count_diff_state:: "state_regex ⇒ state_regex ⇒ nat"
  where "count_diff_state [] [] = 0"
  | "count_diff_state trace [] = count_nonS_trace trace"
  | "count_diff_state [] trace = count_nonS_trace trace"
  | "count_diff_state (h1#t1) (h2#t2) = (if (h1 = h2) then (count_diff_state t1 t2) else (1 + (count_diff_state t1 t2)))"

fun count_diff:: "trace_regex ⇒ trace_regex ⇒ nat"
  where "count_diff [] [] = 0"
  | "count_diff [] (h#t) = (count_diff_state [] h) + (count_diff [] t)"
  | "count_diff (h#t) [] = (count_diff_state [] h) + (count_diff [] t)"
  | "count_diff (h1#t1) (h2#t2) = (count_diff_state h1 h2) + (count_diff t1 t2)"

fun check_simp:: "trace_regex ⇒ trace_regex ⇒ bool"
  where "check_simp trace1 trace2 = ((count_diff trace1 trace2) ≤ 1 ∧ length trace1 = length trace2)"

fun enumerate_pairs :: "nat list ⇒ (nat * nat) list" where
  "enumerate_pairs [] = []" |
  "enumerate_pairs (x#xs) = map (λy. (x, y)) xs @ enumerate_pairs xs"

fun enum_pairs:: "'a list ⇒ (nat * nat) list"
  where "enum_pairs L = enumerate_pairs [0 ..< length L]"

fun remove_element_at_index:: "nat ⇒ 'a list ⇒ 'a list"
  where "remove_element_at_index n L = (take n L)@(drop (n+1) L)"

text ‹ This assumes (fst h) < (snd h) ›
fun update_L:: "WEST_regex ⇒ (nat × nat) ⇒ nat ⇒ WEST_regex"
  where "update_L L h num_vars =
(remove_element_at_index (fst h) (remove_element_at_index (snd h) L))@[WEST_simp_trace (L!(fst h)) (L!(snd h)) num_vars]"

paragraph ‹ Defining and Proving Termination of WEST-simp ›

lemma length_enumerate_pairs:
  shows "length (enumerate_pairs L) ≤ (length L)^2"
proof (induction L)
  case Nil
  then show ?case by auto
next
  case (Cons a L)
  have length_L: "(length (a # L))⇧2 = (1 + (length L))^2" by auto
  then have length_L: "(length (a # L))⇧2 = 1 + 2*(length L) + (length L)^2" by algebra
  have "length (map (Pair a) L) ≤ length L"
    by simp
  then show ?case
    unfolding enumerate_pairs.simps using Cons length_L by simp
qed

lemma length_enum_pairs:
  shows "length (enum_pairs L) ≤ (length L)^2"
proof-
  show ?thesis unfolding enum_pairs.simps using length_enumerate_pairs
    by (metis length_upt minus_nat.diff_0)
qed

lemma enumerate_pairs_fact:
  assumes "∀ i j. (i < j ∧ i < length L ∧ j < length L) ⟶ (L!i) < (L!j)"
  shows "∀ pair ∈ set (enumerate_pairs L). (fst pair) < (snd pair)"
  using assms
proof(induct "length L" arbitrary:L)
  case 0
  then show ?case by auto
next
  case (Suc x)
  then obtain h T where obt_hT: "L = h#T"
    by (metis length_Suc_conv)
  then have enum_L: "enumerate_pairs L = map (Pair h) T @ enumerate_pairs T"
    using enumerate_pairs.simps obt_hT by blast
  then have "⋀ pair. pair ∈ set (enumerate_pairs L) ⟹ fst pair < snd pair"
  proof-
    fix pair
    assume "pair ∈ set (enumerate_pairs L)"
    then have "pair ∈ set (map (Pair h) T @ enumerate_pairs T)" using enum_L by auto
    then have pair_or: "pair ∈ set (map (Pair h) T) ∨ pair ∈ set(enumerate_pairs T)"
      by auto
    {assume in_base: "pair ∈ set (map (Pair h) T)"
      have "∀j. 0 < j ∧ j < length L ⟶ h < L ! j"
        using Suc.prems obt_hT by force
      then have "∀j < length T. h < T!j"
        using obt_hT by force
      then have "∀t ∈ set T. h < t"
        using obt_hT by (metis in_set_conv_nth)
      then have "fst pair < snd pair"
        using in_base by auto
    } moreover {
      assume in_rec: "pair ∈ set(enumerate_pairs T)"
      have "fst pair < snd pair"
        using Suc.hyps(1)[of T] Suc.prems obt_hT in_rec
        by (smt (verit, ccfv_SIG) Ex_less_Suc Suc.hyps(1) Suc.hyps(2) length_Cons less_trans_Suc nat.inject nth_Cons_Suc)
    }
    ultimately show "fst pair < snd pair" using enum_L obt_hT pair_or by blast
  qed
  then show ?case by blast
qed

lemma enum_pairs_fact:
  shows "∀ pair ∈ set (enum_pairs L). (fst pair) < (snd pair)"
  unfolding enum_pairs.simps using enumerate_pairs_fact[of "[0..<length L]"]
  by simp

lemma enum_pairs_bound_snd:
  assumes " pair ∈ set (enumerate_pairs L)"
  shows "(snd pair) ∈ set L"
  using assms
proof (induct "length L" arbitrary: L)
  case 0
  then show ?case by auto
next
  case (Suc x)
  then obtain h T where ht: "L = h#T"
    by (metis enumerate_pairs.cases enumerate_pairs.simps(1) in_set_member member_rec(2))
  then have eo: "pair ∈ set (map (Pair h) T) ∨ pair ∈ set (enumerate_pairs T)"
    using Suc by simp
  {assume *: "pair ∈ set (map (Pair h) T)"
    then have ?case
      using ht
      using imageE by auto
  } moreover {assume *: "pair ∈ set (enumerate_pairs T)"
    then have "snd pair ∈ set T"
      using Suc(1)[of T] ht
      using Suc.hyps(2) by fastforce
    then have ?case using ht
      by simp
  }
  ultimately show ?case using eo by blast
qed


lemma enum_pairs_bound:
  shows "∀ pair ∈ set (enum_pairs L). (snd pair) < length L"
  unfolding enum_pairs.simps enumerate_pairs.simps
proof(induct "length L" arbitrary: L)
  case 0
  then show ?case by simp
next
  case (Suc x)
  then have enum_L: "enumerate_pairs ([0..<length L]) =
    map (Pair 0) [1..<length L] @ enumerate_pairs [1..<length L]"
    using enumerate_pairs.simps(2)[of 0 "[1 ..< length L]"]
    by (metis One_nat_def upt_conv_Cons zero_less_Suc)
  then have "pair∈set (enumerate_pairs [0..<length L]) ⟹ snd pair < length L" for pair
    using enum_pairs_bound_snd[of pair "[0..<length L]"]
    by auto
  then show ?case unfolding enum_pairs.simps by blast
qed

lemma WEST_simp_termination1_bound:
  fixes a::"nat"
  shows "a^3+a^2 < (a+1)^3"
proof-
  have cubed: "(a+1)^3 = a^3 + 3*a^2 + 3*a + 1"
  proof-
    have "(a+1)^3 = (a+1)*(a+1)*(a+1)"
      by algebra
    then show ?thesis
      by (simp add: add.commute add_mult_distrib2 mult.commute power2_eq_square power3_eq_cube)
  qed
  have "0 < 2*a^2 + 2*a + 1" by simp
  then have "a^3 + a^2 < a^3 + 3*a^2 + 3*a + 1" by simp
  then show ?thesis using cubed
    by simp
qed

lemma WEST_simp_termination1:
  fixes L::"WEST_regex"
  assumes "¬ (idx_pairs ≠ enum_pairs L ∨ length idx_pairs ≤ i)"
  assumes "check_simp (L ! fst (idx_pairs ! i)) (L ! snd (idx_pairs ! i))"
  assumes "x = update_L L (idx_pairs ! i) num_vars"
  shows "((x, enum_pairs x, 0, num_vars), L, idx_pairs, i, num_vars)
       ∈ measure (λ(L, idx_list, i, num_vars). length L ^ 3 + length idx_list - i)"
proof-
  let ?i = "fst (idx_pairs ! i)"
  let ?j = "snd (idx_pairs ! i)"
  have i_le_j: "?i < ?j" using enum_pairs_fact assms
    by (metis linorder_le_less_linear nth_mem)
  have j_bound: "?j < length L"
    using assms(1) enum_pairs_bound[of L]
    by simp
  then have i_bound: "?i < (length L)-1"
    using i_le_j by auto
  have len_orsimp: "length [WEST_simp_trace (L ! ?i) (L ! ?j) num_vars] = 1"
    by simp
  have "length (remove_element_at_index ?j L) = length L - 1"
    using assms(3) j_bound by auto
  then have "length (remove_element_at_index ?i (remove_element_at_index ?j L)) = length L - 2"
    using assms(3) i_bound j_bound by simp
  then have length_x: "length x = (length L) - 1"
    using assms(3) len_orsimp
    unfolding update_L.simps[of L "idx_pairs ! i" num_vars]
    by (metis (no_types, lifting) add.commute add_diff_inverse_nat diff_diff_left gr_implies_not0 i_bound length_append less_one nat_1_add_1)
  have i_bound: "i < length idx_pairs" using assms by force

  { assume short_L: "length L = 0"
    then have ?thesis using assms
      using j_bound by linarith
  } moreover {
    assume long_L: "length L ≥ 1"
    then have "length L - 1 ≥ 0" by blast
    then have "(length L - 1) ^ 3 + (length L - 1) ^ 2 < length L ^ 3"
      using WEST_simp_termination1_bound[of "length L-1"]
      by (metis long_L ordered_cancel_comm_monoid_diff_class.le_imp_diff_is_add)
    then have "(length L - 1) ^ 3 + length (enumerate_pairs [0..<length x]) < length L ^ 3"
      using length_enumerate_pairs[of "[0..<length x]"] length_x by auto
    then have "length x ^ 3 + length (enumerate_pairs [0..<length x])
      < length L ^ 3 + length idx_pairs - i"
      using i_bound length_x by simp
    then have ?thesis by simp
  }
  ultimately show ?thesis by linarith
qed


function WEST_simp_helper:: "WEST_regex ⇒ (nat × nat) list ⇒ nat ⇒ nat ⇒ WEST_regex"
  where "WEST_simp_helper L idx_pairs i num_vars =
  (if (idx_pairs ≠ enum_pairs L ∨ i ≥ length idx_pairs) then L else
    (if (check_simp (L!(fst (idx_pairs!i))) (L!(snd (idx_pairs!i)))) then
    (let newL = update_L L (idx_pairs!i) num_vars in
    WEST_simp_helper newL (enum_pairs newL) 0 num_vars)
    else WEST_simp_helper L idx_pairs (i+1) num_vars))"
  apply fast by blast
termination
  apply (relation "measure (λ(L , idx_list, i, num_vars). (length L^3 + length idx_list - i))")
    apply simp using WEST_simp_termination1 apply blast by auto

declare WEST_simp_helper.simps[simp del]

fun WEST_simp:: "WEST_regex ⇒ nat ⇒ WEST_regex"
  where "WEST_simp L num_vars =
  WEST_simp_helper L (enum_pairs L) 0 num_vars"

value "WEST_simp [[[S, S, One]],[[S, One, S]], [[S, S, Zero]]] 3"
value "WEST_simp [[[S, One]],[[One, S]], [[Zero, Zero]]] 2"
value "WEST_simp [[[One, One]],[[Zero, Zero]], [[One, Zero]], [[Zero, One]]] 2"


subsubsection ‹ AND and OR operations with WEST-simp ›

fun WEST_and_simp:: "WEST_regex ⇒ WEST_regex ⇒ nat ⇒ WEST_regex"
  where "WEST_and_simp L1 L2 num_vars = WEST_simp (WEST_and L1 L2) num_vars"

fun WEST_or_simp:: "WEST_regex ⇒ WEST_regex ⇒ nat ⇒ WEST_regex"
  where "WEST_or_simp L1 L2 num_vars = WEST_simp (L1@L2) num_vars"

subsubsection ‹ Useful Helper Functions ›

fun arbitrary_state::"nat ⇒ state_regex"
  where "arbitrary_state num_vars = map (λ k. S) [0 ..< num_vars]"

fun arbitrary_trace::"nat ⇒ nat ⇒ trace_regex"
  where "arbitrary_trace num_vars num_pad = map (λ k. (arbitrary_state num_vars)) [0 ..< num_pad]"

fun shift:: "WEST_regex ⇒ nat ⇒ nat ⇒ WEST_regex"
  where "shift traceList num_vars num_pad = map (λ trace. (arbitrary_trace num_vars num_pad)@trace) traceList"

fun pad:: "trace_regex ⇒ nat ⇒ nat ⇒ trace_regex"
  where "pad trace num_vars num_pad = trace@(arbitrary_trace num_vars num_pad)"


subsubsection ‹ WEST Temporal Operations ›

fun WEST_global:: "WEST_regex ⇒ nat ⇒ nat ⇒ nat ⇒ WEST_regex"
where "WEST_global L a b num_vars = (
if (a = b) then (shift L num_vars a)
   else ( if (a < b) then (WEST_and_simp (shift L num_vars b)
                 (WEST_global L a (b-1) num_vars) num_vars)
      else []))"


fun WEST_future:: "WEST_regex ⇒ nat ⇒ nat ⇒ nat ⇒ WEST_regex"
  where "WEST_future L a b num_vars = (
  if (a = b)
  then (shift L num_vars a)
  else (
    if (a < b)
    then WEST_or_simp (shift L num_vars b) (WEST_future L a (b-1) num_vars) num_vars
    else []))"


fun WEST_until:: "WEST_regex ⇒ WEST_regex ⇒ nat ⇒
                  nat ⇒ nat ⇒ WEST_regex"
  where "WEST_until L_φ L_ψ a b num_vars = (
  if (a=b)
  then (WEST_global L_ψ a a num_vars)
  else (
    if (a < b)
    then WEST_or_simp (WEST_until L_φ L_ψ a (b-1) num_vars)
         (WEST_and_simp (WEST_global L_φ a (b-1) num_vars)
                    (WEST_global L_ψ b b num_vars) num_vars) num_vars
    else []))"


fun WEST_release_helper:: "WEST_regex ⇒ WEST_regex ⇒
                   nat ⇒ nat ⇒ nat ⇒ WEST_regex"
  where "WEST_release_helper L_φ L_ψ a ub num_vars = (
  if (a=ub)
  then (WEST_and_simp (WEST_global L_φ a a num_vars) (WEST_global L_ψ a a num_vars) num_vars)
  else (
    if (a < ub)
    then WEST_or_simp (WEST_release_helper L_φ L_ψ a (ub-1) num_vars)
         (WEST_and_simp (WEST_global L_ψ a ub num_vars)
                    (WEST_global L_φ ub ub num_vars) num_vars) num_vars
    else []))"

fun WEST_release:: "WEST_regex ⇒ WEST_regex ⇒ nat
                    ⇒ nat ⇒ nat ⇒ WEST_regex"
  where "WEST_release L_φ L_ψ a b num_vars = (
  if (b > a)
  then (WEST_or_simp (WEST_global L_ψ a b num_vars) (WEST_release_helper L_φ L_ψ a (b-1) num_vars) num_vars)
  else (WEST_global L_ψ a b num_vars))"


subsubsection ‹ WEST recursive reg Function ›
lemma exhaustive:
  shows "⋀x:: nat mltl × nat. ⋀P::bool. (⋀num_vars::nat. x = (True_mltl, num_vars) ⟹ P) ⟹
           (⋀num_vars::nat. x = (False_mltl, num_vars) ⟹ P) ⟹
           (⋀p num_vars::nat. x = (Prop_mltl p, num_vars) ⟹ P) ⟹
           (⋀p num_vars::nat. x = (Not_mltl (Prop_mltl p), num_vars) ⟹ P) ⟹
           (⋀φ ψ num_vars. x = (Or_mltl φ ψ, num_vars) ⟹ P) ⟹
           (⋀φ ψ num_vars. x = (And_mltl φ ψ, num_vars) ⟹ P) ⟹
           (⋀φ a b num_vars. x = (Future_mltl φ a b, num_vars) ⟹ P) ⟹
           (⋀φ a b num_vars. x = (Global_mltl φ a b, num_vars) ⟹ P) ⟹
           (⋀φ ψ a b num_vars. x = (Until_mltl φ ψ a b, num_vars) ⟹ P) ⟹
           (⋀φ ψ a b num_vars. x = (Release_mltl φ ψ a b, num_vars) ⟹ P) ⟹
           (⋀num_vars. x = (Not_mltl True_mltl, num_vars) ⟹ P) ⟹
           (⋀num_vars. x = (Not_mltl False_mltl, num_vars) ⟹ P) ⟹
           (⋀φ ψ num_vars. x = (Not_mltl (And_mltl φ ψ), num_vars) ⟹ P) ⟹
           (⋀φ ψ num_vars. x = (Not_mltl (Or_mltl φ ψ), num_vars) ⟹ P) ⟹
           (⋀φ a b num_vars. x = (Not_mltl (Future_mltl φ a b), num_vars) ⟹ P) ⟹
           (⋀φ a b num_vars. x = (Not_mltl (Global_mltl φ a b), num_vars) ⟹ P) ⟹
           (⋀φ ψ a b num_vars. x = (Not_mltl (Until_mltl φ ψ a b), num_vars) ⟹ P) ⟹
           (⋀φ ψ a b num_vars. x = (Not_mltl (Release_mltl φ ψ a b), num_vars) ⟹ P) ⟹
           (⋀φ num_vars. x = (Not_mltl (Not_mltl φ), num_vars) ⟹ P) ⟹ P"
proof -
  fix x::"nat mltl × nat"
  fix P:: "bool"
  assume t: "(⋀num_vars::nat. x = (True_mltl, num_vars) ⟹ P)"
  assume fa: "(⋀num_vars::nat. x = (False_mltl, num_vars) ⟹ P)"
  assume p: "(⋀p num_vars::nat. x = (Prop_mltl p, num_vars) ⟹ P) "
  assume n1: "(⋀p num_vars::nat. x = (Not_mltl (Prop_mltl p), num_vars) ⟹ P) "
  assume o: "(⋀φ ψ num_vars. x = (Or_mltl φ ψ, num_vars) ⟹ P) "
  assume a: "(⋀φ ψ num_vars. x = (And_mltl φ ψ, num_vars) ⟹ P) "
  assume f: "(⋀φ a b num_vars. x = (Future_mltl φ a b, num_vars) ⟹ P) "
  assume g: "(⋀φ a b num_vars. x = (Global_mltl φ a b, num_vars) ⟹ P) "
  assume u: "(⋀φ ψ a b num_vars. x = (Until_mltl φ ψ a b, num_vars) ⟹ P) "
  assume r: "(⋀φ ψ a b num_vars. x = (Release_mltl φ ψ a b, num_vars) ⟹ P) "
  assume n2: "(⋀num_vars. x = (Not_mltl True_mltl, num_vars) ⟹ P) "
  assume n3: "(⋀num_vars. x = (Not_mltl False_mltl, num_vars) ⟹ P) "
  assume n4: "(⋀φ ψ num_vars. x = (Not_mltl (And_mltl φ ψ), num_vars) ⟹ P) "
  assume n5: "(⋀φ ψ num_vars. x = (Not_mltl (Or_mltl φ ψ), num_vars) ⟹ P) "
  assume n6: "(⋀φ a b num_vars. x = (Not_mltl (Future_mltl φ a b), num_vars) ⟹ P) "
  assume n7: "(⋀φ a b num_vars. x = (Not_mltl (Global_mltl φ a b), num_vars) ⟹ P) "
  assume n8: "(⋀φ ψ a b num_vars. x = (Not_mltl (Until_mltl φ ψ a b), num_vars) ⟹ P) "
  assume n9: "(⋀φ ψ a b num_vars. x = (Not_mltl (Release_mltl φ ψ a b), num_vars) ⟹ P) "
  assume n10: "(⋀φ num_vars. x = (Not_mltl (Not_mltl φ), num_vars) ⟹ P)"
  show "P" proof (cases "fst x")
    case True_mltl
    then show ?thesis using t
      by (metis eq_fst_iff)
  next
    case False_mltl
    then show ?thesis using fa eq_fst_iff by metis
  next
    case (Prop_mltl p)
    then show ?thesis using p
      by (metis prod.collapse)
  next
    case (Not_mltl φ)
    then have fst_x: "fst x = Not_mltl φ"
      by auto
    then show ?thesis proof (cases φ)
      case True_mltl
      then show ?thesis using n2
        by (metis Not_mltl split_pairs)
    next
      case False_mltl
      then show ?thesis using n3
        by (metis Not_mltl prod.collapse)
    next
      case (Prop_mltl p)
      then show ?thesis using n1
        by (metis Not_mltl split_pairs)
    next
      case (Not_mltl φ1)
      then show ?thesis using n10 fst_x
        by (metis prod.collapse)
    next
      case (And_mltl φ1 φ2)
      then show ?thesis
        by (metis Not_mltl n4 prod.collapse)
    next
      case (Or_mltl φ1 φ2)
      then show ?thesis using n5 Not_mltl
        by (metis prod.collapse)
    next
      case (Future_mltl a b φ1)
      then show ?thesis  using n6 Not_mltl
        by (metis prod.collapse)
    next
      case (Global_mltl a b φ1)
      then show ?thesis  using n7 Not_mltl
        by (metis prod.collapse)
    next
      case (Until_mltl φ1 a b φ2)
      then show ?thesis  using n8 Not_mltl
        by (metis prod.collapse)
    next
      case (Release_mltl φ1 a b φ2)
      then show ?thesis  using n9 Not_mltl
        by (metis prod.collapse)
    qed
  next
    case (And_mltl φ1 φ2)
    then show ?thesis using a
      by (metis prod.collapse)
  next
    case (Or_mltl φ1 φ2)
    then show ?thesis using o
      by (metis prod.collapse)
  next
    case (Future_mltl a b φ1)
    then show ?thesis using f
      by (metis split_pairs)
  next
    case (Global_mltl a b φ1)
    then show ?thesis using g
      by (metis prod.collapse)
  next
    case (Until_mltl φ1 a b φ2)
    then show ?thesis using u
      by (metis split_pairs)
  next
    case (Release_mltl φ1 a b φ2)
    then show ?thesis using r
      by (metis split_pairs)
  qed
qed


fun WEST_termination_measure:: "(nat) mltl ⇒ nat"
  where "WEST_termination_measure True⇩m = 1"
  | "WEST_termination_measure (Not⇩m True⇩m) = 4"
  | "WEST_termination_measure False⇩m = 1"
  | "WEST_termination_measure (Not⇩m False⇩m) = 4"
  | "WEST_termination_measure (Prop⇩m (p)) = 1"
  | "WEST_termination_measure (Not⇩m (Prop⇩m (p))) = 4"
  | "WEST_termination_measure (φ Or⇩m ψ) = 1 + (WEST_termination_measure φ) + (WEST_termination_measure ψ)"
  | "WEST_termination_measure (φ And⇩m ψ) = 1 + (WEST_termination_measure φ) + (WEST_termination_measure ψ)"
  | "WEST_termination_measure (F⇩m [a,b] φ) = 1 + (WEST_termination_measure φ)"
  | "WEST_termination_measure (G⇩m [a,b] φ) = 1 + (WEST_termination_measure φ)"
  | "WEST_termination_measure (φ U⇩m[a,b] ψ) = 1 + (WEST_termination_measure φ) + (WEST_termination_measure ψ)"
  | "WEST_termination_measure (φ R⇩m[a,b] ψ) = 1 + (WEST_termination_measure φ) + (WEST_termination_measure ψ)"
  | "WEST_termination_measure (Not⇩m (φ Or⇩m ψ)) = 1 + 3 * (WEST_termination_measure (φ Or⇩m ψ))"
  | "WEST_termination_measure (Not⇩m (φ And⇩m ψ)) = 1 + 3 * (WEST_termination_measure (φ And⇩m ψ))"
  | "WEST_termination_measure (Not⇩m (F⇩m[a,b] φ)) = 1 + 3 * (WEST_termination_measure (F⇩m[a,b] φ))"
  | "WEST_termination_measure (Not⇩m (G⇩m[a,b] φ)) = 1 + 3 * (WEST_termination_measure (G⇩m[a,b] φ))"
  | "WEST_termination_measure (Not⇩m (φ U⇩m[a,b] ψ)) = 1 + 3 * (WEST_termination_measure (φ U⇩m[a,b] ψ))"
  | "WEST_termination_measure (Not⇩m (φ R⇩m[a,b] ψ)) = 1 + 3 * (WEST_termination_measure (φ R⇩m[a,b] ψ))"
  | "WEST_termination_measure (Not⇩m (Not⇩m φ)) = 1 + 3 * (WEST_termination_measure (Not⇩m φ))"

lemma WEST_termination_measure_not:
  fixes φ::"(nat) mltl"
  shows "WEST_termination_measure (Not_mltl φ) = 1 + 3 * (WEST_termination_measure φ)"
  apply (induction φ) by simp_all


function WEST_reg_aux:: "(nat) mltl ⇒ nat ⇒ WEST_regex"
  where "WEST_reg_aux True⇩m num_vars = [[(map (λ j. S) [0 ..< num_vars])]]"
  | "WEST_reg_aux False⇩m num_vars = []"
  | "WEST_reg_aux (Prop⇩m (p)) num_vars = [[(map (λ j. (if (p=j) then One else S)) [0 ..< num_vars])]]"
  | "WEST_reg_aux (Not⇩m (Prop⇩m (p))) num_vars = [[(map (λ j. (if (p=j) then Zero else S)) [0 ..< num_vars])]]"
  | "WEST_reg_aux (φ Or⇩m ψ) num_vars = WEST_or_simp (WEST_reg_aux φ num_vars) (WEST_reg_aux ψ num_vars) num_vars"
  | "WEST_reg_aux (φ And⇩m ψ) num_vars = (WEST_and_simp (WEST_reg_aux φ num_vars) (WEST_reg_aux ψ num_vars) num_vars)"
  | "WEST_reg_aux (F⇩m[a,b] φ) num_vars = (WEST_future (WEST_reg_aux φ num_vars) a b num_vars)"
  | "WEST_reg_aux (G⇩m[a,b] φ) num_vars = (WEST_global (WEST_reg_aux φ num_vars) a b num_vars)"
  | "WEST_reg_aux (φ U⇩m[a,b] ψ) num_vars = (WEST_until (WEST_reg_aux φ num_vars) (WEST_reg_aux ψ num_vars) a b num_vars)"
  | "WEST_reg_aux (φ R⇩m[a,b] ψ) num_vars = WEST_release (WEST_reg_aux φ num_vars) (WEST_reg_aux ψ num_vars) a b num_vars"
  | "WEST_reg_aux (Not⇩m True⇩m) num_vars = WEST_reg_aux False⇩m num_vars"
  | "WEST_reg_aux (Not⇩m False⇩m) num_vars = WEST_reg_aux True⇩m num_vars"
  | "WEST_reg_aux (Not⇩m (φ And⇩m ψ)) num_vars = WEST_reg_aux ((Not⇩m φ) Or⇩m (Not⇩m ψ)) num_vars"
  | "WEST_reg_aux (Not⇩m (φ Or⇩m ψ)) num_vars = WEST_reg_aux ((Not⇩m φ) And⇩m (Not⇩m ψ)) num_vars"
  | "WEST_reg_aux (Not⇩m (F⇩m[a,b] φ)) num_vars = WEST_reg_aux (G⇩m[a,b] (Not⇩m φ)) num_vars"
  | "WEST_reg_aux (Not⇩m (G⇩m[a,b] φ)) num_vars = WEST_reg_aux (F⇩m[a,b] (Not⇩m φ)) num_vars"
  | "WEST_reg_aux (Not⇩m (φ U⇩m[a,b] ψ)) num_vars = WEST_reg_aux ((Not⇩m φ) R⇩m[a,b] (Not⇩m ψ)) num_vars"
  | "WEST_reg_aux (Not⇩m (φ R⇩m[a,b] ψ)) num_vars = WEST_reg_aux ((Not⇩m φ) U⇩m[a,b] (Not⇩m ψ)) num_vars"
  | "WEST_reg_aux (Not⇩m (Not⇩m φ)) num_vars = WEST_reg_aux φ num_vars"
   using exhaustive convert_nnf.cases using exhaustive apply (smt (z3)) (* May take a second to load *)
  defer apply blast apply simp_all .
termination
  apply (relation "measure (λ(F,num_vars). (WEST_termination_measure F))")
  using WEST_termination_measure_not by simp_all


fun WEST_num_vars:: "(nat) mltl ⇒ nat"
  where "WEST_num_vars True⇩m = 1"
  | "WEST_num_vars False⇩m = 1"
  | "WEST_num_vars (Prop⇩m (p)) = p+1"
  | "WEST_num_vars (Not⇩m φ) = WEST_num_vars φ"
  | "WEST_num_vars (φ And⇩m ψ) = Max {(WEST_num_vars φ), (WEST_num_vars ψ)}"
  | "WEST_num_vars (φ Or⇩m ψ) = Max {(WEST_num_vars φ), (WEST_num_vars ψ)}"
  | "WEST_num_vars (F⇩m[a,b] φ) = WEST_num_vars φ"
  | "WEST_num_vars (G⇩m[a,b] φ) = WEST_num_vars φ"
  | "WEST_num_vars (φ U⇩m[a,b] ψ) = Max {(WEST_num_vars φ), (WEST_num_vars ψ)}"
  | "WEST_num_vars (φ R⇩m[a,b] ψ) = Max {(WEST_num_vars φ), (WEST_num_vars ψ)}"


fun WEST_reg:: "(nat) mltl ⇒ WEST_regex"
  where "WEST_reg F = (let nnf_F = convert_nnf F in WEST_reg_aux nnf_F (WEST_num_vars F))"

subsubsection ‹ Adding padding ›
fun pad_WEST_reg:: "nat mltl ⇒ WEST_regex"
  where "pad_WEST_reg φ = (let unpadded = WEST_reg φ in
                               (let complen = complen_mltl φ in
                                (let num_vars = WEST_num_vars φ in
                                (map (λ L. (if (length L < complen)then (pad L num_vars (complen-(length L))) else L))) unpadded)))"

fun simp_pad_WEST_reg:: "nat mltl ⇒ WEST_regex"
  where "simp_pad_WEST_reg φ = WEST_simp (pad_WEST_reg φ) (WEST_num_vars φ)"


section ‹ Some examples and Code Export ›

text ‹ Base cases ›
value "WEST_reg True⇩m"
value "WEST_reg False⇩m"
value "WEST_reg (Prop⇩m (1))"
value "WEST_reg (Not⇩m (Prop⇩m (0)))"

text ‹ Test cases for recursion ›
value "WEST_reg ((Not⇩m (Prop⇩m (0))) And⇩m (Prop⇩m (1)))"
value "WEST_reg (F⇩m[0,2] (Prop⇩m (1)))"
value "WEST_reg ((Not⇩m (Prop⇩m (0))) Or⇩m (Prop⇩m (0)))"

value "pad_WEST_reg ((Prop⇩m (0)) U⇩m[0,2] (Prop⇩m (0)))"
value "simp_pad_WEST_reg ((Prop_mltl 0) U⇩m[0,2] (Prop_mltl 0))"

export_code WEST_reg in Haskell module_name WEST
export_code simp_pad_WEST_reg in Haskell module_name WEST_simp_pad

end