equal
deleted
inserted
replaced
1 theory PIPBasics |
1 theory PIPBasics |
2 imports PIPDefs |
2 imports PIPDefs |
3 begin |
3 begin |
|
4 |
|
5 text {* (* ddd *) |
|
6 Following the HOL convention of {\em definitional extension}, we have |
|
7 given a concise and miniature model of PIP. To assure ourselves of |
|
8 the correctness of this model, we are going to derive a series of |
|
9 expected properties out of it. |
|
10 |
|
11 This file contains the very basic properties, useful for self-assurance, |
|
12 as well as for deriving more advance properties concerning |
|
13 the correctness and implementation of PIP. |
|
14 *} |
|
15 |
4 |
16 |
5 section {* Generic aulxiliary lemmas *} |
17 section {* Generic aulxiliary lemmas *} |
6 |
18 |
7 lemma rel_eqI: |
19 lemma rel_eqI: |
8 assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B" |
20 assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B" |