11565
|
1 |
(* Title: HOL/NanoJava/Example.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
Copyright 2001 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
header "Example"
|
|
8 |
|
|
9 |
theory Example = Equivalence:
|
|
10 |
|
|
11 |
text {*
|
|
12 |
|
|
13 |
\begin{verbatim}
|
|
14 |
class Nat {
|
|
15 |
|
|
16 |
Nat pred;
|
|
17 |
|
|
18 |
Nat suc()
|
|
19 |
{ Nat n = new Nat(); n.pred = this; return n; }
|
|
20 |
|
|
21 |
Nat eq(Nat n)
|
|
22 |
{ if (this.pred != null) if (n.pred != null) return this.pred.eq(n.pred);
|
|
23 |
else return n.pred; // false
|
|
24 |
else if (n.pred != null) return this.pred; // false
|
|
25 |
else return this.suc(); // true
|
|
26 |
}
|
|
27 |
|
|
28 |
Nat add(Nat n)
|
|
29 |
{ if (this.pred != null) return this.pred.add(n.suc()); else return n; }
|
|
30 |
|
|
31 |
public static void main(String[] args) // test x+1=1+x
|
|
32 |
{
|
|
33 |
Nat one = new Nat().suc();
|
|
34 |
Nat x = new Nat().suc().suc().suc().suc();
|
|
35 |
Nat ok = x.suc().eq(x.add(one));
|
|
36 |
System.out.println(ok != null);
|
|
37 |
}
|
|
38 |
}
|
|
39 |
\end{verbatim}
|
|
40 |
|
|
41 |
*}
|
|
42 |
|
|
43 |
axioms This_neq_Par [simp]: "This \<noteq> Par"
|
|
44 |
Res_neq_This [simp]: "Res \<noteq> This"
|
|
45 |
|
|
46 |
|
|
47 |
subsection "Program representation"
|
|
48 |
|
|
49 |
consts N :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *)
|
|
50 |
consts pred :: fname
|
|
51 |
consts suc :: mname
|
|
52 |
add :: mname
|
|
53 |
consts any :: vname
|
|
54 |
syntax dummy:: expr ("<>")
|
|
55 |
one :: expr
|
|
56 |
translations
|
|
57 |
"<>" == "LAcc any"
|
|
58 |
"one" == "{Nat}new Nat..suc(<>)"
|
|
59 |
|
|
60 |
text {* The following properties could be derived from a more complete
|
|
61 |
program model, which we leave out for laziness. *}
|
|
62 |
|
|
63 |
axioms Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)"
|
|
64 |
|
|
65 |
axioms method_Nat_add [simp]: "method Nat add = Some
|
|
66 |
\<lparr> par=Class Nat, res=Class Nat, lcl=[],
|
|
67 |
bdy= If((LAcc This..pred))
|
|
68 |
(Res :== {Nat}(LAcc This..pred)..add({Nat}LAcc Par..suc(<>)))
|
|
69 |
Else Res :== LAcc Par \<rparr>"
|
|
70 |
|
|
71 |
axioms method_Nat_suc [simp]: "method Nat suc = Some
|
|
72 |
\<lparr> par=NT, res=Class Nat, lcl=[],
|
|
73 |
bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \<rparr>"
|
|
74 |
|
|
75 |
axioms field_Nat [simp]: "field Nat = empty(pred\<mapsto>Class Nat)"
|
|
76 |
|
|
77 |
lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s"
|
|
78 |
by (simp add: init_locs_def init_vars_def)
|
|
79 |
|
|
80 |
lemma init_locs_Nat_suc [simp]: "init_locs Nat suc s = s"
|
|
81 |
by (simp add: init_locs_def init_vars_def)
|
|
82 |
|
|
83 |
lemma upd_obj_new_obj_Nat [simp]:
|
|
84 |
"upd_obj a pred v (new_obj a Nat s) = hupd(a\<mapsto>(Nat, empty(pred\<mapsto>v))) s"
|
|
85 |
by (simp add: new_obj_def init_vars_def upd_obj_def Let_def)
|
|
86 |
|
|
87 |
|
|
88 |
subsection "``atleast'' relation for interpretation of Nat ``values''"
|
|
89 |
|
|
90 |
consts Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50)
|
|
91 |
primrec "s:x\<ge>0 = (x\<noteq>Null)"
|
|
92 |
"s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
|
|
93 |
|
|
94 |
lemma Nat_atleast_lupd [rule_format, simp]:
|
|
95 |
"\<forall>s v. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"
|
|
96 |
apply (induct n)
|
|
97 |
by auto
|
|
98 |
|
|
99 |
lemma Nat_atleast_set_locs [rule_format, simp]:
|
|
100 |
"\<forall>s v. set_locs l s:v \<ge> n = (s:v \<ge> n)"
|
|
101 |
apply (induct n)
|
|
102 |
by auto
|
|
103 |
|
11772
|
104 |
lemma Nat_atleast_del_locs [rule_format, simp]:
|
|
105 |
"\<forall>s v. del_locs s:v \<ge> n = (s:v \<ge> n)"
|
11565
|
106 |
apply (induct n)
|
|
107 |
by auto
|
|
108 |
|
|
109 |
lemma Nat_atleast_NullD [rule_format]: "s:Null \<ge> n \<longrightarrow> False"
|
|
110 |
apply (induct n)
|
|
111 |
by auto
|
|
112 |
|
|
113 |
lemma Nat_atleast_pred_NullD [rule_format]:
|
|
114 |
"Null = get_field s a pred \<Longrightarrow> s:Addr a \<ge> n \<longrightarrow> n = 0"
|
|
115 |
apply (induct n)
|
|
116 |
by (auto dest: Nat_atleast_NullD)
|
|
117 |
|
|
118 |
lemma Nat_atleast_mono [rule_format]:
|
|
119 |
"\<forall>a. s:get_field s a pred \<ge> n \<longrightarrow> heap s a \<noteq> None \<longrightarrow> s:Addr a \<ge> n"
|
|
120 |
apply (induct n)
|
|
121 |
by auto
|
|
122 |
|
|
123 |
lemma Nat_atleast_newC [rule_format]:
|
|
124 |
"heap s aa = None \<Longrightarrow> \<forall>v. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> n"
|
|
125 |
apply (induct n)
|
|
126 |
apply auto
|
|
127 |
apply (case_tac "aa=a")
|
|
128 |
apply auto
|
|
129 |
apply (tactic "smp_tac 1 1")
|
|
130 |
apply (case_tac "aa=a")
|
|
131 |
apply auto
|
|
132 |
done
|
|
133 |
|
|
134 |
|
|
135 |
subsection "Proof(s) using the Hoare logic"
|
|
136 |
|
12742
|
137 |
theorem add_homomorph_lb:
|
11565
|
138 |
"{} \<turnstile> {\<lambda>s. s:s<This> \<ge> X \<and> s:s<Par> \<ge> Y} Meth(Nat,add) {\<lambda>s. s:s<Res> \<ge> X+Y}"
|
12742
|
139 |
apply (rule hoare_ehoare.Meth) (* 1 *)
|
11565
|
140 |
apply clarsimp
|
|
141 |
apply (rule_tac P'= "\<lambda>Z s. (s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z) \<and> D=Nat" and
|
|
142 |
Q'= "\<lambda>Z s. s:s<Res> \<ge> fst Z+snd Z" in Conseq)
|
|
143 |
prefer 2
|
|
144 |
apply (clarsimp simp add: init_locs_def init_vars_def)
|
|
145 |
apply rule
|
|
146 |
apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
|
|
147 |
apply (rule_tac P = "\<lambda>Z Cm s. s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z" in Impl1)
|
12742
|
148 |
apply (clarsimp simp add: body_def) (* 4 *)
|
11565
|
149 |
apply (rename_tac n m)
|
|
150 |
apply (rule_tac Q = "\<lambda>v s. (s:s<This> \<ge> n \<and> s:s<Par> \<ge> m) \<and>
|
|
151 |
(\<exists>a. s<This> = Addr a \<and> v = get_field s a pred)" in hoare_ehoare.Cond)
|
|
152 |
apply (rule hoare_ehoare.FAcc)
|
|
153 |
apply (rule eConseq1)
|
|
154 |
apply (rule hoare_ehoare.LAcc)
|
|
155 |
apply fast
|
|
156 |
apply auto
|
|
157 |
prefer 2
|
|
158 |
apply (rule hoare_ehoare.LAss)
|
|
159 |
apply (rule eConseq1)
|
|
160 |
apply (rule hoare_ehoare.LAcc)
|
|
161 |
apply (auto dest: Nat_atleast_pred_NullD)
|
|
162 |
apply (rule hoare_ehoare.LAss)
|
|
163 |
apply (rule_tac
|
|
164 |
Q = "\<lambda>v s. (\<forall>m. n = Suc m \<longrightarrow> s:v \<ge> m) \<and> s:s<Par> \<ge> m" and
|
|
165 |
R = "\<lambda>T P s. (\<forall>m. n = Suc m \<longrightarrow> s:T \<ge> m) \<and> s:P \<ge> Suc m"
|
12742
|
166 |
in hoare_ehoare.Call) (* 13 *)
|
11565
|
167 |
apply (rule hoare_ehoare.FAcc)
|
|
168 |
apply (rule eConseq1)
|
|
169 |
apply (rule hoare_ehoare.LAcc)
|
|
170 |
apply clarify
|
|
171 |
apply (drule sym, rotate_tac -1, frule (1) trans)
|
|
172 |
apply simp
|
|
173 |
prefer 2
|
|
174 |
apply clarsimp
|
12742
|
175 |
apply (rule hoare_ehoare.Meth) (* 17 *)
|
11565
|
176 |
apply clarsimp
|
|
177 |
apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
|
|
178 |
apply (rule Conseq)
|
|
179 |
apply rule
|
12742
|
180 |
apply (rule hoare_ehoare.Asm) (* 20 *)
|
11565
|
181 |
apply (rule_tac a = "((case n of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+)
|
|
182 |
apply (clarsimp split add: nat.split_asm dest!: Nat_atleast_mono)
|
|
183 |
apply rule
|
12742
|
184 |
apply (rule hoare_ehoare.Call) (* 21 *)
|
11565
|
185 |
apply (rule hoare_ehoare.LAcc)
|
|
186 |
apply rule
|
|
187 |
apply (rule hoare_ehoare.LAcc)
|
|
188 |
apply clarify
|
12742
|
189 |
apply (rule hoare_ehoare.Meth) (* 24 *)
|
11565
|
190 |
apply clarsimp
|
|
191 |
apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
|
|
192 |
apply (rule Impl1)
|
|
193 |
apply (clarsimp simp add: body_def)
|
12742
|
194 |
apply (rule hoare_ehoare.Comp) (* 26 *)
|
11565
|
195 |
prefer 2
|
|
196 |
apply (rule hoare_ehoare.FAss)
|
|
197 |
prefer 2
|
|
198 |
apply rule
|
|
199 |
apply (rule hoare_ehoare.LAcc)
|
|
200 |
apply (rule hoare_ehoare.LAcc)
|
|
201 |
apply (rule hoare_ehoare.LAss)
|
|
202 |
apply (rule eConseq1)
|
12742
|
203 |
apply (rule hoare_ehoare.NewC) (* 32 *)
|
11565
|
204 |
apply (auto dest!: new_AddrD elim: Nat_atleast_newC)
|
|
205 |
done
|
|
206 |
|
|
207 |
|
|
208 |
end
|