equal
deleted
inserted
replaced
370 else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) |
370 else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) |
371 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) |
371 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) |
372 | _ => trm |
372 | _ => trm |
373 *} |
373 *} |
374 |
374 |
|
375 ML {* |
|
376 fun my_reg_inst lthy rel rty trm = |
|
377 case rel of |
|
378 Const (n, _) => Syntax.check_term lthy |
|
379 (my_reg lthy (Const (n, dummyT)) rty trm) |
|
380 *} |
|
381 |
|
382 (*ML {* |
|
383 (*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow>bool"};*) |
|
384 val r = Free ("R", dummyT); |
|
385 val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"}); |
|
386 val t2 = Syntax.check_term @{context} t; |
|
387 Toplevel.program (fn () => cterm_of @{theory} t2) |
|
388 *}*) |
|
389 |
375 text {* Assumes that the given theorem is atomized *} |
390 text {* Assumes that the given theorem is atomized *} |
376 ML {* |
391 ML {* |
377 fun build_regularize_goal thm rty rel lthy = |
392 fun build_regularize_goal thm rty rel lthy = |
378 Logic.mk_implies |
393 Logic.mk_implies |
379 ((prop_of thm), |
394 ((prop_of thm), |
380 (my_reg lthy rel rty (prop_of thm))) |
395 (my_reg_inst lthy rel rty (prop_of thm))) |
381 *} |
396 *} |
382 |
397 |
383 lemma universal_twice: |
398 lemma universal_twice: |
384 "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))" |
399 "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))" |
385 by auto |
400 by auto |