-
Notifications
You must be signed in to change notification settings - Fork 0
/
Weaken_Stat_Imp.thy
111 lines (91 loc) · 5.01 KB
/
Weaken_Stat_Imp.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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
(*
Title: Psi-calculi
Based on the AFP entry by Jesper Bengtson ([email protected]), 2012
*)
theory Weaken_Stat_Imp
imports Weaken_Transition
begin
context weak begin
definition
"weakenStatImp" :: "'b \<Rightarrow> ('a, 'b, 'c) psi \<Rightarrow>
('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set \<Rightarrow>
('a, 'b, 'c) psi \<Rightarrow> bool" ("_ \<rhd> _ \<lessapprox>\<^sub>w<_> _" [80, 80, 80, 80] 80)
where "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q \<equiv> \<exists>Q'. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q' \<and> insert_assertion(extract_frame P) \<Psi> \<hookrightarrow>\<^sub>F insert_assertion(extract_frame Q') \<Psi> \<and> (\<Psi>, P, Q') \<in> Rel"
lemma weakenStatImpMonotonic:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and A :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and B :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
assumes "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<A> Q"
and "A \<subseteq> B"
shows "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<B> Q"
using assms
by(auto simp add: weakenStatImp_def)
lemma weakenStatImpI:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and \<Psi>' :: 'b
assumes "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'"
and "insert_assertion(extract_frame P) \<Psi> \<hookrightarrow>\<^sub>F insert_assertion(extract_frame Q') \<Psi>"
and "(\<Psi>, P, Q') \<in> Rel"
shows "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q"
using assms
by(auto simp add: weakenStatImp_def)
lemma weakenStatImpE:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and \<Psi>' :: 'b
assumes "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q"
obtains Q' where "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'" and "insert_assertion(extract_frame P) \<Psi> \<hookrightarrow>\<^sub>F insert_assertion(extract_frame Q') \<Psi> " and "(\<Psi>, P, Q') \<in> Rel"
using assms
by(auto simp add: weakenStatImp_def)
lemma weak_stat_impWeakenStatImp:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
assumes cSim: "\<Psi> \<rhd> P \<lessapprox><Rel> Q"
and cStatEq: "\<And>\<Psi>' R S \<Psi>''. \<lbrakk>(\<Psi>', R, S) \<in> Rel; \<Psi>' \<simeq> \<Psi>''\<rbrakk> \<Longrightarrow> (\<Psi>'', R, S) \<in> Rel"
shows "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q"
proof -
from `\<Psi> \<rhd> P \<lessapprox><Rel> Q`
obtain Q' Q'' where QChain: "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'"
and PImpQ': "insert_assertion(extract_frame P) \<Psi> \<hookrightarrow>\<^sub>F insert_assertion(extract_frame Q') \<Psi>"
and Q'Chain: "\<Psi> \<otimes> \<one> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''" and "(\<Psi> \<otimes> \<one>, P, Q'') \<in> Rel"
by(rule weak_stat_impE)
from Q'Chain Identity have Q'Chain: "\<Psi> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''" by(rule tau_chain_stat_eq)
with QChain have "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''" by auto
moreover from Q'Chain have "insert_assertion(extract_frame Q') \<Psi> \<hookrightarrow>\<^sub>F insert_assertion(extract_frame Q'') \<Psi>"
by(rule statImpTauChainDerivative)
with PImpQ' have "insert_assertion(extract_frame P) \<Psi> \<hookrightarrow>\<^sub>F insert_assertion(extract_frame Q'') \<Psi>"
by(rule Frame_stat_imp_trans)
moreover from `(\<Psi> \<otimes> \<one>, P, Q'') \<in> Rel` Identity have "(\<Psi>, P, Q'') \<in> Rel" by(rule cStatEq)
ultimately show ?thesis by(rule weakenStatImpI)
qed
lemma weakenStatImpWeakStatImp:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
assumes "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q"
and cExt: "\<And>\<Psi>' R S \<Psi>''. (\<Psi>', R, S) \<in> Rel \<Longrightarrow> (\<Psi>' \<otimes> \<Psi>'', R, S) \<in> Rel"
shows "\<Psi> \<rhd> P \<lessapprox><Rel> Q"
proof(induct rule: weak_stat_impI)
case(cStatImp \<Psi>')
from `\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q`
obtain Q' where QChain: "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'"
and PImpQ': "insert_assertion(extract_frame P) \<Psi> \<hookrightarrow>\<^sub>F insert_assertion(extract_frame Q') \<Psi>"
and "(\<Psi>, P, Q') \<in> Rel"
by(rule weakenStatImpE)
note QChain PImpQ'
moreover have "\<Psi> \<otimes> \<Psi>' \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'" by simp
moreover from `(\<Psi>, P, Q') \<in> Rel` have "(\<Psi> \<otimes> \<Psi>', P, Q') \<in> Rel" by(rule cExt)
ultimately show ?case by blast
qed
end
end