44 thm trm.fv_bn_eqvt |
44 thm trm.fv_bn_eqvt |
45 thm trm.size_eqvt |
45 thm trm.size_eqvt |
46 thm trm.supp |
46 thm trm.supp |
47 thm trm.supp[simplified] |
47 thm trm.supp[simplified] |
48 |
48 |
49 lemma swap_at_base_sort: "sort_of (atom a) \<noteq> sort_of (atom x) \<Longrightarrow> sort_of (atom b) \<noteq> sort_of (atom x) \<Longrightarrow> (atom a \<rightleftharpoons> atom b) \<bullet> x = x" |
49 lemma swap_at_base_sort: |
|
50 "sort_of (atom a) \<noteq> sort_of (atom x) \<Longrightarrow> sort_of (atom b) \<noteq> sort_of (atom x) |
|
51 \<Longrightarrow> (atom a \<rightleftharpoons> atom b) \<bullet> x = x" |
50 by (rule swap_fresh_fresh) (simp_all add: fresh_at_base(1)) |
52 by (rule swap_fresh_fresh) (simp_all add: fresh_at_base(1)) |
51 |
53 |
52 nominal_primrec (* (invariant "\<lambda>(_, e, d) y. atom e \<sharp> y \<and> atom d \<sharp> y") *) |
54 nominal_primrec |
53 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
55 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
54 where |
56 where |
55 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
57 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
56 | "atom a \<sharp> (d, e) \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])" |
58 | "atom a \<sharp> (d, e) \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])" |
57 | "(NotR (x).M a)[d\<turnstile>c>e] = (if a=d then NotR (x).(M[d\<turnstile>c>e]) e else NotR (x).(M[d\<turnstile>c>e]) a)" |
59 | "(NotR (x).M a)[d\<turnstile>c>e] = (if a=d then NotR (x).(M[d\<turnstile>c>e]) e else NotR (x).(M[d\<turnstile>c>e]) a)" |
69 (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)" |
71 (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)" |
70 | "atom a \<sharp> (d, e) \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y" |
72 | "atom a \<sharp> (d, e) \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y" |
71 apply(simp only: eqvt_def) |
73 apply(simp only: eqvt_def) |
72 apply(simp only: crename_graph_def) |
74 apply(simp only: crename_graph_def) |
73 apply (rule, perm_simp, rule) |
75 apply (rule, perm_simp, rule) |
74 (*apply(erule crename_graph.induct) |
|
75 apply(simp add: trm.fresh)*) |
|
76 apply(rule TrueI) |
76 apply(rule TrueI) |
77 -- "covered all cases" |
77 -- "covered all cases" |
78 apply(case_tac x) |
78 apply(case_tac x) |
79 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
79 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
80 apply (simp_all add: fresh_star_def)[12] |
80 apply (simp_all add: fresh_star_def)[12] |
89 apply(erule fresh_eqvt_at) |
89 apply(erule fresh_eqvt_at) |
90 apply(simp add: finite_supp) |
90 apply(simp add: finite_supp) |
91 apply(simp add: fresh_Pair fresh_at_base(1)) |
91 apply(simp add: fresh_Pair fresh_at_base(1)) |
92 apply(simp add: eqvt_at_def swap_at_base_sort) |
92 apply(simp add: eqvt_at_def swap_at_base_sort) |
93 apply simp |
93 apply simp |
|
94 apply(elim conjE) |
|
95 apply(erule Abs_lst1_fcb) |
|
96 apply(simp add: Abs_fresh_iff) |
|
97 apply(simp add: Abs_fresh_iff) |
|
98 apply(erule fresh_eqvt_at) |
|
99 apply(simp add: finite_supp) |
|
100 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
101 apply(simp add: fresh_Pair) |
|
102 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
103 apply simp |
|
104 apply(elim conjE) |
|
105 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
|
106 apply(erule Abs_lst1_fcb) |
|
107 apply(simp add: Abs_fresh_iff) |
|
108 apply(simp add: Abs_fresh_iff) |
|
109 apply(erule fresh_eqvt_at) |
|
110 apply(simp add: finite_supp) |
|
111 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
112 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
113 apply simp |
|
114 apply(blast) |
|
115 apply(elim conjE) |
|
116 apply(erule Abs_lst1_fcb) |
|
117 apply(simp add: Abs_fresh_iff) |
|
118 apply(simp add: Abs_fresh_iff) |
|
119 apply(erule fresh_eqvt_at) |
|
120 apply(simp add: finite_supp) |
|
121 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
122 apply(simp add: fresh_Pair) |
|
123 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
124 apply simp |
|
125 apply(erule conjE)+ |
|
126 apply(rule conjI) |
|
127 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
|
128 apply(erule Abs_lst1_fcb) |
|
129 apply(simp add: Abs_fresh_iff) |
|
130 apply(simp add: Abs_fresh_iff) |
|
131 apply(erule fresh_eqvt_at) |
|
132 apply(simp add: finite_supp) |
|
133 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
134 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
135 apply simp |
|
136 apply(blast) |
|
137 apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)") |
|
138 apply(erule Abs_lst1_fcb) |
|
139 apply(simp add: Abs_fresh_iff) |
|
140 apply(simp add: Abs_fresh_iff) |
|
141 apply(erule fresh_eqvt_at) |
|
142 apply(simp add: finite_supp) |
|
143 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
144 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
145 apply simp |
|
146 apply(blast) |
|
147 apply(elim conjE) |
|
148 apply(erule Abs_lst1_fcb) |
|
149 apply(simp add: Abs_fresh_iff) |
|
150 apply(simp add: Abs_fresh_iff) |
|
151 apply(erule fresh_eqvt_at) |
|
152 apply(simp add: finite_supp) |
|
153 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
154 apply(simp add: fresh_Pair) |
|
155 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
156 apply simp |
|
157 apply(elim conjE) |
|
158 apply(erule Abs_lst1_fcb) |
|
159 apply(simp add: Abs_fresh_iff) |
|
160 apply(simp add: Abs_fresh_iff) |
|
161 apply(erule fresh_eqvt_at) |
|
162 apply(simp add: finite_supp) |
|
163 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
164 apply(simp add: fresh_Pair) |
|
165 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
166 apply simp |
|
167 apply(erule conjE)+ |
|
168 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
|
169 apply(erule Abs_lst1_fcb) |
|
170 apply(simp add: Abs_fresh_iff) |
|
171 apply(simp add: Abs_fresh_iff) |
|
172 apply(erule fresh_eqvt_at) |
|
173 apply(simp add: finite_supp) |
|
174 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
175 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
176 apply simp |
|
177 apply(blast) |
|
178 apply(erule conjE)+ |
|
179 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
|
180 apply(erule Abs_lst1_fcb) |
|
181 apply(simp add: Abs_fresh_iff) |
|
182 apply(simp add: Abs_fresh_iff) |
|
183 apply(erule fresh_eqvt_at) |
|
184 apply(simp add: finite_supp) |
|
185 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
186 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
187 apply simp |
|
188 apply(blast) |
|
189 apply(rule conjI) |
|
190 apply(elim conjE) |
|
191 apply(erule Abs_lst1_fcb) |
|
192 apply(simp add: Abs_fresh_iff) |
|
193 apply(simp add: Abs_fresh_iff) |
|
194 apply(erule fresh_eqvt_at) |
|
195 apply(simp add: finite_supp) |
|
196 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
197 apply(simp add: eqvt_at_def swap_at_base_sort) |
|
198 apply simp |
|
199 apply(elim conjE) |
|
200 apply(erule Abs_lst1_fcb) |
|
201 apply(simp add: Abs_fresh_iff) |
|
202 apply(simp add: Abs_fresh_iff) |
|
203 apply(erule fresh_eqvt_at) |
|
204 apply(simp add: finite_supp) |
|
205 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
206 apply(simp add: fresh_Pair) |
|
207 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
208 apply simp |
|
209 apply(erule conjE)+ |
|
210 defer |
|
211 apply(elim conjE) |
|
212 apply(rule conjI) |
|
213 apply(erule Abs_lst1_fcb) |
|
214 apply(simp add: Abs_fresh_iff) |
|
215 apply(simp add: Abs_fresh_iff) |
|
216 apply(erule fresh_eqvt_at) |
|
217 apply(simp add: finite_supp) |
|
218 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
219 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
220 apply simp |
|
221 apply(erule Abs_lst1_fcb) |
|
222 apply(simp add: Abs_fresh_iff) |
|
223 apply(simp add: Abs_fresh_iff) |
|
224 apply(erule fresh_eqvt_at) |
|
225 apply(simp add: finite_supp) |
|
226 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
227 apply(simp add: fresh_Pair) |
|
228 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
229 apply simp |
94 oops |
230 oops |
95 |
231 |
96 end |
232 end |
97 |
233 |
98 |
234 |