Hi again,
It seems that my original question has a positive answer. I got a proof from
Thomas Tuerk saying:
val BIGUNION_IMAGE_COUNT_IMP_UNIV =
⊢ ∀f g.
(∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ⇒
(BIGUNION (IMAGE f 핌(:num)) = BIGUNION (IMAGE g 핌(:num)))
that’s amazing...
—Chun
(* provided by Thomas Tuerk, amazing! *)
val BIGUNION_IMAGE_COUNT_IMP_UNIV = store_thm
("BIGUNION_IMAGE_COUNT_IMP_UNIV",
``!f g. (!n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ==>
(BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``,
(* proof *)
`!f g. (!n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ==>
(BIGUNION (IMAGE f UNIV) SUBSET BIGUNION (IMAGE g UNIV))`
suffices_by PROVE_TAC [SUBSET_ANTISYM]
>> REWRITE_TAC [SUBSET_DEF]
>> REPEAT STRIP_TAC
>> rename1 `e IN BIGUNION _`
>> Know `?n. e IN BIGUNION (IMAGE f (count n))`
>- (FULL_SIMP_TAC std_ss [IN_BIGUNION, IN_IMAGE, PULL_EXISTS, IN_COUNT] \\
rename1 `e IN f n'` \\
Q.EXISTS_TAC `SUC n'` \\
Q.EXISTS_TAC `n'` \\
ASM_SIMP_TAC arith_ss [])
>> STRIP_TAC
>> `e IN BIGUNION (IMAGE g (count n))` by PROVE_TAC []
>> FULL_SIMP_TAC std_ss [IN_BIGUNION, IN_IMAGE, PULL_EXISTS, IN_UNIV]
>> METIS_TAC []);
> Il giorno 16 set 2018, alle ore 08:37, Chun Tian (binghe)
> ha scritto:
>
> Cancel this question. Finally I found a way to reduce the original goal to
>
> ∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))
>
> but it deeply relies on the definition of g, otherwise it seems impossible.
> Sorry for disturbing.
>
> —Chun
>
>> Il giorno 15 set 2018, alle ore 22:26, Chun Tian (binghe)
>> ha scritto:
>>
>> Hi,
>>
>> I have a need to prove that, for two certain functions f, (g :num->’a set)
>>
>> BIGUNION (IMAGE f 핌(:num)) = BIGUNION (IMAGE g 핌(:num))
>>
>> Following its informal proof, it seems only possible to prove the following
>> result (by induction) first:
>>
>> !(n :num). BIGUNION (IMAGE f (count n)) = BIGUNION (IMAGE g (count n))
>>
>> but once I got this intermediate result, how I can reach to the original
>> statement? Is there any other assumption needed for going from finite to
>> infinite union?
>>
>> Thanks,
>>
>> Chun Tian
>>
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
