equal
deleted
inserted
replaced
22 list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> List.member (map fst (step pc (phi!pc))) pc') [0..<length phi]" |
22 list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> List.member (map fst (step pc (phi!pc))) pc') [0..<length phi]" |
23 by (force simp: list_ex_iff member_def is_target_def) |
23 by (force simp: list_ex_iff member_def is_target_def) |
24 |
24 |
25 |
25 |
26 locale lbvc = lbv + |
26 locale lbvc = lbv + |
27 fixes phi :: "'a list" ("\<phi>") |
27 fixes phi :: "'a list" (\<open>\<phi>\<close>) |
28 fixes c :: "'a list" |
28 fixes c :: "'a list" |
29 defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>" |
29 defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>" |
30 |
30 |
31 assumes mono: "mono r step (length \<phi>) A" |
31 assumes mono: "mono r step (length \<phi>) A" |
32 assumes pres: "pres_type step (length \<phi>) A" |
32 assumes pres: "pres_type step (length \<phi>) A" |