|
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).*) |
|
73 fun process_rules rls = foldr add_rule (rls, ([],[])); |
|
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 |