src/Provers/classical.ML
changeset 3705 76f3b2803982
parent 3546 de164676a202
child 3727 ed63c05d7992
equal deleted inserted replaced
3704:2f99d7a0dccc 3705:76f3b2803982
    82   val haz_step_tac 	: claset -> int -> tactic
    82   val haz_step_tac 	: claset -> int -> tactic
    83   val joinrules 	: thm list * thm list -> (bool * thm) list
    83   val joinrules 	: thm list * thm list -> (bool * thm) list
    84   val mp_tac		: int -> tactic
    84   val mp_tac		: int -> tactic
    85   val safe_tac 		: claset -> tactic
    85   val safe_tac 		: claset -> tactic
    86   val safe_step_tac 	: claset -> int -> tactic
    86   val safe_step_tac 	: claset -> int -> tactic
       
    87   val clarify_tac 	: claset -> int -> tactic
       
    88   val clarify_step_tac 	: claset -> int -> tactic
    87   val step_tac 		: claset -> int -> tactic
    89   val step_tac 		: claset -> int -> tactic
    88   val slow_step_tac	: claset -> int -> tactic
    90   val slow_step_tac	: claset -> int -> tactic
    89   val swap		: thm                 (* ~P ==> (~Q ==> P) ==> Q *)
    91   val swap		: thm                 (* ~P ==> (~Q ==> P) ==> Q *)
    90   val swapify 		: thm list -> thm list
    92   val swapify 		: thm list -> thm list
    91   val swap_res_tac 	: thm list -> int -> tactic
    93   val swap_res_tac 	: thm list -> int -> tactic
   100   val AddSDs		: thm list -> unit
   102   val AddSDs		: thm list -> unit
   101   val AddSEs		: thm list -> unit
   103   val AddSEs		: thm list -> unit
   102   val AddSIs		: thm list -> unit
   104   val AddSIs		: thm list -> unit
   103   val Delrules		: thm list -> unit
   105   val Delrules		: thm list -> unit
   104   val Safe_step_tac	: int -> tactic
   106   val Safe_step_tac	: int -> tactic
       
   107   val Clarify_tac 	: int -> tactic
       
   108   val Clarify_step_tac 	: int -> tactic
   105   val Step_tac 		: int -> tactic
   109   val Step_tac 		: int -> tactic
   106   val Fast_tac 		: int -> tactic
   110   val Fast_tac 		: int -> tactic
   107   val Best_tac 		: int -> tactic
   111   val Best_tac 		: int -> tactic
   108   val Slow_tac 		: int -> tactic
   112   val Slow_tac 		: int -> tactic
   109   val Slow_best_tac     : int -> tactic
   113   val Slow_best_tac     : int -> tactic
   529 
   533 
   530 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   534 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   531 fun safe_tac cs = REPEAT_DETERM_FIRST 
   535 fun safe_tac cs = REPEAT_DETERM_FIRST 
   532 	(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   536 	(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   533 
   537 
       
   538 
       
   539 (*** Clarify_tac: do safe steps without causing branching ***)
       
   540 
       
   541 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
       
   542 
       
   543 (*version of bimatch_from_nets_tac that only applies rules that
       
   544   create precisely n subgoals.*)
       
   545 fun n_bimatch_from_nets_tac n = 
       
   546     biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true;
       
   547 
       
   548 fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
       
   549 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
       
   550 
       
   551 (*Two-way branching is allowed only if one of the branches immediately closes*)
       
   552 fun bimatch2_tac netpair i =
       
   553     n_bimatch_from_nets_tac 2 netpair i THEN
       
   554     (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
       
   555 
       
   556 (*Attack subgoals using safe inferences -- matching, not resolution*)
       
   557 fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
       
   558   getSWrapper cs (FIRST' [
       
   559 	eq_assume_contr_tac,
       
   560 	bimatch_from_nets_tac safe0_netpair,
       
   561 	FIRST' hyp_subst_tacs,
       
   562 	n_bimatch_from_nets_tac 1 safep_netpair,
       
   563         bimatch2_tac safep_netpair]);
       
   564 
       
   565 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
       
   566 
       
   567 
       
   568 (*** Unsafe steps instantiate variables or lose information ***)
       
   569 
   534 (*But these unsafe steps at least solve a subgoal!*)
   570 (*But these unsafe steps at least solve a subgoal!*)
   535 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   571 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   536   assume_tac 			  APPEND' 
   572   assume_tac 			  APPEND' 
   537   contr_tac 			  APPEND' 
   573   contr_tac 			  APPEND' 
   538   biresolve_from_nets_tac safe0_netpair;
   574   biresolve_from_nets_tac safe0_netpair;
   642 
   678 
   643 (*Cannot have Safe_tac, as it takes no arguments; must delay dereferencing!*)
   679 (*Cannot have Safe_tac, as it takes no arguments; must delay dereferencing!*)
   644 
   680 
   645 fun Safe_step_tac i = safe_step_tac (!claset) i; 
   681 fun Safe_step_tac i = safe_step_tac (!claset) i; 
   646 
   682 
       
   683 fun Clarify_step_tac i = clarify_step_tac (!claset) i;
       
   684 
       
   685 fun Clarify_tac i = clarify_tac (!claset) i;
       
   686 
   647 fun Step_tac i = step_tac (!claset) i; 
   687 fun Step_tac i = step_tac (!claset) i; 
   648 
   688 
   649 fun Fast_tac i = fast_tac (!claset) i; 
   689 fun Fast_tac i = fast_tac (!claset) i; 
   650 
   690 
   651 fun Best_tac i = best_tac (!claset) i; 
   691 fun Best_tac i = best_tac (!claset) i;