equal
deleted
inserted
replaced
416 cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); |
416 cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); |
417 cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}) |
417 cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}) |
418 *} |
418 *} |
419 |
419 |
420 |
420 |
421 term Respects |
421 ML {* |
422 |
422 fun atomize_thm thm = |
423 ML {* |
423 let |
424 fun atomize_thm t = |
424 val thm' = forall_intr_vars thm |
425 MetaSimplifier.rewrite_rule [ObjectLogic.atomize (cterm_of @{theory} (prop_of t))] t |
425 val thm'' = ObjectLogic.atomize (cprop_of thm') |
426 *} |
426 in |
427 |
427 Simplifier.rewrite_rule [thm''] thm' |
428 ML {* |
428 end |
429 fun meta_quantify t = |
429 *} |
430 let |
430 |
431 val vars = Term.add_vars (prop_of t) []; |
431 thm list.induct |
432 val cvars = map (fn x => cterm_of @{theory} (Var x)) vars |
432 ML {* atomize_thm @{thm list.induct} *} |
433 in |
|
434 fold forall_intr cvars t |
|
435 end |
|
436 *} |
|
437 |
|
438 ML {* atomize_thm (meta_quantify @{thm list.induct}) *} |
|
439 |
433 |
440 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
434 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
441 trm == new_trm |
435 trm == new_trm |
442 *) |
436 *) |
443 |
437 |
1117 apply (tactic {* foo_tac' @{context} 1 *}) |
1111 apply (tactic {* foo_tac' @{context} 1 *}) |
1118 done |
1112 done |
1119 |
1113 |
1120 thm list.induct |
1114 thm list.induct |
1121 |
1115 |
1122 ML {* val li = Thm.freezeT (atomize_thm (meta_quantify @{thm list.induct})) *} |
1116 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *} |
1123 |
1117 |
1124 ML {* |
1118 ML {* |
1125 Syntax.string_of_term @{context} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}) |
1119 Syntax.string_of_term @{context} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}) |
1126 |> writeln |
1120 |> writeln |
1127 *} |
1121 *} |
1179 |
1173 |
1180 ML {* |
1174 ML {* |
1181 fun lift_theorem_fset name thm lthy = |
1175 fun lift_theorem_fset name thm lthy = |
1182 let |
1176 let |
1183 val lifted_thm = lift_theorem_fset_aux thm lthy; |
1177 val lifted_thm = lift_theorem_fset_aux thm lthy; |
1184 val (_, lthy2) = note_thm (name, lifted_thm) lthy; |
1178 val (_, lthy2) = note (name, lifted_thm) lthy; |
1185 in |
1179 in |
1186 lthy2 |
1180 lthy2 |
1187 end; |
1181 end; |
1188 *} |
1182 *} |
1189 |
1183 |