equal
deleted
inserted
replaced
25 lemma [code]: "list_ex P (x#xs) = (P x \<or> list_ex P xs)" by (simp add: list_ex_def) |
25 lemma [code]: "list_ex P (x#xs) = (P x \<or> list_ex P xs)" by (simp add: list_ex_def) |
26 |
26 |
27 lemma [code]: |
27 lemma [code]: |
28 "is_target step phi pc' = |
28 "is_target step phi pc' = |
29 list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]" |
29 list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]" |
30 apply (simp add: list_ex_def is_target_def set_mem_eq) |
30 apply (simp add: list_ex_def is_target_def mem_iff) |
31 apply force |
31 apply force |
32 done |
32 done |
33 |
33 |
34 locale (open) lbvc = lbv + |
34 locale (open) lbvc = lbv + |
35 fixes phi :: "'a list" ("\<phi>") |
35 fixes phi :: "'a list" ("\<phi>") |