Hi Chun,
TypeBase stores information about algebraic datatypes. So, you won't
find information for your inductive relations or recursive functions in
there. Use
TypeBasePure.listItems (TypeBase.theTypeBase())
to get an idea what types are currently in the TypeBase. I found the
reference to "Induct_on" in the description in section 5.6.1 on page
187. I was not aware of this feature. I looked up how it is implemented.
In "src/basicProof/BasicProvers.sml" line 259 you can see that the
TypeBase is not used. Instead, "src/IndDef/IndDefLib.sig" defines a map
"rule_induction_map" that contains these induction theorems.
If you want to get your hands on the strong induction theorem, I would
use DB.fetch, i.e.
DB.fetch "-" "R_strongind"
Cheers
Thomas
On 18.01.2017 14:34, Chun Tian (binghe) wrote:
> Sorry, one more question here: how to fetch from TypeBase the
> induction theorems generated by relation?
>
> I recall in The HOL System DESCRIPTION, section 5.6.1 (Proofs with
> Inductive Relations), it says that we can use (Induct_on `R`) or
> (Induct_on `R x y`) to do inductions on relation R, and internally it
> actually calls (HO_MATCH_MP_TAC R_strongind). And the information is
> taken from TypeBase (I can't find a exact reference for this, but
> sometimes when I failed to call Induct_on, it said there's no such
> types in TypeBase).
>
> Still using my above example, if I try the type of my relation subF, I
> got nothing, and errors:
>
> > TypeBase.fetch ``:'a form -> 'a form -> bool``;
> val it = NONE: tyinfo option
>
> > TypeBase.induction_of ``:'a form -> 'a form -> bool``;
> Exception-
> HOL_ERR
> {message = "unable to find \"min$fun\" in the TypeBase",
> origin_function = "induction_of", origin_structure = "TypeBase"}
> raised
>
>
> On 18 January 2017 at 13:55, Thomas Tuerk <tho...@tuerk-brechen.de
> <mailto:tho...@tuerk-brechen.de>> wrote:
>
> 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
>> <tho...@tuerk-brechen.de> 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
>>> hol-info@lists.sourceforge.net
>>> <mailto:hol-info@lists.sourceforge.net>
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>> <https://lists.sourceforge.net/lists/listinfo/hol-info>
>>
>> --
>> ---
>> Chun Tian (binghe)
>> University of Bologna (Italy)
>
> --
> ---
> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
