281 apply simp |
281 apply simp |
282 apply (force simp add: nth_Cons split: list.split nat.split) |
282 apply (force simp add: nth_Cons split: list.split nat.split) |
283 done |
283 done |
284 |
284 |
285 |
285 |
286 lemma (in semilat) plus_list_ub1 [rule_format]: |
286 lemma (in Semilat) plus_list_ub1 [rule_format]: |
287 "\<lbrakk> set xs <= A; set ys <= A; size xs = size ys \<rbrakk> |
287 "\<lbrakk> set xs <= A; set ys <= A; size xs = size ys \<rbrakk> |
288 \<Longrightarrow> xs <=[r] xs +[f] ys" |
288 \<Longrightarrow> xs <=[r] xs +[f] ys" |
289 apply (unfold unfold_lesub_list) |
289 apply (unfold unfold_lesub_list) |
290 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
290 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
291 done |
291 done |
292 |
292 |
293 lemma (in semilat) plus_list_ub2: |
293 lemma (in Semilat) plus_list_ub2: |
294 "\<lbrakk>set xs <= A; set ys <= A; size xs = size ys \<rbrakk> |
294 "\<lbrakk>set xs <= A; set ys <= A; size xs = size ys \<rbrakk> |
295 \<Longrightarrow> ys <=[r] xs +[f] ys" |
295 \<Longrightarrow> ys <=[r] xs +[f] ys" |
296 apply (unfold unfold_lesub_list) |
296 apply (unfold unfold_lesub_list) |
297 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
297 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
298 done |
298 done |
299 |
299 |
300 lemma (in semilat) plus_list_lub [rule_format]: |
300 lemma (in Semilat) plus_list_lub [rule_format]: |
301 shows "!xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A |
301 shows "!xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A |
302 \<longrightarrow> size xs = n & size ys = n \<longrightarrow> |
302 \<longrightarrow> size xs = n & size ys = n \<longrightarrow> |
303 xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs" |
303 xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs" |
304 apply (unfold unfold_lesub_list) |
304 apply (unfold unfold_lesub_list) |
305 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
305 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
306 done |
306 done |
307 |
307 |
308 lemma (in semilat) list_update_incr [rule_format]: |
308 lemma (in Semilat) list_update_incr [rule_format]: |
309 "x\<in> A \<Longrightarrow> set xs <= A \<longrightarrow> |
309 "x\<in> A \<Longrightarrow> set xs <= A \<longrightarrow> |
310 (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])" |
310 (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])" |
311 apply (unfold unfold_lesub_list) |
311 apply (unfold unfold_lesub_list) |
312 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
312 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
313 apply (induct xs) |
313 apply (induct xs) |
378 |
378 |
379 |
379 |
380 lemma Listn_sl_aux: |
380 lemma Listn_sl_aux: |
381 assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))" |
381 assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))" |
382 proof - |
382 proof - |
383 interpret semilat [A r f] by fact |
383 interpret Semilat [A r f] using assms by (rule Semilat.intro) |
384 show ?thesis |
384 show ?thesis |
385 apply (unfold Listn.sl_def) |
385 apply (unfold Listn.sl_def) |
386 apply (simp (no_asm) only: semilat_Def split_conv) |
386 apply (simp (no_asm) only: semilat_Def split_conv) |
387 apply (rule conjI) |
387 apply (rule conjI) |
388 apply simp |
388 apply simp |
515 "err_semilat (A,r,f) \<Longrightarrow> |
515 "err_semilat (A,r,f) \<Longrightarrow> |
516 err_semilat (list n A, Listn.le r, sup f)" |
516 err_semilat (list n A, Listn.le r, sup f)" |
517 apply (unfold Err.sl_def) |
517 apply (unfold Err.sl_def) |
518 apply (simp only: split_conv) |
518 apply (simp only: split_conv) |
519 apply (simp (no_asm) only: semilat_Def plussub_def) |
519 apply (simp (no_asm) only: semilat_Def plussub_def) |
520 apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup) |
520 apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup) |
521 apply (rule conjI) |
521 apply (rule conjI) |
522 apply (drule semilat.orderI) |
522 apply (drule Semilat.orderI [OF Semilat.intro]) |
523 apply simp |
523 apply simp |
524 apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def) |
524 apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def) |
525 apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split) |
525 apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split) |
526 apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D) |
526 apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D) |
527 done |
527 done |