Theory SM.SM_Sticky

theory SM_Sticky
imports 
  SM_Indep
  DFS_Framework.Reachable_Nodes
  DFS_Framework.Feedback_Arcs
  Partial_Order_Reduction.Ample_Analysis
begin

  lemma eq_conv_sym: 
    assumes "(a=b) = c"
    shows "(b=a) = c"
    using assms by auto

  lemma neq_conv_sym: 
    assumes "(ab) = c"
    shows "(ba) = c"
    using assms by auto

  lemmas [iff] = not_None_eq[THEN neq_conv_sym]

  lemma none_notin_set_map_Some_conv: "None  set w  (w'. w=map Some w')"
    apply rule
      apply (induction w)
      apply (auto simp: map_eq_Cons_conv[THEN eq_conv_sym]) [2]

      apply auto []
    done

  context cprog begin 
    definition "cfgc_V0  comp.γ ` cfg_V0 prog"
    definition "cfgc_V0_list  map comp.γ (cfg_V0_list prog)"

    lemma cfgc_V0_list_refine: "(cfgc_V0_list, cfgc_V0)  Idlist_set_rel"
      unfolding cfgc_V0_def cfgc_V0_list_def list_set_rel_def br_def
      using cfg_V0_list_invar cfg_V0_list_refine
      apply (auto simp: distinct_map intro!: inj_onI)
      using comp.α_γ_inverse comp.rl_reachable
      apply auto
      by (meson Image_iff comp.γ_inj inj_onD inj_on_subset rtrancl.rtrancl_refl)

    definition "cfgc_E  {(c,c'). a. cfgc c a c'}"
    definition "cfgc_E_succ  remdups o map snd o comp.succ_impl"

    lemma cfgc_E_succ_refine: "(cfgc_E_succ, cfgc_E)  nat_relslg_rel"
      unfolding cfgc_E_def cfgc_E_succ_def comp.astep_impl_def
      unfolding slg_rel_def build_rel_def
      apply (rule relcompI[where b="λc. snd`set (comp.succ_impl c)"])
      apply (auto simp: list_set_rel_def build_rel_def comp.succ_impl_invar)
      done

    definition "cfgc_G   g_V = UNIV, g_E = cfgc_E, g_V0 = cfgc_V0 "
    definition "cfgc_G_impl   gi_V = λ _. True, gi_E = cfgc_E_succ, gi_V0 = cfgc_V0_list "

    lemma cfg_G_simps[simp]:
      "g_V cfgc_G = UNIV"
      "g_E cfgc_G = cfgc_E"
      "g_V0 cfgc_G = cfgc_V0"
      unfolding cfgc_G_def by auto

    lemma cfgc_G_impl_refine: "(cfgc_G_impl, cfgc_G)  unit_rel, nat_relg_impl_rel_ext"
      unfolding cfgc_G_def cfgc_G_impl_def
      by (parametricity add: fun_set_UNIV_refine cfgc_V0_list_refine cfgc_E_succ_refine)

    lemma cfgc_V0_invarc: "ccfgc_V0  comp.invar c"
      unfolding cfgc_V0_def comp.invar_def
      apply auto
      apply (rule comp.γ_invar)
      apply (auto simp: approx_reachable_list_refine cfg_V0_def approx_reachable_prog0)
      done

    lemma cfgc_Estar_invarc: "comp.invar c; (c,c')cfgc_E*  comp.invar c'"
      apply (rotate_tac)
      apply (induction rule: rtrancl_induct)
      apply (auto simp: cfgc_E_def comp.astep_impl_invarc)
      done
  
  end

  context visible_prog
  begin

    lemma pid_valid_preserve[simp]: "pid_valid (ga_ex a gc) pid = pid_valid gc pid"  
      by (auto 
        simp: ga_ex_def ga_gex_def stutter_extend_ex_def
        split: option.splits prod.splits
      )

    lemma pid_valid_preserve_fold[simp]: "pid_valid (fold ga_ex w gc) pid = pid_valid gc pid"  
      by (induction w arbitrary: gc) auto

    lemma pid_valid_ga_gen: "(pid,cac)ga_gen gc  pid_valid gc pid"
      by (auto simp: ga_gen_def)

    lemma pid_valid_ga_en: "Some (pid,cac)ga_en gc  pid_valid gc pid"
      by (auto simp: some_ga_en_eq pid_valid_ga_gen)

    sublocale sys_graph: fb_graph cfgc_G
      apply unfold_locales
      apply (simp_all add: cfgc_V0_def cfg_V0_def cfgc_E_def)
      done

    lemma finite_cfgE_reachable[simp, intro!]: "finite (cfgc_E* `` cfgc_V0)"
      apply (rule finite_ImageI)
      using sys_graph.finite_V0
      apply simp
      apply (rule finite_subset[where B="Collect comp.invar"])
      apply (auto intro: cfgc_V0_invarc cfgc_Estar_invarc) []
      apply (simp add: comp.invar_def[abs_def])      
      done

    definition "vis_edges  {(c,c'). a. cfgc c a c'  write_globals a  vis_vars  {}}"

    fun ga_is_pid :: "global_action option  pid  bool" where
      "ga_is_pid None _  True"
    | "ga_is_pid (Some (pid',_)) pid  pid'=pid"


    lemma 
      assumes "(pid,c,a,c')  ga_gen gc"
      shows 
        ga_gen_cmd: "cmd_of_pid gc pid = c" and 
        ga_gen_cmd': "cmd_of_pid (ga_gex (pid,c,a,c') gc) pid = c'" and 
        ga_gen_edge: "(c,c')cfgc_E"
      using assms
      apply -
      apply (cases a)
      apply (auto 
        simp: cfgc_E_def
        simp: ga_gen_def la_en'_def
        simp: ga_gex_def la_ex'_def
        split: option.splits
        ) [5]
      apply (cases a)
      apply (auto 
        simp: cfgc_E_def
        simp: ga_gen_def la_en'_def
        simp: ga_gex_def la_ex'_def
        split: option.splits
        ) [5]
      apply (cases a)
      apply (auto 
        simp: cfgc_E_def
        simp: ga_gen_def la_en'_def
        simp: ga_gex_def la_ex'_def
        split: option.splits
        ) [5]
      done      

    lemmas ga_gen_cmd_cfg = ga_gen_cmd ga_gen_cmd' ga_gen_edge

    lemma ga_gex_other: 
      assumes "pid'pid"
      shows "cmd_of_pid (ga_gex (pid',c,a,c') gc) pid = cmd_of_pid gc pid"
      using assms
      apply (cases a)
      apply (auto 
        simp: ga_gex_def la_ex'_def
        split: option.splits
        ) [5]
      done

    lemma proj_word_fin_to_cfg_E:
      assumes "jsys.path (map Some w) gc"
      assumes "fold ga_gex w gc = gc'"
      shows "(cmd_of_pid gc pid, cmd_of_pid gc' pid) 
         (cfgc_E  (λ(_,c,_,c'). (c,c'))`set w)*" (is "_(?E w)*")
      using assms
    proof (induction w arbitrary: gc)
      case (Cons ga w)
      from Cons.prems have 
        EN: "ga  ga_gen gc" and
        WF': "jsys.path (map Some w) (ga_gex ga gc)" and
        EX': "fold ga_gex w (ga_gex ga gc) = gc'"
        by (auto simp: some_ga_en_eq some_ga_ex_eq)
      obtain pid' c a c' where [simp]: "ga = (pid',c,a,c')"
        by (cases ga)

      have "(cmd_of_pid gc pid, cmd_of_pid (ga_gex ga gc) pid)  (?E (ga#w))*"
      proof (cases "pid'=pid")  
        case True
        note True[simp]
        from EN have "(pid,c,a,c')ga_gen gc" by simp
        from ga_gen_cmd_cfg[OF this] 
        have "(cmd_of_pid gc pid, cmd_of_pid (ga_gex ga gc) pid)  ?E (ga#w)" 
          by auto
        thus ?thesis ..
      next
        case False
        hence "cmd_of_pid (ga_gex ga gc) pid = cmd_of_pid gc pid"
          by (simp add: ga_gex_other)
        thus ?thesis by auto
      qed
      also from Cons.IH[OF WF' EX'] have 
        "(cmd_of_pid (ga_gex ga gc) pid, cmd_of_pid gc' pid)  (?E (ga#w))*"
        apply (rule set_rev_mp[OF _ rtrancl_mono])
        by auto
      finally show ?case .
    qed simp

    lemma words_fin_None_fmt:
      assumes "jsys.path w gc"
      obtains w' n where "w=map Some w'@replicate n None"
      using assms
    proof (induction arbitrary: thesis)
      case nil thus ?case by simp
    next
      case (cons a gc w)
      from cons.IH obtain w' n where [simp]: "w=map Some w'@replicate n None" .
      show ?case proof (cases a)
        case None
        note None[simp] 
        from cons.hyps have [simp]: "w'=[]" 
          by (cases w') (auto simp: none_ga_en_eq some_ga_en_eq) 
        show ?thesis apply (rule cons.prems[of "[]" "Suc n"]) by simp
      next
        case (Some aa)
        note Some[simp]
        show ?thesis apply (rule cons.prems[of "aa#w'" n]) by simp
      qed
    qed

    lemma proj_reachable_to_cfgE:
      assumes R: "gcjsys.nodes"
      assumes PIDV: "pid_valid gc pid"
      shows "c0cfgc_V0. (c0,cmd_of_pid gc pid)cfgc_E*"
    proof -
      from R obtain w where 
        WF: "jsys.path w pid_init_gc"
        and EX: "fold ga_ex w (pid_init_gc) = gc"
        by rule auto
      from words_fin_None_fmt[OF WF] obtain w' n where 
        [simp]: "w = map Some w'@replicate n None" .

      from EX have "fold ga_ex (map Some w') (pid_init_gc) = gc" 
        by simp  
      hence EX': "fold ga_gex w' (pid_init_gc) = gc"
        by (simp add: fold_map some_ga_ex_eq)

      from WF have WF': "jsys.path (map Some w') pid_init_gc" 
        by auto
        
      from proj_word_fin_to_cfg_E[OF WF' EX', of pid] have
        G: "(cmd_of_pid (pid_init_gc) pid,cmd_of_pid gc pid)  cfgc_E*"
        by (rule set_rev_mp[OF _ rtrancl_mono]) auto
        
      show ?thesis proof (cases "pid_valid (pid_init_gc) pid")
        case True 
        hence "cmd_of_pid (pid_init_gc) pid  cfgc_V0"
          by (auto simp: cfgc_V0_def cfg_V0_def pid_init_gc_def init_pc_def)
        with G show ?thesis ..
      next
        case False 
        hence "¬pid_valid gc pid"
          unfolding EX[symmetric] by simp 
        with PIDV have False by blast thus ?thesis ..
      qed
    qed

    lemma proj_ne_word_fin_to_cfg_E:
      assumes WF: "jsys.path (map Some w) gc"
      assumes EX: "fold ga_gex w gc = gc'"
      assumes [simp]: "w=(pid,cac)#w'" (is "w=?ga#_")
      shows "(cmd_of_pid gc pid, cmd_of_pid gc' pid) 
         (cfgc_E  (λ(_,c,_,c'). (c,c'))`set w)+" (is "_?E+")
    proof -
      from WF EX have 
        EN: "?ga  ga_gen gc" and
        WF': "jsys.path (map Some w') (ga_gex ?ga gc)" and
        EX': "fold ga_gex w' (ga_gex ?ga gc) = gc'"
        by (auto simp: some_ga_en_eq some_ga_ex_eq)

      obtain c a c' where [simp]: "cac = (c,a,c')" by (cases cac)

      from EN have "(pid,c,a,c')ga_gen gc" by simp
      from ga_gen_cmd_cfg[OF this] 
      have "(cmd_of_pid gc pid, cmd_of_pid (ga_gex ?ga gc) pid)  ?E" 
        by auto
      also from proj_word_fin_to_cfg_E[OF WF' EX'] 
      have "(cmd_of_pid (ga_gex ?ga gc) pid, cmd_of_pid gc' pid)  ?E*"
        apply (rule set_rev_mp[OF _ rtrancl_mono])
        by auto
      finally (rtrancl_into_trancl2) show ?thesis .
    qed

  end

  locale sticky_prog = visible_prog +
    fixes sticky_E
    assumes sticky_E_fas: "is_fas cfgc_G sticky_E"  
    assumes sticky_E_vis: "vis_edges  sticky_E"
  begin

    definition "sticky_ga  Collect (
      λNone  True 
    | Some (pid,c,a,c')  (c,c')sticky_E)"

    lemma sticky_ga_approx_visible: "jsys.visible  sticky_ga"
    proof -
      have aux: "s s'. sm_props s  sm_props s'  s  s'"
        by auto

      show ?thesis
        apply (clarsimp simp: sticky_ga_def split: option.split)
        apply (rule set_mp[OF sticky_E_vis])
        apply (clarsimp 
          elim!: jsys.visibleE 
          simp: sticky_ga_def
          split: option.split)
        apply (clarsimp 
          split: prod.splits
          simp: ga_en_def ga_gen_def ga_ex_def ga_gex_def
          simp: pid_interp_gc_def interp_gs_def
          simp: vis_edges_def)
        apply (intro exI conjI, assumption) 
        apply (drule ex_mod_limit)
        
        apply (drule aux)
        apply (fastforce simp: eq_on_def restrict_map_def)
        done
    qed  

    lemma sticky_ga_breaks_cycles:
      assumes "gcjsys.nodes"
      assumes "wjsys.cycles gc"
      assumes "w[]"
      shows "set w  sticky_ga  {}"
    proof (cases "None  set w")
      case True
      thus ?thesis
        by (auto simp: sticky_ga_def)
    next
      case False
      then obtain w' where [simp]: "w=map Some w'"
        by (auto simp: none_notin_set_map_Some_conv)

      have aux1: "Some ` set w'  sticky_ga 
        = Some ` (set w'  {(pid,c,a,c'). (c,c')sticky_E})"
        by (auto simp: sticky_ga_def)
  

      show ?thesis 
      proof (cases "(pid,c,a,c')set w'. (c,c')sticky_E")
        case True thus ?thesis by (auto simp: aux1)
      next  
        case False 
        let ?E = "(cfgc_E  (λ(_, c, _, c'). (c, c')) ` set w')"

        from False have NO_STICKY: "?E  sticky_E = {}" by auto

        from w[] obtain pid cac w'' where W'_FMT[simp]: "w'=(pid,cac)#w''"
          by (auto simp: neq_Nil_conv)

        from wjsys.cycles gc have PIDV: "pid_valid gc pid"
          by (auto simp: pid_valid_ga_en)

        have "(cmd_of_pid gc pid, cmd_of_pid gc pid) ?E+"
          apply (rule proj_ne_word_fin_to_cfg_E[OF _ _ W'_FMT])
          using wjsys.cycles gc
          by (auto simp: fold_map some_ga_ex_eq)
        hence CYC: "(cmd_of_pid gc pid, cmd_of_pid gc pid)  (cfgc_E-sticky_E)+"
          apply (rule trancl_mono)
          using NO_STICKY by blast

        from proj_reachable_to_cfgE[OF gcjsys.nodes PIDV] obtain
          c0 where C0: "c0cfgc_V0" and REACH: "(c0,cmd_of_pid gc pid)cfgc_E*" ..

        from CYC C0 REACH sticky_E_fas[unfolded is_fas_def]
          have False by force
        thus ?thesis ..
      qed
    qed
      
    sublocale jsys: transition_system_sticky 
      ga_ex "λ a p. a  ga_en p" "λ p. p = pid_init_gc" pid_interp_gc sticky_ga
      apply unfold_locales
      using sticky_ga_breaks_cycles apply blast
      using sticky_ga_approx_visible apply blast
      done

    sublocale jsys: transition_system_ample ga_ex "λ a p. a  ga_en p" "λ p. p = pid_init_gc"
      pid_interp_gc sticky_ga ind
      by unfold_locales

  end

end