240 s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) |
240 s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) |
241 | _ => fold (curry s_disj) lits @{term False}) |
241 | _ => fold (curry s_disj) lits @{term False}) |
242 end |
242 end |
243 |> HOLogic.mk_Trueprop |> finish_off |
243 |> HOLogic.mk_Trueprop |> finish_off |
244 |
244 |
245 fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show |
245 fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] |
246 |
246 |
247 fun isar_steps outer predecessor accum [] = |
247 fun isar_steps outer predecessor accum [] = |
248 accum |
248 accum |
249 |> (if tainted = [] then |
249 |> (if tainted = [] then |
|
250 (* e.g., trivial, empty proof by Z3 *) |
250 cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], |
251 cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], |
251 sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")) |
252 sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")) |
252 else |
253 else |
253 I) |
254 I) |
254 |> rev |
255 |> rev |
267 else if is_arith_rule rule then arith_methods |
268 else if is_arith_rule rule then arith_methods |
268 else if is_datatype_rule rule then datatype_methods |
269 else if is_datatype_rule rule then datatype_methods |
269 else systematic_methods') |
270 else systematic_methods') |
270 |> massage_methods |
271 |> massage_methods |
271 |
272 |
272 fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "") |
273 fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "") |
273 fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs |
274 fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs |
274 in |
275 in |
275 if is_clause_tainted c then |
276 if is_clause_tainted c then |
276 (case gamma of |
277 (case gamma of |
277 [g] => |
278 [g] => |
300 isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs |
301 isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs |
301 val c = succedent_of_cases cases |
302 val c = succedent_of_cases cases |
302 val l = label_of_clause c |
303 val l = label_of_clause c |
303 val t = prop_of_clause c |
304 val t = prop_of_clause c |
304 val step = |
305 val step = |
305 Prove (maybe_show outer c [], [], l, t, |
306 Prove (maybe_show outer c, [], l, t, |
306 map isar_case (filter_out (null o snd) cases), |
307 map isar_case (filter_out (null o snd) cases), |
307 sort_facts (the_list predecessor, []), massage_methods systematic_methods', "") |
308 sort_facts (the_list predecessor, []), massage_methods systematic_methods', "") |
308 in |
309 in |
309 isar_steps outer (SOME l) (step :: accum) infs |
310 isar_steps outer (SOME l) (step :: accum) infs |
310 end |
311 end |
317 refute_graph |
318 refute_graph |
318 |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph) |
319 |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph) |
319 |> redirect_graph axioms tainted bot |
320 |> redirect_graph axioms tainted bot |
320 |> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof) |
321 |> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof) |
321 |> isar_proof true params assms lems |
322 |> isar_proof true params assms lems |
|
323 |> postprocess_isar_proof_remove_show_stuttering |
322 |> postprocess_isar_proof_remove_unreferenced_steps I |
324 |> postprocess_isar_proof_remove_unreferenced_steps I |
323 |> relabel_isar_proof_canonically |
325 |> relabel_isar_proof_canonically |
324 |
326 |
325 val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof |
327 val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof |
326 |
328 |