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
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
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
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
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
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
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
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
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
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
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
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
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
", 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
/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
“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
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
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.)
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
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
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
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:
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
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
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),
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
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
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
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
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
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
31 matches
Mail list logo