equal
deleted
inserted
replaced
424 | NONE => error "insert_tagged_brl: elimination rule with no premises") |
424 | NONE => error "insert_tagged_brl: elimination rule with no premises") |
425 else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); |
425 else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); |
426 |
426 |
427 (*build a pair of nets for biresolution*) |
427 (*build a pair of nets for biresolution*) |
428 fun build_netpair netpair brls = |
428 fun build_netpair netpair brls = |
429 Library.foldr insert_tagged_brl (taglist 1 brls, netpair); |
429 foldr insert_tagged_brl netpair (taglist 1 brls); |
430 |
430 |
431 (*delete one kbrl from the pair of nets*) |
431 (*delete one kbrl from the pair of nets*) |
432 local |
432 local |
433 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th') |
433 fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th') |
434 in |
434 in |
471 fun insert_krl (krl as (k,th), net) = |
471 fun insert_krl (krl as (k,th), net) = |
472 Net.insert_term ((concl_of th, krl), net, K false); |
472 Net.insert_term ((concl_of th, krl), net, K false); |
473 |
473 |
474 (*build a net of rules for resolution*) |
474 (*build a net of rules for resolution*) |
475 fun build_net rls = |
475 fun build_net rls = |
476 Library.foldr insert_krl (taglist 1 rls, Net.empty); |
476 foldr insert_krl Net.empty (taglist 1 rls); |
477 |
477 |
478 (*resolution using a net rather than rules; pred supports filt_resolve_tac*) |
478 (*resolution using a net rather than rules; pred supports filt_resolve_tac*) |
479 fun filt_resolution_from_net_tac match pred net = |
479 fun filt_resolution_from_net_tac match pred net = |
480 SUBGOAL |
480 SUBGOAL |
481 (fn (prem,i) => |
481 (fn (prem,i) => |
642 fun prove sign xs asms prop tac = |
642 fun prove sign xs asms prop tac = |
643 let |
643 let |
644 val statement = Logic.list_implies (asms, prop); |
644 val statement = Logic.list_implies (asms, prop); |
645 val frees = map Term.dest_Free (Term.term_frees statement); |
645 val frees = map Term.dest_Free (Term.term_frees statement); |
646 val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees; |
646 val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees; |
647 val fixed_tfrees = Library.foldr Term.add_typ_tfree_names (map #2 fixed_frees, []); |
647 val fixed_tfrees = foldr Term.add_typ_tfree_names [] (map #2 fixed_frees); |
648 val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs; |
648 val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs; |
649 |
649 |
650 fun err msg = raise ERROR_MESSAGE |
650 fun err msg = raise ERROR_MESSAGE |
651 (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^ |
651 (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^ |
652 Sign.string_of_term sign (Term.list_all_free (params, statement))); |
652 Sign.string_of_term sign (Term.list_all_free (params, statement))); |