author | nipkow |
Sun, 04 Nov 2018 12:07:24 +0100 | |
changeset 69232 | 2b913054a9cf |
parent 63170 | eae6549dbea2 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
42150 | 1 |
(* Title: HOL/MicroJava/DFA/Typing_Framework_err.thy |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
2 |
Author: Gerwin Klein |
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 |
|
61361 | 6 |
section \<open>Lifting the Typing Framework to err, app, and eff\<close> |
33954
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 Typing_Framework_err |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
9 |
imports Typing_Framework SemilatAlg |
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 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
12 |
definition wt_err_step :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
13 |
"wt_err_step r step ts \<equiv> wt_step (Err.le r) Err step ts" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
14 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
15 |
definition wt_app_eff :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
16 |
"wt_app_eff r app step ts \<equiv> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
17 |
\<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
18 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
19 |
definition map_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'c) list" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
20 |
"map_snd f \<equiv> map (\<lambda>(x,y). (x, f y))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
21 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
22 |
definition error :: "nat \<Rightarrow> (nat \<times> 'a err) list" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
23 |
"error n \<equiv> map (\<lambda>x. (x,Err)) [0..<n]" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
24 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
25 |
definition err_step :: "nat \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
26 |
"err_step n app step p t \<equiv> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
27 |
case t of |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
28 |
Err \<Rightarrow> error n |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
29 |
| OK t' \<Rightarrow> if app p t' then map_snd OK (step p t') else error n" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
30 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
31 |
definition app_mono :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
32 |
"app_mono r app n A \<equiv> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
33 |
\<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> app p s" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
34 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
35 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
36 |
lemmas err_step_defs = err_step_def map_snd_def error_def |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
37 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
38 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
39 |
lemma bounded_err_stepD: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
40 |
"bounded (err_step n app step) n \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
41 |
p < n \<Longrightarrow> app p a \<Longrightarrow> (q,b) \<in> set (step p a) \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
42 |
q < n" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
43 |
apply (simp add: bounded_def err_step_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
44 |
apply (erule allE, erule impE, assumption) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
45 |
apply (erule_tac x = "OK a" in allE, drule bspec) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
46 |
apply (simp add: map_snd_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
47 |
apply fast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
48 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
49 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
50 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
51 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
52 |
lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
53 |
apply (induct xs) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
54 |
apply (auto simp add: map_snd_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
55 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
56 |
|
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 bounded_err_stepI: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
59 |
"\<forall>p. p < n \<longrightarrow> (\<forall>s. ap p s \<longrightarrow> (\<forall>(q,s') \<in> set (step p s). q < n)) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
60 |
\<Longrightarrow> bounded (err_step n ap step) n" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
61 |
apply (clarsimp simp: bounded_def err_step_def split: err.splits) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
62 |
apply (simp add: error_def image_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
63 |
apply (blast dest: in_map_sndD) |
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 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
67 |
lemma bounded_lift: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
68 |
"bounded step n \<Longrightarrow> bounded (err_step n app step) n" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
69 |
apply (unfold bounded_def err_step_def error_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
70 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
71 |
apply (erule allE, erule impE, assumption) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
72 |
apply (case_tac s) |
62390 | 73 |
apply (auto simp add: map_snd_def split: if_split_asm) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
74 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
75 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
76 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
77 |
lemma le_list_map_OK [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
78 |
"\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
79 |
apply (induct a) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
80 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
81 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
82 |
apply (case_tac b) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
83 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
84 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
85 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
86 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
87 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
88 |
lemma map_snd_lessI: |
61994 | 89 |
"x \<le>|r| y \<Longrightarrow> map_snd OK x \<le>|Err.le r| map_snd OK y" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
90 |
apply (induct x) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
91 |
apply (unfold lesubstep_type_def map_snd_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
92 |
apply auto |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
93 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
94 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
95 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
96 |
lemma mono_lift: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
97 |
"order r \<Longrightarrow> app_mono r app n A \<Longrightarrow> bounded (err_step n app step) n \<Longrightarrow> |
61994 | 98 |
\<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> step p s \<le>|r| step p t \<Longrightarrow> |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
99 |
mono (Err.le r) (err_step n app step) n (err A)" |
63170 | 100 |
apply (simp only: app_mono_def mono_def err_step_def) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
101 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
102 |
apply (case_tac s) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
103 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
104 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
105 |
apply (case_tac t) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
106 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
107 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
108 |
apply (simp add: lesubstep_type_def error_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
109 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
110 |
apply (drule in_map_sndD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
111 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
112 |
apply (drule bounded_err_stepD, assumption+) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
113 |
apply (rule exI [of _ Err]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
114 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
115 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
116 |
apply (erule allE, erule allE, erule allE, erule impE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
117 |
apply (rule conjI, assumption) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
118 |
apply (rule conjI, assumption) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
119 |
apply assumption |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
120 |
apply (rule conjI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
121 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
122 |
apply (erule allE, erule allE, erule allE, erule impE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
123 |
apply (rule conjI, assumption) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
124 |
apply (rule conjI, assumption) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
125 |
apply assumption |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
126 |
apply (erule impE, assumption) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
127 |
apply (rule map_snd_lessI, assumption) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
128 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
129 |
apply (simp add: lesubstep_type_def error_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
130 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
131 |
apply (drule in_map_sndD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
132 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
133 |
apply (drule bounded_err_stepD, assumption+) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
134 |
apply (rule exI [of _ Err]) |
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 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
137 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
138 |
lemma in_errorD: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
139 |
"(x,y) \<in> set (error n) \<Longrightarrow> y = Err" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
140 |
by (auto simp add: error_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
141 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
142 |
lemma pres_type_lift: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
143 |
"\<forall>s\<in>A. \<forall>p. p < n \<longrightarrow> app p s \<longrightarrow> (\<forall>(q, s')\<in>set (step p s). s' \<in> A) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
144 |
\<Longrightarrow> pres_type (err_step n app step) n (err A)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
145 |
apply (unfold pres_type_def err_step_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
146 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
147 |
apply (case_tac b) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
148 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
149 |
apply (case_tac s) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
150 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
151 |
apply (drule in_errorD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
152 |
apply simp |
62390 | 153 |
apply (simp add: map_snd_def split: if_split_asm) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
154 |
apply fast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
155 |
apply (drule in_errorD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
156 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
157 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
158 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
159 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
160 |
|
61361 | 161 |
text \<open> |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
162 |
There used to be a condition here that each instruction must have a |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
163 |
successor. This is not needed any more, because the definition of |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
164 |
@{term error} trivially ensures that there is a successor for |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
165 |
the critical case where @{term app} does not hold. |
61361 | 166 |
\<close> |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
167 |
lemma wt_err_imp_wt_app_eff: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
168 |
assumes wt: "wt_err_step r (err_step (size ts) app step) ts" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
169 |
assumes b: "bounded (err_step (size ts) app step) (size ts)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
170 |
shows "wt_app_eff r app step (map ok_val ts)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
171 |
proof (unfold wt_app_eff_def, intro strip, rule conjI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
172 |
fix p assume "p < size (map ok_val ts)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
173 |
hence lp: "p < size ts" by simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
174 |
hence ts: "0 < size ts" by (cases p) auto |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
175 |
hence err: "(0,Err) \<in> set (error (size ts))" by (simp add: error_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
176 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
177 |
from wt lp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
178 |
have [intro?]: "\<And>p. p < size ts \<Longrightarrow> ts ! p \<noteq> Err" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
179 |
by (unfold wt_err_step_def wt_step_def) simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
180 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
181 |
show app: "app p (map ok_val ts ! p)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
182 |
proof (rule ccontr) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
183 |
from wt lp obtain s where |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
184 |
OKp: "ts ! p = OK s" and |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
185 |
less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
186 |
by (unfold wt_err_step_def wt_step_def stable_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
187 |
(auto iff: not_Err_eq) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
188 |
assume "\<not> app p (map ok_val ts ! p)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
189 |
with OKp lp have "\<not> app p s" by simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
190 |
with OKp have "err_step (size ts) app step p (ts!p) = error (size ts)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
191 |
by (simp add: err_step_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
192 |
with err ts obtain q where |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
193 |
"(q,Err) \<in> set (err_step (size ts) app step p (ts!p))" and |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
194 |
q: "q < size ts" by auto |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
195 |
with less have "ts!q = Err" by auto |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
196 |
moreover from q have "ts!q \<noteq> Err" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
197 |
ultimately show False by blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
198 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
199 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
200 |
show "\<forall>(q,t)\<in>set(step p (map ok_val ts ! p)). t <=_r map ok_val ts ! q" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
201 |
proof clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
202 |
fix q t assume q: "(q,t) \<in> set (step p (map ok_val ts ! p))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
203 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
204 |
from wt lp q |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
205 |
obtain s where |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
206 |
OKp: "ts ! p = OK s" and |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
207 |
less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
208 |
by (unfold wt_err_step_def wt_step_def stable_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
209 |
(auto iff: not_Err_eq) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
210 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
211 |
from b lp app q have lq: "q < size ts" by (rule bounded_err_stepD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
212 |
hence "ts!q \<noteq> Err" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
213 |
then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
214 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
215 |
from lp lq OKp OKq app less q |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
216 |
show "t <=_r map ok_val ts ! q" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
217 |
by (auto simp add: err_step_def map_snd_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
218 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
219 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
220 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
221 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
222 |
lemma wt_app_eff_imp_wt_err: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
223 |
assumes app_eff: "wt_app_eff r app step ts" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
224 |
assumes bounded: "bounded (err_step (size ts) app step) (size ts)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
225 |
shows "wt_err_step r (err_step (size ts) app step) (map OK ts)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
226 |
proof (unfold wt_err_step_def wt_step_def, intro strip, rule conjI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
227 |
fix p assume "p < size (map OK ts)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
228 |
hence p: "p < size ts" by simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
229 |
thus "map OK ts ! p \<noteq> Err" by simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
230 |
{ fix q t |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
231 |
assume q: "(q,t) \<in> set (err_step (size ts) app step p (map OK ts ! p))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
232 |
with p app_eff obtain |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
233 |
"app p (ts ! p)" "\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
234 |
by (unfold wt_app_eff_def) blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
235 |
moreover |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
236 |
from q p bounded have "q < size ts" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
237 |
by - (rule boundedD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
238 |
hence "map OK ts ! q = OK (ts!q)" by simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
239 |
moreover |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
240 |
have "p < size ts" by (rule p) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
241 |
moreover note q |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
242 |
ultimately |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
243 |
have "t <=_(Err.le r) map OK ts ! q" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
244 |
by (auto simp add: err_step_def map_snd_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
245 |
} |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
246 |
thus "stable (Err.le r) (err_step (size ts) app step) (map OK ts) p" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
247 |
by (unfold stable_def) blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
248 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
249 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
250 |
end |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
251 |