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
> [email protected]
> 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.
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
