10 files "Tools/rewrite_hol_proof.ML" |
10 files "Tools/rewrite_hol_proof.ML" |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Setup *} |
13 subsection {* Setup *} |
14 |
14 |
15 ML_setup {* |
15 setup {* |
|
16 let |
16 fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $ |
17 fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $ |
17 (Const ("op :", _) $ x $ S)) = (case strip_comb S of |
18 (Const ("op :", _) $ x $ S)) = (case strip_comb S of |
18 (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @ |
19 (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @ |
19 [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x])) |
20 [HOLogic.dest_setT (body_type U)] ---> HOLogic.boolT), ts @ [x])) |
20 | (Free (s, U), ts) => SOME (list_comb (Free (s, binder_types U @ |
21 | (Free (s, U), ts) => SOME (list_comb (Free (s, binder_types U @ |
31 |
32 |
32 fun mk_realizes_set r rT s (setT as Type ("set", [elT])) = |
33 fun mk_realizes_set r rT s (setT as Type ("set", [elT])) = |
33 Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $ |
34 Abs ("x", elT, Const ("realizes", rT --> HOLogic.boolT --> HOLogic.boolT) $ |
34 incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $ |
35 incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $ |
35 Bound 0 $ incr_boundvars 1 s)); |
36 Bound 0 $ incr_boundvars 1 s)); |
36 |
37 in |
37 Context.>> (fn thy => thy |> |
38 [Extraction.add_types |
38 Extraction.add_types |
|
39 [("bool", ([], NONE)), |
39 [("bool", ([], NONE)), |
40 ("set", ([realizes_set_proc], SOME mk_realizes_set))] |> |
40 ("set", ([realizes_set_proc], SOME mk_realizes_set))], |
41 Extraction.set_preprocessor (fn sg => |
41 Extraction.set_preprocessor (fn sg => |
42 Proofterm.rewrite_proof_notypes |
42 Proofterm.rewrite_proof_notypes |
43 ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) :: |
43 ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) :: |
44 ProofRewriteRules.rprocs true) o |
44 ProofRewriteRules.rprocs true) o |
45 Proofterm.rewrite_proof (Sign.tsig_of sg) |
45 Proofterm.rewrite_proof (Sign.tsig_of sg) |
46 (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o |
46 (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o |
47 ProofRewriteRules.elim_vars (curry Const "arbitrary"))) |
47 ProofRewriteRules.elim_vars (curry Const "arbitrary"))] |
|
48 end |
48 *} |
49 *} |
49 |
50 |
50 lemmas [extraction_expand] = |
51 lemmas [extraction_expand] = |
51 atomize_eq atomize_all atomize_imp |
52 atomize_eq atomize_all atomize_imp |
52 allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |
53 allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |