hol-developers Mailing List for HOL theorem-proving system

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 454-5900

I wonder if the mailing list infrastructure at SourceForge is working.

Michael

Hi all,

Prompted by https://github.com/HOL-Theorem-Prover/HOL/pull/643 I'm tempted to push on and merge the remove-eqterm-type branch into develop, and then master.  This will remove the ability to use = on term values.  Instead, you will have to use aconv (available as infix ~~), or just possibly identical (which insists that bound variables are named the same way).

Using = is only conceivably right when comparing variables and/or constants: elsewhere explicit substitutions and/or bound variables can mean that = is too narrow.

Please let me know if you think that we should keep =, and why.

Best,
Michael

Prompted by (completely justified) kvetching by CakeML developers, I have recently been trying a different workflow for HOL development.  Instead of pushing directly to master, I've been doing everything with respect to the develop branch.  My regression test machinery attempts to build develop at selftest level 3 every day.  If that passes, then I fast-forward master up to the passing commit. 

To enforce this, I have used github's facilities to make it impossible for anyone except owners/administrators to push to HOL master.  At the moment, the owner set is {Ramana; Konrad; Michael}. 

So please feel free to push to develop in just the same way that you have historically pushed to master.  I will semi-automatically roll master forward when I see the tests of develop pass.  

Net effect: master should always be in a known-good state.

Michael

Thanks! In my case, I was running through a topsorted list of prospective
definitions, and making the definitions. Which promptly failed because they
were being made in reverse order!

Konrad.

On Wed, Dec 12, 2018 at 4:14 PM <Mic...@da...> wrote:

> I’ve just pushed a revised version to HOL master.
>
>
>
> Michael
>
>
>
> *From: *"Mic...@da..." <Mic...@da...
> >
> *Date: *Wednesday, 12 December 2018 at 16:21
> *To: *"kon...@gm..." <kon...@gm...>, hol-developers
> mailing list <hol...@li...>
> *Subject: *[ExternalEmail] Re: [Hol-developers] mapfilter wrong?
>
>
>
> I agree that the current behaviour is “wrong”.  I think I can just use the
> Basis library’s List.mapPartial in conjunction with total (as in your
> example) to implement this.  (I’ve checked that List.mapPartial does
> evaluated L-to-R.)
>
>
>
> Michael
>
>
>
> *From: *Konrad Slind <kon...@gm...>
> *Date: *Tuesday, 11 December 2018 at 15:32
> *To: *hol-developers mailing list <hol...@li...>
> *Subject: *Re: [Hol-developers] mapfilter wrong?
>
>
>
> Replacement:
>
>
>
> fun mapfilter f list =
>
>   let fun mapf [] acc = rev acc
>
>         | mapf (h::t) acc =
>
>              case total f h
>
>                of NONE => mapf t acc
>
>                |  SOME h' => mapf t (h'::acc)
>
>   in
>
>    mapf list []
>
>   end;
>
>
>
>
>
> On Mon, Dec 10, 2018 at 10:24 PM Konrad Slind <kon...@gm...>
> wrote:
>
> I just spent some time being quite puzzled by Lib.mapfilter:
>
>
>
> fun mapfilter f list =
>
>    itlist (fn i => fn L => (f i :: L)
>
>                 handle Interrupt => raise Interrupt
>
>                      | otherwise => L)
>
>           list []
>
>
>
> I was assuming that it executes left-to-right on the list, but the itlist
> shows that the traversal is back to front. When parameter f is imperative
> code, this can lead to unexpected behaviour. Also, the itlist isn't tail
> rec. and mapfilter should be.
>
>
>
> Konrad.
>
>
>
>

I’ve just pushed a revised version to HOL master.

Michael

From: "Mic...@da..." <Mic...@da...>
Date: Wednesday, 12 December 2018 at 16:21
To: "kon...@gm..." <kon...@gm...>, hol-developers mailing list <hol...@li...>
Subject: [ExternalEmail] Re: [Hol-developers] mapfilter wrong?

I agree that the current behaviour is “wrong”.  I think I can just use the Basis library’s List.mapPartial in conjunction with total (as in your example) to implement this.  (I’ve checked that List.mapPartial does evaluated L-to-R.)

Michael

From: Konrad Slind <kon...@gm...>
Date: Tuesday, 11 December 2018 at 15:32
To: hol-developers mailing list <hol...@li...>
Subject: Re: [Hol-developers] mapfilter wrong?

Replacement:

fun mapfilter f list =
  let fun mapf [] acc = rev acc
        | mapf (h::t) acc =
             case total f h
               of NONE => mapf t acc
               |  SOME h' => mapf t (h'::acc)
  in
   mapf list []
  end;

On Mon, Dec 10, 2018 at 10:24 PM Konrad Slind <kon...@gm...<mailto:kon...@gm...>> wrote:
I just spent some time being quite puzzled by Lib.mapfilter:

fun mapfilter f list =
   itlist (fn i => fn L => (f i :: L)
                handle Interrupt => raise Interrupt
                     | otherwise => L)
          list []

I was assuming that it executes left-to-right on the list, but the itlist shows that the traversal is back to front. When parameter f is imperative code, this can lead to unexpected behaviour. Also, the itlist isn't tail rec. and mapfilter should be.

Konrad.

I agree that the current behaviour is “wrong”.  I think I can just use the Basis library’s List.mapPartial in conjunction with total (as in your example) to implement this.  (I’ve checked that List.mapPartial does evaluated L-to-R.)

Michael

From: Konrad Slind <kon...@gm...>
Date: Tuesday, 11 December 2018 at 15:32
To: hol-developers mailing list <hol...@li...>
Subject: Re: [Hol-developers] mapfilter wrong?

Replacement:

fun mapfilter f list =
  let fun mapf [] acc = rev acc
        | mapf (h::t) acc =
             case total f h
               of NONE => mapf t acc
               |  SOME h' => mapf t (h'::acc)
  in
   mapf list []
  end;

On Mon, Dec 10, 2018 at 10:24 PM Konrad Slind <kon...@gm...<mailto:kon...@gm...>> wrote:
I just spent some time being quite puzzled by Lib.mapfilter:

fun mapfilter f list =
   itlist (fn i => fn L => (f i :: L)
                handle Interrupt => raise Interrupt
                     | otherwise => L)
          list []

I was assuming that it executes left-to-right on the list, but the itlist shows that the traversal is back to front. When parameter f is imperative code, this can lead to unexpected behaviour. Also, the itlist isn't tail rec. and mapfilter should be.

Konrad.

Replacement:

fun mapfilter f list =
  let fun mapf [] acc = rev acc
        | mapf (h::t) acc =
             case total f h
               of NONE => mapf t acc
               |  SOME h' => mapf t (h'::acc)
  in
   mapf list []
  end;

On Mon, Dec 10, 2018 at 10:24 PM Konrad Slind <kon...@gm...>
wrote:

> I just spent some time being quite puzzled by Lib.mapfilter:
>
> fun mapfilter f list =
>    itlist (fn i => fn L => (f i :: L)
>                 handle Interrupt => raise Interrupt
>                      | otherwise => L)
>           list []
>
> I was assuming that it executes left-to-right on the list, but the itlist
> shows that the traversal is back to front. When parameter f is imperative
> code, this can lead to unexpected behaviour. Also, the itlist isn't tail
> rec. and mapfilter should be.
>
> Konrad.
>
>

I just spent some time being quite puzzled by Lib.mapfilter:

fun mapfilter f list =
   itlist (fn i => fn L => (f i :: L)
                handle Interrupt => raise Interrupt
                     | otherwise => L)
          list []

I was assuming that it executes left-to-right on the list, but the itlist
shows that the traversal is back to front. When parameter f is imperative
code, this can lead to unexpected behaviour. Also, the itlist isn't tail
rec. and mapfilter should be.

Konrad.

I've just made "isolated" (i.e, surrounded by whitespace) dollar signs available as identifiers in the parser.  (Previously, they would have caused bad error messages.)

Given that no-one has ever been able to use these before, they're like virgin territory with which we can do anything we want.

I'm tempted to make the single $ sign act like Haskell's $ operator in the parser. 

In SML, you'd write

  infixr 0 $
  fun (f $ x) = f x

to get the Haskell-ish behaviour.

The utility is in being able to write deeply nested function applications with fewer parentheses.  Like parentheses, the $ does not persist past parsing of concrete syntax. 

Thus we could write

  > “f $ g $ x + 1”;
  <<HOL message: inventing new type variable names: 'a, 'b>>
  val it = “f (g (x + 1))”: term

or

  > EVAL ``MAP SUC $ GENLIST (\x. x * 2) 4``;
  val it = ⊢ MAP SUC (GENLIST (λx. x * 2) 4) = [1; 3; 5; 7]: thm

Note that I don't know how to print the term back except with the standard parentheses (there might be an algorithm for deciding which form "looks better", but I'm not sure it'd be wise to use it even if you thought it was always picking the nicest formulation).

Is there any other obvious use people might want to put $ signs to?  

Note that
- $$, $$$ etc are all available as well
- for a custom application, the standard functions make it easy to remove the rule for $ in the global grammar and put in one's own constant/syntax.

Any thoughts?

Michael

The CakeML experience has led to the creation of a theorem-tactic, drule, that “resolves” the theorem argument against an assumption and puts the result into the goal using mp_tac.

Thus, something like

   drule (|- !x y. P x /\ Q x y ==> ?z. R x y z) ([..., ``P 3``, ...], Goal) 

results in the new goal

   ([..., ``P 3``, ...], ``(!y. Q 3 y ==> ?z. R 3 y z) ==> Goal``)

This is an improvement on IMP_RES_TAC because it doesn’t look for all possible matches against all possible “normalisations” of the implicational theorem.  For example, 

  IMP_RES_TAC th ([``P 3``, ``Q 10 y``], Goal)

puts two new assumptions into the assumptions because both the P and the Q assumptions match against the input theorem. The primitive that IMP_RES_TAC builds on (IMP_RES_THEN) has the same sort of issue because it depends on RES_CANON, which produces lists of implicational forms. In particular, P /\ Q ==> R gets turned into P ==> (Q ==> R) as well as Q ==> (P ==> R).

There is an enormous family of plausible tactics in this area, and they’re all relatively easy to implement. The bigger problem is coming up with a naming scheme that makes them easy for people to learn, and to keep in their heads so that they stand some chance of getting used. 

I suggest that we can first split the “space” into three orthogonal dimensions:

1. how the assumption gets treated after it has been resolved against the implicated. The drule tactic leaves it alone. Two other possibilities would be to (a) remove it from the assumption list (this could be indicated by an ‘x’ in the name by analogy with first_x_assum etc); (b) mark it so that it cannot get used again until ‘released’. This may seem odd, but if you are resolving many assumptions at once, and your implication is something like a confluence theorem or IH, then may not want to remove each occurrence of R x y, but you don’t want to use the same R x y when you are resolving against something like !a b c. R a b /\ R a c ==> ?d. …

2. what the continuation should be. IMP_RES_TAC uses STRIP_ASSUME_TAC; drule uses mp_tac.  We can’t encode all possible continuations into the name, but we might encode some, and then have one last “more primitive” form that takes the continuation as a parameter

3. how many assumptions of the implicational theorem should be resolved against.  (Consuming multiple assumptions in one go is not quite the same thing as simply using REPEAT, though the latter comes close.) drule consumes 1. It’s easy to see how to implement a tactic that attempts to consume all (and fails if this is not possible). I don’t quite see how to get one that finds the maximal use of assumptions, but this might also be possible.

- - 

I am ignoring another dimension, which is to play around with which hypothesis in the implication should be resolved against. This is doable with the mp_then primitive, but I can’t see a nice way to fitting it into the following scheme.  This certainly needs control (IMP_RES_TAC’s failing in my mind is that it doesn’t do this, and only gives you the “try all assumptions and see how far you get” approach).

- - 

Naming proposal:

  drule   - as it is now

  dxrule  - removes the assumption resolved against

  drulek  - takes continuation as parameter, e.g., drulek strip_assume_tac myimpthm

  dxrulek - takes continutation, removes assumption

  drule_all - fails if after resolving as much as possible the result is still an implication (possibly hiding under universal quantifiers)

Then: dxrule_all, drule_allk, dxrule_allk are, I hope, clear.

Instead of ‘x’, you might also have ‘m’ (“marked”) to stop assumptions from being used a second time.  The multi-assumption tactics (e.g., with all) could clear all marks after completion, or leave that up to the user. I suspect the -k variants would be used with strip_assume_tac  more often than not. Perhaps there should be a variant that did this instead of mp_tac.  I don’t know how one might indicate this.  (Perhaps with ‘s’ instead of ‘d’ giving sxrule_allk as an example.  Yikes.)

Finally, if it was possible to figure out how to do it, you might have ‘max’ as well as ‘all’. Note that specific (small) numbers of resolutions can be done with -k variants. E.g., 

   drulek drule impthm

There is a point of diminishing returns here, and I think it’s clear that mp_then will probably allow everything useful underneath, so that there is no need to cater to super-obscure usages, when a custom mp_then tactic can be written out by hand.

- -

Please let me know if there’s an obvious dimension I’ve missed out, or if there’s another point I haven’t considered on the existing dimensions. If you come up with a naming scheme that fits into the above, I can also go ahead and implement what I’ve already proposed anyway… (

Michael

Bid Writing Workshops for Charities, Schools, Associations and Not For Profit OrganisationsNFP WORKSHOPS
 Affordable training courses for charities, schools, associations and social enterprises

Bid Writing : The Basics 
TOPICS COVERED
Who are the winners and losers in grant funding. How to identify the weaknesses in your project. What questions will funders will ask themselves about your bid. Common reasons for applications being rejected. The key terms in bid writing explained with examples of each. Make your application short but effective. 
Start telling funders the things they really want to hear. How to build greater credibility in the eyes of funders. Demonstrating that the beneficiaries of your project are involved. The importance of getting your numbers and totals right. What to do with all your supporting documents. Make your proofreading foolproof.
ATTENDEES  
Staff members, volunteers, board members or trustees of charities, schools, associations or not for profit organisations who are about to submit grant funding applications to grant making trusts and foundations.
COST  
£95 including booking fees. Refreshments provided. Each attendee will receive a full set of notes and copies of eight real successful funding bids by e-mail after the workshop.
PAYMENT
All places must be booked using a debit or credit card through the online booking system. We do not issue invoices or accept bank or cheque payments. If you do not have a debit card from your organisation please use a personal one and claim reimbursement using the booking confirmation e-mail as proof of purchase.
BOOKING TERMS  
Workshop bookings are non cancellable, non refundable and non transferable between dates. If you are unable to attend on the date booked you may send someone else in your place.
QUESTIONS
Fully booked means fully booked. There are no waiting lists for people hoping for a cancellation. If you have a question please e-mail wor...@nf... and you will usually receive a response within 24 hours.

Bid Writing : Advanced 
TOPICS COVERED
Are you applying to the right trusts ? Are you looking for trusts in all the right places ? Are you applying to enough trusts ? Are you applying in the right ways ? Are your projects the most fundable projects ? How do you compare with your competitors for funding ? 
Are you carrying out trust fundraising in a professional way ? Do you understand what trusts are looking for ? Do you know how to turn your competitors into your ambassadors ? Is the rest of your fundraising hampering your bids to trusts ?  
ATTENDEES  
Staff members, volunteers, board members or trustees of charities, schools, associations or not for profit organisations who are about to submit grant funding applications to grant making trusts and foundations. 
It is assumed that you already know the basic bid writing skills of good preparation, eligibility checking, clear writing and adequate proof reading. If you do not you should attend The Basics workshop first. Around half of all attendees attend both The Basics and Advanced workshops on the same day but there is no discount for attending both.
COST  
£95 including booking fees. Refreshments provided. Each attendee will receive a full set of notes and copies of eight real successful funding bids by e-mail after the workshop.
PAYMENT
All places must be booked using a debit or credit card through the online booking system. We do not issue invoices or accept bank or cheque payments. If you do not have a debit card from your organisation please use a personal one and claim reimbursement using the booking confirmation e-mail as proof of purchase.
BOOKING TERMS  
Workshop bookings are non cancellable, non refundable and non transferable between dates. If you are unable to attend on the date booked you may send someone else in your place.
QUESTIONS  
Fully booked means fully booked. There are no waiting lists for people hoping for a cancellation. If you have a question please e-mail wor...@nf... and you will usually receive a response within 24 hours.
 London
Bid Writing : The Basics 30 Oct 2017Fully Booked
Bid Writing : Advanced30 Oct 2017Fully Booked
Bid Writing : The Basics 31 Oct 2017Fully Booked
Bid Writing : Advanced31 Oct 2017Fully Booked
Bid Writing : The Basics 06 Nov 2017Fully Booked
Bid Writing : Advanced06 Nov 2017Fully Booked
Bid Writing : The Basics 04 Dec 2017Fully Booked
Bid Writing : Advanced04 Dec 2017Fully Booked
Bid Writing : The Basics 08 Jan 2018Booking Details
Bid Writing : Advanced08 Jan 2018Booking Details
Bid Writing : The Basics 15 Jan 2018Fully Booked
Bid Writing : Advanced15 Jan 2018Last 9 Places
Bid Writing : The Basics 16 Jan 2018Last 4 Places
Bid Writing : Advanced16 Jan 2018Booking Details
Bid Writing : The Basics 22 Jan 2018Booking Details
Bid Writing : Advanced22 Jan 2018Booking Details
Bristol
Bid Writing : The Basics 02 Nov 2017Fully Booked
Bid Writing : Advanced02 Nov 2017Fully Booked
Bid Writing : The Basics 05 Dec 2017Fully Booked
Bid Writing : Advanced05 Dec 2017Last 4 Places
Bid Writing : The Basics 18 Jan 2018Booking Details
Bid Writing : Advanced18 Jan 2018Booking Details
Manchester
Bid Writing : The Basics 09 Nov 2017Fully Booked
Bid Writing : Advanced09 Nov 2017Fully Booked
Bid Writing : The Basics 06 Dec 2017Last 9 Places
Bid Writing : Advanced06 Dec 2017Last Place
Bid Writing : The Basics 25 Jan 2018Last 8 Places
Bid Writing : Advanced25 Jan 2018Booking Details
Leeds
Bid Writing : The Basics 10 Nov 2017Last 3 Places
Bid Writing : Advanced10 Nov 2017Fully Booked
Bid Writing : The Basics 07 Dec 2017Last 7 Places
Bid Writing : Advanced07 Dec 2017Last Place
Bid Writing : The Basics 26 Jan 2018Last 5 Places
Bid Writing : Advanced26 Jan 2018Last 8 Places
Edinburgh
Bid Writing : The Basics 10 Jan 2018Last 4 Places
Bid Writing : Advanced10 Jan 2018Last 6 Places
Southampton
Bid Writing : The Basics 01 Nov 2017Last Place
Bid Writing : Advanced01 Nov 2017Fully Booked
Bid Writing : The Basics 17 Jan 2018Booking Details
Bid Writing : Advanced17 Jan 2018Booking Details
Nottingham
Bid Writing : The Basics 07 Nov 2017Fully Booked
Bid Writing : Advanced07 Nov 2017Fully Booked
Bid Writing : The Basics 23 Jan 2018Last 10 Places
Bid Writing : Advanced23 Jan 2018Last 10 Places
Birmingham
Bid Writing : The Basics 08 Nov 2017Fully Booked
Bid Writing : Advanced08 Nov 2017Fully Booked
Bid Writing : The Basics 24 Jan 2018Booking Details
Bid Writing : Advanced24 Jan 2018Booking Details

What Past Attendees Have Said About Our Bid Writing Workshops
The workshop was excellent. I consider myself fairly experienced in bid writing and have been fairly successful. To your credit I learnt a lot from you which I will certainly put into practice.  I felt re-invigorated and encouraged. 
You definitely know your stuff. The course was certainly packed with information. Gave me plenty to think about and ways forward. I’m more used to courses where they pack half an hour into a full day!! 
For a person like me who writes lots of proposals it was exactly what I needed. Straight to the point, less "water", more sense and fantastic examples! The course was excellent. 
I picked up some great new ideas and tips. It’s hard to find good quality info these days re attracting funding – but on this occasion the juice was definitely worth the squeeze! 
I thought it was really useful training and you managed to fit a huge amount of information into 2.5 hours without it feeling too much to take in. Well done. Remarkably concise and useful. 
Plenty of useful do's and don'ts. Having attended dozens of training courses over the years, it was a very pleasant surprise not to have my time wasted with pointless break out groups, workshop exercises or unrelated show and tell experiences.  
I really enjoyed the workshop yesterday. I thought the pace and delivery was excellent and it has really given me the confidence to move forward. Thank you so much – definitely money well spent. I will now be more time-efficient 
Did just what it said on the tin. I thought the workshop was very informative. It was an interesting couple of hours, style delivery was to the point and no fussy power point’s to contend with.
We learned a great deal from your courses. I liked your engagement with the subject and your personal anecdotes. The course material overall was truly inspiring! Put things into perspective for us.
I did like your matter of fact approach I thought that your presentations were really excellent and will, I know, prove extremely useful in the coming months.
I feel much better prepared and have a much longer to do list now! A brilliant workshop. 
I shall recommend your workshop others. The pace, delivery and content was tremendously helpful and informative.  
I thought you as a trainer were friendly and relaxed, easy to be with and kept us engaged and you made learning interesting. Thoroughly enjoyed your insights and anecdotes. 
It was great and great value for money also. I thought that learning in a small group was really good and meant that we were able to communicate with you a lot easier. 
Thank you so much for your professionalism, sense of humour and all the knowledge you kindly shared with us. I now realise I have been emphasising many of the wrong angles. 
Informative, to the point and engaging.I just want to thank you for a most informative session. I certainly picked up some great ideas and hints to enhance my future bid applications.
I found it very informative I feel a lot more confidant about the process of bid writing.  I would certainly recommend your course to others.

Sign Up For Your Own Copy 
If you are reading a mailer sent to a colleague and wish to receive your own copy in future please e-mail si...@nf... quoting your email address in the subject line.
Unsubscribe From Our Mailing List 
CLICK TO REMOVE YOUR E-MAIL ADDRESS FROM OUR MAILING LIST
Alternatively send a blank e-mail to uns...@nf... quoting the email address we are sending to i.e. hol...@li... in the subject line in lower case letters. Our automated system will remove all email addresses in the subject line from our mailing lists within 7 days. If you leave the subject line blank, use capital letters, type a person's name, unsubscribe or anything else then nothing will be removed from our lists. Any text within the body of the email will not be read.  
NFP Workshops, Blake House, 18 Blake Street, York YO1 8QH 

6cQqGQq

Affordable Training Courses for Charities, Schools, Associations and Not For Profit OrganisationsNFP WORKSHOPS
 Affordable training courses for charities, schools, associations and social enterprises

Bid Writing : The Basics 
TOPICS COVERED
Who are the winners and losers in grant funding. How to identify the weaknesses in your project. What questions will funders will ask themselves about your bid. Common reasons for applications being rejected. The key terms in bid writing explained with examples of each. Make your application short but effective. 
Start telling funders the things they really want to hear. How to build greater credibility in the eyes of funders. Demonstrating that the beneficiaries of your project are involved. The importance of getting your numbers and totals right. What to do with all your supporting documents. Make your proofreading foolproof.
ATTENDEES  
Staff members, volunteers, board members or trustees of charities, schools, associations or not for profit organisations who are about to submit grant funding applications to grant making trusts and foundations.
COST  
£95 including booking fees. Refreshments provided. Each attendee will receive a full set of notes and copies of eight real successful funding bids by e-mail after the workshop.
PAYMENT
All places must be booked using a debit or credit card through the online booking system. We do not issue invoices or accept bank or cheque payments. If you do not have a debit card from your organisation please use a personal one and claim reimbursement using the booking confirmation e-mail as proof of purchase.
BOOKING TERMS  
Workshop bookings are non cancellable, non refundable and non transferable between dates. If you are unable to attend on the date booked you may send someone else in your place.
QUESTIONS
Fully booked means fully booked. There are no waiting lists for people hoping for a cancellation. If you have a question please e-mail wor...@nf... and you will usually receive a response within 24 hours.

Bid Writing : Advanced 
TOPICS COVERED
Are you applying to the right trusts ? Are you looking for trusts in all the right places ? Are you applying to enough trusts ? Are you applying in the right ways ? Are your projects the most fundable projects ? How do you compare with your competitors for funding ? 
Are you carrying out trust fundraising in a professional way ? Do you understand what trusts are looking for ? Do you know how to turn your competitors into your ambassadors ? Is the rest of your fundraising hampering your bids to trusts ?  
ATTENDEES  
Staff members, volunteers, board members or trustees of charities, schools, associations or not for profit organisations who are about to submit grant funding applications to grant making trusts and foundations. 
It is assumed that you already know the basic bid writing skills of good preparation, eligibility checking, clear writing and adequate proof reading. If you do not you should attend The Basics workshop first. Around half of all attendees attend both The Basics and Advanced workshops on the same day but there is no discount for attending both.
COST  
£95 including booking fees. Refreshments provided. Each attendee will receive a full set of notes and copies of eight real successful funding bids by e-mail after the workshop.
PAYMENT
All places must be booked using a debit or credit card through the online booking system. We do not issue invoices or accept bank or cheque payments. If you do not have a debit card from your organisation please use a personal one and claim reimbursement using the booking confirmation e-mail as proof of purchase.
BOOKING TERMS  
Workshop bookings are non cancellable, non refundable and non transferable between dates. If you are unable to attend on the date booked you may send someone else in your place.
QUESTIONS  
Fully booked means fully booked. There are no waiting lists for people hoping for a cancellation. If you have a question please e-mail wor...@nf... and you will usually receive a response within 24 hours.
 London
Bid Writing : The Basics 30 Oct 2017Fully Booked
Bid Writing : Advanced30 Oct 2017Fully Booked
Bid Writing : The Basics 31 Oct 2017Fully Booked
Bid Writing : Advanced31 Oct 2017Last Place
Bid Writing : The Basics 06 Nov 2017Fully Booked
Bid Writing : Advanced06 Nov 2017Fully Booked
Bid Writing : The Basics 04 Dec 2017Fully Booked
Bid Writing : Advanced04 Dec 2017Fully Booked
Bid Writing : The Basics 08 Jan 2018Booking Details
Bid Writing : Advanced08 Jan 2018Booking Details
Bid Writing : The Basics 15 Jan 2018Last 2 Places
Bid Writing : Advanced15 Jan 2018Booking Details
Bid Writing : The Basics 16 Jan 2018Last 7 Places
Bid Writing : Advanced16 Jan 2018Booking Details
Bid Writing : The Basics 22 Jan 2018Booking Details
Bid Writing : Advanced22 Jan 2018Booking Details
Bristol
Bid Writing : The Basics 02 Nov 2017Fully Booked
Bid Writing : Advanced02 Nov 2017Fully Booked
Bid Writing : The Basics 05 Dec 2017Fully Booked
Bid Writing : Advanced05 Dec 2017Last 4 Places
Bid Writing : The Basics 18 Jan 2018Booking Details
Bid Writing : Advanced18 Jan 2018Booking Details
Manchester
Bid Writing : The Basics 09 Nov 2017Fully Booked
Bid Writing : Advanced09 Nov 2017Fully Booked
Bid Writing : The Basics 06 Dec 2017Last 9 Places
Bid Writing : Advanced06 Dec 2017Last 2 Places
Bid Writing : The Basics 25 Jan 2018Booking Details
Bid Writing : Advanced25 Jan 2018Booking Details
Leeds
Bid Writing : The Basics 10 Nov 2017Last 3 Places
Bid Writing : Advanced10 Nov 2017Fully Booked
Bid Writing : The Basics 07 Dec 2017Last 9 Places
Bid Writing : Advanced07 Dec 2017Last 3 Places
Bid Writing : The Basics 26 Jan 2018Last 8 Places
Bid Writing : Advanced26 Jan 2018Booking Details
Edinburgh
Bid Writing : The Basics 25 Oct 2017Fully Booked
Bid Writing : Advanced25 Oct 2017Fully Booked
Bid Writing : The Basics 10 Jan 2018Last 3 Places
Bid Writing : Advanced10 Jan 2018Last 4 Places
Southampton
Bid Writing : The Basics 01 Nov 2017Last Place
Bid Writing : Advanced01 Nov 2017Last Place
Bid Writing : The Basics 17 Jan 2018Booking Details
Bid Writing : Advanced17 Jan 2018Booking Details
Nottingham
Bid Writing : The Basics 07 Nov 2017Last Place
Bid Writing : Advanced07 Nov 2017Fully Booked
Bid Writing : The Basics 23 Jan 2018Booking Details
Bid Writing : Advanced23 Jan 2018Booking Details
Birmingham
Bid Writing : The Basics 08 Nov 2017Fully Booked
Bid Writing : Advanced08 Nov 2017Fully Booked
Bid Writing : The Basics 24 Jan 2018Booking Details
Bid Writing : Advanced24 Jan 2018Booking Details

What Past Attendees Have Said About Our Bid Writing Workshops
The workshop was excellent. I consider myself fairly experienced in bid writing and have been fairly successful. To your credit I learnt a lot from you which I will certainly put into practice.  I felt re-invigorated and encouraged. 
You definitely know your stuff. The course was certainly packed with information. Gave me plenty to think about and ways forward. I’m more used to courses where they pack half an hour into a full day!! 
For a person like me who writes lots of proposals it was exactly what I needed. Straight to the point, less "water", more sense and fantastic examples! The course was excellent. 
I picked up some great new ideas and tips. It’s hard to find good quality info these days re attracting funding – but on this occasion the juice was definitely worth the squeeze! 
I thought it was really useful training and you managed to fit a huge amount of information into 2.5 hours without it feeling too much to take in. Well done. Remarkably concise and useful. 
Plenty of useful do's and don'ts. Having attended dozens of training courses over the years, it was a very pleasant surprise not to have my time wasted with pointless break out groups, workshop exercises or unrelated show and tell experiences.  
I really enjoyed the workshop yesterday. I thought the pace and delivery was excellent and it has really given me the confidence to move forward. Thank you so much – definitely money well spent. I will now be more time-efficient 
Did just what it said on the tin. I thought the workshop was very informative. It was an interesting couple of hours, style delivery was to the point and no fussy power point’s to contend with.
We learned a great deal from your courses. I liked your engagement with the subject and your personal anecdotes. The course material overall was truly inspiring! Put things into perspective for us.
I did like your matter of fact approach I thought that your presentations were really excellent and will, I know, prove extremely useful in the coming months.
I feel much better prepared and have a much longer to do list now! A brilliant workshop. 
I shall recommend your workshop others. The pace, delivery and content was tremendously helpful and informative.  
I thought you as a trainer were friendly and relaxed, easy to be with and kept us engaged and you made learning interesting. Thoroughly enjoyed your insights and anecdotes. 
It was great and great value for money also. I thought that learning in a small group was really good and meant that we were able to communicate with you a lot easier. 
Thank you so much for your professionalism, sense of humour and all the knowledge you kindly shared with us. I now realise I have been emphasising many of the wrong angles. 
Informative, to the point and engaging.I just want to thank you for a most informative session. I certainly picked up some great ideas and hints to enhance my future bid applications.
I found it very informative I feel a lot more confidant about the process of bid writing.  I would certainly recommend your course to others.

Sign Up For Your Own Copy 
If you are reading a mailer sent to a colleague and wish to receive your own copy in future please e-mail si...@nf... quoting your email address in the subject line.
Unsubscribe From Our Mailing List 
CLICK TO REMOVE YOUR E-MAIL ADDRESS FROM OUR MAILING LIST
Alternatively send a blank e-mail to uns...@nf... quoting the email address we are sending to i.e. hol...@li... in the subject line in lower case letters. Our automated system will remove all email addresses in the subject line from our mailing lists within 7 days. If you leave the subject line blank, use capital letters, type a person's name, unsubscribe or anything else then nothing will be removed from our lists. Any text within the body of the email will not be read.  
NFP Workshops, Blake House, 18 Blake Street, York YO1 8QH 

C8Joi3b

Affordable Training Courses for Charities, Schools, Associations and Not For Profit OrganisationsNFP WORKSHOPS
 Affordable training courses for charities, schools, associations and social enterprises

Bid Writing : The Basics 
TOPICS COVERED
Who are the winners and losers in grant funding. How to identify the weaknesses in your project. What questions will funders will ask themselves about your bid. Common reasons for applications being rejected. The key terms in bid writing explained with examples of each. Make your application short but effective. 
Start telling funders the things they really want to hear. How to build greater credibility in the eyes of funders. Demonstrating that the beneficiaries of your project are involved. The importance of getting your numbers and totals right. What to do with all your supporting documents. Make your proofreading foolproof.
ATTENDEES  
Staff members, volunteers, board members or trustees of charities, schools, associations or not for profit organisations who are about to submit grant funding applications to grant making trusts and foundations.
COST  
£95 including booking fees. Refreshments provided. Each attendee will receive a full set of notes and copies of eight real successful funding bids by e-mail after the workshop.
PAYMENT
All places must be booked using a debit or credit card through the online booking system. We do not issue invoices or accept bank or cheque payments. If you do not have a debit card from your organisation please use a personal one and claim reimbursement using the booking confirmation e-mail as proof of purchase.
BOOKING TERMS  
Workshop bookings are non cancellable, non refundable and non transferable between dates. If you are unable to attend on the date booked you may send someone else in your place.
QUESTIONS
Fully booked means fully booked. There are no waiting lists for people hoping for a cancellation. If you have a question please e-mail wor...@nf... and you will usually receive a response within 24 hours.

Bid Writing : Advanced 
TOPICS COVERED
Are you applying to the right trusts ? Are you looking for trusts in all the right places ? Are you applying to enough trusts ? Are you applying in the right ways ? Are your projects the most fundable projects ? How do you compare with your competitors for funding ? 
Are you carrying out trust fundraising in a professional way ? Do you understand what trusts are looking for ? Do you know how to turn your competitors into your ambassadors ? Is the rest of your fundraising hampering your bids to trusts ?  
ATTENDEES  
Staff members, volunteers, board members or trustees of charities, schools, associations or not for profit organisations who are about to submit grant funding applications to grant making trusts and foundations. 
It is assumed that you already know the basic bid writing skills of good preparation, eligibility checking, clear writing and adequate proof reading. If you do not you should attend The Basics workshop first. Around half of all attendees attend both The Basics and Advanced workshops on the same day but there is no discount for attending both.
COST  
£95 including booking fees. Refreshments provided. Each attendee will receive a full set of notes and copies of eight real successful funding bids by e-mail after the workshop.
PAYMENT
All places must be booked using a debit or credit card through the online booking system. We do not issue invoices or accept bank or cheque payments. If you do not have a debit card from your organisation please use a personal one and claim reimbursement using the booking confirmation e-mail as proof of purchase.
BOOKING TERMS  
Workshop bookings are non cancellable, non refundable and non transferable between dates. If you are unable to attend on the date booked you may send someone else in your place.
QUESTIONS  
Fully booked means fully booked. There are no waiting lists for people hoping for a cancellation. If you have a question please e-mail wor...@nf... and you will usually receive a response within 24 hours.
 London
Bid Writing : The Basics 30 Oct 2017Fully Booked
Bid Writing : Advanced30 Oct 2017Fully Booked
Bid Writing : The Basics 31 Oct 2017Fully Booked
Bid Writing : Advanced31 Oct 2017Last 5 Places
Bid Writing : The Basics 06 Nov 2017Fully Booked
Bid Writing : Advanced06 Nov 2017Fully Booked
Bid Writing : The Basics 04 Dec 2017Fully Booked
Bid Writing : Advanced04 Dec 2017Last 3 Places
Bid Writing : The Basics 15 Jan 2018Last 5 Places
Bid Writing : Advanced15 Jan 2018Booking Details
Bid Writing : The Basics 16 Jan 2018Last 9 Places
Bid Writing : Advanced16 Jan 2018Booking Details
Bristol
Bid Writing : The Basics 02 Nov 2017Fully Booked
Bid Writing : Advanced02 Nov 2017Fully Booked
Bid Writing : The Basics 05 Dec 2017Last 5 Places
Bid Writing : Advanced05 Dec 2017Last 6 Places
Bid Writing : The Basics 18 Jan 2018Booking Details
Bid Writing : Advanced18 Jan 2018Booking Details
Manchester
Bid Writing : The Basics 09 Nov 2017Fully Booked
Bid Writing : Advanced09 Nov 2017Fully Booked
Bid Writing : The Basics 06 Dec 2017Booking Details
Bid Writing : Advanced06 Dec 2017Last 5 Places
Bid Writing : The Basics 25 Jan 2018Booking Details
Bid Writing : Advanced25 Jan 2018Booking Details
Leeds
Bid Writing : The Basics 10 Nov 2017Last 3 Places
Bid Writing : Advanced10 Nov 2017Fully Booked
Bid Writing : The Basics 07 Dec 2017Last 10 Places
Bid Writing : Advanced07 Dec 2017Last 9 Places
Bid Writing : The Basics 26 Jan 2018Booking Details
Bid Writing : Advanced26 Jan 2018Booking Details
Edinburgh
Bid Writing : The Basics 25 Oct 2017Fully Booked
Bid Writing : Advanced25 Oct 2017Fully Booked
Bid Writing : The Basics 10 Jan 2018Booking Details
Bid Writing : Advanced10 Jan 2018Booking Details
Southampton
Bid Writing : The Basics 01 Nov 2017Last 2 Places
Bid Writing : Advanced01 Nov 2017Last 2 Places
Bid Writing : The Basics 17 Jan 2018Booking Details
Bid Writing : Advanced17 Jan 2018Booking Details
Nottingham
Bid Writing : The Basics 07 Nov 2017Last 3 Places
Bid Writing : Advanced07 Nov 2017Fully Booked
Bid Writing : The Basics 23 Jan 2018Booking Details
Bid Writing : Advanced23 Jan 2018Booking Details
Birmingham
Bid Writing : The Basics 08 Nov 2017Fully Booked
Bid Writing : Advanced08 Nov 2017Fully Booked
Bid Writing : The Basics 24 Jan 2018Booking Details
Bid Writing : Advanced24 Jan 2018Booking Details

What Past Attendees Have Said About Our Bid Writing Workshops
The workshop was excellent. I consider myself fairly experienced in bid writing and have been fairly successful. To your credit I learnt a lot from you which I will certainly put into practice.  I felt re-invigorated and encouraged. 
You definitely know your stuff. The course was certainly packed with information. Gave me plenty to think about and ways forward. I’m more used to courses where they pack half an hour into a full day!! 
For a person like me who writes lots of proposals it was exactly what I needed. Straight to the point, less "water", more sense and fantastic examples! The course was excellent. 
I picked up some great new ideas and tips. It’s hard to find good quality info these days re attracting funding – but on this occasion the juice was definitely worth the squeeze! 
I thought it was really useful training and you managed to fit a huge amount of information into 2.5 hours without it feeling too much to take in. Well done. Remarkably concise and useful. 
Plenty of useful do's and don'ts. Having attended dozens of training courses over the years, it was a very pleasant surprise not to have my time wasted with pointless break out groups, workshop exercises or unrelated show and tell experiences.  
I really enjoyed the workshop yesterday. I thought the pace and delivery was excellent and it has really given me the confidence to move forward. Thank you so much – definitely money well spent. I will now be more time-efficient 
Did just what it said on the tin. I thought the workshop was very informative. It was an interesting couple of hours, style delivery was to the point and no fussy power point’s to contend with.
We learned a great deal from your courses. I liked your engagement with the subject and your personal anecdotes. The course material overall was truly inspiring! Put things into perspective for us.
I did like your matter of fact approach I thought that your presentations were really excellent and will, I know, prove extremely useful in the coming months.
I feel much better prepared and have a much longer to do list now! A brilliant workshop. 
I shall recommend your workshop others. The pace, delivery and content was tremendously helpful and informative.  
I thought you as a trainer were friendly and relaxed, easy to be with and kept us engaged and you made learning interesting. Thoroughly enjoyed your insights and anecdotes. 
It was great and great value for money also. I thought that learning in a small group was really good and meant that we were able to communicate with you a lot easier. 
Thank you so much for your professionalism, sense of humour and all the knowledge you kindly shared with us. I now realise I have been emphasising many of the wrong angles. 
Informative, to the point and engaging.I just want to thank you for a most informative session. I certainly picked up some great ideas and hints to enhance my future bid applications.
I found it very informative I feel a lot more confidant about the process of bid writing.  I would certainly recommend your course to others.

Sign Up For Your Own Copy 
If you are reading a mailer sent to a colleague and wish to receive your own copy in future please e-mail si...@nf... quoting your email address in the subject line.
Unsubscribe From Our Mailing List 
CLICK TO REMOVE YOUR E-MAIL ADDRESS FROM OUR MAILING LIST
Alternatively send a blank e-mail to uns...@nf... quoting the email address we are sending to i.e. hol...@li... in the subject line in lower case letters. Our automated system will remove all email addresses in the subject line from our mailing lists within 7 days. If you leave the subject line blank, use capital letters, type a person's name, unsubscribe or anything else then nothing will be removed from our lists. Any text within the body of the email will not be read.  
NFP Workshops, Blake House, 18 Blake Street, York YO1 8QH    01133 280988

ZEy1Kd

Hi Peter,

This email came when I was on holidays, and I didn't reply when catching 
up immediately on my return, because I wanted to study what you had done 
- and I'm sorry to say I haven't that (yet).  So I'll at least give a 
brief comment:

a couple of quick-and-dirty additions to HOL (which I'm afraid is rather 
my style) seem to roughly do what you describe :

eg  VALIDATE (CONV_TAC (DEPTH_CONV (REWR_CONV_A (
     UNDISCH (SPEC_ALL RAT_RDIV_EQ)))))

will rewrite using the consequent of ratTheory.RAT_RDIV_EQ and leave the 
relevant instantiated antecedents to be proven as additional subgoals.

This required REWR_CONV_A which uses PART_MATCH_A (_A stands for 
assumptions) which will allow substitution for variables which appear in 
the assumptions), and VALIDATE, which, where a tactic is invalid on 
account of the validation returned by the tactic proving a theorem with 
"extra" assumptions, will return additional subgoals to prove those 
extra assumptions.

Cheers,

Jeremy

On 02/06/16 21:41, Peter Vincent Homeier wrote:
> Perhaps it might help if I shared a bit more about dependent rewriting,
> and its purpose.
>
> The basic idea of dependent rewriting is that it is more assertive.
> Suppose we have proven a useful lemma of the form
>
> LEMMA:
> |- !x y z. ant1 /\ ant2 /\ ant3 ==> (lhs = rhs)
>
> and suppose we are facing a goal which contains an instance of lhs. If
> there were no antecedents in LEMMA, we could simply rewrite with LEMMA
> using REWRITE_TAC, etc. If the antecedents were all present in the
> hypotheses of the goal, perhaps IMP_RES_TAC would create a new
> hypothesis which is the specialized equality
>
> lhs[a,b,c/x,y,z] = rhs[a,b,c/x,y,z]
>
> and we could then do ASM_REWRITE_TAC (assuming no other hypotheses got
> in the way and confused things).
>
> Unfortunately, this approach is weak. IMP_RES_TAC is famous for spinning
> off and creating dozens or hundreds of new hypotheses, most of which are
> completely irrelevant to the proof. What a mess. (Actually, in this
> case, perhaps the simplifier would be the way to go.)
>
> But more likely, not all of the necessary instances of the antecedents
> are already present in the hypotheses, just sitting there ready to be
> used. Then one might proceed by doing other tactics to produce the
> missing necessary antecedents, and gradually work up to the point of
> being able to apply IMP_RES_TAC. But while valid, this feels
> distracting, that we are moving our attention away from the goal to a
> set of new subgoals, while still having to remember to finish up our
> main goal.
>
> So dependent rewriting basically says, I want you, HOL theorem prover,
> to do the rewrite lhs = rhs, suitably instantiated for this goal, and
> don't force me to justify the antecedents first. I'll get to those
> later, but for now, just do the rewriting that I am telling you to do.
> Afterwards, I'll deal with those antecedents appropriately.
>
> This is the sense in which dependent rewriting is more assertive. Using
> dependent rewriting contains an inherent promise that you will discharge
> the antecedents later. This means that it is also an assertion that you
> know what you are doing, and that this implication LEMMA is the right
> thing to do at this point in the proof. It is a choice that if wrong,
> can change a provable goal into an unprovable goal, in exactly the same
> way that MATCH_MP_TAC can.
>
> But when dependent rewriting is used appropriately, with theorems that
> actually do apply to the goal, it serves to clean up the task of
> reasoning with theorems that have antecedents, treating them as side
> conditions to be handled on the side, and changing the feel to one that
> is more comfortable, closer to the familiar REWRITE_TAC.
>
> Peter
>
>
> On Wed, Jun 1, 2016 at 7:30 PM, Ramana Kumar <Ram...@cl...
> <mailto:Ram...@cl...>> wrote:
>
>     I started creating .doc files for the dependent rewrite tactics by
>     copying from Peter's documentation in the signature file. (Thank you
>     Peter! I think they are documented well there. The automated
>     documentation-generating system in HOL requires these .doc files
>     though.)
>
>     This was the commit:
>     https://github.com/HOL-Theorem-Prover/HOL/commit/bfc04058b2f9f52233b56be40bd941f7effd22e3
>
>     I created SEEALSO entries for some entry-points which I did not
>     document yet, so I didn't consider this "done" yet. But I think it's
>     mostly done, and I'd be happy if someone else wanted to do the rest,
>     or if we just considered this enough for opening the structure in
>     bossLib.
>
>     (By the way, it's a pity implicational rewriting tactics haven't
>     gone much further
>     (https://github.com/HOL-Theorem-Prover/HOL/issues/160).)
>
>     On 1 June 2016 at 05:27, Konrad Slind <kon...@gm...
>     <mailto:kon...@gm...>> wrote:
>
>         One way to proceed would be to construct a LaTex-ed version of
>         the above, with a
>         few examples sprinkled in, and add it to the Description, somewhere
>         after the section on the simplifier. After that, you could
>         easily add a collection
>         of .doc files for the entrypoints that point to the DESCRIPTION.
>
>         Konrad.
>
>
>         On Tue, May 31, 2016 at 11:02 AM, Peter Vincent Homeier
>         <pal...@tr...
>         <mailto:pal...@tr...>> wrote:
>
>             The dependent rewriting tactics are documented, as much as
>             they are, in comments at the beginning of dep_rewrite.sig.
>             These comments are copied below.
>
>             The tactics are meant to be deft, quick, and light-weight,
>             and to make proofs more robust under normal proof evolution,
>             by reducing the number of explicit terms that are needed in
>             the tactic. These are much less sophisticated tools than the
>             HOL simplifier, but may be easier to control when one just
>             wants to apply a particular implication theorem to an
>             assumption and the goal.
>
>             Perhaps the text below could be adapted into a better form
>             of documentation. What would people like?
>
>             Peter
>
>             (*
>             ==================================================================
>             *)
>             (*
>             ==================================================================
>             *)
>             (*                     DEPENDENT REWRITING TACTICS
>                      *)
>             (*
>             ==================================================================
>             *)
>             (*
>             ==================================================================
>             *)
>             (*
>                      *)
>             (* This file contains new tactics for dependent rewriting,
>                      *)
>             (* a generalization of the rewriting tactics of standard
>             HOL.         *)
>             (*
>                      *)
>             (* The main tactics are named DEP_REWRITE_TAC[thm1,...],
>             etc., with   *)
>             (* the standard variations (PURE,ONCE,ASM).  In addition,
>             tactics     *)
>             (* with LIST instead of ONCE are provided, making 12 tactics
>             in all.  *)
>             (*
>                      *)
>             (* The argument theorems thm1,... are typically
>             implications.         *)
>             (* These tactics identify the consequents of the argument
>             theorems,   *)
>             (* and attempt to match these against the current goal.  If
>             a match   *)
>             (* is found, the goal is rewritten according to the matched
>             instance  *)
>             (* of the consequent, after which the corresponding
>             hypotheses of     *)
>             (* the argument theorems are added to the goal as new
>             conjuncts on    *)
>             (* the left.
>                      *)
>             (*
>                      *)
>             (* Care needs to be taken that the implications will match
>             the goal   *)
>             (* properly, that is, instances where the hypotheses in fact
>             can be   *)
>             (* proven.  Also, even more commonly than with REWRITE_TAC,
>                       *)
>             (* the rewriting process may diverge.
>                       *)
>             (*
>                      *)
>             (* Each implication theorem for rewriting may have a number
>             of layers *)
>             (* of universal quantification and implications.  At the
>             bottom of    *)
>             (* these layers is the base, which will either be an
>             equality, a      *)
>             (* negation, or a general term.  The pattern for matching
>             will be     *)
>             (* the left-hand-side of an equality, the term negated of a
>             negation, *)
>             (* or the term itself in the third case.  The search is
>             top-to-bottom,*)
>             (* left-to-right, depending on the quantifications of
>             variables.      *)
>             (*
>                      *)
>             (* To assist in focusing the matching to useful cases, the
>             goal is    *)
>             (* searched for a subterm matching the pattern.  The
>             matching of the  *)
>             (* pattern to subterms is performed by higher-order
>             matching, so for  *)
>             (* example, ``!x. P x`` will match the term ``!n. (n+m) <
>             4*n``.      *)
>             (*
>                      *)
>             (* The argument theorems may each be either an implication
>             or not.    *)
>             (* For those which are implications, the hypotheses of the
>             instance   *)
>             (* of each theorem which matched the goal are added to the
>             goal as    *)
>             (* conjuncts on the left side.  For those argument theorems
>             which     *)
>             (* are not implications, the goal is simply rewritten with
>             them.      *)
>             (* This rewriting is also higher order.
>                       *)
>             (*
>                      *)
>             (* Deep inner universal quantifications of consequents are
>             supported. *)
>             (* Thus, an argument theorem like EQ_LIST:
>                      *)
>             (* |- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==>
>                      *)
>             (*                  (CONS h1 l1 = CONS h2 l2))
>                      *)
>             (* before it is used, is internally converted to appear as
>                      *)
>             (* |- !h1 h2 l1 l2. (h1 = h2) /\ (l1 = l2) ==>
>                      *)
>             (*                  (CONS h1 l1 = CONS h2 l2)
>                       *)
>             (*
>                      *)
>             (* As much as possible, the newly added hypotheses are
>             analyzed to    *)
>             (* remove duplicates; thus, several theorems with the same
>                      *)
>             (* hypothesis, or several uses of the same theorem, will
>             generate     *)
>             (* a minimal additional proof burden.
>                       *)
>             (*
>                      *)
>             (* The new hypotheses are added as conjuncts rather than as
>             a         *)
>             (* separate subgoal to reduce the user's burden of subgoal
>             splits     *)
>             (* when creating tactics to prove theorems.  If a separate
>             subgoal    *)
>             (* is desired, simply use CONJ_TAC after the dependent
>             rewriting to   *)
>             (* split the goal into two, where the first contains the
>             hypotheses   *)
>             (* and the second contains the rewritten version of the
>             original      *)
>             (* goal.
>                      *)
>             (*
>                      *)
>             (* The tactics including PURE in their name will only use
>             the         *)
>             (* listed theorems for all rewriting; otherwise, the
>             standard         *)
>             (* rewrites are used for normal rewriting, but they are not
>                       *)
>             (* considered for dependent rewriting.
>                      *)
>             (*
>                      *)
>             (* The tactics including ONCE in their name attempt to use
>             each       *)
>             (* theorem in the list, only once, in order, left to right.
>                       *)
>             (* The hypotheses added in the process of dependent
>             rewriting are     *)
>             (* not rewritten by the ONCE tactics.  This gives a more
>             restrained   *)
>             (* version of dependent rewriting.
>                      *)
>             (*
>                      *)
>             (* The tactics with LIST take a list of lists of theorems,
>             and        *)
>             (* uses each list of theorems once in order, left-to-right.
>             For      *)
>             (* each list of theorems, the goal is rewritten as much as
>             possible,  *)
>             (* until no further changes can be achieved in the goal.
>             Hypotheses  *)
>             (* are collected from all rewriting and added to the goal,
>             but they   *)
>             (* are not themselves rewritten.
>                      *)
>             (*
>                      *)
>             (* The tactics without ONCE or LIST attempt to reuse all
>             theorems     *)
>             (* repeatedly, continuing to rewrite until no changes can be
>                      *)
>             (* achieved in the goal.  Hypotheses are rewritten as well,
>             and       *)
>             (* their hypotheses as well, ad infinitum.
>                      *)
>             (*
>                      *)
>             (* The tactics with ASM in their name add the assumption
>             list to      *)
>             (* the list of theorems used for dependent rewriting.
>                       *)
>             (*
>                      *)
>             (* There are also three more general tactics provided,
>                      *)
>             (* DEP_FIND_THEN, DEP_ONCE_FIND_THEN, and
>             DEP_LIST_FIND_THEN,         *)
>             (* from which the others are constructed.
>                       *)
>             (*
>                      *)
>             (* The differences among these is that DEP_ONCE_FIND_THEN
>             uses        *)
>             (* each of its theorems only once, in order left-to-right as
>             given,   *)
>             (* whereas DEP_FIND_THEN continues to reuse its theorems
>             repeatedly   *)
>             (* as long as forward progress and change is possible.  In
>             contrast   *)
>             (* to the others, DEP_LIST_FIND_THEN takes as its argument a
>             list     *)
>             (* of lists of theorems, and processes these in order,
>             left-to-right. *)
>             (* For each list of theorems, the goal is rewritten as many
>             times     *)
>             (* as they apply.  The hypotheses for all these rewritings
>             are        *)
>             (* collected into one set, added to the goal after all
>             rewritings.    *)
>             (*
>                      *)
>             (* DEP_ONCE_FIND_THEN and DEP_LIST_FIND_THEN will not attack
>             the      *)
>             (* hypotheses generated as a byproduct of the dependent
>             rewriting;    *)
>             (* in contrast, DEP_FIND_THEN will.  DEP_ONCE_FIND_THEN and
>                       *)
>             (* DEP_LIST_FIND_THEN might be fruitfully applied again to
>             their      *)
>             (* results; DEP_FIND_THEN will complete any possible
>             rewriting,       *)
>             (* and need not be reapplied.
>                       *)
>             (*
>                      *)
>             (* These take as argument a thm_tactic, a function which
>             takes a      *)
>             (* theorem and yields a tactic.  It is this which is used to
>             apply    *)
>             (* the instantiated consequent of each successfully matched
>                       *)
>             (* implication to the current goal.  Usually this is
>             something like   *)
>             (* (fn th => REWRITE_TAC[th]), but the user is free to
>             supply any     *)
>             (* thm_tactic he wishes.
>                      *)
>             (*
>                      *)
>             (* One significant note: because of the strategy of adding
>             new        *)
>             (* hypotheses as conjuncts to the current goal, it is not
>             fruitful    *)
>             (* to add *any* new assumptions to the current goal, as one
>             might     *)
>             (* think would happen from using, say, ASSUME_TAC.
>                      *)
>             (*
>                      *)
>             (* Rather, any such new assumptions introduced by thm_tactic
>             are      *)
>             (* specifically removed.  Instead, one might wish to try
>             MP_TAC,      *)
>             (* which will have the effect of ASSUME_TAC and then
>             undischarging    *)
>             (* that assumption to become an antecedent of the goal.
>             Other        *)
>             (* thm_tactics may be used, and they may even convert the
>             single      *)
>             (* current subgoal into multiple subgoals.  If this happens,
>             it is    *)
>             (* fine, but note that the control strategy of DEP_FIND_THEN
>             will     *)
>             (* continue to attack only the first of the multiple
>             subgoals.        *)
>             (*
>                      *)
>             (*
>             ==================================================================
>             *)
>             (*
>             ==================================================================
>             *)
>
>
>
>             On Mon, Feb 22, 2016 at 1:00 AM, Michael Norrish
>             <Mic...@ni...
>             <mailto:Mic...@ni...>> wrote:
>
>                 If it's going to that "public", it would be nice if the
>                 main entry-points were documented.
>
>                 Michael
>
>                 > On 22 Feb 2016, at 16:21, Ramana Kumar
>                 <Ram...@cl...
>                 <mailto:Ram...@cl...>> wrote:
>                 >
>                 > What needs to be documented? I think I just meant put
>                 an "open
>                 > dep_rewrite" into bossLib.
>                 >
>                 > On 22 February 2016 at 11:19, Michael Norrish
>                 > <Mic...@ni...
>                 <mailto:Mic...@ni...>> wrote:
>                 >> Please document somewhere, but yes.
>                 >>
>                 >> Michael
>                 >>
>                 >>> On 22 Feb 2016, at 09:24, Ramana Kumar
>                 <Ram...@cl...
>                 <mailto:Ram...@cl...>> wrote:
>                 >>>
>                 >>> So, yes?
>                 >>>
>                 >>> On 2 February 2016 at 15:51, Ramana Kumar
>                 <Ram...@cl...
>                 <mailto:Ram...@cl...>> wrote:
>                 >>>> On 2 February 2016 at 15:04, Michael Norrish
>                 <Mic...@ni...
>                 <mailto:Mic...@ni...>>
>                 >>>> wrote:
>                 >>>>>
>                 >>>>> Don't know.
>                 >>>>>
>                 >>>>> Is it clearly adding functionality we don't have
>                 any other way?
>                 >>>>
>                 >>>>
>                 >>>> Yes, I think so. The other way to get the
>                 functionality is cumbersome:
>                 >>>> abbreviate lots of your goal and try to instantiate
>                 the dependent rewrite
>                 >>>> theorem manually.
>                 >>>>
>                 >>>>>
>                 >>>>>
>                 >>>>> Is it big (makes a difference to Moscow ML); does
>                 it contaminate the
>                 >>>>> environment at all (declares new constants;
>                 adjusts grammars; adjusts other
>                 >>>>> global elements of the system)?
>                 >>>>
>                 >>>>
>                 >>>> It doesn't touch the logical environment, and I
>                 don't think it's very big.
>                 >>>>
>                 >>>> Implicational rewriting (issue #160) would be
>                 better, but we don't have
>                 >>>> that.
>                 >>>>
>                 >>>>>
>                 >>>>>
>                 >>>>> Michael
>                 >>>>>
>                 >>>>> On 2 Feb 2016, at 12:17, Ramana Kumar
>                 <Ram...@cl...
>                 <mailto:Ram...@cl...>> wrote:
>                 >>>>>
>                 >>>>> Tap tap tap... is this thing on?
>                 >>>>>
>                 >>>>> On 22 January 2016 at 17:56, Ramana Kumar
>                 <Ram...@cl...
>                 <mailto:Ram...@cl...>>
>                 >>>>> wrote:
>                 >>>>>>
>                 >>>>>> Would there be any harm in adding dep_rewrite to
>                 the standard set of
>                 >>>>>> libraries that are loaded by default? (Similarly
>                 to how quantHeuristicsLib
>                 >>>>>> was added some time recently.)
>                 >>>>>
>                 >>>>>
>                 >>>>>
>                 >>>>>
>                 ------------------------------------------------------------------------------
>                 >>>>> Site24x7 APM Insight: Get Deep Visibility into
>                 Application Performance
>                 >>>>> APM + Mobile APM + RUM: Monitor 3 App instances at
>                 just $35/Month
>                 >>>>> Monitor end-to-end web transactions and take
>                 corrective actions now
>                 >>>>> Troubleshoot faster and improve end-user
>                 experience. Signup Now!
>                 >>>>>
>                 >>>>>
>                 http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140_______________________________________________
>                 >>>>> Hol-developers mailing list
>                 >>>>> Hol...@li...
>                 <mailto:Hol...@li...>
>                 >>>>>
>                 https://lists.sourceforge.net/lists/listinfo/hol-developers
>                 >>>>>
>                 >>>>>
>                 >>>>>
>                 >>>>> ________________________________
>                 >>>>>
>                 >>>>> The information in this e-mail may be confidential
>                 and subject to legal
>                 >>>>> professional privilege and/or copyright. National
>                 ICT Australia Limited
>                 >>>>> accepts no liability for any damage caused by this
>                 email or its attachments.
>                 >>>>
>                 >>>>
>                 >>
>                 >>
>                 >> ________________________________
>                 >>
>                 >> The information in this e-mail may be confidential
>                 and subject to legal professional privilege and/or
>                 copyright. National ICT Australia Limited accepts no
>                 liability for any damage caused by this email or its
>                 attachments.
>                 >>
>                 >>
>                 ------------------------------------------------------------------------------
>                 >> Site24x7 APM Insight: Get Deep Visibility into
>                 Application Performance
>                 >> APM + Mobile APM + RUM: Monitor 3 App instances at
>                 just $35/Month
>                 >> Monitor end-to-end web transactions and take
>                 corrective actions now
>                 >> Troubleshoot faster and improve end-user experience.
>                 Signup Now!
>                 >>
>                 http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
>                 >> _______________________________________________
>                 >> hol-info mailing list
>                 >> hol...@li...
>                 <mailto:hol...@li...>
>                 >> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>                 ------------------------------------------------------------------------------
>                 Site24x7 APM Insight: Get Deep Visibility into
>                 Application Performance
>                 APM + Mobile APM + RUM: Monitor 3 App instances at just
>                 $35/Month
>                 Monitor end-to-end web transactions and take corrective
>                 actions now
>                 Troubleshoot faster and improve end-user experience.
>                 Signup Now!
>                 http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
>                 _______________________________________________
>                 Hol-developers mailing list
>                 Hol...@li...
>                 <mailto:Hol...@li...>
>                 https://lists.sourceforge.net/lists/listinfo/hol-developers
>
>
>
>
>             --
>
>
>             "In Your majesty ride prosperously
>             because of truth, humility, and righteousness;
>             and Your right hand shall teach You awesome things." (Psalm
>             45:4)
>
>             ------------------------------------------------------------------------------
>             What NetFlow Analyzer can do for you? Monitors network
>             bandwidth and traffic
>             patterns at an interface-level. Reveals which users, apps,
>             and protocols are
>             consuming the most bandwidth. Provides multi-vendor support
>             for NetFlow,
>             J-Flow, sFlow and other flows. Make informed decisions using
>             capacity
>             planning reports.
>             https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
>             _______________________________________________
>             Hol-developers mailing list
>             Hol...@li...
>             <mailto:Hol...@li...>
>             https://lists.sourceforge.net/lists/listinfo/hol-developers
>
>
>
>
>
>
> --
>
>
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
>
>
> ------------------------------------------------------------------------------
> What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
> patterns at an interface-level. Reveals which users, apps, and protocols are
> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
> J-Flow, sFlow and other flows. Make informed decisions using capacity
> planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
>
>
>
> _______________________________________________
> Hol-developers mailing list
> Hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-developers
>

The tweaks to the interaction manual shouldn’t particularly be on pr398; apologies.

Michael

My proposal using constant definitions would not work if the metavar
instantiations contain free variables.
One way to recover is to add the free variables as arguments to the
constant.

I think in your example, there is no problem, because you never have a
lifted tactic followed by an evars-tactic that instantiates metavars that
the lifted tactic can see.

However, I think Magnus's suggestion (change the tactic type in HOL to
support evars) is more worth exploring than my suggestion based on defining
constants and re-running lifted tactics inside their validation (which is
rather slow/ugly).

On 1 September 2016 at 02:28, Armaël Guéneau <arm...@en...>
wrote:

> > >     This discussion should probably move to the HOL mailing lists,
> >     even though most active HOL developers are also on the CakeML dev
> >     list. > > I agree. Therefore, I am replying to the HOL dev mailing
> list. See the initial thread copied below. > > I have a suggestion for
> defining lift, following your approach that re-runs the tactic in the
> validation. > How about introducing intermediate terms for the
> specialisation, to avoid the tactic doing too much? > Thus, I suggest
> something like: > > fun lift tac metavars g = >   let >     val (gls, _) =
> tac g >     fun validation inst thl = >       let >         val
> (inst1,defs) = fresh_evars metavars inst >         val thl1 = uninst_thms
> gls defs thl >         val g1 = inst_goal inst1 g >       in >         snd
> (tac g1) thl1 >       end >   in (gls, validation) end > > Given an
> instantiation inst which takes metavars x and y to 2 and 3, I suggest
> fresh_evars introduce new constants representing the instantiated evars, Cx
> and Cy, and returns inst1 = [x|->Cx, y|->Cy] and defs = [|- Cx = 2, |- Cy =
> 3]. > > Then, uninst_thms looks for places in the proved subgoals where a
> metavar has been instantiated, and uses the defs to replace the
> instantiation with the new constant. So if you had |- 2 = 2 in thl, but the
> original subgoal was ?- x = 2, then the new thl1 becomes |- Cx = 2, by
> rewriting the lhs with SYM (el 1 defs). > > I'm not sure if this is
> possible to achieve without definitions of new constants. You could
> possibly do it with fresh variables, but you may need to carry around the
> defs as assumptions in that case. The advantage of constants is that their
> definitions can be kept around in separate theorems. But you probably want
> to delete them afterwards, and it's quite heavyweight.
>
> I don't know much about the constant definition system, but how would that
> work if the metavariable is instantiated by a free variable (at that time)?
> More precisely, how would the following "proof with evars" work:
>
> g `!x. ?y. x = y`
> e (lift gen_tac \\ meta_exists \\ meta_inst1 `y` `x` \\ lift (fs []))
>
> (where meta_exists turns a goal of the form `?y. P` into `P` where `y`
> became a metavariable; and meta_inst1 instantiates a metavariable). `y` as
> a metavariable is instantiated with `x`, a free variable that then gets
> generalized by gen_tac. Do you think that would work with the method you
> suggest?
>
> — Armaël
>
> > By the way I also want to note that Isabelle/HOL has schematic variables
> for these metavars. So Coq has evars, Isabelle has schematic vars, ... are
> we about to join that club? It would be really nice to find a lighter
> weight way of achieving this. > > > On 21 August 2016 at 07:51, Konrad
> Slind <kon...@gm...> <kon...@gm...> wrote: > >
> Datapoint: years ago, John Harrison spent some time implementing >
> meta-variables for HOL Light. Not sure if this was inside the kernel, or
> just >     on top. (The latter, I think, which means that he had to deal
> with the same >     issues as being discussed here.) > >     He dropped the
> effort on the grounds that the code was becoming too complex >     for his
> goals in HOL Light, e.g., simplicity.  But there is no doubt more to >
> the story and you should go to the source (have cc'ed John). > >
> Cheers, >     Konrad. > > > >     On Sat, Aug 20, 2016 at 12:09 PM, Magnus
> Myreen <mag...@gm...> <mag...@gm...> wrote: >
> >         Hi Armaël and dev, > >         Thanks for the clear explanation.
> > >         > 2) Implement metavariables in HOL. >         > >         >
> Provided that they work nicely, they would have the advantage of producing
> nicer >         > goals. [...] > >         I prefer option (2) because it
> seems like the right thing to do for >         the long term. > >         >
> Implementing metavars requires defining a custom proof manager, and (among
> >         > others) an alternative [Evars.tactic] type, for tactics that
> know about >         > metavariables, and that can instantiate them. >
> >         Having two proof managers sounds like a mess. > >         Would
> it be possible to change the tactic type in HOL to support evars? >
> >         I know such a change could potentially cause an enormous amount
> of >         breakage. However, as far as I know, most tactic
> implementations are >         written as compositions of very low-level
> tactics. If the breakage >         would mostly be limited to simple
> adjustments to the very lowest level >         tactics, then maybe there is
> a chance to change the tactic type to >         allow evars. I'm thinking
> that we might be able to get things working >         as they were before
> for all proofs that do not use metavariables, and >         then one could
> gradually make match_mp_tac etc. smarter in cases where >         evars are
> present. > >         I'm keen to hear what Michael and the other HOL
> developers think of >         this. This discussion should probably move to
> the HOL mailing lists, >         even though most active HOL developers are
> also on the CakeML dev >         list. > >         Cheers, >         Magnus
> > > >         On 20 August 2016 at 16:15, Armaël Guéneau
> <arm...@en...> <arm...@en...> wrote:
> >         > >         > Hi dev, >         > >         > I appear to be
> half-stuck/indecise on the question of how to get the proper >         >
> tactics to deal with CFs for let. So I thought I'd ask for advices.
> >         > >         > Currently, when dealing with the CF for [let val x
> = e1 in e2 end], one has to >         > provide manually beforehand the
> postcondition for evaluating [e1]. This is not >         > ideal, and can
> be avoided. In particular, in CFML it is not required. >         >
> >         > The goal corresponding to a CF for [let val x = e1 in e2 end]
> is of the form: >         > >         >   cf_let x (cf e1) (cf e2) env H Q
> >         > >         > After some unfolding, it becomes: >         >
> >         >   ?Q'. >         >     (cf e1) env H Q' /\ >         >     !xv.
> (cf e2) ((x, xv)::env) (Q' xv) Q >         > >         > Now, 99% of the
> time, you do not want to give an instantiation for Q' right >         >
> away: H being known, proving the first subgoal [(cf e1) env H Q'] will in
> fact >         > end up providing an instantiation for Q'. >         >
> >         > CFML deals with that by using the "metavariables" mechanism of
> Coq (or "evars"), >         > which allows instantiating an exists by a
> metavariable, which will be actually >         > instantiated later in the
> proof. >         > >         > If _Q' is the metavariable for Q', then the
> goal becomes >         > >         >   (cf e1) env H _Q' /\ >         >
> !xv. (cf e2) ((x, xv)::env) (_Q' xv) Q >         > >         > It is then
> easy to split it, prove the first subgoal, which will instantiate _Q'
> >         > to the real thing, and then the proof can continue with
> >         > [!xv. (cf e2) ((x, xv)::env) (Q'' xv) Q] for some Q''.
> >         > >         > >         > For CFs in CakeML, as HOL doesn't
> currently have such a feature, I experimented >         > with two options:
> >         > >         > 1) Implement a small library of composable
> "rewrites", à la conseqConv, that >         > would apply under existential
> quantifications, and that would be able to >         > instantiate them.
> >         > >         > With a goal of the form >         > >         >
> ?Q'. >         >     X /\ >         >     Y >         > >         > the CF
> tactics would do some work on X, hopefully eventually instantiating Q',
> >         > such that the goal would reduce to Y[Q''/Q']. >         >
> >         > Now, in full generality, these composable rewrites need not
> only to apply under >         > exists, but under a succession of exists
> and forall, which spices things up a >         > bit. >         > >
> > For example, consider a program of the form: >         > >         >
> let val x = >         >     let val y = e1 >         >     in e2 end
> >         >   in e3 end >         > >         > The corresponding goal is
> of the form (for some env, H, Q): >         > >         >   cf_let x
> >         >     (cf_let y (cf e1) (cf e2)) >         >     (cf e3)
> >         > >         > and after some unfolding: >         > >         >
> ?Q' Q''. >         >     ((cf e1) env H Q'' /\ >         >      !yv. (cf
> e2) ((y, yv)::env) (Q'' yv) Q') /\ >         >     !xv. (cf e3) ((x,
> xv)::env) (Q' xv) Q >         > >         > After doing work on [(cf e1)
> env H Q''], Q'' usually gets instantiated, and the >         > goal
> becomes: >         > >         >   ?Q'. >         >     (!yv. (cf e2) ((y,
> yv)::env) (Q'' yv) Q') /\ >         >     !xv. (cf e3) ((x, xv)::env) (Q'
> xv) Q >         > >         > We want to do work on [(cf e2) ((y, yv)::env)
> (Q'' yv) Q'], and hopefully >         > instantiate Q'. >         >
> >         > -------/ end of the example /--------- >         > >         >
> For the moment (and with the help of Thomas Tuerk), I have a small library
> of >         > conseqConv+instantiations that only work under toplevel
> exists, and allow to >         > instantiate them. >         > >         >
> I think I can extend it to handle nestings of forall and exists. My
> concerns are >         > that: >         > >         > - Although they
> appear only when nesting lets (which I guess is not so common >         >
> but can definitely happen), these goals with nested exists and forall may
> look >         >   scary and annoying to manipulate for the user. >
> > >         > - In non-trivial program proofs, CF-specific tactics should
> clearly make less >         >   than half of the proof. Most of the work
> would be proving invariants of the >         >   specific program that is
> being certified. >         > >         >   Then, would that mean the user
> would also have to use complex proof machinery >         >   to deal with
> this goals, where the current "subgoal" is under several exists >
> >   and forall?  Maybe it's not too bad, but it's definitely an additionnal
> >         >   difficulty to be taken into account. >         > >         >
> >         > 2) Implement metavariables in HOL. >         > >         >
> Provided that they work nicely, they would have the advantage of producing
> nicer >         > goals. The intuition is that they allow to strip the
> exists and forall from the >         > goal altogether, and then check that
> metavariables are not instantiated using >         > foralls that have been
> introduced after them. >         > And with the way the CF tactics are
> designed, this kind of illegal >         > instantiations will likely never
> be an issue, or appear to the user. >         > >         > Implementing
> metavars requires defining a custom proof manager, and (among >         >
> others) an alternative [Evars.tactic] type, for tactics that know about
> >         > metavariables, and that can instantiate them. >         >
> >         > I implemented that, although it's hardly tested and probably
> buggued, + some >         > features are missing. >         > >         >
> However, the main issue is as follows: there needs to be a "lift" function,
> of >         > type [Abbrev.tactic -> Evars.tactic]. This is such that
> users can use their >         > everyday tactics when arriving to the bulk
> of the proof. And also such that not >         > every tactic in the world
> needs to be reimplemented "with evars". >         > >         > The way the
> proofmanager with evars works is as follows: >         > >         > -
> metavariables (evars) are free variables of the goal >         > - an
> Evars.tactic is called with the goal, and the list of free variables that
> >         >   are metavariables >         > - the Evars.tactic produces
> subgoals >         > - the theorems that the validation function receives
> prove the subgoals, *except >         >   that some metavariables may have
> been instantiated*. >         > >         > This last point is problematic
> for lifting standard tactics. These do not expect >         > to receive
> theorems for the validation function that do not directly prove the
> >         > subgoals. >         > >         > Therefore, the naive
> implementation of lift does not work: >         > >         >   fun lift
> tac metavars g = >         >     tac g >         > >         > For example,
> [MATCH_MP_TAC (|- P x ==> Q x)] produces a ``P x`` subgoal, and a >
> > validation function that expects (|- P x) as input. If given (|- P 3),
> the >         > validation function will of course fail, and not produce
> (|- Q 3). >         > >         > I do not know if it's possible to define
> lift in a way that works around this >         > problem. >         >
> >         > I thought of re-running the tactic entirely in the validation
> function, but this >         > does not work as the tactic may perform too
> much work on the specialized goal. >         > >         >   fun lift tac
> metavars g = >         >     let >         >       val (gls, _) = tac g
> >         >       fun validation inst thl = >         >         snd (tac
> (inst_goal inst g)) thl >         >     in (gls, validation) end >
> > >         > For example, EVAL_TAC on [x = 2] produces the subgoal [x =
> 2], so even if x is a >         > metavariable that is specialized to 2
> afterwards, lifted EVAL_TAC should produce >         > the subgoal [2 = 2].
> Re-runing EVAL_TAC in the lift's validation on [2 = 2] will >         >
> produce a validation function that solves the goal instead. >         >
> >         > One idea would be to extend the common HOL tactics so that they
> handle this >         > situation. I don't know what amount of work this
> represent, in order to cover >         > most of the everyday tactics. Or
> whether it is possible to be implemented >         > without too much
> overhead (as this may mean re-running some parts of the tactic >         >
> in the validation function, if the input theorems only prove a
> specialization of >         > the subgoals). Or whether this is a change
> that is even remotely likely to get >         > merged... >         >
> >         > >         > Thoughts? >         > Sorry for the wall of text.
> >         > >         > — Armaël >         > >         > >         >
> _______________________________________________ >         > Dev mailing
> list >         > De...@ca... >         > https://lists.cakeml.org/
> listinfo/dev > >         _______________________________________________
> >         Dev mailing list >         De...@ca... >
> https://lists.cakeml.org/listinfo/dev > > > >
> _______________________________________________ >     Dev mailing list
> >     De...@ca... >     https://lists.cakeml.org/listinfo/dev > >
>
>

> >     This discussion should probably move to the HOL mailing lists, >     even though most active HOL developers are also on the CakeML dev >     list. > > I agree. Therefore, I am replying to the HOL dev mailing list. See the initial thread copied below. > > I have a suggestion for defining lift, following your approach that re-runs the tactic in the validation. > How about introducing intermediate terms for the specialisation, to avoid the tactic doing too much? > Thus, I suggest something like: > > fun lift tac metavars g = >   let >     val (gls, _) = tac g >     fun validation inst thl = >       let >         val (inst1,defs) = fresh_evars metavars inst >         val thl1 = uninst_thms gls defs thl >         val g1 = inst_goal inst1 g >       in >         snd (tac g1) thl1 >       end >   in (gls, validation) end > > Given an instantiation inst which takes metavars x and y to 2 and 3, I suggest fresh_evars introduce new constants representing the instantiated evars, Cx
and Cy, and returns inst1 = [x|->Cx, y|->Cy] and defs = [|- Cx = 2, |- Cy = 3]. > > Then, uninst_thms looks for places in the proved subgoals where a metavar has been instantiated, and uses the defs to replace the instantiation with the new constant. So if you had |- 2 = 2 in thl, but the original subgoal was ?- x = 2, then the new thl1 becomes |- Cx = 2, by rewriting the lhs with SYM (el 1 defs). > > I'm not sure if this is possible to achieve without definitions of new constants. You could possibly do it with fresh variables, but you may need to carry around the defs as assumptions in that case. The advantage of constants is that their definitions can be kept around in separate theorems. But you probably want to delete them afterwards, and it's quite heavyweight.

I don't know much about the constant definition system, but how would that work if the metavariable is instantiated by a free variable (at that time)?
More precisely, how would the following "proof with evars" work:

g `!x. ?y. x = y`
e (lift gen_tac \\ meta_exists \\ meta_inst1 `y` `x` \\ lift (fs []))

(where meta_exists turns a goal of the form `?y. P` into `P` where `y` became a metavariable; and meta_inst1 instantiates a metavariable). `y` as a metavariable is instantiated with `x`, a free variable that then gets generalized by gen_tac. Do you think that would work with the method you suggest?

— Armaël

> By the way I also want to note that Isabelle/HOL has schematic variables for these metavars. So Coq has evars, Isabelle has schematic vars, ... are we about to join that club? It would be really nice to find a lighter weight way of achieving this. > > > On 21 August 2016 at 07:51, Konrad Slind <kon...@gm...> wrote: > >       Datapoint: years ago, John Harrison spent some time implementing >     meta-variables for HOL Light. Not sure if this was inside the kernel, or just >     on top. (The latter, I think, which means that he had to deal with the same >     issues as being discussed here.) > >     He dropped the effort on the grounds that the code was becoming too complex >     for his goals in HOL Light, e.g., simplicity.  But there is no doubt more to >     the story and you should go to the source (have cc'ed John). > >     Cheers, >     Konrad. > > > >     On Sat, Aug 20, 2016 at 12:09 PM, Magnus Myreen <mag...@gm...> wrote: > >         Hi Armaël and dev, > >         Thanks for the clear explanation. > >         > 2) Implement metavariables in HOL. >         > >         > Provided that they work nicely, they would have the advantage of producing nicer >         > goals. [...] > >         I
prefer option (2) because it seems like the right thing to do for >         the long term. > >         > Implementing metavars requires defining a custom proof manager, and (among >         > others) an alternative [Evars.tactic] type, for tactics that know about >         > metavariables, and that can instantiate them. > >         Having two proof managers sounds like a mess. > >         Would it be possible to change the tactic type in HOL to support evars? > >         I know such a change could potentially cause an enormous amount of >         breakage. However, as far as I know, most tactic implementations are >         written as compositions of very low-level tactics. If the breakage >         would mostly be limited to simple adjustments to the very lowest level >         tactics, then maybe there is a chance to change the tactic type to >         allow evars. I'm thinking that we might be able to get things working >         as they were before for all proofs that do
not use metavariables, and >         then one could gradually make match_mp_tac etc. smarter in cases where >         evars are present. > >         I'm keen to hear what Michael and the other HOL developers think of >         this. This discussion should probably move to the HOL mailing lists, >         even though most active HOL developers are also on the CakeML dev >         list. > >         Cheers, >         Magnus > > >         On 20 August 2016 at 16:15, Armaël Guéneau <arm...@en...> wrote: >         > >         > Hi dev, >         > >         > I appear to be half-stuck/indecise on the question of how to get the proper >         > tactics to deal with CFs for let. So I thought I'd ask for advices. >         > >         > Currently, when dealing with the CF for [let val x = e1 in e2 end], one has to >         > provide manually beforehand the postcondition for evaluating [e1]. This is not >         > ideal, and can be avoided. In particular, in CFML it
is not required. >         > >         > The goal corresponding to a CF for [let val x = e1 in e2 end] is of the form: >         > >         >   cf_let x (cf e1) (cf e2) env H Q >         > >         > After some unfolding, it becomes: >         > >         >   ?Q'. >         >     (cf e1) env H Q' /\ >         >     !xv. (cf e2) ((x, xv)::env) (Q' xv) Q >         > >         > Now, 99% of the time, you do not want to give an instantiation for Q' right >         > away: H being known, proving the first subgoal [(cf e1) env H Q'] will in fact >         > end up providing an instantiation for Q'. >         > >         > CFML deals with that by using the "metavariables" mechanism of Coq (or "evars"), >         > which allows instantiating an exists by a metavariable, which will be actually >         > instantiated later in the proof. >         > >         > If _Q' is the metavariable for Q', then the goal becomes >         > >         >   (cf e1) env H _Q' /\ >         >   !xv.
(cf e2) ((x, xv)::env) (_Q' xv) Q >         > >         > It is then easy to split it, prove the first subgoal, which will instantiate _Q' >         > to the real thing, and then the proof can continue with >         > [!xv. (cf e2) ((x, xv)::env) (Q'' xv) Q] for some Q''. >         > >         > >         > For CFs in CakeML, as HOL doesn't currently have such a feature, I experimented >         > with two options: >         > >         > 1) Implement a small library of composable "rewrites", à la conseqConv, that >         > would apply under existential quantifications, and that would be able to >         > instantiate them. >         > >         > With a goal of the form >         > >         >   ?Q'. >         >     X /\ >         >     Y >         > >         > the CF tactics would do some work on X, hopefully eventually instantiating Q', >         > such that the goal would reduce to Y[Q''/Q']. >         > >         > Now, in full generality, these composable rewrites
need not only to apply under >         > exists, but under a succession of exists and forall, which spices things up a >         > bit. >         > >         > For example, consider a program of the form: >         > >         >   let val x = >         >     let val y = e1 >         >     in e2 end >         >   in e3 end >         > >         > The corresponding goal is of the form (for some env, H, Q): >         > >         >   cf_let x >         >     (cf_let y (cf e1) (cf e2)) >         >     (cf e3) >         > >         > and after some unfolding: >         > >         >   ?Q' Q''. >         >     ((cf e1) env H Q'' /\ >         >      !yv. (cf e2) ((y, yv)::env) (Q'' yv) Q') /\ >         >     !xv. (cf e3) ((x, xv)::env) (Q' xv) Q >         > >         > After doing work on [(cf e1) env H Q''], Q'' usually gets instantiated, and the >         > goal becomes: >         > >         >   ?Q'. >         >     (!yv. (cf e2) ((y, yv)::env) (Q'' yv) Q') /\ >         >     !xv.
(cf e3) ((x, xv)::env) (Q' xv) Q >         > >         > We want to do work on [(cf e2) ((y, yv)::env) (Q'' yv) Q'], and hopefully >         > instantiate Q'. >         > >         > -------/ end of the example /--------- >         > >         > For the moment (and with the help of Thomas Tuerk), I have a small library of >         > conseqConv+instantiations that only work under toplevel exists, and allow to >         > instantiate them. >         > >         > I think I can extend it to handle nestings of forall and exists. My concerns are >         > that: >         > >         > - Although they appear only when nesting lets (which I guess is not so common >         >   but can definitely happen), these goals with nested exists and forall may look >         >   scary and annoying to manipulate for the user. >         > >         > - In non-trivial program proofs, CF-specific tactics should clearly make less >         >   than half of the proof. Most of the work would be
proving invariants of the >         >   specific program that is being certified. >         > >         >   Then, would that mean the user would also have to use complex proof machinery >         >   to deal with this goals, where the current "subgoal" is under several exists >         >   and forall?  Maybe it's not too bad, but it's definitely an additionnal >         >   difficulty to be taken into account. >         > >         > >         > 2) Implement metavariables in HOL. >         > >         > Provided that they work nicely, they would have the advantage of producing nicer >         > goals. The intuition is that they allow to strip the exists and forall from the >         > goal altogether, and then check that metavariables are not instantiated using >         > foralls that have been introduced after them. >         > And with the way the CF tactics are designed, this kind of illegal >         > instantiations will likely never be an issue, or appear to the user.
>         > >         > Implementing metavars requires defining a custom proof manager, and (among >         > others) an alternative [Evars.tactic] type, for tactics that know about >         > metavariables, and that can instantiate them. >         > >         > I implemented that, although it's hardly tested and probably buggued, + some >         > features are missing. >         > >         > However, the main issue is as follows: there needs to be a "lift" function, of >         > type [Abbrev.tactic -> Evars.tactic]. This is such that users can use their >         > everyday tactics when arriving to the bulk of the proof. And also such that not >         > every tactic in the world needs to be reimplemented "with evars". >         > >         > The way the proofmanager with evars works is as follows: >         > >         > - metavariables (evars) are free variables of the goal >         > - an Evars.tactic is called with the goal, and the list of free variables that
>         >   are metavariables >         > - the Evars.tactic produces subgoals >         > - the theorems that the validation function receives prove the subgoals, *except >         >   that some metavariables may have been instantiated*. >         > >         > This last point is problematic for lifting standard tactics. These do not expect >         > to receive theorems for the validation function that do not directly prove the >         > subgoals. >         > >         > Therefore, the naive implementation of lift does not work: >         > >         >   fun lift tac metavars g = >         >     tac g >         > >         > For example, [MATCH_MP_TAC (|- P x ==> Q x)] produces a ``P x`` subgoal, and a >         > validation function that expects (|- P x) as input. If given (|- P 3), the >         > validation function will of course fail, and not produce (|- Q 3). >         > >         > I do not know if it's possible to define lift in a way that works around this
>         > problem. >         > >         > I thought of re-running the tactic entirely in the validation function, but this >         > does not work as the tactic may perform too much work on the specialized goal. >         > >         >   fun lift tac metavars g = >         >     let >         >       val (gls, _) = tac g >         >       fun validation inst thl = >         >         snd (tac (inst_goal inst g)) thl >         >     in (gls, validation) end >         > >         > For example, EVAL_TAC on [x = 2] produces the subgoal [x = 2], so even if x is a >         > metavariable that is specialized to 2 afterwards, lifted EVAL_TAC should produce >         > the subgoal [2 = 2]. Re-runing EVAL_TAC in the lift's validation on [2 = 2] will >         > produce a validation function that solves the goal instead. >         > >         > One idea would be to extend the common HOL tactics so that they handle this >         > situation. I don't know what amount of work this
represent, in order to cover >         > most of the everyday tactics. Or whether it is possible to be implemented >         > without too much overhead (as this may mean re-running some parts of the tactic >         > in the validation function, if the input theorems only prove a specialization of >         > the subgoals). Or whether this is a change that is even remotely likely to get >         > merged... >         > >         > >         > Thoughts? >         > Sorry for the wall of text. >         > >         > — Armaël >         > >         > >         > _______________________________________________ >         > Dev mailing list >         > De...@ca... >         > https://lists.cakeml.org/listinfo/dev > >         _______________________________________________ >         Dev mailing list >         De...@ca... >         https://lists.cakeml.org/listinfo/dev > > > >     _______________________________________________ >     Dev mailing list >     De...@ca...
>     https://lists.cakeml.org/listinfo/dev > >

>
> This discussion should probably move to the HOL mailing lists,
> even though most active HOL developers are also on the CakeML dev
> list.

I agree. Therefore, I am replying to the HOL dev mailing list. See the
initial thread copied below.

I have a suggestion for defining lift, following your approach that re-runs
the tactic in the validation.
How about introducing intermediate terms for the specialisation, to avoid
the tactic doing too much?
Thus, I suggest something like:

fun lift tac metavars g =
  let
    val (gls, _) = tac g
    fun validation inst thl =
      let
        val (inst1,defs) = fresh_evars metavars inst
        val thl1 = uninst_thms gls defs thl
        val g1 = inst_goal inst1 g
      in
        snd (tac g1) thl1
      end
  in (gls, validation) end

Given an instantiation inst which takes metavars x and y to 2 and 3, I
suggest fresh_evars introduce new constants representing the instantiated
evars, Cx and Cy, and returns inst1 = [x|->Cx, y|->Cy] and defs = [|- Cx =
2, |- Cy = 3].

Then, uninst_thms looks for places in the proved subgoals where a metavar
has been instantiated, and uses the defs to replace the instantiation with
the new constant. So if you had |- 2 = 2 in thl, but the original subgoal
was ?- x = 2, then the new thl1 becomes |- Cx = 2, by rewriting the lhs
with SYM (el 1 defs).

I'm not sure if this is possible to achieve without definitions of new
constants. You could possibly do it with fresh variables, but you may need
to carry around the defs as assumptions in that case. The advantage of
constants is that their definitions can be kept around in separate
theorems. But you probably want to delete them afterwards, and it's quite
heavyweight.

By the way I also want to note that Isabelle/HOL has schematic variables
for these metavars. So Coq has evars, Isabelle has schematic vars, ... are
we about to join that club? It would be really nice to find a lighter
weight way of achieving this.

On 21 August 2016 at 07:51, Konrad Slind <kon...@gm...> wrote:

>   Datapoint: years ago, John Harrison spent some time implementing
> meta-variables for HOL Light. Not sure if this was inside the kernel, or
> just
> on top. (The latter, I think, which means that he had to deal with the same
> issues as being discussed here.)
>
> He dropped the effort on the grounds that the code was becoming too
> complex
> for his goals in HOL Light, e.g., simplicity.  But there is no doubt more
> to
> the story and you should go to the source (have cc'ed John).
>
> Cheers,
> Konrad.
>
>
>
> On Sat, Aug 20, 2016 at 12:09 PM, Magnus Myreen <mag...@gm...>
> wrote:
>
>> Hi Armaël and dev,
>>
>> Thanks for the clear explanation.
>>
>> > 2) Implement metavariables in HOL.
>> >
>> > Provided that they work nicely, they would have the advantage of
>> producing nicer
>> > goals. [...]
>>
>> I prefer option (2) because it seems like the right thing to do for
>> the long term.
>>
>> > Implementing metavars requires defining a custom proof manager, and
>> (among
>> > others) an alternative [Evars.tactic] type, for tactics that know about
>> > metavariables, and that can instantiate them.
>>
>> Having two proof managers sounds like a mess.
>>
>> Would it be possible to change the tactic type in HOL to support evars?
>>
>> I know such a change could potentially cause an enormous amount of
>> breakage. However, as far as I know, most tactic implementations are
>> written as compositions of very low-level tactics. If the breakage
>> would mostly be limited to simple adjustments to the very lowest level
>> tactics, then maybe there is a chance to change the tactic type to
>> allow evars. I'm thinking that we might be able to get things working
>> as they were before for all proofs that do not use metavariables, and
>> then one could gradually make match_mp_tac etc. smarter in cases where
>> evars are present.
>>
>> I'm keen to hear what Michael and the other HOL developers think of
>> this. This discussion should probably move to the HOL mailing lists,
>> even though most active HOL developers are also on the CakeML dev
>> list.
>>
>> Cheers,
>> Magnus
>>
>>
>> On 20 August 2016 at 16:15, Armaël Guéneau <arm...@en...>
>> wrote:
>> >
>> > Hi dev,
>> >
>> > I appear to be half-stuck/indecise on the question of how to get the
>> proper
>> > tactics to deal with CFs for let. So I thought I'd ask for advices.
>> >
>> > Currently, when dealing with the CF for [let val x = e1 in e2 end], one
>> has to
>> > provide manually beforehand the postcondition for evaluating [e1]. This
>> is not
>> > ideal, and can be avoided. In particular, in CFML it is not required.
>> >
>> > The goal corresponding to a CF for [let val x = e1 in e2 end] is of the
>> form:
>> >
>> >   cf_let x (cf e1) (cf e2) env H Q
>> >
>> > After some unfolding, it becomes:
>> >
>> >   ?Q'.
>> >     (cf e1) env H Q' /\
>> >     !xv. (cf e2) ((x, xv)::env) (Q' xv) Q
>> >
>> > Now, 99% of the time, you do not want to give an instantiation for Q'
>> right
>> > away: H being known, proving the first subgoal [(cf e1) env H Q'] will
>> in fact
>> > end up providing an instantiation for Q'.
>> >
>> > CFML deals with that by using the "metavariables" mechanism of Coq (or
>> "evars"),
>> > which allows instantiating an exists by a metavariable, which will be
>> actually
>> > instantiated later in the proof.
>> >
>> > If _Q' is the metavariable for Q', then the goal becomes
>> >
>> >   (cf e1) env H _Q' /\
>> >   !xv. (cf e2) ((x, xv)::env) (_Q' xv) Q
>> >
>> > It is then easy to split it, prove the first subgoal, which will
>> instantiate _Q'
>> > to the real thing, and then the proof can continue with
>> > [!xv. (cf e2) ((x, xv)::env) (Q'' xv) Q] for some Q''.
>> >
>> >
>> > For CFs in CakeML, as HOL doesn't currently have such a feature, I
>> experimented
>> > with two options:
>> >
>> > 1) Implement a small library of composable "rewrites", à la conseqConv,
>> that
>> > would apply under existential quantifications, and that would be able to
>> > instantiate them.
>> >
>> > With a goal of the form
>> >
>> >   ?Q'.
>> >     X /\
>> >     Y
>> >
>> > the CF tactics would do some work on X, hopefully eventually
>> instantiating Q',
>> > such that the goal would reduce to Y[Q''/Q'].
>> >
>> > Now, in full generality, these composable rewrites need not only to
>> apply under
>> > exists, but under a succession of exists and forall, which spices
>> things up a
>> > bit.
>> >
>> > For example, consider a program of the form:
>> >
>> >   let val x =
>> >     let val y = e1
>> >     in e2 end
>> >   in e3 end
>> >
>> > The corresponding goal is of the form (for some env, H, Q):
>> >
>> >   cf_let x
>> >     (cf_let y (cf e1) (cf e2))
>> >     (cf e3)
>> >
>> > and after some unfolding:
>> >
>> >   ?Q' Q''.
>> >     ((cf e1) env H Q'' /\
>> >      !yv. (cf e2) ((y, yv)::env) (Q'' yv) Q') /\
>> >     !xv. (cf e3) ((x, xv)::env) (Q' xv) Q
>> >
>> > After doing work on [(cf e1) env H Q''], Q'' usually gets instantiated,
>> and the
>> > goal becomes:
>> >
>> >   ?Q'.
>> >     (!yv. (cf e2) ((y, yv)::env) (Q'' yv) Q') /\
>> >     !xv. (cf e3) ((x, xv)::env) (Q' xv) Q
>> >
>> > We want to do work on [(cf e2) ((y, yv)::env) (Q'' yv) Q'], and
>> hopefully
>> > instantiate Q'.
>> >
>> > -------/ end of the example /---------
>> >
>> > For the moment (and with the help of Thomas Tuerk), I have a small
>> library of
>> > conseqConv+instantiations that only work under toplevel exists, and
>> allow to
>> > instantiate them.
>> >
>> > I think I can extend it to handle nestings of forall and exists. My
>> concerns are
>> > that:
>> >
>> > - Although they appear only when nesting lets (which I guess is not so
>> common
>> >   but can definitely happen), these goals with nested exists and forall
>> may look
>> >   scary and annoying to manipulate for the user.
>> >
>> > - In non-trivial program proofs, CF-specific tactics should clearly
>> make less
>> >   than half of the proof. Most of the work would be proving invariants
>> of the
>> >   specific program that is being certified.
>> >
>> >   Then, would that mean the user would also have to use complex proof
>> machinery
>> >   to deal with this goals, where the current "subgoal" is under several
>> exists
>> >   and forall?  Maybe it's not too bad, but it's definitely an
>> additionnal
>> >   difficulty to be taken into account.
>> >
>> >
>> > 2) Implement metavariables in HOL.
>> >
>> > Provided that they work nicely, they would have the advantage of
>> producing nicer
>> > goals. The intuition is that they allow to strip the exists and forall
>> from the
>> > goal altogether, and then check that metavariables are not instantiated
>> using
>> > foralls that have been introduced after them.
>> > And with the way the CF tactics are designed, this kind of illegal
>> > instantiations will likely never be an issue, or appear to the user.
>> >
>> > Implementing metavars requires defining a custom proof manager, and
>> (among
>> > others) an alternative [Evars.tactic] type, for tactics that know about
>> > metavariables, and that can instantiate them.
>> >
>> > I implemented that, although it's hardly tested and probably buggued, +
>> some
>> > features are missing.
>> >
>> > However, the main issue is as follows: there needs to be a "lift"
>> function, of
>> > type [Abbrev.tactic -> Evars.tactic]. This is such that users can use
>> their
>> > everyday tactics when arriving to the bulk of the proof. And also such
>> that not
>> > every tactic in the world needs to be reimplemented "with evars".
>> >
>> > The way the proofmanager with evars works is as follows:
>> >
>> > - metavariables (evars) are free variables of the goal
>> > - an Evars.tactic is called with the goal, and the list of free
>> variables that
>> >   are metavariables
>> > - the Evars.tactic produces subgoals
>> > - the theorems that the validation function receives prove the
>> subgoals, *except
>> >   that some metavariables may have been instantiated*.
>> >
>> > This last point is problematic for lifting standard tactics. These do
>> not expect
>> > to receive theorems for the validation function that do not directly
>> prove the
>> > subgoals.
>> >
>> > Therefore, the naive implementation of lift does not work:
>> >
>> >   fun lift tac metavars g =
>> >     tac g
>> >
>> > For example, [MATCH_MP_TAC (|- P x ==> Q x)] produces a ``P x``
>> subgoal, and a
>> > validation function that expects (|- P x) as input. If given (|- P 3),
>> the
>> > validation function will of course fail, and not produce (|- Q 3).
>> >
>> > I do not know if it's possible to define lift in a way that works
>> around this
>> > problem.
>> >
>> > I thought of re-running the tactic entirely in the validation function,
>> but this
>> > does not work as the tactic may perform too much work on the
>> specialized goal.
>> >
>> >   fun lift tac metavars g =
>> >     let
>> >       val (gls, _) = tac g
>> >       fun validation inst thl =
>> >         snd (tac (inst_goal inst g)) thl
>> >     in (gls, validation) end
>> >
>> > For example, EVAL_TAC on [x = 2] produces the subgoal [x = 2], so even
>> if x is a
>> > metavariable that is specialized to 2 afterwards, lifted EVAL_TAC
>> should produce
>> > the subgoal [2 = 2]. Re-runing EVAL_TAC in the lift's validation on [2
>> = 2] will
>> > produce a validation function that solves the goal instead.
>> >
>> > One idea would be to extend the common HOL tactics so that they handle
>> this
>> > situation. I don't know what amount of work this represent, in order to
>> cover
>> > most of the everyday tactics. Or whether it is possible to be
>> implemented
>> > without too much overhead (as this may mean re-running some parts of
>> the tactic
>> > in the validation function, if the input theorems only prove a
>> specialization of
>> > the subgoals). Or whether this is a change that is even remotely likely
>> to get
>> > merged...
>> >
>> >
>> > Thoughts?
>> > Sorry for the wall of text.
>> >
>> > — Armaël
>> >
>> >
>> > _______________________________________________
>> > Dev mailing list
>> > De...@ca...
>> > https://lists.cakeml.org/listinfo/dev
>>
>> _______________________________________________
>> Dev mailing list
>> De...@ca...
>> https://lists.cakeml.org/listinfo/dev
>>
>
>
> _______________________________________________
> Dev mailing list
> De...@ca...
> https://lists.cakeml.org/listinfo/dev
>
>

Hi HOL developers,

This is an automatic email sent on behalf of the maintainer of the
Gilith OpenTheory Repo.

The reason for this email is that I just took delivery of a theory
package upload that obsoletes one or more of your packages, made by

HOL OpenTheory Packager <ope...@ho...>

Hopefully they've followed the recommended practice and contacted you
to discuss taking over the maintenance of some of your packages, and
if so this notification won't be a surprise to you.

Please visit

http://opentheory.gilith.com/?confirm=0d3e848b0571f5f09108872cbca2883a

to view the details of the package upload, particularly the section
called "Obsoleted Packages" to see which of your packages are
affected. After examining the upload, please click one of the links in
the "Actions" section at the bottom to either sign off on the upload
or send a report to me that this was not previously agreed.

Thank you for your contributions to the repo,

Joe Leslie-Hurd

Hi HOL developers,

This is an automatic email sent on behalf of the maintainer of the
Gilith OpenTheory Repo.

The reason for this email is that I just took delivery of a theory
package upload that obsoletes one or more of your packages, made by

HOL OpenTheory Packager <ope...@ho...>

Hopefully they've followed the recommended practice and contacted you
to discuss taking over the maintenance of some of your packages, and
if so this notification won't be a surprise to you.

Please visit

http://opentheory.gilith.com/?confirm=c7b886a8379ff9fe248327c155793160

to view the details of the package upload, particularly the section
called "Obsoleted Packages" to see which of your packages are
affected. After examining the upload, please click one of the links in
the "Actions" section at the bottom to either sign off on the upload
or send a report to me that this was not previously agreed.

Thank you for your contributions to the repo,

Joe Leslie-Hurd

Hi HOL developers,

This is an automatic email sent on behalf of the maintainer of the
Gilith OpenTheory Repo.

The reason for this email is that I just took delivery of a theory
package upload that obsoletes one or more of your packages, made by

HOL OpenTheory Packager <ope...@ho...>

Hopefully they've followed the recommended practice and contacted you
to discuss taking over the maintenance of some of your packages, and
if so this notification won't be a surprise to you.

Please visit

http://opentheory.gilith.com/?confirm=657f37e9325cf254691205560bdc0aa3

to view the details of the package upload, particularly the section
called "Obsoleted Packages" to see which of your packages are
affected. After examining the upload, please click one of the links in
the "Actions" section at the bottom to either sign off on the upload
or send a report to me that this was not previously agreed.

Thank you for your contributions to the repo,

Joe Leslie-Hurd

Perhaps it might help if I shared a bit more about dependent rewriting, and
its purpose.

The basic idea of dependent rewriting is that it is more assertive. Suppose
we have proven a useful lemma of the form

LEMMA:
|- !x y z. ant1 /\ ant2 /\ ant3 ==> (lhs = rhs)

and suppose we are facing a goal which contains an instance of lhs. If
there were no antecedents in LEMMA, we could simply rewrite with LEMMA
using REWRITE_TAC, etc. If the antecedents were all present in the
hypotheses of the goal, perhaps IMP_RES_TAC would create a new hypothesis
which is the specialized equality

lhs[a,b,c/x,y,z] = rhs[a,b,c/x,y,z]

and we could then do ASM_REWRITE_TAC (assuming no other hypotheses got in
the way and confused things).

Unfortunately, this approach is weak. IMP_RES_TAC is famous for spinning
off and creating dozens or hundreds of new hypotheses, most of which are
completely irrelevant to the proof. What a mess. (Actually, in this case,
perhaps the simplifier would be the way to go.)

But more likely, not all of the necessary instances of the antecedents are
already present in the hypotheses, just sitting there ready to be used.
Then one might proceed by doing other tactics to produce the missing
necessary antecedents, and gradually work up to the point of being able to
apply IMP_RES_TAC. But while valid, this feels distracting, that we are
moving our attention away from the goal to a set of new subgoals, while
still having to remember to finish up our main goal.

So dependent rewriting basically says, I want you, HOL theorem prover, to
do the rewrite lhs = rhs, suitably instantiated for this goal, and don't
force me to justify the antecedents first. I'll get to those later, but for
now, just do the rewriting that I am telling you to do. Afterwards, I'll
deal with those antecedents appropriately.

This is the sense in which dependent rewriting is more assertive. Using
dependent rewriting contains an inherent promise that you will discharge
the antecedents later. This means that it is also an assertion that you
know what you are doing, and that this implication LEMMA is the right thing
to do at this point in the proof. It is a choice that if wrong, can change
a provable goal into an unprovable goal, in exactly the same way that
MATCH_MP_TAC can.

But when dependent rewriting is used appropriately, with theorems that
actually do apply to the goal, it serves to clean up the task of reasoning
with theorems that have antecedents, treating them as side conditions to be
handled on the side, and changing the feel to one that is more comfortable,
closer to the familiar REWRITE_TAC.

Peter

On Wed, Jun 1, 2016 at 7:30 PM, Ramana Kumar <Ram...@cl...>
wrote:

> I started creating .doc files for the dependent rewrite tactics by copying
> from Peter's documentation in the signature file. (Thank you Peter! I think
> they are documented well there. The automated documentation-generating
> system in HOL requires these .doc files though.)
>
> This was the commit:
> https://github.com/HOL-Theorem-Prover/HOL/commit/bfc04058b2f9f52233b56be40bd941f7effd22e3
>
> I created SEEALSO entries for some entry-points which I did not document
> yet, so I didn't consider this "done" yet. But I think it's mostly done,
> and I'd be happy if someone else wanted to do the rest, or if we just
> considered this enough for opening the structure in bossLib.
>
> (By the way, it's a pity implicational rewriting tactics haven't gone much
> further (https://github.com/HOL-Theorem-Prover/HOL/issues/160).)
>
> On 1 June 2016 at 05:27, Konrad Slind <kon...@gm...> wrote:
>
>> One way to proceed would be to construct a LaTex-ed version of the above,
>> with a
>> few examples sprinkled in, and add it to the Description, somewhere
>> after the section on the simplifier. After that, you could easily add a
>> collection
>> of .doc files for the entrypoints that point to the DESCRIPTION.
>>
>> Konrad.
>>
>>
>> On Tue, May 31, 2016 at 11:02 AM, Peter Vincent Homeier <
>> pal...@tr...> wrote:
>>
>>> The dependent rewriting tactics are documented, as much as they are, in
>>> comments at the beginning of dep_rewrite.sig. These comments are copied
>>> below.
>>>
>>> The tactics are meant to be deft, quick, and light-weight, and to make
>>> proofs more robust under normal proof evolution, by reducing the number of
>>> explicit terms that are needed in the tactic. These are much less
>>> sophisticated tools than the HOL simplifier, but may be easier to control
>>> when one just wants to apply a particular implication theorem to an
>>> assumption and the goal.
>>>
>>> Perhaps the text below could be adapted into a better form of
>>> documentation. What would people like?
>>>
>>> Peter
>>>
>>> (* ================================================================== *)
>>> (* ================================================================== *)
>>> (*                     DEPENDENT REWRITING TACTICS                    *)
>>> (* ================================================================== *)
>>> (* ================================================================== *)
>>> (*                                                                    *)
>>> (* This file contains new tactics for dependent rewriting,            *)
>>> (* a generalization of the rewriting tactics of standard HOL.         *)
>>> (*                                                                    *)
>>> (* The main tactics are named DEP_REWRITE_TAC[thm1,...], etc., with   *)
>>> (* the standard variations (PURE,ONCE,ASM).  In addition, tactics     *)
>>> (* with LIST instead of ONCE are provided, making 12 tactics in all.  *)
>>> (*                                                                    *)
>>> (* The argument theorems thm1,... are typically implications.         *)
>>> (* These tactics identify the consequents of the argument theorems,   *)
>>> (* and attempt to match these against the current goal.  If a match   *)
>>> (* is found, the goal is rewritten according to the matched instance  *)
>>> (* of the consequent, after which the corresponding hypotheses of     *)
>>> (* the argument theorems are added to the goal as new conjuncts on    *)
>>> (* the left.                                                          *)
>>> (*                                                                    *)
>>> (* Care needs to be taken that the implications will match the goal   *)
>>> (* properly, that is, instances where the hypotheses in fact can be   *)
>>> (* proven.  Also, even more commonly than with REWRITE_TAC,           *)
>>> (* the rewriting process may diverge.                                 *)
>>> (*                                                                    *)
>>> (* Each implication theorem for rewriting may have a number of layers *)
>>> (* of universal quantification and implications.  At the bottom of    *)
>>> (* these layers is the base, which will either be an equality, a      *)
>>> (* negation, or a general term.  The pattern for matching will be     *)
>>> (* the left-hand-side of an equality, the term negated of a negation, *)
>>> (* or the term itself in the third case.  The search is top-to-bottom,*)
>>> (* left-to-right, depending on the quantifications of variables.      *)
>>> (*                                                                    *)
>>> (* To assist in focusing the matching to useful cases, the goal is    *)
>>> (* searched for a subterm matching the pattern.  The matching of the  *)
>>> (* pattern to subterms is performed by higher-order matching, so for  *)
>>> (* example, ``!x. P x`` will match the term ``!n. (n+m) < 4*n``.      *)
>>> (*                                                                    *)
>>> (* The argument theorems may each be either an implication or not.    *)
>>> (* For those which are implications, the hypotheses of the instance   *)
>>> (* of each theorem which matched the goal are added to the goal as    *)
>>> (* conjuncts on the left side.  For those argument theorems which     *)
>>> (* are not implications, the goal is simply rewritten with them.      *)
>>> (* This rewriting is also higher order.                               *)
>>> (*                                                                    *)
>>> (* Deep inner universal quantifications of consequents are supported. *)
>>> (* Thus, an argument theorem like EQ_LIST:                            *)
>>> (* |- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==>                    *)
>>> (*                  (CONS h1 l1 = CONS h2 l2))                        *)
>>> (* before it is used, is internally converted to appear as            *)
>>> (* |- !h1 h2 l1 l2. (h1 = h2) /\ (l1 = l2) ==>                        *)
>>> (*                  (CONS h1 l1 = CONS h2 l2)                         *)
>>> (*                                                                    *)
>>> (* As much as possible, the newly added hypotheses are analyzed to    *)
>>> (* remove duplicates; thus, several theorems with the same            *)
>>> (* hypothesis, or several uses of the same theorem, will generate     *)
>>> (* a minimal additional proof burden.                                 *)
>>> (*                                                                    *)
>>> (* The new hypotheses are added as conjuncts rather than as a         *)
>>> (* separate subgoal to reduce the user's burden of subgoal splits     *)
>>> (* when creating tactics to prove theorems.  If a separate subgoal    *)
>>> (* is desired, simply use CONJ_TAC after the dependent rewriting to   *)
>>> (* split the goal into two, where the first contains the hypotheses   *)
>>> (* and the second contains the rewritten version of the original      *)
>>> (* goal.                                                              *)
>>> (*                                                                    *)
>>> (* The tactics including PURE in their name will only use the         *)
>>> (* listed theorems for all rewriting; otherwise, the standard         *)
>>> (* rewrites are used for normal rewriting, but they are not           *)
>>> (* considered for dependent rewriting.                                *)
>>> (*                                                                    *)
>>> (* The tactics including ONCE in their name attempt to use each       *)
>>> (* theorem in the list, only once, in order, left to right.           *)
>>> (* The hypotheses added in the process of dependent rewriting are     *)
>>> (* not rewritten by the ONCE tactics.  This gives a more restrained   *)
>>> (* version of dependent rewriting.                                    *)
>>> (*                                                                    *)
>>> (* The tactics with LIST take a list of lists of theorems, and        *)
>>> (* uses each list of theorems once in order, left-to-right.  For      *)
>>> (* each list of theorems, the goal is rewritten as much as possible,  *)
>>> (* until no further changes can be achieved in the goal.  Hypotheses  *)
>>> (* are collected from all rewriting and added to the goal, but they   *)
>>> (* are not themselves rewritten.                                      *)
>>> (*                                                                    *)
>>> (* The tactics without ONCE or LIST attempt to reuse all theorems     *)
>>> (* repeatedly, continuing to rewrite until no changes can be          *)
>>> (* achieved in the goal.  Hypotheses are rewritten as well, and       *)
>>> (* their hypotheses as well, ad infinitum.                            *)
>>> (*                                                                    *)
>>> (* The tactics with ASM in their name add the assumption list to      *)
>>> (* the list of theorems used for dependent rewriting.                 *)
>>> (*                                                                    *)
>>> (* There are also three more general tactics provided,                *)
>>> (* DEP_FIND_THEN, DEP_ONCE_FIND_THEN, and DEP_LIST_FIND_THEN,         *)
>>> (* from which the others are constructed.                             *)
>>> (*                                                                    *)
>>> (* The differences among these is that DEP_ONCE_FIND_THEN uses        *)
>>> (* each of its theorems only once, in order left-to-right as given,   *)
>>> (* whereas DEP_FIND_THEN continues to reuse its theorems repeatedly   *)
>>> (* as long as forward progress and change is possible.  In contrast   *)
>>> (* to the others, DEP_LIST_FIND_THEN takes as its argument a list     *)
>>> (* of lists of theorems, and processes these in order, left-to-right. *)
>>> (* For each list of theorems, the goal is rewritten as many times     *)
>>> (* as they apply.  The hypotheses for all these rewritings are        *)
>>> (* collected into one set, added to the goal after all rewritings.    *)
>>> (*                                                                    *)
>>> (* DEP_ONCE_FIND_THEN and DEP_LIST_FIND_THEN will not attack the      *)
>>> (* hypotheses generated as a byproduct of the dependent rewriting;    *)
>>> (* in contrast, DEP_FIND_THEN will.  DEP_ONCE_FIND_THEN and           *)
>>> (* DEP_LIST_FIND_THEN might be fruitfully applied again to their      *)
>>> (* results; DEP_FIND_THEN will complete any possible rewriting,       *)
>>> (* and need not be reapplied.                                         *)
>>> (*                                                                    *)
>>> (* These take as argument a thm_tactic, a function which takes a      *)
>>> (* theorem and yields a tactic.  It is this which is used to apply    *)
>>> (* the instantiated consequent of each successfully matched           *)
>>> (* implication to the current goal.  Usually this is something like   *)
>>> (* (fn th => REWRITE_TAC[th]), but the user is free to supply any     *)
>>> (* thm_tactic he wishes.                                              *)
>>> (*                                                                    *)
>>> (* One significant note: because of the strategy of adding new        *)
>>> (* hypotheses as conjuncts to the current goal, it is not fruitful    *)
>>> (* to add *any* new assumptions to the current goal, as one might     *)
>>> (* think would happen from using, say, ASSUME_TAC.                    *)
>>> (*                                                                    *)
>>> (* Rather, any such new assumptions introduced by thm_tactic are      *)
>>> (* specifically removed.  Instead, one might wish to try MP_TAC,      *)
>>> (* which will have the effect of ASSUME_TAC and then undischarging    *)
>>> (* that assumption to become an antecedent of the goal.  Other        *)
>>> (* thm_tactics may be used, and they may even convert the single      *)
>>> (* current subgoal into multiple subgoals.  If this happens, it is    *)
>>> (* fine, but note that the control strategy of DEP_FIND_THEN will     *)
>>> (* continue to attack only the first of the multiple subgoals.        *)
>>> (*                                                                    *)
>>> (* ================================================================== *)
>>> (* ================================================================== *)
>>>
>>>
>>>
>>> On Mon, Feb 22, 2016 at 1:00 AM, Michael Norrish <
>>> Mic...@ni...> wrote:
>>>
>>>> If it's going to that "public", it would be nice if the main
>>>> entry-points were documented.
>>>>
>>>> Michael
>>>>
>>>> > On 22 Feb 2016, at 16:21, Ramana Kumar <Ram...@cl...>
>>>> wrote:
>>>> >
>>>> > What needs to be documented? I think I just meant put an "open
>>>> > dep_rewrite" into bossLib.
>>>> >
>>>> > On 22 February 2016 at 11:19, Michael Norrish
>>>> > <Mic...@ni...> wrote:
>>>> >> Please document somewhere, but yes.
>>>> >>
>>>> >> Michael
>>>> >>
>>>> >>> On 22 Feb 2016, at 09:24, Ramana Kumar <Ram...@cl...>
>>>> wrote:
>>>> >>>
>>>> >>> So, yes?
>>>> >>>
>>>> >>> On 2 February 2016 at 15:51, Ramana Kumar <
>>>> Ram...@cl...> wrote:
>>>> >>>> On 2 February 2016 at 15:04, Michael Norrish <
>>>> Mic...@ni...>
>>>> >>>> wrote:
>>>> >>>>>
>>>> >>>>> Don't know.
>>>> >>>>>
>>>> >>>>> Is it clearly adding functionality we don't have any other way?
>>>> >>>>
>>>> >>>>
>>>> >>>> Yes, I think so. The other way to get the functionality is
>>>> cumbersome:
>>>> >>>> abbreviate lots of your goal and try to instantiate the dependent
>>>> rewrite
>>>> >>>> theorem manually.
>>>> >>>>
>>>> >>>>>
>>>> >>>>>
>>>> >>>>> Is it big (makes a difference to Moscow ML); does it contaminate
>>>> the
>>>> >>>>> environment at all (declares new constants; adjusts grammars;
>>>> adjusts other
>>>> >>>>> global elements of the system)?
>>>> >>>>
>>>> >>>>
>>>> >>>> It doesn't touch the logical environment, and I don't think it's
>>>> very big.
>>>> >>>>
>>>> >>>> Implicational rewriting (issue #160) would be better, but we don't
>>>> have
>>>> >>>> that.
>>>> >>>>
>>>> >>>>>
>>>> >>>>>
>>>> >>>>> Michael
>>>> >>>>>
>>>> >>>>> On 2 Feb 2016, at 12:17, Ramana Kumar <Ram...@cl...>
>>>> wrote:
>>>> >>>>>
>>>> >>>>> Tap tap tap... is this thing on?
>>>> >>>>>
>>>> >>>>> On 22 January 2016 at 17:56, Ramana Kumar <
>>>> Ram...@cl...>
>>>> >>>>> wrote:
>>>> >>>>>>
>>>> >>>>>> Would there be any harm in adding dep_rewrite to the standard
>>>> set of
>>>> >>>>>> libraries that are loaded by default? (Similarly to how
>>>> quantHeuristicsLib
>>>> >>>>>> was added some time recently.)
>>>> >>>>>
>>>> >>>>>
>>>> >>>>>
>>>> >>>>>
>>>> ------------------------------------------------------------------------------
>>>> >>>>> Site24x7 APM Insight: Get Deep Visibility into Application
>>>> Performance
>>>> >>>>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>>>> >>>>> Monitor end-to-end web transactions and take corrective actions
>>>> now
>>>> >>>>> Troubleshoot faster and improve end-user experience. Signup Now!
>>>> >>>>>
>>>> >>>>>
>>>> http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140_______________________________________________
>>>> >>>>> Hol-developers mailing list
>>>> >>>>> Hol...@li...
>>>> >>>>> https://lists.sourceforge.net/lists/listinfo/hol-developers
>>>> >>>>>
>>>> >>>>>
>>>> >>>>>
>>>> >>>>> ________________________________
>>>> >>>>>
>>>> >>>>> The information in this e-mail may be confidential and subject to
>>>> legal
>>>> >>>>> professional privilege and/or copyright. National ICT Australia
>>>> Limited
>>>> >>>>> accepts no liability for any damage caused by this email or its
>>>> attachments.
>>>> >>>>
>>>> >>>>
>>>> >>
>>>> >>
>>>> >> ________________________________
>>>> >>
>>>> >> The information in this e-mail may be confidential and subject to
>>>> legal professional privilege and/or copyright. National ICT Australia
>>>> Limited accepts no liability for any damage caused by this email or its
>>>> attachments.
>>>> >>
>>>> >>
>>>> ------------------------------------------------------------------------------
>>>> >> Site24x7 APM Insight: Get Deep Visibility into Application
>>>> Performance
>>>> >> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>>>> >> Monitor end-to-end web transactions and take corrective actions now
>>>> >> Troubleshoot faster and improve end-user experience. Signup Now!
>>>> >> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
>>>> >> _______________________________________________
>>>> >> hol-info mailing list
>>>> >> hol...@li...
>>>> >> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>>
>>>>
>>>>
>>>> ------------------------------------------------------------------------------
>>>> Site24x7 APM Insight: Get Deep Visibility into Application Performance
>>>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>>>> Monitor end-to-end web transactions and take corrective actions now
>>>> Troubleshoot faster and improve end-user experience. Signup Now!
>>>> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
>>>> _______________________________________________
>>>> Hol-developers mailing list
>>>> Hol...@li...
>>>> https://lists.sourceforge.net/lists/listinfo/hol-developers
>>>>
>>>
>>>
>>>
>>> --
>>>
>>>
>>> "In Your majesty ride prosperously
>>> because of truth, humility, and righteousness;
>>> and Your right hand shall teach You awesome things." (Psalm 45:4)
>>>
>>>
>>> ------------------------------------------------------------------------------
>>> What NetFlow Analyzer can do for you? Monitors network bandwidth and
>>> traffic
>>> patterns at an interface-level. Reveals which users, apps, and protocols
>>> are
>>> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
>>> J-Flow, sFlow and other flows. Make informed decisions using capacity
>>> planning reports.
>>> https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
>>> _______________________________________________
>>> Hol-developers mailing list
>>> Hol...@li...
>>> https://lists.sourceforge.net/lists/listinfo/hol-developers
>>>
>>>
>>
>

-- 

"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)

I started creating .doc files for the dependent rewrite tactics by copying
from Peter's documentation in the signature file. (Thank you Peter! I think
they are documented well there. The automated documentation-generating
system in HOL requires these .doc files though.)

This was the commit:
https://github.com/HOL-Theorem-Prover/HOL/commit/bfc04058b2f9f52233b56be40bd941f7effd22e3

I created SEEALSO entries for some entry-points which I did not document
yet, so I didn't consider this "done" yet. But I think it's mostly done,
and I'd be happy if someone else wanted to do the rest, or if we just
considered this enough for opening the structure in bossLib.

(By the way, it's a pity implicational rewriting tactics haven't gone much
further (https://github.com/HOL-Theorem-Prover/HOL/issues/160).)

On 1 June 2016 at 05:27, Konrad Slind <kon...@gm...> wrote:

> One way to proceed would be to construct a LaTex-ed version of the above,
> with a
> few examples sprinkled in, and add it to the Description, somewhere
> after the section on the simplifier. After that, you could easily add a
> collection
> of .doc files for the entrypoints that point to the DESCRIPTION.
>
> Konrad.
>
>
> On Tue, May 31, 2016 at 11:02 AM, Peter Vincent Homeier <
> pal...@tr...> wrote:
>
>> The dependent rewriting tactics are documented, as much as they are, in
>> comments at the beginning of dep_rewrite.sig. These comments are copied
>> below.
>>
>> The tactics are meant to be deft, quick, and light-weight, and to make
>> proofs more robust under normal proof evolution, by reducing the number of
>> explicit terms that are needed in the tactic. These are much less
>> sophisticated tools than the HOL simplifier, but may be easier to control
>> when one just wants to apply a particular implication theorem to an
>> assumption and the goal.
>>
>> Perhaps the text below could be adapted into a better form of
>> documentation. What would people like?
>>
>> Peter
>>
>> (* ================================================================== *)
>> (* ================================================================== *)
>> (*                     DEPENDENT REWRITING TACTICS                    *)
>> (* ================================================================== *)
>> (* ================================================================== *)
>> (*                                                                    *)
>> (* This file contains new tactics for dependent rewriting,            *)
>> (* a generalization of the rewriting tactics of standard HOL.         *)
>> (*                                                                    *)
>> (* The main tactics are named DEP_REWRITE_TAC[thm1,...], etc., with   *)
>> (* the standard variations (PURE,ONCE,ASM).  In addition, tactics     *)
>> (* with LIST instead of ONCE are provided, making 12 tactics in all.  *)
>> (*                                                                    *)
>> (* The argument theorems thm1,... are typically implications.         *)
>> (* These tactics identify the consequents of the argument theorems,   *)
>> (* and attempt to match these against the current goal.  If a match   *)
>> (* is found, the goal is rewritten according to the matched instance  *)
>> (* of the consequent, after which the corresponding hypotheses of     *)
>> (* the argument theorems are added to the goal as new conjuncts on    *)
>> (* the left.                                                          *)
>> (*                                                                    *)
>> (* Care needs to be taken that the implications will match the goal   *)
>> (* properly, that is, instances where the hypotheses in fact can be   *)
>> (* proven.  Also, even more commonly than with REWRITE_TAC,           *)
>> (* the rewriting process may diverge.                                 *)
>> (*                                                                    *)
>> (* Each implication theorem for rewriting may have a number of layers *)
>> (* of universal quantification and implications.  At the bottom of    *)
>> (* these layers is the base, which will either be an equality, a      *)
>> (* negation, or a general term.  The pattern for matching will be     *)
>> (* the left-hand-side of an equality, the term negated of a negation, *)
>> (* or the term itself in the third case.  The search is top-to-bottom,*)
>> (* left-to-right, depending on the quantifications of variables.      *)
>> (*                                                                    *)
>> (* To assist in focusing the matching to useful cases, the goal is    *)
>> (* searched for a subterm matching the pattern.  The matching of the  *)
>> (* pattern to subterms is performed by higher-order matching, so for  *)
>> (* example, ``!x. P x`` will match the term ``!n. (n+m) < 4*n``.      *)
>> (*                                                                    *)
>> (* The argument theorems may each be either an implication or not.    *)
>> (* For those which are implications, the hypotheses of the instance   *)
>> (* of each theorem which matched the goal are added to the goal as    *)
>> (* conjuncts on the left side.  For those argument theorems which     *)
>> (* are not implications, the goal is simply rewritten with them.      *)
>> (* This rewriting is also higher order.                               *)
>> (*                                                                    *)
>> (* Deep inner universal quantifications of consequents are supported. *)
>> (* Thus, an argument theorem like EQ_LIST:                            *)
>> (* |- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==>                    *)
>> (*                  (CONS h1 l1 = CONS h2 l2))                        *)
>> (* before it is used, is internally converted to appear as            *)
>> (* |- !h1 h2 l1 l2. (h1 = h2) /\ (l1 = l2) ==>                        *)
>> (*                  (CONS h1 l1 = CONS h2 l2)                         *)
>> (*                                                                    *)
>> (* As much as possible, the newly added hypotheses are analyzed to    *)
>> (* remove duplicates; thus, several theorems with the same            *)
>> (* hypothesis, or several uses of the same theorem, will generate     *)
>> (* a minimal additional proof burden.                                 *)
>> (*                                                                    *)
>> (* The new hypotheses are added as conjuncts rather than as a         *)
>> (* separate subgoal to reduce the user's burden of subgoal splits     *)
>> (* when creating tactics to prove theorems.  If a separate subgoal    *)
>> (* is desired, simply use CONJ_TAC after the dependent rewriting to   *)
>> (* split the goal into two, where the first contains the hypotheses   *)
>> (* and the second contains the rewritten version of the original      *)
>> (* goal.                                                              *)
>> (*                                                                    *)
>> (* The tactics including PURE in their name will only use the         *)
>> (* listed theorems for all rewriting; otherwise, the standard         *)
>> (* rewrites are used for normal rewriting, but they are not           *)
>> (* considered for dependent rewriting.                                *)
>> (*                                                                    *)
>> (* The tactics including ONCE in their name attempt to use each       *)
>> (* theorem in the list, only once, in order, left to right.           *)
>> (* The hypotheses added in the process of dependent rewriting are     *)
>> (* not rewritten by the ONCE tactics.  This gives a more restrained   *)
>> (* version of dependent rewriting.                                    *)
>> (*                                                                    *)
>> (* The tactics with LIST take a list of lists of theorems, and        *)
>> (* uses each list of theorems once in order, left-to-right.  For      *)
>> (* each list of theorems, the goal is rewritten as much as possible,  *)
>> (* until no further changes can be achieved in the goal.  Hypotheses  *)
>> (* are collected from all rewriting and added to the goal, but they   *)
>> (* are not themselves rewritten.                                      *)
>> (*                                                                    *)
>> (* The tactics without ONCE or LIST attempt to reuse all theorems     *)
>> (* repeatedly, continuing to rewrite until no changes can be          *)
>> (* achieved in the goal.  Hypotheses are rewritten as well, and       *)
>> (* their hypotheses as well, ad infinitum.                            *)
>> (*                                                                    *)
>> (* The tactics with ASM in their name add the assumption list to      *)
>> (* the list of theorems used for dependent rewriting.                 *)
>> (*                                                                    *)
>> (* There are also three more general tactics provided,                *)
>> (* DEP_FIND_THEN, DEP_ONCE_FIND_THEN, and DEP_LIST_FIND_THEN,         *)
>> (* from which the others are constructed.                             *)
>> (*                                                                    *)
>> (* The differences among these is that DEP_ONCE_FIND_THEN uses        *)
>> (* each of its theorems only once, in order left-to-right as given,   *)
>> (* whereas DEP_FIND_THEN continues to reuse its theorems repeatedly   *)
>> (* as long as forward progress and change is possible.  In contrast   *)
>> (* to the others, DEP_LIST_FIND_THEN takes as its argument a list     *)
>> (* of lists of theorems, and processes these in order, left-to-right. *)
>> (* For each list of theorems, the goal is rewritten as many times     *)
>> (* as they apply.  The hypotheses for all these rewritings are        *)
>> (* collected into one set, added to the goal after all rewritings.    *)
>> (*                                                                    *)
>> (* DEP_ONCE_FIND_THEN and DEP_LIST_FIND_THEN will not attack the      *)
>> (* hypotheses generated as a byproduct of the dependent rewriting;    *)
>> (* in contrast, DEP_FIND_THEN will.  DEP_ONCE_FIND_THEN and           *)
>> (* DEP_LIST_FIND_THEN might be fruitfully applied again to their      *)
>> (* results; DEP_FIND_THEN will complete any possible rewriting,       *)
>> (* and need not be reapplied.                                         *)
>> (*                                                                    *)
>> (* These take as argument a thm_tactic, a function which takes a      *)
>> (* theorem and yields a tactic.  It is this which is used to apply    *)
>> (* the instantiated consequent of each successfully matched           *)
>> (* implication to the current goal.  Usually this is something like   *)
>> (* (fn th => REWRITE_TAC[th]), but the user is free to supply any     *)
>> (* thm_tactic he wishes.                                              *)
>> (*                                                                    *)
>> (* One significant note: because of the strategy of adding new        *)
>> (* hypotheses as conjuncts to the current goal, it is not fruitful    *)
>> (* to add *any* new assumptions to the current goal, as one might     *)
>> (* think would happen from using, say, ASSUME_TAC.                    *)
>> (*                                                                    *)
>> (* Rather, any such new assumptions introduced by thm_tactic are      *)
>> (* specifically removed.  Instead, one might wish to try MP_TAC,      *)
>> (* which will have the effect of ASSUME_TAC and then undischarging    *)
>> (* that assumption to become an antecedent of the goal.  Other        *)
>> (* thm_tactics may be used, and they may even convert the single      *)
>> (* current subgoal into multiple subgoals.  If this happens, it is    *)
>> (* fine, but note that the control strategy of DEP_FIND_THEN will     *)
>> (* continue to attack only the first of the multiple subgoals.        *)
>> (*                                                                    *)
>> (* ================================================================== *)
>> (* ================================================================== *)
>>
>>
>>
>> On Mon, Feb 22, 2016 at 1:00 AM, Michael Norrish <
>> Mic...@ni...> wrote:
>>
>>> If it's going to that "public", it would be nice if the main
>>> entry-points were documented.
>>>
>>> Michael
>>>
>>> > On 22 Feb 2016, at 16:21, Ramana Kumar <Ram...@cl...>
>>> wrote:
>>> >
>>> > What needs to be documented? I think I just meant put an "open
>>> > dep_rewrite" into bossLib.
>>> >
>>> > On 22 February 2016 at 11:19, Michael Norrish
>>> > <Mic...@ni...> wrote:
>>> >> Please document somewhere, but yes.
>>> >>
>>> >> Michael
>>> >>
>>> >>> On 22 Feb 2016, at 09:24, Ramana Kumar <Ram...@cl...>
>>> wrote:
>>> >>>
>>> >>> So, yes?
>>> >>>
>>> >>> On 2 February 2016 at 15:51, Ramana Kumar <Ram...@cl...>
>>> wrote:
>>> >>>> On 2 February 2016 at 15:04, Michael Norrish <
>>> Mic...@ni...>
>>> >>>> wrote:
>>> >>>>>
>>> >>>>> Don't know.
>>> >>>>>
>>> >>>>> Is it clearly adding functionality we don't have any other way?
>>> >>>>
>>> >>>>
>>> >>>> Yes, I think so. The other way to get the functionality is
>>> cumbersome:
>>> >>>> abbreviate lots of your goal and try to instantiate the dependent
>>> rewrite
>>> >>>> theorem manually.
>>> >>>>
>>> >>>>>
>>> >>>>>
>>> >>>>> Is it big (makes a difference to Moscow ML); does it contaminate
>>> the
>>> >>>>> environment at all (declares new constants; adjusts grammars;
>>> adjusts other
>>> >>>>> global elements of the system)?
>>> >>>>
>>> >>>>
>>> >>>> It doesn't touch the logical environment, and I don't think it's
>>> very big.
>>> >>>>
>>> >>>> Implicational rewriting (issue #160) would be better, but we don't
>>> have
>>> >>>> that.
>>> >>>>
>>> >>>>>
>>> >>>>>
>>> >>>>> Michael
>>> >>>>>
>>> >>>>> On 2 Feb 2016, at 12:17, Ramana Kumar <Ram...@cl...>
>>> wrote:
>>> >>>>>
>>> >>>>> Tap tap tap... is this thing on?
>>> >>>>>
>>> >>>>> On 22 January 2016 at 17:56, Ramana Kumar <
>>> Ram...@cl...>
>>> >>>>> wrote:
>>> >>>>>>
>>> >>>>>> Would there be any harm in adding dep_rewrite to the standard set
>>> of
>>> >>>>>> libraries that are loaded by default? (Similarly to how
>>> quantHeuristicsLib
>>> >>>>>> was added some time recently.)
>>> >>>>>
>>> >>>>>
>>> >>>>>
>>> >>>>>
>>> ------------------------------------------------------------------------------
>>> >>>>> Site24x7 APM Insight: Get Deep Visibility into Application
>>> Performance
>>> >>>>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>>> >>>>> Monitor end-to-end web transactions and take corrective actions now
>>> >>>>> Troubleshoot faster and improve end-user experience. Signup Now!
>>> >>>>>
>>> >>>>>
>>> http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140_______________________________________________
>>> >>>>> Hol-developers mailing list
>>> >>>>> Hol...@li...
>>> >>>>> https://lists.sourceforge.net/lists/listinfo/hol-developers
>>> >>>>>
>>> >>>>>
>>> >>>>>
>>> >>>>> ________________________________
>>> >>>>>
>>> >>>>> The information in this e-mail may be confidential and subject to
>>> legal
>>> >>>>> professional privilege and/or copyright. National ICT Australia
>>> Limited
>>> >>>>> accepts no liability for any damage caused by this email or its
>>> attachments.
>>> >>>>
>>> >>>>
>>> >>
>>> >>
>>> >> ________________________________
>>> >>
>>> >> The information in this e-mail may be confidential and subject to
>>> legal professional privilege and/or copyright. National ICT Australia
>>> Limited accepts no liability for any damage caused by this email or its
>>> attachments.
>>> >>
>>> >>
>>> ------------------------------------------------------------------------------
>>> >> Site24x7 APM Insight: Get Deep Visibility into Application Performance
>>> >> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>>> >> Monitor end-to-end web transactions and take corrective actions now
>>> >> Troubleshoot faster and improve end-user experience. Signup Now!
>>> >> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
>>> >> _______________________________________________
>>> >> hol-info mailing list
>>> >> hol...@li...
>>> >> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>>
>>>
>>> ------------------------------------------------------------------------------
>>> Site24x7 APM Insight: Get Deep Visibility into Application Performance
>>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>>> Monitor end-to-end web transactions and take corrective actions now
>>> Troubleshoot faster and improve end-user experience. Signup Now!
>>> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
>>> _______________________________________________
>>> Hol-developers mailing list
>>> Hol...@li...
>>> https://lists.sourceforge.net/lists/listinfo/hol-developers
>>>
>>
>>
>>
>> --
>>
>>
>> "In Your majesty ride prosperously
>> because of truth, humility, and righteousness;
>> and Your right hand shall teach You awesome things." (Psalm 45:4)
>>
>>
>> ------------------------------------------------------------------------------
>> What NetFlow Analyzer can do for you? Monitors network bandwidth and
>> traffic
>> patterns at an interface-level. Reveals which users, apps, and protocols
>> are
>> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
>> J-Flow, sFlow and other flows. Make informed decisions using capacity
>> planning reports.
>> https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
>> _______________________________________________
>> Hol-developers mailing list
>> Hol...@li...
>> https://lists.sourceforge.net/lists/listinfo/hol-developers
>>
>>
>

One way to proceed would be to construct a LaTex-ed version of the above,
with a
few examples sprinkled in, and add it to the Description, somewhere
after the section on the simplifier. After that, you could easily add a
collection
of .doc files for the entrypoints that point to the DESCRIPTION.

Konrad.

On Tue, May 31, 2016 at 11:02 AM, Peter Vincent Homeier <
pal...@tr...> wrote:

> The dependent rewriting tactics are documented, as much as they are, in
> comments at the beginning of dep_rewrite.sig. These comments are copied
> below.
>
> The tactics are meant to be deft, quick, and light-weight, and to make
> proofs more robust under normal proof evolution, by reducing the number of
> explicit terms that are needed in the tactic. These are much less
> sophisticated tools than the HOL simplifier, but may be easier to control
> when one just wants to apply a particular implication theorem to an
> assumption and the goal.
>
> Perhaps the text below could be adapted into a better form of
> documentation. What would people like?
>
> Peter
>
> (* ================================================================== *)
> (* ================================================================== *)
> (*                     DEPENDENT REWRITING TACTICS                    *)
> (* ================================================================== *)
> (* ================================================================== *)
> (*                                                                    *)
> (* This file contains new tactics for dependent rewriting,            *)
> (* a generalization of the rewriting tactics of standard HOL.         *)
> (*                                                                    *)
> (* The main tactics are named DEP_REWRITE_TAC[thm1,...], etc., with   *)
> (* the standard variations (PURE,ONCE,ASM).  In addition, tactics     *)
> (* with LIST instead of ONCE are provided, making 12 tactics in all.  *)
> (*                                                                    *)
> (* The argument theorems thm1,... are typically implications.         *)
> (* These tactics identify the consequents of the argument theorems,   *)
> (* and attempt to match these against the current goal.  If a match   *)
> (* is found, the goal is rewritten according to the matched instance  *)
> (* of the consequent, after which the corresponding hypotheses of     *)
> (* the argument theorems are added to the goal as new conjuncts on    *)
> (* the left.                                                          *)
> (*                                                                    *)
> (* Care needs to be taken that the implications will match the goal   *)
> (* properly, that is, instances where the hypotheses in fact can be   *)
> (* proven.  Also, even more commonly than with REWRITE_TAC,           *)
> (* the rewriting process may diverge.                                 *)
> (*                                                                    *)
> (* Each implication theorem for rewriting may have a number of layers *)
> (* of universal quantification and implications.  At the bottom of    *)
> (* these layers is the base, which will either be an equality, a      *)
> (* negation, or a general term.  The pattern for matching will be     *)
> (* the left-hand-side of an equality, the term negated of a negation, *)
> (* or the term itself in the third case.  The search is top-to-bottom,*)
> (* left-to-right, depending on the quantifications of variables.      *)
> (*                                                                    *)
> (* To assist in focusing the matching to useful cases, the goal is    *)
> (* searched for a subterm matching the pattern.  The matching of the  *)
> (* pattern to subterms is performed by higher-order matching, so for  *)
> (* example, ``!x. P x`` will match the term ``!n. (n+m) < 4*n``.      *)
> (*                                                                    *)
> (* The argument theorems may each be either an implication or not.    *)
> (* For those which are implications, the hypotheses of the instance   *)
> (* of each theorem which matched the goal are added to the goal as    *)
> (* conjuncts on the left side.  For those argument theorems which     *)
> (* are not implications, the goal is simply rewritten with them.      *)
> (* This rewriting is also higher order.                               *)
> (*                                                                    *)
> (* Deep inner universal quantifications of consequents are supported. *)
> (* Thus, an argument theorem like EQ_LIST:                            *)
> (* |- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==>                    *)
> (*                  (CONS h1 l1 = CONS h2 l2))                        *)
> (* before it is used, is internally converted to appear as            *)
> (* |- !h1 h2 l1 l2. (h1 = h2) /\ (l1 = l2) ==>                        *)
> (*                  (CONS h1 l1 = CONS h2 l2)                         *)
> (*                                                                    *)
> (* As much as possible, the newly added hypotheses are analyzed to    *)
> (* remove duplicates; thus, several theorems with the same            *)
> (* hypothesis, or several uses of the same theorem, will generate     *)
> (* a minimal additional proof burden.                                 *)
> (*                                                                    *)
> (* The new hypotheses are added as conjuncts rather than as a         *)
> (* separate subgoal to reduce the user's burden of subgoal splits     *)
> (* when creating tactics to prove theorems.  If a separate subgoal    *)
> (* is desired, simply use CONJ_TAC after the dependent rewriting to   *)
> (* split the goal into two, where the first contains the hypotheses   *)
> (* and the second contains the rewritten version of the original      *)
> (* goal.                                                              *)
> (*                                                                    *)
> (* The tactics including PURE in their name will only use the         *)
> (* listed theorems for all rewriting; otherwise, the standard         *)
> (* rewrites are used for normal rewriting, but they are not           *)
> (* considered for dependent rewriting.                                *)
> (*                                                                    *)
> (* The tactics including ONCE in their name attempt to use each       *)
> (* theorem in the list, only once, in order, left to right.           *)
> (* The hypotheses added in the process of dependent rewriting are     *)
> (* not rewritten by the ONCE tactics.  This gives a more restrained   *)
> (* version of dependent rewriting.                                    *)
> (*                                                                    *)
> (* The tactics with LIST take a list of lists of theorems, and        *)
> (* uses each list of theorems once in order, left-to-right.  For      *)
> (* each list of theorems, the goal is rewritten as much as possible,  *)
> (* until no further changes can be achieved in the goal.  Hypotheses  *)
> (* are collected from all rewriting and added to the goal, but they   *)
> (* are not themselves rewritten.                                      *)
> (*                                                                    *)
> (* The tactics without ONCE or LIST attempt to reuse all theorems     *)
> (* repeatedly, continuing to rewrite until no changes can be          *)
> (* achieved in the goal.  Hypotheses are rewritten as well, and       *)
> (* their hypotheses as well, ad infinitum.                            *)
> (*                                                                    *)
> (* The tactics with ASM in their name add the assumption list to      *)
> (* the list of theorems used for dependent rewriting.                 *)
> (*                                                                    *)
> (* There are also three more general tactics provided,                *)
> (* DEP_FIND_THEN, DEP_ONCE_FIND_THEN, and DEP_LIST_FIND_THEN,         *)
> (* from which the others are constructed.                             *)
> (*                                                                    *)
> (* The differences among these is that DEP_ONCE_FIND_THEN uses        *)
> (* each of its theorems only once, in order left-to-right as given,   *)
> (* whereas DEP_FIND_THEN continues to reuse its theorems repeatedly   *)
> (* as long as forward progress and change is possible.  In contrast   *)
> (* to the others, DEP_LIST_FIND_THEN takes as its argument a list     *)
> (* of lists of theorems, and processes these in order, left-to-right. *)
> (* For each list of theorems, the goal is rewritten as many times     *)
> (* as they apply.  The hypotheses for all these rewritings are        *)
> (* collected into one set, added to the goal after all rewritings.    *)
> (*                                                                    *)
> (* DEP_ONCE_FIND_THEN and DEP_LIST_FIND_THEN will not attack the      *)
> (* hypotheses generated as a byproduct of the dependent rewriting;    *)
> (* in contrast, DEP_FIND_THEN will.  DEP_ONCE_FIND_THEN and           *)
> (* DEP_LIST_FIND_THEN might be fruitfully applied again to their      *)
> (* results; DEP_FIND_THEN will complete any possible rewriting,       *)
> (* and need not be reapplied.                                         *)
> (*                                                                    *)
> (* These take as argument a thm_tactic, a function which takes a      *)
> (* theorem and yields a tactic.  It is this which is used to apply    *)
> (* the instantiated consequent of each successfully matched           *)
> (* implication to the current goal.  Usually this is something like   *)
> (* (fn th => REWRITE_TAC[th]), but the user is free to supply any     *)
> (* thm_tactic he wishes.                                              *)
> (*                                                                    *)
> (* One significant note: because of the strategy of adding new        *)
> (* hypotheses as conjuncts to the current goal, it is not fruitful    *)
> (* to add *any* new assumptions to the current goal, as one might     *)
> (* think would happen from using, say, ASSUME_TAC.                    *)
> (*                                                                    *)
> (* Rather, any such new assumptions introduced by thm_tactic are      *)
> (* specifically removed.  Instead, one might wish to try MP_TAC,      *)
> (* which will have the effect of ASSUME_TAC and then undischarging    *)
> (* that assumption to become an antecedent of the goal.  Other        *)
> (* thm_tactics may be used, and they may even convert the single      *)
> (* current subgoal into multiple subgoals.  If this happens, it is    *)
> (* fine, but note that the control strategy of DEP_FIND_THEN will     *)
> (* continue to attack only the first of the multiple subgoals.        *)
> (*                                                                    *)
> (* ================================================================== *)
> (* ================================================================== *)
>
>
>
> On Mon, Feb 22, 2016 at 1:00 AM, Michael Norrish <
> Mic...@ni...> wrote:
>
>> If it's going to that "public", it would be nice if the main entry-points
>> were documented.
>>
>> Michael
>>
>> > On 22 Feb 2016, at 16:21, Ramana Kumar <Ram...@cl...>
>> wrote:
>> >
>> > What needs to be documented? I think I just meant put an "open
>> > dep_rewrite" into bossLib.
>> >
>> > On 22 February 2016 at 11:19, Michael Norrish
>> > <Mic...@ni...> wrote:
>> >> Please document somewhere, but yes.
>> >>
>> >> Michael
>> >>
>> >>> On 22 Feb 2016, at 09:24, Ramana Kumar <Ram...@cl...>
>> wrote:
>> >>>
>> >>> So, yes?
>> >>>
>> >>> On 2 February 2016 at 15:51, Ramana Kumar <Ram...@cl...>
>> wrote:
>> >>>> On 2 February 2016 at 15:04, Michael Norrish <
>> Mic...@ni...>
>> >>>> wrote:
>> >>>>>
>> >>>>> Don't know.
>> >>>>>
>> >>>>> Is it clearly adding functionality we don't have any other way?
>> >>>>
>> >>>>
>> >>>> Yes, I think so. The other way to get the functionality is
>> cumbersome:
>> >>>> abbreviate lots of your goal and try to instantiate the dependent
>> rewrite
>> >>>> theorem manually.
>> >>>>
>> >>>>>
>> >>>>>
>> >>>>> Is it big (makes a difference to Moscow ML); does it contaminate the
>> >>>>> environment at all (declares new constants; adjusts grammars;
>> adjusts other
>> >>>>> global elements of the system)?
>> >>>>
>> >>>>
>> >>>> It doesn't touch the logical environment, and I don't think it's
>> very big.
>> >>>>
>> >>>> Implicational rewriting (issue #160) would be better, but we don't
>> have
>> >>>> that.
>> >>>>
>> >>>>>
>> >>>>>
>> >>>>> Michael
>> >>>>>
>> >>>>> On 2 Feb 2016, at 12:17, Ramana Kumar <Ram...@cl...>
>> wrote:
>> >>>>>
>> >>>>> Tap tap tap... is this thing on?
>> >>>>>
>> >>>>> On 22 January 2016 at 17:56, Ramana Kumar <
>> Ram...@cl...>
>> >>>>> wrote:
>> >>>>>>
>> >>>>>> Would there be any harm in adding dep_rewrite to the standard set
>> of
>> >>>>>> libraries that are loaded by default? (Similarly to how
>> quantHeuristicsLib
>> >>>>>> was added some time recently.)
>> >>>>>
>> >>>>>
>> >>>>>
>> >>>>>
>> ------------------------------------------------------------------------------
>> >>>>> Site24x7 APM Insight: Get Deep Visibility into Application
>> Performance
>> >>>>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>> >>>>> Monitor end-to-end web transactions and take corrective actions now
>> >>>>> Troubleshoot faster and improve end-user experience. Signup Now!
>> >>>>>
>> >>>>>
>> http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140_______________________________________________
>> >>>>> Hol-developers mailing list
>> >>>>> Hol...@li...
>> >>>>> https://lists.sourceforge.net/lists/listinfo/hol-developers
>> >>>>>
>> >>>>>
>> >>>>>
>> >>>>> ________________________________
>> >>>>>
>> >>>>> The information in this e-mail may be confidential and subject to
>> legal
>> >>>>> professional privilege and/or copyright. National ICT Australia
>> Limited
>> >>>>> accepts no liability for any damage caused by this email or its
>> attachments.
>> >>>>
>> >>>>
>> >>
>> >>
>> >> ________________________________
>> >>
>> >> The information in this e-mail may be confidential and subject to
>> legal professional privilege and/or copyright. National ICT Australia
>> Limited accepts no liability for any damage caused by this email or its
>> attachments.
>> >>
>> >>
>> ------------------------------------------------------------------------------
>> >> Site24x7 APM Insight: Get Deep Visibility into Application Performance
>> >> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>> >> Monitor end-to-end web transactions and take corrective actions now
>> >> Troubleshoot faster and improve end-user experience. Signup Now!
>> >> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
>> >> _______________________________________________
>> >> hol-info mailing list
>> >> hol...@li...
>> >> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>>
>> ------------------------------------------------------------------------------
>> Site24x7 APM Insight: Get Deep Visibility into Application Performance
>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
>> Monitor end-to-end web transactions and take corrective actions now
>> Troubleshoot faster and improve end-user experience. Signup Now!
>> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
>> _______________________________________________
>> Hol-developers mailing list
>> Hol...@li...
>> https://lists.sourceforge.net/lists/listinfo/hol-developers
>>
>
>
>
> --
>
>
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
>
>
> ------------------------------------------------------------------------------
> What NetFlow Analyzer can do for you? Monitors network bandwidth and
> traffic
> patterns at an interface-level. Reveals which users, apps, and protocols
> are
> consuming the most bandwidth. Provides multi-vendor support for NetFlow,
> J-Flow, sFlow and other flows. Make informed decisions using capacity
> planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
> _______________________________________________
> Hol-developers mailing list
> Hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-developers
>
>

The dependent rewriting tactics are documented, as much as they are, in
comments at the beginning of dep_rewrite.sig. These comments are copied
below.

The tactics are meant to be deft, quick, and light-weight, and to make
proofs more robust under normal proof evolution, by reducing the number of
explicit terms that are needed in the tactic. These are much less
sophisticated tools than the HOL simplifier, but may be easier to control
when one just wants to apply a particular implication theorem to an
assumption and the goal.

Perhaps the text below could be adapted into a better form of
documentation. What would people like?

Peter

(* ================================================================== *)
(* ================================================================== *)
(*                     DEPENDENT REWRITING TACTICS                    *)
(* ================================================================== *)
(* ================================================================== *)
(*                                                                    *)
(* This file contains new tactics for dependent rewriting,            *)
(* a generalization of the rewriting tactics of standard HOL.         *)
(*                                                                    *)
(* The main tactics are named DEP_REWRITE_TAC[thm1,...], etc., with   *)
(* the standard variations (PURE,ONCE,ASM).  In addition, tactics     *)
(* with LIST instead of ONCE are provided, making 12 tactics in all.  *)
(*                                                                    *)
(* The argument theorems thm1,... are typically implications.         *)
(* These tactics identify the consequents of the argument theorems,   *)
(* and attempt to match these against the current goal.  If a match   *)
(* is found, the goal is rewritten according to the matched instance  *)
(* of the consequent, after which the corresponding hypotheses of     *)
(* the argument theorems are added to the goal as new conjuncts on    *)
(* the left.                                                          *)
(*                                                                    *)
(* Care needs to be taken that the implications will match the goal   *)
(* properly, that is, instances where the hypotheses in fact can be   *)
(* proven.  Also, even more commonly than with REWRITE_TAC,           *)
(* the rewriting process may diverge.                                 *)
(*                                                                    *)
(* Each implication theorem for rewriting may have a number of layers *)
(* of universal quantification and implications.  At the bottom of    *)
(* these layers is the base, which will either be an equality, a      *)
(* negation, or a general term.  The pattern for matching will be     *)
(* the left-hand-side of an equality, the term negated of a negation, *)
(* or the term itself in the third case.  The search is top-to-bottom,*)
(* left-to-right, depending on the quantifications of variables.      *)
(*                                                                    *)
(* To assist in focusing the matching to useful cases, the goal is    *)
(* searched for a subterm matching the pattern.  The matching of the  *)
(* pattern to subterms is performed by higher-order matching, so for  *)
(* example, ``!x. P x`` will match the term ``!n. (n+m) < 4*n``.      *)
(*                                                                    *)
(* The argument theorems may each be either an implication or not.    *)
(* For those which are implications, the hypotheses of the instance   *)
(* of each theorem which matched the goal are added to the goal as    *)
(* conjuncts on the left side.  For those argument theorems which     *)
(* are not implications, the goal is simply rewritten with them.      *)
(* This rewriting is also higher order.                               *)
(*                                                                    *)
(* Deep inner universal quantifications of consequents are supported. *)
(* Thus, an argument theorem like EQ_LIST:                            *)
(* |- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==>                    *)
(*                  (CONS h1 l1 = CONS h2 l2))                        *)
(* before it is used, is internally converted to appear as            *)
(* |- !h1 h2 l1 l2. (h1 = h2) /\ (l1 = l2) ==>                        *)
(*                  (CONS h1 l1 = CONS h2 l2)                         *)
(*                                                                    *)
(* As much as possible, the newly added hypotheses are analyzed to    *)
(* remove duplicates; thus, several theorems with the same            *)
(* hypothesis, or several uses of the same theorem, will generate     *)
(* a minimal additional proof burden.                                 *)
(*                                                                    *)
(* The new hypotheses are added as conjuncts rather than as a         *)
(* separate subgoal to reduce the user's burden of subgoal splits     *)
(* when creating tactics to prove theorems.  If a separate subgoal    *)
(* is desired, simply use CONJ_TAC after the dependent rewriting to   *)
(* split the goal into two, where the first contains the hypotheses   *)
(* and the second contains the rewritten version of the original      *)
(* goal.                                                              *)
(*                                                                    *)
(* The tactics including PURE in their name will only use the         *)
(* listed theorems for all rewriting; otherwise, the standard         *)
(* rewrites are used for normal rewriting, but they are not           *)
(* considered for dependent rewriting.                                *)
(*                                                                    *)
(* The tactics including ONCE in their name attempt to use each       *)
(* theorem in the list, only once, in order, left to right.           *)
(* The hypotheses added in the process of dependent rewriting are     *)
(* not rewritten by the ONCE tactics.  This gives a more restrained   *)
(* version of dependent rewriting.                                    *)
(*                                                                    *)
(* The tactics with LIST take a list of lists of theorems, and        *)
(* uses each list of theorems once in order, left-to-right.  For      *)
(* each list of theorems, the goal is rewritten as much as possible,  *)
(* until no further changes can be achieved in the goal.  Hypotheses  *)
(* are collected from all rewriting and added to the goal, but they   *)
(* are not themselves rewritten.                                      *)
(*                                                                    *)
(* The tactics without ONCE or LIST attempt to reuse all theorems     *)
(* repeatedly, continuing to rewrite until no changes can be          *)
(* achieved in the goal.  Hypotheses are rewritten as well, and       *)
(* their hypotheses as well, ad infinitum.                            *)
(*                                                                    *)
(* The tactics with ASM in their name add the assumption list to      *)
(* the list of theorems used for dependent rewriting.                 *)
(*                                                                    *)
(* There are also three more general tactics provided,                *)
(* DEP_FIND_THEN, DEP_ONCE_FIND_THEN, and DEP_LIST_FIND_THEN,         *)
(* from which the others are constructed.                             *)
(*                                                                    *)
(* The differences among these is that DEP_ONCE_FIND_THEN uses        *)
(* each of its theorems only once, in order left-to-right as given,   *)
(* whereas DEP_FIND_THEN continues to reuse its theorems repeatedly   *)
(* as long as forward progress and change is possible.  In contrast   *)
(* to the others, DEP_LIST_FIND_THEN takes as its argument a list     *)
(* of lists of theorems, and processes these in order, left-to-right. *)
(* For each list of theorems, the goal is rewritten as many times     *)
(* as they apply.  The hypotheses for all these rewritings are        *)
(* collected into one set, added to the goal after all rewritings.    *)
(*                                                                    *)
(* DEP_ONCE_FIND_THEN and DEP_LIST_FIND_THEN will not attack the      *)
(* hypotheses generated as a byproduct of the dependent rewriting;    *)
(* in contrast, DEP_FIND_THEN will.  DEP_ONCE_FIND_THEN and           *)
(* DEP_LIST_FIND_THEN might be fruitfully applied again to their      *)
(* results; DEP_FIND_THEN will complete any possible rewriting,       *)
(* and need not be reapplied.                                         *)
(*                                                                    *)
(* These take as argument a thm_tactic, a function which takes a      *)
(* theorem and yields a tactic.  It is this which is used to apply    *)
(* the instantiated consequent of each successfully matched           *)
(* implication to the current goal.  Usually this is something like   *)
(* (fn th => REWRITE_TAC[th]), but the user is free to supply any     *)
(* thm_tactic he wishes.                                              *)
(*                                                                    *)
(* One significant note: because of the strategy of adding new        *)
(* hypotheses as conjuncts to the current goal, it is not fruitful    *)
(* to add *any* new assumptions to the current goal, as one might     *)
(* think would happen from using, say, ASSUME_TAC.                    *)
(*                                                                    *)
(* Rather, any such new assumptions introduced by thm_tactic are      *)
(* specifically removed.  Instead, one might wish to try MP_TAC,      *)
(* which will have the effect of ASSUME_TAC and then undischarging    *)
(* that assumption to become an antecedent of the goal.  Other        *)
(* thm_tactics may be used, and they may even convert the single      *)
(* current subgoal into multiple subgoals.  If this happens, it is    *)
(* fine, but note that the control strategy of DEP_FIND_THEN will     *)
(* continue to attack only the first of the multiple subgoals.        *)
(*                                                                    *)
(* ================================================================== *)
(* ================================================================== *)

On Mon, Feb 22, 2016 at 1:00 AM, Michael Norrish <
Mic...@ni...> wrote:

> If it's going to that "public", it would be nice if the main entry-points
> were documented.
>
> Michael
>
> > On 22 Feb 2016, at 16:21, Ramana Kumar <Ram...@cl...>
> wrote:
> >
> > What needs to be documented? I think I just meant put an "open
> > dep_rewrite" into bossLib.
> >
> > On 22 February 2016 at 11:19, Michael Norrish
> > <Mic...@ni...> wrote:
> >> Please document somewhere, but yes.
> >>
> >> Michael
> >>
> >>> On 22 Feb 2016, at 09:24, Ramana Kumar <Ram...@cl...>
> wrote:
> >>>
> >>> So, yes?
> >>>
> >>> On 2 February 2016 at 15:51, Ramana Kumar <Ram...@cl...>
> wrote:
> >>>> On 2 February 2016 at 15:04, Michael Norrish <
> Mic...@ni...>
> >>>> wrote:
> >>>>>
> >>>>> Don't know.
> >>>>>
> >>>>> Is it clearly adding functionality we don't have any other way?
> >>>>
> >>>>
> >>>> Yes, I think so. The other way to get the functionality is cumbersome:
> >>>> abbreviate lots of your goal and try to instantiate the dependent
> rewrite
> >>>> theorem manually.
> >>>>
> >>>>>
> >>>>>
> >>>>> Is it big (makes a difference to Moscow ML); does it contaminate the
> >>>>> environment at all (declares new constants; adjusts grammars;
> adjusts other
> >>>>> global elements of the system)?
> >>>>
> >>>>
> >>>> It doesn't touch the logical environment, and I don't think it's very
> big.
> >>>>
> >>>> Implicational rewriting (issue #160) would be better, but we don't
> have
> >>>> that.
> >>>>
> >>>>>
> >>>>>
> >>>>> Michael
> >>>>>
> >>>>> On 2 Feb 2016, at 12:17, Ramana Kumar <Ram...@cl...>
> wrote:
> >>>>>
> >>>>> Tap tap tap... is this thing on?
> >>>>>
> >>>>> On 22 January 2016 at 17:56, Ramana Kumar <Ram...@cl...
> >
> >>>>> wrote:
> >>>>>>
> >>>>>> Would there be any harm in adding dep_rewrite to the standard set of
> >>>>>> libraries that are loaded by default? (Similarly to how
> quantHeuristicsLib
> >>>>>> was added some time recently.)
> >>>>>
> >>>>>
> >>>>>
> >>>>>
> ------------------------------------------------------------------------------
> >>>>> Site24x7 APM Insight: Get Deep Visibility into Application
> Performance
> >>>>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> >>>>> Monitor end-to-end web transactions and take corrective actions now
> >>>>> Troubleshoot faster and improve end-user experience. Signup Now!
> >>>>>
> >>>>>
> http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140_______________________________________________
> >>>>> Hol-developers mailing list
> >>>>> Hol...@li...
> >>>>> https://lists.sourceforge.net/lists/listinfo/hol-developers
> >>>>>
> >>>>>
> >>>>>
> >>>>> ________________________________
> >>>>>
> >>>>> The information in this e-mail may be confidential and subject to
> legal
> >>>>> professional privilege and/or copyright. National ICT Australia
> Limited
> >>>>> accepts no liability for any damage caused by this email or its
> attachments.
> >>>>
> >>>>
> >>
> >>
> >> ________________________________
> >>
> >> The information in this e-mail may be confidential and subject to legal
> professional privilege and/or copyright. National ICT Australia Limited
> accepts no liability for any damage caused by this email or its attachments.
> >>
> >>
> ------------------------------------------------------------------------------
> >> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> >> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> >> Monitor end-to-end web transactions and take corrective actions now
> >> Troubleshoot faster and improve end-user experience. Signup Now!
> >> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
> >> _______________________________________________
> >> hol-info mailing list
> >> hol...@li...
> >> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
> ------------------------------------------------------------------------------
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
> _______________________________________________
> Hol-developers mailing list
> Hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-developers
>

-- 

"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)

2001	Jan	Feb	Mar	Apr	May	Jun	Jul	Aug	Sep	Oct (74)	Nov (85)	Dec (42)
2002	Jan (30)	Feb (6)	Mar (34)	Apr (53)	May (30)	Jun (25)	Jul (17)	Aug (12)	Sep (4)	Oct	Nov (2)	Dec (6)
2003	Jan (17)	Feb (7)	Mar (25)	Apr (9)	May (17)	Jun (32)	Jul (10)	Aug (1)	Sep (2)	Oct (15)	Nov (5)	Dec (2)
2004	Jan (22)	Feb (1)	Mar (1)	Apr	May (14)	Jun (7)	Jul (18)	Aug (3)	Sep	Oct (14)	Nov (7)	Dec (5)
2005	Jan (17)	Feb (19)	Mar (18)	Apr (23)	May (8)	Jun (8)	Jul (11)	Aug (23)	Sep (11)	Oct (2)	Nov (32)	Dec (3)
2006	Jan	Feb (14)	Mar (3)	Apr (5)	May (37)	Jun (9)	Jul (5)	Aug (37)	Sep (54)	Oct (28)	Nov (12)	Dec (8)
2007	Jan (28)	Feb (2)	Mar (15)	Apr (6)	May (9)	Jun (11)	Jul (11)	Aug (7)	Sep (4)	Oct (24)	Nov (6)	Dec (3)
2008	Jan (3)	Feb (3)	Mar (12)	Apr (13)	May (13)	Jun (2)	Jul (11)	Aug (25)	Sep (3)	Oct (12)	Nov	Dec
2009	Jan (11)	Feb (4)	Mar (2)	Apr (13)	May (16)	Jun (36)	Jul (45)	Aug (8)	Sep (47)	Oct (8)	Nov (3)	Dec (6)
2010	Jan (25)	Feb (5)	Mar (21)	Apr (19)	May (2)	Jun (10)	Jul (8)	Aug (1)	Sep (9)	Oct (6)	Nov (2)	Dec (1)
2011	Jan (4)	Feb	Mar	Apr (25)	May (11)	Jun (1)	Jul	Aug (8)	Sep (14)	Oct (2)	Nov	Dec
2012	Jan	Feb (1)	Mar (9)	Apr (18)	May	Jun (4)	Jul (2)	Aug (2)	Sep (10)	Oct (18)	Nov (4)	Dec (1)
2013	Jan	Feb (5)	Mar (1)	Apr	May	Jun	Jul	Aug (5)	Sep	Oct	Nov	Dec
2014	Jan	Feb (3)	Mar	Apr	May (1)	Jun (2)	Jul (2)	Aug (9)	Sep	Oct (15)	Nov (5)	Dec (1)
2015	Jan (7)	Feb	Mar	Apr (1)	May	Jun (1)	Jul (5)	Aug (8)	Sep (3)	Oct (13)	Nov	Dec (14)
2016	Jan (24)	Feb (7)	Mar (1)	Apr (13)	May (13)	Jun (5)	Jul	Aug (2)	Sep (1)	Oct	Nov	Dec
2017	Jan	Feb (2)	Mar	Apr	May	Jun	Jul	Aug	Sep	Oct (3)	Nov	Dec (1)
2018	Jan	Feb	Mar	Apr	May (1)	Jun	Jul	Aug	Sep	Oct	Nov	Dec (5)
2019	Jan (2)	Feb	Mar	Apr	May	Jun	Jul	Aug	Sep	Oct	Nov	Dec
2021	Jan	Feb	Mar	Apr	May	Jun (1)	Jul	Aug	Sep	Oct	Nov	Dec

hol-developers Mailing List for HOL theorem-proving system

hol-developers — For technical implementation-level discussions of the HOL system.