author | wenzelm |
Sat, 28 Jun 2008 22:52:03 +0200 | |
changeset 27388 | 226835ea8d2b |
parent 15574 | b1d1b5bfc464 |
child 30190 | 479806475f3c |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: typedsimp |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Functor for constructing simplifiers. Suitable for Constructive Type |
|
7 |
Theory with its typed reflexivity axiom a:A ==> a=a:A. For most logics try |
|
8 |
simp.ML. |
|
9 |
*) |
|
10 |
||
11 |
signature TSIMP_DATA = |
|
12 |
sig |
|
13 |
val refl: thm (*Reflexive law*) |
|
14 |
val sym: thm (*Symmetric law*) |
|
15 |
val trans: thm (*Transitive law*) |
|
16 |
val refl_red: thm (* reduce(a,a) *) |
|
17 |
val trans_red: thm (* [|a=b; reduce(b,c) |] ==> a=c *) |
|
18 |
val red_if_equal: thm (* a=b ==> reduce(a,b) *) |
|
19 |
(*Built-in rewrite rules*) |
|
20 |
val default_rls: thm list |
|
21 |
(*Type checking or similar -- solution of routine conditions*) |
|
22 |
val routine_tac: thm list -> int -> tactic |
|
23 |
end; |
|
24 |
||
25 |
signature TSIMP = |
|
26 |
sig |
|
27 |
val asm_res_tac: thm list -> int -> tactic |
|
28 |
val cond_norm_tac: ((int->tactic) * thm list * thm list) -> tactic |
|
29 |
val cond_step_tac: ((int->tactic) * thm list * thm list) -> int -> tactic |
|
30 |
val norm_tac: (thm list * thm list) -> tactic |
|
31 |
val process_rules: thm list -> thm list * thm list |
|
32 |
val rewrite_res_tac: int -> tactic |
|
33 |
val split_eqn: thm |
|
34 |
val step_tac: (thm list * thm list) -> int -> tactic |
|
35 |
val subconv_res_tac: thm list -> int -> tactic |
|
36 |
end; |
|
37 |
||
38 |
||
39 |
functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP = |
|
40 |
struct |
|
41 |
local open TSimp_data |
|
42 |
in |
|
43 |
||
44 |
(*For simplifying both sides of an equation: |
|
45 |
[| a=c; b=c |] ==> b=a |
|
46 |
Can use resolve_tac [split_eqn] to prepare an equation for simplification. *) |
|
47 |
val split_eqn = standard (sym RSN (2,trans) RS sym); |
|
48 |
||
49 |
||
50 |
(* [| a=b; b=c |] ==> reduce(a,c) *) |
|
51 |
val red_trans = standard (trans RS red_if_equal); |
|
52 |
||
53 |
(*For REWRITE rule: Make a reduction rule for simplification, e.g. |
|
54 |
[| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *) |
|
55 |
fun simp_rule rl = rl RS trans; |
|
56 |
||
57 |
(*For REWRITE rule: Make rule for resimplifying if possible, e.g. |
|
58 |
[| a: C(0); ...; a=c: C(0) |] ==> reduce(rec(0,a,b), c) *) |
|
59 |
fun resimp_rule rl = rl RS red_trans; |
|
60 |
||
61 |
(*For CONGRUENCE rule, like a=b ==> succ(a) = succ(b) |
|
62 |
Make rule for simplifying subterms, e.g. |
|
63 |
[| a=b: N; reduce(succ(b), c) |] ==> succ(a)=c: N *) |
|
64 |
fun subconv_rule rl = rl RS trans_red; |
|
65 |
||
66 |
(*If the rule proves an equality then add both forms to simp_rls |
|
67 |
else add the rule to other_rls*) |
|
68 |
fun add_rule (rl, (simp_rls, other_rls)) = |
|
69 |
(simp_rule rl :: resimp_rule rl :: simp_rls, other_rls) |
|
70 |
handle THM _ => (simp_rls, rl :: other_rls); |
|
71 |
||
72 |
(*Given the list rls, return the pair (simp_rls, other_rls).*) |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
73 |
fun process_rules rls = foldr add_rule ([],[]) rls; |
0 | 74 |
|
75 |
(*Given list of rewrite rules, return list of both forms, reject others*) |
|
76 |
fun process_rewrites rls = |
|
77 |
case process_rules rls of |
|
78 |
(simp_rls,[]) => simp_rls |
|
79 |
| (_,others) => raise THM |
|
80 |
("process_rewrites: Ill-formed rewrite", 0, others); |
|
81 |
||
82 |
(*Process the default rewrite rules*) |
|
83 |
val simp_rls = process_rewrites default_rls; |
|
84 |
||
85 |
(*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac |
|
86 |
will fail! The filter will pass all the rules, and the bound permits |
|
87 |
no ambiguity.*) |
|
88 |
||
89 |
(*Resolution with rewrite/sub rules. Builds the tree for filt_resolve_tac.*) |
|
90 |
val rewrite_res_tac = filt_resolve_tac simp_rls 2; |
|
91 |
||
92 |
(*The congruence rules for simplifying subterms. If subgoal is too flexible |
|
93 |
then only refl,refl_red will be used (if even them!). *) |
|
94 |
fun subconv_res_tac congr_rls = |
|
95 |
filt_resolve_tac (map subconv_rule congr_rls) 2 |
|
96 |
ORELSE' filt_resolve_tac [refl,refl_red] 1; |
|
97 |
||
98 |
(*Resolve with asms, whether rewrites or not*) |
|
99 |
fun asm_res_tac asms = |
|
100 |
let val (xsimp_rls,xother_rls) = process_rules asms |
|
101 |
in routine_tac xother_rls ORELSE' |
|
102 |
filt_resolve_tac xsimp_rls 2 |
|
103 |
end; |
|
104 |
||
105 |
(*Single step for simple rewriting*) |
|
106 |
fun step_tac (congr_rls,asms) = |
|
107 |
asm_res_tac asms ORELSE' rewrite_res_tac ORELSE' |
|
108 |
subconv_res_tac congr_rls; |
|
109 |
||
110 |
(*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*) |
|
111 |
fun cond_step_tac (prove_cond_tac, congr_rls, asms) = |
|
112 |
asm_res_tac asms ORELSE' rewrite_res_tac ORELSE' |
|
113 |
(resolve_tac [trans, red_trans] THEN' prove_cond_tac) ORELSE' |
|
114 |
subconv_res_tac congr_rls; |
|
115 |
||
116 |
(*Unconditional normalization tactic*) |
|
117 |
fun norm_tac arg = REPEAT_FIRST (step_tac arg) THEN |
|
118 |
TRYALL (resolve_tac [red_if_equal]); |
|
119 |
||
120 |
(*Conditional normalization tactic*) |
|
121 |
fun cond_norm_tac arg = REPEAT_FIRST (cond_step_tac arg) THEN |
|
122 |
TRYALL (resolve_tac [red_if_equal]); |
|
123 |
||
124 |
end; |
|
125 |
end; |
|
126 |
||
127 |