Theory Location_Addition

theory Location_Addition
  imports
    Cooperation_Program
begin
  
datatype ('f,'v,'t,'l,'tr) location_addition_info = Location_Addition_Info 'l 'l 'tr "('f,'v,'t,'l) transition_rule"

fun change_target :: "'l ⇒ ('f,'v,'t,'l) transition_rule ⇒ ('f,'v,'t,'l) transition_rule" where
  "change_target l (Transition src tgt φ) = Transition src l φ" 

fun change_source :: "'l ⇒ ('f,'v,'t,'l) transition_rule ⇒ ('f,'v,'t,'l) transition_rule" where
  "change_source l (Transition src tgt φ) = Transition l tgt φ" 
  
lemma if_sharp_change_target[simp]: "is_sharp_transition (change_target l tau) = is_sharp_transition tau" by (cases tau, auto)
lemma if_sharp_change_source[simp]: "is_sharp_transition (change_source l tau) = is_sharp l" by (cases tau, auto)

context lts
begin

lemma transition_rule_change_target[simp]: "transition_rule (change_target l tau) = transition_rule tau" 
  by (cases tau, auto)

lemma transition_rule_change_source[simp]: "transition_rule (change_source l tau) = transition_rule tau" 
  by (cases tau, auto)
    
context
  fixes P P'
  assumes SN: "cooperation_SN P'"
  and flat_id: "flat_transitions_of P' = flat_transitions_of P"
  and init_id: "lts.initial P' = lts.initial P" 
    "⋀ l. l ∈ lts.initial P ⟹ assertion P l = assertion P' l"
  and lc: "⋀ l. l ∈ nodes_lts P ⟹ assertion P' l = assertion P l" 
begin
lemma add_new_sharp_location_in_out:  
  assumes sharp_new: "⋀ τ. τ ∈ sharp_transitions_of P - sharp_transitions_of P' ⟹ 
    ∃ τ' l. τ' ∈ sharp_transitions_of P' ∧ skip_transition τ' ∧ 
      ((change_target l τ ∈ sharp_transitions_of P' 
        ∧ source τ' = l ∧ target τ' = target τ 
        ∧ assertion P' l = assertion P (target τ)) 
    ∨ (change_source l τ ∈ sharp_transitions_of P' 
        ∧ source τ' = source τ ∧ target τ' = l 
        ∧ assertion P' l = assertion P (source τ)))" 
  shows "cooperation_SN P" 
proof -
  interpret P': indexed_rewriting "transition_step_lts P'" .
  from init_id have init: "initial_states P' = initial_states P" unfolding initial_states_def  by auto
  show ?thesis
  proof (rule cooperation_SN_on_trancl_image[OF _ _ SN[unfolded init flat_id]])
    fix τ
    assume mem: "τ ∈ sharp_transitions_of P"
    with lc[of "source τ"] lc[of "target τ"]
    have lc: "assertion P' (source τ) = assertion P (source τ)" 
      "assertion P' (target τ) = assertion P (target τ)" 
      unfolding nodes_lts_def by auto
    show "∃ps. ps ≠ {} ∧ ps ⊆ {τ ∈ transition_rules P'. is_sharp_transition τ} ∧ transition_step_lts P τ ⊆ indexed_rewriting.traverse (transition_step_lts P') ps"
    proof(cases "τ ∈ sharp_transitions_of P'")
      case True
      have "transition_step_lts P τ ⊆ P'.traverse {τ}" 
      proof
        fix a b
        assume "(a,b) ∈ transition_step_lts P τ" 
        then have "(a,b) ∈ transition_step_lts P' τ" using lc
          by (cases a; cases b; cases τ, auto)
        then show "(a,b) ∈ P'.traverse {τ}" 
          by (intro P'.mem_traverseI[of "λ i. if i = 0 then a else b" _ 1], auto intro: indexed_rewriting.traversed.intros)
      qed
      then show ?thesis
        by (intro exI[of _ "{τ}"], insert mem True, auto)
    next
      case False
      with mem sharp_new[of τ] obtain τ2 l where 
          t2: "τ2 ∈ sharp_transitions_of P'" 
           "skip_transition τ2" 
        and choice: "change_target l τ ∈ sharp_transitions_of P' ∧ source τ2 = l ∧ target τ2 = target τ
          ∧ assertion P' l = assertion P (target τ) ∨
            change_source l τ ∈ sharp_transitions_of P' ∧ source τ2 = source τ ∧ target τ2 = l
          ∧ assertion P' l = assertion P (source τ)
            " (is "?one ∨ ?two") by auto
      from choice
      show ?thesis
      proof 
        assume *: ?one
        let ?t1 = "change_target l τ" 
        have "transition_step_lts P τ ⊆ P'.traverse {τ2, ?t1}" 
        proof
          fix a b
          assume ab: "(a,b) ∈ transition_step_lts P τ" 
          obtain la sa where a: "a = State sa la" by (cases a, auto)
          obtain lb sb where b: "b = State sb lb" by (cases b, auto)
          let ?c = "State sb l" 
          from ab * t2 have 1: "(a, ?c) ∈ transition_step_lts P' ?t1" and 
            t2'': "target τ2 = lb" and sb: "assignment sb" 
            unfolding a b using lc by (cases τ, auto)                       
          from * have src: "source τ2 = l" by simp
          have 2: "(?c, b) ∈ transition_step_lts P' τ2" unfolding b 
            by (rule skip_transition_step[OF t2(2) sb, unfolded src t2''], 
              insert lc * a b ab, cases τ, auto)
          show "(a,b) ∈ P'.traverse {τ2, ?t1}" by 
            (intro P'.mem_traverseI[of "λ i. if i = 0 then a else if i = 1 then ?c else b" _ "Suc (Suc 0)"], 
            force+, intro P'.traversed.intros, insert 1 2, auto)        
        qed
        with * t2 show ?thesis by (intro exI[of _ "{τ2, ?t1}"], auto)
      next
        assume *: ?two
        let ?t1 = "change_source l τ" 
        have "transition_step_lts P τ ⊆ P'.traverse {?t1, τ2}" 
        proof
          fix a b
          assume ab: "(a,b) ∈ transition_step_lts P τ" 
          obtain la sa where a: "a = State sa la" by (cases a, auto)
          obtain lb sb where b: "b = State sb lb" by (cases b, auto)
          let ?c = "State sa l" 
          from ab * have 1: "(?c, b) ∈ transition_step_lts P' ?t1" and t2'': "source ?t1 = l" "source τ = la" and sa: "assignment sa" 
            unfolding a b using lc * by (cases τ, auto)
          from * have src: "source τ2 = source τ" by simp
          have 2: "(a, ?c) ∈ transition_step_lts P' τ2" unfolding a
            by (insert skip_transition_step[OF t2(2) sa, unfolded src t2'']
              lc * a b ab, cases τ, auto)
          show "(a,b) ∈ P'.traverse {?t1, τ2}" by 
            (intro P'.mem_traverseI[of "λ i. if i = 0 then a else if i = 1 then ?c else b" _ "Suc (Suc 0)"], 
            force+, intro P'.traversed.intros, insert 1 2, auto)        
        qed
        with * t2 show ?thesis by (intro exI[of _ "{ ?t1, τ2}"], auto)
      qed
    qed
  next
    fix τ
    assume mem: "τ ∈ flat_transitions_of P"
    with lc[of "source τ"] lc[of "target τ"]
    have lc: "assertion P' (source τ) = assertion P (source τ)" 
      "assertion P' (target τ) = assertion P (target τ)" 
      unfolding nodes_lts_def by auto
    then show "transition_step_lts P τ = transition_step_lts P' τ" by (cases τ, auto)
  qed
qed

  
lemma add_new_sharp_location_incoming:  
  assumes sharp_new: "⋀ τ. τ ∈ sharp_transitions_of P - sharp_transitions_of P' ⟹ 
    ∃ τ' l. change_target l τ ∈ sharp_transitions_of P' ∧ τ' ∈ sharp_transitions_of P' 
        ∧ skip_transition τ' 
        ∧ source τ' = l ∧ target τ' = target τ 
        ∧ assertion P' l = assertion P (target τ)" 
  shows "cooperation_SN P" 
  by (rule add_new_sharp_location_in_out, insert sharp_new, blast)
    
lemma add_new_sharp_location_outgoing:  
  assumes sharp_new: "⋀ τ. τ ∈ sharp_transitions_of P - sharp_transitions_of P' ⟹ 
    ∃ τ' l. change_source l τ ∈ sharp_transitions_of P' ∧ τ' ∈ sharp_transitions_of P' 
        ∧ skip_transition τ'       
        ∧ source τ' = source τ ∧ target τ' = l 
        ∧ assertion P' l = assertion P (source τ)" 
  shows "cooperation_SN P" 
  by (rule add_new_sharp_location_in_out, insert sharp_new, blast)
end
end

context pre_lts_checker
begin
fun location_addition_incoming where
  "location_addition_incoming P (Location_Addition_Info new old skip_ID skip) = (do {
      check (new ∉ set (nodes_lts_impl P)) (showsl_lit (STR ''location-id '') o showsl new o showsl_lit (STR '' is not fresh''));
      check (is_sharp new) (showsl_lit (STR ''new location '') o showsl new o showsl_lit (STR '' must be sharp location'')); 
      check (is_sharp old) (showsl_lit (STR ''copied location '') o showsl old o showsl_lit (STR '' must be sharp location'')); 
      check (transition_rule skip) (showsl_lit (STR ''new transition '') o showsl skip_ID o showsl_lit (STR '' seems to be ill-formed''));
      check_skip_transition skip <+? (λ s. showsl_lit (STR ''new transition '') o showsl skip_ID o showsl_lit (STR '' must be skip transition⏎'') o s); 
      check (source skip = new ∧ target skip = old) (showsl_lit (STR ''new skip transition '') o showsl skip_ID o showsl_lit (STR '' must be from '')
        o showsl new o showsl_lit (STR '' to '') o showsl old);
      let trans = lts_impl.transitions_impl P;
      let (sharp, flat) = partition (λ tau. is_sharp_transition (snd tau)) trans;
      let (sharp_modify, sharp_keep) = partition (λ tau. target (snd tau) = old) sharp;
      let Q = Lts_Impl (lts_impl.initial P) ((skip_ID, skip) # 
         flat @ sharp_keep @ map (λ tau. (fst tau, change_target new (snd tau))) sharp_modify)
         ((new, assertion_of P old) # assertion_impl P);
      check_allm (λ l. check (assertion_of P l =
        assertion_of Q l) (showsl_lit (STR ''location condition of initial state '') o showsl l o showsl_lit (STR '' has been changed''))) (lts_impl.initial P);
      return Q
    })" 

fun location_addition_outgoing where
  "location_addition_outgoing P (Location_Addition_Info old new skip_ID skip) = (do {
      check (new ∉ set (nodes_lts_impl P)) (showsl_lit (STR ''location-id '') o showsl new o showsl_lit (STR '' is not fresh''));
      check (is_sharp new) (showsl_lit (STR ''new location '') o showsl new o showsl_lit (STR '' must be sharp location'')); 
      check (is_sharp old) (showsl_lit (STR ''copied location '') o showsl old o showsl_lit (STR '' must be sharp location'')); 
      check (transition_rule skip) (showsl_lit (STR ''new transition '') o showsl skip_ID o showsl_lit (STR '' seems to be ill-formed''));
      check_skip_transition skip <+? (λ s. showsl_lit (STR ''new transition '') o showsl skip_ID o showsl_lit (STR '' must be skip transition⏎'') o s); 
      check (source skip = old ∧ target skip = new) (showsl_lit (STR ''new skip transition '') o showsl skip_ID o showsl_lit (STR '' must be from '')
        o showsl old o showsl_lit (STR '' to '') o showsl new);
      let trans = lts_impl.transitions_impl P;
      let (sharp, flat) = partition (λ tau. is_sharp_transition (snd tau)) trans;
      let (sharp_modify, sharp_keep) = partition (λ tau. source (snd tau) = old) sharp;
      let Q = Lts_Impl (lts_impl.initial P) ((skip_ID, skip) # 
         flat @ sharp_keep @ map (λ tau. (fst tau, change_source new (snd tau))) sharp_modify)
         ((new, assertion_of P old) # assertion_impl P); 
      check_allm (λ l. check (assertion_of P l =
        assertion_of Q l) (showsl_lit (STR ''location condition of initial state '') o showsl l o showsl_lit (STR '' has been changed''))) (lts_impl.initial P);
      return Q
    })" 
  
definition location_addition where
  "location_addition P info = (case info of Location_Addition_Info src tgt _ _ ⇒ if
     src ∉ set (nodes_lts_impl P) 
    then location_addition_incoming P info 
    else location_addition_outgoing P info)"
  
end

declare pre_lts_checker.location_addition_incoming.simps[code]
declare pre_lts_checker.location_addition_outgoing.simps[code]
declare pre_lts_checker.location_addition_def[code]

lemma filter_mset_union:
  shows "filter_mset f M + filter_mset g M = filter_mset (λx. f x ∨ g x) M + filter_mset (λx. f x ∧ g x) M"
  by(fold count_inject, auto)

lemma mset_filter_union:
  "mset (filter f xs) + mset (filter g xs) = mset (filter (λx. f x ∨ g x) xs) + mset (filter (λx. f x ∧ g x) xs)"
proof-
  have "mset (filter f xs) + mset (filter g xs) = filter_mset f (mset xs) + filter_mset g (mset xs)" by (simp add: mset_filter)
  also have "... = filter_mset (λx. f x ∨ g x) (mset xs) + filter_mset (λx. f x ∧ g x) (mset xs)"
    by (rule filter_mset_union)
  finally show ?thesis by (simp add: mset_filter)
qed

context lts_checker
begin

lemma location_addition_incoming: assumes SN: "cooperation_SN_impl Q"
  and la: "location_addition_incoming P info = return Q"
shows "cooperation_SN_impl P"
proof (cases info)
  case (Location_Addition_Info new old skip_ID skip)
  note la = la[unfolded this]
  note la = la[simplified, unfolded Let_def o_def, simplified]
  from la have Q: "Q = Lts_Impl (lts_impl.initial P)
   ((skip_ID, skip) #
    [tau←transitions_impl P . ¬ is_sharp_transition (snd tau)] @
    [x←transitions_impl P . is_sharp_transition (snd x) ∧ target (snd x) ≠ old] @
    map (λtau. (fst tau, change_target new (snd tau))) [x←transitions_impl P . is_sharp_transition (snd x) ∧ target (snd x) = old])
    ( (new, assertion_of P old) # assertion_impl P)" by auto
  from la have "isOK(check_skip_transition skip)" by auto
  from check_skip_transition[OF this] la
  have skip: "skip_transition skip" "transition_rule skip" by auto
  from la have sharp_skip: "skip ∈ sharp_transitions_of (lts_of Q)" by (cases skip; auto)
  then have flat_skip: "is_sharp_transition skip" by (cases skip; cases "source skip", auto)
  show ?thesis
  proof (intro cooperation_SN_implI)
    assume P: "lts_impl P"
    then have impl: "lts_impl Q"
    proof (intro lts_implI)
      show "(tr, τ) ∈ set (transitions_impl Q) ⟹ transition_rule τ" for tr τ
        using P skip(2) by (auto elim!: lts_implE simp: Q)
      show "(l, φ) ∈ set (assertion_impl Q) ⟹ formula φ " for l φ
        using P by (auto elim!: lts_implE simp: Q assertion_of_def intro: map_of_defaultI)
    qed
    show "cooperation_SN (lts_of P)"
    proof (rule add_new_sharp_location_incoming)
      show "cooperation_SN (lts_of Q)" using SN impl by (elim cooperation_SN_implE)
      show "lts.initial (lts_of Q) = lts.initial (lts_of P)" by (auto simp: Q)
      show "flat_transitions_of (lts_of Q) = flat_transitions_of (lts_of P)" by (auto simp: flat_skip Q)
      show "l ∈ lts.initial (lts_of P) ⟹ assertion (lts_of P) l = assertion (lts_of Q) l" for l using la by auto
      fix τ
      assume "τ ∈ sharp_transitions_of (lts_of P) - sharp_transitions_of (lts_of Q)" 
      then have tau: "target τ = old" "change_target new τ ∈ sharp_transitions_of (lts_of Q)" unfolding Q by auto
      have lc: "assertion (lts_of Q) new = assertion (lts_of P) old" 
        unfolding Q 
        by (auto simp: assertion_of_def map_of_default_def lookup_default_def lookup_of_alist)
      show "∃τ' l. change_target l τ ∈ sharp_transitions_of (lts_of Q) ∧
                τ' ∈ sharp_transitions_of (lts_of Q) ∧ skip_transition τ' ∧ source τ' = l ∧ target τ' = target τ
             ∧ assertion (lts_of Q) l = assertion (lts_of P) (target τ)" 
        by (intro exI conjI, rule tau(2), rule sharp_skip, rule skip, unfold tau, insert la lc, auto)
    next
      fix l 
      assume "l ∈ nodes_lts (lts_of P)" 
      with la have "l ≠ new" by auto
      then show "assertion (lts_of Q) l = assertion (lts_of P) l"
        by (auto simp: Q map_of_default_def lookup_default_def assertion_of_def lookup_of_alist)
    qed
  qed
qed

lemma location_addition_outgoing: assumes SN: "cooperation_SN_impl Q"
  and la: "location_addition_outgoing P info = return Q"
shows "cooperation_SN_impl P"
proof (cases info)
  case (Location_Addition_Info old new skip_ID skip) 
  note la = la[unfolded this]
  note la = la[simplified, unfolded Let_def o_def, simplified]
  from la have Q: "Q = Lts_Impl (lts_impl.initial P)
   ((skip_ID, skip) #
    [tau←transitions_impl P . ¬ is_sharp_transition (snd tau)] @
    [x←transitions_impl P . is_sharp_transition (snd x) ∧ source (snd x) ≠ old] @
    map (λtau. (fst tau, change_source new (snd tau))) [x←transitions_impl P . is_sharp_transition (snd x) ∧ source (snd x) = old])
    ( (new, assertion_of P old) # assertion_impl P)" by auto
  from la have "isOK(check_skip_transition skip)" by auto
  from check_skip_transition[OF this] la
  have skip: "skip_transition skip" "transition_rule skip" by auto
  from la have sharp_skip: "skip ∈ sharp_transitions_of (lts_of Q)" by (cases skip; auto)
  then have flat_skip: "is_sharp_transition skip" by (cases skip; cases "source skip", auto)
  show ?thesis
  proof
    assume P: "lts_impl P"
    then have impl: "lts_impl Q"
    proof (intro lts_implI)
      show "(tr, τ) ∈ set (transitions_impl Q) ⟹ transition_rule τ" for tr τ
        using P skip(2) by (auto elim!: lts_implE simp: Q)
      show "(l, φ) ∈ set (assertion_impl Q) ⟹ formula φ " for l φ
        using P by (auto elim!: lts_implE simp: Q assertion_of_def intro: map_of_defaultI)
    qed
    show "cooperation_SN (lts_of P)"
    proof (rule add_new_sharp_location_outgoing)
      show "cooperation_SN (lts_of Q)" using impl SN by auto
      show "lts.initial (lts_of Q) = lts.initial (lts_of P)" by (auto simp: Q)
      from la have sharp_new: "is_sharp new" by auto
      then show "flat_transitions_of (lts_of Q) = flat_transitions_of (lts_of P)" by (auto simp: flat_skip Q)
      show "l ∈ lts.initial (lts_of P) ⟹ assertion (lts_of P) l = assertion (lts_of Q) l" for l using la by auto
      fix τ
      assume "τ ∈ sharp_transitions_of (lts_of P) - sharp_transitions_of (lts_of Q)" 
      with sharp_new have tau: "source τ = old" "change_source new τ ∈ sharp_transitions_of (lts_of Q)" unfolding Q by auto
      have lc: "assertion (lts_of Q) new = assertion (lts_of P) old" 
        unfolding Q 
        by (auto simp: assertion_of_def map_of_default_def lookup_default_def lookup_of_alist)
      show "∃τ' l. change_source l τ ∈ sharp_transitions_of (lts_of Q) ∧
                τ' ∈ sharp_transitions_of (lts_of Q) ∧ skip_transition τ' ∧ source τ' = source τ ∧ target τ' = l
             ∧ assertion (lts_of Q) l = assertion (lts_of P) (source τ)" 
        by (intro exI conjI, rule tau(2), rule sharp_skip, rule skip, unfold tau, insert la lc, auto)
    next
      fix l 
      assume "l ∈ nodes_lts (lts_of P)" 
      with la have "l ≠ new" by auto
      then show "assertion (lts_of Q) l = assertion (lts_of P) l"
        by (auto simp: Q map_of_default_def lookup_default_def assertion_of_def lookup_of_alist)
    qed
  qed
qed

lemma location_addition: assumes SN: "cooperation_SN_impl Q"
  and la: "location_addition P info = return Q"
shows "cooperation_SN_impl P"
proof (cases info)
  case (Location_Addition_Info src)
  from la[unfolded location_addition_def this location_addition_info.simps, folded this]
    location_addition_incoming location_addition_outgoing SN
  show ?thesis by (auto split: if_splits)
qed

end

end