src/Provers/classical.ML
changeset 26412 0918f5c0bbca
parent 24867 e5b55d7be9bb
child 26425 6561665c5cb1
equal deleted inserted replaced
26411:cd74690f3bfb 26412:0918f5c0bbca
    25 type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    25 type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    26 type wrapper = (int -> tactic) -> (int -> tactic);
    26 type wrapper = (int -> tactic) -> (int -> tactic);
    27 
    27 
    28 signature CLASSICAL_DATA =
    28 signature CLASSICAL_DATA =
    29 sig
    29 sig
    30   val mp        : thm           (* [| P-->Q;  P |] ==> Q *)
    30   val imp_elim  : thm           (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
    31   val not_elim  : thm           (* [| ~P;  P |] ==> R *)
    31   val not_elim  : thm           (* ~P ==> P ==> R *)
    32   val classical : thm           (* (~P ==> P) ==> P *)
    32   val swap      : thm           (* ~ P ==> (~ R ==> P) ==> R *)
       
    33   val classical : thm           (* (~ P ==> P) ==> P *)
    33   val sizef     : thm -> int    (* size function for BEST_FIRST *)
    34   val sizef     : thm -> int    (* size function for BEST_FIRST *)
    34   val hyp_subst_tacs: (int -> tactic) list
    35   val hyp_subst_tacs: (int -> tactic) list
    35 end;
    36 end;
    36 
    37 
    37 signature BASIC_CLASSICAL =
    38 signature BASIC_CLASSICAL =
   131 end;
   132 end;
   132 
   133 
   133 signature CLASSICAL =
   134 signature CLASSICAL =
   134 sig
   135 sig
   135   include BASIC_CLASSICAL
   136   include BASIC_CLASSICAL
   136   val swap: thm  (* ~P ==> (~Q ==> P) ==> Q *)
       
   137   val classical_rule: thm -> thm
   137   val classical_rule: thm -> thm
   138   val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   138   val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   139   val del_context_safe_wrapper: string -> theory -> theory
   139   val del_context_safe_wrapper: string -> theory -> theory
   140   val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   140   val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   141   val del_context_unsafe_wrapper: string -> theory -> theory
   141   val del_context_unsafe_wrapper: string -> theory -> theory
   204 val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
   204 val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
   205 
   205 
   206 
   206 
   207 (*** Useful tactics for classical reasoning ***)
   207 (*** Useful tactics for classical reasoning ***)
   208 
   208 
   209 val imp_elim = (*cannot use bind_thm within a structure!*)
       
   210   store_thm ("imp_elim", Thm.transfer (the_context ()) (classical_rule (Tactic.make_elim mp)));
       
   211 
       
   212 (*Prove goal that assumes both P and ~P.
   209 (*Prove goal that assumes both P and ~P.
   213   No backtracking if it finds an equal assumption.  Perhaps should call
   210   No backtracking if it finds an equal assumption.  Perhaps should call
   214   ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
   211   ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
   215 val contr_tac = eresolve_tac [not_elim]  THEN'
   212 val contr_tac = eresolve_tac [not_elim]  THEN'
   216                 (eq_assume_tac ORELSE' assume_tac);
   213                 (eq_assume_tac ORELSE' assume_tac);
   217 
   214 
   218 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   215 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   219   Could do the same thing for P<->Q and P... *)
   216   Could do the same thing for P<->Q and P... *)
   220 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;
   217 fun mp_tac i = eresolve_tac [not_elim, Data.imp_elim] i  THEN  assume_tac i;
   221 
   218 
   222 (*Like mp_tac but instantiates no variables*)
   219 (*Like mp_tac but instantiates no variables*)
   223 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
   220 fun eq_mp_tac i = ematch_tac [not_elim, Data.imp_elim] i  THEN  eq_assume_tac i;
   224 
       
   225 val swap =
       
   226   store_thm ("swap", Thm.transfer (the_context ())
       
   227     (rule_by_tactic (etac thin_rl 1) (not_elim RS classical)));
       
   228 
   221 
   229 (*Creates rules to eliminate ~A, from rules to introduce A*)
   222 (*Creates rules to eliminate ~A, from rules to introduce A*)
   230 fun swapify intrs = intrs RLN (2, [swap]);
   223 fun swapify intrs = intrs RLN (2, [Data.swap]);
   231 fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, swap))) x;
   224 fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, Data.swap))) x;
   232 
   225 
   233 (*Uses introduction rules in the normal way, or on negated assumptions,
   226 (*Uses introduction rules in the normal way, or on negated assumptions,
   234   trying rules in order. *)
   227   trying rules in order. *)
   235 fun swap_res_tac rls =
   228 fun swap_res_tac rls =
   236     let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
   229     let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
   237     in  assume_tac      ORELSE'
   230     in  assume_tac      ORELSE'
   238         contr_tac       ORELSE'
   231         contr_tac       ORELSE'
   239         biresolve_tac (foldr addrl [] rls)
   232         biresolve_tac (foldr addrl [] rls)
   240     end;
   233     end;
   241 
   234