Re: [Hol-info] How were type variables added to higher order logic?

2008-10-09 Thread Jeremy Dawson
would find it more natural to say the former. But does the answer to that question matter? Jeremy Dawson - This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based

Re: [Hol-info] prove a goal in HOL4

2010-04-07 Thread Jeremy Dawson
liy_...@encs.concordia.ca wrote: I have to prove a goal in HOL4 as following: g `!a b c. (indep bern a c) /\ (indep bern b c) == (a IN events bern) /\ (b IN events bern) /\ (c IN events bern) /\ (prob bern (a INTER b INTER c) = prob bern (a INTER b) * prob bern c)`; Here, a

Re: [Hol-info] useful HOL statistics to show the amount of proof work?

2012-05-21 Thread Jeremy Dawson
Ramana Kumar wrote: On Mon, May 21, 2012 at 3:29 AM, Lu Zhao luz...@cs.utah.edu wrote: This is particularly dangerous when I have proof automation scripts that try different rewriting rules. The number reported is not representative on the complexity of the problem, but the number of

Re: [Hol-info] Proof assistants for way more people

2012-07-11 Thread Jeremy Dawson
Mark wrote: on 9/7/12 5:48 PM, Cris Perdue c...@perdues.com wrote: What I was talking about though is ease of use of software products, and a proof assistant is definitely a software product. To get many people to use a software product, especially one that is not just a minor

Re: [Hol-info] merging duplicate subgoals

2015-02-02 Thread Jeremy Dawson
Yes, indeed. When the subgoals are identical (including the assumptions), Tactical.USE_SG_THEN ACCEPT_TAC should do it. Otherwise, the doc for USE_SG_THEN gives a couple of examples how it can be used. This requires you to identify which subgoal is to be used in proving which other. They

Re: [Hol-info] irule vs MP_CANON

2015-11-16 Thread Jeremy Dawson
Hi Ramana, Well, they are both ways of matching the final consequent of a1 ==> a2 ==> a3 ==> ... ==> c with the goal. Until I saw your question I hadn't been aware of the existence of MP_CANON. Possibly the biggest difference is that irule will produce multiple new subgoals (eg, in the above

Re: [Hol-info] map_option

2015-09-25 Thread Jeremy Dawson
Hi Ramana, It's rather a similar situation to what I wrote about in http://users.cecs.anu.edu.au/~jeremy/pubs/fgc/fgs/fgs.pdf and also http://users.cecs.anu.edu.au/~jeremy/pubs/fgc/cats/fgc.ps except that I seem to have used sets instead of lists (which I don't think should make a

Re: [Hol-info] About the use of symbol | in HOL4

2015-11-29 Thread Jeremy Dawson
Hi Ada, In the first case you're trying to define a function in the HOL logic. In the second case you're defining a SML function Jeremy On 29/11/15 22:15, Ada wrote: > Hey guys, > > I am learning to use HOL. I find an interesting thing about the use of > symbol | in HOL4. > I defined an

Re: [Hol-info] some questions about the use of HD and TL in listTheory

2015-11-30 Thread Jeremy Dawson
Hi Ada, when you enter first ([0,1,0,1,0],3); this refers to the SML function first whose type is given by first ; val it = fn: ('a -> bool) -> 'a list -> 'a What you want is the HOL term ``first ([0,1,0,1,0],3)`` which will also give you a type error, since your definition of first

Re: [Hol-info] [SPAM] some questions about the proving process in HOL4

2015-12-14 Thread Jeremy Dawson
Hi Ada, You need to search for suitable theorems. In this case > apropos ``TAKE 0`` ; <> val it = [(("list", "TAKE_0"), (|- TAKE 0 l = [], Thm)), so from the initial goal e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute); e (ASM_REWRITE_TAC [listTheory.TAKE_0]) ; This should work

Re: [Hol-info] How to transform list format from "(cx l q p)" to "l"

2016-02-28 Thread Jeremy Dawson
It might be easier to avoid using TAKE_DROP_LENGTH but instead try to simplify your subgoal using LENGTH_TAKE_EQ and LENGTH_DROP Then I think you'll have to instantiate your subgoal 0 once with p,q and once with q,p Cheers, Jeremy On 28/02/16 22:48, Ada wrote: > Hey,guys > > I am learning

Re: [Hol-info] How to prove this theorem about relations?

2017-01-20 Thread Jeremy Dawson
Hi Chun, I don't think your example captures the distinction, since, as you prove, AList and BList are the same. you're right about > 1. [] is List > and > 2. If l = h::t and t is List, then l is List. In fact the only subset satisfying these (which is therefore both the least and the

Re: [Hol-info] Strange tactics bug when using match_mp_tac

2017-08-23 Thread Jeremy Dawson
I've been caught out with the same thing for MATCH_MP, I defined (* MATCH_MP2 delays raising an exception until second argument is seen, *) fun MATCH_MP2 th1 th2 = MATCH_MP th1 th2 ; Jeremy On 23/08/17 17:03, michael.norr...@data61.csiro.au wrote: You are being caught by the fact that

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

2017-10-05 Thread Jeremy Dawson
", ie the best compromise between ease of use and expressive power. Cheers, Jeremy Dawson On 06/10/17 03:46, Mario Castelán Castro wrote: On 04/10/17 20:09, Ramana Kumar wrote: Perhaps it would make more sense to ask people who are using rich type systems what their motivations are :) (On

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

2017-10-05 Thread Jeremy Dawson
/10/17 11:53, Jeremy Dawson wrote: Hi Mario, Slightly off-topic, I had experience with the type system of HOL-Omega (system F, if I recall the terminology right, not dependent types, so my experience may not be very relevant) My dominant recollection is the difficulty of getting the system to do

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

2017-10-05 Thread Jeremy Dawson
“proofs” (or can we say “proofs” are 1st-class objects?) also a consequence of “rich” type systems? Regards, Chun Tian Il giorno 05 ott 2017, alle ore 18:53, Jeremy Dawson <jeremy.daw...@anu.edu.au> ha scritto: Hi Mario, Slightly off-topic, I had experience with the type system of

Re: [Hol-info] Proof about sorting

2017-12-03 Thread Jeremy Dawson
You might like to try the following (1) a predicate sorted, to mean each list member is <= the next one (2) a lemma that inserting an element into a sorted list gives a sorted list Jeremy On 04/12/17 12:58, Liu Gengyang wrote: Hi, Recently I am meeting a problem, it has been confusing me a

Re: [Hol-info] INVERSE of function?

2018-05-27 Thread Jeremy Dawson
Hi Chun, See LINV and RINV in pred_set. I found the definitions of these pointlessly restrictive since they only applied for an injective/surjective function. So I changed things to define them both in terms of LINV_OPT which I defined. (Hence the old theorem names LINV_DEF and RINV_DEF.)

Re: [Hol-info] Formalizing logical puzzles

2018-06-26 Thread Jeremy Dawson
Hi Dylan, I'm familiar with HOL4 not HOL Light, but it looks as though they are similar at this point: you have made a definition of a function called goldInsc and you have named that definition (ie the theorem stating the definition) goldInsc Jeremy On 06/27/2018 12:37 AM, Dylan Melville

Re: [Hol-info] working proof that shouldn't need to be so complicated

2018-01-05 Thread Jeremy Dawson
Sorry if I've missed your point (just a quick reply) but On 01/06/2018 05:18 AM, Michael Beeson wrote: SIMP isn't a conversion SIMP_CONV is a conversion, which may give what you want And if RHS_CONV would do what you want, no need to use PAT_CONV Jeremy

Re: [Hol-info] Share list of terms with later theories

2018-01-16 Thread Jeremy Dawson
A related question: some time back I was looking at how datatypes are constructed, and found stuff in theory ind_type, and theorems like list_TY_DEF (which one finds by doing find "ty_def") But it seems that there are also theorems created which define the constructors of the list datatype in

Re: [Hol-info] Applying a theorem to a specific subgoal

2018-08-08 Thread Jeremy Dawson
Hi Dylan, from HOL/help/Docfiles/HTML/Tactical.NTH_GOAL.html (or help "NTH_GOAL" ; ) Where tac1 and tac2 are tactics, tac1 THEN_LT NTH_GOAL n tac2 applies tac1 to a goal, and then applies tac2 to the n’th resulting subgoal. Cheers, Jeremy On 08/08/2018 03:24 PM, Dylan Melville wrote:

Re: [Hol-info] Using Assumptions

2018-08-16 Thread Jeremy Dawson
Also, if ever giving a pattern to match your chosen assumption doesn't suit, you can use ASSUM_LIST - which gives you a list of all assumptions to use in constructing your next tactic, and you can pick one of that list. But note the caveat in the doc page about relying on the order of

Re: [Hol-info] About the experimental kernel

2018-04-11 Thread Jeremy Dawson
On 12/04/18 01:59, Mario Xerxes Castelán Castro wrote: for explicit lazy beta conversions (with an internal explicit substitution calculus) I assume this refers to Clos, mk_clos etc in src/0/Term.sml My questions is: is this actually used? I can't see where anything in the source code

Re: [Hol-info] assumption matching in SPLIT_LT

2018-10-12 Thread Jeremy Dawson
Hi Waqar, Firstly (simplest), SPLIT_LT 2 (ALLGOALS tac1, ALL_LT) applies tac1 to the first two subgoals and does nothing to the remainder. Then you can work on the remaining goal. But you want to also apply EVERY [tac2, tac3, ...] to the third subgoal (which is the only remaining one),

Re: [Hol-info] New grammar of defining theorems?

2019-01-07 Thread Jeremy Dawson
This summary seems to make it clear that this new feature achieves very little, with the following costs: - it gives users yet something else (as if there isn't already enough!) to lookup in the documentation, or ask questions about - it's positively confusing, in that "Theorem name ... " has

Re: [Hol-info] New grammar of defining theorems?

2019-01-07 Thread Jeremy Dawson
On 8/1/19 4:49 pm, michael.norr...@data61.csiro.au wrote: > I think you've misunderstood. that's true, sorry. > Here the advantage is quite clear and valuable: in the existing system, you > have to type the same string of symbols twice in order to avoid annoying > maintenance issues when

Re: [Hol-info] 0 / 0 = 0 ???

2019-02-14 Thread Jeremy Dawson
Sorry for my previous confusing email, this is something I didn't know about. It seems now TL and TL_T are the same. Jeremy On 02/15/2019 09:59 AM, michael.norr...@data61.csiro.au wrote: > the updated definition of TL. ___ hol-info mailing list

[Hol-info] CFP - ICFEM 2020 - Int'l Conf on Formal Engineering Methods

2020-04-01 Thread Jeremy Dawson
CALL FOR PAPERS 22nd International Conference on Formal Engineering Methods (ICFEM 2020), 2-6 November 2020, Singapore. http://formal-analysis.com/icfem/2020/ Since 1997, ICFEM provides a forum for both researchers and

[Hol-info] ICFEM'20 - submission deadline extended

2020-05-19 Thread Jeremy Dawson
Due to the requests from authors, the submission deadline of ICFEM 2020 has been extended to 24 May 2020 (AOE). Here is the revised CFP --- CALL FOR PAPERS --- 22nd International Conference on Formal Engineering Methods (ICFEM 2020), 2-6 November 2020, Singapore

[Hol-info] ICFEM'20 deadline extended to 17th May 2020

2020-05-02 Thread Jeremy Dawson
of Singapore, Singapore Ranald Clouston, Australian National University, Australia Sylvain Conchon, Universite Paris-Sud, France Florin Craciun, Babes-Bolyai University, Romania Jeremy Dawson, Australian National University, Australia Frank De Boer, Centrum Wiskunde & Informatica (CWI), Netherl