Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Mon, 29 Mar 1993 16:38:59 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28778; Mon, 29 Mar 93 07:15:59 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from air52.larc.nasa.gov by ted.cs.uidaho.edu (16.6/1.34) id AA28773; Mon, 29 Mar 93 07:15:53 -0800 Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA07550; Mon, 29 Mar 93 10:16:00 -0500 Message-Id: <9303291516.AA07550@air52.larc.nasa.gov> Date: Mon, 29 Mar 93 10:16:00 -0500 From: Victor "A." Carreno To: val@com.netcom Subject: Re: Beginners Questions In-Reply-To: Mail from 'val@netcom.com (Dewey Val Schorre)' dated: Mon, 29 Mar 93 05:45:03 -0800 Cc: info-hol@edu.uidaho.cs.ted > ... Is there a list of the Pre-defined ML > identifers that are grouped together in a logical way? I don't think you are going to find such a list; since almost any function relates to another function, the groups will be all inclusive. At the end of the each documentation entry there is a `SEE ALSO` entry. > 2. Is there a tactic that will drive negation down? For example, > it should change the goal ... this will work on your example: e (CONV_TAC NOT_EXISTS_CONV THEN REWRITE_TAC[DE_MORGAN_THM]);; > 3. Where are 0 and 1 defined. I want to prove ~(0=1). I think in `prim_rec` but not sure. There are several theorems that will allow you to show ~(0=1). For example SUC_NOT |- !n. ~(0 = SUC n) since 1 = SUC 0. The library `reduce` by John Harrison will proof this and many concrete numerical relations. load_library `reduce`;;Loading library reduce ... REDUCE_CONV "~(0=1)";;|- ~(0 = 1) = T REDUCE_CONV "23 < 12";;|- 23 < 12 = F > 4. Are that there functions that would list all currently available: > > 1) theorems > 2) tactics > 3) conversions > 4) derrived rules of inference I will highly recomend that you use `xholhelp` (Sarah Kalvala). You can search the HOL documentation by using partial strings. For example `apropos ASM` will give you any rule conversion or tactic with the string `ASM` in it: ADD_ASSUM : (term -> thm -> thm) Adds an assumption to a theorem. ASSUME : (term -> thm) Introduces an assumption. ASSUME_TAC : thm_tactic Adds an assumption to a goal. ASSUM_LIST : ((thm list -> tactic) -> tactic) Applies a tactic generated from the goal's assumption list. CHECK_ASSUME_TAC : thm_tactic Adds a t ... By using the `theorems` button and the wildcard `*` you can get all theorems. The wildcard `*` does not work by itself with apropos. Good lock, Victor.