Theory SM.Pid_Scheduler

theory Pid_Scheduler
imports Gen_Scheduler_Refine Partial_Order_Reduction.Transition_System_Extensions
begin

  lemma system_complete_language_eq_lsystem_accept:
    fixes ex en init int
    defines "S ≡ ⦇ g_V = UNIV, g_E = rel_of_enex (en, ex), g_V0 = {init}, sa_L = int ⦈"
    assumes "sa S"
    shows "snth ` transition_system_complete.language ex (λ a p. a ∈ en p) (λ p. p = init) int = {w. sa.accept S w}"
  proof -
    interpret jsys?: transition_system_complete ex "λ a p. a ∈ en p" "λ p. p = init" int by this
    interpret psys?: sa S by fact
    show ?thesis
    unfolding jsys.language_def
    unfolding psys.accept_def
    proof safe
      fix p w
      assume 1: "run w init"
      show "∃ r. is_run r ∧ snth (smap int (init ## trace w init)) = L ∘ r"
      unfolding is_run_def ipath_def
      unfolding S_def graph_rec.simps sa_rec.simps
      unfolding rel_of_enex_def Let_def prod.case
      proof (intro allI exI conjI)
        fix i
        show "(init ## trace w init) !! 0 ∈ {init}" by simp
        show "snth (smap int (init ## trace w init)) = int ∘ snth (init ## trace w init)"
          by (metis (full_types) fun_comp_eq_conv smap_alt)
        have 10: "w = stake i w @- [w !! i] @- sdrop (Suc i) w" using id_stake_snth_sdrop by auto
        have 20: "run (stake i w @- [w !! i] @- sdrop (Suc i) w) init" using 1 10 by simp
        have 1: "w !! i ∈ en (target (stake i w) init)" using 20 by auto
        have 2: "ex (w !! i) (target (stake i w) init) = target (stake (Suc i) w) init"
          using 20 unfolding stake_Suc by auto
        show "((init ## trace w init) !! i, (init ## trace w init) !! Suc i) ∈
          {(s, ex a s) |s a. a ∈ en s}" using 1 2 by force
      qed
    next
      fix r
      assume 1: "is_run r"
      obtain w where 2: "r 0 = init" "⋀ i. w i ∈ en (r i)" "⋀ i. r (Suc i) = ex (w i) (r i)"
        using 1
        unfolding is_run_def ipath_def
        unfolding S_def graph_rec.simps
        unfolding rel_of_enex_def Let_def prod.case
        by simp metis
      have 3: "L ∘ r = snth (smap int (smap r nats))" unfolding assms(1) by auto
      have 4: "(init ## trace (smap w nats) init) !! i = smap r nats !! i" for i
        using 2 by (induct i) (auto)
      have 5: "smap r nats = init ## trace (smap w nats) init" using eqI_snth 4 by metis
      have 6: "target (stake k (smap w nats)) init = smap r nats !! k" for k
        unfolding sscan_scons_snth 5 by rule
      have 7: "run (smap w nats) init" using 2(2) 6 by (auto intro: snth_run)
      show "L ∘ r ∈ (!!) ` {smap int (p ## trace w p) |p w. p = init ∧ run w p}"
        unfolding 3 using 5 7 by force
    qed
  qed

  (* TODO: Move *)  
  lemma prod_splitE:
    assumes "∀a b. p=(a,b) ⟶ P a b"
    obtains a b where "p=(a,b)" "P a b"
    using assms
    by (cases p) auto

  lemma sngp_sym_conv: "(λp. p=x) = (=) x" by auto  


  lemma in_multiset_of_conv_nth: "x ∈# mset l ⟷ (∃i<length l. x = l!i)"
    by (metis in_multiset_in_set in_set_conv_nth)
    
  lemma multiset_of_em_conv_nth: "mset l = {#x#} + m' 
    ⟷ (∃i<length l. x = l!i ∧ m' = mset l - {#x#})"
    by (metis add_diff_cancel_left' in_multiset_of_conv_nth 
      insert_DiffM multi_member_this)

  
  type_synonym pid = nat
  record ('c,'ls,'gs) pid_global_config =
    processes :: "('c,'ls) local_config list"  
    state :: 'gs

  definition pidgc_α 
    :: "('c,'ls,'gs) pid_global_config ⇒ ('c,'ls,'gs) global_config" where
    "pidgc_α pgc ≡ ⦇     
      global_config.processes = mset (pid_global_config.processes pgc),
      global_config.state = pid_global_config.state pgc
    ⦈"

  abbreviation pid_valid :: "('c,'ls,'gs) pid_global_config ⇒ pid ⇒ bool" 
    where
    "pid_valid gc pid ≡ pid < length (pid_global_config.processes gc)"
    
  abbreviation "lc_of_pid gc pid 
    ≡ pid_global_config.processes gc ! pid"
  
  abbreviation "cmd_of_pid gc pid 
    ≡ local_config.command (lc_of_pid gc pid)"
    
  abbreviation "ls_of_pid gc pid 
    ≡ local_config.state (lc_of_pid gc pid)"


  context Gen_Scheduler'
  begin

    definition pid_gstep_succ 
      :: "('c,'ls,'gs) pid_global_config ⇒ ('c,'ls,'gs) pid_global_config set" 
      where
      "pid_gstep_succ gc ≡ do {
        ― ‹ Select process ›
        let lcs = pid_global_config.processes gc;
        pid ← {0..<length lcs};
        let lc = lcs!pid;
        ― ‹ Focus state ›
        let gs = pid_global_config.state gc;
        let ls = local_config.state lc;
  
        ― ‹ Select action ›
        let cmd = local_config.command lc;
        (a,cmd') ← {(a,cmd'). cstep cmd a cmd'};
  
        if en (ls,gs) a then {do { 
          ― ‹ Execute ›
          let (ls,gs) = ex (ls,gs) a;
          ― ‹ Unfocus state. ›
          let lc = ⦇ local_config.command = cmd', local_config.state = ls⦈;
          ⦇ 
            pid_global_config.processes = lcs[pid:=lc],
            pid_global_config.state = gs  
          ⦈
        }}
      else {}
    }"

    lemma pid_gstep_succE:
      assumes "gc' ∈ pid_gstep_succ gc"
      obtains pid a c' ls' gs' where
        "pid_valid gc pid"
        "cstep (cmd_of_pid gc pid) a c'"
        "en (ls_of_pid gc pid, pid_global_config.state gc) a"
        "ex (ls_of_pid gc pid, pid_global_config.state gc) a = (ls',gs')"
        "gc' = ⦇ 
          pid_global_config.processes = (pid_global_config.processes gc)
            [pid := 
              ⦇ local_config.command = c', local_config.state = ls'⦈
            ],
          pid_global_config.state = gs'⦈"
      using assms
      unfolding pid_gstep_succ_def
      by (auto 
        split: if_split_asm prod.splits 
        elim!: prod_splitE
        simp: all_conj_distrib)

  lemma pid_gstep_succI:
    assumes
      "pid_valid gc pid"
      "cstep (cmd_of_pid gc pid) a c'"
      "en (ls_of_pid gc pid, pid_global_config.state gc) a"
      "ex (ls_of_pid gc pid, pid_global_config.state gc) a = (ls',gs')"
    shows "
      ⦇ 
        pid_global_config.processes = (pid_global_config.processes gc)
          [pid := 
            ⦇ local_config.command = c', local_config.state = ls'⦈
          ],
        pid_global_config.state = gs'
      ⦈ ∈ pid_gstep_succ gc"
    using assms
    unfolding pid_gstep_succ_def
    by fastforce

  lemma pid_gc_state_eq: 
    "pid_global_config.state pgc = global_config.state (pidgc_α pgc)"
    unfolding pidgc_α_def by auto  
    
  lemma pid_gc_proc_eq:
    assumes "pid_valid gc pid"  
    shows "
      global_config.processes (pidgc_α gc) 
      = {#lc_of_pid gc pid#} 
      + (global_config.processes (pidgc_α gc) - {#lc_of_pid gc pid#})"
    using assms
    by (auto simp: pidgc_α_def multiset_of_em_conv_nth)


  lemma pid_gstep_correct: 
    "gstep_succ (pidgc_α pgc) = pidgc_α`pid_gstep_succ pgc"
    apply safe
    apply (erule gstep_succE)
    apply (clarsimp simp: pidgc_α_def multiset_of_em_conv_nth)
    apply (frule (3) pid_gstep_succI)
    apply (erule image_eqI[rotated])
    apply (auto simp: pidgc_α_def mset_update add_ac union_mset_add_mset_right) []

    apply (erule pid_gstep_succE)
    apply (clarsimp simp: pidgc_α_def mset_update)
    apply (simp add: pid_gc_state_eq)
    apply (frule (2) gstep_succI[rotated])
    apply (rule pid_gc_proc_eq, assumption)
    apply (auto simp: add_ac pidgc_α_def union_mset_add_mset_left) []
    done

  abbreviation "pid_gstep ≡ rel_of_succ pid_gstep_succ"
  definition "pid_step ≡ stutter_extend_edges UNIV pid_gstep"

end

locale Pid_Gen_Scheduler_linit = 
  Gen_Scheduler'_linit cstep en ex init label
  for cstep :: "'c ⇒ 'a ⇒ 'c ⇒ bool"
  and en :: "('ls×'gs) ⇒ 'a ⇒ bool"
  and ex :: "('ls×'gs) ⇒ 'a ⇒ ('ls×'gs)"
  and init :: "('c,'ls,'gs) global_config set"
  and label :: "('c,'ls,'gs) global_config ⇒ 'l" +
  fixes pid_init :: "('c,'ls,'gs) pid_global_config"
  and pid_label :: "('c,'ls,'gs) pid_global_config ⇒ 'l"
  assumes pid_init_eq: "gc ∈ init ⟷ (gc=pidgc_α pid_init)"
  assumes pid_label_eq: "label (pidgc_α pgc) = pid_label pgc"
begin

  definition pid_system_automaton' :: "(('c,'ls,'gs) pid_global_config, 'l) sa_rec"
    where "pid_system_automaton' ≡
      ⦇ g_V = UNIV, g_E = pid_gstep, g_V0 = {pid_init}, sa_L = pid_label ⦈"

  lemma pid_system_automaton'_simps[simp]:
    "g_V pid_system_automaton' = UNIV"
    "g_E pid_system_automaton' = pid_gstep"
    "g_V0 pid_system_automaton' = {pid_init}"
    "sa_L pid_system_automaton' = pid_label"
    unfolding pid_system_automaton'_def by auto

  definition pid_system_automaton :: "(('c,'ls,'gs) pid_global_config, 'l) sa_rec"
    where "pid_system_automaton ≡
      ⦇ g_V = UNIV, g_E = pid_step, g_V0 = {pid_init}, sa_L = pid_label ⦈"

  lemma pid_system_automaton_simps[simp]:
    "g_V pid_system_automaton = UNIV"
    "g_E pid_system_automaton = pid_step"
    "g_V0 pid_system_automaton = {pid_init}"
    "sa_L pid_system_automaton = pid_label"
    unfolding pid_system_automaton_def by auto

  lemma pid_system_automaton_alt_def: "pid_system_automaton = stutter_extend pid_system_automaton'"
    unfolding pid_step_def pid_system_automaton'_def pid_system_automaton_def stutter_extend_def
    by simp

  sublocale pid': sa pid_system_automaton' by unfold_locales auto
  sublocale pid: sa pid_system_automaton
    unfolding pid_system_automaton_alt_def using pid'.stutter_extend_sa by this

  sublocale bisim: lbisimulation "br pidgc_α (λ_. True)" pid_system_automaton system_automaton
  proof -
    interpret bisim: lbisimulation "br pidgc_α (λ_. True)" pid_system_automaton' system_automaton'
      apply unfold_locales
      apply (auto simp: build_rel_def pid_init_eq pid_gstep_correct pid_label_eq)
      done
    interpret bisim: lbisimulation "br pidgc_α (λ_. True)" pid_system_automaton system_automaton
      unfolding system_automaton_alt_def pid_system_automaton_alt_def
      using bisim.lstutter_extend by this
    show "lbisimulation (br pidgc_α (λ _. True)) pid_system_automaton system_automaton"
      by unfold_locales
  qed

  lemma pid_accept_eq: "pid.accept = sa.accept" by (rule bisim.accept_bisim)

  lemma pid_run_conv: "sa.g.is_run r ⟷ (∃r'. r=pidgc_α o r' ∧ pid.g.is_run r')"
    by (rule bisim.br_run_conv[OF refl])   

  lemma pid_run_sim: "pid.g.is_run r ⟹ sa.g.is_run (pidgc_α o r)"
    by (rule bisim.s1.br_run_sim[OF refl])

section "Global Actions"

text ‹
  A global action consists of a PID and a control flow graph edge
›
type_synonym (in -) ('c,'a) global_action = "pid × 'c × 'a × 'c"


abbreviation (in -) "fs_of_pid gc pid ≡ (ls_of_pid gc pid,pid_global_config.state gc)"

  definition ga_gen 
    :: "('c,'ls,'gs) pid_global_config ⇒ ('c,'a) global_action set"
  where
    "ga_gen gc ≡ { (pid,c,a,c') .
      cstep c a c' 
    ∧ pid_valid gc pid 
    ∧ c=cmd_of_pid gc pid
    ∧ en (fs_of_pid gc pid) a }"

  definition ga_gex
    :: "('c,'a) global_action ⇒ ('c,'ls,'gs) pid_global_config ⇒ ('c,'ls,'gs) pid_global_config"
  where
    "ga_gex ga gc ≡ let 
      (pid,c,a,c') = ga;
      fs = fs_of_pid gc pid;
      (ls',gs') = ex 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'"

  definition "ga_gstep ≡ rel_of_enex (ga_gen,ga_gex)"
  definition "ga_en ≡ stutter_extend_en ga_gen"
  definition "ga_ex ≡ stutter_extend_ex ga_gex"
  definition "ga_step ≡ stutter_extend_edges UNIV ga_gstep"
  lemma ga_step_alt: "ga_step = rel_of_enex (ga_en,ga_ex)"
    unfolding ga_step_def ga_gstep_def ga_en_def ga_ex_def
    by (auto simp: stutter_extend_pred_of_enex_conv)

  lemma some_ga_en_eq: 
    "Some a ∈ ga_en gc ⟷ a ∈ ga_gen gc"
    by (auto simp: ga_en_def)
  lemma some_ga_ex_eq: 
    "ga_ex (Some a) gc = ga_gex a gc"
    "ga_ex ∘ Some = ga_gex"
    by (auto simp: ga_ex_def intro!: ext)
  lemma none_ga_en_eq: "None ∈ ga_en gc ⟷ ga_gen gc = {}"
    by (auto simp: ga_en_def stutter_extend_en_def)
  lemma ga_ex_none[simp]: "ga_ex None = id"   
    by (auto simp: ga_ex_def)

  lemma ga_gstep_eq: "ga_gstep = pid_gstep"
    apply safe
    apply (auto 
      simp: ga_gstep_def ga_gen_def ga_gex_def 
      split: prod.splits elim!: prod_splitE
      intro: pid_gstep_succI) []
     
    apply (fastforce 
      simp: pred_of_succ_def ga_gstep_def ga_gen_def ga_gex_def
      split: prod.splits
      elim!: pid_gstep_succE)
    done

  lemma ga_step_eq: "ga_step = pid_step" 
    unfolding ga_step_def pid_step_def ga_gstep_eq by rule

  definition ga_automaton :: "(('c,'ls,'gs) pid_global_config, 'l) sa_rec"
    where "ga_automaton ≡ ⦇ g_V = UNIV, g_E = ga_step, g_V0 = {pid_init}, sa_L = pid_label ⦈"

  lemma ga_automaton_simps[simp]:
    "g_V ga_automaton = UNIV"
    "g_E ga_automaton = ga_step"
    "g_V0 ga_automaton = {pid_init}"
    "sa_L ga_automaton = pid_label"
    unfolding ga_automaton_def by simp+

  lemma ga_pid_system_automaton: "ga_automaton = pid_system_automaton"
    unfolding ga_automaton_def pid_system_automaton_def ga_step_eq by rule

  sublocale jsys: transition_system ga_ex "λ a p. a ∈ ga_en p" .
  sublocale ga: sa ga_automaton unfolding ga_pid_system_automaton by unfold_locales

  sublocale ga_bisim: lbisimulation Id ga_automaton pid_system_automaton
    unfolding ga_pid_system_automaton by auto

  lemma ga_accept_eq: "ga.accept = sa.accept" 
    by (simp add: ga_bisim.accept_bisim pid_accept_eq) 

  lemma ga_run_eq: "pid.g.is_run r = ga.is_run r"
    using ga_bisim.br_run_conv[of id "λ_. True" r]
    by (auto simp: build_rel_def[abs_def])

  sublocale jsys: transition_system_initial ga_ex "λ a p. a ∈ ga_en p" "λ p. p = pid_init" . 

  lemma reachable_alt: "jsys.nodes = ga.E⇧* `` ga.V0"
  proof safe
    fix gc
    assume "gc ∈ jsys.nodes"
    thus "gc ∈ ga.E⇧* `` ga.V0"
      unfolding ga_automaton_def ga_step_alt rel_of_enex_def
      by (induct, auto intro: rtrancl_into_rtrancl)
  next
    fix gc gc'
    assume "(gc, gc') ∈ ga.E⇧*" "gc ∈ ga.V0"
    thus "gc' ∈ jsys.nodes" unfolding ga_automaton_def ga_step_alt by induct auto
  qed

  lemma rtrancl_step_exec_word_conv:  
    "(gc, gc') ∈ ga_step⇧* ⟷ (∃w. jsys.path w gc ∧ gc' = jsys.target w gc)"
  proof safe
    assume "(gc, gc') ∈ ga_step⇧*"
    thus "∃ w. jsys.path w gc ∧ gc' = jsys.target w gc"
      apply induction
      apply force
      apply (force simp: ga_step_alt pred_of_enex_def)
      done
  next
    fix w
    assume "jsys.path w gc"
    thus "(gc, jsys.target w gc) ∈ ga_step⇧*"
      apply induction
      apply (auto simp: ga_step_alt rel_of_enex_def
        intro: converse_rtrancl_into_rtrancl)
      done
  qed

  sublocale jsys: transition_system_complete ga_ex "λ a p. a ∈ ga_en p" "λ p. p = pid_init" pid_label .

  lemma accept_eq_lang: "snth ` jsys.language = Collect sa.accept"
    unfolding ga_accept_eq[symmetric]
    unfolding ga_automaton_def
    unfolding ga_step_alt
    apply (rule system_complete_language_eq_lsystem_accept)
    unfolding ga_step_alt[symmetric]
    unfolding ga_automaton_def[symmetric]
    by unfold_locales

end

end