Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9208031611.AA10370@air52.larc.nasa.gov>
Date: Mon, 3 Aug 92 12:11:20 -0400
From: Victor "A." Carreno <vac@gov.nasa.larc.air16>
To: info-hol@edu.uidaho.cs.ted
Subject: the case of the lost postings
Cc: John.Harrison@uk.ac.cam.cl


I don't know why, but it seems that some messages from inf-hol arrive at
some sites but not anothers. I did not receive the message:
Gavan Tredoux         CHOOSE breaks
which is why I didn't know what jrh was talking about when he replied:

Gavan Tredoux writes:

> In the process of complex proof, I've managed to break
> REPEAT STRIP_TAC, due to an error in CHOOSE. etc.

I sent a message to info-hol (included) on 31 AUG 92, which I got, but is
not in jrh's info-hol archives,so I don't think it reached Cambridge.

Be in the alert,

Victor.

>From info-hol-request@ted.cs.uidaho.edu Fri Jul 31 10:30:13 1992
Received: from air12.larc.nasa.gov by air16.larc.nasa.gov with SMTP
        (5.65.1/server2.4) id AA01096; Fri, 31 Jul 92 10:30:10 -0400
Received: by air12.larc.nasa.gov (5.57/Ultrix2.4-C)
        id AA29154; Fri, 31 Jul 92 10:28:02 EDT
Received: by ted.cs.uidaho.edu (16.6/1.34)
        id AA07223; Fri, 31 Jul 92 06:54:45 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Received: from air52.larc.nasa.gov by ted.cs.uidaho.edu (16.6/1.34)
        id AA07218; Fri, 31 Jul 92 06:54:37 -0700
Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4)
        id AA09835; Fri, 31 Jul 92 09:54:29 -0400
Message-Id: <9207311354.AA09835@air52.larc.nasa.gov>
Date: Fri, 31 Jul 92 09:54:29 -0400
From: Victor A. Carreno <vac>
To: info-hol@ted.cs.uidaho.edu
Subject: Re: stripping failure
Status: RO

R.B.Jones writes:

> The following simple example fails with HOL88v1.11 and its equivalent fails
> also with ICL HOL (now known as ProofPower).

> set_goal([],"?(x:*).(?(y:*)(x:*). P x y) /\ Q (x:*) ==> F");;
> e STRIP_TAC;;

[deleted]

> Incidentally, can anyone explain why the last type cast (i.e., the fourth ":*"
)

> in the above term is necessary?  (it fails "types indeterminate" without it)

the following term parses:
set_goal([],"?(x:*).(?(y:*)(z:*). P z y) /\ Q x ==> F");;

and so does:
set_goal([],"?x.(?(y:*)(x:*). P x y) /\ Q (x:*) ==> F");;

It appears there is a conflict between the variable "x" in the first
quantification and the variable "x" in the second.

This term produces the message:

let t = "~(!x:**.(?(y:*)(x:*). P x y) /\ Q x)";;
evaluation failed     types in quotation

and so does:

let t = "~(!x:**.(?(y:*)(x:*). P x y) /\ Q (x:**))";;
evaluation failed     types in quotation

In general:
let t = "!x:*. P x /\ (!x:**. Q x)";;
evaluation failed     types in quotation

let t = "!x:*. P x /\ (!z:**. Q z)";;
t = "!x. P x /\ (!z. Q z)" : term

Doesn't the "x" in "Q x" supposed to be bound by the second quantification
and unaffected by the first ?

Victor.