-
Notifications
You must be signed in to change notification settings - Fork 0
/
Close_Subst.thy
99 lines (76 loc) · 3.25 KB
/
Close_Subst.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
(*
Title: Psi-calculi
Based on the AFP entry by Jesper Bengtson ([email protected]), 2012
*)
theory Close_Subst
imports Agent Subst_Term
begin
context subst_psi
begin
definition close_subst :: "('b::fs_name \<times> ('a::fs_name, 'b, 'c::fs_name) psi \<times> ('a, 'b, 'c) psi) set \<Rightarrow> ('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
where "close_subst Rel \<equiv> {(\<Psi>, P, Q) | \<Psi> P Q. (\<forall>\<sigma>. well_formed_subst \<sigma> \<longrightarrow> (\<Psi>, P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel)}"
lemma close_substI:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
assumes "\<And>\<sigma>. well_formed_subst \<sigma> \<Longrightarrow> (\<Psi>, P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel"
shows "(\<Psi>, P, Q) \<in> close_subst Rel"
using assms
by(unfold close_subst_def) auto
lemma close_substE:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and \<sigma> :: "(name list \<times> 'a list) list"
assumes "(\<Psi>, P, Q) \<in> close_subst Rel"
and "well_formed_subst \<sigma>"
shows "(\<Psi>, P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel"
using assms
by(unfold close_subst_def) auto
lemma close_subst_closed:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and p :: "name prm"
assumes "eqvt Rel"
and "(\<Psi>, P, Q) \<in> close_subst Rel"
shows "(p \<bullet> \<Psi>, p \<bullet> P, p \<bullet> Q) \<in> close_subst Rel"
proof(rule close_substI)
fix \<sigma>
assume "well_formed_subst(\<sigma>::(name list \<times> 'a list) list)"
with `(\<Psi>, P, Q) \<in> close_subst Rel` `well_formed_subst \<sigma>`
have "(\<Psi>, P[<(rev p \<bullet> \<sigma>)>], Q[<(rev p \<bullet> \<sigma>)>]) \<in> Rel"
by(rule_tac close_substE) auto
hence "(p \<bullet> \<Psi>, p \<bullet> (P[<(rev p \<bullet> \<sigma>)>]), p \<bullet> (Q[<(rev p \<bullet> \<sigma>)>])) \<in> Rel"
by(drule_tac p=p in eqvtI[OF `eqvt Rel`]) (simp add: eqvts)
thus "(p \<bullet> \<Psi>, (p \<bullet> P)[<\<sigma>>], (p \<bullet> Q)[<\<sigma>>]) \<in> Rel"
by(simp del: seq_subs_def add: eqvts)
qed
lemma close_subst_eqvt:
assumes "eqvt Rel"
shows "eqvt(close_subst Rel)"
proof(auto simp add: eqvt_def)
fix \<Psi> P Q p
assume "(\<Psi>, P, Q) \<in> close_subst Rel"
thus "((p::name prm) \<bullet> \<Psi>, p \<bullet> P, p \<bullet> Q) \<in> close_subst Rel"
by(drule_tac p=p in close_subst_closed[OF `eqvt Rel`]) (simp add: eqvts)
qed
lemma close_subst_unfold:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and \<sigma> :: "(name list \<times> 'a list) list"
assumes "(\<Psi>, P, Q) \<in> close_subst Rel"
and "well_formed_subst \<sigma>"
shows "(\<Psi>, P[<\<sigma>>], Q[<\<sigma>>]) \<in> close_subst Rel"
proof(rule close_substI)
fix \<sigma>'::"(name list \<times> 'a list) list"
assume "well_formed_subst \<sigma>'"
with `well_formed_subst \<sigma>` have "well_formed_subst(\<sigma>@\<sigma>')" by simp
with `(\<Psi>, P, Q) \<in> close_subst Rel` have "(\<Psi>, P[<(\<sigma>@\<sigma>')>], Q[<(\<sigma>@\<sigma>')>]) \<in> Rel"
by(rule close_substE)
thus "(\<Psi>, P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel"
by simp
qed
end
end