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
------------------------------------------------------------------------------
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
