Theory SM.SM_Ample_Impl

theory SM_Ample_Impl
imports SM_Datastructures "../Analysis/SM_POR"
  "HOL-Library.RBT_Mapping"
begin

  text ‹
    Given a sticky program, we implement
    a valid ample-function by picking the transitions from the first
    PID that qualifies as an ample-set›
  context visible_prog
  begin
    definition ga_gample
      :: "(cmdc×cmdc) set  pid_global_config  global_action set" 
    where
      "ga_gample sticky_E gc  let
        lcs = pid_global_config.processes gc;
        gs = pid_global_config.state gc;
        as = find_min_idx_f (λlc.
          let
            c = local_config.command lc;
            ls = local_config.state lc;
            as = set (comp.succ_impl c)
          in
            if ((a,_)as. read_globals a = {}  write_globals a = {}) then
              let 
                as = {(a,c')as. la_en' (ls,gs) a}
              in
                if as={}  ((a,c')as. (c,c')sticky_E) then 
                  None 
                else 
                  Some (c,as)
            else
              None
        ) lcs
      in
        case as of
          Some (pid,c,as)  (λ(a,c'). (pid,c,a,c'))`as
        | None  ga_gen gc"
    
    definition "ga_ample sticky_E 
       stutter_extend_en (ga_gample sticky_E)"

    lemma ga_gample_subset: "ga_gample sticky_E gc  ga_gen gc"
      unfolding ga_gample_def ga_gen_def
      by (auto 
        simp: comp.astep_impl_def
        split: option.splits if_split_asm 
        dest!: find_min_idx_f_SomeD)

    lemma ga_gample_empty_iff: "ga_gample sticky_E gc = {}  ga_gen gc = {}"  
      unfolding ga_gample_def ga_gen_def
      by (fastforce 
        simp: comp.astep_impl_def
        split: option.splits if_split_asm 
        dest!: find_min_idx_f_SomeD)

    lemma ga_ample_None_iff: "None  ga_ample sticky_E gc  None  ga_en gc"
      by (auto 
        simp: ga_ample_def ga_en_def stutter_extend_en_def ga_gample_empty_iff)
      
    lemma ga_ample_neq_en_eq:
      assumes "ga_ample sticky_E gc  ga_en gc"
      shows "ga_ample sticky_E gc = Some`ga_gample sticky_E gc  ga_en gc = Some`ga_gen gc"
      using assms ga_gample_subset
      unfolding ga_ample_def ga_en_def stutter_extend_en_def
      by (auto split: if_split_asm simp: ga_gample_empty_iff)

    lemma pid_pac_alt: "pid_pac pid = insert None (Some`{(pid',cac). pid'=pid})" 
      apply (auto simp: pid_pac_def split: option.splits)
      apply (case_tac x)
      apply auto
      done
  end    

  context sticky_prog begin
    sublocale ample_prog prog is_vis_var sticky_E "ga_ample sticky_E"
    proof -
      have aux: "Some ` A = Some ` B  pid_pac pid  A = {(pid', cac). (pid', cac)  B  pid' = pid}"
        for A B pid
      proof
        assume 1: "Some ` A = Some ` B  pid_pac pid"
        show "A = {(pid', cac). (pid', cac)  B  pid' = pid}"
          using 1
          apply (auto simp: pid_pac_alt)
          unfolding image_def
          apply auto
          using 1 by blast
      next
        show "Some ` A = Some ` B  pid_pac pid" if "A = {(pid', cac). (pid', cac)  B  pid' = pid}"
          using that by (auto simp: pid_pac_alt)
      qed
      show "ample_prog prog is_vis_var sticky_E (ga_ample sticky_E)"
        apply unfold_locales
        apply (frule ga_ample_neq_en_eq, clarsimp)
        apply (intro conjI)
        apply (auto 
          simp: ga_gample_def sticky_ga_def
          dest!: find_min_idx_f_SomeD
          split: option.splits if_split_asm) []
        apply (fastforce
          simp: ga_gample_def sticky_ga_def
          dest!: find_min_idx_f_SomeD
          split: option.splits if_split_asm) []
        unfolding aux (* TODO: Clean up! *)
        apply (simp add: inj_image_eq_iff pid_pac_def)
        apply (thin_tac "ga_ample c a = b" for a b c)
        apply (simp add: ga_gample_def split: option.splits prod.splits)
        apply (thin_tac "a  ga_gen b" for a b)
        apply (drule find_min_idx_f_SomeD)
        apply clarsimp
        apply (rename_tac gc pid c as)
        apply (rule_tac x=pid in exI)
        apply (auto 
          split: if_split_asm prod.splits 
          simp: ga_gen_def comp.astep_impl_def)
        unfolding is_ample_static_def comp.astep_impl_def
        apply force
        done
    qed

  end

  text ‹ The following locale expresses a correct ample-reduction on 
    the level of subset and stuttering-equivalences of traces ›

  locale hl_reduction =
    visible_prog +
    ample: sa " g_V = UNIV, g_E = step, g_V0 = {pid_init_gc}, sa_L = pid_interp_gc "
    for step +
    assumes ample_accept_subset: "ample.accept w  lv.sa.accept w"
    assumes ample_accept_stuttering: "lv.sa.accept w  w'. ww'  ample.accept w'"

  locale hl_ample_reduction =
    visible_prog +
    ample: sa " g_V = UNIV, g_E = rel_of_enex (ample, ga_ex), g_V0 = {pid_init_gc},
      sa_L = pid_interp_gc "
    for ample +
    assumes ample_accept_subset: "ample.accept w  lv.sa.accept w"
    assumes ample_accept_stuttering: "lv.sa.accept w  w'. ww'  ample.accept w'"
  begin
    sublocale hl_reduction prog is_vis_var "rel_of_enex (ample, ga_ex)"
      apply unfold_locales
      using ample_accept_subset ample_accept_stuttering by auto
  end


  context sticky_prog
  begin
    sublocale hl_ample: hl_ample_reduction prog is_vis_var "ga_ample sticky_E"
      apply unfold_locales
      unfolding ample_rel_def[symmetric]
      unfolding reduced_automaton_def[symmetric]
      apply simp
      apply simp
      using ample_accept_subset
      apply simp
      apply (erule ample_accept_stuttering)
      apply blast
      done
  end    

  text ‹Next, we implement the selection of a set of sticky edges›
  context visible_prog begin
    definition "cr_ample  do {
      sticky_E  find_fas_init cfgc_G vis_edges;
      RETURN (ga_ample (sticky_E))
    }"

    lemma cr_ample_reduction: 
      "cr_ample  SPEC (hl_ample_reduction prog is_vis_var)"
      unfolding cr_ample_def
      apply (refine_vcg order_trans[OF find_fas_init_correct])
      apply unfold_locales[]
      apply simp
    proof clarify  
      fix sticky_E
      assume "is_fas cfgc_G sticky_E" "vis_edges  sticky_E"
      then interpret sticky_prog prog is_vis_var sticky_E
        by unfold_locales

      show "hl_ample_reduction prog is_vis_var (ga_ample sticky_E)" by unfold_locales
    qed
  end  

  text ‹We derive an implementation for finding the feedback arcs,
    and an efficient implementation for ga_gample.›

  text ‹We replace finding the sticky edges by an efficient algorithm›

  context visible_prog begin
    definition ga_gample_m 
      :: "_  _  pid_global_config  global_action set" 
    where
      "ga_gample_m mem sticky_E gc  let
        lcs = pid_global_config.processes gc;
        gs = pid_global_config.state gc;
        as = find_min_idx_f (λlc.
          let
            c = local_config.command lc;
            ls = local_config.state lc;
            as = set (comp.succ_impl c)
          in
            if ((a,_)as. read_globals a = {}  write_globals a = {}) then
              let 
                as = {(a,c')as. la_en' (ls,gs) a}
              in
                if as={}  ((a,c')as. mem (c,c') sticky_E) then 
                  None 
                else 
                  Some (c,as)
            else
              None
        ) lcs
      in
        case as of
          Some (pid,c,as)  (λ(a,c'). (pid,c,a,c'))`as
        | None  ga_gen gc"

    lemma ga_gample_m_refine:
      fixes Rs :: "('si×'s) set"
      shows "(ga_gample_m, ga_gample_m)  (Id×rId  Rs  bool_rel)  Rs  Id  Idset_rel"
    proof (intro fun_relI, simp)  
      fix m :: "cmdc×cmdc  's  bool" and m' :: "cmdc×cmdc  'si  bool" 
        and se se' gc
      assume "(m',m)Id  Rs  bool_rel" and "(se',se)Rs"
      hence "c c'. (m' (c,c') se', m (c,c') se)Id" 
        by parametricity simp_all
      hence A: "c c'. m' (c,c') se' = m (c,c') se" by simp
      show "ga_gample_m m' se' gc = ga_gample_m m se gc"
        unfolding ga_gample_m_def
        by (subst A) (rule refl)
    qed             

    lemma ga_gample_eq_gample_m: "ga_gample = ga_gample_m (∈)"
      unfolding ga_gample_def[abs_def] ga_gample_m_def[abs_def]
      by auto

    lemma stutter_extend_en_refine: 
      "(stutter_extend_en, stutter_extend_en)  (R  Idset_rel)  R  Idoption_relset_rel"
      unfolding stutter_extend_en_def[abs_def]
      apply parametricity
      by auto

    lemma is_vis_var_refine: "(is_vis_var, is_vis_var)  Id  bool_rel" by simp  

    lemma vis_edges_refine: "(λx. xvis_edges,vis_edges)Id×rIdfun_set_rel"
      by (simp add: fun_set_rel_def br_def)

    lemma [autoref_op_pat_def]: 
      "vis_edges  Autoref_Tagging.OP vis_edges"  
      "ga_gample_m  Autoref_Tagging.OP ga_gample_m"  
      "cfgc_G  Autoref_Tagging.OP cfgc_G"
      by simp_all

    schematic_goal cr_ample_impl1_aux:
      notes [autoref_rules] = 
        ga_gample_m_refine stutter_extend_en_refine is_vis_var_refine
        cfgc_G_impl_refine
        vis_edges_refine IdI[of prog]
      shows "(RETURN (?c::?'c),cr_ample)?R"
      unfolding cr_ample_def ga_ample_def ga_gample_eq_gample_m
      using [[autoref_trace_failed_id, autoref_trace_intf_unif]]
      by (autoref_monadic (plain, trace))
    concrete_definition cr_ample_impl1 uses cr_ample_impl1_aux

    lemma cr_ample_impl1_reduction: 
      "hl_ample_reduction prog is_vis_var cr_ample_impl1"
    proof -
      note cr_ample_impl1.refine[THEN nres_relD]
      also note cr_ample_reduction
      finally show ?thesis by simp
    qed

  end

  text ‹The efficient implementation of @{const visible_prog.ga_gample} uses 
    the @{const collecti_index} function› 

  lemma collecti_index_cong:
    assumes C: "i. i<length l  f i (l!i) = f' i (l'!i)"
    assumes [simp]: "l=l'"
    shows "collecti_index f l = collecti_index f' l'"
  proof -
    {
      fix i0 s0
      assume "i<length l. f (i0+i) (l!i) = f' (i0+i) (l!i)"
      hence "collecti_index' i0 s0 f l = collecti_index' i0 s0 f' l"
      proof (induction l arbitrary: i0 s0)
        case (Cons a l)

        from Cons.prems[THEN spec, of 0] have 
          [simp]: "f i0 a = f' i0 a" by simp

        from Cons.prems have 
          IHP: "i<length l. f (Suc i0+i) (l!i) = f' (Suc i0+i) (l!i)"
          by auto

        show ?case by (auto split: bool.splits simp: Cons.IH[OF IHP])
      qed simp
    } from this[of 0 "{}"] show ?thesis using assms by simp
  qed  

  lemma find_min_idx_f_cong:
    assumes "x. xset l  f x = f' x"
    assumes "l=l'"
    shows "find_min_idx_f f l = find_min_idx_f f' l'"
    unfolding assms(2)[symmetric]
    using assms(1)
    apply (induction l)
    apply (auto split: option.split)
    done


  lemma find_min_idx_impl_collecti: "(
      case find_min_idx_f f l of
        Some (i,r)  {i} × s1 i r
      | None  {(i,r) | i r. i<length l  rs2 i (l!i)}  
    )
  = (
    collecti_index (λi x. 
      case f x of
        Some r  (True, s1 i r)
      | None  (False, s2 i x)
    ) l
  )" (is "?l=?r" is "_ = collecti_index ?fc l") 
  proof (cases "i<length l. f (l!i)  None")
    define i where "i  LEAST i. i < length l  f (l ! i)  None"
    
    have C_ALT: "(i<length l. f (l!i)  None) 
       (i. i < length l  fst (?fc i (l ! i)))"
      by (auto split: option.split)

    have i_alt: "i = (LEAST i. i < length l  fst (?fc i (l ! i)))" 
      unfolding i_def 
      apply (fo_rule arg_cong)
      by (auto split: option.split)

    {  
      case True
  
      from LeastI_ex[OF True] obtain r where [simp]: "i<length l" "f (l!i) = Some r"
        by (auto simp: i_def)
  
      from True find_min_idx_f_LEAST_eq[of f l] 
        have "find_min_idx_f f l = Some (i, the (f (l ! i)))" 
        by (simp add: i_def)
      hence LEQ: "?l = {i} × s1 i r" by simp

      from collecti_index_collect[of ?fc l, folded i_alt] True C_ALT have 
        REQ: "?r = {i} × snd (?fc i (l!i))" 
        by simp
      show "?l=?r" unfolding LEQ unfolding REQ by auto
    }
    {
      case False
      from False find_min_idx_f_LEAST_eq[of f l] 
        have "find_min_idx_f f l = None" by simp
      hence LEQ: "?l = {(i,r) | i r. i<length l  rs2 i (l!i)}" by simp

      from False C_ALT collecti_index_collect[of ?fc l] have
        REQ: "?r = {(i, x) |i x. i < length l  x  snd (?fc i (l ! i))}"
        by auto

      show "?l=?r" unfolding LEQ unfolding REQ using False by auto
    }
  qed


  lemma find_min_idx_impl_collecti_scheme: 
    assumes "x. s11 x = (case x of (i,r)  {i} × iss i r)"
    assumes "s12 = {(i,r) | i r. i<length l  risn i (l!i)}"
    assumes "i. i<length l  f2 i (l!i) = (case f (l!i) of
        Some r  (True, iss i r)
      | None  (False, isn i (l!i)))"
    shows "(case find_min_idx_f f l of Some x  s11 x | None  s12)
      = (collecti_index f2 l)"
    apply (simp only: assms(1,2,3) cong: collecti_index_cong)  
    apply (subst find_min_idx_impl_collecti)
    apply simp
    done


  schematic_goal stutter_extend_en_list_aux: "(?c, stutter_extend_en) 
     (R  Slist_set_rel)  R  Soption_rellist_set_rel"
    unfolding stutter_extend_en_def[abs_def]
    apply (autoref)
    done
  concrete_definition stutter_extend_en_list uses stutter_extend_en_list_aux

  lemma succ_of_enex_impl_aux: 
    "{s'. aen s. s'=ex a s} = (λa. ex a s)`en s" by auto

  schematic_goal succ_of_enex_list_aux: "(?c, succ_of_enex)  
    (Id  Idlist_set_rel) ×r (Id  Id  Id)  Id  Idlist_set_rel"
    unfolding succ_of_enex_def[abs_def]
    unfolding succ_of_enex_impl_aux
    by (autoref (trace, keep_goal))
  concrete_definition succ_of_enex_list uses succ_of_enex_list_aux

  schematic_goal pred_of_enex_list_aux: "(?c, pred_of_enex)  
    (Id  Idlist_set_rel) ×r (Id  Id  Id)  Id  Id  bool_rel"
    unfolding pred_of_enex_def[abs_def]
    by (autoref (trace, keep_goal))
  concrete_definition pred_of_enex_list uses pred_of_enex_list_aux

  (* TODO: can this be defined using autoref? *)
  definition "rel_of_enex_list enex  rel_of_pred (pred_of_enex_list enex)"
  lemma rel_of_enex_list_refine: "(rel_of_enex_list, rel_of_enex)  
    (Id  Idlist_set_rel) ×r (Id  Id  Id)  Id ×r Id set_rel"
  proof -
    have 1: "rel_of_enex_list = rel_of_pred  pred_of_enex_list" using rel_of_enex_list_def by force
    have 2: "rel_of_enex = rel_of_pred  pred_of_enex" by auto
    have 3: "(rel_of_pred, rel_of_pred)  (Id  Id  bool_rel)  Id ×r Idset_rel" by auto
    show ?thesis unfolding 1 2 by (parametricity add: 3 pred_of_enex_list.refine)
  qed

  context visible_prog begin
    definition "ga_gample_mi2 mem sticky_E (gc::pid_global_config) = (
      let 
        lcs = pid_global_config.processes gc;
        gs = pid_global_config.state gc
      in
        collecti_index (λ_ lc. let
            c = local_config.command lc;
            ls = local_config.state lc;
            as = set (comp.succ_impl c);
            s={(a,c')as. la_en' (ls,gs) a};
            ample = 
              s{} 
             ((a,_)as. read_globals a = {}  write_globals a = {}) 
             ((a,c')s. ¬ mem (c,c') sticky_E)
          in
            (ample,{c}×s)
        ) lcs
    )"

    lemma ga_gample_mi2_impl: 
      "ga_gample_m mem sticky_E gc = ga_gample_mi2 mem sticky_E gc"
      unfolding ga_gample_m_def ga_gample_mi2_def
      apply simp
      apply (rule find_min_idx_impl_collecti_scheme[where 
          iss="λpid (c,S). (λ(a,c'). (c,a,c'))`S" and
          isn="λpid lc. {(c,a,c'). cfgc c a c' 
             c = cmd_of_pid gc pid 
             la_en' (local_config.state lc, pid_global_config.state gc) a}"]
      )
      apply auto []
      unfolding ga_gen_def
      apply auto []
      apply (auto simp: comp.astep_impl_def)
      done

    definition "cr_ample_impl2 
      let sticky = find_fas_init_code (=) bounded_hashcode_nat
         (def_hashmap_size TYPE(nat)) cfgc_G_impl (λx. x  vis_edges)
      in stutter_extend_en (ga_gample_mi2 (λx f. f x) sticky)"

    definition "ample_step_impl2  rel_of_enex (cr_ample_impl2,ga_ex)"

    lemma cr_ample_impl2_reduction: 
      "hl_reduction prog is_vis_var ample_step_impl2"
    proof -
      from cr_ample_impl1_reduction 
      interpret hl_ample_reduction prog is_vis_var cr_ample_impl1 .
      
      have 1: "ample_step_impl2 = rel_of_enex (cr_ample_impl1, ga_ex)"
        unfolding ample_step_impl2_def cr_ample_impl1_def cr_ample_impl2_def
        unfolding ga_gample_mi2_impl[abs_def]
        by simp

      show ?thesis
        apply unfold_locales
        unfolding 1
        apply simp
        apply simp
        apply (blast intro: ample_accept_subset ample_accept_stuttering)+
        done
    qed
  end
        
text ‹Implementing the State›
type_synonym valuation_impl = "(ident,uint32) mapping"

definition "vi_α  map_option Rep_uint32 ∘∘ Mapping.rep"
abbreviation "vi_rel  br vi_α (λ_. True)"

abbreviation "val_rel  br Rep_uint32 (λ_. True)"

lemma vi_rel_rew: 
  "(x = vi_α y)  (y,x)vi_rel"
  "(vi_α y = x)  (y,x)vi_rel"
  by (auto simp: br_def)

export_code Mapping.lookup Mapping.update Mapping.empty checking SML

lift_definition vi_empty :: "valuation_impl" 
  is "Map.empty::valuation" .

lemma [code]: "vi_empty = Mapping.empty" by transfer simp
lemma vi_empty_correct: "vi_α vi_empty = Map.empty"
  unfolding vi_α_def
  by transfer auto

lift_definition vi_lookup :: "valuation_impl  ident  uint32" 
  is "λvi::valuation. λx. vi x" .
lemma [code]: "vi_lookup = Mapping.lookup"
  apply (intro ext)
  unfolding vi_lookup_def Mapping.lookup_def map_fun_def[abs_def] o_def
    id_apply option.map_comp Rep_uint32_inverse option.map_ident
  by simp

lemma vi_lookup_correct: "vi_lookup v x = map_option Abs_uint32 (vi_α v x)"
  unfolding vi_α_def
  apply transfer
  apply (simp add: option.map_comp o_def option.map_ident)
  done

lift_definition vi_update :: "ident  uint32  valuation_impl  valuation_impl" 
  is "λx v. λvi::valuation. vi(xv)" .
lemma [code]: "vi_update = Mapping.update"
  by transfer simp

lemma vi_update_correct: "vi_α (vi_update k v m) = (vi_α m) (kRep_uint32 v)"
  unfolding vi_α_def
  by transfer simp

export_code vi_lookup vi_update vi_empty checking SML 


record local_state_impl = 
  variables :: valuation_impl

record global_state_impl = 
  variables :: valuation_impl

type_synonym focused_state_impl = "local_state_impl × global_state_impl"

type_synonym local_config_impl 
  = "(cmdc,local_state_impl) Gen_Scheduler.local_config"
type_synonym pid_global_config_impl 
  = "(cmdc,local_state_impl,global_state_impl) Pid_Scheduler.pid_global_config"

definition "local_state_rel  {
  ( local_state_impl.variables = vi ,  local_state.variables = v  ) | vi v.
    v = vi_α vi 
  }"

definition "global_state_rel  {
  ( global_state_impl.variables = vi ,  global_state.variables = v  ) | vi v.
    v = vi_α vi 
  }"

abbreviation "focused_state_rel  local_state_rel ×r global_state_rel"

definition "local_config_rel  {
  ( local_config.command = ci, local_config.state=lsi , 
    local_config.command = c, local_config.state=ls  ) | ci c lsi ls.
    (ci::cmdc,c)Id  (lsi,ls)local_state_rel
  }"

definition "global_config_rel  {
  ( pid_global_config.processes = psi, pid_global_config.state = gsi ,
    pid_global_config.processes = ps, pid_global_config.state = gs ) | psi ps gsi gs.
   (psi,ps)local_config_rellist_rel  (gsi,gs)global_state_rel
}"

definition "init_valuation_impl vd  fold (λx v. vi_update x 0 v) vd (vi_empty)"

lemma init_valuation_impl: 
  "(init_valuation_impl, init_valuation)  Idlist_rel  vi_rel"
proof -
  {
    fix vd m
    have "m ++ init_valuation vd = fold (λx v. v(x0)) vd m"
      apply (rule sym)
      apply (induction vd arbitrary: m)
      unfolding init_valuation_def[abs_def]
      apply (auto intro!: ext simp: Map.map_add_def)
      done
  } note aux=this
  have E1: "vd. init_valuation vd = fold (λx v. v(x0)) vd Map.empty"
    by (subst aux[symmetric]) simp
    
  have E2: "vdi vd. (vdi,vd)Idlist_rel 
     (init_valuation_impl vdi, fold (λx v. v(x0)) vd Map.empty)  vi_rel"
    unfolding init_valuation_impl_def
    apply parametricity
    apply (auto simp: vi_update_correct vi_empty_correct br_def zero_uint32.rep_eq)
    done

  show ?thesis
    apply (intro fun_relI)
    apply (subst E1)
    apply (rule E2)
    by auto
qed

context cprog begin

  definition init_pc_impl :: "proc_decl  local_config_impl" where
    "init_pc_impl pd  
      local_config.command = comp.γ (proc_decl.body pd),
      local_config.state = 
        local_state_impl.variables = init_valuation_impl (proc_decl.local_vars pd)
      
    "

  lemma init_pc_impl: "(init_pc_impl, init_pc)  Id  local_config_rel"
    apply (rule fun_relI)
    unfolding init_pc_impl_def init_pc_def local_config_rel_def local_state_rel_def
    apply (simp del: pair_in_Id_conv, intro conjI)
    apply simp
    apply (simp only: vi_rel_rew)
    apply (parametricity add: init_valuation_impl)
    apply simp
    done
  
  definition pid_init_gc_impl :: "pid_global_config_impl" where
    "pid_init_gc_impl  
      pid_global_config.processes = (map init_pc_impl (program.processes prog)),
      pid_global_config.state = 
        global_state_impl.variables = init_valuation_impl (program.global_vars prog)
      
    "
  
  lemma pid_init_gc_impl: "(pid_init_gc_impl, pid_init_gc)  global_config_rel"
    unfolding pid_init_gc_impl_def pid_init_gc_def global_config_rel_def global_state_rel_def
    apply (simp del: pair_in_Id_conv, intro conjI)
    apply (parametricity add: init_pc_impl)
    apply simp
    apply (simp only: vi_rel_rew)
    apply (parametricity add: init_valuation_impl)
    apply simp
    done  

end
  
lift_definition val_of_bool_impl :: "bool  uint32" is val_of_bool .
lemma [code]: "val_of_bool_impl b = (if b then 1 else 0)"
  by transfer auto

lift_definition bool_of_val_impl :: "uint32  bool" is bool_of_val .
lemma [code]: "bool_of_val_impl v = (v0)"
  by transfer (auto simp: bool_of_val_def)

definition "set_of_rel R  {(a,b) . R b a}"
definition "rel_of_set S  λb a. (a,b)S"

lemma [simp]: 
  "(a,b)set_of_rel R  R b a"
  "rel_of_set S b a  (a,b)S"
  unfolding rel_of_set_def set_of_rel_def
  by auto

lemma [simp]:
  "set_of_rel (rel_of_set S) = S"
  "rel_of_set (set_of_rel R) = R"
  unfolding rel_of_set_def set_of_rel_def
  by auto

lemma rel_fun_2set: "rel_fun A B = rel_of_set (set_of_rel A  set_of_rel B)"
  unfolding rel_fun_def fun_rel_def
  unfolding rel_of_set_def set_of_rel_def
  by (auto)

lemma [simp]: 
  "set_of_rel cr_uint32 = val_rel"
  "set_of_rel (=) = Id"
  by (auto simp: br_def cr_uint32_def)

lemma bool_of_val_impl: "(bool_of_val_impl, bool_of_val)  val_rel  bool_rel"
  using bool_of_val_impl.transfer
  by (simp add: rel_fun_2set)
  

lemma smod_by_div_abs: "a smod b = a - a sdiv b * b" for a b :: 'a::len word
  by (subst (2) sdiv_smod_id [of a b, symmetric]) simp

lift_definition sdiv_impl :: "uint32  uint32  uint32" is "(sdiv)" .
lift_definition smod_impl :: "uint32  uint32  uint32" is "(smod)" .

(* TODO: Is there a more efficient way? *)
lemma [code]: "sdiv_impl x y = Abs_uint32' (Rep_uint32' x sdiv Rep_uint32' y)"
  apply transfer
  by simp

lemma [code]: "smod_impl a b = a - sdiv_impl a b * b"
  by transfer (simp add: smod_by_div_abs)

context
  includes bit_operations_syntax
begin

primrec eval_bin_op_impl_aux :: "bin_op  uint32  uint32  uint32" where
  "eval_bin_op_impl_aux bo_plus v1 v2 = v1+v2"
| "eval_bin_op_impl_aux bo_minus v1 v2 = v1-v2"
| "eval_bin_op_impl_aux bo_mul v1 v2 = v1*v2"
| "eval_bin_op_impl_aux bo_div v1 v2 = sdiv_impl v1 v2"
| "eval_bin_op_impl_aux bo_mod v1 v2 = smod_impl v1 v2"
| "eval_bin_op_impl_aux bo_less v1 v2 = val_of_bool_impl (v1 < v2)"
| "eval_bin_op_impl_aux bo_less_eq v1 v2 = val_of_bool_impl (v1  v2)"
| "eval_bin_op_impl_aux bo_eq v1 v2 = val_of_bool_impl (v1 = v2)"
| "eval_bin_op_impl_aux bo_and v1 v2 = v1 AND v2"
| "eval_bin_op_impl_aux bo_or v1 v2 = v1 OR v2"
| "eval_bin_op_impl_aux bo_xor v1 v2 = v1 XOR v2"

end

lift_definition eval_bin_op_impl :: "bin_op  uint32  uint32  uint32"
  is eval_bin_op .

lemma [code]: "eval_bin_op_impl bop v1 v2 = eval_bin_op_impl_aux bop v1 v2"
  apply (cases bop)
  apply (transfer; simp)+
  done

primrec eval_un_op_impl_aux :: "un_op  uint32  uint32" where
  "eval_un_op_impl_aux uo_minus v = -v"
| "eval_un_op_impl_aux uo_not v = Bit_Operations.not v"

lift_definition eval_un_op_impl :: "un_op  uint32  uint32"
  is eval_un_op .

lemma [code]: "eval_un_op_impl uop v = eval_un_op_impl_aux uop v"
  apply (cases uop)
  apply simp_all
  apply (transfer, simp)+
  done  




fun eval_exp_impl :: "exp  focused_state_impl  uint32" where
  "eval_exp_impl (e_var x) (ls,gs) = do {
    let lv = local_state_impl.variables ls; 
    let gv = global_state_impl.variables gs;
    case vi_lookup lv x of
      Some v  Some v
    | None  (case vi_lookup gv x of
        Some v  Some v
      | None  None)
  }"
| "eval_exp_impl (e_localvar x) (ls,gs) = vi_lookup (local_state_impl.variables ls) x"
| "eval_exp_impl (e_globalvar x) (ls,gs) = vi_lookup (global_state_impl.variables gs) x"
| "eval_exp_impl (e_const n) fs = do {
    assert_option (nmin_signed  nmax_signed);
    Some (uint32_of_int n)
  }"
| "eval_exp_impl (e_bin bop e1 e2) fs = do {
    v1eval_exp_impl e1 fs;
    v2eval_exp_impl e2 fs;
    Some (eval_bin_op_impl bop v1 v2)
    }"
| "eval_exp_impl (e_un uop e) fs = do {
    veval_exp_impl e fs;
    Some (eval_un_op_impl uop v)
    }"

(* TODO: Move *)
lemma map_option_bind: "map_option f (mg) = m  (map_option f o g)"
  by (auto split: Option.bind_split)

lemma val_option_rel_as_eq: "(a,b)val_reloption_rel  map_option Rep_uint32 a = b"
  unfolding br_def
  apply (cases a)
  apply (cases b, simp_all)
  apply (cases b, auto)
  done

lemma eval_exp_impl: "(eval_exp_impl, eval_exp)  Id  focused_state_rel  val_reloption_rel"
proof -
  {
    fix e ls gs lsi gsi
    assume "(lsi,ls)local_state_rel" "(gsi,gs)global_state_rel"
    hence "map_option Rep_uint32 (eval_exp_impl e (lsi,gsi)) = eval_exp e (ls,gs)"
      apply (induction e)
      apply (auto 
        simp: local_state_rel_def global_state_rel_def br_def
        simp: vi_lookup_correct vi_update_correct
        simp: Abs_uint32_inverse[simplified] uint32_of_int.rep_eq signed_of_int_def
        simp: option.map_comp option.map_ident o_def map_option_bind
        simp: eval_bin_op_impl.rep_eq eval_un_op_impl.rep_eq
        split: option.splits)
      apply (drule sym)
      apply (drule sym)
      apply (simp split: Option.bind_split)

      apply (drule sym)
      apply (simp split: Option.bind_split)
      done
  } thus ?thesis
    by (auto simp: val_option_rel_as_eq)
qed

text ‹Enabledness and effects of actions›
primrec la_en_impl :: "focused_state_impl  action  bool" where
  "la_en_impl fs (AAssign e _ _) = do {
    v  eval_exp_impl e fs;
    Some (bool_of_val_impl v)}"
| "la_en_impl fs (AAssign_local e _ _) = do {
    v  eval_exp_impl e fs;
    Some (bool_of_val_impl v)}"
| "la_en_impl fs (AAssign_global e _ _) = do {
    v  eval_exp_impl e fs;
    Some (bool_of_val_impl v)}"
| "la_en_impl fs (ATest e) = do {
    v  eval_exp_impl e fs;
    Some (bool_of_val_impl v)}"
| "la_en_impl _ (ASkip) = Some True"

lemma param_rec_action[param]: "(rec_action, rec_action)  (Id  Id  Id  A)
     (Id  Id  Id  A)
        (Id  Id  Id  A)  (Id  A)  A  Id  A"
  apply (intro fun_relI)
  subgoal for fi1 f1 fi2 f2 fi3 f3 fi4 f4 fi5 f5 ai a
    apply simp
    apply (induction a)
    apply simp_all
    apply (parametricity, simp_all?)+
    done
  done 

(* TODO: Move *)
lemma param_option_bind[param]:
  "(Option.bind, Option.bind)  Aoption_rel  (A  Boption_rel)  Boption_rel"
  unfolding Option.bind_def by parametricity

lemma la_en_impl: "(la_en_impl,la_en)  focused_state_rel  Id  Idoption_rel"
  unfolding la_en_impl_def la_en_def
  by (parametricity add: eval_exp_impl bool_of_val_impl)

definition "la_en'_impl fs a  case la_en_impl fs a of Some b  b | None  False"
  
lemma la_en'_impl: "(la_en'_impl,la_en')  focused_state_rel  Id  bool_rel"
  unfolding la_en'_impl_def[abs_def] la_en'_def[abs_def]
  by (parametricity add: la_en_impl)    

abbreviation "exists_var_impl v x  vi_lookup v x  None"

fun la_ex_impl :: "focused_state_impl  action  focused_state_impl" where
  "la_ex_impl (ls,gs) (AAssign ge x e) = do {
    v  eval_exp_impl ge (ls,gs);
    assert_option (bool_of_val_impl v); 
    v  eval_exp_impl e (ls,gs);
    if exists_var_impl (local_state_impl.variables ls) x then do {
      let ls = local_state_impl.variables_update (vi_update x v) ls;
      Some (ls,gs)
    } else do {
      assert_option (exists_var_impl (global_state_impl.variables gs) x);
      let gs = global_state_impl.variables_update (vi_update x v) gs;
      Some (ls,gs)
    }
  }"
| "la_ex_impl (ls,gs) (AAssign_local ge x e) = do {
    v  eval_exp_impl ge (ls,gs);
    assert_option (bool_of_val_impl v); 
    v  eval_exp_impl e (ls,gs);
    assert_option (exists_var_impl (local_state_impl.variables ls) x);
    let ls = local_state_impl.variables_update (vi_update x v) ls;
    Some (ls,gs)
  }"
| "la_ex_impl (ls,gs) (AAssign_global ge x e) = do {
    v  eval_exp_impl ge (ls,gs);
    assert_option (bool_of_val_impl v); 
    v  eval_exp_impl e (ls,gs);
    assert_option (exists_var_impl (global_state_impl.variables gs) x);
    let gs = global_state_impl.variables_update (vi_update x v) gs;
    Some (ls,gs)
  }"
| "la_ex_impl fs (ATest e) = do {
    v  eval_exp_impl e fs;
    assert_option (bool_of_val_impl v); 
    Some fs
  }"
| "la_ex_impl fs ASkip = Some fs"

(* TODO: Move *)
lemma param_assert_option[param]:
  "(assert_option, assert_option)  bool_rel  unit_reloption_rel"
  unfolding assert_option_def by parametricity


lemma la_ex_impl: "(la_ex_impl, la_ex) 
   focused_state_rel  Id  focused_state_reloption_rel"
proof (intro fun_relI)
  fix fsi fs and ai a :: action
  assume "(fsi,fs)focused_state_rel" "(ai,a)Id"
  thus "(la_ex_impl fsi ai, la_ex fs a)focused_state_reloption_rel"
    apply (cases fs, cases fsi, clarsimp)
    apply (cases a)
    apply simp_all
    apply (parametricity add: eval_exp_impl bool_of_val_impl)
    apply (auto 
      simp: local_state_rel_def global_state_rel_def
      simp: vi_lookup_correct vi_update_correct 
      simp: br_def 
      intro: domI) [7]
    apply (parametricity add: eval_exp_impl bool_of_val_impl)
    apply (auto 
      simp: local_state_rel_def global_state_rel_def
      simp: vi_lookup_correct vi_update_correct 
      br_def intro: domI) [9]
    apply (parametricity add: eval_exp_impl bool_of_val_impl)
    apply (auto 
      simp: local_state_rel_def global_state_rel_def
      simp: vi_lookup_correct vi_update_correct 
      br_def intro: domI) [4]
    apply (parametricity add: eval_exp_impl bool_of_val_impl)
    apply simp
    done
qed    

definition "la_ex'_impl fs a  case la_ex_impl fs a of Some fs'  fs' | None  fs"
lemma la_ex'_impl: "(la_ex'_impl,la_ex')  focused_state_rel  Id  focused_state_rel"
  unfolding la_ex'_impl_def[abs_def] la_ex'_def[abs_def]
  by (parametricity add: la_ex_impl)

lemma param_collecti_index: "(collecti_index, collecti_index)  
    (nat_rel  B  bool_rel ×r Idset_rel)  Blist_rel  nat_rel ×r Idset_rel"
  unfolding collecti_index'_def
  apply parametricity  
  apply auto
  done

export_code la_ex_impl la_en_impl checking SML

context visible_prog
begin

  definition "ga_gample_mi3 mem sticky_E (gc::pid_global_config_impl) = (
    let 
      lcs = pid_global_config.processes gc;
      gs = pid_global_config.state gc
    in
      collecti_index (λ_ lc. let
          c = local_config.command lc;
          ls = local_config.state lc;
          as = set (comp.succ_impl c);
          s={(a,c')as. la_en'_impl (ls,gs) a};
          ample = 
            s{} 
           ((a,_)as. read_globals a = {}  write_globals a = {}) 
           ((a,c')s. ¬ mem (c,c') sticky_E)
        in
          (ample,{c}×s)
      ) lcs
  )"

  lemma ga_gample_mi3_refine: 
    "(ga_gample_mi3, ga_gample_mi2) 
      Id  Id  global_config_rel  nat_rel ×r Idset_rel"
  proof -
    have [param]: "(comp.succ_impl,comp.succ_impl)IdId×rIdlist_rel"
      by simp

    from la_en'_impl have aux1: "fsi fs a. (fsi,fs)focused_state_rel 
      la_en'_impl fsi a = la_en' fs a"
      apply (rule_tac IdD)
      apply parametricity
      by auto

    show ?thesis
      using [[goals_limit=1]]
      apply (intro fun_relI)
      unfolding ga_gample_mi3_def ga_gample_mi2_def
      apply (parametricity add: param_collecti_index la_en'_impl)
      apply (auto simp add: global_config_rel_def local_config_rel_def) []
      apply (auto simp add: global_config_rel_def local_config_rel_def) []
      apply (auto simp add: global_config_rel_def local_config_rel_def) []
      apply (auto simp add: global_config_rel_def local_config_rel_def) []
      apply simp
      using aux1
      apply (auto simp add: global_config_rel_def local_config_rel_def) []
      apply simp_all
      done

  qed    

  definition (in cprog) "is_vis_edge is_vis_var  λ(c,c'). 
    (a,cc')set (comp.succ_impl c). c'=cc'  (vwrite_globals a. is_vis_var v)"

  lemma is_vis_edge_correct: "is_vis_edge is_vis_var = (λx. xvis_edges)"
    unfolding is_vis_edge_def vis_edges_def
    by (auto intro!: ext simp: comp.astep_impl_def)


  definition "cr_ample_impl3 
    let sticky = find_fas_init_code (=) bounded_hashcode_nat
         (def_hashmap_size TYPE(nat)) cfgc_G_impl (λx. x  vis_edges)
    in stutter_extend_en (ga_gample_mi3 (λx f. f x) sticky)"

    
  lemma cr_ample_impl3_refine: "(cr_ample_impl3, cr_ample_impl2) 
     global_config_rel  nat_rel×rIdoption_relset_rel"
  proof -
    have [param]: "R S. S=Id  
      (stutter_extend_en, stutter_extend_en)
         (R  Sset_rel)  R  Soption_relset_rel"
      apply (simp only: )
      by (rule stutter_extend_en_refine)
    
    show ?thesis  
      unfolding cr_ample_impl3_def cr_ample_impl2_def is_vis_edge_correct
      apply (parametricity add: stutter_extend_en_refine ga_gample_mi3_refine)
      apply (rule IdI)
      by auto
  qed      
      
(* TODO: The current Pid_Scheduler-locale is focused on refinement.
  We cannot use it to get an instantiation of ga_gex_impl.*)

  definition (in -) ga_gex_impl 
    :: "global_action  pid_global_config_impl  pid_global_config_impl"
  where
    "ga_gex_impl ga gc  let 
      (pid,c,a,c') = ga;
      fs = fs_of_pid gc pid;
      (ls',gs') = la_ex'_impl fs a;
      gc' =  
          pid_global_config.processes = (pid_global_config.processes gc)
            [pid := 
               local_config.command = c', local_config.state = ls'
            ],
          pid_global_config.state = gs'
    in
      gc'"


  lemma lc_of_pid_refine:
    assumes V: "pid_valid gc pid"    
    assumes [param]: "(pidi,pid)nat_rel"
    assumes GCI: "(gci,gc)global_config_rel"
    shows "(lc_of_pid gci pidi, lc_of_pid gc pid)local_config_rel"
    apply parametricity
    apply fact
    using GCI by (auto simp: global_config_rel_def)
    
  lemma ls_of_pid_refine:
    assumes "pid_valid gc pid"    
    assumes "(pidi,pid)nat_rel"
    assumes "(gci,gc)global_config_rel"
    shows "(ls_of_pid gci pidi, ls_of_pid gc pid)local_state_rel"
    using lc_of_pid_refine[OF assms] unfolding local_config_rel_def by auto


  lemma ga_gex_impl:
    assumes V: "pid_valid gc pid"    
    assumes [param]: "(pidi,pid)Id" "(ci,c)Id" 
      "(ai,a)Id" and CI'I: "(ci',c')Id" and GCI[param]: "(gci,gc)global_config_rel"
    shows "(ga_gex_impl (pidi,ci,ai,ci') gci, ga_gex (pid,c,a,c') gc)  global_config_rel"
    unfolding ga_gex_impl_def[abs_def] ga_gex_def[abs_def]
    apply simp
    apply (parametricity add: la_ex'_impl ls_of_pid_refine[OF V])
    using GCI CI'I
    apply (auto simp: global_config_rel_def local_config_rel_def) []
    apply parametricity
    apply auto []
    using GCI
    apply (auto simp: global_config_rel_def) []
    done

  definition (in -) "ga_ex_impl  stutter_extend_ex ga_gex_impl"

  fun ga_valid where
    "ga_valid gc None = True"
  | "ga_valid gc (Some (pid,c,a,c')) = pid_valid gc pid"  


  lemma ga_ex_impl:
    assumes V: "ga_valid gc ga"    
    assumes P: "(gai,ga)Id" "(gci,gc)global_config_rel"
    shows "(ga_ex_impl gai gci, ga_ex ga gc)  global_config_rel"
    using assms
    apply (cases "(gc,ga)" rule: ga_valid.cases)
    using P
    apply (simp add: ga_ex_impl_def)

    apply (simp add: ga_ex_impl_def ga_ex_def)
    apply (parametricity add: ga_gex_impl)
    by auto

  definition "ample_step_impl3  rel_of_enex (cr_ample_impl3,ga_ex_impl)"

  definition (in -) pid_interp_gc_impl 
    :: "(ident  bool)  pid_global_config_impl  exp set"
  where
    "pid_interp_gc_impl is_vis_var gci  sm_props (
    vi_α (global_state_impl.variables (pid_global_config.state gci)) |` Collect is_vis_var
  )"

  lemma pid_interp_gc_impl: 
    "(pid_interp_gc_impl is_vis_var, pid_interp_gc)  global_config_rel  Id"
    apply rule
    unfolding pid_interp_gc_impl_def pid_interp_gc_def
    apply (auto simp: global_config_rel_def global_state_rel_def 
      interp_gs_def sm_props_def br_def)
    done

  lemma cr_ample_impl3_sim_aux:
    assumes GCI: "(gci, gc)  global_config_rel"
    assumes GA: "ga  cr_ample_impl3 gci"
    shows "gc'. gacr_ample_impl2 gc 
       gc'=ga_ex ga gc 
       (ga_ex_impl ga gci, gc')global_config_rel"
  proof (clarsimp, safe)
    show G1: "gacr_ample_impl2 gc"
      using cr_ample_impl3_refine[param_fo, OF GCI] GA by auto

    { (* TODO: We are re-proving the validity of the action, due
        to the lack of a clean refinement argumentation *)
      fix mem sticky_E gc pid c
      assume "(pid,c)ga_gample_m mem sticky_E gc"
      hence "pid_valid gc pid"
        unfolding ga_gample_m_def
        apply (auto split: option.splits)
        apply (auto simp: ga_gen_def) []
        apply (auto dest: find_min_idx_f_SomeD)
        done
    } note aux=this 
    from G1 have "ga_valid gc ga" 
      unfolding cr_ample_impl2_def stutter_extend_en_def
      apply (simp split: if_split_asm)
      unfolding ga_gample_mi2_impl[symmetric]
      apply (auto dest: aux)
      done
    thus "(ga_ex_impl ga gci, ga_ex ga gc)global_config_rel"
      by (parametricity add: ga_ex_impl GCI IdI[of ga])
  qed    

  lemma cr_ample_impl3_sim_aux2:
    assumes GCI: "(gci, gc)  global_config_rel"
    assumes GA: "ga  cr_ample_impl2 gc"
    shows "gacr_ample_impl3 gci 
       (ga_ex_impl ga gci, ga_ex ga gc)  global_config_rel"
  proof
    show G1: "gacr_ample_impl3 gci"
      using cr_ample_impl3_refine[param_fo, OF GCI] GA by auto
    
    from cr_ample_impl3_sim_aux[OF GCI G1] show 
      "(ga_ex_impl ga gci, ga_ex ga gc)  global_config_rel"
      by auto
  qed    

  sublocale impl3: sa " g_V = UNIV, g_E = ample_step_impl3, g_V0 = {pid_init_gc_impl},
      sa_L = pid_interp_gc_impl is_vis_var " by unfold_locales auto

  sublocale impl3_sim: lbisimulation 
    global_config_rel
    " g_V = UNIV, g_E = ample_step_impl3, g_V0 = {pid_init_gc_impl},
      sa_L = pid_interp_gc_impl is_vis_var "
    " g_V = UNIV, g_E = ample_step_impl2, g_V0 = {pid_init_gc},
      sa_L = pid_interp_gc "
    apply unfold_locales
    apply simp
    apply simp
    apply simp
    using pid_init_gc_impl
    apply (auto dest: fun_relD) []
    unfolding ample_step_impl2_def ample_step_impl3_def
    apply (auto dest: cr_ample_impl3_sim_aux) []
    using pid_interp_gc_impl
    apply (auto dest: fun_relD) []
    apply simp
    
    using pid_init_gc_impl
    apply (auto dest: fun_relD) []
    defer    
    using pid_interp_gc_impl
    apply (auto dest: fun_relD) []
    apply auto

    apply (auto dest: cr_ample_impl3_sim_aux2) []
    done

  text ‹Correctness of impl3›
  (* TODO: Locale hl_reduction seems very special, and we cannot use it here*)
  lemma impl3_accept_subset: "impl3.accept w  lv.sa.accept w"
    using impl3_sim.accept_bisim cr_ample_impl2_reduction hl_reduction.ample_accept_subset
    by simp

  lemma impl3_accept_stuttering: "lv.sa.accept w  w'. ww'  impl3.accept w'"
    using impl3_sim.accept_bisim cr_ample_impl2_reduction hl_reduction.ample_accept_stuttering
    by simp

  text ‹Next, we go from sets of actions to lists of actions›
  definition (in cprog) "ga_gample_mil4 mem sticky_Ei (gc::pid_global_config_impl) = (
    let 
      lcs = pid_global_config.processes gc;
      gs = pid_global_config.state gc
    in
      collecti_index_list (λ_ lc. let
          c = local_config.command lc;
          ls = local_config.state lc;
          as = comp.succ_impl c;
          s = filter (la_en'_impl (ls,gs) o fst) as;
          ample = s[] 
           ((a,_)set as. read_globals a = {}  write_globals a = {}) 
           ((a,c')set s. ¬mem (c,c') sticky_Ei)
        in
          (ample,map (Pair c) s)
      ) lcs
  )"

  lemma ga_gample_mil4_refine:
    "(ga_gample_mil4, ga_gample_mi3) 
     (Id×rId  Id  bool_rel)  Id  Id  nat_rel ×r Idlist_set_rel"
    apply (intro fun_relI)
    unfolding ga_gample_mil4_def ga_gample_mi3_def
    apply (parametricity)
    apply simp
    apply (rule IdI)
    apply simp
    apply (rule IdI)
    apply (intro fun_relI)
    apply (rule collecti_index_list_refine[param_fo])
    apply (intro fun_relI)
    apply (simp add: list_set_rel_def br_def distinct_map 
      comp.succ_impl_invar)
    apply (auto simp: filter_empty_conv)
    apply force
    done

  definition (in cprog) "cr_ample_impl4 is_vis_var 
    let sticky = find_fas_init_code (=) bounded_hashcode_nat
         (def_hashmap_size TYPE(nat)) cfgc_G_impl (is_vis_edge is_vis_var)
    in stutter_extend_en_list (ga_gample_mil4 (λx f. f x) sticky)"
      
  lemma cr_ample_impl4_refine:
    "(cr_ample_impl4 is_vis_var, cr_ample_impl3)Id  nat_rel ×r Idoption_rellist_set_rel"
    unfolding cr_ample_impl4_def cr_ample_impl3_def
    apply (parametricity add: stutter_extend_en_list.refine ga_gample_mil4_refine)
    apply (simp_all add: is_vis_edge_correct)
    done

  text ‹Finally, we combine the ample-implementation and the executable implementation
    to get a step function›  
  definition (in cprog) "ample_step_impl4 is_vis_var 
    rel_of_enex_list (cr_ample_impl4 is_vis_var,ga_ex_impl)"

  lemma ample_step_impl4: 
    "(ample_step_impl4 is_vis_var, ample_step_impl3)  Id ×r Id set_rel"
    unfolding ample_step_impl4_def ample_step_impl3_def rel_of_pred_def
    apply (parametricity add: rel_of_enex_list_refine cr_ample_impl4_refine[simplified])
    by auto

  sublocale impl4: sa " g_V = UNIV, g_E = ample_step_impl4 is_vis_var,
    g_V0 = {pid_init_gc_impl}, sa_L = pid_interp_gc_impl is_vis_var " by unfold_locales auto

  lemma impl4_accept_subset: "impl4.accept w  lv.sa.accept w"
    using impl3_accept_subset ample_step_impl4
    by simp

  lemma impl4_accept_stuttering: "lv.sa.accept w  w'. ww'  impl4.accept w'"
    using impl3_accept_stuttering ample_step_impl4
    by simp
    
  lemma (in -) pred_of_succ_of_enex_list:
    fixes enex :: "('c  'a list) × ('a  'c  'c)"
    shows "pred_of_succ (set o succ_of_enex_list enex) = pred_of_enex_list enex"
  proof -
    { fix x and l
      have "glist_member (=) x l  xset l"
        by (induction l) auto
    } note [simp] = this

    {
      fix l :: "'a list" and g and l0
      have "set (foldli l (λ_. True) (λx. glist_insert (=) (g x)) l0) = set l0  g`set l"
        by (induction l arbitrary: l0) (auto simp: glist_insert_def)
    } note [simp] = this

    {
      fix l::"'a list" and P i
      have "foldli l Not (λx _. P x) i  i  (xset l. P x)"
        by (induction l arbitrary: i) auto
    } note [simp] = this


    show ?thesis
      unfolding succ_of_enex_list_def[abs_def] pred_of_enex_list_def[abs_def]
      by (auto simp: pred_of_succ_def gen_image_def gen_bex_def intro!: ext)
  qed    
  lemma (in -) rel_of_succ_of_enex_list:
    fixes enex :: "('c  'a list) × ('a  'c  'c)"
    shows "rel_of_succ (set o succ_of_enex_list enex) = rel_of_enex_list enex"
    unfolding rel_of_enex_list_def
    unfolding pred_of_succ_of_enex_list[symmetric]
    by simp

  definition (in cprog) "impl4_succ is_vis_var
     succ_of_enex_list (cr_ample_impl4 is_vis_var,ga_ex_impl)"
  lemma impl4_succ_pred: 
    "rel_of_succ (set o (impl4_succ is_vis_var)) = ample_step_impl4 is_vis_var"
    unfolding impl4_succ_def ample_step_impl4_def 
    by (simp add: rel_of_succ_of_enex_list)
    
end

export_code ga_ex_impl checking SML

definition "ccfg_E_succ_impl mst  remdups o map snd o ccfg_succ_impl mst"

lemma (in cprog) ccfg_E_succ_impl: "ccfg_E_succ_impl (comp_info_of prog) = cfgc_E_succ"
  apply (intro ext) 
  unfolding ccfg_E_succ_impl_def cfgc_E_succ_def
  by (simp add: ccfg_succ_impl)


definition init_pc_impl_impl :: "comp_info  proc_decl  local_config_impl" where
  "init_pc_impl_impl mst pd  
    local_config.command = comp_γ_impl mst (proc_decl.body pd),
    local_config.state = 
      local_state_impl.variables = init_valuation_impl (proc_decl.local_vars pd)
    
  "

lemma (in cprog) init_pc_impl_impl: "init_pc_impl_impl (comp_info_of prog) = init_pc_impl"
  apply (intro ext)
  unfolding init_pc_impl_impl_def init_pc_impl_def
  by (simp add: comp_γ_impl)

definition pid_init_gc_impl_impl :: "program  comp_info  pid_global_config_impl" where
  "pid_init_gc_impl_impl prog mst  
    pid_global_config.processes = (map (init_pc_impl_impl mst) (program.processes prog)),
    pid_global_config.state = 
      global_state_impl.variables = init_valuation_impl (program.global_vars prog)
    
  "

lemma (in cprog) pid_init_gc_impl_impl: 
  "pid_init_gc_impl_impl prog (comp_info_of prog) = pid_init_gc_impl"
  unfolding pid_init_gc_impl_impl_def pid_init_gc_impl_def
  by (simp add: init_pc_impl_impl)

definition "ccfg_V0_impl prog mst  map (comp_γ_impl mst) (cfg_V0_list prog)"

lemma (in cprog) ccfg_V0_impl: "ccfg_V0_impl prog (comp_info_of prog) = cfgc_V0_list"
  unfolding ccfg_V0_impl_def cfgc_V0_list_def
  by (simp add: comp_γ_impl)

definition "ccfg_G_impl_impl prog mst 
   gi_V = λ _. True, gi_E = ccfg_E_succ_impl mst, gi_V0 = ccfg_V0_impl prog mst "

lemma (in cprog) ccfg_G_impl_impl: "ccfg_G_impl_impl prog (comp_info_of prog) = cfgc_G_impl"
  unfolding ccfg_G_impl_impl_def cfgc_G_impl_def
  unfolding ccfg_E_succ_impl ccfg_V0_impl
  by rule

definition "is_vis_edge_impl mst is_vis_var  λ(c,c'). 
  (a,cc')set (ccfg_succ_impl mst c). c'=cc'  (vwrite_globals a. is_vis_var v)"

lemma (in cprog) is_vis_edge_impl: "is_vis_edge_impl (comp_info_of prog) = is_vis_edge"
  apply (intro ext)
  unfolding is_vis_edge_impl_def is_vis_edge_def
  by (simp add: ccfg_succ_impl)

definition "ga_gample_mil4_impl mst mem sticky_Ei (gc::pid_global_config_impl) = (
  let 
    lcs = pid_global_config.processes gc;
    gs = pid_global_config.state gc
  in
    collecti_index_list (λ_ lc. let
        c = local_config.command lc;
        ls = local_config.state lc;
        as = ccfg_succ_impl mst c;
        s = filter (la_en'_impl (ls,gs) o fst) as;
        ample = s[] 
         ((a,_)set as. read_globals a = {}  write_globals a = {}) 
         ((a,c')set s. ¬mem (c,c') sticky_Ei)
      in
        (ample,map (Pair c) s)
    ) lcs
)"

lemma (in cprog) ga_gample_mil4_impl: "ga_gample_mil4_impl (comp_info_of prog) = ga_gample_mil4"
  apply (intro ext)
  unfolding ga_gample_mil4_impl_def ga_gample_mil4_def
  by (simp add: ccfg_succ_impl)


definition "cr_ample_impl4_impl prog mst is_vis_var 
  let sticky = find_fas_init_code (=) bounded_hashcode_nat
       (def_hashmap_size TYPE(nat)) (ccfg_G_impl_impl prog mst)
       (is_vis_edge_impl mst is_vis_var)
  in stutter_extend_en_list (ga_gample_mil4_impl mst (λx f. f x) sticky)"

lemma (in cprog) cr_ample_impl4_impl: "cr_ample_impl4_impl prog (comp_info_of prog) = cr_ample_impl4"
  apply (intro ext)
  unfolding cr_ample_impl4_impl_def cr_ample_impl4_def
  by (simp add: ga_gample_mil4_impl ccfg_G_impl_impl is_vis_edge_impl)

definition "impl4_succ_impl prog mst is_vis_var
     succ_of_enex_list (cr_ample_impl4_impl prog mst is_vis_var,ga_ex_impl)"

lemma (in cprog) impl4_succ_impl: 
  "impl4_succ_impl prog (comp_info_of prog) = impl4_succ"
  apply (intro ext)
  unfolding impl4_succ_impl_def impl4_succ_def
  by (simp add: cr_ample_impl4_impl)

definition "ample_step_impl4_impl prog mst is_vis_var 
   rel_of_enex_list (cr_ample_impl4_impl prog mst is_vis_var,ga_ex_impl)"

lemma (in cprog) ample_step_impl4_impl: 
  "ample_step_impl4_impl prog (comp_info_of prog) = ample_step_impl4"
  apply (intro ext)
  unfolding ample_step_impl4_impl_def ample_step_impl4_def
  by (simp add: cr_ample_impl4_impl)
  
export_code impl4_succ_impl pid_init_gc_impl_impl comp_info_of checking SML

end