equal
deleted
inserted
replaced
65 | "(OrL (x).M (y).N z)[d\<turnstile>c>e] = OrL (x).(M[d\<turnstile>c>e]) (y).(N[d\<turnstile>c>e]) z" |
65 | "(OrL (x).M (y).N z)[d\<turnstile>c>e] = OrL (x).(M[d\<turnstile>c>e]) (y).(N[d\<turnstile>c>e]) z" |
66 | "atom a \<sharp> (d, e) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] = |
66 | "atom a \<sharp> (d, e) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] = |
67 (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)" |
67 (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)" |
68 | "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" |
68 | "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" |
69 apply(simp only: eqvt_def) |
69 apply(simp only: eqvt_def) |
70 apply(simp only: crename_graph_def) |
70 apply(simp only: crename_graph_aux_def) |
71 apply (rule, perm_simp, rule) |
71 apply (rule, perm_simp, rule) |
72 apply(rule TrueI) |
72 apply(rule TrueI) |
73 -- "covered all cases" |
73 -- "covered all cases" |
74 apply(case_tac x) |
74 apply(case_tac x) |
75 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
75 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
270 (if z=u then OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) v else OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) z)" |
270 (if z=u then OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) v else OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) z)" |
271 | "atom x \<sharp> (u, v) \<Longrightarrow> (ImpR (x).<a>.M b)[u\<turnstile>n>v] = ImpR (x).<a>.(M[u\<turnstile>n>v]) b" |
271 | "atom x \<sharp> (u, v) \<Longrightarrow> (ImpR (x).<a>.M b)[u\<turnstile>n>v] = ImpR (x).<a>.(M[u\<turnstile>n>v]) b" |
272 | "atom x \<sharp> (u, v) \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = |
272 | "atom x \<sharp> (u, v) \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = |
273 (if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)" |
273 (if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)" |
274 apply(simp only: eqvt_def) |
274 apply(simp only: eqvt_def) |
275 apply(simp only: nrename_graph_def) |
275 apply(simp only: nrename_graph_aux_def) |
276 apply (rule, perm_simp, rule) |
276 apply (rule, perm_simp, rule) |
277 apply(rule TrueI) |
277 apply(rule TrueI) |
278 -- "covered all cases" |
278 -- "covered all cases" |
279 apply(case_tac x) |
279 apply(case_tac x) |
280 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
280 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
472 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b" |
472 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b" |
473 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = |
473 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = |
474 (if y=z then Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z' |
474 (if y=z then Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z' |
475 else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)" |
475 else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)" |
476 apply(simp only: eqvt_def) |
476 apply(simp only: eqvt_def) |
477 apply(simp only: substn_graph_def) |
477 apply(simp only: substn_graph_aux_def) |
478 apply (rule, perm_simp, rule) |
478 apply (rule, perm_simp, rule) |
479 apply(rule TrueI) |
479 apply(rule TrueI) |
480 -- "covered all cases" |
480 -- "covered all cases" |
481 apply(case_tac x) |
481 apply(case_tac x) |
482 apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust) |
482 apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust) |