# HG changeset patch
# User nipkow
# Date 1447771908 -3600
# Node ID df4a03527b565f7df9b2136c054f9785738b96c8
# Parent  6571c78c966714772cb5feb20dc77f661cc73a3b
derive lemmas uniformly

diff -r 6571c78c9667 -r df4a03527b56 src/HOL/Data_Structures/AList_Upd_Del.thy
--- a/src/HOL/Data_Structures/AList_Upd_Del.thy	Tue Nov 17 12:32:08 2015 +0000
+++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Tue Nov 17 15:51:48 2015 +0100
@@ -70,13 +70,22 @@
  apply auto
 done
 
-lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [a]); x < a \<rbrakk> \<Longrightarrow>
-  upd_list x y (ps @ (a,b) # qs) =  upd_list x y ps @ (a,b) # qs"
+lemma upd_list_sorted: "sorted1 (ps @ [(a,b)]) \<Longrightarrow>
+  upd_list x y (ps @ (a,b) # qs) =
+    (if x < a then upd_list x y ps @ (a,b) # qs
+    else ps @ upd_list x y ((a,b) # qs))"
 by(induction ps) (auto simp: sorted_lems)
 
-lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [a]); a \<le> x \<rbrakk> \<Longrightarrow>
+text\<open>In principle, @{thm upd_list_sorted} suffices, but the following two
+corollaries speed up proofs.\<close>
+
+corollary upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [a]); x < a \<rbrakk> \<Longrightarrow>
+  upd_list x y (ps @ (a,b) # qs) =  upd_list x y ps @ (a,b) # qs"
+by (auto simp: upd_list_sorted)
+
+corollary upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [a]); a \<le> x \<rbrakk> \<Longrightarrow>
   upd_list x y (ps @ (a,b) # qs) = ps @ upd_list x y ((a,b) # qs)"
-by(induction ps) (auto simp: sorted_lems)
+by (auto simp: upd_list_sorted)
 
 lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2
 
@@ -93,33 +102,41 @@
 lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs"
 by (induct xs) auto
 
-lemma del_list_sorted1: "sorted1 (xs @ [(a,b)]) \<Longrightarrow> a \<le> x \<Longrightarrow>
+lemma del_list_sorted: "sorted1 (ps @ (a,b) # qs) \<Longrightarrow>
+  del_list x (ps @ (a,b) # qs) =
+    (if x < a then del_list x ps @ (a,b) # qs
+     else ps @ del_list x ((a,b) # qs))"
+by(induction ps)
+  (fastforce simp: sorted_lems sorted_Cons_iff intro!: del_list_idem)+
+
+text\<open>In principle, @{thm del_list_sorted} suffices, but the following
+corollaries speed up proofs.\<close>
+
+corollary del_list_sorted1: "sorted1 (xs @ (a,b) # ys) \<Longrightarrow> a \<le> x \<Longrightarrow>
   del_list x (xs @ (a,b) # ys) = xs @ del_list x ((a,b) # ys)"
-by (induction xs) (auto simp: sorted_mid_iff2)
+by (auto simp: del_list_sorted)
 
 lemma del_list_sorted2: "sorted1 (xs @ (a,b) # ys) \<Longrightarrow> x < a \<Longrightarrow>
   del_list x (xs @ (a,b) # ys) = del_list x xs @ (a,b) # ys"
-by (induction xs) (fastforce simp: sorted_Cons_iff intro!: del_list_idem)+
+by (auto simp: del_list_sorted)
 
 lemma del_list_sorted3:
   "sorted1 (xs @ (a,a') # ys @ (b,b') # zs) \<Longrightarrow> x < b \<Longrightarrow>
   del_list x (xs @ (a,a') # ys @ (b,b') # zs) = del_list x (xs @ (a,a') # ys) @ (b,b') # zs"
-by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2 ball_Un)
+by (auto simp: del_list_sorted sorted_lems)
 
 lemma del_list_sorted4:
   "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) \<Longrightarrow> x < c \<Longrightarrow>
   del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) = del_list x (xs @ (a,a') # ys @ (b,b') # zs) @ (c,c') # us"
-by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
+by (auto simp: del_list_sorted sorted_lems)
 
 lemma del_list_sorted5:
   "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) \<Longrightarrow> x < d \<Longrightarrow>
    del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) =
    del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) @ (d,d') # vs" 
-by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
+by (auto simp: del_list_sorted sorted_lems)
 
-lemmas del_list_sorted =
+lemmas del_list_simps = sorted_lems
   del_list_sorted1 del_list_sorted2 del_list_sorted3 del_list_sorted4 del_list_sorted5
 
-lemmas del_list_simps = sorted_lems del_list_sorted
-
 end