48 done |
48 done |
49 |
49 |
50 (*lemma alpha5_eqvt: |
50 (*lemma alpha5_eqvt: |
51 "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and> |
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> |
52 (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and> |
53 (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))" |
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 *}) |
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*) |
55 done*) |
56 |
56 |
57 local_setup {* |
57 local_setup {* |
58 (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), |
58 (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), |
73 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
73 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
74 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
74 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
75 apply (simp_all add: alpha5_inj) |
75 apply (simp_all add: alpha5_inj) |
76 apply (erule exE) |
76 apply (erule exE) |
77 apply (rule_tac x="- pi" in exI) |
77 apply (rule_tac x="- pi" in exI) |
|
78 apply (simp add: alpha_gen) |
|
79 apply(simp add: fresh_star_def fresh_minus_perm) |
78 apply clarify |
80 apply clarify |
79 apply (rule conjI) |
81 apply (rule conjI) |
80 apply (erule_tac [!] alpha_gen_compose_sym) |
82 apply (rotate_tac 3) |
81 apply (simp_all add: alpha5_eqvt) |
83 apply (frule_tac p="- pi" in alpha5_eqvt(2)) |
|
84 apply simp |
|
85 apply (rule conjI) |
|
86 apply (rotate_tac 5) |
|
87 apply (frule_tac p="- pi" in alpha5_eqvt(1)) |
|
88 apply simp |
|
89 apply (rotate_tac 6) |
|
90 apply simp |
|
91 apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) |
|
92 apply (simp) |
82 done |
93 done |
83 |
94 |
84 lemma alpha5_transp: |
95 lemma alpha5_transp: |
85 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
96 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
86 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> |
97 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> |
92 apply (simp_all add: alpha5_inj) |
103 apply (simp_all add: alpha5_inj) |
93 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
104 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
94 apply (simp_all add: alpha5_inj) |
105 apply (simp_all add: alpha5_inj) |
95 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
106 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
96 apply (simp_all add: alpha5_inj) |
107 apply (simp_all add: alpha5_inj) |
|
108 defer |
|
109 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
110 apply (simp_all add: alpha5_inj) |
|
111 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
112 apply (simp_all add: alpha5_inj) |
97 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
113 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
|
114 apply (simp add: alpha_gen) |
98 apply clarify |
115 apply clarify |
|
116 apply(simp add: fresh_star_plus) |
99 apply (rule conjI) |
117 apply (rule conjI) |
100 apply (erule alpha_gen_compose_trans) |
118 apply (erule_tac x="- pi \<bullet> rltsaa" in allE) |
101 apply (assumption) |
119 apply (rotate_tac 5) |
102 apply (simp add: alpha5_eqvt) |
120 apply (drule_tac p="- pi" in alpha5_eqvt(2)) |
103 apply (erule alpha_gen_compose_trans) |
121 apply simp |
104 apply (assumption) |
122 apply (drule_tac p="pi" in alpha5_eqvt(2)) |
105 apply (simp add: alpha5_eqvt) |
123 apply simp |
106 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
124 apply (erule_tac x="- pi \<bullet> rtrm5aa" in allE) |
107 apply (simp_all add: alpha5_inj) |
125 apply (rotate_tac 7) |
108 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
126 apply (drule_tac p="- pi" in alpha5_eqvt(1)) |
109 apply (simp_all add: alpha5_inj) |
127 apply simp |
|
128 apply (rotate_tac 3) |
|
129 apply (drule_tac p="pi" in alpha5_eqvt(1)) |
|
130 apply simp |
110 done |
131 done |
111 |
132 |
112 lemma alpha5_equivp: |
133 lemma alpha5_equivp: |
113 "equivp alpha_rtrm5" |
134 "equivp alpha_rtrm5" |
114 "equivp alpha_rlts" |
135 "equivp alpha_rlts" |
144 "(alpha_rbv5 b c \<Longrightarrow> True)" |
165 "(alpha_rbv5 b c \<Longrightarrow> True)" |
145 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
166 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
146 apply(simp_all add: eqvts) |
167 apply(simp_all add: eqvts) |
147 apply(simp add: alpha_gen) |
168 apply(simp add: alpha_gen) |
148 apply(clarify) |
169 apply(clarify) |
149 apply(simp) |
170 apply blast |
150 done |
171 done |
151 |
172 |
152 lemma bv_list_rsp: |
173 lemma bv_list_rsp: |
153 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
174 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
154 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
175 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
232 end |
253 end |
233 |
254 |
234 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
255 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
235 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
256 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
236 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
257 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
237 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
258 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] |
238 lemmas alpha5_DIS = alpha_dis[quot_lifted] |
259 lemmas alpha5_DIS = alpha_dis[quot_lifted] |
|
260 |
|
261 (* why is this not in Isabelle? *) |
|
262 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
|
263 by auto |
239 |
264 |
240 lemma lets_bla: |
265 lemma lets_bla: |
241 "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))" |
266 "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))" |
242 apply (simp only: alpha5_INJ) |
267 apply (simp only: alpha5_INJ bv5) |
243 apply (simp only: bv5) |
|
244 apply simp |
268 apply simp |
245 apply (rule allI) |
269 apply (rule allI) |
246 apply (simp_all add: alpha_gen) |
270 apply (simp_all add: alpha_gen) |
247 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) |
271 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) |
248 apply (rule impI) |
272 apply (rule impI) |
249 apply (rule impI) |
273 apply (rule impI) |
250 sorry (* The assumption is false, so it is true *) |
274 apply (rule impI) |
|
275 apply (simp add: set_sub) |
|
276 done |
251 |
277 |
252 lemma lets_ok: |
278 lemma lets_ok: |
253 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
279 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
254 thm alpha5_INJ |
280 thm alpha5_INJ |
255 apply (simp only: alpha5_INJ) |
281 apply (simp only: alpha5_INJ) |
256 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
282 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
257 apply (simp_all add: alpha_gen) |
283 apply (simp_all add: alpha_gen) |
258 apply (simp add: permute_trm5_lts fresh_star_def) |
284 apply (simp add: permute_trm5_lts fresh_star_def) |
|
285 apply (simp add: eqvts) |
259 done |
286 done |
260 |
287 |
261 lemma lets_ok3: |
288 lemma lets_ok3: |
262 "x \<noteq> y \<Longrightarrow> |
289 "x \<noteq> y \<Longrightarrow> |
263 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
290 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |