author  immler@in.tum.de 
Thu, 26 Feb 2009 10:13:43 +0100  
changeset 30151  629f3a92863e 
parent 15574  b1d1b5bfc464 
child 30190  479806475f3c 
permissions  rwrr 
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 
(*Builtin 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: Illformed 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 