equal
deleted
inserted
replaced
449 |
449 |
450 lemma max_of_list_append [simp]: |
450 lemma max_of_list_append [simp]: |
451 "max_of_list (xs @ ys) = max (max_of_list xs) (max_of_list ys)" |
451 "max_of_list (xs @ ys) = max (max_of_list xs) (max_of_list ys)" |
452 apply (simp add: max_of_list_def) |
452 apply (simp add: max_of_list_def) |
453 apply (induct xs) |
453 apply (induct xs) |
454 apply simp |
454 apply simp_all |
455 using [[linarith_split_limit = 0]] |
|
456 apply simp |
|
457 apply arith |
|
458 done |
455 done |
459 |
456 |
460 |
457 |
461 lemma app_mono_mxs: "\<lbrakk> app i G mxs rT pc et s; mxs \<le> mxs' \<rbrakk> |
458 lemma app_mono_mxs: "\<lbrakk> app i G mxs rT pc et s; mxs \<le> mxs' \<rbrakk> |
462 \<Longrightarrow> app i G mxs' rT pc et s" |
459 \<Longrightarrow> app i G mxs' rT pc et s" |