Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Conditionally_Complete_Lattices.thy Sprache: Isabelle

Original von: Isabelle^©

(* Author: Tobias Nipkow *)

section \<open>Association List Update and Deletion\<close>

theory AList_Upd_Del
imports Sorted_Less
begin

abbreviation "sorted1 ps \ sorted(map fst ps)"

text\<open>Define own \<open>map_of\<close> function to avoid pulling in an unknown
amount of lemmas implicitly (via the simpset).\<close>

hide_const (open) map_of

fun map_of :: "('a*'b)list \ 'a \ 'b option" where
"map_of [] = (\x. None)" |
"map_of ((a,b)#ps) = (\x. if x=a then Some b else map_of ps x)"

text \<open>Updating an association list:\<close>

fun upd_list :: "'a::linorder \ 'b \ ('a*'b) list \ ('a*'b) list" where
"upd_list x y [] = [(x,y)]" |
"upd_list x y ((a,b)#ps) =
  (if x < a then (x,y)#(a,b)#ps else
  if x = a then (x,y)#ps else (a,b) # upd_list x y ps)"

fun del_list :: "'a::linorder \ ('a*'b)list \ ('a*'b)list" where
"del_list x [] = []" |
"del_list x ((a,b)#ps) = (if x = a then ps else (a,b) # del_list x ps)"

subsection \<open>Lemmas for \<^const>\<open>map_of\<close>\<close>

lemma map_of_ins_list: "map_of (upd_list x y ps) = (map_of ps)(x := Some y)"
by(induction ps) auto

lemma map_of_append: "map_of (ps @ qs) x =
  (case map_of ps x of None \<Rightarrow> map_of qs x | Some y \<Rightarrow> Some y)"
by(induction ps)(auto)

lemma map_of_None: "sorted (x # map fst ps) \ map_of ps x = None"
by (induction ps) (fastforce simp: sorted_lems sorted_wrt_Cons)+

lemma map_of_None2: "sorted (map fst ps @ [x]) \ map_of ps x = None"
by (induction ps) (auto simp: sorted_lems)

lemma map_of_del_list: "sorted1 ps \
  map_of(del_list x ps) = (map_of ps)(x := None)"
by(induction ps) (auto simp: map_of_None sorted_lems fun_eq_iff)

lemma map_of_sorted_Cons: "sorted (a # map fst ps) \ x < a \
   map_of ps x = None"
by (simp add: map_of_None sorted_Cons_le)

lemma map_of_sorted_snoc: "sorted (map fst ps @ [a]) \ a \ x \
  map_of ps x = None"
by (simp add: map_of_None2 sorted_snoc_le)

lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc
lemmas map_of_simps = sorted_lems map_of_append map_of_sorteds

subsection \<open>Lemmas for \<^const>\<open>upd_list\<close>\<close>

lemma sorted_upd_list: "sorted1 ps \ sorted1 (upd_list x y ps)"
apply(induction ps)
apply simp
apply(case_tac ps)
apply auto
done

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)

text\<open>In principle, @{thm upd_list_sorted} suffices, but the following two
corollaries speed up proofs.\<close>

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 (auto simp: upd_list_sorted)

lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2

text\<open>Splay trees need two additional \<^const>\<open>upd_list\<close> lemmas:\<close>

lemma upd_list_Cons:
  "sorted1 ((x,y) # xs) \ upd_list x y xs = (x,y) # xs"
by (induction xs) auto

lemma upd_list_snoc:
  "sorted1 (xs @ [(x,y)]) \ upd_list x y xs = xs @ [(x,y)]"
by(induction xs) (auto simp add: sorted_mid_iff2)

subsection \<open>Lemmas for \<^const>\<open>del_list\<close>\<close>

lemma sorted_del_list: "sorted1 ps \ sorted1 (del_list x ps)"
apply(induction ps)
apply simp
apply(case_tac ps)
apply (auto simp: sorted_Cons_le)
done

lemma del_list_idem: "x \ set(map fst xs) \ del_list x xs = xs"
by (induct xs) auto

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_wrt_Cons 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) \ a \ x \
  del_list x (xs @ (a,b) # ys) = xs @ del_list x ((a,b) # ys)"
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 (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 (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 (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 (auto simp: del_list_sorted sorted_lems)

lemmas del_list_simps = sorted_lems
  del_list_sorted1
  del_list_sorted2
  del_list_sorted3
  del_list_sorted4
  del_list_sorted5

text\<open>Splay trees need two additional \<^const>\<open>del_list\<close> lemmas:\<close>

lemma del_list_notin_Cons: "sorted (x # map fst xs) \ del_list x xs = xs"
by(induction xs)(fastforce simp: sorted_wrt_Cons)+

lemma del_list_sorted_app:
  "sorted(map fst xs @ [x]) \ del_list x (xs @ ys) = xs @ del_list x ys"
by (induction xs) (auto simp: sorted_mid_iff2)

end

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.