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 nee
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 difference)
certain compound monads.
Cheers,
Jeremy
On 26/09/15 09:56, Ramana Kumar wrote:
> Hi Jeremy,
>
> Thanks for the links and information. It's rather more than I was
> expecting. Do you (or anyone on list) think that function deserves a
> place (perhaps under a different name) in
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 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 functi
ction in the HOL logic, how
> could I use it ?
>
>
> -- ------
> *??:* "Jeremy Dawson";;
> *:* 2015??11??29??(??) 7:56
> *??:* "";
> "hol-info";
> *:* Re: [Hol-info
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
requir
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 bu
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 to
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 grea
Hi Chun,
It looks as though you have this worked out, so I won't give a long
reply, but here's a few short comments:
There's a distinction between an inductively defined set (in Isabelle or
HOL) and a datatype, though they can look similar. I don't know which
corresponds better to your Coq co
It's not a consistent solution, that command returns nothing for me, and
ldd output doesn't include libpolyml (why?)
[jeremy@hp2016 private]$ ldd /usr/local/bin/poly
linux-vdso.so.1 (0x7ffed5163000)
libpthread.so.0 => /lib64/libpthread.so.0 (0x7f99a52dc000)
libgmp.
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 match_m
t;, 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
Castelán Castro wrote:
On 05/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 difficul
s to do reasoning directly on “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
ha scritto:
Hi Mario,
Slightly off-topic, I had experience with the type system of HOL-O
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 f
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
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 cr
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 w
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
assum
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), tog
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 to
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 th
There's a total version of TL, called TL_T, it's in theory rich_list
Jeremy
On 02/15/2019 04:13 AM, Thomas Sewell wrote:
> "TL [] = []"
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
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-in
or a meta-level
statement about an object level term x? I 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 M
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)`;
>
> He
Ramana Kumar wrote:
> On Mon, May 21, 2012 at 3:29 AM, Lu Zhao 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 inference steps
Mark wrote:
> on 9/7/12 5:48 PM, Cris Perdue 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 varia
Difficult questions. Regarding any term with an undefined subterm as
undefined is simplest - then you can have theorems like (A DIV B) TIMES
B = A without side conditions.
Problem is, though, you want to be able to write
"if A NOT EQ [] THEN HD A ..."
which can have an undefined subterm (HD A).
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
practitioners
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
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 (sub
37 matches
Mail list logo