author | wenzelm |
Wed, 07 Oct 2015 23:28:49 +0200 | |
changeset 61361 | 8b5f00202e1a |
parent 59807 | 22bc39064290 |
child 61424 | c3658c18b7bc |
permissions | -rw-r--r-- |
42150 | 1 |
(* Title: HOL/MicroJava/DFA/Listn.thy |
33954
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 |
|
61361 | 6 |
section \<open>Fixed Length Lists\<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 Listn |
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 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
12 |
definition list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
13 |
"list n A == {xs. length xs = n & set xs <= A}" |
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:
35102
diff
changeset
|
15 |
definition le :: "'a ord \<Rightarrow> ('a list)ord" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
16 |
"le r == list_all2 (%x y. x <=_r y)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
17 |
|
35102 | 18 |
abbreviation |
19 |
lesublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool" |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
20 |
("(_ /<=[_] _)" [50, 0, 51] 50) |
35102 | 21 |
where "x <=[r] y == x <=_(le r) y" |
22 |
||
23 |
abbreviation |
|
24 |
lesssublist_syntax :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool" |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
25 |
("(_ /<[_] _)" [50, 0, 51] 50) |
35102 | 26 |
where "x <[r] y == x <_(le r) y" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
27 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
28 |
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
29 |
"map2 f == (%xs ys. map (split f) (zip xs ys))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
30 |
|
35102 | 31 |
abbreviation |
32 |
plussublist_syntax :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list" |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
33 |
("(_ /+[_] _)" [65, 0, 66] 65) |
35102 | 34 |
where "x +[f] y == x +_(map2 f) y" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
35 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
36 |
primrec coalesce :: "'a err list \<Rightarrow> 'a list err" where |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
37 |
"coalesce [] = OK[]" |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
38 |
| "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
39 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
40 |
definition sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
41 |
"sl n == %(A,r,f). (list n A, le r, map2 f)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
42 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
43 |
definition sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list err" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
44 |
"sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
45 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
46 |
definition upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
47 |
"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)" |
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 |
lemmas [simp] = set_update_subsetI |
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 |
lemma unfold_lesub_list: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
52 |
"xs <=[r] ys == Listn.le r xs ys" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
53 |
by (simp add: lesub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
54 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
55 |
lemma Nil_le_conv [iff]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
56 |
"([] <=[r] ys) = (ys = [])" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
57 |
apply (unfold lesub_def Listn.le_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
58 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
59 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
60 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
61 |
lemma Cons_notle_Nil [iff]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
62 |
"~ x#xs <=[r] []" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
63 |
apply (unfold lesub_def Listn.le_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
64 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
65 |
done |
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 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
68 |
lemma Cons_le_Cons [iff]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
69 |
"x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
70 |
apply (unfold lesub_def Listn.le_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
71 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
72 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
73 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
74 |
lemma Cons_less_Conss [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
75 |
"order r \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
76 |
x#xs <_(Listn.le r) y#ys = |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
77 |
(x <_r y & xs <=[r] ys | x = y & xs <_(Listn.le r) ys)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
78 |
apply (unfold lesssub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
79 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
80 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
81 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
82 |
lemma list_update_le_cong: |
58860 | 83 |
"\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
84 |
apply (unfold unfold_lesub_list) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
85 |
apply (unfold Listn.le_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
86 |
apply (simp add: list_all2_conv_all_nth nth_list_update) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
87 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
88 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
89 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
90 |
lemma le_listD: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
91 |
"\<lbrakk> xs <=[r] ys; p < size xs \<rbrakk> \<Longrightarrow> xs!p <=_r ys!p" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
92 |
apply (unfold Listn.le_def lesub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
93 |
apply (simp add: list_all2_conv_all_nth) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
94 |
done |
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 le_list_refl: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
97 |
"!x. x <=_r x \<Longrightarrow> xs <=[r] xs" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
98 |
apply (unfold unfold_lesub_list) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
99 |
apply (simp add: Listn.le_def list_all2_conv_all_nth) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
100 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
101 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
102 |
lemma le_list_trans: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
103 |
"\<lbrakk> order r; xs <=[r] ys; ys <=[r] zs \<rbrakk> \<Longrightarrow> xs <=[r] zs" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
104 |
apply (unfold unfold_lesub_list) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
105 |
apply (simp add: Listn.le_def list_all2_conv_all_nth) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
106 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
107 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
108 |
apply (blast intro: order_trans) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
109 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
110 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
111 |
lemma le_list_antisym: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
112 |
"\<lbrakk> order r; xs <=[r] ys; ys <=[r] xs \<rbrakk> \<Longrightarrow> xs = ys" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
113 |
apply (unfold unfold_lesub_list) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
114 |
apply (simp add: Listn.le_def list_all2_conv_all_nth) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
115 |
apply (rule nth_equalityI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
116 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
117 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
118 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
119 |
apply (blast intro: order_antisym) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
120 |
done |
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 |
lemma order_listI [simp, intro!]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
123 |
"order r \<Longrightarrow> order(Listn.le r)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
124 |
apply (subst Semilat.order_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
125 |
apply (blast intro: le_list_refl le_list_trans le_list_antisym |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
126 |
dest: order_refl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
127 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
128 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
129 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
130 |
lemma lesub_list_impl_same_size [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
131 |
"xs <=[r] ys \<Longrightarrow> size ys = size xs" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
132 |
apply (unfold Listn.le_def lesub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
133 |
apply (simp add: list_all2_conv_all_nth) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
134 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
135 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
136 |
lemma lesssub_list_impl_same_size: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
137 |
"xs <_(Listn.le r) ys \<Longrightarrow> size ys = size xs" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
138 |
apply (unfold lesssub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
139 |
apply auto |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
140 |
done |
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 le_list_appendI: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
143 |
"\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
144 |
apply (induct a) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
145 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
146 |
apply (case_tac b) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
147 |
apply auto |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
148 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
149 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
150 |
lemma le_listI: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
151 |
"length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
152 |
apply (unfold lesub_def Listn.le_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
153 |
apply (simp add: list_all2_conv_all_nth) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
154 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
155 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
156 |
lemma listI: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
157 |
"\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
158 |
apply (unfold list_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
159 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
160 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
161 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
162 |
lemma listE_length [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
163 |
"xs : list n A \<Longrightarrow> length xs = n" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
164 |
apply (unfold list_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
165 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
166 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
167 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
168 |
lemma less_lengthI: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
169 |
"\<lbrakk> xs : list n A; p < n \<rbrakk> \<Longrightarrow> p < length xs" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
170 |
by simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
171 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
172 |
lemma listE_set [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
173 |
"xs : list n A \<Longrightarrow> set xs <= A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
174 |
apply (unfold list_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
175 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
176 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
177 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
178 |
lemma list_0 [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
179 |
"list 0 A = {[]}" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
180 |
apply (unfold list_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
181 |
apply auto |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
182 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
183 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
184 |
lemma in_list_Suc_iff: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
185 |
"(xs : list (Suc n) A) = (\<exists>y\<in> A. \<exists>ys\<in> list n A. xs = y#ys)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
186 |
apply (unfold list_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
187 |
apply (case_tac "xs") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
188 |
apply auto |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
189 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
190 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
191 |
lemma Cons_in_list_Suc [iff]: |
58860 | 192 |
"(x#xs : list (Suc n) A) = (x\<in> A & xs : list n A)" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
193 |
apply (simp add: in_list_Suc_iff) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
194 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
195 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
196 |
lemma list_not_empty: |
58860 | 197 |
"\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
198 |
apply (induct "n") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
199 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
200 |
apply (simp add: in_list_Suc_iff) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
201 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
202 |
done |
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 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
205 |
lemma nth_in [rule_format, simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
206 |
"!i n. length xs = n \<longrightarrow> set xs <= A \<longrightarrow> i < n \<longrightarrow> (xs!i) : A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
207 |
apply (induct "xs") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
208 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
209 |
apply (simp add: nth_Cons split: nat.split) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
210 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
211 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
212 |
lemma listE_nth_in: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
213 |
"\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
214 |
by auto |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
215 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
216 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
217 |
lemma listn_Cons_Suc [elim!]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
218 |
"l#xs \<in> list n A \<Longrightarrow> (\<And>n'. n = Suc n' \<Longrightarrow> l \<in> A \<Longrightarrow> xs \<in> list n' A \<Longrightarrow> P) \<Longrightarrow> P" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
219 |
by (cases n) auto |
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 |
lemma listn_appendE [elim!]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
222 |
"a@b \<in> list n A \<Longrightarrow> (\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P) \<Longrightarrow> P" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
223 |
proof - |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
224 |
have "\<And>n. a@b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n=n1+n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
225 |
(is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
226 |
proof (induct a) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
227 |
fix n assume "?list [] n" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
228 |
hence "?P [] n 0 n" by simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
229 |
thus "\<exists>n1 n2. ?P [] n n1 n2" by fast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
230 |
next |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
231 |
fix n l ls |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
232 |
assume "?list (l#ls) n" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44179
diff
changeset
|
233 |
then obtain n' where n: "n = Suc n'" "l \<in> A" and list_n': "ls@b \<in> list n' A" by fastforce |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
234 |
assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
235 |
hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" by this (rule list_n') |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
236 |
then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
237 |
with n have "?P (l#ls) n (n1+1) n2" by simp |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44179
diff
changeset
|
238 |
thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastforce |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
239 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
240 |
moreover |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
241 |
assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P" |
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 |
show ?thesis by blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
244 |
qed |
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 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
247 |
lemma listt_update_in_list [simp, intro!]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
248 |
"\<lbrakk> xs : list n A; x\<in> A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
249 |
apply (unfold list_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
250 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
251 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
252 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
253 |
lemma plus_list_Nil [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
254 |
"[] +[f] xs = []" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
255 |
apply (unfold plussub_def map2_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
256 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
257 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
258 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
259 |
lemma plus_list_Cons [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
260 |
"(x#xs) +[f] ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x +_f y)#(xs +[f] ys))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
261 |
by (simp add: plussub_def map2_def split: list.split) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
262 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
263 |
lemma length_plus_list [rule_format, simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
264 |
"!ys. length(xs +[f] ys) = min(length xs) (length ys)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
265 |
apply (induct xs) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
266 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
267 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
268 |
apply (simp (no_asm_simp) split: list.split) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
269 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
270 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
271 |
lemma nth_plus_list [rule_format, simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
272 |
"!xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i<n \<longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
273 |
(xs +[f] ys)!i = (xs!i) +_f (ys!i)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
274 |
apply (induct n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
275 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
276 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
277 |
apply (case_tac xs) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
278 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
279 |
apply (force simp add: nth_Cons split: list.split nat.split) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
280 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
281 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
282 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
283 |
lemma (in Semilat) plus_list_ub1 [rule_format]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
284 |
"\<lbrakk> set xs <= A; set ys <= A; size xs = size ys \<rbrakk> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
285 |
\<Longrightarrow> xs <=[r] xs +[f] ys" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
286 |
apply (unfold unfold_lesub_list) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
287 |
apply (simp add: Listn.le_def list_all2_conv_all_nth) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
288 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
289 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
290 |
lemma (in Semilat) plus_list_ub2: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
291 |
"\<lbrakk>set xs <= A; set ys <= A; size xs = size ys \<rbrakk> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
292 |
\<Longrightarrow> ys <=[r] xs +[f] ys" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
293 |
apply (unfold unfold_lesub_list) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
294 |
apply (simp add: Listn.le_def list_all2_conv_all_nth) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
295 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
296 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
297 |
lemma (in Semilat) plus_list_lub [rule_format]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
298 |
shows "!xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
299 |
\<longrightarrow> size xs = n & size ys = n \<longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
300 |
xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
301 |
apply (unfold unfold_lesub_list) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
302 |
apply (simp add: Listn.le_def list_all2_conv_all_nth) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
303 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
304 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
305 |
lemma (in Semilat) list_update_incr [rule_format]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
306 |
"x\<in> A \<Longrightarrow> set xs <= A \<longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
307 |
(!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
308 |
apply (unfold unfold_lesub_list) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
309 |
apply (simp add: Listn.le_def list_all2_conv_all_nth) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
310 |
apply (induct xs) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
311 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
312 |
apply (simp add: in_list_Suc_iff) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
313 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
314 |
apply (simp add: nth_Cons split: nat.split) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
315 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
316 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
317 |
lemma acc_le_listI [intro!]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
318 |
"\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
319 |
apply (unfold acc_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
320 |
apply (subgoal_tac |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
321 |
"wf(UN n. {(ys,xs). size xs = n \<and> size ys = n \<and> xs <_(Listn.le r) ys})") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
322 |
apply (erule wf_subset) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
323 |
apply (blast intro: lesssub_list_impl_same_size) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
324 |
apply (rule wf_UN) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
325 |
prefer 2 |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
326 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
327 |
apply (rename_tac m n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
328 |
apply (case_tac "m=n") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
329 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
330 |
apply (fast intro!: equals0I dest: not_sym) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
331 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
332 |
apply (rename_tac n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
333 |
apply (induct_tac n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
334 |
apply (simp add: lesssub_def cong: conj_cong) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
335 |
apply (rename_tac k) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
336 |
apply (simp add: wf_eq_minimal) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
337 |
apply (simp (no_asm) add: length_Suc_conv cong: conj_cong) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
338 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
339 |
apply (rename_tac M m) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
340 |
apply (case_tac "\<exists>x xs. size xs = k \<and> x#xs \<in> M") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
341 |
prefer 2 |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
342 |
apply (erule thin_rl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
343 |
apply (erule thin_rl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
344 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
345 |
apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs:M}" in allE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
346 |
apply (erule impE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
347 |
apply blast |
59807 | 348 |
apply (thin_tac "\<exists>x xs. P x xs" for P) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
349 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
350 |
apply (rename_tac maxA xs) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
351 |
apply (erule_tac x = "{ys. size ys = size xs \<and> maxA#ys \<in> M}" in allE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
352 |
apply (erule impE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
353 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
354 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
355 |
apply (thin_tac "m \<in> M") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
356 |
apply (thin_tac "maxA#xs \<in> M") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
357 |
apply (rule bexI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
358 |
prefer 2 |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
359 |
apply assumption |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
360 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
361 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
362 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
363 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
364 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
365 |
lemma closed_listI: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
366 |
"closed S f \<Longrightarrow> closed (list n S) (map2 f)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
367 |
apply (unfold closed_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
368 |
apply (induct n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
369 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
370 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
371 |
apply (simp add: in_list_Suc_iff) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
372 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
373 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
374 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
375 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
376 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
377 |
lemma Listn_sl_aux: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
378 |
assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
379 |
proof - |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
380 |
interpret Semilat A r f using assms by (rule Semilat.intro) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
381 |
show ?thesis |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
382 |
apply (unfold Listn.sl_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
383 |
apply (simp (no_asm) only: semilat_Def split_conv) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
384 |
apply (rule conjI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
385 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
386 |
apply (rule conjI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
387 |
apply (simp only: closedI closed_listI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
388 |
apply (simp (no_asm) only: list_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
389 |
apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
390 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
391 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
392 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
393 |
lemma Listn_sl: "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
394 |
by(simp add: Listn_sl_aux split_tupled_all) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
395 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
396 |
lemma coalesce_in_err_list [rule_format]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
397 |
"!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
398 |
apply (induct n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
399 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
400 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
401 |
apply (simp add: in_list_Suc_iff) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
402 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
403 |
apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
404 |
apply force |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
405 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
406 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
407 |
lemma lem: "\<And>x xs. x +_(op #) xs = x#xs" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
408 |
by (simp add: plussub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
409 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
410 |
lemma coalesce_eq_OK1_D [rule_format]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
411 |
"semilat(err A, Err.le r, lift2 f) \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
412 |
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
413 |
(!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
414 |
apply (induct n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
415 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
416 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
417 |
apply (simp add: in_list_Suc_iff) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
418 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
419 |
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
420 |
apply (force simp add: semilat_le_err_OK1) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
421 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
422 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
423 |
lemma coalesce_eq_OK2_D [rule_format]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
424 |
"semilat(err A, Err.le r, lift2 f) \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
425 |
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
426 |
(!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
427 |
apply (induct n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
428 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
429 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
430 |
apply (simp add: in_list_Suc_iff) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
431 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
432 |
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
433 |
apply (force simp add: semilat_le_err_OK2) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
434 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
435 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
436 |
lemma lift2_le_ub: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
437 |
"\<lbrakk> semilat(err A, Err.le r, lift2 f); x\<in> A; y\<in> A; x +_f y = OK z; |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
438 |
u\<in> A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
439 |
apply (unfold semilat_Def plussub_def err_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
440 |
apply (simp add: lift2_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
441 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
442 |
apply (rotate_tac -3) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
443 |
apply (erule thin_rl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
444 |
apply (erule thin_rl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
445 |
apply force |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
446 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
447 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
448 |
lemma coalesce_eq_OK_ub_D [rule_format]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
449 |
"semilat(err A, Err.le r, lift2 f) \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
450 |
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
451 |
(!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
452 |
& us : list n A \<longrightarrow> zs <=[r] us))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
453 |
apply (induct n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
454 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
455 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
456 |
apply (simp add: in_list_Suc_iff) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
457 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
458 |
apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
459 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
460 |
apply (rule conjI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
461 |
apply (blast intro: lift2_le_ub) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
462 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
463 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
464 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
465 |
lemma lift2_eq_ErrD: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
466 |
"\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x\<in> A; y\<in> A \<rbrakk> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
467 |
\<Longrightarrow> ~(\<exists>u\<in> A. x <=_r u & y <=_r u)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
468 |
by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
469 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
470 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
471 |
lemma coalesce_eq_Err_D [rule_format]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
472 |
"\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
473 |
\<Longrightarrow> !xs. xs\<in> list n A \<longrightarrow> (!ys. ys\<in> list n A \<longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
474 |
coalesce (xs +[f] ys) = Err \<longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
475 |
~(\<exists>zs\<in> list n A. xs <=[r] zs & ys <=[r] zs))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
476 |
apply (induct n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
477 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
478 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
479 |
apply (simp add: in_list_Suc_iff) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
480 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
481 |
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
482 |
apply (blast dest: lift2_eq_ErrD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
483 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
484 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
485 |
lemma closed_err_lift2_conv: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
486 |
"closed (err A) (lift2 f) = (\<forall>x\<in> A. \<forall>y\<in> A. x +_f y : err A)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
487 |
apply (unfold closed_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
488 |
apply (simp add: err_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
489 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
490 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
491 |
lemma closed_map2_list [rule_format]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
492 |
"closed (err A) (lift2 f) \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
493 |
\<forall>xs. xs : list n A \<longrightarrow> (\<forall>ys. ys : list n A \<longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
494 |
map2 f xs ys : list n (err A))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
495 |
apply (unfold map2_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
496 |
apply (induct n) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
497 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
498 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
499 |
apply (simp add: in_list_Suc_iff) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
500 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
501 |
apply (simp add: plussub_def closed_err_lift2_conv) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
502 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
503 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
504 |
lemma closed_lift2_sup: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
505 |
"closed (err A) (lift2 f) \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
506 |
closed (err (list n A)) (lift2 (sup f))" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44179
diff
changeset
|
507 |
by (fastforce simp add: closed_def plussub_def sup_def lift2_def |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
508 |
coalesce_in_err_list closed_map2_list |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
509 |
split: err.split) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
510 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
511 |
lemma err_semilat_sup: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
512 |
"err_semilat (A,r,f) \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
513 |
err_semilat (list n A, Listn.le r, sup f)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
514 |
apply (unfold Err.sl_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
515 |
apply (simp only: split_conv) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
516 |
apply (simp (no_asm) only: semilat_Def plussub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
517 |
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
|
518 |
apply (rule conjI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
519 |
apply (drule Semilat.orderI [OF Semilat.intro]) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
520 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
521 |
apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
522 |
apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
523 |
apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
524 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
525 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
526 |
lemma err_semilat_upto_esl: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
527 |
"\<And>L. err_semilat L \<Longrightarrow> err_semilat(upto_esl m L)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
528 |
apply (unfold Listn.upto_esl_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
529 |
apply (simp (no_asm_simp) only: split_tupled_all) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
530 |
apply simp |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44179
diff
changeset
|
531 |
apply (fastforce intro!: err_semilat_UnionI err_semilat_sup |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
532 |
dest: lesub_list_impl_same_size |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
533 |
simp add: plussub_def Listn.sup_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
534 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
535 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
536 |
end |