180 where |
180 where |
181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
182 |
182 |
183 thm akind_aty_atrm.induct |
183 thm akind_aty_atrm.induct |
184 |
184 |
185 lemma left_ball_regular: |
|
186 assumes a: "EQUIV R" |
|
187 shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P" |
|
188 apply (rule LEFT_RES_FORALL_REGULAR) |
|
189 using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"] |
|
190 apply (simp) |
|
191 done |
|
192 |
|
193 lemma right_bex_regular: |
|
194 assumes a: "EQUIV R" |
|
195 shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P" |
|
196 apply (rule RIGHT_RES_EXISTS_REGULAR) |
|
197 using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"] |
|
198 apply (simp) |
|
199 done |
|
200 |
|
201 lemma ball_respects_refl: |
|
202 fixes P::"'a \<Rightarrow> bool" |
|
203 and x::"'a" |
|
204 assumes a: "EQUIV R2" |
|
205 shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))" |
|
206 apply(rule iffI) |
|
207 apply(rule allI) |
|
208 apply(drule_tac x="\<lambda>y. f x" in bspec) |
|
209 apply(simp add: Respects_def IN_RESPECTS) |
|
210 apply(rule impI) |
|
211 using a EQUIV_REFL_SYM_TRANS[of "R2"] |
|
212 apply(simp add: REFL_def) |
|
213 apply(simp) |
|
214 apply(simp) |
|
215 done |
|
216 |
|
217 ML {* |
185 ML {* |
218 fun ball_simproc rel_eqvs ss redex = |
186 fun ball_reg_eqv_simproc rel_eqvs ss redex = |
219 let |
187 let |
220 val ctxt = Simplifier.the_context ss |
188 val ctxt = Simplifier.the_context ss |
221 val thy = ProofContext.theory_of ctxt |
189 val thy = ProofContext.theory_of ctxt |
222 in |
190 in |
223 case redex of |
191 case redex of |
224 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
192 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
225 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ P1)) => |
193 ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => |
|
194 (let |
|
195 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; |
|
196 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
|
197 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
|
198 val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]); |
|
199 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) |
|
200 in |
|
201 SOME thm |
|
202 end |
|
203 handle _ => NONE |
|
204 ) |
|
205 | _ => NONE |
|
206 end |
|
207 *} |
|
208 |
|
209 ML {* |
|
210 fun ball_reg_eqv_range_simproc rel_eqvs ss redex = |
|
211 let |
|
212 val ctxt = Simplifier.the_context ss |
|
213 val thy = ProofContext.theory_of ctxt |
|
214 in |
|
215 case redex of |
|
216 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
|
217 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => |
226 (let |
218 (let |
227 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; |
219 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; |
228 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
220 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
229 val _ = tracing (Syntax.string_of_term ctxt glc); |
221 val _ = tracing (Syntax.string_of_term ctxt glc); |
230 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
222 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
231 val thm = (@{thm eq_reflection} OF [@{thm ball_respects_refl} OF [eqv]]); |
223 val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); |
232 val R1c = cterm_of @{theory} R1; |
224 val R1c = cterm_of thy R1; |
233 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
225 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
234 val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); |
226 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) |
235 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
227 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
236 val _ = tracing "AAA"; |
228 val _ = tracing "AAA"; |
237 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
229 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
238 val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); |
230 val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); |
239 in |
231 in |
247 *} |
239 *} |
248 |
240 |
249 ML {* |
241 ML {* |
250 fun regularize_tac ctxt rel_eqvs = |
242 fun regularize_tac ctxt rel_eqvs = |
251 let |
243 let |
252 val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs; |
244 val pat1 = [@{term "Ball (Respects R) P"}]; |
253 val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs; |
245 val pat2 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
254 val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2); |
|
255 val pat = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
|
256 val thy = ProofContext.theory_of ctxt |
246 val thy = ProofContext.theory_of ctxt |
257 val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs)) |
247 val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) |
258 in |
248 val simproc2 = Simplifier.simproc_i thy "" pat2 (K (ball_reg_eqv_range_simproc rel_eqvs)) |
259 (ObjectLogic.full_atomize_tac) THEN' |
249 val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2] |
260 (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) THEN' |
250 in |
|
251 ObjectLogic.full_atomize_tac THEN' |
|
252 simp_tac simp_ctxt THEN' |
261 REPEAT_ALL_NEW (FIRST' [ |
253 REPEAT_ALL_NEW (FIRST' [ |
262 (rtac @{thm RIGHT_RES_FORALL_REGULAR}), |
254 rtac @{thm ball_reg_right}, |
263 (rtac @{thm LEFT_RES_EXISTS_REGULAR}), |
255 rtac @{thm bex_reg_left}, |
264 (rtac @{thm left_ball_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
256 resolve_tac (Inductive.get_monos ctxt), |
265 (rtac @{thm right_bex_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
|
266 (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
|
267 (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
|
268 (resolve_tac (Inductive.get_monos ctxt)), |
|
269 rtac @{thm move_forall}, |
257 rtac @{thm move_forall}, |
270 rtac @{thm move_exists}, |
258 rtac @{thm move_exists}, |
271 (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) |
259 simp_tac simp_ctxt |
272 ]) |
260 ]) |
273 end |
261 end |
274 *} |
262 *} |
275 |
263 |
276 ML {* val defs = |
264 ML {* val defs = |
335 val gc = Drule.strip_imp_concl (cprop_of lpi); |
323 val gc = Drule.strip_imp_concl (cprop_of lpi); |
336 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
324 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
337 val te = @{thm eq_reflection} OF [t] |
325 val te = @{thm eq_reflection} OF [t] |
338 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
326 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
339 val tl = Thm.lhs_of ts; |
327 val tl = Thm.lhs_of ts; |
340 (* val _ = rrrt := ts; |
|
341 val _ = rrr1 := ctrm; |
|
342 val _ = rrr2 := tl;*) |
|
343 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
328 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
344 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
329 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
345 (* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
330 (* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
346 in |
331 in |
347 (* Conv.all_conv ctrm*) |
332 (* Conv.all_conv ctrm*) |
376 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
361 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
377 ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *} |
362 ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *} |
378 ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *} |
363 ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *} |
379 ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *} |
364 ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *} |
380 apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *}) |
365 apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *}) |
381 thm FORALL_PRS[symmetric] |
|
382 ML_prf {* |
|
383 fun allex_prs_tac lthy quot = |
|
384 (EqSubst.eqsubst_tac lthy [1] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
|
385 THEN' (quotient_tac quot); |
|
386 *} |
|
387 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
366 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
388 ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} |
367 ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} |
389 ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} |
368 ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} |
390 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
369 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
391 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
370 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |