177 |
177 |
178 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
178 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
179 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *} |
179 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *} |
180 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
180 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
181 |
181 |
|
182 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
|
183 |
182 local_setup {* |
184 local_setup {* |
183 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
185 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
184 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
186 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
185 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |
187 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |
186 Quotient.note (@{binding "a1"}, a1) #> snd #> |
188 Quotient.note (@{binding "a1"}, a1) #> snd #> |
187 Quotient.note (@{binding "a2"}, a2) #> snd #> |
189 Quotient.note (@{binding "a2"}, a2) #> snd #> |
188 Quotient.note (@{binding "a3"}, a3) #> snd |
190 Quotient.note (@{binding "a3"}, a3) #> snd #> |
|
191 Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd |
189 *} |
192 *} |
190 |
193 |
191 thm alpha.cases |
194 thm alpha.cases |
|
195 thm alpha_cases |
192 |
196 |
193 thm rlam.inject |
197 thm rlam.inject |
194 thm pi_var |
198 thm pi_var |
195 |
199 |
196 lemma var_inject: |
200 lemma var_inject: |
215 |
219 |
216 |
220 |
217 |
221 |
218 |
222 |
219 |
223 |
220 |
|
221 lemma get_rid: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))" |
|
222 apply (auto) |
|
223 done |
|
224 |
|
225 lemma get_rid2: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
|
226 apply (auto) |
|
227 done |
|
228 |
|
229 ML {* val t_a = atomize_thm @{thm alpha.cases} *} |
224 ML {* val t_a = atomize_thm @{thm alpha.cases} *} |
230 prove {* build_regularize_goal t_a rty rel @{context} *} |
|
231 ML_prf {* fun tac ctxt = |
|
232 (FIRST' [ |
|
233 rtac rel_refl, |
|
234 atac, |
|
235 rtac @{thm get_rid}, |
|
236 rtac @{thm get_rid2}, |
|
237 (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
|
238 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
239 (@{thm equiv_res_exists} OF [rel_eqv])]) i)), |
|
240 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl) |
|
241 ]); |
|
242 *} |
|
243 apply (atomize(full)) |
|
244 apply (tactic {* tac @{context} 1 *}) |
|
245 apply (rule get_rid) |
|
246 apply (rule get_rid) |
|
247 apply (rule get_rid2) |
|
248 apply (simp) |
|
249 apply (rule get_rid) |
|
250 apply (rule get_rid2) |
|
251 apply (rule get_rid) |
|
252 apply (rule get_rid2) |
|
253 apply (rule impI) |
|
254 apply (simp) |
|
255 apply (tactic {* tac @{context} 1 *}) |
|
256 apply (rule get_rid2) |
|
257 apply (rule impI) |
|
258 apply (simp) |
|
259 apply (tactic {* tac @{context} 1 *}) |
|
260 apply (simp) |
|
261 apply (rule get_rid2) |
|
262 apply (rule get_rid) |
|
263 apply (rule get_rid) |
|
264 apply (rule get_rid) |
|
265 apply (rule get_rid2) |
|
266 apply (rule impI) |
|
267 apply (simp) |
|
268 apply (tactic {* tac @{context} 1 *}) |
|
269 apply (rule get_rid) |
|
270 apply (rule get_rid2) |
|
271 |
|
272 |
|
273 apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *}) |
|
274 ML_prf {* |
|
275 fun focus_compose t = Subgoal.FOCUS (fn {concl, ...} => |
|
276 rtac t 1) |
|
277 *} |
|
278 thm spec[of _ "x"] |
|
279 apply (rule allI) |
|
280 apply (drule_tac x="a2" in spec) |
|
281 apply (rule impI) |
|
282 apply (erule impE) |
|
283 apply (assumption) |
|
284 apply (rule allI) |
|
285 apply (drule_tac x="P" in spec) |
|
286 apply (atomize(full)) |
|
287 apply (rule allI) |
|
288 apply (rule allI) |
|
289 apply (rule allI) |
|
290 apply (rule impI) |
|
291 apply (rule get_rid2) |
|
292 |
|
293 thm get_rid2 |
|
294 apply (tactic {* compose_tac (false, @{thm get_rid2}, 0) 1 *}) |
|
295 |
|
296 thm spec |
|
297 |
|
298 ML_prf {* val t = snd (Subgoal.focus @{context} 1 (Isar.goal ())) *} |
|
299 ML_prf {* Seq.pull (compose_tac (false, @{thm get_rid}, 2) 1 t) *} |
|
300 |
|
301 |
|
302 thm get_rid |
|
303 apply (rule allI) |
|
304 apply (drule spec) |
|
305 |
|
306 thm spec |
|
307 apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *}) |
|
308 |
|
309 apply (tactic {* tac @{context} 1 *}) |
|
310 apply (tactic {* tac @{context} 1 *}) |
|
311 apply (rule impI) |
|
312 apply (erule impE) |
|
313 apply (assumption) |
|
314 apply (tactic {* tac @{context} 1 *}) |
|
315 apply (rule impI) |
|
316 apply (erule impE) |
|
317 apply (tactic {* tac @{context} 1 *}) |
|
318 apply (tactic {* tac @{context} 1 *}) |
|
319 apply (tactic {* tac @{context} 1 *}) |
|
320 apply (tactic {* tac @{context} 1 *}) |
|
321 |
|
322 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
225 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
323 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
226 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
|
227 ML {* val abs = findabs rty (prop_of t_a); *} |
|
228 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
324 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
229 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
325 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
230 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
326 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym |
231 ML {* val defs_sym = add_lower_defs @{context} defs; *} |
327 |
232 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *} |
|
233 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
|
234 ML {* ObjectLogic.rulify t_r *} |
328 |
235 |
329 |
236 |
330 |
237 |
331 fun |
238 fun |
332 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
239 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
356 apply (simp only: option_map.simps) |
263 apply (simp only: option_map.simps) |
357 apply (subst option_rel.simps) |
264 apply (subst option_rel.simps) |
358 (* Simp starts hanging so don't know how to continue *) |
265 (* Simp starts hanging so don't know how to continue *) |
359 sorry |
266 sorry |
360 |
267 |
361 (* Not sure if it make sense or if it will be needed *) |
|
362 lemma abs_fun_rsp: "(op = ===> alpha ===> op = ===> op =) abs_fun abs_fun" |
|
363 sorry |
|
364 |
|
365 (* Should not be needed *) |
|
366 lemma eq_rsp2: "((op = ===> op =) ===> (op = ===> op =) ===> op =) op = op =" |
|
367 apply auto |
|
368 apply (rule ext) |
|
369 apply auto |
|
370 apply (rule ext) |
|
371 apply auto |
|
372 done |
|
373 |
|
374 (* Should not be needed *) |
|
375 lemma perm_rsp_eq: "(op = ===> (op = ===> op =) ===> op = ===> op =) op \<bullet> op \<bullet>" |
|
376 apply auto |
|
377 thm arg_cong2 |
|
378 apply (rule_tac f="perm x" in arg_cong2) |
|
379 apply (auto) |
|
380 apply (rule ext) |
|
381 apply (auto) |
|
382 done |
|
383 |
|
384 (* Should not be needed *) |
|
385 lemma fresh_rsp_eq: "(op = ===> (op = ===> op =) ===> op =) fresh fresh" |
|
386 apply (simp add: FUN_REL.simps) |
|
387 apply (metis ext) |
|
388 done |
|
389 |
|
390 (* It is just a test, it doesn't seem true... *) |
|
391 lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)" |
|
392 sorry |
|
393 |
|
394 ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *} |
|
395 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} |
|
396 |
|
397 thm a3 |
|
398 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} |
|
399 thm a3 |
|
400 ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *} |
|
401 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} t_u1 *} |
|
402 |
|
403 (* T_U *) |
|
404 |
|
405 ML {* val t_a = atomize_thm @{thm rfv_var} *} |
|
406 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
|
407 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
|
408 |
|
409 ML {* fun r_mk_comb_tac_lam ctxt = |
|
410 r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms |
|
411 *} |
|
412 |
|
413 instance lam :: fs_name |
|
414 apply(intro_classes) |
|
415 sorry |
|
416 |
|
417 prove asdf: {* Logic.mk_implies (concl_of t_r, (@{term "Trueprop (\<forall>t\<Colon>rlam\<in>Respects |
|
418 alpha. |
|
419 \<forall>(a\<Colon>name) b\<Colon>name. |
|
420 \<forall>s\<Colon>rlam\<in>Respects |
|
421 alpha. |
|
422 t \<approx> ([(a, |
|
423 b)] \<bullet> s) \<longrightarrow> |
|
424 a = b \<or> |
|
425 a |
|
426 \<notin> {a\<Colon>name. |
|
427 infinite |
|
428 {b\<Colon>name. Not |
|
429 (([(a, b)] \<bullet> |
|
430 s) \<approx> |
|
431 s)}} \<longrightarrow> |
|
432 rLam a |
|
433 t \<approx> rLam |
|
434 b s)"})) *} |
|
435 apply (tactic {* full_simp_tac ((Simplifier.context @{context} HOL_ss) addsimps |
|
436 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
437 (@{thm equiv_res_exists} OF [rel_eqv])]) 1 *}) |
|
438 apply (rule allI) |
|
439 apply (drule_tac x="t" in spec) |
|
440 apply (rule allI) |
|
441 apply (drule_tac x="a" in spec) |
|
442 apply (rule allI) |
|
443 apply (drule_tac x="b" in spec) |
|
444 apply (rule allI) |
|
445 apply (drule_tac x="s" in spec) |
|
446 apply (rule impI) |
|
447 apply (drule_tac mp) |
|
448 apply (simp) |
|
449 apply (simp) |
|
450 apply (rule impI) |
|
451 apply (rule a3) |
|
452 apply (simp) |
|
453 apply (simp add: abs_fresh(1)) |
|
454 apply (case_tac "a = b") |
|
455 apply (simp) |
|
456 apply (simp) |
|
457 apply (auto) |
|
458 apply (unfold fresh_def) |
|
459 apply (unfold supp_def) |
|
460 apply (simp) |
|
461 prefer 2 |
|
462 apply (simp) |
|
463 sorry |
|
464 |
|
465 ML {* val abs = findabs rty (prop_of t_a) *} |
|
466 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
|
467 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
|
468 |
|
469 ML {* val t_r' = @{thm asdf} OF [t_r] *} |
|
470 ML {* val t_t = repabs @{context} t_r' consts rty qty quot rel_refl trans2 rsp_thms *} |
|
471 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
|
472 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
|
473 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *} |
|
474 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
|
475 ML {* val tt = MetaSimplifier.rewrite_rule [symmetric @{thm supp_def}, symmetric @{thm fresh_def}] t_r *} |
|
476 ML {* val rr = @{thm sym} OF @{thms abs_fresh(1)} *} |
|
477 ML {* val ttt = eqsubst_thm @{context} [rr] tt *} |
|
478 ML {* ObjectLogic.rulify ttt *} |
|
479 |
|
480 lemma |
|
481 assumes a: "a \<notin> {a\<Colon>name. infinite {b\<Colon>name. \<not> ([(a, b)] \<bullet> s) \<approx> s}}" |
|
482 shows "a \<notin> {a\<Colon>name. infinite {b\<Colon>name. [(a, b)] \<bullet> s \<noteq> s}}" |
|
483 using a apply simp |
|
484 sorry (* Not true... *) |
|