author  wenzelm 
Wed, 24 May 2000 19:09:50 +0200  
changeset 8966  916966f68907 
parent 8807  0046be1769f9 
child 9194  a57987e0250b 
permissions  rwrr 
5824  1 
(* Title: Pure/Isar/method.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

8807  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5824  5 

6 
Proof methods. 

7 
*) 

8 

9 
signature BASIC_METHOD = 

10 
sig 

11 
val print_methods: theory > unit 

12 
val Method: bstring > (Args.src > Proof.context > Proof.method) > string > unit 

13 
end; 

14 

15 
signature METHOD = 

16 
sig 

17 
include BASIC_METHOD 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

18 
val print_global_rules: theory > unit 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

19 
val print_local_rules: Proof.context > unit 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

20 
val dest_global: theory attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

21 
val elim_global: theory attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

22 
val intro_global: theory attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

23 
val delrule_global: theory attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

24 
val dest_local: Proof.context attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

25 
val elim_local: Proof.context attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

26 
val intro_local: Proof.context attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

27 
val delrule_local: Proof.context attribute 
6091  28 
val METHOD: (thm list > tactic) > Proof.method 
8372  29 
val METHOD_CASES: 
30 
(thm list > thm > (thm * (string * RuleCases.T) list) Seq.seq) > Proof.method 

5824  31 
val METHOD0: tactic > Proof.method 
32 
val fail: Proof.method 

33 
val succeed: Proof.method 

8167  34 
val defer: int option > Proof.method 
35 
val prefer: int > Proof.method 

7419  36 
val insert_tac: thm list > int > tactic 
7574  37 
val insert: thm list > Proof.method 
7555  38 
val insert_facts: Proof.method 
7601  39 
val unfold: thm list > Proof.method 
7419  40 
val fold: thm list > Proof.method 
41 
val multi_resolve: thm list > thm > thm Seq.seq 

42 
val multi_resolves: thm list > thm list > thm Seq.seq 

8335  43 
val resolveq_tac: thm Seq.seq > int > tactic 
8372  44 
val resolveq_cases_tac: (thm * string list) Seq.seq 
45 
> int > thm > (thm * (string * RuleCases.T) list) Seq.seq 

6091  46 
val rule_tac: thm list > thm list > int > tactic 
47 
val rule: thm list > Proof.method 

7130  48 
val erule: thm list > Proof.method 
8220  49 
val drule: thm list > Proof.method 
50 
val frule: thm list > Proof.method 

8195  51 
val this: Proof.method 
7555  52 
val assumption: Proof.context > Proof.method 
8351  53 
val set_tactic: (Proof.context > thm list > tactic) > unit 
54 
val tactic: string > Proof.context > Proof.method 

5916  55 
exception METHOD_FAIL of (string * Position.T) * exn 
8720  56 
val help_methods: theory option > Pretty.T list 
5824  57 
val method: theory > Args.src > Proof.context > Proof.method 
58 
val add_methods: (bstring * (Args.src > Proof.context > Proof.method) * string) list 

59 
> theory > theory 

5884  60 
val syntax: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list)) > 
8282  61 
Args.src > Proof.context > Proof.context * 'a 
8351  62 
val simple_args: (Args.T list > 'a * Args.T list) 
63 
> ('a > Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 

7555  64 
val ctxt_args: (Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 
5884  65 
val no_args: Proof.method > Args.src > Proof.context > Proof.method 
7268  66 
type modifier 
7601  67 
val sectioned_args: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list)) > 
7268  68 
(Args.T list > modifier * Args.T list) list > 
5884  69 
('a > Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 
7601  70 
val bang_sectioned_args: 
71 
(Args.T list > modifier * Args.T list) list > 

7555  72 
(thm list > Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 
7601  73 
val only_sectioned_args: 
74 
(Args.T list > modifier * Args.T list) list > 

5884  75 
(Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 
8093  76 
val thms_ctxt_args: (thm list > Proof.context > Proof.method) 
77 
> Args.src > Proof.context > Proof.method 

6091  78 
val thms_args: (thm list > Proof.method) > Args.src > Proof.context > Proof.method 
5824  79 
datatype text = 
80 
Basic of (Proof.context > Proof.method)  

81 
Source of Args.src  

82 
Then of text list  

83 
Orelse of text list  

84 
Try of text  

85 
Repeat1 of text 

86 
val refine: text > Proof.state > Proof.state Seq.seq 

8238  87 
val refine_end: text > Proof.state > Proof.state Seq.seq 
5824  88 
val proof: text option > Proof.state > Proof.state Seq.seq 
8966  89 
val local_qed: bool > text option 
6981  90 
> ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 
6736  91 
> Proof.state > Proof.state Seq.seq 
6981  92 
val local_terminal_proof: text * text option 
93 
> ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 

6736  94 
> Proof.state > Proof.state Seq.seq 
6981  95 
val local_default_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 
6736  96 
> Proof.state > Proof.state Seq.seq 
8966  97 
val local_immediate_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 
98 
> Proof.state > Proof.state Seq.seq 

99 
val local_done_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 

100 
> Proof.state > Proof.state Seq.seq 

101 
val global_qed: bool > text option 

102 
> Proof.state > theory * {kind: string, name: string, thm: thm} 

6934  103 
val global_terminal_proof: text * text option 
104 
> Proof.state > theory * {kind: string, name: string, thm: thm} 

8966  105 
val global_default_proof: Proof.state > theory * {kind: string, name: string, thm: thm} 
6532  106 
val global_immediate_proof: Proof.state > theory * {kind: string, name: string, thm: thm} 
8966  107 
val global_done_proof: Proof.state > theory * {kind: string, name: string, thm: thm} 
5824  108 
val setup: (theory > theory) list 
109 
end; 

110 

111 
structure Method: METHOD = 

112 
struct 

113 

114 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

115 
(** global and local rule data **) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

116 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

117 
fun prt_rules kind ths = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

118 
Pretty.writeln (Pretty.big_list ("standard " ^ kind ^ " rules:") (map Display.pretty_thm ths)); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

119 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

120 
fun print_rules (intro, elim) = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

121 
(prt_rules "introduction" intro; prt_rules "elimination" elim); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

122 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

123 
fun merge_rules (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

124 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

125 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

126 
(* theory data kind 'Isar/rules' *) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

127 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

128 
structure GlobalRulesArgs = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

129 
struct 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

130 
val name = "Isar/rules"; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

131 
type T = thm list * thm list; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

132 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

133 
val empty = ([], []); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

134 
val copy = I; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

135 
val prep_ext = I; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

136 
fun merge ((intro1, elim1), (intro2, elim2)) = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

137 
(merge_rules (intro1, intro2), merge_rules (elim1, elim2)); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

138 
fun print _ = print_rules; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

139 
end; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

140 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

141 
structure GlobalRules = TheoryDataFun(GlobalRulesArgs); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

142 
val print_global_rules = GlobalRules.print; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

143 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

144 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

145 
(* proof data kind 'Isar/rules' *) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

146 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

147 
structure LocalRulesArgs = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

148 
struct 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

149 
val name = "Isar/rules"; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

150 
type T = thm list * thm list; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

151 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

152 
val init = GlobalRules.get; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

153 
fun print _ = print_rules; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

154 
end; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

155 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

156 
structure LocalRules = ProofDataFun(LocalRulesArgs); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

157 
val print_local_rules = LocalRules.print; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

158 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

159 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

160 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

161 
(** attributes **) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

162 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

163 
(* add rules *) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

164 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

165 
local 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

166 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

167 
fun add_rule thm rules = Library.gen_ins Thm.eq_thm (thm, rules); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

168 
fun del_rule thm rules = Library.gen_rem Thm.eq_thm (rules, thm); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

169 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

170 
fun add_dest thm (intro, elim) = (intro, add_rule (Tactic.make_elim thm) elim); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

171 
fun add_elim thm (intro, elim) = (intro, add_rule thm elim); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

172 
fun add_intro thm (intro, elim) = (add_rule thm intro, elim); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

173 
fun delrule thm (intro, elim) = (del_rule thm intro, del_rule thm elim); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

174 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

175 
fun mk_att f g (x, thm) = (f (g thm) x, thm); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

176 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

177 
in 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

178 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

179 
val dest_global = mk_att GlobalRules.map add_dest; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

180 
val elim_global = mk_att GlobalRules.map add_elim; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

181 
val intro_global = mk_att GlobalRules.map add_intro; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

182 
val delrule_global = mk_att GlobalRules.map delrule; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

183 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

184 
val dest_local = mk_att LocalRules.map add_dest; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

185 
val elim_local = mk_att LocalRules.map add_elim; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

186 
val intro_local = mk_att LocalRules.map add_intro; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

187 
val delrule_local = mk_att LocalRules.map delrule; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

188 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

189 
end; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

190 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

191 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

192 
(* concrete syntax *) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

193 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

194 
val rule_atts = 
8519  195 
[("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local), "declare destruction rule"), 
196 
("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local), "declare elimination rule"), 

197 
("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), "declare introduction rule"), 

198 
("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local), "undeclare rule")]; 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

199 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

200 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

201 

5824  202 
(** proof methods **) 
203 

8372  204 
(* make methods *) 
5824  205 

6849  206 
val METHOD = Proof.method; 
8372  207 
val METHOD_CASES = Proof.method_cases; 
208 

8966  209 
fun METHOD0 tac = METHOD (fn [] => tac  _ => error "Cannot handle current facts"); 
5824  210 

211 

212 
(* primitive *) 

213 

214 
val fail = METHOD (K no_tac); 

215 
val succeed = METHOD (K all_tac); 

216 

217 

8167  218 
(* shuffle *) 
219 

8240  220 
fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1))); 
8167  221 
fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1))); 
222 

223 

7419  224 
(* insert *) 
225 

226 
local 

5824  227 

6981  228 
fun cut_rule_tac raw_rule = 
229 
let 

230 
val rule = Drule.forall_intr_vars raw_rule; 

231 
val revcut_rl = Drule.incr_indexes_wrt [] [] [] [rule] Drule.revcut_rl; 

7555  232 
in Tactic.rtac (rule COMP revcut_rl) end; 
6981  233 

7419  234 
in 
5824  235 

7419  236 
fun insert_tac [] i = all_tac 
237 
 insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); 

6981  238 

7555  239 
val insert_facts = METHOD (ALLGOALS o insert_tac); 
7664  240 
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); 
7419  241 

242 
end; 

5824  243 

244 

7601  245 
(* unfold / fold definitions *) 
6532  246 

7601  247 
fun unfold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN rewrite_goals_tac thms); 
7555  248 
fun fold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN fold_goals_tac thms); 
6532  249 

250 

7419  251 
(* multi_resolve *) 
252 

253 
local 

254 

255 
fun res th i rule = 

256 
Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty; 

257 

258 
fun multi_res _ [] rule = Seq.single rule 

259 
 multi_res i (th :: ths) rule = Seq.flat (Seq.map (res th i) (multi_res (i + 1) ths rule)); 

260 

261 
in 

262 

263 
val multi_resolve = multi_res 1; 

8372  264 
fun multi_resolves facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules)); 
7419  265 

266 
end; 

267 

268 

8372  269 
(* general rule *) 
5824  270 

8335  271 
fun gen_resolveq_tac tac rules i st = 
8372  272 
Seq.flat (Seq.map (fn rule => tac rule i st) rules); 
273 

274 
val resolveq_tac = gen_resolveq_tac Tactic.rtac; 

8335  275 

8372  276 
val resolveq_cases_tac = gen_resolveq_tac (fn (rule, cases) => fn i => fn st => 
277 
Seq.map (rpair (RuleCases.make rule cases)) (Tactic.rtac rule i st)); 

8335  278 

279 

8372  280 
(* simple rule *) 
281 

7419  282 
local 
5824  283 

7130  284 
fun gen_rule_tac tac rules [] = tac rules 
8372  285 
 gen_rule_tac tac erules facts = gen_resolveq_tac (tac o single) (multi_resolves facts erules); 
7130  286 

8671  287 
fun gen_rule tac rules = METHOD (HEADGOAL o tac rules); 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

288 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

289 
fun gen_rule' tac arg_rules ctxt = METHOD (fn facts => 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

290 
let val rules = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

291 
if not (null arg_rules) then arg_rules 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

292 
else if null facts then #1 (LocalRules.get ctxt) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

293 
else op @ (LocalRules.get ctxt); 
8671  294 
in HEADGOAL (tac rules facts) end); 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

295 

8220  296 
fun setup raw_tac = 
297 
let val tac = gen_rule_tac raw_tac 

298 
in (tac, gen_rule tac, gen_rule' tac) end; 

299 

7419  300 
in 
301 

8220  302 
val (rule_tac, rule, some_rule) = setup Tactic.resolve_tac; 
303 
val (erule_tac, erule, some_erule) = setup Tactic.eresolve_tac; 

304 
val (drule_tac, drule, some_drule) = setup Tactic.dresolve_tac; 

305 
val (frule_tac, frule, some_frule) = setup Tactic.forward_tac; 

5824  306 

7419  307 
end; 
308 

309 

8195  310 
(* this *) 
311 

8671  312 
val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac)); 
8195  313 

314 

315 
(* assumption *) 

7555  316 

317 
fun assm_tac ctxt = 

318 
assume_tac APPEND' resolve_tac (filter Thm.no_prems (ProofContext.prems_of ctxt)); 

7419  319 

7555  320 
fun assumption_tac ctxt [] = assm_tac ctxt 
321 
 assumption_tac _ [fact] = resolve_tac [fact] 

322 
 assumption_tac _ _ = K no_tac; 

7419  323 

8671  324 
fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt); 
7419  325 

326 

8329  327 
(* res_inst_tac emulations *) 
8238  328 

8329  329 
(*Note: insts refer to the implicit (!) goal context; use at your own risk*) 
8537  330 
fun gen_res_inst tac (quant, (insts, thm)) = 
331 
METHOD (fn facts => (quant (insert_tac facts THEN' tac insts thm))); 

8238  332 

333 
val res_inst = gen_res_inst Tactic.res_inst_tac; 

334 
val eres_inst = gen_res_inst Tactic.eres_inst_tac; 

335 
val dres_inst = gen_res_inst Tactic.dres_inst_tac; 

336 
val forw_inst = gen_res_inst Tactic.forw_inst_tac; 

337 

338 

8329  339 
(* simple Prolog interpreter *) 
340 

341 
fun prolog_tac rules facts = 

342 
DEPTH_SOLVE_1 (HEADGOAL (Tactic.assume_tac APPEND' Tactic.resolve_tac (facts @ rules))); 

343 

344 
val prolog = METHOD o prolog_tac; 

345 

346 

8351  347 
(* ML tactics *) 
348 

349 
val tactic_ref = ref ((fn _ => raise Match): Proof.context > thm list > tactic); 

350 
fun set_tactic f = tactic_ref := f; 

351 

352 
fun tactic txt ctxt = METHOD (fn facts => 

8372  353 
(Context.use_mltext 
8671  354 
("let fun tactic (ctxt: PureIsar.Proof.context) (facts: thm list) : tactic = \ 
8613  355 
\let val thm = PureIsar.ProofContext.get_thm ctxt and thms = PureIsar.ProofContext.get_thms ctxt in\n" 
8372  356 
^ txt ^ 
8613  357 
"\nend in PureIsar.Method.set_tactic tactic end") 
8372  358 
false (Some (ProofContext.theory_of ctxt)); ! tactic_ref ctxt facts)); 
8351  359 

360 

5824  361 

362 
(** methods theory data **) 

363 

364 
(* data kind 'Isar/methods' *) 

365 

366 
structure MethodsDataArgs = 

367 
struct 

368 
val name = "Isar/methods"; 

369 
type T = 

370 
{space: NameSpace.T, 

371 
meths: (((Args.src > Proof.context > Proof.method) * string) * stamp) Symtab.table}; 

372 

373 
val empty = {space = NameSpace.empty, meths = Symtab.empty}; 

6546  374 
val copy = I; 
5824  375 
val prep_ext = I; 
376 
fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) = 

377 
{space = NameSpace.merge (space1, space2), 

378 
meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups => 

379 
error ("Attempt to merge different versions of methods " ^ commas_quote dups)}; 

380 

8720  381 
fun pretty_meths verbose {space, meths} = 
5824  382 
let 
383 
fun prt_meth (name, ((_, comment), _)) = Pretty.block 

6849  384 
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; 
5824  385 
in 
8720  386 
(if not verbose then [] else [Display.pretty_name_space ("method name space", space)]) @ 
387 
[Pretty.big_list "methods:" (map prt_meth (NameSpace.cond_extern_table space meths))] 

5824  388 
end; 
7367  389 

8720  390 
fun print _ = Pretty.writeln o Pretty.chunks o pretty_meths true; 
5824  391 
end; 
392 

393 
structure MethodsData = TheoryDataFun(MethodsDataArgs); 

394 
val print_methods = MethodsData.print; 

7611  395 

8720  396 
fun help_methods None = [Pretty.str "methods: (unkown theory context)"] 
397 
 help_methods (Some thy) = MethodsDataArgs.pretty_meths false (MethodsData.get thy); 

5824  398 

399 

400 
(* get methods *) 

401 

5916  402 
exception METHOD_FAIL of (string * Position.T) * exn; 
403 

5824  404 
fun method thy = 
405 
let 

406 
val {space, meths} = MethodsData.get thy; 

407 

5884  408 
fun meth src = 
409 
let 

410 
val ((raw_name, _), pos) = Args.dest_src src; 

411 
val name = NameSpace.intern space raw_name; 

412 
in 

5824  413 
(case Symtab.lookup (meths, name) of 
414 
None => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos) 

5916  415 
 Some ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src)) 
5824  416 
end; 
417 
in meth end; 

418 

419 

420 
(* add_methods *) 

421 

422 
fun add_methods raw_meths thy = 

423 
let 

424 
val full = Sign.full_name (Theory.sign_of thy); 

425 
val new_meths = 

426 
map (fn (name, f, comment) => (full name, ((f, comment), stamp ()))) raw_meths; 

427 

428 
val {space, meths} = MethodsData.get thy; 

429 
val space' = NameSpace.extend (space, map fst new_meths); 

430 
val meths' = Symtab.extend (meths, new_meths) handle Symtab.DUPS dups => 

431 
error ("Duplicate declaration of method(s) " ^ commas_quote dups); 

432 
in 

433 
thy > MethodsData.put {space = space', meths = meths'} 

434 
end; 

435 

436 
(*implicit version*) 

437 
fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]); 

438 

439 

5884  440 

441 
(** method syntax **) 

5824  442 

5884  443 
(* basic *) 
444 

445 
fun syntax (scan: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list))) = 

446 
Args.syntax "method" scan; 

5824  447 

8351  448 
fun simple_args scan f src ctxt : Proof.method = 
449 
#2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt); 

450 

7555  451 
fun ctxt_args (f: Proof.context > Proof.method) src ctxt = 
8282  452 
#2 (syntax (Scan.succeed (f ctxt)) src ctxt); 
7555  453 

454 
fun no_args m = ctxt_args (K m); 

5884  455 

456 

8351  457 

5884  458 
(* sections *) 
5824  459 

7268  460 
type modifier = (Proof.context > Proof.context) * Proof.context attribute; 
461 

462 
local 

463 

8381  464 
fun sect ss = Scan.first (map Scan.lift ss); 
5884  465 
fun thms ss = Scan.unless (sect ss) Attrib.local_thms; 
466 
fun thmss ss = Scan.repeat (thms ss) >> flat; 

467 

7268  468 
fun apply (f, att) (ctxt, ths) = Thm.applys_attributes ((f ctxt, ths), [att]); 
5824  469 

7268  470 
fun section ss = (sect ss  thmss ss) : (fn (m, ths) => Scan.depend (fn ctxt => 
471 
Scan.succeed (apply m (ctxt, ths)))) >> #2; 

5884  472 

7601  473 
fun sectioned args ss = args  Scan.repeat (section ss); 
5884  474 

7268  475 
in 
5824  476 

5884  477 
fun sectioned_args args ss f src ctxt = 
8282  478 
let val (ctxt', (x, _)) = syntax (sectioned args ss) src ctxt 
5921  479 
in f x ctxt' end; 
5884  480 

7601  481 
fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f; 
482 
fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f); 

7268  483 

8093  484 
fun thms_ctxt_args f = sectioned_args (thmss []) [] f; 
485 
fun thms_args f = thms_ctxt_args (K o f); 

5824  486 

7268  487 
end; 
488 

5824  489 

8238  490 
(* insts *) 
491 

492 
val insts = 

8537  493 
Args.enum1 "and" (Scan.lift (Args.name  Args.!!! (Args.$$$ "="  Args.name)))  
8238  494 
(Scan.lift (Args.$$$ "in")  Attrib.local_thm); 
495 

8537  496 
fun inst_args f = f oo (#2 oo syntax (Args.goal_spec HEADGOAL  insts)); 
497 

498 

499 
(* subgoal *) 

500 

501 
fun subgoal x = (Args.goal_spec HEADGOAL  Scan.lift Args.name >> 

502 
(fn (quant, s) => METHOD (fn facts => quant (insert_tac facts THEN' Tactic.subgoal_tac s)))) x; 

503 

504 
val subgoal_meth = #2 oo syntax subgoal; 

8238  505 

506 

5824  507 

508 
(** method text **) 

509 

510 
(* datatype text *) 

511 

512 
datatype text = 

513 
Basic of (Proof.context > Proof.method)  

514 
Source of Args.src  

515 
Then of text list  

516 
Orelse of text list  

517 
Try of text  

518 
Repeat1 of text; 

519 

520 

521 
(* refine *) 

522 

8238  523 
fun gen_refine f text state = 
5824  524 
let 
525 
val thy = Proof.theory_of state; 

526 

8238  527 
fun eval (Basic mth) = f mth 
528 
 eval (Source src) = f (method thy src) 

5824  529 
 eval (Then txts) = Seq.EVERY (map eval txts) 
530 
 eval (Orelse txts) = Seq.FIRST (map eval txts) 

531 
 eval (Try txt) = Seq.TRY (eval txt) 

532 
 eval (Repeat1 txt) = Seq.REPEAT1 (eval txt); 

533 
in eval text state end; 

534 

8238  535 
val refine = gen_refine Proof.refine; 
536 
val refine_end = gen_refine Proof.refine_end; 

6404  537 

5824  538 

6404  539 
(* structured proof steps *) 
5824  540 

7506  541 
val default_text = Source (Args.src (("default", []), Position.none)); 
8195  542 
val this_text = Basic (K this); 
8966  543 
val done_text = Basic (K (METHOD0 all_tac)); 
7555  544 

8966  545 
fun close_text asm = Basic (fn ctxt => METHOD (K 
546 
(FILTER Thm.no_prems ((if asm then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac)))); 

547 

548 
fun finish_text asm None = close_text asm 

549 
 finish_text asm (Some txt) = Then [txt, close_text asm]; 

6872  550 

5824  551 
fun proof opt_text state = 
552 
state 

553 
> Proof.assert_backward 

6404  554 
> refine (if_none opt_text default_text) 
8242  555 
> Seq.map (Proof.goal_facts (K [])) 
5824  556 
> Seq.map Proof.enter_forward; 
557 

8966  558 
fun local_qed asm opt_text = Proof.local_qed (refine (finish_text asm opt_text)); 
559 
fun local_terminal_proof (text, opt_text) pr = 

560 
Seq.THEN (proof (Some text), local_qed true opt_text pr); 

561 
val local_default_proof = local_terminal_proof (default_text, None); 

8195  562 
val local_immediate_proof = local_terminal_proof (this_text, None); 
8966  563 
fun local_done_proof pr = Seq.THEN (proof (Some done_text), local_qed false None pr); 
5824  564 

6872  565 

8966  566 
fun global_qeds asm opt_text = Proof.global_qed (refine (finish_text asm opt_text)); 
5824  567 

8966  568 
fun global_qed asm opt_text state = 
6872  569 
state 
8966  570 
> global_qeds asm opt_text 
6872  571 
> Proof.check_result "Failed to finish proof" state 
572 
> Seq.hd; 

573 

8966  574 
fun global_term_proof asm (text, opt_text) state = 
6872  575 
state 
576 
> proof (Some text) 

577 
> Proof.check_result "Terminal proof method failed" state 

8966  578 
> (Seq.flat o Seq.map (global_qeds asm opt_text)) 
6872  579 
> Proof.check_result "Failed to finish proof (after successful terminal method)" state 
580 
> Seq.hd; 

581 

8966  582 
val global_terminal_proof = global_term_proof true; 
6934  583 
val global_default_proof = global_terminal_proof (default_text, None); 
8966  584 
val global_immediate_proof = global_terminal_proof (this_text, None); 
585 
val global_done_proof = global_term_proof false (done_text, None); 

5824  586 

587 

588 
(** theory setup **) 

589 

590 
(* pure_methods *) 

591 

592 
val pure_methods = 

593 
[("fail", no_args fail, "force failure"), 

594 
("succeed", no_args succeed, "succeed"), 

7574  595 
("", no_args insert_facts, "do nothing, inserting current facts only"), 
7664  596 
("insert", thms_args insert, "insert theorems, ignoring facts (improper!)"), 
7601  597 
("unfold", thms_args unfold, "unfold definitions"), 
598 
("fold", thms_args fold, "fold definitions"), 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

599 
("default", thms_ctxt_args some_rule, "apply some rule"), 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

600 
("rule", thms_ctxt_args some_rule, "apply some rule"), 
8220  601 
("erule", thms_ctxt_args some_erule, "apply some rule in elimination manner (improper!)"), 
602 
("drule", thms_ctxt_args some_drule, "apply some rule in destruct manner (improper!)"), 

603 
("frule", thms_ctxt_args some_frule, "apply some rule in forward manner (improper!)"), 

8195  604 
("this", no_args this, "apply current facts as rules"), 
8238  605 
("assumption", ctxt_args assumption, "proof by assumption, preferring facts"), 
8537  606 
("res_inst_tac", inst_args res_inst, "res_inst_tac emulation (dynamic instantiation!)"), 
607 
("eres_inst_tac", inst_args eres_inst, "eres_inst_tac emulation (dynamic instantiation!)"), 

608 
("dres_inst_tac", inst_args dres_inst, "dres_inst_tac emulation (dynamic instantiation!)"), 

609 
("forw_inst_tac", inst_args forw_inst, "forw_inst_tac emulation (dynamic instantiation!)"), 

610 
("subgoal_tac", subgoal_meth, "subgoal_tac emulation (dynamic instantiation!)"), 

8351  611 
("prolog", thms_args prolog, "simple prolog interpreter"), 
612 
("tactic", simple_args Args.name tactic, "ML tactic as proof method")]; 

5824  613 

614 

615 
(* setup *) 

616 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

617 
val setup = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

618 
[GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts, 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

619 
MethodsData.init, add_methods pure_methods]; 
5824  620 

621 

622 
end; 

623 

624 

625 
structure BasicMethod: BASIC_METHOD = Method; 

626 
open BasicMethod; 