1 theory Terms |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 text {* primrec seems to be genarally faster than fun *} |
|
8 |
|
9 section {*** lets with binding patterns ***} |
|
10 |
|
11 datatype rtrm1 = |
|
12 rVr1 "name" |
|
13 | rAp1 "rtrm1" "rtrm1" |
|
14 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
|
15 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
|
16 and bp = |
|
17 BUnit |
|
18 | BVr "name" |
|
19 | BPr "bp" "bp" |
|
20 |
|
21 print_theorems |
|
22 |
|
23 (* to be given by the user *) |
|
24 |
|
25 primrec |
|
26 bv1 |
|
27 where |
|
28 "bv1 (BUnit) = {}" |
|
29 | "bv1 (BVr x) = {atom x}" |
|
30 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
|
31 |
|
32 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} |
|
33 thm permute_rtrm1_permute_bp.simps |
|
34 |
|
35 local_setup {* |
|
36 snd o define_fv_alpha "Terms.rtrm1" |
|
37 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
|
38 [[], [[]], [[], []]]] *} |
|
39 |
|
40 notation |
|
41 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
|
42 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
|
43 thm alpha_rtrm1_alpha_bp.intros |
|
44 thm fv_rtrm1_fv_bp.simps |
|
45 |
|
46 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *} |
|
47 thm alpha1_inj |
|
48 |
|
49 local_setup {* |
|
50 snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)}) |
|
51 *} |
|
52 |
|
53 local_setup {* |
|
54 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} |
|
55 *} |
|
56 |
|
57 |
|
58 local_setup {* |
|
59 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), |
|
60 build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) |
|
61 *} |
|
62 print_theorems |
|
63 |
|
64 lemma alpha1_eqvt_proper[eqvt]: |
|
65 "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))" |
|
66 "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))" |
|
67 apply (simp_all only: eqvts) |
|
68 apply rule |
|
69 apply (simp_all add: alpha1_eqvt) |
|
70 apply (subst permute_minus_cancel(2)[symmetric,of "t" "pi"]) |
|
71 apply (subst permute_minus_cancel(2)[symmetric,of "s" "pi"]) |
|
72 apply (simp_all only: alpha1_eqvt) |
|
73 apply rule |
|
74 apply (simp_all add: alpha1_eqvt) |
|
75 apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"]) |
|
76 apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"]) |
|
77 apply (simp_all only: alpha1_eqvt) |
|
78 done |
|
79 |
|
80 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
|
81 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} |
|
82 thm alpha1_equivp |
|
83 |
|
84 local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] |
|
85 (rtac @{thm alpha1_equivp(1)} 1) *} |
|
86 |
|
87 local_setup {* |
|
88 (fn ctxt => ctxt |
|
89 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
|
90 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
|
91 |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1})) |
|
92 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
|
93 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
|
94 *} |
|
95 print_theorems |
|
96 |
|
97 thm alpha_rtrm1_alpha_bp.induct |
|
98 local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}] |
|
99 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *} |
|
100 local_setup {* prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}] |
|
101 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
102 local_setup {* prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}] |
|
103 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
104 local_setup {* prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}] |
|
105 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
106 local_setup {* prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}] |
|
107 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
|
108 local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}] |
|
109 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
|
110 |
|
111 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
|
112 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
|
113 |
|
114 setup {* define_lifted_perms ["Terms.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})] |
|
115 @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *} |
|
116 |
|
117 lemmas |
|
118 permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] |
|
119 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
|
120 and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt(1)[quot_lifted] |
|
121 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
122 |
|
123 lemma supports: |
|
124 "(supp (atom x)) supports (Vr1 x)" |
|
125 "(supp t \<union> supp s) supports (Ap1 t s)" |
|
126 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
|
127 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
|
128 "{} supports BUnit" |
|
129 "(supp (atom x)) supports (BVr x)" |
|
130 "(supp a \<union> supp b) supports (BPr a b)" |
|
131 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1) |
|
132 apply(rule_tac [!] allI)+ |
|
133 apply(rule_tac [!] impI) |
|
134 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
|
135 apply(simp_all add: fresh_atom) |
|
136 done |
|
137 |
|
138 lemma rtrm1_bp_fs: |
|
139 "finite (supp (x :: trm1))" |
|
140 "finite (supp (b :: bp))" |
|
141 apply (induct x and b rule: trm1_bp_inducts) |
|
142 apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) |
|
143 apply(simp_all add: supp_atom) |
|
144 done |
|
145 |
|
146 instance trm1 :: fs |
|
147 apply default |
|
148 apply (rule rtrm1_bp_fs(1)) |
|
149 done |
|
150 |
|
151 lemma fv_eq_bv: "fv_bp bp = bv1 bp" |
|
152 apply(induct bp rule: trm1_bp_inducts(2)) |
|
153 apply(simp_all) |
|
154 done |
|
155 |
|
156 lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}" |
|
157 apply auto |
|
158 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI) |
|
159 apply auto |
|
160 done |
|
161 |
|
162 lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)" |
|
163 apply rule |
|
164 apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2)) |
|
165 apply (simp_all add: equivp_reflp[OF alpha1_equivp(2)]) |
|
166 done |
|
167 |
|
168 lemma alpha_bp_eq: "alpha_bp = (op =)" |
|
169 apply (rule ext)+ |
|
170 apply (rule alpha_bp_eq_eq) |
|
171 done |
|
172 |
|
173 lemma supp_fv: |
|
174 "supp t = fv_trm1 t" |
|
175 "supp b = fv_bp b" |
|
176 apply(induct t and b rule: trm1_bp_inducts) |
|
177 apply(simp_all) |
|
178 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
179 apply(simp only: supp_at_base[simplified supp_def]) |
|
180 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
181 apply(simp add: Collect_imp_eq Collect_neg_eq) |
|
182 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") |
|
183 apply(simp add: supp_Abs fv_trm1) |
|
184 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) |
|
185 apply(simp add: alpha1_INJ) |
|
186 apply(simp add: Abs_eq_iff) |
|
187 apply(simp add: alpha_gen.simps) |
|
188 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
|
189 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
|
190 apply(simp add: supp_Abs fv_trm1 fv_eq_bv) |
|
191 apply(simp (no_asm) add: supp_def permute_trm1) |
|
192 apply(simp add: alpha1_INJ alpha_bp_eq) |
|
193 apply(simp add: Abs_eq_iff) |
|
194 apply(simp add: alpha_gen) |
|
195 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
|
196 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2) |
|
197 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
|
198 apply(simp (no_asm) add: supp_def eqvts) |
|
199 apply(fold supp_def) |
|
200 apply(simp add: supp_at_base) |
|
201 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) |
|
202 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) |
|
203 done |
|
204 |
|
205 lemma trm1_supp: |
|
206 "supp (Vr1 x) = {atom x}" |
|
207 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
|
208 "supp (Lm1 x t) = (supp t) - {atom x}" |
|
209 "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)" |
|
210 by (simp_all add: supp_fv fv_trm1 fv_eq_bv) |
|
211 |
|
212 lemma trm1_induct_strong: |
|
213 assumes "\<And>name b. P b (Vr1 name)" |
|
214 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
|
215 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
|
216 and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)" |
|
217 shows "P a rtrma" |
|
218 sorry |
|
219 |
|
220 section {*** lets with single assignments ***} |
|
221 |
|
222 datatype rtrm2 = |
|
223 rVr2 "name" |
|
224 | rAp2 "rtrm2" "rtrm2" |
|
225 | rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)" |
|
226 | rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)" |
|
227 and rassign = |
|
228 rAs "name" "rtrm2" |
|
229 |
|
230 (* to be given by the user *) |
|
231 primrec |
|
232 rbv2 |
|
233 where |
|
234 "rbv2 (rAs x t) = {atom x}" |
|
235 |
|
236 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} |
|
237 |
|
238 local_setup {* snd o define_fv_alpha "Terms.rtrm2" |
|
239 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], |
|
240 [[[], []]]] *} |
|
241 |
|
242 notation |
|
243 alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and |
|
244 alpha_rassign ("_ \<approx>2b _" [100, 100] 100) |
|
245 thm alpha_rtrm2_alpha_rassign.intros |
|
246 |
|
247 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *} |
|
248 thm alpha2_inj |
|
249 |
|
250 lemma alpha2_eqvt: |
|
251 "t \<approx>2 s \<Longrightarrow> (pi \<bullet> t) \<approx>2 (pi \<bullet> s)" |
|
252 "a \<approx>2b b \<Longrightarrow> (pi \<bullet> a) \<approx>2b (pi \<bullet> b)" |
|
253 sorry |
|
254 |
|
255 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []), |
|
256 (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *} |
|
257 thm alpha2_equivp |
|
258 |
|
259 local_setup {* define_quotient_type |
|
260 [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})), |
|
261 (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))] |
|
262 ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *} |
|
263 |
|
264 local_setup {* |
|
265 (fn ctxt => ctxt |
|
266 |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2})) |
|
267 |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2})) |
|
268 |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2})) |
|
269 |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2})) |
|
270 |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs})) |
|
271 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) |
|
272 |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) |
|
273 *} |
|
274 print_theorems |
|
275 |
|
276 local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}] |
|
277 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *} |
|
278 local_setup {* prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}] |
|
279 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *} |
|
280 local_setup {* prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}] |
|
281 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
|
282 local_setup {* prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}] |
|
283 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
|
284 local_setup {* prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}] |
|
285 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
|
286 local_setup {* prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}] |
|
287 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *} |
|
288 local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}] |
|
289 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} |
|
290 |
|
291 |
|
292 section {*** lets with many assignments ***} |
|
293 |
|
294 datatype rtrm3 = |
|
295 rVr3 "name" |
|
296 | rAp3 "rtrm3" "rtrm3" |
|
297 | rLm3 "name" "rtrm3" --"bind (name) in (trm3)" |
|
298 | rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)" |
|
299 and rassigns = |
|
300 rANil |
|
301 | rACons "name" "rtrm3" "rassigns" |
|
302 |
|
303 (* to be given by the user *) |
|
304 primrec |
|
305 bv3 |
|
306 where |
|
307 "bv3 rANil = {}" |
|
308 | "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)" |
|
309 |
|
310 setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *} |
|
311 |
|
312 local_setup {* snd o define_fv_alpha "Terms.rtrm3" |
|
313 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], |
|
314 [[], [[], [], []]]] *} |
|
315 print_theorems |
|
316 |
|
317 notation |
|
318 alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and |
|
319 alpha_rassigns ("_ \<approx>3a _" [100, 100] 100) |
|
320 thm alpha_rtrm3_alpha_rassigns.intros |
|
321 |
|
322 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *} |
|
323 thm alpha3_inj |
|
324 |
|
325 lemma alpha3_eqvt: |
|
326 "t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)" |
|
327 "a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)" |
|
328 sorry |
|
329 |
|
330 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []), |
|
331 (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *} |
|
332 thm alpha3_equivp |
|
333 |
|
334 quotient_type |
|
335 trm3 = rtrm3 / alpha_rtrm3 |
|
336 and |
|
337 assigns = rassigns / alpha_rassigns |
|
338 by (rule alpha3_equivp(1)) (rule alpha3_equivp(2)) |
|
339 |
|
340 |
|
341 section {*** lam with indirect list recursion ***} |
|
342 |
|
343 datatype rtrm4 = |
|
344 rVr4 "name" |
|
345 | rAp4 "rtrm4" "rtrm4 list" |
|
346 | rLm4 "name" "rtrm4" --"bind (name) in (trm)" |
|
347 print_theorems |
|
348 |
|
349 thm rtrm4.recs |
|
350 |
|
351 (* there cannot be a clause for lists, as *) |
|
352 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
|
353 setup {* snd o define_raw_perms ["rtrm4"] ["Terms.rtrm4"] *} |
|
354 |
|
355 (* "repairing" of the permute function *) |
|
356 lemma repaired: |
|
357 fixes ts::"rtrm4 list" |
|
358 shows "permute_rtrm4_list p ts = p \<bullet> ts" |
|
359 apply(induct ts) |
|
360 apply(simp_all) |
|
361 done |
|
362 |
|
363 thm permute_rtrm4_permute_rtrm4_list.simps |
|
364 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
|
365 |
|
366 local_setup {* snd o define_fv_alpha "Terms.rtrm4" [ |
|
367 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} |
|
368 print_theorems |
|
369 |
|
370 notation |
|
371 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
|
372 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
|
373 thm alpha_rtrm4_alpha_rtrm4_list.intros |
|
374 |
|
375 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} |
|
376 thm alpha4_inj |
|
377 thm alpha_rtrm4_alpha_rtrm4_list.induct |
|
378 |
|
379 local_setup {* |
|
380 snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct} |
|
381 *} |
|
382 print_theorems |
|
383 |
|
384 local_setup {* |
|
385 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), |
|
386 build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) |
|
387 *} |
|
388 print_theorems |
|
389 |
|
390 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), |
|
391 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} |
|
392 thm alpha4_equivp |
|
393 |
|
394 quotient_type |
|
395 qrtrm4 = rtrm4 / alpha_rtrm4 and |
|
396 qrtrm4list = "rtrm4 list" / alpha_rtrm4_list |
|
397 by (simp_all add: alpha4_equivp) |
|
398 |
|
399 |
|
400 datatype rtrm5 = |
|
401 rVr5 "name" |
|
402 | rAp5 "rtrm5" "rtrm5" |
|
403 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
|
404 and rlts = |
|
405 rLnil |
|
406 | rLcons "name" "rtrm5" "rlts" |
|
407 |
|
408 primrec |
|
409 rbv5 |
|
410 where |
|
411 "rbv5 rLnil = {}" |
|
412 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
|
413 |
|
414 |
|
415 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} |
|
416 print_theorems |
|
417 |
|
418 local_setup {* snd o define_fv_alpha "Terms.rtrm5" [ |
|
419 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
|
420 print_theorems |
|
421 |
|
422 (* Alternate version with additional binding of name in rlts in rLcons *) |
|
423 (*local_setup {* snd o define_fv_alpha "Terms.rtrm5" [ |
|
424 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} |
|
425 print_theorems*) |
|
426 |
|
427 notation |
|
428 alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and |
|
429 alpha_rlts ("_ \<approx>l _" [100, 100] 100) |
|
430 thm alpha_rtrm5_alpha_rlts.intros |
|
431 |
|
432 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} |
|
433 thm alpha5_inj |
|
434 |
|
435 lemma rbv5_eqvt[eqvt]: |
|
436 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
|
437 apply (induct x) |
|
438 apply (simp_all add: eqvts atom_eqvt) |
|
439 done |
|
440 |
|
441 lemma fv_rtrm5_rlts_eqvt[eqvt]: |
|
442 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
|
443 "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)" |
|
444 apply (induct x and l) |
|
445 apply (simp_all add: eqvts atom_eqvt) |
|
446 done |
|
447 |
|
448 lemma alpha5_eqvt: |
|
449 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
|
450 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
|
451 apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) |
|
452 apply (simp_all add: alpha5_inj) |
|
453 apply (tactic {* |
|
454 ALLGOALS ( |
|
455 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
|
456 (etac @{thm alpha_gen_compose_eqvt}) |
|
457 ) *}) |
|
458 apply (simp_all only: eqvts atom_eqvt) |
|
459 done |
|
460 |
|
461 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), |
|
462 (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *} |
|
463 thm alpha5_equivp |
|
464 |
|
465 quotient_type |
|
466 trm5 = rtrm5 / alpha_rtrm5 |
|
467 and |
|
468 lts = rlts / alpha_rlts |
|
469 by (auto intro: alpha5_equivp) |
|
470 |
|
471 local_setup {* |
|
472 (fn ctxt => ctxt |
|
473 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) |
|
474 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) |
|
475 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
|
476 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
|
477 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
|
478 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
|
479 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
|
480 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) |
|
481 *} |
|
482 print_theorems |
|
483 |
|
484 lemma alpha5_rfv: |
|
485 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
|
486 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
|
487 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
|
488 apply(simp_all add: alpha_gen) |
|
489 done |
|
490 |
|
491 lemma bv_list_rsp: |
|
492 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
|
493 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) |
|
494 apply(simp_all) |
|
495 done |
|
496 |
|
497 lemma [quot_respect]: |
|
498 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
|
499 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
|
500 "(alpha_rlts ===> op =) rbv5 rbv5" |
|
501 "(op = ===> alpha_rtrm5) rVr5 rVr5" |
|
502 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
|
503 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
|
504 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
|
505 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
|
506 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
|
507 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
|
508 apply (clarify) apply (rule conjI) |
|
509 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
510 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
511 done |
|
512 |
|
513 lemma |
|
514 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
|
515 by (simp add: bv_list_rsp) |
|
516 |
|
517 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
|
518 |
|
519 instantiation trm5 and lts :: pt |
|
520 begin |
|
521 |
|
522 quotient_definition |
|
523 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5" |
|
524 is |
|
525 "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5" |
|
526 |
|
527 quotient_definition |
|
528 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
529 is |
|
530 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
|
531 |
|
532 instance by default |
|
533 (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) |
|
534 |
|
535 end |
|
536 |
|
537 lemmas |
|
538 permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
|
539 and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
540 and bv5[simp] = rbv5.simps[quot_lifted] |
|
541 and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
|
542 |
|
543 lemma lets_ok: |
|
544 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
|
545 apply (subst alpha5_INJ) |
|
546 apply (rule conjI) |
|
547 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
548 apply (simp only: alpha_gen) |
|
549 apply (simp add: permute_trm5_lts fresh_star_def) |
|
550 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
551 apply (simp only: alpha_gen) |
|
552 apply (simp add: permute_trm5_lts fresh_star_def) |
|
553 done |
|
554 |
|
555 lemma lets_ok2: |
|
556 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
|
557 (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
558 apply (subst alpha5_INJ) |
|
559 apply (rule conjI) |
|
560 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
561 apply (simp only: alpha_gen) |
|
562 apply (simp add: permute_trm5_lts fresh_star_def) |
|
563 apply (rule_tac x="0 :: perm" in exI) |
|
564 apply (simp only: alpha_gen) |
|
565 apply (simp add: permute_trm5_lts fresh_star_def) |
|
566 done |
|
567 |
|
568 |
|
569 lemma lets_not_ok1: |
|
570 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
571 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
572 apply (simp add: alpha5_INJ(3) alpha_gen) |
|
573 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1)) |
|
574 done |
|
575 |
|
576 lemma distinct_helper: |
|
577 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
|
578 apply auto |
|
579 apply (erule alpha_rtrm5.cases) |
|
580 apply (simp_all only: rtrm5.distinct) |
|
581 done |
|
582 |
|
583 lemma distinct_helper2: |
|
584 shows "(Vr5 x) \<noteq> (Ap5 y z)" |
|
585 by (lifting distinct_helper) |
|
586 |
|
587 lemma lets_nok: |
|
588 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
589 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
590 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
591 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) |
|
592 apply (simp add: distinct_helper2) |
|
593 done |
|
594 |
|
595 |
|
596 (* example with a bn function defined over the type itself *) |
|
597 datatype rtrm6 = |
|
598 rVr6 "name" |
|
599 | rLm6 "name" "rtrm6" --"bind name in rtrm6" |
|
600 | rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" |
|
601 |
|
602 primrec |
|
603 rbv6 |
|
604 where |
|
605 "rbv6 (rVr6 n) = {}" |
|
606 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t" |
|
607 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
|
608 |
|
609 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} |
|
610 print_theorems |
|
611 |
|
612 local_setup {* snd o define_fv_alpha "Terms.rtrm6" [ |
|
613 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} |
|
614 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100) |
|
615 (* HERE THE RULES DIFFER *) |
|
616 thm alpha_rtrm6.intros |
|
617 |
|
618 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} |
|
619 thm alpha6_inj |
|
620 |
|
621 local_setup {* |
|
622 snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}) |
|
623 *} |
|
624 |
|
625 local_setup {* |
|
626 snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct} |
|
627 *} |
|
628 |
|
629 local_setup {* |
|
630 (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), |
|
631 build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) |
|
632 *} |
|
633 |
|
634 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), |
|
635 (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} |
|
636 thm alpha6_equivp |
|
637 |
|
638 quotient_type |
|
639 trm6 = rtrm6 / alpha_rtrm6 |
|
640 by (auto intro: alpha6_equivp) |
|
641 |
|
642 local_setup {* |
|
643 (fn ctxt => ctxt |
|
644 |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6})) |
|
645 |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6})) |
|
646 |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6})) |
|
647 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6})) |
|
648 |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6}))) |
|
649 *} |
|
650 print_theorems |
|
651 |
|
652 lemma [quot_respect]: |
|
653 "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute" |
|
654 by (auto simp add: alpha6_eqvt) |
|
655 |
|
656 (* Definitely not true , see lemma below *) |
|
657 lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6" |
|
658 apply simp apply clarify |
|
659 apply (erule alpha_rtrm6.induct) |
|
660 oops |
|
661 |
|
662 lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha_rtrm6 ===> op =) rbv6 rbv6" |
|
663 apply simp |
|
664 apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI) |
|
665 apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI) |
|
666 apply simp |
|
667 apply (simp add: alpha6_inj) |
|
668 apply (rule_tac x="(a \<leftrightarrow> b)" in exI) |
|
669 apply (simp add: alpha_gen fresh_star_def) |
|
670 apply (simp add: alpha6_inj) |
|
671 done |
|
672 |
|
673 lemma fv6_rsp: "x \<approx>6 y \<Longrightarrow> fv_rtrm6 x = fv_rtrm6 y" |
|
674 apply (induct_tac x y rule: alpha_rtrm6.induct) |
|
675 apply simp_all |
|
676 apply (erule exE) |
|
677 apply (simp_all add: alpha_gen) |
|
678 done |
|
679 |
|
680 lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6" |
|
681 by (simp add: fv6_rsp) |
|
682 |
|
683 lemma [quot_respect]: |
|
684 "(op = ===> alpha_rtrm6) rVr6 rVr6" |
|
685 "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6" |
|
686 apply auto |
|
687 apply (simp_all add: alpha6_inj) |
|
688 apply (rule_tac x="0::perm" in exI) |
|
689 apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm) |
|
690 done |
|
691 |
|
692 lemma [quot_respect]: |
|
693 "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6" |
|
694 apply auto |
|
695 apply (simp_all add: alpha6_inj) |
|
696 apply (rule_tac [!] x="0::perm" in exI) |
|
697 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm) |
|
698 (* needs rbv6_rsp *) |
|
699 oops |
|
700 |
|
701 instantiation trm6 :: pt begin |
|
702 |
|
703 quotient_definition |
|
704 "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6" |
|
705 is |
|
706 "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6" |
|
707 |
|
708 instance |
|
709 apply default |
|
710 sorry |
|
711 end |
|
712 |
|
713 lemma lifted_induct: |
|
714 "\<lbrakk>x1 = x2; \<And>name namea. name = namea \<Longrightarrow> P (Vr6 name) (Vr6 namea); |
|
715 \<And>name rtrm6 namea rtrm6a. |
|
716 \<lbrakk>True; |
|
717 \<exists>pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \<and> |
|
718 (fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk> |
|
719 \<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a); |
|
720 \<And>rtrm61 rtrm61a rtrm62 rtrm62a. |
|
721 \<lbrakk>rtrm61 = rtrm61a; P rtrm61 rtrm61a; |
|
722 \<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and> |
|
723 (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk> |
|
724 \<Longrightarrow> P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\<rbrakk> |
|
725 \<Longrightarrow> P x1 x2" |
|
726 apply (lifting alpha_rtrm6.induct[unfolded alpha_gen]) |
|
727 apply injection |
|
728 (* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) |
|
729 oops |
|
730 |
|
731 lemma lifted_inject_a3: |
|
732 "(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) = |
|
733 (rtrm61 = rtrm61a \<and> |
|
734 (\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and> |
|
735 (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a))" |
|
736 apply(lifting alpha6_inj(3)[unfolded alpha_gen]) |
|
737 apply injection |
|
738 (* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) |
|
739 oops |
|
740 |
|
741 |
|
742 |
|
743 |
|
744 (* example with a respectful bn function defined over the type itself *) |
|
745 |
|
746 datatype rtrm7 = |
|
747 rVr7 "name" |
|
748 | rLm7 "name" "rtrm7" --"bind left in right" |
|
749 | rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)" |
|
750 |
|
751 primrec |
|
752 rbv7 |
|
753 where |
|
754 "rbv7 (rVr7 n) = {atom n}" |
|
755 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" |
|
756 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r" |
|
757 |
|
758 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} |
|
759 thm permute_rtrm7.simps |
|
760 |
|
761 local_setup {* snd o define_fv_alpha "Terms.rtrm7" [ |
|
762 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} |
|
763 print_theorems |
|
764 notation |
|
765 alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100) |
|
766 (* HERE THE RULES DIFFER *) |
|
767 thm alpha_rtrm7.intros |
|
768 thm fv_rtrm7.simps |
|
769 inductive |
|
770 alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100) |
|
771 where |
|
772 a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)" |
|
773 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s" |
|
774 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2" |
|
775 |
|
776 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7" |
|
777 apply simp |
|
778 apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) |
|
779 apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) |
|
780 apply simp |
|
781 apply (rule a3) |
|
782 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
783 apply (simp_all add: alpha_gen fresh_star_def) |
|
784 apply (rule a1) |
|
785 apply (rule refl) |
|
786 done |
|
787 |
|
788 |
|
789 |
|
790 |
|
791 |
|
792 datatype rfoo8 = |
|
793 Foo0 "name" |
|
794 | Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo" |
|
795 and rbar8 = |
|
796 Bar0 "name" |
|
797 | Bar1 "name" "name" "rbar8" --"bind second name in b" |
|
798 |
|
799 primrec |
|
800 rbv8 |
|
801 where |
|
802 "rbv8 (Bar0 x) = {}" |
|
803 | "rbv8 (Bar1 v x b) = {atom v}" |
|
804 |
|
805 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} |
|
806 print_theorems |
|
807 |
|
808 local_setup {* snd o define_fv_alpha "Terms.rfoo8" [ |
|
809 [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
|
810 notation |
|
811 alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and |
|
812 alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100) |
|
813 (* HERE THE RULE DIFFERS *) |
|
814 thm alpha_rfoo8_alpha_rbar8.intros |
|
815 |
|
816 |
|
817 inductive |
|
818 alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100) |
|
819 and |
|
820 alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100) |
|
821 where |
|
822 a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)" |
|
823 | a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)" |
|
824 | a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2" |
|
825 | a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2" |
|
826 |
|
827 lemma "(alpha8b ===> op =) rbv8 rbv8" |
|
828 apply simp apply clarify |
|
829 apply (erule alpha8f_alpha8b.inducts(2)) |
|
830 apply (simp_all) |
|
831 done |
|
832 |
|
833 lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y" |
|
834 apply (erule alpha8f_alpha8b.inducts(2)) |
|
835 apply (simp_all add: alpha_gen) |
|
836 done |
|
837 lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8" |
|
838 apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp) |
|
839 done |
|
840 |
|
841 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" |
|
842 apply simp apply clarify |
|
843 apply (erule alpha8f_alpha8b.inducts(1)) |
|
844 apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) |
|
845 done |
|
846 |
|
847 |
|
848 |
|
849 |
|
850 |
|
851 |
|
852 datatype rlam9 = |
|
853 Var9 "name" |
|
854 | Lam9 "name" "rlam9" --"bind name in rlam" |
|
855 and rbla9 = |
|
856 Bla9 "rlam9" "rlam9" --"bind bv(first) in second" |
|
857 |
|
858 primrec |
|
859 rbv9 |
|
860 where |
|
861 "rbv9 (Var9 x) = {}" |
|
862 | "rbv9 (Lam9 x b) = {atom x}" |
|
863 |
|
864 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} |
|
865 print_theorems |
|
866 |
|
867 local_setup {* snd o define_fv_alpha "Terms.rlam9" [ |
|
868 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} |
|
869 notation |
|
870 alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and |
|
871 alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100) |
|
872 (* HERE THE RULES DIFFER *) |
|
873 thm alpha_rlam9_alpha_rbla9.intros |
|
874 |
|
875 |
|
876 inductive |
|
877 alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100) |
|
878 and |
|
879 alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100) |
|
880 where |
|
881 a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)" |
|
882 | a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2" |
|
883 | a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2" |
|
884 |
|
885 quotient_type |
|
886 lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b |
|
887 sorry |
|
888 |
|
889 local_setup {* |
|
890 (fn ctxt => ctxt |
|
891 |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9})) |
|
892 |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9})) |
|
893 |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9})) |
|
894 |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9})) |
|
895 |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9})) |
|
896 |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9}))) |
|
897 *} |
|
898 print_theorems |
|
899 |
|
900 instantiation lam9 and bla9 :: pt |
|
901 begin |
|
902 |
|
903 quotient_definition |
|
904 "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9" |
|
905 is |
|
906 "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9" |
|
907 |
|
908 quotient_definition |
|
909 "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9" |
|
910 is |
|
911 "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9" |
|
912 |
|
913 instance |
|
914 sorry |
|
915 |
|
916 end |
|
917 |
|
918 lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk> |
|
919 \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2" |
|
920 apply (lifting a3[unfolded alpha_gen]) |
|
921 apply injection |
|
922 sorry |
|
923 |
|
924 |
|
925 |
|
926 |
|
927 |
|
928 |
|
929 |
|
930 |
|
931 text {* type schemes *} |
|
932 datatype ty = |
|
933 Var "name" |
|
934 | Fun "ty" "ty" |
|
935 |
|
936 setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *} |
|
937 print_theorems |
|
938 |
|
939 datatype tyS = |
|
940 All "name set" "ty" |
|
941 |
|
942 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *} |
|
943 print_theorems |
|
944 |
|
945 local_setup {* snd o define_fv_alpha "Terms.ty" [[[[]], [[], []]]] *} |
|
946 print_theorems |
|
947 |
|
948 (* |
|
949 Doesnot work yet since we do not refer to fv_ty |
|
950 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *} |
|
951 print_theorems |
|
952 *) |
|
953 |
|
954 primrec |
|
955 fv_tyS |
|
956 where |
|
957 "fv_tyS (All xs T) = (fv_ty T - atom ` xs)" |
|
958 |
|
959 inductive |
|
960 alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100) |
|
961 where |
|
962 a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2)) |
|
963 \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2" |
|
964 |
|
965 lemma |
|
966 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))" |
|
967 apply(rule a1) |
|
968 apply(simp add: alpha_gen) |
|
969 apply(rule_tac x="0::perm" in exI) |
|
970 apply(simp add: fresh_star_def) |
|
971 done |
|
972 |
|
973 lemma |
|
974 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))" |
|
975 apply(rule a1) |
|
976 apply(simp add: alpha_gen) |
|
977 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
|
978 apply(simp add: fresh_star_def) |
|
979 done |
|
980 |
|
981 lemma |
|
982 shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))" |
|
983 apply(rule a1) |
|
984 apply(simp add: alpha_gen) |
|
985 apply(rule_tac x="0::perm" in exI) |
|
986 apply(simp add: fresh_star_def) |
|
987 done |
|
988 |
|
989 lemma |
|
990 assumes a: "a \<noteq> b" |
|
991 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))" |
|
992 using a |
|
993 apply(clarify) |
|
994 apply(erule alpha_tyS.cases) |
|
995 apply(simp add: alpha_gen) |
|
996 apply(erule conjE)+ |
|
997 apply(erule exE) |
|
998 apply(erule conjE)+ |
|
999 apply(clarify) |
|
1000 apply(simp) |
|
1001 apply(simp add: fresh_star_def) |
|
1002 apply(auto) |
|
1003 done |
|
1004 |
|
1005 |
|
1006 end |
|