author  nipkow 
Wed, 05 Jan 1994 19:47:14 +0100  
changeset 217  c972c57e7762 
parent 146  dbee71d43339 
child 406  4d4e0442b106 
permissions  rwrr 
1  1 
(* Title: Provers/simplifier 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1993 TU Munich 

5 

6 
Generic simplifier, suitable for most logics. 

7 

8 
*) 

88  9 
infix addsimps addeqcongs delsimps 
0  10 
setsolver setloop setmksimps setsubgoaler; 
11 

12 
signature SIMPLIFIER = 

13 
sig 

14 
type simpset 

1  15 
val addeqcongs: simpset * thm list > simpset 
0  16 
val addsimps: simpset * thm list > simpset 
88  17 
val delsimps: simpset * thm list > simpset 
0  18 
val asm_full_simp_tac: simpset > int > tactic 
19 
val asm_simp_tac: simpset > int > tactic 

20 
val empty_ss: simpset 

21 
val merge_ss: simpset * simpset > simpset 

22 
val prems_of_ss: simpset > thm list 

23 
val rep_ss: simpset > {simps: thm list, congs: thm list} 

24 
val setsolver: simpset * (thm list > int > tactic) > simpset 

25 
val setloop: simpset * (int > tactic) > simpset 

26 
val setmksimps: simpset * (thm > thm list) > simpset 

27 
val setsubgoaler: simpset * (simpset > int > tactic) > simpset 

28 
val simp_tac: simpset > int > tactic 

29 
end; 

30 

31 
structure Simplifier:SIMPLIFIER = 

32 
struct 

33 

34 
datatype simpset = 

35 
SS of {mss: meta_simpset, 

36 
simps: thm list, 

37 
congs: thm list, 

38 
subgoal_tac: simpset > int > tactic, 

39 
finish_tac: thm list > int > tactic, 

40 
loop_tac: int > tactic}; 

41 

42 
val empty_ss = 

43 
SS{mss=empty_mss, 

44 
simps= [], 

45 
congs= [], 

46 
subgoal_tac= K(K no_tac), 

47 
finish_tac= K(K no_tac), 

48 
loop_tac= K no_tac}; 

49 

50 

51 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac = 

52 
SS{mss=mss, 

53 
simps= simps, 

54 
congs= congs, 

55 
subgoal_tac= subgoal_tac, 

56 
finish_tac=finish_tac, 

57 
loop_tac=loop_tac}; 

58 

59 
fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac = 

60 
SS{mss=mss, 

61 
simps= simps, 

62 
congs= congs, 

63 
subgoal_tac= subgoal_tac, 

64 
finish_tac=finish_tac, 

65 
loop_tac=loop_tac}; 

66 

67 
fun (SS{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler subgoal_tac = 

68 
SS{mss=mss, 

69 
simps= simps, 

70 
congs= congs, 

71 
subgoal_tac= subgoal_tac, 

72 
finish_tac=finish_tac, 

73 
loop_tac=loop_tac}; 

74 

75 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps mk_simps = 

76 
SS{mss=Thm.set_mk_rews(mss,mk_simps), 

77 
simps= simps, 

78 
congs= congs, 

79 
subgoal_tac= subgoal_tac, 

80 
finish_tac=finish_tac, 

81 
loop_tac=loop_tac}; 

82 

83 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews = 

88  84 
let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in 
0  85 
SS{mss= Thm.add_simps(mss,rews'), 
86 
simps= rews' @ simps, 

87 
congs= congs, 

88 
subgoal_tac= subgoal_tac, 

89 
finish_tac=finish_tac, 

90 
loop_tac=loop_tac} 

91 
end; 

92 

88  93 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews = 
94 
let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in 

95 
SS{mss= Thm.del_simps(mss,rews'), 

96 
simps= foldl (gen_rem eq_thm) (simps,rews'), 

97 
congs= congs, 

98 
subgoal_tac= subgoal_tac, 

99 
finish_tac=finish_tac, 

100 
loop_tac=loop_tac} 

101 
end; 

102 

1  103 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs = 
0  104 
SS{mss= Thm.add_congs(mss,newcongs), 
105 
simps= simps, 

106 
congs= newcongs @ congs, 

107 
subgoal_tac= subgoal_tac, 

108 
finish_tac=finish_tac, 

109 
loop_tac=loop_tac}; 

110 

111 
fun merge_ss(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}, 

112 
SS{simps=simps2,congs=congs2,...}) = 

113 
let val simps' = gen_union eq_thm (simps,simps2) 

114 
val congs' = gen_union eq_thm (congs,congs2) 

115 
val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss) 

116 
val mss' = Thm.add_simps(mss',simps') 

117 
val mss' = Thm.add_congs(mss',congs') 

118 
in SS{mss= mss', 

119 
simps= simps, 

120 
congs= congs', 

121 
subgoal_tac= subgoal_tac, 

122 
finish_tac= finish_tac, 

123 
loop_tac= loop_tac} 

124 
end; 

125 

126 
fun prems_of_ss(SS{mss,...}) = prems_of_mss mss; 

127 

128 
fun rep_ss(SS{simps,congs,...}) = {simps=simps,congs=congs}; 

129 

1  130 
fun NEWSUBGOALS tac tacf = 
131 
STATE(fn state0 => 

132 
tac THEN STATE(fn state1 => tacf(nprems_of state1  nprems_of state0))); 

133 

217
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset

134 
fun gen_simp_tac mode = 
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset

135 
fn (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) => 
0  136 
let fun solve_all_tac mss = 
137 
let val ss = SS{mss=mss,simps=simps,congs=congs, 

138 
subgoal_tac=subgoal_tac, 

139 
finish_tac=finish_tac, loop_tac=loop_tac} 

1  140 
val solve1_tac = 
141 
NEWSUBGOALS (subgoal_tac ss 1) 

142 
(fn n => if n<0 then all_tac else no_tac) 

143 
in DEPTH_SOLVE(solve1_tac) end 

0  144 

145 
fun simp_loop i thm = 

217
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset

146 
tapply(asm_rewrite_goal_tac mode solve_all_tac mss i THEN 
1  147 
(finish_tac (prems_of_mss mss) i ORELSE looper i), 
0  148 
thm) 
1  149 
and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0)) 
150 
and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i)) 

0  151 
and simp_loop_tac i = Tactic(simp_loop i) 
152 

217
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset

153 
in simp_loop_tac end; 
0  154 

217
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset

155 
val asm_full_simp_tac = gen_simp_tac (true,true); 
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset

156 
val asm_simp_tac = gen_simp_tac (false,true); 
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset

157 
val simp_tac = gen_simp_tac (false,false); 
0  158 

159 
end; 