equal
deleted
inserted
replaced
47 case Seq2 thus ?case by auto (metis D_mono D.intros(3)) |
47 case Seq2 thus ?case by auto (metis D_mono D.intros(3)) |
48 qed (auto intro: D.intros) |
48 qed (auto intro: D.intros) |
49 |
49 |
50 theorem D_sound: |
50 theorem D_sound: |
51 "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' |
51 "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' |
52 \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs'' \<or> c' = SKIP" |
52 \<Longrightarrow> (\<exists>cs''. (c',s') \<rightarrow> cs'') \<or> c' = SKIP" |
53 apply(induction arbitrary: A' rule:star_induct) |
53 apply(induction arbitrary: A' rule:star_induct) |
54 apply (metis progress) |
54 apply (metis progress) |
55 by (metis D_preservation) |
55 by (metis D_preservation) |
56 |
56 |
57 end |
57 end |