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