src/Pure/tactic.ML
changeset 60775 4592a9118d0b
parent 60774 6c28d8ed2488
child 60776 2164e7b47454
equal deleted inserted replaced
60774:6c28d8ed2488 60775:4592a9118d0b
    16   val biresolve_tac: Proof.context -> (bool * thm) list -> int -> tactic
    16   val biresolve_tac: Proof.context -> (bool * thm) list -> int -> tactic
    17   val resolve0_tac: thm list -> int -> tactic
    17   val resolve0_tac: thm list -> int -> tactic
    18   val resolve_tac: Proof.context -> thm list -> int -> tactic
    18   val resolve_tac: Proof.context -> thm list -> int -> tactic
    19   val eresolve0_tac: thm list -> int -> tactic
    19   val eresolve0_tac: thm list -> int -> tactic
    20   val eresolve_tac: Proof.context -> thm list -> int -> tactic
    20   val eresolve_tac: Proof.context -> thm list -> int -> tactic
    21   val forward0_tac: thm list -> int -> tactic
       
    22   val forward_tac: Proof.context -> thm list -> int -> tactic
    21   val forward_tac: Proof.context -> thm list -> int -> tactic
    23   val dresolve0_tac: thm list -> int -> tactic
    22   val dresolve0_tac: thm list -> int -> tactic
    24   val dresolve_tac: Proof.context -> thm list -> int -> tactic
    23   val dresolve_tac: Proof.context -> thm list -> int -> tactic
    25   val atac: int -> tactic
    24   val atac: int -> tactic
    26   val rtac: thm -> int -> tactic
    25   val rtac: thm -> int -> tactic
    27   val dtac: thm -> int -> tactic
    26   val dtac: thm -> int -> tactic
    28   val etac: thm -> int -> tactic
    27   val etac: thm -> int -> tactic
    29   val ftac: thm -> int -> tactic
       
    30   val ares_tac: Proof.context -> thm list -> int -> tactic
    28   val ares_tac: Proof.context -> thm list -> int -> tactic
    31   val solve_tac: Proof.context -> thm list -> int -> tactic
    29   val solve_tac: Proof.context -> thm list -> int -> tactic
    32   val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
    30   val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
    33   val match_tac: Proof.context -> thm list -> int -> tactic
    31   val match_tac: Proof.context -> thm list -> int -> tactic
    34   val ematch_tac: Proof.context -> thm list -> int -> tactic
    32   val ematch_tac: Proof.context -> thm list -> int -> tactic
   129 (*Resolution with elimination rules only*)
   127 (*Resolution with elimination rules only*)
   130 fun eresolve0_tac rules = biresolve0_tac (map (pair true) rules);
   128 fun eresolve0_tac rules = biresolve0_tac (map (pair true) rules);
   131 fun eresolve_tac ctxt rules = biresolve_tac ctxt (map (pair true) rules);
   129 fun eresolve_tac ctxt rules = biresolve_tac ctxt (map (pair true) rules);
   132 
   130 
   133 (*Forward reasoning using destruction rules.*)
   131 (*Forward reasoning using destruction rules.*)
   134 fun forward0_tac rls = resolve0_tac (map make_elim rls) THEN' atac;
       
   135 fun forward_tac ctxt rls = resolve_tac ctxt (map make_elim rls) THEN' atac;
   132 fun forward_tac ctxt rls = resolve_tac ctxt (map make_elim rls) THEN' atac;
   136 
   133 
   137 (*Like forward_tac, but deletes the assumption after use.*)
   134 (*Like forward_tac, but deletes the assumption after use.*)
   138 fun dresolve0_tac rls = eresolve0_tac (map make_elim rls);
   135 fun dresolve0_tac rls = eresolve0_tac (map make_elim rls);
   139 fun dresolve_tac ctxt rls = eresolve_tac ctxt (map make_elim rls);
   136 fun dresolve_tac ctxt rls = eresolve_tac ctxt (map make_elim rls);
   140 
   137 
   141 (*Shorthand versions: for resolution with a single theorem*)
   138 (*Shorthand versions: for resolution with a single theorem*)
   142 fun rtac rl =  resolve0_tac [rl];
   139 fun rtac rl =  resolve0_tac [rl];
   143 fun dtac rl = dresolve0_tac [rl];
   140 fun dtac rl = dresolve0_tac [rl];
   144 fun etac rl = eresolve0_tac [rl];
   141 fun etac rl = eresolve0_tac [rl];
   145 fun ftac rl =  forward0_tac [rl];
       
   146 
   142 
   147 (*Use an assumption or some rules*)
   143 (*Use an assumption or some rules*)
   148 fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules;
   144 fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules;
   149 
   145 
   150 fun solve_tac ctxt rules = resolve_tac ctxt rules THEN_ALL_NEW assume_tac ctxt;
   146 fun solve_tac ctxt rules = resolve_tac ctxt rules THEN_ALL_NEW assume_tac ctxt;