equal
deleted
inserted
replaced
57 qed |
57 qed |
58 |
58 |
59 end |
59 end |
60 |
60 |
61 lemma less_eq_acom_annos: |
61 lemma less_eq_acom_annos: |
62 "C1 \<le> C2 \<longleftrightarrow> strip C1 = strip C2 \<and> list_all2 (op \<le>) (annos C1) (annos C2)" |
62 "C1 \<le> C2 \<longleftrightarrow> strip C1 = strip C2 \<and> list_all2 (\<le>) (annos C1) (annos C2)" |
63 by(auto simp add: less_eq_acom_def anno_def list_all2_conv_all_nth size_annos_same2) |
63 by(auto simp add: less_eq_acom_def anno_def list_all2_conv_all_nth size_annos_same2) |
64 |
64 |
65 lemma SKIP_le[simp]: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')" |
65 lemma SKIP_le[simp]: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')" |
66 by (cases c) (auto simp:less_eq_acom_def anno_def) |
66 by (cases c) (auto simp:less_eq_acom_def anno_def) |
67 |
67 |