[isabelle] calculational reasoning for transitive relations

Joachim Breitner wrote: 
>> Also, it would be nice if the transitivity rules for <o, <=o, =o were
>> set up to work with Isar’s "also... also... finally".

Good point.  I actually though about this too, but did not investigate if it is 

Now I see that a paper on the topic, 


states that 

"Certainly, creative users of Isabelle/Isar may
invent further ways of calculational reasoning at any time."

It was not clear to me if this applies to the following situation: 
any combination of equalities and a relation proven to be transitive.  

Best regards, 

----- Original Message ----
From: Joachim Breitner <mail at joachim-breitner.de>
To: Andrei Popescu <uuomul at yahoo.com>
Cc: cl-isabelle-users at lists.cam.ac.uk
Sent: Wed, September 22, 2010 2:56:48 AM
Subject: Re:  FuncSet without extensional? (Joachim Breitner)

Hi Andrei,

Am Sonntag, den 19.09.2010, 20:20 -0700 schrieb Andrei Popescu:
> >> BTW, are there already theories about uncountable sets? I?d need, as a
> >> lemma, the fact that the M* (the set of finite words) of a uncountably
> >> infinte set M has the same cardinality.
> Actually, quite a bit of the ZF theory of cardinals can be done in HOL.  
> I have already set the basis of such a theory: it is in the Isabelle AFP, and 
> fairly well documented.  
> http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml
> Your lemma is stated there in the theory Cardinal_order_relation, in subsection 
> "Cardinals versus lists", as 
> List_infinite_bij_betw
> (NB: it holds for any infinite set, including the countably infinite ones.)

just FYI: I finished my results using your theory and committed my
changes to the AFP mercurial repository. Thanks, it was exactly what I
was expecting.

In case you update your AFP entry to use List.lists instead of your own
List definition, my theory will probably not compile any more. You can
fix that by removing the lines:

moreover (* Remove this if Ordinals_and_Cardinals uses List.lists as well *)
have "|lists ((UNIV::bool set)\<times>X)| = |List ((UNIV::bool set)\<times>X)|"
  by (simp add: List_def lists_eq_set)

from Free-Groups/Isomorphisms.thy

Also, it would be nice if the transitivity rules for <o, <=o, =o were
set up to work with Isar’s "also... also... finally". This would make my
lemma "free_group_card_infinite" a bit more straight-forward to
implement... but no big deal.

Thanks for your theory!

Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.