|
1 theory Term5 |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 datatype rtrm5 = |
|
8 rVr5 "name" |
|
9 | rAp5 "rtrm5" "rtrm5" |
|
10 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
|
11 and rlts = |
|
12 rLnil |
|
13 | rLcons "name" "rtrm5" "rlts" |
|
14 |
|
15 primrec |
|
16 rbv5 |
|
17 where |
|
18 "rbv5 rLnil = {}" |
|
19 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
|
20 |
|
21 |
|
22 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} |
|
23 print_theorems |
|
24 |
|
25 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") |
|
26 [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} |
|
27 print_theorems |
|
28 |
|
29 notation |
|
30 alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and |
|
31 alpha_rlts ("_ \<approx>l _" [100, 100] 100) |
|
32 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros |
|
33 |
|
34 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} |
|
35 thm alpha5_inj |
|
36 |
|
37 lemma rbv5_eqvt[eqvt]: |
|
38 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
|
39 apply (induct x) |
|
40 apply (simp_all add: eqvts atom_eqvt) |
|
41 done |
|
42 |
|
43 lemma fv_rtrm5_rlts_eqvt[eqvt]: |
|
44 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
|
45 "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)" |
|
46 apply (induct x and l) |
|
47 apply (simp_all add: eqvts atom_eqvt) |
|
48 done |
|
49 |
|
50 (*lemma alpha5_eqvt: |
|
51 "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and> |
|
52 (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and> |
|
53 (alpha_rbv5 b c \<longrightarrow> alpha_rbv5 (p \<bullet> b) (p \<bullet> c))" |
|
54 apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) |
|
55 done*) |
|
56 |
|
57 local_setup {* |
|
58 (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), |
|
59 build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} |
|
60 print_theorems |
|
61 |
|
62 lemma alpha5_reflp: |
|
63 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 x x)" |
|
64 apply (rule rtrm5_rlts.induct) |
|
65 apply (simp_all add: alpha5_inj) |
|
66 apply (rule_tac x="0::perm" in exI) |
|
67 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) |
|
68 done |
|
69 |
|
70 lemma alpha5_symp: |
|
71 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
|
72 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
|
73 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
|
74 apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *}) |
|
75 done |
|
76 |
|
77 lemma alpha5_symp1: |
|
78 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
|
79 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
|
80 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
|
81 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
|
82 apply (simp_all add: alpha5_inj) |
|
83 apply (erule exE) |
|
84 apply (rule_tac x="- pi" in exI) |
|
85 apply (simp add: alpha_gen) |
|
86 apply(simp add: fresh_star_def fresh_minus_perm) |
|
87 apply clarify |
|
88 apply (rule conjI) |
|
89 apply (rotate_tac 3) |
|
90 apply (frule_tac p="- pi" in alpha5_eqvt(2)) |
|
91 apply simp |
|
92 apply (rule conjI) |
|
93 apply (rotate_tac 5) |
|
94 apply (frule_tac p="- pi" in alpha5_eqvt(1)) |
|
95 apply simp |
|
96 apply (rotate_tac 6) |
|
97 apply simp |
|
98 apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) |
|
99 apply (simp) |
|
100 done |
|
101 |
|
102 thm alpha_gen_sym[no_vars] |
|
103 thm alpha_gen_compose_sym[no_vars] |
|
104 |
|
105 lemma tt: |
|
106 "\<lbrakk>R (- p \<bullet> x) y \<Longrightarrow> R (p \<bullet> y) x; (bs, x) \<approx>gen R f (- p) (cs, y)\<rbrakk> \<Longrightarrow> (cs, y) \<approx>gen R f p (bs, x)" |
|
107 unfolding alphas |
|
108 unfolding fresh_star_def |
|
109 by (auto simp add: fresh_minus_perm) |
|
110 |
|
111 lemma alpha5_symp2: |
|
112 shows "a \<approx>5 b \<Longrightarrow> b \<approx>5 a" |
|
113 and "x \<approx>l y \<Longrightarrow> y \<approx>l x" |
|
114 and "alpha_rbv5 x y \<Longrightarrow> alpha_rbv5 y x" |
|
115 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
|
116 (* non-binding case *) |
|
117 apply(simp add: alpha5_inj) |
|
118 (* non-binding case *) |
|
119 apply(simp add: alpha5_inj) |
|
120 (* binding case *) |
|
121 apply(simp add: alpha5_inj) |
|
122 apply(erule exE) |
|
123 apply(rule_tac x="- pi" in exI) |
|
124 apply(rule tt) |
|
125 apply(simp add: alphas) |
|
126 apply(erule conjE)+ |
|
127 apply(drule_tac p="- pi" in alpha5_eqvt(2)) |
|
128 apply(drule_tac p="- pi" in alpha5_eqvt(2)) |
|
129 apply(drule_tac p="- pi" in alpha5_eqvt(1)) |
|
130 apply(drule_tac p="- pi" in alpha5_eqvt(1)) |
|
131 apply(simp) |
|
132 apply(simp add: alphas) |
|
133 apply(erule conjE)+ |
|
134 apply metis |
|
135 (* non-binding case *) |
|
136 apply(simp add: alpha5_inj) |
|
137 (* non-binding case *) |
|
138 apply(simp add: alpha5_inj) |
|
139 (* non-binding case *) |
|
140 apply(simp add: alpha5_inj) |
|
141 (* non-binding case *) |
|
142 apply(simp add: alpha5_inj) |
|
143 done |
|
144 |
|
145 lemma alpha5_transp: |
|
146 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
|
147 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> |
|
148 (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))" |
|
149 (*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*) |
|
150 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
|
151 apply (rule_tac [!] allI) |
|
152 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
153 apply (simp_all add: alpha5_inj) |
|
154 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
155 apply (simp_all add: alpha5_inj) |
|
156 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
157 apply (simp_all add: alpha5_inj) |
|
158 defer |
|
159 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
160 apply (simp_all add: alpha5_inj) |
|
161 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
162 apply (simp_all add: alpha5_inj) |
|
163 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
|
164 (* HERE *) |
|
165 (* |
|
166 apply(rule alpha_gen_trans) |
|
167 thm alpha_gen_trans |
|
168 defer |
|
169 apply (simp add: alpha_gen) |
|
170 apply clarify |
|
171 apply(simp add: fresh_star_plus) |
|
172 apply (rule conjI) |
|
173 apply (erule_tac x="- pi \<bullet> rltsaa" in allE) |
|
174 apply (rotate_tac 5) |
|
175 apply (drule_tac p="- pi" in alpha5_eqvt(2)) |
|
176 apply simp |
|
177 apply (drule_tac p="pi" in alpha5_eqvt(2)) |
|
178 apply simp |
|
179 apply (erule_tac x="- pi \<bullet> rtrm5aa" in allE) |
|
180 apply (rotate_tac 7) |
|
181 apply (drule_tac p="- pi" in alpha5_eqvt(1)) |
|
182 apply simp |
|
183 apply (rotate_tac 3) |
|
184 apply (drule_tac p="pi" in alpha5_eqvt(1)) |
|
185 apply simp |
|
186 done |
|
187 *) |
|
188 sorry |
|
189 |
|
190 lemma alpha5_equivp: |
|
191 "equivp alpha_rtrm5" |
|
192 "equivp alpha_rlts" |
|
193 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
|
194 apply (simp_all only: alpha5_reflp) |
|
195 apply (meson alpha5_symp alpha5_transp) |
|
196 apply (meson alpha5_symp alpha5_transp) |
|
197 done |
|
198 |
|
199 quotient_type |
|
200 trm5 = rtrm5 / alpha_rtrm5 |
|
201 and |
|
202 lts = rlts / alpha_rlts |
|
203 by (auto intro: alpha5_equivp) |
|
204 |
|
205 local_setup {* |
|
206 (fn ctxt => ctxt |
|
207 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) |
|
208 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) |
|
209 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
|
210 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
|
211 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
|
212 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
|
213 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
|
214 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) |
|
215 |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) |
|
216 *} |
|
217 print_theorems |
|
218 |
|
219 lemma alpha5_rfv: |
|
220 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
|
221 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
|
222 "(alpha_rbv5 b c \<Longrightarrow> True)" |
|
223 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
|
224 apply(simp_all add: eqvts) |
|
225 apply(simp add: alpha_gen) |
|
226 apply(clarify) |
|
227 apply blast |
|
228 done |
|
229 |
|
230 lemma bv_list_rsp: |
|
231 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
|
232 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
|
233 apply(simp_all) |
|
234 apply(clarify) |
|
235 apply simp |
|
236 done |
|
237 |
|
238 local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} |
|
239 print_theorems |
|
240 |
|
241 local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms rtrm5.exhaust rlts.exhaust} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} |
|
242 thm alpha_bn_rsp |
|
243 |
|
244 lemma [quot_respect]: |
|
245 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
|
246 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
|
247 "(alpha_rlts ===> op =) rbv5 rbv5" |
|
248 "(op = ===> alpha_rtrm5) rVr5 rVr5" |
|
249 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
|
250 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
|
251 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
|
252 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
|
253 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
|
254 "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
|
255 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_bn_rsp) |
|
256 apply (clarify) |
|
257 apply (rule_tac x="0" in exI) |
|
258 apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
259 done |
|
260 |
|
261 |
|
262 lemma |
|
263 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
|
264 by (simp add: bv_list_rsp) |
|
265 |
|
266 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
|
267 |
|
268 instantiation trm5 and lts :: pt |
|
269 begin |
|
270 |
|
271 quotient_definition |
|
272 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5" |
|
273 is |
|
274 "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5" |
|
275 |
|
276 quotient_definition |
|
277 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
278 is |
|
279 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
|
280 |
|
281 instance by default |
|
282 (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) |
|
283 |
|
284 end |
|
285 |
|
286 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
|
287 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
|
288 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
|
289 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] |
|
290 lemmas alpha5_DIS = alpha_dis[quot_lifted] |
|
291 |
|
292 (* why is this not in Isabelle? *) |
|
293 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
|
294 by auto |
|
295 |
|
296 lemma lets_bla: |
|
297 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" |
|
298 apply (simp only: alpha5_INJ bv5) |
|
299 apply simp |
|
300 apply (rule allI) |
|
301 apply (simp_all add: alpha_gen) |
|
302 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) |
|
303 apply (rule impI) |
|
304 apply (rule impI) |
|
305 apply (rule impI) |
|
306 apply (simp add: set_sub) |
|
307 done |
|
308 |
|
309 lemma lets_ok: |
|
310 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
|
311 thm alpha5_INJ |
|
312 apply (simp only: alpha5_INJ) |
|
313 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
314 apply (simp_all add: alpha_gen) |
|
315 apply (simp add: permute_trm5_lts fresh_star_def) |
|
316 apply (simp add: eqvts) |
|
317 done |
|
318 |
|
319 lemma lets_ok3: |
|
320 "x \<noteq> y \<Longrightarrow> |
|
321 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
322 (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
323 apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ) |
|
324 done |
|
325 |
|
326 |
|
327 lemma lets_not_ok1: |
|
328 "x \<noteq> y \<Longrightarrow> |
|
329 (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
330 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
331 apply (simp add: alpha5_INJ alpha_gen) |
|
332 apply (simp add: permute_trm5_lts eqvts) |
|
333 apply (simp add: alpha5_INJ) |
|
334 done |
|
335 |
|
336 lemma lets_nok: |
|
337 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
338 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
339 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
340 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) |
|
341 apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts) |
|
342 done |
|
343 |
|
344 end |