# 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"

+ 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={#})"

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#})"
with CASE D have "?SIZE = sum (count (S-{#t#})) (set_mset (S - {#t#})) + 1"
}
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#})"
lemma union_diff_assoc_se2: "t ∈# A ⟹ (A+B)-{#t#} = (A-{#t#}) + B"
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)"

lemma mset_union_2_elem: "{#a#}+{#b#} = M + {#c#} ⟹ {#a#}=M & b=c | a=c & {#b#}=M"

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
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
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 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: "s≠r'"
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 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 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 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"
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
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]

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
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

lemmas mset_le_decr_left = mset_le_decr_left1 mset_le_decr_left2 mset_le_add_mset_decr_left1

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"

lemma mset_le_subtract_add_mset_right: "add_mset x B ⊆# (X::'a multiset) ⟹ {#x#} ⊆# X-B ∧ B⊆#X"

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

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
} 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"

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'#}"

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"
lemma list_Cons_eq_append_cases: "⟦x#xs = ys@zs; ⟦ys=[]; zs=x#xs⟧ ⟹ P; !!ys'. ⟦ ys=x#ys'; ys'@zs=xs ⟧ ⟹ P ⟧ ⟹ P"

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. x∈set 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 "bool⇒bool"}›
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]: "a⋅S = (#) a  S"

definition list_set_append :: "'a list ⇒ 'a list set ⇒ 'a list set" (infixr "⊙" 65)
where [simp]: "a⊙S = (@) 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 ∈ b⋅S = (a=b & l∈S)"
by auto
lemma append_set_append_eq: "⟦length a = length b⟧ ⟹ a@l ∈ b⊙S = (a=b & l∈S)"
by auto

lemma list_set_cons_cases[cases set]: "⟦w∈a⋅S; !!w'. ⟦ w=a#w'; w'∈S ⟧ ⟹ P⟧ ⟹ P"
by auto
lemma list_set_append_cases[cases set]: "⟦w∈a⊙S; !!w'. ⟦ w=a@w'; w'∈S ⟧ ⟹ P⟧ ⟹ P"
by auto

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

lemma interleave_cons2: "l ∈ a⊗b ⟹ x#l ∈ a ⊗ x#b"
apply(case_tac a)
apply(auto)
done

lemmas interleave_cons = interleave_cons1 interleave_cons2

lemma interleave_empty[simp]: "[]∈a⊗b = (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 : a⊗b . length x = length a + length b"
apply(induct rule: interleave.induct)
apply(auto)
done

lemma interleave_same[simp]: "y∈l⊗y = (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]: "a⊗b = b⊗a" (is "?P f a b")
apply(induct rule: interleave.induct)
apply(auto)
done

lemma interleave_cont_conc[rule_format, simp]: "ALL b . a@b ∈ a⊗b"
apply(induct_tac a)
done

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

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

lemma cons_interleave_split: "⟦a#l ∈ l1⊗l2⟧ ⟹ (EX lh . l1=a#lh & l ∈ lh⊗l2 | l2=a#lh & l ∈ l1⊗lh )"
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 ∈ l1⊗l2; !!lh . ⟦l1=a#lh; l ∈ lh⊗l2⟧ ⟹ P; !!lh. ⟦l2=a#lh; l ∈ l1⊗lh⟧ ⟹ P⟧ ⟹ P"
by (blast dest: cons_interleave_split)

lemma interleave_cases[cases set, case_names empty left right]: "⟦l∈l1⊗l2; ⟦ 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'∈l1⊗l2'⟧ ⟹ 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. ⟦ w∈w1⊗w2; P [] [] []; !!e w w1 w2. ⟦ P w w1 w2; w∈w1⊗w2 ⟧ ⟹ P (e#w) (e#w1) w2; !!e w w1 w2. ⟦ P w w1 w2; w∈w1⊗w2 ⟧ ⟹ 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 ∈ a⊗b ⟶ 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 ∈ a⊗b"
then obtain c where SPLIT: "a=e#c & l∈c⊗b | b=e#c & l∈a⊗c" 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 ∈ a⊗b ⟹ l@[x] ∈ a ⊗ b@[x]"
proof -
assume "l ∈ a⊗b"
hence "l∈b⊗a" 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 ∈ a⊗b⟧ ⟹ x@l ∈ x@a ⊗ b" proof -
have "ALL l a b . l ∈ a⊗b ⟶ 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 ∈ a⊗b⟧ ⟹ x@l ∈ a ⊗ x@b" proof -
have "ALL l a b . l ∈ a⊗b ⟶ 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. w∈a⊗b ⟹ 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: "w∈a⊗b ⟹ 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 . (w∈w1⊗w2) ⟶ (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' & w∈w'⊗w2 | w2=e#w' & w∈w1⊗w'" by (blast dest: cons_interleave_split)
with IH have "w1=e#w' & rev w∈rev 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) ⟹ (w∈w1⊗w2)"
apply (subgoal_tac "(rev w∈rev w1⊗rev 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] ∈ l1⊗l2⟧ ⟹ (EX lh . l1=lh@[a] & l ∈ lh⊗l2 | l2=lh@[a] & l ∈ l1⊗lh )"
proof -
assume "l@[a] ∈ l1⊗l2"
hence "a#rev l ∈ rev l1 ⊗ rev l2" by (auto dest: interleave_rev)
then obtain lh where "rev l1 = a#lh & rev l ∈ lh⊗rev 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 . (w∈w1⊗ws & ws∈w2⊗w3 ⟶ (EX ws' : w1⊗w2 . w ∈ ws'⊗w3))" proof (induct w)
case Nil show ?case by (auto)
case (Cons e w)
assume IH: "ALL w1 ws w2 w3 . w∈w1⊗ws & ws∈w2⊗w3 ⟶ (EX ws' : w1⊗w2 . 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 & w∈wh⊗ws | ws=e#wh & w∈w1⊗wh" by (blast dest!: cons_interleave_split)
moreover {
assume CASE: "w1=e#wh & w∈wh⊗ws"
with A IH obtain ws' where "ws'∈wh⊗w2 & w∈ws'⊗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 & w∈w1⊗wh"
with A obtain whh where "w2=e#whh & wh∈whh⊗w3 | w3=e#whh & wh∈w2⊗whh" by (blast dest!: cons_interleave_split)
moreover {
assume SCASE: "w2=e#whh & wh∈whh⊗w3"
with CASE IH obtain ws' where "ws'∈w1⊗whh & w∈ws'⊗w3" by blast
with SCASE have "e#ws'∈w1⊗w2 & 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 & wh∈w2⊗whh"
with CASE IH obtain ws' where "ws'∈w1⊗w2 & w∈ws'⊗whh" by blast
with SCASE have "ws'∈w1⊗w2 & 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: "⟦w∈ws⊗w3; ws∈w1⊗w2⟧ ⟹ EX ws' : w2⊗w3 . w ∈ w1⊗ws'" proof -
assume "w ∈ ws ⊗ w3" "ws ∈ w1 ⊗ w2"
hence "w ∈ w3 ⊗ ws & ws ∈ w2 ⊗ w1" by simp
hence "EX ws':w3⊗w2 . w∈ws'⊗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: "w∈w1⊗w2 ⟹ set w = set w1 ∪ set w2"
by (induct rule: interleave_elem_induct) auto
lemma interleave_map: "w∈w1⊗w2 ⟹ map f w ∈ map f w1 ⊗ map f w2"
by (induct rule: interleave_elem_induct) (auto intro!: interleave_cons)
lemma interleave_filter: "w∈w1⊗w2 ⟹ 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. l∈lb ⊗ l'" proof (rule eq_reflection)
{fix l' l have "l'≼l ⟹ ∃lb. l∈lb ⊗ l'" by (induct rule: less_eq_list_induct) (simp, (blast intro: interleave_cons)+)}
moreover {fix l have "!!lb l'. l∈lb⊗l' ⟹ l'≼l" by (induct l) (auto intro: less_eq_list_drop elim!: cons_interleave_cases)}
ultimately show "(l'≼l) = (∃lb. l∈lb ⊗ l')" by blast
qed

lemma ileq_interleave: "w∈w1⊗w2 ⟹ w1≼w & w2≼w"
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: "⟦w∈w1⊗w2; w1~=[]⟧ ⟹ w2<w"
by (simp only: ilt_ex_notempty, blast)
lemma ilt_interleave2: "⟦w∈w1⊗w2; 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 & wa∈w1a⊗w2a & wb∈w1b⊗w2b)"
(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#w∈w1b⊗w2" 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 & w∈wh⊗w2 | w2=e#wh & w∈w1a@w1b⊗wh" by (blast dest: cons_interleave_split)
moreover {
assume SCASE: "w1a@w1b=e#wh & w∈wh⊗w2"
with CASE obtain w1ah where W1AFMT: "w1a=e#w1ah & w1ah@w1b=wh" by (cases w1a, auto)
with SCASE have "w∈w1ah@w1b⊗w2" by auto
with IH[of w1ah w1b w2] obtain wa wb w2a w2b where "w=wa@wb & w2=w2a@w2b & wa∈w1ah⊗w2a & wb∈w1b⊗w2b" by (blast)
with W1AFMT have "e#w=(e#wa)@wb & e#w∈e#wa⊗wb & w2=w2a@w2b & e#wa∈w1a⊗w2a & wb∈w1b⊗w2b" by (auto simp add: interleave_cons)
hence "?CONS (e#w) w1a w1b w2" by blast
} moreover {
assume SCASE: "w2=e#wh & w∈w1a@w1b⊗wh"
with IH[of w1a w1b wh] obtain wa wb w2a w2b where "w=wa@wb & wh=w2a@w2b & wa∈w1a⊗w2a & wb∈w1b⊗w2b" by blast
with SCASE have "e#w=(e#wa)@wb & w2=(e#w2a)@w2b & e#wa∈w1a⊗e#w2a & wb∈w1b⊗w2b" 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: "w∈w1⊗(w2a@w2b) ⟹ EX wa wb w1a w1b . w=wa@wb & w1=w1a@w1b & wa∈w1a⊗w2a & wb∈w1b⊗w2b"
proof -
assume "w∈w1⊗(w2a@w2b)"
hence "w∈(w2a@w2b)⊗w1" by auto
hence "EX wa wb w1a w1b . w=wa@wb & w1=w1a@w1b & wa∈w2a⊗w1a & wb∈w2b⊗w1b" 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 ∈ w1⊗w2 ⟹ ∃ w11 w12 w21 w22 . w1=w11@w12 ∧ w2=w21@w22 ∧ l1∈w11⊗w21 ∧ l2∈w12⊗w22"
proof (induct l1)
case Nil hence "w1=[]@w1 & w2=[]@w2 & []∈[]⊗[] & l2∈w1⊗w2" by auto
thus ?case by fast
next
case (Cons e l1') note IHP=this
hence "e#(l1'@l2)∈w1⊗w2" by auto
with cons_interleave_split obtain w' where "(w1=e#w' & l1'@l2∈w'⊗w2) | (w2=e#w' & l1'@l2∈w1⊗w')" (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 ∧ l2∈w12'⊗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'∈w11⊗w21' ∧ l2∈w12⊗w22'" 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 . ⟦l1∈w11⊗w21;l2∈w12⊗w22⟧ ⟹ 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'∈w11⊗w')" (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 ∈ w1⊗w2 = (∃ w11 w12 w21 w22 . w1=w11@w12 ∧ w2=w21@w22 ∧ l1∈w11⊗w21 ∧ l2∈w12⊗w22)"
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: "w≼w' ⟹ mon_pl w ⊆ mon_pl w'"
by (induct rule: less_eq_list_induct) auto

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

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

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

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

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

lemma cil_induct'[case_names both_empty left_empty right_empty append]: "⟦
⋀α. P α [] [];
⋀α 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 α [] [];
⋀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 α [] [];
⋀z aa. P α (z # aa) [];
⋀e1 w1 e2 w2. ⟦
fst (α e1) ∩ mon_pl (map α (e2 # w2)) = {} ⟹ P α w1 (e2 # w2);
fst (α e2) ∩ mon_pl (map α (e1 # w1)) = {} ⟹ P α (e1 # w1) w2⟧
⟹ P α (e1 # w1) (e2 # w2)
⟧ ⟹ P α wa wb"
apply (induct wa α wb rule: cil.induct)
apply (case_tac w)
apply auto
done

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

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

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

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

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

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

subsection "Properties of consistent interleaving"

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

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

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

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

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

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

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

lemma cil_assoc2:
assumes A: "w∈w1⊗⇘α⇙wr" and B: "wr∈w2⊗⇘α⇙w3"
shows "∃wl. w∈wl⊗⇘α⇙w3 ∧ wl∈w1⊗⇘α⇙w2"
proof -
from A have A': "w∈wr⊗⇘α⇙w1" by (simp add: cil_commute)
from B have B': "wr∈w3⊗⇘α⇙w2" by (simp add: cil_commute)
from cil_assoc1[OF A' B'] obtain wl where "w ∈ w3 ⊗⇘α⇙ wl ∧ wl ∈ w2 ⊗⇘α⇙ w1" by blast
thus ?thesis by (auto simp add: cil_commute)
qed

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

end


# 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 "m∈h 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 = {} ∨ m∈h m }"

lemma ah_cases[cases set]: "⟦h∈ah; 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. m1∈h2 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:
"⟦ h1∈ah; h2∈ah; 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 m∈fst 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: "⟦m∈fst e; x∈fst e ∪ snd e ∪ mon_pl w⟧ ⟹ x∈αah (e#w) m"
by auto
lemma αah_tl: "⟦m∉fst 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'; m∈fst e; x∈fst e ∪ snd e ∪ mon_pl w'⟧ ⟹ P;
!!e w'. ⟦w=e#w'; m∉fst 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;
⟦m∈fst e; x∈fst e ∪ snd e ∪ mon_pl w'⟧ ⟹ P;
⟦m∉fst 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: "w1≼w2 ⟹ α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 "x∈mon_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 "(m2∈fst (α e) ∧ m1 ∈ fst (α e) ∪ snd (α e) ∪ mon_pl (map α w1')) ∨ (m2∉fst (α 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: "m2∈fst (α 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 "(m1∈fst (α e) ∧ m2 ∈ fst (α e) ∪ snd (α e) ∪ mon_pl (map α w2')) ∨ (m1∉fst (α e) ∧ m2 ∈ αah (map α w2') m1)" (is "?CASE1 ∨ ?CASE2")
by (auto split: if_split_asm)
moreover {
assume ?CASE1 hence C: "m1∈fst (α 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 "m1∈fst (α e1)" "m1∈mon_pl (map α w2)" "m2∈fst (α e2)" "m2∈mon_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 m∈fst 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'; M⊆M'⟧
⟹ 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'; U⊆U'; M⊆M'⟧
⟹ 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: "x∈trcl (S∩R) ⟹ x∈trcl S" "x∈trcl (S∩R) ⟹ x∈trcl R"
proof -
assume "x∈trcl (S∩R)"
with trcl_mono[of "S∩R" S] show "x∈trcl S" by auto
next
assume "x∈trcl (S∩R)"
with trcl_mono[of "S∩R" R] show "x∈trcl 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;
⟦c∈Domain S; c'∈Range (Range S)⟧⟹P
⟧ ⟹ P"
apply (erule_tac trcl_rev_cases)
apply auto
apply (erule trcl.cases)
apply auto
done

end


(*  Title:       Conflict analysis/Thread Tracking
Author:      Peter Lammich <peter.lammich@uni-muenster.de>
Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)
imports Main "HOL-Library.Multiset" LTS Misc
begin

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 }"

by (unfold gtr_def, auto)
lemma gtrI: "((s,c),w,(s',c'))∈trcl 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)

(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]: "⟦
!!s' ce'. ⟦ c'=add_mset s' ce'; ((s,ce),e,(s',ce'))∈gtrs ⟧ ⟹ P;
((ss,add_mset s cc),e,(ss',ce'))∈gtrs ⟧ ⟹ P
⟧ ⟹ P"

lemma gtr_rev_cases[cases set, case_names loc other]: "⟦
!!s ce. ⟦ c=add_mset s ce; ((s,ce),e,(s',ce'))∈gtrs ⟧ ⟹ P;
((ss,ce),e,(ss',add_mset s' cc))∈gtrs ⟧ ⟹ P
⟧ ⟹ P"

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[‹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.
⟹ P" and
ENV: "!!ss ss' ce csp.
⟹ 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
moreover from CC(2) CASE'(2) have "ce'=add_mset ss' (csp+(ce-{#s'#}))" by (simp add: union_assoc)
ultimately show ?thesis using CASE'(3) CASE(3) CC(1) ENV by metis
qed
qed

subsection "Explicit local context"
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.

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_s∘LOC = id"
"le_rem_s∘ENV = 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"

subsubsection "Relation between multiset- and loc/env-semantics"
lemma gtrp2gtr_s:
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"
qed

lemma gtrp2gtr:
"((s,c),w,(s',c'))∈trcl (gtrp 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)" .
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⟧
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⟧
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

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
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) = {}"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma valid_split1:
"valid fg (c+c') ⟹ valid fg c ∧ valid fg c' ∧ mon_c fg c ∩ mon_c fg c' = {}"
apply (unfold valid_def)
apply (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)

"valid fg (add_mset x c') ⟷ (valid fg c' ∧ mon_s fg x ∩ mon_c fg c' = {})"

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

subsection ‹Configurations at control points›

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

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

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

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

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

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

lemma atU_union[simp]: "atU U (c1+c2) = (atU U c1 ∨ atU U c2)"

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

lemma atU_add_mset[simp]: "atU U (add_mset c c2) = (atU_s U c ∨ atU U c2)"

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 (subst union_commute)
done

atUV U V (add_mset c c2) ⟷
(
(atUV U V c2) ∨
(atU U {#c#} ∧ atU V c2) ∨
(atU V {#c#} ∧ atU U 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) ⟧
― ‹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) ⟧
― ‹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) ⟧

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
(('n list * 'n conf) * ('p,'ba) label * ('n list * 'n conf)) set"
for fg
where
((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_spawn: "⟦ (u,Spawn p,v)∈edges 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"
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"
lemma trss_ret': "⟦ s=(return fg p)#r; e=LRet ⟧ ⟹ ((s,c),e,(r,c)) ∈ trss fg"
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"
*)

― ‹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}›
by (blast dest: mon_n_same_proc edges_part)+

"⟦((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 (erule gtrE)
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]: "⟦
⟦ 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"
⟹ ∃csp. c'=csp+c ∧
(csp={#} ∨ (∃p. e=LSpawn p ∧ csp={#[ entry fg p ]#}))"

!!csp. ⟦c'=csp+c; mon_c fg csp={}⟧ ⟹ P
⟧ ⟹ P"
apply (subgoal_tac "c'={#}+c")
apply (fastforce)
apply auto
done

lemma trss_c_cases[cases set, case_names c_case]: "!!s c. ⟦
!!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
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 *)
shows "mon_c fg c' = mon_c fg c"
using A
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 *)
"((s,c),w,(s',c'))∈trcl (trss fg) ⟹ mon_c fg c' = mon_c fg c"
proof -
fix csp x
assume "x∈mon_c fg csp"
then obtain s where "s ∈# csp" and M: "x∈mon_s fg s" by (unfold mon_c_def, auto)
moreover assume "∀s. s ∈# csp ⟶ (∃p. s = [entry fg p] ∧ (∃u v. (u, Spawn p, v) ∈ edges fg) ∧ initialproc fg p)"
ultimately obtain p u v where "s=[entry fg p]" and "(u,Spawn p,v)∈edges fg" by blast
hence "mon_s fg s = {}" by (simp)
with M have False by simp
thus "x∈mon_c fg c" ..
qed

"((s,c),LSpawn p, (s',c'))∈trss fg ⟹ mon fg p = {}"

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. ⟦
c={#s#}+ce; c'={#s'#}+ce
⟧ ⟹ P"
assumes A_SPAWN: "!!s ce s' p. ⟦
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

subsubsection "Stack composition / decomposition"

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

⟹ ∃sp'. s'=sp'@r ∧ ((s,c),e,(sp',c'))∈trss fg"

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

(* TODO: Try backward induction proof … is this simpler ? *)
lemma trss_return_cases[cases set]: "!!u r c. ⟦
!! 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 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 IHP(4)[OF _ this(2)] SPLIT2 have ?case by auto
} moreover {
fix q
assume CASE: "e=LCall q"
with SPLIT1 obtain u' where SHFMT: "sh=entry fg q # u' # r" "(([u],c),e,(entry fg q # [u'],ch))∈trss fg" by (auto elim!: trss.cases intro: trss.intros)
with SPLIT2 have "((entry fg q # u' # r,ch),w,(r',c'))∈trcl (trss fg)" by simp
hence ?case proof (cases rule: IHP(1)[of w, simplified, cases set])
case (1 st ut) note CC=this
from trss_stack_comp[OF CC(2), where r="[u']"] have "((entry fg q#[u'], ch), w, (st @ [ut]) @ [u'], c') ∈ trcl (trss fg)" by auto
with SHFMT(2) have "(([u],c),e#w, (st @ [ut]) @ [u'], c') ∈ trcl (trss fg)" by auto
from IHP(3)[OF _ this] CC(1) show ?thesis by simp
next
case (2 wa wb ct) note CC=this
from trss_stack_comp[OF CC(2), where r="[u']"] have "((entry fg q # [u'], ch), wa, [u'], ct) ∈ trcl (trss fg)" by simp
with SHFMT have PREPATH: "(([u],c),e#wa, [u'], ct) ∈ trcl (trss fg)" by simp
from CC have L: "length wb≤length w" by simp
from CC(3) show ?case proof (cases rule: IHP(1)[OF L, cases set])
case (1 s'' u'') note CCC=this from trcl_concat[OF PREPATH CCC(2)] CC(1) have "(([u],c),e#w,(s''@[u''],c'))∈trcl (trss fg)" by (simp)
from IHP(3)[OF CCC(1) this] show ?thesis .
next
case (2 wba wbb c'') note CCC=this from trcl_concat[OF PREPATH CCC(2)] CC(1) CCC(1) have "e#w = (e#wa@wba)@wbb" "(([u], c), e # wa @ wba, [], c'') ∈ trcl (trss fg)" by auto
from IHP(4)[OF this CCC(3)] show ?thesis .
qed
qed
} ultimately show ?case by (cases e, auto)
qed

"!!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 ∧
((rh,ch),LCall p,((entry fg p)#r',ch))∈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)
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"
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}›
assumes A: "(([sp],c),w,(return fg p#[u'],c')) ∈ trcl (trss fg)"
and EX: "!!uh ch wa wb. ⟦
w=wa@(LCall p)#wb;
(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

"!!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›
"(([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] .

∃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

apply (subgoal_tac "(([return fg p],c'),LRet,([],c'))∈trss fg")
by (auto dest: trcl_rev_cons intro: trss.intros)

by (induct rule: trcl_pair_induct) (auto dest: trss_env_increasing_s order_trans)

subsubsection "Conversion between environment and monitor restrictions"
"((s,c),e,(s',c'))∈trss fg ⟹ mon_e fg e ∩ mon_c fg c = {}"
"((s,c),w,(s',c'))∈trcl (trss fg) ⟹ mon_w fg w ∩ mon_c fg c = {}"

"!!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"

⟹ ∀cn. mon_w fg w ∩ mon_c fg cn = {}
⟶ (∃csp. c'=csp+c ∧ mon_c fg csp = {} ∧
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

"⟦((s,c),e,(s',c'))∈trss fg; mon_e fg e ∩ mon_c fg ce = {}⟧

by (erule trss.cases) (auto