theory Size_Change_Termination
imports
"HOL-Library.Ramsey"
"Abstract-Rewriting.Abstract_Rewriting"
QTRS.Linear_Orders
"../Auxiliaries/RTrancl2"
QTRS.Util
begin
subsection ‹Size change graphs and algorithms working on them›
datatype ('pp, 'ap) scg =
Null -- ‹zero element to make composition total›
| Scg 'pp 'pp "('ap * 'ap) list" "('ap * 'ap) list"
text ‹Composition›
definition comp :: "('ap :: linorder * 'ap) list ⇒ ('ap * 'ap) list ⇒ ('ap * 'ap) list"
where "comp es es' = remdups_sort [ (x, z). (x,y) ← es, (y',z) ← es', y = y' ]"
lemma set_comp[simp]:
"set (comp es es') = set es O set es'"
unfolding comp_def by (auto split: if_splits intro!: relcompI)
text ‹
Scg composition depends on an (executable) relation @{term conn} that describes
connectedness of program points
›
fun scg_comp :: "('pp ⇒ 'pp ⇒ bool) ⇒ ('pp, 'ap :: linorder) scg ⇒ ('pp, 'ap) scg ⇒ ('pp, 'ap) scg"
where
"scg_comp conn (Scg p q str wk) (Scg p' q' str' wk') =
(if ¬conn q p' then Null else
let strs = remdups_sort (comp str str' @ comp str wk' @ comp wk str');
wks = subtract_list_sorted (remdups_sort (comp wk wk')) strs
in Scg p q' strs wks)"
| "scg_comp conn Null G = Null"
| "scg_comp conn G Null = Null"
text ‹Subsumption›
fun subsumes :: "('pp, 'ap) scg ⇒ ('pp, 'ap) scg ⇒ bool"
where
"subsumes (Scg p q str wk) (Scg p' q' str' wk') =
(p = p' ∧ q = q' ∧ set str ⊆ set str' ∧ set wk ⊆ set (str' @ wk'))"
| "subsumes G Null = True"
| "subsumes Null G = False"
lemma subsumes_refl[simp]: "subsumes G G"
by (cases G) auto
lemma subsumes_trans[trans]:
"subsumes F G ⟹ subsumes G H ⟹ subsumes F H"
by (cases H, simp, induct F G rule: subsumes.induct) auto
lemma subsumes_comp_mono:
"subsumes G G' ⟹ subsumes H H'
⟹ subsumes (scg_comp conn G H) (scg_comp conn G' H')"
apply (induct G G' rule: subsumes.induct)
apply auto
apply (induct H H' rule: subsumes.induct)
apply (auto simp: Let_def)
apply blast+
done
definition subsume :: "('pp, 'ap) scg set ⇒ ('pp, 'ap) scg set ⇒ bool"
where
"subsume Gs Hs = (∀H∈Hs. H ≠ Null ⟶ (∃G∈Gs. subsumes G H))"
lemma subsume_refl[simp]: "subsume Gs Gs"
by (force simp: subsume_def)
lemma subsume_trans[trans]:
assumes "subsume Fs Gs" "subsume Gs Hs"
shows "subsume Fs Hs"
unfolding subsume_def
proof (intro ballI impI)
fix H assume "H ∈ Hs" "H ≠ Null"
with ‹subsume Gs Hs›
obtain G where G: "G ∈ Gs" "subsumes G H" unfolding subsume_def by auto
with ‹H ≠ Null› have "G ≠ Null" by (cases G, cases H, auto)
with ‹subsume Fs Gs› G
obtain F where F: "F ∈ Fs" "subsumes F G" unfolding subsume_def by auto
from F G show "∃F∈Fs. subsumes F H" using subsumes_trans by auto
qed
lemma subsume_Un[simp]:
"subsume Fs (Gs ∪ Hs) = (subsume Fs Gs ∧ subsume Fs Hs)"
by (auto simp: subsume_def)
lemma subsume_insert:
"subsume Fs (insert G Gs) = (subsume Fs {G} ∧ subsume Fs Gs)"
by (auto simp: subsume_def)
text ‹Transitivity check›
definition trans_scgs
where
"trans_scgs conn Gs =
(∀G∈set Gs. ∀H∈set Gs.
let GH = scg_comp conn G H
in (∃G'∈set Gs. subsumes G' GH))"
subsubsection ‹Checking the Scgs for descent›
text ‹Check for in-situ descent›
primrec in_situ :: "('pp, 'ap) scg ⇒ bool"
where
"in_situ Null = True"
| "in_situ (Scg p q str wk) = (∃(x,y)∈set str. x = y)"
lemma subsumes_in_situ:
"subsumes G H ⟹ in_situ G ⟹ in_situ H"
by (induct G H rule: subsumes.induct) auto
text ‹Sagiv's test (aka cycles check): Some power of G has a strict descent:›
primrec exp :: "('pp ⇒ 'pp ⇒ bool) ⇒ ('pp, 'ap :: linorder) scg ⇒ nat ⇒ ('pp, 'ap) scg"
where
"exp conn G 0 = G"
| "exp conn G (Suc n) = scg_comp conn (exp conn G n) G"
lemma exp_Null[simp]: "exp conn Null n = Null"
by (induct n) auto
definition sagiv
where
[code del]: "sagiv conn G = (∃n. in_situ (exp conn G n))"
text ‹Executable version:›
fun combine :: "('pp, 'ap :: linorder) scg ⇒ ('pp, 'ap) scg ⇒ ('pp, 'ap) scg"
where
"combine (Scg p q str wk) (Scg p' q' str' wk') =
Scg p q (union_list_sorted str str') (union_list_sorted wk wk')"
| "combine Null S = Null"
| "combine S Null = Null"
lemma in_situ_combine: "in_situ (combine G H) = (in_situ G ∨ in_situ H)"
by (induct G H rule: combine.induct) auto
inductive scg_eqv where
"scg_eqv Null Null"
| "set str = set str' ⟹ set str ∪ set wk = set str' ∪ set wk'
⟹ scg_eqv (Scg p q str wk) (Scg p q str' wk')"
lemma equiv_class_eq:
fixes R :: "'a ⇒ 'a ⇒ bool" (infix "≈" 70)
assumes refl: "⋀x. x ≈ x"
assumes trans: "⋀x y z. x ≈ y ⟹ y ≈ z ⟹ x ≈ z"
assumes sym: "⋀x y. x ≈ y ⟹ y ≈ x"
shows "x ≈ y = (R x = R y)"
proof
{ fix x y assume "x ≈ y"
have "{z. R x z} ⊆ {z. R y z}"
proof
fix z assume "z ∈ {z. R x z}" hence "x ≈ z" by simp
from trans[OF sym[OF this] ‹x ≈ y›, THEN sym]
show "z ∈ {z. R y z}" by simp
qed
} note sub = this
assume "x ≈ y"
from sub[OF this] and sub[OF sym[OF this]]
have "{z. x ≈ z} = {z. y ≈ z}" by simp
hence eq: "⋀z. z ∈ {z. x ≈ z} ⟷ z ∈ {z. y ≈ z}" by simp
show "R x = R y" by (rule ext) (rule eq[to_pred])
next
assume "R x = R y" thus "x ≈ y" by (simp add: refl)
qed
lemma scg_eqv: "scg_eqv G H = (scg_eqv G = scg_eqv H)"
proof (rule equiv_class_eq)
fix G show "scg_eqv G G"
by (cases G) (auto intro: scg_eqv.intros)
next
fix F G H assume "scg_eqv F G" "scg_eqv G H"
thus "scg_eqv F H" by (auto elim!: scg_eqv.cases intro!: scg_eqv.intros)
next
fix F G assume "scg_eqv F G"
thus "scg_eqv G F" by (auto elim!: scg_eqv.cases intro!: scg_eqv.intros)
qed
lemma scg_eqv1: "scg_eqv G = scg_eqv H ⟹ scg_eqv G H"
by (rule iffD2[OF scg_eqv])
lemma scg_eqv2: "scg_eqv G H ⟹ scg_eqv G = scg_eqv H"
by (rule iffD1[OF scg_eqv])
lemma comp_assoc:
"scg_eqv (scg_comp conn (scg_comp conn F G) H)
(scg_comp conn F (scg_comp conn G H))"
proof (cases "scg_comp conn (scg_comp conn F G) H")
case Null
thus ?thesis using scg_eqv.intros[intro]
by (cases F, auto, cases G, auto, cases H, auto simp: Let_def)
next
case Scg
then obtain p1 q1 s1 w1 p2 q2 s2 w2 p3 q3 s3 w3
where "F = Scg p1 q1 s1 w1"
"G = Scg p2 q2 s2 w2"
"H = Scg p3 q3 s3 w3" "conn q1 p2" "conn q2 p3"
by (cases F, simp, cases G, simp, cases H, simp_all add: Let_def split: if_splits)
thus ?thesis
apply (simp add: Let_def)
apply (rule scg_eqv.intros)
apply (auto 0 0)
apply (blast 16)+
done
qed
lemma comp_cong:
assumes G: "scg_eqv G = scg_eqv G'" and H: "scg_eqv H = scg_eqv H'"
shows "scg_eqv (scg_comp conn G H) = scg_eqv (scg_comp conn G' H')"
proof (cases G)
case Null
from G[THEN scg_eqv1] have Null': "G' = Null"
by (rule scg_eqv.cases) (auto simp: Null)
show ?thesis
by (rule scg_eqv2) (auto simp: Null Null' intro: scg_eqv.intros)
next
case (Scg p q s w)
note scg' = this
with G[THEN scg_eqv1] obtain sa wa
where G': "G' = Scg p q sa wa"
and G_eq: "set s = set sa" "set s ∪ set w = set sa ∪ set wa"
by (auto elim!: scg_eqv.cases)
show ?thesis
proof (cases H)
case Null
from H[THEN scg_eqv1] have Null': "H' = Null"
by (rule scg_eqv.cases) (auto simp: Null)
show ?thesis
by (rule scg_eqv2) (auto simp: scg' G' Null Null' intro: scg_eqv.intros)
next
case (Scg p' q' s' w')
with H[THEN scg_eqv1] obtain sa' wa'
where H': "H' = Scg p' q' sa' wa'"
and H_eq: "set s' = set sa'"
"set s' ∪ set w' = set sa' ∪ set wa'"
by (auto elim!: scg_eqv.cases)
show ?thesis
proof (cases "conn q p'")
case True
have "set s O (set s' ∪ set w')
∪ (set s ∪ set w) O set s'
= set sa O (set sa' ∪ set wa')
∪ (set sa ∪ set wa) O set sa'"
by (simp only: G_eq(2) H_eq(2), simp only: G_eq H_eq)
then have 1:
"(set s O set s' ∪ (set s O set w' ∪ set w O set s'))
= (set sa O set sa' ∪ (set sa O set wa' ∪ set wa O set sa'))"
by (simp add: Un_ac)
have 2: "(set s ∪ set w) O (set s' ∪ set w')
= (set sa ∪ set wa) O (set sa' ∪ set wa')"
by (simp only: G_eq(2) H_eq(2))
show ?thesis unfolding scg' Scg G' H'
apply (rule scg_eqv2)
apply (simp add: Let_def True)
apply (rule scg_eqv.intros)
apply (simp add: 1)
apply (insert 2, simp add: Un_ac)
done
next
case False
show ?thesis unfolding scg' Scg G' H'
by (rule scg_eqv2)
(auto simp: Let_def False intro: scg_eqv.intros)
qed
qed
qed
lemma exp_cong: "scg_eqv G = scg_eqv H
⟹ scg_eqv (exp conn G n) = scg_eqv (exp conn H n)"
by (induct n) (auto intro!: comp_cong)
lemma exp_comm: "scg_eqv (scg_comp conn G (exp conn G n))
= scg_eqv (scg_comp conn (exp conn G n) G)"
proof (induct n)
case 0 show ?case by simp
next
case (Suc n)
show ?case
apply simp
apply (unfold comp_assoc[THEN scg_eqv2, symmetric])
apply (rule comp_cong)
apply (unfold Suc[symmetric])
by auto
qed
lemma exp_compose:
"scg_eqv (scg_comp conn (exp conn G n) (exp conn G m))
= scg_eqv (exp conn G (Suc (n + m)))"
proof (induct n)
case 0 show ?case by (simp add: exp_comm)
next
case (Suc n)
have "scg_eqv (scg_comp conn (scg_comp conn (exp conn G n) G) (exp conn G m))
= scg_eqv (scg_comp conn (exp conn G n) (scg_comp conn G (exp conn G m)))"
by (simp add: comp_assoc[THEN scg_eqv2])
also have "... = scg_eqv (scg_comp conn (exp conn G n) (scg_comp conn (exp conn G m) G))"
by (rule comp_cong) (auto simp: exp_comm)
also have "... = scg_eqv (scg_comp conn (scg_comp conn (exp conn G n) (exp conn G m)) G)"
by (simp add: comp_assoc[THEN scg_eqv2])
also have "... = scg_eqv (scg_comp conn (exp conn G (Suc (n + m))) G)"
by (rule comp_cong) (auto simp: Suc)
finally show ?case by simp
qed
primrec strict_edge :: "'ap ⇒ 'ap ⇒ ('pp, 'ap) scg ⇒ bool"
where
"strict_edge i j Null = True"
| "strict_edge i j (Scg _ _ str _) = ((i,j)∈set str)"
primrec weak_edge :: "'ap ⇒ 'ap ⇒ ('pp, 'ap) scg ⇒ bool"
where
"weak_edge i j Null = True"
| "weak_edge i j (Scg _ _ str wk) = ((i,j)∈set wk ∪ set str)"
lemma edge_combine[simp]:
"strict_edge i j (combine G H) = (strict_edge i j G ∨ strict_edge i j H)"
"weak_edge i j (combine G H) = (weak_edge i j G ∨ weak_edge i j H)"
by (induct G H rule: combine.induct) auto
lemma weak_edge_decompose:
assumes "scg_comp conn G H ≠ Null"
assumes "weak_edge i k (scg_comp conn G H)"
obtains j where "weak_edge i j G" "weak_edge j k H"
using assms
by (induct conn G H rule: scg_comp.induct) (auto simp: Let_def split: if_splits)
lemma strict_edge_decompose:
assumes "scg_comp conn G H ≠ Null"
assumes "strict_edge i k (scg_comp conn G H)"
obtains j where "strict_edge i j G" "strict_edge j k H"
| j where "strict_edge i j G" "weak_edge j k H"
| j where "weak_edge i j G" "strict_edge j k H"
using assms
by (induct conn G H rule: scg_comp.induct) (auto simp: Let_def split: if_splits)
lemma exp_compose_strict: "strict_edge i j (scg_comp conn (exp conn G n) (exp conn G m))
= strict_edge i j (exp conn G (Suc (n + m)))"
using exp_compose[THEN scg_eqv1, of conn G n m]
by rule auto
lemma exp_compose_weak: "weak_edge i j (scg_comp conn (exp conn G n) (exp conn G m))
= weak_edge i j (exp conn G (Suc (n + m)))"
using exp_compose[THEN scg_eqv1, of conn G n m]
by rule auto
lemma subsumes_exp_mono:
assumes "subsumes G H"
shows "subsumes (exp conn G n) (exp conn H n)"
by (induct n) (auto intro: subsumes_comp_mono assms)
lemma combine_subsumes: "subsumes G (combine G H)"
by (induct G H rule: combine.induct) auto
lemma in_situ_subsumes:
"subsumes G H ⟹ in_situ G ⟹ in_situ H"
by (induct G H rule: subsumes.induct) auto
lemma sagiv_subsumes:
assumes sub: "subsumes G H" and G: "sagiv conn G"
shows "sagiv conn H"
proof -
from G obtain n where 1: "in_situ (exp conn G n)" unfolding sagiv_def ..
from sub have "subsumes (exp conn G n) (exp conn H n)"
by (rule subsumes_exp_mono)
from this 1 have "in_situ (exp conn H n)" by (rule in_situ_subsumes)
thus ?thesis unfolding sagiv_def ..
qed
lemma sagiv_step:
"sagiv conn G ⟷ sagiv conn (combine G (scg_comp conn G G))"
(is "?A ⟷ ?B")
proof
assume ?A
then show ?B by (rule sagiv_subsumes[OF combine_subsumes])
next
let ?G' = "combine G (scg_comp conn G G)"
assume ?B show ?A
proof (cases ?G')
case Null
hence "G = Null ∨ scg_comp conn G G = Null" by (cases G) (auto simp: Let_def)
thus ?thesis
proof
assume "G = Null" thus ?thesis
by (auto simp: sagiv_def)
next
assume "scg_comp conn G G = Null"
hence "in_situ (exp conn G 1)" by auto
thus ?thesis unfolding sagiv_def ..
qed
next
case (Scg p q str wk)
then obtain str' wk' where Scg': "G = Scg p q str' wk'"
by (cases G) (auto split: if_splits simp: Let_def)
with Scg have composable: "conn q p" by (auto split: if_splits)
{
fix n
from composable Scg
have "∃s w. exp conn ?G' n = Scg p q s w" by (induct n) (auto simp: Let_def)
hence "exp conn ?G' n ≠ Null" by auto
}
note nonnull = this
{
fix i j
assume "strict_edge i j ?G'"
from this[simplified]
have "∃m. strict_edge i j (exp conn G m)"
proof
assume "strict_edge i j G" then have "strict_edge i j (exp conn G 0)" by auto
thus ?thesis ..
next
assume "strict_edge i j (scg_comp conn G G)" then have "strict_edge i j (exp conn G 1)" by auto
thus ?thesis ..
qed
}
note strict_step = this
{
fix i j
assume "weak_edge i j ?G'"
from this[simplified]
have "∃m. weak_edge i j (exp conn G m)"
proof
assume "weak_edge i j G" then have "weak_edge i j (exp conn G 0)" by auto
thus ?thesis ..
next
assume "weak_edge i j (scg_comp conn G G)" then have "weak_edge i j (exp conn G 1)" by auto
thus ?thesis ..
qed
}
note weak_step = this
{
fix i j n
have "strict_edge i j (exp conn ?G' n) ⟹ ∃m. strict_edge i j (exp conn G m)"
and "weak_edge i j (exp conn ?G' n) ⟹ ∃m. weak_edge i j (exp conn G m)"
proof (induct n arbitrary: i j)
case 0 case 1 thus ?case by (simp add: strict_step)
next
case 0 case 2
hence "weak_edge i j G ∨ weak_edge i j (scg_comp conn G G)"
(is "?X ∨ ?Y") by auto
thus ?case
proof
assume ?X then have "weak_edge i j (exp conn G 0)" by auto
thus ?thesis ..
next
assume ?Y then have "weak_edge i j (exp conn G 1)" by auto
thus ?thesis ..
qed
next
case (Suc n) case (1 i k)
then have a: "strict_edge i k (scg_comp conn (exp conn ?G' n) ?G')" by simp
show ?case
proof (rule strict_edge_decompose[OF nonnull[of "Suc n", simplified] a])
fix j
assume 1: "strict_edge i j (exp conn ?G' n)"
and 2: "strict_edge j k ?G'"
from Suc(1)[OF 1] strict_step[OF 2]
obtain m m'
where "strict_edge i j (exp conn G m)" "strict_edge j k (exp conn G m')"
by auto
then have "strict_edge i k (scg_comp conn (exp conn G m) (exp conn G m'))"
by (cases "exp conn G m", auto, cases "exp conn G m'", auto simp: Let_def)
then have "strict_edge i k (exp conn G (Suc (m + m')))" unfolding exp_compose_strict .
thus "∃m. strict_edge i k (exp conn G m)" ..
next
fix j
assume 1: "strict_edge i j (exp conn ?G' n)"
and 2: "weak_edge j k ?G'"
from Suc(1)[OF 1] weak_step[OF 2]
obtain m m'
where "strict_edge i j (exp conn G m)" "weak_edge j k (exp conn G m')"
by auto
then have "strict_edge i k (scg_comp conn (exp conn G m) (exp conn G m'))"
by (cases "exp conn G m", auto, cases "exp conn G m'", auto simp: Let_def)
then have "strict_edge i k (exp conn G (Suc (m + m')))" unfolding exp_compose_strict .
thus "∃m. strict_edge i k (exp conn G m)" ..
next
fix j
assume 1: "weak_edge i j (exp conn ?G' n)"
and 2: "strict_edge j k ?G'"
from Suc(2)[OF 1] strict_step[OF 2]
obtain m m'
where "weak_edge i j (exp conn G m)" "strict_edge j k (exp conn G m')"
by auto
then have "strict_edge i k (scg_comp conn (exp conn G m) (exp conn G m'))"
apply (cases "exp conn G m", auto)
apply (cases "exp conn G m'", auto simp: Let_def)
apply (cases "exp conn G m'", auto simp: Let_def) done
then have "strict_edge i k (exp conn G (Suc (m + m')))" unfolding exp_compose_strict .
thus "∃m. strict_edge i k (exp conn G m)" ..
qed
next
case (Suc n) case (2 i k)
then have a: "weak_edge i k (scg_comp conn (exp conn ?G' n) ?G')" by simp
show ?case
proof (rule weak_edge_decompose[OF nonnull[of "Suc n", simplified] a])
fix j
assume 1: "weak_edge i j (exp conn ?G' n)"
and 2: "weak_edge j k ?G'"
from Suc(2)[OF 1] weak_step[OF 2]
obtain m m'
where "weak_edge i j (exp conn G m)" "weak_edge j k (exp conn G m')"
by auto
then have "weak_edge i k (scg_comp conn (exp conn G m) (exp conn G m'))"
apply (cases "exp conn G m", auto)
apply (cases "exp conn G m'", auto simp: Let_def)
apply (cases "exp conn G m'", auto simp: Let_def) done
then have "weak_edge i k (exp conn G (Suc (m + m')))" unfolding exp_compose_weak .
thus "∃m. weak_edge i k (exp conn G m)" ..
qed
qed
}
note r = this(1)
from ‹?B› obtain n
where "in_situ (exp conn ?G' n)"
unfolding sagiv_def ..
with nonnull
obtain i
where "strict_edge i i (exp conn ?G' n)"
by (cases "exp conn (combine G (scg_comp conn G G)) n") auto
from r[OF this]
obtain m where "strict_edge i i (exp conn G m)" ..
then
have "in_situ (exp conn G m)"
by (cases "exp conn G m") auto
thus "sagiv conn G"
unfolding sagiv_def ..
qed
qed
lemma sagiv_code[code]:
"sagiv conn G =
(if in_situ G
then True
else let GG = scg_comp conn G G
in if subsumes GG G then False
else sagiv conn (combine G GG))"
proof cases
assume G: "in_situ G"
hence "in_situ (exp conn G 0)" by simp
hence "sagiv conn G" unfolding sagiv_def ..
with G show ?thesis by simp
next
assume nG: "¬ in_situ G"
show ?thesis
proof cases
assume sub: "subsumes (scg_comp conn G G) G"
{
fix n have "subsumes (exp conn G n) G"
proof (induct n)
case 0 show ?case by simp
next
case (Suc n)
from this subsumes_refl
have "subsumes (scg_comp conn (exp conn G n) G) (scg_comp conn G G)"
by (rule subsumes_comp_mono)
also have "subsumes (…) G" by (fact sub)
finally show ?case by simp
qed
}
from subsumes_in_situ[OF this] and nG
have "¬ sagiv conn G" unfolding sagiv_def by auto
with nG sub show ?thesis by auto
next
assume nsub: "¬ subsumes (scg_comp conn G G) G"
with nG sagiv_step
show ?thesis by auto
qed
qed
subsection ‹Transition system semantics›
locale sct_semantics =
fixes S NS :: "'a rel"
fixes conn :: "'pp :: compare_order ⇒ 'pp ⇒ bool"
assumes wf_S: "SN S"
assumes SN_compat: "NS O S ⊆ S"
begin
abbreviation "trN == (NS ∪ S)^*"
abbreviation "trS == trN O S O trN"
lemma tr_subset: "trS ⊆ trN"
proof -
have "trS ⊆ trN O trN O trN"
by (intro relcomp_mono) auto
also have "… ⊆ trN" by auto
finally show ?thesis .
qed
lemma SN_compat': "trN O trS ⊆ trS"
by (simp add: O_assoc[symmetric])
lemma NS_compat': "trS O trN ⊆ trS"
by (simp add: O_assoc)
lemma SS_compat': "trS O trS ⊆ trS"
using tr_subset NS_compat'
by (blast 7)
lemma NN_compat': "trN O trN ⊆ trN"
by auto
lemma SN_trS: "SN trS"
using SN_compat wf_S by (rule compatible_SN')
primrec steps :: "('pp, 'ap) scg ⇒ ('pp × ('ap ⇒ 'a)) rel"
where
"steps Null = {}"
| "steps (Scg p q str wk) =
{ ((p, f) , (r, g)) | f g r.
(∀(x,y)∈set str. (f x, g y) ∈ trS)
∧ (∀(x,y)∈set wk. (f x, g y) ∈ trN) ∧ conn q r }"
lemma steps_subsumes: "subsumes G G' ⟹ steps G' ⊆ steps G"
using tr_subset
by (induct G G' rule: subsumes.induct) (auto, blast+)
lemma steps_comp:
shows "steps G O steps G' ⊆ steps (scg_comp conn G G')"
proof (induct "c::'pp⇒'pp⇒bool" G G' rule: scg_comp.induct)
case (1 _ p q str wk p' q' str' wk')
have FalseI: "⋀ P. ~P ⟹ P ⟹ False" by auto
from 1 show ?case
proof (rule, simp_all only: split_paired_all)
fix pa qa f g
assume "((pa,f), (qa,g))
∈ steps (Scg p q str wk) O steps (Scg p' q' str' wk')"
then obtain r h where
"((pa,f), (r,h)) ∈ steps (Scg p q str wk)"
"((r,h), (qa,g)) ∈ steps (Scg p' q' str' wk')"
by auto
thus "((pa,f), (qa,g))
∈ steps (scg_comp conn (Scg p q str wk) (Scg p' q' str' wk'))"
apply (auto 1 0 simp: Let_def)
apply (rule subsetD[OF SS_compat'])
apply (rule_tac b="h y" in relcompI, force, force)
apply (rule subsetD[OF NS_compat'])
apply (rule_tac b="h y" in relcompI, force, force)
apply (rule subsetD[OF SN_compat'])
apply (rule_tac b="h y" in relcompI, force, force)
apply (rule ccontr, rule_tac FalseI[of "(f x, g z) ∈ trN" for x z], force)
apply (rule subsetD[OF NN_compat'])
apply (rule_tac b="h y" in relcompI, force, force)
done
qed
qed auto
lemma trans_scgs:
assumes tr: "trans_scgs conn Gs"
shows "trans (⋃G∈set Gs. steps G)" (is "trans ?R")
proof (rule transI, simp only: split_paired_all)
fix p q r f g h
assume "((p, f), (q, g)) ∈ ?R" "((q, g), (r, h)) ∈ ?R"
then obtain G H where GH: "G ∈ set Gs" "H ∈ set Gs"
and "((p, f), (q, g)) ∈ steps G"
"((q, g), (r, h)) ∈ steps H"
by auto
hence comp: "((p, f), (r, h)) ∈ steps (scg_comp conn G H)" using steps_comp by auto
from tr GH obtain G' where "G' ∈ set Gs"
and "subsumes G' (scg_comp conn G H)"
unfolding trans_scgs_def by auto
with comp have "((p, f), (r, h)) ∈ steps G'" using steps_subsumes by auto
with ‹G' ∈ set Gs› show "((p, f), (r, h)) ∈ ?R" by auto
qed
lemma in_situ_SN:
"in_situ G ⟹ SN (steps G)"
proof (induct G)
case (Scg p q str wk)
then obtain x where "(x,x) ∈ set str" by auto
then have subset: "steps (Scg p q str wk) ⊆ inv_image trS (λ(p,f). f x)"
unfolding inv_image_def by auto
have "SN (inv_image trS (λ(p,f). f x))"
by (intro SN_inv_image SN_trS)
then show ?case using subset
by (rule SN_subset)
qed auto
lemma steps_exp: "steps G ^^ Suc n ⊆ steps (exp conn G n)"
proof (induct n)
case (Suc n)
have "steps G ^^ (Suc (Suc n)) = steps G ^^ (Suc n) O steps G" by simp
also have "... ⊆ steps (exp conn G n) O steps G" by (intro relcomp_mono Suc subset_refl)
also have "... ⊆ steps (scg_comp conn (exp conn G n) G)" by (rule steps_comp)
also have "... ⊆ steps (exp conn G (Suc n))" by simp
finally show ?case .
qed auto
lemma sagiv_SN:
assumes a: "sagiv conn G"
shows "SN (steps G)"
using a
unfolding sagiv_def
proof
fix n assume "in_situ (exp conn G n)"
hence "SN (steps (exp conn G n))" by (rule in_situ_SN)
from this steps_exp
have "SN (steps G ^^ Suc n)" by (rule SN_subset)
thus "SN (steps G)" unfolding SN_pow[symmetric] .
qed
text ‹Version that assumes that the closure is already given›
lemma SCT_correctness:
fixes R :: "('pp × ('ap :: linorder ⇒ 'a)) rel"
assumes abst: "R ⊆ (⋃G∈set Gs. steps G)"
assumes trans: "trans_scgs conn Ts"
assumes super: "subsume (set Ts) (set Gs)"
assumes good: "∀G∈set Ts. sagiv conn G"
shows "SN R"
proof -
from good
have "⋀G. G ∈ set Ts ⟹ SN (steps G)"
by (auto dest!: sagiv_SN)
hence disj: "disj_wf ((⋃G∈set Ts. steps G)^-1)"
unfolding disj_wf_def
apply (rule_tac x = "λi. (steps (Ts ! i))^-1" in exI)
apply (rule_tac x = "length Ts" in exI)
apply (simp add: SN_iff_wf)
apply auto
apply (metis in_set_conv_nth lessThan_iff)
apply (metis in_set_conv_nth)
done
from trans
have "trans (⋃G∈set Ts. steps G)"
by (rule trans_scgs)
from this and disj
have SN: "SN (⋃G∈set Ts. steps G)"
unfolding SN_iff_wf
by (auto intro: trans_disj_wf_implies_wf)
note abst
also from super have
"(⋃G∈set Gs. steps G) ⊆ (⋃G∈set Ts. steps G)"
by (force simp: subsume_def dest!: steps_subsumes)
finally
show "SN R" by (rule SN_subset[OF SN])
qed
end
text ‹Transitive closure computation›
definition generate_scgs :: "('pp ⇒ 'pp ⇒ bool) ⇒ ('pp, 'ap :: linorder) scg list ⇒ ('pp, 'ap) scg ⇒ ('pp,'ap) scg list"
where "generate_scgs conn base g ≡ filter (λ g. g ≠ Null) (map (scg_comp conn g) base)"
fun pps_of :: "('pp, 'ap) scg ⇒ 'pp set"
where
"pps_of Null = {}"
| "pps_of (Scg p q _ _) = {p,q}"
fun aps_of :: "('pp, 'ap) scg ⇒ 'ap set"
where
"aps_of Null = {}"
| "aps_of (Scg _ _ str wk) = set (map fst str) ∪ set (map snd str) ∪ set (map fst wk) ∪ set (map snd wk)"
lemma finite_pps[simp]: "finite (pps_of G)" by (cases G) auto
lemma finite_aps[simp]: "finite (aps_of G)" by (cases G) auto
lemma image_fst_snd: "(a,b)∈S ⟹ a ∈ fst ` S" "(a,b)∈S ⟹ b ∈ snd ` S"
by force+
lemma pps_of_comp: "pps_of (scg_comp conn G H) ⊆ pps_of G ∪ pps_of H"
by (induct conn G H rule: scg_comp.induct) (auto simp: Let_def)
lemma aps_of_comp: "aps_of (scg_comp conn G H) ⊆ aps_of G ∪ aps_of H"
by (induct conn G H rule: scg_comp.induct) (auto simp: image_fst_snd Let_def)
definition graph_bound where
"graph_bound T =
(let P = (⋃H∈T. pps_of H); A = (⋃H∈T. aps_of H)
in (λ(p,q,str,wk). Scg p q str wk) ` (P × P × {xs . distinct xs ∧ set xs ⊆ A × A} × {xs . distinct xs ∧ set xs ⊆ A × A})) ∪ {Null}"
lemma finite_graph_bound[intro]: "finite G ⟹ finite (graph_bound G)"
unfolding graph_bound_def Let_def
by (intro finite_UnI finite_imageI,
intro finite_SigmaI finite_distinct_subset, auto)
lemma graph_bound_subsetI:
"(⋃G∈S. pps_of G) ⊆ (⋃G∈T. pps_of G)
⟹ (⋃G∈S. aps_of G) ⊆ (⋃G∈T. aps_of G)
⟹ graph_bound S ⊆ graph_bound T"
unfolding graph_bound_def Let_def
by (intro Un_mono image_mono, auto)
lemma graph_bound_mono: "Gs ⊆ Hs ⟹ graph_bound Gs ⊆ graph_bound Hs"
by (rule graph_bound_subsetI) auto
lemma graph_boundI:
assumes G: "G = Scg p q str wk"
and disj: "distinct str" "distinct wk"
shows "G ∈ graph_bound {G}"
unfolding graph_bound_def assms G Let_def
using disj
by (intro UnI1 image_eqI[of _ _ "(p,q,str,wk)"],
auto simp: image_fst_snd)
lemma graph_bound_scg_comp:
assumes GT: "G ∈ graph_bound T ∪ T"
and BT: "B ∈ T"
shows "scg_comp conn G B ∈ graph_bound T"
proof -
let ?G = "scg_comp conn G B"
show ?thesis
proof (cases "?G = Null")
case True
thus ?thesis unfolding graph_bound_def by auto
next
case False
then obtain p1 q1 s1 w1 where G: "G = Scg p1 q1 s1 w1" by (cases G, auto)
from False G obtain p2 q2 s2 w2 where B: "B = Scg p2 q2 s2 w2" by (cases B, auto)
from False G B have c: "conn q1 p2 = True" by (cases "conn q1 p2", auto)
from B BT have q: "q2 ∈ ⋃ {pps_of B | B. B ∈ T}" by auto
from G GT have p: "p1 ∈ ⋃ {pps_of B | B. B ∈ T}"
unfolding graph_bound_def by auto
let ?A = "UNION T aps_of"
let ?D = "{xs. distinct xs ∧ set xs ⊆ ?A × ?A}"
let ?s = "(remdups_sort (comp s1 s2 @ comp s1 w2 @ comp w1 s2))"
let ?w = "(subtract_list_sorted (remdups_sort (comp w1 w2)) ?s)"
have GG: "?G = Scg p1 q2 ?s ?w"
unfolding G B using c by (simp add: Let_def)
have mem: "?G ∈ graph_bound {?G}"
by (rule graph_boundI[OF GG], auto)
let ?all = "set s1 ∪ set s2 ∪ set w1 ∪ set w2"
show ?thesis
proof (rule set_mp[OF graph_bound_subsetI mem])
show "(⋃ G ∈ {?G}. pps_of G) ⊆ (⋃G∈T. pps_of G)" unfolding GG using p q by auto
next
have "(⋃ G ∈ {?G}. aps_of G) = aps_of ?G" unfolding GG by simp
also have "... ⊆ fst ` ?all ∪ snd ` ?all" unfolding GG
by (auto simp add: image_fst_snd)
also have "... ⊆ (aps_of B ∪ aps_of G)" unfolding B G by auto
also have "... ⊆ (⋃G ∈ T. aps_of G) ∪ aps_of G" using BT by auto
also have "... ⊆ (⋃G ∈ T. aps_of G)" using GT
proof
assume "G ∈ T" thus ?thesis by auto
next
assume GT: "G ∈ graph_bound T"
from GT
have "(s1,w1) ∈ ?D × ?D" using GT
unfolding G graph_bound_def Let_def by auto
hence "aps_of G ⊆ (⋃G ∈ T. aps_of G)" unfolding G aps_of.simps
by (auto simp: image_fst_snd, force+)
thus ?thesis by auto
qed
finally show "(⋃ G ∈ {?G}. aps_of G) ⊆ (⋃ G ∈ T. aps_of G)" .
qed
qed
qed
lemma finite_generate_scgs: "finite {g'. (g,g') ∈ {(a,b). b ∈ set (generate_scgs conn Gs a)}^*}" (is "finite ?S")
proof -
let ?G = "graph_bound (insert g (set Gs)) ∪ (insert g (set Gs))"
have fin: "finite ?G" by auto
show ?thesis
proof (rule finite_subset[OF _ fin], rule)
fix g'
assume "g' ∈ ?S"
hence "(g,g') ∈ {(a,b). b ∈ set (generate_scgs conn Gs a)}^*" by auto
thus "g' ∈ ?G"
proof (induct rule: rtrancl_induct)
case base show ?case by simp
next
case (step g1 g2)
from step(2)[unfolded generate_scgs_def]
obtain b where g2: "g2 = scg_comp conn g1 b" and b: "b ∈ insert g (set Gs)" by auto
from graph_bound_scg_comp[OF step(3) b]
show ?case unfolding g2 by auto
qed
qed
qed
derive compare_order scg
definition check_SCT :: "('pp :: compare_order ⇒ 'pp ⇒ bool) ⇒ ('pp, 'ap :: compare_order) scg list ⇒ bool"
where
"check_SCT conn Gs =
rs.ball (mk_rtrancl_set (generate_scgs conn Gs) Gs) (sagiv conn)"
lemma scg_eqv_subsumes: "scg_eqv G = scg_eqv H ⟹ subsumes I G = subsumes I H"
unfolding scg_eqv[symmetric]
by (induct rule: scg_eqv.induct, auto, (cases I, auto)+)
lemma (in sct_semantics) SCT_correctness2:
fixes R :: "('pp × ('ap :: compare_order ⇒ 'a)) rel"
assumes abst: "R ⊆ (⋃G∈set Gs. steps G)"
assumes check: "check_SCT conn Gs"
shows "SN R"
proof -
let ?r = "generate_scgs conn Gs"
let ?R = "{(a,b). b ∈ set (?r a)}"
let ?S = "mk_rtrancl_set ?r Gs"
note d = generate_scgs_def
note sub_refl = subsumes_refl
interpret relation_subsumption_set ?r
proof
fix g
show "finite {g'. (g,g') ∈ {(a,b). b ∈ set (?r a)}^*}" by (rule finite_generate_scgs)
qed
have S: "rs.α ?S = mk_rtrancl Gs" unfolding mk_rtrancl_set ..
def S ≡ "rs.to_list ?S"
have SS: "set S = rs.α ?S" unfolding S_def by (auto simp: rs.correct)
note abst
moreover
have "trans_scgs conn S"
unfolding trans_scgs_def
unfolding S SS Let_def
unfolding mk_rtrancl_no_subsumption[OF refl]
proof (clarify)
fix G BG H BH
assume BG: "BG ∈ set Gs" and BGG: "(BG,G) ∈ ?R^*"
assume BH: "BH ∈ set Gs" and BHH: "(BH,H) ∈ ?R^*"
let ?C = "scg_comp conn"
from BHH
have "∃ I. scg_eqv (?C G H) = scg_eqv I ∧ ((BG,I) ∈ ?R^* ∨ I = Null)"
proof (induct rule: rtrancl_induct)
case base
have "BH ∈ set Gs ⟹ (BG,?C G BH) ∈ ?R^* ∨ ?C G BH = Null"
using BGG
proof (induct arbitrary: BH rule: rtrancl_induct)
case base
thus ?case using BG unfolding d by auto
next
case (step G H)
from step(2) have GH: "H ∈ set (?r G)" by simp
then obtain B where B: "B ∈ set Gs" and H: "H = ?C G B" and N: "H ≠ Null" unfolding d by auto
from step(1) have BGG: "(BG, G) ∈ ?R^*" .
from step(3)[OF B] have H: "(BG,H) ∈ ?R^* ∨ H = Null" unfolding H .
show ?case
proof (cases "?C H BH = Null")
case True
thus ?thesis by simp
next
case False
hence "(H,?C H BH) ∈ ?R" using step(4) unfolding d by auto
moreover from False H have H: "(BG,H) ∈ ?R^*" by (cases H, auto)
ultimately have steps: "(BG,?C H BH) ∈ ?R^* O ?R" by auto
have "(BG, ?C H BH) ∈ ?R^*"
by (rule set_mp[OF _ steps], regexp)
thus ?thesis by auto
qed
qed
from this[OF BH]
show ?case by auto
next
case (step H I)
from step(3) obtain J where eq: "scg_eqv (?C G H) = scg_eqv J"
and BGI: "(BG, J) ∈ ?R^* ∨ J = Null" by auto
from step(2) obtain B where B: "B ∈ set Gs" and
I: "I = ?C H B" and N: "I ≠ Null" unfolding d by auto
have assoc: "scg_eqv (scg_comp conn G (scg_comp conn G1 H)) = scg_eqv (scg_comp conn (scg_comp conn G G1) H)"
for G1 H
by (rule sym, subst scg_eqv[symmetric], rule comp_assoc)
note J = comp_cong[OF eq refl, of conn B]
show ?case unfolding I J assoc
proof (cases "?C J B = Null")
case True
thus "∃ I. scg_eqv (?C J B) = scg_eqv I ∧ ((BG,I) ∈ ?R^* ∨ I = Null)"
by auto
next
case False
hence R: "(J, ?C J B) ∈ ?R" using B unfolding d by auto
from False have J: "J ≠ Null" by auto
with BGI R
have steps: "(BG, ?C J B) ∈ ?R^* O ?R" by auto
have "(BG, ?C J B) ∈ ?R^*"
by (rule set_mp[OF _ steps], regexp)
thus "∃ I. scg_eqv (?C J B) = scg_eqv I ∧ ((BG,I) ∈ ?R^* ∨ I = Null)"
by auto
qed
qed
then obtain I where eq: "scg_eqv (?C G H) = scg_eqv I"
and BGI: "(BG,I) ∈ ?R^* ∨ I = Null" by auto
from scg_eqv_subsumes[OF eq]
have eq: "⋀ J. subsumes J (?C G H) = subsumes J I" by simp
from BGI BG have "I ∈ ?R^* `` set Gs ∨ I = Null" by auto
thus "∃ J ∈ ?R^* `` set Gs. subsumes J (?C G H)"
proof
assume "I ∈ ?R^* `` set Gs"
thus ?thesis unfolding eq using sub_refl by blast
next
assume "I = Null"
thus ?thesis using BG unfolding eq by auto
qed
qed
moreover have "subsume (set S) (set Gs)"
unfolding subsume_def S SS
unfolding mk_rtrancl_no_subsumption[OF refl]
proof (clarify)
fix G
assume G: "G ∈ set Gs"
hence "G ∈ ?R^* `` set Gs" by auto
thus "∃ H ∈ ?R^* `` set Gs. subsumes H G"
using sub_refl[of G] by blast
qed
moreover from check[unfolded check_SCT_def Let_def]
have "∀G∈set S. sagiv conn G" by (simp add: rs.correct S SS)
ultimately show "SN R"
by (rule SCT_correctness)
qed
end