41 "sup S maxs maxr == snd(snd(sl S maxs maxr))" |
41 "sup S maxs maxr == snd(snd(sl S maxs maxr))" |
42 |
42 |
43 |
43 |
44 constdefs |
44 constdefs |
45 sup_ty_opt :: "['code prog,ty err,ty err] => bool" |
45 sup_ty_opt :: "['code prog,ty err,ty err] => bool" |
46 ("_ \<turnstile> _ <=o _" [71,71] 70) |
46 ("_ |- _ <=o _" [71,71] 70) |
47 "sup_ty_opt G == Err.le (subtype G)" |
47 "sup_ty_opt G == Err.le (subtype G)" |
48 |
48 |
49 sup_loc :: "['code prog,locvars_type,locvars_type] => bool" |
49 sup_loc :: "['code prog,locvars_type,locvars_type] => bool" |
50 ("_ \<turnstile> _ <=l _" [71,71] 70) |
50 ("_ |- _ <=l _" [71,71] 70) |
51 "sup_loc G == Listn.le (sup_ty_opt G)" |
51 "sup_loc G == Listn.le (sup_ty_opt G)" |
52 |
52 |
53 sup_state :: "['code prog,state_type,state_type] => bool" |
53 sup_state :: "['code prog,state_type,state_type] => bool" |
54 ("_ \<turnstile> _ <=s _" [71,71] 70) |
54 ("_ |- _ <=s _" [71,71] 70) |
55 "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)" |
55 "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)" |
56 |
56 |
57 sup_state_opt :: "['code prog,state_type option,state_type option] => bool" |
57 sup_state_opt :: "['code prog,state_type option,state_type option] => bool" |
58 ("_ \<turnstile> _ <=' _" [71,71] 70) |
58 ("_ |- _ <=' _" [71,71] 70) |
59 "sup_state_opt G == Opt.le (sup_state G)" |
59 "sup_state_opt G == Opt.le (sup_state G)" |
60 |
60 |
61 |
61 |
62 syntax (HTML) |
62 syntax (xsymbols) |
63 sup_ty_opt :: "['code prog,ty err,ty err] => bool" |
63 sup_ty_opt :: "['code prog,ty err,ty err] => bool" |
64 ("_ |- _ <=o _") |
64 ("_ \<turnstile> _ <=o _" [71,71] 70) |
65 sup_loc :: "['code prog,locvars_type,locvars_type] => bool" |
65 sup_loc :: "['code prog,locvars_type,locvars_type] => bool" |
66 ("_ |- _ <=l _" [71,71] 70) |
66 ("_ \<turnstile> _ <=l _" [71,71] 70) |
67 sup_state :: "['code prog,state_type,state_type] => bool" |
67 sup_state :: "['code prog,state_type,state_type] => bool" |
68 ("_ |- _ <=s _" [71,71] 70) |
68 ("_ \<turnstile> _ <=s _" [71,71] 70) |
69 sup_state_opt :: "['code prog,state_type option,state_type option] => bool" |
69 sup_state_opt :: "['code prog,state_type option,state_type option] => bool" |
70 ("_ |- _ <=' _" [71,71] 70) |
70 ("_ \<turnstile> _ <=' _" [71,71] 70) |
71 |
71 |
72 |
72 |
73 lemma JVM_states_unfold: |
73 lemma JVM_states_unfold: |
74 "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*> |
74 "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*> |
75 list maxr (err(types S))))" |
75 list maxr (err(types S))))" |