72 |> Local_Theory.note ((bind, []), user_thms) |
72 |> Local_Theory.note ((bind, []), user_thms) |
73 end |
73 end |
74 *} |
74 *} |
75 |
75 |
76 ML {* |
76 ML {* |
77 fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct |
|
78 *} |
|
79 |
|
80 ML {* |
|
81 fun fvbv_rsp_tac induct fvbv_simps ctxt = |
77 fun fvbv_rsp_tac induct fvbv_simps ctxt = |
82 ind_tac induct THEN_ALL_NEW |
78 rel_indtac induct THEN_ALL_NEW |
83 (TRY o rtac @{thm TrueI}) THEN_ALL_NEW |
79 (TRY o rtac @{thm TrueI}) THEN_ALL_NEW |
84 asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
80 asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
85 asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW |
81 asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW |
86 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
82 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
87 asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW |
83 asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW |
90 |
86 |
91 ML {* |
87 ML {* |
92 fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt) |
88 fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt) |
93 fun all_eqvts ctxt = |
89 fun all_eqvts ctxt = |
94 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
90 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
95 val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
|
96 *} |
91 *} |
97 |
92 |
98 ML {* |
93 ML {* |
99 fun constr_rsp_tac inj rsp = |
94 fun constr_rsp_tac inj rsp = |
100 REPEAT o rtac impI THEN' |
95 REPEAT o rtac impI THEN' |
101 simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW |
96 simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW |
102 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
97 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
103 REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW |
98 REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW |
104 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
99 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
105 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
100 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
106 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) |
101 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) |
107 )) |
102 )) |
108 *} |
103 *} |
109 |
104 |
110 (* Testing code |
|
111 local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}] |
|
112 (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*) |
|
113 |
|
114 (*ML {* |
|
115 val rsp_goals = map (const_rsp @{context}) [@{term rbv2}] |
|
116 val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals) |
|
117 val fixed' = distinct (op =) (flat fixed) |
|
118 val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals) |
|
119 *} |
|
120 prove ug: {* user_goal *} |
|
121 ML_prf {* |
|
122 val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)} |
|
123 val fv_simps = @{thms rbv2.simps} |
|
124 *} |
|
125 *) |
|
126 |
|
127 ML {* |
105 ML {* |
128 fun perm_arg arg = |
106 fun perm_arg arg = |
129 let |
107 let |
130 val ty = fastype_of arg |
108 val ty = fastype_of arg |
131 in |
109 in |
148 setmksimps (mksimps []) |
126 setmksimps (mksimps []) |
149 *} |
127 *} |
150 |
128 |
151 ML {* |
129 ML {* |
152 fun alpha_eqvt_tac induct simps ctxt = |
130 fun alpha_eqvt_tac induct simps ctxt = |
153 ind_tac induct THEN_ALL_NEW |
131 rel_indtac induct THEN_ALL_NEW |
154 simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW |
132 simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW |
155 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW |
133 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW |
156 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
134 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
157 asm_full_simp_tac (HOL_ss addsimps |
135 asm_full_simp_tac (HOL_ss addsimps |
158 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW |
136 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW |
159 (split_conjs THEN_ALL_NEW TRY o resolve_tac |
137 (split_conj_tac THEN_ALL_NEW TRY o resolve_tac |
160 @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) |
138 @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) |
161 THEN_ALL_NEW |
139 THEN_ALL_NEW |
162 asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps)) |
140 asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps)) |
163 *} |
141 *} |
164 |
142 |
240 "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b" |
220 "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b" |
241 unfolding equivp_reflp_symp_transp symp_def transp_def |
221 unfolding equivp_reflp_symp_transp symp_def transp_def |
242 by blast |
222 by blast |
243 |
223 |
244 ML {* |
224 ML {* |
245 fun prove_alpha_bn_rsp alphas inducts exhausts inj_dis equivps ctxt (alpha_bn, n) = |
225 fun alpha_bn_rsp_tac simps res exhausts a ctxt = |
246 let |
226 rtac allI THEN_ALL_NEW |
247 val alpha = nth alphas n; |
227 case_rules_tac ctxt a exhausts THEN_ALL_NEW |
248 val ty = domain_type (fastype_of alpha); |
228 asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW |
249 val ([x, y, a], ctxt') = Variable.variant_fixes ["x","y","a"] ctxt; |
229 TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW |
250 val [l, r] = map (fn x => (Free (x, ty))) [x, y] |
230 TRY o eresolve_tac res THEN_ALL_NEW |
251 val lhs = HOLogic.mk_Trueprop (alpha $ l $ r) |
231 asm_full_simp_tac (HOL_ss addsimps simps); |
252 val g1 = |
232 *} |
253 Logic.mk_implies (lhs, |
233 |
254 HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty, |
234 |
255 HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)))); |
235 ML {* |
256 val g2 = |
236 fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt = |
257 Logic.mk_implies (lhs, |
237 let |
258 HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty, |
238 val ty = domain_type (fastype_of alpha_bn); |
259 HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r)))); |
239 val (l, r) = the (AList.lookup (op=) alphas ty); |
|
240 in |
|
241 ([HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)), |
|
242 HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))], ctxt) |
|
243 end |
|
244 *} |
|
245 |
|
246 ML {* |
|
247 fun prove_alpha_bn_rsp alphas ind simps equivps exhausts alpha_bns ctxt = |
|
248 let |
|
249 val ([a], ctxt') = Variable.variant_fixes ["a"] ctxt; |
260 val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps; |
250 val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps; |
261 val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps; |
251 val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps; |
262 fun tac {context, ...} = ( |
252 val ths_loc = prove_by_rel_induct alphas (build_alpha_bn_rsp_gl a) ind |
263 etac (nth inducts n) THEN_ALL_NEW |
253 (alpha_bn_rsp_tac simps (resl @ resr) exhausts a) alpha_bns ctxt |
264 (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW |
254 in |
265 split_conjs THEN_ALL_NEW |
255 Variable.export ctxt' ctxt ths_loc |
266 InductTacs.case_rule_tac context a (nth exhausts n) THEN_ALL_NEW |
256 end |
267 asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW |
257 *} |
268 TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW |
258 |
269 TRY o eresolve_tac (resl @ resr) THEN_ALL_NEW |
259 end |
270 asm_full_simp_tac (HOL_ss addsimps inj_dis) |
|
271 ) 1; |
|
272 val t1 = Goal.prove ctxt [] [] g1 tac; |
|
273 val t2 = Goal.prove ctxt [] [] g2 tac; |
|
274 in |
|
275 Variable.export ctxt' ctxt [t1, t2] |
|
276 end |
|
277 *} |
|
278 |
|
279 |
|
280 end |
|