Add theorems for relations and bisimulations

[FieryIceStickie]

Adds:

• Cases and induction theorems for bisimulationScript's ETS
• Theorems for BISIM_REL for easy conversion for a particular transition system to complete the existing set of theorems, and a WBISIM theorem
• Theorems for interactions between RSUBSET, RUNION, RINTER, and inv, to allow for point free reasoning in proofs
• Definitions and theorems involving relation transformers: rmonotone, rpreserves, and is_closure_op (links together things like symmetric and SC)

Last three definitions are for the final theorem

Theorem RMONOTONE_IMP_CLOSURE_RSUBSET:
  is_closure_op f C ∧ rmonotone b ∧ rpreserves f b ==> C (b R) ⊆ᵣ b (C R)

which I needed for a proof.

Some theorems involving set theory constructs (reflexive and transitive are sets for example) were moved to pred_setScript.sml

[binghe]

Many new theorems could have toplevel unversal quantifiers (some already have, and the style is not consistant). Maybe these quantifiers are not needed when the theorems are used by MATCH_MP_TAC but making calling Q.SPECL harder (need to GEN_ALL first).

Treating predicates like reflexive, symmetric as sets of relations seem unnecessary in proving the main results, i.e. theorems like equivalence_thm should be avoided and gives no new value. This style really belongs to set_relationTheory.

[FieryIceStickie]

Many new theorems could have toplevel unversal quantifiers (some already have, and the style is not consistant). Maybe these quantifiers are not needed when the theorems are used by MATCH_MP_TAC but making calling Q.SPECL harder (need to GEN_ALL first).

I've added universal quantifiers to the theorems now.

Treating predicates like reflexive, symmetric as sets of relations seem unnecessary in proving the main results, i.e. theorems like equivalence_thm should be avoided and gives no new value. This style really belongs to set_relationTheory.

The reason why I added equivalence_thm was because I needed it in the proof of is_closure_op_equivalence_EQC, because the proof is applying is_closure_inter twice so I needed to write equivalence in that shape. I could move those theorems to set_relationTheory if that's preferable.

[binghe]

Treating predicates like reflexive, symmetric as sets of relations seem unnecessary in proving the main results, i.e. theorems like equivalence_thm should be avoided and gives no new value. This style really belongs to set_relationTheory.

The reason why I added equivalence_thm was because I needed it in the proof of is_closure_op_equivalence_EQC, because the proof is applying is_closure_inter twice so I needed to write equivalence in that shape. I could move those theorems to set_relationTheory if that's preferable.

How about mark equivalence_thm as a [local] theorem? I doubt anyone else may need it.

P. S. Note that relations in set_relationTheory have different type ('a # 'a -> bool instead of 'a -> 'a -> bool), so are contants like reflexive in set_relationTheory. So you can't simply move your theorems to it without big proof changes. And bisimulationTheory builds earlier than set_relation, thus it cannot open it.

[FieryIceStickie]

How about mark equivalence_thm as a [local] theorem? I doubt anyone else may need it.

P. S. Note that relations in set_relationTheory have different type ('a # 'a -> bool instead of 'a -> 'a -> bool), so are contants like reflexive in set_relationTheory. So you can't simply move your theorems to it without big proof changes. And bisimulationTheory builds earlier than set_relation, thus it cannot open it.

I've now removed equivalence_thm.

[mn200]

Thanks for all this work! One last request: please describe the new constants in the relevant section of the Description manual. Edit the theories.smd file in the right place, and use a selection of ##thm commands to illustrate the important features.