CLAIM_TAC : string -> term -> tactic

SYNOPSIS

Breaks down and labels an intermediate claim in a proof.

DESCRIPTION

Given a Boolean term t and a string s of the form expected by DESTRUCT_TAC indicating how to break down and label that assertion, CLAIM_TAC s t breaks the current goal into two or more subgoals. One of these is to establish t using the current context and the others are to establish the original goal with the broken-down form of t as additional assumptions.

FAILURE CONDITIONS

Fails if the term is not Boolean or the pattern is ill-formed or does not match the form of the theorem.

EXAMPLE

Here we show how we can attack a propositional goal (admittedly trivial with TAUT).

  # g `(p <=> q) ==> p \/ ~q`;;

  val it : goalstack = 1 subgoal (1 total)

  `(p <=> q) ==> p \/ ~q`

  # e DISCH_TAC;;
  val it : goalstack = 1 subgoal (1 total)

    0 [`p <=> q`]

  `p \/ ~q`

We establish the intermediate goal p /\ q \/ ~p /\ ~q, the disjunction being in turn broken down into two labelled hypotheses yes and no:

  # e(CLAIM_TAC "yes|no" `p /\ q \/ ~p /\ ~q`);;
  val it : goalstack = 3 subgoals (3 total)

    0 [`p <=> q`]
    1 [`~p /\ ~q`] (no)

  `p \/ ~q`

    0 [`p <=> q`]
    1 [`p /\ q`] (yes)

  `p \/ ~q`

    0 [`p <=> q`]

  `p /\ q \/ ~p /\ ~q`