280 |
280 |
281 fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; |
281 fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls; |
282 fun delete x = delete_tagged_list (joinrules x); |
282 fun delete x = delete_tagged_list (joinrules x); |
283 fun delete' x = delete_tagged_list (joinrules' x); |
283 fun delete' x = delete_tagged_list (joinrules' x); |
284 |
284 |
285 fun string_of_thm NONE = Display.string_of_thm_without_context |
285 fun bad_thm (SOME context) msg th = |
286 | string_of_thm (SOME context) = Display.string_of_thm (Context.proof_of context); |
286 error (msg ^ "\n" ^ Display.string_of_thm (Context.proof_of context) th) |
287 |
287 | bad_thm NONE msg th = raise THM (msg, 0, [th]); |
288 fun make_elim context th = |
288 |
289 if has_fewer_prems 1 th then |
289 fun make_elim opt_context th = |
290 error ("Ill-formed destruction rule\n" ^ string_of_thm context th) |
290 if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed destruction rule" th |
291 else Tactic.make_elim th; |
291 else Tactic.make_elim th; |
292 |
292 |
293 fun warn_thm (SOME (Context.Proof ctxt)) msg th = |
293 fun warn_thm (SOME (Context.Proof ctxt)) msg th = |
294 if Context_Position.is_really_visible ctxt |
294 if Context_Position.is_really_visible ctxt |
295 then warning (msg ^ Display.string_of_thm ctxt th) else () |
295 then warning (msg ^ Display.string_of_thm ctxt th) else () |
296 | warn_thm _ _ _ = (); |
296 | warn_thm _ _ _ = (); |
297 |
297 |
298 fun warn_rules context msg rules th = |
298 fun warn_rules opt_context msg rules th = |
299 Item_Net.member rules th andalso (warn_thm context msg th; true); |
299 Item_Net.member rules th andalso (warn_thm opt_context msg th; true); |
300 |
300 |
301 fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) = |
301 fun warn_claset opt_context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) = |
302 warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse |
302 warn_rules opt_context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse |
303 warn_rules context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse |
303 warn_rules opt_context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse |
304 warn_rules context "Rule already declared as introduction (intro)\n" hazIs th orelse |
304 warn_rules opt_context "Rule already declared as introduction (intro)\n" hazIs th orelse |
305 warn_rules context "Rule already declared as elimination (elim)\n" hazEs th; |
305 warn_rules opt_context "Rule already declared as elimination (elim)\n" hazEs th; |
306 |
306 |
307 |
307 |
308 (*** Safe rules ***) |
308 (*** Safe rules ***) |
309 |
309 |
310 fun addSI w context th |
310 fun addSI w opt_context th |
311 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
311 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
312 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
312 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
313 if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs |
313 if warn_rules opt_context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs |
314 else |
314 else |
315 let |
315 let |
316 val ctxt = default_context context th; |
316 val ctxt = default_context opt_context th; |
317 val th' = flat_rule ctxt th; |
317 val th' = flat_rule ctxt th; |
318 val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
318 val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
319 List.partition Thm.no_prems [th']; |
319 List.partition Thm.no_prems [th']; |
320 val nI = Item_Net.length safeIs + 1; |
320 val nI = Item_Net.length safeIs + 1; |
321 val nE = Item_Net.length safeEs; |
321 val nE = Item_Net.length safeEs; |
322 val _ = warn_claset context th cs; |
322 val _ = warn_claset opt_context th cs; |
323 in |
323 in |
324 CS |
324 CS |
325 {safeIs = Item_Net.update th safeIs, |
325 {safeIs = Item_Net.update th safeIs, |
326 safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, |
326 safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, |
327 safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, |
327 safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, |
333 haz_netpair = haz_netpair, |
333 haz_netpair = haz_netpair, |
334 dup_netpair = dup_netpair, |
334 dup_netpair = dup_netpair, |
335 xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} |
335 xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} |
336 end; |
336 end; |
337 |
337 |
338 fun addSE w context th |
338 fun addSE w opt_context th |
339 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
339 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
340 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
340 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
341 if warn_rules context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs |
341 if warn_rules opt_context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs |
342 else if has_fewer_prems 1 th then |
342 else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th |
343 error ("Ill-formed elimination rule\n" ^ string_of_thm context th) |
|
344 else |
343 else |
345 let |
344 let |
346 val ctxt = default_context context th; |
345 val ctxt = default_context opt_context th; |
347 val th' = classical_rule ctxt (flat_rule ctxt th); |
346 val th' = classical_rule ctxt (flat_rule ctxt th); |
348 val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
347 val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
349 List.partition (fn rl => Thm.nprems_of rl=1) [th']; |
348 List.partition (fn rl => Thm.nprems_of rl=1) [th']; |
350 val nI = Item_Net.length safeIs; |
349 val nI = Item_Net.length safeIs; |
351 val nE = Item_Net.length safeEs + 1; |
350 val nE = Item_Net.length safeEs + 1; |
352 val _ = warn_claset context th cs; |
351 val _ = warn_claset opt_context th cs; |
353 in |
352 in |
354 CS |
353 CS |
355 {safeEs = Item_Net.update th safeEs, |
354 {safeEs = Item_Net.update th safeEs, |
356 safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, |
355 safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, |
357 safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, |
356 safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, |
363 haz_netpair = haz_netpair, |
362 haz_netpair = haz_netpair, |
364 dup_netpair = dup_netpair, |
363 dup_netpair = dup_netpair, |
365 xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} |
364 xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} |
366 end; |
365 end; |
367 |
366 |
368 fun addSD w context th = addSE w context (make_elim context th); |
367 fun addSD w opt_context th = addSE w opt_context (make_elim opt_context th); |
369 |
368 |
370 |
369 |
371 (*** Hazardous (unsafe) rules ***) |
370 (*** Hazardous (unsafe) rules ***) |
372 |
371 |
373 fun addI w context th |
372 fun addI w opt_context th |
374 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
373 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
375 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
374 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
376 if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs |
375 if warn_rules opt_context "Ignoring duplicate introduction (intro)\n" hazIs th then cs |
377 else |
376 else |
378 let |
377 let |
379 val ctxt = default_context context th; |
378 val ctxt = default_context opt_context th; |
380 val th' = flat_rule ctxt th; |
379 val th' = flat_rule ctxt th; |
381 val nI = Item_Net.length hazIs + 1; |
380 val nI = Item_Net.length hazIs + 1; |
382 val nE = Item_Net.length hazEs; |
381 val nE = Item_Net.length hazEs; |
383 val _ = warn_claset context th cs; |
382 val _ = warn_claset opt_context th cs; |
384 in |
383 in |
385 CS |
384 CS |
386 {hazIs = Item_Net.update th hazIs, |
385 {hazIs = Item_Net.update th hazIs, |
387 haz_netpair = insert (nI, nE) ([th'], []) haz_netpair, |
386 haz_netpair = insert (nI, nE) ([th'], []) haz_netpair, |
388 dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair, |
387 dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair, |
394 safe0_netpair = safe0_netpair, |
393 safe0_netpair = safe0_netpair, |
395 safep_netpair = safep_netpair, |
394 safep_netpair = safep_netpair, |
396 xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair} |
395 xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair} |
397 end |
396 end |
398 handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) |
397 handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) |
399 error ("Ill-formed introduction rule\n" ^ string_of_thm context th); |
398 bad_thm opt_context "Ill-formed introduction rule" th; |
400 |
399 |
401 fun addE w context th |
400 fun addE w opt_context th |
402 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
401 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
403 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
402 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
404 if warn_rules context "Ignoring duplicate elimination (elim)\n" hazEs th then cs |
403 if warn_rules opt_context "Ignoring duplicate elimination (elim)\n" hazEs th then cs |
405 else if has_fewer_prems 1 th then |
404 else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th |
406 error ("Ill-formed elimination rule\n" ^ string_of_thm context th) |
|
407 else |
405 else |
408 let |
406 let |
409 val ctxt = default_context context th; |
407 val ctxt = default_context opt_context th; |
410 val th' = classical_rule ctxt (flat_rule ctxt th); |
408 val th' = classical_rule ctxt (flat_rule ctxt th); |
411 val nI = Item_Net.length hazIs; |
409 val nI = Item_Net.length hazIs; |
412 val nE = Item_Net.length hazEs + 1; |
410 val nE = Item_Net.length hazEs + 1; |
413 val _ = warn_claset context th cs; |
411 val _ = warn_claset opt_context th cs; |
414 in |
412 in |
415 CS |
413 CS |
416 {hazEs = Item_Net.update th hazEs, |
414 {hazEs = Item_Net.update th hazEs, |
417 haz_netpair = insert (nI, nE) ([], [th']) haz_netpair, |
415 haz_netpair = insert (nI, nE) ([], [th']) haz_netpair, |
418 dup_netpair = insert (nI, nE) ([], [dup_elim ctxt th']) dup_netpair, |
416 dup_netpair = insert (nI, nE) ([], [dup_elim ctxt th']) dup_netpair, |
424 safe0_netpair = safe0_netpair, |
422 safe0_netpair = safe0_netpair, |
425 safep_netpair = safep_netpair, |
423 safep_netpair = safep_netpair, |
426 xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair} |
424 xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair} |
427 end; |
425 end; |
428 |
426 |
429 fun addD w context th = addE w context (make_elim context th); |
427 fun addD w opt_context th = addE w opt_context (make_elim opt_context th); |
430 |
428 |
431 |
429 |
432 |
430 |
433 (*** Deletion of rules |
431 (*** Deletion of rules |
434 Working out what to delete, requires repeating much of the code used |
432 Working out what to delete, requires repeating much of the code used |
435 to insert. |
433 to insert. |
436 ***) |
434 ***) |
437 |
435 |
438 fun delSI context th |
436 fun delSI opt_context th |
439 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
437 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
440 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
438 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
441 if Item_Net.member safeIs th then |
439 if Item_Net.member safeIs th then |
442 let |
440 let |
443 val ctxt = default_context context th; |
441 val ctxt = default_context opt_context th; |
444 val th' = flat_rule ctxt th; |
442 val th' = flat_rule ctxt th; |
445 val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']; |
443 val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']; |
446 in |
444 in |
447 CS |
445 CS |
448 {safe0_netpair = delete (safe0_rls, []) safe0_netpair, |
446 {safe0_netpair = delete (safe0_rls, []) safe0_netpair, |
457 dup_netpair = dup_netpair, |
455 dup_netpair = dup_netpair, |
458 xtra_netpair = delete' ([th], []) xtra_netpair} |
456 xtra_netpair = delete' ([th], []) xtra_netpair} |
459 end |
457 end |
460 else cs; |
458 else cs; |
461 |
459 |
462 fun delSE context th |
460 fun delSE opt_context th |
463 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
461 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
464 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
462 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
465 if Item_Net.member safeEs th then |
463 if Item_Net.member safeEs th then |
466 let |
464 let |
467 val ctxt = default_context context th; |
465 val ctxt = default_context opt_context th; |
468 val th' = classical_rule ctxt (flat_rule ctxt th); |
466 val th' = classical_rule ctxt (flat_rule ctxt th); |
469 val (safe0_rls, safep_rls) = List.partition (fn rl => Thm.nprems_of rl = 1) [th']; |
467 val (safe0_rls, safep_rls) = List.partition (fn rl => Thm.nprems_of rl = 1) [th']; |
470 in |
468 in |
471 CS |
469 CS |
472 {safe0_netpair = delete ([], safe0_rls) safe0_netpair, |
470 {safe0_netpair = delete ([], safe0_rls) safe0_netpair, |
481 dup_netpair = dup_netpair, |
479 dup_netpair = dup_netpair, |
482 xtra_netpair = delete' ([], [th]) xtra_netpair} |
480 xtra_netpair = delete' ([], [th]) xtra_netpair} |
483 end |
481 end |
484 else cs; |
482 else cs; |
485 |
483 |
486 fun delI context th |
484 fun delI opt_context th |
487 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
485 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
488 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
486 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
489 if Item_Net.member hazIs th then |
487 if Item_Net.member hazIs th then |
490 let |
488 let |
491 val ctxt = default_context context th; |
489 val ctxt = default_context opt_context th; |
492 val th' = flat_rule ctxt th; |
490 val th' = flat_rule ctxt th; |
493 in |
491 in |
494 CS |
492 CS |
495 {haz_netpair = delete ([th'], []) haz_netpair, |
493 {haz_netpair = delete ([th'], []) haz_netpair, |
496 dup_netpair = delete ([dup_intr th'], []) dup_netpair, |
494 dup_netpair = delete ([dup_intr th'], []) dup_netpair, |
504 safep_netpair = safep_netpair, |
502 safep_netpair = safep_netpair, |
505 xtra_netpair = delete' ([th], []) xtra_netpair} |
503 xtra_netpair = delete' ([th], []) xtra_netpair} |
506 end |
504 end |
507 else cs |
505 else cs |
508 handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) |
506 handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) |
509 error ("Ill-formed introduction rule\n" ^ string_of_thm context th); |
507 bad_thm opt_context "Ill-formed introduction rule" th; |
510 |
508 |
511 fun delE context th |
509 fun delE opt_context th |
512 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
510 (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
513 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
511 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
514 if Item_Net.member hazEs th then |
512 if Item_Net.member hazEs th then |
515 let |
513 let |
516 val ctxt = default_context context th; |
514 val ctxt = default_context opt_context th; |
517 val th' = classical_rule ctxt (flat_rule ctxt th); |
515 val th' = classical_rule ctxt (flat_rule ctxt th); |
518 in |
516 in |
519 CS |
517 CS |
520 {haz_netpair = delete ([], [th']) haz_netpair, |
518 {haz_netpair = delete ([], [th']) haz_netpair, |
521 dup_netpair = delete ([], [dup_elim ctxt th']) dup_netpair, |
519 dup_netpair = delete ([], [dup_elim ctxt th']) dup_netpair, |
530 xtra_netpair = delete' ([], [th]) xtra_netpair} |
528 xtra_netpair = delete' ([], [th]) xtra_netpair} |
531 end |
529 end |
532 else cs; |
530 else cs; |
533 |
531 |
534 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) |
532 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) |
535 fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = |
533 fun delrule opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = |
536 let val th' = Tactic.make_elim th in |
534 let val th' = Tactic.make_elim th in |
537 if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse |
535 if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse |
538 Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse |
536 Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse |
539 Item_Net.member safeEs th' orelse Item_Net.member hazEs th' |
537 Item_Net.member safeEs th' orelse Item_Net.member hazEs th' |
540 then |
538 then |
541 delSI context th |
539 delSI opt_context th |
542 (delSE context th |
540 (delSE opt_context th |
543 (delI context th |
541 (delI opt_context th |
544 (delE context th (delSE context th' (delE context th' cs))))) |
542 (delE opt_context th (delSE opt_context th' (delE opt_context th' cs))))) |
545 else (warn_thm context "Undeclared classical rule\n" th; cs) |
543 else (warn_thm opt_context "Undeclared classical rule\n" th; cs) |
546 end; |
544 end; |
547 |
545 |
548 |
546 |
549 |
547 |
550 (** claset data **) |
548 (** claset data **) |
856 |
854 |
857 |
855 |
858 (* attributes *) |
856 (* attributes *) |
859 |
857 |
860 fun attrib f = |
858 fun attrib f = |
861 Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context); |
859 Thm.declaration_attribute (fn th => fn opt_context => |
|
860 map_cs (f (SOME opt_context) th) opt_context); |
862 |
861 |
863 val safe_elim = attrib o addSE; |
862 val safe_elim = attrib o addSE; |
864 val safe_intro = attrib o addSI; |
863 val safe_intro = attrib o addSI; |
865 val safe_dest = attrib o addSD; |
864 val safe_dest = attrib o addSD; |
866 val haz_elim = attrib o addE; |
865 val haz_elim = attrib o addE; |
867 val haz_intro = attrib o addI; |
866 val haz_intro = attrib o addI; |
868 val haz_dest = attrib o addD; |
867 val haz_dest = attrib o addD; |
869 |
868 |
870 val rule_del = |
869 val rule_del = |
871 Thm.declaration_attribute (fn th => fn context => |
870 Thm.declaration_attribute (fn th => fn opt_context => |
872 context |> map_cs (delrule (SOME context) th) |> |
871 opt_context |> map_cs (delrule (SOME opt_context) th) |> |
873 Thm.attribute_declaration Context_Rules.rule_del th); |
872 Thm.attribute_declaration Context_Rules.rule_del th); |
874 |
873 |
875 |
874 |
876 |
875 |
877 (** concrete syntax of attributes **) |
876 (** concrete syntax of attributes **) |