| changeset 1225 | 28aaf6d01e10 |
| parent 1222 | 0d059450a3fa |
| child 1227 | ec2e0116779e |
| 1222:0d059450a3fa | 1225:28aaf6d01e10 |
|---|---|
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 |
143 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
143 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
144 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
144 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
145 *} |
145 *} |
146 print_theorems |
146 print_theorems |
147 |
147 |
148 prove fv_rtrm1_rsp': {* |
148 |
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})) *} |
149 ML {* |
150 fun const_rsp const lthy = |
|
151 let |
|
152 val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy) |
|
153 val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty); |
|
154 in |
|
155 HOLogic.mk_Trueprop (rel $ const $ const) |
|
156 end |
|
157 *} |
|
158 |
|
159 (*local_setup {* |
|
160 snd o Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), @{thms refl}) *} *) |
|
161 |
|
162 prove fv_rtrm1_rsp': {* const_rsp @{term fv_rtrm1} @{context} *} |
|
150 by (tactic {* |
163 by (tactic {* |
151 (rtac @{thm fun_rel_id} THEN' |
164 (rtac @{thm fun_rel_id} THEN' |
152 eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW |
165 eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW |
153 asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fv_rtrm1_fv_bp.simps})) 1 *}) |
166 asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fv_rtrm1_fv_bp.simps})) 1 *}) |
154 |
167 |
172 asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ |
185 asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ |
173 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
186 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
174 )) |
187 )) |
175 end |
188 end |
176 *} |
189 *} |
190 |
|
191 ML {* |
|
192 fun remove_alls trm = |
|
193 let |
|
194 val fs = rev (map Free (strip_all_vars trm)) |
|
195 in |
|
196 subst_bounds (fs, (strip_all_body trm)) |
|
197 end |
|
198 *} |
|
199 |
|
200 ML {* |
|
201 fun rsp_goal thy trm = |
|
202 let |
|
203 val goalstate = Goal.init (cterm_of thy trm); |
|
204 val tac = REPEAT o rtac @{thm fun_rel_id}; |
|
205 in |
|
206 case (SINGLE (tac 1) goalstate) of |
|
207 NONE => error "rsp_goal failed" |
|
208 | SOME th => remove_alls (term_of (cprem_of th 1)) |
|
209 end |
|
210 *} |
|
211 |
|
212 prove rAp1_rsp': {* rsp_goal @{theory} (const_rsp @{term rAp1} @{context}) *} |
|
213 by (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *}) |
|
214 |
|
215 thm apply_rsp'[OF apply_rsp'[OF rAp1_rsp']] |
|
216 |
|
177 |
217 |
178 lemma [quot_respect]: |
218 lemma [quot_respect]: |
179 "(op = ===> alpha_rtrm1) rVr1 rVr1" |
219 "(op = ===> alpha_rtrm1) rVr1 rVr1" |
180 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" |
220 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" |
181 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" |
221 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" |