178 quotient_def |
178 quotient_def |
179 perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
179 perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
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 |
|
184 |
|
185 |
|
186 |
|
187 |
|
188 |
|
189 |
|
190 |
|
191 |
|
192 ML {* val defs = |
183 ML {* val defs = |
193 @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def |
184 @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def |
194 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
185 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
195 *} |
186 *} |
196 ML {* val consts = lookup_quot_consts defs *} |
187 ML {* val consts = lookup_quot_consts defs *} |
197 |
188 |
198 thm akind_aty_atrm.induct |
189 thm akind_aty_atrm.induct |
199 |
190 |
200 ML {* |
191 lemma left_ball_regular: |
201 fun regularize_monos_tac lthy eqvs = |
192 assumes a: "EQUIV R" |
202 let |
193 shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P" |
203 val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) eqvs |
194 apply (rule LEFT_RES_FORALL_REGULAR) |
204 val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) eqvs |
195 using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"] |
205 in |
196 apply (simp) |
206 REPEAT_ALL_NEW (FIRST' [ |
|
207 (rtac @{thm impI} THEN' atac), |
|
208 (rtac @{thm my_equiv_res_forallR}), |
|
209 (rtac @{thm my_equiv_res_forallL}), |
|
210 (rtac @{thm Set.imp_mono}), |
|
211 (resolve_tac (Inductive.get_monos lthy)), |
|
212 (EqSubst.eqsubst_tac lthy [0] (subs1 @ subs2)) |
|
213 ]) |
|
214 end |
|
215 *} |
|
216 |
|
217 ML {* |
|
218 val subs1 = map (fn x => @{thm eq_reflection} OF [@{thm equiv_res_forall} OF [x]]) @{thms alpha_EQUIVs} |
|
219 *} |
|
220 |
|
221 ML {* |
|
222 fun regularize_tac ctxt rel_eqvs rel_refls = |
|
223 let |
|
224 val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs |
|
225 val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs |
|
226 in |
|
227 (ObjectLogic.full_atomize_tac) THEN' |
|
228 REPEAT_ALL_NEW (FIRST' [ |
|
229 FIRST' (map rtac rel_refls), |
|
230 atac, |
|
231 rtac @{thm universal_twice}, |
|
232 rtac @{thm impI} THEN' atac, |
|
233 rtac @{thm implication_twice}, |
|
234 EqSubst.eqsubst_tac ctxt [0] (subs1 @ subs2), |
|
235 (* For a = b \<longrightarrow> a \<approx> b *) |
|
236 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
237 ]) |
|
238 end |
|
239 *} |
|
240 thm RIGHT_RES_FORALL_REGULAR |
|
241 thm my_equiv_res_forallR |
|
242 |
|
243 (* |
|
244 lemma "\<And>i j xb\<Colon>trm \<Rightarrow> trm \<Rightarrow> bool. Respects (atrm ===> atrm ===> op =) xb \<Longrightarrow> (\<forall>m\<Colon>trm \<Rightarrow> trm\<in>Respects (atrm ===> atrm). xb (Const i) (m (Const j))) \<longrightarrow> (\<forall>m\<Colon>trm \<Rightarrow> trm. xb (Const i) (m (Const j)))" |
|
245 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
246 apply (metis COMBK_def al_refl(3)) |
|
247 *) |
|
248 |
|
249 lemma move_quant: "((\<forall>y. \<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>y. \<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))" |
|
250 by auto |
|
251 |
|
252 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
|
253 apply(auto) |
|
254 done |
197 done |
255 |
198 |
256 lemma test: |
199 lemma right_bex_regular: |
257 fixes P Q::"'a \<Rightarrow> bool" |
200 assumes a: "EQUIV R" |
|
201 shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P" |
|
202 apply (rule RIGHT_RES_EXISTS_REGULAR) |
|
203 using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"] |
|
204 apply (simp) |
|
205 done |
|
206 |
|
207 lemma ball_respects_refl: |
|
208 fixes P::"'a \<Rightarrow> bool" |
258 and x::"'a" |
209 and x::"'a" |
259 assumes a: "REFL R2" |
210 assumes a: "EQUIV R2" |
260 and b: "\<And>f. Q (f x) \<longrightarrow> P (f x)" |
211 shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))" |
261 shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>f. P (f x)))" |
212 apply(rule iffI) |
262 apply(rule impI) |
|
263 apply(rule allI) |
213 apply(rule allI) |
264 apply(drule_tac x="\<lambda>y. f x" in bspec) |
214 apply(drule_tac x="\<lambda>y. f x" in bspec) |
265 apply(simp add: Respects_def IN_RESPECTS) |
215 apply(simp add: Respects_def IN_RESPECTS) |
266 apply(rule impI) |
216 apply(rule impI) |
267 using a |
217 using a EQUIV_REFL_SYM_TRANS[of "R2"] |
268 apply(simp add: REFL_def) |
218 apply(simp add: REFL_def) |
269 using b |
219 apply(simp) |
270 apply(simp) |
220 apply(simp) |
271 done |
221 done |
|
222 |
|
223 ML {* |
|
224 fun ball_simproc rel_eqvs ss redex = |
|
225 let |
|
226 val ctxt = Simplifier.the_context ss |
|
227 val thy = ProofContext.theory_of ctxt |
|
228 in |
|
229 case redex of |
|
230 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
|
231 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ P1)) => |
|
232 (let |
|
233 val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; |
|
234 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
|
235 val _ = tracing (Syntax.string_of_term ctxt glc); |
|
236 val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
|
237 val thm = (@{thm eq_reflection} OF [@{thm ball_respects_refl} OF [eqv]]); |
|
238 val R1c = cterm_of @{theory} R1; |
|
239 val thmi = Drule.instantiate' [] [SOME R1c] thm; |
|
240 val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); |
|
241 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
|
242 val _ = tracing "AAA"; |
|
243 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
|
244 val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); |
|
245 in |
|
246 SOME thm2 |
|
247 end |
|
248 handle _ => NONE |
|
249 |
|
250 ) |
|
251 | _ => NONE |
|
252 end |
|
253 *} |
|
254 |
|
255 ML {* |
|
256 fun regularize_tac ctxt rel_eqvs = |
|
257 let |
|
258 val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs; |
|
259 val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs; |
|
260 val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2); |
|
261 val pat = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
|
262 val thy = ProofContext.theory_of ctxt |
|
263 val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs)) |
|
264 in |
|
265 (ObjectLogic.full_atomize_tac) THEN' |
|
266 (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) |
|
267 THEN' |
|
268 REPEAT_ALL_NEW (FIRST' [ |
|
269 (rtac @{thm RIGHT_RES_FORALL_REGULAR}), |
|
270 (rtac @{thm LEFT_RES_EXISTS_REGULAR}), |
|
271 (rtac @{thm left_ball_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
|
272 (rtac @{thm right_bex_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
|
273 (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
|
274 (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
|
275 (resolve_tac (Inductive.get_monos ctxt)), |
|
276 rtac @{thm move_forall}, |
|
277 rtac @{thm move_exists} |
|
278 ]) |
|
279 end |
|
280 *} |
|
281 |
272 |
282 |
273 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K'); |
283 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K'); |
274 \<And>A A' K x x' K'. |
284 \<And>A A' K x x' K'. |
275 \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> |
285 \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> |
276 \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K'); |
286 \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K'); |
287 \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> |
297 \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> |
288 \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk> |
298 \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk> |
289 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
299 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
290 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
300 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
291 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
301 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
|
302 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
|
303 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
304 |
|
305 apply(rule LEFT_RES_FORALL_REGULAR) |
292 apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *}) |
306 apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *}) |
293 apply(atomize (full)) |
307 apply(atomize (full)) |
294 apply(rule RIGHT_RES_FORALL_REGULAR) |
308 apply(rule RIGHT_RES_FORALL_REGULAR) |
295 apply(rule RIGHT_RES_FORALL_REGULAR) |
309 apply(rule RIGHT_RES_FORALL_REGULAR) |
296 apply(rule RIGHT_RES_FORALL_REGULAR) |
310 apply(rule RIGHT_RES_FORALL_REGULAR) |
297 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
|
298 apply(rule test) |
311 apply(rule test) |
299 defer |
312 defer |
300 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
313 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+ |
301 apply(rule test) |
314 apply(rule test) |
302 defer |
315 defer |