Theory Observability
section ‹Observability›
text ‹This theory presents the classical algorithm for transforming FSMs into
language-equivalent observable FSMs in analogy to the determinisation of nondeterministic
finite automata.›
theory Observability
imports FSM
begin
lemma fPow_Pow : "Pow (fset A) = fset (fset |`| fPow A)"
proof (induction A)
case empty
then show ?case by auto
next
case (insert x A)
have "Pow (fset (finsert x A)) = Pow (fset A) ∪ (insert x) ` Pow (fset A)"
by (simp add: Pow_insert)
moreover have "fset (fset |`| fPow (finsert x A)) = fset (fset |`| fPow A) ∪ (insert x) ` fset (fset |`| fPow A)"
proof -
have "fset |`| ((fPow A) |∪| (finsert x) |`| (fPow A)) = (fset |`| fPow A) |∪| (insert x) |`| (fset |`| fPow A)"
unfolding fimage_funion
by fastforce
moreover have "(fPow (finsert x A)) = (fPow A) |∪| (finsert x) |`| (fPow A)"
by (simp add: fPow_finsert)
ultimately show ?thesis
by auto
qed
ultimately show ?case
using insert.IH by simp
qed
lemma fcard_fsubset: "¬ fcard (A |-| (B |∪| C)) < fcard (A |-| B) ⟹ C |⊆| A ⟹ C |⊆| B"
proof (induction C)
case empty
then show ?case by auto
next
case (insert x C)
then show ?case
unfolding finsert_fsubset funion_finsert_right not_less
proof -
assume a1: "fcard (A |-| B) ≤ fcard (A |-| finsert x (B |∪| C))"
assume "⟦fcard (A |-| B) ≤ fcard (A |-| (B |∪| C)); C |⊆| A⟧ ⟹ C |⊆| B"
assume a2: "x |∈| A ∧ C |⊆| A"
have "A |-| (C |∪| finsert x B) = A |-| B ∨ ¬ A |-| (C |∪| finsert x B) |⊆| A |-| B"
using a1 by (metis (no_types) fcard_seteq funion_commute funion_finsert_right)
then show "x |∈| B ∧ C |⊆| B"
using a2 by blast
qed
qed
lemma make_observable_transitions_qtrans_helper:
assumes "qtrans = ffUnion (fimage (λ q . (let qts = ffilter (λt . t_source t |∈| q) A;
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . (q,x,y, t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) qts)))) ios)) nexts)"
shows "⋀ t . t |∈| qtrans ⟷ t_source t |∈| nexts ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' . t' |∈| A ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
proof -
have "fset qtrans = { (q,x,y,q') | q x y q' . q |∈| nexts ∧ q' ≠ {||} ∧ fset q' = t_target ` {t' . t' |∈| A ∧ t_source t' |∈| q ∧ t_input t' = x ∧ t_output t' = y}}"
proof -
have "⋀ q . fset (ffilter (λt . t_source t |∈| q) A) = Set.filter (λt . t_source t |∈| q) (fset A)"
using ffilter.rep_eq assms(1) by auto
then have "⋀ q . fset (fimage (λ t . (t_input t, t_output t)) (ffilter (λt . t_source t |∈| q) A)) = image (λ t . (t_input t, t_output t)) (Set.filter (λt . t_source t |∈| q) (fset A))"
by simp
then have *:"⋀ q . fset (fimage (λ(x,y) . (q,x,y, (t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) (ffilter (λt . t_source t |∈| q) (A))))))) (fimage (λ t . (t_input t, t_output t)) (ffilter (λt . t_source t |∈| q) (A))))
= image (λ(x,y) . (q,x,y, (t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) (ffilter (λt . t_source t |∈| q) (A))))))) (image (λ t . (t_input t, t_output t)) (Set.filter (λt . t_source t |∈| q) (fset A)))"
by (metis (no_types, lifting) ffilter.rep_eq fset.set_map)
have **: "⋀ f1 f2 xs ys ys' . (⋀ x . fset (f1 x ys) = (f2 x ys')) ⟹
fset (ffUnion (fimage (λ x . (f1 x ys)) xs)) = (⋃ x ∈ fset xs . (f2 x ys'))"
unfolding ffUnion.rep_eq fimage.rep_eq by force
have "fset (ffUnion (fimage (λ q . (fimage (λ(x,y) . (q,x,y, (t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) (ffilter (λt . t_source t |∈| q) (A))))))) (fimage (λ t . (t_input t, t_output t)) (ffilter (λt . t_source t |∈| q) (A))))) nexts))
= (⋃ q ∈ fset nexts . image (λ(x,y) . (q,x,y, (t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) (ffilter (λt . t_source t |∈| q) (A))))))) (image (λ t . (t_input t, t_output t)) (Set.filter (λt . t_source t |∈| q) (fset A))))"
unfolding ffUnion.rep_eq fimage.rep_eq
using "*" by force
also have "… = { (q,x,y,q') | q x y q' . q |∈| nexts ∧ q' ≠ {||} ∧ fset q' = t_target ` {t' . t' |∈| A ∧ t_source t' |∈| q ∧ t_input t' = x ∧ t_output t' = y}}"
(is "?A = ?B") proof -
have "⋀ t . t ∈ ?A ⟹ t ∈ ?B"
proof -
fix t assume "t ∈ ?A"
then obtain q where "q ∈ fset nexts"
and "t ∈ image (λ(x,y) . (q,x,y, (t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) (ffilter (λt . t_source t |∈| q) (A))))))) (image (λ t . (t_input t, t_output t)) (Set.filter (λt . t_source t |∈| q) (fset A)))"
by blast
then obtain x y q' where *: "(x,y) ∈ (image (λ t . (t_input t, t_output t)) (Set.filter (λt . t_source t |∈| q) (fset A)))"
and "t = (q,x,y,q')"
and **:"q' = (t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) (ffilter (λt . t_source t |∈| q) (A)))))"
by force
have "q |∈| nexts"
using ‹q ∈ fset nexts›
by simp
moreover have "q' ≠ {||}"
proof -
have ***:"(Set.filter (λt . t_source t |∈| q) (fset A)) = fset (ffilter (λt . t_source t |∈| q) (A))"
by auto
have "∃ t . t |∈| (ffilter (λt. t_source t |∈| q) A) ∧ (t_input t, t_output t) = (x,y)"
using *
by (metis (no_types, lifting) "***" image_iff)
then show ?thesis unfolding **
by force
qed
moreover have "fset q' = t_target ` {t' . t' |∈| A ∧ t_source t' |∈| q ∧ t_input t' = x ∧ t_output t' = y}"
proof -
have "{t' . t' |∈| A ∧ t_source t' |∈| q ∧ t_input t' = x ∧ t_output t' = y} = ((Set.filter (λt . (t_input t, t_output t) = (x,y)) (fset (ffilter (λt . t_source t |∈| q) (A)))))"
by fastforce
also have "… = fset ((ffilter (λt . (t_input t, t_output t) = (x,y)) (ffilter (λt . t_source t |∈| q) (A))))"
by fastforce
finally have "{t' . t' |∈| A ∧ t_source t' |∈| q ∧ t_input t' = x ∧ t_output t' = y} = fset ((ffilter (λt . (t_input t, t_output t) = (x,y)) (ffilter (λt . t_source t |∈| q) (A))))" .
then show ?thesis
unfolding **
by simp
qed
ultimately show "t ∈ ?B"
unfolding ‹t = (q,x,y,q')›
by blast
qed
moreover have "⋀ t . t ∈ ?B ⟹ t ∈ ?A"
proof -
fix t assume "t ∈ ?B"
then obtain q x y q' where "t = (q,x,y,q')" and "(q,x,y,q') ∈ ?B" by force
then have "q |∈| nexts"
and "q' ≠ {||}"
and *: "fset q' = t_target ` {t' . t' |∈| A ∧ t_source t' |∈| q ∧ t_input t' = x ∧ t_output t' = y}"
by force+
then have "fset q' ≠ {}"
by (metis bot_fset.rep_eq fset_inject)
have "(x,y) ∈ (image (λ t . (t_input t, t_output t)) (Set.filter (λt . t_source t |∈| q) (fset A)))"
using ‹fset q' ≠ {}› unfolding * Set.filter_def by blast
moreover have "q' = t_target |`| ffilter (λt. (t_input t, t_output t) = (x, y)) (ffilter (λt. t_source t |∈| q) A)"
proof -
have "{t' . t' |∈| A ∧ t_source t' |∈| q ∧ t_input t' = x ∧ t_output t' = y} = ((Set.filter (λt . (t_input t, t_output t) = (x,y)) (fset (ffilter (λt . t_source t |∈| q) (A)))))"
by fastforce
also have "… = fset ((ffilter (λt . (t_input t, t_output t) = (x,y)) (ffilter (λt . t_source t |∈| q) (A))))"
by fastforce
finally have ***:"{t' . t' |∈| A ∧ t_source t' |∈| q ∧ t_input t' = x ∧ t_output t' = y} = fset ((ffilter (λt . (t_input t, t_output t) = (x,y)) (ffilter (λt . t_source t |∈| q) (A))))" .
show ?thesis
using *
unfolding ***
by (metis (no_types, lifting) fimage.rep_eq fset_inject)
qed
ultimately show "t ∈ ?A"
using ‹q |∈| nexts›
unfolding ‹t = (q,x,y,q')›
by force
qed
ultimately show ?thesis
by (metis (no_types, lifting) Collect_cong Sup_set_def mem_Collect_eq)
qed
finally show ?thesis
unfolding assms Let_def by blast
qed
then show "⋀ t . t |∈| qtrans ⟷ t_source t |∈| nexts ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' . t' |∈| A ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
by force
qed
function make_observable_transitions :: "('a,'b,'c) transition fset ⇒ 'a fset fset ⇒ 'a fset fset ⇒ ('a fset × 'b × 'c × 'a fset) fset ⇒ ('a fset × 'b × 'c × 'a fset) fset" where
"make_observable_transitions base_trans nexts dones ts = (let
qtrans = ffUnion (fimage (λ q . (let qts = ffilter (λt . t_source t |∈| q) base_trans;
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . (q,x,y, t_target |`| (ffilter (λt . (t_input t, t_output t) = (x,y)) qts))) ios)) nexts);
dones' = dones |∪| nexts;
ts' = ts |∪| qtrans;
nexts' = (fimage t_target qtrans) |-| dones'
in if nexts' = {||}
then ts'
else make_observable_transitions base_trans nexts' dones' ts')"
by auto
termination
proof -
{
fix base_trans :: "('a,'b,'c) transition fset"
fix nexts :: "'a fset fset"
fix dones :: "'a fset fset"
fix ts :: "('a fset × 'b × 'c × 'a fset) fset"
fix q x y q'
assume assm1: "¬ fcard
(fPow (t_source |`| base_trans |∪| t_target |`| base_trans) |-|
(dones |∪| nexts |∪|
t_target |`|
ffUnion
((λq. let qts = ffilter (λt. t_source t |∈| q) base_trans
in ((λ(x, y). (q, x, y, t_target |`| ffilter (λt. t_input t = x ∧ t_output t = y) qts)) ∘ (λt. (t_input t, t_output t))) |`|
qts) |`|
nexts)))
< fcard (fPow (t_source |`| base_trans |∪| t_target |`| base_trans) |-| (dones |∪| nexts))"
and assm2: "(q, x, y, q') |∈|
ffUnion
((λq. let qts = ffilter (λt. t_source t |∈| q) base_trans
in ((λ(x, y). (q, x, y, t_target |`| ffilter (λt. t_input t = x ∧ t_output t = y) qts)) ∘ (λt. (t_input t, t_output t))) |`| qts) |`|
nexts)"
and assm3: "q' |∉| nexts"
define qtrans where qtrans_def: "qtrans = ffUnion (fimage (λ q . (let qts = ffilter (λt . t_source t |∈| q) base_trans;
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . (q,x,y, t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) qts)))) ios)) nexts)"
have qtrans_prop: "⋀ t . t |∈| qtrans ⟷ t_source t |∈| nexts ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' | t' . t' |∈| base_trans ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
using make_observable_transitions_qtrans_helper[OF qtrans_def]
by presburger
have "⋀ t . t |∈| qtrans ⟹ t_target t |∈| fPow (t_target |`| base_trans)"
proof -
fix t assume "t |∈| qtrans"
then have *: "fset (t_target t) = t_target ` {t' . t' |∈| base_trans ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
using qtrans_prop by blast
then have "fset (t_target t) ⊆ t_target ` (fset base_trans)"
by (metis (mono_tags, lifting) imageI image_Collect_subsetI)
then show "t_target t |∈| fPow (t_target |`| base_trans)"
by (simp add: less_eq_fset.rep_eq)
qed
then have "t_target |`| qtrans |⊆| (fPow (t_source |`| base_trans |∪| t_target |`| base_trans))"
by fastforce
moreover have " ¬ fcard (fPow (t_source |`| base_trans |∪| t_target |`| base_trans) |-| (dones |∪| nexts |∪| t_target |`| qtrans))
< fcard (fPow (t_source |`| base_trans |∪| t_target |`| base_trans) |-| (dones |∪| nexts))"
using assm1 unfolding qtrans_def by force
ultimately have "t_target |`| qtrans |⊆| dones |∪| nexts"
using fcard_fsubset by fastforce
moreover have "q' |∈| t_target |`| qtrans"
using assm2 unfolding qtrans_def by force
ultimately have "q' |∈| dones"
using ‹q' |∉| nexts› by blast
} note t = this
show ?thesis
apply (relation "measure (λ (base_trans, nexts, dones, ts) . fcard ((fPow (t_source |`| base_trans |∪| t_target |`| base_trans)) |-| (dones |∪| nexts)))")
apply auto
by (erule t)
qed
lemma make_observable_transitions_mono: "ts |⊆| (make_observable_transitions base_trans nexts dones ts)"
proof (induction rule: make_observable_transitions.induct[of "λ base_trans nexts dones ts . ts |⊆| (make_observable_transitions base_trans nexts dones ts)"])
case (1 base_trans nexts dones ts)
define qtrans where qtrans_def: "qtrans = ffUnion (fimage (λ q . (let qts = ffilter (λt . t_source t |∈| q) base_trans;
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . (q,x,y, t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) qts)))) ios)) nexts)"
have qtrans_prop: "⋀ t . t |∈| qtrans ⟷ t_source t |∈| nexts ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' | t' . t' |∈| base_trans ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
using make_observable_transitions_qtrans_helper[OF qtrans_def]
by presburger
let ?dones' = "dones |∪| nexts"
let ?ts' = "ts |∪| qtrans"
let ?nexts' = "(fimage t_target qtrans) |-| ?dones'"
have res_cases: "make_observable_transitions base_trans nexts dones ts = (if ?nexts' = {||}
then ?ts'
else make_observable_transitions base_trans ?nexts' ?dones' ?ts')"
unfolding make_observable_transitions.simps[of base_trans nexts dones ts] qtrans_def Let_def by simp
show ?case proof (cases "?nexts' = {||}")
case True
then show ?thesis using res_cases by simp
next
case False
then have "make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans ?nexts' ?dones' ?ts'"
using res_cases by simp
moreover have "ts |∪| qtrans |⊆| make_observable_transitions base_trans ?nexts' ?dones' ?ts'"
using "1"[OF qtrans_def _ _ _ False, of ?dones' ?ts'] by blast
ultimately show ?thesis
by blast
qed
qed
inductive pathlike :: "('state, 'input, 'output) transition fset ⇒ 'state ⇒ ('state, 'input, 'output) path ⇒ bool"
where
nil[intro!] : "pathlike ts q []" |
cons[intro!] : "t |∈| ts ⟹ pathlike ts (t_target t) p ⟹ pathlike ts (t_source t) (t#p)"
inductive_cases pathlike_nil_elim[elim!]: "pathlike ts q []"
inductive_cases pathlike_cons_elim[elim!]: "pathlike ts q (t#p)"
lemma make_observable_transitions_t_source :
assumes "⋀ t . t |∈| ts ⟹ t_source t |∈| dones ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' . t' |∈| base_trans ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
and "⋀ q t' . q |∈| dones ⟹ t' |∈| base_trans ⟹ t_source t' |∈| q ⟹ ∃ t . t |∈| ts ∧ t_source t = q ∧ t_input t = t_input t' ∧ t_output t = t_output t'"
and "t |∈| make_observable_transitions base_trans ((fimage t_target ts) |-| dones) dones ts"
and "t_source t |∈| dones"
shows "t |∈| ts"
using assms proof (induction base_trans "(fimage t_target ts) |-| dones" dones ts rule: make_observable_transitions.induct)
case (1 base_trans dones ts)
let ?nexts = "(fimage t_target ts) |-| dones"
define qtrans where qtrans_def: "qtrans = ffUnion (fimage (λ q . (let qts = ffilter (λt . t_source t |∈| q) base_trans;
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . (q,x,y, t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) qts)))) ios)) ?nexts)"
have qtrans_prop: "⋀ t . t |∈| qtrans ⟷ t_source t |∈| ?nexts ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' . t' |∈| base_trans ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
using make_observable_transitions_qtrans_helper[OF qtrans_def]
by presburger
let ?dones' = "dones |∪| ?nexts"
let ?ts' = "ts |∪| qtrans"
let ?nexts' = "(fimage t_target qtrans) |-| ?dones'"
have res_cases: "make_observable_transitions base_trans ?nexts dones ts = (if ?nexts' = {||}
then ?ts'
else make_observable_transitions base_trans ?nexts' ?dones' ?ts')"
unfolding make_observable_transitions.simps[of base_trans ?nexts dones ts] qtrans_def Let_def by simp
show ?case proof (cases "?nexts' = {||}")
case True
then have "make_observable_transitions base_trans ?nexts dones ts = ?ts'"
using res_cases by auto
then have "t |∈| ts |∪| qtrans"
using ‹t |∈| make_observable_transitions base_trans ?nexts dones ts› ‹t_source t |∈| dones› by blast
then show ?thesis
using qtrans_prop "1.prems"(3,4) by blast
next
case False
then have "make_observable_transitions base_trans ?nexts dones ts = make_observable_transitions base_trans ?nexts' ?dones' ?ts'"
using res_cases by simp
have i1: "(⋀t. t |∈| ts |∪| qtrans ⟹
t_source t |∈| dones |∪| ?nexts ∧
t_target t ≠ {||} ∧
fset (t_target t) =
t_target `
{t' . t' |∈| base_trans ∧
t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t})"
using "1.prems"(1) qtrans_prop by blast
have i3: "t_target |`| qtrans |-| (dones |∪| ?nexts) = t_target |`| (ts |∪| qtrans) |-| (dones |∪| ?nexts)"
unfolding "1.prems"(3) by blast
have i2: "(⋀q t'.
q |∈| dones |∪| ?nexts ⟹
t' |∈| base_trans ⟹
t_source t' |∈| q ⟹
∃t. t |∈| ts |∪| qtrans ∧ t_source t = q ∧ t_input t = t_input t' ∧ t_output t = t_output t')"
proof -
fix q t' assume "q |∈| dones |∪| ?nexts"
and *:"t' |∈| base_trans"
and **:"t_source t' |∈| q"
then consider (a) "q |∈| dones" | (b) "q |∈| ?nexts" by blast
then show "∃t. t |∈| ts |∪| qtrans ∧ t_source t = q ∧ t_input t = t_input t' ∧ t_output t = t_output t'"
proof cases
case a
then show ?thesis using * **
using "1.prems"(2) by blast
next
case b
let ?tgts = "{t'' . t'' |∈| base_trans ∧ t_source t'' |∈| q ∧ t_input t'' = t_input t' ∧ t_output t'' = t_output t'}"
define tgts where tgts: "tgts = Abs_fset (t_target ` ?tgts)"
have "?tgts ⊆ fset base_trans"
by fastforce
then have "finite (t_target ` ?tgts)"
by (meson finite_fset finite_imageI finite_subset)
then have "fset tgts = (t_target ` ?tgts)"
unfolding tgts
using Abs_fset_inverse
by blast
have "?tgts ≠ {}"
using * ** by blast
then have "t_target ` ?tgts ≠ {}"
by blast
then have "tgts ≠ {||}"
using ‹fset tgts = (t_target ` ?tgts)›
by force
then have "(q, t_input t', t_output t', tgts) |∈| qtrans"
using b
unfolding qtrans_prop[of "(q,t_input t',t_output t',tgts)"]
unfolding fst_conv snd_conv
unfolding ‹fset tgts = (t_target ` ?tgts)›[symmetric]
by blast
then show ?thesis
by auto
qed
qed
have "t |∈| make_observable_transitions base_trans ?nexts dones ts ⟹ t_source t |∈| dones |∪| ?nexts ⟹ t |∈| ts |∪| qtrans"
unfolding ‹make_observable_transitions base_trans ?nexts dones ts = make_observable_transitions base_trans ?nexts' ?dones' ?ts'›
using "1.hyps"[OF qtrans_def _ _ _ _ i1 i2] False i3 by force
then have "t |∈| ts |∪| qtrans"
using ‹t |∈| make_observable_transitions base_trans ?nexts dones ts› ‹t_source t |∈| dones› by blast
then show ?thesis
using qtrans_prop "1.prems"(3,4) by blast
qed
qed
lemma make_observable_transitions_path :
assumes "⋀ t . t |∈| ts ⟹ t_source t |∈| dones ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' ∈ transitions M . t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
and "⋀ q t' . q |∈| dones ⟹ t' ∈ transitions M ⟹ t_source t' |∈| q ⟹ ∃ t . t |∈| ts ∧ t_source t = q ∧ t_input t = t_input t' ∧ t_output t = t_output t'"
and "⋀ q . q |∈| (fimage t_target ts) |-| dones ⟹ q |∈| fPow (t_source |`| ftransitions M |∪| t_target |`| ftransitions M)"
and "⋀ q . q |∈| dones ⟹ q |∈| fPow (t_source |`| ftransitions M |∪| t_target |`| ftransitions M |∪| {|initial M|})"
and "{||} |∉| dones"
and "q |∈| dones"
shows "(∃ q' p . q' |∈| q ∧ path M q' p ∧ p_io p = io) ⟷ (∃ p'. pathlike (make_observable_transitions (ftransitions M) ((fimage t_target ts) |-| dones) dones ts) q p' ∧ p_io p' = io)"
using assms proof (induction "ftransitions M" "(fimage t_target ts) |-| dones" dones ts arbitrary: q io rule: make_observable_transitions.induct)
case (1 dones ts q)
let ?obs = "(make_observable_transitions (ftransitions M) ((fimage t_target ts) |-| dones) dones ts)"
let ?nexts = "(fimage t_target ts) |-| dones"
show ?case proof (cases io)
case Nil
have scheme: "⋀ q q' X . q' |∈| q ⟹ q |∈| fPow X ⟹ q' |∈| X"
by (simp add: fsubsetD)
obtain q' where "q' |∈| q"
using ‹{||} |∉| dones› ‹q |∈| dones›
by (metis all_not_in_conv bot_fset.rep_eq fset_cong)
have "q' |∈| t_source |`| ftransitions M |∪| t_target |`| ftransitions M |∪| {|FSM.initial M|}"
using scheme[OF ‹q' |∈| q› "1.prems"(4)[OF ‹q |∈| dones›]] .
then have "q' ∈ states M"
using ftransitions_source[of q' M]
using ftransitions_target[of q' M]
by force
then have "∃ q' p . q' |∈| q ∧ path M q' p ∧ p_io p = io"
using ‹q' |∈| q› Nil by auto
moreover have "(∃ p'. pathlike ?obs q p' ∧ p_io p' = io)"
using Nil by auto
ultimately show ?thesis
by simp
next
case (Cons ioT ioP)
define qtrans where qtrans_def: "qtrans = ffUnion (fimage (λ q . (let qts = ffilter (λt . t_source t |∈| q) (ftransitions M);
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . (q,x,y, t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) qts)))) ios)) ?nexts)"
have qtrans_prop: "⋀ t . t |∈| qtrans ⟷ t_source t |∈| ?nexts ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' . t' |∈| (ftransitions M) ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
using make_observable_transitions_qtrans_helper[OF qtrans_def]
by presburger
let ?dones' = "dones |∪| ?nexts"
let ?ts' = "ts |∪| qtrans"
let ?nexts' = "(fimage t_target qtrans) |-| ?dones'"
have res_cases: "make_observable_transitions (ftransitions M) ?nexts dones ts = (if ?nexts' = {||}
then ?ts'
else make_observable_transitions (ftransitions M) ?nexts' ?dones' ?ts')"
unfolding make_observable_transitions.simps[of "ftransitions M" ?nexts dones ts] qtrans_def Let_def by simp
have i1: "(⋀t. t |∈| ts |∪| qtrans ⟹
t_source t |∈| dones |∪| ?nexts ∧
t_target t ≠ {||} ∧
fset (t_target t) =
t_target `
{t' ∈ FSM.transitions M .
t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t})"
using "1.prems"(1) qtrans_prop
using ftransitions_set[of M]
by (metis (mono_tags, lifting) Collect_cong funion_iff)
have i2: "(⋀q t'.
q |∈| dones |∪| ?nexts ⟹
t' ∈ FSM.transitions M ⟹
t_source t' |∈| q ⟹
∃t. t |∈| ts |∪| qtrans ∧ t_source t = q ∧ t_input t = t_input t' ∧ t_output t = t_output t')"
proof -
fix q t' assume "q |∈| dones |∪| ?nexts"
and *:"t' ∈ FSM.transitions M"
and **:"t_source t' |∈| q"
then consider (a) "q |∈| dones" | (b) "q |∈| ?nexts" by blast
then show "∃t. t |∈| ts |∪| qtrans ∧ t_source t = q ∧ t_input t = t_input t' ∧ t_output t = t_output t'"
proof cases
case a
then show ?thesis using "1.prems"(2) * ** by blast
next
case b
let ?tgts = "{t'' ∈ FSM.transitions M. t_source t'' |∈| q ∧ t_input t'' = t_input t' ∧ t_output t'' = t_output t'}"
have "?tgts ≠ {}"
using * ** by blast
let ?tgts = "{t'' . t'' |∈| ftransitions M ∧ t_source t'' |∈| q ∧ t_input t'' = t_input t' ∧ t_output t'' = t_output t'}"
define tgts where tgts: "tgts = Abs_fset (t_target ` ?tgts)"
have "?tgts ⊆ transitions M"
using ftransitions_set[of M]
by (metis (no_types, lifting) mem_Collect_eq subsetI)
then have "finite (t_target ` ?tgts)"
by (meson finite_imageI finite_subset fsm_transitions_finite)
then have "fset tgts = (t_target ` ?tgts)"
unfolding tgts
using Abs_fset_inverse
by blast
have "?tgts ≠ {}"
using * **
by (metis (mono_tags, lifting) empty_iff ftransitions_set mem_Collect_eq)
then have "t_target ` ?tgts ≠ {}"
by blast
then have "tgts ≠ {||}"
using ‹fset tgts = (t_target ` ?tgts)›
by force
then have "(q, t_input t', t_output t', tgts) |∈| qtrans"
using b
unfolding qtrans_prop[of "(q,t_input t',t_output t',tgts)"]
unfolding fst_conv snd_conv
unfolding ‹fset tgts = (t_target ` ?tgts)›[symmetric]
by blast
then show ?thesis
by auto
qed
qed
have i3: "t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones)) = t_target |`| qtrans |-| (dones |∪| (t_target |`| ts |-| dones))"
by blast
have i4: "(⋀q. q |∈| t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones)) ⟹
q |∈| fPow (t_source |`| ftransitions M |∪| t_target |`| ftransitions M))"
proof -
fix q assume "q |∈| t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones))"
then have "q |∈| t_target |`| qtrans"
by auto
then obtain t where "t |∈| qtrans" and "t_target t = q"
by auto
then have "fset q = t_target ` {t'. t' |∈| ftransitions M ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
unfolding qtrans_prop by auto
then have "fset q ⊆ t_target ` transitions M"
by (metis (no_types, lifting) ftransitions_set image_Collect_subsetI image_eqI)
then show "q |∈| fPow (t_source |`| ftransitions M |∪| t_target |`| ftransitions M)"
by (metis (no_types, lifting) fPowI fset.set_map fset_inject ftransitions_set le_supI2 sup.orderE sup.orderI sup_fset.rep_eq)
qed
have i5: "(⋀q. q |∈| dones |∪| ?nexts ⟹ q |∈| fPow (t_source |`| ftransitions M |∪| t_target |`| ftransitions M |∪| {|initial M|}))"
using "1.prems"(4,3) qtrans_prop
by auto
have i7: "{||} |∉| dones |∪| ?nexts"
using "1.prems" by fastforce
show ?thesis
proof (cases "?nexts' ≠ {||}")
case False
then have "?obs = ?ts'"
using res_cases by auto
have "⋀ q io . q |∈| ?dones' ⟹ q ≠ {||} ⟹ (∃q' p. q' |∈| q ∧ path M q' p ∧ p_io p = io) ⟷ (∃p'. pathlike ?obs q p' ∧ p_io p' = io)"
proof -
fix q io assume "q |∈| ?dones'" and "q ≠ {||}"
then show "(∃q' p. q' |∈| q ∧ path M q' p ∧ p_io p = io) ⟷ (∃p'. pathlike ?obs q p' ∧ p_io p' = io)"
proof (induction io arbitrary: q)
case Nil
have scheme: "⋀ q q' X . q' |∈| q ⟹ q |∈| fPow X ⟹ q' |∈| X"
by (simp add: fsubsetD)
obtain q' where "q' |∈| q"
using ‹q ≠ {||}› by fastforce
have "q' |∈| t_source |`| ftransitions M |∪| t_target |`| ftransitions M |∪| {|FSM.initial M|}"
using scheme[OF ‹q' |∈| q› i5[OF ‹q |∈| ?dones'›]] .
then have "q' ∈ states M"
using ftransitions_source[of q' M]
using ftransitions_target[of q' M]
by force
then have "∃ q' p . q' |∈| q ∧ path M q' p ∧ p_io p = []"
using ‹q' |∈| q› by auto
moreover have "(∃ p'. pathlike ?obs q p' ∧ p_io p' = [])"
by auto
ultimately show ?case
by simp
next
case (Cons ioT ioP)
have "(∃q' p. q' |∈| q ∧ path M q' p ∧ p_io p = ioT # ioP) ⟹ (∃p'. pathlike ?obs q p' ∧ p_io p' = ioT # ioP)"
proof -
assume "∃q' p. q' |∈| q ∧ path M q' p ∧ p_io p = ioT # ioP"
then obtain q' p where "q' |∈| q" and "path M q' p" and "p_io p = ioT # ioP"
by meson
then obtain tM pM where "p = tM # pM"
by auto
then have "tM ∈ transitions M" and "t_source tM |∈| q"
using ‹path M q' p› ‹q' |∈| q› by blast+
then obtain tP where "tP |∈| ts |∪| qtrans"
and "t_source tP = q"
and "t_input tP = t_input tM"
and "t_output tP = t_output tM"
using Cons.prems i2 by blast
have "path M (t_target tM) pM" and "p_io pM = ioP"
using ‹path M q' p› ‹p_io p = ioT # ioP› unfolding ‹p = tM # pM› by auto
moreover have "t_target tM |∈| t_target tP"
using i1[OF ‹tP |∈| ts |∪| qtrans›]
using ‹p = tM # pM› ‹path M q' p› ‹q' |∈| q›
unfolding ‹t_input tP = t_input tM› ‹t_output tP = t_output tM› ‹t_source tP = q›
by fastforce
ultimately have "∃q' p. q' |∈| t_target tP ∧ path M q' p ∧ p_io p = ioP"
using ‹p_io pM = ioP› ‹path M (t_target tM) pM› by blast
have "t_target tP |∈| dones |∪| (t_target |`| ts |-| dones)"
using False ‹tP |∈| ts |∪| qtrans› by blast
moreover have "t_target tP ≠ {||}"
using i1[OF ‹tP |∈| ts |∪| qtrans›] by blast
ultimately obtain pP where "pathlike ?obs (t_target tP) pP" and "p_io pP = ioP"
using Cons.IH ‹∃q' p. q' |∈| t_target tP ∧ path M q' p ∧ p_io p = ioP› by blast
then have "pathlike ?obs q (tP#pP)"
using ‹t_source tP = q› ‹tP |∈| ts |∪| qtrans› ‹?obs = ?ts'› by auto
moreover have "p_io (tP#pP) = ioT # ioP"
using ‹t_input tP = t_input tM› ‹t_output tP = t_output tM› ‹p_io p = ioT # ioP› ‹p = tM # pM› ‹p_io pP = ioP› by simp
ultimately show ?thesis
by auto
qed
moreover have "(∃p'. pathlike ?obs q p' ∧ p_io p' = ioT # ioP) ⟹ (∃q' p. q' |∈| q ∧ path M q' p ∧ p_io p = ioT # ioP)"
proof -
assume "∃p'. pathlike ?obs q p' ∧ p_io p' = ioT # ioP"
then obtain p' where "pathlike ?ts' q p'" and "p_io p' = ioT # ioP"
unfolding ‹?obs = ?ts'› by meson
then obtain tP pP where "p' = tP#pP"
by auto
then have "t_source tP = q" and "tP |∈| ?ts'"
using ‹pathlike ?ts' q p'› by auto
have "pathlike ?ts' (t_target tP) pP" and "p_io pP = ioP"
using ‹pathlike ?ts' q p'› ‹p_io p' = ioT # ioP› ‹p' = tP#pP› by auto
then have "∃p'. pathlike ?ts' (t_target tP) p' ∧ p_io p' = ioP"
by auto
moreover have "t_target tP |∈| dones |∪| (t_target |`| ts |-| dones)"
using False ‹tP |∈| ts |∪| qtrans› by blast
moreover have "t_target tP ≠ {||}"
using i1[OF ‹tP |∈| ts |∪| qtrans›] by blast
ultimately obtain q'' pM where "q'' |∈| t_target tP" and "path M q'' pM" and "p_io pM = ioP"
using Cons.IH unfolding ‹?obs = ?ts'› by blast
then obtain tM where "t_source tM |∈| q" and "tM ∈ transitions M" and "t_input tM = t_input tP" and "t_output tM = t_output tP" and "t_target tM = q''"
using i1[OF ‹tP |∈| ts |∪| qtrans›]
using ‹q'' |∈| t_target tP›
unfolding ‹t_source tP = q› by force
have "path M (t_source tM) (tM#pM)"
using ‹tM ∈ transitions M› ‹t_target tM = q''› ‹path M q'' pM› by auto
moreover have "p_io (tM#pM) = ioT # ioP"
using ‹p_io pM = ioP› ‹t_input tM = t_input tP› ‹t_output tM = t_output tP› ‹p_io p' = ioT # ioP› ‹p' = tP#pP› by auto
ultimately show ?thesis
using ‹t_source tM |∈| q› by meson
qed
ultimately show ?case
by meson
qed
qed
then show ?thesis
using ‹q |∈| dones› ‹{||} |∉| dones› by blast
next
case True
have "make_observable_transitions (ftransitions M) ?nexts' ?dones' ?ts' = make_observable_transitions (ftransitions M) ?nexts dones ts"
proof (cases "?nexts' = {||}")
case True
then have "?obs = ?ts'"
using qtrans_def by auto
moreover have "make_observable_transitions (ftransitions M) ?nexts' ?dones' ?ts' = ?ts'"
unfolding make_observable_transitions.simps[of "ftransitions M" ?nexts' ?dones' ?ts']
unfolding True Let_def by auto
ultimately show ?thesis
by blast
next
case False
then show ?thesis
unfolding make_observable_transitions.simps[of "ftransitions M" ?nexts dones ts] qtrans_def Let_def by auto
qed
then have IStep: "⋀ q io . q |∈| ?dones' ⟹
(∃q' p. q' |∈| q ∧ path M q' p ∧ p_io p = io) =
(∃p'. pathlike (make_observable_transitions (ftransitions M) ?nexts dones ts) q p' ∧ p_io p' = io)"
using "1.hyps"[OF qtrans_def _ _ _ _ i1 i2 i4 i5 i7] True
unfolding i3
by presburger
show ?thesis
unfolding ‹io = ioT # ioP›
proof
show "∃q' p. q' |∈| q ∧ path M q' p ∧ p_io p = ioT # ioP ⟹ ∃p'. pathlike ?obs q p' ∧ p_io p' = ioT # ioP"
proof -
assume "∃q' p. q' |∈| q ∧ path M q' p ∧ p_io p = ioT # ioP"
then obtain q' p where "q' |∈| q" and "path M q' p" and "p_io p = ioT # ioP"
by meson
then obtain tM pM where "p = tM # pM"
by auto
then have "tM ∈ transitions M" and "t_source tM |∈| q"
using ‹path M q' p› ‹q' |∈| q› by blast+
then obtain tP where "tP |∈| ts"
and "t_source tP = q"
and "t_input tP = t_input tM"
and "t_output tP = t_output tM"
using "1.prems"(2,6) by blast
then have i9: "t_target tP |∈| dones |∪| ?nexts"
by simp
have "path M (t_target tM) pM" and "p_io pM = ioP"
using ‹path M q' p› ‹p_io p = ioT # ioP› unfolding ‹p = tM # pM› by auto
moreover have "t_target tM |∈| t_target tP"
using "1.prems"(1)[OF ‹tP |∈| ts›] ‹p = tM # pM› ‹path M q' p› ‹q' |∈| q›
unfolding ‹t_input tP = t_input tM› ‹t_output tP = t_output tM› ‹t_source tP = q›
by fastforce
ultimately have "∃q' p. q' |∈| t_target tP ∧ path M q' p ∧ p_io p = ioP"
using ‹p_io pM = ioP› ‹path M (t_target tM) pM› by blast
obtain pP where "pathlike ?obs (t_target tP) pP" and "p_io pP = ioP"
using ‹∃q' p. q' |∈| t_target tP ∧ path M q' p ∧ p_io p = ioP› unfolding IStep[OF i9]
using that by blast
then have "pathlike ?obs q (tP#pP)"
using ‹t_source tP = q› ‹tP |∈| ts› make_observable_transitions_mono by blast
moreover have "p_io (tP#pP) = ioT # ioP"
using ‹t_input tP = t_input tM› ‹t_output tP = t_output tM› ‹p_io p = ioT # ioP› ‹p = tM # pM› ‹p_io pP = ioP› by simp
ultimately show ?thesis
by auto
qed
show "∃p'. pathlike ?obs q p' ∧ p_io p' = ioT # ioP ⟹ ∃q' p. q' |∈| q ∧ path M q' p ∧ p_io p = ioT # ioP"
proof -
assume "∃p'. pathlike ?obs q p' ∧ p_io p' = ioT # ioP"
then obtain p' where "pathlike ?obs q p'" and "p_io p' = ioT # ioP"
by meson
then obtain tP pP where "p' = tP#pP"
by auto
have "⋀ t' . t' |∈| ftransitions M = (t' ∈ transitions M)"
using ftransitions_set
by metis
from ‹p' = tP#pP› have "t_source tP = q" and "tP |∈| ?obs"
using ‹pathlike ?obs q p'› by auto
then have "tP |∈| ts"
using "1.prems"(6) make_observable_transitions_t_source[of ts dones "ftransitions M"] "1.prems"(1,2)
unfolding ‹⋀ t' . t' |∈| ftransitions M = (t' ∈ transitions M)›
by blast
then have i9: "t_target tP |∈| dones |∪| ?nexts"
by simp
have "pathlike ?obs (t_target tP) pP" and "p_io pP = ioP"
using ‹pathlike ?obs q p'› ‹p_io p' = ioT # ioP› ‹p' = tP#pP› by auto
then have "∃p'. pathlike ?obs (t_target tP) p' ∧ p_io p' = ioP"
by auto
then obtain q'' pM where "q'' |∈| t_target tP" and "path M q'' pM" and "p_io pM = ioP"
using IStep[OF i9] by blast
obtain tM where "t_source tM |∈| q" and "tM ∈ transitions M" and "t_input tM = t_input tP" and "t_output tM = t_output tP" and "t_target tM = q''"
using "1.prems"(1)[OF ‹tP |∈| ts›] ‹q'' |∈| t_target tP›
unfolding ‹t_source tP = q›
by force
have "path M (t_source tM) (tM#pM)"
using ‹tM ∈ transitions M› ‹t_target tM = q''› ‹path M q'' pM› by auto
moreover have "p_io (tM#pM) = ioT # ioP"
using ‹p_io pM = ioP› ‹t_input tM = t_input tP› ‹t_output tM = t_output tP› ‹p_io p' = ioT # ioP› ‹p' = tP#pP› by auto
ultimately show ?thesis
using ‹t_source tM |∈| q› by meson
qed
qed
qed
qed
qed
fun observable_fset :: "('a,'b,'c) transition fset ⇒ bool" where
"observable_fset ts = (∀ t1 t2 . t1 |∈| ts ⟶ t2 |∈| ts ⟶
t_source t1 = t_source t2 ⟶ t_input t1 = t_input t2 ⟶ t_output t1 = t_output t2
⟶ t_target t1 = t_target t2)"
lemma make_observable_transitions_observable :
assumes "⋀ t . t |∈| ts ⟹ t_source t |∈| dones ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' . t' |∈| base_trans ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
and "observable_fset ts"
shows "observable_fset (make_observable_transitions base_trans ((fimage t_target ts) |-| dones) dones ts)"
using assms proof (induction base_trans "(fimage t_target ts) |-| dones" dones ts rule: make_observable_transitions.induct)
case (1 base_trans dones ts)
let ?nexts = "(fimage t_target ts) |-| dones"
define qtrans where qtrans_def: "qtrans = ffUnion (fimage (λ q . (let qts = ffilter (λt . t_source t |∈| q) base_trans;
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . (q,x,y, t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) qts)))) ios)) ?nexts)"
have qtrans_prop: "⋀ t . t |∈| qtrans ⟷ t_source t |∈| ?nexts ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' . t' |∈| base_trans ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
using make_observable_transitions_qtrans_helper[OF qtrans_def]
by presburger
let ?dones' = "dones |∪| ?nexts"
let ?ts' = "ts |∪| qtrans"
let ?nexts' = "(fimage t_target qtrans) |-| ?dones'"
have "observable_fset qtrans"
using qtrans_prop
unfolding observable_fset.simps
by (metis (mono_tags, lifting) Collect_cong fset_inject)
moreover have "t_source |`| qtrans |∩| t_source |`| ts = {||}"
using "1.prems"(1) qtrans_prop by force
ultimately have "observable_fset ?ts'"
using "1.prems"(2) unfolding observable_fset.simps
by blast
have res_cases: "make_observable_transitions base_trans ?nexts dones ts = (if ?nexts' = {||}
then ?ts'
else make_observable_transitions base_trans ?nexts' ?dones' ?ts')"
unfolding make_observable_transitions.simps[of base_trans ?nexts dones ts] qtrans_def Let_def by simp
show ?case proof (cases "?nexts' = {||}")
case True
then have "make_observable_transitions base_trans ?nexts dones ts = ?ts'"
using res_cases by simp
then show ?thesis
using ‹observable_fset ?ts'› by simp
next
case False
then have *: "make_observable_transitions base_trans ?nexts dones ts = make_observable_transitions base_trans ?nexts' ?dones' ?ts'"
using res_cases by simp
have i1: "(⋀t. t |∈| ts |∪| qtrans ⟹
t_source t |∈| dones |∪| ?nexts ∧
t_target t ≠ {||} ∧
fset (t_target t) =
t_target `
{t' . t' |∈| base_trans ∧
t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t})"
using "1.prems"(1) qtrans_prop by blast
have i3: "t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones)) = t_target |`| qtrans |-| (dones |∪| (t_target |`| ts |-| dones))"
by auto
have i4: "t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones)) ≠ {||}"
using False by auto
show ?thesis
using "1.hyps"[OF qtrans_def _ _ i3 i4 i1 ‹observable_fset ?ts'›] unfolding * i3 by metis
qed
qed
lemma make_observable_transitions_transition_props :
assumes "⋀ t . t |∈| ts ⟹ t_source t |∈| dones ∧ t_target t |∈| dones |∪| ((fimage t_target ts) |-| dones) ∧ t_input t |∈| t_input |`| base_trans ∧ t_output t |∈| t_output |`| base_trans"
assumes "t |∈| make_observable_transitions base_trans ((fimage t_target ts) |-| dones) dones ts"
shows "t_source t |∈| dones |∪| (t_target |`| (make_observable_transitions base_trans ((fimage t_target ts) |-| dones) dones ts))"
and "t_target t |∈| dones |∪| (t_target |`| (make_observable_transitions base_trans ((fimage t_target ts) |-| dones) dones ts))"
and "t_input t |∈| t_input |`| base_trans"
and "t_output t |∈| t_output |`| base_trans"
proof -
have "t_source t |∈| dones |∪| (t_target |`| (make_observable_transitions base_trans ((fimage t_target ts) |-| dones) dones ts))
∧ t_target t |∈| dones |∪| (t_target |`| (make_observable_transitions base_trans ((fimage t_target ts) |-| dones) dones ts))
∧ t_input t |∈| t_input |`| base_trans
∧ t_output t |∈| t_output |`| base_trans"
using assms(1,2)
proof (induction base_trans "((fimage t_target ts) |-| dones)" dones ts rule: make_observable_transitions.induct)
case (1 base_trans dones ts)
let ?nexts = "((fimage t_target ts) |-| dones)"
define qtrans where qtrans_def: "qtrans = ffUnion (fimage (λ q . (let qts = ffilter (λt . t_source t |∈| q) base_trans;
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . (q,x,y, t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) qts)))) ios)) ?nexts)"
have qtrans_prop: "⋀ t . t |∈| qtrans ⟷ t_source t |∈| ?nexts ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' . t' |∈| base_trans ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
using make_observable_transitions_qtrans_helper[OF qtrans_def]
by presburger
let ?dones' = "dones |∪| ?nexts"
let ?ts' = "ts |∪| qtrans"
let ?nexts' = "(fimage t_target qtrans) |-| ?dones'"
have res_cases: "make_observable_transitions base_trans ?nexts dones ts = (if ?nexts' = {||}
then ?ts'
else make_observable_transitions base_trans ?nexts' ?dones' ?ts')"
unfolding make_observable_transitions.simps[of base_trans ?nexts dones ts] qtrans_def Let_def by simp
have qtrans_trans_prop: "(⋀t. t |∈| qtrans ⟹
t_source t |∈| dones |∪| (t_target |`| ts |-| dones) ∧
t_target t |∈| dones |∪| (t_target |`| ts |-| dones) |∪| (t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones))) ∧
t_input t |∈| t_input |`| base_trans ∧ t_output t |∈| t_output |`| base_trans)" (is "⋀ t . t |∈| qtrans ⟹ ?P t")
proof -
fix t assume "t |∈| qtrans"
then have "t_source t |∈| dones |∪| (t_target |`| ts |-| dones)"
using ‹t |∈| qtrans› unfolding qtrans_prop[of t] by blast
moreover have "t_target t |∈| dones |∪| (t_target |`| ts |-| dones) |∪| (t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones)))"
using ‹t |∈| qtrans› "1.prems"(1) by blast
moreover have "t_input t |∈| t_input |`| base_trans ∧ t_output t |∈| t_output |`| base_trans"
proof -
obtain t' where "t' ∈ {t'. t' |∈| base_trans ∧ t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
using ‹t |∈| qtrans› unfolding qtrans_prop[of t]
by (metis (mono_tags, lifting) Collect_empty_eq bot_fset.rep_eq empty_is_image fset_inject mem_Collect_eq)
then show ?thesis
by force
qed
ultimately show "?P t"
by blast
qed
show ?case proof (cases "?nexts' = {||}")
case True
then have "t |∈| ?ts'"
using "1.prems"(2) res_cases by force
then show ?thesis
using "1.prems"(1) qtrans_trans_prop
by (metis True fimage_funion funion_fminus_cancel funion_iff res_cases)
next
case False
then have *: "make_observable_transitions base_trans ?nexts dones ts = make_observable_transitions base_trans ?nexts' ?dones' ?ts'"
using res_cases by simp
have i1: "t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones)) = t_target |`| qtrans |-| (dones |∪| (t_target |`| ts |-| dones))"
by blast
have i2: "t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones)) ≠ {||}"
using False by blast
have i3: "(⋀t. t |∈| ts |∪| qtrans ⟹
t_source t |∈| dones |∪| (t_target |`| ts |-| dones) ∧
t_target t |∈| dones |∪| (t_target |`| ts |-| dones) |∪| (t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones))) ∧
t_input t |∈| t_input |`| base_trans ∧ t_output t |∈| t_output |`| base_trans)"
using "1.prems"(1) qtrans_trans_prop by blast
have i4: "t |∈| make_observable_transitions base_trans (t_target |`| (ts |∪| qtrans) |-| (dones |∪| (t_target |`| ts |-| dones))) (dones |∪| (t_target |`| ts |-| dones)) (ts |∪| qtrans)"
using "1.prems"(2) unfolding * i1 by assumption
show ?thesis
using "1.hyps"[OF qtrans_def _ _ i1 i2 i3 i4] unfolding i1 unfolding *[symmetric]
using make_observable_transitions_mono[of ts base_trans ?nexts dones] by blast
qed
qed
then show "t_source t |∈| dones |∪| (t_target |`| (make_observable_transitions base_trans ((fimage t_target ts) |-| dones) dones ts))"
and "t_target t |∈| dones |∪| (t_target |`| (make_observable_transitions base_trans ((fimage t_target ts) |-| dones) dones ts))"
and "t_input t |∈| t_input |`| base_trans"
and "t_output t |∈| t_output |`| base_trans"
by blast+
qed
fun make_observable :: "('a :: linorder,'b :: linorder,'c :: linorder) fsm ⇒ ('a fset,'b,'c) fsm" where
"make_observable M = (let
initial_trans = (let qts = ffilter (λt . t_source t = initial M) (ftransitions M);
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . ({|initial M|},x,y, t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) qts)))) ios);
nexts = fimage t_target initial_trans |-| {|{|initial M|}|};
ptransitions = make_observable_transitions (ftransitions M) nexts {|{|initial M|}|} initial_trans;
pstates = finsert {|initial M|} (t_target |`| ptransitions);
M' = create_unconnected_fsm_from_fsets {|initial M|} pstates (finputs M) (foutputs M)
in add_transitions M' (fset ptransitions))"
lemma make_observable_language_observable :
shows "L (make_observable M) = L M"
and "observable (make_observable M)"
and "initial (make_observable M) = {|initial M|}"
and "inputs (make_observable M) = inputs M"
and "outputs (make_observable M) = outputs M"
proof -
define initial_trans where "initial_trans = (let qts = ffilter (λt . t_source t = initial M) (ftransitions M);
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . ({|initial M|},x,y, t_target |`| ((ffilter (λt . (t_input t, t_output t) = (x,y)) qts)))) ios)"
moreover define ptransitions where "ptransitions = make_observable_transitions (ftransitions M) (fimage t_target initial_trans |-| {|{|initial M|}|}) {|{|initial M|}|} initial_trans"
moreover define pstates where "pstates = finsert {|initial M|} (t_target |`| ptransitions)"
moreover define M' where "M' = create_unconnected_fsm_from_fsets {|initial M|} pstates (finputs M) (foutputs M)"
ultimately have "make_observable M = add_transitions M' (fset ptransitions)"
unfolding make_observable.simps Let_def by blast
have "{|initial M|} |∈| pstates"
unfolding pstates_def by blast
have "inputs M' = inputs M"
unfolding M'_def create_unconnected_fsm_from_fsets_simps(3)[OF ‹{|initial M|} |∈| pstates›, of "finputs M" "foutputs M"]
using fset_of_list.rep_eq inputs_as_list_set by fastforce
have "outputs M' = outputs M"
unfolding M'_def create_unconnected_fsm_from_fsets_simps(4)[OF ‹{|initial M|} |∈| pstates›, of "finputs M" "foutputs M"]
using fset_of_list.rep_eq outputs_as_list_set by fastforce
have "states M' = fset pstates" and "transitions M' = {}" and "initial M' = {|initial M|}"
unfolding M'_def create_unconnected_fsm_from_fsets_simps(1,2,5)[OF ‹{|initial M|} |∈| pstates›] by simp+
have initial_trans_prop: "⋀ t . t |∈| initial_trans ⟷ t_source t |∈| {|{|FSM.initial M|}|} ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' ∈ transitions M . t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
proof -
have *:"⋀ t' . t' |∈| ftransitions M = (t' ∈ transitions M)"
using ftransitions_set
by metis
have **: "initial_trans = ffUnion (fimage (λ q . (let qts = ffilter (λt . t_source t |∈| q) (ftransitions M);
ios = fimage (λ t . (t_input t, t_output t)) qts
in fimage (λ(x,y) . (q,x,y, t_target |`| (ffilter (λt . (t_input t, t_output t) = (x,y)) qts))) ios)) {|{|initial M|}|})"
unfolding initial_trans_def by auto
show "⋀ t . t |∈| initial_trans ⟷ t_source t |∈| {|{|FSM.initial M|}|} ∧ t_target t ≠ {||} ∧ fset (t_target t) = t_target ` {t' ∈ transitions M . t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
unfolding make_observable_transitions_qtrans_helper[OF **] *
by presburger
qed
have well_formed_transitions: "⋀ t . t ∈ (fset ptransitions) ⟹ t_source t ∈ states M' ∧ t_input t ∈ inputs M' ∧ t_output t ∈ outputs M' ∧ t_target t ∈ states M'"
(is "⋀ t . t ∈ (fset ptransitions) ⟹ ?P1 t ∧ ?P2 t ∧ ?P3 t ∧ ?P4 t")
proof -
fix t assume "t ∈ (fset ptransitions)"
then have i2: "t |∈| make_observable_transitions (ftransitions M) (fimage t_target initial_trans |-| {|{|initial M|}|}) {|{|initial M|}|} initial_trans"
using ptransitions_def
by metis
have i1: "(⋀t. t |∈| initial_trans ⟹
t_source t |∈| {|{|FSM.initial M|}|} ∧
t_target t |∈| {|{|FSM.initial M|}|} |∪| (t_target |`| initial_trans |-| {|{|FSM.initial M|}|}) ∧
t_input t |∈| t_input |`| ftransitions M ∧ t_output t |∈| t_output |`| ftransitions M)" (is "⋀ t . t |∈| initial_trans ⟹ ?P t")
proof -
fix t assume *: "t |∈| initial_trans"
then have "t_source t |∈| {|{|FSM.initial M|}|}"
and "t_target t ≠ {||}"
and "fset (t_target t) = t_target ` {t' ∈ FSM.transitions M. t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}"
using initial_trans_prop by blast+
have "t_target t |∈| {|{|FSM.initial M|}|} |∪| (t_target |`| initial_trans |-| {|{|FSM.initial M|}|})"
using "*" by blast
moreover have "t_input t |∈| t_input |`| ftransitions M ∧ t_output t |∈| t_output |`| ftransitions M"
proof -
obtain t' where "t' ∈ transitions M" and "t_input t = t_input t'" and "t_output t = t_output t'"
using ‹t_target t ≠ {||}› ‹fset (t_target t) = t_target ` {t' ∈ FSM.transitions M. t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t}›
by (metis (mono_tags, lifting) bot_fset.rep_eq empty_Collect_eq fset_inject image_empty)
have "fset (ftransitions M) = transitions M"
by (simp add: fset_of_list.rep_eq fsm_transitions_finite)
then show ?thesis
unfolding ‹t_input t = t_input t'› ‹t_output t = t_output t'›
using ‹t' ∈ transitions M›
by auto
qed
ultimately show "?P t"
using ‹t_source t |∈| {|{|FSM.initial M|}|}› by blast
qed
have "?P1 t"
using make_observable_transitions_transition_props(1)[OF i1 i2] unfolding pstates_def ptransitions_def ‹states M' = fset pstates›
by (metis finsert_is_funion)
moreover have "?P2 t"
proof-
have "t_input t |∈| t_input |`| ftransitions M"
using make_observable_transitions_transition_props(3)[OF i1 i2] by blast
then have "t_input t ∈ t_input ` transitions M"
using ftransitions_set by (metis (mono_tags, lifting) fset.set_map)
then show ?thesis
using finputs_set fsm_transition_input ‹inputs M' = inputs M› by fastforce
qed
moreover have "?P3 t"
proof-
have "t_output t |∈| t_output |`| ftransitions M"
using make_observable_transitions_transition_props(4)[OF i1 i2] by blast
then have "t_output t ∈ t_output ` transitions M"
using ftransitions_set by (metis (mono_tags, lifting) fset.set_map)
then show ?thesis
using foutputs_set fsm_transition_output ‹outputs M' = outputs M› by fastforce
qed
moreover have "?P4 t"
using make_observable_transitions_transition_props(2)[OF i1 i2] unfolding pstates_def ptransitions_def ‹states M' = fset pstates›
by (metis finsert_is_funion)
ultimately show "?P1 t ∧ ?P2 t ∧ ?P3 t ∧ ?P4 t"
by blast
qed
have "initial (make_observable M) = {|initial M|}"
and "states (make_observable M) = fset pstates"
and "inputs (make_observable M) = inputs M"
and "outputs (make_observable M) = outputs M"
and "transitions (make_observable M) = fset ptransitions"
using add_transitions_simps[OF well_formed_transitions, of "fset ptransitions"]
unfolding ‹make_observable M = add_transitions M' (fset ptransitions)›[symmetric]
‹inputs M' = inputs M› ‹outputs M' = outputs M› ‹initial M' = {|initial M|}› ‹states M' = fset pstates› ‹transitions M' = {}›
by blast+
then show "initial (make_observable M) = {|initial M|}" and "inputs (make_observable M) = inputs M" and "outputs (make_observable M) = outputs M"
by presburger+
have i1: "(⋀t. t |∈| initial_trans ⟹
t_source t |∈| {|{|FSM.initial M|}|} ∧
t_target t ≠ {||} ∧
fset (t_target t) = t_target ` {t' ∈ FSM.transitions M. t_source t' |∈| t_source t ∧ t_input t' = t_input t ∧ t_output t' = t_output t})"
using initial_trans_prop by blast
have i2: "(⋀q t'.
q |∈| {|{|FSM.initial M|}|} ⟹
t' ∈ FSM.transitions M ⟹ t_source t' |∈| q ⟹ ∃t. t |∈| initial_trans ∧ t_source t = q ∧ t_input t = t_input t' ∧ t_output t = t_output t')"
proof -
fix q t' assume "q |∈| {|{|FSM.initial M|}|}" and "t' ∈ FSM.transitions M" and "t_source t' |∈| q"
then have "q = {|FSM.initial M|}" and "t_source t' = initial M"
by auto
define tgt where "tgt = t_target ` {t'' ∈ FSM.transitions M. t_source t'' |∈| {|FSM.initial M|} ∧ t_input t'' = t_input t' ∧ t_output t'' = t_output t'}"
have "t_target t' ∈ tgt"
unfolding tgt_def using ‹t' ∈ FSM.transitions M› ‹t_source t' = initial M› by auto
then have "tgt ≠ {}"
by auto
have "finite tgt"
using fsm_transitions_finite[of M] unfolding tgt_def by auto
then have "fset (Abs_fset tgt) = tgt"
by (simp add: Abs_fset_inverse)
then have "Abs_fset tgt ≠ {||}"
using ‹tgt ≠ {}› by auto
let ?t = "({|FSM.initial M|}, t_input t', t_output t', Abs_fset tgt)"
have "?t |∈| initial_trans"
unfolding initial_trans_prop fst_conv snd_conv ‹fset (Abs_fset tgt) = tgt›
unfolding ‹tgt = t_target ` {t'' ∈ FSM.transitions M. t_source t'' |∈| {|FSM.initial M|} ∧ t_input t'' = t_input t' ∧ t_output t'' = t_output t'}›[symmetric]
using ‹Abs_fset tgt ≠ {||}›
by blast
then show "∃t. t |∈| initial_trans ∧ t_source t = q ∧ t_input t = t_input t' ∧ t_output t = t_output t'"
using ‹q = {|FSM.initial M|}› by auto
qed
have i3: "(⋀q. q |∈| t_target |`| initial_trans |-| {|{|FSM.initial M|}|} ⟹ q |∈| fPow (t_source |`| ftransitions M |∪| t_target |`| ftransitions M))"
proof -
fix q assume "q |∈| t_target |`| initial_trans |-| {|{|FSM.initial M|}|}"
then obtain t where "t |∈| initial_trans" and "t_target t = q"
by auto
have "fset q ⊆ t_target ` (transitions M)"
using ‹t |∈| initial_trans›
unfolding initial_trans_prop ‹t_target t = q›
by auto
then have "q |⊆| (t_target |`| ftransitions M)"
using ftransitions_set[of M]
by (simp add: less_eq_fset.rep_eq)
then show "q |∈| fPow (t_source |`| ftransitions M |∪| t_target |`| ftransitions M)"
by auto
qed
have i4: "(⋀q. q |∈| {|{|FSM.initial M|}|} ⟹ q |∈| fPow (t_source |`| ftransitions M |∪| t_target |`| ftransitions M |∪| {|FSM.initial M|}))"
and i5: "{||} |∉| {|{|FSM.initial M|}|}"
and i6: "{|FSM.initial M|} |∈| {|{|FSM.initial M|}|}"
by blast+
show "L (make_observable M) = L M"
proof -
have *: "⋀ p . pathlike ptransitions {|initial M|} p = path (make_observable M) {|initial M|} p"
proof
have "⋀ q p . p ≠ [] ⟹ pathlike ptransitions q p ⟹ path (make_observable M) q p"
proof -
fix q p assume "p ≠ []" and "pathlike ptransitions q p"
then show "path (make_observable M) q p"
proof (induction p arbitrary: q)
case Nil
then show ?case by blast
next
case (Cons t p)
then have "t |∈| ptransitions" and "pathlike ptransitions (t_target t) p" and "t_source t = q"
by blast+
have "t ∈ transitions (make_observable M)"
using ‹t |∈| ptransitions› ‹transitions (make_observable M) = fset ptransitions›
by metis
moreover have "path (make_observable M) (t_target t) p"
using Cons.IH[OF _ ‹pathlike ptransitions (t_target t) p›] calculation by blast
ultimately show ?case
using ‹t_source t = q› by blast
qed
qed
then show "⋀ p . pathlike ptransitions {|initial M|} p ⟹ path (make_observable M) {|initial M|} p"
by (metis ‹FSM.initial (make_observable M) = {|FSM.initial M|}› fsm_initial path.nil)
show "⋀ q p . path (make_observable M) q p ⟹ pathlike ptransitions q p"
proof -
fix q p assume "path (make_observable M) q p"
then show "pathlike ptransitions q p"
proof (induction p arbitrary: q rule: list.induct)
case Nil
then show ?case by blast
next
case (Cons t p)
then have "t ∈ transitions (make_observable M)" and "path (make_observable M) (t_target t) p" and "t_source t = q"
by blast+
have "t |∈| ptransitions"
using ‹t ∈ transitions (make_observable M)› ‹transitions (make_observable M) = fset ptransitions›
by metis
then show ?case
using Cons.IH[OF ‹path (make_observable M) (t_target t) p›] ‹t_source t = q› by blast
qed
qed
qed
have "⋀ io . (∃q' p. q' |∈| {|FSM.initial M|} ∧ path M q' p ∧ p_io p = io) = (∃p'. pathlike ptransitions {|FSM.initial M|} p' ∧ p_io p' = io)"
using make_observable_transitions_path[OF i1 i2 i3 i4 i5 i6] unfolding ptransitions_def[symmetric] by blast
then have "⋀ io . (∃p. path M (FSM.initial M) p ∧ p_io p = io) = (∃p' . path (make_observable M) {|initial M|} p' ∧ p_io p' = io)"
unfolding *
by (metis (no_types, lifting) fempty_iff finsert_iff)
then show ?thesis
unfolding LS.simps ‹initial (make_observable M) = {|initial M|}› by (metis (no_types, lifting))
qed
show "observable (make_observable M)"
proof -
have i2: "observable_fset initial_trans"
unfolding observable_fset.simps
unfolding initial_trans_prop
using fset_inject
by metis
have "⋀ t' . t' |∈| ftransitions M = (t' ∈ transitions M)"
using ftransitions_set
by metis
have "observable_fset ptransitions"
using make_observable_transitions_observable[OF _ i2, of "{| {|initial M|} |}" "ftransitions M"] i1
unfolding ptransitions_def ‹⋀ t' . t' |∈| ftransitions M = (t' ∈ transitions M)›
by blast
then show ?thesis
unfolding observable.simps observable_fset.simps ‹transitions (make_observable M) = fset ptransitions›
by metis
qed
qed
end