author  wenzelm 
Fri, 13 May 2011 22:55:00 +0200  
changeset 42793  88bee9f6eec7 
parent 42784  a2dca9a3d0da 
child 42805  a6dafa3d7ada 
permissions  rwrr 
9772  1 
(* Title: Provers/clasimp.ML 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

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

3 

5219  4 
Combination of classical reasoner and simplifier (depends on 
16019  5 
splitter.ML, classical.ML, blast.ML). 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

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

7 

5219  8 
signature CLASIMP_DATA = 
9 
sig 

8469  10 
structure Splitter: SPLITTER 
5219  11 
structure Classical: CLASSICAL 
12 
structure Blast: BLAST 

9860  13 
val notE: thm 
14 
val iffD1: thm 

15 
val iffD2: thm 

42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

16 
end; 
5219  17 

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

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

19 
sig 
42793  20 
val addSss: Proof.context > Proof.context 
21 
val addss: Proof.context > Proof.context 

22 
val addss': Proof.context > Proof.context 

23 
val clarsimp_tac: Proof.context > int > tactic 

24 
val mk_auto_tac: Proof.context > int > int > tactic 

25 
val auto_tac: Proof.context > tactic 

26 
val force_tac: Proof.context > int > tactic 

27 
val fast_simp_tac: Proof.context > int > tactic 

28 
val slow_simp_tac: Proof.context > int > tactic 

29 
val best_simp_tac: Proof.context > int > tactic 

18728  30 
val iff_add: attribute 
31 
val iff_add': attribute 

32 
val iff_del: attribute 

30513  33 
val iff_modifiers: Method.modifier parser list 
34 
val clasimp_modifiers: Method.modifier parser list 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26425
diff
changeset

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

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

37 

42478  38 
functor Clasimp(Data: CLASIMP_DATA): CLASIMP = 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

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

40 

42478  41 
structure Splitter = Data.Splitter; 
42 
structure Classical = Data.Classical; 

43 
structure Blast = Data.Blast; 

5219  44 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26425
diff
changeset

45 

42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

46 
(* simp as classical wrapper *) 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

47 

9402  48 
(*not totally safe: may instantiate unknowns that appear also in other subgoals*) 
42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

49 
val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true); 
9402  50 

42793  51 
fun clasimp f name tac ctxt = 
52 
Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt; 

42478  53 

42793  54 
(*Add a simpset to the claset!*) 
55 
(*Caution: only one simpset added can be added by each of addSss and addss*) 

56 
val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac; 

57 
val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac; 

58 
(* FIXME "asm_lr_simp_tac" !? *) 

59 
val addss' = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_lr_simp_tac; 

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

60 

42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

61 

9860  62 
(* iffs: addition of rules to simpsets and clasets simultaneously *) 
63 

42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

64 
local 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

65 

11344  66 
(*Takes (possibly conditional) theorems of the form A<>B to 
9860  67 
the Safe Intr rule B==>A and 
68 
the Safe Destruct rule A==>B. 

69 
Also ~A goes to the Safe Elim rule A ==> ?R 

11462  70 
Failing other cases, A is added as a Safe Intr rule*) 
9860  71 

42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

72 
fun app (att: attribute) th context = #1 (att (context, th)); 
9860  73 

42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

74 
fun add_iff safe unsafe = 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

75 
Thm.declaration_attribute (fn th => 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

76 
let 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

77 
val n = nprems_of th; 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

78 
val (elim, intro) = if n = 0 then safe else unsafe; 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

79 
val zero_rotate = zero_var_indexes o rotate_prems n; 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

80 
in 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

81 
app intro (zero_rotate (th RS Data.iffD2)) #> 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

82 
app elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1))) 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

83 
handle THM _ => (app elim (zero_rotate (th RS Data.notE)) handle THM _ => app intro th) 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

84 
end); 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

85 

a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

86 
fun del_iff del = Thm.declaration_attribute (fn th => 
11902  87 
let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in 
42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

88 
app del (zero_rotate (th RS Data.iffD2)) #> 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

89 
app del (Tactic.make_elim (zero_rotate (th RS Data.iffD1))) 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

90 
handle THM _ => (app del (zero_rotate (th RS Data.notE)) handle THM _ => app del th) 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

91 
end); 
18630  92 

9860  93 
in 
94 

42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

95 
val iff_add = 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

96 
add_iff 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

97 
(Classical.safe_elim NONE, Classical.safe_intro NONE) 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

98 
(Classical.haz_elim NONE, Classical.haz_intro NONE) 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

99 
#> Simplifier.simp_add; 
10033
fc4e7432b2b1
added iff_add_global', iff_add_local' (syntax "iff?");
wenzelm
parents:
9952
diff
changeset

100 

42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

101 
val iff_add' = 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

102 
add_iff 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

103 
(Context_Rules.elim_query NONE, Context_Rules.intro_query NONE) 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

104 
(Context_Rules.elim_query NONE, Context_Rules.intro_query NONE); 
12375  105 

42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

106 
val iff_del = 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

107 
del_iff Classical.rule_del #> 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

108 
del_iff Context_Rules.rule_del #> 
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

109 
Simplifier.simp_del; 
12375  110 

9860  111 
end; 
112 

113 

42478  114 
(* tactics *) 
5219  115 

42793  116 
fun clarsimp_tac ctxt = 
117 
safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW 

118 
Classical.clarify_tac (addSss ctxt); 

12375  119 

5483  120 

5219  121 
(* auto_tac *) 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

122 

42793  123 
fun blast_depth_tac ctxt m i thm = 
124 
Blast.depth_tac ctxt m i thm 

42478  125 
handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty); 
9772  126 

127 
(* a variant of depth_tac that avoids interference of the simplifier 

5219  128 
with dup_step_tac when they are combined by auto_tac *) 
5756
8ef5288c24b0
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5567
diff
changeset

129 
local 
42478  130 

42793  131 
fun slow_step_tac' ctxt = 
132 
Classical.appWrappers ctxt 

133 
(Classical.instp_step_tac ctxt APPEND' Classical.haz_step_tac ctxt); 

42478  134 

135 
in 

136 

42793  137 
fun nodup_depth_tac ctxt m i st = 
42478  138 
SELECT_GOAL 
42793  139 
(Classical.safe_steps_tac ctxt 1 THEN_ELSE 
140 
(DEPTH_SOLVE (nodup_depth_tac ctxt m 1), 

141 
Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac 

142 
(slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m  1) 1)))) i st; 

42479  143 

5756
8ef5288c24b0
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5567
diff
changeset

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

145 

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

147 
in some of the subgoals*) 
42793  148 
fun mk_auto_tac ctxt m n = 
42478  149 
let 
150 
val main_tac = 

42793  151 
blast_depth_tac ctxt m (* fast but can't use wrappers *) 
42478  152 
ORELSE' 
42793  153 
(CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *) 
42478  154 
in 
42793  155 
PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac (simpset_of ctxt))) THEN 
156 
TRY (Classical.safe_tac ctxt) THEN 

42479  157 
REPEAT_DETERM (FIRSTGOAL main_tac) THEN 
42793  158 
TRY (Classical.safe_tac (addSss ctxt)) THEN 
42479  159 
prune_params_tac 
42478  160 
end; 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

161 

42793  162 
fun auto_tac ctxt = mk_auto_tac ctxt 4 2; 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

163 

9772  164 

5219  165 
(* force_tac *) 
166 

4659  167 
(* aimed to solve the given subgoal totally, using whatever tools possible *) 
42793  168 
fun force_tac ctxt = 
169 
let val ctxt' = addss ctxt in 

42479  170 
SELECT_GOAL 
42793  171 
(Classical.clarify_tac ctxt' 1 THEN 
172 
IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN 

173 
ALLGOALS (Classical.first_best_tac ctxt')) 

42478  174 
end; 
4659  175 

5219  176 

9805  177 
(* basic combinations *) 
178 

42793  179 
val fast_simp_tac = Classical.fast_tac o addss; 
180 
val slow_simp_tac = Classical.slow_tac o addss; 

181 
val best_simp_tac = Classical.best_tac o addss; 

9591  182 

183 

8639  184 

42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

185 
(** concrete syntax **) 
9860  186 

187 
(* attributes *) 

188 

30528  189 
fun iff_att x = (Scan.lift 
18688  190 
(Args.del >> K iff_del  
191 
Scan.option Args.add  Args.query >> K iff_add'  

30528  192 
Scan.option Args.add >> K iff_add)) x; 
9860  193 

194 

195 
(* method modifiers *) 

196 

197 
val iffN = "iff"; 

198 

199 
val iff_modifiers = 

18728  200 
[Args.$$$ iffN  Scan.option Args.add  Args.colon >> K ((I, iff_add): Method.modifier), 
201 
Args.$$$ iffN  Scan.option Args.add  Args.query_colon >> K (I, iff_add'), 

202 
Args.$$$ iffN  Args.del  Args.colon >> K (I, iff_del)]; 

9860  203 

8469  204 
val clasimp_modifiers = 
9860  205 
Simplifier.simp_modifiers @ Splitter.split_modifiers @ 
206 
Classical.cla_modifiers @ iff_modifiers; 

207 

208 

209 
(* methods *) 

5926  210 

30541  211 
fun clasimp_method' tac = 
42793  212 
Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac); 
9772  213 

30541  214 
val auto_method = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36601
diff
changeset

215 
Scan.lift (Scan.option (Parse.nat  Parse.nat))  
35613  216 
Method.sections clasimp_modifiers >> 
42793  217 
(fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac 
218 
 SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n)))); 

9772  219 

220 

221 
(* theory setup *) 

222 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26425
diff
changeset

223 
val clasimp_setup = 
30541  224 
Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #> 
225 
Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp" #> 

226 
Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #> 

227 
Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #> 

228 
Method.setup @{binding force} (clasimp_method' force_tac) "force" #> 

229 
Method.setup @{binding auto} auto_method "auto" #> 

230 
Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac)) 

231 
"clarify simplified goal"; 

5926  232 

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

233 
end; 