Theory SM_Finite_Reachable

```theory SM_Finite_Reachable
imports Type_System
begin

(* TODO: Move to Misc, near lists_of_len_fin1 - lemma *)
lemma lists_le_len_fin: "finite P ⟹ finite (lists P ∩ { l. length l ≤ n })"
proof (induct n)
case 0 thus ?case by auto
next
case (Suc n)
have "lists P ∩ { l. length l ≤ Suc n }
= (lists P ∩ {l. length l ≤ n})
∪ (λ(a,l). a#l) ` (P × (lists P ∩ {l. length l ≤ n}))"
apply auto
apply (case_tac x)
apply auto
done
moreover from Suc have "finite …" by auto
ultimately show ?case by simp
qed

lemma obtain_list_of_multiset:
obtains l where "mset l = m"
proof -
have "∃l. mset l = m"
apply (induction m)
apply auto
apply (rule_tac x="x#l" in exI)
apply auto
done
thus ?thesis using that by blast
qed

lemma finitely_many_lists_for_multiset[simp, intro!]:
"finite {l . mset l = m}"
proof -
have "{l . mset l = m} ⊆ {l. set l ⊆ set_mset m ∧ length l = size m}"
by auto
also note finite_lists_length_eq
finally (finite_subset) show ?thesis by auto
qed

lemma finite_size_bounded_msets:
assumes "finite S"
shows "finite { m . size m ≤ len ∧ set_mset m ⊆ S }"
proof -
have "{ m . size m ≤ len ∧ set_mset m ⊆ S }
⊆ mset`(lists S ∩ {l. length l ≤ len})"
apply clarsimp
apply (rule_tac m=x in obtain_list_of_multiset)
apply (auto intro!: imageI)
done
also have "finite (mset`(lists S ∩ {l. length l ≤ len}))"
apply (rule finite_imageI)
apply (rule lists_le_len_fin)
by (rule assms)
finally (finite_subset) show ?thesis .
qed

lemma finite_maps_to_finite_type:
assumes "finite (D::'a set)" "finite (UNIV::'v set)"
shows "finite ((dom::(_ ⇀ 'v) ⇒ _) -` Pow D)"
proof -
{fix DD::"'a set"
have "{x. dom x ⊆ DD} = ⋃{ {x. dom x = D } | D.  D⊆DD }"
by auto
} note aux2=this

from assms show ?thesis
apply (subst aux2)
apply (rule finite_Union)
apply simp
apply clarsimp
apply (rule finite_set_of_finite_maps[where B="UNIV::'v set", simplified])
apply (erule finite_subset)
apply simp
by simp
qed

text ‹In the following, we prove that the set of reachable states is finite.›

text ‹Approximation of reachable CFG-states›
definition "cfg_approx prog
≡ ⋃{approx_reachable ((proc_decl.body p)) | p. p∈set (program.processes prog)}"

definition "local_var_approx prog ≡ ⋃{
set (proc_decl.local_vars p) | p. p∈set (program.processes prog) }"
definition "global_var_approx prog ≡ set (program.global_vars prog)"

definition "lc_approx prog ≡ {
⦇
local_config.command = c,
local_config.state = ⦇ local_state.variables = v⦈ ⦈
| c v. c ∈ cfg_approx prog ∧ dom v ⊆ local_var_approx prog }"

definition "gc_approx prog ≡ {
⦇ global_config.processes = lcs,
global_config.state = ⦇ global_state.variables = v ⦈
⦈ | lcs v.
size lcs ≤ length (program.processes prog)
∧ set_mset lcs ⊆ lc_approx prog
∧ dom v ⊆ global_var_approx prog
}"

definition "gco_approx prog ≡ insert None (Some`gc_approx prog)"

lemma ginit_approx: "init_gc prog∈gc_approx prog"
unfolding init_gc_def gc_approx_def
apply auto
apply (auto simp:
init_pc_def lc_approx_def cfg_approx_def local_var_approx_def
global_var_approx_def )
done

lemma init_approx: "gc ∈ li.init prog ⟹ gc ∈ gco_approx prog"
apply (cases gc)
apply (auto simp: gco_approx_def ginit_approx li.init_conv)
done

lemma cfg_approx:
assumes "c∈cfg_approx prog"
assumes "cfg c a c'"
shows "c'∈cfg_approx prog"
using assms
unfolding cfg_approx_def
by (auto dest: approx_reachable_closed)

lemma step_approx:
assumes "gc∈gco_approx prog"
assumes "(gc, gc') ∈ li.step"
shows "gc'∈gco_approx prog"
using assms
unfolding li.step_def
apply (cases gc, simp_all add: gco_approx_def)
apply (auto simp: li.gstep_eq_conv elim!: stutter_extend_edgesE) []
apply (cases gc', simp_all)
apply (rule imageI)
apply (auto simp: li.gstep_eq_conv elim!: stutter_extend_edgesE) []

unfolding li.gstep_succ_def
apply clarsimp
apply (clarsimp split: sum.splits option.splits bool.splits Option.bind_splits)
apply (clarsimp simp: gco_approx_def gc_approx_def)
apply (case_tac bb, clarsimp_all)
apply (frule la_ex_pres_gs_vars, clarsimp)
apply (clarsimp simp: lc_approx_def)
apply (case_tac ac, clarsimp_all)
apply (frule la_ex_pres_ls_vars, clarsimp)

apply (auto simp: cfg_approx) []
done

lemma finite_local_var_approx[simp, intro!]: "finite (local_var_approx prog)"
unfolding local_var_approx_def
apply (rule finite_Union)
apply simp
apply clarsimp
done

lemma finite_global_var_approx[simp, intro!]: "finite (global_var_approx prog)"
unfolding global_var_approx_def
by simp

lemma gco_approx_finite[simp, intro!]: "finite (gco_approx prog)"
proof -
have aux1: "({lcs.
size lcs
≤ length (program.processes prog)} ∩
set_mset -` Pow (lc_approx prog))
= {lcs. size lcs ≤ length (program.processes prog) ∧ set_mset lcs ⊆ lc_approx prog }"
by auto

{fix DD::"ident set"
have "{x. dom x ⊆ DD} = ⋃{ {x. dom x = D } | D.  D⊆DD }"
by auto
} note aux2=this

show ?thesis
unfolding gco_approx_def
apply simp
apply (rule finite_imageI)
unfolding gc_approx_def
apply simp
apply (rule finite_imageI)
apply (subst aux1)
apply (rule finite_cartesian_product)
apply (rule finite_size_bounded_msets)
unfolding lc_approx_def
apply simp
apply (rule finite_imageI)
apply (rule finite_cartesian_product)
unfolding cfg_approx_def
apply (rule finite_Union)
apply simp
apply auto []
done
qed

lemma sys_finite_reachable: "finite ((g_E (li.system_automaton prog))⇧* ``
g_V0 (li.system_automaton prog))"
proof -
have "(g_E (li.system_automaton prog))⇧* `` g_V0 (li.system_automaton prog) ⊆ gco_approx prog"
apply safe
apply (erule rtrancl_induct)
apply (auto intro: step_approx init_approx)
done
also note gco_approx_finite
finally (finite_subset) show ?thesis .
qed

lemma "finite ((g_E (li.system_automaton (dloc prog)))⇧* ``
g_V0 (li.system_automaton (dloc prog)))"
by (rule sys_finite_reachable)

context well_typed_prog begin
lemma li'_finite_reachable: "finite ((g_E li'.s2.system_automaton)⇧* `` g_V0 li'.s2.system_automaton)"
proof -
show ?thesis
apply (rule li'.bisim.s1.reachable_finite_sim)
apply (rule sys_finite_reachable)
apply (clarsimp simp: build_rel_def)
apply (case_tac b)
apply simp
apply simp
done
qed
end

end

```