author  wenzelm 
Sun, 07 Feb 2010 19:33:34 +0100  
changeset 35021  c839a4c670c6 
parent 33339  d41f77196338 
child 45659  09539cdffcd7 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

1 
(* Title: Provers/typedsimp.ML 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1993 University of Cambridge 
4 

5 
Functor for constructing simplifiers. Suitable for Constructive Type 

6 
Theory with its typed reflexivity axiom a:A ==> a=a:A. For most logics try 

7 
simp.ML. 

8 
*) 

9 

10 
signature TSIMP_DATA = 

11 
sig 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

12 
val refl: thm (*Reflexive law*) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

13 
val sym: thm (*Symmetric law*) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

14 
val trans: thm (*Transitive law*) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

15 
val refl_red: thm (* reduce(a,a) *) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

16 
val trans_red: thm (* [a=b; reduce(b,c) ] ==> a=c *) 
0  17 
val red_if_equal: thm (* a=b ==> reduce(a,b) *) 
18 
(*Builtin rewrite rules*) 

19 
val default_rls: thm list 

20 
(*Type checking or similar  solution of routine conditions*) 

21 
val routine_tac: thm list > int > tactic 

22 
end; 

23 

24 
signature TSIMP = 

25 
sig 

26 
val asm_res_tac: thm list > int > tactic 

27 
val cond_norm_tac: ((int>tactic) * thm list * thm list) > tactic 

28 
val cond_step_tac: ((int>tactic) * thm list * thm list) > int > tactic 

29 
val norm_tac: (thm list * thm list) > tactic 

30 
val process_rules: thm list > thm list * thm list 

31 
val rewrite_res_tac: int > tactic 

32 
val split_eqn: thm 

33 
val step_tac: (thm list * thm list) > int > tactic 

34 
val subconv_res_tac: thm list > int > tactic 

35 
end; 

36 

37 

38 
functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP = 

39 
struct 

40 
local open TSimp_data 

41 
in 

42 

43 
(*For simplifying both sides of an equation: 

44 
[ a=c; b=c ] ==> b=a 

45 
Can use resolve_tac [split_eqn] to prepare an equation for simplification. *) 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33339
diff
changeset

46 
val split_eqn = Drule.export_without_context (sym RSN (2,trans) RS sym); 
0  47 

48 

49 
(* [ a=b; b=c ] ==> reduce(a,c) *) 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33339
diff
changeset

50 
val red_trans = Drule.export_without_context (trans RS red_if_equal); 
0  51 

52 
(*For REWRITE rule: Make a reduction rule for simplification, e.g. 

53 
[ a: C(0); ... ; a=c: C(0) ] ==> rec(0,a,b) = c: C(0) *) 

54 
fun simp_rule rl = rl RS trans; 

55 

56 
(*For REWRITE rule: Make rule for resimplifying if possible, e.g. 

57 
[ a: C(0); ...; a=c: C(0) ] ==> reduce(rec(0,a,b), c) *) 

58 
fun resimp_rule rl = rl RS red_trans; 

59 

60 
(*For CONGRUENCE rule, like a=b ==> succ(a) = succ(b) 

61 
Make rule for simplifying subterms, e.g. 

62 
[ a=b: N; reduce(succ(b), c) ] ==> succ(a)=c: N *) 

63 
fun subconv_rule rl = rl RS trans_red; 

64 

65 
(*If the rule proves an equality then add both forms to simp_rls 

66 
else add the rule to other_rls*) 

33339  67 
fun add_rule rl (simp_rls, other_rls) = 
0  68 
(simp_rule rl :: resimp_rule rl :: simp_rls, other_rls) 
69 
handle THM _ => (simp_rls, rl :: other_rls); 

70 

71 
(*Given the list rls, return the pair (simp_rls, other_rls).*) 

33339  72 
fun process_rules rls = fold_rev add_rule rls ([], []); 
0  73 

74 
(*Given list of rewrite rules, return list of both forms, reject others*) 

75 
fun process_rewrites rls = 

76 
case process_rules rls of 

77 
(simp_rls,[]) => simp_rls 

78 
 (_,others) => raise THM 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

79 
("process_rewrites: Illformed rewrite", 0, others); 
0  80 

81 
(*Process the default rewrite rules*) 

82 
val simp_rls = process_rewrites default_rls; 

83 

84 
(*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac 

85 
will fail! The filter will pass all the rules, and the bound permits 

86 
no ambiguity.*) 

87 

88 
(*Resolution with rewrite/sub rules. Builds the tree for filt_resolve_tac.*) 

89 
val rewrite_res_tac = filt_resolve_tac simp_rls 2; 

90 

91 
(*The congruence rules for simplifying subterms. If subgoal is too flexible 

92 
then only refl,refl_red will be used (if even them!). *) 

93 
fun subconv_res_tac congr_rls = 

94 
filt_resolve_tac (map subconv_rule congr_rls) 2 

95 
ORELSE' filt_resolve_tac [refl,refl_red] 1; 

96 

97 
(*Resolve with asms, whether rewrites or not*) 

98 
fun asm_res_tac asms = 

99 
let val (xsimp_rls,xother_rls) = process_rules asms 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

100 
in routine_tac xother_rls ORELSE' 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

101 
filt_resolve_tac xsimp_rls 2 
0  102 
end; 
103 

104 
(*Single step for simple rewriting*) 

105 
fun step_tac (congr_rls,asms) = 

106 
asm_res_tac asms ORELSE' rewrite_res_tac ORELSE' 

107 
subconv_res_tac congr_rls; 

108 

109 
(*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*) 

110 
fun cond_step_tac (prove_cond_tac, congr_rls, asms) = 

111 
asm_res_tac asms ORELSE' rewrite_res_tac ORELSE' 

112 
(resolve_tac [trans, red_trans] THEN' prove_cond_tac) ORELSE' 

113 
subconv_res_tac congr_rls; 

114 

115 
(*Unconditional normalization tactic*) 

116 
fun norm_tac arg = REPEAT_FIRST (step_tac arg) THEN 

117 
TRYALL (resolve_tac [red_if_equal]); 

118 

119 
(*Conditional normalization tactic*) 

120 
fun cond_norm_tac arg = REPEAT_FIRST (cond_step_tac arg) THEN 

121 
TRYALL (resolve_tac [red_if_equal]); 

122 

123 
end; 

124 
end; 

125 

126 