Hi Thomas,
Thanks for pointing out the related source code! Looking at ML function
Induct_on() and induct_on_type(), it's quite clear what they do exactly.
From the way Induct_on() generating tactics (MAP_FIRST HO_MATCH_MP_TAC
indth ORELSE induct_on_type st ty), I can see that, if the
"rule_induction_map" didn't contain the desired theorem, the function
induct_on_type() will be called next, and if it also fails (which is
most of the case), the final error message will only mention TypeBase,
and this is why I thought the relation induction theorems were also
stored in TypeBase :) Now by looking at all items in the TypeBase using
the way you taught, I see only things defined by HOL Define() for data
types.
Next time I should try to read the source code before raising a question
here :)
Regards,
Chun
Thomas Tuerk wrote:
>
> 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 <[email protected]
>> <mailto:[email protected]>> 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
>>> <[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]
https://lists.sourceforge.net/lists/listinfo/hol-info
