Session Program-Conflict-Analysis

Theory Misc

(*  Title:       Miscellanneous Definitions and Lemmas
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)

section ‹Miscellanneous Definitions and Lemmas›

theory Misc
imports Main "HOL-Library.Multiset" "HOL-Library.Subseq_Order"
begin
text_raw ‹\label{thy:Misc}›

text ‹Here we provide a collection of miscellaneous definitions and helper lemmas›

subsection "Miscellanneous (1)"
text ‹This stuff is used in this theory itself, and thus occurs in first place. There is another ,,Miscellaneous''-section at the end of this theory›
subsubsection "AC-operators"
  
text ‹Locale to declare AC-laws as simplification rules›
locale AC =
  fixes f
  assumes commute[simp]: "f x y = f y x"
  assumes assoc[simp]: "f (f x y) z = f x (f y z)"

lemma (in AC) left_commute[simp]: "f x (f y z) = f y (f x z)"
  by (simp only: assoc[symmetric]) simp

text ‹Locale to define functions from surjective, unique relations›
locale su_rel_fun =
  fixes F and f
  assumes unique: "(A,B)F; (A,B')F  B=B'"
  assumes surjective: "!!B. (A,B)F  P  P"
  assumes f_def: "f A == THE B. (A,B)F"

lemma (in su_rel_fun) repr1: "(A,f A)F" proof (unfold f_def)
  obtain B where "(A,B)F" by (rule surjective)
  with theI[where P="λB. (A,B)F", OF this] show "(A, THE x. (A, x)  F)  F" by (blast intro: unique)
qed
  
lemma (in su_rel_fun) repr2: "(A,B)F  B=f A" using repr1
  by (blast intro: unique)

lemma (in su_rel_fun) repr: "(f A = B) = ((A,B)F)" using repr1 repr2
  by (blast) 


subsection ‹Abbreviations for list order›

abbreviation ileq :: "'a list  'a list  bool"  (infix "" 50) where
  "(≼)  (≤)"

abbreviation ilt :: "'a list  'a list  bool"  (infix "" 50) where
  "(≺)  (<)"


subsection ‹Multisets›

(*
  The following is a syntax extension for multisets. Unfortunately, it depends on a change in the Library/Multiset.thy, so it is commented out here, until it will be incorporated 
  into Library/Multiset.thy by its maintainers.

  The required change in Library/Multiset.thy is removing the syntax for single:
     - single :: "'a => 'a multiset"    ("{#_#}")
     + single :: "'a => 'a multiset"

  And adding the following translations instead:
  
     + syntax
     + "_multiset" :: "args ⇒ 'a multiset" ("{#(_)#}")

     + translations
     +   "{#x, xs#}" == "{#x#} + {#xs#}" 
     +   "{# x #}" == "single x"

  This translates "{# … #}" into a sum of singletons, that is parenthesized to the right. ?? Can we also achieve left-parenthesizing ??

*)


  (* Let's try what happens if declaring AC-rules for multiset union as simp-rules *)
(*declare union_ac[simp] -- don't do it !*)

subsubsection ‹Case distinction›

lemma multiset_induct'[case_names empty add]: "P {#}; M x. P M  P ({#x#}+M)  P M"
  by (induct rule: multiset_induct) (auto simp add: union_commute)

subsubsection ‹Count›
  lemma count_ne_remove: " x ~= t  count S x = count (S-{#t#}) x"
    by (auto)
  lemma mset_empty_count[simp]: "(p. count M p = 0) = (M={#})"
    by (auto simp add: multiset_eq_iff)

subsubsection ‹Union, difference and intersection›

  lemma size_diff_se: "t ∈# S  size S = size (S - {#t#}) + 1" proof (unfold size_multiset_overloaded_eq)
    let ?SIZE = "sum (count S) (set_mset S)"
    assume A: "t ∈# S"
    from A have SPLITPRE: "finite (set_mset S) & {t}(set_mset S)" by auto
    hence "?SIZE = sum (count S) (set_mset S - {t}) + sum (count S) {t}" by (blast dest: sum.subset_diff)
    hence "?SIZE = sum (count S) (set_mset S - {t}) + count (S) t" by auto
    moreover with A have "count S t = count (S-{#t#}) t + 1" by auto
    ultimately have D: "?SIZE = sum (count S) (set_mset S - {t}) + count (S-{#t#}) t + 1" by (arith)
    moreover have "sum (count S) (set_mset S - {t}) = sum (count (S-{#t#})) (set_mset S - {t})" proof -
      have "ALL x:(set_mset S - {t}) . count S x = count (S-{#t#}) x" by (auto iff add: count_ne_remove)
      thus ?thesis by simp
    qed
    ultimately have D: "?SIZE = sum (count (S-{#t#})) (set_mset S - {t}) + count (S-{#t#}) t + 1" by (simp)
    moreover
    { assume CASE: "t ∉# S - {#t#}"
      from CASE have "set_mset S - {t} = set_mset (S - {#t#})"
        by (simp add: at_most_one_mset_mset_diff)
      with CASE D have "?SIZE = sum (count (S-{#t#})) (set_mset (S - {#t#})) + 1"
        by (simp add: not_in_iff)
    }
    moreover
    { assume CASE: "t ∈# S - {#t#}"
      from CASE have 1: "set_mset S = set_mset (S-{#t#})"
        by (rule more_than_one_mset_mset_diff [symmetric])
      moreover from D have "?SIZE = sum (count (S-{#t#})) (set_mset S - {t}) + sum (count (S-{#t#})) {t} + 1" by simp
      moreover from SPLITPRE sum.subset_diff have "sum (count (S-{#t#})) (set_mset S) = sum (count (S-{#t#})) (set_mset S - {t}) + sum (count (S-{#t#})) {t}" by (blast)
      ultimately have "?SIZE = sum (count (S-{#t#})) (set_mset (S-{#t#})) + 1" by simp
    }
    ultimately show "?SIZE = sum (count (S-{#t#})) (set_mset (S - {#t#})) + 1" by blast
  qed

  (* TODO: Check whether this proof can be done simpler *)
  lemma mset_union_diff_comm: "t ∈# S  T + (S - {#t#}) = (T + S) - {#t#}" proof -
    assume "t ∈# S"
    then obtain S' where S: "S = add_mset t S'"
      by (metis insert_DiffM)
    then show ?thesis
      by auto
  qed

  lemma mset_right_cancel_union: "a ∈# A+B; ~(a ∈# B)  a∈#A"
    by (simp)
  lemma mset_left_cancel_union: "a ∈# A+B; ~(a ∈# A)  a∈#B"
    by (simp)
  
  lemmas mset_cancel_union = mset_right_cancel_union mset_left_cancel_union

  lemma mset_right_cancel_elem: "a ∈# A+{#b#}; a~=b  a∈#A"
    apply(subgoal_tac "~(a ∈# {#b#})")
    apply(auto)
  done

  lemma mset_left_cancel_elem: "a ∈# {#b#}+A; a~=b  a∈#A"
    apply(subgoal_tac "~(a ∈# {#b#})")
    apply(auto)
  done

  lemmas mset_cancel_elem = mset_right_cancel_elem mset_left_cancel_elem

  lemma mset_diff_cancel1elem[simp]: "~(a ∈# B)  {#a#}-B = {#a#}" proof -
    assume A: "~(a ∈# B)"
    hence "count ({#a#}-B) a = count ({#a#}) a" by (auto simp add: not_in_iff)
    moreover have "ALL e . e~=a  count ({#a#}-B) e = count ({#a#}) e" by auto
    ultimately show ?thesis by (auto simp add: multiset_eq_iff)
  qed

  (*lemma union_diff_assoc_se: "t ∈# B ⟹ (A+B)-{#t#} = A + (B-{#t#})"
    by (auto iff add: multiset_eq_iff)
  lemma union_diff_assoc_se2: "t ∈# A ⟹ (A+B)-{#t#} = (A-{#t#}) + B"
    by (auto iff add: multiset_eq_iff)
  lemmas union_diff_assoc_se = union_diff_assoc_se1 union_diff_assoc_se2*)

  lemma union_diff_assoc: "C-B={#}  (A+B)-C = A + (B-C)"
    by (simp add: multiset_eq_iff)

  lemma mset_union_2_elem: "{#a#}+{#b#} = M + {#c#}  {#a#}=M & b=c | a=c & {#b#}=M"
    by (auto simp: add_eq_conv_diff)

  lemma mset_un_cases[cases set, case_names left right]:
    "a ∈# A + B; a∈#A  P; a∈#B  P  P"
    by (auto)

  lemma mset_unplusm_dist_cases[cases set, case_names left right]:
    assumes A: "add_mset s A = B+C"
    assumes L: "B=add_mset s (B-{#s#}); A=(B-{#s#})+C  P"
    assumes R: "C=add_mset s (C-{#s#}); A=B+(C-{#s#})  P" 
    shows P
  proof -
    from A[symmetric] have "s ∈# B+C" by simp
    thus ?thesis proof (cases rule: mset_un_cases)
      case left hence 1: "B=add_mset s (B-{#s#})" by simp
      with A have "add_mset s A = add_mset s ((B-{#s#})+C)" by (simp add: union_ac)
      hence 2: "A = (B-{#s#})+C" by (simp)
      from L[OF 1 2] show ?thesis .
    next
      case right hence 1: "C=add_mset s (C-{#s#})" by simp
      with A have "add_mset s A = add_mset s (B+(C-{#s#}))" by (simp add: union_ac)
      hence 2: "A = B+(C-{#s#})" by (simp)
      from R[OF 1 2] show ?thesis .
    qed
  qed

  lemma mset_unplusm_dist_cases2[cases set, case_names left right]:
    assumes A: "B+C = add_mset s A"
    assumes L: "B=add_mset s (B-{#s#}); A=(B-{#s#})+C  P"
    assumes R: "C=add_mset s (C-{#s#}); A=B+(C-{#s#})  P" 
    shows P
    using mset_unplusm_dist_cases[OF A[symmetric]] L R by blast

  lemma mset_single_cases[cases set, case_names loc env]: 
    assumes A: "add_mset s c = add_mset r' c'" 
    assumes CASES: "s=r'; c=c'  P" "c'={#s#}+(c'-{#s#}); c={#r'#}+(c-{#r'#}); c-{#r'#} = c'-{#s#}   P" 
    shows "P"
  proof -
    { assume CASE: "s=r'"
      with A have "c=c'" by simp
      with CASE CASES have ?thesis by auto
    } moreover {
      assume CASE: "sr'"
      have "s∈#{#s#}+c" by simp
      with A have "s ∈# {#r'#} + c'" by simp
      with CASE have "s ∈# c'" 
        by simp
      from insert_DiffM[OF this, symmetric] have 1: "c' = add_mset s (c' - {#s#})" .
      with A have "{#s#}+c = {#s#}+({#r'#}+(c' - {#s#}))" by (auto simp add: union_ac)
      hence 2: "c={#r'#}+(c' - {#s#})" by (auto)
      hence 3: "c-{#r'#} = (c' - {#s#})" by auto
      from 1 2 3 CASES have ?thesis by auto
    } ultimately show ?thesis by blast
  qed

  lemma mset_single_cases'[cases set, case_names loc env]: 
    assumes A: "add_mset s c = add_mset r' c'" 
    assumes CASES: "s=r'; c=c'  P" "!!cc. c'={#s#}+cc; c={#r'#}+cc; c'-{#s#}=cc; c-{#r'#}=cc  P" 
    shows "P"
    using A  CASES by (auto elim!: mset_single_cases)

  lemma mset_single_cases2[cases set, case_names loc env]: 
    assumes A: "add_mset s c = add_mset r' c'" 
    assumes CASES: "s=r'; c=c'  P" "c'=(c'-{#s#})+{#s#}; c=(c-{#r'#})+{#r'#}; c-{#r'#} = c'-{#s#}   P" 
    shows "P" 
  proof -
    from A have "add_mset s c = add_mset r' c'" by simp
    thus ?thesis proof (cases rule: mset_single_cases)
      case loc with CASES show ?thesis by simp
    next
      case env with CASES show ?thesis by (simp add: union_ac)
    qed
  qed

  lemma mset_single_cases2'[cases set, case_names loc env]: 
    assumes A: "add_mset s c = add_mset r' c'" 
    assumes CASES: "s=r'; c=c'  P" "!!cc. c'=cc+{#s#}; c=cc+{#r'#}; c'-{#s#}=cc; c-{#r'#}=cc  P" 
    shows "P"
    using A  CASES by (auto elim!: mset_single_cases2)

  lemma mset_un_single_un_cases [consumes 1, case_names left right]:
    assumes A: "add_mset a A = B + C"
      and CASES: "a ∈# B  A = (B - {#a#}) + C  P"
        "a ∈# C  A = B + (C - {#a#})  P"
    shows P
  proof -
    have "a ∈# A+{#a#}" by simp
    with A have "a ∈# B+C" by auto
    thus ?thesis proof (cases rule: mset_un_cases)
      case left hence "B=B-{#a#}+{#a#}" by auto
      with A have "A+{#a#} = (B-{#a#})+C+{#a#}" by (auto simp add: union_ac)
      hence "A=(B-{#a#})+C" by simp
      with CASES(1)[OF left] show ?thesis by blast
    next
      case right hence "C=C-{#a#}+{#a#}" by auto
      with A have "A+{#a#} = B+(C-{#a#})+{#a#}" by (auto simp add: union_ac)
      hence "A=B+(C-{#a#})" by simp
      with CASES(2)[OF right] show ?thesis by blast
    qed
  qed

      (* TODO: Can this proof be done more automatically ? *)
  lemma mset_distrib[consumes 1, case_names dist]: assumes A: "(A::'a multiset)+B = M+N" "!!Am An Bm Bn. A=Am+An; B=Bm+Bn; M=Am+Bm; N=An+Bn  P" shows "P"
  proof -
    have BN_MA: "B - N = M - A"
      by (metis (no_types) add_diff_cancel_right assms(1) union_commute)
    have H: "A = A∩# C + (A - C) ∩# D" if "A + B = C + D" for A B C D :: "'a multiset"
      by (metis add.commute diff_intersect_left_idem mset_subset_eq_add_left subset_eq_diff_conv
          subset_mset.add_diff_inverse subset_mset.inf_absorb1 subset_mset.inf_le1 that)
    have A': "A = A∩# M + (A - M) ∩# N"
      using A(1) H by blast
    moreover have B': "B = (B - N) ∩# M + B∩# N"
      using A(1) H[of B A N M] by (auto simp: ac_simps)
    moreover have "M = A ∩# M + (B - N) ∩# M"
      using H[of M N A B] BN_MA[symmetric] A(1) by (metis (no_types) diff_intersect_left_idem
          diff_union_cancelR multiset_inter_commute subset_mset.diff_add subset_mset.inf.cobounded1
          union_commute)
    moreover have "N = (A - M) ∩# N + B ∩# N"
      by (metis A' assms(1) diff_union_cancelL inter_union_distrib_left inter_union_distrib_right
          mset_subset_eq_multiset_union_diff_commute subset_mset.inf.cobounded1 subset_mset.inf.commute)
    ultimately show P
      using A(2) by blast
  qed


subsubsection ‹Singleton multisets›   

lemma mset_size_le1_cases[case_names empty singleton,consumes 1]: " size M  Suc 0; M={#}  P; !!m. M={#m#}  P   P"
  by (cases M) auto

lemma diff_union_single_conv2:
  "a ∈# J  J + I - {#a#} = (J - {#a#}) + I"
  using diff_union_single_conv [of a J I]
  by (simp add: union_ac)

lemmas diff_union_single_convs = diff_union_single_conv diff_union_single_conv2

lemma mset_contains_eq: "(m ∈# M) = ({#m#}+(M-{#m#})=M)" proof (auto)
  assume "add_mset m (M - {#m#}) = M"
  moreover have "m ∈# {#m#} + (M - {#m#})" by simp
  ultimately show "m ∈# M" by simp
qed


subsubsection ‹Pointwise ordering›

  lemma mset_le_incr_right1: "(a::'a multiset)⊆#b  a⊆#b+c" using mset_subset_eq_mono_add[of a b "{#}" c, simplified] .
  lemma mset_le_incr_right2: "(a::'a multiset)⊆#b  a⊆#c+b" using mset_le_incr_right1
    by (auto simp add: union_commute)
  lemmas mset_le_incr_right = mset_le_incr_right1 mset_le_incr_right2

  lemma mset_le_decr_left1: "(a::'a multiset)+c⊆#b  a⊆#b" using mset_le_incr_right1 mset_subset_eq_mono_add_right_cancel
    by blast
  lemma mset_le_decr_left2: "c+(a::'a multiset)⊆#b  a⊆#b" using mset_le_decr_left1
    by (auto simp add: union_ac)
  lemma mset_le_add_mset_decr_left1: "add_mset c a⊆#(b::'a multiset)  a⊆#b"
    by (simp add: mset_subset_eq_insertD subset_mset.dual_order.strict_implies_order)
  lemma mset_le_add_mset_decr_left2: "add_mset c a⊆#(b::'a multiset)  {#c#}⊆#b"
    by (simp add: mset_subset_eq_insertD subset_mset.dual_order.strict_implies_order)

  lemmas mset_le_decr_left = mset_le_decr_left1 mset_le_decr_left2 mset_le_add_mset_decr_left1
    mset_le_add_mset_decr_left2
  
  lemma mset_le_subtract: "(A::'a multiset)⊆#B  A-C ⊆# B-C"
    apply (unfold subseteq_mset_def)
    apply auto
    apply (subgoal_tac "count A a  count B a")
    apply arith
    apply simp
    done

  lemma mset_union_subset: "(A::'a multiset)+B ⊆# C  A⊆#C  B⊆#C"
    by (auto dest: mset_le_decr_left)
 
  lemma mset_le_add_mset: "add_mset x B ⊆# C  {#x#}⊆#C  B⊆#(C::'a multiset)"
    by (auto dest: mset_le_decr_left)
  
  lemma mset_le_subtract_left: "(A::'a multiset)+B ⊆# X  B ⊆# X-A  A⊆#X"
    by (auto dest: mset_le_subtract[of "A+B" "X" "A"] mset_union_subset)
  lemma mset_le_subtract_right: "(A::'a multiset)+B ⊆# X  A ⊆# X-B  B⊆#X"
    by (auto dest: mset_le_subtract[of "A+B" "X" "B"] mset_union_subset)

lemma mset_le_subtract_add_mset_left: "add_mset x B ⊆# (X::'a multiset)  B ⊆# X-{#x#}  {#x#}⊆#X"
    by (auto dest: mset_le_subtract[of "add_mset x B" "X" "{#x#}"] mset_le_add_mset)

  lemma mset_le_subtract_add_mset_right: "add_mset x B ⊆# (X::'a multiset)  {#x#} ⊆# X-B  B⊆#X"
    by (auto dest: mset_le_subtract[of "add_mset x B" "X" "B"] mset_le_add_mset)

  lemma mset_le_addE: " (xs::'a multiset) ⊆# ys; !!zs. ys=xs+zs  P   P" using mset_subset_eq_exists_conv
    by blast

  declare subset_mset.diff_add[simp, intro]

  lemma mset_2dist2_cases:
    assumes A: "{#a, b#} ⊆# A + B"
    assumes CASES: "{#a, b#} ⊆# A  P" "{#a, b#} ⊆# B  P"
      "a ∈# A  b ∈# B  P" "a ∈# B  b ∈# A  P"
    shows "P"
  proof -
    from A have "count A a + count B a  1"
      "count A b + count B b  1"
      using mset_subset_eq_count [of "{#a, b#}" "A + B" a] mset_subset_eq_count [of "{#a, b#}" "A + B" b]
      by (auto split: if_splits)
    then have B: "a ∈# A  a ∈# B"
      "b ∈# A  b ∈# B"
      by (auto simp add: not_in_iff Suc_le_eq)
    { assume C: "a ∈# A" "b ∈# A - {#a#}" 
      with mset_subset_eq_mono_add [of "{#a#}" "{#a#}" "{#b#}" "A-{#a#}"]
      have "{#a, b#} ⊆# A" by (auto simp: add_mset_commute)
    } moreover {
      assume C: "a ∈# A" "b ∉# A - {#a#}"
      with B A have "b ∈# B"
        by (auto simp: insert_subset_eq_iff diff_union_single_convs
            simp del: subset_mset.add_diff_assoc2)
    } moreover {
      assume C: "a ∉# A" "b ∈# B - {#a#}"
      with A have "a ∈# B" using B by blast
      with C mset_subset_eq_mono_add [of "{#a#}" "{#a#}" "{#b#}" "B-{#a#}"]
      have "{#a, b#} ⊆# B" by (auto simp: add_mset_commute)
    } moreover {
      assume C: "a ∉# A" "b ∉# B - {#a#}"
      with A have "a ∈# B  b ∈# A"
        apply (intro conjI)
         apply (auto dest!: mset_subset_eq_insertD simp: insert_union_subset_iff; fail)[]
        by (metis (no_types, lifting) B(1) add_mset_remove_trivial insert_DiffM2 
            mset_diff_cancel1elem single_subset_iff subset_eq_diff_conv subset_mset.diff_diff_right
            union_single_eq_member)
    } ultimately show P using CASES by blast
  qed

  lemma mset_union_subset_s: "{#a#}+B ⊆# C  a ∈# C  B ⊆# C"
    by (drule mset_union_subset) simp
  
  lemma mset_le_single_cases[consumes 1, case_names empty singleton]: "M⊆#{#a#}; M={#}  P; M={#a#}  P  P"
    by (induct M) auto
      
  lemma mset_le_distrib[consumes 1, case_names dist]: "X⊆#(A::'a multiset)+B; !!Xa Xb. X=Xa+Xb; Xa⊆#A; Xb⊆#B  P   P"
    by (auto elim!: mset_le_addE mset_distrib)

  lemma mset_le_mono_add_single: "a ∈# ys; b ∈# ws  {#a, b#} ⊆# ys + ws" using mset_subset_eq_mono_add[of "{#a#}" _ "{#b#}", simplified] by (simp add: add_mset_commute)

  lemma mset_size1elem: "size P  1; q ∈# P  P={#q#}"
    by (auto elim: mset_size_le1_cases)
  lemma mset_size2elem: "size P  2; {#q#}+{#q'#} ⊆# P  P={#q#}+{#q'#}"
    by (auto elim: mset_le_addE)


subsubsection ‹Image under function›

notation image_mset (infixr "`#" 90)

lemma mset_map_single_rightE[consumes 1, case_names orig]: "f `# P = {#y#}; !!x.  P={#x#}; f x = y   Q   Q"
  by (cases P) auto

lemma mset_map_split_orig: "!!M1 M2. f `# P = M1+M2; !!P1 P2. P=P1+P2; f `# P1 = M1; f `# P2 = M2  Q   Q"
  apply (induct P)
  apply fastforce
  apply (force elim!: mset_un_single_un_cases simp add: union_ac) (* TODO: This proof need's quite long. Try to write a faster one. *)
  done

lemma mset_map_id: "!!x. f (g x) = x  f `# g `# X = X"
  by (induct X) auto

text ‹The following is a very specialized lemma. Intuitively, it splits the original multiset›
text ‹The following is a very specialized   by a splitting of some pointwise supermultiset of its image.

  Application:
  This lemma came in handy when proving the correctness of a constraint system that collects at most k sized submultisets of the sets of spawned threads.
›
lemma mset_map_split_orig_le: assumes A: "f `# P ⊆# M1+M2" and EX: "!!P1 P2. P=P1+P2; f `# P1 ⊆# M1; f `# P2 ⊆# M2  Q" shows "Q"
  using A EX by (auto elim: mset_le_distrib mset_map_split_orig)


subsection ‹Lists›

subsubsection ‹Reverse lists›
  lemma list_rev_decomp[rule_format]: "l~=[]  (EX ll e . l = ll@[e])"
    apply(induct_tac l)
    apply(auto)
  done
    
  (* Was already there as rev_induct
  lemma list_rev_induct: "⟦P []; !! l e . P l ⟹ P (l@[e]) ⟧ ⟹ P l"
    by (blast intro: rev_induct)
  proof (induct l rule: measure_induct[of length])
    fix x :: "'a list"
    assume A: "∀y. length y < length x ⟶ P [] ⟶ (∀x xa. P (x::'a list) ⟶ P (x @ [xa])) ⟶ P y" "P []" and IS: "⋀l e. P l ⟹ P (l @ [e])"
    show "P x" proof (cases "x=[]")
      assume "x=[]" with A show ?thesis by simp
    next
      assume CASE: "x~=[]"
      then obtain xx e where DECOMP: "x=xx@[e]" by (blast dest: list_rev_decomp)
      hence LEN: "length xx < length x" by auto
      with A IS have "P xx" by auto
      with IS have "P (xx@[e])" by auto
      with DECOMP show ?thesis by auto
    qed
  qed
  *)

  text ‹Caution: Same order of case variables in snoc-case as @{thm [source] rev_exhaust}, the other way round than @{thm [source] rev_induct} !›
  lemma length_compl_rev_induct[case_names Nil snoc]: "P []; !! l e . !! ll . length ll <= length l  P ll  P (l@[e])  P l"
    apply(induct_tac l rule: length_induct)
    apply(case_tac "xs" rule: rev_cases)
    apply(auto)
  done

  lemma list_append_eq_Cons_cases: "ys@zs = x#xs; ys=[]; zs=x#xs  P; !!ys'.  ys=x#ys'; ys'@zs=xs   P   P"
    by (auto iff add: append_eq_Cons_conv)
  lemma list_Cons_eq_append_cases: "x#xs = ys@zs; ys=[]; zs=x#xs  P; !!ys'.  ys=x#ys'; ys'@zs=xs   P   P"
    by (auto iff add: Cons_eq_append_conv)

subsubsection "folding"

text "Ugly lemma about foldl over associative operator with left and right neutral element"
lemma foldl_A1_eq: "!!i.  !! e. f n e = e; !! e. f e n = e; !!a b c. f a (f b c) = f (f a b) c   foldl f i ww = f i (foldl f n ww)"
proof (induct ww)
  case Nil thus ?case by simp
next
  case (Cons a ww i) note IHP[simplified]=this
  have "foldl f i (a # ww) = foldl f (f i a) ww" by simp
  also from IHP have " = f (f i a) (foldl f n ww)" by blast
  also from IHP(4) have " = f i (f a (foldl f n ww))" by simp
  also from IHP(1)[OF IHP(2,3,4), where i=a] have " = f i (foldl f a ww)" by simp
  also from IHP(2)[of a] have " = f i (foldl f (f n a) ww)" by simp
  also have " = f i (foldl f n (a#ww))" by simp
  finally show ?case .
qed

lemmas foldl_conc_empty_eq = foldl_A1_eq[of "(@)" "[]", simplified]
lemmas foldl_un_empty_eq = foldl_A1_eq[of "(∪)" "{}", simplified, OF Un_assoc[symmetric]]

lemma foldl_set: "foldl (∪) {} l = {x. xset l}"
  apply (induct l)
  apply simp_all
  apply (subst foldl_un_empty_eq)
  apply auto
  done


subsubsection ‹Miscellaneous›
  lemma length_compl_induct[case_names Nil Cons]: "P []; !! e l . !! ll . length ll <= length l  P ll  P (e#l)  P l"
    apply(induct_tac l rule: length_induct)
    apply(case_tac "xs")
    apply(auto)
  done


  text ‹Simultaneous induction over two lists, prepending an element to one of the lists in each step›
  lemma list_2pre_induct[case_names base left right]: assumes BASE: "P [] []" and LEFT: "!!e w1' w2. P w1' w2  P (e#w1') w2" and RIGHT: "!!e w1 w2'. P w1 w2'  P w1 (e#w2')" shows "P w1 w2" 
  proof -
    { ― ‹The proof is done by induction over the sum of the lengths of the lists›
      fix n
      have "!!w1 w2. length w1 + length w2 = n; P [] []; !!e w1' w2. P w1' w2  P (e#w1') w2; !!e w1 w2'. P w1 w2'  P w1 (e#w2')   P w1 w2 " 
        apply (induct n)
        apply simp
        apply (case_tac w1)
        apply auto
        apply (case_tac w2)
        apply auto
        done
    } from this[OF _ BASE LEFT RIGHT] show ?thesis by blast
  qed


  lemma list_decomp_1: "length l=1  EX a . l=[a]"
    by (case_tac l, auto)

  lemma list_decomp_2: "length l=2  EX a b . l=[a,b]"
    by (case_tac l, auto simp add: list_decomp_1)


  lemma drop_all_conc: "drop (length a) (a@b) = b"
    by (simp)

  lemma list_rest_coinc: "length s2 <= length s1; s1@r1 = s2@r2  EX r1p . r2=r1p@r1"
  proof -
    assume A: "length s2 <= length s1" "s1@r1 = s2@r2"
    hence "r1 = drop (length s1) (s2@r2)" by (auto simp only:drop_all_conc dest: sym)
    moreover from A have "length s1 = length s1 - length s2 + length s2" by arith
    ultimately have "r1 = drop ((length s1 - length s2)) r2" by (auto)
    hence "r2 = take ((length s1 - length s2)) r2 @ r1" by auto
    thus ?thesis by auto
  qed

  lemma list_tail_coinc: "n1#r1 = n2#r2  n1=n2 & r1=r2"
    by (auto)


  lemma last_in_set[intro]: "l[]  last l  set l"
    by (induct l) auto

subsection ‹Induction on nat›
  lemma nat_compl_induct[case_names 0 Suc]: "P 0; !! n . ALL nn . nn <= n  P nn  P (Suc n)  P n"
    apply(induct_tac n rule: nat_less_induct)
    apply(case_tac n)
    apply(auto)
  done


subsection ‹Functions of type @{typ "boolbool"}
  lemma boolfun_cases_helper: "g=(λx. False) | g=(λx. x) | g=(λx. True) | g= (λx. ¬x)" 
  proof -
    { assume "g False" "g True"
      hence "g = (λx. True)" by (rule_tac ext, case_tac x, auto)
    } moreover {
      assume "g False" "¬g True"
      hence "g = (λx. ¬x)" by (rule_tac ext, case_tac x, auto)
    } moreover {
      assume "¬g False" "g True"
      hence "g = (λx. x)" by (rule_tac ext, case_tac x, auto)
    } moreover {
      assume "¬g False" "¬g True"
      hence "g = (λx. False)" by (rule_tac ext, case_tac x, auto)
    } ultimately show ?thesis by fast
  qed

  lemma boolfun_cases[case_names False Id True Neg]: "g=(λx. False)  P g; g=(λx. x)  P g; g=(λx. True)  P g; g=(λx. ¬x)  P g  P g"
  proof -
    note boolfun_cases_helper[of g]
    moreover assume "g=(λx. False)  P g" "g=(λx. x)  P g" "g=(λx. True)  P g" "g=(λx. ¬x)  P g"
    ultimately show ?thesis by fast
  qed


  subsection ‹Definite and indefinite description›
  text "Combined definite and indefinite description for binary predicate"
  lemma some_theI: assumes EX: "a b . P a b" and BUN: "!! b1 b2 . a . P a b1; a . P a b2  b1=b2" 
    shows "P (SOME a . b . P a b) (THE b . a . P a b)"
  proof -
    from EX have "EX b . P (SOME a . EX b . P a b) b" by (rule someI_ex)
    moreover from EX have "EX b . EX a . P a b" by blast
    with BUN theI'[of "λb . EX a . P a b"] have "EX a . P a (THE b . EX a . P a b)" by (unfold Ex1_def, blast)
    moreover note BUN
    ultimately show ?thesis by (fast)
  qed
  


end

Theory Interleave

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

text ‹
  This theory defines an operator to return the set of all possible interleavings of two lists.
›

(*
  Is ⨂-operator needed ?
    Should we better do a reformulation of ⊗ on sets of lists, to get an associative, commutative operator with identity (ACI ?) ?
*)

subsection "Definitions"

subsubsection "Prepend and concatenate lifted to sets"

definition list_set_cons :: "'a  'a list set  'a list set" (infixr "" 65)
  where [simp]: "aS = (#) a ` S"

definition list_set_append :: "'a list  'a list set  'a list set" (infixr "" 65)
  where [simp]: "aS = (@) a ` S"

subsubsection "The interleaving operator"

function
  interleave :: "'a list  'a list  'a list set" (infixr "" 64)
where
  "[]b = {b}"
  | "a[] = {a}"
  | "a#l  b#r = ((a(l  b#r))  (b(a#l  r)))"
by pat_completeness auto
termination by lexicographic_order


subsection "Properties"

subsubsection "Lifted prepend and concatenate operators"
lemma cons_set_cons_eq: "a#l  bS = (a=b & lS)"
  by auto
lemma append_set_append_eq: "length a = length b  a@l  bS = (a=b & lS)"
  by auto

lemma list_set_cons_cases[cases set]: "waS; !!w'.  w=a#w'; w'S   P  P"
  by auto
lemma list_set_append_cases[cases set]: "waS; !!w'.  w=a@w'; w'S   P  P"
  by auto

subsubsection "Standard simplification-, introduction-, elimination-, and induction rules"
lemma interleave_cons1: "l  ab  x#l  x#a  b"
  apply(case_tac b)
  apply(auto)
done
  
lemma interleave_cons2: "l  ab  x#l  a  x#b"
  apply(case_tac a)
  apply(auto)
done

lemmas interleave_cons = interleave_cons1 interleave_cons2


lemma interleave_empty[simp]: "[]ab = (a=[] & b=[])"
  apply(case_tac a)
  apply(case_tac b)
  apply(simp)
  apply(simp)
  apply(case_tac b)
  apply(auto)
done

(* TODO: Is this wise as default simp ?*)
lemma interleave_length[rule_format, simp]: "ALL x : ab . length x = length a + length b"
  apply(induct rule: interleave.induct)
  apply(auto)
done

lemma interleave_same[simp]: "yly = (l=[])"
  apply (rule iffI)
  apply (subgoal_tac "length y = length l + length y")
  apply (simp del: interleave_length)
  apply (erule interleave_length)
  apply simp
done

lemma interleave_comm[simp]: "ab = ba" (is "?P f a b")
  apply(induct rule: interleave.induct)
  apply(auto)
done

lemma interleave_cont_conc[rule_format, simp]: "ALL b . a@b  ab"
  apply(induct_tac a)
  apply(auto simp add: interleave_cons)
done

lemma interleave_cont_rev_conc[simp]: "b@a  ab"
  apply (subgoal_tac "b@a  ba")
  apply(simp)
  apply(simp only: interleave_cont_conc)
done

lemma interleave_not_empty: "ab ~= {}" 
  apply(induct rule: interleave.induct)
  apply(auto)
done

lemma cons_interleave_split: "a#l  l1l2  (EX lh . l1=a#lh & l  lhl2 | l2=a#lh & l  l1lh )"
  apply(case_tac l1)
  apply(auto)
  apply(case_tac l2)
  apply(auto)
done

lemma cons_interleave_cases[cases set, case_names left right]: "a#l  l1l2; !!lh . l1=a#lh; l  lhl2  P; !!lh. l2=a#lh; l  l1lh  P  P"
  by (blast dest: cons_interleave_split)

lemma interleave_cases[cases set, case_names empty left right]: "ll1l2;  l=[]; l1=[]; l2=[]   P; !!a l' l1'. l=a#l'; l1=a#l1'; l'l1'l2  P; !!a l' l2'. l=a#l'; l2=a#l2'; l'l1l2'  P   P"
  apply (cases l)
  apply (simp)
  apply simp
  apply (erule cons_interleave_cases)
  apply simp_all
  done

lemma interleave_elem_induct[induct set, case_names empty left right]: 
  "!!w1 w2.  ww1w2; P [] [] []; !!e w w1 w2.  P w w1 w2; ww1w2   P (e#w) (e#w1) w2; !!e w w1 w2.  P w w1 w2; ww1w2   P (e#w) w1 (e#w2)   P w w1 w2"
  by (induct w) (auto elim!: cons_interleave_cases intro!: interleave_cons)

lemma interleave_rev_cons1[rule_format]: "ALL a b . l  ab  l@[x]  a@[x]  b" (is "?P l") 
proof (induct l)
  case Nil show ?case by (simp)
  case (Cons e l)
    assume IH[rule_format]: "?P l"
    show "?P (e#l)" proof (intro allI impI)
      fix a b
      assume "e#l  ab"
      then obtain c where SPLIT: "a=e#c & lcb | b=e#c & lac" by (blast dest: cons_interleave_split)
      with IH have "a=e#c & l@[x]c@[x]b | b=e#c & l@[x]a@[x]c" by auto
      hence "a=e#c & e#l@[x]e#c@[x]b | b=e#c & e#l@[x]a@[x]e#c" by (auto simp add: interleave_cons)
      thus "(e#l)@[x]a@[x]b" by auto
    qed
qed

corollary interleave_rev_cons2: "l  ab  l@[x]  a  b@[x]"
proof -
  assume "l  ab"
  hence "lba" by auto
  hence "l@[x]  b@[x]  a" by (blast dest: interleave_rev_cons1)
  thus ?thesis by auto
qed

lemmas interleave_rev_cons = interleave_rev_cons1 interleave_rev_cons2


subsubsection "Interleaving and list concatenation"

lemma interleave_append1: "l  ab  x@l  x@a  b" proof -
  have "ALL l a b . l  ab  x@l  x@a  b" (is "?P x") proof (induct x)
    show "?P []" by simp
  next
    fix e
    fix x::"'a list"
    assume IH: "?P x"
    show "?P (e#x)" proof (intro impI allI)
      fix l::"'a list" 
      fix a b
      assume "l  a  b"
      with IH have "x@l  x@a  b" by auto
      with interleave_cons1 show "(e # x) @ l  (e # x) @ a  b" by force
    qed
  qed
  moreover assume "l  a  b"
  ultimately show ?thesis by blast
qed

lemma interleave_append2: "l  ab  x@l  a  x@b" proof -
  have "ALL l a b . l  ab  x@l  a  x@b" (is "?P x") proof (induct x)
    show "?P []" by simp
  next
    fix a 
    fix x::"'a list"
    assume IH: "l a b. l  a  b  x @ l  a  x @ b"
    show "l aa b. l  aa  b  (a # x) @ l  aa  (a # x) @ b" proof (intro impI allI)
      fix l::"'a list" 
      fix aa b
      assume "l  aa  b"

      with IH have "x@l  aa  x@b" by auto
      with interleave_cons2 show "(a # x) @ l  aa  (a # x) @ b" by force
    qed
  qed
  moreover assume "l  a  b"
  ultimately show ?thesis by blast
qed

lemmas interleave_append = interleave_append1 interleave_append2

lemma interleave_rev_append1: "!!a b w. wab  w@w'  a@w'  b"
proof (induct w' rule: rev_induct)
  case Nil thus ?case by simp
next
  case (snoc e w') note IHP=this
  hence "w@w'a@w'b" by auto
  thus ?case using interleave_rev_cons1[of "w@w'" "a@w'" "b"] by (simp)
qed
lemma interleave_rev_append2: "wab  w@w'  a  b@w'"
  by (simp only: interleave_comm[of a b] interleave_comm[of a "b@w'"]) (blast dest: interleave_rev_append1)
lemmas interleave_rev_append = interleave_rev_append1 interleave_rev_append2

lemma interleave_rev1[rule_format]: "ALL w1 w2 . (ww1w2)  (rev w  rev w1  rev w2)" (is "?P w")
proof (induct w)
  case Nil show ?case by (simp)
  case (Cons e w)
    assume IH[rule_format]: "?P w"
    show ?case proof (clarsimp)
      fix w1 w2
      assume "e # w  w1  w2"
      then obtain w' where "w1=e#w' & ww'w2 | w2=e#w' & ww1w'" by (blast dest: cons_interleave_split)
      with IH have "w1=e#w' & rev wrev w'  rev w2 | w2=e#w' & rev w  rev w1  rev w'" by auto
      thus "rev w @ [e]rev w1  rev w2" by (auto simp add: interleave_rev_cons)
    qed
qed

corollary interleave_rev2: "(rev w  rev w1  rev w2)  (ww1w2)" 
  apply (subgoal_tac "(rev wrev w1rev w2) = (rev (rev w)  rev (rev w1)  rev (rev w2))")
  apply(simp)
  apply (blast dest: interleave_rev1)
done

lemmas interleave_rev = interleave_rev1 interleave_rev2

lemma rev_cons_interleave_split: "l@[a]  l1l2  (EX lh . l1=lh@[a] & l  lhl2 | l2=lh@[a] & l  l1lh )"
proof -
  assume "l@[a]  l1l2"
  hence "a#rev l  rev l1  rev l2" by (auto dest: interleave_rev)
  then obtain lh where "rev l1 = a#lh & rev l  lhrev l2 | rev l2 = a#lh & rev l  rev l1  lh" by (blast dest: cons_interleave_split)
  hence "rev l1 = a#lh & l  rev lh  l2 | rev l2 = a#lh & l  l1  rev lh" by (auto dest: interleave_rev)
  hence "l1 = rev lh @ [a] & l  rev lh  l2 | l2 = rev lh @ [a] & l  l1  rev lh" by (simp add: rev_swap)
  thus ?thesis by blast
qed

subsubsection "Associativity"
 
lemma interleave_s_assoc1[rule_format]: "ALL w1 ws w2 w3 . (ww1ws & wsw2w3  (EX ws' : w1w2 . w  ws'w3))" proof (induct w)
  case Nil show ?case by (auto)
  case (Cons e w)
    assume IH: "ALL w1 ws w2 w3 . ww1ws & wsw2w3  (EX ws' : w1w2 . w  ws'w3)"
    show ?case proof (intro impI allI)
      fix w1 ws w2 w3
      assume A: "e#w  w1  ws  ws  w2  w3"
      then obtain wh where CASES: "w1=e#wh & wwhws | ws=e#wh & ww1wh" by (blast dest!: cons_interleave_split)
      moreover {
        assume CASE: "w1=e#wh & wwhws"
        with A IH obtain ws' where "ws'whw2 & wws'w3" by (blast)
        hence "e#ws' (e#wh)w2 & e#w  (e#ws')w3" by (auto simp add: interleave_cons)
        with CASE have "ws'w1  w2. e # w  ws'  w3" by blast
      } moreover {
        assume CASE: "ws=e#wh & ww1wh"
        with A obtain whh where "w2=e#whh & whwhhw3 | w3=e#whh & whw2whh" by (blast dest!: cons_interleave_split)
        moreover {
          assume SCASE: "w2=e#whh & whwhhw3"
          with CASE IH obtain ws' where "ws'w1whh & wws'w3" by blast
          with SCASE have "e#ws'w1w2 & e#w  (e#ws')w3" by (auto simp add: interleave_cons)
          hence "ws'w1  w2. e # w  ws'  w3" by blast
        } moreover {
          assume SCASE: "w3=e#whh & whw2whh"
          with CASE IH obtain ws' where "ws'w1w2 & wws'whh" by blast
          with SCASE have "ws'w1w2 & e#w  ws'w3" by (auto simp add: interleave_cons)
          hence "ws'w1  w2. e # w  ws'  w3" by blast
        } ultimately have "ws'w1  w2. e # w  ws'  w3" by blast
      } ultimately show "ws'w1  w2. e # w  ws'  w3" by blast
    qed
qed

lemma interleave_s_assoc2: "wwsw3; wsw1w2  EX ws' : w2w3 . w  w1ws'" proof -
  assume "w  ws  w3" "ws  w1  w2"
  hence "w  w3  ws & ws  w2  w1" by simp
  hence "EX ws':w3w2 . wws'w1" by (simp only: interleave_s_assoc1)
  thus ?thesis by simp
qed
  
lemmas interleave_s_assoc = interleave_s_assoc1 interleave_s_assoc2

subsubsection "Relation to other standard list operations"

lemma interleave_set: "ww1w2  set w = set w1  set w2"
  by (induct rule: interleave_elem_induct) auto
lemma interleave_map: "ww1w2  map f w  map f w1  map f w2"
  by (induct rule: interleave_elem_induct) (auto intro!: interleave_cons)
lemma interleave_filter: "ww1w2  filter f w  filter f w1  filter f w2"
  by (induct rule: interleave_elem_induct) (auto intro!: interleave_cons)


subsubsection "Relation to sublist order"

lemma ileq_interleave_alt: "l'l == lb. llb  l'" proof (rule eq_reflection)
  {fix l' l have "l'l  lb. llb  l'" by (induct rule: less_eq_list_induct) (simp, (blast intro: interleave_cons)+)}
  moreover {fix l have "!!lb l'. llbl'  l'l" by (induct l) (auto intro: less_eq_list_drop elim!: cons_interleave_cases)}
  ultimately show "(l'l) = (lb. llb  l')" by blast
qed

lemma ileq_interleave: "ww1w2  w1w & w2w"
  by (unfold ileq_interleave_alt, auto)

lemma ilt_ex_notempty: "x < y  (xs. xs  []  y  xs  x)"
  apply (auto simp add: order_less_le ileq_interleave_alt)
  apply (case_tac lb)
  apply auto
done


lemma ilt_interleave1: "ww1w2; w1~=[]  w2<w"
  by (simp only: ilt_ex_notempty, blast)
lemma ilt_interleave2: "ww1w2; w2~=[]  w1<w"
  by (simp only: ilt_ex_notempty interleave_comm[of w1 w2], blast)
lemmas ilt_interleave = ilt_interleave1 ilt_interleave2


subsubsection "Exotic/specialized lemmas"
― ‹Recover structure of @{text w} wrt. to structure of @{text "w1"}
lemma interleave_recover1[rule_format]: "ALL w1a w1b w2 . w(w1a@w1b)w2  (EX wa wb w2a w2b . w=wa@wb & w2=w2a@w2b & waw1aw2a & wbw1bw2b)" 
  (is "?P w" is "ALL w1a w1b w2 . ?PRE w w1a w1b w2  ?CONS w w1a w1b w2")
proof (induct w)
  case Nil show ?case by (auto)
  case (Cons e w)
    assume IH[rule_format]: "?P w"
    show "?P (e#w)" proof (intro allI impI)
      fix w1a w1b w2
      assume PRE: "e # w  w1a @ w1b  w2"
      {
        assume CASE: "w1a=[]"
        with PRE have "e#w=[]@(e#w) & w2=[]@w2 & []w1a[] & e#ww1bw2" by (auto)
        hence "?CONS (e#w) w1a w1b w2" by blast
      } moreover {
        assume CASE: "w1a~=[]"
        with PRE obtain wh where SCASES: "w1a@w1b=e#wh & wwhw2 | w2=e#wh & ww1a@w1bwh" by (blast dest: cons_interleave_split)
        moreover {
          assume SCASE: "w1a@w1b=e#wh & wwhw2"
          with CASE obtain w1ah where W1AFMT: "w1a=e#w1ah & w1ah@w1b=wh" by (cases w1a, auto)
          with SCASE have "ww1ah@w1bw2" by auto
          with IH[of w1ah w1b w2] obtain wa wb w2a w2b where "w=wa@wb & w2=w2a@w2b & waw1ahw2a & wbw1bw2b" by (blast)
          with W1AFMT have "e#w=(e#wa)@wb & e#we#wawb & w2=w2a@w2b & e#waw1aw2a & wbw1bw2b" by (auto simp add: interleave_cons)
          hence "?CONS (e#w) w1a w1b w2" by blast
        } moreover {
          assume SCASE: "w2=e#wh & ww1a@w1bwh"
          with IH[of w1a w1b wh] obtain wa wb w2a w2b where "w=wa@wb & wh=w2a@w2b & waw1aw2a & wbw1bw2b" by blast
          with SCASE have "e#w=(e#wa)@wb & w2=(e#w2a)@w2b & e#waw1ae#w2a & wbw1bw2b" by (auto simp add: interleave_cons)
          hence "?CONS (e#w) w1a w1b w2" by blast
        }
        ultimately have "?CONS (e#w) w1a w1b w2" by blast
      }
      ultimately show "?CONS (e#w) w1a w1b w2" by blast
    qed
qed

lemma interleave_recover2: "ww1(w2a@w2b)  EX wa wb w1a w1b . w=wa@wb & w1=w1a@w1b & waw1aw2a & wbw1bw2b"
proof -
  assume "ww1(w2a@w2b)"
  hence "w(w2a@w2b)w1" by auto
  hence "EX wa wb w1a w1b . w=wa@wb & w1=w1a@w1b & waw2aw1a & wbw2bw1b" by (blast dest: interleave_recover1)
  thus ?thesis by auto
qed

lemmas interleave_recover = interleave_recover1 interleave_recover2

― ‹Split operands according to element of result›
lemma interleave_unconc: "!! l2 w1 w2 . l1@l2  w1w2   w11 w12 w21 w22 . w1=w11@w12  w2=w21@w22  l1w11w21  l2w12w22"
proof (induct l1)
  case Nil hence "w1=[]@w1 & w2=[]@w2 & [][][] & l2w1w2" by auto
  thus ?case by fast
next
  case (Cons e l1') note IHP=this
  hence "e#(l1'@l2)w1w2" by auto
  with cons_interleave_split obtain w' where "(w1=e#w' & l1'@l2w'w2) | (w2=e#w' & l1'@l2w1w')" (is "?C1 | ?C2") by (fast)
  moreover {
    assume CASE: ?C1
    moreover then obtain w11' w12' w21 w22 where "w'=w11'@w12'  w2=w21@w22  l1'w11'w21  l2w12'w22" by (fast dest: IHP(1))
    moreover hence "e#w'=(e#w11')@w12' & e#l1'(e#w11')w21" by (auto dest: interleave_cons)
    ultimately have ?case by fast
  } moreover {
    assume CASE: ?C2
    moreover then obtain w11 w12 w21' w22' where "w1=w11@w12  w'=w21'@w22'  l1'w11w21'  l2w12w22'" by (fast dest: IHP(1))
    moreover hence "e#w'=(e#w21')@w22' & e#l1'w11(e#w21')" by (auto dest: interleave_cons)
    ultimately have ?case by fast
  } ultimately show ?case by fast
qed

― ‹Reverse direction of @{thm [source] "interleave_unconc"}
lemma interleave_reconc: "!!w11 w21 l2 w12 w22 . l1w11w21;l2w12w22  l1@l2(w11@w12)(w21@w22)"
proof (induct l1)
  case Nil thus ?case by (auto)
next
  case (Cons e l1') note IHP=this
  then obtain w' where "(w11=e#w' & l1'w'w21) | (w21=e#w' & l1'w11w')" (is "?C1 | ?C2") by (fast dest: cons_interleave_split)
  moreover {
    assume CASE: ?C1
    moreover with IHP have "l1'@l2(w'@w12)(w21@w22)" by auto
    ultimately have ?case by (auto dest: interleave_cons)
  } moreover {
    assume CASE: ?C2
    moreover with IHP have "l1'@l2(w11@w12)(w'@w22)" by auto
    ultimately have ?case by (auto dest: interleave_cons)
  } ultimately show ?case by fast
qed

(* interleave_unconc and interleave_reconc as equivalence *)
lemma interleave_unconc_eq: "!! l2 w1 w2 . l1@l2  w1w2 = ( w11 w12 w21 w22 . w1=w11@w12  w2=w21@w22  l1w11w21  l2w12w22)"
  by (fast dest: interleave_reconc interleave_unconc)


end

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: "ww'  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. eset 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]: "
   we1#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]: "
   wwaα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'; ww1'αw2; fst (α e)  mon_pl (map α w2) = {}   P;
  !!w2'. w2=e#w2'; ww1α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.  
    ww1α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.  
    ww1α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: "wwaαwb; fst (α e)  mon_pl (map α wb) = {} 
                   e#w  e#waα wb"
  by (cases wb) auto
lemma cil_cons2: "wwaα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'  ww'"
  apply (induct w α w' rule: cil.induct)
  apply simp_all
  apply safe
  apply auto
  done

lemma cil_subset_il': "ww1αw2  ww1w2" 
  using cil_subset_il by (auto)

― ‹Consistent interleaving preserves the set of letters of both operands›
lemma cil_set: "ww1αw2  set w = set w1  set w2"
  by (induct rule: cil_set_induct_fixα) auto
corollary cil_mon_pl: "ww1α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]: "wwaα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: "ww1αw2  w1w  w2w"
  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.  wwlαw3; wlw1αw2  
   wr. ww1αwr  wrw2α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#we#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: "ww1αwr" and B: "wrw2αw3" 
  shows "wl. wwlαw3  wlw1αw2" 
proof -
  from A have A': "wwrαw1" by (simp add: cil_commute)
  from B have B': "wrw3α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: "ww1(α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

Theory AcquisitionHistory

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

text ‹The concept of {\em acquisition histories} was introduced by Kahlon, Ivancic, and Gupta \cite{KIG05} as a bounded size abstraction of executions that acquire and release locks that contains enough information
  to decide consistent interleavability. In this work, we use this concept for reentrant monitors.
  As in Section~\ref{thy:ConsInterleave}, we encode monitor usage information in pairs of sets of monitors, and regard lists of such pairs as (abstract) executions.
  An item @{term "(E,U)"} of such a list describes a sequence of steps of the concrete execution that first enters the monitors in @{term E} and then passes through the monitors in @{term U}. The monitors in @{term E} are
  never left by the execution. Note that due to the syntactic binding of monitors to the program structure, any execution of a single thread can be abstracted to a sequence of @{term "(E,U)"}-pairs. 
  Restricting the possible schedules (see Section \ref{thy:Normalization}) will allow us to also abstract executions reaching a single program point to a sequence of such pairs.

  We want to decide whether two executions are interleavable. The key observation of \cite{KIG05} is, that two executions @{term "e"} and @{term "e'"} are {\em not} interleavable if and only if 
  there is a conflicting pair @{term "(m,m')"} of monitors, such that @{term e} enters (and never leaves) @{term m} and then uses @{term m'} and @{term e'} enters (and never leaves) @{term m'} and then uses @{term m}.  

  An acquisition history is a map from monitors to set of monitors. The acquisition history of an execution maps a monitor @{term m} that is allocated at the end of the execution to all monitors that are used after or in the 
  same step that finally enters @{term m}. Monitors that are not allocated at the end of an execution are mapped to the empty set. Though originally used for a setting without reentrant monitors, acquisition histories also work
  for our setting with reentrant monitors. 

  This theory contains the definition of acquisition histories and acquisition history interleavability, an ordering on acquisition histories that reflects the blocking potential of acquisition histories, 
  and a mapping function from paths to acquisition histories that is shown to be compatible with monitor consistent interleaving.›

subsection "Definitions"
text ‹Acquisition histories are modeled as functions from monitors to sets of monitors. Intuitively @{term "m'h m"} models that an execution finally is in @{term m}, and monitor @{term m'} has been used (i.e. passed or entered)
  after or at the same time @{term m} has been finally entered. By convention, we have @{term "mh m"} or @{term "h m = {}"}.
›

  (* TODO: Make acquisition histories an own type, with access and update operator of sort order  *)
definition "ah == { (h::'m  'm set) .  m. h m = {}  mh m }"

lemma ah_cases[cases set]: "hah; h m = {}  P ; m  h m  P  P"
  by (unfold ah_def) blast

subsection "Interleavability"
text ‹Two acquisition histories @{term h1} and @{term h2} are considered interleavable, iff there is no conflicting pair of monitors @{term m1} and @{term m2}, 
  where a pair of monitors @{term m1} and @{term m2} is called {\em conflicting} iff @{term m1} is used in @{term h2} after entering @{term m2} and, vice versa, @{term m2} is used in @{term h1} after entering @{term m1}.›  
definition
  ah_il :: "('m  'm set)  ('m  'm set)  bool" (infix "[*]" 65) 
  where
  "h1 [*] h2 == ¬(m1 m2. m1h2 m2  m2  h1 m1)"

text ‹From our convention, it follows (as expected) that the sets of entered monitors (lock-sets) of two interleavable acquisition histories are disjoint›
lemma ah_il_lockset_disjoint: 
  " h1ah; h2ah; h1 [*] h2   h1 m = {}  h2 m = {}"
  by (unfold ah_il_def) (auto elim: ah_cases)    

text ‹Of course, acquisition history interleavability is commutative›
lemma ah_il_commute: "h1 [*] h2  h2 [*] h1"
  by (unfold ah_il_def) auto

subsection "Used monitors"
text ‹Let's define the monitors of an acquisition history, as all monitors that occur in the acquisition history›
definition 
  mon_ah :: "('m  'm set)  'm set"
  where
  "mon_ah h == { h(m) | m. True}"


subsection "Ordering"
text ‹The element-wise subset-ordering on acquisition histories intuitively reflects the blocking potential: The bigger the acquisition history, the fewer acquisition histories are interleavable with it.›
text ‹Note that the Isabelle standard library automatically lifts the subset ordering to functions, so we need no explicit definition here.›
  
― ‹The ordering is compatible with interleavability, i.e.\ smaller acquisition histories are more likely to be interleavable.›
lemma ah_leq_il: " h1 [*] h2; h1'  h1; h2'  h2   h1' [*] h2'"
  by (unfold ah_il_def le_fun_def [where 'b="'a set"]) blast+
lemma ah_leq_il_left: " h1 [*] h2; h1'  h1   h1' [*] h2" and 
      ah_leq_il_right: " h1 [*] h2; h2'  h2   h1 [*] h2'"
  by (unfold ah_il_def le_fun_def [where 'b="'a set"]) blast+

subsection "Acquisition histories of executions"
text ‹Next we define a function that abstracts from executions (lists of enter/use pairs) to acquisition histories›
primrec αah :: "('m set × 'm set) list  'm  'm set" where
  "αah [] m = {}"
| "αah (e#w) m = (if mfst e then fst e  snd e  mon_pl w else αah w m)"

― ‹@{term αah} generates valid acquisition histories›
lemma αah_ah: "αah w  ah"
  apply (induct w)
  apply (unfold ah_def)
  apply simp
  apply (fastforce split: if_split_asm)
  done

lemma αah_hd: "mfst e; xfst e  snd e  mon_pl w  xαah (e#w) m"
  by auto
lemma αah_tl: "mfst e; xαah w m  xαah (e#w) m"
  by auto

lemma αah_cases[cases set, case_names hd tl]: "
    xαah w m; 
    !!e w'. w=e#w'; mfst e; xfst e  snd e  mon_pl w'  P; 
    !!e w'. w=e#w'; mfst e; xαah w' m  P
    P"
  by (cases w) (simp_all split: if_split_asm)

lemma αah_cons_cases[cases set, case_names hd tl]: "
    xαah (e#w') m;  
    mfst e; xfst e  snd e  mon_pl w'  P; 
    mfst e; xαah w' m  P
    P"
  by (simp_all split: if_split_asm)

lemma mon_ah_subset: "mon_ah (αah w)  mon_pl w"
  by (induct w) (auto simp add: mon_ah_def)

― ‹Subwords generate smaller acquisition histories›
lemma αah_ileq: "w1w2  αah w1  αah w2" 
proof (induct rule: less_eq_list_induct)
  case empty thus ?case by (unfold le_fun_def [where 'b="'a set"], simp)
next
  case (drop l' l a) show ?case
  proof (unfold le_fun_def  [where 'b="'a set"], intro allI subsetI)
    fix m x
    assume A: "x  αah l' m"
    with drop(2) have "xαah l m" by (unfold le_fun_def  [where 'b="'a set"], auto)
    moreover hence "xmon_pl l" using mon_ah_subset[unfolded mon_ah_def] by fast
    ultimately show "xαah (a # l) m" by auto
  qed
next
  case (take a b l' l) show ?case
  proof (unfold le_fun_def [where 'b="'a set"], intro allI subsetI)
    fix m x
    assume A: "xαah (a#l') m"
    thus "x  αah (b # l) m"
    proof (cases rule: αah_cons_cases)
      case hd
      with mon_pl_ileq[OF take.hyps(2)] and a = b
      show ?thesis by auto
    next
      case tl
      with take.hyps(3)[unfolded le_fun_def [where 'b="'a set"]] and a = b
      show ?thesis by auto
    qed
  qed
qed
      
text ‹We can now prove the relation of monitor consistent interleavability and interleavability of the acquisition histories.›
lemma ah_interleavable1: 
  "w  w1α w2  αah (map α w1) [*] αah (map α w2)" 
  ― ‹The lemma is shown by induction on the structure of the monitor consistent interleaving operator›
proof (induct w α w1 w2 rule: cil_set_induct_fixα) 
  case empty show ?case by (simp add: ah_il_def) ― ‹The base case is trivial by the definition of @{term "([*])"}
next
  ― ‹Case: First step comes from the left word›
  case (left e w' w1' w2) show ?case 
  proof (rule ccontr) ― ‹We do a proof by contradiction›
    ― ‹Assume there is a conflicting pair in the acquisition histories›
    assume "¬ αah (map α (e # w1')) [*] αah (map α w2)" 
    then obtain m1 m2 where CPAIR: "m1  αah (map α (e#w1')) m2" "m2  αah (map α w2) m1" by (unfold ah_il_def, blast) 
    ― ‹It comes either from the first step or not›
    from CPAIR(1) have "(m2fst (α e)  m1  fst (α e)  snd (α e)  mon_pl (map α w1'))  (m2fst (α e)  m1  αah (map α w1') m2)" (is "?CASE1  ?CASE2") 
      by (auto split: if_split_asm) 
    moreover {
      ― ‹Case: One monitor of the conflicting pair is entered in the first step of the left path›
      assume ?CASE1 hence C: "m2fst (α e)" .. 
      ― ‹Because the paths are consistently interleavable, the monitors entered in the first step must not occur in the other path›
      from left(2) mon_ah_subset[of "map α w2"] have "fst (α e)  mon_ah (αah (map α w2)) = {}" by auto 
      ― ‹But this is a contradiction to being a conflicting pair›
      with C CPAIR(2) have False by (unfold mon_ah_def, blast) 
    } moreover {
      ― ‹Case: The first monitor of the conflicting pair is entered after the first step of the left path›
      assume ?CASE2 hence C: "m1  αah (map α w1') m2" .. 
      ― ‹But this is a contradiction to the induction hypothesis, that says that the acquisition histories of the tail of the left path and the 
        right path are interleavable›
      with left(3) CPAIR(2) have False by (unfold ah_il_def, blast) 
    } ultimately show False ..
  qed
next
  ― ‹Case: First step comes from the right word. This case is shown completely analogous›
  case (right e w' w2' w1) show ?case 
  proof (rule ccontr)
    assume "¬ αah (map α w1) [*] αah (map α (e#w2'))" 
    then obtain m1 m2 where CPAIR: "m1  αah (map α w1) m2" "m2  αah (map α (e#w2')) m1" by (unfold ah_il_def, blast) 
    from CPAIR(2) have "(m1fst (α e)  m2  fst (α e)  snd (α e)  mon_pl (map α w2'))  (m1fst (α e)  m2  αah (map α w2') m1)" (is "?CASE1  ?CASE2") 
      by (auto split: if_split_asm)
    moreover {
      assume ?CASE1 hence C: "m1fst (α e)" .. 
      from right(2) mon_ah_subset[of "map α w1"] have "fst (α e)  mon_ah (αah (map α w1)) = {}" by auto 
      with C CPAIR(1) have False by (unfold mon_ah_def, blast) 
    } moreover {
      assume ?CASE2 hence C: "m2  αah (map α w2') m1" .. 
      with right(3) CPAIR(1) have False by (unfold ah_il_def, blast) 
    } ultimately show False ..
  qed
qed


lemma ah_interleavable2: 
  assumes A: "αah (map α w1) [*] αah (map α w2)" 
  shows "w1α w2  {}"
  ― ‹This lemma is shown by induction on the sum of the word lengths›
proof -
  ― ‹To apply this induction in Isabelle, we have to rewrite the lemma a bit›
  { fix n
    have "!!w1 w2. αah (map α w1) [*] αah (map α w2); n=length w1 + length w2  w1α w2  {}" 
    proof (induct n rule: nat_less_induct[case_names I])
      ― ‹We first rule out the cases that one of the words is empty›
      case (I n w1 w2) show ?case proof (cases w1) 
        ― ‹If the first word is empty, the lemma is trivial›
        case Nil with I.prems show ?thesis by simp 
      next
        case (Cons e1 w1') note CONS1=this show ?thesis proof (cases w2)
          ― ‹If the second word is empty, the lemma is also trivial›
          case Nil with I.prems show ?thesis by simp 
        next
          ― ‹The interesting case is if both words are not empty›
          case (Cons e2 w2') note CONS2=this 
          ― ‹In this case, we check whether the first step of one of the words can safely be executed without blocking any steps of the other word›
          show ?thesis proof (cases "fst (α e1)  mon_pl (map α w2) = {}")
            case True ― ‹The first step of the first word can safely be executed›
            ― ‹From the induction hypothesis, we get that there is a consistent interleaving of the rest of the first word and the second word›
            have "w1'αw2  {}" proof -
              from I.prems(1) CONS1 ah_leq_il_left[OF _ αah_ileq[OF le_list_map, OF less_eq_list_drop[OF order_refl]]] have "αah (map α w1') [*] αah (map α w2)" by fast
              moreover from CONS1 I.prems(2) have "length w1'+length w2 < n" by simp
              ultimately show ?thesis using I.hyps by blast
            qed
            ― ‹And because the first step of the first word can be safely executed, we can prepend it to that consistent interleaving›
            with cil_cons1[OF _ True] CONS1 show ?thesis by blast
          next
            case False note C1=this
            show ?thesis proof (cases "fst (α e2)  mon_pl (map α w1) = {}")
              case True ― ‹The first step of the second word can safely be executed›
              ― ‹This case is shown analogously to the latter one›
              have "w1αw2'  {}" proof -
                from I.prems(1) CONS2 ah_leq_il_right[OF _ αah_ileq[OF le_list_map, OF less_eq_list_drop[OF order_refl]]] have "αah (map α w1) [*] αah (map α w2')" by fast
                moreover from CONS2 I.prems(2) have "length w1+length w2' < n" by simp
                ultimately show ?thesis using I.hyps by blast
              qed
              with cil_cons2[OF _ True] CONS2 show ?thesis by blast
            next
              case False note C2=this ― ‹Neither first step can safely be executed. This is exactly the situation from that we can extract a conflicting pair›
              from C1 C2 obtain m1 m2 where "m1fst (α e1)" "m1mon_pl (map α w2)" "m2fst (α e2)" "m2mon_pl (map α w1)" by blast
              with CONS1 CONS2 have "m2  αah (map α w1) m1" "m1  αah (map α w2) m2" by auto
              ― ‹But by assumption, there are no conflicting pairs, thus we get a contradiction›
              with I.prems(1) have False by (unfold ah_il_def) blast 
              thus ?thesis ..
            qed
          qed
        qed
      qed
    qed
  } with A show ?thesis by blast
qed
              
  
text ‹Finally, we can state the relationship between monitor consistent interleaving and interleaving of acquisition histories›
theorem ah_interleavable: 
  "(αah (map α w1) [*] αah (map α w2))  (w1αw2{})" 
  using ah_interleavable1 ah_interleavable2 by blast

subsection "Acquisition history backward update"
text ‹We define a function to update an acquisition history backwards. This function is useful for constructing acquisition histories in backward constraint systems.›
definition
  ah_update :: "('m  'm set)  ('m set * 'm set)  'm set  ('m  'm set)"
  where
  "ah_update h F M m == if mfst F then fst F  snd F  M else h m"

text ‹
  Intuitively, @{term "ah_update h (E,U) M m"} means to prepend a step @{term "(E,U)"} to the acquisition history @{term h} of a path that uses monitors @{term M}. Note that we need the extra parameter @{term M}, since
  an acquisition history does not contain information about the monitors that are used on a path before the first monitor that will not be left has been entered. 
›
lemma ah_update_cons: "αah (e#w) = ah_update (αah w) e (mon_pl w)"
  by (auto intro!: ext simp add: ah_update_def)

text ‹The backward-update function is monotonic in the first and third argument as well as in the used monitors of the second argument. 
  Note that it is, in general, not monotonic in the entered monitors of the second argument.›
lemma ah_update_mono: "h  h'; F=F'; MM' 
   ah_update h F M  ah_update h' F' M'"
  by (auto simp add: ah_update_def le_fun_def [where 'b="'a set"])
lemma ah_update_mono2: "h  h'; UU'; MM' 
   ah_update h (E,U) M  ah_update h' (E,U') M'"
  by (auto simp add: ah_update_def le_fun_def [where 'b="'a set"])

end

Theory LTS

(*  Title:       Conflict analysis/Labelled transition systems
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)
section ‹Labeled transition systems›
theory LTS
imports Main
begin
text_raw ‹\label{thy:LTS}›

text ‹
  Labeled transition systems (LTS) provide a model of a state transition system with named transitions.
›

subsection ‹Definitions›
text ‹An LTS is modeled as a ternary relation between start configuration, transition label and end configuration›
type_synonym ('c,'a) LTS = "('c × 'a × 'c) set"

text ‹Transitive reflexive closure›

inductive_set 
  trcl :: "('c,'a) LTS  ('c,'a list) LTS"
  for t
  where
  empty[simp]: "(c,[],c)  trcl t"
  | cons[simp]: " (c,a,c')  t; (c',w,c'')  trcl t   (c,a#w,c'')  trcl t"

subsection ‹Basic properties of transitive reflexive closure›
lemma trcl_empty_cons: "(c,[],c')trcl t  (c=c')"
  by (auto elim: trcl.cases)
lemma trcl_empty_simp[simp]: "(c,[],c')trcl t = (c=c')"
  by (auto elim: trcl.cases intro: trcl.intros)

lemma trcl_single[simp]: "((c,[a],c')  trcl t) = ((c,a,c')  t)"
  by (auto elim: trcl.cases)
lemma trcl_uncons: "(c,a#w,c')trcl t  ch . (c,a,ch)t  (ch,w,c')  trcl t"
  by (auto elim: trcl.cases)
lemma trcl_uncons_cases: "
    (c,e#w,c')trcl S; 
    !!ch.  (c,e,ch)S; (ch,w,c')trcl S   P 
    P"
  by (blast dest: trcl_uncons)
lemma trcl_one_elem: "(c,e,c')t  (c,[e],c')trcl t"
  by auto

lemma trcl_unconsE[cases set, case_names split]: " 
    (c,e#w,c')trcl S; 
    !!ch. (c,e,ch)S; (ch,w,c')trcl S  P
    P"
  by (blast dest: trcl_uncons)
lemma trcl_pair_unconsE[cases set, case_names split]: " 
    ((s,c),e#w,(s',c'))trcl S; 
    !!sh ch. ((s,c),e,(sh,ch))S; ((sh,ch),w,(s',c'))trcl S  P
    P"
  by (fast dest: trcl_uncons)

lemma trcl_concat: "!! c .  (c,w1,c')trcl t; (c',w2,c'')trcl t  
   (c,w1@w2,c'')trcl t" 
proof (induct w1)
  case Nil thus ?case by (subgoal_tac "c=c'") auto
next
  case (Cons a w) thus ?case by (auto dest: trcl_uncons) 
qed    
  
lemma trcl_unconcat: "!! c . (c,w1@w2,c')trcl t 
   ch . (c,w1,ch)trcl t  (ch,w2,c')trcl t" 
proof (induct w1)
  case Nil hence "(c,[],c)trcl t  (c,w2,c')trcl t" by auto
  thus ?case by fast
next
  case (Cons a w1) note IHP = this
  hence "(c,a#(w1@w2),c')trcl t" by simp (* Auto/fast/blast do not get the point _#(_@_) = (_#_)@_ in next step, so making it explicit *)
  with trcl_uncons obtain chh where "(c,a,chh)t  (chh,w1@w2,c')trcl t" by fast
  moreover with IHP obtain ch where "(chh,w1,ch)trcl t  (ch,w2,c')trcl t" by fast
  ultimately have "(c,a#w1,ch)trcl t  (ch,w2,c')trcl t" by auto
  thus ?case by fast
qed

subsubsection "Appending of elements to paths"
lemma trcl_rev_cons: " (c,w,ch)trcl T; (ch,e,c')T   (c,w@[e],c')trcl T"
  by (auto dest: trcl_concat iff add: trcl_single)
lemma trcl_rev_uncons: "(c,w@[e],c')trcl T 
   ch. (c,w,ch)trcl T  (ch,e,c')T"
  by (force dest: trcl_unconcat)
lemma trcl_rev_induct[induct set, consumes 1, case_names empty snoc]: "!! c'.  
    (c,w,c')trcl S; 
    !!c. P c [] c; 
    !!c w c' e c''.  (c,w,c')trcl S; (c',e,c'')S; P c w c'   P c (w@[e]) c'' 
    P c w c'"
  by (induct w rule: rev_induct) (auto dest: trcl_rev_uncons)
lemma trcl_rev_cases: "!!c c'.  
    (c,w,c')trcl S; 
    w=[]; c=c'P; 
    !!ch e wh.  w=wh@[e]; (c,wh,ch)trcl S; (ch,e,c')S P 
    P"
  by (induct w rule: rev_induct) (auto dest: trcl_rev_uncons)

lemma trcl_cons2: " (c,e,ch)T; (ch,f,c')T   (c,[e,f],c')trcl T"
  by auto

subsubsection "Transitivity reasoning setup"
declare trcl_cons2[trans]    ― ‹It's important that this is declared before @{thm [source] trcl_concat}, because we want @{thm [source] trcl_concat} to be tried first by the transitivity reasoner›
declare cons[trans]
declare trcl_concat[trans]
declare trcl_rev_cons[trans]

subsubsection "Monotonicity"
lemma trcl_mono: "!!A B. A  B  trcl A  trcl B" (* FIXME: Why can't this be declared as [mono] or [mono_set] ? *) 
  apply (clarsimp)
  apply (erule trcl.induct)
  apply auto
done

lemma trcl_inter_mono: "xtrcl (SR)  xtrcl S" "xtrcl (SR)  xtrcl R"
proof -
  assume "xtrcl (SR)"
  with trcl_mono[of "SR" S] show "xtrcl S" by auto
next
  assume "xtrcl (SR)"
  with trcl_mono[of "SR" R] show "xtrcl R" by auto
qed


subsubsection "Special lemmas for reasoning about states that are pairs"
lemmas trcl_pair_induct = trcl.induct[of "(xc1,xc2)" "xb" "(xa1,xa2)", split_format (complete), consumes 1, case_names empty cons]
lemmas trcl_rev_pair_induct = trcl_rev_induct[of "(xc1,xc2)" "xb" "(xa1,xa2)", split_format (complete), consumes 1, case_names empty snoc]

(*lemma trcl_pair_induct[induct set]: 
  "⟦((xc1,xc2), xb, (xa1,xa2)) ∈ trcl t; ⋀c1 c2. P c1 c2 [] c1 c2; ⋀a c1 c2 c1' c2' c1'' c2'' w. ⟦((c1,c2), a, (c1',c2')) ∈ t; ((c1',c2'), w, (c1'',c2'')) ∈ trcl t; P c1' c2' w c1'' c2''⟧ ⟹ P c1 c2 (a # w) c1'' c2''⟧ 
  ⟹ P xc1 xc2 xb xa1 xa2" 
  using trcl.induct[of "(xc1,xc2)" xb "(xa1,xa2)" t "λc w c'. let (c1,c2)=c in let (c1',c2')=c' in P c1 c2 w c1' c2'"] by auto
*)

subsubsection "Invariants"
(* TODO: Do we really need this ? Is this formulation usable ? *)
lemma trcl_prop_trans[cases set, consumes 1, case_names empty steps]: "
    (c,w,c')trcl S; 
    c=c'; w=[]  P;  
    cDomain S; c'Range (Range S)P 
    P"
  apply (erule_tac trcl_rev_cases)
  apply auto
  apply (erule trcl.cases)
  apply auto
  done


end

Theory ThreadTracking

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

text ‹
  This theory defines some general notion of an interleaving semantics. It defines how to extend a semantics specified on a single thread and a context to a semantic on multisets of threads.
  The context is needed in order to keep track of synchronization.
›

subsection "Semantic on multiset configuration"
text ‹The interleaving semantics is defined on a multiset of stacks. The thread to make the next step is nondeterministically chosen from all threads ready to make steps.›
definition 
  "gtr gtrs == { (add_mset s c,e,add_mset s' c') | s c e s' c' . ((s,c),e,(s',c'))gtrs }"

lemma gtrI_s: "((s,c),e,(s',c'))gtrs  (add_mset s c,e,add_mset s' c')gtr gtrs"
  by (unfold gtr_def, auto)
lemma gtrI: "((s,c),w,(s',c'))trcl gtrs 
   (add_mset s c,w,add_mset s' c')trcl (gtr gtrs)"
  by (induct rule: trcl_pair_induct) (auto dest: gtrI_s)

lemma gtrE: "
    (c,e,c')gtr T; 
    !!s ce s' ce'.  c=add_mset s ce; c'=add_mset s' ce'; ((s,ce),e,(s',ce'))T   P 
    P"
  by (unfold gtr_def) auto

lemma gtr_empty_conf_s[simp]: 
  "({#},w,c')gtr S" 
  "(c,w,{#})gtr S"
  by (auto elim: gtrE)
lemma gtr_empty_conf1[simp]: "(({#},w,c')trcl (gtr S))  (w=[]  c'={#})"
  by (induct w) (auto dest: trcl_uncons)
lemma gtr_empty_conf2[simp]: "((c,w,{#})trcl (gtr S))  (w=[]  c={#})"
  by (induct w rule: rev_induct) (auto dest: trcl_rev_uncons)

lemma gtr_find_thread: "
    (c,e,c')gtr gtrs; 
    !!s ce s' ce'. c=add_mset s ce; c'=add_mset s' ce'; ((s,ce),e,(s',ce'))gtrs  P 
    P"
  by (unfold gtr_def) auto

lemma gtr_step_cases[cases set, case_names loc other]: " 
    (add_mset s ce,e,c')gtr gtrs; 
    !!s' ce'.  c'=add_mset s' ce'; ((s,ce),e,(s',ce'))gtrs   P;
    !!cc ss ss' ce'.  ce=add_mset ss cc; c'=add_mset ss' ce'; 
                       ((ss,add_mset s cc),e,(ss',ce'))gtrs   P 
    P" 
  by (auto elim!: gtr_find_thread mset_single_cases)

lemma gtr_rev_cases[cases set, case_names loc other]: " 
    (c,e,add_mset s' ce')gtr gtrs; 
    !!s ce.  c=add_mset s ce; ((s,ce),e,(s',ce'))gtrs   P;
    !!cc ss ss' ce.  c=add_mset ss ce; ce'=add_mset ss' cc; 
                      ((ss,ce),e,(ss',add_mset s' cc))gtrs   P 
    P" 
  by (auto elim!: gtr_find_thread mset_single_cases)

subsection "Invariants"
lemma gtr_preserve_s: " 
    (c,e,c')gtr T; 
    P c; 
    !!s c s' c' e. P (add_mset s c); ((s,c),e,(s',c'))T  P (add_mset s' c') 
    P c'"
  by (unfold gtr_def) blast

lemma gtr_preserve: " 
    (c,w,c')trcl (gtr T); 
    P c; 
    !!s c s' c' e. P (add_mset s c); ((s,c),e,(s',c'))T  P (add_mset s' c') 
    P c'"
  apply (induct rule: trcl.induct)
  apply simp
  apply (subgoal_tac "P c'")
  apply blast
  apply (blast intro: gtr_preserve_s)
done  


subsection "Context preservation assumption"
text ‹
  We now assume that the original semantics does not modify threads in the context, i.e. it may only add new threads to the context and use the context to obtain monitor information, but not change any
  existing thread in the context. This assumption is valid for our semantics, where the context is just needed to determine the set of allocated monitors. It allows us to generally derive some further properties of
  such semantics.
›
locale env_no_step =
  fixes gtrs :: "(('s×'s multiset),'l) LTS"
  assumes env_no_step_s[cases set, case_names csp]: 
    "((s,c),e,(s',c'))gtrs; !!csp. c'=csp+c  P   P"

― ‹The property of not changing existing threads in the context transfers to paths›
lemma (in env_no_step) env_no_step[cases set, case_names csp]: "
    ((s,c),w,(s',c'))trcl gtrs; 
    !! csp. c'=csp+c  P 
    P" 
proof -
  have "((s,c),w,(s',c'))trcl gtrs  csp. c'=csp+c" proof (induct rule: trcl_pair_induct)
    case empty thus ?case by (auto intro: exI[of _ "{#}"])
  next
    case (cons s c e sh ch w s' c') note IHP=this
    from env_no_step_s[OF IHP(1)] obtain csph where "ch=csph+c" by auto
    moreover from IHP(3) obtain csp' where "c'=csp'+ch" by auto
    ultimately have "c'=csp'+csph+c" by (simp add: union_assoc)
    thus ?case by blast
  qed
  moreover assume "((s,c),w,(s',c'))trcl gtrs" "!! csp. c'=csp+c  P"
  ultimately show ?thesis by blast
qed

text ‹
  The following lemma can be used to make a case distinction how a step operated on a given thread in the end configuration:
    \begin{description}
      \item[loc›] The thread made the step
      \item[spawn›] The thread was spawned by the step
      \item[env›] The thread was not involved in the step
    \end{description}
›

lemma (in env_no_step) rev_cases_p[cases set, case_names loc spawn env]: 
  assumes STEP: "(c,e,add_mset s' ce')gtr gtrs" and
  LOC: "!!s ce.  c={#s#}+ce; ((s,ce),e,(s',ce'))gtrs   P" and
  SPAWN: "!!ss ss' ce csp. 
             c=add_mset ss ce; ce'=add_mset ss' (csp+ce); 
              ((ss,ce),e,(ss',add_mset s' (csp+ce)))gtrs  
            P" and
  ENV: "!!ss ss' ce csp. 
             c=add_mset ss (add_mset s' ce); ce'=add_mset ss' (csp+ce); 
              ((ss,add_mset s' ce),e,(ss',csp+(add_mset s' ce)))gtrs  
            P"
  shows "P"
proof (rule gtr_rev_cases[OF STEP], goal_cases)
  case 1 thus ?thesis using LOC by auto
next
  case CASE: (2 cc ss ss' ce)
  hence CASE': "c = {#ss#} + ce" "ce' = {#ss'#} + cc" "((ss, ce), e, ss', {#s'#} + cc)  gtrs" by simp_all
  from env_no_step_s[OF CASE'(3)] obtain csp where EQ: "add_mset s' cc = csp + ce" by auto
  thus ?thesis proof (cases rule: mset_unplusm_dist_cases)
    case left note CC=this
    with CASE' have "ce'={#ss'#} + (csp-{#s'#}) + ce" by (auto simp add: union_assoc)
    moreover from CC(2) have "{#s'#}+cc = {#s'#} + (csp-{#s'#}) + ce" by (simp add: union_assoc)
    ultimately show ?thesis using CASE'(1,3) CASE(2) SPAWN by auto
  next
    case right note CC=this
    from CC(1) CASE'(1) have "c=add_mset ss (add_mset s' (ce - {#s'#}))" by (simp add: union_assoc)
    moreover from CC(2) CASE'(2) have "ce'=add_mset ss' (csp+(ce-{#s'#}))" by (simp add: union_assoc)
    moreover from CC(2) have "add_mset s' cc = csp+(add_mset s' (ce-{#s'#}))" by (simp add: union_ac)
    ultimately show ?thesis using CASE'(3) CASE(3) CC(1) ENV by metis
  qed
qed

subsection "Explicit local context"
text_raw ‹\label{sec:ThreadTracking:exp_local}›
text ‹
  In the multiset semantics, a single thread has no identity. This may become a problem when reasoning about a fixed thread during an execution. For example, in our constraint-system-based approach
  the operational characterization of the least solution of the constraint system requires to state properties of the steps of the initial thread in some execution. With the multiset semantics, we are unable 
  to identify those steps among all steps.

  There are many solutions to this problem, for example, using thread ids either as part of the thread's configuration or as part of the whole configuration by using 
  lists of stacks or maps from ids to stacks as configuration datatype. 

  In the following we present a special solution that is strong enough to suit our purposes but not meant as a general solution. 

  Instead of identifying every single thread uniquely, we only distinguish one thread as the {\em local} thread. The other
  threads are {\em environment} threads. We then attach to every step the information whether it was on the local or on some environment thread. 

  We call this semantics {\em loc/env}-semantics in contrast to the {\em multiset}-semantics of the last section.
›

subsubsection "Lifted step datatype"
datatype 'a el_step = LOC 'a | ENV 'a

definition
  "loc w == filter (λe. case e of LOC a  True | ENV a  False) w"

definition
  "env w == filter (λe. case e of LOC a  False | ENV a  True) w"

definition
  "le_rem_s e == case e of LOC a  a | ENV a  a"

text ‹Standard simplification lemmas›
lemma loc_env_simps[simp]: 
  "loc [] = []" 
  "env [] = []"
  by (unfold loc_def env_def) auto

lemma loc_single[simp]: "loc [a] = (case a of LOC e  [a] | ENV e  [])"
  by (unfold loc_def) (auto split: el_step.split)
lemma loc_uncons[simp]: 
  "loc (a#b) = (case a of LOC e  [a] | ENV e  [])@loc b"
  by (unfold loc_def) (auto split: el_step.split)
lemma loc_unconc[simp]: "loc (a@b) = loc a @ loc b"
  by (unfold loc_def, simp)

lemma env_single[simp]: "env [a] = (case a of LOC e  [] | ENV e  [a])"
  by (unfold env_def) (auto split: el_step.split)
lemma env_uncons[simp]: 
  "env (a#b) = (case a of LOC e  [] | ENV e  [a]) @ env b"
  by (unfold env_def) (auto split: el_step.split)
lemma env_unconc[simp]: "env (a@b) = env a @ env b"
  by (unfold env_def, simp)

text ‹The following simplification lemmas are for converting between paths of the multiset- and loc/env-semantics›
lemma le_rem_simps [simp]: 
  "le_rem_s (LOC a) = a" 
  "le_rem_s (ENV a) = a"
  by (unfold le_rem_s_def, auto) 
lemma le_rem_id_simps[simp]: 
  "le_rem_sLOC = id" 
  "le_rem_sENV = id"
  by (auto intro: ext) 

lemma le_rem_id_map[simp]: 
  "map le_rem_s (map LOC w) = w" 
  "map le_rem_s (map ENV w) = w"
  by auto

lemma env_map_env [simp]: "env (map ENV w) = map ENV w"
  by (unfold env_def) simp
lemma env_map_loc [simp]: "env (map LOC w) = []"
  by (unfold env_def) simp
lemma loc_map_env [simp]: "loc (map ENV w) = []"
  by (unfold loc_def) simp
lemma loc_map_loc [simp]: "loc (map LOC w) = map LOC w"
  by (unfold loc_def) simp

subsubsection "Definition of the loc/env-semantics"
type_synonym 's el_conf = "('s × 's multiset)"

inductive_set
  gtrp :: "('s el_conf,'l) LTS  ('s el_conf,'l el_step) LTS"
  for S
  where
  gtrp_loc: "((s,c),e,(s',c'))S  ((s,c),LOC e,(s',c'))gtrp S"
  | gtrp_env: "((s,add_mset sl c),e,(s',add_mset sl c'))S
                ((sl,add_mset s c),ENV e,(sl,add_mset s' c'))gtrp S"


subsubsection "Relation between multiset- and loc/env-semantics"
lemma gtrp2gtr_s: 
  "((s,c),e,(s',c'))gtrp T  (add_mset s c,le_rem_s e,add_mset s' c')gtr T" 
proof (cases rule: gtrp.cases, auto intro: gtrI_s) 
  fix c c' e ss ss' assume "((ss,add_mset s c),e,(ss',add_mset s c'))T"
  hence "(add_mset ss (add_mset s c),e,add_mset ss' (add_mset s c'))  gtr T" by (auto intro!: gtrI_s)
  thus "(add_mset s (add_mset ss c), e, add_mset s (add_mset ss' c'))  gtr T"  by (auto simp add: add_mset_commute)
qed


lemma gtrp2gtr: 
  "((s,c),w,(s',c'))trcl (gtrp T) 
   (add_mset s c,map le_rem_s w,add_mset s' c')trcl (gtr T)" 
  by (induct rule: trcl_pair_induct) (auto dest: gtrp2gtr_s)

lemma (in env_no_step) gtr2gtrp_s[cases set, case_names gtrp]: 
  assumes A: "(add_mset s c,e,c')gtr gtrs" 
  and CASE: "!!s' ce' ee. c'=add_mset s' ce'; e=le_rem_s ee; 
                          ((s,c),ee,(s',ce'))gtrp gtrs 
                          P"
  shows "P" 
  using A 
proof (cases rule: gtr_step_cases)
  case (loc s' ce') hence "((s,c),LOC e,(s',ce'))gtrp gtrs" by (blast intro: gtrp_loc)
  with loc(1) show ?thesis by (rule_tac CASE) auto
next
  case (other cc ss ss' ce') from env_no_step_s[OF other(3)] obtain csp where CE'FMT: "ce'=csp + (add_mset s cc)" .
  with other(3) have "((ss,add_mset s cc),e,(ss',add_mset s (csp+cc)))gtrs" by auto
  from gtrp_env[OF this] other(1) have "((s, c), ENV e, s, {#ss'#} + (csp + cc))  gtrp gtrs" by simp
  moreover from other CE'FMT have "c' = {#s#} + ({#ss'#} + (csp + cc))" by (simp add: union_ac)
  ultimately show ?thesis by (rule_tac CASE) auto
qed

lemma (in env_no_step) gtr2gtrp[cases set, case_names gtrp]: 
  assumes A: "(add_mset s c,w,c')trcl (gtr gtrs)" 
  and CASE: "!!s' ce' ww. c'=add_mset s' ce'; w=map le_rem_s ww; 
                           ((s,c),ww,(s',ce'))trcl (gtrp gtrs) 
                           P" 
  shows P 
proof -
  have "!!s c. (add_mset s c,w,c')trcl (gtr gtrs)  s' ce' ww. c'=add_mset s' ce'  w=map le_rem_s ww  ((s,c),ww,(s',ce'))trcl (gtrp gtrs)" proof (induct w)
    case Nil thus ?case by auto
  next
    case (Cons e w) then obtain ch where SPLIT: "(add_mset s c,e,ch)gtr gtrs" "(ch,w,c')trcl (gtr gtrs)" by (auto dest: trcl_uncons)
    from gtr2gtrp_s[OF SPLIT(1)] obtain sh ceh ee where FS: "ch = add_mset sh  ceh" "e = le_rem_s ee" "((s, c), ee, sh, ceh)  gtrp gtrs" by blast
    moreover from FS(1) SPLIT(2) Cons.hyps obtain s' ce' ww where IH: "c'=add_mset s' ce'" "w=map le_rem_s ww" "((sh,ceh),ww,(s',ce'))trcl (gtrp gtrs)" by blast
    ultimately have "((s,c),ee#ww,(s',ce'))trcl (gtrp gtrs)" "e#w = map le_rem_s (ee#ww)" by auto
    with IH(1) show ?case by iprover
  qed
  with A CASE show ?thesis by blast
qed
   
subsubsection "Invariants"
lemma gtrp_preserve_s: 
  assumes A: "((s,c),e,(s',c'))gtrp T" 
  and INIT: "P (add_mset s c)" 
  and PRES: "!!s c s' c' e. P (add_mset s c); ((s,c),e,(s',c'))T 
                             P (add_mset s' c')" 
  shows "P (add_mset s' c')" 
proof -
  from gtr_preserve_s[OF gtrp2gtr_s[OF A], where P=P, OF INIT] PRES show "P (add_mset s' c')" by blast
qed

lemma gtrp_preserve: 
  assumes A: "((s,c),w,(s',c'))trcl (gtrp T)" 
  and INIT: "P (add_mset s c)" 
  and PRES: "!!s c s' c' e. P (add_mset s c); ((s,c),e,(s',c'))T 
                             P (add_mset s' c')" 
  shows "P (add_mset s' c')" 
proof -
  from gtr_preserve[OF gtrp2gtr[OF A], where P=P, OF INIT] PRES show "P (add_mset s' c')" by blast
qed
    

end

Theory Flowgraph

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

text ‹
  We use a flowgraph-based program model that extends the one we used previously \cite{LM07}. 
  A program is represented as an edge annotated graph and a set of procedures. The nodes of the graph are partitioned by the procedures, i.e. every node belongs to exactly one procedure. There are no edges
  between nodes of different procedures. Every procedure has a distinguished entry and return node and a set of monitors it synchronizes on. Additionally, the program has a distinguished {\em main} procedure.
  The edges are annotated with statements. A statement is either a base statement, a procedure call or a thread creation (spawn). Procedure calls and thread creations refer to the called procedure or to the initial procedure
  of the spawned thread, respectively.

  We require that the main procedure and any initial procedure of a spawned thread does not to synchronize on any monitors. This avoids that spawning of a procedure together with entering a monitor is available in our 
  model as an atomic step, which would be an unrealistic assumption for practical problems. Technically, our model would become strictly more powerful without this assumption.


  If we allowed this, our model would become strictly more powerful, 
›

subsection "Definitions"
  
datatype ('p,'ba) edgeAnnot = Base 'ba | Call 'p | Spawn 'p
type_synonym ('n,'p,'ba) edge = "('n × ('p,'ba) edgeAnnot × 'n)"

record ('n,'p,'ba,'m) flowgraph_rec =
  edges :: "('n,'p,'ba) edge set" ― ‹Set of annotated edges›
  main :: "'p" ― ‹Main procedure›
  entry :: "'p  'n" ― ‹Maps a procedure to its entry point›
  return :: "'p  'n" ― ‹Maps a procedure to its return point›
  mon :: "'p  'm set" ― ‹Maps procedures to the set of monitors they allocate›
  proc_of :: "'n  'p" ― ‹Maps a node to the procedure it is contained in›

definition 
  "initialproc fg p == p=main fg  (u v. (u,Spawn p,v)edges fg)"

lemma main_is_initial[simp]: "initialproc fg (main fg)"
  by (unfold initialproc_def) simp

locale flowgraph =
  fixes fg :: "('n,'p,'ba,'m,'more) flowgraph_rec_scheme" (structure)
  (* Type annotation unnecessary, but perhaps makes it more readable
     for the unaware reader ;) *)
  ― ‹Edges are inside procedures only›
  assumes edges_part: "(u,a,v)edges fg  proc_of fg u = proc_of fg v" 
  ― ‹The entry point of a procedure must be in that procedure›
  assumes entry_valid[simp]: "proc_of fg (entry fg p) = p" 
  ― ‹The return point of a procedure must be in that procedure›
  assumes return_valid[simp]: "proc_of fg (return fg p) = p" 
  ― ‹Initial procedures do not synchronize on any monitors›
  assumes initial_no_mon[simp]: "initialproc fg p  mon fg p = {}" 

subsection "Basic properties"
lemma (in flowgraph) spawn_no_mon[simp]: 
  "(u, Spawn p, v)  edges fg  mon fg p = {}" 
  using initial_no_mon by (unfold initialproc_def, blast)
lemma (in flowgraph) main_no_mon[simp]: "mon fg (main fg) = {}" 
  using initial_no_mon by (unfold initialproc_def, blast)

lemma (in flowgraph) entry_return_same_proc[simp]: 
  "entry fg p = return fg p'  p=p'"
  apply (subgoal_tac "proc_of fg (entry fg p) = proc_of fg (return fg p')")
  apply (simp (no_asm_use))
  by simp

lemma (in flowgraph) entry_entry_same_proc[simp]: 
  "entry fg p = entry fg p'  p=p'"
  apply (subgoal_tac "proc_of fg (entry fg p) = proc_of fg (entry fg p')")
  apply (simp (no_asm_use))
  by simp

lemma (in flowgraph) return_return_same_proc[simp]: 
  "return fg p = return fg p'  p=p'"
  apply (subgoal_tac "proc_of fg (return fg p) = proc_of fg (entry fg p')")
  apply (simp (no_asm_use))
  by simp

subsection "Extra assumptions for flowgraphs"
text_raw ‹\label{sec:Flowgraph:extra_asm}›
text ‹
  In order to simplify the definition of our restricted schedules (cf. Section~\ref{thy:Normalization}), we make some extra constraints on flowgraphs. 
  Note that these are no real restrictions, as we can always rewrite flowgraphs to match these constraints, preserving the set of conflicts. We leave it to future work to consider such a rewriting formally. 

  The background of this restrictions is that we want to start an execution of a thread with a procedure call that never returns. This will allow easier technical treatment in Section~\ref{thy:Normalization}. Here we enforce this
  semantic restrictions by syntactic properties of the flowgraph.
›

text ‹The return node of a procedure is called {\em isolated}, if it has no incoming edges and is different from the entry node. A procedure with an isolated return node will never return. 
  See Section~\ref{sec:Normalization:eflowgraph} for a proof of this.›
definition 
  "isolated_ret fg p == 
    (u l. ¬(u,l,return fg p)edges fg)  entry fg p  return fg p"

text ‹The following syntactic restrictions guarantee that each thread's execution starts with a non-returning call. See Section~\ref{sec:Normalization:eflowgraph} for a proof of this.›
locale eflowgraph = flowgraph +
  ― ‹Initial procedure's entry node isn't equal to its return node›
  assumes initial_no_ret: "initialproc fg p  entry fg p  return fg p" 
  ― ‹The only outgoing edges of initial procedures' entry nodes are call edges to procedures with isolated return node›
  assumes initial_call_no_ret: "initialproc fg p; (entry fg p,l,v)edges fg 
     p'. l=Call p'  isolated_ret fg p'" 

subsection ‹Example Flowgraph›
text_raw ‹\label{sec:Flowgraph:ex_flowgraph}›
text ‹This section contains a check that there exists a (non-trivial) flowgraph, i.e. that the assumptions made in the flowgraph› and eflowgraph› 
  locales are consistent and have at least one non-trivial model.›
definition 
  "example_fg ==  
    edges = {((0::nat,0::nat),Call 1,(0,1)), ((1,0),Spawn 0,(1,0)), 
             ((1,0),Call 0, (1,0))}, 
    main = 0, 
    entry = λp. (p,0), 
    return = λp. (p,1), 
    mon = λp. if p=1 then {0} else {}, 
    proc_of= λ (p,x). p "

lemma exists_eflowgraph: "eflowgraph example_fg"
  apply (unfold_locales)
  apply (unfold example_fg_def)
  apply simp
  apply fast
  apply simp
  apply simp
  apply (simp add: initialproc_def)
  apply (simp add: initialproc_def)
  apply (simp add: initialproc_def isolated_ret_def)
  done


end

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: "nset s; mmon_n fg n  mmon_s fg s"
  by (unfold mon_s_def, auto)
lemma mon_sD: "mmon_s fg s  nset s. mmon_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; mmon_s fg s  mmon_c fg c"
  by (unfold mon_c_def, auto)
lemma mon_cD: "mmon_c fg c  s. s ∈# c  mmon_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: "ww'  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) = (uU)"

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; uiU  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#} = (uU)" 
  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 "xmon_c fg csp"
  then obtain s where "s ∈# csp" and M: "xmon_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 "xmon_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 "eLRet"
      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 wblength 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