author  berghofe 
Fri, 13 Oct 2006 18:15:18 +0200  
changeset 21020  9af9ceb16d58 
parent 16417  9bc16273c2d4 
child 32960  69916a850301 
permissions  rwrr 
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 

16417  9 
theory Example imports Equivalence begin 
11565  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]: 

21020  95 
"\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)" 
11565  96 
apply (induct n) 
97 
by auto 

98 

99 
lemma Nat_atleast_set_locs [rule_format, simp]: 

21020  100 
"\<forall>s v::val. set_locs l s:v \<ge> n = (s:v \<ge> n)" 
11565  101 
apply (induct n) 
102 
by auto 

103 

11772  104 
lemma Nat_atleast_del_locs [rule_format, simp]: 
21020  105 
"\<forall>s v::val. 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]: 

21020  124 
"heap s aa = None \<Longrightarrow> \<forall>v::val. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> n" 
11565  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 

12934
6003b4f916c0
Clarification wrt. use of polymorphic variants of Hoare logic rules
oheimb
parents:
12742
diff
changeset

142 
Q'= "\<lambda>Z s. s:s<Res> \<ge> fst Z+snd Z" in AxSem.Conseq) 
11565  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) 

12934
6003b4f916c0
Clarification wrt. use of polymorphic variants of Hoare logic rules
oheimb
parents:
12742
diff
changeset

147 
apply (rule_tac P = "\<lambda>Z Cm s. s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z" in AxSem.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) 

12934
6003b4f916c0
Clarification wrt. use of polymorphic variants of Hoare logic rules
oheimb
parents:
12742
diff
changeset

178 
apply (rule AxSem.Conseq) 
11565  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) 

12934
6003b4f916c0
Clarification wrt. use of polymorphic variants of Hoare logic rules
oheimb
parents:
12742
diff
changeset

192 
apply (rule AxSem.Impl1) 
11565  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 