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" |
|
50 by (rule swap_fresh_fresh) (simp_all add: fresh_at_base(1)) |
|
51 |
49 nominal_primrec (* (invariant "\<lambda>(_, e, d) y. atom e \<sharp> y \<and> atom d \<sharp> y") *) |
52 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) |
53 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
51 where |
54 where |
52 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
55 "(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])" |
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])" |
72 apply(simp add: trm.fresh)*) |
75 apply(simp add: trm.fresh)*) |
73 apply(rule TrueI) |
76 apply(rule TrueI) |
74 -- "covered all cases" |
77 -- "covered all cases" |
75 apply(case_tac x) |
78 apply(case_tac x) |
76 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) |
77 apply(simp) |
80 apply (simp_all add: fresh_star_def)[12] |
78 apply(blast) |
81 apply(metis)+ |
79 apply(simp add: fresh_star_def) |
|
80 apply(blast) |
|
81 apply(simp add: fresh_star_def) |
|
82 apply(blast) |
|
83 apply(simp add: fresh_star_def) |
|
84 apply(blast) |
|
85 apply(simp add: fresh_star_def) |
|
86 apply(blast) |
|
87 apply(simp add: fresh_star_def) |
|
88 apply(blast) |
|
89 apply(simp add: fresh_star_def) |
|
90 apply(blast) |
|
91 apply(simp add: fresh_star_def) |
|
92 apply(blast) |
|
93 apply(simp add: fresh_star_def) |
|
94 apply(blast) |
|
95 apply(simp add: fresh_star_def) |
|
96 apply(metis) |
|
97 apply(simp add: fresh_star_def) |
|
98 apply(metis) |
|
99 apply(simp add: fresh_star_def) |
|
100 apply(metis) |
|
101 -- "compatibility" |
82 -- "compatibility" |
102 apply(simp_all) |
83 apply(simp_all) |
103 apply(rule conjI) |
84 apply(rule conjI) |
104 apply(erule conjE)+ |
85 apply(elim conjE) |
105 apply(erule Abs_lst1_fcb) |
86 apply(erule Abs_lst1_fcb) |
106 apply(simp add: Abs_fresh_iff) |
87 apply(simp add: Abs_fresh_iff) |
107 apply(simp add: Abs_fresh_iff) |
88 apply(simp add: Abs_fresh_iff) |
108 apply(erule fresh_eqvt_at) |
89 apply(erule fresh_eqvt_at) |
109 apply(simp add: finite_supp) |
90 apply(simp add: finite_supp) |
110 apply(simp add: fresh_Pair fresh_at_base(1)) |
91 apply(simp add: fresh_Pair fresh_at_base(1)) |
111 apply(drule sym) |
92 apply(simp add: eqvt_at_def swap_at_base_sort) |
112 apply(drule sym) |
93 apply simp |
113 apply(drule sym) |
|
114 apply(drule sym) |
|
115 apply(simp add: eqvt_at_def swap_fresh_fresh) |
|
116 oops |
94 oops |
117 |
95 |
118 end |
96 end |
119 |
97 |
120 |
98 |