# 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: "\ sorted (map fst ps @ [a]); x < a \ \ - upd_list x y (ps @ (a,b) # qs) = upd_list x y ps @ (a,b) # qs" +lemma upd_list_sorted: "sorted1 (ps @ [(a,b)]) \ + 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: "\ sorted (map fst ps @ [a]); a \ x \ \ +text\In principle, @{thm upd_list_sorted} suffices, but the following two +corollaries speed up proofs.\ + +corollary upd_list_sorted1: "\ sorted (map fst ps @ [a]); x < a \ \ + 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: "\ sorted (map fst ps @ [a]); a \ x \ \ 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 \ set(map fst xs) \ del_list x xs = xs" by (induct xs) auto -lemma del_list_sorted1: "sorted1 (xs @ [(a,b)]) \ a \ x \ +lemma del_list_sorted: "sorted1 (ps @ (a,b) # qs) \ + 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\In principle, @{thm del_list_sorted} suffices, but the following +corollaries speed up proofs.\ + +corollary del_list_sorted1: "sorted1 (xs @ (a,b) # ys) \ a \ x \ 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) \ x < a \ 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) \ x < b \ 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) \ x < c \ 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) \ x < d \ 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