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]
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
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')"
then have **: "(⋀x. Mapping.lookup x = set_as_map (RBT_set t) ⟹ x = (?C1 (RBT_set t)))"

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
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')"
then have **: "(⋀x. Mapping.lookup x = set_as_map (DList_set xs) ⟹ x = (?C2 (DList_set xs)))"

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
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]
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
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')"
then have **: "(⋀x. Mapping.lookup x = set_as_map (image f1 (RBT_set t)) ⟹ x = (?C1 (RBT_set t)))"

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
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')"
then have **: "(⋀x. Mapping.lookup x = set_as_map (image f2 (DList_set xs)) ⟹ x = (?C2 (DList_set xs)))"
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)))"

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
```