`PSTRIP_GOAL_THEN : (thm_tactic -> tactic)`
STRUCTURE
LIBRARY
pair
SYNOPSIS
Splits a goal by eliminating one outermost connective, applying the given theorem-tactic to the antecedents of implications.
DESCRIPTION
Given a theorem-tactic ttac and a goal (A,t), PSTRIP_GOAL_THEN removes one outermost occurrence of one of the connectives !, ==>, ~ or /\ from the conclusion of the goal t. If t is a universally quantified term, then STRIP_GOAL_THEN strips off the quantifier. Note that PSTRIP_GOAL_THEN will strip off paired universal quantifications.
```      A ?- !p. u
==============  PSTRIP_GOAL_THEN ttac
A ?- u[p'/p]
```
where p' is a primed variant that contains no variables that appear free in the assumptions A. If t is a conjunction, then PSTRIP_GOAL_THEN simply splits the conjunction into two subgoals:
```      A ?- v /\ w
=================  PSTRIP_GOAL_THEN ttac
A ?- v   A ?- w
```
If t is an implication "u ==> v" and if:
```      A ?- v
===============  ttac (u |- u)
A' ?- v'
```
then:
```      A ?- u ==> v
====================  PSTRIP_GOAL_THEN ttac
A' ?- v'
```
Finally, a negation ~t is treated as the implication t ==> F.
FAILURE
PSTRIP_GOAL_THEN ttac (A,t) fails if t is not a paired universally quantified term, an implication, a negation or a conjunction. Failure also occurs if the application of ttac fails, after stripping the goal.
USES
PSTRIP_GOAL_THEN is used when manipulating intermediate results (obtained by stripping outer connectives from a goal) directly, rather than as assumptions.
SEEALSO
HOL  Kananaskis-14
{"ft_lang_label":"__label__en","ft_lang_prob":0.69692075,"math_prob":0.92726654,"size":871,"snap":"2021-04-2021-17","text_gpt3_token_len":266,"char_repetition_ratio":0.21799308,"word_repetition_ratio":0.0,"special_character_ratio":0.347876,"punctuation_ratio":0.16770187,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.96171254,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-04-22T23:51:45Z\",\"WARC-Record-ID\":\"<urn:uuid:3129970f-aaa9-43b9-b510-1c3c5340b4f0>\",\"Content-Length\":\"4797\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:b4e00747-5a12-499f-a602-8f0fdd5926ce>\",\"WARC-Concurrent-To\":\"<urn:uuid:4a68a90d-af70-42f6-a5ab-793eed1b41cc>\",\"WARC-IP-Address\":\"176.58.119.245\",\"WARC-Target-URI\":\"https://hol-theorem-prover.org/kananaskis-14-helpdocs/help/Docfiles/HTML/PairRules.PSTRIP_GOAL_THEN.html\",\"WARC-Payload-Digest\":\"sha1:QZVNEO4D6GJDPA5353ILQHZMZTNJ7UQH\",\"WARC-Block-Digest\":\"sha1:4J6GFR5TFOSFQC2VXQSL7CPHWQ7EQOZQ\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-17/CC-MAIN-2021-17_segments_1618039563095.86_warc_CC-MAIN-20210422221531-20210423011531-00594.warc.gz\"}"}