201 Note: We don't do this if the wf conditions fail to be solved, as each 
201 Note: We don't do this if the wf conditions fail to be solved, as each 
202 case may have a different wf condition. We could group the conditions 
202 case may have a different wf condition. We could group the conditions 
203 together and say that they must be true to solve the general case, 
203 together and say that they must be true to solve the general case, 
204 but that would hide from the user which subcase they were related 
204 but that would hide from the user which subcase they were related 
205 to. Probably this is not important, and it would work fine, but, for now, I 
205 to. Probably this is not important, and it would work fine, but, for now, I 
206 prefer leaving more finegrain control to the user. *) 
206 prefer leaving more finegrain control to the user. 

207  Lucas Dixon, Aug 2004 *) 
207 local 
208 local 
208 fun get_related_thms i = 
209 fun get_related_thms i = 
209 mapfilter ((fn (r,x) => if x = i then Some r else None)); 
210 mapfilter ((fn (r,x) => if x = i then Some r else None)); 
210 
211 
211 fun solve_eq (th, [], i) = 
212 fun solve_eq (th, [], i) = 
212 raise ERROR_MESSAGE "derive_init_eqs: missing rules" 
213 raise ERROR_MESSAGE "derive_init_eqs: missing rules" 
213  solve_eq (th, [a], i) = [(a, i)] 
214  solve_eq (th, [a], i) = [(a, i)] 
214  solve_eq (th, splitths as (_ :: _), i) = 
215  solve_eq (th, splitths as (_ :: _), i) = 

216 (writeln "Proving unsplit equation..."; 
215 [((standard o ObjectLogic.rulify_no_asm) 
217 [((standard o ObjectLogic.rulify_no_asm) 
216 (CaseSplit.splitto splitths th), i)] 
218 (CaseSplit.splitto splitths th), i)]) 
217 (* if there's an error, pretend nothing happened with this definition 
219 (* if there's an error, pretend nothing happened with this definition 
218 We should probably print something out so that the user knows...? *) 
220 We should probably print something out so that the user knows...? *) 
219 handle ERROR_MESSAGE _ => map (fn x => (x,i)) splitths; 
221 handle ERROR_MESSAGE s => 

222 (writeln ("WARNING:post.ML:solve_eq: " ^ s); map (fn x => (x,i)) splitths); 
220 in 
223 in 
221 fun derive_init_eqs sgn rules eqs = 
224 fun derive_init_eqs sgn rules eqs = 
222 let 
225 let 
223 val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
226 val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
224 eqs 
227 eqs 
235 * Defining a function with an associated termination relation. 
238 * Defining a function with an associated termination relation. 
236 **) 
239 **) 
237 fun define_i strict thy cs ss congs wfs fid R eqs = 
240 fun define_i strict thy cs ss congs wfs fid R eqs = 
238 let val {functional,pats} = Prim.mk_functional thy eqs 
241 let val {functional,pats} = Prim.mk_functional thy eqs 
239 val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional 
242 val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional 
240 in (thy, simplify_defn strict thy cs ss congs wfs fid pats def) end; 
243 val {induct, rules, tcs} = 

244 simplify_defn strict thy cs ss congs wfs fid pats def 

245 val rules' = 

246 if strict then derive_init_eqs (Theory.sign_of thy) rules eqs 

247 else rules 

248 in (thy, {rules = rules', induct = induct, tcs = tcs}) end; 
241 
249 
242 fun define strict thy cs ss congs wfs fid R seqs = 
250 fun define strict thy cs ss congs wfs fid R seqs = 
243 define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs) 
251 define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs) 
244 handle U.ERR {mesg,...} => error mesg; 
252 handle U.ERR {mesg,...} => error mesg; 
245 
253 