src/Provers/classical.ML
changeset 1524 524879632d88
parent 1231 91d2c1bb5803
child 1587 e7d8a4957bac
equal deleted inserted replaced
1523:7513fbe502fb 1524:524879632d88
    88 
    88 
    89 local open Data in
    89 local open Data in
    90 
    90 
    91 (** Useful tactics for classical reasoning **)
    91 (** Useful tactics for classical reasoning **)
    92 
    92 
    93 val imp_elim = make_elim mp;
    93 val imp_elim = (*cannot use bind_thm within a structure!*)
       
    94   store_thm ("imp_elim", make_elim mp);
    94 
    95 
    95 (*Solve goal that assumes both P and ~P. *)
    96 (*Solve goal that assumes both P and ~P. *)
    96 val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;
    97 val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;
    97 
    98 
    98 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
    99 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   100 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;
   101 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;
   101 
   102 
   102 (*Like mp_tac but instantiates no variables*)
   103 (*Like mp_tac but instantiates no variables*)
   103 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
   104 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
   104 
   105 
   105 val swap = rule_by_tactic (etac thin_rl 1) (not_elim RS classical);
   106 val swap =
       
   107   store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical));
   106 
   108 
   107 (*Creates rules to eliminate ~A, from rules to introduce A*)
   109 (*Creates rules to eliminate ~A, from rules to introduce A*)
   108 fun swapify intrs = intrs RLN (2, [swap]);
   110 fun swapify intrs = intrs RLN (2, [swap]);
   109 
   111 
   110 (*Uses introduction rules in the normal way, or on negated assumptions,
   112 (*Uses introduction rules in the normal way, or on negated assumptions,