equal
deleted
inserted
replaced
1 theory Rsp |
1 theory Rsp |
2 imports Abs Tacs |
2 imports Abs Tacs |
3 begin |
3 begin |
4 |
|
5 ML {* |
|
6 fun define_quotient_type args tac ctxt = |
|
7 let |
|
8 val mthd = Method.SIMPLE_METHOD tac |
|
9 val mthdt = Method.Basic (fn _ => mthd) |
|
10 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
|
11 in |
|
12 bymt (Quotient_Type.quotient_type args ctxt) |
|
13 end |
|
14 *} |
|
15 |
4 |
16 ML {* |
5 ML {* |
17 fun const_rsp lthy const = |
6 fun const_rsp lthy const = |
18 let |
7 let |
19 val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy) |
8 val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy) |
45 in |
34 in |
46 case (SINGLE (tac 1) goalstate) of |
35 case (SINGLE (tac 1) goalstate) of |
47 NONE => error "rsp_goal failed" |
36 NONE => error "rsp_goal failed" |
48 | SOME th => prepare_goal (term_of (cprem_of th 1)) |
37 | SOME th => prepare_goal (term_of (cprem_of th 1)) |
49 end |
38 end |
50 *} |
|
51 |
|
52 ML {* |
|
53 fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm |
|
54 *} |
39 *} |
55 |
40 |
56 ML {* |
41 ML {* |
57 fun prove_const_rsp bind consts tac ctxt = |
42 fun prove_const_rsp bind consts tac ctxt = |
58 let |
43 let |
118 apply (rule_tac x="pi \<bullet> pia" in exI) |
103 apply (rule_tac x="pi \<bullet> pia" in exI) |
119 by auto |
104 by auto |
120 |
105 |
121 |
106 |
122 ML {* |
107 ML {* |
123 fun mk_minimal_ss ctxt = |
|
124 Simplifier.context ctxt empty_ss |
|
125 setsubgoaler asm_simp_tac |
|
126 setmksimps (mksimps []) |
|
127 *} |
|
128 |
|
129 ML {* |
|
130 fun alpha_eqvt_tac induct simps ctxt = |
108 fun alpha_eqvt_tac induct simps ctxt = |
131 rel_indtac induct THEN_ALL_NEW |
109 rel_indtac induct THEN_ALL_NEW |
132 simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW |
110 simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW |
133 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW |
111 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW |
134 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
112 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
135 asm_full_simp_tac (HOL_ss addsimps |
113 asm_full_simp_tac (HOL_ss addsimps |
136 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW |
114 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW |
137 (split_conj_tac THEN_ALL_NEW TRY o resolve_tac |
115 (split_conj_tac THEN_ALL_NEW TRY o resolve_tac |
150 val perm_args = map (fn x => perm_arg x $ pi $ x) args |
128 val perm_args = map (fn x => perm_arg x $ pi $ x) args |
151 in |
129 in |
152 (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names) |
130 (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names) |
153 end |
131 end |
154 *} |
132 *} |
155 |
|
156 ML {* fold_map build_alpha_eqvt *} |
|
157 |
133 |
158 ML {* |
134 ML {* |
159 fun build_alpha_eqvts funs tac ctxt = |
135 fun build_alpha_eqvts funs tac ctxt = |
160 let |
136 let |
161 val (gls, names) = fold_map build_alpha_eqvt funs ["p"] |
137 val (gls, names) = fold_map build_alpha_eqvt funs ["p"] |
254 in |
230 in |
255 Variable.export ctxt' ctxt ths_loc |
231 Variable.export ctxt' ctxt ths_loc |
256 end |
232 end |
257 *} |
233 *} |
258 |
234 |
259 end |
235 ML {* |
|
236 fun build_alpha_alpha_bn_gl alphas alpha_bn ctxt = |
|
237 let |
|
238 val ty = domain_type (fastype_of alpha_bn); |
|
239 val (l, r) = the (AList.lookup (op=) alphas ty); |
|
240 in |
|
241 ([alpha_bn $ l $ r], ctxt) |
|
242 end |
|
243 *} |
|
244 |
|
245 ML {* |
|
246 fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt = |
|
247 prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind |
|
248 (fn _ => asm_full_simp_tac (HOL_ss addsimps simps)) alpha_bns ctxt |
|
249 *} |
|
250 |
|
251 ML {* |
|
252 fun build_rsp_gl alphas fnctn ctxt = |
|
253 let |
|
254 val typ = domain_type (fastype_of fnctn); |
|
255 val (argl, argr) = the (AList.lookup (op=) alphas typ); |
|
256 in |
|
257 ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt) |
|
258 end |
|
259 *} |
|
260 |
|
261 ML {* |
|
262 fun fvbv_rsp_tac' simps ctxt = |
|
263 asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
|
264 asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW |
|
265 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
|
266 asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW |
|
267 TRY o blast_tac (claset_of ctxt) |
|
268 *} |
|
269 |
|
270 ML {* |
|
271 fun build_fvbv_rsps alphas ind simps fnctns ctxt = |
|
272 prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt |
|
273 *} |
|
274 |
|
275 end |