13 opstack_type = ty list |
13 opstack_type = ty list |
14 state_type = "opstack_type \\<times> locvars_type" |
14 state_type = "opstack_type \\<times> locvars_type" |
15 |
15 |
16 constdefs |
16 constdefs |
17 |
17 |
18 sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ >= _") |
18 sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ <=o _") |
19 "G \\<turnstile> a >= a' \\<equiv> |
19 "G \\<turnstile> a' <=o a \\<equiv> |
20 case a of |
20 case a of |
21 None \\<Rightarrow> True |
21 None \\<Rightarrow> True |
22 | Some t \\<Rightarrow> case a' of |
22 | Some t \\<Rightarrow> case a' of |
23 None \\<Rightarrow> False |
23 None \\<Rightarrow> False |
24 | Some t' \\<Rightarrow> G \\<turnstile> t' \\<preceq> t" |
24 | Some t' \\<Rightarrow> G \\<turnstile> t' \\<preceq> t" |
25 |
25 |
26 sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ >>= _" [71,71] 70) |
26 sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ <=l _" [71,71] 70) |
27 "G \\<turnstile> LT >>= LT' \\<equiv> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t >= t')" |
27 "G \\<turnstile> LT <=l LT' \\<equiv> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t <=o t')" |
28 |
28 |
29 |
29 |
30 sup_state :: "['code prog,state_type,state_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ >>>= _" [71,71] 70) |
30 sup_state :: "['code prog,state_type,state_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ <=s _" [71,71] 70) |
31 "G \\<turnstile> s >>>= s' \\<equiv> G \\<turnstile> map Some (fst s) >>= map Some (fst s') \\<and> G \\<turnstile> snd s >>= snd s'" |
31 "G \\<turnstile> s <=s s' \\<equiv> G \\<turnstile> map Some (fst s) <=l map Some (fst s') \\<and> G \\<turnstile> snd s <=l snd s'" |
32 |
32 |
33 end |
33 end |