equal
deleted
inserted
replaced
345 case rel of |
345 case rel of |
346 Const (n, _) => Syntax.check_term lthy |
346 Const (n, _) => Syntax.check_term lthy |
347 (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm) |
347 (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm) |
348 *} |
348 *} |
349 |
349 |
350 (*ML {* |
350 (* |
351 (*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow>bool"};*) |
351 ML {* |
|
352 text {*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow>bool"};*} |
352 val r = Free ("R", dummyT); |
353 val r = Free ("R", dummyT); |
353 val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"}); |
354 val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"}); |
354 val t2 = Syntax.check_term @{context} t; |
355 val t2 = Syntax.check_term @{context} t; |
355 Toplevel.program (fn () => cterm_of @{theory} t2) |
356 Toplevel.program (fn () => cterm_of @{theory} t2) |
356 *}*) |
357 *}*) |
375 by auto*) |
376 by auto*) |
376 |
377 |
377 ML {* |
378 ML {* |
378 fun regularize thm rty rel rel_eqv rel_refl lthy = |
379 fun regularize thm rty rel rel_eqv rel_refl lthy = |
379 let |
380 let |
380 val g = build_regularize_goal thm rty rel lthy; |
381 val goal = build_regularize_goal thm rty rel lthy; |
381 fun tac ctxt = |
382 fun tac ctxt = |
382 (ObjectLogic.full_atomize_tac) THEN' |
383 (ObjectLogic.full_atomize_tac) THEN' |
383 REPEAT_ALL_NEW (FIRST' [ |
384 REPEAT_ALL_NEW (FIRST' [ |
384 rtac rel_refl, |
385 rtac rel_refl, |
385 atac, |
386 atac, |
388 rtac @{thm implication_twice}, |
389 rtac @{thm implication_twice}, |
389 (*rtac @{thm equality_twice},*) |
390 (*rtac @{thm equality_twice},*) |
390 EqSubst.eqsubst_tac ctxt [0] |
391 EqSubst.eqsubst_tac ctxt [0] |
391 [(@{thm equiv_res_forall} OF [rel_eqv]), |
392 [(@{thm equiv_res_forall} OF [rel_eqv]), |
392 (@{thm equiv_res_exists} OF [rel_eqv])], |
393 (@{thm equiv_res_exists} OF [rel_eqv])], |
393 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
394 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
394 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
395 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
395 ]); |
396 ]); |
396 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
397 val cthm = Goal.prove lthy [] [] goal |
|
398 (fn {context,...} => tac context 1); |
397 in |
399 in |
398 cthm OF [thm] |
400 cthm OF [thm] |
399 end |
401 end |
400 *} |
402 *} |
401 |
403 |