If you want to see the stored rule induction principles, you might use:
ThmSetData.all_data "rule_induction";
Or
IndDefLib.thy_rule_inductions "list";
where you get to provide the theory name.
Michael
From: Thomas Tuerk <tho...@tuerk-brechen.de>
Date: Thursday, 19 January 2017 at 03:22
To: "Chun Tian (binghe)" <binghe.l...@gmail.com>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] How to prove this theorem about relations?
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<mailto: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
--
---
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
