Theory Prelim
section ‹Introduction›
text ‹
This development provides a formalization of a trace-based Rely-Guarantee semantics.
The core approach is built upon the foundational work of Xu et al.~\cite{Xu_et_al},
who established a framework for reasoning about concurrent programs using interactive traces.
To support this semantics, we first define an abstract programming language featuring
sequential composition, while loops, and parallel execution. This language is equipped
with an operational semantics explicitly designed to facilitate concurrent reasoning by
interleaving command executions with environment steps.
Building upon these trace-based foundations, we develop a robust reasoning infrastructure.
This includes comprehensive Rely-Guarantee inversion rules that characterize the structural
decomposition of traces, abstract definitions of trace satisfiability, and standard
soundness proofs adapted for both unary and binary postcondition settings.
The formalization presented here serves as the foundational basis for the broader
investigations into coinductive Rely-Guarantee semantics and equivalence proofs
described by Derrick et al.~\cite{RelyGuarantee}.
›
section ‹Preliminaries›
text ‹This theory sets up notation and preliminary definitions used throughout the mechanization ›
theory Prelim imports Complex_Main
begin
thm le_fun_def
thm relcompp_apply
thm relcompp.simps
hide_const stable
lemma map_Pair_zip_replicate_length:
"map (Pair x) ys = zip (replicate (length ys) x) ys"
by (simp add: zip_replicate1)
lemma OO_rtranclp_le:
assumes "U OO A ≤ V" "(U OO Z^**) OO (Z OO A) ≤ V"
shows "(U OO Z^**) OO A ≤ V"
using assms unfolding OO_def
by auto (smt (verit, best) predicate2D rtranclp.simps)
lemma rtranclp_chain:
assumes "R⇧*⇧* a b"
shows "∃n as. as 0 = a ∧ as n = b ∧ (∀i<n. R (as i) (as (Suc i)))"
using assms proof induction
case base
then show ?case
apply(intro exI[of _ 0] exI[of _ "λi. a"])
by auto
next
case (step b c)
show ?case using step apply safe
subgoal for n as
apply(intro exI[of _ "Suc n"] exI[of _ "λi. if i ≤ n then as i else c"])
using le_less_Suc_eq by force .
qed
lemma chain_rtranclp:
assumes "as 0 = a" "as n = b" "∀i<n. R (as i) (as (Suc i))"
shows "R⇧*⇧* a b"
using assms apply(induct n arbitrary: b) by auto
definition notP :: "('a ⇒ bool) ⇒ ('a ⇒ bool)"
("¬1 _" [40] 70)
where
"¬1 P ≡ λa. ¬ P a"
definition conjP :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)"
(infixr "∧1" 65)
where
"P1 ∧1 P2 ≡ λa. P1 a ∧ P2 a"
definition disjP :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)"
(infixr "∨1" 60)
where
"P1 ∨1 P2 ≡ λa. P1 a ∨ P2 a"
definition notR :: "('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool)"
("¬2 _" [40] 40)
where
"¬2 R ≡ λa b. ¬ R a b"
definition conjR ::
"('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool)"
(infixr "∧2" 65)
where
"R1 ∧2 R2 ≡ λa b. R1 a b ∧ R2 a b"
definition disjR ::
"('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool)"
(infixr "∨2" 60)
where
"R1 ∨2 R2 ≡ λa b. R1 a b ∨ R2 a b"
definition interR ::
"('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool)"
(infixr "∩2" 70)
where
"R1 ∩2 R2 ≡ λa b. ∀c d. R1 c d ∧ R2 c d ⟶ a = c ∧ b = d "
definition satR ::
"('a ⇒ 'b ⇒ bool)"
where
"satR ≡ λa b. True"
definition imR :: "('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('b ⇒ bool)" where
"imR R P ≡ λb. ∃a. P a ∧ R a b"
lemmas imR_defs = imR_def le_bool_def le_fun_def
definition rimR :: "('a ⇒ 'b ⇒ bool) ⇒ ('b ⇒ bool) ⇒ ('a ⇒ bool)" where
"rimR R P ≡ λa. ∃b. P b ∧ R a b"
definition grR :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b ⇒ bool" where
"grR f ≡ (λa b. f a = b)"
definition diagR :: "('a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" where
"diagR P ≡ λa b. a = b ∧ P a"
definition lift1 :: "('a ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool"
where "lift1 P ≡ λa b. P a"
definition lift2 :: "('b ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool"
where "lift2 P ≡ λa b. P b"
lemma lift1_mono: "P1 ≤ P2 ⟹ lift1 P1 ≤ lift1 P2"
unfolding lift1_def by auto
lemma lift2_mono: "P1 ≤ P2 ⟹ lift2 P1 ≤ lift2 P2"
unfolding lift2_def by auto
lemma conjR_lift2_rel_1_OO: "(R ∧2 lift2 P) OO Q = R OO (lift1 P ∧2 Q)"
unfolding conjR_def lift2_def lift1_def by auto
lemma conjP_idem[simp]: "P ∧1 P = P"
unfolding conjP_def by auto
lemma disjP_idem[simp]: "P ∨1 P = P"
unfolding disjP_def by auto
lemma conjR_idem[simp]: "R ∧2 R = R"
unfolding conjR_def by auto
lemma disjR_idem[simp]: "R ∨2 R = R"
unfolding disjR_def by auto
lemma conjP_idem2[simp]: "P ∧1 P ∧1 P' = P ∧1 P'"
by (simp add: conjP_def)
lemma notP_item: "¬ P s ⟷ (¬1 P) s"
by (simp add: notP_def)
lemma disjR_I1[intro]:"P s s' ⟹ (P ∨2 Q) s s'" unfolding disjR_def by auto
lemma disjR_I2[intro]:"Q s s' ⟹ (P ∨2 Q) s s'" unfolding disjR_def by auto
lemma conjR_I:"Q1 s s' ∧ Q2 s s' ⟹ Q1 ∧2 Q2 ≤ Q ⟹ Q s s'" unfolding conjR_def by auto
lemma lift1_inject:"lift1 P ≤ Q ⟹ P s ⟹ ∀s'. Q s s' " unfolding lift1_def le_bool_def le_fun_def by auto
definition stable :: "('s ⇒ bool) ⇒ ('s ⇒ 's ⇒ bool) ⇒ bool" where
"stable P R ≡ ∀ s s'. P s ∧ R s s' ⟶ P s'"
definition stableLeft :: "('s ⇒ 's ⇒ bool) ⇒ ('s ⇒ 's ⇒ bool) ⇒ bool" where
"stableLeft Q R ≡ R OO Q ≤ Q"
definition stableRight :: "('s ⇒ 's ⇒ bool) ⇒ ('s ⇒ 's ⇒ bool) ⇒ bool" where
"stableRight Q R ≡ Q OO R ≤ Q"
definition stable2 :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool" where
"stable2 Q R ≡ stableLeft Q R ∧ stableRight Q R"
lemma stable2_def2: "stable2 Q R ⟷ R OO Q ≤ Q ∧ Q OO R ≤ Q"
by (simp add: stable2_def stableLeft_def stableRight_def)
lemma stableLeft_alt:
"stableLeft Q R ⟷
(∀ s s' s''. R s s' ∧ Q s' s'' ⟶ Q s s'')"
unfolding stableLeft_def by auto
lemma stableRight_alt:
"stableRight Q R ⟷
(∀ s s' s''. Q s s' ∧ R s' s'' ⟶ Q s s'')"
unfolding stableRight_def by auto
lemmas stable2_defs = stable2_def stableRight_alt stableLeft_alt
lemma stable_stable2:
"stable P R ⟷ stable2 (lift2 P) R"
unfolding stable_def stable2_def stableLeft_def
stableRight_def lift2_def by auto
lemma stable_rtraclp:
assumes "stable P R"
shows "stable P R^**"
unfolding stable_def proof safe
fix s s' assume "R⇧*⇧* s s'" "P s"
thus "P s'"
apply induct using assms unfolding stable_def by auto
qed
lemma stableLeft_rtraclp:
assumes "stableLeft Q R"
shows "stableLeft Q R^**"
unfolding stableLeft_def OO_def proof safe
fix s s' s'' assume "R⇧*⇧* s s'" "Q s' s''"
thus "Q s s''"
apply induct using assms unfolding stableLeft_def by auto
qed
lemma stableRight_rtraclp:
assumes "stableRight Q R"
shows "stableRight Q R^**"
unfolding stableRight_def OO_def proof safe
fix s s' s'' assume "R⇧*⇧* s' s''" "Q s s'"
thus "Q s s''"
apply induct using assms unfolding stableRight_def by auto
qed
lemma stable2_rtraclp:
assumes "stable2 Q R"
shows "stable2 Q R^**"
using assms stable2_def stableLeft_rtraclp stableRight_rtraclp by blast
lemma stable_Eq[simp,intro!]:
"stable P (=)"
unfolding stable_def by blast
lemma stable_OO:
assumes "stable P R1" "stable P R2"
shows "stable P (R1 OO R2)"
using assms unfolding stable_def by blast
lemma stableLeft_Eq[simp,intro!]:
"stableLeft Q (=)"
unfolding stableLeft_def by blast
lemma stableLeft_OO:
assumes "stableLeft Q R1" "stableLeft Q R2"
shows "stableLeft Q (R1 OO R2)"
using assms unfolding stableLeft_def by blast
lemma stableRight_Eq[simp,intro!]:
"stableRight Q (=)"
unfolding stableRight_def by blast
lemma stableRight_OO:
assumes "stableRight Q R1" "stableRight Q R2"
shows "stableRight Q (R1 OO R2)"
using assms unfolding stableRight_def by blast
lemma stable2_Eq[simp,intro!]:
"stable2 Q (=)"
unfolding stable2_def by blast
lemma stable2_OO:
assumes "stable2 Q R1" "stable2 Q R2"
shows "stable2 Q (R1 OO R2)"
by (meson assms stable2_def stableLeft_OO stableRight_OO)
lemma stable_iff_imR: "stable P R ⟷ imR R P ≤ P"
unfolding stable_def imR_def by auto
lemma stable_imR_rtraclp: "stable P R ⟹ imR (R^**) P ≤ P"
by (meson stable_iff_imR stable_rtraclp)
lemma stable_lift1_lift2: "stable P R ⟹ lift1 P ∧2 R ≤ R ∧2 lift2 P"
unfolding stable_def lift1_def lift2_def conjR_def by auto
lemma stable_lift1_lift2_rtraclp: "stable P R ⟹ lift1 P ∧2 R^** ≤ R^** ∧2 lift2 P"
by (simp add: stable_lift1_lift2 stable_rtraclp)
lemma stableLeft_OO_leq: "stableLeft Q R ⟹ Q1 ≤ Q ⟹ R OO Q1 ≤ Q"
by (simp add: order_subst2 relcompp_mono stableLeft_def)
lemma stable2_OO_leqL: "stable2 Q R ⟹ Q1 ≤ Q ⟹ R OO Q1 ≤ Q"
by (simp add: stable2_def stableLeft_OO_leq)
lemma stableRight_OO_leq: "stableRight Q R ⟹ Q1 ≤ Q ⟹ Q1 OO R ≤ Q"
by (meson dual_order.trans order_refl relcompp_mono stableRight_def)
lemma stable2_OO_leqR: "stable2 Q R ⟹ Q1 ≤ Q ⟹ Q1 OO R ≤ Q"
by (simp add: stable2_def stableRight_OO_leq)
lemma stable2_imp_OO:
assumes "stable2 Q R1" "stable2 Q R2"
shows "R1 OO Q OO R2 ≤ Q"
by (meson assms stable2_OO_leqL stable2_def stableRight_def)
lemma stable2_OO_leq: "stable2 Q R1 ⟹ stable2 Q R2 ⟹
Q' ≤ Q ⟹ R1 OO Q' OO R2 ≤ Q"
by (simp add: stable2_OO_leqL stable2_OO_leqR)
lemma stableLeft_lift2[simp,intro!]: "stableLeft (lift2 P) R"
unfolding stableLeft_def lift2_def by auto
lemma stableRight_lift1[simp,intro!]: "stableRight (lift1 P) R"
unfolding stableRight_def lift1_def by auto
lemma rtranclp_least: "(=) ≤ Z ⟹ Z OO A ≤ Z ⟹ A⇧*⇧* ≤ Z"
by (metis eq_OO stableRight_OO_leq stableRight_def stableRight_rtraclp)
inductive
R_star where
refl[simp]: "R_star 0 R s s" |
stepRel: "R s s' ⟹ R_star n R s' s'' ⟹ R_star (Suc n) R s s'' "
lemma R_star0[simp]:"Ex (R_star 0 R sa)" by (meson R_star.refl)
lemma R_star_refl:"R_star 0 R s s' ⟹ s = s'" using refl by (metis R_star.simps Zero_not_Suc)
lemma R_starRR:"R_star n R s s' ⟹ R s' s'' ⟹ R_star (Suc n) R s s''"
apply(induction rule: R_star.induct)
subgoal for s by(rule stepRel, auto)
subgoal by (meson R_star.stepRel) .
lemma R_star_imp: "R_star n R s s' ⟹ R⇧*⇧* s s'"
apply(induction rule: R_star.induct)
using R_star.cases by auto
lemma R_step_star:"R⇧*⇧* s s' = (∃n. R_star n R s s')"
apply(standard)
subgoal by(induction rule: rtranclp.induct,(metis R_star.refl R_starRR)+)
using R_star_imp by metis
lemma Suc_assoc:"(Suc (x + y)) = (Suc x + y)" by auto
lemma R_star_trans:
assumes "R_star n R x y"
and "R_star m R y z"
shows "R_star (n+m) R x z"
using assms(2,1) apply-apply(induction arbitrary: n x rule: R_star.induct,simp_all)
subgoal premises p for R s s' n s'' na x unfolding Suc_assoc
apply(rule p(3)[of "Suc na" x])
using p(1,4) apply-by(drule R_starRR, assumption+) .
inductive
star :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
for r where
refl: "star r x x" |
step: "r x y ⟹ star r y z ⟹ star r x z"
hide_fact (open) refl step
lemma star_trans:
"star r x y ⟹ star r y z ⟹ star r x z"
proof(induction rule: star.induct)
case refl thus ?case .
next
case step thus ?case by (metis star.step)
qed
lemmas star_induct =
star.induct[of "r:: 'a*'b ⇒ 'a*'b ⇒ bool", split_format(complete)]
lemmas star_cases =
star.cases[of "r:: 'a*'b ⇒ 'a*'b ⇒ bool", split_format(complete)]
declare star.refl[simp,intro]
lemma star_step1[simp, intro]: "r x y ⟹ star r x y"
by(metis star.refl star.step)
definition "final r x ≡ ∀y. ¬ r x y"
lemma final_star_eq: "final r x ⟹ star r x y ⟹ x = y"
by (metis final_def star.cases)
code_pred star .
lemma add_less:"∀i'. i ≠ (x::nat) + i' ⟹ x ≠ 0 ⟹ i < x" by (metis add_diff_inverse_nat)
lemma Suc_red:"Suc x = n + Suc m' ⟷ x = n + m'" "Suc x = Suc n + m' ⟷ x = n + m'" by auto
lemma le_Suc_iff0: ‹m ≤ Suc n ⟷ m = 0 ∨ (∃m'. m = Suc m' ∧ m' ≤ n)›
by presburger
locale Step =
fixes
small_step :: "'com × 'state ⇒ 'com × 'state ⇒ bool" (infix "→" 55) and
final :: "'com × 'state ⇒ bool"
begin
abbreviation
small_steps :: "'com × 'state ⇒ 'com × 'state ⇒ bool" (infix "→*" 55)
where "x →* y == star small_step x y"
inductive step_rel where
R_Step:"R s s' ⟹ step_rel R (c, s) (c, s')"
|
S_Step:"small_step (c, s) (c', s') ⟹ step_rel R (c, s) (c', s')"
lemma step_rel_cases_cfg [consumes 1, case_names R_Step S_Step, elim]:
assumes "step_rel R (c, s) cfg'"
obtains (R_Step) s' where "cfg' = (c, s')" and "R s s'"
| (S_Step) c' s' where "cfg' = (c', s')" and "(c, s) → (c', s')"
using assms by (cases rule: step_rel.cases) auto
inductive_cases step_rel_inv_cases [elim!]: "step_rel R (c, s) (c', s')"
lemma step_rel_strengthenR:"step_rel R (c, s) (c', s') ⟹ R ≤ R' ⟹ step_rel R' (c, s) (c', s')"
apply(cases rule: step_rel.cases)
using predicate1D step_rel.simps by auto
lemma step_rel_cases: "step_rel R (c, s) (c', s') ⟹ (c = c' ⟹ R s s' ⟹ P) ⟹
((c, s) → (c', s') ⟹ P) ⟹ P"
by(cases rule: step_rel.cases[of R "(c, s)" "(c', s')"], simp_all)
definition "lift R ≡ (λ(c,s) (c',s'). c' = c ∧ R s s')"
lemma :
assumes "(lift R)⇧*⇧* (c, s) (c', s')"
shows "c = c' ∧ R⇧*⇧* s s'"
using assms
apply (induct rule: rtranclp_induct2, simp)
unfolding lift_def case_prod_beta by auto
definition "fstep_rel R ≡ rtranclp (lift R) OO small_step "
lemma rel_incl_lift_rtranclp: "R⇧*⇧* s s'' ⟹ (lift R)⇧*⇧* (c, s) (c, s'')"
apply(induct rule: rtranclp.induct)
subgoal by simp
subgoal for s s' s'' apply(subgoal_tac "(lift R) (c, s') (c, s'')")
subgoal by simp
subgoal unfolding lift_def by simp . .
lemma rtranclp_small_step_fstep_rel:
assumes R: "R⇧*⇧* s s''" and st: "(c, s'') → (c1, s1)"
shows "fstep_rel R (c, s) (c1, s1)"
proof-
have "rtranclp (lift R) (c, s) (c, s'')" using rel_incl_lift_rtranclp[OF R] .
thus ?thesis using st unfolding fstep_rel_def by blast
qed
lemma lift_fst: "lift R cfg cfg' ⟹ fst cfg' = fst cfg"
unfolding lift_def by auto
lemma rtranclp_lift_fst: "rtranclp (lift R) cfg cfg' ⟹ fst cfg' = fst cfg"
apply (induct rule: rtranclp.induct) using lift_fst by auto
end
lemma whileAssms_inject:
assumes st: "stable P R" "stable2 Q R" "stable2 Pt1 R"
and Pr1: "(evalT t) ∧1 P ≤ Pr1"
and P: "imR Pt1 ((evalT t) ∧1 Pr1) ≤ P"
and Q: "lift1 P ∧2 (lift1 (evalT t ∧1 P) ∧2 Pt1)^** ∧2 lift2 (¬1 evalT t) ≤ Q"
shows
"imR (R⇧*⇧* ∧2 lift2 (evalT t)) P ≤ Pr1"
"imR Pt1 (imR R⇧*⇧* (imR R⇧*⇧* P ∧1 evalT t) ∧1 Pr1) ≤ P"
"(lift1 P ∧2 ((((lift1 P ∧2 R⇧*⇧*) ∧2 lift2 (evalT t)) OO R⇧*⇧*) OO Pt1)⇧*⇧*) OO (R⇧*⇧* ∧2 lift2 (¬1 evalT t)) OO R⇧*⇧* ≤ Q"
proof-
have sst: "stable P R^**" "stable2 Q R^**" "stable2 Pt1 R^**"
by (simp add: st stable_rtraclp stable2_rtraclp)+
have Pt0: "lift1 P ∧2 (=) ∧2 lift2 (¬1 evalT t) ≤ Q"
using Q unfolding conjR_def lift2_def by auto
have Pt00: "lift1 P ∧2 (lift1 (evalT t ∧1 P) ∧2 Pt1) ∧2 lift2 (¬1 evalT t) ≤ Q"
using Q unfolding conjR_def lift2_def by auto
thus PPr1: "imR ((R^** ∧2 lift2 (evalT t))) P ≤ Pr1" using Pr1
using sst(1) unfolding imR_def conjR_def conjP_def lift2_def stable_def by auto
have "imR Pt1 (imR R^** (imR R^** P ∧1 (evalT t)) ∧1 Pr1) ≤ imR Pt1 ((evalT t) ∧1 Pr1)"
using sst(3) st(1) Pr1 le_boolD
unfolding imR_def conjP_def stable2_def2 stable_def conjP_def le_fun_def le_bool_def
by (smt (verit) relcomppI rtranclp_induct)
thus PPr: "imR Pt1 (imR R^** (imR R^** P ∧1 (evalT t)) ∧1 Pr1) ≤ P"
using P by auto
define A B where
A_def: "A = (lift1 P ∧2 R^**) OO (lift1 (evalT t ∧1 P) ∧2 Pt1)" and
B_def: "B = (R^** ∧2 lift2 (¬1 evalT t))"
have AA: "(((lift1 P ∧2 R^** ) ∧2 lift2 (evalT t)) OO R^** ) OO Pt1 ≤
A"
using sst(1,3)
unfolding A_def lift1_def lift2_def conjR_def conjP_def OO_def stable_def stable2_def2
by blast
hence 0: "((((lift1 P ∧2 R^**) ∧2 lift2 (evalT t)) OO R^**) OO Pt1)^** OO
((R^** ∧2 lift2 (¬1 evalT t)) OO R^**)
≤
A ^** OO ((R^** ∧2 lift2 (¬1 evalT t)) OO R^**)"
by (simp add: relcompp_mono rtranclp_mono)
have 11: "A OO B ≤ A ∧2 lift2 (¬1 evalT t)"
using sst(3) unfolding lift2_def conjR_def OO_def A_def B_def lift1_def stable2_def2
by blast
have 111: "A^** OO B = ((A^** OO A) OO B) ∨2 B"
unfolding OO_def disjR_def fun_eq_iff
by (smt (verit, ccfv_threshold) OO_def disjR_def predicate2I rtranclp.simps)
have 2: "A^** OO B ≤ (A^** OO (A ∧2 lift2 (¬1 evalT t))) ∨2 B"
unfolding 111 using 11
by (smt (verit) disjR_def predicate2D predicate2I relcompp_assoc relcompp_mono)
have "A^** OO (A ∧2 lift2 (¬1 evalT t)) ≤ A^** ∧2 lift2 (¬1 evalT t)"
unfolding OO_def lift2_def conjR_def by auto
hence AB: "A^** OO B ≤ (A^** ∧2 lift2 (¬1 evalT t)) ∨2 B"
by (smt (z3) "11" "111" disjR_def predicate2D predicate2I relcompp_assoc relcompp_mono)
have B: "lift1 P ∧2 B ≤ Q" unfolding B_def
using Pt0 unfolding lift2_def conjR_def
using sst(2) unfolding stable2_def2
by (smt (z3) Prelim.stable_def le_fun_def predicate2I lift1_def relcomppI rev_predicate1D sst(1))
define Z where "Z ≡ R^** OO (lift1 (evalT t ∧1 P) ∧2 Pt1)⇧*⇧*"
have Z1: "(=) ≤ Z" unfolding Z_def by auto
have OO_A_lq: "(lift1 (evalT t ∧1 P) ∧2 Pt1) OO A ≤ (lift1 (evalT t ∧1 P) ∧2 Pt1)⇧*⇧*"
unfolding A_def lift1_def conjR_def conjP_def OO_def
by auto (smt (verit, del_insts) converse_rtranclp_into_rtranclp le_fun_def
predicate1D r_into_rtranclp relcomppI sst(3) stable2_def2)
have Z2: "Z OO A ≤ Z"
unfolding Z_def apply(rule OO_rtranclp_le)
subgoal unfolding A_def lift1_def conjR_def conjP_def OO_def
using rtranclp_trans by fastforce
subgoal using OO_A_lq predicate2D by fastforce .
have "A^** ≤ Z" using Z1 Z2 rtranclp_least by blast
moreover have "lift1 P ∧2 Z ∧2 lift2 (¬1 evalT t) ≤ Q" using Q unfolding Z_def
using sst(1,2) unfolding lift1_def lift2_def conjR_def stable_def stable2_def2
by blast
ultimately have C: "lift1 P ∧2 A^** ∧2 lift2 (¬1 evalT t) ≤ Q"
by (smt (verit, del_insts) conjR_def predicate2D predicate2I)
have aux: "(lift1 P ∧2 A^**) OO B = lift1 P ∧2 (A^** OO B)"
by (metis (no_types, opaque_lifting) conjR_lift2_rel_1_OO eq_OO relcompp_assoc)
have "(lift1 P ∧2 A^**) OO B ≤ Q" unfolding aux using B C AB
by (smt (verit, ccfv_threshold) conjR_def disjR_def le_fun_def order_refl)
hence 00: "(lift1 P ∧2 A^**) OO (B OO R^**) ≤ Q"
using sst(2) stable2_OO_leqR by fastforce
thus PPt: "(lift1 P ∧2 ((((lift1 P ∧2 R^**) ∧2 lift2 (evalT t)) OO R^**) OO Pt1)^**) OO
((R^** ∧2 lift2 (¬1 evalT t)) OO R^**) ≤ Q"
using 0 AA unfolding A_def B_def using conjR_def predicate2I relcompp_mono rev_predicate2D rtranclp_mono
by (smt (z3))
qed
inductive terminFrom for R where
"(⋀cfg'. R cfg cfg' ⟹ terminFrom R cfg') ⟹ terminFrom R cfg"
lemma terminFrom_induct_split [consumes 1, case_names Step]:
assumes "terminFrom R (c, s)"
assumes "⋀c s. (⋀c' s'. R (c, s) (c', s') ⟹ terminFrom R (c', s') ∧ P c' s') ⟹ P c s"
shows "P c s"
using assms(1)
proof (induct cfg ≡ "(c,s)" arbitrary: c s rule: terminFrom.induct)
case (1 c_inner s_inner)
then show ?case
using assms(2) by blast
qed
context Step
begin
lemma terminFrom_env_step:
assumes "terminFrom (fstep_rel R) (c, s)"
assumes "R^** s s'"
shows "terminFrom (fstep_rel R) (c, s')"
proof (rule terminFrom.intros)
fix cfg'
assume "fstep_rel R (c, s') cfg'"
then obtain u where "(lift R)⇧*⇧* (c, s') u" and "small_step u cfg'"
unfolding fstep_rel_def OO_def by auto
have "(lift R)⇧*⇧* (c, s) (c, s')"
using ‹R⇧*⇧* s s'› by (simp add: rel_incl_lift_rtranclp)
then have "(lift R)⇧*⇧* (c, s) u"
using ‹(lift R)⇧*⇧* (c, s') u› by (metis rtranclp_trans)
then have "fstep_rel R (c, s) cfg'"
unfolding fstep_rel_def OO_def using ‹small_step u cfg'› by blast
then show "terminFrom (fstep_rel R) cfg'"
using assms(1) by (meson terminFrom.cases)
qed
lemma step_rel_refl:
assumes "R s s"
shows "step_rel R (c, s) (c, s)"
using step_rel.R_Step assms by blast
lemma lift_step_rel:
assumes "lift R x y"
shows "step_rel R x y"
proof -
obtain c s where "x = (c,s)" by (cases x)
obtain c' s' where "y = (c',s')" by (cases y)
from assms have "c' = c ∧ R s s'" unfolding lift_def ‹x = (c,s)› ‹y = (c',s')› by auto
then show ?thesis using ‹x = (c,s)› ‹y = (c',s')› step_rel.R_Step by auto
qed
lemma step_rel_not_small_lift:
assumes "step_rel R x y" and "¬ small_step x y"
shows "lift R x y"
using assms proof (cases rule: step_rel.cases)
case (R_Step s s' c)
then show ?thesis unfolding lift_def by auto
next
case (S_Step c s c' s')
with ‹¬ small_step x y› show ?thesis by auto
qed
lemma fstep_has_fseq:
assumes "fstep_rel R x y"
shows "∃N f. f 0 = x ∧ f N = y ∧ N > 0 ∧
(∀i<N. step_rel R (f i) (f (Suc i))) ∧
(small_step (f (N - 1)) (f N))"
proof -
from assms obtain u where 1: "(lift R)⇧*⇧* x u" and 2: "small_step u y"
unfolding fstep_rel_def OO_def by auto
from 1 obtain n1 as1 where as1: "as1 0 = x" "as1 n1 = u" "∀i<n1. lift R (as1 i) (as1 (Suc i))"
using rtranclp_chain by metis
define N where "N = Suc n1"
define f where "f = (λk. if k ≤ n1 then as1 k else y)"
have f_0: "f 0 = x" using as1 f_def by simp
have f_N: "f N = y" using f_def N_def by simp
have N_pos: "N > 0" by (simp add: N_def)
have step_all: "∀i<N. step_rel R (f i) (f (Suc i))"
proof (intro allI impI)
fix i assume "i < N"
show "step_rel R (f i) (f (Suc i))"
proof (cases "i < n1")
case True
then have "f i = as1 i" and "f (Suc i) = as1 (Suc i)" unfolding f_def by auto
then show ?thesis using as1 True lift_step_rel by auto
next
case False
then have "i = n1" using ‹i < N› N_def by auto
then have "f i = u" and "f (Suc i) = y" using as1 f_def N_def by auto
then show ?thesis using 2 step_rel.S_Step by (metis old.prod.exhaust)
qed
qed
have small: "small_step (f (N - 1)) (f N)"
using 2 unfolding N_def f_def by (simp add: as1(2))
show ?thesis using f_0 f_N N_pos step_all small by blast
qed
fun ch_step :: "(nat ⇒ nat) ⇒ nat ⇒ nat × nat" where
"ch_step N 0 = (0,0)"
| "ch_step N (Suc k) =
(let (i,j) = ch_step N k in
if Suc j < N i then (i, Suc j)
else (Suc i, 0))"
fun start_idx :: "(nat ⇒ nat) ⇒ nat ⇒ nat" where
"start_idx N 0 = 0" |
"start_idx N (Suc i) = start_idx N i + N i"
fun forwardSS :: "(nat ⇒ nat) ⇒ nat ⇒ nat" where
"forwardSS next_ss 0 = 0" |
"forwardSS next_ss (Suc n) = Suc (next_ss (forwardSS next_ss n))"
lemma fstep_rel_iff_fair_step_rel:
"(∃ch. ch 0 = cfg ∧ (∀i. fstep_rel R (ch i) (ch (Suc i))))
⟷
(∃ch'. ch' 0 = cfg ∧ (∀i. step_rel R (ch' i) (ch' (Suc i))) ∧ (∀i. ∃j ≥ i. small_step (ch' j) (ch' (Suc j))))"
proof
assume "∃ch. ch 0 = cfg ∧ (∀i. fstep_rel R (ch i) (ch (Suc i)))"
then obtain ch where ch_0: "ch 0 = cfg" and ch_fstep: "∀i. fstep_rel R (ch i) (ch (Suc i))" by blast
define Prop where "Prop = (λi N f. f 0 = ch i ∧ f N = ch (Suc i) ∧ N > 0
∧ (∀k < N - 1. step_rel R (f k) (f (Suc k))) ∧ small_step (f (N - 1)) (f N))"
have "∀i. ∃N f. Prop i N f" unfolding Prop_def using ch_fstep fstep_has_fseq
by (smt (verit, del_insts) diff_right_commute not_gr_zero zero_diff zero_less_diff)
then have "∀i. ∃f. Prop i (SOME N. ∃f. Prop i N f) f" by (metis (full_types))
then have ex_f: "∀i. Prop i (SOME N. ∃f. Prop i N f) (SOME f. Prop i (SOME N. ∃f. Prop i N f) f)" by (metis someI_ex)
define N where "N = (λi. SOME N. ∃f. Prop i N f)"
define f_seq where "f_seq = (λi. SOME f. Prop i (N i) f)"
have N_f_prop: "Prop i (N i) (f_seq i)" for i using ex_f unfolding N_def f_seq_def by blast
let ?ch_step = "ch_step N"
define ch' where "ch' = (λk. let (i, j) = ?ch_step k in f_seq i j)"
have ch_step_snd_bound: "snd (?ch_step k) < N (fst (?ch_step k))" for k
proof (induct k)
case 0 then show ?case using N_f_prop[of 0] unfolding Prop_def by simp
next
case (Suc k)
obtain i j where eq: "?ch_step k = (i, j)" by (cases "?ch_step k", auto)
show ?case
proof (cases "Suc j < N i")
case True then show ?thesis using eq by (simp add: Let_def split_beta)
next
case False then show ?thesis using eq N_f_prop[of "Suc i"] unfolding Prop_def by (simp add: Let_def split_beta)
qed
qed
have ch'_step_rel: "step_rel R (ch' k) (ch' (Suc k))" for k
proof -
obtain i j where eq: "?ch_step k = (i, j)" by (cases "?ch_step k", auto)
have j_less: "j < N i" using ch_step_snd_bound[of k] eq by simp
show ?thesis
proof (cases "Suc j < N i")
case True
then show ?thesis unfolding ch'_def using eq N_f_prop[of i] j_less unfolding Prop_def by (auto simp add: Let_def split_beta)
next
case False
with j_less have j:"Suc j = N i" by simp
have "ch' (Suc k) = f_seq (Suc i) 0" unfolding ch'_def using eq False by (simp add: Let_def split_beta)
also have "... = ch (Suc i)" using N_f_prop[of "Suc i"] unfolding Prop_def by simp
also have "... = f_seq i (N i)" using N_f_prop[of i] unfolding Prop_def by simp
also have "... = f_seq i (Suc j)" using ‹Suc j = N i› by simp
finally have "ch' (Suc k) = f_seq i (Suc j)" .
moreover have "ch' k = f_seq i j" unfolding ch'_def using eq by (simp add: Let_def split_beta)
have small: "small_step (f_seq i (N i - 1)) (f_seq i (N i))"
using N_f_prop[of i] unfolding Prop_def by blast
have ch_k: "ch' k = f_seq i (N i - 1)"
using ‹ch' k = f_seq i j› j by (metis diff_Suc_1)
have ch_suc_k: "ch' (Suc k) = f_seq i (N i)"
using ‹ch' (Suc k) = f_seq i (Suc j)› j by simp
show ?thesis
unfolding ch_k ch_suc_k
using step_rel.S_Step small
by (metis surj_pair)
qed
qed
let ?start_idx = "start_idx N"
have ch_step_start: "j < N i ⟹ ?ch_step (?start_idx i + j) = (i, j)" for i j
proof (induct i arbitrary: j)
case 0
show ?case using 0
proof (induct j)
case 0 then show ?case by simp
next
case (Suc j)
have "j < N 0" using Suc.prems by simp
then have "?ch_step j = (0, j)" using Suc.hyps by auto
then show ?case using Suc.prems by (simp add: Let_def split_beta)
qed
next
case (Suc i)
have Ni_pos: "N i > 0" using N_f_prop[of i] unfolding Prop_def by blast
have "N i - 1 < N i" using Ni_pos by simp
then have prev: "?ch_step (?start_idx i + (N i - 1)) = (i, N i - 1)"
using Suc.hyps by blast
have "?start_idx (Suc i) = Suc (?start_idx i + (N i - 1))"
using Ni_pos by simp
then have "?ch_step (?start_idx (Suc i)) = ?ch_step (Suc (?start_idx i + (N i - 1)))"
by simp
also have "... = (let (i', j') = ?ch_step (?start_idx i + (N i - 1)) in if Suc j' < N i' then (i', Suc j') else (Suc i', 0))"
by simp
also have "... = (Suc i, 0)"
unfolding prev Let_def split_beta using Ni_pos by simp
finally have base: "?ch_step (?start_idx (Suc i)) = (Suc i, 0)" .
show ?case using ‹j < N (Suc i)›
proof (induct j)
case 0 then show ?case using base by simp
next
case (Suc j)
have "j < N (Suc i)" using Suc.prems by simp
then have "?ch_step (?start_idx (Suc i) + j) = (Suc i, j)" using Suc.hyps by blast
then show ?case using Suc.prems by (simp add: Let_def split_beta)
qed
qed
have k_eq: "k = ?start_idx (fst (?ch_step k)) + snd (?ch_step k)" for k
proof (induct k)
case 0 show ?case by simp
next
case (Suc k)
obtain i j where eq: "?ch_step k = (i, j)" by (cases "?ch_step k", auto)
show ?case using Suc.hyps eq N_f_prop[of i] ch_step_snd_bound[of k] unfolding Prop_def
by (cases "Suc j < N i") (auto simp add: Let_def split_beta)
qed
have ch'_fair: "∀k. ∃k'≥k. small_step (ch' k') (ch' (Suc k'))"
proof (intro allI)
fix k
obtain i j where eq: "?ch_step k = (i, j)" by (cases "?ch_step k", auto)
have j_less: "j < N i" using ch_step_snd_bound[of k] eq by simp
obtain ss where ss_less: "ss < N i" and ss_step: "small_step (f_seq i ss) (f_seq i (Suc ss))"
using N_f_prop[of i] unfolding Prop_def by (metis Suc_diff_1 diff_less less_one)
show "∃k'≥k. small_step (ch' k') (ch' (Suc k'))"
proof (cases "ss ≥ j")
case True
define k' where "k' = ?start_idx i + ss"
have "k' ≥ k" using k_eq[of k] eq True k'_def by simp
have ch_step_k': "?ch_step k' = (i, ss)" using ch_step_start ss_less k'_def by simp
have "ch' k' = f_seq i ss" unfolding ch'_def ch_step_k' by (simp add: Let_def split_beta)
moreover have "ch' (Suc k') = f_seq i (Suc ss)"
proof (cases "Suc ss < N i")
case True then show ?thesis unfolding ch'_def using ch_step_k' by (simp add: Let_def split_beta)
next
case False
with ss_less have "Suc ss = N i" by simp
then show ?thesis unfolding ch'_def using ch_step_k' N_f_prop[of i] N_f_prop[of "Suc i"] unfolding Prop_def by (auto simp add: Let_def split_beta)
qed
ultimately show ?thesis using ss_step ‹k' ≥ k› by auto
next
case False
obtain ss_n where ss_n_less: "ss_n < N (Suc i)" and ss_n_step: "small_step (f_seq (Suc i) ss_n) (f_seq (Suc i) (Suc ss_n))"
using N_f_prop[of "Suc i"] unfolding Prop_def by (metis Suc_pred' diff_less less_one)
define k' where "k' = ?start_idx (Suc i) + ss_n"
have "k' ≥ k" using k_eq[of k] eq j_less k'_def by simp
have ch_step_k': "?ch_step k' = (Suc i, ss_n)" using ch_step_start ss_n_less k'_def by blast
have "ch' k' = f_seq (Suc i) ss_n" unfolding ch'_def ch_step_k' by (simp add: Let_def split_beta)
moreover have "ch' (Suc k') = f_seq (Suc i) (Suc ss_n)"
proof (cases "Suc ss_n < N (Suc i)")
case True then show ?thesis unfolding ch'_def using ch_step_k' by (simp add: Let_def split_beta)
next
case False
with ss_n_less have "Suc ss_n = N (Suc i)" by simp
then show ?thesis unfolding ch'_def using ch_step_k' N_f_prop[of "Suc i"] N_f_prop[of "Suc (Suc i)"] unfolding Prop_def by (auto simp add: Let_def split_beta)
qed
ultimately show ?thesis using ss_n_step ‹k' ≥ k› by auto
qed
qed
have "ch' 0 = cfg" unfolding ch'_def using N_f_prop[of 0] ch_0 unfolding Prop_def by (simp add: Let_def split_beta)
then show "∃ch'. ch' 0 = cfg ∧ (∀i. step_rel R (ch' i) (ch' (Suc i))) ∧ (∀i. ∃j≥i. small_step (ch' j) (ch' (Suc j)))"
using ch'_step_rel ch'_fair by blast
next
assume "∃ch'. ch' 0 = cfg ∧ (∀i. step_rel R (ch' i) (ch' (Suc i))) ∧ (∀i. ∃j≥i. small_step (ch' j) (ch' (Suc j)))"
then obtain ch' where ch'_0: "ch' 0 = cfg" and ch'_step: "∀i. step_rel R (ch' i) (ch' (Suc i))" and ch'_fair: "∀i. ∃j≥i. small_step (ch' j) (ch' (Suc j))" by blast
define next_ss where "next_ss = (λi. LEAST j. j ≥ i ∧ small_step (ch' j) (ch' (Suc j)))"
have next_ss_prop: "next_ss i ≥ i ∧ small_step (ch' (next_ss i)) (ch' (Suc (next_ss i)))" for i
unfolding next_ss_def using LeastI_ex[OF ch'_fair[rule_format, of i]] .
have next_ss_least: "k ≥ i ⟹ k < next_ss i ⟹ ¬ small_step (ch' k) (ch' (Suc k))" for i k
unfolding next_ss_def by (metis (mono_tags, lifting) Least_le not_le)
let ?f = "forwardSS next_ss"
define ch where "ch = (λn. ch' (?f n))"
have "fstep_rel R (ch n) (ch (Suc n))" for n
proof -
have "(lift R)⇧*⇧* (ch' (?f n)) (ch' (next_ss (?f n)))"
proof (rule chain_rtranclp[of "λk. ch' (?f n + k)" _ "next_ss (?f n) - ?f n"])
show "ch' (?f n + 0) = ch' (?f n)" by simp
show "ch' (?f n + (next_ss (?f n) - ?f n)) = ch' (next_ss (?f n))" using next_ss_prop[of "?f n"] by simp
have f_Suc_eq:"⋀i. ?f n + Suc i = Suc (?f n + i)" by simp
show "∀i<next_ss (?f n) - ?f n. lift R (ch' (?f n + i)) (ch' (?f n + (Suc i)))"
proof (unfold f_Suc_eq, intro allI impI)
fix i assume "i < next_ss (?f n) - ?f n"
let ?k = "?f n + i"
have "?k ≥ ?f n" and "?k < next_ss (?f n)" using ‹i < next_ss (?f n) - ?f n› by auto
then have "¬ small_step (ch' ?k) (ch' (Suc ?k))" using next_ss_least[of "?f n" ?k] by simp
then show "lift R (ch' ?k) (ch' (Suc ?k))" using step_rel_not_small_lift ch'_step by blast
qed
qed
moreover have "small_step (ch' (next_ss (?f n))) (ch' (Suc (next_ss (?f n))))" using next_ss_prop by blast
moreover have "(lift R)⇧*⇧* (ch' (Suc (next_ss (?f n)))) (ch' (Suc (next_ss (?f n))))" by simp
ultimately show ?thesis unfolding fstep_rel_def OO_def ch_def by fastforce
qed
then show "∃ch. ch 0 = cfg ∧ (∀i. fstep_rel R (ch i) (ch (Suc i)))" using ch'_0 ch_def by (metis Step.forwardSS.simps(1))
qed
end
definition "stableWithDescent R P ord ≡ ∀n s s'. P n s ∧ R s s' ⟶ (∃m. (m,n) ∈ ord ∧ P m s')"
lemma rtranclp_Id: "(=)^** = (=)"
by (metis conversep_eq eq_OO leq_conversepI order_antisym_conv reflclp_tranclp rtranclp_least sup.coboundedI2)
end