author  wenzelm 
Fri, 28 Jan 2000 12:10:47 +0100  
changeset 8153  9bdbcb71dc56 
parent 8093  d5eb246c94ec 
child 8167  7574835ed01e 
permissions  rwrr 
5824  1 
(* Title: Pure/Isar/method.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Proof methods. 

6 
*) 

7 

8 
signature BASIC_METHOD = 

9 
sig 

10 
val print_methods: theory > unit 

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

12 
end; 

13 

14 
signature METHOD = 

15 
sig 

16 
include BASIC_METHOD 

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

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

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

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

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

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

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

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

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

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

26 
val delrule_local: Proof.context attribute 
6091  27 
val METHOD: (thm list > tactic) > Proof.method 
5824  28 
val METHOD0: tactic > Proof.method 
29 
val fail: Proof.method 

30 
val succeed: Proof.method 

7419  31 
val insert_tac: thm list > int > tactic 
7574  32 
val insert: thm list > Proof.method 
7555  33 
val insert_facts: Proof.method 
7601  34 
val unfold: thm list > Proof.method 
7419  35 
val fold: thm list > Proof.method 
36 
val multi_resolve: thm list > thm > thm Seq.seq 

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

6091  38 
val rule_tac: thm list > thm list > int > tactic 
7130  39 
val erule_tac: thm list > thm list > int > tactic 
6091  40 
val rule: thm list > Proof.method 
7130  41 
val erule: thm list > Proof.method 
7555  42 
val assumption: Proof.context > Proof.method 
5916  43 
exception METHOD_FAIL of (string * Position.T) * exn 
7611  44 
val help_methods: theory option > unit 
5824  45 
val method: theory > Args.src > Proof.context > Proof.method 
46 
val add_methods: (bstring * (Args.src > Proof.context > Proof.method) * string) list 

47 
> theory > theory 

5884  48 
val syntax: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list)) > 
49 
Proof.context > Args.src > Proof.context * 'a 

7555  50 
val ctxt_args: (Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 
5884  51 
val no_args: Proof.method > Args.src > Proof.context > Proof.method 
7268  52 
type modifier 
7601  53 
val sectioned_args: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list)) > 
7268  54 
(Args.T list > modifier * Args.T list) list > 
5884  55 
('a > Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 
7601  56 
val bang_sectioned_args: 
57 
(Args.T list > modifier * Args.T list) list > 

7555  58 
(thm list > Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 
7601  59 
val only_sectioned_args: 
60 
(Args.T list > modifier * Args.T list) list > 

5884  61 
(Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 
8093  62 
val thms_ctxt_args: (thm list > Proof.context > Proof.method) 
63 
> Args.src > Proof.context > Proof.method 

6091  64 
val thms_args: (thm list > Proof.method) > Args.src > Proof.context > Proof.method 
5824  65 
datatype text = 
66 
Basic of (Proof.context > Proof.method)  

67 
Source of Args.src  

68 
Then of text list  

69 
Orelse of text list  

70 
Try of text  

71 
Repeat1 of text 

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

7506  73 
val refine_no_facts: text > Proof.state > Proof.state Seq.seq 
5824  74 
val proof: text option > Proof.state > Proof.state Seq.seq 
6981  75 
val local_qed: text option 
76 
> ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 

6736  77 
> Proof.state > Proof.state Seq.seq 
6981  78 
val local_terminal_proof: text * text option 
79 
> ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 

6736  80 
> Proof.state > Proof.state Seq.seq 
6981  81 
val local_immediate_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 
82 
> Proof.state > Proof.state Seq.seq 

83 
val local_default_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 

6736  84 
> Proof.state > Proof.state Seq.seq 
6951  85 
val global_qed: text option > Proof.state > theory * {kind: string, name: string, thm: thm} 
6934  86 
val global_terminal_proof: text * text option 
87 
> Proof.state > theory * {kind: string, name: string, thm: thm} 

6532  88 
val global_immediate_proof: Proof.state > theory * {kind: string, name: string, thm: thm} 
89 
val global_default_proof: Proof.state > theory * {kind: string, name: string, thm: thm} 

5824  90 
val setup: (theory > theory) list 
91 
end; 

92 

93 
structure Method: METHOD = 

94 
struct 

95 

96 

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

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

98 

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

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

100 
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

101 

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

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

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

104 

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

105 
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

106 

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

107 

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

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

109 

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

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

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

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

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

114 

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

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

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

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

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

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

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

121 
end; 
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 
structure GlobalRules = TheoryDataFun(GlobalRulesArgs); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

124 
val print_global_rules = GlobalRules.print; 
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 

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

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

128 

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

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

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

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

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

133 

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

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

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

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

137 

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

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

139 
val print_local_rules = LocalRules.print; 
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 

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

142 

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

143 
(** attributes **) 
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 
(* add 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 
local 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

148 

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

149 
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

150 
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

151 

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

152 
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

153 
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

154 
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

155 
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

156 

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

157 
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

158 

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

159 
in 
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 
val dest_global = mk_att GlobalRules.map add_dest; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

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

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

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

165 

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

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

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

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

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

170 

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

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

172 

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

173 

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

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

175 

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

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

177 
[("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local), "destruction rule"), 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

178 
("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local), "elimination rule"), 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

179 
("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), "introduction rule"), 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

180 
("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local), "delete rule")]; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

181 

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

182 

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

183 

5824  184 
(** proof methods **) 
185 

186 
(* method from tactic *) 

187 

6849  188 
val METHOD = Proof.method; 
5824  189 
fun METHOD0 tac = METHOD (fn [] => tac  _ => error "Method may not be used with facts"); 
190 

191 

192 
(* primitive *) 

193 

194 
val fail = METHOD (K no_tac); 

195 
val succeed = METHOD (K all_tac); 

196 

197 

7419  198 
(* insert *) 
199 

200 
local 

5824  201 

6981  202 
fun cut_rule_tac raw_rule = 
203 
let 

204 
val rule = Drule.forall_intr_vars raw_rule; 

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

7555  206 
in Tactic.rtac (rule COMP revcut_rl) end; 
6981  207 

7419  208 
in 
5824  209 

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

6981  212 

7555  213 
val insert_facts = METHOD (ALLGOALS o insert_tac); 
7664  214 
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); 
7419  215 

216 
end; 

5824  217 

218 

7601  219 
(* unfold / fold definitions *) 
6532  220 

7601  221 
fun unfold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN rewrite_goals_tac thms); 
7555  222 
fun fold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN fold_goals_tac thms); 
6532  223 

224 

7419  225 
(* multi_resolve *) 
226 

227 
local 

228 

229 
fun res th i rule = 

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

231 

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

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

234 

235 
in 

236 

237 
val multi_resolve = multi_res 1; 

238 
fun multi_resolves facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules)); 

239 

240 
end; 

241 

242 

5824  243 
(* rule *) 
244 

7419  245 
local 
5824  246 

7130  247 
fun gen_rule_tac tac rules [] = tac rules 
248 
 gen_rule_tac tac erules facts = 

5824  249 
let 
7419  250 
val rules = multi_resolves facts erules; 
7130  251 
fun tactic i state = Seq.flat (Seq.map (fn rule => tac [rule] i state) rules); 
252 
in tactic end; 

253 

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

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

255 

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

256 
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

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

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

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

260 
else op @ (LocalRules.get ctxt); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

261 
in FINDGOAL (tac rules facts) end); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

262 

7419  263 
in 
264 

7130  265 
val rule_tac = gen_rule_tac Tactic.resolve_tac; 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

266 
val rule = gen_rule rule_tac; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

267 
val some_rule = gen_rule' rule_tac; 
5824  268 

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

269 
val erule_tac = gen_rule_tac Tactic.eresolve_tac; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

270 
val erule = gen_rule erule_tac; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

271 
val some_erule = gen_rule' erule_tac; 
5824  272 

7419  273 
end; 
274 

275 

7555  276 
(* assumption / finish *) 
277 

278 
fun assm_tac ctxt = 

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

7419  280 

7555  281 
fun assumption_tac ctxt [] = assm_tac ctxt 
282 
 assumption_tac _ [fact] = resolve_tac [fact] 

283 
 assumption_tac _ _ = K no_tac; 

7419  284 

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

285 
fun assumption ctxt = METHOD (FINDGOAL o assumption_tac ctxt); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

286 
fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac))); 
7419  287 

288 

5824  289 

290 
(** methods theory data **) 

291 

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

293 

294 
structure MethodsDataArgs = 

295 
struct 

296 
val name = "Isar/methods"; 

297 
type T = 

298 
{space: NameSpace.T, 

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

300 

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

6546  302 
val copy = I; 
5824  303 
val prep_ext = I; 
304 
fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) = 

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

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

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

308 

7367  309 
fun print_meths verbose {space, meths} = 
5824  310 
let 
311 
fun prt_meth (name, ((_, comment), _)) = Pretty.block 

6849  312 
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; 
5824  313 
in 
7367  314 
if not verbose then () 
315 
else Pretty.writeln (Display.pretty_name_space ("method name space", space)); 

6849  316 
Pretty.writeln (Pretty.big_list "methods:" 
317 
(map prt_meth (NameSpace.cond_extern_table space meths))) 

5824  318 
end; 
7367  319 

320 
fun print _ = print_meths true; 

5824  321 
end; 
322 

323 
structure MethodsData = TheoryDataFun(MethodsDataArgs); 

324 
val print_methods = MethodsData.print; 

7611  325 

326 
fun help_methods None = writeln "methods: (unkown theory context)" 

327 
 help_methods (Some thy) = MethodsDataArgs.print_meths false (MethodsData.get thy); 

5824  328 

329 

330 
(* get methods *) 

331 

5916  332 
exception METHOD_FAIL of (string * Position.T) * exn; 
333 

5824  334 
fun method thy = 
335 
let 

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

337 

5884  338 
fun meth src = 
339 
let 

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

341 
val name = NameSpace.intern space raw_name; 

342 
in 

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

5916  345 
 Some ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src)) 
5824  346 
end; 
347 
in meth end; 

348 

349 

350 
(* add_methods *) 

351 

352 
fun add_methods raw_meths thy = 

353 
let 

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

355 
val new_meths = 

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

357 

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

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

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

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

362 
in 

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

364 
end; 

365 

366 
(*implicit version*) 

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

368 

369 

5884  370 

371 
(** method syntax **) 

5824  372 

5884  373 
(* basic *) 
374 

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

376 
Args.syntax "method" scan; 

5824  377 

7555  378 
fun ctxt_args (f: Proof.context > Proof.method) src ctxt = 
379 
#2 (syntax (Scan.succeed (f ctxt)) ctxt src); 

380 

381 
fun no_args m = ctxt_args (K m); 

5884  382 

383 

384 
(* sections *) 

5824  385 

7268  386 
type modifier = (Proof.context > Proof.context) * Proof.context attribute; 
387 

388 
local 

389 

5884  390 
fun sect ss = Scan.first (map (fn s => Scan.lift (s  Args.$$$ ":")) ss); 
391 
fun thms ss = Scan.unless (sect ss) Attrib.local_thms; 

392 
fun thmss ss = Scan.repeat (thms ss) >> flat; 

393 

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

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

5884  398 

7601  399 
fun sectioned args ss = args  Scan.repeat (section ss); 
5884  400 

7268  401 
in 
5824  402 

5884  403 
fun sectioned_args args ss f src ctxt = 
5921  404 
let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src 
405 
in f x ctxt' end; 

5884  406 

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

7268  409 

8093  410 
fun thms_ctxt_args f = sectioned_args (thmss []) [] f; 
411 
fun thms_args f = thms_ctxt_args (K o f); 

5824  412 

7268  413 
end; 
414 

5824  415 

416 

417 
(** method text **) 

418 

419 
(* datatype text *) 

420 

421 
datatype text = 

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

423 
Source of Args.src  

424 
Then of text list  

425 
Orelse of text list  

426 
Try of text  

427 
Repeat1 of text; 

428 

429 

430 
(* refine *) 

431 

432 
fun refine text state = 

433 
let 

434 
val thy = Proof.theory_of state; 

435 

436 
fun eval (Basic mth) = Proof.refine mth 

437 
 eval (Source src) = Proof.refine (method thy src) 

438 
 eval (Then txts) = Seq.EVERY (map eval txts) 

439 
 eval (Orelse txts) = Seq.FIRST (map eval txts) 

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

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

442 
in eval text state end; 

443 

7506  444 
fun refine_no_facts text state = 
445 
state 

446 
> Proof.goal_facts (K []) 

447 
> refine text; 

6404  448 

5824  449 

6404  450 
(* structured proof steps *) 
5824  451 

7506  452 
val default_text = Source (Args.src (("default", []), Position.none)); 
7555  453 

454 
fun finish_text None = Basic finish 

455 
 finish_text (Some txt) = Then [txt, Basic finish]; 

6872  456 

5824  457 
fun proof opt_text state = 
458 
state 

459 
> Proof.assert_backward 

6404  460 
> refine (if_none opt_text default_text) 
5824  461 
> Seq.map Proof.enter_forward; 
462 

7439  463 
fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_text)); 
6934  464 
fun local_terminal_proof (text, opt_text) pr = Seq.THEN (proof (Some text), local_qed opt_text pr); 
7555  465 
val local_immediate_proof = local_terminal_proof (Basic assumption, None); 
6934  466 
val local_default_proof = local_terminal_proof (default_text, None); 
5824  467 

6872  468 

7439  469 
fun global_qeds opt_text = Proof.global_qed (refine (finish_text opt_text)); 
5824  470 

6951  471 
fun global_qed opt_text state = 
6872  472 
state 
6951  473 
> global_qeds opt_text 
6872  474 
> Proof.check_result "Failed to finish proof" state 
475 
> Seq.hd; 

476 

6934  477 
fun global_terminal_proof (text, opt_text) state = 
6872  478 
state 
479 
> proof (Some text) 

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

6951  481 
> (Seq.flat o Seq.map (global_qeds opt_text)) 
6872  482 
> Proof.check_result "Failed to finish proof (after successful terminal method)" state 
483 
> Seq.hd; 

484 

7555  485 
val global_immediate_proof = global_terminal_proof (Basic assumption, None); 
6934  486 
val global_default_proof = global_terminal_proof (default_text, None); 
5824  487 

488 

489 

490 
(** theory setup **) 

491 

492 
(* pure_methods *) 

493 

494 
val pure_methods = 

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

496 
("succeed", no_args succeed, "succeed"), 

7574  497 
("", no_args insert_facts, "do nothing, inserting current facts only"), 
7664  498 
("insert", thms_args insert, "insert theorems, ignoring facts (improper!)"), 
7601  499 
("unfold", thms_args unfold, "unfold definitions"), 
500 
("fold", thms_args fold, "fold definitions"), 

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

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

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

503 
("erule", thms_ctxt_args some_erule, "apply some erule (improper!)"), 
7555  504 
("assumption", ctxt_args assumption, "proof by assumption, preferring facts")]; 
5824  505 

506 

507 
(* setup *) 

508 

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

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

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

511 
MethodsData.init, add_methods pure_methods]; 
5824  512 

513 

514 
end; 

515 

516 

517 
structure BasicMethod: BASIC_METHOD = Method; 

518 
open BasicMethod; 