On 03/12/14 13:19, David Sanán wrote: > offtopic, Always I send I message to the mailing list I get > moderator approval message, although I signed up to HOL4 mailing > list with this email address. Is this the normal behaviour??? > Thanks!
At the moment, this is normal for new posters, whether or not they’re subscribed. However, now that you’ve prompted me to think about it at all, I think I can adjust this to be a little less of a barrier. Thanks, Michael > On Mon, Dec 1, 2014 at 7:46 AM, Michael Norrish <michael.norr...@nicta.com.au > <mailto:michael.norr...@nicta.com.au>> wrote: > How are you using the induction theorem? > I think the safest way would be to write > HO_MATCH_MP_TAC ITSET_IND > If that's what you're doing and you're getting the bad free variable, > then I'd > adjust the above to > HO_MATCH_MP_TAC (GEN_ALL ITSET_IND) > I hope this helps, > Michael > On 29/11/14 01:07, David Sanán wrote: > > Hi all, > > I am using ITSET to iteratively apply a function over the elements of a > FMAP > > over the FMAP itself. I need to use induction over ITSET, but with the > current > > definition of ITSET: > > val ITSET_def = > > let open TotalDefn > > in > > tDefine "ITSET" > > `ITSET (s:'a->bool) (b:'b) = > > if FINITE s then > > if s={} then b > > else ITSET (REST s) (f (CHOICE s) b) > > else ARB` > > (WF_REL_TAC `measure (CARD o FST)` THEN > > METIS_TAC [CARD_PSUBSET, REST_PSUBSET]) > > end; > > The induction theorem should look something like > > |- ∀f P. > > (∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒ > > ∀v v1. P v v1 > > Instead, f is free in the induction theorem: > > |- ∀P. > > (∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒ > > ∀v v1. P v v1 > > Then to prove something like > > A b ==> B (ITSET my_function s b), > > after applying induction and stripping I get is something like: > > A b ==> B (ITSET my_function s b) > > ------------------------------------ > > FINITE s ∧ s ≠ ∅ ==> A (f (CHOICE s) h) ==> B (ITSET my_function > (REST s) (f > > (CHOICE s) b)) > > I make a dirty and quick workaround without explicitly defining and > proving the > > induction theorem, redefining ITSET: > > val ITSET_def = > > let open TotalDefn > > in > > tDefine "ITSET" > > `ITSET f (s:'a->bool) (b:'b) = > > if FINITE s then > > if s={} then b > > else ITSET f (REST s) (f (CHOICE s) b) > > else ARB` > > (WF_REL_TAC `measure (CARD o FST o SND)` THEN > > METIS_TAC [CARD_PSUBSET, REST_PSUBSET]) > > end; > > and then f is not free anymore in the induction theorem and then adding > > explicitly to my predicate > > (f=my_function) /\A b ==> B (ITSET my_function s b) > > I can prove my property. > > But of course this is not the ideal case... > > My question, I am missing something here????? > > BTW, I am using HOL4 9. > > Thanks a lot, > > David. > > > ------------------------------------------------------------------------------ > > Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server > > from Actuate! Instantly Supercharge Your Business Reports and Dashboards > > with Interactivity, Sharing, Native Excel Exports, App Integration & > more > > Get technology previously reserved for billion-dollar corporations, FREE > > > http://pubads.g.doubleclick.net/gampad/clk?id=157005751&iu=/4140/ostg.clktrk > > _______________________________________________ > > hol-info mailing list > > hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> > > https://lists.sourceforge.net/lists/listinfo/hol-info > ________________________________ > 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. ------------------------------------------------------------------------------ Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server from Actuate! Instantly Supercharge Your Business Reports and Dashboards with Interactivity, Sharing, Native Excel Exports, App Integration & more Get technology previously reserved for billion-dollar corporations, FREE http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
