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