10 begin |
10 begin |
11 |
11 |
12 types |
12 types |
13 's certificate = "'s list" |
13 's certificate = "'s list" |
14 |
14 |
15 consts |
15 primrec merge :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> nat \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's \<Rightarrow> 's" where |
16 merge :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> nat \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's \<Rightarrow> 's" |
16 "merge cert f r T pc [] x = x" |
17 primrec |
17 | "merge cert f r T pc (s#ss) x = merge cert f r T pc ss (let (pc',s') = s in |
18 "merge cert f r T pc [] x = x" |
|
19 "merge cert f r T pc (s#ss) x = merge cert f r T pc ss (let (pc',s') = s in |
|
20 if pc'=pc+1 then s' +_f x |
18 if pc'=pc+1 then s' +_f x |
21 else if s' <=_r (cert!pc') then x |
19 else if s' <=_r (cert!pc') then x |
22 else T)" |
20 else T)" |
23 |
21 |
24 constdefs |
22 definition wtl_inst :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> |
25 wtl_inst :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> |
23 's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" where |
26 's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" |
|
27 "wtl_inst cert f r T step pc s \<equiv> merge cert f r T pc (step pc s) (cert!(pc+1))" |
24 "wtl_inst cert f r T step pc s \<equiv> merge cert f r T pc (step pc s) (cert!(pc+1))" |
28 |
25 |
29 wtl_cert :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> |
26 definition wtl_cert :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> |
30 's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" |
27 's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" where |
31 "wtl_cert cert f r T B step pc s \<equiv> |
28 "wtl_cert cert f r T B step pc s \<equiv> |
32 if cert!pc = B then |
29 if cert!pc = B then |
33 wtl_inst cert f r T step pc s |
30 wtl_inst cert f r T step pc s |
34 else |
31 else |
35 if s <=_r (cert!pc) then wtl_inst cert f r T step pc (cert!pc) else T" |
32 if s <=_r (cert!pc) then wtl_inst cert f r T step pc (cert!pc) else T" |
36 |
33 |
37 consts |
34 primrec wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> |
38 wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> |
35 's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" where |
39 's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's" |
36 "wtl_inst_list [] cert f r T B step pc s = s" |
40 primrec |
37 | "wtl_inst_list (i#is) cert f r T B step pc s = |
41 "wtl_inst_list [] cert f r T B step pc s = s" |
|
42 "wtl_inst_list (i#is) cert f r T B step pc s = |
|
43 (let s' = wtl_cert cert f r T B step pc s in |
38 (let s' = wtl_cert cert f r T B step pc s in |
44 if s' = T \<or> s = T then T else wtl_inst_list is cert f r T B step (pc+1) s')" |
39 if s' = T \<or> s = T then T else wtl_inst_list is cert f r T B step (pc+1) s')" |
45 |
40 |
46 constdefs |
41 definition cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> 's set \<Rightarrow> bool" where |
47 cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> 's set \<Rightarrow> bool" |
|
48 "cert_ok cert n T B A \<equiv> (\<forall>i < n. cert!i \<in> A \<and> cert!i \<noteq> T) \<and> (cert!n = B)" |
42 "cert_ok cert n T B A \<equiv> (\<forall>i < n. cert!i \<in> A \<and> cert!i \<noteq> T) \<and> (cert!n = B)" |
49 |
43 |
50 constdefs |
44 definition bottom :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool" where |
51 bottom :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
|
52 "bottom r B \<equiv> \<forall>x. B <=_r x" |
45 "bottom r B \<equiv> \<forall>x. B <=_r x" |
53 |
|
54 |
46 |
55 locale lbv = Semilat + |
47 locale lbv = Semilat + |
56 fixes T :: "'a" ("\<top>") |
48 fixes T :: "'a" ("\<top>") |
57 fixes B :: "'a" ("\<bottom>") |
49 fixes B :: "'a" ("\<bottom>") |
58 fixes step :: "'a step_type" |
50 fixes step :: "'a step_type" |