author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 58048  aa6296d09e0e 
child 58826  2ed2eaabe3df 
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 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

47 
(* FIXME !? *) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

48 
fun clasimp f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt)); 
42478  49 

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

50111  52 
val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac; 
42793  53 
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

54 

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

55 

9860  56 
(* iffs: addition of rules to simpsets and clasets simultaneously *) 
57 

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

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

59 

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

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

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

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

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

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

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

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

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

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

72 
in 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

73 
Thm.attribute_declaration intro (zero_rotate (th RS Data.iffD2)) #> 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

74 
Thm.attribute_declaration elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1))) 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

75 
handle THM _ => 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

76 
(Thm.attribute_declaration elim (zero_rotate (th RS Data.notE)) 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

77 
handle THM _ => Thm.attribute_declaration intro th) 
42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

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

79 

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

80 
fun del_iff del = Thm.declaration_attribute (fn th => 
11902  81 
let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

82 
Thm.attribute_declaration del (zero_rotate (th RS Data.iffD2)) #> 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

83 
Thm.attribute_declaration del (Tactic.make_elim (zero_rotate (th RS Data.iffD1))) 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

84 
handle THM _ => 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

85 
(Thm.attribute_declaration del (zero_rotate (th RS Data.notE)) 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

86 
handle THM _ => Thm.attribute_declaration del th) 
42784
a2dca9a3d0da
simplified clasimpset declarations  prefer attributes;
wenzelm
parents:
42479
diff
changeset

87 
end); 
18630  88 

9860  89 
in 
90 

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

91 
val iff_add = 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

92 
Thm.declaration_attribute (fn th => 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

93 
Thm.attribute_declaration (add_iff 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

94 
(Classical.safe_elim NONE, Classical.safe_intro NONE) 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

95 
(Classical.haz_elim NONE, Classical.haz_intro NONE)) th 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

96 
#> Thm.attribute_declaration Simplifier.simp_add th); 
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 = 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

104 
Thm.declaration_attribute (fn th => 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

105 
Thm.attribute_declaration (del_iff Classical.rule_del) th #> 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

106 
Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #> 
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
44890
diff
changeset

107 
Thm.attribute_declaration Simplifier.simp_del th); 
12375  108 

9860  109 
end; 
110 

111 

42478  112 
(* tactics *) 
5219  113 

42793  114 
fun clarsimp_tac ctxt = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

115 
Simplifier.safe_asm_full_simp_tac ctxt THEN_ALL_NEW 
42793  116 
Classical.clarify_tac (addSss ctxt); 
12375  117 

5483  118 

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

120 

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

123 
local 
42478  124 

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

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

42478  128 

129 
in 

130 

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

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

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

42479  137 

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

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

139 

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

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

141 
in some of the subgoals*) 
42793  142 
fun mk_auto_tac ctxt m n = 
42478  143 
let 
144 
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

145 
Blast.depth_tac ctxt m (* fast but can't use wrappers *) 
42478  146 
ORELSE' 
42793  147 
(CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *) 
42478  148 
in 
58008  149 
PARALLEL_ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN 
42793  150 
TRY (Classical.safe_tac ctxt) THEN 
42479  151 
REPEAT_DETERM (FIRSTGOAL main_tac) THEN 
42793  152 
TRY (Classical.safe_tac (addSss ctxt)) THEN 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset

153 
prune_params_tac ctxt 
42478  154 
end; 
4652
d24cca140eeb
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff
changeset

155 

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

157 

9772  158 

5219  159 
(* force_tac *) 
160 

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

42479  164 
SELECT_GOAL 
42793  165 
(Classical.clarify_tac ctxt' 1 THEN 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset

166 
IF_UNSOLVED (Simplifier.asm_full_simp_tac ctxt 1) THEN 
42793  167 
ALLGOALS (Classical.first_best_tac ctxt')) 
42478  168 
end; 
4659  169 

5219  170 

9805  171 
(* basic combinations *) 
172 

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

173 
val fast_force_tac = Classical.fast_tac o addss; 
42793  174 
val slow_simp_tac = Classical.slow_tac o addss; 
175 
val best_simp_tac = Classical.best_tac o addss; 

9591  176 

47967
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
45375
diff
changeset

177 

c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
45375
diff
changeset

178 

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

179 
(** concrete syntax **) 
9860  180 

181 
(* attributes *) 

182 

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

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

188 

189 
(* method modifiers *) 

190 

191 
val iffN = "iff"; 

192 

193 
val iff_modifiers = 

58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58008
diff
changeset

194 
[Args.$$$ iffN  Scan.option Args.add  Args.colon >> K (Method.modifier iff_add @{here}), 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58008
diff
changeset

195 
Args.$$$ iffN  Scan.option Args.add  Args.query_colon >> K (Method.modifier iff_add' @{here}), 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58008
diff
changeset

196 
Args.$$$ iffN  Args.del  Args.colon >> K (Method.modifier iff_del @{here})]; 
9860  197 

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

201 

202 

203 
(* methods *) 

5926  204 

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

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

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

9772  213 

214 

215 
(* theory setup *) 

216 

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

217 
val clasimp_setup = 
30541  218 
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

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

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

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

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

225 
"clarify simplified goal"; 

5926  226 

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

227 
end; 