Theory FSM_Code_Datatype

section ‹Data Refinement on FSM Representations›

text ‹This section introduces a refinement of the type of finite state machines for 
      code generation, maintaining mappings to access the transition relation to
      avoid repeated computations.›

theory FSM_Code_Datatype
imports FSM "HOL-Library.Mapping" Containers.Containers 
begin

subsection ‹Mappings and Function @{text "h"}›

fun list_as_mapping :: "('a × 'c) list ⇒ ('a,'c set) mapping" where
  "list_as_mapping xs = (foldr (λ (x,z) m . case Mapping.lookup m x of
                                                None ⇒ Mapping.update x {z} m |
                                                Some zs ⇒ Mapping.update x (insert z zs) m)
                                xs
                                Mapping.empty)"


lemma list_as_mapping_lookup: 
  fixes xs :: "('a × 'c) list"
  shows "(Mapping.lookup (list_as_mapping xs)) = (λ x . if (∃ z . (x,z) ∈ (set xs)) then Some {z . (x,z) ∈ (set xs)} else None)"
proof - 
  let ?P = "λm :: ('a,'c set) mapping . (Mapping.lookup m) = (λ x . if (∃ z . (x,z) ∈ (set xs)) then Some {z . (x,z) ∈ (set xs)} else None)"

  have "?P (list_as_mapping xs)"
  proof (induction xs)
    case Nil
    then show ?case
      using Mapping.lookup_empty by fastforce
  next
    case (Cons xz xs)
    then obtain x z where "xz = (x,z)" 
      by (metis (mono_tags, opaque_lifting) surj_pair)

    have *: "(list_as_mapping ((x,z)#xs)) = (case Mapping.lookup (list_as_mapping xs) x of
                                None ⇒ Mapping.update x {z} (list_as_mapping xs) |
                                Some zs ⇒ Mapping.update x (insert z zs) (list_as_mapping xs))"
      unfolding list_as_mapping.simps
      by auto

    show ?case proof (cases "Mapping.lookup (list_as_mapping xs) x")
      case None
      then have **: "Mapping.lookup (list_as_mapping ((x,z)#xs)) = (Mapping.lookup (Mapping.update x {z} (list_as_mapping xs)))" 
        using * by auto
      then have m1: "Mapping.lookup (list_as_mapping ((x,z)#xs)) = (λ x' . if x' = x then Some {z} else Mapping.lookup (list_as_mapping xs) x')"
        by (metis (lifting) lookup_update') 

      have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = None"
        using None Cons by auto
      then have "¬(∃ z . (x,z) ∈ set xs)"
        by (metis (mono_tags, lifting) option.distinct(1))
      then have "(∃ z . (x,z) ∈ set ((x,z)#xs))" and "{z' . (x,z') ∈ set ((x,z)#xs)} = {z}"
        by auto
      then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set ((x,z)#xs)) 
                                then Some {z' . (x',z') ∈ set ((x,z)#xs)} 
                                else None)
                   = (λ x' . if x' = x 
                                then Some {z} else (λ x . if (∃ z . (x,z) ∈ set xs) 
                                                            then Some {z . (x,z) ∈ set xs} 
                                                            else None) x')"
        by force

      show ?thesis using m1 m2 Cons
        using ‹xz = (x, z)› by presburger
    next
      case (Some zs)
      then have **: "Mapping.lookup (list_as_mapping ((x,z)#xs)) = (Mapping.lookup (Mapping.update x (insert z zs) (list_as_mapping xs)))" 
        using * by auto
       then have m1: "Mapping.lookup (list_as_mapping ((x,z)#xs)) = (λ x' . if x' = x then Some (insert z zs) else Mapping.lookup (list_as_mapping xs) x')"
        by (metis (lifting) lookup_update') 

      have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs"
        using Some Cons by auto
      then have "(∃ z . (x,z) ∈ set xs)"
        unfolding case_prod_conv using  option.distinct(2) by metis
      then have "(∃ z . (x,z) ∈ set ((x,z)#xs))" by simp

      have "{z' . (x,z') ∈ set ((x,z)#xs)} = insert z zs"
      proof -
        have "Some {z . (x,z) ∈ set xs} = Some zs"
          using ‹(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x 
                  = Some zs›
          unfolding case_prod_conv using  option.distinct(2) by metis
        then have "{z . (x,z) ∈ set xs} = zs" by auto
        then show ?thesis by auto
      qed

      have "⋀ a  . (λ x' . if (∃ z' . (x',z') ∈ set ((x,z)#xs)) 
                              then Some {z' . (x',z') ∈ set ((x,z)#xs)} else None) a
                   = (λ x' . if x' = x 
                              then Some (insert z zs) 
                              else (λ x . if (∃ z . (x,z) ∈ set xs) 
                                            then Some {z . (x,z) ∈ set xs} else None) x') a" 
      proof -
        fix a show "(λ x' . if (∃ z' . (x',z') ∈ set ((x,z)#xs)) 
                              then Some {z' . (x',z') ∈ set ((x,z)#xs)} else None) a
                   = (λ x' . if x' = x 
                              then Some (insert z zs) 
                              else (λ x . if (∃ z . (x,z) ∈ set xs) 
                                            then Some {z . (x,z) ∈ set xs} else None) x') a"
        using ‹{z' . (x,z') ∈ set ((x,z)#xs)} = insert z zs› ‹(∃ z . (x,z) ∈ set ((x,z)#xs))›
        by (cases "a = x"; auto)
      qed

      then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set ((x,z)#xs)) 
                                then Some {z' . (x',z') ∈ set ((x,z)#xs)} else None)
                   = (λ x' . if x' = x 
                                then Some (insert z zs) 
                                else (λ x . if (∃ z . (x,z) ∈ set xs) 
                                              then Some {z . (x,z) ∈ set xs} else None) x')"
        by auto


      show ?thesis using m1 m2 Cons
        using ‹xz = (x, z)› by presburger
    qed
  qed
  then show ?thesis .
qed


lemma list_as_mapping_lookup_transitions : 
  "(case (Mapping.lookup (list_as_mapping (map (λ(q,x,y,q') . ((q,x),y,q')) ts)) (q,x)) of Some ts ⇒ ts | None ⇒ {}) = { (y,q') . (q,x,y,q') ∈ set ts}"
(is "?S1 = ?S2")
proof (cases "∃z. ((q, x), z) ∈ set (map (λ(q, x, y, q'). ((q, x), y, q')) ts)")
  case True
  then have "?S1 = {z. ((q, x), z) ∈ set (map (λ(q, x, y, q'). ((q, x), y, q')) ts)}"
    unfolding list_as_mapping_lookup by auto
  also have "… = ?S2"
    by (induction ts; auto)
  finally show ?thesis .
next
  case False
  then have "?S1 = {}"
    unfolding list_as_mapping_lookup by auto
  also have "… = ?S2"
    using False by (induction ts; auto) 
  finally show ?thesis .
qed

lemma list_as_mapping_Nil :
  "list_as_mapping [] = Mapping.empty"
  by auto


definition set_as_mapping :: "('a × 'c) set ⇒ ('a,'c set) mapping" where
  "set_as_mapping s = (THE m . Mapping.lookup m = (set_as_map s))"

lemma set_as_mapping_ob :
  obtains m where "set_as_mapping s = m" and "Mapping.lookup m = set_as_map s"
proof -
  obtain m where *:"Mapping.lookup m = set_as_map s"
    using Mapping.lookup.abs_eq by auto
  moreover have "(THE x. Mapping.lookup x = set_as_map s) = m"
    using the_equality[of "λm . Mapping.lookup m = set_as_map s", OF *] 
    unfolding *[symmetric]
    by (simp add: mapping_eqI) 
  ultimately show ?thesis 
    using that[of m] unfolding set_as_mapping_def by blast
qed

lemma set_as_mapping_refined[code] :
  fixes t :: "('a :: ccompare × 'c :: ccompare) set_rbt" 
  and   xs:: "('b :: ceq × 'd :: ceq) set_dlist"
  shows "set_as_mapping (RBT_set t) = (case ID CCOMPARE(('a × 'c)) of
           Some _ ⇒ (RBT_Set2.fold (λ (x,z) m . case Mapping.lookup m (x) of
                        None ⇒ Mapping.update (x) {z} m |
                        Some zs ⇒ Mapping.update (x) (Set.insert z zs) m)
                      t
                      Mapping.empty) |
           None   ⇒ Code.abort (STR ''set_as_map RBT_set: ccompare = None'') 
                                (λ_. set_as_mapping (RBT_set t)))"
    (is "set_as_mapping (RBT_set t) = ?C1 (RBT_set t)")
  and   "set_as_mapping (DList_set xs) = (case ID CEQ(('b × 'd)) of
            Some _ ⇒ (DList_Set.fold (λ (x,z) m . case Mapping.lookup m (x) of
                        None ⇒ Mapping.update (x) {z} m |
                        Some zs ⇒ Mapping.update (x) (Set.insert z zs) m)
                      xs
                      Mapping.empty) |
           None   ⇒ Code.abort (STR ''set_as_map RBT_set: ccompare = None'') 
                                (λ_. set_as_mapping (DList_set xs)))"
    (is "set_as_mapping (DList_set xs) = ?C2 (DList_set xs)")
proof -
  show "set_as_mapping (RBT_set t) = ?C1 (RBT_set t)"
  proof (cases "ID CCOMPARE(('a × 'c))")
    case None
    then show ?thesis by auto
  next
    case (Some a)
    
    let ?f' = "(λ t' . (RBT_Set2.fold (λ (x,z) m . case Mapping.lookup m x of
                                                  None ⇒ Mapping.update x {z} m |
                                                  Some zs ⇒ Mapping.update x (Set.insert z zs) m)
                             t'
                             Mapping.empty))"
   
    let ?f = "λ xs . (fold (λ (x,z) m . case Mapping.lookup m x of
                                                  None ⇒ Mapping.update x {z} m |
                                                  Some zs ⇒ Mapping.update x (Set.insert z zs) m)
                            xs Mapping.empty)"
    have "⋀ xs :: ('a × 'c) list . Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None)"
    proof - 
      fix xs :: "('a × 'c) list"
      show "Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None)"
      proof (induction xs rule: rev_induct)
        case Nil
        then show ?case 
          by (simp add: Mapping.empty.abs_eq Mapping.lookup.abs_eq)
      next
        case (snoc xz xs)
        then obtain x z where "xz = (x,z)" 
          by (metis (mono_tags, opaque_lifting) surj_pair)
    
        have *: "(?f (xs@[(x,z)])) = (case Mapping.lookup (?f xs) x of
                                    None ⇒ Mapping.update x {z} (?f xs) |
                                    Some zs ⇒ Mapping.update x (Set.insert z zs) (?f xs))"
          by auto
    
        then show ?case proof (cases "Mapping.lookup (?f xs) x")
          case None
          then have **: "Mapping.lookup (?f (xs@[(x,z)])) = Mapping.lookup (Mapping.update x {z} (?f xs))" using * by auto
    
          have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
            by (metis lookup_update')
    
    
          have m1: "Mapping.lookup (?f (xs@[(x,z)])) = (λ x' . if x' = x then Some {z} else Mapping.lookup (?f xs) x')"
            unfolding ** 
            unfolding scheme by force
    
          have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = None"
          using None snoc by auto
          then have "¬(∃ z . (x,z) ∈ set xs)"
            by (metis (mono_tags, lifting) option.distinct(1))
          then have "(∃ z' . (x,z') ∈ set (xs@[(x,z)]))" and "{z' . (x,z') ∈ set (xs@[(x,z)])} = {z}"
            by fastforce+
          then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None)
                       = (λ x' . if x' = x then Some {z} else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x')"
            by force
          
          show ?thesis using m1 m2 snoc
            using ‹xz = (x, z)› by presburger
        next
          case (Some zs)
          then have **: "Mapping.lookup (?f (xs@[(x,z)])) = Mapping.lookup (Mapping.update x (Set.insert z zs) (?f xs))" using * by auto
          have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
            by (metis lookup_update')
    
          have m1: "Mapping.lookup (?f (xs@[(x,z)])) = (λ x' . if x' = x then Some (Set.insert z zs) else Mapping.lookup (?f xs) x')"
            unfolding ** 
            unfolding scheme by force
    
    
          have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs"
            using Some snoc by auto
          then have "(∃ z' . (x,z') ∈ set xs)"
            unfolding case_prod_conv using  option.distinct(2) by metis
          then have "(∃ z' . (x,z') ∈ set (xs@[(x,z)]))" by fastforce
    
          have "{z' . (x,z') ∈ set (xs@[(x,z)])} = Set.insert z zs"
          proof -
            have "Some {z . (x,z) ∈ set xs} = Some zs"
              using ‹(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs›
              unfolding case_prod_conv using  option.distinct(2) by metis
            then have "{z . (x,z) ∈ set xs} = zs" by auto
            then show ?thesis by auto
          qed
    
          have "⋀ a  . (λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
                     = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x') a" 
          proof -
            fix a show "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
                       = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x') a"
            using ‹{z' . (x,z') ∈ set (xs@[(x,z)])} = Set.insert z zs› ‹(∃ z' . (x,z') ∈ set (xs@[(x,z)]))›
            by (cases "a = x"; auto)
          qed
  
          then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None)
                       = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x')"
            by auto
    
    
          show ?thesis using m1 m2 snoc
            using ‹xz = (x, z)› by presburger
        qed
      qed
    qed
    then have "Mapping.lookup (?f' t) = (λ x . if (∃ z . (x,z) ∈ set (RBT_Set2.keys t)) then Some {z . (x,z) ∈ set (RBT_Set2.keys t)} else None)"
      unfolding fold_conv_fold_keys by metis
    moreover have "set (RBT_Set2.keys t) = (RBT_set t)" 
      using Some by (simp add: RBT_set_conv_keys) 
    ultimately have "Mapping.lookup (?f' t) = (λ x . if (∃ z . (x,z) ∈ (RBT_set t)) then Some {z . (x,z) ∈ (RBT_set t)} else None)"
      by force
    then have "Mapping.lookup (?f' t) = set_as_map (RBT_set t)"
      unfolding set_as_map_def by blast
    then have *:"Mapping.lookup (?C1 (RBT_set t)) = set_as_map (RBT_set t)"
      unfolding Some by force
    
    have "⋀ t' . Mapping.lookup (?C1 (RBT_set t)) = Mapping.lookup (?C1 t') ⟹ (?C1 (RBT_set t)) = (?C1 t')"
      by (simp add: Some)
    then have **: "(⋀x. Mapping.lookup x = set_as_map (RBT_set t) ⟹ x = (?C1 (RBT_set t)))"
      by (simp add: "*" mapping_eqI)


    show ?thesis
      using the_equality[of "λ m . Mapping.lookup m = (set_as_map (RBT_set t))", OF * **]
      unfolding set_as_mapping_def by blast
  qed

  show "set_as_mapping (DList_set xs) = ?C2 (DList_set xs)"
  proof (cases "ID CEQ(('b × 'd))")
    case None
    then show ?thesis by auto
  next
    case (Some a)
    
    let ?f' = "(λ t' . (DList_Set.fold (λ (x,z) m . case Mapping.lookup m x of
                                                  None ⇒ Mapping.update x {z} m |
                                                  Some zs ⇒ Mapping.update x (Set.insert z zs) m)
                             t'
                             Mapping.empty))"
   
    let ?f = "λ xs . (fold (λ (x,z) m . case Mapping.lookup m x of
                                                  None ⇒ Mapping.update x {z} m |
                                                  Some zs ⇒ Mapping.update x (Set.insert z zs) m)
                            xs Mapping.empty)"
    have *: "⋀ xs :: ('b × 'd) list . Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None)"
    proof - 
      fix xs :: "('b × 'd) list"
      show "Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None)"
      proof (induction xs rule: rev_induct)
        case Nil
        then show ?case 
          by (simp add: Mapping.empty.abs_eq Mapping.lookup.abs_eq)
      next
        case (snoc xz xs)
        then obtain x z where "xz = (x,z)" 
          by (metis (mono_tags, opaque_lifting) surj_pair)
    
        have *: "(?f (xs@[(x,z)])) = (case Mapping.lookup (?f xs) x of
                                    None ⇒ Mapping.update x {z} (?f xs) |
                                    Some zs ⇒ Mapping.update x (Set.insert z zs) (?f xs))"
          by auto
    
        then show ?case proof (cases "Mapping.lookup (?f xs) x")
          case None
          then have **: "Mapping.lookup (?f (xs@[(x,z)])) = Mapping.lookup (Mapping.update x {z} (?f xs))" using * by auto
    
          have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
            by (metis lookup_update')
    
    
          have m1: "Mapping.lookup (?f (xs@[(x,z)])) = (λ x' . if x' = x then Some {z} else Mapping.lookup (?f xs) x')"
            unfolding ** 
            unfolding scheme by force
    
          have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = None"
          using None snoc by auto
          then have "¬(∃ z . (x,z) ∈ set xs)"
            by (metis (mono_tags, lifting) option.distinct(1))
          then have "(∃ z' . (x,z') ∈ set (xs@[(x,z)]))" and "{z' . (x,z') ∈ set (xs@[(x,z)])} = {z}"
            by fastforce+
          then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None)
                       = (λ x' . if x' = x then Some {z} else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x')"
            by force
          
          show ?thesis using m1 m2 snoc
            using ‹xz = (x, z)› by presburger
        next
          case (Some zs)
          then have **: "Mapping.lookup (?f (xs@[(x,z)])) = Mapping.lookup (Mapping.update x (Set.insert z zs) (?f xs))" using * by auto
          have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
            by (metis lookup_update')
    
          have m1: "Mapping.lookup (?f (xs@[(x,z)])) = (λ x' . if x' = x then Some (Set.insert z zs) else Mapping.lookup (?f xs) x')"
            unfolding ** 
            unfolding scheme by force
    
    
          have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs"
            using Some snoc by auto
          then have "(∃ z' . (x,z') ∈ set xs)"
            unfolding case_prod_conv using  option.distinct(2) by metis
          then have "(∃ z' . (x,z') ∈ set (xs@[(x,z)]))" by fastforce
    
          have "{z' . (x,z') ∈ set (xs@[(x,z)])} = Set.insert z zs"
          proof -
            have "Some {z . (x,z) ∈ set xs} = Some zs"
              using ‹(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs›
              unfolding case_prod_conv using  option.distinct(2) by metis
            then have "{z . (x,z) ∈ set xs} = zs" by auto
            then show ?thesis by auto
          qed
    
          have "⋀ a  . (λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
                     = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x') a" 
          proof -
            fix a show "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
                       = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x') a"
            using ‹{z' . (x,z') ∈ set (xs@[(x,z)])} = Set.insert z zs› ‹(∃ z' . (x,z') ∈ set (xs@[(x,z)]))›
            by (cases "a = x"; auto)
          qed
  
          then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None)
                       = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x')"
            by auto
    
    
          show ?thesis using m1 m2 snoc
            using ‹xz = (x, z)› by presburger
        qed
      qed
    qed

    have "ID CEQ('b × 'd) ≠ None"
      using Some by auto
    then have **: "⋀ x . x ∈ set (list_of_dlist xs) = (x ∈ (DList_set xs))" 
      using DList_Set.member.rep_eq[of xs]
      using Set_member_code(2) ceq_class.ID_ceq in_set_member by fastforce 
    
    have "Mapping.lookup (?f' xs) = (λ x . if (∃ z . (x,z) ∈ (DList_set xs)) then Some {z . (x,z) ∈ (DList_set xs)} else None)"
      using *[of "(list_of_dlist xs)"] 
      unfolding DList_Set.fold.rep_eq ** by assumption
    then have "Mapping.lookup (?f' xs) = set_as_map (DList_set xs)"
      unfolding set_as_map_def by blast
    then have *:"Mapping.lookup (?C2 (DList_set xs)) = set_as_map (DList_set xs)"
      unfolding Some by force
    
    have "⋀ t' . Mapping.lookup (?C2 (DList_set xs)) = Mapping.lookup (?C2 t') ⟹ (?C2 (DList_set xs)) = (?C2 t')"
      by (simp add: Some)
    then have **: "(⋀x. Mapping.lookup x = set_as_map (DList_set xs) ⟹ x = (?C2 (DList_set xs)))"
      by (simp add: "*" mapping_eqI)


    show ?thesis
      using the_equality[of "λ m . Mapping.lookup m = (set_as_map (DList_set xs))", OF * **]
      unfolding set_as_mapping_def by blast
  qed
qed


fun h_obs_impl_from_h :: "(('state × 'input), ('output × 'state) set) mapping ⇒ ('state × 'input, ('output, 'state) mapping) mapping" where
  "h_obs_impl_from_h h' = Mapping.map_values
                            (λ _ yqs . let m' = set_as_mapping yqs;
                                           m'' = Mapping.filter (λ y qs . card qs = 1) m';
                                           m''' = Mapping.map_values (λ _ qs . the_elem qs) m''
                                        in m''')
                            h'"

fun h_obs_impl :: "(('state × 'input), ('output × 'state) set) mapping ⇒ 'state ⇒ 'input ⇒ 'output ⇒ 'state option" where
  "h_obs_impl h' q x y  = (let 
      tgts = snd ` Set.filter (λ(y',q') . y' = y) (case (Mapping.lookup h' (q,x)) of Some ts ⇒ ts | None ⇒ {})
    in if card tgts = 1
      then Some (the_elem tgts)
      else None)"

abbreviation(input) "h_obs_lookup ≡ (λ h' q x y . (case Mapping.lookup h' (q,x) of Some m ⇒ Mapping.lookup m y | None ⇒ None))" 

lemma h_obs_impl_from_h_invar : "h_obs_impl h' q x y = h_obs_lookup (h_obs_impl_from_h h') q x y" 
  (is "?A q x y = ?B q x y")
proof (cases "Mapping.lookup h' (q,x)")
  case None

  then have "Mapping.lookup (h_obs_impl_from_h h') (q,x) = None"
    unfolding h_obs_impl_from_h.simps Mapping.lookup_map_values
    by auto
  then have "?B q x y = None"
    by auto
  moreover have "?A q x y = None"
    unfolding h_obs_impl.simps Let_def None
    by (simp add: Set.filter_def) 
  ultimately show ?thesis 
    by presburger
next
  case (Some yqs)

  define m' where "m' = set_as_mapping yqs"
  define m'' where "m'' = Mapping.filter (λ y qs . card qs = 1) m'"
  define m''' where "m''' = Mapping.map_values (λ _ qs . the_elem qs) m''"

  have "Mapping.lookup (h_obs_impl_from_h h') (q,x) = Some m'''"
    unfolding m'''_def m''_def m'_def h_obs_impl_from_h.simps Let_def 
    unfolding Mapping.lookup_map_values Some
    by auto

  have "Mapping.lookup m' = set_as_map yqs"
    using set_as_mapping_ob m'_def
    by auto 

  have *:"(snd ` Set.filter (λ(y', q'). y' = y) (case Some yqs of None ⇒ {} | Some ts ⇒ ts)) = {z. (y, z) ∈ yqs}"
    by force

  have "⋀ qs . Mapping.lookup m'' y = Some qs ⟷ qs = {z. (y, z) ∈ yqs} ∧ card {z. (y, z) ∈ yqs} = 1"
    unfolding m''_def Mapping.lookup_filter 
    unfolding ‹Mapping.lookup m' = set_as_map yqs› set_as_map_def
    by auto
  then have **:"⋀ q' . Mapping.lookup m''' y = Some q' ⟷ card {z. (y, z) ∈ yqs} = 1 ∧ q' = the_elem {z. (y, z) ∈ yqs}"
    unfolding m'''_def lookup_map_values by auto
  then show ?thesis
    unfolding h_obs_impl.simps Let_def 
    unfolding ‹Mapping.lookup (h_obs_impl_from_h h') (q,x) = Some m'''›
    using "*" Some by force
qed







definition set_as_mapping_image :: "('a1 × 'a2) set ⇒ (('a1 × 'a2) ⇒ ('b1 × 'b2)) ⇒ ('b1, 'b2 set) mapping" where 
  "set_as_mapping_image s f = (THE m . Mapping.lookup m = set_as_map (image f s))"

lemma set_as_mapping_image_ob :
  obtains m where "set_as_mapping_image s f = m" and "Mapping.lookup m = set_as_map (image f s)"
proof -
  obtain m where *:"Mapping.lookup m = set_as_map (image f s)"
    using Mapping.lookup.abs_eq by auto
  moreover have "(THE x. Mapping.lookup x = set_as_map (image f s)) = m"
    using the_equality[of "λm . Mapping.lookup m = set_as_map (image f s)", OF *] 
    unfolding *[symmetric]
    by (simp add: mapping_eqI) 
  ultimately show ?thesis 
    using that[of m] unfolding set_as_mapping_image_def by blast
qed

lemma set_as_mapping_image_code[code]  :
  fixes t :: "('a1 ::ccompare × 'a2 :: ccompare) set_rbt" 
  and   f1 :: "('a1 × 'a2) ⇒ ('b1 :: ccompare × 'b2 ::ccompare)"
  and   xs :: "('c1 :: ceq × 'c2 :: ceq) set_dlist" 
  and   f2 :: "('c1 × 'c2) ⇒ ('d1 × 'd2)"
shows "set_as_mapping_image (RBT_set t) f1 = (case ID CCOMPARE(('a1 × 'a2)) of
           Some _ ⇒ (RBT_Set2.fold (λ kv m1 .
                        ( case f1 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1)))
                      t
                      Mapping.empty) |
           None   ⇒ Code.abort (STR ''set_as_map_image RBT_set: ccompare = None'') 
                                (λ_. set_as_mapping_image (RBT_set t) f1))"
  (is "set_as_mapping_image (RBT_set t) f1 = ?C1 (RBT_set t)")
and   "set_as_mapping_image (DList_set xs) f2 = (case ID CEQ(('c1 × 'c2)) of
            Some _ ⇒ (DList_Set.fold (λ kv m1 . 
                        ( case f2 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1)))
                      xs
                      Mapping.empty) |
           None   ⇒ Code.abort (STR ''set_as_map_image DList_set: ccompare = None'') 
                                (λ_. set_as_mapping_image (DList_set xs) f2))"
  (is "set_as_mapping_image (DList_set xs) f2 = ?C2 (DList_set xs)")
proof -
  show "set_as_mapping_image (RBT_set t) f1 = ?C1 (RBT_set t)"

  proof (cases "ID CCOMPARE(('a1 × 'a2))")
    case None
    then show ?thesis by auto
  next
    case (Some a)
  
    let ?f' = "λ t . (RBT_Set2.fold (λ kv m1 .
                          ( case f1 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1)))
                        t
                        Mapping.empty)"
  
    let ?f = "λ xs . (fold (λ kv m1 . case f1 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1))
                              xs Mapping.empty)"
    have "⋀ xs :: ('a1 × 'a2) list . Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None)"
    proof -
      fix xs :: "('a1 × 'a2) list"
      show "Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None)"
      proof (induction xs rule: rev_induct)
        case Nil
        then show ?case 
          by (simp add: Mapping.empty.abs_eq Mapping.lookup.abs_eq) 
      next
        case (snoc xz xs)
        then obtain x z where "f1  xz = (x,z)" 
          by (metis (mono_tags, opaque_lifting) surj_pair)
    
        then have *: "(?f (xs@[xz])) = (case Mapping.lookup (?f xs) x of
                                    None ⇒ Mapping.update x {z} (?f xs) |
                                    Some zs ⇒ Mapping.update x (Set.insert z zs) (?f xs))"
          by auto
    
        then show ?case proof (cases "Mapping.lookup (?f xs) x")
          case None
          then have **: "Mapping.lookup (?f (xs@[xz])) = Mapping.lookup (Mapping.update x {z} (?f xs))" using * by auto
    
          have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
            by (metis lookup_update')
    
    
          have m1: "Mapping.lookup (?f (xs@[xz])) = (λ x' . if x' = x then Some {z} else Mapping.lookup (?f xs) x')"
            unfolding ** 
            unfolding scheme by force
    
          have "(λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x = None"
          using None snoc by auto
          then have "¬(∃ z . (x,z) ∈ f1 ` set xs)"
            by (metis (mono_tags, lifting) option.distinct(1))
          then have "(∃ z' . (x,z') ∈ f1 ` set (xs@[xz]))" and "{z' . (x,z') ∈ f1 ` set (xs@[xz])} = {z}"
            using ‹f1  xz = (x,z)› by fastforce+
          then have m2: "(λ x' . if (∃ z' . (x',z') ∈ f1 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f1 ` set (xs@[xz])} else None)
                       = (λ x' . if x' = x then Some {z} else (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x')"
            using ‹f1  xz = (x,z)› by fastforce
          
          show ?thesis using m1 m2 snoc
            using ‹f1 xz = (x, z)› by presburger
        next
          case (Some zs)
          then have **: "Mapping.lookup (?f (xs@[xz])) = Mapping.lookup (Mapping.update x (Set.insert z zs) (?f xs))" using * by auto
          have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
            by (metis lookup_update')
    
          have m1: "Mapping.lookup (?f (xs@[xz])) = (λ x' . if x' = x then Some (Set.insert z zs) else Mapping.lookup (?f xs) x')"
            unfolding ** 
            unfolding scheme by force
    
    
          have "(λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x = Some zs"
            using Some snoc by auto
          then have "(∃ z' . (x,z') ∈ f1 ` set xs)"
            unfolding case_prod_conv using  option.distinct(2) by metis
          then have "(∃ z' . (x,z') ∈ f1 ` set (xs@[xz]))" by fastforce
    
          have "{z' . (x,z') ∈ f1 ` set (xs@[xz])} = Set.insert z zs"
          proof -
            have "Some {z . (x,z) ∈ f1 ` set xs} = Some zs"
              using ‹(λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x = Some zs›
              unfolding case_prod_conv using  option.distinct(2) by metis
            then have "{z . (x,z) ∈ f1 ` set xs} = zs" by auto
            then show ?thesis 
              using ‹f1 xz = (x, z)› by auto
          qed
    
          have "⋀ a  . (λ x' . if (∃ z' . (x',z') ∈ f1 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f1 ` set (xs@[xz])} else None) a
                     = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x') a" 
          proof -
            fix a show "(λ x' . if (∃ z' . (x',z') ∈ f1 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f1 ` set (xs@[xz])} else None) a
                       = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x') a"
            using ‹{z' . (x,z') ∈ f1 ` set (xs@[xz])} = Set.insert z zs› ‹(∃ z' . (x,z') ∈ f1 ` set (xs@[xz]))› ‹f1 xz = (x, z)›
            by (cases "a = x"; auto)
          qed
  
          then have m2: "(λ x' . if (∃ z' . (x',z') ∈ f1 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f1 ` set (xs@[xz])} else None)
                       = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ f1 ` set xs) then Some {z . (x,z) ∈ f1 ` set xs} else None) x')"
            by auto
    
    
          show ?thesis using m1 m2 snoc
            using ‹f1 xz = (x, z)› by presburger
        qed
      qed
    qed
  
  
    
    then have "Mapping.lookup (?f' t) = (λ x . if (∃ z . (x,z) ∈ f1 ` set (RBT_Set2.keys t)) then Some {z . (x,z) ∈ f1 ` set (RBT_Set2.keys t)} else None)"
      unfolding fold_conv_fold_keys by metis
    moreover have "set (RBT_Set2.keys t) = (RBT_set t)" 
      using Some by (simp add: RBT_set_conv_keys) 
    ultimately have "Mapping.lookup (?f' t) = (λ x . if (∃ z . (x,z) ∈ f1 ` (RBT_set t)) then Some {z . (x,z) ∈ f1 ` (RBT_set t)} else None)"
      by force
  
    then have "Mapping.lookup (?f' t) = set_as_map (image f1 (RBT_set t))"
      unfolding set_as_map_def by blast
    then have *:"Mapping.lookup (?C1 (RBT_set t)) = set_as_map (image f1 (RBT_set t))"
      unfolding Some by force
    
    have "⋀ t' . Mapping.lookup (?C1 (RBT_set t)) = Mapping.lookup (?C1 t') ⟹ (?C1 (RBT_set t)) = (?C1 t')"
      by (simp add: Some)
    then have **: "(⋀x. Mapping.lookup x = set_as_map (image f1 (RBT_set t)) ⟹ x = (?C1 (RBT_set t)))"
      by (simp add: "*" mapping_eqI)
  
    show ?thesis
      using the_equality[of "λ m . Mapping.lookup m = (set_as_map (image f1 (RBT_set t)))", OF * **]
      unfolding set_as_mapping_image_def by blast
  qed

  show "set_as_mapping_image (DList_set xs) f2 = ?C2 (DList_set xs)"
  proof (cases "ID CEQ(('c1 × 'c2))")
    case None
    then show ?thesis by auto
  next
    case (Some a)
  
    let ?f' = "λ t . (DList_Set.fold (λ kv m1 .
                          ( case f2 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1)))
                        t
                        Mapping.empty)"
  
    let ?f = "λ xs . (fold (λ kv m1 . case f2 kv of (x,z) ⇒ (case Mapping.lookup m1 (x) of None ⇒ Mapping.update (x) {z} m1 | Some zs ⇒ Mapping.update (x) (Set.insert z zs) m1))
                              xs Mapping.empty)"
    have *:"⋀ xs :: ('c1 × 'c2) list . Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ f2 ` set xs) then Some {z . (x,z) ∈ f2 ` set xs} else None)"
    proof -
      fix xs :: "('c1 × 'c2) list"
      show "Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ f2 ` set xs) then Some {z . (x,z) ∈ f2 ` set xs} else None)"
      proof (induction xs rule: rev_induct)
        case Nil
        then show ?case 
          by (simp add: Mapping.empty.abs_eq Mapping.lookup.abs_eq) 
      next
        case (snoc xz xs)
        then obtain x z where "f2  xz = (x,z)" 
          by (metis (mono_tags, opaque_lifting) surj_pair)
    
        then have *: "(?f (xs@[xz])) = (case Mapping.lookup (?f xs) x of
                                    None ⇒ Mapping.update x {z} (?f xs) |
                                    Some zs ⇒ Mapping.update x (Set.insert z zs) (?f xs))"
          by auto
    
        then show ?case proof (cases "Mapping.lookup (?f xs) x")
          case None
          then have **: "Mapping.lookup (?f (xs@[xz])) = Mapping.lookup (Mapping.update x {z} (?f xs))" using * by auto
    
          have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
            by (metis lookup_update')
    
    
          have m1: "Mapping.lookup (?f (xs@[xz])) = (λ x' . if x' = x then Some {z} else Mapping.lookup (?f xs) x')"
            unfolding ** 
            unfolding scheme by force
    
          have "(λ x . if (∃ z . (x,z) ∈ f2 ` set xs) then Some {z . (x,z) ∈ f2 ` set xs} else None) x = None"
          using None snoc by auto
          then have "¬(∃ z . (x,z) ∈ f2 ` set xs)"
            by (metis (mono_tags, lifting) option.distinct(1))
          then have "(∃ z' . (x,z') ∈ f2 ` set (xs@[xz]))" and "{z' . (x,z') ∈ f2 ` set (xs@[xz])} = {z}"
            using ‹f2  xz = (x,z)› by fastforce+
          then have m2: "(λ x' . if (∃ z' . (x',z') ∈ f2 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f2 ` set (xs@[xz])} else None)
                       = (λ x' . if x' = x then Some {z} else (λ x . if (∃ z . (x,z) ∈ f2 ` set xs) then Some {z . (x,z) ∈ f2 ` set xs} else None) x')"
            using ‹f2  xz = (x,z)› by fastforce
          
          show ?thesis using m1 m2 snoc
            using ‹f2 xz = (x, z)› by presburger
        next
          case (Some zs)
          then have **: "Mapping.lookup (?f (xs@[xz])) = Mapping.lookup (Mapping.update x (Set.insert z zs) (?f xs))" using * by auto
          have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
            by (metis lookup_update')
    
          have m1: "Mapping.lookup (?f (xs@[xz])) = (λ x' . if x' = x then Some (Set.insert z zs) else Mapping.lookup (?f xs) x')"
            unfolding ** 
            unfolding scheme by force
    
    
          have "(λ x . if (∃ z . (x,z) ∈ f2 ` set xs) then Some {z . (x,z) ∈ f2 ` set xs} else None) x = Some zs"
            using Some snoc by auto
          then have "(∃ z' . (x,z') ∈ f2 ` set xs)"
            unfolding case_prod_conv using  option.distinct(2) by metis
          then have "(∃ z' . (x,z') ∈ f2 ` set (xs@[xz]))" by fastforce
    
          have "{z' . (x,z') ∈ f2 ` set (xs@[xz])} = Set.insert z zs"
          proof -
            have "Some {z . (x,z) ∈ f2 ` set xs} = Some zs"
              using ‹(λ x . if (∃ z . (x,z) ∈ f2 ` set xs) then Some {z . (x,z) ∈ f2 ` set xs} else None) x = Some zs›
              unfolding case_prod_conv using  option.distinct(2) by metis
            then have "{z . (x,z) ∈ f2 ` set xs} = zs" by auto
            then show ?thesis 
              using ‹f2 xz = (x, z)› by auto
          qed
    
          have "⋀ a  . (λ x' . if (∃ z' . (x',z') ∈ f2 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f2 ` set (xs@[xz])} else None) a
                     = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ f2 ` set xs) then Some {z . (x,z) ∈ f2 ` set xs} else None) x') a" 
          proof -
            fix a show "(λ x' . if (∃ z' . (x',z') ∈ f2 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f2 ` set (xs@[xz])} else None) a
                       = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ f2 ` set xs) then Some {z . (x,z) ∈ f2 ` set xs} else None) x') a"
            using ‹{z' . (x,z') ∈ f2 ` set (xs@[xz])} = Set.insert z zs› ‹(∃ z' . (x,z') ∈ f2 ` set (xs@[xz]))› ‹f2 xz = (x, z)›
            by (cases "a = x"; auto)
          qed
  
          then have m2: "(λ x' . if (∃ z' . (x',z') ∈ f2 ` set (xs@[xz])) then Some {z' . (x',z') ∈ f2 ` set (xs@[xz])} else None)
                       = (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ f2 ` set xs) then Some {z . (x,z) ∈ f2 ` set xs} else None) x')"
            by auto
    
    
          show ?thesis using m1 m2 snoc
            using ‹f2 xz = (x, z)› by presburger
        qed
      qed
    qed


    have "ID CEQ('c1 × 'c2) ≠ None"
      using Some by auto
    then have **: "⋀ x . x ∈ f2 ` set (list_of_dlist xs) = (x ∈ f2 ` (DList_set xs))" 
      using DList_Set.member.rep_eq[of xs]
      using Set_member_code(2) ceq_class.ID_ceq in_set_member by fastforce 
    
    have "Mapping.lookup (?f' xs) = (λ x . if (∃ z . (x,z) ∈ f2 ` (DList_set xs)) then Some {z . (x,z) ∈ f2 ` (DList_set xs)} else None)"
      using *[of "(list_of_dlist xs)"] 
      unfolding DList_Set.fold.rep_eq ** .
    then have "Mapping.lookup (?f' xs) = set_as_map (image f2 (DList_set xs))"
      unfolding set_as_map_def by blast
    then have *:"Mapping.lookup (?C2 (DList_set xs)) = set_as_map (image f2 (DList_set xs))"
      unfolding Some by force
    
    have "⋀ t' . Mapping.lookup (?C2 (DList_set xs)) = Mapping.lookup (?C2 t') ⟹ (?C2 (DList_set xs)) = (?C2 t')"
      by (simp add: Some)
    then have **: "(⋀x. Mapping.lookup x = set_as_map (image f2 (DList_set xs)) ⟹ x = (?C2 (DList_set xs)))"
      by (simp add: "*" mapping_eqI)    
    then show ?thesis
      using *
      using set_as_mapping_image_ob by blast 
  qed
qed


subsection ‹Impl Datatype›

text ‹The following type extends @{text "fsm_impl"} with fields for  @{text "h"} and  @{text "h_obs"}.›

datatype ('state, 'input, 'output) fsm_with_precomputations_impl = 
        FSMWPI (initial_wpi : 'state)  
               (states_wpi : "'state set")
               (inputs_wpi  : "'input set")
               (outputs_wpi : "'output set")
               (transitions_wpi : "('state × 'input × 'output × 'state) set")
               (h_wpi : "(('state × 'input), ('output × 'state) set) mapping")
               (h_obs_wpi: "('state × 'input, ('output, 'state) mapping) mapping")

fun fsm_with_precomputations_impl_from_list :: "'a ⇒ ('a × 'b × 'c × 'a) list ⇒ ('a, 'b, 'c) fsm_with_precomputations_impl" where
  "fsm_with_precomputations_impl_from_list q [] = FSMWPI q {q} {} {} {} Mapping.empty Mapping.empty" |
  "fsm_with_precomputations_impl_from_list q (t#ts) = (let ts' = set (t#ts)
                                   in FSMWPI (t_source t)
                                      ((image t_source ts') ∪ (image t_target ts'))
                                      (image t_input ts')
                                      (image t_output ts')
                                      (ts')
                                      (list_as_mapping (map (λ(q,x,y,q') . ((q,x),y,q')) (t#ts)))
                                      (h_obs_impl_from_h (list_as_mapping (map (λ(q,x,y,q') . ((q,x),y,q')) (t#ts)))))"

fun fsm_with_precomputations_impl_from_list' :: "'a ⇒ ('a × 'b × 'c × 'a) list ⇒ ('a, 'b, 'c) fsm_with_precomputations_impl" where
  "fsm_with_precomputations_impl_from_list' q [] = FSMWPI q {q} {} {} {} Mapping.empty Mapping.empty" |
  "fsm_with_precomputations_impl_from_list' q (t#ts) = (let tsr = (remdups (t#ts));
                                                            h'  = (list_as_mapping (map (λ(q,x,y,q') . ((q,x),y,q')) tsr))
                                   in FSMWPI (t_source t)
                                      (set (remdups ((map t_source tsr) @ (map t_target tsr))))
                                      (set (remdups (map t_input tsr)))
                                      (set (remdups (map t_output tsr)))
                                      (set tsr)
                                      h'
                                      (h_obs_impl_from_h h'))"



lemma fsm_impl_from_list_code[code] :
  "fsm_with_precomputations_impl_from_list q ts = fsm_with_precomputations_impl_from_list' q ts" 
proof (cases ts)
  case Nil
  then show ?thesis by auto
next
  case (Cons t ts)
  have **: "set (t#ts) = set (remdups (t#ts))"
    by auto
  have *: "set (map (λ(q,x,y,q') . ((q,x),y,q')) (t#ts)) = set (map (λ(q,x,y,q') . ((q,x),y,q')) (remdups (t#ts)))"
    by (metis remdups_map_remdups set_remdups)
  have "Mapping.lookup (list_as_mapping (map (λ(q,x,y,q') . ((q,x),y,q')) (t#ts)))
             = Mapping.lookup (list_as_mapping (map (λ(q,x,y,q') . ((q,x),y,q')) (remdups (t#ts))))"
    unfolding list_as_mapping_lookup * by simp
  then have ***: "list_as_mapping (map (λ(q,x,y,q') . ((q,x),y,q')) (t#ts)) = list_as_mapping (map (λ(q,x,y,q') . ((q,x),y,q')) (remdups (t#ts)))"
    by (simp add: mapping_eqI)

  have ****: "(set (map t_source (remdups (t # ts)) @ map t_target (remdups (t # ts)))) = (t_source ` set (t # ts) ∪ t_target ` set (t # ts))"
    by auto

  have *****: "⋀ f xs . set (map f (remdups xs)) = f ` set xs"
    by auto

  show ?thesis
    unfolding Cons fsm_with_precomputations_impl_from_list'.simps fsm_with_precomputations_impl_from_list.simps Let_def
    unfolding ** *** 
    unfolding set_remdups ****  ***** 
    unfolding remdups_map_remdups 
    by presburger
qed 



subsection ‹Refined Datatype›

text ‹Well-formedness now also encompasses the new fields for  @{text "h"} and  @{text "h_obs"}.›


fun well_formed_fsm_with_precomputations :: "('state, 'input, 'output) fsm_with_precomputations_impl ⇒ bool" where 
  "well_formed_fsm_with_precomputations M = (initial_wpi M ∈ states_wpi M
      ∧ finite (states_wpi M)
      ∧ finite (inputs_wpi M)
      ∧ finite (outputs_wpi M)
      ∧ finite (transitions_wpi M)
      ∧ (∀ t ∈ transitions_wpi M . t_source t ∈ states_wpi M ∧ 
                                t_input t ∈ inputs_wpi M ∧ 
                                t_target t ∈ states_wpi M ∧ 
                                t_output t ∈ outputs_wpi M)
      ∧ (∀ q x . (case (Mapping.lookup (h_wpi M) (q,x)) of Some ts ⇒ ts | None ⇒ {}) = { (y,q') . (q,x,y,q') ∈ transitions_wpi M })
      ∧ (∀ q x y . h_obs_impl (h_wpi M) q x y = h_obs_lookup (h_obs_wpi M) q x y))"

lemma well_formed_h_set_as_mapping :
  assumes "h_wpi M = set_as_mapping_image (transitions_wpi M) (λ(q,x,y,q') . ((q,x),y,q'))"
  shows "(case (Mapping.lookup (h_wpi M) (q,x)) of Some ts ⇒ ts | None ⇒ {}) = { (y,q') . (q,x,y,q') ∈ transitions_wpi M }"
(is "?A q x = ?B q x")
proof -
  have *:"Mapping.lookup (h_wpi M) = (set_as_map (image (λ(q,x,y,q') . ((q,x),y,q')) (transitions_wpi M)))"
    unfolding assms using set_as_mapping_image_ob
    by auto 
  have **: "(case Mapping.lookup (h_wpi M) (q, x) of None ⇒ {} | Some ts ⇒ ts) = {a. case a of (y, q') ⇒ (q, x, y, q') ∈ (transitions_wpi M)}"
    unfolding *
    unfolding set_as_map_def by force

  show ?thesis
    unfolding  ** by force
qed

lemma well_formed_h_obs_impl_from_h :
  assumes "h_obs_wpi M = h_obs_impl_from_h (h_wpi M)"
  shows "h_obs_impl  (h_wpi M) q x y = (h_obs_lookup  (h_obs_wpi M) q x y)"
  unfolding assms h_obs_impl_from_h_invar by presburger


typedef ('state, 'input, 'output) fsm_with_precomputations = 
  "{ M :: ('state, 'input, 'output) fsm_with_precomputations_impl . well_formed_fsm_with_precomputations M}"
  morphisms fsm_with_precomputations_impl_of_fsm_with_precomputations Abs_fsm_with_precomputations
proof -
  obtain q :: 'state where "True" by blast
  define M :: "('state, 'input, 'output) fsm_with_precomputations_impl" where 
    M: "M = FSMWPI q {q} {} {} {} Mapping.empty Mapping.empty"
  
  have "(⋀ q x . (case (Mapping.lookup (h_wpi M) (q,x)) of Some ts ⇒ ts | None ⇒ {}) = { (y,q') . (q,x,y,q') ∈ transitions_wpi M })"
  proof -
    fix q x 
    have "{ (y,q') . (q,x,y,q') ∈ transitions_wpi M } = {}"
      unfolding M by auto
    moreover have "(case (Mapping.lookup (h_wpi M) (q,x)) of Some ts ⇒ ts | None ⇒ {}) = {}"
      unfolding M by (metis fsm_with_precomputations_impl.sel(6) lookup_default_def lookup_default_empty) 
    ultimately show "(case (Mapping.lookup (h_wpi M) (q,x)) of Some ts ⇒ ts | None ⇒ {}) = { (y,q') . (q,x,y,q') ∈ transitions_wpi M }"
      by blast
  qed
  moreover have "(∀ q x y . h_obs_impl  (h_wpi M) q x y = (h_obs_lookup  (h_obs_wpi M) q x y))"
    unfolding h_obs_impl.simps Let_def
    unfolding calculation M
    by (simp add: Mapping.empty_def Mapping.lookup.abs_eq Set.filter_def) 
  ultimately have "well_formed_fsm_with_precomputations M"
    unfolding M by auto
  then show ?thesis 
    by blast
qed


setup_lifting type_definition_fsm_with_precomputations

lift_definition initial_wp :: "('state, 'input, 'output) fsm_with_precomputations ⇒ 'state" is FSM_Code_Datatype.initial_wpi done
lift_definition states_wp :: "('state, 'input, 'output) fsm_with_precomputations ⇒ 'state set" is FSM_Code_Datatype.states_wpi done
lift_definition inputs_wp :: "('state, 'input, 'output) fsm_with_precomputations ⇒ 'input set" is FSM_Code_Datatype.inputs_wpi done
lift_definition outputs_wp :: "('state, 'input, 'output) fsm_with_precomputations ⇒ 'output set" is FSM_Code_Datatype.outputs_wpi done
lift_definition transitions_wp :: 
  "('state, 'input, 'output) fsm_with_precomputations ⇒ ('state × 'input × 'output × 'state) set" 
  is FSM_Code_Datatype.transitions_wpi done
lift_definition h_wp :: 
  "('state, 'input, 'output) fsm_with_precomputations ⇒ (('state × 'input), ('output × 'state) set) mapping" 
  is FSM_Code_Datatype.h_wpi done
lift_definition h_obs_wp :: 
  "('state, 'input, 'output) fsm_with_precomputations ⇒ (('state × 'input), ('output, 'state) mapping) mapping" 
  is FSM_Code_Datatype.h_obs_wpi done


lemma fsm_with_precomputations_initial: "initial_wp M ∈ states_wp M" 
  by (transfer; auto)
lemma fsm_with_precomputations_states_finite: "finite (states_wp M)" 
  by (transfer; auto)
lemma fsm_with_precomputations_inputs_finite: "finite (inputs_wp M)" 
  by (transfer; auto)
lemma fsm_with_precomputations_outputs_finite: "finite (outputs_wp M)" 
  by (transfer; auto)
lemma fsm_with_precomputations_transitions_finite: "finite (transitions_wp M)" 
  by (transfer; auto)
lemma fsm_with_precomputations_transition_props: "t ∈ transitions_wp M ⟹ t_source t ∈ states_wp M ∧ 
                                                                        t_input t ∈ inputs_wp M ∧ 
                                                                        t_target t ∈ states_wp M ∧ 
                                                                        t_output t ∈ outputs_wp M" 
  by (transfer; auto)
lemma fsm_with_precomputations_h_prop: "(case (Mapping.lookup (h_wp M) (q,x)) of Some ts ⇒ ts | None ⇒ {}) = { (y,q') . (q,x,y,q') ∈ transitions_wp M }" 
  by (transfer; auto)


lemma fsm_with_precomputations_h_obs_prop: "(h_obs_lookup  (h_obs_wp M) q x y) = h_obs_impl  (h_wp M) q x y"
proof -
  define M' where "M' = fsm_with_precomputations_impl_of_fsm_with_precomputations M"
  then have "well_formed_fsm_with_precomputations M'"
    by (transfer;blast)
  then have *:"h_obs_impl  (fsm_with_precomputations_impl.h_wpi M') q x y = (h_obs_lookup (h_obs_wpi M') q x y)"
    unfolding well_formed_fsm_with_precomputations.simps by blast

  have **: "(h_obs_lookup (h_obs_wpi M') q x y) = h_obs_impl (fsm_with_precomputations_impl.h_wpi M') q x y"
    unfolding * by auto  
  have ***: "h_wp M = (fsm_with_precomputations_impl.h_wpi M')"
    unfolding M'_def apply transfer by presburger
  have ****: "h_obs_wp M = (fsm_with_precomputations_impl.h_obs_wpi M')"
    unfolding M'_def apply transfer by presburger

  show ?thesis
    using "**" "***" "****" by presburger 
qed

lemma map_values_empty : "Mapping.map_values f Mapping.empty = Mapping.empty"
  by (metis Mapping.keys_empty empty_iff keys_map_values mapping_eqI')

lift_definition fsm_with_precomputations_from_list :: "'a ⇒ ('a × 'b × 'c × 'a) list ⇒ ('a, 'b, 'c) fsm_with_precomputations" 
  is fsm_with_precomputations_impl_from_list
proof -
  fix q  :: 'a 
  fix ts :: "('a × 'b × 'c × 'a) list"

  define M where "M = fsm_with_precomputations_impl_from_list q ts"

  have base_props: "(initial_wpi M ∈ states_wpi M
      ∧ finite (states_wpi M)
      ∧ finite (inputs_wpi M)
      ∧ finite (outputs_wpi M)
      ∧ finite (transitions_wpi M))"
  proof (cases ts)
    case Nil
    show ?thesis 
      unfolding M_def Nil fsm_with_precomputations_impl_from_list.simps by auto
  next
    case (Cons t ts')
    show ?thesis 
      unfolding M_def Cons fsm_with_precomputations_impl_from_list.simps Let_def by force
  qed
  

  have transition_prop: "(∀ t ∈ transitions_wpi M . t_source t ∈ states_wpi M ∧ 
                                t_input t ∈ inputs_wpi M ∧ 
                                t_target t ∈ states_wpi M ∧ 
                                t_output t ∈ outputs_wpi M)"
  proof (cases ts)
    case Nil
    show ?thesis 
      unfolding M_def Nil fsm_with_precomputations_impl_from_list.simps by auto
  next
    case (Cons t ts')
    show ?thesis 
      unfolding M_def Cons fsm_with_precomputations_impl_from_list.simps Let_def by force
  qed


  have h_prop:"⋀ qa x .
        (case Mapping.lookup (h_wpi M) (qa, x) of None ⇒ {} | Some ts ⇒ ts) =
        {a. case a of (y, q') ⇒ (qa, x, y, q') ∈ transitions_wpi M}"
  (is "⋀ qa x . ?P qa x")
  proof -
    fix qa x 
    show "?P qa x" unfolding M_def
    proof (induction ts)
      case Nil
      have "(case Mapping.lookup (h_wpi (fsm_with_precomputations_impl_from_list q [])) (qa, x) of None ⇒ {} | Some ts ⇒ ts) = {}"
        by simp   
      moreover have "transitions_wpi (fsm_with_precomputations_impl_from_list q []) = {}"
        by auto
      ultimately show ?case
        by blast
    next
      case (Cons t ts)
      have *: "(h_wpi (fsm_with_precomputations_impl_from_list q (t#ts))) = (list_as_mapping (map (λ(q,x,y,q') . ((q,x),y,q')) (t#ts)))"
        unfolding fsm_with_precomputations_impl_from_list.simps Let_def by simp
      show ?case proof (cases "∃z. ((qa, x), z) ∈ set (map (λ(q, x, y, q'). ((q, x), y, q')) (t # ts))")
        case True
        then have "(case Mapping.lookup (h_wpi (fsm_with_precomputations_impl_from_list q (t#ts))) (qa, x) of None ⇒ {} | Some ts ⇒ ts) = {z. ((qa, x), z) ∈ set (map (λ(q, x, y, q'). ((q, x), y, q')) (t # ts))}"
          unfolding * list_as_mapping_lookup by auto
        also have "… = {a. case a of (y, q') ⇒ (qa, x, y, q') ∈ transitions_wpi (fsm_with_precomputations_impl_from_list q (t#ts))}"
          unfolding fsm_with_precomputations_impl_from_list.simps Let_def 
          by (induction ts; cases t; auto)
        finally show ?thesis .
      next
        case False
        then have "(case Mapping.lookup (h_wpi (fsm_with_precomputations_impl_from_list q (t#ts))) (qa, x) of None ⇒ {} | Some ts ⇒ ts) = {}"
          unfolding * list_as_mapping_lookup by auto 
        also have "… = {a. case a of (y, q') ⇒ (qa, x, y, q') ∈ transitions_wpi (fsm_with_precomputations_impl_from_list q (t#ts))}"
          using False unfolding fsm_with_precomputations_impl_from_list.simps Let_def 
          by (induction ts; cases t; auto)
        finally show ?thesis .
      qed
    qed
  qed

  have h_obs_prop: "(∀ q x y . h_obs_impl  (h_wpi M) q x y = (h_obs_lookup  (h_obs_wpi M) q x y))"
  proof -
    have ***:"h_obs_wpi M = (h_obs_impl_from_h  (h_wpi M))"
    proof (cases ts)
      case Nil
      then have *:"h_wpi M = Mapping.empty" and **:"h_obs_wpi M = Mapping.empty"
        unfolding M_def by auto
      show ?thesis 
        unfolding * ** h_obs_impl_from_h.simps map_values_empty by simp
    next
      case (Cons t ts')
      show ?thesis 
        unfolding Cons M_def fsm_with_precomputations_impl_from_list.simps Let_def by simp
    qed
    then show ?thesis
      unfolding h_obs_impl_from_h_invar
      by simp
  qed

  show "well_formed_fsm_with_precomputations (fsm_with_precomputations_impl_from_list q ts)"  
    using base_props transition_prop h_prop h_obs_prop
    unfolding well_formed_fsm_with_precomputations.simps  M_def[symmetric]
    by blast
qed

lemma fsm_with_precomputations_from_list_Nil_simps :
  "initial_wp (fsm_with_precomputations_from_list q []) = q"
  "states_wp (fsm_with_precomputations_from_list q []) = {q}"
  "inputs_wp (fsm_with_precomputations_from_list q []) = {}"
  "outputs_wp (fsm_with_precomputations_from_list q []) = {}"
  "transitions_wp (fsm_with_precomputations_from_list q []) = {}"
  by (transfer; auto)+
  
lemma fsm_with_precomputations_from_list_Cons_simps :
  "initial_wp (fsm_with_precomputations_from_list q (t#ts)) = (t_source t)"
  "states_wp (fsm_with_precomputations_from_list q (t#ts)) = ((image t_source (set (t#ts))) ∪ (image t_target (set (t#ts))))"
  "inputs_wp (fsm_with_precomputations_from_list q (t#ts)) = (image t_input (set (t#ts)))"
  "outputs_wp (fsm_with_precomputations_from_list q (t#ts)) = (image t_output (set (t#ts)))"
  "transitions_wp (fsm_with_precomputations_from_list q (t#ts)) = (set (t#ts))"
  by (transfer; auto)+

definition Fsm_with_precomputations :: "('a,'b,'c) fsm_with_precomputations_impl ⇒ ('a,'b,'c) fsm_with_precomputations" where
  "Fsm_with_precomputations M = Abs_fsm_with_precomputations (if well_formed_fsm_with_precomputations M then M else FSMWPI undefined {undefined} {} {} {} Mapping.empty Mapping.empty)"

lemma fsm_with_precomputations_code_abstype [code abstype] :
  "Fsm_with_precomputations (fsm_with_precomputations_impl_of_fsm_with_precomputations M) = M"
proof -
  have "well_formed_fsm_with_precomputations (fsm_with_precomputations_impl_of_fsm_with_precomputations M)"
    using fsm_with_precomputations_impl_of_fsm_with_precomputations[of M] by blast
  then show ?thesis
    unfolding Fsm_with_precomputations_def
    using fsm_with_precomputations_impl_of_fsm_with_precomputations_inverse[of M] by presburger
qed

lemma fsm_with_precomputations_impl_of_fsm_with_precomputations_code [code] :
  "fsm_with_precomputations_impl_of_fsm_with_precomputations (fsm_with_precomputations_from_list q ts) = fsm_with_precomputations_impl_from_list q ts"
  by (fact fsm_with_precomputations_from_list.rep_eq)
                                


definition FSMWP :: "('state, 'input, 'output) fsm_with_precomputations ⇒ ('state, 'input, 'output) fsm_impl" where
  "FSMWP M = FSMI (initial_wp M)
             (states_wp M)
             (inputs_wp M)
             (outputs_wp M)
             (transitions_wp M)"

code_datatype FSMWP 


subsection ‹Lifting›


declare [[code drop: fsm_impl_from_list]]
lemma fsm_impl_from_list[code] :
  "fsm_impl_from_list q ts = FSMWP (fsm_with_precomputations_from_list q ts)"
proof (induction ts)
  case Nil
  show ?case unfolding fsm_impl_from_list.simps FSMWP_def fsm_with_precomputations_from_list_Nil_simps by simp
next
  case (Cons t ts)
  show ?case unfolding fsm_impl_from_list.simps FSMWP_def fsm_with_precomputations_from_list_Cons_simps Let_def by simp
qed


declare [[code drop: fsm_impl.initial fsm_impl.states fsm_impl.inputs fsm_impl.outputs fsm_impl.transitions]]
lemma fsm_impl_FSMWP_initial[code,simp] : "fsm_impl.initial (FSMWP M) = initial_wp M"
  by (simp add: FSMWP_def) 
lemma fsm_impl_FSMWP_states[code,simp] : "fsm_impl.states (FSMWP M) = states_wp M"
  by (simp add: FSMWP_def) 
lemma fsm_impl_FSMWP_inputs[code,simp] : "fsm_impl.inputs (FSMWP M) = inputs_wp M"
  by (simp add: FSMWP_def) 
lemma fsm_impl_FSMWP_outputs[code,simp] : "fsm_impl.outputs (FSMWP M) = outputs_wp M"
  by (simp add: FSMWP_def) 
lemma fsm_impl_FSMWP_transitions[code,simp] : "fsm_impl.transitions (FSMWP M) = transitions_wp M"
  by (simp add: FSMWP_def) 


lemma well_formed_FSMWP:  "well_formed_fsm (FSMWP M)"
proof -
  have *: "well_formed_fsm_with_precomputations (fsm_with_precomputations_impl_of_fsm_with_precomputations M)"
    using fsm_with_precomputations_impl_of_fsm_with_precomputations by blast
  then have "(initial_wp M ∈ states_wp M
      ∧ finite (states_wp M)
      ∧ finite (inputs_wp M)
      ∧ finite (outputs_wp M)
      ∧ finite (transitions_wp M)
      ∧ (∀ t ∈ transitions_wp M . t_source t ∈ states_wp M ∧ 
                                t_input t ∈ inputs_wp M ∧ 
                                t_target t ∈ states_wp M ∧ 
                                t_output t ∈ outputs_wp M))" 
    unfolding well_formed_fsm_with_precomputations.simps
    by (simp add: FSM_Code_Datatype.initial_wp.rep_eq FSM_Code_Datatype.inputs_wp.rep_eq FSM_Code_Datatype.outputs_wp.rep_eq FSM_Code_Datatype.states_wp.rep_eq FSM_Code_Datatype.transitions_wp.rep_eq)
  then show ?thesis
    unfolding FSMWP_def by simp
qed




declare [[code drop: FSM_Impl.h ]]
lemma h_with_precomputations_code [code] : "FSM_Impl.h ((FSMWP M)) = (λ (q,x) . case Mapping.lookup (h_wp M) (q,x) of Some yqs ⇒ yqs | None ⇒ {})"
proof -
  have *: "⋀ q x . (case (Mapping.lookup (h_wp M) (q,x)) of Some ts ⇒ ts | None ⇒ {}) = { (y,q') . (q,x,y,q') ∈ transitions_wp M }"
    by (transfer; auto)

  have **: "fsm_impl.transitions ((FSMWP M)) = transitions_wp M" 
    by (simp add: FSMWP_def)
      
  have "⋀ q x . FSM_Impl.h ((FSMWP M)) (q,x) = (λ (q,x) . case Mapping.lookup (h_wp M) (q,x) of Some yqs ⇒ yqs | None ⇒ {}) (q,x)"
    unfolding * FSM_Impl.h.simps case_prod_unfold fst_conv snd_conv ** by blast
  then show ?thesis
    by blast
qed

declare [[code drop: FSM_Impl.h_obs ]]
lemma h_obs_with_precomputations_code [code] : "FSM_Impl.h_obs ((FSMWP M)) q x y = (h_obs_lookup  (h_obs_wp M) q x y)"
  unfolding fsm_with_precomputations_h_obs_prop
  unfolding FSM_Impl.h_obs.simps
  unfolding h_obs_impl.simps
  unfolding Let_def
  unfolding FSM_Impl.h.simps[of "FSMWP M" q x]
  unfolding fsm_with_precomputations_h_prop[of M q x]
  by auto



fun filter_states_impl :: "('a,'b,'c) fsm_with_precomputations_impl ⇒ ('a ⇒ bool) ⇒ ('a,'b,'c) fsm_with_precomputations_impl" where
  "filter_states_impl M P = (if P (initial_wpi M) 
                          then (let 
                                  h' = Mapping.filter (λ (q,x) yqs . P q) (h_wpi M);
                                  h'' = Mapping.map_values (λ _ yqs . Set.filter (λ (y,q') . P q') yqs) h'
                                in
                                   FSMWPI (initial_wpi M)
                                   (Set.filter P (states_wpi M))
                                   (inputs_wpi M)
                                   (outputs_wpi M)
                                   (Set.filter (λ t . P (t_source t) ∧ P (t_target t)) (transitions_wpi M))
                                   h''
                                   (h_obs_impl_from_h h''))   
                          else M)"

lift_definition filter_states :: "('a,'b,'c) fsm_with_precomputations ⇒ ('a ⇒ bool) ⇒ ('a,'b,'c) fsm_with_precomputations"
  is filter_states_impl
proof -
  fix M :: "('a,'b,'c) fsm_with_precomputations_impl" 
  fix P :: "('a ⇒ bool)"

  let ?M = "(filter_states_impl M P)"

  show "well_formed_fsm_with_precomputations M ⟹ well_formed_fsm_with_precomputations ?M"
  proof -
    assume assm: "well_formed_fsm_with_precomputations M"  
    show "well_formed_fsm_with_precomputations ?M"
    proof (cases "P (initial_wpi M)")
      case False
      then have "?M = M" by auto
      then show ?thesis using assm by presburger
    next
      case True

      have "initial_wpi ?M = initial_wpi M"
        unfolding filter_states_impl.simps Let_def by auto
      have "states_wpi ?M = Set.filter P (states_wpi M)"
        using True unfolding filter_states_impl.simps Let_def by auto
      have "inputs_wpi ?M = inputs_wpi M"
        unfolding filter_states_impl.simps Let_def by auto
      have "outputs_wpi ?M = outputs_wpi M"
        unfolding filter_states_impl.simps Let_def by auto
      have "transitions_wpi ?M = (Set.filter (λ t . P (t_source t) ∧ P (t_target t)) (transitions_wpi M))"
        using True unfolding filter_states_impl.simps Let_def by auto

      define h' where "h' = Mapping.filter (λ (q,x) yqs . P q) (h_wpi M)"
      define h'' where "h'' = Mapping.map_values (λ _ yqs . Set.filter (λ (y,q') . P q') yqs) h'"

      have "h_wpi ?M = h''"
        unfolding h''_def h'_def using True unfolding filter_states_impl.simps Let_def by auto
      then have "h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)"
        using True unfolding filter_states_impl.simps Let_def by auto

      have base_props: "(initial_wpi ?M ∈ states_wpi ?M
                          ∧ finite (states_wpi ?M)
                          ∧ finite (inputs_wpi ?M)
                          ∧ finite (outputs_wpi ?M)
                          ∧ finite (transitions_wpi ?M))"
        using assm True unfolding filter_states_impl.simps Let_def by auto
  

      have transition_prop: "(∀ t ∈ transitions_wpi ?M . t_source t ∈ states_wpi ?M ∧ 
                                      t_input t ∈ inputs_wpi ?M ∧ 
                                      t_target t ∈ states_wpi ?M ∧ 
                                      t_output t ∈ outputs_wpi ?M)"
        using assm True unfolding filter_states_impl.simps Let_def by auto

      
      have h_prop:"⋀ qa x .
            (case Mapping.lookup (h_wpi ?M) (qa, x) of None ⇒ {} | Some ts ⇒ ts) =
            {a. case a of (y, q') ⇒ (qa, x, y, q') ∈ transitions_wpi ?M}"
      (is "⋀ qa x . ?A qa x = ?B qa x")
      proof -
        fix q x 
        show "?A q x = ?B q x"
        proof (cases "P q")
          case False
          then have "Mapping.lookup h' (q,x) = None"
            unfolding h'_def 
            unfolding Mapping.lookup_filter case_prod_conv
            by (metis (mono_tags) not_None_eq option.simps(4) option.simps(5)) 
          then have "?A q x = {}"
            unfolding ‹h_wpi ?M = h''› h''_def 
            unfolding Mapping.lookup_map_values
            by simp 
          moreover have "?B q x = {}"
            unfolding ‹transitions_wpi ?M = (Set.filter (λ t . P (t_source t) ∧ P (t_target t)) (transitions_wpi M))›
            using False by auto
          ultimately show ?thesis by blast
        next
          case True
          then have "Mapping.lookup h' (q,x) = Mapping.lookup (h_wpi M) (q,x)"
            unfolding h'_def 
            unfolding Mapping.lookup_filter case_prod_conv
            by (cases "Mapping.lookup (h_wpi M) (q, x)"; auto)
          have "?A q x = Set.filter (λ (y,q') . P q') (case Mapping.lookup (h_wpi M) (q, x) of None ⇒ {} | Some ts ⇒ ts)"
            unfolding ‹h_wpi ?M = h''› h''_def 
            unfolding Mapping.lookup_map_values 
            unfolding ‹Mapping.lookup h' (q,x) = Mapping.lookup (h_wpi M) (q,x)› 
            by (cases "Mapping.lookup (h_wpi M) (q, x)"; auto)
          also have "… = ?B q x"
          proof -
            have *:"(case Mapping.lookup (h_wpi M) (q, x) of None ⇒ {} | Some ts ⇒ ts) = {a. case a of (y, q') ⇒ (q, x, y, q') ∈ transitions_wpi M}"
              using assm by auto
            show ?thesis
              unfolding *
              unfolding ‹transitions_wpi ?M = (Set.filter (λ t . P (t_source t) ∧ P (t_target t)) (transitions_wpi M))›
              using True
              by auto
          qed
          finally show ?thesis .
        qed
      qed

      show ?thesis
        using base_props transition_prop h_prop well_formed_h_obs_impl_from_h[OF ‹h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)›]
        unfolding well_formed_fsm_with_precomputations.simps by blast
    qed
  qed
qed

lemma filter_states_simps:
  "initial_wp (filter_states M P) = initial_wp M"
  "states_wp (filter_states M P) = (if P (initial_wp M) then Set.filter P (states_wp M) else states_wp M)"
  "inputs_wp (filter_states M P) = inputs_wp M"
  "outputs_wp (filter_states M P) = outputs_wp M"
  "transitions_wp (filter_states M P) = (if P (initial_wp M) then (Set.filter (λ t . P (t_source t) ∧ P (t_target t)) (transitions_wp M)) else transitions_wp M)"
  by (transfer; simp add: Let_def)+



declare [[code drop: FSM_Impl.filter_states ]]
lemma filter_states_with_precomputations_code [code] : "FSM_Impl.filter_states ((FSMWP M)) P = FSMWP (filter_states M P)"
  unfolding FSM_Impl.filter_states.simps Let_def
  unfolding fsm_impl_FSMWP_initial fsm_impl_FSMWP_states fsm_impl_FSMWP_inputs fsm_impl_FSMWP_outputs fsm_impl_FSMWP_transitions
  using filter_states_simps[of M P]
  by (simp add: FSMWP_def) 

  


fun create_unconnected_fsm_from_fsets_impl :: "'a ⇒ 'a fset ⇒ 'b fset ⇒ 'c fset ⇒ ('a,'b,'c) fsm_with_precomputations_impl" where
  "create_unconnected_fsm_from_fsets_impl q ns ins outs = FSMWPI q (insert q (fset ns)) (fset ins) (fset outs) {} Mapping.empty Mapping.empty"

lift_definition create_unconnected_fsm_from_fsets :: "'a ⇒ 'a fset ⇒ 'b fset ⇒ 'c fset ⇒ ('a,'b,'c) fsm_with_precomputations" 
  is create_unconnected_fsm_from_fsets_impl
proof -
  fix q :: 'a 
  fix ns 
  fix ins :: "'b fset" 
  fix outs :: "'c fset"

  let ?M = "(create_unconnected_fsm_from_fsets_impl q ns ins outs)"

  show "well_formed_fsm_with_precomputations (create_unconnected_fsm_from_fsets_impl q ns ins outs)"
  proof -

    have base_props: "(initial_wpi ?M ∈ states_wpi ?M
                        ∧ finite (states_wpi ?M)
                        ∧ finite (inputs_wpi ?M)
                        ∧ finite (outputs_wpi ?M)
                        ∧ finite (transitions_wpi ?M))"
      by auto


    have transition_prop: "(∀ t ∈ transitions_wpi ?M . t_source t ∈ states_wpi ?M ∧ 
                                    t_input t ∈ inputs_wpi ?M ∧ 
                                    t_target t ∈ states_wpi ?M ∧ 
                                    t_output t ∈ outputs_wpi ?M)"
      by auto

    have *: "(h_wpi ?M) = Mapping.empty"
      by auto
    have **: "transitions_wpi ?M = {}"
      by auto
    have ***: "(h_obs_wpi ?M) = Mapping.empty"
      by auto

    have h_prop:"⋀ qa x .
          (case Mapping.lookup (h_wpi ?M) (qa, x) of None ⇒ {} | Some ts ⇒ ts) =
          {a. case a of (y, q') ⇒ (qa, x, y, q') ∈ transitions_wpi ?M}"
      unfolding * ** Mapping.lookup_empty by auto

    have h_obs_prop: "⋀ q x y . h_obs_impl  (h_wpi ?M) q x y = h_obs_lookup  (h_obs_wpi ?M) q x y"
      unfolding h_obs_impl.simps Let_def
      unfolding * *** Mapping.lookup_empty
      by (simp add: Set.filter_def) 

    show ?thesis
      using base_props transition_prop h_prop h_obs_prop
      unfolding well_formed_fsm_with_precomputations.simps by blast
  qed
qed

lemma fsm_with_precomputations_impl_of_code [code] :
  "fsm_with_precomputations_impl_of_fsm_with_precomputations (create_unconnected_fsm_from_fsets q ns ins outs) = create_unconnected_fsm_from_fsets_impl q ns ins outs"
  by (fact create_unconnected_fsm_from_fsets.rep_eq)

lemma create_unconnected_fsm_from_fsets_simps:
  "initial_wp (create_unconnected_fsm_from_fsets q ns ins outs) = q"
  "states_wp (create_unconnected_fsm_from_fsets q ns ins outs) = (insert q (fset ns))"
  "inputs_wp (create_unconnected_fsm_from_fsets q ns ins outs) = fset ins"
  "outputs_wp (create_unconnected_fsm_from_fsets q ns ins outs) = fset outs"
  "transitions_wp (create_unconnected_fsm_from_fsets q ns ins outs) = {}"
  by (transfer; simp add: Let_def)+


declare [[code drop: FSM_Impl.create_unconnected_fsm_from_fsets ]]
lemma create_unconnected_fsm_with_precomputations_code [code] : "FSM_Impl.create_unconnected_fsm_from_fsets q ns ins outs = FSMWP (create_unconnected_fsm_from_fsets q ns ins outs)"
  unfolding FSM_Impl.create_unconnected_fsm_from_fsets.simps 
  unfolding FSMWP_def
  unfolding create_unconnected_fsm_from_fsets_simps
  by presburger 


fun add_transitions_impl :: "('a,'b,'c) fsm_with_precomputations_impl ⇒ ('a × 'b × 'c × 'a) set ⇒ ('a,'b,'c) fsm_with_precomputations_impl" where
  "add_transitions_impl M ts = (if (∀ t ∈ ts . t_source t ∈ states_wpi M ∧ t_input t ∈ inputs_wpi M ∧ t_output t ∈ outputs_wpi M ∧ t_target t ∈ states_wpi M)
    then (let ts' = ((transitions_wpi M) ∪ ts);
              h' = set_as_mapping_image ts' (λ(q,x,y,q') . ((q,x),y,q'))
          in FSMWPI
             (initial_wpi M)
             (states_wpi M)
             (inputs_wpi M)
             (outputs_wpi M)
             ts'
             h'
             (h_obs_impl_from_h h'))
    else M)"

(* TODO: consider using Mapping.combine in add_transitions to avoid recomputation of h on the already known transitions *)

lift_definition add_transitions :: "('a,'b,'c) fsm_with_precomputations ⇒ ('a × 'b × 'c × 'a) set ⇒ ('a,'b,'c) fsm_with_precomputations"
  is add_transitions_impl
proof -
  fix M :: "('a,'b,'c) fsm_with_precomputations_impl"
  fix ts 

  let ?M = "(add_transitions_impl M ts)"

  show "well_formed_fsm_with_precomputations M ⟹ well_formed_fsm_with_precomputations ?M"
  proof -
    assume assm: "well_formed_fsm_with_precomputations M"

    show "well_formed_fsm_with_precomputations ?M"
    proof (cases "(∀ t ∈ ts . t_source t ∈ states_wpi M ∧ t_input t ∈ inputs_wpi M ∧ t_output t ∈ outputs_wpi M ∧ t_target t ∈ states_wpi M)")
      case False
      then have "?M = M" by auto
      then show ?thesis using assm by presburger
    next
      case True
      then have "ts ⊆ states_wpi M × inputs_wpi M × outputs_wpi M × states_wpi M" 
        by fastforce
      moreover have "finite (states_wpi M × inputs_wpi M × outputs_wpi M × states_wpi M)" 
        using assm unfolding well_formed_fsm_with_precomputations.simps by blast
      ultimately have "finite ts"
        using rev_finite_subset by auto 

      have "initial_wpi ?M = initial_wpi M"
        unfolding add_transitions_impl.simps Let_def by auto
      have "states_wpi ?M = states_wpi M"
        unfolding add_transitions_impl.simps Let_def by auto
      have "inputs_wpi ?M = inputs_wpi M"
        unfolding add_transitions_impl.simps Let_def by auto
      have "outputs_wpi ?M = outputs_wpi M"
        unfolding add_transitions_impl.simps Let_def by auto
      have "transitions_wpi ?M = (transitions_wpi M) ∪ ts"
        using True unfolding add_transitions_impl.simps Let_def by auto
    
      define ts' where "ts' = ((transitions_wpi M) ∪ ts)"
      define h' where "h' = set_as_mapping_image ts' (λ(q,x,y,q') . ((q,x),y,q'))"

      have "h_wpi ?M = set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q'))"
        unfolding h'_def ts'_def using True unfolding add_transitions_impl.simps Let_def by auto
      have "h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)"
        unfolding h'_def ts'_def using True unfolding add_transitions_impl.simps Let_def by auto

      have base_props: "(initial_wpi ?M ∈ states_wpi ?M
                          ∧ finite (states_wpi ?M)
                          ∧ finite (inputs_wpi ?M)
                          ∧ finite (outputs_wpi ?M)
                          ∧ finite (transitions_wpi ?M))"
        using assm True ‹finite ts› unfolding add_transitions_impl.simps Let_def by auto
  

      have transition_prop: "(∀ t ∈ transitions_wpi ?M . t_source t ∈ states_wpi ?M ∧ 
                                      t_input t ∈ inputs_wpi ?M ∧ 
                                      t_target t ∈ states_wpi ?M ∧ 
                                      t_output t ∈ outputs_wpi ?M)"
        using assm True unfolding add_transitions_impl.simps Let_def by auto

      
      have h_prop:"⋀ qa x .
            (case Mapping.lookup (h_wpi ?M) (qa, x) of None ⇒ {} | Some ts ⇒ ts) =
            {a. case a of (y, q') ⇒ (qa, x, y, q') ∈ transitions_wpi ?M}"
      (is "⋀ qa x . ?A qa x = ?B qa x")
      proof -
        fix q x 
        show "?A q x = ?B q x"
        proof -

          have *:"Mapping.lookup (h_wpi ?M) = (set_as_map (image (λ(q,x,y,q') . ((q,x),y,q')) (transitions_wpi ?M)))"
            unfolding ‹h_wpi ?M = set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q'))› using set_as_mapping_image_ob
            by auto 

          have **: "⋀ z . ((q, x), z) ∈ (λ(q, x, y, q'). ((q, x), y, q')) ` (transitions_wpi ?M) = ((q,x,z) ∈ (transitions_wpi ?M))"
            by force

          show ?thesis 
            unfolding * set_as_map_def ** by force
        qed
      qed

      show ?thesis
        using base_props transition_prop h_prop well_formed_h_obs_impl_from_h[OF ‹h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)›]
        unfolding well_formed_fsm_with_precomputations.simps by blast
    qed
  qed
qed

lemma add_transitions_simps:
  "initial_wp (add_transitions M ts) = initial_wp M"
  "states_wp (add_transitions M ts) = states_wp M"
  "inputs_wp (add_transitions M ts) = inputs_wp M"
  "outputs_wp (add_transitions M ts) = outputs_wp M"
  "transitions_wp (add_transitions M ts) = (if (∀ t ∈ ts . t_source t ∈ states_wp M ∧ t_input t ∈ inputs_wp M ∧ t_output t ∈ outputs_wp M ∧ t_target t ∈ states_wp M)
                                          then transitions_wp M ∪ ts else transitions_wp M)"
  by (transfer; simp add: Let_def)+


declare [[code drop: FSM_Impl.add_transitions ]]
lemma add_transitions_with_precomputations_code [code] : "FSM_Impl.add_transitions ((FSMWP M)) ts = FSMWP (add_transitions M ts)"
  unfolding FSM_Impl.add_transitions.simps 
  unfolding fsm_impl_FSMWP_initial fsm_impl_FSMWP_states fsm_impl_FSMWP_inputs fsm_impl_FSMWP_outputs fsm_impl_FSMWP_transitions
  unfolding FSMWP_def
  unfolding add_transitions_simps  
  by presburger 



fun rename_states_impl :: "('a,'b,'c) fsm_with_precomputations_impl ⇒ ('a ⇒ 'd) ⇒ ('d,'b,'c) fsm_with_precomputations_impl" where
  "rename_states_impl M f = (let ts = ((λt . (f (t_source t), t_input t, t_output t, f (t_target t))) ` transitions_wpi M);
                                 h' = set_as_mapping_image ts (λ(q,x,y,q') . ((q,x),y,q'))
                             in
                              FSMWPI (f (initial_wpi M))
                                     (f ` states_wpi M)
                                     (inputs_wpi M)
                                     (outputs_wpi M)
                                     ts
                                     h'
                                     (h_obs_impl_from_h h'))"

lift_definition rename_states :: "('a,'b,'c) fsm_with_precomputations ⇒('a ⇒ 'd) ⇒ ('d,'b,'c) fsm_with_precomputations"
  is rename_states_impl
proof -
  fix M :: "('a,'b,'c) fsm_with_precomputations_impl"
  fix f :: "('a ⇒ 'd)"

  let ?M = "(rename_states_impl M f)"

  show "well_formed_fsm_with_precomputations M ⟹ well_formed_fsm_with_precomputations ?M"
  proof -
    assume assm: "well_formed_fsm_with_precomputations M"

    show "well_formed_fsm_with_precomputations ?M"
    proof -

      have "initial_wpi ?M = f (initial_wpi M)"
        unfolding rename_states_impl.simps Let_def by auto
      have "states_wpi ?M = f ` states_wpi M"
        unfolding rename_states_impl.simps Let_def by auto
      have "inputs_wpi ?M = inputs_wpi M"
        unfolding rename_states_impl.simps Let_def by auto
      have "outputs_wpi ?M = outputs_wpi M"
        unfolding rename_states_impl.simps Let_def by auto
      have "transitions_wpi ?M = ((λt . (f (t_source t), t_input t, t_output t, f (t_target t))) ` transitions_wpi M)"
        unfolding rename_states_impl.simps Let_def by auto

      define ts where "ts = ((λt . (f (t_source t), t_input t, t_output t, f (t_target t))) ` transitions_wpi M)"
      define h' where "h' = set_as_mapping_image ts (λ(q,x,y,q') . ((q,x),y,q'))"

      have "transitions_wpi ?M = ts"
        unfolding ts_def rename_states_impl.simps Let_def by auto
      then have "h_wpi ?M = set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q'))"
        unfolding h'_def unfolding rename_states_impl.simps Let_def by auto
      then have "h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)"
        unfolding rename_states_impl.simps Let_def by auto

      have base_props: "(initial_wpi ?M ∈ states_wpi ?M
                          ∧ finite (states_wpi ?M)
                          ∧ finite (inputs_wpi ?M)
                          ∧ finite (outputs_wpi ?M)
                          ∧ finite (transitions_wpi ?M))"
        using assm  unfolding rename_states_impl.simps Let_def by auto
  

      have transition_prop: "(∀ t ∈ transitions_wpi ?M . t_source t ∈ states_wpi ?M ∧ 
                                      t_input t ∈ inputs_wpi ?M ∧ 
                                      t_target t ∈ states_wpi ?M ∧ 
                                      t_output t ∈ outputs_wpi ?M)"
        using assm unfolding rename_states_impl.simps Let_def by auto


      show ?thesis
        using base_props transition_prop 
              well_formed_h_set_as_mapping[OF ‹h_wpi ?M = set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q'))›] 
              well_formed_h_obs_impl_from_h[OF ‹h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)›]
        unfolding well_formed_fsm_with_precomputations.simps by blast
    qed
  qed
qed


lemma rename_states_simps:
  "initial_wp (rename_states M f) = f (initial_wp M)"
  "states_wp (rename_states M f) = f ` states_wp M"
  "inputs_wp (rename_states M f) = inputs_wp M"
  "outputs_wp (rename_states M f) = outputs_wp M"
  "transitions_wp (rename_states M f) = ((λt . (f (t_source t), t_input t, t_output t, f (t_target t))) ` transitions_wp M)"
  by (transfer; simp add: Let_def)+

declare [[code drop: FSM_Impl.rename_states ]]
lemma rename_states_with_precomputations_code[code] : "FSM_Impl.rename_states ((FSMWP M)) f = FSMWP (rename_states M f)"
  unfolding FSM_Impl.rename_states.simps 
  unfolding fsm_impl_FSMWP_initial fsm_impl_FSMWP_states fsm_impl_FSMWP_inputs fsm_impl_FSMWP_outputs fsm_impl_FSMWP_transitions
  unfolding FSMWP_def
  unfolding rename_states_simps  
  by presburger 


fun filter_transitions_impl :: "('a,'b,'c) fsm_with_precomputations_impl ⇒ (('a × 'b × 'c × 'a) ⇒ bool) ⇒ ('a,'b,'c) fsm_with_precomputations_impl" where
  "filter_transitions_impl M P = (let ts = (Set.filter P (transitions_wpi M));
                                            h' = (set_as_mapping_image ts (λ(q,x,y,q') . ((q,x),y,q')))
                                  in FSMWPI (initial_wpi M)
                                            (states_wpi M)
                                            (inputs_wpi M)
                                            (outputs_wpi M)
                                            ts
                                            h'
                                            (h_obs_impl_from_h h'))"

lift_definition filter_transitions :: "('a,'b,'c) fsm_with_precomputations ⇒ (('a × 'b × 'c × 'a) ⇒ bool) ⇒ ('a,'b,'c) fsm_with_precomputations"
  is filter_transitions_impl
proof -
  fix M :: "('a,'b,'c) fsm_with_precomputations_impl"
  fix P :: "(('a × 'b × 'c × 'a) ⇒ bool) "

  let ?M = "filter_transitions_impl M P"

  show "well_formed_fsm_with_precomputations M ⟹ well_formed_fsm_with_precomputations ?M"
  proof -
    assume assm: "well_formed_fsm_with_precomputations M"

    show "well_formed_fsm_with_precomputations ?M"
    proof -

      have "initial_wpi ?M = initial_wpi M"
        unfolding filter_transitions_impl.simps Let_def by auto
      have "states_wpi ?M = states_wpi M"
        unfolding filter_transitions_impl.simps Let_def by auto
      have "inputs_wpi ?M = inputs_wpi M"
        unfolding filter_transitions_impl.simps Let_def by auto
      have "outputs_wpi ?M = outputs_wpi M"
        unfolding filter_transitions_impl.simps Let_def by auto
      have "transitions_wpi ?M = (Set.filter P (transitions_wpi M))"
        unfolding filter_transitions_impl.simps Let_def by auto

      have "h_wpi ?M = (set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q')))"
        unfolding filter_transitions_impl.simps Let_def by auto
      then have "h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)"
        unfolding filter_transitions_impl.simps Let_def by auto

      have base_props: "(initial_wpi ?M ∈ states_wpi ?M
                          ∧ finite (states_wpi ?M)
                          ∧ finite (inputs_wpi ?M)
                          ∧ finite (outputs_wpi ?M)
                          ∧ finite (transitions_wpi ?M))"
        using assm  unfolding filter_transitions_impl.simps Let_def by auto
  

      have transition_prop: "(∀ t ∈ transitions_wpi ?M . t_source t ∈ states_wpi ?M ∧ 
                                      t_input t ∈ inputs_wpi ?M ∧ 
                                      t_target t ∈ states_wpi ?M ∧ 
                                      t_output t ∈ outputs_wpi ?M)"
        using assm unfolding filter_transitions_impl.simps Let_def by auto


      show ?thesis
        using base_props transition_prop 
              well_formed_h_set_as_mapping[OF ‹h_wpi ?M = set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q'))›] 
              well_formed_h_obs_impl_from_h[OF ‹h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)›]
        unfolding well_formed_fsm_with_precomputations.simps by blast
    qed
  qed
qed

lemma filter_transitions_simps:
  "initial_wp (filter_transitions M P) = initial_wp M"
  "states_wp (filter_transitions M P) = states_wp M"
  "inputs_wp (filter_transitions M P) = inputs_wp M"
  "outputs_wp (filter_transitions M P) = outputs_wp M"
  "transitions_wp (filter_transitions M P) = Set.filter P (transitions_wp M)"
  by (transfer; simp add: Let_def)+

declare [[code drop: FSM_Impl.filter_transitions ]]
lemma filter_transitions_with_precomputations_code [code] : "FSM_Impl.filter_transitions ((FSMWP M)) P = FSMWP (filter_transitions M P)"
  unfolding FSM_Impl.filter_transitions.simps 
  unfolding fsm_impl_FSMWP_initial fsm_impl_FSMWP_states fsm_impl_FSMWP_inputs fsm_impl_FSMWP_outputs fsm_impl_FSMWP_transitions
  unfolding FSMWP_def
  unfolding filter_transitions_simps  
  by presburger 


fun initial_singleton_impl :: "('a,'b,'c) fsm_with_precomputations_impl ⇒ ('a,'b,'c) fsm_with_precomputations_impl" where
  "initial_singleton_impl M = FSMWPI (initial_wpi M)
                                     {initial_wpi M}
                                     (inputs_wpi M)
                                     (outputs_wpi M)
                                     {}
                                     Mapping.empty 
                                     Mapping.empty"

lemma set_as_mapping_empty :
  "set_as_mapping_image {} f = Mapping.empty"
proof -
  obtain m where "set_as_mapping_image {} f = m" and "Mapping.lookup m = set_as_map (f ` {})"
    using set_as_mapping_image_ob by blast
  then have "⋀ k . Mapping.lookup m k = None"
    unfolding set_as_map_def
    by simp 
  then show ?thesis
    unfolding ‹set_as_mapping_image {} f = m›
    by (simp add: mapping_eqI) 
qed

lemma h_obs_from_impl_h : "h_obs_impl_from_h Mapping.empty = Mapping.empty"
  unfolding h_obs_impl_from_h.simps
  by (simp add: map_values_empty)

lift_definition initial_singleton :: "('a,'b,'c) fsm_with_precomputations ⇒ ('a,'b,'c) fsm_with_precomputations"
  is initial_singleton_impl
proof -
  fix M :: "('a,'b,'c) fsm_with_precomputations_impl"

  let ?M = "initial_singleton_impl M"

  show "well_formed_fsm_with_precomputations M ⟹ well_formed_fsm_with_precomputations ?M"
  proof -
    assume assm: "well_formed_fsm_with_precomputations M"

    show "well_formed_fsm_with_precomputations ?M"
    proof -

      have "transitions_wpi ?M = {}"
        unfolding filter_transitions_impl.simps Let_def by auto

      have "h_wpi ?M = Mapping.empty" and "h_obs_wpi ?M = Mapping.empty"
        unfolding filter_transitions_impl.simps Let_def by auto
      have "h_wpi ?M = (set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q')))"
        unfolding ‹h_wpi ?M = Mapping.empty› ‹transitions_wpi ?M = {}›
        unfolding set_as_mapping_empty by presburger
      have "h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)"
        unfolding ‹h_wpi ?M = Mapping.empty› ‹h_obs_wpi ?M = Mapping.empty›
        unfolding h_obs_from_impl_h by simp

      have base_props: "(initial_wpi ?M ∈ states_wpi ?M
                          ∧ finite (states_wpi ?M)
                          ∧ finite (inputs_wpi ?M)
                          ∧ finite (outputs_wpi ?M)
                          ∧ finite (transitions_wpi ?M))"
        using assm  unfolding filter_transitions_impl.simps Let_def by auto
  

      have transition_prop: "(∀ t ∈ transitions_wpi ?M . t_source t ∈ states_wpi ?M ∧ 
                                      t_input t ∈ inputs_wpi ?M ∧ 
                                      t_target t ∈ states_wpi ?M ∧ 
                                      t_output t ∈ outputs_wpi ?M)"
        using assm unfolding filter_transitions_impl.simps Let_def by auto


      show ?thesis
        using base_props transition_prop 
              well_formed_h_set_as_mapping[OF ‹h_wpi ?M = set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q'))›] 
              well_formed_h_obs_impl_from_h[OF ‹h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)›]
        unfolding well_formed_fsm_with_precomputations.simps by blast
    qed
  qed
qed

lemma initial_singleton_simps:
  "initial_wp (initial_singleton M) = initial_wp M"
  "states_wp (initial_singleton M) = {initial_wp M}"
  "inputs_wp (initial_singleton M) = inputs_wp M"
  "outputs_wp (initial_singleton M) = outputs_wp M"
  "transitions_wp (initial_singleton M) = {}"
  by (transfer; simp add: Let_def)+

declare [[code drop: FSM_Impl.initial_singleton]]
lemma initial_singleton_with_precomputations_code[code] : "FSM_Impl.initial_singleton ((FSMWP M)) = FSMWP (initial_singleton M)"
  unfolding FSM_Impl.initial_singleton.simps 
  unfolding fsm_impl_FSMWP_initial fsm_impl_FSMWP_states fsm_impl_FSMWP_inputs fsm_impl_FSMWP_outputs fsm_impl_FSMWP_transitions
  unfolding FSMWP_def
  unfolding initial_singleton_simps  
  by presburger 


fun canonical_separator'_impl :: "('a,'b,'c) fsm_with_precomputations_impl ⇒ (('a × 'a),'b,'c) fsm_with_precomputations_impl ⇒ 'a ⇒ 'a ⇒ (('a × 'a) + 'a,'b,'c) fsm_with_precomputations_impl" where
  "canonical_separator'_impl M P q1 q2 = (if initial_wpi P = (q1,q2) 
  then
    (let f'  = set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions_wpi M));
         f   = (λqx . (case f' qx of Some yqs ⇒ yqs | None ⇒ {}));
         shifted_transitions' = shifted_transitions (transitions_wpi P);
         distinguishing_transitions_lr = distinguishing_transitions f q1 q2 (states_wpi P) (inputs_wpi P);
         ts = shifted_transitions' ∪ distinguishing_transitions_lr;
         h' = set_as_mapping_image ts (λ(q,x,y,q') . ((q,x),y,q'))
     in 
  
      FSMWPI (Inl (q1,q2))
      ((image Inl (states_wpi P)) ∪ {Inr q1, Inr q2})
      (inputs_wpi M ∪ inputs_wpi P)
      (outputs_wpi M ∪ outputs_wpi P)
      ts
      h'
      (h_obs_impl_from_h h'))
  else FSMWPI (Inl (q1,q2)) {Inl (q1,q2)} {} {} {} Mapping.empty Mapping.empty)"

lemma canonical_separator'_impl_refined[code]:
  "canonical_separator'_impl M P q1 q2 = (if initial_wpi P = (q1,q2) 
  then
    (let f'  = set_as_mapping_image (transitions_wpi M) (λ(q,x,y,q') . ((q,x),y));
         f   = (λqx . (case Mapping.lookup f' qx of Some yqs ⇒ yqs | None ⇒ {}));
         shifted_transitions' = shifted_transitions (transitions_wpi P);
         distinguishing_transitions_lr = distinguishing_transitions f q1 q2 (states_wpi P) (inputs_wpi P);
         ts = shifted_transitions' ∪ distinguishing_transitions_lr;
         h' = set_as_mapping_image ts (λ(q,x,y,q') . ((q,x),y,q'))
     in 
  
      FSMWPI (Inl (q1,q2))
      ((image Inl (states_wpi P)) ∪ {Inr q1, Inr q2})
      (inputs_wpi M ∪ inputs_wpi P)
      (outputs_wpi M ∪ outputs_wpi P)
      ts
      h'
      (h_obs_impl_from_h h'))
  else FSMWPI (Inl (q1,q2)) {Inl (q1,q2)} {} {} {} Mapping.empty Mapping.empty)"
  unfolding canonical_separator'_impl.simps 
  using set_as_mapping_image_ob[of "(transitions_wpi M)" "(λ(q,x,y,q') . ((q,x),y))"]
  by fastforce


lift_definition canonical_separator' :: "('a,'b,'c) fsm_with_precomputations ⇒ (('a × 'a),'b,'c) fsm_with_precomputations ⇒ 'a ⇒ 'a ⇒ (('a × 'a) + 'a,'b,'c) fsm_with_precomputations"
  is canonical_separator'_impl
proof -
  fix M :: "('a,'b,'c) fsm_with_precomputations_impl"
  fix P q1 q2
  show "well_formed_fsm_with_precomputations M ⟹ well_formed_fsm_with_precomputations P ⟹ well_formed_fsm_with_precomputations (canonical_separator'_impl M P q1 q2)"
  proof -
    assume a1: "well_formed_fsm_with_precomputations M"
    assume a2: "well_formed_fsm_with_precomputations P"

    let ?M = "canonical_separator'_impl M P q1 q2"

    show "well_formed_fsm_with_precomputations ?M"
    proof (cases "initial_wpi P = (q1,q2)")
      case False

      have "h_wpi ?M = Mapping.empty" and "h_obs_wpi ?M = Mapping.empty" and "transitions_wpi ?M = {}"
        using False unfolding canonical_separator'_impl.simps Let_def by auto
      have "h_wpi ?M = (set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q')))"
        unfolding ‹h_wpi ?M = Mapping.empty› ‹transitions_wpi ?M = {}›
        unfolding set_as_mapping_empty by presburger
      have "h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)"
        unfolding ‹h_wpi ?M = Mapping.empty› ‹h_obs_wpi ?M = Mapping.empty›
        unfolding h_obs_from_impl_h by simp

      have base_props: "(initial_wpi ?M ∈ states_wpi ?M
                          ∧ finite (states_wpi ?M)
                          ∧ finite (inputs_wpi ?M)
                          ∧ finite (outputs_wpi ?M)
                          ∧ finite (transitions_wpi ?M))"
        using a1 False unfolding canonical_separator'_impl.simps Let_def by auto
  

      have transition_prop: "(∀ t ∈ transitions_wpi ?M . t_source t ∈ states_wpi ?M ∧ 
                                      t_input t ∈ inputs_wpi ?M ∧ 
                                      t_target t ∈ states_wpi ?M ∧ 
                                      t_output t ∈ outputs_wpi ?M)"
        using a1 False unfolding canonical_separator'_impl.simps Let_def by auto


      show ?thesis
        using base_props transition_prop 
              well_formed_h_set_as_mapping[OF ‹h_wpi ?M = set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q'))›] 
              well_formed_h_obs_impl_from_h[OF ‹h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)›]
        unfolding well_formed_fsm_with_precomputations.simps by blast
    next
      case True

      let ?f = "(λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions_wpi M))) qx of Some yqs ⇒ yqs | None ⇒ {}))"
  
      have "⋀ qx . (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions_wpi M))) qx of Some yqs ⇒ yqs | None ⇒ {})) qx = (λ qx . {z. (qx, z) ∈ (λ(q, x, y, q'). ((q, x), y)) ` transitions_wpi M}) qx"
        by (metis (mono_tags, lifting) Collect_cong Collect_mem_eq set_as_map_containment set_as_map_elem)
      moreover have "⋀ qx . (λ qx . {z. (qx, z) ∈ (λ(q, x, y, q'). ((q, x), y)) ` transitions_wpi M}) qx = (λ qx . {y | y . ∃ q' . (fst qx, snd qx, y, q') ∈ transitions_wpi M}) qx"
        by force
      ultimately have *:" ?f = (λ qx . {y | y . ∃ q' . (fst qx, snd qx, y, q') ∈ transitions_wpi M})" 
        by blast
        
      let ?shifted_transitions' = "shifted_transitions (transitions_wpi P)"
      let ?distinguishing_transitions_lr = "distinguishing_transitions ?f q1 q2 (states_wpi P) (inputs_wpi P)"
      let ?ts = "?shifted_transitions' ∪ ?distinguishing_transitions_lr"
    
      have "states_wpi ?M = (image Inl (states_wpi P)) ∪ {Inr q1, Inr q2}"
      and  "transitions_wpi ?M = ?ts"
        unfolding canonical_separator'_impl.simps Let_def True by simp+
  
      have p2: "finite (states_wpi ?M)"
        unfolding ‹states_wpi ?M = (image Inl (states_wpi P)) ∪ {Inr q1, Inr q2}› using a2 by auto
    
      have "initial_wpi ?M = Inl (q1,q2)" by auto
      then have p1: "initial_wpi ?M ∈ states_wpi ?M" 
        using a1 a2 unfolding canonical_separator'.simps True by auto
      have p3: "finite (inputs_wpi ?M)"
        using a1 a2 by auto
      have p4: "finite (outputs_wpi ?M)"
        using a1 a2 by auto
  
      have "finite (states_wpi P × inputs_wpi P)"
        using a2 by auto
      moreover have **: "⋀ x q1 . finite ({y |y. ∃q'. (fst (q1, x), snd (q1, x), y, q') ∈ transitions_wpi M})"
      proof - 
        fix x q1
        have "{y |y. ∃q'. (fst (q1, x), snd (q1, x), y, q') ∈ transitions_wpi M} = {t_output t | t . t ∈ transitions_wpi M ∧ t_source t = q1 ∧ t_input t = x}"
          by auto
        then have "{y |y. ∃q'. (fst (q1, x), snd (q1, x), y, q') ∈ transitions_wpi M} ⊆ image t_output (transitions_wpi M)"
          unfolding fst_conv snd_conv by blast
        moreover have "finite (image t_output (transitions_wpi M))"
          using a1 by auto
        ultimately show "finite ({y |y. ∃q'. (fst (q1, x), snd (q1, x), y, q') ∈ transitions_wpi M})"
          by (simp add: finite_subset)
      qed
      ultimately have "finite ?distinguishing_transitions_lr"
        unfolding * distinguishing_transitions_def by force
      moreover have "finite ?shifted_transitions'"
        unfolding shifted_transitions_def using a2 by auto
      ultimately have "finite ?ts" by blast
      then have p5: "finite (transitions_wpi ?M)"
        by simp
       
      have "inputs_wpi ?M = inputs_wpi M ∪ inputs_wpi P"
        using True by auto
      have "outputs_wpi ?M = outputs_wpi M ∪ outputs_wpi P "
        using True by auto
    
      have "⋀ t . t ∈ ?shifted_transitions' ⟹ t_source t ∈ states_wpi ?M ∧ t_target t ∈ states_wpi ?M"
        unfolding ‹states_wpi ?M = (image Inl (states_wpi P)) ∪ {Inr q1, Inr q2}› shifted_transitions_def 
        using a2 by auto
      moreover have "⋀ t . t ∈ ?distinguishing_transitions_lr ⟹ t_source t ∈ states_wpi ?M ∧ t_target t ∈ states_wpi ?M"
        unfolding ‹states_wpi ?M = (image Inl (states_wpi P)) ∪ {Inr q1, Inr q2}› distinguishing_transitions_def * by force
      ultimately have "⋀ t . t ∈ ?ts ⟹ t_source t ∈ states_wpi ?M ∧ t_target t ∈ states_wpi ?M"
        by blast
      moreover have "⋀ t . t ∈ ?shifted_transitions' ⟹ t_input t ∈ inputs_wpi ?M ∧ t_output t ∈ outputs_wpi ?M"
      proof -
        have "⋀ t . t ∈ ?shifted_transitions' ⟹ t_input t ∈ inputs_wpi P ∧ t_output t ∈ outputs_wpi P"
          unfolding shifted_transitions_def using a2 by auto
        then show "⋀ t . t ∈ ?shifted_transitions' ⟹ t_input t ∈ inputs_wpi ?M ∧ t_output t ∈ outputs_wpi ?M"
          unfolding ‹inputs_wpi ?M = inputs_wpi M ∪ inputs_wpi P›
                    ‹outputs_wpi ?M = outputs_wpi M ∪ outputs_wpi P› by blast
      qed
      moreover have "⋀ t . t ∈ ?distinguishing_transitions_lr ⟹ t_input t ∈ inputs_wpi ?M ∧ t_output t ∈ outputs_wpi ?M"
        unfolding * distinguishing_transitions_def using a1 a2 True by auto
      ultimately have p6: "(∀t∈transitions_wpi ?M.
                t_source t ∈ states_wpi ?M ∧
                t_input t ∈ inputs_wpi ?M ∧ t_target t ∈ states_wpi ?M ∧
                                                 t_output t ∈ outputs_wpi ?M)"
        unfolding ‹transitions_wpi ?M = ?ts› by blast
  
      have "h_wpi ?M = set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q'))"
       and "h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)"
        using True unfolding canonical_separator'_impl.simps Let_def by auto
  
      show "well_formed_fsm_with_precomputations ?M"
        using p1 p2 p3 p4 p5 p6 
        using well_formed_h_set_as_mapping[OF ‹h_wpi ?M = set_as_mapping_image (transitions_wpi ?M) (λ(q,x,y,q') . ((q,x),y,q'))›] 
              well_formed_h_obs_impl_from_h[OF ‹h_obs_wpi ?M = h_obs_impl_from_h (h_wpi ?M)›]
        unfolding well_formed_fsm_with_precomputations.simps by blast
    qed
  qed
qed

lemma canonical_separator'_simps :
        "initial_wp (canonical_separator' M P q1 q2) = Inl (q1,q2)"
        "states_wp (canonical_separator' M P q1 q2) = (if initial_wp P = (q1,q2) then (image Inl (states_wp P)) ∪ {Inr q1, Inr q2} else {Inl (q1,q2)})"
        "inputs_wp (canonical_separator' M P q1 q2) = (if initial_wp P = (q1,q2) then inputs_wp M ∪ inputs_wp P else {})"
        "outputs_wp (canonical_separator' M P q1 q2) = (if initial_wp P = (q1,q2) then outputs_wp M ∪ outputs_wp P else {})"
        "transitions_wp (canonical_separator' M P q1 q2) = (if initial_wp P = (q1,q2) then shifted_transitions (transitions_wp P) ∪ distinguishing_transitions (λ (q,x) . {y . ∃ q' . (q,x,y,q') ∈ transitions_wp M}) q1 q2 (states_wp P) (inputs_wp P) else {})"
  unfolding h_out_impl_helper by (transfer; simp add: Let_def)+


declare [[code drop: FSM_Impl.canonical_separator']]
lemma canonical_separator_with_precomputations_code [code] : "FSM_Impl.canonical_separator' ((FSMWP M)) ((FSMWP P)) q1 q2 = FSMWP (canonical_separator' M P q1 q2)"
proof -

  have *:"⋀ M1 M2 . (M1 = M2) = (fsm_impl.initial M1 = fsm_impl.initial M2 
                                ∧ fsm_impl.states M1 = fsm_impl.states M2 
                                ∧ fsm_impl.inputs M1 = fsm_impl.inputs M2 
                                ∧ fsm_impl.outputs M1 = fsm_impl.outputs M2 
                                ∧ fsm_impl.transitions M1 = fsm_impl.transitions M2 )"
    by (meson fsm_impl.expand)

  show ?thesis
    unfolding *
    unfolding FSM_Impl.canonical_separator'_simps
    unfolding fsm_impl_FSMWP_initial fsm_impl_FSMWP_states fsm_impl_FSMWP_inputs fsm_impl_FSMWP_outputs fsm_impl_FSMWP_transitions
    unfolding canonical_separator'_simps  
    by blast
qed


fun product_impl :: "('a,'b,'c) fsm_with_precomputations_impl ⇒ ('d,'b,'c) fsm_with_precomputations_impl ⇒ ('a × 'd,'b,'c) fsm_with_precomputations_impl" where
  "product_impl A B = (let ts = (image (λ((qA,x,y,qA'), (qB,x',y',qB')) . ((qA,qB),x,y,(qA',qB'))) (Set.filter (λ((qA,x,y,qA'), (qB,x',y',qB')) . x = x' ∧ y = y') (⋃(image (λ tA . image (λ tB . (tA,tB)) (transitions_wpi B)) (transitions_wpi A)))));
                           h' = set_as_mapping_image ts (λ(q,x,y,q') . ((q,x),y,q'))
                        in
                          FSMWPI ((initial_wpi A, initial_wpi B))
                                 ((states_wpi A) × (states_wpi B))
                                 (inputs_wpi A ∪ inputs_wpi B)
                                 (outputs_wpi A ∪ outputs_wpi B)
                                 ts
                                 h'
                                 (h_obs_impl_from_h h'))"
                                       
lift_definition product :: "('a,'b,'c) fsm_with_precomputations ⇒ ('d,'b,'c) fsm_with_precomputations ⇒ ('a × 'd,'b,'c) fsm_with_precomputations" is product_impl 
proof -
  fix A :: "('a,'b,'c) fsm_with_precomputations_impl"
  fix B :: "('d,'b,'c) fsm_with_precomputations_impl"
  assume a1: "well_formed_fsm_with_precomputations A" and a2: "well_formed_fsm_with_precomputations B"

  let ?P = "product_impl A B"

  have "(⋃(image (λ tA . image (λ tB . (tA,tB)) (transitions_wpi B)) (transitions_wpi A))) = {(tA,tB) | tA tB . tA ∈ transitions_wpi A ∧ tB ∈ transitions_wpi B}"
    by auto
  then have "(Set.filter (λ((qA,x,y,qA'), (qB,x',y',qB')) . x = x' ∧ y = y') (⋃(image (λ tA . image (λ tB . (tA,tB)) (transitions_wpi B)) (transitions_wpi A)))) = {((qA,x,y,qA'),(qB,x,y,qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions_wpi A ∧ (qB,x,y,qB') ∈ transitions_wpi B}"
    by auto
  then have "image (λ((qA,x,y,qA'), (qB,x',y',qB')) . ((qA,qB),x,y,(qA',qB'))) (Set.filter (λ((qA,x,y,qA'), (qB,x',y',qB')) . x = x' ∧ y = y') (⋃(image (λ tA . image (λ tB . (tA,tB)) (transitions_wpi B)) (transitions_wpi A)))) 
              = image (λ((qA,x,y,qA'), (qB,x',y',qB')) . ((qA,qB),x,y,(qA',qB'))) {((qA,x,y,qA'),(qB,x,y,qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions_wpi A ∧ (qB,x,y,qB') ∈ transitions_wpi B}"
    by auto
  then have "transitions_wpi ?P = image (λ((qA,x,y,qA'), (qB,x',y',qB')) . ((qA,qB),x,y,(qA',qB'))) {((qA,x,y,qA'),(qB,x,y,qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions_wpi A ∧ (qB,x,y,qB') ∈ transitions_wpi B}"
    by auto
  also have "… =  {((qA,qB),x,y,(qA',qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions_wpi A ∧ (qB,x,y,qB') ∈ transitions_wpi B}"
    by force
  finally have "transitions_wpi ?P = {((qA,qB),x,y,(qA',qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions_wpi A ∧ (qB,x,y,qB') ∈ transitions_wpi B}" .
  
  have "h_wpi ?P = set_as_mapping_image (transitions_wpi ?P) (λ(q,x,y,q') . ((q,x),y,q'))"
   and "h_obs_wpi ?P = h_obs_impl_from_h (h_wpi ?P)"
    unfolding canonical_separator'_impl.simps Let_def by auto
  
  have "initial_wpi ?P ∈ states_wpi ?P" 
    using a1 a2 by auto
  moreover have "finite (states_wpi ?P)"
    using a1 a2 by auto
  moreover have "finite (inputs_wpi ?P)"
    using a1 a2 by auto
  moreover have "finite (outputs_wpi ?P)"
    using a1 a2 by auto
  moreover have "finite (transitions_wpi ?P)"
    using a1 a2 unfolding product_code_naive by auto
  moreover have "(∀t∈transitions_wpi ?P.
            t_source t ∈ states_wpi ?P ∧
            t_input t ∈ inputs_wpi ?P ∧ t_target t ∈ states_wpi ?P ∧
                                             t_output t ∈ outputs_wpi ?P)"
    using a1 a2 unfolding well_formed_fsm_with_precomputations.simps
    unfolding ‹transitions_wpi ?P = {((qA,qB),x,y,(qA',qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions_wpi A ∧ (qB,x,y,qB') ∈ transitions_wpi B}› 
    by fastforce
  ultimately show "well_formed_fsm_with_precomputations ?P"
    using well_formed_h_set_as_mapping[OF ‹h_wpi ?P = set_as_mapping_image (transitions_wpi ?P) (λ(q,x,y,q') . ((q,x),y,q'))›] 
          well_formed_h_obs_impl_from_h[OF ‹h_obs_wpi ?P = h_obs_impl_from_h (h_wpi ?P)›]
    unfolding well_formed_fsm_with_precomputations.simps by blast
qed

lemma product_simps:
  "initial_wp (product A B) = (initial_wp A, initial_wp B)"  
  "states_wp (product A B) = (states_wp A) × (states_wp B)"
  "inputs_wp (product A B) = inputs_wp A ∪ inputs_wp B"
  "outputs_wp (product A B) = outputs_wp A ∪ outputs_wp B"  
  "transitions_wp (product A B) = (image (λ((qA,x,y,qA'), (qB,x',y',qB')) . ((qA,qB),x,y,(qA',qB'))) (Set.filter (λ((qA,x,y,qA'), (qB,x',y',qB')) . x = x' ∧ y = y') (⋃(image (λ tA . image (λ tB . (tA,tB)) (transitions_wp B)) (transitions_wp A)))))"
  by (transfer; simp)+

declare [[code drop: FSM_Impl.product]]
lemma product_with_precomputations_code [code] : "FSM_Impl.product ((FSMWP A)) ((FSMWP B)) = FSMWP (product A B)"
  unfolding FSM_Impl.product_code_naive 
  unfolding fsm_impl_FSMWP_initial fsm_impl_FSMWP_states fsm_impl_FSMWP_inputs fsm_impl_FSMWP_outputs fsm_impl_FSMWP_transitions
  unfolding FSMWP_def
  unfolding product_simps  
  by presburger 


fun from_FSMI_impl :: "('a,'b,'c) fsm_with_precomputations_impl ⇒ 'a ⇒ ('a,'b,'c) fsm_with_precomputations_impl" where
  "from_FSMI_impl M q = (if q ∈ states_wpi M then FSMWPI q (states_wpi M) (inputs_wpi M) (outputs_wpi M) (transitions_wpi M) (h_wpi M) (h_obs_wpi M) else M)"

lift_definition from_FSMI :: "('a,'b,'c) fsm_with_precomputations ⇒ 'a ⇒ ('a,'b,'c) fsm_with_precomputations" is from_FSMI_impl  
proof -
  fix M :: "('a,'b,'c) fsm_with_precomputations_impl"
  fix q
  assume "well_formed_fsm_with_precomputations M"
  then show "well_formed_fsm_with_precomputations (from_FSMI_impl M q)"
    by (cases "q ∈ states_wpi M"; auto)
qed

lemma from_FSMI_simps:
  "initial_wp (from_FSMI M q) = (if q ∈ states_wp M then q else initial_wp M)"
  "states_wp (from_FSMI M q) = states_wp M"
  "inputs_wp (from_FSMI M q) = inputs_wp M"
  "outputs_wp (from_FSMI M q) = outputs_wp M"
  "transitions_wp (from_FSMI M q) = transitions_wp M"
  by (transfer; simp add: Let_def)+

declare [[code drop: FSM_Impl.from_FSMI]]
lemma from_FSMI_with_precomputations_code [code] : "FSM_Impl.from_FSMI ((FSMWP M)) q = FSMWP (from_FSMI M q)"
  unfolding FSM_Impl.from_FSMI.simps 
  unfolding fsm_impl_FSMWP_initial fsm_impl_FSMWP_states fsm_impl_FSMWP_inputs fsm_impl_FSMWP_outputs fsm_impl_FSMWP_transitions
  unfolding FSMWP_def
  unfolding from_FSMI_simps  
  by presburger 

end