14 |
14 |
15 setup \<open> |
15 setup \<open> |
16 Extraction.add_types |
16 Extraction.add_types |
17 [("bool", ([], NONE))] #> |
17 [("bool", ([], NONE))] #> |
18 Extraction.set_preprocessor (fn thy => |
18 Extraction.set_preprocessor (fn thy => |
|
19 let val ctxt = Proof_Context.init_global thy in |
19 Proofterm.rewrite_proof_notypes |
20 Proofterm.rewrite_proof_notypes |
20 ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o |
21 ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o |
21 Proofterm.rewrite_proof thy |
22 Proofterm.rewrite_proof thy |
22 (RewriteHOLProof.rews, |
23 (RewriteHOLProof.rews, |
23 ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o |
24 ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class ctxt]) o |
24 ProofRewriteRules.elim_vars (curry Const @{const_name default})) |
25 ProofRewriteRules.elim_vars (curry Const @{const_name default}) |
|
26 end) |
25 \<close> |
27 \<close> |
26 |
28 |
27 lemmas [extraction_expand] = |
29 lemmas [extraction_expand] = |
28 meta_spec atomize_eq atomize_all atomize_imp atomize_conj |
30 meta_spec atomize_eq atomize_all atomize_imp atomize_conj |
29 allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |
31 allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |