author  oheimb 
Thu, 26 Feb 1998 15:45:33 +0100  
changeset 4659  a78ecc7341e3 
parent 4652  d24cca140eeb 
child 4717  1370ad043564 
permissions  rwrr 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

1 
(* Title: Provers/clasimp.ML 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

2 
ID: $Id$ 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

3 
Author: David von Oheimb, TU Muenchen 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

4 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

5 
Combination of classical reasoner and simplifier 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

6 
to be used after installing both of them 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

7 
*) 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

8 

4659  9 
type clasimpset = claset * simpset; 
10 

4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

11 
infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

12 
addsimps2 delsimps2 addcongs2 delcongs2; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

13 
infix 4 addSss addss; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

14 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

15 
signature CLASIMP = 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

16 
sig 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

17 
val addSIs2 : clasimpset * thm list > clasimpset 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

18 
val addSEs2 : clasimpset * thm list > clasimpset 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

19 
val addSDs2 : clasimpset * thm list > clasimpset 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

20 
val addIs2 : clasimpset * thm list > clasimpset 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

21 
val addEs2 : clasimpset * thm list > clasimpset 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

22 
val addDs2 : clasimpset * thm list > clasimpset 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

23 
val addsimps2 : clasimpset * thm list > clasimpset 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

24 
val delsimps2 : clasimpset * thm list > clasimpset 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

25 
val addSss : claset * simpset > claset 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

26 
val addss : claset * simpset > claset 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

27 
val mk_auto_tac:clasimpset > int > int > tactic 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

28 
val auto_tac : clasimpset > tactic 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

29 
val Auto_tac : tactic 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

30 
val auto : unit > unit 
4659  31 
val smart_tac : clasimpset > int > tactic 
32 
val Smart_tac : int > tactic 

33 
val smart : int > unit 

4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

34 
end; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

35 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

36 
structure Clasimp: CLASIMP = 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

37 
struct 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

38 

4659  39 
(* this interface for updating a clasimpset is rudimentary and just for 
40 
convenience for the most common cases. 

41 
In other cases a clasimpset may be dealt with componentwise. *) 

4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

42 
local 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

43 
fun pair_upd1 f ((a,b),x) = (f(a,x), b); 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

44 
fun pair_upd2 f ((a,b),x) = (a, f(b,x)); 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

45 
in 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

46 
fun op addSIs2 arg = pair_upd1 (op addSIs) arg; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

47 
fun op addSEs2 arg = pair_upd1 (op addSEs) arg; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

48 
fun op addSDs2 arg = pair_upd1 (op addSDs) arg; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

49 
fun op addIs2 arg = pair_upd1 (op addIs ) arg; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

50 
fun op addEs2 arg = pair_upd1 (op addEs ) arg; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

51 
fun op addDs2 arg = pair_upd1 (op addDs ) arg; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

52 
fun op addsimps2 arg = pair_upd2 (op addsimps) arg; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

53 
fun op delsimps2 arg = pair_upd2 (op delsimps) arg; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

54 
fun op addcongs2 arg = pair_upd2 (op addcongs) arg; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

55 
fun op delcongs2 arg = pair_upd2 (op delcongs) arg; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

56 
end; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

57 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

58 
(*an unsatisfactory fix for the incomplete safe_asm_full_simp_tac! 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

59 
better: asm_really_full_simp_tac, a yet to be implemented version of 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

60 
asm_full_simp_tac that applies all equalities in the 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

61 
premises to all the premises *) 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

62 
fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

63 
safe_asm_full_simp_tac ss; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

64 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

65 
(*Add a simpset to a classical set!*) 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

66 
(*Caution: only one simpset added can be added by each of addSss and addss*) 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

67 
fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac", 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

68 
CHANGED o (safe_asm_more_full_simp_tac ss)); 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

69 
fun cs addss ss = cs addbefore ( "asm_full_simp_tac", 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

70 
asm_full_simp_tac ss); 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

71 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

72 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

73 
local 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

74 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

75 
fun blast_depth_tac cs m i thm = Blast.depth_tac cs m i thm 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

76 
handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty); 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

77 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

78 
(* a variant of depth_tac that avoids interference of the simplifier 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

79 
with dup_step_tac when they are combined by auto_tac *) 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

80 
fun nodup_depth_tac cs m i state = 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

81 
SELECT_GOAL 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

82 
(appWrappers cs 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

83 
(fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

84 
(safe_step_tac cs i)) THEN_ELSE 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

85 
(DEPTH_SOLVE (nodup_depth_tac cs m i), 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

86 
inst0_step_tac cs i APPEND 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

87 
COND (K(m=0)) no_tac 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

88 
((instp_step_tac cs i APPEND step_tac cs i) 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

89 
THEN DEPTH_SOLVE (nodup_depth_tac cs (m1) i)))) 1) 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

90 
i state; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

91 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

92 
in 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

93 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

94 
(*Designed to be idempotent, except if best_tac instantiates variables 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

95 
in some of the subgoals*) 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

96 
fun mk_auto_tac (cs, ss) m n = 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

97 
let val cs' = cs addss ss 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

98 
val maintac = 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

99 
blast_depth_tac cs m (*fast but can't use addss*) 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

100 
ORELSE' 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

101 
nodup_depth_tac cs' n; (*slower but more general*) 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

102 
in EVERY [ALLGOALS (asm_full_simp_tac ss), 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

103 
TRY (safe_tac cs'), 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

104 
REPEAT (FIRSTGOAL maintac), 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

105 
TRY (safe_tac (cs addSss ss)), 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

106 
prune_params_tac] 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

107 
end; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

108 
end; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

109 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

110 
fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

111 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

112 
fun Auto_tac st = auto_tac (claset(), simpset()) st; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

113 

d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

114 
fun auto () = by Auto_tac; 
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

115 

4659  116 
(* aimed to solve the given subgoal totally, using whatever tools possible *) 
117 
fun smart_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [ 

118 
clarify_tac cs' 1, 

119 
IF_UNSOLVED (asm_full_simp_tac ss 1), 

120 
IF_UNSOLVED (fast_tac cs' 1)]) end; 

121 
fun Smart_tac i = smart_tac (claset(), simpset()) i; 

122 
fun smart i = by (Smart_tac i); 

123 

4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

124 
end; 