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"}.›