Theory Semantics

(*  Title:       Conflict analysis/Operational Semantics
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)
section "Operational Semantics"
theory Semantics
imports Main Flowgraph "HOL-Library.Multiset" LTS Interleave ThreadTracking
begin
text_raw ‹\label{thy:Semantics}›

subsection "Configurations and labels"
text ‹
  The state of a single thread is described by a stack of control nodes. The top node is the current control node and the nodes deeper in the stack are stored return addresses. 
  The configuration of a whole program is described by a multiset of stacks. 

  Note that we model stacks as lists here, the first element being the top element.
›
type_synonym 'n conf = "('n list) multiset"

text ‹
  A step is labeled according to the executed edge. Additionally, we introduce a label for a procedure return step, that has no corresponding edge. 
›
datatype ('p,'ba) label = LBase 'ba | LCall 'p | LRet | LSpawn 'p

subsection ‹Monitors›
text ‹
  The following defines the monitors of nodes, stacks, configurations, step labels and paths (sequences of step labels)
›
definition
  ― ‹The monitors of a node are the monitors the procedure of the node synchronizes on›
  "mon_n fg n == mon fg (proc_of fg n)"

definition
  ― ‹The monitors of a stack are the monitors of all its nodes›
  "mon_s fg s == ⋃ { mon_n fg n | n . n ∈ set s }"

definition
  ― ‹The monitors of a configuration are the monitors of all its stacks›
  "mon_c fg c == ⋃ { mon_s fg s | s . s ∈# c }"

― ‹The monitors of a step label are the monitors of procedures that are called by this step›
definition mon_e :: "('b, 'c, 'd, 'a, 'e) flowgraph_rec_scheme ⇒ ('c, 'f) label ⇒ 'a set" where
  "mon_e fg e = (case e of (LCall p) ⇒ mon fg p | _ ⇒ {})"

lemma mon_e_simps [simp]:
  "mon_e fg (LBase a) = {}"
  "mon_e fg (LCall p) = mon fg p"
  "mon_e fg (LRet) = {}"
  "mon_e fg (LSpawn p) = {}"
  by (simp_all add: mon_e_def)

― ‹The monitors of a path are the monitors of all procedures that are called on the path›
definition
  "mon_w fg w == ⋃ { mon_e fg e | e. e ∈ set w}"

lemma mon_s_alt: "mon_s fg s == ⋃ (mon fg ` proc_of fg ` set s)"
  by (unfold mon_s_def mon_n_def) (auto intro!: eq_reflection)
lemma mon_c_alt: "mon_c fg c == ⋃ (mon_s fg ` set_mset c)"
  by (unfold mon_c_def set_mset_def) (auto intro!: eq_reflection)
lemma mon_w_alt: "mon_w fg w == ⋃ (mon_e fg ` set w)"
  by (unfold mon_w_def) (auto intro!: eq_reflection)

lemma mon_sI: "⟦n∈set s; m∈mon_n fg n⟧ ⟹ m∈mon_s fg s"
  by (unfold mon_s_def, auto)
lemma mon_sD: "m∈mon_s fg s ⟹ ∃n∈set s. m∈mon_n fg n"
  by (unfold mon_s_def, auto)

lemma mon_n_same_proc: 
  "proc_of fg n = proc_of fg n' ⟹ mon_n fg n = mon_n fg n'"
  by (unfold mon_n_def, simp)
lemma mon_s_same_proc: 
  "proc_of fg ` set s = proc_of fg ` set s' ⟹ mon_s fg s = mon_s fg s'"
  by (unfold mon_s_alt, simp)

lemma (in flowgraph) mon_of_entry[simp]: "mon_n fg (entry fg p) = mon fg p"
  by (unfold mon_n_def, simp add: entry_valid)
lemma (in flowgraph) mon_of_ret[simp]: "mon_n fg (return fg p) = mon fg p"
  by (unfold mon_n_def, simp add: return_valid)

lemma mon_c_single[simp]: "mon_c fg {#s#} = mon_s fg s"
  by (unfold mon_c_def) auto
lemma mon_s_single[simp]: "mon_s fg [n] = mon_n fg n"
  by (unfold mon_s_def) auto
lemma mon_s_empty[simp]: "mon_s fg [] = {}"
  by (unfold mon_s_def) auto
lemma mon_c_empty[simp]: "mon_c fg {#} = {}"
  by (unfold mon_c_def) auto

lemma mon_s_unconc: "mon_s fg (a@b) = mon_s fg a ∪ mon_s fg b"
  by (unfold mon_s_def) auto
lemma mon_s_uncons[simp]: "mon_s fg (a#as) = mon_n fg a ∪ mon_s fg as"
  by (rule mon_s_unconc[where a="[a]", simplified])

lemma mon_c_union_conc: "mon_c fg (a+b) = mon_c fg a ∪ mon_c fg b"
  by (unfold mon_c_def) auto

lemma mon_c_add_mset_unconc: "mon_c fg (add_mset x b) = mon_s fg x ∪ mon_c fg b"
  by (unfold mon_c_def) auto

lemmas mon_c_unconc = mon_c_union_conc mon_c_add_mset_unconc

lemma mon_cI: "⟦s ∈# c; m∈mon_s fg s⟧ ⟹ m∈mon_c fg c"
  by (unfold mon_c_def, auto)
lemma mon_cD: "⟦m∈mon_c fg c⟧ ⟹ ∃s. s ∈# c ∧ m∈mon_s fg s"
  by (unfold mon_c_def, auto)

lemma mon_s_mono: "set s ⊆ set s' ⟹ mon_s fg s ⊆ mon_s fg s'"
  by (unfold mon_s_def) auto
lemma mon_c_mono: "c⊆#c' ⟹ mon_c fg c ⊆ mon_c fg c'"
  by (unfold mon_c_def) (auto dest: mset_subset_eqD)

lemma mon_w_empty[simp]: "mon_w fg [] = {}"
  by (unfold mon_w_def, auto)
lemma mon_w_single[simp]: "mon_w fg [e] = mon_e fg e"
  by (unfold mon_w_def, auto)
lemma mon_w_unconc: "mon_w fg (wa@wb) = mon_w fg wa ∪ mon_w fg wb"
  by (unfold mon_w_def) auto
lemma mon_w_uncons[simp]: "mon_w fg (e#w) = mon_e fg e ∪ mon_w fg w"
  by (rule mon_w_unconc[where wa="[e]", simplified])
lemma mon_w_ileq: "w≼w' ⟹ mon_w fg w ⊆ mon_w fg w'"
  by (induct rule: less_eq_list_induct) auto



subsection ‹Valid configurations›
text_raw ‹\label{sec:Semantics:validity}›
text ‹We call a configuration {\em valid} if each monitor is owned by at most one thread.›
definition
  "valid fg c == ∀s s'. {#s, s'#} ⊆# c ⟶ mon_s fg s ∩ mon_s fg s' = {}"

lemma valid_empty[simp, intro!]: "valid fg {#}" 
  by (unfold valid_def, auto)

lemma valid_single[simp, intro!]: "valid fg {#s#}" 
  by (unfold valid_def subset_mset_def) auto

lemma valid_split1: 
  "valid fg (c+c') ⟹ valid fg c ∧ valid fg c' ∧ mon_c fg c ∩ mon_c fg c' = {}"
  apply (unfold valid_def)
  apply (auto simp add: mset_le_incr_right)
  apply (drule mon_cD)+
  apply auto
  apply (subgoal_tac "{#s#}+{#sa#} ⊆# c+c'")
  apply (auto dest!: multi_member_split)
  done
  
lemma valid_split2: 
  "⟦valid fg c; valid fg c'; mon_c fg c ∩ mon_c fg c' = {}⟧ ⟹ valid fg (c+c')"
  apply (unfold valid_def)
  apply (intro impI allI)
  apply (erule mset_2dist2_cases)
  apply simp_all
  apply (blast intro: mon_cI)+
  done

lemma valid_union_conc: 
  "valid fg (c+c') ⟷ (valid fg c ∧ valid fg c' ∧ mon_c fg c ∩ mon_c fg c' = {})" 
  by (blast dest: valid_split1 valid_split2)

lemma valid_add_mset_conc: 
  "valid fg (add_mset x c') ⟷ (valid fg c' ∧ mon_s fg x ∩ mon_c fg c' = {})"
  unfolding add_mset_add_single[of x c'] valid_union_conc by (auto simp: mon_s_def)

lemmas valid_unconc = valid_union_conc valid_add_mset_conc

lemma valid_no_mon: "mon_c fg c = {} ⟹ valid fg c" 
proof (unfold valid_def, intro allI impI)
  fix s s'
  assume A: "mon_c fg c = {}" and B: "{#s, s'#} ⊆# c"
  from mon_c_mono[OF B, of fg] A have "mon_s fg s = {}" "mon_s fg s' = {}" by (auto simp add: mon_c_unconc)
  thus "mon_s fg s ∩ mon_s fg s' = {}" by blast
qed

subsection ‹Configurations at control points›

― ‹A stack is {\em at} @{term U} if its top node is from the set @{term U}›
primrec atU_s :: "'n set ⇒ 'n list ⇒ bool" where
  "atU_s U [] = False"
| "atU_s U (u#r) = (u∈U)"

lemma atU_s_decomp[simp]: "atU_s U (s@s') = (atU_s U s ∨ (s=[] ∧ atU_s U s'))"
  by (induct s) auto

― ‹A configuration is {\em at} @{term U} if it contains a stack that is at @{term U}›
definition
  "atU U c == ∃s. s ∈# c ∧ atU_s U s"

lemma atU_fmt: "⟦atU U c; !!ui r. ⟦ui#r ∈# c; ui∈U⟧ ⟹ P⟧ ⟹ P"
  apply (unfold atU_def)
  apply auto
  apply (case_tac s)
  apply auto
  done

lemma atU_union_cases[case_names left right, consumes 1]: "⟦ 
    atU U (c1+c2); 
    atU U c1 ⟹ P; 
    atU U c2 ⟹ P 
  ⟧ ⟹ P"
  by (unfold atU_def) (blast elim: mset_un_cases)

lemma atU_add: "atU U c ⟹ atU U (c+ce) ∧ atU U (ce+c)"
  by (unfold atU_def) (auto simp add: union_ac)

lemma atU_union[simp]: "atU U (c1+c2) = (atU U c1 ∨ atU U c2)"
  by (auto simp add: atU_add elim: atU_union_cases)

lemma atU_empty[simp]: "¬atU U {#}"
  by (unfold atU_def, auto)
lemma atU_single[simp]: "atU U {#s#} = atU_s U s"
  by (unfold atU_def, auto)
lemma atU_single_top[simp]: "atU U {#u#r#} = (u∈U)" 
  by (auto) (* This is also done by atU_single, atU_s.simps *)

lemma atU_add_mset[simp]: "atU U (add_mset c c2) = (atU_s U c ∨ atU U c2)"
  unfolding add_mset_add_single[of c c2] atU_union by auto

lemma atU_xchange_stack: "atU U (add_mset (u#r) c) ⟹ atU U (add_mset (u#r') c)"
  by (simp)

― ‹A configuration is {\em simultaneously at} @{term U} and @{term V} if it contains a stack at @{term U} and another one at @{term V}›
definition 
  "atUV U V c == ∃su sv. {#su#}+{#sv#} ⊆# c ∧ atU_s U su ∧ atU_s V sv"

lemma atUV_empty[simp]: "¬atUV U V {#}"
  by (unfold atUV_def) auto
lemma atUV_single[simp]: "¬atUV U V {#s#}"
  by (unfold atUV_def) auto

lemma atUV_union[simp]: "
  atUV U V (c1+c2) ⟷ 
  (
    (atUV U V c1) ∨ 
    (atUV U V c2) ∨ 
    (atU U c1 ∧ atU V c2) ∨ 
    (atU V c1 ∧ atU U c2)
  )"
  apply (unfold atUV_def atU_def)
  apply (auto elim!: mset_2dist2_cases intro: mset_le_incr_right iff add: mset_le_mono_add_single)
  apply (subst union_commute)
  apply (auto iff add: mset_le_mono_add_single)
  done

lemma atUV_add_mset[simp]: "
  atUV U V (add_mset c c2) ⟷
  (
    (atUV U V c2) ∨
    (atU U {#c#} ∧ atU V c2) ∨
    (atU V {#c#} ∧ atU U c2)
  )"
  unfolding add_mset_add_single[of c c2]
  unfolding atUV_union
  by auto

lemma atUV_union_cases[case_names left right lr rl, consumes 1]: "⟦
    atUV U V (c1+c2); 
    atUV U V c1 ⟹ P; 
    atUV U V c2 ⟹ P; 
    ⟦atU U c1; atU V c2⟧ ⟹ P; 
    ⟦atU V c1; atU U c2⟧ ⟹ P 
  ⟧ ⟹ P"
  by auto

subsection ‹Operational semantics›

subsubsection "Semantic reference point"
text ‹We now define our semantic reference point. We assess correctness and completeness of analyses relative to this reference point.›
inductive_set 
  refpoint :: "('n,'p,'ba,'m,'more) flowgraph_rec_scheme ⇒ 
                 ('n conf × ('p,'ba) label × 'n conf) set"
  for fg
where
  ― ‹A base edge transforms the top node of one stack and leaves the other stacks untouched.›
  refpoint_base: "⟦ (u,Base a,v)∈edges fg; valid fg ({#u#r#}+c) ⟧ 
    ⟹ (add_mset (u#r) c,LBase a,add_mset (v#r) c)∈refpoint fg" |
  ― ‹A call edge transforms the top node of a stack and then pushes the entry node of the called procedure onto that stack. 
      It can only be executed if all monitors the called procedure synchronizes on are available. Reentrant monitors are modeled here by
      checking availability of monitors just against the other stacks, not against the stack of the thread that executes the call. The other stacks are left untouched.›
  refpoint_call: "⟦ (u,Call p,v)∈edges fg; valid fg ({#u#r#}+c); 
                    mon fg p ∩ mon_c fg c = {} ⟧ 
    ⟹ (add_mset (u#r) c,LCall p, add_mset (entry fg p#v#r) c)∈refpoint fg" |
  ― ‹A return step pops a return node from a stack. There is no corresponding flowgraph edge for a return step. The other stacks are left untouched.›
  refpoint_ret: "⟦ valid fg ({#return fg p#r#}+c) ⟧ 
    ⟹ (add_mset (return fg p#r) c,LRet,(add_mset r c))∈refpoint fg" |
  ― ‹A spawn edge transforms the top node of a stack and adds a new stack to the environment, with the entry node of the spawned procedure at the top and no stored return addresses. The other stacks are also left untouched.›
  refpoint_spawn: "⟦ (u,Spawn p,v)∈edges fg; valid fg (add_mset (u#r) c) ⟧ 
    ⟹ (add_mset (u#r) c,LSpawn p, add_mset (v#r) (add_mset [entry fg p] c))∈refpoint fg"

text ‹
  Instead of working directly with the reference point semantics, we define the operational semantics of flowgraphs by describing how a single stack is transformed in a context of environment threads, 
  and then use the theory developed in Section~\ref{thy:ThreadTracking} to derive an interleaving semantics. 
  Note that this semantics is also defined for invalid configurations (cf. Section~\ref{sec:Semantics:validity}). In Section~\ref{sec:Semantics:valid_preserve} we will show that it preserves validity
  of a configuration, and in Section~\ref{sec:Semantics: refpoint_eq} we show that it is equivalent 
  to the reference point semantics on valid configurations.
›

inductive_set
  trss :: "('n,'p,'ba,'m,'more) flowgraph_rec_scheme ⇒ 
             (('n list * 'n conf) * ('p,'ba) label * ('n list * 'n conf)) set"
  for fg
  where
    trss_base: "⟦(u,Base a,v)∈edges fg⟧ ⟹ 
      ((u#r,c), LBase a, (v#r,c) ) ∈ trss fg"
  | trss_call: "⟦(u,Call p,v)∈edges fg; mon fg p ∩ mon_c fg c = {} ⟧ ⟹ 
    ((u#r,c),LCall p, ((entry fg p)#v#r,c)) ∈ trss fg"
  | trss_ret: "((((return fg p)#r),c),LRet,(r,c)) ∈ trss fg"
  | trss_spawn: "⟦ (u,Spawn p,v)∈edges fg ⟧ ⟹ 
    ((u#r,c),LSpawn p,(v#r,add_mset [entry fg p] c)) ∈ trss fg"

(* Not needed
lemma trss_base': "⟦(u,Base a,v)∈edges fg; s=u#r; s'=v#r; e=LBase a⟧ ⟹ ((s,c), e, (s',c) ) ∈ trss fg"
  by (simp add: trss_base)
lemma trss_call': "⟦(u,Call p,v)∈edges fg; mon fg p ∩ mon_c fg c = {}; s=u#r; e=LCall p; s'=(entry fg p)#v#r⟧ ⟹ ((s,c),e, (s',c)) ∈ trss fg"
  by (simp add: trss_call)
lemma trss_ret': "⟦ s=(return fg p)#r; e=LRet ⟧ ⟹ ((s,c),e,(r,c)) ∈ trss fg"
  by (simp add: trss_ret)
lemma trss_spawn': "⟦ (u,Spawn p,v)∈edges fg; s=u#r; e=LSpawn p; s'=v#r; c'={#[entry fg p]#}+c⟧ ⟹ ((s,c),e,(s',c')) ∈ trss fg"
  by (simp add: trss_spawn)
*)

― ‹The interleaving semantics is generated using the general techniques from Section~\ref{thy:ThreadTracking}›
abbreviation tr where "tr fg == gtr (trss fg)"
― ‹We also generate the loc/env-semantics›
abbreviation trp where "trp fg == gtrp (trss fg)"


subsection "Basic properties"
subsubsection "Validity"
text_raw‹\label{sec:Semantics:valid_preserve}›
lemma (in flowgraph) trss_valid_preserve_s: 
  "⟦valid fg (add_mset s c); ((s,c),e,(s',c'))∈trss fg⟧ ⟹ valid fg (add_mset s' c')"
  apply (erule trss.cases)
  apply (simp_all add: valid_unconc mon_c_unconc)
by (blast dest: mon_n_same_proc edges_part)+

lemma (in flowgraph) trss_valid_preserve: 
  "⟦((s,c),w,(s',c'))∈trcl (trss fg); valid fg ({#s#}+c)⟧ ⟹ valid fg ({#s'#}+c')"
  by (induct rule: trcl_pair_induct) (auto intro: trss_valid_preserve_s)

lemma (in flowgraph) tr_valid_preserve_s: 
  "⟦(c,e,c')∈tr fg; valid fg c⟧ ⟹ valid fg c'"
  by (rule gtr_preserve_s[where P="valid fg"]) (auto dest: trss_valid_preserve_s)

lemma (in flowgraph) tr_valid_preserve: 
  "⟦(c,w,c')∈trcl (tr fg); valid fg c⟧ ⟹ valid fg c'"
  by (rule gtr_preserve[where P="valid fg"]) (auto dest: trss_valid_preserve_s)
  
lemma (in flowgraph) trp_valid_preserve_s: 
  "⟦((s,c),e,(s',c'))∈trp fg; valid fg (add_mset s c)⟧ ⟹ valid fg (add_mset s' c')"
  by (rule gtrp_preserve_s[where P="valid fg"]) (auto dest: trss_valid_preserve_s)

lemma (in flowgraph) trp_valid_preserve: 
  "⟦((s,c),w,(s',c'))∈trcl (trp fg); valid fg ({#s#}+c)⟧ ⟹ valid fg (add_mset s' c')"
  by (rule gtrp_preserve[where P="valid fg"]) (auto dest: trss_valid_preserve_s)


subsubsection "Equivalence to reference point"
text_raw ‹\label{sec:Semantics: refpoint_eq}›
― ‹The equivalence between the semantics that we derived using the techniques from Section~\ref{thy:ThreadTracking} and the semantic reference point is shown nearly automatically.›
lemma refpoint_eq_s: "valid fg c ⟹ ((c,e,c')∈refpoint fg) ⟷ ((c,e,c')∈tr fg)"
  apply rule
  apply (erule refpoint.cases)
      apply (auto intro: gtrI_s trss.intros simp add: union_assoc add_mset_commute)
  apply (erule gtrE)
  apply (erule trss.cases)
  apply (auto intro: refpoint.intros simp add: union_assoc[symmetric] add_mset_commute)
  done
  
lemma (in flowgraph) refpoint_eq: 
  "valid fg c ⟹ ((c,w,c')∈trcl (refpoint fg)) ⟷ ((c,w,c')∈trcl (tr fg))" 
proof -
  have "((c,w,c')∈trcl (refpoint fg)) ⟹ valid fg c ⟹ ((c,w,c')∈trcl (tr fg))" by (induct rule: trcl.induct) (auto simp add: refpoint_eq_s tr_valid_preserve_s)
  moreover have "((c,w,c')∈trcl (tr fg)) ⟹ valid fg c ⟹ ((c,w,c')∈trcl (refpoint fg))" by (induct rule: trcl.induct) (auto simp add: refpoint_eq_s tr_valid_preserve_s)
  ultimately show "valid fg c ⟹ ((c,w,c')∈trcl (refpoint fg)) = ((c,w,c')∈trcl (tr fg))" ..
qed

subsubsection ‹Case distinctions›

lemma trss_c_cases_s[cases set, case_names no_spawn spawn]: "⟦ 
    ((s,c),e,(s',c'))∈trss fg; 
    ⟦ c'=c ⟧ ⟹ P; 
    !!p u v. ⟦ e=LSpawn p; (u,Spawn p,v)∈edges fg; 
               hd s=u; hd s'=v; c'={#[ entry fg p ]#}+c ⟧ ⟹ P 
  ⟧ ⟹ P" 
by (auto elim!: trss.cases)
lemma trss_c_fmt_s: "⟦((s,c),e,(s',c'))∈trss fg⟧ 
  ⟹ ∃csp. c'=csp+c ∧ 
        (csp={#} ∨ (∃p. e=LSpawn p ∧ csp={#[ entry fg p ]#}))"
  by (force elim!: trss_c_cases_s)
  
lemma (in flowgraph) trss_c'_split_s: "⟦
    ((s,c),e,(s',c'))∈trss fg; 
    !!csp. ⟦c'=csp+c; mon_c fg csp={}⟧ ⟹ P 
  ⟧ ⟹ P" 
  apply (erule trss_c_cases_s)
  apply (subgoal_tac "c'={#}+c")
  apply (fastforce)
  apply auto
  done

lemma trss_c_cases[cases set, case_names c_case]: "!!s c. ⟦ 
    ((s,c),w,(s',c'))∈trcl (trss fg); 
    !!csp. ⟦ c'=csp+c; !!s. s ∈# csp ⟹ ∃p u v. s=[entry fg p] ∧ 
                                               (u,Spawn p,v)∈edges fg ∧ 
                                               initialproc fg p⟧ 
            ⟹ P 
  ⟧ ⟹ P" 
proof (induct w)
  case Nil note A=this 
  hence "s'=s" "c'=c" by simp_all
  hence "c'={#}+c" by simp
  from A(2)[OF this] show P by simp
next  
  case (Cons e w) note IHP=this
  then obtain sh ch where SPLIT1: "((s,c),e,(sh,ch))∈trss fg" and SPLIT2: "((sh,ch),w,(s',c'))∈trcl (trss fg)" by (fastforce dest: trcl_uncons)
  from SPLIT2 show ?case proof (rule IHP(1))
    fix csp
    assume C'FMT: "c'=csp+ch" and CSPFMT: "!!s. s ∈# csp ⟹ ∃p u v. s=[entry fg p] ∧ (u,Spawn p, v)∈edges fg ∧ initialproc fg p"
    from SPLIT1 show ?thesis
    proof (rule trss_c_cases_s)
      assume "ch=c" with C'FMT CSPFMT IHP(3) show ?case by blast
    next
      fix p
      assume EFMT: "e=LSpawn p" and CHFMT: "ch={#[entry fg p]#}+c" 
      with C'FMT have "c'=({#[entry fg p]#}+csp)+c" by (simp add: union_ac)
      moreover 
      from EFMT SPLIT1 have "∃u v. (u,Spawn p, v)∈edges fg" by (blast elim!: trss.cases)
      hence "!!s. s ∈# {#[entry fg p]#} + csp ⟹ ∃p u v. s=[entry fg p] ∧ (u,Spawn p, v)∈edges fg ∧ initialproc fg p" using CSPFMT by (unfold initialproc_def, erule_tac mset_un_cases) (auto)
      ultimately show ?case using IHP(3) by blast
    qed
  qed
qed

lemma (in flowgraph) c_of_initial_no_mon: 
  assumes A: "!!s. s ∈# csp ⟹ ∃p. s=[entry fg p] ∧ initialproc fg p" 
  shows "mon_c fg csp = {}"
  by (unfold mon_c_def) (auto dest: A initial_no_mon)
  
  (* WARNING: Don't declare this [simp], as c=c' will cause a simplifier loop *)
lemma (in flowgraph) trss_c_no_mon_s: 
  assumes A: "((s,c),e,(s',c'))∈trss fg" 
  shows "mon_c fg c' = mon_c fg c" 
  using A 
proof (erule_tac trss_c_cases_s)
  assume "c'=c" thus ?thesis by simp
next
  fix p assume EFMT: "e=LSpawn p" and C'FMT: "c'={#[entry fg p]#} + c"
  from EFMT obtain u v where "(u,Spawn p,v)∈edges fg" using A by (auto elim: trss.cases)
  with spawn_no_mon have "mon_c fg {#[entry fg p]#} = {}" by simp
  with C'FMT show ?thesis by (simp add: mon_c_unconc)
qed
        
  (* WARNING: Don't declare this [simp], as c=c' will cause a simplifier loop *)
  (* FIXME: Dirty proof, not very robust *)
corollary (in flowgraph) trss_c_no_mon: 
  "((s,c),w,(s',c'))∈trcl (trss fg) ⟹ mon_c fg c' = mon_c fg c" 
  apply (auto elim!: trss_c_cases simp add: mon_c_unconc)
proof -
  fix csp x
  assume "x∈mon_c fg csp"
  then obtain s where "s ∈# csp" and M: "x∈mon_s fg s" by (unfold mon_c_def, auto) 
  moreover assume "∀s. s ∈# csp ⟶ (∃p. s = [entry fg p] ∧ (∃u v. (u, Spawn p, v) ∈ edges fg) ∧ initialproc fg p)"
  ultimately obtain p u v where "s=[entry fg p]" and "(u,Spawn p,v)∈edges fg" by blast
  hence "mon_s fg s = {}" by (simp)
  with M have False by simp
  thus "x∈mon_c fg c" ..
qed


lemma (in flowgraph) trss_spawn_no_mon_step[simp]: 
  "((s,c),LSpawn p, (s',c'))∈trss fg ⟹ mon fg p = {}"
  by (auto elim: trss.cases)

lemma trss_no_empty_s[simp]: "(([],c),e,(s',c'))∈trss fg = False"
  by (auto elim!: trss.cases)
lemma trss_no_empty[simp]: 
  assumes A: "(([],c),w,(s',c'))∈trcl (trss fg)" 
  shows "w=[] ∧ s'=[] ∧ c=c'" 
proof -
  note A 
  moreover { 
    fix s
    have "((s,c),w,(s',c'))∈trcl (trss fg) ⟹ s=[] ⟹ w=[] ∧ s'=[] ∧ c=c'"
      by (induct rule: trcl_pair_induct) auto
  } ultimately show ?thesis by blast
qed


lemma trs_step_cases[cases set, case_names NO_SPAWN SPAWN]: 
  assumes A: "(c,e,c')∈tr fg" 
  assumes A_NO_SPAWN: "!!s ce s' csp. ⟦
      ((s,ce),e,(s',ce))∈trss fg; 
      c={#s#}+ce; c'={#s'#}+ce
    ⟧ ⟹ P"
  assumes A_SPAWN: "!!s ce s' p. ⟦
      ((s,ce),LSpawn p,(s',{#[entry fg p]#}+ce))∈trss fg; 
      c={#s#}+ce; 
      c'={#s'#}+{#[entry fg p]#}+ce; 
      e=LSpawn p
    ⟧ ⟹ P"
  shows P
proof -
  from A show ?thesis proof (erule_tac gtr_find_thread)
    fix s ce s' ce' 
    assume FMT: "c = add_mset s ce" "c' = add_mset s' ce'"
    assume B: "((s, ce), e, s', ce') ∈ trss fg" thus ?thesis proof (cases rule: trss_c_cases_s)
      case no_spawn thus ?thesis using FMT B by (-) (rule A_NO_SPAWN, auto)  
    next
      case (spawn p) thus ?thesis using FMT B by (-) (rule A_SPAWN, auto simp add: union_assoc)
    qed
  qed
qed

subsection "Advanced properties"
subsubsection "Stack composition / decomposition"
lemma trss_stack_comp_s: 
  "((s,c),e,(s',c'))∈trss fg ⟹ ((s@r,c),e,(s'@r,c'))∈trss fg"
  by (auto elim!: trss.cases intro: trss.intros)

lemma trss_stack_comp: 
  "((s,c),w,(s',c'))∈trcl (trss fg) ⟹ ((s@r,c),w,(s'@r,c'))∈trcl (trss fg)" 
proof (induct rule: trcl_pair_induct)
  case empty thus ?case by auto
next
  case (cons s c e sh ch w s' c') note IHP=this
  from trss_stack_comp_s[OF IHP(1)] have "((s @ r, c), e, sh @ r, ch) ∈ trss fg" .
  also note IHP(3)
  finally show ?case .
qed

lemma trss_stack_decomp_s: "⟦ ((s@r,c),e,(s',c'))∈trss fg; s≠[] ⟧ 
  ⟹ ∃sp'. s'=sp'@r ∧ ((s,c),e,(sp',c'))∈trss fg" 
  by (cases s, simp) (auto intro: trss.intros elim!: trss.cases)

lemma trss_find_return: "⟦ 
    ((s@r,c),w,(r,c'))∈trcl (trss fg); 
    !!wa wb ch. ⟦ w=wa@wb; ((s,c),wa,([],ch))∈trcl (trss fg); 
                  ((r,ch),wb,(r,c'))∈trcl (trss fg) ⟧ ⟹ P 
  ⟧ ⟹ P"
  ― ‹If @{term "s=[]"}, the proposition follows trivially›
  apply (cases "s=[]")
  apply fastforce
proof -
  ― ‹For @{term "s≠[]"}, we use induction by @{term w}›
  have IM: "!!s c. ⟦ ((s@r,c),w,(r,c'))∈trcl (trss fg); s≠[] ⟧ ⟹ ∃wa wb ch. w=wa@wb ∧ ((s,c),wa,([],ch))∈trcl (trss fg) ∧ ((r,ch),wb,(r,c'))∈trcl (trss fg)"
  proof (induct w)
    case Nil thus ?case by (auto)
  next
    case (Cons e w) note IHP=this
    then obtain sh ch where SPLIT1: "((s@r,c),e,(sh,ch))∈trss fg" and SPLIT2: "((sh,ch),w,(r,c'))∈trcl (trss fg)" by (fast dest: trcl_uncons)
    { assume CASE: "e=LRet"
      with SPLIT1 obtain p where EDGE: "s@r=return fg p # sh" "c=ch" by (auto elim!: trss.cases)
      with IHP(3) obtain ss where SHFMT: "s=return fg p # ss" "sh=ss@r" by (cases s, auto) 
      { assume CC: "ss≠[]"
        with SHFMT have "∃ss. ss≠[] ∧ sh=ss@r" by blast
      } moreover {
        assume CC: "ss=[]"
        with CASE SHFMT EDGE have "((s,c),[e],([],ch))∈trcl (trss fg)" "e#w=[e]@w" by (auto intro: trss_ret)
        moreover from SPLIT2 SHFMT CC have "((r,ch),w,(r,c'))∈trcl (trss fg)" by simp
        ultimately have ?case by blast
      } ultimately have "?case ∨ (∃ss. ss≠[] ∧ sh=ss@r)" by blast
    } moreover {
      assume "e≠LRet"
      with SPLIT1 IHP(3) have "(∃ss. ss≠[] ∧ sh=ss@r)" by (force elim!: trss.cases simp add: append_eq_Cons_conv)
    } moreover {
      assume "(∃ss. ss≠[] ∧ sh=ss@r)"
      then obtain ss where CASE: "ss≠[]" "sh=ss@r" by blast
      with SPLIT2 have "((ss@r, ch), w, r, c') ∈ trcl (trss fg)" by simp
      from IHP(1)[OF this CASE(1)] obtain wa wb ch' where IHAPP: "w=wa@wb" "((ss,ch),wa,([],ch'))∈trcl (trss fg)" "((r,ch'),wb,(r,c'))∈trcl (trss fg)" by blast
      moreover from CASE SPLIT1 have "((s @ r, c), e, ss@r, ch) ∈ trss fg" by simp
      from trss_stack_decomp_s[OF this IHP(3)] have "((s, c), e, ss, ch) ∈ trss fg" by auto
      with IHAPP have "((s, c), e#wa, ([],ch')) ∈ trcl (trss fg)" by (rule_tac trcl.cons)
      moreover from IHAPP have "e#w=(e#wa)@wb" by auto
      ultimately have ?case by blast
    } ultimately show ?case by blast
  qed
  assume "((s @ r, c), w, r, c') ∈ trcl (trss fg)" "s ≠ []" "!!wa wb ch. ⟦ w=wa@wb; ((s,c),wa,([],ch))∈trcl (trss fg); ((r,ch),wb,(r,c'))∈trcl (trss fg) ⟧ ⟹ P" thus P by (blast dest: IM)
qed

    (* TODO: Try backward induction proof … is this simpler ? *)
lemma trss_return_cases[cases set]: "!!u r c. ⟦ 
    ((u#r,c),w,(r',c'))∈trcl (trss fg);
    !! s' u'. ⟦ r'=s'@u'#r; (([u],c),w,(s'@[u'],c'))∈trcl (trss fg) ⟧ ⟹ P; 
    !! wa wb ch. ⟦ w=wa@wb; (([u],c),wa,([],ch))∈trcl (trss fg); 
                   ((r,ch),wb,(r',c'))∈trcl (trss fg) ⟧ ⟹ P 
  ⟧ ⟹ P"
proof (induct w rule: length_compl_induct)
  case Nil thus ?case by auto
next
  case (Cons e w) note IHP=this
  then obtain sh ch where SPLIT1: "((u#r,c),e,(sh,ch))∈trss fg" and SPLIT2: "((sh,ch),w,(r',c'))∈trcl (trss fg)" by (fast dest: trcl_uncons)
  {
    fix ba q
    assume CASE: "e=LBase ba ∨ e=LSpawn q"
    with SPLIT1 obtain v where E: "sh=v#r" "(([u],c),e,([v],ch))∈trss fg" by (auto elim!: trss.cases intro: trss.intros)
    with SPLIT2 have "((v#r,ch),w,(r',c'))∈trcl (trss fg)" by simp
    hence ?case proof (cases rule: IHP(1)[of w, simplified, cases set])
      case (1 s' u') note CC=this
      with E(2) have "(([u],c),e#w,(s'@[u'],c'))∈trcl (trss fg)" by simp
      from IHP(3)[OF CC(1) this] show ?thesis .
    next
      case (2 wa wb ct) note CC=this
      with E(2) have "(([u],c),e#wa,([],ct))∈trcl (trss fg)" "e#w = (e#wa)@wb" by simp_all
      from IHP(4)[OF this(2,1) CC(3)] show ?thesis .
    qed
  } moreover {
    assume CASE: "e=LRet"
    with SPLIT1 have "sh=r" "(([u],c),[e],([],ch))∈trcl (trss fg)" by (auto elim!: trss.cases intro: trss.intros)
    with IHP(4)[OF _ this(2)] SPLIT2 have ?case by auto
  } moreover {
    fix q
    assume CASE: "e=LCall q"
    with SPLIT1 obtain u' where SHFMT: "sh=entry fg q # u' # r" "(([u],c),e,(entry fg q # [u'],ch))∈trss fg" by (auto elim!: trss.cases intro: trss.intros)
    with SPLIT2 have "((entry fg q # u' # r,ch),w,(r',c'))∈trcl (trss fg)" by simp
    hence ?case proof (cases rule: IHP(1)[of w, simplified, cases set])
      case (1 st ut) note CC=this
      from trss_stack_comp[OF CC(2), where r="[u']"] have "((entry fg q#[u'], ch), w, (st @ [ut]) @ [u'], c') ∈ trcl (trss fg)" by auto
      with SHFMT(2) have "(([u],c),e#w, (st @ [ut]) @ [u'], c') ∈ trcl (trss fg)" by auto
      from IHP(3)[OF _ this] CC(1) show ?thesis by simp
    next
      case (2 wa wb ct) note CC=this
      from trss_stack_comp[OF CC(2), where r="[u']"] have "((entry fg q # [u'], ch), wa, [u'], ct) ∈ trcl (trss fg)" by simp
      with SHFMT have PREPATH: "(([u],c),e#wa, [u'], ct) ∈ trcl (trss fg)" by simp
      from CC have L: "length wb≤length w" by simp
      from CC(3) show ?case proof (cases rule: IHP(1)[OF L, cases set])
        case (1 s'' u'') note CCC=this from trcl_concat[OF PREPATH CCC(2)] CC(1) have "(([u],c),e#w,(s''@[u''],c'))∈trcl (trss fg)" by (simp)
        from IHP(3)[OF CCC(1) this] show ?thesis .
      next
        case (2 wba wbb c'') note CCC=this from trcl_concat[OF PREPATH CCC(2)] CC(1) CCC(1) have "e#w = (e#wa@wba)@wbb" "(([u], c), e # wa @ wba, [], c'') ∈ trcl (trss fg)" by auto
        from IHP(4)[OF this CCC(3)] show ?thesis .
      qed
    qed
  } ultimately show ?case by (cases e, auto)
qed

lemma (in flowgraph) trss_find_call: 
  "!!v r' c'. ⟦ (([sp],c),w,(v#r',c')) ∈ trcl (trss fg); r'≠[] ⟧ 
  ⟹ ∃rh ch p wa wb. 
        w=wa@(LCall p)#wb ∧ 
        proc_of fg v = p ∧ 
        (([sp],c),wa,(rh,ch))∈trcl (trss fg) ∧ 
        ((rh,ch),LCall p,((entry fg p)#r',ch))∈trss fg ∧ 
        (([entry fg p],ch),wb,([v],c'))∈trcl (trss fg)"
proof (induct w rule: length_compl_rev_induct)
  case Nil thus ?case by (auto) 
next
  case (snoc w e) note IHP=this
  then obtain rh ch where SPLIT1: "(([sp],c),w,(rh,ch))∈trcl (trss fg)" and SPLIT2: "((rh,ch),e,(v#r',c'))∈trss fg" by (fast dest: trcl_rev_uncons)

  {
    assume "∃u. rh=u#r'"
    then obtain u where RHFMT[simp]: "rh=u#r'" by blast
    with SPLIT2 have "proc_of fg u = proc_of fg v" by (auto elim: trss.cases intro: edges_part)
    moreover from IHP(1)[of w u r' ch, OF _ SPLIT1[simplified] IHP(3)] obtain rt ct p wa wb where 
      IHAPP: "w = wa @ LCall p # wb" "proc_of fg u = p" "(([sp], c), wa, (rt, ct)) ∈ trcl (trss fg)" "((rt, ct), LCall p, entry fg p # r', ct) ∈ trss fg"  
          "(([entry fg p], ct), wb, ([u], ch)) ∈ trcl (trss fg)" by (blast)
    moreover
    have "(([entry fg p], ct), wb@[e], ([v], c')) ∈ trcl (trss fg)" proof -
      note IHAPP(5)
      also from SPLIT2 have "(([u],ch),e,([v],c')) ∈ trss fg" by (auto elim!: trss.cases intro!: trss.intros)
      finally show ?thesis .
    qed
    moreover from IHAPP have "w@[e] = wa @ LCall p # (wb@[e])" by auto
    ultimately have ?case by auto
  }
  moreover have "(∃u. rh=u#r') ∨ ?case"
  proof (rule trss.cases[OF SPLIT2], simp_all, goal_cases) ― ‹Cases for base- and spawn edge are discharged automatically›
      ― ‹Case: call-edge›
    case (1 ca p r u vv) with SPLIT1 SPLIT2 show ?case by fastforce 
  next
      ― ‹Case: return edge›
    case CC: (2 q r ca)
    hence [simp]: "rh=(return fg q)#v#r'" by simp
    with IHP(1)[of w "(return fg q)" "v#r'" ch, OF _ SPLIT1[simplified]] obtain rt ct wa wb where 
      IHAPP: "w = wa @ LCall q # wb" "(([sp], c), wa, rt, ct) ∈ trcl (trss fg)" "((rt, ct), LCall q, entry fg q # v # r', ct) ∈ trss fg"
          "(([entry fg q], ct), wb, [return fg q], ch) ∈ trcl (trss fg)" by force
    then obtain u where RTFMT [simp]: "rt=u#r'" and PROC_OF_U: "proc_of fg u = proc_of fg v" by (auto elim: trss.cases intro: edges_part)
    from IHAPP(1) have LENWA: "length wa ≤ length w" by auto
    from IHP(1)[OF LENWA IHAPP(2)[simplified] IHP(3)] obtain rhh chh p waa wab where 
      IHAPP': "wa=waa@LCall p # wab" "proc_of fg u = p" "(([sp],c),waa,(rhh,chh))∈trcl (trss fg)" "((rhh,chh),LCall p, (entry fg p#r',chh))∈trss fg" 
          "(([entry fg p],chh),wab,([u],ct))∈trcl (trss fg)" 
      by blast
    from IHAPP IHAPP' PROC_OF_U have "w@[e]=waa@LCall p#(wab@LCall q#wb@[e]) ∧ proc_of fg v = p" by auto
    moreover have "(([entry fg p],chh),wab@(LCall q)#wb@[e],([v],c'))∈trcl (trss fg)" proof -
      note IHAPP'(5)
      also from IHAPP have "(([u], ct), LCall q, entry fg q # [v], ct) ∈ trss fg" by (auto elim!: trss.cases intro!: trss.intros)
      also from trss_stack_comp[OF IHAPP(4)] have "((entry fg q#[v],ct),wb,(return fg q#[v],ch))∈trcl (trss fg)" by simp
      also from CC have "((return fg q#[v],ch),e,([v],c'))∈trss fg" by (auto intro: trss_ret)
      finally show ?thesis by simp
    qed
    moreover note IHAPP' CC
    ultimately show ?case by auto
  qed
  ultimately show ?case by blast
qed

― ‹This lemma is better suited for application in soundness proofs of constraint systems than @{thm [source] flowgraph.trss_find_call}›
lemma (in flowgraph) trss_find_call': 
  assumes A: "(([sp],c),w,(return fg p#[u'],c')) ∈ trcl (trss fg)" 
  and EX: "!!uh ch wa wb. ⟦
      w=wa@(LCall p)#wb; 
      (([sp],c),wa,([uh],ch))∈trcl (trss fg); 
      (([uh],ch),LCall p,((entry fg p)#[u'],ch))∈trss fg;
      (uh,Call p,u')∈edges fg; 
      (([entry fg p],ch),wb,([return fg p],c'))∈trcl (trss fg)
    ⟧ ⟹ P" 
  shows "P"
proof -
  from trss_find_call[OF A] obtain rh ch wa wb where FC: 
    "w = wa @ LCall p # wb" 
    "(([sp], c), wa, rh, ch) ∈ trcl (trss fg)" 
    "((rh, ch), LCall p, [entry fg p, u'], ch) ∈ trss fg" 
    "(([entry fg p], ch), wb, [return fg p], c') ∈ trcl (trss fg)"
    by auto
  moreover from FC(3) obtain uh where ADD: "rh=[uh]" "(uh,Call p,u')∈edges fg" by (auto elim: trss.cases)
  ultimately show ?thesis using EX by auto
qed
      
lemma (in flowgraph) trss_bot_proc_const: 
  "!!s' u' c'. ((s@[u],c),w,(s'@[u'],c'))∈trcl (trss fg) 
    ⟹ proc_of fg u = proc_of fg u'" 
proof (induct w rule: rev_induct)
  case Nil thus ?case by auto
next
  case (snoc e w) note IHP=this then obtain sh ch where SPLIT1: "((s@[u],c),w,(sh,ch))∈trcl (trss fg)" and SPLIT2: "((sh,ch),e,(s'@[u'],c'))∈trss fg" by (fast dest: trcl_rev_uncons)
  from SPLIT2 have "sh≠[]" by (auto elim!: trss.cases)
  then obtain ssh uh where SHFMT: "sh=ssh@[uh]" by (blast dest: list_rev_decomp)
  with IHP(1)[of ssh uh ch] SPLIT1 have "proc_of fg u = proc_of fg uh" by auto
  also from SPLIT2 SHFMT have "proc_of fg uh = proc_of fg u'" by (cases rule: trss.cases) (cases ssh, auto simp add: edges_part)+
  finally show ?case .
qed

― ‹Specialized version of @{thm [source] flowgraph.trss_bot_proc_const}that comes in handy for precision proofs of constraint systems›
lemma (in flowgraph) trss_er_path_proc_const: 
  "(([entry fg p],c),w,([return fg q],c'))∈trcl (trss fg) ⟹ p=q"
  using trss_bot_proc_const[of "[]" "entry fg p" _ _ "[]" "return fg q", simplified] .

lemma trss_2empty_to_2return: "⟦ ((s,c),w,([],c'))∈trcl (trss fg); s≠[] ⟧ ⟹ 
  ∃w' p. w=w'@[LRet] ∧ ((s,c),w',([return fg p],c'))∈trcl (trss fg)" 
proof -
  assume A: "((s,c),w,([],c'))∈trcl (trss fg)" "s≠[]"
  hence "w≠[]" by auto
  then obtain w' e where WD: "w=w'@[e]" by (blast dest: list_rev_decomp)
  with A(1) obtain sh ch where SPLIT: "((s,c),w',(sh,ch))∈trcl (trss fg)" "((sh,ch),e,([],c'))∈trss fg" by (fast dest: trcl_rev_uncons)
  from SPLIT(2) obtain p where "e=LRet" "sh=[return fg p]" "ch=c'" by (cases rule: trss.cases, auto)
  with SPLIT(1) WD show ?thesis by blast
qed
  
lemma trss_2return_to_2empty: "⟦ ((s,c),w,([return fg p],c'))∈trcl (trss fg) ⟧ 
  ⟹ ((s,c),w@[LRet],([],c'))∈trcl (trss fg)"
  apply (subgoal_tac "(([return fg p],c'),LRet,([],c'))∈trss fg")
  by (auto dest: trcl_rev_cons intro: trss.intros)

subsubsection "Adding threads"
lemma trss_env_increasing_s: "((s,c),e,(s',c'))∈trss fg ⟹ c⊆#c'"
  by (auto elim!: trss.cases)
lemma trss_env_increasing: "((s,c),w,(s',c'))∈trcl (trss fg) ⟹ c⊆#c'"
  by (induct rule: trcl_pair_induct) (auto dest: trss_env_increasing_s order_trans)

subsubsection "Conversion between environment and monitor restrictions"
lemma trss_mon_e_no_ctx: 
  "((s,c),e,(s',c'))∈trss fg ⟹ mon_e fg e ∩ mon_c fg c = {}"
  by (erule trss.cases) auto
lemma (in flowgraph) trss_mon_w_no_ctx: 
  "((s,c),w,(s',c'))∈trcl (trss fg) ⟹ mon_w fg w ∩ mon_c fg c = {}"
  by (induct rule: trcl_pair_induct) (auto dest: trss_mon_e_no_ctx simp add: trss_c_no_mon_s)

lemma (in flowgraph) trss_modify_context_s: 
  "!!cn. ⟦((s,c),e,(s',c'))∈trss fg; mon_e fg e ∩ mon_c fg cn = {}⟧ 
    ⟹ ∃csp. c'=csp+c ∧ mon_c fg csp = {} ∧ ((s,cn),e,(s',csp+cn))∈trss fg"
  by (erule trss.cases) (auto intro!: trss.intros)

lemma (in flowgraph) trss_modify_context[rule_format]: 
  "⟦((s,c),w,(s',c'))∈trcl (trss fg)⟧ 
  ⟹ ∀cn. mon_w fg w ∩ mon_c fg cn = {} 
      ⟶ (∃csp. c'=csp+c ∧ mon_c fg csp = {} ∧ 
                 ((s,cn),w,(s',csp+cn))∈trcl (trss fg))"
proof (induct rule: trcl_pair_induct)
  case empty thus ?case by simp 
next
  case (cons s c e sh ch w s' c') note IHP=this show ?case 
  proof (intro allI impI)
    fix cn
    assume MON: "mon_w fg (e # w) ∩ mon_c fg cn = {}"
    from trss_modify_context_s[OF IHP(1)] MON obtain csph where S1: "ch = csph + c" "mon_c fg csph={}" "((s, cn), e, sh, csph + cn) ∈ trss fg" by auto
    with MON have "mon_w fg w ∩ mon_c fg (csph+cn) = {}" by (auto simp add: mon_c_unconc)
    with IHP(3)[rule_format] obtain csp where S2: "c'=csp+ch" "mon_c fg csp={}" "((sh,csph+cn),w,(s',csp+(csph+cn)))∈trcl (trss fg)" by blast 
    from S1 S2 have "c'=(csp+csph)+c" "mon_c fg (csp+csph)={}" "((s,cn),e#w,(s',(csp+csph)+cn))∈trcl (trss fg)" by (auto simp add: union_assoc mon_c_unconc)
    thus "∃csp. c' = csp + c ∧ mon_c fg csp = {} ∧ ((s, cn), e # w, s', csp + cn) ∈ trcl (trss fg)" by blast
  qed
qed

lemma trss_add_context_s: 
  "⟦((s,c),e,(s',c'))∈trss fg; mon_e fg e ∩ mon_c fg ce = {}⟧ 
    ⟹ ((s,c+ce),e,(s',c'+ce))∈trss fg"
  by (auto elim!: trss.cases intro!: trss.intros simp add: union_assoc mon_c_unconc)

lemma trss_add_context: 
  "⟦((s,c),w,(s',c'))∈trcl (trss fg); mon_w fg w ∩ mon_c fg ce = {}⟧ 
    ⟹ ((s,c+ce),w,(s',c'+ce))∈trcl (trss fg)" 
proof (induct rule: trcl_pair_induct)
  case empty thus ?case by simp
next
  case (cons s c e sh ch w s' c') note IHP=this
  from IHP(4) have MM: "mon_e fg e ∩ mon_c fg ce = {}" "mon_w fg w ∩ mon_c fg ce = {}" by auto
  from trcl.cons[OF trss_add_context_s[OF IHP(1) MM(1)] IHP(3)[OF MM(2)]] show ?case .
qed
  
lemma trss_drop_context_s: "⟦ ((s,c+ce),e,(s',c'+ce))∈trss fg ⟧ 
  ⟹ ((s,c),e,(s',c'))∈trss fg ∧ mon_e fg e ∩ mon_c fg ce = {}"
  by (erule trss.cases) (auto intro!: trss.intros simp add: mon_c_unconc union_assoc[of _ c ce, symmetric])

lemma trss_drop_context: "!!s c. ⟦ ((s,c+ce),w,(s',c'+ce))∈trcl (trss fg) ⟧ 
  ⟹ ((s,c),w,(s',c'))∈trcl (trss fg) ∧ mon_w fg w ∩ mon_c fg ce = {}" 
proof (induct w)
  case Nil thus ?case by auto
next
  case (Cons e w) note IHP=this
  then obtain sh ch where SPLIT: "((s,c+ce),e,(sh,ch))∈trss fg" "((sh,ch),w,(s',c'+ce))∈ trcl (trss fg)" by (fast dest: trcl_uncons)
  from trss_c_fmt_s[OF SPLIT(1)] obtain csp where CHFMT: "ch = (csp + c) + ce" by (auto simp add: union_assoc)
  from CHFMT trss_drop_context_s SPLIT(1) have "((s,c),e,(sh,csp+c))∈trss fg" "mon_e fg e ∩ mon_c fg ce = {}" by blast+
  moreover from CHFMT IHP(1) SPLIT(2) have "((sh,csp+c),w,(s',c'))∈trcl (trss fg)" "mon_w fg w ∩ mon_c fg ce = {}" by blast+
  ultimately show ?case by auto
qed

lemma trss_xchange_context_s: 
  assumes A: "((s,c),e,(s',csp+c))∈trss fg" 
  and M:"mon_c fg cn ⊆ mon_c fg c" 
  shows "((s,cn),e,(s',csp+cn))∈trss fg"
proof -
  from trss_drop_context_s[of _ "{#}", simplified, OF A] have DC: "((s, {#}), e, s', csp) ∈ trss fg" "mon_e fg e ∩ mon_c fg c = {}" by simp_all
  with M have "mon_e fg e ∩ mon_c fg cn = {}" by auto
  from trss_add_context_s[OF DC(1) this] show ?thesis by auto
qed
  
lemma trss_xchange_context: 
  assumes A: "((s,c),w,(s',csp+c))∈trcl (trss fg)" 
  and M:"mon_c fg cn ⊆ mon_c fg c" 
  shows "((s,cn),w,(s',csp+cn))∈trcl (trss fg)"
proof -
  from trss_drop_context[of _ "{#}", simplified, OF A] have DC: "((s, {#}), w, s', csp) ∈ trcl (trss fg)" "mon_w fg w ∩ mon_c fg c = {}" by simp_all
  with M have "mon_w fg w ∩ mon_c fg cn = {}" by auto
  from trss_add_context[OF DC(1) this] show ?thesis by auto
qed

lemma trss_drop_all_context_s[cases set, case_names dropped]: 
  assumes A: "((s,c),e,(s',c'))∈trss fg" 
  and C: "!!csp. ⟦ c'=csp+c; ((s,{#}),e,(s',csp))∈trss fg ⟧ ⟹ P" 
  shows P
using A proof (cases rule: trss_c_cases_s)
  case no_spawn with trss_xchange_context_s[of s c e s' "{#}" fg "{#}"] A C show P by auto
next
  case (spawn p u v) with trss_xchange_context_s[of s c e s' "{#[entry fg p]#}" fg "{#}"] A C show P by auto
qed

lemma trss_drop_all_context[cases set, case_names dropped]: 
  assumes A: "((s,c),w,(s',c'))∈trcl (trss fg)" 
  and C: "!!csp. ⟦ c'=csp+c; ((s,{#}),w,(s',csp))∈trcl (trss fg)⟧ ⟹ P" 
  shows P
using A proof (cases rule: trss_c_cases)
  case (c_case csp) with trss_xchange_context[of s c w s' csp fg "{#}"] A C show P by auto
qed

lemma tr_add_context_s: 
  "⟦ (c,e,c')∈tr fg; mon_e fg e ∩ mon_c fg ce = {} ⟧ ⟹ (c+ce,e,c'+ce)∈tr fg"
  by (erule gtrE) (auto simp add: mon_c_unconc union_assoc intro: gtrI_s dest: trss_add_context_s)

lemma tr_add_context: 
  "⟦ (c,w,c')∈trcl (tr fg); mon_w fg w ∩ mon_c fg ce = {} ⟧ 
    ⟹ (c+ce,w,c'+ce)∈trcl (tr fg)" 
proof (induct rule: trcl.induct)
  case empty thus ?case by auto
next
  case (cons c e c' w c'') note IHP=this
  from tr_add_context_s[OF IHP(1), of ce] IHP(4) have "(c + ce, e, c' + ce) ∈ tr fg" by auto
  also from IHP(3,4) have "(c' + ce, w, c'' + ce) ∈ trcl (tr fg)" by auto
  finally show ?case .
qed
   
end