Theory SM.Rename_Cfg

theory Rename_Cfg
imports "../RefPoint/SM_Cfg"
  Type_System SM_Finite_Reachable Gen_Cfg_Bisim
  "HOL-Library.IArray"
begin

(* TODO: Move *)
lemma set_list_bind[simp]: "set (List.bind m f) = Set.bind (set m) (λx. set (f x))"
  by (auto simp: List.bind_def)

lemma rel_mset_of_mapI:
  assumes "∀x∈set l. R (f x) (g x)"
  shows "rel_mset R (mset (map f l)) (mset (map g l))"
  using assms
  apply (induction l)
  apply (auto simp: rel_mset_Zero rel_mset_Plus)
  done


(* TODO: Move? *)
lemma finite_max1_elemI:
  assumes "(∀x y. x∈S ∧ y∈S ⟶ x=y)"  
  shows "finite S"
proof (cases "S={}")
  case False 
  with assms obtain x where "S={x}" by auto
  thus ?thesis by auto
qed auto


lemma left_unique_finite_sngI: 
  assumes "left_unique R" 
  shows "finite {a. R a b}"
proof (rule finite_subset)
  { 
    fix x y
    assume "x∈{a. R a b}" "y∈{a. R a b}"
    hence "x=y" using assms
      by (auto dest: left_uniqueD)
  } thus "finite {a. R a b}"
    by (blast intro: finite_max1_elemI)
qed auto   



function approx_reachable_list_aux :: "cmd ⇒ cmd list" where
  "approx_reachable_list_aux (Assign c x e) = [Assign c x e, Skip]"
| "approx_reachable_list_aux (Assign_local c x e) = [Assign_local c x e, Skip]"
| "approx_reachable_list_aux (Assign_global c x e) = [Assign_global c x e, Skip]"
| "approx_reachable_list_aux (Test e) = [Test e, Skip]"
| "approx_reachable_list_aux (Skip) = [Skip]"
| "approx_reachable_list_aux (Seq c1 c2) = (approx_reachable_list_aux c2) @ (do { c1←approx_reachable_list_aux c1; [Seq c1 c2] })"
| "approx_reachable_list_aux (Or c1 c2) = (Or c1 c2) # (approx_reachable_list_aux c1 @ approx_reachable_list_aux c2)"
| "approx_reachable_list_aux (Break) = [Break,Invalid]"
| "approx_reachable_list_aux (Continue) = [Continue,Invalid]"
| "approx_reachable_list_aux (Iterate c1 c2) = Skip #
    (do { c1←approx_reachable_list_aux c1; [Iterate c1 c2] })
  @ (do { c2'←approx_reachable_list_aux c2; [Iterate c2' c2] })"
| "approx_reachable_list_aux Invalid = [Invalid]"
by pat_completeness auto

termination
  apply (relation "reachable_term_order_aux <*mlex*> measure size")
  apply (metis wf_measure wf_mlex)
  apply (auto simp: mlex_prod_def)
  done

lemma approx_reachable_list_aux_refine: 
  "set (approx_reachable_list_aux c) = approx_reachable c"
  apply (induction c rule: approx_reachable.induct)
  apply (simp_all)
  done

definition "cfg_V0 prog ≡ proc_decl.body ` set (program.processes prog)"
definition "cfg_V0_list prog ≡ remdups (map proc_decl.body (program.processes prog))"

lemma cfg_V0_list_invar: "distinct (cfg_V0_list prog)"
  unfolding cfg_V0_list_def by auto

lemma cfg_V0_list_refine: "set (cfg_V0_list prog) = cfg_V0 prog"
  unfolding cfg_V0_list_def cfg_V0_def by auto


definition "approx_reachable_list prog ≡ 
  remdups (concat (map approx_reachable_list_aux (cfg_V0_list prog)))"

definition "approx_reachable_prog prog ≡ ⋃(approx_reachable`(cfg_V0 prog))"


lemma approx_reachable_list_invar: "distinct (approx_reachable_list prog)"
  unfolding approx_reachable_list_def
  by auto

lemma approx_reachable_list_refine: 
  "set (approx_reachable_list prog) = approx_reachable_prog prog"
  unfolding approx_reachable_list_def approx_reachable_prog_def
  by (auto simp: approx_reachable_list_aux_refine cfg_V0_list_refine)

text ‹CFG successors›
primrec cfg_succ :: "cmd ⇒ ((action+brk_ctd) × cmd) set" where
  "cfg_succ (Assign c x e) = {((Inl (AAssign c x e)), Skip)}"
| "cfg_succ (Assign_local c x e) = {((Inl (AAssign_local c x e)), Skip)}"
| "cfg_succ (Assign_global c x e) = {((Inl (AAssign_global c x e)), Skip)}"
| "cfg_succ (Test e) = {((Inl (ATest e)), Skip)}"
| "cfg_succ (Seq c1 c2) =
  ( if c1=Skip then 
      {((Inl ASkip), c2)}
    else
      { (e,if c1'=Skip then c2 else Seq c1' c2) | c1' e.  (e,c1')∈cfg_succ c1}
  )"
| "cfg_succ (Or c1 c2) = cfg_succ c1 ∪ cfg_succ c2"
| "cfg_succ (Break) = {(Inr AIBreak, Invalid)}"
| "cfg_succ (Continue) = {(Inr AIContinue, Invalid)}"
| cfg_succ_iterate: 
  "cfg_succ (Iterate c cb) =
  (if c=Skip then {(Inl ASkip, Iterate cb cb)} else {})
  ∪ (
    λ (Inl e,c') ⇒ (Inl e, if c'=Skip then Iterate cb cb else Iterate c' cb)
    | (Inr AIBreak,_) ⇒ (Inl ASkip,Skip)
    | (Inr AIContinue,_) ⇒ (Inl ASkip, Iterate cb cb)
  )`cfg_succ c"
| "cfg_succ Skip = {}"
| "cfg_succ Invalid = {}"


declare cfg_succ_iterate[simp del]
lemma cfg_succ_iterate'[simp]: "cfg_succ (Iterate c cb) = 
  (if c=Skip then {(Inl ASkip, Iterate cb cb)} else {})
  ∪ { (Inl e, if c'=Skip then Iterate cb cb else Iterate c' cb) | e c'. (Inl e, c') ∈ cfg_succ c }
  ∪ (if ∃c'. (Inr AIBreak,c')∈ cfg_succ c then { (Inl ASkip, Skip)} else {})
  ∪ (if ∃c'. (Inr AIContinue,c')∈ cfg_succ c then { (Inl ASkip, Iterate cb cb)} else {})"
  unfolding cfg_succ_iterate
  apply (rule sym)
  apply (cases "c=Skip")
  apply simp
  apply safe
  apply simp_all
  apply force
  apply (force split: if_split_asm)
  apply (force split: if_split_asm)
  apply (auto split: if_split_asm sum.splits brk_ctd.splits)
  done

lemma cfg_succ_iff_cfg: "(a,c')∈cfg_succ c ⟷ cfg c a c'"
  apply rule
  apply (induction c arbitrary: a c')
  apply ((auto intro: cfg.intros split: if_split_asm) [])+
  
  apply (induction rule: cfg.induct)
  apply auto
  done

theorem cfg_succ_correct: "cfg_succ c = {(a,c'). cfg c a c'}"
  using cfg_succ_iff_cfg by auto

lemma cfg_succ_finite[simp, intro!]: "finite (cfg_succ c)"
  apply (induction c)
  using [[simproc add: finite_Collect]]
  apply (simp_all del: cfg_succ_iterate' add: cfg_succ_iterate)
  done
 

primrec cfg_succ_list :: "cmd ⇒ ((action+brk_ctd) × cmd) list" where
  "cfg_succ_list (Assign ge x e) = [((Inl (AAssign ge x e)), Skip)]"
| "cfg_succ_list (Assign_local ge x e) = [((Inl (AAssign_local ge x e)), Skip)]"
| "cfg_succ_list (Assign_global ge x e) = [((Inl (AAssign_global ge x e)), Skip)]"
| "cfg_succ_list (Test e) = [((Inl (ATest e)), Skip)]"
| "cfg_succ_list (Seq c1 c2) =
    ( if c1=Skip then 
        [((Inl ASkip), c2)] 
      else 
        map (λ(e,c1'). (e,if c1'=Skip then c2 else Seq c1' c2)) (cfg_succ_list c1)
    )"
| "cfg_succ_list (Or c1 c2) = remdups (cfg_succ_list c1 @ cfg_succ_list c2)"
| "cfg_succ_list (Break) = [(Inr AIBreak, Invalid)]"
| "cfg_succ_list (Continue) = [(Inr AIContinue, Invalid)]"
| cfg_succ_list_iterate: 
  "cfg_succ_list (Iterate c cb) =
  (if c=Skip then [(Inl ASkip, Iterate cb cb)] else [])
  @ remdups (map (
    λ (Inl e,c') ⇒ (Inl e, if c'=Skip then Iterate cb cb else Iterate c' cb)
    | (Inr AIBreak,_) ⇒ (Inl ASkip,Skip)
    | (Inr AIContinue,_) ⇒ (Inl ASkip, Iterate cb cb)
  ) (cfg_succ_list c))"
| "cfg_succ_list Skip = []"
| "cfg_succ_list Invalid = []"

(* FIXME: Strange, the simplifier should know such lemmas!? *)
lemma Seq_ne_structural[simp]:
  "Seq a b ≠ a"
  "Seq a b ≠ b"
  "a ≠ Seq a b"
  "b ≠ Seq a b"
proof -
  show G1: "Seq a b ≠ a"
    by (induction a arbitrary: b) auto
  show G2: "Seq a b ≠ b"
    by (induction b arbitrary: a) auto
  show "a ≠ Seq a b" using G1 by simp
  show "b ≠ Seq a b" using G2 by simp
qed

lemma cfg_succ_list_invar: "distinct (cfg_succ_list c)"
  apply (induction c)
  apply (auto simp: distinct_map)
  apply (rule inj_onI)
  apply (auto split: if_split_asm ) []
  done  

lemma cfg_succ_list_refine: "set (cfg_succ_list c) = cfg_succ c"
  apply (induction c)
  apply (simp_all only: cfg_succ.simps cfg_succ_list.simps 
    if_distrib[of set] set_map)
  apply (simp_all)
  apply (auto, force+) []
  done

definition "cfg'_succ_list c ≡ map (map_prod projl id) (filter (isl o fst) (cfg_succ_list c))"

lemma cfg'_succ_list_invar: "distinct (cfg'_succ_list c)"
  unfolding cfg'_succ_list_def
  apply (auto simp: distinct_map cfg_succ_list_invar intro!: inj_onI)
  apply (rename_tac a a' foo)
  apply (case_tac a, simp_all)
  done
  
lemma cfg'_succ_list_refine: "set (cfg'_succ_list c) = {(a,c'). cfg' c a c'}"
  unfolding cfg'_succ_list_def
  by (force simp: cfg_succ_list_refine cfg'_def cfg_succ_correct)





definition "index_of l x ≡ 
  if ∃i<length l. l!i=x then
    Some (THE i. i<length l ∧ l!i=x)
  else None"

lemma index_of_Some_conv:
  assumes "distinct l"
  shows "index_of l x = Some i ⟷ i < length l ∧ l ! i = x"
proof safe
  show "index_of l x = Some i ⟹ i < length l"
    using assms unfolding index_of_def distinct_conv_nth
    by (metis (mono_tags, lifting) option.distinct(1) option.inject theI)
  show "index_of l x = Some i ⟹ l ! i = x"
    using assms unfolding index_of_def distinct_conv_nth
    by (metis (mono_tags, lifting) option.distinct(1) option.inject theI)
  show "i < length l ⟹ x = l ! i ⟹ index_of l (l ! i) = Some i"
    using assms unfolding index_of_def distinct_conv_nth by auto
qed

lemma dom_index_of: "dom (index_of l) = set l"
  by (auto simp: index_of_def in_set_conv_nth split: if_split_asm)

lemma index_of_None_conv: "index_of l x = None ⟷ x∉set l"
  using dom_index_of[of l] by auto

lemma index_of_Nil: "index_of [] x = None"
  by (auto simp: index_of_None_conv)

lemma index_of_Cons: "distinct (a#l) 
  ⟹ index_of (a#l) x = (if x=a then Some 0 else map_option Suc (index_of l x))"
  apply (auto simp: index_of_Some_conv)
  apply (cases "index_of (a # l) x")
  apply (simp_all only: )
  apply (cases "index_of l x")
  apply (simp_all only: ) [2]
  apply (auto simp: index_of_Some_conv index_of_None_conv) [2]
  apply (cases "index_of l x")
  apply (simp_all only: )
  apply (auto simp: index_of_Some_conv index_of_None_conv 
    in_set_conv_nth nth_Cons nth_eq_iff_index_eq split: nat.splits)
  done

primrec cr_index_of where
  "cr_index_of [] x = None"
| "cr_index_of (a#l) x = (if x=a then Some 0 else map_option Suc (cr_index_of l x))"

lemma cr_index_of_eq: "distinct l ⟹ cr_index_of l = index_of l"
  apply (induction l)
  apply (auto simp: index_of_Nil index_of_Cons)
  done

locale sl_graph = asystem +
  fixes rlist and succ_list
  assumes rl_distinct: "distinct rlist"
  assumes rl_reachable: "E⇧* `` V0 ⊆ set rlist"
  assumes rl_closed: "⋀c c'. ⟦c∈set rlist; (c, c') ∈ step⟧ ⟹ c'∈set rlist"
  assumes sl_distinct: "c∈set rlist ⟹ distinct (succ_list c)"
  assumes sl_succs: "set (succ_list c) = {(a,c'). astep c a c'}"
begin
  definition "succs_tab ≡ map succ_list rlist"

  lemma astep_succs_tab_conv:
    assumes R: "c∈set rlist"
    shows "astep c a c' ⟷ (∃i<length succs_tab. c=rlist!i ∧ (a,c')∈set (succs_tab!i))"
  proof -
    from R obtain i where "i<length rlist" and RLI[simp]: "rlist!i=c"
      by (auto simp: in_set_conv_nth)
    hence 1: "i<length succs_tab" "succs_tab!i=succ_list c"
      unfolding succs_tab_def
      by auto

    have AUX: "⋀j. ⟦c = rlist!j; j<length succs_tab⟧ ⟹ i=j" 
    proof -
      fix j
      assume "c = rlist!j" "j<length succs_tab"
      hence "rlist!j=rlist!i" "j<length rlist" by (simp_all add: succs_tab_def)
      with nth_eq_iff_index_eq[OF rl_distinct ‹i<length rlist› ‹j<length rlist›]  
      show "i=j" by simp
    qed

    from 1 show ?thesis using sl_succs 
      by (auto dest: AUX)
  qed

  lemma succs_tab_invar: "i<length succs_tab ⟹ distinct (succs_tab!i)"
    unfolding succs_tab_def 
    using rl_reachable sl_distinct
    by auto

  lemma succs_tab_rl: "⟦i<length rlist; (a,c')∈set (succs_tab!i)⟧ 
    ⟹ c' ∈ set rlist"
    unfolding succs_tab_def
    apply (simp add: sl_succs)
    apply (rule rl_closed[rotated])
    unfolding step_def
    apply blast
    apply simp
    done

  definition "mapped_succs_tab ≡ IArray (
    map (map (λ(a,c'). (a,the (cr_index_of rlist c')))) succs_tab)"

  lemma [simp]: 
    "IArray.length mapped_succs_tab = length succs_tab"  
    "length succs_tab = length rlist"
    unfolding mapped_succs_tab_def succs_tab_def by auto

  definition "γ c ≡ the (cr_index_of rlist c)"
  definition "α i ≡ rlist!i"
  definition "succ_impl ci ≡ 
    if ci<IArray.length mapped_succs_tab then 
      mapped_succs_tab!!ci
    else []"
  definition "astep_impl c a c' ≡ (a,c')∈set (succ_impl c)"

  lemma astep_succ_finite[simp, intro!]: 
    "finite {(a,c'). astep_impl c a c'}"
    unfolding astep_impl_def
    by auto

  lemma astep_succ_finite_c[simp, intro!]:
    "finite ({c'. ∃a. astep_impl c a c'})"
  proof -
    have "{c'. ∃a. astep_impl c a c'} = snd`{(a,c'). astep_impl c a c'}"
      by auto
    also have "finite …" by auto
    finally show ?thesis .
  qed  

  lemma α_inj: "inj_on α {0..<length rlist}"
    by (auto intro!: inj_onI simp: α_def nth_eq_iff_index_eq[OF rl_distinct])

  lemma γ_inj: "inj_on γ (set rlist)"
    using rl_reachable
    apply (auto intro!: inj_onI 
      simp: γ_def rl_distinct 
      cr_index_of_eq)
    by (metis index_of_None_conv index_of_Some_conv not_None_eq 
      option.sel rl_distinct)
    
  lemma γ_α_inverse: "i<length rlist ⟹ γ (α i) = i"  
    unfolding α_def γ_def
    apply (auto simp: cr_index_of_eq[OF rl_distinct])
    apply (cases "index_of rlist (rlist ! i)", simp_all)
    apply (auto simp: index_of_None_conv index_of_Some_conv[OF rl_distinct]
      simp: nth_eq_iff_index_eq[OF rl_distinct])
    done
    
  lemma α_γ_inverse: "c∈set rlist ⟹ α (γ c) = c"  
    unfolding α_def γ_def
    apply (auto simp: cr_index_of_eq[OF rl_distinct])
    apply (cases "index_of rlist c", simp_all)
    apply (auto simp: index_of_None_conv index_of_Some_conv[OF rl_distinct]
      simp: nth_eq_iff_index_eq[OF rl_distinct])
    done

  lemma γ_invar: "c∈set rlist ⟹ γ c < length rlist"
    apply (auto simp: γ_def cr_index_of_eq rl_distinct)
    by (metis index_of_None_conv index_of_Some_conv 
      not_None_eq option.sel rl_distinct)

  lemma α_invar: "i<length rlist ⟹ α i ∈ set rlist"
    unfolding α_def by simp  

  definition "invar i ≡ i<length rlist"    
  definition "rel ≡ brp α invar"  
  definition "reli ≡ brp γ (λx. x∈set rlist)"  

  lemma bi_unique_rel: "bi_unique rel"
    apply (intro bi_uniqueI left_uniqueI right_uniqueI)
    by (auto simp: rel_def build_relp_def invar_def
      inj_onD[OF α_inj])

  lemma bi_unique_reli: "bi_unique reli"
    apply (intro bi_uniqueI left_uniqueI right_uniqueI)
    by (auto simp: reli_def build_relp_def 
      inj_onD[OF γ_inj])

  lemma rel_inv_eq_reli: "rel¯¯ = reli"
    by (auto 
      intro!: ext 
      simp: rel_def reli_def build_relp_def invar_def
      simp: γ_α_inverse α_γ_inverse γ_invar α_invar
      )

  corollary reli_inv_eq_rel: "reli¯¯ = rel"
    using arg_cong[where f="λr. r¯¯", OF rel_inv_eq_reli, simplified]
    by simp

  lemma rel_unfold1: "c∈set rlist ⟹ rel i c ⟷ i = γ c"  
    unfolding reli_inv_eq_rel[symmetric]
    by (simp add: reli_def build_relp_def)

  lemma is_reachable_criE:
    assumes R: "c ∈ E⇧* `` V0"
    obtains i where "cr_index_of rlist c = Some i"
  proof -
    from R have IS: "c∈set rlist" using rl_reachable by auto

    show ?thesis
      using IS
      by (auto 
        simp: cr_index_of_eq[OF rl_distinct] index_of_Some_conv[OF rl_distinct]
        simp: in_set_conv_nth
        intro: that)
  qed

  lemma sim1i: "⟦ astep c1 a c2; reli c1 c1' ⟧ ⟹ ∃c2'. reli c2 c2' ∧ astep_impl c1' a c2'"
    apply (auto simp: reli_def build_relp_def)
    apply (rule rl_closed, auto simp: step_def) []
  proof -
    assume R: "c1∈set rlist" and S: "astep c1 a c2"
    then obtain i where L: "i<length succs_tab" 
      and C1: "c1=rlist!i" and AC': "(a,c2)∈set (succs_tab!i)"
      by (auto simp: astep_succs_tab_conv)

    have [simp]: "i<length rlist" using L by simp  
    note [simp] = L

    from C1 have [simp]: "γ c1 = i"  
      unfolding γ_def
      apply (cases "cr_index_of rlist c1")
      apply simp_all
      apply (auto simp: cr_index_of_eq[OF rl_distinct] 
        index_of_Some_conv[OF rl_distinct] index_of_None_conv 
        nth_eq_iff_index_eq[OF rl_distinct])        
      done

    show "astep_impl (γ c1) a (γ c2)" 
      using AC'
      apply (auto simp: astep_impl_def succ_impl_def mapped_succs_tab_def)
      apply (auto simp: γ_def)
      done
  qed

  lemma sim2i: "⟦ astep_impl c1' a c2'; reli c1 c1' ⟧ ⟹ ∃c2. reli c2 c2' ∧ astep c1 a c2"
  proof -
    assume "reli c1 c1'"
    hence R: "c1∈set rlist" and [simp]: "c1'=γ c1" 
      by (auto simp: reli_def build_relp_def)
    
    hence [simp]: "γ c1 < length rlist"
      unfolding γ_def using rl_reachable
      apply (cases "cr_index_of rlist c1", simp_all)
      apply (auto simp: α_def cr_index_of_eq[OF rl_distinct] 
        index_of_None_conv index_of_Some_conv[OF rl_distinct])
      done

    have [simp]: "rlist!γ c1 = c1"
      unfolding α_def[symmetric]
      by (simp add: α_γ_inverse R)

    assume "astep_impl c1' a c2'"
    then obtain c2 where "(a, c2) ∈ set (succs_tab ! γ c1)" and [simp]: "c2' = γ c2"
      apply (auto simp: astep_impl_def succ_impl_def mapped_succs_tab_def)
      apply (auto simp: γ_def)
      done
    with astep_succs_tab_conv[THEN iffD2, OF R, OF exI, of c1' a c2]
      have "astep c1 a c2" by auto
     moreover hence "c2∈set rlist" 
      using rl_closed[OF R, of c2] by (auto simp: step_def)
    hence "reli c2 c2'"
      by (auto simp: reli_def build_relp_def)
    ultimately show "∃c2. reli c2 c2' ∧ astep c1 a c2" by blast  
  qed    

  corollary sim1: "⟦ astep_impl c1' a c2'; rel c1' c1 ⟧ ⟹ ∃c2. rel c2' c2 ∧ astep c1 a c2"
    using sim2i unfolding reli_inv_eq_rel[symmetric] by simp

  corollary sim2: "⟦ astep c1 a c2; rel c1' c1 ⟧ ⟹ ∃c2'. rel c2' c2 ∧ astep_impl c1' a c2'"
    using sim1i unfolding reli_inv_eq_rel[symmetric] by simp


  lemma succ_impl_invar: "distinct (succ_impl ci)"
    unfolding succ_impl_def mapped_succs_tab_def invar_def
    using succs_tab_invar[of ci]
    apply (clarsimp simp: distinct_map)
    apply (fold γ_def)
    apply (rule inj_onI)
    apply clarsimp (* TODO: This proof is not particular clean *)
    apply (drule (1) succs_tab_rl[rotated])
    apply (drule (1) succs_tab_rl[rotated])
    by (metis α_γ_inverse local.α_def)
    
  lemma succ_impl_invarc: "⟦invar c; (a,c')∈set (succ_impl c)⟧ ⟹ invar c'"
    unfolding succ_impl_def mapped_succs_tab_def invar_def
    apply (clarsimp)
    by (metis γ_def γ_invar succs_tab_rl)
        
  lemma astep_impl_invarc: "⟦invar c; astep_impl c a c'⟧ ⟹ invar c'"  
    unfolding astep_impl_def
    by (auto intro: succ_impl_invarc)

end

lemma path'_path_conv:
  "li'.cs.path c p c' ⟷ cfg_lts.path c (map Inl p) c'"
  by (induction p arbitrary: c) (auto simp: cfg'_def)

lemma approx_reachable_approx': "li'.cs.reachable c c' ⟹ c' ∈ approx_reachable c"
  using approx_reachable_approx[of c c']
  by (auto simp: LTS.reachable_def path'_path_conv)

(* TODO: Move *)
lemma approx_reachable_closed':
  assumes "c∈approx_reachable c0"
  assumes "cfg' c a c'"
  shows "c'∈approx_reachable c0"
  using assms
  unfolding cfg'_def
  using approx_reachable_closed
  by blast

type_synonym cmdc = nat
type_synonym local_config = "(cmdc, local_state) Gen_Scheduler.local_config"
type_synonym global_config = "(cmdc, local_state, global_state) Gen_Scheduler.global_config"

locale cprog = 
  fixes prog :: program
begin
  sublocale comp: asystem "λx. x∈cfg_V0 prog" cfg' .

  sublocale comp: sl_graph 
    "λx. x∈cfg_V0 prog" cfg' 
    "approx_reachable_list prog" "cfg'_succ_list" 
  apply unfold_locales
  apply (simp_all 
    add: approx_reachable_list_invar approx_reachable_list_refine
    add: cfg'_succ_list_invar cfg'_succ_list_refine
    add: approx_reachable_prog_def 
    ) 
  using approx_reachable_approx'
  apply (auto simp: comp.step_path_conv LTS.reachable_def) []

  using approx_reachable_closed' unfolding comp.step_def
  by blast

  abbreviation "cfgc ≡ comp.astep_impl"

  definition init_pc :: "proc_decl ⇒ local_config" where
    "init_pc pd ≡ ⦇
      local_config.command = comp.γ (proc_decl.body pd),
      local_config.state = ⦇
        local_state.variables = init_valuation (proc_decl.local_vars pd)
      ⦈
    ⦈"
  
  definition init_gc :: "global_config" where
    "init_gc ≡ ⦇
      global_config.processes = mset (map init_pc (program.processes prog)),
      global_config.state = ⦇
        global_state.variables = init_valuation (program.global_vars prog)
      ⦈
    ⦈"


  sublocale lih': Gen_Scheduler'_linit 
    cfgc la_en' la_ex' 
    "{init_gc}" global_config.state .

  sublocale hc_bisim: Gen_Cfg_Bisim_Pre comp.rel
    cfgc cfg' la_en' la_ex'
    apply unfold_locales
    apply (blast dest: comp.sim1)
    apply (blast dest: comp.sim2)
    done

  lemma approx_reachable_prog0: "p ∈ set (program.processes prog) ⟹
         body p ∈ approx_reachable_prog prog"  
    unfolding approx_reachable_prog_def
    by (auto simp: cfg_V0_def intro!: bexI)


  sublocale hc_bisim: Gen_Cfg_LBisim comp.rel
    cfgc "{init_gc}" global_config.state
    cfg' "{SM_Semantics.init_gc prog}" global_config.state la_en' la_ex'
    apply unfold_locales
    apply (auto 
      simp: init_gc_def SM_Semantics.init_gc_def 
      simp: init_pc_def SM_Semantics.init_pc_def 
      simp: hc_bisim.rel_gc_def hc_bisim.rel_lc_def
      simp del: mset_map simp: mset_map[symmetric]
      intro!: rel_mset_of_mapI)

    apply (subst comp.rel_unfold1)
    apply (unfold approx_reachable_list_refine)
    apply (simp add: approx_reachable_prog0)
    apply simp

    apply (subst comp.rel_unfold1)
    apply (unfold approx_reachable_list_refine)
    apply (simp add: approx_reachable_prog0)
    apply simp
    done
    
  lemma lih'_accept_eq_li': "lih'.sa.accept = li'.sa.accept prog"  
    by (rule hc_bisim.accept_bisim)


  definition "lc_α lc ≡ ⦇
    local_config.command = comp.α (local_config.command lc),
    local_config.state = local_config.state lc
  ⦈"
  definition "lc_invar lc ≡ comp.invar (local_config.command lc)"

  lemma hc_bisim_rel_lc_brp_conv: "hc_bisim.rel_lc = brp lc_α lc_invar"
    apply (intro ext)
    unfolding hc_bisim.rel_lc_def 
    unfolding comp.rel_def lc_α_def lc_invar_def build_relp_def
    by auto
    
  definition "gc_α gc ≡ ⦇
    global_config.processes = image_mset lc_α (global_config.processes gc),
    global_config.state = global_config.state gc
  ⦈"
  definition "gc_invar gc ≡ ∀lc. lc ∈# global_config.processes gc ⟶ lc_invar lc"

  lemma hc_bisim_rel_gc_brp_conv: "hc_bisim.rel_gc = brp gc_α gc_invar"
    apply (intro ext)
    unfolding hc_bisim.rel_gc_def hc_bisim_rel_lc_brp_conv
    unfolding comp.rel_def gc_α_def gc_invar_def
    apply (auto simp: rel_mset_brp)
    apply (auto simp: build_relp_def)
    done

  lemmas bi_unique_rel_gc = hc_bisim.bi_unique_rel_gcI[OF comp.bi_unique_rel] 
  lemmas bi_unique_rel_lc = hc_bisim.bi_unique_rel_lcI[OF comp.bi_unique_rel] 

  lemma run_sim_lih'_li: "lih'.sa.is_run r ⟹ li'.sa.is_run prog (gc_α o r)"
    apply (rule hc_bisim.s1.br_run_sim)
    unfolding hc_bisim_rel_gc_brp_conv
    by auto

  lemmas lih'_reachable_finite_sim = hc_bisim.s1.reachable_finite_sim

end

context well_typed_prog begin 
  sublocale cprog .

  lemma lih'_accept_eq: "lih'.sa.accept = ref_accept prog"  
    by (simp add: lih'_accept_eq_li' li'.accept_eq)

  lemma lih'_is_run_sim: "lih'.sa.is_run r ⟹ ref_is_run prog (Some o gc_α o r)"
    apply (drule run_sim_lih'_li)
    unfolding li'.is_run_conv 
    by (auto simp: o_def)

  lemma lih'_finite_reachable: "finite ((g_E lih'.system_automaton)⇧* `` g_V0 lih'.system_automaton)"
    apply (rule lih'_reachable_finite_sim)
    apply (rule li'_finite_reachable)
    unfolding rel_of_pred_def
    apply simp
    apply (rule left_unique_finite_sngI)
    using bi_unique_rel_gc
    apply (simp add: bi_unique_alt_def)
    done
  
end

(* Executable *)
type_synonym comp_info = "(cmd list × (action × nat) list iarray)"
(* TODO: Using a list is slow. Could use a hashmap to map commands to
  their indices *)

definition comp_info_of :: "program ⇒ comp_info" where
  "comp_info_of prog ≡ let
  rlist = approx_reachable_list prog;
  succs_tab = map cfg'_succ_list rlist;
  mapped_succs_tab = IArray (
    map (map (λ(a,c'). (a,the (cr_index_of rlist c')))) succs_tab)
in
  (rlist,mapped_succs_tab)"

definition ccfg_succ_impl 
  :: "comp_info ⇒ nat ⇒ (action × nat) list"
where
  "ccfg_succ_impl cinf c ≡ 
    let mst=snd cinf in 
      if c<IArray.length mst then mst!!c else []"

lemma (in cprog) ccfg_succ_impl: 
  "ccfg_succ_impl (comp_info_of prog) = comp.succ_impl"
  apply (intro ext)
  unfolding comp.succ_impl_def comp.mapped_succs_tab_def comp.succs_tab_def
  unfolding ccfg_succ_impl_def comp_info_of_def
  by simp

definition comp_γ_impl :: "comp_info ⇒ cmd ⇒ cmdc" where
  "comp_γ_impl cinf c ≡ the (cr_index_of (fst cinf) c)"

lemma (in cprog) comp_γ_impl: "comp_γ_impl (comp_info_of prog) = comp.γ"
  apply (intro ext)
  unfolding comp.γ_def
  unfolding comp_γ_impl_def comp_info_of_def
  by simp
  

export_code comp_info_of ccfg_succ_impl comp_γ_impl checking SML


end