Re: [Hol-info] How to prove this theorem about relations?

[Michael.Norrish]

Note that the cases theorem does not capture “leastness”.  A coinductive 
definition of the same relation would give you the same cases theorem.  The 
cases theorem is just giving you the fix-point property.

One easy example for thinking about these sorts of things is lists.  Imagine 
you have:

  isAList l <=> l = [] \/ ?h t. l = h::t /\ isAList t

(where l ranges over a type large enough to encompass lists and lazy lists 
both, and the isAList predicate is identifying the appropriate subsets of that 
type).

If the cases theorem is true for algebraic and co-algebraic lists then 
leastness and greatness must be captured elsewhere.  In fact, leastness is 
captured by the induction principle which says

  P [] /\ (!h t. P t ==> P(h::t)) ==> !l. isAList l ==> P l

Michael


From: "Chun Tian (binghe)" 
Date: Wednesday, 18 January 2017 at 21:58
To: hol-info 
Subject: [Hol-info] How to prove this theorem about relations?

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

Re: [Hol-info] How to prove this theorem about relations?

[Michael.Norrish]

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 
Date: Thursday, 19 January 2017 at 03:22
To: "Chun Tian (binghe)" 
Cc: hol-info 
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 
> 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 
> 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 

Re: [Hol-info] How to prove this theorem about relations?

[Chun Tian (binghe)]

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

Re: [Hol-info] How to prove this theorem about relations?

[Thomas Tuerk]

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

Re: [Hol-info] How to prove this theorem about relations?

[Thomas Tuerk]

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

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Chun Tian (binghe)]

Hi Makarius,

Yeah, this is why I never succeeded in building PolyML on Windows in Cygwin
or MinGW.  When the building process stopped at some assembly code files, I
thought they're for Microsoft compilers only.  I don't believe PolyML
depends on any deep GCC feature which is only available in old versions,
because PolyML builds correctly on Linux and Mac using whatever versions of
GCC.  PolyML maintainers may be interested enough to fix the building
issues, if both HOL-4 and Isabelle want to have Windows versions based on
easily build-able PolyML.

And thank you very much for pointing out the hidden Mercurial repository of
Isabelle [1] ^_^ Now I can see how "active" it is for a "not dying" theorem
prover: stable 10-20 code commits on everyday basis, and new theories keep
going into core Isabelle libraries.

Regards,

Chun Tian

[1] hg clone http://isabelle.in.tum.de/repos/isabelle/


On 18 January 2017 at 11:54, Makarius  wrote:

> On 17/01/17 15:24, Chun Tian (binghe) wrote:
> > Sorry, I re-checked my Isabelle environment and found that the PolyML in
> > Isabelle is actually built by GCC (mingw versions), so my statement
> > about "PolyML cannot be built in ..." was completely wrong. The rest
> > ideas should still hold.
>
> It is indeed built with MinGW, but that is very difficult to do. See
> http://isabelle.in.tum.de/repos/isabelle/raw-file/
> Isabelle2016-1/Admin/polyml/INSTALL-MinGW
> which is just a reminder for me for the precise versions need to be
> used. Otherwise it won't work.
>
> Maybe we can open a discussion on the Poly/ML mailing list, if this
> rather old version of gcc on MinGW is still needed, or if things can be
> updated and simplified.
>
>
> Concerning system structures in ML, see also:
>
> http://isabelle.in.tum.de/repos/isabelle/raw-file/
> Isabelle2016-1/src/Pure/ML/ml_system.ML
>
> http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/src/Pure/
> System/bash.ML
>
> Here the bash.exe is the one from Cygwin -- that is required for add-on
> tools of Isabelle.
>
>
> Makarius
>
>


-- 
---

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

Re: [Hol-info] How to prove this theorem about relations?

[Thomas Tuerk]

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

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Makarius]

On 17/01/17 15:24, Chun Tian (binghe) wrote:
> Sorry, I re-checked my Isabelle environment and found that the PolyML in
> Isabelle is actually built by GCC (mingw versions), so my statement
> about "PolyML cannot be built in ..." was completely wrong. The rest
> ideas should still hold.

It is indeed built with MinGW, but that is very difficult to do. See
http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/Admin/polyml/INSTALL-MinGW
which is just a reminder for me for the precise versions need to be
used. Otherwise it won't work.

Maybe we can open a discussion on the Poly/ML mailing list, if this
rather old version of gcc on MinGW is still needed, or if things can be
updated and simplified.


Concerning system structures in ML, see also:

http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/src/Pure/ML/ml_system.ML

http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/src/Pure/System/bash.ML

Here the bash.exe is the one from Cygwin -- that is required for add-on
tools of Isabelle.


Makarius


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

[Hol-info] How to prove this theorem about relations?

[Chun Tian (binghe)]

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