118 where "\<Gamma> \<turnstile> s \<longleftrightarrow> (\<forall>x. type (s x) = \<Gamma> x)" |
118 where "\<Gamma> \<turnstile> s \<longleftrightarrow> (\<forall>x. type (s x) = \<Gamma> x)" |
119 |
119 |
120 lemma apreservation: |
120 lemma apreservation: |
121 "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>" |
121 "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>" |
122 apply(induct arbitrary: v rule: atyping.induct) |
122 apply(induct arbitrary: v rule: atyping.induct) |
123 apply (fastsimp simp: styping_def)+ |
123 apply (fastforce simp: styping_def)+ |
124 done |
124 done |
125 |
125 |
126 lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v" |
126 lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v" |
127 proof(induct rule: atyping.induct) |
127 proof(induct rule: atyping.induct) |
128 case (Plus_ty \<Gamma> a1 t a2) |
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 |
129 then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast |
130 show ?case |
130 show ?case |
131 proof (cases v1) |
131 proof (cases v1) |
132 case Iv |
132 case Iv |
133 with Plus_ty(1,3,5) v show ?thesis |
133 with Plus_ty(1,3,5) v show ?thesis |
134 by(fastsimp intro: taval.intros(4) dest!: apreservation) |
134 by(fastforce intro: taval.intros(4) dest!: apreservation) |
135 next |
135 next |
136 case Rv |
136 case Rv |
137 with Plus_ty(1,3,5) v show ?thesis |
137 with Plus_ty(1,3,5) v show ?thesis |
138 by(fastsimp intro: taval.intros(5) dest!: apreservation) |
138 by(fastforce intro: taval.intros(5) dest!: apreservation) |
139 qed |
139 qed |
140 qed (auto intro: taval.intros) |
140 qed (auto intro: taval.intros) |
141 |
141 |
142 lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v" |
142 lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v" |
143 proof(induct rule: btyping.induct) |
143 proof(induct rule: btyping.induct) |
146 by (metis aprogress) |
146 by (metis aprogress) |
147 show ?case |
147 show ?case |
148 proof (cases v1) |
148 proof (cases v1) |
149 case Iv |
149 case Iv |
150 with Less_ty v show ?thesis |
150 with Less_ty v show ?thesis |
151 by (fastsimp intro!: tbval.intros(4) dest!:apreservation) |
151 by (fastforce intro!: tbval.intros(4) dest!:apreservation) |
152 next |
152 next |
153 case Rv |
153 case Rv |
154 with Less_ty v show ?thesis |
154 with Less_ty v show ?thesis |
155 by (fastsimp intro!: tbval.intros(5) dest!:apreservation) |
155 by (fastforce intro!: tbval.intros(5) dest!:apreservation) |
156 qed |
156 qed |
157 qed (auto intro: tbval.intros) |
157 qed (auto intro: tbval.intros) |
158 |
158 |
159 theorem progress: |
159 theorem progress: |
160 "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'" |
160 "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'" |