|
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 |
|
104 lemma Nat_atleast_reset_locs [rule_format, simp]: |
|
105 "\<forall>s v. reset_locs s:v \<ge> n = (s:v \<ge> n)" |
|
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 |
|
137 theorem add_triang: |
|
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}" |
|
139 apply (rule hoare_ehoare.Meth) |
|
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) |
|
148 apply (clarsimp simp add: body_def) |
|
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" |
|
166 in hoare_ehoare.Call) |
|
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 |
|
175 apply (rule hoare_ehoare.Meth) |
|
176 apply clarsimp |
|
177 apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse) |
|
178 apply (rule Conseq) |
|
179 apply rule |
|
180 apply (rule hoare_ehoare.Asm) |
|
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 |
|
184 apply (rule hoare_ehoare.Call) |
|
185 apply (rule hoare_ehoare.LAcc) |
|
186 apply rule |
|
187 apply (rule hoare_ehoare.LAcc) |
|
188 apply clarify |
|
189 apply (rule hoare_ehoare.Meth) |
|
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) |
|
194 apply (rule hoare_ehoare.Comp) |
|
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) |
|
203 apply (rule hoare_ehoare.NewC) |
|
204 apply (auto dest!: new_AddrD elim: Nat_atleast_newC) |
|
205 done |
|
206 |
|
207 |
|
208 end |