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 (simp add: vimage_def)
    apply (subst aux2)
    apply (rule finite_Union)
    using [[simproc add: finite_Collect]]
    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)"
  using [[simproc add: finite_Collect]]
  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)"
  using [[simproc add: finite_Collect]]
  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
    using [[simproc add: finite_Collect]]
    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 []
    apply (simp add: finite_maps_to_finite_type)
    apply (simp add: finite_maps_to_finite_type)
    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