-
Notifications
You must be signed in to change notification settings - Fork 10
/
Copy pathutp_rel_opsem.thy
80 lines (61 loc) · 3.35 KB
/
utp_rel_opsem.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
section \<open> Relational Operational Semantics \<close>
theory utp_rel_opsem
imports
utp_rel_laws
utp_hoare
begin
text \<open> This theory uses the laws of relational calculus to create a basic operational semantics.
It is based on Chapter 10 of the UTP book~\cite{Hoare&98}. \<close>
fun trel :: "'\<alpha> usubst \<times> '\<alpha> hrel \<Rightarrow> '\<alpha> usubst \<times> '\<alpha> hrel \<Rightarrow> bool" (infix "\<rightarrow>\<^sub>u" 85) where
"(\<sigma>, P) \<rightarrow>\<^sub>u (\<rho>, Q) \<longleftrightarrow> (\<langle>\<sigma>\<rangle>\<^sub>a ;; P) \<sqsubseteq> (\<langle>\<rho>\<rangle>\<^sub>a ;; Q)"
lemma trans_trel:
"\<lbrakk> (\<sigma>, P) \<rightarrow>\<^sub>u (\<rho>, Q); (\<rho>, Q) \<rightarrow>\<^sub>u (\<phi>, R) \<rbrakk> \<Longrightarrow> (\<sigma>, P) \<rightarrow>\<^sub>u (\<phi>, R)"
by auto
lemma skip_trel: "(\<sigma>, II) \<rightarrow>\<^sub>u (\<sigma>, II)"
by simp
lemma assigns_trel: "(\<sigma>, \<langle>\<rho>\<rangle>\<^sub>a) \<rightarrow>\<^sub>u (\<rho> \<circ>\<^sub>s \<sigma>, II)"
by (simp add: assigns_comp)
lemma assign_trel:
"(\<sigma>, x := v) \<rightarrow>\<^sub>u (\<sigma>(&x \<mapsto>\<^sub>s \<sigma> \<dagger> v), II)"
by (simp add: assigns_comp usubst)
lemma seq_trel:
assumes "(\<sigma>, P) \<rightarrow>\<^sub>u (\<rho>, Q)"
shows "(\<sigma>, P ;; R) \<rightarrow>\<^sub>u (\<rho>, Q ;; R)"
by (metis (no_types, lifting) assms order_refl seqr_assoc seqr_mono trel.simps)
lemma seq_skip_trel:
"(\<sigma>, II ;; P) \<rightarrow>\<^sub>u (\<sigma>, P)"
by simp
lemma nondet_left_trel:
"(\<sigma>, P \<sqinter> Q) \<rightarrow>\<^sub>u (\<sigma>, P)"
by (metis (no_types, opaque_lifting) disj_comm disj_upred_def semilattice_sup_class.sup.absorb_iff1 semilattice_sup_class.sup.left_idem seqr_or_distr trel.simps)
lemma nondet_right_trel:
"(\<sigma>, P \<sqinter> Q) \<rightarrow>\<^sub>u (\<sigma>, Q)"
by (simp add: seqr_mono)
lemma rcond_true_trel:
assumes "\<sigma> \<dagger> b = true"
shows "(\<sigma>, P \<triangleleft> b \<triangleright>\<^sub>r Q) \<rightarrow>\<^sub>u (\<sigma>, P)"
using assms
by (simp add: assigns_r_comp usubst alpha)
lemma rcond_false_trel:
assumes "\<sigma> \<dagger> b = false"
shows "(\<sigma>, P \<triangleleft> b \<triangleright>\<^sub>r Q) \<rightarrow>\<^sub>u (\<sigma>, Q)"
using assms
by (simp add: assigns_r_comp usubst alpha)
lemma while_true_trel:
assumes "\<sigma> \<dagger> b = true"
shows "(\<sigma>, while b do P od) \<rightarrow>\<^sub>u (\<sigma>, P ;; while b do P od)"
by (metis assms rcond_true_trel while_unfold)
lemma while_false_trel:
assumes "\<sigma> \<dagger> b = false"
shows "(\<sigma>, while b do P od) \<rightarrow>\<^sub>u (\<sigma>, II)"
by (metis assms rcond_false_trel while_unfold)
text \<open> Theorem linking Hoare calculus and operational semantics. If we start $Q$ in a state $\sigma_0$
satisfying $p$, and $Q$ reaches final state $\sigma_1$ then $r$ holds in this final state. \<close>
theorem hoare_opsem_link:
"\<lbrace>p\<rbrace>Q\<lbrace>r\<rbrace>\<^sub>u = (\<forall> \<sigma>\<^sub>0 \<sigma>\<^sub>1. `\<sigma>\<^sub>0 \<dagger> p` \<and> (\<sigma>\<^sub>0, Q) \<rightarrow>\<^sub>u (\<sigma>\<^sub>1, II) \<longrightarrow> `\<sigma>\<^sub>1 \<dagger> r`)"
apply (rel_auto)
apply (rename_tac a b)
apply (metis (full_types) lit.rep_eq)
done
declare trel.simps [simp del]
end