equal
deleted
inserted
replaced
7 atom_decl name |
7 atom_decl name |
8 atom_decl coname |
8 atom_decl coname |
9 |
9 |
10 nominal_datatype trm = |
10 nominal_datatype trm = |
11 Ax "name" "coname" |
11 Ax "name" "coname" |
12 | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
12 | Cut c::"coname" t1::"trm" n::"name" t2::"trm" bind n in t1, bind c in t2 |
13 ("Cut <_>._ '(_')._" [100,100,100,100] 100) |
13 ("Cut <_>._ '(_')._" [100,100,100,100] 100) |
14 | NotR n::"name" t::"trm" "coname" bind n in t |
14 | NotR n::"name" t::"trm" "coname" bind n in t |
15 ("NotR '(_')._ _" [100,100,100] 100) |
15 ("NotR '(_')._ _" [100,100,100] 100) |
16 | NotL c::"coname" t::"trm" "name" bind c in t |
16 | NotL c::"coname" t::"trm" "name" bind c in t |
17 ("NotL <_>._ _" [100,100,100] 100) |
17 ("NotL <_>._ _" [100,100,100] 100) |
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 nominal_primrec |
49 nominal_primrec (* (invariant "\<lambda>(_, e, d) y. atom e \<sharp> y \<and> atom d \<sharp> y") *) |
50 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
50 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
51 where |
51 where |
52 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
52 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
53 | "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])" |
53 | "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])" |
54 | "(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)" |
54 | "(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)" |
66 (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)" |
66 (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)" |
67 | "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" |
67 | "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 apply(simp only: eqvt_def) |
68 apply(simp only: eqvt_def) |
69 apply(simp only: crename_graph_def) |
69 apply(simp only: crename_graph_def) |
70 apply (rule, perm_simp, rule) |
70 apply (rule, perm_simp, rule) |
|
71 (*apply(erule crename_graph.induct) |
|
72 apply(simp add: trm.fresh)*) |
71 apply(rule TrueI) |
73 apply(rule TrueI) |
72 -- "covered all cases" |
74 -- "covered all cases" |
73 apply(case_tac x) |
75 apply(case_tac x) |
74 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
76 apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust) |
75 apply(simp) |
77 apply(simp) |
94 apply(metis) |
96 apply(metis) |
95 apply(simp add: fresh_star_def) |
97 apply(simp add: fresh_star_def) |
96 apply(metis) |
98 apply(metis) |
97 apply(simp add: fresh_star_def) |
99 apply(simp add: fresh_star_def) |
98 apply(metis) |
100 apply(metis) |
99 -- "clashes" |
101 -- "compatibility" |
100 apply(simp_all) |
102 apply(simp_all) |
|
103 apply(rule conjI) |
|
104 apply(erule conjE)+ |
|
105 apply(erule Abs_lst1_fcb) |
|
106 apply(simp add: Abs_fresh_iff) |
|
107 apply(simp add: Abs_fresh_iff) |
|
108 apply(erule fresh_eqvt_at) |
|
109 apply(simp add: finite_supp) |
|
110 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
111 apply(drule sym) |
|
112 apply(drule sym) |
|
113 apply(drule sym) |
|
114 apply(drule sym) |
|
115 apply(simp add: eqvt_at_def swap_fresh_fresh) |
101 oops |
116 oops |
102 |
117 |
103 end |
118 end |
104 |
119 |
105 |
120 |