Hi,
glad I could be of help.
I forgot to mention TypeBase. This is where such theorems about a type
are collected. It is used by tools like the case or induct tactics. So,
some other nice way of getting such theorems is
TypeBase.fetch ``:'a form``
or specialized ones via
TypeBase.distinct_of ``:'a form``
TypeBase.one_one_of ``:'a form``
...
Best
Thomas
On 18.01.2017 13:22, Chun Tian (binghe) wrote:
> Hi Thomas,
>
> Oh my god ... I've learnt so much from each line of your reply. Thank
> you so much!
>
> Best regards,
>
> Chun
>
>
> On 18 January 2017 at 12:53, Thomas Tuerk <[email protected]
> <mailto:[email protected]>> wrote:
>
> Hi Chun,
>
> you are on the right way with the cases theorem. Essentially you
> need to rewrite once with it. Then you end up with
>
> ∀A a.(atom a = A) ∨ (∃B C. (atom a = dot B C) ∧ subF A B) ⇒ (A =
> atom a)
>
> Now you need to use the fact that "atom _ = dot B C" does not
> hold. This distinctiveness is proved by the datatype package, just
> not returned directly. It is stored in the theory. You can fetch
> it via
>
> fetch "-" "form_distinct"
>
> The injectivity of constructors you asked for you get via
>
> fetch "-" "form_11"
>
> Just search for "form" and you get interesting stuff
>
> DB.print_find "form"
>
>
> So your proof might look like
>
> -----------------------------------------
>
> val form_distinct = DB.fetch "-" "form_distinct"
>
> val myTHM = prove(``!A (a:'a). subF A (atom a) ==> (A = atom a)``,
>
> ONCE_REWRITE_TAC [subF_cases] THEN
> SIMP_TAC std_ss [form_distinct])
>
> ---------------------------------------
>
>
> There are other ways of accessing the generated theorems, though.
> Most commonly used, but sometimes doing also extra unwanted stuff
> is the stateful simpset. So something like
>
> SIMP_TAC (srw_ss ()) []
>
> does work as well.
>
> I personally prefer the DatatypeSimps to keep tight control over
> what rewrites I use. This is a highly controversial personal taste
> though.
>
> So, I either use the version above or
>
>
> val form_ss = DatatypeSimps.type_rewrites_ss [``:'a form``]
>
> val myTHM = prove(``!A (a:'a). subF A (atom a) ==> (A = atom a)``,
>
> ONCE_REWRITE_TAC [subF_cases] THEN
> SIMP_TAC (std_ss++form_ss) [])
>
>
> I hope this helps
>
> Thomas
>
>
> On 18.01.2017 11:58, Chun Tian (binghe) wrote:
>> Hi,
>>
>> Sorry for disturbing again, but I met new difficulties when
>> proving theorems about relations.
>>
>> Suppose I have the following simple recursive datatype and a "sub
>> formula" relation about it:
>>
>> val _ = Datatype `form = atom 'a | dot form form`;
>>
>> val (subF_rules, subF_ind, subF_cases) = Hol_reln
>> `(!(A:'a form). subF A A) /\
>> (!(A:'a form) B C. subF A B ==> subF A (dot B C)) `;
>>
>> Now I need to prove this goal: `!A a. subF A (atom a) ==> (A =
>> atom a)`.
>>
>> I have successfully proved some theorems about relations defined
>> by Hol_reln, but this one brings some difficulties that I never
>> met before.
>>
>> The main problem is, "atom" never appears in the definition of
>> Hol_reln, thus I don't have any theorem talking about it.
>>
>> But I recall the fact that, an inductive relation defines the
>> *least* relation satisfying the rules, thus anything undefined is
>> by default false. I believe this fact has been correctly
>> captured by (and only by) subF_cases generated from above
>> Hol_reln definition:
>>
>> val subF_cases =
>> |- ∀a0 a1. subF a0 a1 ⇔ (a1 = a0) ∨ ∃B C. (a1 = dot B C) ∧
>> subF a0 B:
>> thm
>>
>> If I do cases analysis on `A`, I got a seeming good start point:
>>
>> > e (Cases_on `A:'a form`);
>> OK..
>> 2 subgoals:
>> val it =
>> ∀a. subF (dot f f0) (atom a) ⇒ (dot f f0 = atom a)
>> ∀a'. subF (atom a) (atom a') ⇒ (atom a = atom a')
>> 2 subgoals
>> : proof
>>
>> But I still don't know how to prove any of these sub-goals. I
>> have no useful theorems for rewrite or anything else. The
>> relation rules only tells me that, forall A, (subFor A A) is
>> true, but it didn't say anything about the other direction: (subF
>> A B) => A = B (if A and B are both shapes like (atom ...)
>>
>> Also, I even don't know how to prove this fundamental truth about
>> datatypes: ``(atom A) = (atom B) ==> A = B``, again, I have no
>> theorems to use ... because the Datatype definition didn't return
>> anything that I can (directly) use inside a store_thm().
>>
>> On the other side, Coq proves the same theorem quite simply:
>>
>> Lemma subAt :
>> forall (Atoms : Set) (A : Form Atoms) (at_ : Atoms),
>> subFormula A (At at_) -> A = At at_.
>> intros Atoms A at_ H.
>> inversion H.
>> reflexivity.
>> Qed.
>>
>> Need help ...
>>
>> Regards,
>>
>> Chun Tian (binghe)
>> University of Bologna (Italy)
>>
>>
>>
>>
>> ------------------------------------------------------------------------------
>> Check out the vibrant tech community on one of the world's most
>> engaging tech sites, SlashDot.org! http://sdm.link/slashdot
>>
>> _______________________________________________
>> hol-info mailing list
>> [email protected]
>> <mailto:[email protected]>
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>> <https://lists.sourceforge.net/lists/listinfo/hol-info>
>
> --
> ---
> Chun Tian (binghe)
> University of Bologna (Italy)
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
