equal
deleted
inserted
replaced
153 "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)" |
153 "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)" |
154 by(simp add: err_semilat_eslI_aux split_tupled_all) |
154 by(simp add: err_semilat_eslI_aux split_tupled_all) |
155 |
155 |
156 lemma acc_err [simp, intro!]: "acc r \<Longrightarrow> acc(le r)" |
156 lemma acc_err [simp, intro!]: "acc r \<Longrightarrow> acc(le r)" |
157 apply (unfold acc_def lesub_def le_def lesssub_def) |
157 apply (unfold acc_def lesub_def le_def lesssub_def) |
158 apply (simp add: wf_eq_minimal split: err.split) |
158 apply (simp add: wfP_eq_minimal split: err.split) |
159 apply clarify |
159 apply clarify |
160 apply (case_tac "Err : Q") |
160 apply (case_tac "Err : Q") |
161 apply blast |
161 apply blast |
162 apply (erule_tac x = "{a . OK a : Q}" in allE) |
162 apply (erule_tac x = "{a . OK a : Q}" in allE) |
163 apply (case_tac "x") |
163 apply (case_tac "x") |