# HG changeset patch # User blanchet # Date 1271425786 -7200 # Node ID 2c787345c0831f4aeace6c3ce5eb990b62220e70 # Parent da7b40aa221598cf6e701fa384851d0ea3212f5e# Parent 0cdb76723c88023bed5a2f4f8c032be78cebca05 merged diff -r 0cdb76723c88 -r 2c787345c083 Admin/isatest/isatest-makeall --- a/Admin/isatest/isatest-makeall Fri Apr 16 15:49:13 2010 +0200 +++ b/Admin/isatest/isatest-makeall Fri Apr 16 15:49:46 2010 +0200 @@ -186,7 +186,7 @@ echo >> $ERRORLOG FAIL="$FAIL$SHORT " - (cd $ERRORDIR; ln -s $TESTLOG) + (cd $ERRORDIR; cp -a $TESTLOG .) fi rm -f $RUNNING/$SHORT.running diff -r 0cdb76723c88 -r 2c787345c083 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Fri Apr 16 15:49:13 2010 +0200 +++ b/Admin/isatest/isatest-makedist Fri Apr 16 15:49:46 2010 +0200 @@ -55,6 +55,7 @@ echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1 rm -rf $HOME/isabelle-* +ssh atbroy102 "rm -rf isabelle-cygwin-poly" echo "### building distribution" >> $DISTLOG 2>&1 mkdir -p $DISTPREFIX diff -r 0cdb76723c88 -r 2c787345c083 NEWS --- a/NEWS Fri Apr 16 15:49:13 2010 +0200 +++ b/NEWS Fri Apr 16 15:49:46 2010 +0200 @@ -74,6 +74,8 @@ *** Pure *** +* Code generator: simple concept for abstract datatypes obeying invariants. + * Local theory specifications may depend on extra type variables that are not present in the result type -- arguments TYPE('a) :: 'a itself are added internally. For example: @@ -106,6 +108,10 @@ *** HOL *** +* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT' +provides abstract red-black tree type which is backed by RBT_Impl +as implementation. INCOMPATIBILTY. + * Command 'typedef' now works within a local theory context -- without introducing dependencies on parameters or assumptions, which is not possible in Isabelle/Pure/HOL. Note that the logical environment may @@ -292,6 +298,10 @@ * Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw syntax constant (cf. 'syntax' command). +* Antiquotation @{make_string} inlines a function to print arbitrary +values similar to the ML toplevel. The result is compiler dependent +and may fall back on "?" in certain situations. + * Renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation. INCOMPATIBILITY. diff -r 0cdb76723c88 -r 2c787345c083 doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Fri Apr 16 15:49:13 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Fri Apr 16 15:49:46 2010 +0200 @@ -334,7 +334,7 @@ this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}. - \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text + \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text "\"}-equivalence of two terms. This is the basic equality relation on type @{ML_type term}; raw datatype equality should only be used for operations related to parsing or printing! diff -r 0cdb76723c88 -r 2c787345c083 doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Fri Apr 16 15:49:13 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/ML.thy Fri Apr 16 15:49:46 2010 +0200 @@ -209,7 +209,7 @@ options} for type @{ML_type "bool"}/@{ML_type "int"}/@{ML_type "string"} (see structure @{ML_struct Config} and @{ML Attrib.config_bool} etc.), and lists of theorems (see functor - @{ML_functor NamedThmsFun}). + @{ML_functor Named_Thms}). \item Keep components with local state information \emph{re-entrant}. Instead of poking initial values into (private) @@ -623,7 +623,7 @@ whenever such pure finite mappings are neccessary. The key type of tables must be given explicitly by instantiating - the @{ML_functor TableFun} functor which takes the key type + the @{ML_functor Table} functor which takes the key type together with its @{ML_type order}; for convience, we restrict here to the @{ML_struct Symtab} instance with @{ML_type string} as key type. diff -r 0cdb76723c88 -r 2c787345c083 doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Fri Apr 16 15:49:13 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Fri Apr 16 15:49:46 2010 +0200 @@ -222,7 +222,7 @@ \secref{sec:context-data}) there are drop-in replacements that emulate primitive references for common cases of \emph{configuration options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor - \verb|NamedThmsFun|). + \verb|Named_Thms|). \item Keep components with local state information \emph{re-entrant}. Instead of poking initial values into (private) @@ -763,7 +763,7 @@ whenever such pure finite mappings are neccessary. The key type of tables must be given explicitly by instantiating - the \verb|TableFun| functor which takes the key type + the \verb|Table| functor which takes the key type together with its \verb|order|; for convience, we restrict here to the \verb|Symtab| instance with \verb|string| as key type. diff -r 0cdb76723c88 -r 2c787345c083 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Apr 16 15:49:13 2010 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Apr 16 15:49:46 2010 +0200 @@ -178,7 +178,7 @@ \end{matharray} \begin{rail} - 'record' typespec '=' (type '+')? (constdecl +) + 'record' typespecsorts '=' (type '+')? (constdecl +) ; \end{rail} diff -r 0cdb76723c88 -r 2c787345c083 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Apr 16 15:49:13 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Apr 16 15:49:46 2010 +0200 @@ -202,7 +202,7 @@ \end{matharray} \begin{rail} - 'record' typespec '=' (type '+')? (constdecl +) + 'record' typespecsorts '=' (type '+')? (constdecl +) ; \end{rail} diff -r 0cdb76723c88 -r 2c787345c083 doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Fri Apr 16 15:49:13 2010 +0200 +++ b/doc-src/antiquote_setup.ML Fri Apr 16 15:49:46 2010 +0200 @@ -54,7 +54,7 @@ fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;"; -fun ml_functor _ = ""; (*no check!*) +fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt; fun index_ml name kind ml = ThyOutput.antiquotation name (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) diff -r 0cdb76723c88 -r 2c787345c083 src/HOL/Imperative_HOL/ex/SatChecker.thy --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Fri Apr 16 15:49:13 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Fri Apr 16 15:49:46 2010 +0200 @@ -5,7 +5,7 @@ header {* An efficient checker for proofs from a SAT solver *} theory SatChecker -imports RBT Sorted_List "~~/src/HOL/Imperative_HOL/Imperative_HOL" +imports RBT_Impl Sorted_List "~~/src/HOL/Imperative_HOL/Imperative_HOL" begin section{* General settings and functions for our representation of clauses *} @@ -635,24 +635,24 @@ section {* Functional version with RedBlackTrees *} -fun tres_thm :: "(ClauseId, Clause) rbt \ Lit \ ClauseId \ Clause \ Clause Heap" +fun tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \ Lit \ ClauseId \ Clause \ Clause Heap" where "tres_thm t (l, j) cli = - (case (RBT.lookup t j) of + (case (RBT_Impl.lookup t j) of None \ raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'') | Some clj \ res_thm' l cli clj)" -fun tdoProofStep :: " ProofStep \ ((ClauseId, Clause) rbt * Clause list) \ ((ClauseId, Clause) rbt * Clause list) Heap" +fun tdoProofStep :: " ProofStep \ ((ClauseId, Clause) RBT_Impl.rbt * Clause list) \ ((ClauseId, Clause) RBT_Impl.rbt * Clause list) Heap" where "tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) = - (case (RBT.lookup t i) of + (case (RBT_Impl.lookup t i) of None \ raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'') | Some cli \ (do result \ foldM (tres_thm t) rs cli; - return ((RBT.insert saveTo result t), rcl) + return ((RBT_Impl.insert saveTo result t), rcl) done))" -| "tdoProofStep (Delete cid) (t, rcl) = return ((RBT.delete cid t), rcl)" -| "tdoProofStep (Root cid clause) (t, rcl) = return (RBT.insert cid (sort clause) t, (remdups(sort clause)) # rcl)" +| "tdoProofStep (Delete cid) (t, rcl) = return ((RBT_Impl.delete cid t), rcl)" +| "tdoProofStep (Root cid clause) (t, rcl) = return (RBT_Impl.insert cid (sort clause) t, (remdups(sort clause)) # rcl)" | "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" | "tdoProofStep (ProofDone b) (t, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" @@ -660,8 +660,8 @@ where "tchecker n p i = (do - rcs \ foldM (tdoProofStep) p (RBT.Empty, []); - (if (RBT.lookup (fst rcs) i) = Some [] then return (snd rcs) + rcs \ foldM (tdoProofStep) p (RBT_Impl.Empty, []); + (if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs) else raise(''No empty clause'')) done)" diff -r 0cdb76723c88 -r 2c787345c083 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Apr 16 15:49:13 2010 +0200 +++ b/src/HOL/IsaMakefile Fri Apr 16 15:49:46 2010 +0200 @@ -1,3 +1,4 @@ + # # IsaMakefile for HOL # @@ -406,14 +407,15 @@ Library/Library/ROOT.ML Library/Library/document/root.tex \ Library/Library/document/root.bib \ Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \ - Library/Product_ord.thy Library/Char_nat.thy Library/Table.thy \ + Library/Product_ord.thy Library/Char_nat.thy \ Library/Sublist_Order.thy Library/List_lexord.thy \ Library/AssocList.thy Library/Formal_Power_Series.thy \ Library/Binomial.thy Library/Eval_Witness.thy Library/Code_Char.thy \ Library/Code_Char_chr.thy Library/Code_Integer.thy \ Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy \ Library/Boolean_Algebra.thy Library/Countable.thy \ - Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy \ + Library/Diagonalize.thy Library/RBT.thy Library/RBT_Impl.thy \ + Library/Univ_Poly.thy \ Library/Poly_Deriv.thy Library/Polynomial.thy Library/Preorder.thy \ Library/Product_plus.thy Library/Product_Vector.thy \ Library/Enum.thy Library/Float.thy Library/Quotient_List.thy \ diff -r 0cdb76723c88 -r 2c787345c083 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Fri Apr 16 15:49:13 2010 +0200 +++ b/src/HOL/Library/Library.thy Fri Apr 16 15:49:46 2010 +0200 @@ -57,7 +57,6 @@ SML_Quickcheck State_Monad Sum_Of_Squares - Table Transitive_Closure_Table Univ_Poly While_Combinator diff -r 0cdb76723c88 -r 2c787345c083 src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Fri Apr 16 15:49:13 2010 +0200 +++ b/src/HOL/Library/Quotient_List.thy Fri Apr 16 15:49:46 2010 +0200 @@ -217,6 +217,52 @@ apply (simp_all) done +lemma list_rel_rsp: + assumes r: "\x y. R x y \ (\a b. R a b \ S x a = T y b)" + and l1: "list_rel R x y" + and l2: "list_rel R a b" + shows "list_rel S x a = list_rel T y b" + proof - + have a: "length y = length x" by (rule list_rel_len[OF l1, symmetric]) + have c: "length a = length b" by (rule list_rel_len[OF l2]) + show ?thesis proof (cases "length x = length a") + case True + have b: "length x = length a" by fact + show ?thesis using a b c r l1 l2 proof (induct rule: list_induct4) + case Nil + show ?case using assms by simp + next + case (Cons h t) + then show ?case by auto + qed + next + case False + have d: "length x \ length a" by fact + then have e: "\list_rel S x a" using list_rel_len by auto + have "length y \ length b" using d a c by simp + then have "\list_rel T y b" using list_rel_len by auto + then show ?thesis using e by simp + qed + qed + +lemma[quot_respect]: + "((R ===> R ===> op =) ===> list_rel R ===> list_rel R ===> op =) list_rel list_rel" + by (simp add: list_rel_rsp) + +lemma[quot_preserve]: + assumes a: "Quotient R abs1 rep1" + shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_rel = list_rel" + apply (simp add: expand_fun_eq) + apply clarify + apply (induct_tac xa xb rule: list_induct2') + apply (simp_all add: Quotient_abs_rep[OF a]) + done + +lemma[quot_preserve]: + assumes a: "Quotient R abs1 rep1" + shows "(list_rel ((rep1 ---> rep1 ---> id) R) l m) = (l = m)" + by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a]) + lemma list_rel_eq[id_simps]: shows "(list_rel (op =)) = (op =)" unfolding expand_fun_eq diff -r 0cdb76723c88 -r 2c787345c083 src/HOL/Library/RBT.thy --- a/src/HOL/Library/RBT.thy Fri Apr 16 15:49:13 2010 +0200 +++ b/src/HOL/Library/RBT.thy Fri Apr 16 15:49:46 2010 +0200 @@ -1,1100 +1,253 @@ -(* Title: RBT.thy - Author: Markus Reiter, TU Muenchen - Author: Alexander Krauss, TU Muenchen -*) +(* Author: Florian Haftmann, TU Muenchen *) -header {* Red-Black Trees *} +header {* Abstract type of Red-Black Trees *} (*<*) theory RBT -imports Main +imports Main RBT_Impl Mapping begin -subsection {* Datatype of RB trees *} - -datatype color = R | B -datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt" - -lemma rbt_cases: - obtains (Empty) "t = Empty" - | (Red) l k v r where "t = Branch R l k v r" - | (Black) l k v r where "t = Branch B l k v r" -proof (cases t) - case Empty with that show thesis by blast -next - case (Branch c) with that show thesis by (cases c) blast+ -qed - -subsection {* Tree properties *} - -subsubsection {* Content of a tree *} - -primrec entries :: "('a, 'b) rbt \ ('a \ 'b) list" -where - "entries Empty = []" -| "entries (Branch _ l k v r) = entries l @ (k,v) # entries r" - -abbreviation (input) entry_in_tree :: "'a \ 'b \ ('a, 'b) rbt \ bool" -where - "entry_in_tree k v t \ (k, v) \ set (entries t)" - -definition keys :: "('a, 'b) rbt \ 'a list" where - "keys t = map fst (entries t)" - -lemma keys_simps [simp, code]: - "keys Empty = []" - "keys (Branch c l k v r) = keys l @ k # keys r" - by (simp_all add: keys_def) - -lemma entry_in_tree_keys: - assumes "(k, v) \ set (entries t)" - shows "k \ set (keys t)" -proof - - from assms have "fst (k, v) \ fst ` set (entries t)" by (rule imageI) - then show ?thesis by (simp add: keys_def) -qed - -lemma keys_entries: - "k \ set (keys t) \ (\v. (k, v) \ set (entries t))" - by (auto intro: entry_in_tree_keys) (auto simp add: keys_def) - - -subsubsection {* Search tree properties *} - -definition tree_less :: "'a\order \ ('a, 'b) rbt \ bool" -where - tree_less_prop: "tree_less k t \ (\x\set (keys t). x < k)" - -abbreviation tree_less_symbol (infix "|\" 50) -where "t |\ x \ tree_less x t" - -definition tree_greater :: "'a\order \ ('a, 'b) rbt \ bool" (infix "\|" 50) -where - tree_greater_prop: "tree_greater k t = (\x\set (keys t). k < x)" - -lemma tree_less_simps [simp]: - "tree_less k Empty = True" - "tree_less k (Branch c lt kt v rt) \ kt < k \ tree_less k lt \ tree_less k rt" - by (auto simp add: tree_less_prop) - -lemma tree_greater_simps [simp]: - "tree_greater k Empty = True" - "tree_greater k (Branch c lt kt v rt) \ k < kt \ tree_greater k lt \ tree_greater k rt" - by (auto simp add: tree_greater_prop) - -lemmas tree_ord_props = tree_less_prop tree_greater_prop - -lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys -lemmas tree_less_nit = tree_less_prop entry_in_tree_keys - -lemma tree_less_eq_trans: "l |\ u \ u \ v \ l |\ v" - and tree_less_trans: "t |\ x \ x < y \ t |\ y" - and tree_greater_eq_trans: "u \ v \ v \| r \ u \| r" - and tree_greater_trans: "x < y \ y \| t \ x \| t" - by (auto simp: tree_ord_props) - -primrec sorted :: "('a::linorder, 'b) rbt \ bool" -where - "sorted Empty = True" -| "sorted (Branch c l k v r) = (l |\ k \ k \| r \ sorted l \ sorted r)" - -lemma sorted_entries: - "sorted t \ List.sorted (List.map fst (entries t))" -by (induct t) - (force simp: sorted_append sorted_Cons tree_ord_props - dest!: entry_in_tree_keys)+ - -lemma distinct_entries: - "sorted t \ distinct (List.map fst (entries t))" -by (induct t) - (force simp: sorted_append sorted_Cons tree_ord_props - dest!: entry_in_tree_keys)+ - - -subsubsection {* Tree lookup *} - -primrec lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" -where - "lookup Empty k = None" -| "lookup (Branch _ l x y r) k = (if k < x then lookup l k else if x < k then lookup r k else Some y)" - -lemma lookup_keys: "sorted t \ dom (lookup t) = set (keys t)" - by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop) +subsection {* Type definition *} -lemma dom_lookup_Branch: - "sorted (Branch c t1 k v t2) \ - dom (lookup (Branch c t1 k v t2)) - = Set.insert k (dom (lookup t1) \ dom (lookup t2))" +typedef (open) ('a, 'b) rbt = "{t :: ('a\linorder, 'b) RBT_Impl.rbt. is_rbt t}" + morphisms impl_of RBT proof - - assume "sorted (Branch c t1 k v t2)" - moreover from this have "sorted t1" "sorted t2" by simp_all - ultimately show ?thesis by (simp add: lookup_keys) -qed - -lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))" -proof (induct t) - case Empty then show ?case by simp -next - case (Branch color t1 a b t2) - let ?A = "Set.insert a (dom (lookup t1) \ dom (lookup t2))" - have "dom (lookup (Branch color t1 a b t2)) \ ?A" by (auto split: split_if_asm) - moreover from Branch have "finite (insert a (dom (lookup t1) \ dom (lookup t2)))" by simp - ultimately show ?case by (rule finite_subset) -qed - -lemma lookup_tree_less[simp]: "t |\ k \ lookup t k = None" -by (induct t) auto - -lemma lookup_tree_greater[simp]: "k \| t \ lookup t k = None" -by (induct t) auto - -lemma lookup_Empty: "lookup Empty = empty" -by (rule ext) simp - -lemma map_of_entries: - "sorted t \ map_of (entries t) = lookup t" -proof (induct t) - case Empty thus ?case by (simp add: lookup_Empty) -next - case (Branch c t1 k v t2) - have "lookup (Branch c t1 k v t2) = lookup t2 ++ [k\v] ++ lookup t1" - proof (rule ext) - fix x - from Branch have SORTED: "sorted (Branch c t1 k v t2)" by simp - let ?thesis = "lookup (Branch c t1 k v t2) x = (lookup t2 ++ [k \ v] ++ lookup t1) x" - - have DOM_T1: "!!k'. k'\dom (lookup t1) \ k>k'" - proof - - fix k' - from SORTED have "t1 |\ k" by simp - with tree_less_prop have "\k'\set (keys t1). k>k'" by auto - moreover assume "k'\dom (lookup t1)" - ultimately show "k>k'" using lookup_keys SORTED by auto - qed - - have DOM_T2: "!!k'. k'\dom (lookup t2) \ k| t2" by simp - with tree_greater_prop have "\k'\set (keys t2). kdom (lookup t2)" - ultimately show "kdom [k\v]" by simp - moreover have "x\dom (lookup t2)" proof - assume "x\dom (lookup t2)" - with DOM_T2 have "k v] x" by simp - moreover have "x\dom (lookup t1)" proof - assume "x\dom (lookup t1)" - with DOM_T1 have "k>x" by blast - thus False by simp - qed - ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) - } moreover { - assume C: "x>k" - hence "lookup (Branch c t1 k v t2) x = lookup t2 x" by (simp add: less_not_sym[of k x]) - moreover from C have "x\dom [k\v]" by simp - moreover have "x\dom (lookup t1)" proof - assume "x\dom (lookup t1)" - with DOM_T1 have "k>x" by simp - with C show False by simp - qed - ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) - } ultimately show ?thesis using less_linear by blast - qed - also from Branch have "lookup t2 ++ [k \ v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp - finally show ?case by simp -qed - -lemma lookup_in_tree: "sorted t \ lookup t k = Some v \ (k, v) \ set (entries t)" - by (simp add: map_of_entries [symmetric] distinct_entries) - -lemma set_entries_inject: - assumes sorted: "sorted t1" "sorted t2" - shows "set (entries t1) = set (entries t2) \ entries t1 = entries t2" -proof - - from sorted have "distinct (map fst (entries t1))" - "distinct (map fst (entries t2))" - by (auto intro: distinct_entries) - with sorted show ?thesis - by (auto intro: map_sorted_distinct_set_unique sorted_entries simp add: distinct_map) -qed - -lemma entries_eqI: - assumes sorted: "sorted t1" "sorted t2" - assumes lookup: "lookup t1 = lookup t2" - shows "entries t1 = entries t2" -proof - - from sorted lookup have "map_of (entries t1) = map_of (entries t2)" - by (simp add: map_of_entries) - with sorted have "set (entries t1) = set (entries t2)" - by (simp add: map_of_inject_set distinct_entries) - with sorted show ?thesis by (simp add: set_entries_inject) + have "RBT_Impl.Empty \ ?rbt" by simp + then show ?thesis .. qed -lemma entries_lookup: - assumes "sorted t1" "sorted t2" - shows "entries t1 = entries t2 \ lookup t1 = lookup t2" - using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric]) - -lemma lookup_from_in_tree: - assumes "sorted t1" "sorted t2" - and "\v. (k\'a\linorder, v) \ set (entries t1) \ (k, v) \ set (entries t2)" - shows "lookup t1 k = lookup t2 k" -proof - - from assms have "k \ dom (lookup t1) \ k \ dom (lookup t2)" - by (simp add: keys_entries lookup_keys) - with assms show ?thesis by (auto simp add: lookup_in_tree [symmetric]) -qed - - -subsubsection {* Red-black properties *} - -primrec color_of :: "('a, 'b) rbt \ color" -where - "color_of Empty = B" -| "color_of (Branch c _ _ _ _) = c" +lemma is_rbt_impl_of [simp, intro]: + "is_rbt (impl_of t)" + using impl_of [of t] by simp -primrec bheight :: "('a,'b) rbt \ nat" -where - "bheight Empty = 0" -| "bheight (Branch c lt k v rt) = (if c = B then Suc (bheight lt) else bheight lt)" - -primrec inv1 :: "('a, 'b) rbt \ bool" -where - "inv1 Empty = True" -| "inv1 (Branch c lt k v rt) \ inv1 lt \ inv1 rt \ (c = B \ color_of lt = B \ color_of rt = B)" +lemma rbt_eq: + "t1 = t2 \ impl_of t1 = impl_of t2" + by (simp add: impl_of_inject) -primrec inv1l :: "('a, 'b) rbt \ bool" -- {* Weaker version *} -where - "inv1l Empty = True" -| "inv1l (Branch c l k v r) = (inv1 l \ inv1 r)" -lemma [simp]: "inv1 t \ inv1l t" by (cases t) simp+ - -primrec inv2 :: "('a, 'b) rbt \ bool" -where - "inv2 Empty = True" -| "inv2 (Branch c lt k v rt) = (inv2 lt \ inv2 rt \ bheight lt = bheight rt)" - -definition is_rbt :: "('a\linorder, 'b) rbt \ bool" where - "is_rbt t \ inv1 t \ inv2 t \ color_of t = B \ sorted t" - -lemma is_rbt_sorted [simp]: - "is_rbt t \ sorted t" by (simp add: is_rbt_def) - -theorem Empty_is_rbt [simp]: - "is_rbt Empty" by (simp add: is_rbt_def) +lemma [code abstype]: + "RBT (impl_of t) = t" + by (simp add: impl_of_inverse) -subsection {* Insertion *} - -fun (* slow, due to massive case splitting *) - balance :: "('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" -where - "balance (Branch R a w x b) s t (Branch R c y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" | - "balance (Branch R (Branch R a w x b) s t c) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" | - "balance (Branch R a w x (Branch R b s t c)) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" | - "balance a w x (Branch R b s t (Branch R c y z d)) = Branch R (Branch B a w x b) s t (Branch B c y z d)" | - "balance a w x (Branch R (Branch R b s t c) y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" | - "balance a s t b = Branch B a s t b" - -lemma balance_inv1: "\inv1l l; inv1l r\ \ inv1 (balance l k v r)" - by (induct l k v r rule: balance.induct) auto - -lemma balance_bheight: "bheight l = bheight r \ bheight (balance l k v r) = Suc (bheight l)" - by (induct l k v r rule: balance.induct) auto - -lemma balance_inv2: - assumes "inv2 l" "inv2 r" "bheight l = bheight r" - shows "inv2 (balance l k v r)" - using assms - by (induct l k v r rule: balance.induct) auto - -lemma balance_tree_greater[simp]: "(v \| balance a k x b) = (v \| a \ v \| b \ v < k)" - by (induct a k x b rule: balance.induct) auto - -lemma balance_tree_less[simp]: "(balance a k x b |\ v) = (a |\ v \ b |\ v \ k < v)" - by (induct a k x b rule: balance.induct) auto +subsection {* Primitive operations *} -lemma balance_sorted: - fixes k :: "'a::linorder" - assumes "sorted l" "sorted r" "l |\ k" "k \| r" - shows "sorted (balance l k v r)" -using assms proof (induct l k v r rule: balance.induct) - case ("2_2" a x w b y t c z s va vb vd vc) - hence "y < z \ z \| Branch B va vb vd vc" - by (auto simp add: tree_ord_props) - hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) - with "2_2" show ?case by simp -next - case ("3_2" va vb vd vc x w b y s c z) - from "3_2" have "x < y \ tree_less x (Branch B va vb vd vc)" - by simp - hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans) - with "3_2" show ?case by simp -next - case ("3_3" x w b y s c z t va vb vd vc) - from "3_3" have "y < z \ tree_greater z (Branch B va vb vd vc)" by simp - hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) - with "3_3" show ?case by simp -next - case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc) - hence "x < y \ tree_less x (Branch B vd ve vg vf)" by simp - hence 1: "tree_less y (Branch B vd ve vg vf)" by (blast dest: tree_less_trans) - from "3_4" have "y < z \ tree_greater z (Branch B va vb vii vc)" by simp - hence "tree_greater y (Branch B va vb vii vc)" by (blast dest: tree_greater_trans) - with 1 "3_4" show ?case by simp -next - case ("4_2" va vb vd vc x w b y s c z t dd) - hence "x < y \ tree_less x (Branch B va vb vd vc)" by simp - hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans) - with "4_2" show ?case by simp -next - case ("5_2" x w b y s c z t va vb vd vc) - hence "y < z \ tree_greater z (Branch B va vb vd vc)" by simp - hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) - with "5_2" show ?case by simp -next - case ("5_3" va vb vd vc x w b y s c z t) - hence "x < y \ tree_less x (Branch B va vb vd vc)" by simp - hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans) - with "5_3" show ?case by simp -next - case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf) - hence "x < y \ tree_less x (Branch B va vb vg vc)" by simp - hence 1: "tree_less y (Branch B va vb vg vc)" by (blast dest: tree_less_trans) - from "5_4" have "y < z \ tree_greater z (Branch B vd ve vii vf)" by simp - hence "tree_greater y (Branch B vd ve vii vf)" by (blast dest: tree_greater_trans) - with 1 "5_4" show ?case by simp -qed simp+ - -lemma entries_balance [simp]: - "entries (balance l k v r) = entries l @ (k, v) # entries r" - by (induct l k v r rule: balance.induct) auto - -lemma keys_balance [simp]: - "keys (balance l k v r) = keys l @ k # keys r" - by (simp add: keys_def) +definition lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" where + [code]: "lookup t = RBT_Impl.lookup (impl_of t)" -lemma balance_in_tree: - "entry_in_tree k x (balance l v y r) \ entry_in_tree k x l \ k = v \ x = y \ entry_in_tree k x r" - by (auto simp add: keys_def) - -lemma lookup_balance[simp]: -fixes k :: "'a::linorder" -assumes "sorted l" "sorted r" "l |\ k" "k \| r" -shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x" -by (rule lookup_from_in_tree) (auto simp:assms balance_in_tree balance_sorted) - -primrec paint :: "color \ ('a,'b) rbt \ ('a,'b) rbt" -where - "paint c Empty = Empty" -| "paint c (Branch _ l k v r) = Branch c l k v r" - -lemma paint_inv1l[simp]: "inv1l t \ inv1l (paint c t)" by (cases t) auto -lemma paint_inv1[simp]: "inv1l t \ inv1 (paint B t)" by (cases t) auto -lemma paint_inv2[simp]: "inv2 t \ inv2 (paint c t)" by (cases t) auto -lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto -lemma paint_sorted[simp]: "sorted t \ sorted (paint c t)" by (cases t) auto -lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto -lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto) -lemma paint_tree_greater[simp]: "(v \| paint c t) = (v \| t)" by (cases t) auto -lemma paint_tree_less[simp]: "(paint c t |\ v) = (t |\ v)" by (cases t) auto - -fun - ins :: "('a\linorder \ 'b \ 'b \ 'b) \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" -where - "ins f k v Empty = Branch R Empty k v Empty" | - "ins f k v (Branch B l x y r) = (if k < x then balance (ins f k v l) x y r - else if k > x then balance l x y (ins f k v r) - else Branch B l x (f k y v) r)" | - "ins f k v (Branch R l x y r) = (if k < x then Branch R (ins f k v l) x y r - else if k > x then Branch R l x y (ins f k v r) - else Branch R l x (f k y v) r)" - -lemma ins_inv1_inv2: - assumes "inv1 t" "inv2 t" - shows "inv2 (ins f k x t)" "bheight (ins f k x t) = bheight t" - "color_of t = B \ inv1 (ins f k x t)" "inv1l (ins f k x t)" - using assms - by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight) +definition empty :: "('a\linorder, 'b) rbt" where + "empty = RBT RBT_Impl.Empty" -lemma ins_tree_greater[simp]: "(v \| ins f k x t) = (v \| t \ k > v)" - by (induct f k x t rule: ins.induct) auto -lemma ins_tree_less[simp]: "(ins f k x t |\ v) = (t |\ v \ k < v)" - by (induct f k x t rule: ins.induct) auto -lemma ins_sorted[simp]: "sorted t \ sorted (ins f k x t)" - by (induct f k x t rule: ins.induct) (auto simp: balance_sorted) - -lemma keys_ins: "set (keys (ins f k v t)) = { k } \ set (keys t)" - by (induct f k v t rule: ins.induct) auto - -lemma lookup_ins: - fixes k :: "'a::linorder" - assumes "sorted t" - shows "lookup (ins f k v t) x = ((lookup t)(k |-> case lookup t k of None \ v - | Some w \ f k w v)) x" -using assms by (induct f k v t rule: ins.induct) auto - -definition - insert_with_key :: "('a\linorder \ 'b \ 'b \ 'b) \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" -where - "insert_with_key f k v t = paint B (ins f k v t)" - -lemma insertwk_sorted: "sorted t \ sorted (insert_with_key f k x t)" - by (auto simp: insert_with_key_def) - -theorem insertwk_is_rbt: - assumes inv: "is_rbt t" - shows "is_rbt (insert_with_key f k x t)" -using assms -unfolding insert_with_key_def is_rbt_def -by (auto simp: ins_inv1_inv2) - -lemma lookup_insertwk: - assumes "sorted t" - shows "lookup (insert_with_key f k v t) x = ((lookup t)(k |-> case lookup t k of None \ v - | Some w \ f k w v)) x" -unfolding insert_with_key_def using assms -by (simp add:lookup_ins) - -definition - insertw_def: "insert_with f = insert_with_key (\_. f)" - -lemma insertw_sorted: "sorted t \ sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def) -theorem insertw_is_rbt: "is_rbt t \ is_rbt (insert_with f k v t)" by (simp add: insertwk_is_rbt insertw_def) - -lemma lookup_insertw: - assumes "is_rbt t" - shows "lookup (insert_with f k v t) = (lookup t)(k \ (if k:dom (lookup t) then f (the (lookup t k)) v else v))" -using assms -unfolding insertw_def -by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def) +lemma impl_of_empty [code abstract]: + "impl_of empty = RBT_Impl.Empty" + by (simp add: empty_def RBT_inverse) definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where - "insert = insert_with_key (\_ _ nv. nv)" + "insert k v t = RBT (RBT_Impl.insert k v (impl_of t))" + +lemma impl_of_insert [code abstract]: + "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)" + by (simp add: insert_def RBT_inverse) + +definition delete :: "'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "delete k t = RBT (RBT_Impl.delete k (impl_of t))" -lemma insert_sorted: "sorted t \ sorted (insert k v t)" by (simp add: insertwk_sorted insert_def) -theorem insert_is_rbt [simp]: "is_rbt t \ is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def) +lemma impl_of_delete [code abstract]: + "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)" + by (simp add: delete_def RBT_inverse) + +definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" where + [code]: "entries t = RBT_Impl.entries (impl_of t)" + +definition keys :: "('a\linorder, 'b) rbt \ 'a list" where + [code]: "keys t = RBT_Impl.keys (impl_of t)" + +definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" where + "bulkload xs = RBT (RBT_Impl.bulkload xs)" -lemma lookup_insert: - assumes "is_rbt t" - shows "lookup (insert k v t) = (lookup t)(k\v)" -unfolding insert_def -using assms -by (rule_tac ext) (simp add: lookup_insertwk split:option.split) +lemma impl_of_bulkload [code abstract]: + "impl_of (bulkload xs) = RBT_Impl.bulkload xs" + by (simp add: bulkload_def RBT_inverse) + +definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" where + "map_entry k f t = RBT (RBT_Impl.map_entry k f (impl_of t))" + +lemma impl_of_map_entry [code abstract]: + "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)" + by (simp add: map_entry_def RBT_inverse) + +definition map :: "('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" where + "map f t = RBT (RBT_Impl.map f (impl_of t))" + +lemma impl_of_map [code abstract]: + "impl_of (map f t) = RBT_Impl.map f (impl_of t)" + by (simp add: map_def RBT_inverse) + +definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" where + [code]: "fold f t = RBT_Impl.fold f (impl_of t)" + + +subsection {* Derived operations *} + +definition is_empty :: "('a\linorder, 'b) rbt \ bool" where + [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \ True | _ \ False)" -subsection {* Deletion *} - -lemma bheight_paintR'[simp]: "color_of t = B \ bheight (paint R t) = bheight t - 1" -by (cases t rule: rbt_cases) auto - -fun - balance_left :: "('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" -where - "balance_left (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" | - "balance_left bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" | - "balance_left bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))" | - "balance_left t k x s = Empty" +subsection {* Abstract lookup properties *} -lemma balance_left_inv2_with_inv1: - assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt" - shows "bheight (balance_left lt k v rt) = bheight lt + 1" - and "inv2 (balance_left lt k v rt)" -using assms -by (induct lt k v rt rule: balance_left.induct) (auto simp: balance_inv2 balance_bheight) - -lemma balance_left_inv2_app: - assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B" - shows "inv2 (balance_left lt k v rt)" - "bheight (balance_left lt k v rt) = bheight rt" -using assms -by (induct lt k v rt rule: balance_left.induct) (auto simp add: balance_inv2 balance_bheight)+ - -lemma balance_left_inv1: "\inv1l a; inv1 b; color_of b = B\ \ inv1 (balance_left a k x b)" - by (induct a k x b rule: balance_left.induct) (simp add: balance_inv1)+ - -lemma balance_left_inv1l: "\ inv1l lt; inv1 rt \ \ inv1l (balance_left lt k x rt)" -by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1) +lemma lookup_RBT: + "is_rbt t \ lookup (RBT t) = RBT_Impl.lookup t" + by (simp add: lookup_def RBT_inverse) -lemma balance_left_sorted: "\ sorted l; sorted r; tree_less k l; tree_greater k r \ \ sorted (balance_left l k v r)" -apply (induct l k v r rule: balance_left.induct) -apply (auto simp: balance_sorted) -apply (unfold tree_greater_prop tree_less_prop) -by force+ - -lemma balance_left_tree_greater: - fixes k :: "'a::order" - assumes "k \| a" "k \| b" "k < x" - shows "k \| balance_left a x t b" -using assms -by (induct a x t b rule: balance_left.induct) auto - -lemma balance_left_tree_less: - fixes k :: "'a::order" - assumes "a |\ k" "b |\ k" "x < k" - shows "balance_left a x t b |\ k" -using assms -by (induct a x t b rule: balance_left.induct) auto +lemma lookup_impl_of: + "RBT_Impl.lookup (impl_of t) = lookup t" + by (simp add: lookup_def) -lemma balance_left_in_tree: - assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r" - shows "entry_in_tree k v (balance_left l a b r) = (entry_in_tree k v l \ k = a \ v = b \ entry_in_tree k v r)" -using assms -by (induct l k v r rule: balance_left.induct) (auto simp: balance_in_tree) - -fun - balance_right :: "('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" -where - "balance_right a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" | - "balance_right (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" | - "balance_right (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)" | - "balance_right t k x s = Empty" - -lemma balance_right_inv2_with_inv1: - assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt" - shows "inv2 (balance_right lt k v rt) \ bheight (balance_right lt k v rt) = bheight lt" -using assms -by (induct lt k v rt rule: balance_right.induct) (auto simp: balance_inv2 balance_bheight) +lemma entries_impl_of: + "RBT_Impl.entries (impl_of t) = entries t" + by (simp add: entries_def) -lemma balance_right_inv1: "\inv1 a; inv1l b; color_of a = B\ \ inv1 (balance_right a k x b)" -by (induct a k x b rule: balance_right.induct) (simp add: balance_inv1)+ - -lemma balance_right_inv1l: "\ inv1 lt; inv1l rt \ \inv1l (balance_right lt k x rt)" -by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1) - -lemma balance_right_sorted: "\ sorted l; sorted r; tree_less k l; tree_greater k r \ \ sorted (balance_right l k v r)" -apply (induct l k v r rule: balance_right.induct) -apply (auto simp:balance_sorted) -apply (unfold tree_less_prop tree_greater_prop) -by force+ +lemma keys_impl_of: + "RBT_Impl.keys (impl_of t) = keys t" + by (simp add: keys_def) -lemma balance_right_tree_greater: - fixes k :: "'a::order" - assumes "k \| a" "k \| b" "k < x" - shows "k \| balance_right a x t b" -using assms by (induct a x t b rule: balance_right.induct) auto - -lemma balance_right_tree_less: - fixes k :: "'a::order" - assumes "a |\ k" "b |\ k" "x < k" - shows "balance_right a x t b |\ k" -using assms by (induct a x t b rule: balance_right.induct) auto - -lemma balance_right_in_tree: - assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r" - shows "entry_in_tree x y (balance_right l k v r) = (entry_in_tree x y l \ x = k \ y = v \ entry_in_tree x y r)" -using assms by (induct l k v r rule: balance_right.induct) (auto simp: balance_in_tree) +lemma lookup_empty [simp]: + "lookup empty = Map.empty" + by (simp add: empty_def lookup_RBT expand_fun_eq) -fun - combine :: "('a,'b) rbt \ ('a,'b) rbt \ ('a,'b) rbt" -where - "combine Empty x = x" -| "combine x Empty = x" -| "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of - Branch R b2 t z c2 \ (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) | - bc \ Branch R a k x (Branch R bc s y d))" -| "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of - Branch R b2 t z c2 \ Branch R (Branch B a k x b2) t z (Branch B c2 s y d) | - bc \ balance_left a k x (Branch B bc s y d))" -| "combine a (Branch R b k x c) = Branch R (combine a b) k x c" -| "combine (Branch R a k x b) c = Branch R a k x (combine b c)" - -lemma combine_inv2: - assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt" - shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)" -using assms -by (induct lt rt rule: combine.induct) - (auto simp: balance_left_inv2_app split: rbt.splits color.splits) +lemma lookup_insert [simp]: + "lookup (insert k v t) = (lookup t)(k \ v)" + by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of) -lemma combine_inv1: - assumes "inv1 lt" "inv1 rt" - shows "color_of lt = B \ color_of rt = B \ inv1 (combine lt rt)" - "inv1l (combine lt rt)" -using assms -by (induct lt rt rule: combine.induct) - (auto simp: balance_left_inv1 split: rbt.splits color.splits) +lemma lookup_delete [simp]: + "lookup (delete k t) = (lookup t)(k := None)" + by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq) -lemma combine_tree_greater[simp]: - fixes k :: "'a::linorder" - assumes "k \| l" "k \| r" - shows "k \| combine l r" -using assms -by (induct l r rule: combine.induct) - (auto simp: balance_left_tree_greater split:rbt.splits color.splits) - -lemma combine_tree_less[simp]: - fixes k :: "'a::linorder" - assumes "l |\ k" "r |\ k" - shows "combine l r |\ k" -using assms -by (induct l r rule: combine.induct) - (auto simp: balance_left_tree_less split:rbt.splits color.splits) +lemma map_of_entries [simp]: + "map_of (entries t) = lookup t" + by (simp add: entries_def map_of_entries lookup_impl_of) -lemma combine_sorted: - fixes k :: "'a::linorder" - assumes "sorted l" "sorted r" "l |\ k" "k \| r" - shows "sorted (combine l r)" -using assms proof (induct l r rule: combine.induct) - case (3 a x v b c y w d) - hence ineqs: "a |\ x" "x \| b" "b |\ k" "k \| c" "c |\ y" "y \| d" - by auto - with 3 - show ?case - by (cases "combine b c" rule: rbt_cases) - (auto, (metis combine_tree_greater combine_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+) -next - case (4 a x v b c y w d) - hence "x < k \ tree_greater k c" by simp - hence "tree_greater x c" by (blast dest: tree_greater_trans) - with 4 have 2: "tree_greater x (combine b c)" by (simp add: combine_tree_greater) - from 4 have "k < y \ tree_less k b" by simp - hence "tree_less y b" by (blast dest: tree_less_trans) - with 4 have 3: "tree_less y (combine b c)" by (simp add: combine_tree_less) - show ?case - proof (cases "combine b c" rule: rbt_cases) - case Empty - from 4 have "x < y \ tree_greater y d" by auto - hence "tree_greater x d" by (blast dest: tree_greater_trans) - with 4 Empty have "sorted a" and "sorted (Branch B Empty y w d)" and "tree_less x a" and "tree_greater x (Branch B Empty y w d)" by auto - with Empty show ?thesis by (simp add: balance_left_sorted) - next - case (Red lta va ka rta) - with 2 4 have "x < va \ tree_less x a" by simp - hence 5: "tree_less va a" by (blast dest: tree_less_trans) - from Red 3 4 have "va < y \ tree_greater y d" by simp - hence "tree_greater va d" by (blast dest: tree_greater_trans) - with Red 2 3 4 5 show ?thesis by simp - next - case (Black lta va ka rta) - from 4 have "x < y \ tree_greater y d" by auto - hence "tree_greater x d" by (blast dest: tree_greater_trans) - with Black 2 3 4 have "sorted a" and "sorted (Branch B (combine b c) y w d)" and "tree_less x a" and "tree_greater x (Branch B (combine b c) y w d)" by auto - with Black show ?thesis by (simp add: balance_left_sorted) - qed -next - case (5 va vb vd vc b x w c) - hence "k < x \ tree_less k (Branch B va vb vd vc)" by simp - hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans) - with 5 show ?case by (simp add: combine_tree_less) -next - case (6 a x v b va vb vd vc) - hence "x < k \ tree_greater k (Branch B va vb vd vc)" by simp - hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans) - with 6 show ?case by (simp add: combine_tree_greater) -qed simp+ +lemma entries_lookup: + "entries t1 = entries t2 \ lookup t1 = lookup t2" + by (simp add: entries_def lookup_def entries_lookup) + +lemma lookup_bulkload [simp]: + "lookup (bulkload xs) = map_of xs" + by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload) -lemma combine_in_tree: - assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r" - shows "entry_in_tree k v (combine l r) = (entry_in_tree k v l \ entry_in_tree k v r)" -using assms -proof (induct l r rule: combine.induct) - case (4 _ _ _ b c) - hence a: "bheight (combine b c) = bheight b" by (simp add: combine_inv2) - from 4 have b: "inv1l (combine b c)" by (simp add: combine_inv1) +lemma lookup_map_entry [simp]: + "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))" + by (simp add: map_entry_def lookup_RBT lookup_map_entry lookup_impl_of) - show ?case - proof (cases "combine b c" rule: rbt_cases) - case Empty - with 4 a show ?thesis by (auto simp: balance_left_in_tree) - next - case (Red lta ka va rta) - with 4 show ?thesis by auto - next - case (Black lta ka va rta) - with a b 4 show ?thesis by (auto simp: balance_left_in_tree) - qed -qed (auto split: rbt.splits color.splits) +lemma lookup_map [simp]: + "lookup (map f t) k = Option.map (f k) (lookup t k)" + by (simp add: map_def lookup_RBT lookup_map lookup_impl_of) -fun - del_from_left :: "('a\linorder) \ ('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" and - del_from_right :: "('a\linorder) \ ('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" and - del :: "('a\linorder) \ ('a,'b) rbt \ ('a,'b) rbt" -where - "del x Empty = Empty" | - "del x (Branch c a y s b) = (if x < y then del_from_left x a y s b else (if x > y then del_from_right x a y s b else combine a b))" | - "del_from_left x (Branch B lt z v rt) y s b = balance_left (del x (Branch B lt z v rt)) y s b" | - "del_from_left x a y s b = Branch R (del x a) y s b" | - "del_from_right x a y s (Branch B lt z v rt) = balance_right a y s (del x (Branch B lt z v rt))" | - "del_from_right x a y s b = Branch R a y s (del x b)" +lemma fold_fold: + "fold f t = (\s. foldl (\s (k, v). f k v s) s (entries t))" + by (simp add: fold_def expand_fun_eq RBT_Impl.fold_def entries_impl_of) -lemma - assumes "inv2 lt" "inv1 lt" - shows - "\inv2 rt; bheight lt = bheight rt; inv1 rt\ \ - inv2 (del_from_left x lt k v rt) \ bheight (del_from_left x lt k v rt) = bheight lt \ (color_of lt = B \ color_of rt = B \ inv1 (del_from_left x lt k v rt) \ (color_of lt \ B \ color_of rt \