8 theory LBVComplete |
8 theory LBVComplete |
9 imports LBVSpec Typing_Framework |
9 imports LBVSpec Typing_Framework |
10 begin |
10 begin |
11 |
11 |
12 definition is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" where |
12 definition is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" where |
13 "is_target step phi pc' \<equiv> |
13 "is_target step phi pc' \<longleftrightarrow> |
14 \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))" |
14 (\<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc)))" |
15 |
15 |
16 definition make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate" where |
16 definition make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate" where |
17 "make_cert step phi B \<equiv> |
17 "make_cert step phi B = |
18 map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]" |
18 map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]" |
19 |
19 |
20 lemma [code]: |
20 lemma [code]: |
21 "is_target step phi pc' = |
21 "is_target step phi pc' = |
22 list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!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 is_target_def mem_iff) |
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" ("\<phi>") |
28 fixes c :: "'a list" |
28 fixes c :: "'a list" |