Theory ConsInterleave

(*  Title:       Conflict analysis/Monitor Consistent Interleaving
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)
section "Monitor Consistent Interleaving"
theory ConsInterleave
imports Interleave Misc
begin
text_raw ‹\label{thy:ConsInterleave}›

text ‹The monitor consistent interleaving operator is defined on two lists of arbitrary elements, provided an abstraction function @{term α} that maps list elements to pairs of sets of monitors is available.
  @{term "α e = (M,M')"} intuitively means that step @{term e} enters the monitors in @{term M} and passes (enters and leaves) the monitors in @{term M'}.
  The consistent interleaving describes all interleavings of the two lists that are consistent w.r.t. the monitor usage. 
›

subsection "Monitors of lists of monitor pairs"
text ‹The following defines the set of all monitors that occur in a list of pairs of monitors. This definition is used in the following context:
  ‹mon_pl (map α w)› is the set of monitors used by a word ‹w› w.r.t. the abstraction ‹α››
definition 
  "mon_pl w == foldl (∪) {} (map (λe. fst e ∪ snd e) w)"

lemma mon_pl_empty[simp]: "mon_pl [] = {}"
  by (unfold mon_pl_def, auto)
lemma mon_pl_cons[simp]: "mon_pl (e#w) = fst e ∪ snd e ∪ mon_pl w"
  by (unfold mon_pl_def) (simp, subst foldl_un_empty_eq, auto)

lemma mon_pl_unconc: "!!b. mon_pl (a@b) = mon_pl a ∪ mon_pl b"
  by (induct a) auto

lemma mon_pl_ileq: "w≼w' ⟹ mon_pl w ⊆ mon_pl w'"
  by (induct rule: less_eq_list_induct) auto

lemma mon_pl_set: "mon_pl w = ⋃{ fst e ∪ snd e | e. e∈set w }"
  by (auto simp add: mon_pl_def foldl_set) blast+

fun
  cil :: "'a list ⇒ ('a ⇒ ('m set × 'm set)) ⇒ 'a list ⇒ 'a list set" 
    ("_ ⊗⇘_⇙ _" [64,64,64] 64) where
  ― ‹Interleaving with the empty word results in the empty word›
  "[] ⊗⇘α ⇙ w = {w}" 
  | "w ⊗⇘α⇙ [] = {w}"
  ― ‹If both words are not empty, we can take the first step of one word, 
  interleave the rest with the other word and then append
  the first step to all result set elements, provided it does not allocate 
  a monitor that is used by the other word›
  | "e1#w1 ⊗⇘α⇙ e2#w2 = (
    if fst (α e1) ∩ mon_pl (map α (e2#w2)) = {} then 
      e1⋅(w1 ⊗⇘α⇙ e2#w2) 
    else {}
  ) ∪ (
    if fst (α e2) ∩ mon_pl (map α (e1#w1)) = {} then 
      e2⋅(e1#w1 ⊗⇘α⇙ w2) 
    else {}
  )"

text ‹Note that this definition allows reentrant monitors, because it only checks that a monitor that is going to be entered by one word is not used in the {\em other} word. Thus the same word may enter the same monitor
  multiple times.›

text ‹The next lemmas are some auxiliary lemmas to simplify the handling of the consistent interleaving operator.›
lemma cil_last_case_split[cases set, case_names left right]: "
  ⟦ w∈e1#w1 ⊗⇘α⇙ e2#w2; 
    !!w'. ⟦w=e1#w'; w'∈(w1 ⊗⇘α⇙ e2#w2); 
           fst (α e1) ∩ mon_pl (map α (e2#w2)) = {} ⟧ ⟹ P;
    !!w'. ⟦w=e2#w'; w'∈(e1#w1 ⊗⇘α⇙ w2); 
           fst (α e2) ∩ mon_pl (map α (e1#w1)) = {} ⟧ ⟹ P
  ⟧ ⟹ P"
  by (auto elim: list_set_cons_cases split: if_split_asm)

lemma cil_cases[cases set, case_names both_empty left_empty right_empty app_left app_right]: "
  ⟦ w∈wa⊗⇘α⇙wb; 
    ⟦ w=[]; wa=[]; wb=[] ⟧ ⟹ P; 
    ⟦wa=[]; w=wb⟧ ⟹ P; 
    ⟦ w=wa; wb=[] ⟧ ⟹ P; 
    !!ea wa' w'. ⟦w=ea#w'; wa=ea#wa'; w'∈wa'⊗⇘α⇙wb; 
                  fst (α ea) ∩ mon_pl (map α wb) = {}  ⟧ ⟹ P;
    !!eb wb' w'. ⟦w=eb#w'; wb=eb#wb'; w'∈wa⊗⇘α⇙wb'; 
                  fst (α eb) ∩ mon_pl (map α wa) = {}  ⟧ ⟹ P
  ⟧ ⟹ P"
proof (induct wa α wb rule: cil.induct)
  case 1 thus ?case by simp next
  case 2 thus ?case by simp next
  case (3 ea wa' α eb wb') 
  from "3.prems"(1) show ?thesis proof (cases rule: cil_last_case_split)
    case (left w') from "3.prems"(5)[OF left(1) _ left(2,3)] show ?thesis by simp next
    case (right w') from "3.prems"(6)[OF right(1) _ right(2,3)] show ?thesis by simp
  qed
qed

lemma cil_induct'[case_names both_empty left_empty right_empty append]: "⟦
  ⋀α. P α [] []; 
  ⋀α ad ae. P α [] (ad # ae); 
  ⋀α z aa. P α (z # aa) [];
  ⋀α e1 w1 e2 w2. ⟦
    ⟦fst (α e1) ∩ mon_pl (map α (e2 # w2)) = {}⟧ ⟹ P α w1 (e2 # w2); 
    ⟦fst (α e2) ∩ mon_pl (map α (e1 # w1)) = {}⟧ ⟹ P α (e1 # w1) w2⟧ 
  ⟹ P α (e1 # w1) (e2 # w2)
  ⟧ ⟹ P α wa wb"
  apply (induct wa α wb rule: cil.induct)
  apply (case_tac w)
  apply auto
  done
  
lemma cil_induct_fixα: "⟦
  P α [] []; 
  ⋀ad ae. P α [] (ad # ae); 
  ⋀z aa. P α (z # aa) [];
  ⋀e1 w1 e2 w2.
    ⟦fst (α e2) ∩ mon_pl (map α (e1 # w1)) = {} ⟶ P α (e1 # w1) w2;
     fst (α e1) ∩ mon_pl (map α (e2 # w2)) = {} ⟶ P α w1 (e2 # w2)⟧
     ⟹ P α (e1 # w1) (e2 # w2)⟧
  ⟹ P α v w"
  apply (induct v α w rule: cil.induct)
  apply (case_tac w)
  apply auto
  done

lemma cil_induct_fixα'[case_names both_empty left_empty right_empty append]: "⟦
  P α [] []; 
  ⋀ad ae. P α [] (ad # ae); 
  ⋀z aa. P α (z # aa) [];
  ⋀e1 w1 e2 w2. ⟦
    fst (α e1) ∩ mon_pl (map α (e2 # w2)) = {} ⟹ P α w1 (e2 # w2);
    fst (α e2) ∩ mon_pl (map α (e1 # w1)) = {} ⟹ P α (e1 # w1) w2⟧ 
    ⟹ P α (e1 # w1) (e2 # w2)
  ⟧ ⟹ P α wa wb"
  apply (induct wa α wb rule: cil.induct)
  apply (case_tac w)
  apply auto
  done

lemma [simp]: "w⊗⇘α⇙[] = {w}"
  by (cases w, auto)

lemma cil_contains_empty[rule_format, simp]: "([] ∈ wa⊗⇘α⇙wb) = (wa=[] ∧ wb=[])"
  by (induct wa α wb rule: cil.induct) auto

lemma cil_cons_cases[cases set, case_names left right]: "⟦ e#w ∈ w1⊗⇘α⇙w2; 
  !!w1'. ⟦w1=e#w1'; w∈w1'⊗⇘α⇙w2; fst (α e) ∩ mon_pl (map α w2) = {} ⟧ ⟹ P;
  !!w2'. ⟦w2=e#w2'; w∈w1⊗⇘α⇙w2'; fst (α e) ∩ mon_pl (map α w1) = {} ⟧ ⟹ P
⟧ ⟹ P" 
  by (cases rule: cil_cases) auto

lemma cil_set_induct[induct set, case_names empty left right]: "!!α w1 w2. ⟦ 
    w∈w1⊗⇘α⇙w2; 
    !!α. P [] α [] []; 
    !!α e w' w1' w2. ⟦w'∈w1'⊗⇘α⇙w2; fst (α e) ∩ mon_pl (map α w2) = {}; 
                      P w' α w1' w2 ⟧ ⟹ P (e#w') α (e#w1') w2;
    !!α e w' w2' w1. ⟦w'∈w1⊗⇘α⇙w2'; fst (α e) ∩ mon_pl (map α w1) = {}; 
                      P w' α w1 w2' ⟧ ⟹ P (e#w') α w1 (e#w2')
  ⟧ ⟹ P w α w1 w2" 
  by (induct w) (auto intro!: cil_contains_empty elim: cil_cons_cases)

lemma cil_set_induct_fixα[induct set, case_names empty left right]: "!!w1 w2. ⟦ 
    w∈w1⊗⇘α⇙w2; 
    P [] α [] []; 
    !!e w' w1' w2. ⟦w'∈w1'⊗⇘α⇙w2; fst (α e) ∩ mon_pl (map α w2) = {}; 
                    P w' α w1' w2 ⟧ ⟹ P (e#w') α (e#w1') w2;
    !!e w' w2' w1. ⟦w'∈w1⊗⇘α⇙w2'; fst (α e) ∩ mon_pl (map α w1) = {}; 
                    P w' α w1 w2' ⟧ ⟹ P (e#w') α w1 (e#w2')
  ⟧ ⟹ P w α w1 w2" 
  by (induct w) (auto intro!: cil_contains_empty elim: cil_cons_cases)

lemma cil_cons1: "⟦w∈wa⊗⇘α⇙wb; fst (α e) ∩ mon_pl (map α wb) = {}⟧ 
                  ⟹ e#w ∈ e#wa ⊗⇘α⇙ wb"
  by (cases wb) auto
lemma cil_cons2: "⟦w∈wa⊗⇘α⇙wb; fst (α e) ∩ mon_pl (map α wa) = {}⟧ 
                  ⟹ e#w ∈ wa ⊗⇘α⇙ e#wb"
  by (cases wa) auto

subsection "Properties of consistent interleaving"

― ‹Consistent interleaving is a restriction of interleaving›
lemma cil_subset_il: "w⊗⇘α⇙w' ⊆ w⊗w'"
  apply (induct w α w' rule: cil.induct)
  apply simp_all
  apply safe
  apply auto
  done

lemma cil_subset_il': "w∈w1⊗⇘α⇙w2 ⟹ w∈w1⊗w2" 
  using cil_subset_il by (auto)

― ‹Consistent interleaving preserves the set of letters of both operands›
lemma cil_set: "w∈w1⊗⇘α⇙w2 ⟹ set w = set w1 ∪ set w2"
  by (induct rule: cil_set_induct_fixα) auto
corollary cil_mon_pl: "w∈w1⊗⇘α⇙w2 
  ⟹ mon_pl (map α w) = mon_pl (map α w1) ∪ mon_pl (map α w2)" 
  by (subst mon_pl_unconc[symmetric]) (simp add: mon_pl_set cil_set, blast 20)

― ‹Consistent interleaving preserves the length of both operands›
lemma cil_length[rule_format]: "∀w∈wa⊗⇘α⇙wb. length w = length wa + length wb"
  by (induct rule: cil.induct) auto

― ‹Consistent interleaving contains all letters of each operand in the original order›
lemma cil_ileq: "w∈w1⊗⇘α⇙w2 ⟹ w1≼w ∧ w2≼w"
  by (intro conjI cil_subset_il' ileq_interleave)

― ‹Consistent interleaving is commutative and associative›
lemma cil_commute: "w⊗⇘α⇙w' = w'⊗⇘α⇙w"
  by (induct rule: cil.induct) auto

lemma cil_assoc1: "!!wl w1 w2 w3. ⟦ w∈wl⊗⇘α⇙w3; wl∈w1⊗⇘α⇙w2 ⟧ 
  ⟹ ∃wr. w∈w1⊗⇘α⇙wr ∧ wr∈w2⊗⇘α⇙w3" 
proof (induct w rule: length_compl_induct)
  case Nil thus ?case by auto
next
  case (Cons e w) from Cons.prems(1) show ?case proof (cases rule: cil_cons_cases)
    case (left wl') with Cons.prems(2) have "e#wl' ∈ w1⊗⇘α⇙w2" by simp
    thus ?thesis proof (cases rule: cil_cons_cases[case_names left' right'])
      case (left' w1')
      from Cons.hyps[OF _ left(2) left'(2)] obtain wr where IHAPP: "w ∈ w1' ⊗⇘α⇙ wr" "wr ∈ w2 ⊗⇘α⇙ w3" by blast
      have "e#w∈e#w1'⊗⇘α⇙wr" proof (rule cil_cons1[OF IHAPP(1)])
        from left left' cil_mon_pl[OF IHAPP(2)] show "fst (α e) ∩ mon_pl (map α wr) = {}" by auto
      qed
      thus ?thesis using IHAPP(2) left' by blast
    next
      case (right' w2') from Cons.hyps[OF _ left(2) right'(2)] obtain wr where IHAPP: "w ∈ w1 ⊗⇘α⇙ wr" "wr ∈ w2' ⊗⇘α⇙ w3" by blast
      from IHAPP(2) left have "e#wr ∈ e#w2' ⊗⇘α⇙ w3" by (auto intro: cil_cons1)
      moreover from right' IHAPP(1) have "e#w ∈ w1 ⊗⇘α⇙ e#wr" by (auto intro: cil_cons2)
      ultimately show ?thesis using right' by blast
    qed
  next
    case (right w3') from Cons.hyps[OF _ right(2) Cons.prems(2)] obtain wr where IHAPP: "w ∈ w1 ⊗⇘α⇙ wr" "wr ∈ w2 ⊗⇘α⇙ w3'" by blast
    from IHAPP(2) right cil_mon_pl[OF Cons.prems(2)] have "e#wr ∈ w2 ⊗⇘α⇙ e#w3'" by (auto intro: cil_cons2)
    moreover from IHAPP(1) right cil_mon_pl[OF Cons.prems(2)] have "e#w ∈ w1 ⊗⇘α⇙ e#wr" by (auto intro: cil_cons2)
    ultimately show ?thesis using right by blast
  qed
qed
    
lemma cil_assoc2: 
  assumes A: "w∈w1⊗⇘α⇙wr" and B: "wr∈w2⊗⇘α⇙w3" 
  shows "∃wl. w∈wl⊗⇘α⇙w3 ∧ wl∈w1⊗⇘α⇙w2" 
proof -
  from A have A': "w∈wr⊗⇘α⇙w1" by (simp add: cil_commute)
  from B have B': "wr∈w3⊗⇘α⇙w2" by (simp add: cil_commute)
  from cil_assoc1[OF A' B'] obtain wl where "w ∈ w3 ⊗⇘α⇙ wl ∧ wl ∈ w2 ⊗⇘α⇙ w1" by blast
  thus ?thesis by (auto simp add: cil_commute)
qed


― ‹Parts of the abstraction can be moved to the operands›
(* FIXME: ?? Something strange is going on with the simplification of α∘f and implicit η-contraction/expansion, hence this lengthy isar proof. Usually, this proof should be a just few lines apply-script !*)
lemma cil_map: "w∈w1 ⊗⇘(α∘f)⇙ w2 ⟹ map f w ∈ map f w1 ⊗⇘α⇙ map f w2" 
proof (induct rule: cil_set_induct_fixα)
  case empty thus ?case by auto
next
  case (left e w' w1' w2) 
  have "f e # map f w' ∈ f e # map f w1' ⊗⇘α⇙ map f w2" proof (rule cil_cons1)
    from left(2) have "fst ((α∘f) e) ∩ mon_pl (map α (map f w2)) = {}" by (simp only: map_map[symmetric])
    thus "fst (α (f e)) ∩ mon_pl (map α (map f w2)) = {}" by (simp only: o_apply)
  qed (rule left(3))
  thus ?case by simp
next
  case (right e w' w2' w1) 
  have "f e # map f w' ∈ map f w1 ⊗⇘α⇙ f e # map f w2'" proof (rule cil_cons2)
    from right(2) have "fst ((α∘f) e) ∩ mon_pl (map α (map f w1)) = {}" by (simp only: map_map[symmetric])
    thus "fst (α (f e)) ∩ mon_pl (map α (map f w1)) = {}" by (simp only: o_apply)
  qed (rule right(3))
  thus ?case by simp
qed



end