author  wenzelm 
Sat, 14 May 2011 16:22:53 +0200  
changeset 42805  a6dafa3d7ada 
parent 42793  88bee9f6eec7 
child 43331  01f051619eee 
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 clarsimp_tac: Proof.context > int > tactic 

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

24 
val auto_tac: Proof.context > tactic 

25 
val force_tac: Proof.context > int > tactic 

26 
val fast_simp_tac: Proof.context > int > tactic 

27 
val slow_simp_tac: Proof.context > int > tactic 

28 
val best_simp_tac: Proof.context > int > tactic 

18728  29 
val iff_add: attribute 
30 
val iff_add': attribute 

31 
val iff_del: attribute 

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

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

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

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

36 

42478  37 
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

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

39 

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

42 
structure Blast = Data.Blast; 

5219  43 

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

44 

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

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

46 

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

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

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

42478  52 

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

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

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

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

57 

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

58 

9860  59 
(* iffs: addition of rules to simpsets and clasets simultaneously *) 
60 

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

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

62 

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

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

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

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

69 
fun app (att: attribute) th context = #1 (att (context, th)); 
9860  70 

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

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

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

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

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

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

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

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

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

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

80 
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

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

82 

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

83 
fun del_iff del = Thm.declaration_attribute (fn th => 
11902  84 
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

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

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

87 
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

88 
end); 
18630  89 

9860  90 
in 
91 

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

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

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

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

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

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

97 

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

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

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

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

101 
(Context_Rules.elim_query NONE, Context_Rules.intro_query NONE); 
12375  102 

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

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

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

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

106 
Simplifier.simp_del; 
12375  107 

9860  108 
end; 
109 

110 

42478  111 
(* tactics *) 
5219  112 

42793  113 
fun clarsimp_tac ctxt = 
114 
safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW 

115 
Classical.clarify_tac (addSss ctxt); 

12375  116 

5483  117 

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

119 

42793  120 
fun blast_depth_tac ctxt m i thm = 
121 
Blast.depth_tac ctxt m i thm 

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

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

5219  125 
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

126 
local 
42478  127 

42793  128 
fun slow_step_tac' ctxt = 
129 
Classical.appWrappers ctxt 

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

42478  131 

132 
in 

133 

42793  134 
fun nodup_depth_tac ctxt m i st = 
42478  135 
SELECT_GOAL 
42793  136 
(Classical.safe_steps_tac ctxt 1 THEN_ELSE 
137 
(DEPTH_SOLVE (nodup_depth_tac ctxt m 1), 

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

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

42479  140 

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

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

142 

9402  143 
(*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

144 
in some of the subgoals*) 
42793  145 
fun mk_auto_tac ctxt m n = 
42478  146 
let 
147 
val main_tac = 

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

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

158 

42793  159 
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

160 

9772  161 

5219  162 
(* force_tac *) 
163 

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

42479  167 
SELECT_GOAL 
42793  168 
(Classical.clarify_tac ctxt' 1 THEN 
169 
IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN 

170 
ALLGOALS (Classical.first_best_tac ctxt')) 

42478  171 
end; 
4659  172 

5219  173 

9805  174 
(* basic combinations *) 
175 

42793  176 
val fast_simp_tac = Classical.fast_tac o addss; 
177 
val slow_simp_tac = Classical.slow_tac o addss; 

178 
val best_simp_tac = Classical.best_tac o addss; 

9591  179 

180 

8639  181 

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

182 
(** concrete syntax **) 
9860  183 

184 
(* attributes *) 

185 

30528  186 
fun iff_att x = (Scan.lift 
18688  187 
(Args.del >> K iff_del  
188 
Scan.option Args.add  Args.query >> K iff_add'  

30528  189 
Scan.option Args.add >> K iff_add)) x; 
9860  190 

191 

192 
(* method modifiers *) 

193 

194 
val iffN = "iff"; 

195 

196 
val iff_modifiers = 

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

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

9860  200 

8469  201 
val clasimp_modifiers = 
9860  202 
Simplifier.simp_modifiers @ Splitter.split_modifiers @ 
203 
Classical.cla_modifiers @ iff_modifiers; 

204 

205 

206 
(* methods *) 

5926  207 

30541  208 
fun clasimp_method' tac = 
42793  209 
Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac); 
9772  210 

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

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

9772  216 

217 

218 
(* theory setup *) 

219 

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

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

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

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

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

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

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

228 
"clarify simplified goal"; 

5926  229 

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

230 
end; 