13062
|
1 |
(* Title: HOL/MicroJava/BV/SemilatAlg.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gerwin Klein
|
|
4 |
Copyright 2002 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
header {* \isaheader{More on Semilattices} *}
|
|
8 |
|
|
9 |
theory SemilatAlg = Typing_Framework + Product:
|
|
10 |
|
|
11 |
|
13066
|
12 |
constdefs
|
|
13 |
lesubstep_type :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
|
|
14 |
("(_ /<=|_| _)" [50, 0, 51] 50)
|
|
15 |
"x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
|
|
16 |
|
13062
|
17 |
consts
|
|
18 |
"@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
|
|
19 |
primrec
|
|
20 |
"[] ++_f y = y"
|
|
21 |
"(x#xs) ++_f y = xs ++_f (x +_f y)"
|
|
22 |
|
|
23 |
constdefs
|
|
24 |
bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
|
|
25 |
"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"
|
|
26 |
|
|
27 |
pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
|
|
28 |
"pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
|
|
29 |
|
|
30 |
mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
|
|
31 |
"mono r step n A ==
|
|
32 |
\<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
|
|
33 |
|
|
34 |
|
|
35 |
lemma pres_typeD:
|
|
36 |
"\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
|
|
37 |
by (unfold pres_type_def, blast)
|
|
38 |
|
|
39 |
lemma monoD:
|
|
40 |
"\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s <=|r| step p t"
|
|
41 |
by (unfold mono_def, blast)
|
|
42 |
|
|
43 |
lemma boundedD:
|
|
44 |
"\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n"
|
|
45 |
by (unfold bounded_def, blast)
|
|
46 |
|
13066
|
47 |
lemma lesubstep_type_refl [simp, intro]:
|
|
48 |
"(\<And>x. x <=_r x) \<Longrightarrow> x <=|r| x"
|
|
49 |
by (unfold lesubstep_type_def) auto
|
|
50 |
|
|
51 |
lemma lesub_step_typeD:
|
|
52 |
"a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
|
|
53 |
by (unfold lesubstep_type_def) blast
|
|
54 |
|
13062
|
55 |
|
|
56 |
lemma list_update_le_listI [rule_format]:
|
|
57 |
"set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>
|
|
58 |
x <=_r ys!p \<longrightarrow> semilat(A,r,f) \<longrightarrow> x\<in>A \<longrightarrow>
|
|
59 |
xs[p := x +_f xs!p] <=[r] ys"
|
|
60 |
apply (unfold Listn.le_def lesub_def semilat_def)
|
|
61 |
apply (simp add: list_all2_conv_all_nth nth_list_update)
|
|
62 |
done
|
|
63 |
|
|
64 |
|
13074
|
65 |
lemma plusplus_closed: includes semilat shows
|
|
66 |
"\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
|
13062
|
67 |
proof (induct x)
|
|
68 |
show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
|
|
69 |
fix y x xs
|
13074
|
70 |
assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
|
|
71 |
assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
|
|
72 |
from xs obtain x: "x \<in> A" and "set xs \<subseteq> A" by simp
|
13077
|
73 |
from x y have "(x +_f y) \<in> A" ..
|
|
74 |
with xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
|
13062
|
75 |
thus "(x#xs) ++_f y \<in> A" by simp
|
|
76 |
qed
|
|
77 |
|
13074
|
78 |
lemma (in semilat) pp_ub2:
|
|
79 |
"\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
|
13062
|
80 |
proof (induct x)
|
13074
|
81 |
from semilat show "\<And>y. y <=_r [] ++_f y" by simp
|
13062
|
82 |
|
|
83 |
fix y a l
|
|
84 |
assume y: "y \<in> A"
|
|
85 |
assume "set (a#l) \<subseteq> A"
|
13074
|
86 |
then obtain a: "a \<in> A" and x: "set l \<subseteq> A" by simp
|
|
87 |
assume "\<And>y. \<lbrakk>set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
|
13062
|
88 |
hence IH: "\<And>y. y \<in> A \<Longrightarrow> y <=_r l ++_f y" .
|
|
89 |
|
13077
|
90 |
from a y have "y <=_r a +_f y" ..
|
|
91 |
also from a y have "a +_f y \<in> A" ..
|
13062
|
92 |
hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
|
13074
|
93 |
finally have "y <=_r l ++_f (a +_f y)" .
|
13062
|
94 |
thus "y <=_r (a#l) ++_f y" by simp
|
|
95 |
qed
|
|
96 |
|
|
97 |
|
13074
|
98 |
lemma (in semilat) pp_ub1:
|
|
99 |
shows "\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
|
13062
|
100 |
proof (induct ls)
|
|
101 |
show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
|
13074
|
102 |
|
13062
|
103 |
fix y s ls
|
|
104 |
assume "set (s#ls) \<subseteq> A"
|
|
105 |
then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
|
|
106 |
assume y: "y \<in> A"
|
|
107 |
|
|
108 |
assume
|
13074
|
109 |
"\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
|
13062
|
110 |
hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" .
|
|
111 |
|
|
112 |
assume "x \<in> set (s#ls)"
|
|
113 |
then obtain xls: "x = s \<or> x \<in> set ls" by simp
|
|
114 |
moreover {
|
|
115 |
assume xs: "x = s"
|
13077
|
116 |
from s y have "s <=_r s +_f y" ..
|
|
117 |
also from s y have "s +_f y \<in> A" ..
|
13074
|
118 |
with ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule pp_ub2)
|
|
119 |
finally have "s <=_r ls ++_f (s +_f y)" .
|
13062
|
120 |
with xs have "x <=_r ls ++_f (s +_f y)" by simp
|
|
121 |
}
|
|
122 |
moreover {
|
|
123 |
assume "x \<in> set ls"
|
|
124 |
hence "\<And>y. y \<in> A \<Longrightarrow> x <=_r ls ++_f y" by (rule IH)
|
13077
|
125 |
moreover from s y have "s +_f y \<in> A" ..
|
13074
|
126 |
ultimately have "x <=_r ls ++_f (s +_f y)" .
|
13062
|
127 |
}
|
|
128 |
ultimately
|
|
129 |
have "x <=_r ls ++_f (s +_f y)" by blast
|
|
130 |
thus "x <=_r (s#ls) ++_f y" by simp
|
|
131 |
qed
|
|
132 |
|
|
133 |
|
13074
|
134 |
lemma (in semilat) pp_lub:
|
|
135 |
assumes "z \<in> A"
|
13069
|
136 |
shows
|
|
137 |
"\<And>y. y \<in> A \<Longrightarrow> set xs \<subseteq> A \<Longrightarrow> \<forall>x \<in> set xs. x <=_r z \<Longrightarrow> y <=_r z \<Longrightarrow> xs ++_f y <=_r z"
|
|
138 |
proof (induct xs)
|
|
139 |
fix y assume "y <=_r z" thus "[] ++_f y <=_r z" by simp
|
|
140 |
next
|
|
141 |
fix y l ls assume y: "y \<in> A" and "set (l#ls) \<subseteq> A"
|
|
142 |
then obtain l: "l \<in> A" and ls: "set ls \<subseteq> A" by auto
|
|
143 |
assume "\<forall>x \<in> set (l#ls). x <=_r z"
|
|
144 |
then obtain "l <=_r z" and lsz: "\<forall>x \<in> set ls. x <=_r z" by auto
|
13077
|
145 |
assume "y <=_r z" have "l +_f y <=_r z" ..
|
13069
|
146 |
moreover
|
13077
|
147 |
from l y have "l +_f y \<in> A" ..
|
13069
|
148 |
moreover
|
|
149 |
assume "\<And>y. y \<in> A \<Longrightarrow> set ls \<subseteq> A \<Longrightarrow> \<forall>x \<in> set ls. x <=_r z \<Longrightarrow> y <=_r z
|
|
150 |
\<Longrightarrow> ls ++_f y <=_r z"
|
|
151 |
ultimately
|
13077
|
152 |
have "ls ++_f (l +_f y) <=_r z" using ls lsz by -
|
13069
|
153 |
thus "(l#ls) ++_f y <=_r z" by simp
|
|
154 |
qed
|
|
155 |
|
|
156 |
|
13074
|
157 |
lemma ub1': includes semilat
|
|
158 |
shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
|
13062
|
159 |
\<Longrightarrow> b <=_r map snd [(p', t')\<in>S. p' = a] ++_f y"
|
|
160 |
proof -
|
|
161 |
let "b <=_r ?map ++_f y" = ?thesis
|
|
162 |
|
13074
|
163 |
assume "y \<in> A"
|
13062
|
164 |
moreover
|
|
165 |
assume "\<forall>(p,s) \<in> set S. s \<in> A"
|
|
166 |
hence "set ?map \<subseteq> A" by auto
|
|
167 |
moreover
|
|
168 |
assume "(a,b) \<in> set S"
|
|
169 |
hence "b \<in> set ?map" by (induct S, auto)
|
|
170 |
ultimately
|
13074
|
171 |
show ?thesis by - (rule pp_ub1)
|
13062
|
172 |
qed
|
|
173 |
|
|
174 |
|
|
175 |
|
|
176 |
lemma plusplus_empty:
|
|
177 |
"\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
|
|
178 |
(map snd [(p', t')\<in> S. p' = q] ++_f ss ! q) = ss ! q"
|
|
179 |
apply (induct S)
|
|
180 |
apply auto
|
|
181 |
done
|
|
182 |
|
|
183 |
|
|
184 |
end
|