author | haftmann |
Tue, 24 Nov 2009 14:37:23 +0100 | |
changeset 33954 | 1bc3b688548c |
child 35109 | 0015a0a99ae9 |
permissions | -rwxr-xr-x |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/MicroJava/BV/Product.thy |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
2 |
Author: Tobias Nipkow |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
3 |
Copyright 2000 TUM |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
4 |
*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
5 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
6 |
header {* \isaheader{Products as Semilattices} *} |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
7 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
8 |
theory Product |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
9 |
imports Err |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
10 |
begin |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
11 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
12 |
constdefs |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
13 |
le :: "'a ord \<Rightarrow> 'b ord \<Rightarrow> ('a * 'b) ord" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
14 |
"le rA rB == %(a,b) (a',b'). a <=_rA a' & b <=_rB b'" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
15 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
16 |
sup :: "'a ebinop \<Rightarrow> 'b ebinop \<Rightarrow> ('a * 'b)ebinop" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
17 |
"sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
18 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
19 |
esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
20 |
"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
21 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
22 |
syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
23 |
("(_ /<='(_,_') _)" [50, 0, 0, 51] 50) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
24 |
translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
25 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
26 |
lemma unfold_lesub_prod: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
27 |
"p <=(rA,rB) q == le rA rB p q" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
28 |
by (simp add: lesub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
29 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
30 |
lemma le_prod_Pair_conv [iff]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
31 |
"((a1,b1) <=(rA,rB) (a2,b2)) = (a1 <=_rA a2 & b1 <=_rB b2)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
32 |
by (simp add: lesub_def le_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
33 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
34 |
lemma less_prod_Pair_conv: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
35 |
"((a1,b1) <_(Product.le rA rB) (a2,b2)) = |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
36 |
(a1 <_rA a2 & b1 <=_rB b2 | a1 <=_rA a2 & b1 <_rB b2)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
37 |
apply (unfold lesssub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
38 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
39 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
40 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
41 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
42 |
lemma order_le_prod [iff]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
43 |
"order(Product.le rA rB) = (order rA & order rB)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
44 |
apply (unfold Semilat.order_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
45 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
46 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
47 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
48 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
49 |
lemma acc_le_prodI [intro!]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
50 |
"\<lbrakk> acc r\<^isub>A; acc r\<^isub>B \<rbrakk> \<Longrightarrow> acc(Product.le r\<^isub>A r\<^isub>B)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
51 |
apply (unfold acc_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
52 |
apply (rule wf_subset) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
53 |
apply (erule wf_lex_prod) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
54 |
apply assumption |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
55 |
apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
56 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
57 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
58 |
lemma closed_lift2_sup: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
59 |
"\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
60 |
closed (err(A<*>B)) (lift2(sup f g))"; |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
61 |
apply (unfold closed_def plussub_def lift2_def err_def sup_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
62 |
apply (simp split: err.split) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
63 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
64 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
65 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
66 |
lemma unfold_plussub_lift2: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
67 |
"e1 +_(lift2 f) e2 == lift2 f e1 e2" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
68 |
by (simp add: plussub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
69 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
70 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
71 |
lemma plus_eq_Err_conv [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
72 |
assumes "x:A" and "y:A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
73 |
and "semilat(err A, Err.le r, lift2 f)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
74 |
shows "(x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
75 |
proof - |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
76 |
have plus_le_conv2: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
77 |
"\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A; |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
78 |
OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
79 |
by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
80 |
from prems show ?thesis |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
81 |
apply (rule_tac iffI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
82 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
83 |
apply (drule OK_le_err_OK [THEN iffD2]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
84 |
apply (drule OK_le_err_OK [THEN iffD2]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
85 |
apply (drule Semilat.lub [OF Semilat.intro, of _ _ _ "OK x" _ "OK y"]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
86 |
apply assumption |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
87 |
apply assumption |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
88 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
89 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
90 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
91 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
92 |
apply (case_tac "x +_f y") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
93 |
apply assumption |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
94 |
apply (rename_tac "z") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
95 |
apply (subgoal_tac "OK z: err A") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
96 |
apply (frule plus_le_conv2) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
97 |
apply assumption |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
98 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
99 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
100 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
101 |
apply (blast dest: Semilat.orderI [OF Semilat.intro] order_refl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
102 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
103 |
apply (erule subst) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
104 |
apply (unfold semilat_def err_def closed_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
105 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
106 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
107 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
108 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
109 |
lemma err_semilat_Product_esl: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
110 |
"\<And>L1 L2. \<lbrakk> err_semilat L1; err_semilat L2 \<rbrakk> \<Longrightarrow> err_semilat(Product.esl L1 L2)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
111 |
apply (unfold esl_def Err.sl_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
112 |
apply (simp (no_asm_simp) only: split_tupled_all) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
113 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
114 |
apply (simp (no_asm) only: semilat_Def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
115 |
apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
116 |
apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
117 |
apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2 |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
118 |
simp add: lift2_def split: err.split) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
119 |
apply (blast dest: Semilat.orderI [OF Semilat.intro]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
120 |
apply (blast dest: Semilat.orderI [OF Semilat.intro]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
121 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
122 |
apply (rule OK_le_err_OK [THEN iffD1]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
123 |
apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
124 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
125 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
126 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
127 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
128 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
129 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
130 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
131 |
apply (rule OK_le_err_OK [THEN iffD1]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
132 |
apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
133 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
134 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
135 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
136 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
137 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
138 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
139 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
140 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
141 |
end |