author  nipkow 
Mon, 12 Sep 2011 07:55:43 +0200  
changeset 44890  22f665a2e91c 
parent 43331  01f051619eee 
child 45375  7fe19930dfc9 
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 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
43331
diff
changeset

26 
val fast_force_tac: Proof.context > int > tactic 
42793  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 

9772  120 
(* a variant of depth_tac that avoids interference of the simplifier 
5219  121 
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

122 
local 
42478  123 

42793  124 
fun slow_step_tac' ctxt = 
125 
Classical.appWrappers ctxt 

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

42478  127 

128 
in 

129 

42793  130 
fun nodup_depth_tac ctxt m i st = 
42478  131 
SELECT_GOAL 
42793  132 
(Classical.safe_steps_tac ctxt 1 THEN_ELSE 
133 
(DEPTH_SOLVE (nodup_depth_tac ctxt m 1), 

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

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

42479  136 

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

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

138 

43331
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
42805
diff
changeset

139 
(*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

140 
in some of the subgoals*) 
42793  141 
fun mk_auto_tac ctxt m n = 
42478  142 
let 
143 
val main_tac = 

43331
01f051619eee
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents:
42805
diff
changeset

144 
Blast.depth_tac ctxt m (* fast but can't use wrappers *) 
42478  145 
ORELSE' 
42793  146 
(CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *) 
42478  147 
in 
42793  148 
PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac (simpset_of ctxt))) THEN 
149 
TRY (Classical.safe_tac ctxt) THEN 

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

154 

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

156 

9772  157 

5219  158 
(* force_tac *) 
159 

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

42479  163 
SELECT_GOAL 
42793  164 
(Classical.clarify_tac ctxt' 1 THEN 
165 
IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN 

166 
ALLGOALS (Classical.first_best_tac ctxt')) 

42478  167 
end; 
4659  168 

5219  169 

9805  170 
(* basic combinations *) 
171 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
43331
diff
changeset

172 
fun fast_simp_tac ctxt i = 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
43331
diff
changeset

173 
let val _ = legacy_feature "Old name 'fastsimp'  use 'fastforce' instead" 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
43331
diff
changeset

174 
in Classical.fast_tac (addss ctxt) i end; 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
43331
diff
changeset

175 

22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
43331
diff
changeset

176 
val fast_force_tac = Classical.fast_tac o addss; 
42793  177 
val slow_simp_tac = Classical.slow_tac o addss; 
178 
val best_simp_tac = Classical.best_tac o addss; 

9591  179 

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

180 
(** concrete syntax **) 
9860  181 

182 
(* attributes *) 

183 

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

30528  187 
Scan.option Args.add >> K iff_add)) x; 
9860  188 

189 

190 
(* method modifiers *) 

191 

192 
val iffN = "iff"; 

193 

194 
val iff_modifiers = 

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

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

9860  198 

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

202 

203 

204 
(* methods *) 

5926  205 

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

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

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

9772  214 

215 

216 
(* theory setup *) 

217 

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

218 
val clasimp_setup = 
30541  219 
Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #> 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
43331
diff
changeset

220 
Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp (legacy name)" #> 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
43331
diff
changeset

221 
Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #> 
30541  222 
Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #> 
223 
Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #> 

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

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

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

227 
"clarify simplified goal"; 

5926  228 

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

229 
end; 