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