Read about our upcoming Code of Conduct on this issue

Commit 94be6d8e authored by desharna's avatar desharna
Browse files

refactored and added lemma state_behaves_forward_to_backward

parent 1335f4299090
......@@ -47,18 +47,18 @@ subsection \<open>Preservation of behaviour\<close>
corollary behaviour_preservation:
assumes
compiles: "compile p1 = Some p2" and
behaves: "L2.behaves p2 b2" and
behaves: "L2.prog_behaves p2 b2" and
not_wrong: "\<not> is_wrong b2"
shows "\<exists>b1 i. L1.behaves p1 b1 \<and> rel_behaviour (match i) b1 b2"
shows "\<exists>b1 i. L1.prog_behaves p1 b1 \<and> rel_behaviour (match i) b1 b2"
proof -
obtain s2 where "load2 p2 s2" and "L2.sem_behaves s2 b2"
using behaves L2.behaves_def by auto
obtain s2 where "load2 p2 s2" and "L2.state_behaves s2 b2"
using behaves L2.prog_behaves_def by auto
obtain i s1 where "load1 p1 s1" "match i s1 s2"
using compile_load[OF compiles \<open>load2 p2 s2\<close>]
by auto
then show ?thesis
using simulation_behaviour[OF \<open>L2.sem_behaves s2 b2\<close> not_wrong \<open>match i s1 s2\<close>]
by (auto simp: L1.behaves_def)
using simulation_behaviour[OF \<open>L2.state_behaves s2 b2\<close> not_wrong \<open>match i s1 s2\<close>]
by (auto simp: L1.prog_behaves_def)
qed
end
......
......@@ -38,22 +38,21 @@ proof (coinduction arbitrary: x n rule: inf.coinduct)
qed
lemma step_inf:
assumes
deterministic: "\<And>x y z. r x y \<Longrightarrow> r x z \<Longrightarrow> y = z"
assumes "right_unique r"
shows "r x y \<Longrightarrow> inf r x \<Longrightarrow> inf r y"
by (metis deterministic inf.cases)
using right_uniqueD[OF \<open>right_unique r\<close>]
by (metis inf.cases)
lemma star_inf:
assumes
deterministic: "\<And>x y z. r x y \<Longrightarrow> r x z \<Longrightarrow> y = z"
assumes "right_unique r"
shows "r\<^sup>*\<^sup>* x y \<Longrightarrow> inf r x \<Longrightarrow> inf r y"
proof (induction y rule: rtranclp_induct)
case base
then show ?case .
then show ?case by assumption
next
case (step y z)
then show ?case
using step_inf deterministic by metis
using step_inf[OF \<open>right_unique r\<close>] by metis
qed
end
\ No newline at end of file
......@@ -20,28 +20,21 @@ The set of initial states of the transition system is implicitly defined by the
\<close>
subsection \<open>Behaviour of a dynamic execution\<close>
subsection \<open>Program behaviour\<close>
definition behaves :: "'prog \<Rightarrow> 'state behaviour \<Rightarrow> bool" (infix "\<Down>" 50) where
"behaves = load OO sem_behaves"
definition prog_behaves :: "'prog \<Rightarrow> 'state behaviour \<Rightarrow> bool" (infix "\<Down>" 50) where
"prog_behaves = load OO state_behaves"
text \<open>If both the @{term load} and @{term step} relations are deterministic, then so is the behaviour of a program.\<close>
lemma behaves_deterministic:
lemma right_unique_prog_behaves:
assumes
load_deterministic: "\<And>p s s'. load p s \<Longrightarrow> load p s' \<Longrightarrow> s = s'" and
step_deterministic: "\<And>x y z. step x y \<Longrightarrow> step x z \<Longrightarrow> y = z" and
behaves: "p \<Down> b" "p \<Down> b'"
shows "b = b'"
proof -
obtain s where "load p s" and "s \<down> b" and "s \<down> b'"
using behaves load_deterministic
by (auto simp: behaves_def)
thus ?thesis
using step_deterministic sem_behaves_deterministic[OF _ \<open>s \<down> b\<close> \<open>s \<down> b'\<close>]
by simp
qed
right_unique_load: "right_unique load" and
right_unique_step: "right_unique step"
shows "right_unique prog_behaves"
unfolding prog_behaves_def
using right_unique_state_behaves[OF right_unique_step] right_unique_load
by (auto intro: right_unique_OO)
end
......
section \<open>The Dynamic Representation of a Language\<close>
theory Semantics
imports Main Behaviour Inf begin
imports Main Behaviour Inf Transfer_Extras begin
text \<open>
The definition of programming languages is separated into two parts: an abstract semantics and a concrete program representation.
......@@ -49,25 +49,27 @@ notation
inf_step ("'(\<rightarrow>\<^sup>\<infinity>')" [] 50) and
inf_step ("_ \<rightarrow>\<^sup>\<infinity>" [55] 50)
lemma finished_inf: "s \<rightarrow>\<^sup>\<infinity> \<Longrightarrow> \<not> finished step s"
lemma inf_not_finished: "s \<rightarrow>\<^sup>\<infinity> \<Longrightarrow> \<not> finished step s"
using inf.cases finished_step by metis
lemma eval_deterministic:
assumes
deterministic: "\<And>x y z. step x y \<Longrightarrow> step x z \<Longrightarrow> y = z"
shows "s1 \<rightarrow>\<^sup>* s2 \<Longrightarrow> s1 \<rightarrow>\<^sup>* s3 \<Longrightarrow> finished step s2 \<Longrightarrow> finished step s3 \<Longrightarrow> s2 = s3"
proof(induction s1 arbitrary: s3 rule: converse_rtranclp_induct)
case base
then show ?case by (simp add: finished_star)
next
case (step y z)
then show ?case
by (metis converse_rtranclpE deterministic finished_step)
deterministic: "\<And>x y z. step x y \<Longrightarrow> step x z \<Longrightarrow> y = z" and
"s1 \<rightarrow>\<^sup>* s2" and "s1 \<rightarrow>\<^sup>* s3" and "finished step s2" and "finished step s3"
shows "s2 = s3"
proof -
have "right_unique step"
using deterministic by (auto intro: right_uniqueI)
with assms show ?thesis
by (auto simp: finished_def intro: rtranclp_complete_run_right_unique)
qed
lemma step_converges_or_diverges: "(\<exists>s'. s \<rightarrow>\<^sup>* s' \<and> finished step s') \<or> s \<rightarrow>\<^sup>\<infinity>"
by (smt (verit, del_insts) finished_def inf.coinduct rtranclp.intros(2) rtranclp.rtrancl_refl)
subsection \<open>Behaviour of a dynamic execution\<close>
inductive sem_behaves :: "'state \<Rightarrow> 'state behaviour \<Rightarrow> bool" (infix "\<down>" 50) where
inductive state_behaves :: "'state \<Rightarrow> 'state behaviour \<Rightarrow> bool" (infix "\<down>" 50) where
state_terminates:
"s1 \<rightarrow>\<^sup>* s2 \<Longrightarrow> finished step s2 \<Longrightarrow> final s2 \<Longrightarrow> s1 \<down> (Terminates s2)" |
state_diverges:
......@@ -80,59 +82,61 @@ text \<open>
Even though the @{term step} transition relation in the @{locale semantics} locale need not be deterministic, if it happens to be, then the behaviour of a program becomes deterministic too.
\<close>
lemma sem_behaves_deterministic:
lemma right_unique_state_behaves:
assumes
deterministic: "\<And>x y z. step x y \<Longrightarrow> step x z \<Longrightarrow> y = z"
shows "s \<down> b1 \<Longrightarrow> s \<down> b2 \<Longrightarrow> b1 = b2"
proof (induction s b1 rule: sem_behaves.induct)
case (state_terminates s1 s2)
show ?case using state_terminates.prems state_terminates.hyps
proof (induction s1 b2 rule: sem_behaves.induct)
case (state_terminates s1 s3)
then show ?case
using eval_deterministic deterministic by simp
next
case (state_diverges s1)
then show ?case
using deterministic star_inf[THEN finished_inf] by simp
next
case (state_goes_wrong s1 s3)
then show ?case
using eval_deterministic deterministic by blast
qed
next
case (state_diverges s1)
show ?case using state_diverges.prems state_diverges.hyps
proof (induction s1 b2 rule: sem_behaves.induct)
case (state_terminates s1 s2)
then show ?case
using deterministic star_inf[THEN finished_inf] by simp
next
case (state_diverges s1)
then show ?case by simp
next
case (state_goes_wrong s1 s2)
then show ?case
using deterministic star_inf[THEN finished_inf] by simp
qed
next
case (state_goes_wrong s1 s2)
show ?case using state_goes_wrong.prems state_goes_wrong.hyps
proof (induction s1 b2 rule: sem_behaves.induct)
case (state_terminates s1 s3)
then show ?case
using eval_deterministic deterministic by blast
next
case (state_diverges s1)
then show ?case
using deterministic star_inf[THEN finished_inf] by simp
"right_unique (\<rightarrow>)"
shows "right_unique (\<down>)"
proof (rule right_uniqueI)
fix s b1 b2
assume "s \<down> b1" "s \<down> b2"
thus "b1 = b2"
by (auto simp: finished_def simp del: not_ex
elim!: state_behaves.cases
dest: rtranclp_complete_run_right_unique[OF \<open>right_unique (\<rightarrow>)\<close>, of s]
dest: final_finished star_inf[OF \<open>right_unique (\<rightarrow>)\<close>, THEN inf_not_finished])
qed
lemma left_total_state_behaves: "left_total (\<down>)"
proof (rule left_totalI)
fix s
show "\<exists>b. s \<down> b"
using step_converges_or_diverges[of s]
proof (elim disjE exE conjE)
fix s'
assume "s \<rightarrow>\<^sup>* s'" and "finished (\<rightarrow>) s'"
thus "\<exists>b. s \<down> b"
by (cases "final s'") (auto intro: state_terminates state_goes_wrong)
next
case (state_goes_wrong s1 s3)
then show ?case
using eval_deterministic deterministic by simp
assume "s \<rightarrow>\<^sup>\<infinity>"
thus "\<exists>b. s \<down> b"
by (auto intro: state_diverges)
qed
qed
subsection \<open>Safe states\<close>
definition safe where
"safe s \<longleftrightarrow> (\<forall>s'. step\<^sup>*\<^sup>* s s' \<longrightarrow> final s' \<or> (\<exists>s''. step s' s''))"
lemma final_safeI: "final s \<Longrightarrow> safe s"
by (metis final_finished finished_star safe_def)
lemma step_safe: "step s s' \<Longrightarrow> safe s \<Longrightarrow> safe s'"
by (simp add: converse_rtranclp_into_rtranclp safe_def)
lemma steps_safe: "step\<^sup>*\<^sup>* s s' \<Longrightarrow> safe s \<Longrightarrow> safe s'"
by (meson rtranclp_trans safe_def)
lemma safe_state_behaves_not_wrong:
assumes "safe s" and "s \<down> b"
shows "\<not> is_wrong b"
using \<open>s \<down> b\<close>
proof (cases rule: state_behaves.cases)
case (state_goes_wrong s2)
then show ?thesis
using \<open>safe s\<close> by (auto simp: safe_def finished_def)
qed simp_all
end
end
\ No newline at end of file
......@@ -4,6 +4,8 @@ theory Simulation
imports Semantics Inf Well_founded
begin
subsection \<open>Backward simulation\<close>
locale backward_simulation =
L1: semantics step1 final1 +
L2: semantics step2 final2 +
......@@ -32,41 +34,6 @@ The only two assumptions of a backward simulation are that a final state in L2 w
Stuttering is ruled out by the requirement that the index on the @{term match} predicate decreases with respect to the well-founded @{term order} ordering.
\<close>
end
locale forward_simulation =
L1: semantics step1 final1 +
L2: semantics step2 final2 +
well_founded "(\<sqsubset>)"
for
step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
final1 :: "'state1 \<Rightarrow> bool" and
final2 :: "'state2 \<Rightarrow> bool" and
order :: "'index \<Rightarrow> 'index \<Rightarrow> bool" (infix "\<sqsubset>" 70) +
fixes
match :: "'index \<Rightarrow> 'state1 \<Rightarrow> 'state2 \<Rightarrow> bool"
assumes
match_final:
"match i s1 s2 \<Longrightarrow> final1 s1 \<Longrightarrow> final2 s2" and
simulation:
"match i1 s1 s2 \<Longrightarrow> step1 s1 s1' \<Longrightarrow>
(\<exists>i' s2'. step2\<^sup>+\<^sup>+ s2 s2' \<and> match i' s1' s2') \<or> (\<exists>i'. match i' s1 s2' \<and> i' \<sqsubset> i1)"
locale bisimulation =
forward_simulation step1 step2 final1 final2 order match +
backward_simulation step1 step2 final1 final2 order match
for
step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
final1 :: "'state1 \<Rightarrow> bool" and
final2 :: "'state2 \<Rightarrow> bool" and
order :: "'index \<Rightarrow> 'index \<Rightarrow> bool" and
match :: "'index \<Rightarrow> 'state1 \<Rightarrow> 'state2 \<Rightarrow> bool"
context backward_simulation begin
lemma lift_simulation_plus:
"step2\<^sup>+\<^sup>+ s2 s2' \<Longrightarrow> match i1 s1 s2 \<Longrightarrow>
(\<exists>i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \<and> match i2 s1' s2') \<or>
......@@ -122,7 +89,7 @@ next
qed
qed
lemma backward_simulation_inf:
lemma match_inf:
assumes
"match i s1 s2" and
"inf step2 s2"
......@@ -140,7 +107,7 @@ proof -
by (auto intro: inf_wf_to_inf well_founded_axioms)
qed
subsection \<open>Preservation of behaviour\<close>
subsubsection \<open>Preservation of behaviour\<close>
text \<open>
The main correctness theorem states that, for any two matching programs, any not wrong behaviour of the later is also a behaviour of the former.
......@@ -148,15 +115,15 @@ In other words, if the compiled program does not crash, then its behaviour, whet
\<close>
lemma simulation_behaviour :
"L2.sem_behaves s\<^sub>2 b\<^sub>2 \<Longrightarrow> \<not>is_wrong b\<^sub>2 \<Longrightarrow> match i s\<^sub>1 s\<^sub>2 \<Longrightarrow>
\<exists>b\<^sub>1 i'. L1.sem_behaves s\<^sub>1 b\<^sub>1 \<and> rel_behaviour (match i') b\<^sub>1 b\<^sub>2"
proof(induction rule: L2.sem_behaves.cases)
"L2.state_behaves s\<^sub>2 b\<^sub>2 \<Longrightarrow> \<not>is_wrong b\<^sub>2 \<Longrightarrow> match i s\<^sub>1 s\<^sub>2 \<Longrightarrow>
\<exists>b\<^sub>1 i'. L1.state_behaves s\<^sub>1 b\<^sub>1 \<and> rel_behaviour (match i') b\<^sub>1 b\<^sub>2"
proof(induction rule: L2.state_behaves.cases)
case (state_terminates s2 s2')
then obtain i' s1' where "L1.eval s\<^sub>1 s1'" and "match i' s1' s2'"
using lift_simulation_eval by blast
hence "final1 s1'"
by (auto intro: state_terminates.hyps match_final)
hence "L1.sem_behaves s\<^sub>1 (Terminates s1')"
hence "L1.state_behaves s\<^sub>1 (Terminates s1')"
using L1.final_finished
by (simp add: L1.state_terminates \<open>L1.eval s\<^sub>1 s1'\<close>)
moreover have "rel_behaviour (match i') (Terminates s1') b\<^sub>2"
......@@ -165,7 +132,7 @@ proof(induction rule: L2.sem_behaves.cases)
next
case (state_diverges s2)
then show ?case
using backward_simulation_inf L1.state_diverges by fastforce
using match_inf L1.state_diverges by fastforce
next
case (state_goes_wrong s2 s2')
then show ?case using \<open>\<not>is_wrong b\<^sub>2\<close> by simp
......@@ -173,6 +140,136 @@ qed
end
subsection \<open>Forward simulation\<close>
locale forward_simulation =
L1: semantics step1 final1 +
L2: semantics step2 final2 +
well_founded "(\<sqsubset>)"
for
step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
final1 :: "'state1 \<Rightarrow> bool" and
final2 :: "'state2 \<Rightarrow> bool" and
order :: "'index \<Rightarrow> 'index \<Rightarrow> bool" (infix "\<sqsubset>" 70) +
fixes
match :: "'index \<Rightarrow> 'state1 \<Rightarrow> 'state2 \<Rightarrow> bool"
assumes
match_final:
"match i s1 s2 \<Longrightarrow> final1 s1 \<Longrightarrow> final2 s2" and
simulation:
"match i s1 s2 \<Longrightarrow> step1 s1 s1' \<Longrightarrow>
(\<exists>i' s2'. step2\<^sup>+\<^sup>+ s2 s2' \<and> match i' s1' s2') \<or> (\<exists>i'. match i' s1' s2 \<and> i' \<sqsubset> i)"
begin
lemma lift_simulation_eval:
"L1.eval s1 s1' \<Longrightarrow> match i s1 s2 \<Longrightarrow> \<exists>i' s2'. L2.eval s2 s2' \<and> match i' s1' s2'"
proof(induction s1 arbitrary: i s2 rule: converse_rtranclp_induct)
case (base s2)
thus ?case by auto
next
case (step s1 s1'')
show ?case
using simulation[OF \<open>match i s1 s2\<close> \<open>step1 s1 s1''\<close>]
proof (elim disjE exE conjE)
fix i' s2'
assume "step2\<^sup>+\<^sup>+ s2 s2'" and "match i' s1'' s2'"
thus ?thesis
by (auto intro: rtranclp_trans dest!: tranclp_into_rtranclp step.IH)
next
fix i'
assume "match i' s1'' s2" and "i' \<sqsubset> i"
thus ?thesis
by (auto intro: step.IH)
qed
qed
lemma match_inf:
assumes "match i s1 s2" and "inf step1 s1"
shows "inf step2 s2"
proof -
from assms have "inf_wf step2 order i s2"
proof (coinduction arbitrary: i s1 s2)
case inf_wf
obtain s1' where step_s1: "step1 s1 s1'" and inf_s1': "inf step1 s1'"
using inf_wf(2) by (auto elim: inf.cases)
from simulation[OF \<open>match i s1 s2\<close> step_s1] show ?case
using inf_s1' by auto
qed
thus ?thesis using inf_wf_to_inf
by (auto intro: inf_wf_to_inf well_founded_axioms)
qed
subsubsection \<open>Preservation of behaviour\<close>
lemma simulation_behaviour :
"L1.state_behaves s1 b1 \<Longrightarrow> \<not> is_wrong b1 \<Longrightarrow> match i s1 s2 \<Longrightarrow>
\<exists>b2 i'. L2.state_behaves s2 b2 \<and> rel_behaviour (match i') b1 b2"
proof(induction rule: L1.state_behaves.cases)
case (state_terminates s1 s1')
then obtain i' s2' where steps_s2: "L2.eval s2 s2'" and match_s1'_s2': "match i' s1' s2'"
using lift_simulation_eval by blast
hence "final2 s2'"
by (auto intro: state_terminates.hyps match_final)
hence "L2.state_behaves s2 (Terminates s2')"
using L2.final_finished L2.state_terminates[OF steps_s2]
by simp
moreover have "rel_behaviour (match i') b1 (Terminates s2')"
by (simp add: \<open>match i' s1' s2'\<close> state_terminates.hyps)
ultimately show ?case by blast
next
case (state_diverges s2)
then show ?case
using match_inf[THEN L2.state_diverges] by fastforce
next
case (state_goes_wrong s2 s2')
then show ?case using \<open>\<not>is_wrong b1\<close> by simp
qed
subsubsection \<open>Forward to backward\<close>
lemma state_behaves_forward_to_backward:
assumes
match_s1_s2: "match i s1 s2" and
safe_s1: "L1.safe s1" and
behaves_s2: "L2.state_behaves s2 b2" and
right_unique2: "right_unique step2"
shows "\<exists>b1 i. L1.state_behaves s1 b1 \<and> rel_behaviour (match i) b1 b2"
proof -
obtain b1 where behaves_s1: "L1.state_behaves s1 b1"
using L1.left_total_state_behaves
by (auto elim: left_totalE)
have not_wrong_b1: "\<not> is_wrong b1"
by (rule L1.safe_state_behaves_not_wrong[OF safe_s1 behaves_s1])
obtain i' where "L2.state_behaves s2 b2" and rel_b1_B2: "rel_behaviour (match i') b1 b2"
using simulation_behaviour[OF behaves_s1 not_wrong_b1 match_s1_s2]
using L2.right_unique_state_behaves[OF right_unique2, THEN right_uniqueD]
using behaves_s2
by auto
show ?thesis
using behaves_s1 rel_b1_B2 by auto
qed
end
subsection \<open>Bisimulation\<close>
locale bisimulation =
forward_simulation step1 step2 final1 final2 order match +
backward_simulation step1 step2 final1 final2 order match
for
step1 :: "'state1 \<Rightarrow> 'state1 \<Rightarrow> bool" and
step2 :: "'state2 \<Rightarrow> 'state2 \<Rightarrow> bool" and
final1 :: "'state1 \<Rightarrow> bool" and
final2 :: "'state2 \<Rightarrow> bool" and
order :: "'index \<Rightarrow> 'index \<Rightarrow> bool" and
match :: "'index \<Rightarrow> 'state1 \<Rightarrow> 'state2 \<Rightarrow> bool"
subsection \<open>Composition of backward simulations\<close>
definition rel_comp ::
......
theory Transfer_Extras
imports Main
begin
lemma rtranclp_complete_run_right_unique:
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and x y z :: 'a
assumes "right_unique R"
shows "R\<^sup>*\<^sup>* x y \<Longrightarrow> (\<nexists>w. R y w) \<Longrightarrow> R\<^sup>*\<^sup>* x z \<Longrightarrow> (\<nexists>w. R z w) \<Longrightarrow> y = z"
proof (induction x arbitrary: z rule: converse_rtranclp_induct)
case base
then show ?case
by (auto elim: converse_rtranclpE)
next
case (step x w)
hence "R\<^sup>*\<^sup>* w z"
using right_uniqueD[OF \<open>right_unique R\<close>]
by (metis converse_rtranclpE)
with step show ?case
by simp
qed
lemma tranclp_complete_run_right_unique:
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and x y z :: 'a
assumes "right_unique R"
shows "R\<^sup>+\<^sup>+ x y \<Longrightarrow> (\<nexists>w. R y w) \<Longrightarrow> R\<^sup>+\<^sup>+ x z \<Longrightarrow> (\<nexists>w. R z w) \<Longrightarrow> y = z"
using right_uniqueD[OF \<open>right_unique R\<close>, of x]
by (auto dest!: tranclpD intro!: rtranclp_complete_run_right_unique[OF \<open>right_unique R\<close>, of _ y z])
end
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment