30 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
30 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
31 |
31 |
32 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} |
32 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} |
33 thm permute_rtrm1_permute_bp.simps |
33 thm permute_rtrm1_permute_bp.simps |
34 |
34 |
35 local_setup {* |
35 local_setup {* |
36 snd o define_fv_alpha "Terms.rtrm1" |
36 snd o define_fv_alpha "Terms.rtrm1" |
37 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
37 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
38 [[], [[]], [[], []]]] *} |
38 [[], [[]], [[], []]]] *} |
39 |
39 |
40 notation |
40 notation |
118 |
118 |
119 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
119 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
120 (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)) *} |
120 (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)) *} |
121 thm alpha1_equivp |
121 thm alpha1_equivp |
122 |
122 |
123 ML {* |
123 local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] |
124 fun define_quotient_type args tac ctxt = |
124 (rtac @{thm alpha1_equivp(1)} 1) *} |
125 let |
|
126 val mthd = Method.SIMPLE_METHOD tac |
|
127 val mthdt = Method.Basic (fn _ => mthd) |
|
128 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
|
129 in |
|
130 bymt (Quotient_Type.quotient_type args ctxt) |
|
131 end |
|
132 *} |
|
133 |
|
134 local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] |
|
135 (rtac @{thm alpha1_equivp(1)} 1) |
|
136 *} |
|
137 |
125 |
138 local_setup {* |
126 local_setup {* |
139 (fn ctxt => ctxt |
127 (fn ctxt => ctxt |
140 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
128 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
141 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
129 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
143 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
131 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
144 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
132 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
145 *} |
133 *} |
146 print_theorems |
134 print_theorems |
147 |
135 |
148 prove fv_rtrm1_rsp': {* |
136 local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} @{term fv_rtrm1} |
149 (@{term Trueprop} $ (Quotient_Term.equiv_relation_chk @{context} (fastype_of @{term fv_rtrm1}, fastype_of @{term fv_trm1}) $ @{term fv_rtrm1} $ @{term fv_rtrm1})) *} |
137 (fn _ => fv_rsp_tac @{thms alpha_rtrm1_alpha_bp.inducts} @{thms fv_rtrm1_fv_bp.simps} 1) *} |
150 by (tactic {* |
138 local_setup {* prove_const_rsp @{binding rVr1_rsp} @{term rVr1} |
151 (rtac @{thm fun_rel_id} THEN' |
139 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
152 eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW |
140 local_setup {* prove_const_rsp @{binding rAp1_rsp} @{term rAp1} |
153 asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fv_rtrm1_fv_bp.simps})) 1 *}) |
141 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
154 |
142 local_setup {* prove_const_rsp @{binding rLm1_rsp} @{term rLm1} |
155 |
143 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
156 lemmas fv_rtrm1_rsp = apply_rsp'[OF fv_rtrm1_rsp'] |
144 local_setup {* prove_const_rsp @{binding rLt1_rsp} @{term rLt1} |
157 |
145 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
158 (* We need this since 'prove' doesn't support attributes *) |
146 local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"} |
159 lemma [quot_respect]: "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1" |
147 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
160 by (rule fv_rtrm1_rsp') |
|
161 |
|
162 ML {* |
|
163 fun contr_rsp_tac inj rsp equivps = |
|
164 let |
|
165 val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps |
|
166 in |
|
167 REPEAT o rtac @{thm fun_rel_id} THEN' |
|
168 simp_tac (HOL_ss addsimps inj) THEN' |
|
169 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW |
|
170 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
|
171 rtac @{thm exI[of _ "0 :: perm"]} THEN' |
|
172 asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ |
|
173 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
|
174 )) |
|
175 end |
|
176 *} |
|
177 |
|
178 lemma [quot_respect]: |
|
179 "(op = ===> alpha_rtrm1) rVr1 rVr1" |
|
180 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" |
|
181 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" |
|
182 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" |
|
183 apply (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *})+ |
|
184 done |
|
185 |
|
186 |
148 |
187 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
149 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
188 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
150 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
189 |
151 |
190 instantiation trm1 and bp :: pt |
152 instantiation trm1 and bp :: pt |
193 quotient_definition |
155 quotient_definition |
194 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
156 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
195 is |
157 is |
196 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
158 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
197 |
159 |
198 lemma [quot_respect]: |
|
199 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute" |
|
200 by (simp add: alpha1_eqvt) |
|
201 |
|
202 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] |
160 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] |
203 |
161 |
204 instance |
162 instance |
205 apply default |
163 apply default |
206 apply(induct_tac [!] x rule: trm1_bp_inducts(1)) |
164 apply(induct_tac [!] x rule: trm1_bp_inducts(1)) |
207 apply(simp_all) |
165 apply(simp_all) |
208 done |
166 done |
209 |
167 |
210 end |
168 end |
211 |
169 |
212 lemmas fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
170 lemmas |
213 |
171 fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
214 lemmas fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |
172 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |
215 |
173 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
216 lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
217 |
174 |
218 lemma lm1_supp_pre: |
175 lemma lm1_supp_pre: |
219 shows "(supp (atom x, t)) supports (Lm1 x t) " |
176 shows "(supp (atom x, t)) supports (Lm1 x t) " |
220 apply(simp add: supports_def) |
177 apply(simp add: supports_def) |
221 apply(fold fresh_def) |
178 apply(fold fresh_def) |
350 |
307 |
351 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []), |
308 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []), |
352 (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)) *} |
309 (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)) *} |
353 thm alpha2_equivp |
310 thm alpha2_equivp |
354 |
311 |
355 |
312 local_setup {* define_quotient_type |
356 quotient_type |
313 [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})), |
357 trm2 = rtrm2 / alpha_rtrm2 |
314 (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))] |
358 and |
315 ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *} |
359 assign = rassign / alpha_rassign |
|
360 by (rule alpha2_equivp(1)) (rule alpha2_equivp(2)) |
|
361 |
316 |
362 local_setup {* |
317 local_setup {* |
363 (fn ctxt => ctxt |
318 (fn ctxt => ctxt |
364 |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2})) |
319 |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2})) |
365 |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2})) |
320 |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2})) |
368 |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs})) |
323 |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs})) |
369 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) |
324 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) |
370 |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) |
325 |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) |
371 *} |
326 *} |
372 print_theorems |
327 print_theorems |
|
328 |
|
329 (*local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} @{term fv_rtrm2} |
|
330 (fn _ => fv_rsp_tac @{thms alpha_rtrm2_alpha_rassign.inducts} @{thms fv_rtrm2_fv_rassign.simps} 1) *} *) |
|
331 lemma fv_rtrm2_rsp: "x \<approx>2 y \<Longrightarrow> fv_rtrm2 x = fv_rtrm2 y" sorry |
|
332 lemma bv2_rsp: "x \<approx>2b y \<Longrightarrow> rbv2 x = rbv2 y" sorry |
|
333 |
|
334 local_setup {* prove_const_rsp @{binding rVr2_rsp} @{term rVr2} |
|
335 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
|
336 local_setup {* prove_const_rsp @{binding rAp2_rsp} @{term rAp2} |
|
337 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
|
338 local_setup {* prove_const_rsp @{binding rLm2_rsp} @{term rLm2} |
|
339 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
|
340 local_setup {* prove_const_rsp @{binding rLt2_rsp} @{term rLt2} |
|
341 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp bv2_rsp} @{thms alpha2_equivp} 1) *} |
|
342 local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} @{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"} |
|
343 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} |
373 |
344 |
374 |
345 |
375 section {*** lets with many assignments ***} |
346 section {*** lets with many assignments ***} |
376 |
347 |
377 datatype rtrm3 = |
348 datatype rtrm3 = |