Theory SM.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.  DDD }"  
    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. pset (program.processes prog)}"

definition "local_var_approx prog  { 
  set (proc_decl.local_vars p) | p. pset (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 proggc_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 "ccfg_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 "gcgco_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.  DDD }"  
    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