equal
deleted
inserted
replaced
413 cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); |
413 cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); |
414 cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}) |
414 cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}) |
415 *} |
415 *} |
416 |
416 |
417 |
417 |
418 term Respects |
418 ML {* |
419 |
419 fun atomize_thm thm = |
420 ML {* |
420 let |
421 fun atomize_thm t = |
421 val thm' = forall_intr_vars thm |
422 MetaSimplifier.rewrite_rule [ObjectLogic.atomize (cterm_of @{theory} (prop_of t))] t |
422 val thm'' = ObjectLogic.atomize (cprop_of thm') |
423 *} |
423 in |
424 |
424 Simplifier.rewrite_rule [thm''] thm' |
425 ML {* |
425 end |
426 fun meta_quantify t = |
426 *} |
427 let |
427 |
428 val vars = Term.add_vars (prop_of t) []; |
428 thm list.induct |
429 val cvars = map (fn x => cterm_of @{theory} (Var x)) vars |
429 ML {* atomize_thm @{thm list.induct} *} |
430 in |
|
431 fold forall_intr cvars t |
|
432 end |
|
433 *} |
|
434 |
|
435 ML {* atomize_thm (meta_quantify @{thm list.induct}) *} |
|
436 |
430 |
437 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
431 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
438 trm == new_trm |
432 trm == new_trm |
439 *) |
433 *) |
440 |
434 |
1114 apply (tactic {* foo_tac' @{context} 1 *}) |
1108 apply (tactic {* foo_tac' @{context} 1 *}) |
1115 done |
1109 done |
1116 |
1110 |
1117 thm list.induct |
1111 thm list.induct |
1118 |
1112 |
1119 ML {* val li = atomize_thm (meta_quantify @{thm list.induct}) *} |
1113 ML {* val li = atomize_thm @{thm list.induct} *} |
1120 |
1114 |
1121 ML {* (* Doesn't recognize that 'a list = '?a list *) |
1115 ML {* (* Doesn't recognize that 'a list = '?a list *) |
1122 cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}) |
1116 cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}) |
1123 *} |
1117 *} |
1124 |
1118 |
1169 |
1163 |
1170 ML {* |
1164 ML {* |
1171 fun lift_theorem_fset name thm lthy = |
1165 fun lift_theorem_fset name thm lthy = |
1172 let |
1166 let |
1173 val lifted_thm = lift_theorem_fset_aux thm lthy; |
1167 val lifted_thm = lift_theorem_fset_aux thm lthy; |
1174 val (_, lthy2) = note_thm (name, lifted_thm) lthy; |
1168 val (_, lthy2) = note (name, lifted_thm) lthy; |
1175 in |
1169 in |
1176 lthy2 |
1170 lthy2 |
1177 end; |
1171 end; |
1178 *} |
1172 *} |
1179 |
1173 |