Theory OFSM_Tables_Refined

section ‹Alternative OFSM Table Computation›

text ‹The approach to computing OFSM tables presented in the imported theories is easy to use in 
      proofs but inefficient in practice due to repeated recomputation of the same tables.
      Thus, in the following we present a more efficient method for computing and storing tables.›

theory OFSM_Tables_Refined
imports Minimisation Distinguishability 
begin

subsection ‹Computing a List of all OFSM Tables›

type_synonym ('a,'b,'c) ofsm_table = "('a, 'a set) mapping"

fun initial_ofsm_table :: "('a::linorder,'b,'c) fsm ⇒ ('a,'b,'c) ofsm_table" where
  "initial_ofsm_table M = Mapping.tabulate (states_as_list M) (λq . states M)"


abbreviation "ofsm_lookup ≡ Mapping.lookup_default {}"

lemma initial_ofsm_table_lookup_invar: "ofsm_lookup (initial_ofsm_table M) q = ofsm_table M (λq . states M) 0 q"
proof (cases "q ∈ states M")
  case True 
  then have "q ∈ list.set (states_as_list M)"
    using states_as_list_set by auto 
  then have "Mapping.lookup (initial_ofsm_table M) q = Some (states M)"
    unfolding initial_ofsm_table.simps
    by (simp add: lookup_tabulate) 
  then have "ofsm_lookup (initial_ofsm_table M) q = states M"
    by (simp add: lookup_default_def) 
  then show ?thesis 
    using True by auto
next
  case False
  then have "q ∉ list.set (states_as_list M)"
    using states_as_list_set by auto 
  then have "Mapping.lookup (initial_ofsm_table M) q = None"
    unfolding initial_ofsm_table.simps
    by (simp add: lookup_tabulate) 
  then have "ofsm_lookup (initial_ofsm_table M) q = {}"
    by (simp add: lookup_default_def)
  then show ?thesis 
    using False by auto
qed


lemma initial_ofsm_table_keys_invar: "Mapping.keys (initial_ofsm_table M) = states M"
  using states_as_list_set[of M]
  by simp 


fun next_ofsm_table :: "('a::linorder,'b,'c) fsm ⇒ ('a,'b,'c) ofsm_table ⇒ ('a,'b,'c) ofsm_table" where
  "next_ofsm_table M prev_table = Mapping.tabulate (states_as_list M) (λ q . {q' ∈ ofsm_lookup prev_table q . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_lookup prev_table qT = ofsm_lookup prev_table qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None) })"

lemma h_obs_non_state :
  assumes "q ∉ states M"
  shows "h_obs M q x y = None"
proof -
  have *:"⋀ x . h M (q,x) = {}"
    using assms fsm_transition_source
    unfolding h_simps 
    by force
  show ?thesis
    unfolding h_obs_simps Let_def *
    by (simp add: Set.filter_def) 
qed


lemma next_ofsm_table_lookup_invar: 
  assumes "⋀ q . ofsm_lookup prev_table q = ofsm_table M (λq . states M) k q"
  shows "ofsm_lookup (next_ofsm_table M prev_table) q = ofsm_table M (λq . states M) (Suc k) q"
proof (cases "q ∈ states M")
  case True 

  let ?prev_table = "ofsm_table M (λq . states M) k"

  from True have "q ∈ list.set (states_as_list M)"
    using states_as_list_set by auto 
  then have "Mapping.lookup (next_ofsm_table M prev_table) q = Some {q' ∈ ofsm_lookup prev_table q . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_lookup prev_table qT = ofsm_lookup prev_table qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None) }"
    unfolding next_ofsm_table.simps
    by (meson lookup_tabulate states_as_list_distinct)
  then have "ofsm_lookup (next_ofsm_table M prev_table) q = {q' ∈ ofsm_lookup prev_table q . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ofsm_lookup prev_table qT = ofsm_lookup prev_table qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None) }"
    by (simp add: lookup_default_def)
  also have "… = {q' ∈ ?prev_table q . ∀ x ∈ inputs M . ∀ y ∈ outputs M . (case h_obs M q x y of Some qT ⇒ (case h_obs M q' x y of Some qT' ⇒ ?prev_table qT = ?prev_table qT' | None ⇒ False) | None ⇒ h_obs M q' x y = None) }" 
    unfolding assms by presburger
  also have "… = ofsm_table M (λq . states M) (Suc k) q"
    unfolding ofsm_table.simps Let_def by presburger
  finally show ?thesis .
next
  case False
  then have "q ∉ list.set (states_as_list M)"
    using states_as_list_set by auto 
  then have "Mapping.lookup (next_ofsm_table M prev_table) q = None"
    by (simp add: lookup_tabulate)
  then have "ofsm_lookup (next_ofsm_table M prev_table) q = {}"
    by (simp add: lookup_default_def)
  then show ?thesis
    unfolding ofsm_table_non_state[OF False] .
qed

lemma next_ofsm_table_keys_invar: "Mapping.keys (next_ofsm_table M prev_table) = states M"
  using states_as_list_set[of M]
  by simp 


fun compute_ofsm_table_list :: "('a::linorder,'b,'c) fsm ⇒ nat ⇒ ('a,'b,'c) ofsm_table list" where
  "compute_ofsm_table_list M k = rev (foldr (λ _ prev . (next_ofsm_table M (hd prev)) # prev) [0..<k] [initial_ofsm_table M])"


lemma compute_ofsm_table_list_props:
  "length (compute_ofsm_table_list M k) = Suc k"
  "⋀ i q . i < Suc k ⟹ ofsm_lookup ((compute_ofsm_table_list M k) ! i) q = ofsm_table M (λq . states M) i q"
  "⋀ i . i < Suc k ⟹ Mapping.keys ((compute_ofsm_table_list M k) ! i) = states M"
proof -

  define t where "t = (λ k . (foldr (λ _ prev . (next_ofsm_table M (hd prev)) # prev) (rev [0..<k]) [initial_ofsm_table M]))"

  have t_props:"length (t k) = Suc k
          ∧ (∀ i q . i < Suc k ⟶ ofsm_lookup (t k ! (k-i)) q = ofsm_table M (λq . states M) i q)
          ∧ (∀ i . i < Suc k ⟶ Mapping.keys (t k ! i) = states M)"
  proof (induction k)
    case 0
    have "t 0 = [initial_ofsm_table M]"
      unfolding t_def by auto
    show ?case 
      unfolding ‹t 0 = [initial_ofsm_table M]›
      using initial_ofsm_table_lookup_invar[of M]
      using initial_ofsm_table_keys_invar[of M]
      by auto
  next
    case (Suc k)

    have "rev [0..<Suc k] = k # (rev [0..<k])"
      by auto
    have *: "t (Suc k) = (next_ofsm_table M (hd (t k))) # (t k)"
      unfolding t_def ‹rev [0..<Suc k] = k # (rev [0..<k])›
      by auto

    have IH1: "length (t k) = Suc k"
    and  IH2: "⋀i q . i < Suc k ⟹ ofsm_lookup (t k ! (k-i)) q = ofsm_table M (λq. FSM.states M) i q"
    and  IH3: "⋀i . i < Suc k ⟹ Mapping.keys (t k ! i) = FSM.states M"
      using Suc.IH by blast+

    have "length (t (Suc k)) = Suc (Suc k)"
      using IH1 unfolding * by auto
    moreover have "⋀i q . i < Suc (Suc k) ⟹ ofsm_lookup (t (Suc k) ! ((Suc k)-i)) q = ofsm_table M (λq. FSM.states M) i q"
    proof -
      fix i q assume "i < Suc (Suc k)"
      then consider "i = Suc k" | "i < Suc k"
        using less_Suc_eq by blast
      then show "ofsm_lookup (t (Suc k) ! ((Suc k)-i)) q = ofsm_table M (λq. FSM.states M) i q" proof cases
        case 1
        then have "(t (Suc k) ! ((Suc k)-i)) = hd (t (Suc k))"
          by (metis "*" diff_self_eq_0 list.sel(1) nth_Cons_0)          
        then have "(t (Suc k) ! ((Suc k)-i)) = next_ofsm_table M (hd (t k))"
          unfolding * by (metis list.sel(1))
        then have "ofsm_lookup (t (Suc k) ! ((Suc k)-i)) q = ofsm_lookup (next_ofsm_table M (hd (t k))) q"
          by auto
        
        have "(hd (t k)) = (t k ! (k-k))"
          by (metis IH1 diff_self_eq_0 hd_conv_nth list.size(3) nat.simps(3))
        moreover have "k < Suc k" by auto
        ultimately have "ofsm_lookup (next_ofsm_table M (hd (t k))) q = ofsm_table M (λq. FSM.states M) i q"
          by (metis "1" IH2 next_ofsm_table_lookup_invar) 
        then show ?thesis
          unfolding ‹ofsm_lookup (t (Suc k) ! ((Suc k)-i)) q = ofsm_lookup (next_ofsm_table M (hd (t k))) q› .
      next
        case 2
        then have "((Suc k)-i) > 0"
          by auto
        then have "(t (Suc k) ! ((Suc k)-i)) = t k ! (((Suc k)-i) - 1)"
          unfolding * by (meson nth_Cons_pos)
        then have "(t (Suc k) ! ((Suc k)-i)) = t k ! (k-i)"
          by auto
        show "ofsm_lookup (t (Suc k) ! ((Suc k)-i)) q = ofsm_table M (λq. FSM.states M) i q"
          using IH2[OF 2]
          unfolding ‹(t (Suc k) ! ((Suc k)-i)) = t k ! (k-i)› by metis
      qed
    qed
    moreover have "⋀i . i < Suc (Suc k) ⟹ Mapping.keys (t (Suc k) ! i) = FSM.states M"
      by (metis "*" IH3 Suc_diff_1 Suc_less_eq less_Suc_eq_0_disj next_ofsm_table_keys_invar nth_Cons')
    ultimately show ?case
      by blast
  qed
          
  
  have *:"(compute_ofsm_table_list M k) = rev (t k)"
    unfolding compute_ofsm_table_list.simps t_def
    using foldr_length_helper[of "rev [0..<k]" "[0..<k]" "(λ prev . (next_ofsm_table M (hd prev)) # prev)", OF length_rev]
    by metis

  show "length (compute_ofsm_table_list M k) = Suc k"
    using t_props unfolding * length_rev by blast

  have "⋀ i . i < Suc k ⟹ (rev (t k) ! i) = t k ! (k - i)"
    by (simp add: rev_nth t_props)
  then show "⋀i q. i < Suc k ⟹
           ofsm_lookup (compute_ofsm_table_list M k ! i) q = ofsm_table M (λq. FSM.states M) i q"
    unfolding * using t_props
    by presburger 

  show "⋀i. i < Suc k ⟹ Mapping.keys (compute_ofsm_table_list M k ! i) = FSM.states M"
    unfolding * using t_props ‹⋀ i . i < Suc k ⟹ (rev (t k) ! i) = t k ! (k - i)›
    by simp 
qed
      
        
     

fun compute_ofsm_tables :: "('a::linorder,'b,'c) fsm ⇒ nat ⇒ (nat, ('a,'b,'c) ofsm_table) mapping" where
  "compute_ofsm_tables M k = Mapping.bulkload (compute_ofsm_table_list M k)"

lemma compute_ofsm_tables_entries :
  assumes "i < Suc k"
  shows "(the (Mapping.lookup (compute_ofsm_tables M k) i)) = ((compute_ofsm_table_list M k) ! i)"
  using assms 
  unfolding compute_ofsm_tables.simps bulkload_def
  by (metis bulkload.rep_eq bulkload_def compute_ofsm_table_list_props(1) lookup.rep_eq option.sel)

lemma compute_ofsm_tables_lookup_invar :
  assumes "i < Suc k"
  shows "ofsm_lookup (the (Mapping.lookup (compute_ofsm_tables M k) i)) q = ofsm_table M (λq . states M) i q"
  using compute_ofsm_table_list_props(2)[OF assms]
  unfolding compute_ofsm_tables_entries[OF assms] by metis

lemma compute_ofsm_tables_keys_invar :
  assumes "i < Suc k"
  shows "Mapping.keys (the (Mapping.lookup (compute_ofsm_tables M k) i)) = states M"
  using compute_ofsm_table_list_props(3)[OF assms]
  unfolding compute_ofsm_tables_entries[OF assms] by metis


subsection ‹Finding Diverging Tables›


lemma ofsm_table_fix_from_compute_ofsm_tables :
  assumes "q ∈ states M"
shows "ofsm_lookup (the (Mapping.lookup (compute_ofsm_tables M (size M - 1)) (size M - 1))) q = ofsm_table_fix M (λq. FSM.states M) 0 q" 
proof -
  have "((λq. FSM.states M) ` FSM.states M) = {states M}"
    using fsm_initial[of M] by auto
  then have "card ((λq. FSM.states M) ` FSM.states M) = 1"
    by auto
  
  have "ofsm_lookup (the (Mapping.lookup (compute_ofsm_tables M (size M - 1)) (size M - 1))) q = ofsm_table M (λq. FSM.states M) (FSM.size M - 1) q"
    using compute_ofsm_tables_lookup_invar[of "(size M - 1)" "(size M - 1)" M q]
    by linarith
  also have "… = ofsm_table_fix M (λq. FSM.states M) 0 q"
    using ofsm_table_fix_partition_fixpoint[OF minimise_initial_partition _ assms(1), of "size M"]
    unfolding ‹card ((λq. FSM.states M) ` FSM.states M) = 1›
    by blast
  finally show ?thesis .
qed

fun find_first_distinct_ofsm_table' :: "('a::linorder,'b,'c) fsm ⇒ 'a ⇒ 'a ⇒ nat" where
  "find_first_distinct_ofsm_table' M q1 q2 = (let 
    tables = (compute_ofsm_tables M (size M - 1))
in if (q1 ∈ states M 
      ∧ q2 ∈ states M 
      ∧ (ofsm_lookup (the (Mapping.lookup tables (size M - 1))) q1
         ≠ ofsm_lookup (the (Mapping.lookup tables (size M - 1))) q2))
  then the (find_index (λ i . ofsm_lookup (the (Mapping.lookup tables i)) q1 ≠ ofsm_lookup (the (Mapping.lookup tables i)) q2) [0..<size M])
  else 0)"





lemma find_first_distinct_ofsm_table_is_first' :
  assumes "q1 ∈ FSM.states M" 
      and "q2 ∈ FSM.states M"
      and "ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2"
    shows "(find_first_distinct_ofsm_table M q1 q2) = Min {k . ofsm_table M (λq . states M) k q1 ≠ ofsm_table M (λq . states M) k q2
                                                                ∧ (∀k' . k' < k ⟶ ofsm_table M (λq . states M) k' q1 = ofsm_table M (λq . states M) k' q2)}"
(is "find_first_distinct_ofsm_table M q1 q2 = Min ?ks")
proof -
  have "find_first_distinct_ofsm_table M q1 q2 ∈ ?ks"
    using find_first_distinct_ofsm_table_is_first[OF assms]
    by blast 
  moreover have "⋀ k . k ∈ ?ks ⟹ k = find_first_distinct_ofsm_table M q1 q2" 
    using calculation linorder_neqE_nat by blast
  ultimately have "?ks = {find_first_distinct_ofsm_table M q1 q2}"
    by blast
  then show ?thesis 
    by fastforce
qed

lemma find_first_distinct_ofsm_table'_is_first' :
  assumes "q1 ∈ FSM.states M" 
      and "q2 ∈ FSM.states M"
      and "ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2"
    shows "(find_first_distinct_ofsm_table' M q1 q2) = Min {k . ofsm_table M (λq . states M) k q1 ≠ ofsm_table M (λq . states M) k q2
                                                                ∧ (∀k' . k' < k ⟶ ofsm_table M (λq . states M) k' q1 = ofsm_table M (λq . states M) k' q2)}"
(is "find_first_distinct_ofsm_table' M q1 q2 = Min ?ks")
      and "find_first_distinct_ofsm_table' M q1 q2 ≤ size M - 1"
proof -

  define tables where "tables = compute_ofsm_tables M (FSM.size M - 1)"

  have "ofsm_lookup (the (Mapping.lookup tables (FSM.size M - 1))) q1 ≠
           ofsm_lookup (the (Mapping.lookup tables (FSM.size M - 1))) q2"
    unfolding tables_def                                        
    unfolding ofsm_table_fix_from_compute_ofsm_tables[OF assms(1)]
    unfolding ofsm_table_fix_from_compute_ofsm_tables[OF assms(2)]
    using assms(3) .

  then have "find_first_distinct_ofsm_table' M q1 q2 = the (find_index
                   (λi. ofsm_lookup (the (Mapping.lookup tables i)) q1 ≠
                        ofsm_lookup (the (Mapping.lookup tables i)) q2)
                   [0..<FSM.size M])"
    unfolding find_first_distinct_ofsm_table'.simps
    using assms(1,2,3) 
    unfolding Let_def tables_def[symmetric]
    by presburger

  have "FSM.size M - 1 ∈ set [0..<FSM.size M]"
    using fsm_size_Suc[of M] by auto
  then have *:"∃ k ∈ set [0..<FSM.size M] . (λi. ofsm_lookup (the (Mapping.lookup tables i)) q1 ≠
                        ofsm_lookup (the (Mapping.lookup tables i)) q2) k"
    using ‹ofsm_lookup (the (Mapping.lookup tables (FSM.size M - 1))) q1 ≠
           ofsm_lookup (the (Mapping.lookup tables (FSM.size M - 1))) q2›
    by blast
  have "find_index
                   (λi. ofsm_lookup (the (Mapping.lookup tables i)) q1 ≠
                        ofsm_lookup (the (Mapping.lookup tables i)) q2)
                   [0..<FSM.size M] ≠ None"
    using find_index_exhaustive[OF *] .
  then obtain k where *:"find_index
                   (λi. ofsm_lookup (the (Mapping.lookup tables i)) q1 ≠
                        ofsm_lookup (the (Mapping.lookup tables i)) q2)
                   [0..<FSM.size M] = Some k"
    by blast
  then have "find_first_distinct_ofsm_table' M q1 q2 = k"
    unfolding ‹find_first_distinct_ofsm_table' M q1 q2 = the (find_index
                   (λi. ofsm_lookup (the (Mapping.lookup tables i)) q1 ≠
                        ofsm_lookup (the (Mapping.lookup tables i)) q2)
                   [0..<FSM.size M])›
    by auto

  have "⋀ k' . k' ≤ k ⟹ [0..<FSM.size M] ! k' = k'" 
    using find_index_index(1)[OF *]
    by (metis add.left_neutral diff_zero dual_order.trans length_upt not_le nth_upt) 
  then have "[0..<FSM.size M] ! k = k" and "⋀ k' . k' < k ⟹ [0..<FSM.size M] ! k' = k'"
    by auto
  have "k < Suc (size M - 1)"
    using find_index_index(1)[OF *]
    by auto
  
  have "ofsm_lookup (the (Mapping.lookup tables k)) q1 ≠ ofsm_lookup (the (Mapping.lookup tables k)) q2"
    using find_index_index(2)[OF *] 
    unfolding ‹[0..<FSM.size M] ! k = k› .
  then have p1: "ofsm_table M (λq . states M) k q1 ≠ ofsm_table M (λq . states M) k q2"
    unfolding tables_def
    unfolding compute_ofsm_tables_lookup_invar[OF ‹k < Suc (size M - 1)›] .

    
  have "⋀ k' . k' < k ⟹ ofsm_lookup (the (Mapping.lookup tables k')) q1 = ofsm_lookup (the (Mapping.lookup tables k')) q2"
    using ‹⋀ k' . k' < k ⟹ [0..<FSM.size M] ! k' = k'›
    using find_index_index(3)[OF *] 
    by auto
  then have p2: "(∀k' . k' < k ⟶ ofsm_table M (λq . states M) k' q1 = ofsm_table M (λq . states M) k' q2)"
    unfolding tables_def
    using compute_ofsm_tables_lookup_invar[of _ "(size M - 1)" M ] ‹k < Suc (size M - 1)›
    using less_trans by blast

  have "k ∈ ?ks"
    using p1 p2 by blast
  moreover have "⋀ k' . k' ∈ ?ks ⟹ k' = k"
    using calculation linorder_neqE_nat by blast
  ultimately have "?ks = {k}"
    by blast
  then show "find_first_distinct_ofsm_table' M q1 q2 = Min ?ks" 
    unfolding ‹find_first_distinct_ofsm_table' M q1 q2 = k›
    by fastforce

  show "find_first_distinct_ofsm_table' M q1 q2 ≤ FSM.size M - 1"
    unfolding ‹find_first_distinct_ofsm_table' M q1 q2 = k›
    using ‹k < Suc (size M - 1)›
    by auto
qed

lemma find_first_distinct_ofsm_table'_max : 
  "find_first_distinct_ofsm_table' M q1 q2 ≤ size M - 1"
proof (cases "q1 ∈ states M 
      ∧ q2 ∈ states M 
      ∧ (ofsm_lookup (the (Mapping.lookup (compute_ofsm_tables M (size M - 1)) (size M - 1))) q1
         ≠ ofsm_lookup (the (Mapping.lookup (compute_ofsm_tables M (size M - 1)) (size M - 1))) q2)")
  case True
  then show ?thesis using find_first_distinct_ofsm_table'_is_first'(2)[of q1 M q2]
    using ofsm_table_fix_from_compute_ofsm_tables by blast
next
  case False
  then have "find_first_distinct_ofsm_table' M q1 q2 = 0"
    unfolding find_first_distinct_ofsm_table'.simps Let_def by meson
  then show ?thesis 
    by linarith
qed



lemma find_first_distinct_ofsm_table_alt_def:
  "find_first_distinct_ofsm_table M q1 q2 = find_first_distinct_ofsm_table' M q1 q2"
proof (cases "q1 ∈ states M ∧ q2 ∈ states M ∧ ((ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2))")
  case True
  then have **: "q1 ∈ states M"
       and  ***: "q2 ∈ states M"
       and  ****: "(ofsm_table_fix M (λq . states M) 0 q1 ≠ ofsm_table_fix M (λq . states M) 0 q2)"
    by blast+
  show ?thesis 
    unfolding find_first_distinct_ofsm_table'_is_first'[OF ** *** ****]
    unfolding find_first_distinct_ofsm_table_is_first'[OF ** *** ****]
    by presburger
next
  case False

  have "find_first_distinct_ofsm_table M q1 q2 = 0"
    by (meson False find_first_distinct_ofsm_table_gt.simps)
  moreover have "find_first_distinct_ofsm_table' M q1 q2 = 0"
  proof (cases "q1 ∈ states M ∧ q2 ∈ states M")
    case True
    then have **: "q1 ∈ states M"
         and  ***: "q2 ∈ states M"
      by blast+
    then have ****:"((ofsm_table_fix M (λq . states M) 0 q1 = ofsm_table_fix M (λq . states M) 0 q2))"
      using False by blast

    define tables where "tables = compute_ofsm_tables M (FSM.size M - 1)"

    have "ofsm_lookup (the (Mapping.lookup tables (FSM.size M - 1))) q1 =
             ofsm_lookup (the (Mapping.lookup tables (FSM.size M - 1))) q2"
      unfolding tables_def
      unfolding ofsm_table_fix_from_compute_ofsm_tables[OF **]
      unfolding ofsm_table_fix_from_compute_ofsm_tables[OF ***]
      using **** .
    then show ?thesis 
      unfolding find_first_distinct_ofsm_table'.simps Let_def tables_def[symmetric] by auto
  next
    case False
    then show ?thesis 
      unfolding find_first_distinct_ofsm_table'.simps Let_def 
      by meson
  qed
  ultimately show ?thesis
    by presburger
qed


subsection ‹Refining the Computation of Distinguishing Traces via OFSM Tables›

fun select_diverging_ofsm_table_io' :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ ('b × 'c) × ('a option × 'a option)" where
  "select_diverging_ofsm_table_io' M q1 q2 k = (let
      tables = (compute_ofsm_tables M (size M - 1));
      ins = inputs_as_list M;
      outs = outputs_as_list M;
      table = ofsm_lookup (the (Mapping.lookup tables (k-1)));
      f = (λ (x,y) . case (h_obs M q1 x y, h_obs M q2 x y) 
                   of
                      (Some q1', Some q2')  ⇒ if table q1' ≠ table q2'
                                                  then Some ((x,y),(Some q1', Some q2'))
                                                  else None |
                      (None,None)           ⇒ None |
                      (Some q1', None)      ⇒ Some ((x,y),(Some q1', None)) |
                      (None, Some q2')      ⇒ Some ((x,y),(None, Some q2')))
      in 
        hd (List.map_filter f (List.product ins outs)))" 

lemma select_diverging_ofsm_table_io_alt_def :
  assumes "k ≤ size M - 1"
  shows "select_diverging_ofsm_table_io M q1 q2 k = select_diverging_ofsm_table_io' M q1 q2 k"
proof -
  define tables where "tables = compute_ofsm_tables M (FSM.size M - 1)"
  define table where "table = ofsm_lookup (the (Mapping.lookup tables (k-1)))"

  have "k - 1 < Suc (size M - 1)"
    using assms by auto
  have "ofsm_table M (λq . states M) (k-1) = table"
    unfolding table_def tables_def
    unfolding compute_ofsm_tables_lookup_invar[OF ‹k - 1 < Suc (size M - 1)›]
    by presburger

  show ?thesis 
    unfolding select_diverging_ofsm_table_io'.simps
              select_diverging_ofsm_table_io.simps
              Let_def
    unfolding tables_def[symmetric] table_def[symmetric]
    unfolding ‹ofsm_table M (λq . states M) (k-1) = table›
    by meson
qed

fun assemble_distinguishing_sequence_from_ofsm_table' :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ ('b × 'c) list" where
  "assemble_distinguishing_sequence_from_ofsm_table' M q1 q2 0 = []" | 
  "assemble_distinguishing_sequence_from_ofsm_table' M q1 q2 (Suc k) = (case 
      select_diverging_ofsm_table_io' M q1 q2 (Suc k) 
    of
      ((x,y),(Some q1',Some q2')) ⇒ (x,y) # (assemble_distinguishing_sequence_from_ofsm_table' M q1' q2' k) |
      ((x,y),_)                   ⇒ [(x,y)])"

lemma assemble_distinguishing_sequence_from_ofsm_table_alt_def :
  assumes "k ≤ size M - 1"
  shows "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k = assemble_distinguishing_sequence_from_ofsm_table' M q1 q2 k"
using assms proof (induction k arbitrary: q1 q2)
  case 0
  show ?case 
    unfolding assemble_distinguishing_sequence_from_ofsm_table.simps
    unfolding assemble_distinguishing_sequence_from_ofsm_table'.simps    
    by presburger
next
  case (Suc k)
  then have "k ≤ FSM.size M - 1"
    by auto
  show ?case 
    unfolding assemble_distinguishing_sequence_from_ofsm_table.simps
    unfolding assemble_distinguishing_sequence_from_ofsm_table'.simps
    unfolding select_diverging_ofsm_table_io_alt_def[OF ‹Suc k ≤ FSM.size M - 1›]
    unfolding Suc.IH[OF ‹k ≤ FSM.size M - 1›]
    by meson
qed

fun get_distinguishing_sequence_from_ofsm_tables_refined :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ 'a ⇒ ('b × 'c) list" where
  "get_distinguishing_sequence_from_ofsm_tables_refined M q1 q2 = (let
      k = find_first_distinct_ofsm_table' M q1 q2
  in assemble_distinguishing_sequence_from_ofsm_table' M q1 q2 k)"

lemma get_distinguishing_sequence_from_ofsm_tables_refined_alt_def :
  "get_distinguishing_sequence_from_ofsm_tables_refined M q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q1 q2"
proof -
  define k where "k = find_first_distinct_ofsm_table' M q1 q2"
  then have "k ≤ size M - 1"
    using find_first_distinct_ofsm_table'_max by metis
  have "find_first_distinct_ofsm_table M q1 q2 = k"
    unfolding k_def find_first_distinct_ofsm_table_alt_def
    by meson
                                                           
  show ?thesis 
    unfolding get_distinguishing_sequence_from_ofsm_tables_refined.simps
    unfolding get_distinguishing_sequence_from_ofsm_tables.simps
    unfolding Let_def
    unfolding k_def[symmetric] ‹find_first_distinct_ofsm_table M q1 q2 = k›
    unfolding assemble_distinguishing_sequence_from_ofsm_table_alt_def[OF ‹k ≤ size M - 1›]
    by meson
qed

lemma get_distinguishing_sequence_from_ofsm_tables_refined_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "q1 ∈ states M"
  and     "q2 ∈ states M"
  and     "q1 ≠ q2"
shows "distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables_refined M q1 q2)"
  unfolding get_distinguishing_sequence_from_ofsm_tables_refined_alt_def
  using get_distinguishing_sequence_from_ofsm_tables_distinguishes[OF assms] .



fun select_diverging_ofsm_table_io_with_provided_tables :: "(nat, ('a,'b,'c) ofsm_table) mapping ⇒ ('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ ('b × 'c) × ('a option × 'a option)" where
  "select_diverging_ofsm_table_io_with_provided_tables tables M q1 q2 k = (let
      ins = inputs_as_list M;
      outs = outputs_as_list M;
      table = ofsm_lookup (the (Mapping.lookup tables (k-1)));
      f = (λ (x,y) . case (h_obs M q1 x y, h_obs M q2 x y) 
                   of
                      (Some q1', Some q2')  ⇒ if table q1' ≠ table q2'
                                                  then Some ((x,y),(Some q1', Some q2'))
                                                  else None |
                      (None,None)           ⇒ None |
                      (Some q1', None)      ⇒ Some ((x,y),(Some q1', None)) |
                      (None, Some q2')      ⇒ Some ((x,y),(None, Some q2')))
      in 
        hd (List.map_filter f (List.product ins outs)))"

lemma select_diverging_ofsm_table_io_with_provided_tables_simp :
  "select_diverging_ofsm_table_io_with_provided_tables (compute_ofsm_tables M (size M - 1)) M = select_diverging_ofsm_table_io' M"
  unfolding select_diverging_ofsm_table_io_with_provided_tables.simps
            select_diverging_ofsm_table_io'.simps
            Let_def 
  by meson

fun assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables :: "(nat, ('a,'b,'c) ofsm_table) mapping ⇒ ('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ 'a ⇒ nat ⇒ ('b × 'c) list" where
  "assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables tables M q1 q2 0 = []" | 
  "assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables tables M q1 q2 (Suc k) = (case 
      select_diverging_ofsm_table_io_with_provided_tables tables M q1 q2 (Suc k) 
    of
      ((x,y),(Some q1',Some q2')) ⇒ (x,y) # (assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables tables M q1' q2' k) |
      ((x,y),_)                   ⇒ [(x,y)])"

lemma assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables_simp :
  "assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables (compute_ofsm_tables M (size M - 1)) M q1 q2 k= assemble_distinguishing_sequence_from_ofsm_table' M q1 q2 k"
proof (induction k arbitrary: q1 q2)
  case 0
  show ?case
    unfolding assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables.simps
              assemble_distinguishing_sequence_from_ofsm_table'.simps
              Let_def 
    by meson  
next
  case (Suc k')
  show ?case
    unfolding assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables.simps
    unfolding assemble_distinguishing_sequence_from_ofsm_table'.simps
    unfolding Let_def select_diverging_ofsm_table_io_with_provided_tables_simp Suc.IH
    by meson  
qed
  

lemma get_distinguishing_sequence_from_ofsm_tables_refined_code[code] :
  "get_distinguishing_sequence_from_ofsm_tables_refined M q1 q2 = (let
      tables = (compute_ofsm_tables M (size M - 1));
      k = (if (q1 ∈ states M 
                ∧ q2 ∈ states M 
                ∧ (ofsm_lookup (the (Mapping.lookup tables (size M - 1))) q1
                   ≠ ofsm_lookup (the (Mapping.lookup tables (size M - 1))) q2))
            then the (find_index (λ i . ofsm_lookup (the (Mapping.lookup tables i)) q1 ≠ ofsm_lookup (the (Mapping.lookup tables i)) q2) [0..<size M])
            else 0)
  in assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables tables M q1 q2 k)"
  unfolding get_distinguishing_sequence_from_ofsm_tables_refined.simps
            find_first_distinct_ofsm_table'.simps
            Let_def 
            assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables_simp
  by meson

fun get_distinguishing_sequence_from_ofsm_tables_with_provided_tables :: "(nat, ('a,'b,'c) ofsm_table) mapping ⇒ ('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 'a ⇒ 'a ⇒ ('b × 'c) list" where
  "get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2 = (let
      k = (if (q1 ∈ states M 
                ∧ q2 ∈ states M 
                ∧ (ofsm_lookup (the (Mapping.lookup tables (size M - 1))) q1
                   ≠ ofsm_lookup (the (Mapping.lookup tables (size M - 1))) q2))
            then the (find_index (λ i . ofsm_lookup (the (Mapping.lookup tables i)) q1 ≠ ofsm_lookup (the (Mapping.lookup tables i)) q2) [0..<size M])
            else 0)
  in assemble_distinguishing_sequence_from_ofsm_table_with_provided_tables tables M q1 q2 k)"

lemma get_distinguishing_sequence_from_ofsm_tables_with_provided_tables_simp :
  "get_distinguishing_sequence_from_ofsm_tables_with_provided_tables (compute_ofsm_tables M (size M - 1)) M = get_distinguishing_sequence_from_ofsm_tables_refined M"
  unfolding get_distinguishing_sequence_from_ofsm_tables_with_provided_tables.simps
            get_distinguishing_sequence_from_ofsm_tables_refined_code
            Let_def
  by meson


lemma get_distinguishing_sequence_from_ofsm_tables_precomputed:
  "get_distinguishing_sequence_from_ofsm_tables M = (let 
      tables = (compute_ofsm_tables M (size M - 1));
      distMap = mapping_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2))
                        (filter (λ qq . fst qq ≠ snd qq) (List.product (states_as_list M) (states_as_list M))));
      distHelper = (λ q1 q2 . if q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2)
    in distHelper)"
proof -
  define distStates where "distStates = (filter (λ qq . fst qq ≠ snd qq) (List.product (states_as_list M) (states_as_list M)))"

  define distMap where distMap_orig: "distMap = mapping_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables (compute_ofsm_tables M (size M - 1)) M q1 q2))
                                    distStates)"

  have "distinct distStates"
    unfolding distStates_def using states_as_list_distinct
    using distinct_filter distinct_product by blast 
  then have "distinct (map fst (map (λ(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables M q1 q2)) distStates))"
    unfolding map_pair_fst_helper .  
  then have distMap_def: "Mapping.lookup distMap = map_of (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables M q1 q2))
                                          distStates)"
    unfolding distMap_orig get_distinguishing_sequence_from_ofsm_tables_with_provided_tables_simp 
              get_distinguishing_sequence_from_ofsm_tables_refined_alt_def
    using mapping_of_map_of
    by blast     

  define distHelper where "distHelper = (λ q1 q2 . if q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2)"

  have "distHelper = get_distinguishing_sequence_from_ofsm_tables M"
  proof -
    have "⋀ q1 q2 . distHelper q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q1 q2"
    proof -
      fix q1 q2
      show "distHelper q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q1 q2" 
      proof (cases "q1 ∈ states M ∧ q2 ∈ states M ∧ q1 ≠ q2")
        case False
        then show ?thesis 
          unfolding distHelper_def by metis 
      next
        case True
        then have *:"(q1,q2) ∈ list.set distStates"
          using states_as_list_set unfolding distStates_def by fastforce
        
        have "distinct (map fst (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables M q1 q2)) distStates))"
        proof -
          have **: "(map fst (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables M q1 q2)) distStates)) = distStates"
          proof (induction distStates)
            case Nil
            then show ?case by auto
          next
            case (Cons a distStates)
            obtain x y where "a = (x,y)"
              using surjective_pairing by blast
            show ?case 
              using Cons unfolding ‹a = (x,y)› by auto
          qed

          show ?thesis
            unfolding **
            unfolding distStates_def
            by (simp add: distinct_product) 
        qed

        have "((q1,q2), get_distinguishing_sequence_from_ofsm_tables M q1 q2) ∈ list.set (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables M q1 q2)) distStates)"
          using Util.map_set[OF *, of "(λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables M q1 q2))"]
          by force
        then have "the (Mapping.lookup distMap (q1,q2)) = get_distinguishing_sequence_from_ofsm_tables M q1 q2"
          unfolding distMap_def 
          unfolding Map.map_of_eq_Some_iff[OF ‹distinct (map fst (map (λ (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables M q1 q2)) distStates))›, symmetric]
          by (metis option.sel)
        moreover have "distHelper q1 q2 = the (Mapping.lookup distMap (q1,q2))"
          using True unfolding distHelper_def by metis
        ultimately show ?thesis 
          by presburger
      qed
    qed
    then show ?thesis 
      by blast
  qed

  then show ?thesis
    unfolding distHelper_def distMap_orig distStates_def Let_def
    by presburger
qed 


lemma get_distinguishing_sequence_from_ofsm_tables_with_provided_tables_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "q1 ∈ states M"
  and     "q2 ∈ states M"
  and     "q1 ≠ q2"
shows "distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables_with_provided_tables (compute_ofsm_tables M (size M - 1)) M q1 q2)"
  unfolding get_distinguishing_sequence_from_ofsm_tables_with_provided_tables_simp
  using get_distinguishing_sequence_from_ofsm_tables_refined_distinguishes[OF assms] .

subsection ‹Refining Minimisation›

fun minimise_refined :: "('a :: linorder,'b :: linorder,'c :: linorder) fsm ⇒ ('a set,'b,'c) fsm" where
  "minimise_refined M = (let
      tables = (compute_ofsm_tables M (size M - 1));
      eq_class = (ofsm_lookup (the (Mapping.lookup tables (size M - 1))));
      ts = (λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) ` (transitions M);
      q0 = eq_class (initial M);
      eq_states = eq_class |`| fstates M;
      M' = create_unconnected_fsm_from_fsets q0 eq_states (finputs M) (foutputs M)
  in add_transitions M' ts)"

lemma minimise_refined_is_minimise[code] : "minimise M = minimise_refined M"
proof -
  define tables where "tables = compute_ofsm_tables M (FSM.size M - 1)"
  define eq_class_refined where "eq_class_refined = (ofsm_lookup (the (Mapping.lookup tables (size M - 1))))"
  define eq_class where "eq_class = ofsm_table_fix M (λq . states M) 0"

  have "(size M - 1) < Suc (size M - 1)"
    by auto
  have "⋀ q . q ∈ states M ⟹ eq_class q = eq_class_refined q"
    unfolding eq_class_def eq_class_refined_def tables_def
    unfolding compute_ofsm_tables_lookup_invar[OF ‹(size M - 1) < Suc (size M - 1)›]
    by (metis ofsm_table_fix_partition_fixpoint_trivial_partition)


  have ts: "(λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) ` (transitions M)
        = (λ t . (eq_class_refined (t_source t), t_input t, t_output t, eq_class_refined (t_target t))) ` (transitions M)"
    using ‹⋀ q . q ∈ states M ⟹ eq_class q = eq_class_refined q›[OF fsm_transition_source]
    using ‹⋀ q . q ∈ states M ⟹ eq_class q = eq_class_refined q›[OF fsm_transition_target]
    by auto

  have q0: "eq_class (initial M) = eq_class_refined (initial M)"
    using ‹⋀ q . q ∈ states M ⟹ eq_class q = eq_class_refined q›[OF fsm_initial] .

  have eq_states: "eq_class |`| fstates M = eq_class_refined |`| fstates M"
    using fstates_set[of M]
    using ‹⋀ q . q ∈ states M ⟹ eq_class q = eq_class_refined q›
    by (metis fset.map_cong) 

  have M': "create_unconnected_fsm_from_fsets (eq_class (initial M)) (eq_class |`| fstates M) (finputs M) (foutputs M) 
            = create_unconnected_fsm_from_fsets (eq_class_refined (initial M)) (eq_class_refined |`| fstates M) (finputs M) (foutputs M)"
    unfolding q0 eq_states by meson
  
  have res: "add_transitions (create_unconnected_fsm_from_fsets (eq_class (initial M)) (eq_class |`| fstates M) (finputs M) (foutputs M)) ((λ t . (eq_class (t_source t), t_input t, t_output t, eq_class (t_target t))) ` (transitions M))
              = add_transitions (create_unconnected_fsm_from_fsets (eq_class_refined (initial M)) (eq_class_refined |`| fstates M) (finputs M) (foutputs M)) ((λ t . (eq_class_refined (t_source t), t_input t, t_output t, eq_class_refined (t_target t))) ` (transitions M))"
    unfolding M' ts by meson

  show ?thesis
    unfolding minimise.simps minimise_refined.simps Let_def
    unfolding eq_class_def[symmetric]
    unfolding tables_def[symmetric] eq_class_refined_def[symmetric]
    unfolding res 
    by meson
qed

end