-
Notifications
You must be signed in to change notification settings - Fork 0
/
Short_Theory_9_3.thy
184 lines (153 loc) · 8.41 KB
/
Short_Theory_9_3.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
theory Short_Theory_9_3 imports "HOL-IMP.Star" Complex_Main begin
datatype val = Iv int | Rv real
type_synonym vname = string
type_synonym state = "vname \<Rightarrow> val"
datatype aexp = Ic int | Rc real | V vname | Plus aexp aexp
inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
"taval (Ic i) s (Iv i)" |
"taval (Rc r) s (Rv r)" |
"taval (V x) s (s x)" |
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2)
\<Longrightarrow> taval (Plus a1 a2) s (Iv (i1 + i2))" |
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
\<Longrightarrow> taval (Plus a1 a2) s (Rv (r1 + r2))"
inductive_cases [elim!]:
"taval (Ic i) s v" "taval (Rc i) s v"
"taval (V x) s v"
"taval (Plus a1 a2) s v"
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
"tbval (Bc v) s v" |
"tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
"tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;; _" [60, 61] 60)
| If bexp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61)
| While bexp com ("WHILE _ DO _" [0, 61] 61)
| Repeat com bexp ("REPEAT _/ UNTIL _" [60, 0] 61)
inductive small_step :: "com \<times> state \<Rightarrow> com \<times> state \<Rightarrow> bool" (infix "\<rightarrow>" 55) where
Assign: "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" |
Seq1: "(SKIP;;c,s) \<rightarrow> (c,s)" |
Seq2: "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;;c2,s) \<rightarrow> (c1';;c2,s')" |
IfTrue: "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" |
IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)" |
Repeat: "(REPEAT c UNTIL b, s) \<rightarrow> (c;; IF b THEN SKIP ELSE REPEAT c UNTIL b, s)"
lemmas small_step_induct = small_step.induct[split_format(complete)]
datatype ty = Ity | Rty
type_synonym tyenv = "vname \<Rightarrow> ty"
inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
where
Ic_ty: "\<Gamma> \<turnstile> Ic i : Ity" |
Rc_ty: "\<Gamma> \<turnstile> Rc r : Rty" |
V_ty: "\<Gamma> \<turnstile> V x : \<Gamma> x" |
Plus_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Plus a1 a2 : \<tau>"
declare atyping.intros [intro!]
inductive_cases [elim!]:
"\<Gamma> \<turnstile> V x : \<tau>" "\<Gamma> \<turnstile> Ic i : \<tau>" "\<Gamma> \<turnstile> Rc r : \<tau>" "\<Gamma> \<turnstile> Plus a1 a2 : \<tau>"
inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
where
B_ty: "\<Gamma> \<turnstile> Bc v" |
Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"
declare btyping.intros [intro!]
inductive_cases [elim!]: "\<Gamma> \<turnstile> Not b" "\<Gamma> \<turnstile> And b1 b2" "\<Gamma> \<turnstile> Less a1 a2"
inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
Skip_ty: "\<Gamma> \<turnstile> SKIP" |
Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;;c2" |
If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c" |
Repeat_ty: "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> REPEAT c UNTIL b"
declare ctyping.intros [intro!]
inductive_cases [elim!]:
"\<Gamma> \<turnstile> x ::= a" "\<Gamma> \<turnstile> c1;;c2"
"\<Gamma> \<turnstile> IF b THEN c1 ELSE c2"
"\<Gamma> \<turnstile> WHILE b DO c"
"\<Gamma> \<turnstile> REPEAT c UNTIL b"
fun type :: "val \<Rightarrow> ty" where
"type (Iv i) = Ity" |
"type (Rv r) = Rty"
lemma type_eq_Ity[simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
by (cases v) simp_all
lemma type_eq_Rty[simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)"
by (cases v) simp_all
definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>" 50)
where "\<Gamma> \<turnstile> s \<longleftrightarrow> (\<forall>x. type (s x) = \<Gamma> x)"
lemma apreservation: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
by(induct arbitrary: v rule: atyping.induct) (fastforce simp: styping_def)+
lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
proof(induct rule: atyping.induct)
case (Plus_ty \<Gamma> a1 t a2)
then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast
show ?case
proof (cases v1)
case Iv
with Plus_ty v show ?thesis
by(fastforce intro: taval.intros(4) dest!: apreservation)
next
case Rv
with Plus_ty v show ?thesis
by(fastforce intro: taval.intros(5) dest!: apreservation)
qed
qed (auto intro: taval.intros)
lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v"
proof(induct rule: btyping.induct)
case (Less_ty \<Gamma> a1 t a2)
then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
by (metis aprogress)
show ?case
proof (cases v1)
case Iv
with Less_ty v show ?thesis
by (fastforce intro!: tbval.intros(4) dest!:apreservation)
next
case Rv
with Less_ty v show ?thesis
by (fastforce intro!: tbval.intros(5) dest!:apreservation)
qed
qed (auto intro: tbval.intros)
theorem progress: "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
proof(induct rule: ctyping.induct)
case Skip_ty thus ?case by simp
next
case Assign_ty
thus ?case by (metis Assign aprogress)
next
case Seq_ty thus ?case by simp (metis Seq1 Seq2)
next
case (If_ty \<Gamma> b c1 c2)
then obtain bv where "tbval b s bv" by (metis bprogress)
show ?case
proof(cases bv)
assume "bv"
with \<open>tbval b s bv\<close> show ?case by simp (metis IfTrue)
next
assume "\<not>bv"
with \<open>tbval b s bv\<close> show ?case by simp (metis IfFalse)
qed
next
case While_ty show ?case by (metis While)
next
case Repeat_ty show ?case by (metis Repeat)
qed
theorem styping_preservation: "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'"
proof(induct rule: small_step_induct)
case Assign thus ?case
by (auto simp: styping_def) (metis Assign(1,3) apreservation)
qed auto
theorem ctyping_preservation: "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> c'"
by (induct rule: small_step_induct) (auto simp: ctyping.intros)
abbreviation small_steps :: "com \<times> state \<Rightarrow> com \<times> state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
where "x \<rightarrow>* y == star small_step x y"
theorem type_sound: "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP
\<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
by (induction rule:star_induct)
((metis progress)?, metis styping_preservation ctyping_preservation)
end