1 (* Title: Pure/meta_simplifier.ML |
1 (* Title: Pure/meta_simplifier.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow and Stefan Berghofer |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Meta Simplification |
6 Meta-level Simplification. |
7 *) |
7 *) |
|
8 |
|
9 signature BASIC_META_SIMPLIFIER = |
|
10 sig |
|
11 val trace_simp: bool ref |
|
12 val debug_simp: bool ref |
|
13 end; |
8 |
14 |
9 signature META_SIMPLIFIER = |
15 signature META_SIMPLIFIER = |
10 sig |
16 sig |
|
17 include BASIC_META_SIMPLIFIER |
11 exception SIMPLIFIER of string * thm |
18 exception SIMPLIFIER of string * thm |
12 type meta_simpset |
19 type meta_simpset |
13 val dest_mss : meta_simpset -> |
20 val dest_mss : meta_simpset -> |
14 {simps: thm list, congs: thm list, procs: (string * cterm list) list} |
21 {simps: thm list, congs: thm list, procs: (string * cterm list) list} |
15 val empty_mss : meta_simpset |
22 val empty_mss : meta_simpset |
30 val prems_of_mss : meta_simpset -> thm list |
37 val prems_of_mss : meta_simpset -> thm list |
31 val set_mk_rews : meta_simpset * (thm -> thm list) -> meta_simpset |
38 val set_mk_rews : meta_simpset * (thm -> thm list) -> meta_simpset |
32 val set_mk_sym : meta_simpset * (thm -> thm option) -> meta_simpset |
39 val set_mk_sym : meta_simpset * (thm -> thm option) -> meta_simpset |
33 val set_mk_eq_True : meta_simpset * (thm -> thm option) -> meta_simpset |
40 val set_mk_eq_True : meta_simpset * (thm -> thm option) -> meta_simpset |
34 val set_termless : meta_simpset * (term * term -> bool) -> meta_simpset |
41 val set_termless : meta_simpset * (term * term -> bool) -> meta_simpset |
35 val trace_simp : bool ref |
42 val rewrite_cterm: bool * bool * bool -> |
36 val debug_simp : bool ref |
43 (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm |
37 val rewrite_cterm : bool * bool * bool |
44 val full_rewrite_cterm_aux: (meta_simpset -> thm -> thm option) -> thm list -> cterm -> cterm |
38 -> (meta_simpset -> thm -> thm option) |
|
39 -> meta_simpset -> cterm -> thm |
|
40 val rewrite_rule_aux : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm |
45 val rewrite_rule_aux : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm |
41 val rewrite_thm : bool * bool * bool |
46 val rewrite_thm : bool * bool * bool |
42 -> (meta_simpset -> thm -> thm option) |
47 -> (meta_simpset -> thm -> thm option) |
43 -> meta_simpset -> thm -> thm |
48 -> meta_simpset -> thm -> thm |
44 val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm |
49 val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm |
929 in gconv 1 end; |
934 in gconv 1 end; |
930 |
935 |
931 (*Use a conversion to transform a theorem*) |
936 (*Use a conversion to transform a theorem*) |
932 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; |
937 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; |
933 |
938 |
|
939 (*Rewrite a cterm (yielding again a cterm instead of a theorem)*) |
|
940 fun full_rewrite_cterm_aux _ [] = (fn ct => ct) |
|
941 | full_rewrite_cterm_aux prover thms = |
|
942 #2 o Thm.dest_comb o #prop o Thm.crep_thm o |
|
943 rewrite_cterm (true, false, false) prover (mss_of thms); |
|
944 |
934 (*Rewrite a theorem*) |
945 (*Rewrite a theorem*) |
935 fun rewrite_rule_aux _ [] = (fn th => th) |
946 fun rewrite_rule_aux _ [] = (fn th => th) |
936 | rewrite_rule_aux prover thms = |
947 | rewrite_rule_aux prover thms = |
937 fconv_rule (rewrite_cterm (true,false,false) prover (mss_of thms)); |
948 fconv_rule (rewrite_cterm (true,false,false) prover (mss_of thms)); |
938 |
949 |