3 Author: Gerwin Klein |
3 Author: Gerwin Klein |
4 *) |
4 *) |
5 |
5 |
6 header {* \isaheader{Example Welltypings}\label{sec:BVExample} *} |
6 header {* \isaheader{Example Welltypings}\label{sec:BVExample} *} |
7 |
7 |
8 theory BVExample imports JVMListExample BVSpecTypeSafe JVM ExecutableSet begin |
8 theory BVExample |
|
9 imports JVMListExample BVSpecTypeSafe JVM ExecutableSet |
|
10 begin |
9 |
11 |
10 text {* |
12 text {* |
11 This theory shows type correctness of the example program in section |
13 This theory shows type correctness of the example program in section |
12 \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by |
14 \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by |
13 explicitly providing a welltyping. It also shows that the start |
15 explicitly providing a welltyping. It also shows that the start |
113 apply simp |
115 apply simp |
114 done |
116 done |
115 |
117 |
116 lemma field_val [simp]: |
118 lemma field_val [simp]: |
117 "field (E, list_name) val_name = Some (list_name, PrimT Integer)" |
119 "field (E, list_name) val_name = Some (list_name, PrimT Integer)" |
118 apply (unfold field_def) |
120 apply (unfold TypeRel.field_def) |
119 apply (insert class_list) |
121 apply (insert class_list) |
120 apply (unfold list_class_def) |
122 apply (unfold list_class_def) |
121 apply (drule fields_rec_lemma [OF _ wf_subcls1_E]) |
123 apply (drule fields_rec_lemma [OF _ wf_subcls1_E]) |
122 apply simp |
124 apply simp |
123 done |
125 done |
124 |
126 |
125 lemma field_next [simp]: |
127 lemma field_next [simp]: |
126 "field (E, list_name) next_name = Some (list_name, Class list_name)" |
128 "field (E, list_name) next_name = Some (list_name, Class list_name)" |
127 apply (unfold field_def) |
129 apply (unfold TypeRel.field_def) |
128 apply (insert class_list) |
130 apply (insert class_list) |
129 apply (unfold list_class_def) |
131 apply (unfold list_class_def) |
130 apply (drule fields_rec_lemma [OF _ wf_subcls1_E]) |
132 apply (drule fields_rec_lemma [OF _ wf_subcls1_E]) |
131 apply (simp add: name_defs distinct_fields [symmetric]) |
133 apply (simp add: name_defs distinct_fields [symmetric]) |
132 done |
134 done |