39 |
39 |
40 {\bf lemma} @{text Store_correct}:\\ |
40 {\bf lemma} @{text Store_correct}:\\ |
41 @{thm [display] Store_correct [no_vars]} |
41 @{thm [display] Store_correct [no_vars]} |
42 \medskip |
42 \medskip |
43 |
43 |
44 {\bf lemma} @{text conf_Intg_Integer}:\\ |
44 %removed {\bf lemma} {text conf_Intg_Integer}:\\ |
45 @{thm [display] conf_Intg_Integer [no_vars]} |
45 %removed {\bf lemma} {text Bipush_correct}:\\ |
46 \medskip |
|
47 |
|
48 {\bf lemma} @{text Bipush_correct}:\\ |
|
49 @{thm [display] Bipush_correct [no_vars]} |
|
50 \medskip |
|
51 |
46 |
52 {\bf lemma} @{text NT_subtype_conv}:\\ |
47 {\bf lemma} @{text NT_subtype_conv}:\\ |
53 @{thm [display] NT_subtype_conv [no_vars]} |
48 @{thm [display] NT_subtype_conv [no_vars]} |
54 \medskip |
49 \medskip |
55 |
50 |
56 {\bf lemma} @{text Aconst_null_correct}:\\ |
51 %removed {\bf lemma} {text Aconst_null_correct}:\\ |
57 @{thm [display] Aconst_null_correct [no_vars]} |
52 |
58 \medskip |
|
59 |
|
60 {\bf lemma} @{text Cast_conf2}:\\ |
53 {\bf lemma} @{text Cast_conf2}:\\ |
61 @{thm [display] Cast_conf2 [no_vars]} |
54 @{thm [display] Cast_conf2 [no_vars]} |
62 \medskip |
55 \medskip |
63 |
56 |
64 {\bf lemma} @{text Checkcast_correct}:\\ |
57 {\bf lemma} @{text Checkcast_correct}:\\ |
151 |
144 |
152 *} |
145 *} |
153 |
146 |
154 subsubsection {* Theory Conform *} |
147 subsubsection {* Theory Conform *} |
155 text {* |
148 text {* |
156 {\bf theorem} @{text conf_VoidI}:\\ |
149 %removed {\bf theorem} {text conf_VoidI}:\\ |
157 @{thm [display] conf_VoidI [no_vars]} |
150 |
158 \medskip |
151 %removed {\bf theorem} {text conf_BooleanI}:\\ |
159 |
152 |
160 {\bf theorem} @{text conf_BooleanI}:\\ |
153 %removed {\bf theorem} {text conf_IntegerI}:\\ |
161 @{thm [display] conf_BooleanI [no_vars]} |
|
162 \medskip |
|
163 |
|
164 {\bf theorem} @{text conf_IntegerI}:\\ |
|
165 @{thm [display] conf_IntegerI [no_vars]} |
|
166 \medskip |
|
167 |
154 |
168 {\bf theorem} @{text defval_conf}:\\ |
155 {\bf theorem} @{text defval_conf}:\\ |
169 @{thm [display] defval_conf [no_vars]} |
156 @{thm [display] defval_conf [no_vars]} |
170 \medskip |
157 \medskip |
171 |
158 |
235 |
222 |
236 {\bf lemma} @{text not_Some_eq}:\\ |
223 {\bf lemma} @{text not_Some_eq}:\\ |
237 @{thm [display] not_Some_eq [no_vars]} |
224 @{thm [display] not_Some_eq [no_vars]} |
238 \medskip |
225 \medskip |
239 |
226 |
240 {\bf lemma} @{text lift_top_refl}:\\ |
227 %removed {\bf lemma} @{text lift_top_refl}:\\ |
241 @{thm [display] lift_top_refl [no_vars]} |
228 |
242 \medskip |
229 %removed {\bf lemma} @{text lift_top_trans}:\\ |
243 |
230 |
244 {\bf lemma} @{text lift_top_trans}:\\ |
231 %removed {\bf lemma} @{text lift_top_Err_any}:\\ |
245 @{thm [display] lift_top_trans [no_vars]} |
232 |
246 \medskip |
233 %removed {\bf lemma} @{text lift_top_OK_OK}:\\ |
247 |
234 |
248 {\bf lemma} @{text lift_top_Err_any}:\\ |
235 %removed {\bf lemma} @{text lift_top_any_OK}:\\ |
249 @{thm [display] lift_top_Err_any [no_vars]} |
236 |
250 \medskip |
237 %removed {\bf lemma} @{text lift_top_OK_any}:\\ |
251 |
238 |
252 {\bf lemma} @{text lift_top_OK_OK}:\\ |
239 %removed {\bf lemma} @{text lift_bottom_refl}:\\ |
253 @{thm [display] lift_top_OK_OK [no_vars]} |
240 |
254 \medskip |
241 %removed {\bf lemma} @{text lift_bottom_trans}:\\ |
255 |
242 |
256 {\bf lemma} @{text lift_top_any_OK}:\\ |
243 %removed {\bf lemma} @{text lift_bottom_any_None}:\\ |
257 @{thm [display] lift_top_any_OK [no_vars]} |
244 |
258 \medskip |
245 %removed {\bf lemma} @{text lift_bottom_Some_Some}:\\ |
259 |
246 |
260 {\bf lemma} @{text lift_top_OK_any}:\\ |
247 %removed {\bf lemma} @{text lift_bottom_any_Some}:\\ |
261 @{thm [display] lift_top_OK_any [no_vars]} |
248 |
262 \medskip |
249 %removed {\bf lemma} @{text lift_bottom_Some_any}:\\ |
263 |
250 |
264 {\bf lemma} @{text lift_bottom_refl}:\\ |
|
265 @{thm [display] lift_bottom_refl [no_vars]} |
|
266 \medskip |
|
267 |
|
268 {\bf lemma} @{text lift_bottom_trans}:\\ |
|
269 @{thm [display] lift_bottom_trans [no_vars]} |
|
270 \medskip |
|
271 |
|
272 {\bf lemma} @{text lift_bottom_any_None}:\\ |
|
273 @{thm [display] lift_bottom_any_None [no_vars]} |
|
274 \medskip |
|
275 |
|
276 {\bf lemma} @{text lift_bottom_Some_Some}:\\ |
|
277 @{thm [display] lift_bottom_Some_Some [no_vars]} |
|
278 \medskip |
|
279 |
|
280 {\bf lemma} @{text lift_bottom_any_Some}:\\ |
|
281 @{thm [display] lift_bottom_any_Some [no_vars]} |
|
282 \medskip |
|
283 |
|
284 {\bf lemma} @{text lift_bottom_Some_any}:\\ |
|
285 @{thm [display] lift_bottom_Some_any [no_vars]} |
|
286 \medskip |
|
287 |
|
288 {\bf theorem} @{text sup_ty_opt_refl}:\\ |
251 {\bf theorem} @{text sup_ty_opt_refl}:\\ |
289 @{thm [display] sup_ty_opt_refl [no_vars]} |
252 @{thm [display] sup_ty_opt_refl [no_vars]} |
290 \medskip |
253 \medskip |
291 |
254 |
292 {\bf theorem} @{text sup_loc_refl}:\\ |
255 {\bf theorem} @{text sup_loc_refl}:\\ |
681 |
644 |
682 *} |
645 *} |
683 |
646 |
684 subsubsection {* Theory JBasis *} |
647 subsubsection {* Theory JBasis *} |
685 text {* |
648 text {* |
686 {\bf theorem} @{text image_rev}:\\ |
649 %removed {\bf theorem} {text image_rev}:\\ |
687 @{thm [display] image_rev [no_vars]} |
650 |
688 \medskip |
651 %removed {\bf theorem} {text some_subset_the}:\\ |
689 |
652 |
690 {\bf theorem} @{text some_subset_the}:\\ |
|
691 @{thm [display] some_subset_the [no_vars]} |
|
692 \medskip |
|
693 |
|
694 {\bf theorem} @{text fst_in_set_lemma}:\\ |
653 {\bf theorem} @{text fst_in_set_lemma}:\\ |
695 @{thm [display] fst_in_set_lemma [no_vars]} |
654 @{thm [display] fst_in_set_lemma [no_vars]} |
696 \medskip |
655 \medskip |
697 |
656 |
698 {\bf theorem} @{text unique_Nil}:\\ |
657 {\bf theorem} @{text unique_Nil}:\\ |
709 |
668 |
710 {\bf theorem} @{text unique_map_inj}:\\ |
669 {\bf theorem} @{text unique_map_inj}:\\ |
711 @{thm [display] unique_map_inj [no_vars]} |
670 @{thm [display] unique_map_inj [no_vars]} |
712 \medskip |
671 \medskip |
713 |
672 |
714 {\bf theorem} @{text unique_map_Pair}:\\ |
673 %removed {\bf theorem} {text unique_map_Pair}:\\ |
715 @{thm [display] unique_map_Pair [no_vars]} |
674 |
716 \medskip |
|
717 |
|
718 {\bf theorem} @{text image_cong}:\\ |
675 {\bf theorem} @{text image_cong}:\\ |
719 @{thm [display] image_cong [no_vars]} |
676 @{thm [display] image_cong [no_vars]} |
720 \medskip |
677 \medskip |
721 |
678 |
722 {\bf theorem} @{text unique_map_of_Some_conv}:\\ |
679 %removed {\bf theorem} {text unique_map_of_Some_conv}:\\ |
723 @{thm [display] unique_map_of_Some_conv [no_vars]} |
680 |
724 \medskip |
|
725 |
|
726 {\bf theorem} @{text Ball_set_table}:\\ |
681 {\bf theorem} @{text Ball_set_table}:\\ |
727 @{thm [display] Ball_set_table [no_vars]} |
682 @{thm [display] Ball_set_table [no_vars]} |
728 \medskip |
683 \medskip |
729 |
684 |
730 {\bf theorem} @{text map_of_map}:\\ |
685 {\bf theorem} @{text map_of_map}:\\ |
857 |
812 |
858 {\bf lemma} @{text wtl_method_complete}:\\ |
813 {\bf lemma} @{text wtl_method_complete}:\\ |
859 @{thm [display] wtl_method_complete [no_vars]} |
814 @{thm [display] wtl_method_complete [no_vars]} |
860 \medskip |
815 \medskip |
861 |
816 |
862 {\bf lemma} @{text unique_set}:\\ |
817 %removed {\bf lemma} {text unique_set}:\\ |
863 @{thm [display] unique_set [no_vars]} |
818 |
864 \medskip |
819 %removed {\bf lemma} {text unique_epsilon}:\\ |
865 |
820 |
866 {\bf lemma} @{text unique_epsilon}:\\ |
|
867 @{thm [display] unique_epsilon [no_vars]} |
|
868 \medskip |
|
869 |
|
870 {\bf theorem} @{text wtl_complete}:\\ |
|
871 @{thm [display] wtl_complete [no_vars]} |
821 @{thm [display] wtl_complete [no_vars]} |
872 \medskip |
822 \medskip |
873 |
823 |
874 *} |
824 *} |
875 |
825 |
913 |
863 |
914 {\bf lemma} @{text wtl_method_correct}:\\ |
864 {\bf lemma} @{text wtl_method_correct}:\\ |
915 @{thm [display] wtl_method_correct [no_vars]} |
865 @{thm [display] wtl_method_correct [no_vars]} |
916 \medskip |
866 \medskip |
917 |
867 |
918 {\bf lemma} @{text unique_set}:\\ |
|
919 @{thm [display] unique_set [no_vars]} |
|
920 \medskip |
|
921 |
|
922 {\bf lemma} @{text unique_epsilon}:\\ |
|
923 @{thm [display] unique_epsilon [no_vars]} |
|
924 \medskip |
|
925 |
|
926 {\bf theorem} @{text wtl_correct}:\\ |
868 {\bf theorem} @{text wtl_correct}:\\ |
927 @{thm [display] wtl_correct [no_vars]} |
869 @{thm [display] wtl_correct [no_vars]} |
928 \medskip |
870 \medskip |
929 |
871 |
930 *} |
872 *} |
993 |
935 |
994 {\bf lemma} @{text appStore}:\\ |
936 {\bf lemma} @{text appStore}:\\ |
995 @{thm [display] appStore [no_vars]} |
937 @{thm [display] appStore [no_vars]} |
996 \medskip |
938 \medskip |
997 |
939 |
998 {\bf lemma} @{text appBipush}:\\ |
940 %removed {\bf lemma} {text appBipush}:\\ |
999 @{thm [display] appBipush [no_vars]} |
941 |
1000 \medskip |
942 %removed {\bf lemma} {text appAconst}:\\ |
1001 |
|
1002 {\bf lemma} @{text appAconst}:\\ |
|
1003 @{thm [display] appAconst [no_vars]} |
|
1004 \medskip |
|
1005 |
943 |
1006 {\bf lemma} @{text appGetField}:\\ |
944 {\bf lemma} @{text appGetField}:\\ |
1007 @{thm [display] appGetField [no_vars]} |
945 @{thm [display] appGetField [no_vars]} |
1008 \medskip |
946 \medskip |
1009 |
947 |
1228 |
1163 |
1229 {\bf theorem} @{text unique_fields}:\\ |
1164 {\bf theorem} @{text unique_fields}:\\ |
1230 @{thm [display] unique_fields [no_vars]} |
1165 @{thm [display] unique_fields [no_vars]} |
1231 \medskip |
1166 \medskip |
1232 |
1167 |
1233 {\bf theorem} @{text widen_fields_mono}:\\ |
1168 %removed {\bf theorem} {text widen_fields_mono}:\\ |
1234 @{thm [display] widen_fields_mono [no_vars]} |
|
1235 \medskip |
|
1236 |
1169 |
1237 {\bf theorem} @{text widen_cfs_fields}:\\ |
1170 {\bf theorem} @{text widen_cfs_fields}:\\ |
1238 @{thm [display] widen_cfs_fields [no_vars]} |
1171 @{thm [display] widen_cfs_fields [no_vars]} |
1239 \medskip |
1172 \medskip |
1240 |
1173 |