equal
deleted
inserted
replaced
40 |
40 |
41 lemma list_all' [iff]: |
41 lemma list_all' [iff]: |
42 "list_all' P xs = (\<forall>n < size xs. P (xs!n) n)" |
42 "list_all' P xs = (\<forall>n < size xs. P (xs!n) n)" |
43 by (unfold list_all'_def) (simp add: list_all'_rec) |
43 by (unfold list_all'_def) (simp add: list_all'_rec) |
44 |
44 |
45 lemma list_all_ball: |
|
46 "list_all P xs = (\<forall>x \<in> set xs. P x)" |
|
47 by (induct xs) auto |
|
48 |
|
49 lemma [code]: |
45 lemma [code]: |
50 "check_bounded ins et = |
46 "check_bounded ins et = |
51 (list_all' (\<lambda>i pc. list_all (\<lambda>pc'. pc' < length ins) (succs i pc)) ins \<and> |
47 (list_all' (\<lambda>i pc. list_all (\<lambda>pc'. pc' < length ins) (succs i pc)) ins \<and> |
52 list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)" |
48 list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)" |
53 by (simp add: list_all_ball check_bounded_def) |
49 by (simp add: list_all_iff check_bounded_def) |
54 |
50 |
55 |
51 |
56 section {* Connecting JVM and Framework *} |
52 section {* Connecting JVM and Framework *} |
57 |
53 |
58 lemma check_bounded_is_bounded: |
54 lemma check_bounded_is_bounded: |