author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45212  e87feee00a4c 
child 47818  151d137f1095 
permissions  rwrr 
43150  1 
header "A Typed Language" 
2 

3 
theory Types imports Star Complex_Main begin 

4 

5 
subsection "Arithmetic Expressions" 

6 

7 
datatype val = Iv int  Rv real 

8 

45212  9 
type_synonym vname = string 
10 
type_synonym state = "vname \<Rightarrow> val" 

43150  11 

45212  12 
datatype aexp = Ic int  Rc real  V vname  Plus aexp aexp 
43150  13 

14 
inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where 

15 
"taval (Ic i) s (Iv i)"  

16 
"taval (Rc r) s (Rv r)"  

17 
"taval (V x) s (s x)"  

18 
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) 

19 
\<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))"  

44020  20 
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) 
43150  21 
\<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))" 
22 

23 
inductive_cases [elim!]: 

24 
"taval (Ic i) s v" "taval (Rc i) s v" 

25 
"taval (V x) s v" 

26 
"taval (Plus a1 a2) s v" 

27 

28 
subsection "Boolean Expressions" 

29 

45200  30 
datatype bexp = Bc bool  Not bexp  And bexp bexp  Less aexp aexp 
43150  31 

32 
inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where 

45200  33 
"tbval (Bc v) s v"  
43150  34 
"tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)"  
44020  35 
"tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)"  
36 
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)"  

37 
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)" 

43150  38 

39 
subsection "Syntax of Commands" 

40 
(* a copy of Com.thy  keep in sync! *) 

41 

42 
datatype 

43 
com = SKIP 

45212  44 
 Assign vname aexp ("_ ::= _" [1000, 61] 61) 
43150  45 
 Semi com com ("_; _" [60, 61] 60) 
46 
 If bexp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61) 

47 
 While bexp com ("WHILE _ DO _" [0, 61] 61) 

48 

49 

50 
subsection "SmallStep Semantics of Commands" 

51 

52 
inductive 

53 
small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55) 

54 
where 

55 
Assign: "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))"  

56 

57 
Semi1: "(SKIP;c,s) \<rightarrow> (c,s)"  

58 
Semi2: "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')"  

59 

60 
IfTrue: "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)"  

61 
IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)"  

62 

63 
While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)" 

64 

65 
lemmas small_step_induct = small_step.induct[split_format(complete)] 

66 

67 
subsection "The Type System" 

68 

69 
datatype ty = Ity  Rty 

70 

45212  71 
type_synonym tyenv = "vname \<Rightarrow> ty" 
43150  72 

73 
inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool" 

74 
("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50) 

75 
where 

76 
Ic_ty: "\<Gamma> \<turnstile> Ic i : Ity"  

77 
Rc_ty: "\<Gamma> \<turnstile> Rc r : Rty"  

78 
V_ty: "\<Gamma> \<turnstile> V x : \<Gamma> x"  

79 
Plus_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Plus a1 a2 : \<tau>" 

80 

81 
text{* Warning: the ``:'' notation leads to syntactic ambiguities, 

82 
i.e. multiple parse trees, because ``:'' also stands for set membership. 

83 
In most situations Isabelle's type system will reject all but one parse tree, 

84 
but will still inform you of the potential ambiguity. *} 

85 

86 
inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50) 

87 
where 

45200  88 
B_ty: "\<Gamma> \<turnstile> Bc v"  
43150  89 
Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b"  
90 
And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2"  

91 
Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2" 

92 

93 
inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where 

94 
Skip_ty: "\<Gamma> \<turnstile> SKIP"  

95 
Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a"  

96 
Semi_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2"  

97 
If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2"  

98 
While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c" 

99 

100 
inductive_cases [elim!]: 

101 
"\<Gamma> \<turnstile> x ::= a" "\<Gamma> \<turnstile> c1;c2" 

102 
"\<Gamma> \<turnstile> IF b THEN c1 ELSE c2" 

103 
"\<Gamma> \<turnstile> WHILE b DO c" 

104 

105 
subsection "Welltyped Programs Do Not Get Stuck" 

106 

107 
fun type :: "val \<Rightarrow> ty" where 

108 
"type (Iv i) = Ity"  

109 
"type (Rv r) = Rty" 

110 

111 
lemma [simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)" 

112 
by (cases v) simp_all 

113 

114 
lemma [simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)" 

115 
by (cases v) simp_all 

116 

117 
definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>" 50) 

118 
where "\<Gamma> \<turnstile> s \<longleftrightarrow> (\<forall>x. type (s x) = \<Gamma> x)" 

119 

120 
lemma apreservation: 

121 
"\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>" 

45015  122 
apply(induction arbitrary: v rule: atyping.induct) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44020
diff
changeset

123 
apply (fastforce simp: styping_def)+ 
43150  124 
done 
125 

126 
lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v" 

45015  127 
proof(induction rule: atyping.induct) 
43150  128 
case (Plus_ty \<Gamma> a1 t a2) 
129 
then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast 

130 
show ?case 

131 
proof (cases v1) 

132 
case Iv 

45015  133 
with Plus_ty v show ?thesis 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44020
diff
changeset

134 
by(fastforce intro: taval.intros(4) dest!: apreservation) 
43150  135 
next 
136 
case Rv 

45015  137 
with Plus_ty v show ?thesis 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44020
diff
changeset

138 
by(fastforce intro: taval.intros(5) dest!: apreservation) 
43150  139 
qed 
140 
qed (auto intro: taval.intros) 

141 

142 
lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v" 

45015  143 
proof(induction rule: btyping.induct) 
43150  144 
case (Less_ty \<Gamma> a1 t a2) 
145 
then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" 

146 
by (metis aprogress) 

147 
show ?case 

148 
proof (cases v1) 

149 
case Iv 

150 
with Less_ty v show ?thesis 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44020
diff
changeset

151 
by (fastforce intro!: tbval.intros(4) dest!:apreservation) 
43150  152 
next 
153 
case Rv 

154 
with Less_ty v show ?thesis 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44020
diff
changeset

155 
by (fastforce intro!: tbval.intros(5) dest!:apreservation) 
43150  156 
qed 
157 
qed (auto intro: tbval.intros) 

158 

159 
theorem progress: 

160 
"\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'" 

45015  161 
proof(induction rule: ctyping.induct) 
43150  162 
case Skip_ty thus ?case by simp 
163 
next 

164 
case Assign_ty 

165 
thus ?case by (metis Assign aprogress) 

166 
next 

167 
case Semi_ty thus ?case by simp (metis Semi1 Semi2) 

168 
next 

169 
case (If_ty \<Gamma> b c1 c2) 

170 
then obtain bv where "tbval b s bv" by (metis bprogress) 

171 
show ?case 

172 
proof(cases bv) 

173 
assume "bv" 

174 
with `tbval b s bv` show ?case by simp (metis IfTrue) 

175 
next 

176 
assume "\<not>bv" 

177 
with `tbval b s bv` show ?case by simp (metis IfFalse) 

178 
qed 

179 
next 

180 
case While_ty show ?case by (metis While) 

181 
qed 

182 

183 
theorem styping_preservation: 

184 
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'" 

45015  185 
proof(induction rule: small_step_induct) 
43150  186 
case Assign thus ?case 
187 
by (auto simp: styping_def) (metis Assign(1,3) apreservation) 

188 
qed auto 

189 

190 
theorem ctyping_preservation: 

191 
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> c'" 

192 
by (induct rule: small_step_induct) (auto simp: ctyping.intros) 

193 

194 
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55) 

195 
where "x \<rightarrow>* y == star small_step x y" 

196 

197 
theorem type_sound: 

198 
"(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP 

199 
\<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''" 

45015  200 
apply(induction rule:star_induct) 
43150  201 
apply (metis progress) 
202 
by (metis styping_preservation ctyping_preservation) 

203 

204 
end 