--- 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
--- 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
--- 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.
--- 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
"\<alpha>"}-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!
--- 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.
--- 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.
--- 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}
--- 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}
--- 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) ""))
--- 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 \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap"
+fun tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap"
where
"tres_thm t (l, j) cli =
- (case (RBT.lookup t j) of
+ (case (RBT_Impl.lookup t j) of
None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'')
| Some clj \<Rightarrow> res_thm' l cli clj)"
-fun tdoProofStep :: " ProofStep \<Rightarrow> ((ClauseId, Clause) rbt * Clause list) \<Rightarrow> ((ClauseId, Clause) rbt * Clause list) Heap"
+fun tdoProofStep :: " ProofStep \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) \<Rightarrow> ((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 \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
| Some cli \<Rightarrow> (do
result \<leftarrow> 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 \<leftarrow> foldM (tdoProofStep) p (RBT.Empty, []);
- (if (RBT.lookup (fst rcs) i) = Some [] then return (snd rcs)
+ rcs \<leftarrow> foldM (tdoProofStep) p (RBT_Impl.Empty, []);
+ (if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs)
else raise(''No empty clause''))
done)"
--- 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 \
--- 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
--- 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: "\<forall>x y. R x y \<longrightarrow> (\<forall>a b. R a b \<longrightarrow> 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 \<noteq> length a" by fact
+ then have e: "\<not>list_rel S x a" using list_rel_len by auto
+ have "length y \<noteq> length b" using d a c by simp
+ then have "\<not>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
--- 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 \<Rightarrow> ('a \<times> 'b) list"
-where
- "entries Empty = []"
-| "entries (Branch _ l k v r) = entries l @ (k,v) # entries r"
-
-abbreviation (input) entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
-where
- "entry_in_tree k v t \<equiv> (k, v) \<in> set (entries t)"
-
-definition keys :: "('a, 'b) rbt \<Rightarrow> '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) \<in> set (entries t)"
- shows "k \<in> set (keys t)"
-proof -
- from assms have "fst (k, v) \<in> fst ` set (entries t)" by (rule imageI)
- then show ?thesis by (simp add: keys_def)
-qed
-
-lemma keys_entries:
- "k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))"
- by (auto intro: entry_in_tree_keys) (auto simp add: keys_def)
-
-
-subsubsection {* Search tree properties *}
-
-definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
-where
- tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)"
-
-abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
-where "t |\<guillemotleft> x \<equiv> tree_less x t"
-
-definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50)
-where
- tree_greater_prop: "tree_greater k t = (\<forall>x\<in>set (keys t). k < x)"
-
-lemma tree_less_simps [simp]:
- "tree_less k Empty = True"
- "tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> 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) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> 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 |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v"
- and tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
- and tree_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r"
- and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
- by (auto simp: tree_ord_props)
-
-primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
-where
- "sorted Empty = True"
-| "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
-
-lemma sorted_entries:
- "sorted t \<Longrightarrow> 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 \<Longrightarrow> 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\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> '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 \<Longrightarrow> 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) \<Longrightarrow>
- dom (lookup (Branch c t1 k v t2))
- = Set.insert k (dom (lookup t1) \<union> dom (lookup t2))"
+typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>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) \<union> dom (lookup t2))"
- have "dom (lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
- moreover from Branch have "finite (insert a (dom (lookup t1) \<union> dom (lookup t2)))" by simp
- ultimately show ?case by (rule finite_subset)
-qed
-
-lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None"
-by (induct t) auto
-
-lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
-by (induct t) auto
-
-lemma lookup_Empty: "lookup Empty = empty"
-by (rule ext) simp
-
-lemma map_of_entries:
- "sorted t \<Longrightarrow> 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\<mapsto>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 \<mapsto> v] ++ lookup t1) x"
-
- have DOM_T1: "!!k'. k'\<in>dom (lookup t1) \<Longrightarrow> k>k'"
- proof -
- fix k'
- from SORTED have "t1 |\<guillemotleft> k" by simp
- with tree_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto
- moreover assume "k'\<in>dom (lookup t1)"
- ultimately show "k>k'" using lookup_keys SORTED by auto
- qed
-
- have DOM_T2: "!!k'. k'\<in>dom (lookup t2) \<Longrightarrow> k<k'"
- proof -
- fix k'
- from SORTED have "k \<guillemotleft>| t2" by simp
- with tree_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto
- moreover assume "k'\<in>dom (lookup t2)"
- ultimately show "k<k'" using lookup_keys SORTED by auto
- qed
-
- {
- assume C: "x<k"
- hence "lookup (Branch c t1 k v t2) x = lookup t1 x" by simp
- moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
- moreover have "x\<notin>dom (lookup t2)" proof
- assume "x\<in>dom (lookup t2)"
- with DOM_T2 have "k<x" by blast
- with C show False by simp
- qed
- ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
- } moreover {
- assume [simp]: "x=k"
- hence "lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
- moreover have "x\<notin>dom (lookup t1)" proof
- assume "x\<in>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\<notin>dom [k\<mapsto>v]" by simp
- moreover have "x\<notin>dom (lookup t1)" proof
- assume "x\<in>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 \<mapsto> 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 \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> 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) \<longleftrightarrow> 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 \<in> ?rbt" by simp
+ then show ?thesis ..
qed
-lemma entries_lookup:
- assumes "sorted t1" "sorted t2"
- shows "entries t1 = entries t2 \<longleftrightarrow> 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 "\<And>v. (k\<Colon>'a\<Colon>linorder, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)"
- shows "lookup t1 k = lookup t2 k"
-proof -
- from assms have "k \<in> dom (lookup t1) \<longleftrightarrow> k \<in> 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 \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> bool"
-where
- "inv1 Empty = True"
-| "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)"
+lemma rbt_eq:
+ "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
+ by (simp add: impl_of_inject)
-primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- {* Weaker version *}
-where
- "inv1l Empty = True"
-| "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"
-lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+
-
-primrec inv2 :: "('a, 'b) rbt \<Rightarrow> bool"
-where
- "inv2 Empty = True"
-| "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)"
-
-definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
- "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t"
-
-lemma is_rbt_sorted [simp]:
- "is_rbt t \<Longrightarrow> 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 \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)"
- by (induct l k v r rule: balance.induct) auto
-
-lemma balance_bheight: "bheight l = bheight r \<Longrightarrow> 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 \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)"
- by (induct a k x b rule: balance.induct) auto
-
-lemma balance_tree_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> 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 |\<guillemotleft> k" "k \<guillemotleft>| 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 \<and> z \<guillemotleft>| 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> '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) \<longleftrightarrow> entry_in_tree k x l \<or> k = v \<and> x = y \<or> 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 |\<guillemotleft> k" "k \<guillemotleft>| 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 \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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 \<Longrightarrow> inv1l (paint c t)" by (cases t) auto
-lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto
-lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> 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 \<Longrightarrow> 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 \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
-lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
-
-fun
- ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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 \<Longrightarrow> 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\<Colon>linorder, 'b) rbt" where
+ "empty = RBT RBT_Impl.Empty"
-lemma ins_tree_greater[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
- by (induct f k x t rule: ins.induct) auto
-lemma ins_tree_less[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
- by (induct f k x t rule: ins.induct) auto
-lemma ins_sorted[simp]: "sorted t \<Longrightarrow> 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 } \<union> 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 \<Rightarrow> v
- | Some w \<Rightarrow> f k w v)) x"
-using assms by (induct f k v t rule: ins.induct) auto
-
-definition
- insert_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
-where
- "insert_with_key f k v t = paint B (ins f k v t)"
-
-lemma insertwk_sorted: "sorted t \<Longrightarrow> 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 \<Rightarrow> v
- | Some w \<Rightarrow> 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 (\<lambda>_. f)"
-
-lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def)
-theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> 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 \<mapsto> (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\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
- "insert = insert_with_key (\<lambda>_ _ 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\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
+ "delete k t = RBT (RBT_Impl.delete k (impl_of t))"
-lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
-theorem insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> 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\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" where
+ [code]: "entries t = RBT_Impl.entries (impl_of t)"
+
+definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" where
+ [code]: "keys t = RBT_Impl.keys (impl_of t)"
+
+definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('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\<mapsto>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 \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('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 \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('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 \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
+ [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
+
+
+subsection {* Derived operations *}
+
+definition is_empty :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
+ [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
-subsection {* Deletion *}
-
-lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
-by (cases t rule: rbt_cases) auto
-
-fun
- balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> 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: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> lookup (RBT t) = RBT_Impl.lookup t"
+ by (simp add: lookup_def RBT_inverse)
-lemma balance_left_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> 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 \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
- shows "k \<guillemotleft>| 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 |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
- shows "balance_left a x t b |\<guillemotleft> 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 \<or> k = a \<and> v = b \<or> 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 \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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) \<and> 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: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> 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: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>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: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> 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 \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
- shows "k \<guillemotleft>| 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 |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
- shows "balance_right a x t b |\<guillemotleft> 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 \<or> x = k \<and> y = v \<or> 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 \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
- bc \<Rightarrow> 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 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
- bc \<Rightarrow> 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 \<mapsto> 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 \<Longrightarrow> color_of rt = B \<Longrightarrow> 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 \<guillemotleft>| l" "k \<guillemotleft>| r"
- shows "k \<guillemotleft>| 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 |\<guillemotleft> k" "r |\<guillemotleft> k"
- shows "combine l r |\<guillemotleft> 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 |\<guillemotleft> k" "k \<guillemotleft>| 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 |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<longleftrightarrow> 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 \<or> 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\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
- del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
- del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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 = (\<lambda>s. foldl (\<lambda>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
- "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
- inv2 (del_from_left x lt k v rt) \<and> bheight (del_from_left x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_left x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_left x lt k v rt))"
- and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
- inv2 (del_from_right x lt k v rt) \<and> bheight (del_from_right x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_right x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_right x lt k v rt))"
- and del_inv1_inv2: "inv2 (del x lt) \<and> (color_of lt = R \<and> bheight (del x lt) = bheight lt \<and> inv1 (del x lt)
- \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
-using assms
-proof (induct x lt k v rt and x lt k v rt and x lt rule: del_from_left_del_from_right_del.induct)
-case (2 y c _ y')
- have "y = y' \<or> y < y' \<or> y > y'" by auto
- thus ?case proof (elim disjE)
- assume "y = y'"
- with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
- next
- assume "y < y'"
- with 2 show ?thesis by (cases c) auto
- next
- assume "y' < y"
- with 2 show ?thesis by (cases c) auto
- qed
-next
- case (3 y lt z v rta y' ss bb)
- thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+
-next
- case (5 y a y' ss lt z v rta)
- thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+
-next
- case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
-qed auto
+lemma is_empty_empty [simp]:
+ "is_empty t \<longleftrightarrow> t = empty"
+ by (simp add: rbt_eq is_empty_def impl_of_empty split: rbt.split)
-lemma
- del_from_left_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_left x lt k y rt)"
- and del_from_right_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_right x lt k y rt)"
- and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
-by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
- (auto simp: balance_left_tree_less balance_right_tree_less)
-
-lemma del_from_left_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_left x lt k y rt)"
- and del_from_right_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_right x lt k y rt)"
- and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
-by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
- (auto simp: balance_left_tree_greater balance_right_tree_greater)
-
-lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_left x lt k y rt)"
- and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_right x lt k y rt)"
- and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
-proof (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
- case (3 x lta zz v rta yy ss bb)
- from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
- hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
- with 3 show ?case by (simp add: balance_left_sorted)
-next
- case ("4_2" x vaa vbb vdd vc yy ss bb)
- hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
- hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less)
- with "4_2" show ?case by simp
-next
- case (5 x aa yy ss lta zz v rta)
- hence "tree_greater yy (Branch B lta zz v rta)" by simp
- hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
- with 5 show ?case by (simp add: balance_right_sorted)
-next
- case ("6_2" x aa yy ss vaa vbb vdd vc)
- hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
- hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
- with "6_2" show ?case by simp
-qed (auto simp: combine_sorted)
+lemma RBT_lookup_empty [simp]: (*FIXME*)
+ "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
+ by (cases t) (auto simp add: expand_fun_eq)
-lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_left x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
- and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_right x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
- and del_in_tree: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
-proof (induct x lt kt y rt and x lt kt y rt and x t rule: del_from_left_del_from_right_del.induct)
- case (2 xx c aa yy ss bb)
- have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
- from this 2 show ?case proof (elim disjE)
- assume "xx = yy"
- with 2 show ?thesis proof (cases "xx = k")
- case True
- from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
- hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
- with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree)
- qed (simp add: combine_in_tree)
- qed simp+
-next
- case (3 xx lta zz vv rta yy ss bb)
- def mt[simp]: mt == "Branch B lta zz vv rta"
- from 3 have "inv2 mt \<and> inv1 mt" by simp
- hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
- with 3 have 4: "entry_in_tree k v (del_from_left xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balance_left_in_tree)
- thus ?case proof (cases "xx = k")
- case True
- from 3 True have "tree_greater yy bb \<and> yy > k" by simp
- hence "tree_greater k bb" by (blast dest: tree_greater_trans)
- with 3 4 True show ?thesis by (auto simp: tree_greater_nit)
- qed auto
-next
- case ("4_1" xx yy ss bb)
- show ?case proof (cases "xx = k")
- case True
- with "4_1" have "tree_greater yy bb \<and> k < yy" by simp
- hence "tree_greater k bb" by (blast dest: tree_greater_trans)
- with "4_1" `xx = k`
- have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit)
- thus ?thesis by auto
- qed simp+
-next
- case ("4_2" xx vaa vbb vdd vc yy ss bb)
- thus ?case proof (cases "xx = k")
- case True
- with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
- hence "tree_greater k bb" by (blast dest: tree_greater_trans)
- with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
- qed auto
-next
- case (5 xx aa yy ss lta zz vv rta)
- def mt[simp]: mt == "Branch B lta zz vv rta"
- from 5 have "inv2 mt \<and> inv1 mt" by simp
- hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
- with 5 have 3: "entry_in_tree k v (del_from_right xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balance_right_in_tree)
- thus ?case proof (cases "xx = k")
- case True
- from 5 True have "tree_less yy aa \<and> yy < k" by simp
- hence "tree_less k aa" by (blast dest: tree_less_trans)
- with 3 5 True show ?thesis by (auto simp: tree_less_nit)
- qed auto
-next
- case ("6_1" xx aa yy ss)
- show ?case proof (cases "xx = k")
- case True
- with "6_1" have "tree_less yy aa \<and> k > yy" by simp
- hence "tree_less k aa" by (blast dest: tree_less_trans)
- with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit)
- qed simp
-next
- case ("6_2" xx aa yy ss vaa vbb vdd vc)
- thus ?case proof (cases "xx = k")
- case True
- with "6_2" have "k > yy \<and> tree_less yy aa" by simp
- hence "tree_less k aa" by (blast dest: tree_less_trans)
- with True "6_2" show ?thesis by (auto simp: tree_less_nit)
- qed auto
-qed simp
+lemma lookup_empty_empty [simp]:
+ "lookup t = Map.empty \<longleftrightarrow> t = empty"
+ by (cases t) (simp add: empty_def lookup_def RBT_inject RBT_inverse)
+
+lemma sorted_keys [iff]:
+ "sorted (keys t)"
+ by (simp add: keys_def RBT_Impl.keys_def sorted_entries)
+
+lemma distinct_keys [iff]:
+ "distinct (keys t)"
+ by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
-definition delete where
- delete_def: "delete k t = paint B (del k t)"
+subsection {* Implementation of mappings *}
-theorem delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
-proof -
- from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto
- hence "inv2 (del k t) \<and> (color_of t = R \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color_of t = B \<and> bheight (del k t) = bheight t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2)
- hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto
- with assms show ?thesis
- unfolding is_rbt_def delete_def
- by (auto intro: paint_sorted del_sorted)
-qed
-
-lemma delete_in_tree:
- assumes "is_rbt t"
- shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
- using assms unfolding is_rbt_def delete_def
- by (auto simp: del_in_tree)
+definition Mapping :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) mapping" where
+ "Mapping t = Mapping.Mapping (lookup t)"
-lemma lookup_delete:
- assumes is_rbt: "is_rbt t"
- shows "lookup (delete k t) = (lookup t)|`(-{k})"
-proof
- fix x
- show "lookup (delete k t) x = (lookup t |` (-{k})) x"
- proof (cases "x = k")
- assume "x = k"
- with is_rbt show ?thesis
- by (cases "lookup (delete k t) k") (auto simp: lookup_in_tree delete_in_tree)
- next
- assume "x \<noteq> k"
- thus ?thesis
- by auto (metis is_rbt delete_is_rbt delete_in_tree is_rbt_sorted lookup_from_in_tree)
- qed
-qed
+code_datatype Mapping
-
-subsection {* Union *}
+lemma lookup_Mapping [simp, code]:
+ "Mapping.lookup (Mapping t) = lookup t"
+ by (simp add: Mapping_def)
-primrec
- union_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
-where
- "union_with_key f t Empty = t"
-| "union_with_key f t (Branch c lt k v rt) = union_with_key f (union_with_key f (insert_with_key f k v t) lt) rt"
-
-lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (union_with_key f lt rt)"
- by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
-theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (union_with_key f lt rt)"
- by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
+lemma empty_Mapping [code]:
+ "Mapping.empty = Mapping empty"
+ by (rule mapping_eqI) simp
-definition
- union_with where
- "union_with f = union_with_key (\<lambda>_. f)"
-
-theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union_with f lt rt)" unfolding union_with_def by simp
-
-definition union where
- "union = union_with_key (%_ _ rv. rv)"
-
-theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
+lemma is_empty_Mapping [code]:
+ "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
+ by (simp add: rbt_eq Mapping.is_empty_empty Mapping_def)
-lemma union_Branch[simp]:
- "union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt"
- unfolding union_def insert_def
- by simp
+lemma insert_Mapping [code]:
+ "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
+ by (rule mapping_eqI) simp
-lemma lookup_union:
- assumes "is_rbt s" "sorted t"
- shows "lookup (union s t) = lookup s ++ lookup t"
-using assms
-proof (induct t arbitrary: s)
- case Empty thus ?case by (auto simp: union_def)
-next
- case (Branch c l k v r s)
- then have "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
-
- have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
- lookup s ++
- (\<lambda>a. if a < k then lookup l a
- else if k < a then lookup r a else Some v)" (is "?m1 = ?m2")
- proof (rule ext)
- fix a
+lemma delete_Mapping [code]:
+ "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
+ by (rule mapping_eqI) simp
- have "k < a \<or> k = a \<or> k > a" by auto
- thus "?m1 a = ?m2 a"
- proof (elim disjE)
- assume "k < a"
- with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tree_less_trans)
- with `k < a` show ?thesis
- by (auto simp: map_add_def split: option.splits)
- next
- assume "k = a"
- with `l |\<guillemotleft> k` `k \<guillemotleft>| r`
- show ?thesis by (auto simp: map_add_def)
- next
- assume "a < k"
- from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tree_greater_trans)
- with `a < k` show ?thesis
- by (auto simp: map_add_def split: option.splits)
- qed
- qed
+lemma keys_Mapping [code]:
+ "Mapping.keys (Mapping t) = set (keys t)"
+ by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
- from Branch have is_rbt: "is_rbt (RBT.union (RBT.insert k v s) l)"
- by (auto intro: union_is_rbt insert_is_rbt)
- with Branch have IHs:
- "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
- "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
- by auto
-
- with meq show ?case
- by (auto simp: lookup_insert[OF Branch(3)])
+lemma ordered_keys_Mapping [code]:
+ "Mapping.ordered_keys (Mapping t) = keys t"
+ by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping)
-qed
-
-
-subsection {* Modifying existing entries *}
-
-primrec
- map_entry :: "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-where
- "map_entry k f Empty = Empty"
-| "map_entry k f (Branch c lt x v rt) =
- (if k < x then Branch c (map_entry k f lt) x v rt
- else if k > x then (Branch c lt x v (map_entry k f rt))
- else Branch c lt x (f v) rt)"
+lemma Mapping_size_card_keys: (*FIXME*)
+ "Mapping.size m = card (Mapping.keys m)"
+ by (simp add: Mapping.size_def Mapping.keys_def)
-lemma map_entry_color_of: "color_of (map_entry k f t) = color_of t" by (induct t) simp+
-lemma map_entry_inv1: "inv1 (map_entry k f t) = inv1 t" by (induct t) (simp add: map_entry_color_of)+
-lemma map_entry_inv2: "inv2 (map_entry k f t) = inv2 t" "bheight (map_entry k f t) = bheight t" by (induct t) simp+
-lemma map_entry_tree_greater: "tree_greater a (map_entry k f t) = tree_greater a t" by (induct t) simp+
-lemma map_entry_tree_less: "tree_less a (map_entry k f t) = tree_less a t" by (induct t) simp+
-lemma map_entry_sorted: "sorted (map_entry k f t) = sorted t"
- by (induct t) (simp_all add: map_entry_tree_less map_entry_tree_greater)
-
-theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t"
-unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
-
-theorem lookup_map_entry:
- "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
- by (induct t) (auto split: option.splits simp add: expand_fun_eq)
-
+lemma size_Mapping [code]:
+ "Mapping.size (Mapping t) = length (keys t)"
+ by (simp add: Mapping_size_card_keys keys_Mapping distinct_card)
-subsection {* Mapping all entries *}
-
-primrec
- map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'c) rbt"
-where
- "map f Empty = Empty"
-| "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)"
+lemma tabulate_Mapping [code]:
+ "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
+ by (rule mapping_eqI) (simp add: map_of_map_restrict)
-lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)"
- by (induct t) auto
-lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def)
-lemma map_tree_greater: "tree_greater k (map f t) = tree_greater k t" by (induct t) simp+
-lemma map_tree_less: "tree_less k (map f t) = tree_less k t" by (induct t) simp+
-lemma map_sorted: "sorted (map f t) = sorted t" by (induct t) (simp add: map_tree_less map_tree_greater)+
-lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+
-lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+
-lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+
-theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t"
-unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
-
-theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)"
- by (induct t) auto
-
-
-subsection {* Folding over entries *}
-
-definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
- "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)"
+lemma bulkload_Mapping [code]:
+ "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
+ by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
-lemma fold_simps [simp, code]:
- "fold f Empty = id"
- "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
- by (simp_all add: fold_def expand_fun_eq)
-
-
-subsection {* Bulkloading a tree *}
-
-definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where
- "bulkload xs = foldr (\<lambda>(k, v). RBT.insert k v) xs RBT.Empty"
-
-lemma bulkload_is_rbt [simp, intro]:
- "is_rbt (bulkload xs)"
- unfolding bulkload_def by (induct xs) auto
+lemma [code, code del]: "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
-lemma lookup_bulkload:
- "RBT.lookup (bulkload xs) = map_of xs"
-proof -
- obtain ys where "ys = rev xs" by simp
- have "\<And>t. is_rbt t \<Longrightarrow>
- RBT.lookup (foldl (\<lambda>t (k, v). RBT.insert k v t) t ys) = RBT.lookup t ++ map_of (rev ys)"
- by (induct ys) (simp_all add: bulkload_def split_def RBT.lookup_insert)
- from this Empty_is_rbt have
- "RBT.lookup (foldl (\<lambda>t (k, v). RBT.insert k v t) RBT.Empty (rev xs)) = RBT.lookup RBT.Empty ++ map_of xs"
- by (simp add: `ys = rev xs`)
- then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
-qed
+lemma eq_Mapping [code]:
+ "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
+ by (simp add: eq Mapping_def entries_lookup)
-hide (open) const Empty insert delete entries bulkload lookup map_entry map fold union sorted
+hide (open) const impl_of lookup empty insert delete
+ entries keys bulkload map_entry map fold
(*>*)
text {*
- This theory defines purely functional red-black trees which can be
- used as an efficient representation of finite maps.
+ This theory defines abstract red-black trees as an efficient
+ representation of finite maps, backed by the implementation
+ in @{theory RBT_Impl}.
*}
-
subsection {* Data type and invariant *}
text {*
- The type @{typ "('k, 'v) rbt"} denotes red-black trees with keys of
- type @{typ "'k"} and values of type @{typ "'v"}. To function
- properly, the key type musorted belong to the @{text "linorder"} class.
+ The type @{typ "('k, 'v) RBT_Impl.rbt"} denotes red-black trees with
+ keys of type @{typ "'k"} and values of type @{typ "'v"}. To function
+ properly, the key type musorted belong to the @{text "linorder"}
+ class.
A value @{term t} of this type is a valid red-black tree if it
- satisfies the invariant @{text "is_rbt t"}.
- This theory provides lemmas to prove that the invariant is
- satisfied throughout the computation.
+ satisfies the invariant @{text "is_rbt t"}. The abstract type @{typ
+ "('k, 'v) rbt"} always obeys this invariant, and for this reason you
+ should only use this in our application. Going back to @{typ "('k,
+ 'v) RBT_Impl.rbt"} may be necessary in proofs if not yet proven
+ properties about the operations must be established.
The interpretation function @{const "RBT.lookup"} returns the partial
map represented by a red-black tree:
@@ -1106,15 +259,12 @@
$O(\log n)$.
*}
-
subsection {* Operations *}
-print_antiquotations
-
text {*
Currently, the following operations are supported:
- @{term_type [display] "RBT.Empty"}
+ @{term_type [display] "RBT.empty"}
Returns the empty tree. $O(1)$
@{term_type [display] "RBT.insert"}
@@ -1137,9 +287,6 @@
@{term_type [display] "RBT.fold"}
Folds over all entries in a tree. $O(n)$
-
- @{term_type [display] "RBT.union"}
- Forms the union of two trees, preferring entries from the first one.
*}
@@ -1173,8 +320,8 @@
text {*
\noindent
- \underline{@{text "lookup_Empty"}}
- @{thm [display] lookup_Empty}
+ \underline{@{text "lookup_empty"}}
+ @{thm [display] lookup_empty}
\vspace{1ex}
\noindent
@@ -1196,11 +343,6 @@
\underline{@{text "lookup_map"}}
@{thm [display] lookup_map}
\vspace{1ex}
-
- \noindent
- \underline{@{text "lookup_union"}}
- @{thm [display] lookup_union}
- \vspace{1ex}
*}
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/RBT_Impl.thy Fri Apr 16 15:49:46 2010 +0200
@@ -0,0 +1,1084 @@
+(* Title: RBT_Impl.thy
+ Author: Markus Reiter, TU Muenchen
+ Author: Alexander Krauss, TU Muenchen
+*)
+
+header {* Implementation of Red-Black Trees *}
+
+theory RBT_Impl
+imports Main
+begin
+
+text {*
+ For applications, you should use theory @{text RBT} which defines
+ an abstract type of red-black tree obeying the invariant.
+*}
+
+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 \<Rightarrow> ('a \<times> 'b) list"
+where
+ "entries Empty = []"
+| "entries (Branch _ l k v r) = entries l @ (k,v) # entries r"
+
+abbreviation (input) entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
+where
+ "entry_in_tree k v t \<equiv> (k, v) \<in> set (entries t)"
+
+definition keys :: "('a, 'b) rbt \<Rightarrow> '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) \<in> set (entries t)"
+ shows "k \<in> set (keys t)"
+proof -
+ from assms have "fst (k, v) \<in> fst ` set (entries t)" by (rule imageI)
+ then show ?thesis by (simp add: keys_def)
+qed
+
+lemma keys_entries:
+ "k \<in> set (keys t) \<longleftrightarrow> (\<exists>v. (k, v) \<in> set (entries t))"
+ by (auto intro: entry_in_tree_keys) (auto simp add: keys_def)
+
+
+subsubsection {* Search tree properties *}
+
+definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
+where
+ tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)"
+
+abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
+where "t |\<guillemotleft> x \<equiv> tree_less x t"
+
+definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50)
+where
+ tree_greater_prop: "tree_greater k t = (\<forall>x\<in>set (keys t). k < x)"
+
+lemma tree_less_simps [simp]:
+ "tree_less k Empty = True"
+ "tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> 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) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> 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 |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v"
+ and tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
+ and tree_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r"
+ and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
+ by (auto simp: tree_ord_props)
+
+primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
+where
+ "sorted Empty = True"
+| "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
+
+lemma sorted_entries:
+ "sorted t \<Longrightarrow> 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 \<Longrightarrow> 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\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> '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 \<Longrightarrow> dom (lookup t) = set (keys t)"
+ by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
+
+lemma dom_lookup_Branch:
+ "sorted (Branch c t1 k v t2) \<Longrightarrow>
+ dom (lookup (Branch c t1 k v t2))
+ = Set.insert k (dom (lookup t1) \<union> dom (lookup t2))"
+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) \<union> dom (lookup t2))"
+ have "dom (lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
+ moreover from Branch have "finite (insert a (dom (lookup t1) \<union> dom (lookup t2)))" by simp
+ ultimately show ?case by (rule finite_subset)
+qed
+
+lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None"
+by (induct t) auto
+
+lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
+by (induct t) auto
+
+lemma lookup_Empty: "lookup Empty = empty"
+by (rule ext) simp
+
+lemma map_of_entries:
+ "sorted t \<Longrightarrow> 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\<mapsto>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 \<mapsto> v] ++ lookup t1) x"
+
+ have DOM_T1: "!!k'. k'\<in>dom (lookup t1) \<Longrightarrow> k>k'"
+ proof -
+ fix k'
+ from SORTED have "t1 |\<guillemotleft> k" by simp
+ with tree_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto
+ moreover assume "k'\<in>dom (lookup t1)"
+ ultimately show "k>k'" using lookup_keys SORTED by auto
+ qed
+
+ have DOM_T2: "!!k'. k'\<in>dom (lookup t2) \<Longrightarrow> k<k'"
+ proof -
+ fix k'
+ from SORTED have "k \<guillemotleft>| t2" by simp
+ with tree_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto
+ moreover assume "k'\<in>dom (lookup t2)"
+ ultimately show "k<k'" using lookup_keys SORTED by auto
+ qed
+
+ {
+ assume C: "x<k"
+ hence "lookup (Branch c t1 k v t2) x = lookup t1 x" by simp
+ moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
+ moreover have "x\<notin>dom (lookup t2)" proof
+ assume "x\<in>dom (lookup t2)"
+ with DOM_T2 have "k<x" by blast
+ with C show False by simp
+ qed
+ ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
+ } moreover {
+ assume [simp]: "x=k"
+ hence "lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
+ moreover have "x\<notin>dom (lookup t1)" proof
+ assume "x\<in>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\<notin>dom [k\<mapsto>v]" by simp
+ moreover have "x\<notin>dom (lookup t1)" proof
+ assume "x\<in>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 \<mapsto> 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 \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> 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) \<longleftrightarrow> 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)
+qed
+
+lemma entries_lookup:
+ assumes "sorted t1" "sorted t2"
+ shows "entries t1 = entries t2 \<longleftrightarrow> 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 "\<And>v. (k\<Colon>'a\<Colon>linorder, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)"
+ shows "lookup t1 k = lookup t2 k"
+proof -
+ from assms have "k \<in> dom (lookup t1) \<longleftrightarrow> k \<in> 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 \<Rightarrow> color"
+where
+ "color_of Empty = B"
+| "color_of (Branch c _ _ _ _) = c"
+
+primrec bheight :: "('a,'b) rbt \<Rightarrow> 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 \<Rightarrow> bool"
+where
+ "inv1 Empty = True"
+| "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)"
+
+primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- {* Weaker version *}
+where
+ "inv1l Empty = True"
+| "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"
+lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+
+
+primrec inv2 :: "('a, 'b) rbt \<Rightarrow> bool"
+where
+ "inv2 Empty = True"
+| "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)"
+
+definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
+ "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t"
+
+lemma is_rbt_sorted [simp]:
+ "is_rbt t \<Longrightarrow> sorted t" by (simp add: is_rbt_def)
+
+theorem Empty_is_rbt [simp]:
+ "is_rbt Empty" by (simp add: is_rbt_def)
+
+
+subsection {* Insertion *}
+
+fun (* slow, due to massive case splitting *)
+ balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)"
+ by (induct l k v r rule: balance.induct) auto
+
+lemma balance_bheight: "bheight l = bheight r \<Longrightarrow> 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 \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)"
+ by (induct a k x b rule: balance.induct) auto
+
+lemma balance_tree_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
+ by (induct a k x b rule: balance.induct) auto
+
+lemma balance_sorted:
+ fixes k :: "'a::linorder"
+ assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| 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 \<and> z \<guillemotleft>| 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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)
+
+lemma balance_in_tree:
+ "entry_in_tree k x (balance l v y r) \<longleftrightarrow> entry_in_tree k x l \<or> k = v \<and> x = y \<or> 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 |\<guillemotleft> k" "k \<guillemotleft>| 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 \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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 \<Longrightarrow> inv1l (paint c t)" by (cases t) auto
+lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto
+lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> 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 \<Longrightarrow> 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 \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
+lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
+
+fun
+ ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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 \<Longrightarrow> 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)
+
+lemma ins_tree_greater[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
+ by (induct f k x t rule: ins.induct) auto
+lemma ins_tree_less[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
+ by (induct f k x t rule: ins.induct) auto
+lemma ins_sorted[simp]: "sorted t \<Longrightarrow> 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 } \<union> 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 \<Rightarrow> v
+ | Some w \<Rightarrow> f k w v)) x"
+using assms by (induct f k v t rule: ins.induct) auto
+
+definition
+ insert_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
+where
+ "insert_with_key f k v t = paint B (ins f k v t)"
+
+lemma insertwk_sorted: "sorted t \<Longrightarrow> 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 \<Rightarrow> v
+ | Some w \<Rightarrow> 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 (\<lambda>_. f)"
+
+lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def)
+theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> 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 \<mapsto> (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)
+
+definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
+ "insert = insert_with_key (\<lambda>_ _ nv. nv)"
+
+lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
+theorem insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
+
+lemma lookup_insert:
+ assumes "is_rbt t"
+ shows "lookup (insert k v t) = (lookup t)(k\<mapsto>v)"
+unfolding insert_def
+using assms
+by (rule_tac ext) (simp add: lookup_insertwk split:option.split)
+
+
+subsection {* Deletion *}
+
+lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
+by (cases t rule: rbt_cases) auto
+
+fun
+ balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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"
+
+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: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> 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: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balance_left lt k x rt)"
+by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1)
+
+lemma balance_left_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> 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 \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
+ shows "k \<guillemotleft>| 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 |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
+ shows "balance_left a x t b |\<guillemotleft> k"
+using assms
+by (induct a x t b rule: balance_left.induct) auto
+
+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 \<or> k = a \<and> v = b \<or> 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 \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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) \<and> 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 balance_right_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> 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: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>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: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> 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 balance_right_tree_greater:
+ fixes k :: "'a::order"
+ assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
+ shows "k \<guillemotleft>| 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 |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
+ shows "balance_right a x t b |\<guillemotleft> 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 \<or> x = k \<and> y = v \<or> entry_in_tree x y r)"
+using assms by (induct l k v r rule: balance_right.induct) (auto simp: balance_in_tree)
+
+fun
+ combine :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
+ bc \<Rightarrow> 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 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
+ bc \<Rightarrow> 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 combine_inv1:
+ assumes "inv1 lt" "inv1 rt"
+ shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> 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 combine_tree_greater[simp]:
+ fixes k :: "'a::linorder"
+ assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r"
+ shows "k \<guillemotleft>| 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 |\<guillemotleft> k" "r |\<guillemotleft> k"
+ shows "combine l r |\<guillemotleft> k"
+using assms
+by (induct l r rule: combine.induct)
+ (auto simp: balance_left_tree_less split:rbt.splits color.splits)
+
+lemma combine_sorted:
+ fixes k :: "'a::linorder"
+ assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| 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 |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 \<and> 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 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 \<or> 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)
+
+ 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)
+
+fun
+ del_from_left :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
+ del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
+ del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('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
+ assumes "inv2 lt" "inv1 lt"
+ shows
+ "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
+ inv2 (del_from_left x lt k v rt) \<and> bheight (del_from_left x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_left x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_left x lt k v rt))"
+ and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
+ inv2 (del_from_right x lt k v rt) \<and> bheight (del_from_right x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_right x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_right x lt k v rt))"
+ and del_inv1_inv2: "inv2 (del x lt) \<and> (color_of lt = R \<and> bheight (del x lt) = bheight lt \<and> inv1 (del x lt)
+ \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
+using assms
+proof (induct x lt k v rt and x lt k v rt and x lt rule: del_from_left_del_from_right_del.induct)
+case (2 y c _ y')
+ have "y = y' \<or> y < y' \<or> y > y'" by auto
+ thus ?case proof (elim disjE)
+ assume "y = y'"
+ with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
+ next
+ assume "y < y'"
+ with 2 show ?thesis by (cases c) auto
+ next
+ assume "y' < y"
+ with 2 show ?thesis by (cases c) auto
+ qed
+next
+ case (3 y lt z v rta y' ss bb)
+ thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+
+next
+ case (5 y a y' ss lt z v rta)
+ thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+
+next
+ case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
+qed auto
+
+lemma
+ del_from_left_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_left x lt k y rt)"
+ and del_from_right_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_right x lt k y rt)"
+ and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
+by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
+ (auto simp: balance_left_tree_less balance_right_tree_less)
+
+lemma del_from_left_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_left x lt k y rt)"
+ and del_from_right_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_right x lt k y rt)"
+ and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
+by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
+ (auto simp: balance_left_tree_greater balance_right_tree_greater)
+
+lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_left x lt k y rt)"
+ and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_right x lt k y rt)"
+ and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
+proof (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
+ case (3 x lta zz v rta yy ss bb)
+ from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
+ hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
+ with 3 show ?case by (simp add: balance_left_sorted)
+next
+ case ("4_2" x vaa vbb vdd vc yy ss bb)
+ hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
+ hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less)
+ with "4_2" show ?case by simp
+next
+ case (5 x aa yy ss lta zz v rta)
+ hence "tree_greater yy (Branch B lta zz v rta)" by simp
+ hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
+ with 5 show ?case by (simp add: balance_right_sorted)
+next
+ case ("6_2" x aa yy ss vaa vbb vdd vc)
+ hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
+ hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
+ with "6_2" show ?case by simp
+qed (auto simp: combine_sorted)
+
+lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_left x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
+ and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_right x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
+ and del_in_tree: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
+proof (induct x lt kt y rt and x lt kt y rt and x t rule: del_from_left_del_from_right_del.induct)
+ case (2 xx c aa yy ss bb)
+ have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
+ from this 2 show ?case proof (elim disjE)
+ assume "xx = yy"
+ with 2 show ?thesis proof (cases "xx = k")
+ case True
+ from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
+ hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
+ with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree)
+ qed (simp add: combine_in_tree)
+ qed simp+
+next
+ case (3 xx lta zz vv rta yy ss bb)
+ def mt[simp]: mt == "Branch B lta zz vv rta"
+ from 3 have "inv2 mt \<and> inv1 mt" by simp
+ hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
+ with 3 have 4: "entry_in_tree k v (del_from_left xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balance_left_in_tree)
+ thus ?case proof (cases "xx = k")
+ case True
+ from 3 True have "tree_greater yy bb \<and> yy > k" by simp
+ hence "tree_greater k bb" by (blast dest: tree_greater_trans)
+ with 3 4 True show ?thesis by (auto simp: tree_greater_nit)
+ qed auto
+next
+ case ("4_1" xx yy ss bb)
+ show ?case proof (cases "xx = k")
+ case True
+ with "4_1" have "tree_greater yy bb \<and> k < yy" by simp
+ hence "tree_greater k bb" by (blast dest: tree_greater_trans)
+ with "4_1" `xx = k`
+ have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit)
+ thus ?thesis by auto
+ qed simp+
+next
+ case ("4_2" xx vaa vbb vdd vc yy ss bb)
+ thus ?case proof (cases "xx = k")
+ case True
+ with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
+ hence "tree_greater k bb" by (blast dest: tree_greater_trans)
+ with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
+ qed auto
+next
+ case (5 xx aa yy ss lta zz vv rta)
+ def mt[simp]: mt == "Branch B lta zz vv rta"
+ from 5 have "inv2 mt \<and> inv1 mt" by simp
+ hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
+ with 5 have 3: "entry_in_tree k v (del_from_right xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balance_right_in_tree)
+ thus ?case proof (cases "xx = k")
+ case True
+ from 5 True have "tree_less yy aa \<and> yy < k" by simp
+ hence "tree_less k aa" by (blast dest: tree_less_trans)
+ with 3 5 True show ?thesis by (auto simp: tree_less_nit)
+ qed auto
+next
+ case ("6_1" xx aa yy ss)
+ show ?case proof (cases "xx = k")
+ case True
+ with "6_1" have "tree_less yy aa \<and> k > yy" by simp
+ hence "tree_less k aa" by (blast dest: tree_less_trans)
+ with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit)
+ qed simp
+next
+ case ("6_2" xx aa yy ss vaa vbb vdd vc)
+ thus ?case proof (cases "xx = k")
+ case True
+ with "6_2" have "k > yy \<and> tree_less yy aa" by simp
+ hence "tree_less k aa" by (blast dest: tree_less_trans)
+ with True "6_2" show ?thesis by (auto simp: tree_less_nit)
+ qed auto
+qed simp
+
+
+definition delete where
+ delete_def: "delete k t = paint B (del k t)"
+
+theorem delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
+proof -
+ from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto
+ hence "inv2 (del k t) \<and> (color_of t = R \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color_of t = B \<and> bheight (del k t) = bheight t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2)
+ hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto
+ with assms show ?thesis
+ unfolding is_rbt_def delete_def
+ by (auto intro: paint_sorted del_sorted)
+qed
+
+lemma delete_in_tree:
+ assumes "is_rbt t"
+ shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
+ using assms unfolding is_rbt_def delete_def
+ by (auto simp: del_in_tree)
+
+lemma lookup_delete:
+ assumes is_rbt: "is_rbt t"
+ shows "lookup (delete k t) = (lookup t)|`(-{k})"
+proof
+ fix x
+ show "lookup (delete k t) x = (lookup t |` (-{k})) x"
+ proof (cases "x = k")
+ assume "x = k"
+ with is_rbt show ?thesis
+ by (cases "lookup (delete k t) k") (auto simp: lookup_in_tree delete_in_tree)
+ next
+ assume "x \<noteq> k"
+ thus ?thesis
+ by auto (metis is_rbt delete_is_rbt delete_in_tree is_rbt_sorted lookup_from_in_tree)
+ qed
+qed
+
+
+subsection {* Union *}
+
+primrec
+ union_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
+where
+ "union_with_key f t Empty = t"
+| "union_with_key f t (Branch c lt k v rt) = union_with_key f (union_with_key f (insert_with_key f k v t) lt) rt"
+
+lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (union_with_key f lt rt)"
+ by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
+theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (union_with_key f lt rt)"
+ by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
+
+definition
+ union_with where
+ "union_with f = union_with_key (\<lambda>_. f)"
+
+theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union_with f lt rt)" unfolding union_with_def by simp
+
+definition union where
+ "union = union_with_key (%_ _ rv. rv)"
+
+theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
+
+lemma union_Branch[simp]:
+ "union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt"
+ unfolding union_def insert_def
+ by simp
+
+lemma lookup_union:
+ assumes "is_rbt s" "sorted t"
+ shows "lookup (union s t) = lookup s ++ lookup t"
+using assms
+proof (induct t arbitrary: s)
+ case Empty thus ?case by (auto simp: union_def)
+next
+ case (Branch c l k v r s)
+ then have "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
+
+ have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
+ lookup s ++
+ (\<lambda>a. if a < k then lookup l a
+ else if k < a then lookup r a else Some v)" (is "?m1 = ?m2")
+ proof (rule ext)
+ fix a
+
+ have "k < a \<or> k = a \<or> k > a" by auto
+ thus "?m1 a = ?m2 a"
+ proof (elim disjE)
+ assume "k < a"
+ with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tree_less_trans)
+ with `k < a` show ?thesis
+ by (auto simp: map_add_def split: option.splits)
+ next
+ assume "k = a"
+ with `l |\<guillemotleft> k` `k \<guillemotleft>| r`
+ show ?thesis by (auto simp: map_add_def)
+ next
+ assume "a < k"
+ from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tree_greater_trans)
+ with `a < k` show ?thesis
+ by (auto simp: map_add_def split: option.splits)
+ qed
+ qed
+
+ from Branch have is_rbt: "is_rbt (RBT_Impl.union (RBT_Impl.insert k v s) l)"
+ by (auto intro: union_is_rbt insert_is_rbt)
+ with Branch have IHs:
+ "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
+ "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
+ by auto
+
+ with meq show ?case
+ by (auto simp: lookup_insert[OF Branch(3)])
+
+qed
+
+
+subsection {* Modifying existing entries *}
+
+primrec
+ map_entry :: "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
+where
+ "map_entry k f Empty = Empty"
+| "map_entry k f (Branch c lt x v rt) =
+ (if k < x then Branch c (map_entry k f lt) x v rt
+ else if k > x then (Branch c lt x v (map_entry k f rt))
+ else Branch c lt x (f v) rt)"
+
+lemma map_entry_color_of: "color_of (map_entry k f t) = color_of t" by (induct t) simp+
+lemma map_entry_inv1: "inv1 (map_entry k f t) = inv1 t" by (induct t) (simp add: map_entry_color_of)+
+lemma map_entry_inv2: "inv2 (map_entry k f t) = inv2 t" "bheight (map_entry k f t) = bheight t" by (induct t) simp+
+lemma map_entry_tree_greater: "tree_greater a (map_entry k f t) = tree_greater a t" by (induct t) simp+
+lemma map_entry_tree_less: "tree_less a (map_entry k f t) = tree_less a t" by (induct t) simp+
+lemma map_entry_sorted: "sorted (map_entry k f t) = sorted t"
+ by (induct t) (simp_all add: map_entry_tree_less map_entry_tree_greater)
+
+theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t"
+unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
+
+theorem lookup_map_entry:
+ "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
+ by (induct t) (auto split: option.splits simp add: expand_fun_eq)
+
+
+subsection {* Mapping all entries *}
+
+primrec
+ map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'c) rbt"
+where
+ "map f Empty = Empty"
+| "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)"
+
+lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)"
+ by (induct t) auto
+lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def)
+lemma map_tree_greater: "tree_greater k (map f t) = tree_greater k t" by (induct t) simp+
+lemma map_tree_less: "tree_less k (map f t) = tree_less k t" by (induct t) simp+
+lemma map_sorted: "sorted (map f t) = sorted t" by (induct t) (simp add: map_tree_less map_tree_greater)+
+lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+
+lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+
+lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+
+theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t"
+unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
+
+theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)"
+ by (induct t) auto
+
+
+subsection {* Folding over entries *}
+
+definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
+ "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)"
+
+lemma fold_simps [simp, code]:
+ "fold f Empty = id"
+ "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
+ by (simp_all add: fold_def expand_fun_eq)
+
+
+subsection {* Bulkloading a tree *}
+
+definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where
+ "bulkload xs = foldr (\<lambda>(k, v). insert k v) xs Empty"
+
+lemma bulkload_is_rbt [simp, intro]:
+ "is_rbt (bulkload xs)"
+ unfolding bulkload_def by (induct xs) auto
+
+lemma lookup_bulkload:
+ "lookup (bulkload xs) = map_of xs"
+proof -
+ obtain ys where "ys = rev xs" by simp
+ have "\<And>t. is_rbt t \<Longrightarrow>
+ lookup (foldl (\<lambda>t (k, v). insert k v t) t ys) = lookup t ++ map_of (rev ys)"
+ by (induct ys) (simp_all add: bulkload_def split_def lookup_insert)
+ from this Empty_is_rbt have
+ "lookup (foldl (\<lambda>t (k, v). insert k v t) Empty (rev xs)) = lookup Empty ++ map_of xs"
+ by (simp add: `ys = rev xs`)
+ then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
+qed
+
+hide (open) const Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
+
+end
--- a/src/HOL/Library/Table.thy Fri Apr 16 15:49:13 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,229 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Tables: finite mappings implemented by red-black trees *}
-
-theory Table
-imports Main RBT Mapping
-begin
-
-subsection {* Type definition *}
-
-typedef (open) ('a, 'b) table = "{t :: ('a\<Colon>linorder, 'b) rbt. is_rbt t}"
- morphisms tree_of Table
-proof -
- have "RBT.Empty \<in> ?table" by simp
- then show ?thesis ..
-qed
-
-lemma is_rbt_tree_of [simp, intro]:
- "is_rbt (tree_of t)"
- using tree_of [of t] by simp
-
-lemma table_eq:
- "t1 = t2 \<longleftrightarrow> tree_of t1 = tree_of t2"
- by (simp add: tree_of_inject)
-
-lemma [code abstype]:
- "Table (tree_of t) = t"
- by (simp add: tree_of_inverse)
-
-
-subsection {* Primitive operations *}
-
-definition lookup :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a \<rightharpoonup> 'b" where
- [code]: "lookup t = RBT.lookup (tree_of t)"
-
-definition empty :: "('a\<Colon>linorder, 'b) table" where
- "empty = Table RBT.Empty"
-
-lemma tree_of_empty [code abstract]:
- "tree_of empty = RBT.Empty"
- by (simp add: empty_def Table_inverse)
-
-definition update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
- "update k v t = Table (RBT.insert k v (tree_of t))"
-
-lemma tree_of_update [code abstract]:
- "tree_of (update k v t) = RBT.insert k v (tree_of t)"
- by (simp add: update_def Table_inverse)
-
-definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
- "delete k t = Table (RBT.delete k (tree_of t))"
-
-lemma tree_of_delete [code abstract]:
- "tree_of (delete k t) = RBT.delete k (tree_of t)"
- by (simp add: delete_def Table_inverse)
-
-definition entries :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a \<times> 'b) list" where
- [code]: "entries t = RBT.entries (tree_of t)"
-
-definition keys :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a list" where
- [code]: "keys t = RBT.keys (tree_of t)"
-
-definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) table" where
- "bulkload xs = Table (RBT.bulkload xs)"
-
-lemma tree_of_bulkload [code abstract]:
- "tree_of (bulkload xs) = RBT.bulkload xs"
- by (simp add: bulkload_def Table_inverse)
-
-definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
- "map_entry k f t = Table (RBT.map_entry k f (tree_of t))"
-
-lemma tree_of_map_entry [code abstract]:
- "tree_of (map_entry k f t) = RBT.map_entry k f (tree_of t)"
- by (simp add: map_entry_def Table_inverse)
-
-definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
- "map f t = Table (RBT.map f (tree_of t))"
-
-lemma tree_of_map [code abstract]:
- "tree_of (map f t) = RBT.map f (tree_of t)"
- by (simp add: map_def Table_inverse)
-
-definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> 'c \<Rightarrow> 'c" where
- [code]: "fold f t = RBT.fold f (tree_of t)"
-
-
-subsection {* Derived operations *}
-
-definition is_empty :: "('a\<Colon>linorder, 'b) table \<Rightarrow> bool" where
- [code]: "is_empty t = (case tree_of t of RBT.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
-
-
-subsection {* Abstract lookup properties *}
-
-lemma lookup_Table:
- "is_rbt t \<Longrightarrow> lookup (Table t) = RBT.lookup t"
- by (simp add: lookup_def Table_inverse)
-
-lemma lookup_tree_of:
- "RBT.lookup (tree_of t) = lookup t"
- by (simp add: lookup_def)
-
-lemma entries_tree_of:
- "RBT.entries (tree_of t) = entries t"
- by (simp add: entries_def)
-
-lemma keys_tree_of:
- "RBT.keys (tree_of t) = keys t"
- by (simp add: keys_def)
-
-lemma lookup_empty [simp]:
- "lookup empty = Map.empty"
- by (simp add: empty_def lookup_Table expand_fun_eq)
-
-lemma lookup_update [simp]:
- "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
- by (simp add: update_def lookup_Table lookup_insert lookup_tree_of)
-
-lemma lookup_delete [simp]:
- "lookup (delete k t) = (lookup t)(k := None)"
- by (simp add: delete_def lookup_Table RBT.lookup_delete lookup_tree_of restrict_complement_singleton_eq)
-
-lemma map_of_entries [simp]:
- "map_of (entries t) = lookup t"
- by (simp add: entries_def map_of_entries lookup_tree_of)
-
-lemma entries_lookup:
- "entries t1 = entries t2 \<longleftrightarrow> 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_Table RBT.lookup_bulkload)
-
-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_Table lookup_map_entry lookup_tree_of)
-
-lemma lookup_map [simp]:
- "lookup (map f t) k = Option.map (f k) (lookup t k)"
- by (simp add: map_def lookup_Table lookup_map lookup_tree_of)
-
-lemma fold_fold:
- "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
- by (simp add: fold_def expand_fun_eq RBT.fold_def entries_tree_of)
-
-lemma is_empty_empty [simp]:
- "is_empty t \<longleftrightarrow> t = empty"
- by (simp add: table_eq is_empty_def tree_of_empty split: rbt.split)
-
-lemma RBT_lookup_empty [simp]: (*FIXME*)
- "RBT.lookup t = Map.empty \<longleftrightarrow> t = RBT.Empty"
- by (cases t) (auto simp add: expand_fun_eq)
-
-lemma lookup_empty_empty [simp]:
- "lookup t = Map.empty \<longleftrightarrow> t = empty"
- by (cases t) (simp add: empty_def lookup_def Table_inject Table_inverse)
-
-lemma sorted_keys [iff]:
- "sorted (keys t)"
- by (simp add: keys_def RBT.keys_def sorted_entries)
-
-lemma distinct_keys [iff]:
- "distinct (keys t)"
- by (simp add: keys_def RBT.keys_def distinct_entries)
-
-
-subsection {* Implementation of mappings *}
-
-definition Mapping :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) mapping" where
- "Mapping t = Mapping.Mapping (lookup t)"
-
-code_datatype Mapping
-
-lemma lookup_Mapping [simp, code]:
- "Mapping.lookup (Mapping t) = lookup t"
- by (simp add: Mapping_def)
-
-lemma empty_Mapping [code]:
- "Mapping.empty = Mapping empty"
- by (rule mapping_eqI) simp
-
-lemma is_empty_Mapping [code]:
- "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
- by (simp add: table_eq Mapping.is_empty_empty Mapping_def)
-
-lemma update_Mapping [code]:
- "Mapping.update k v (Mapping t) = Mapping (update k v t)"
- by (rule mapping_eqI) simp
-
-lemma delete_Mapping [code]:
- "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
- by (rule mapping_eqI) simp
-
-lemma keys_Mapping [code]:
- "Mapping.keys (Mapping t) = set (keys t)"
- by (simp add: keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
-
-lemma ordered_keys_Mapping [code]:
- "Mapping.ordered_keys (Mapping t) = keys t"
- by (rule sorted_distinct_set_unique) (simp_all add: ordered_keys_def keys_Mapping)
-
-lemma Mapping_size_card_keys: (*FIXME*)
- "Mapping.size m = card (Mapping.keys m)"
- by (simp add: Mapping.size_def Mapping.keys_def)
-
-lemma size_Mapping [code]:
- "Mapping.size (Mapping t) = length (keys t)"
- by (simp add: Mapping_size_card_keys keys_Mapping distinct_card)
-
-lemma tabulate_Mapping [code]:
- "Mapping.tabulate ks f = Mapping (bulkload (List.map (\<lambda>k. (k, f k)) ks))"
- by (rule mapping_eqI) (simp add: map_of_map_restrict)
-
-lemma bulkload_Mapping [code]:
- "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
- by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
-
-lemma [code, code del]: "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
-
-lemma eq_Mapping [code]:
- "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
- by (simp add: eq Mapping_def entries_lookup)
-
-hide (open) const tree_of lookup empty update delete
- entries keys bulkload map_entry map fold
-
-end
--- a/src/HOL/List.thy Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOL/List.thy Fri Apr 16 15:49:46 2010 +0200
@@ -513,6 +513,17 @@
(cases zs, simp_all)
qed
+lemma list_induct4 [consumes 3, case_names Nil Cons]:
+ "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow>
+ P [] [] [] [] \<Longrightarrow> (\<And>x xs y ys z zs w ws. length xs = length ys \<Longrightarrow>
+ length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> P xs ys zs ws \<Longrightarrow>
+ P (x#xs) (y#ys) (z#zs) (w#ws)) \<Longrightarrow> P xs ys zs ws"
+proof (induct xs arbitrary: ys zs ws)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)
+qed
+
lemma list_induct2':
"\<lbrakk> P [] [];
\<And>x xs. P (x#xs) [];
--- a/src/HOL/Statespace/state_fun.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Fri Apr 16 15:49:46 2010 +0200
@@ -193,7 +193,7 @@
(* mk_updterm returns
* - (orig-term-skeleton,simplified-term-skeleton, vars, b)
- * where boolean b tells if a simplification has occured.
+ * where boolean b tells if a simplification has occurred.
"orig-term-skeleton = simplified-term-skeleton" is
* the desired simplification rule.
* The algorithm first walks down the updates to the seed-state while
--- a/src/HOL/Statespace/state_space.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Fri Apr 16 15:49:46 2010 +0200
@@ -478,6 +478,21 @@
Type (name, Ts) => (Ts, name)
| T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T));
+fun read_typ ctxt raw_T env =
+ let
+ val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
+ val T = Syntax.read_typ ctxt' raw_T;
+ val env' = OldTerm.add_typ_tfrees (T, env);
+ in (T, env') end;
+
+fun cert_typ ctxt raw_T env =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val T = Type.no_tvars (Sign.certify_typ thy raw_T)
+ handle TYPE (msg, _, _) => error msg;
+ val env' = OldTerm.add_typ_tfrees (T, env);
+ in (T, env') end;
+
fun gen_define_statespace prep_typ state_space args name parents comps thy =
let (* - args distinct
- only args may occur in comps and parent-instantiations
@@ -500,7 +515,7 @@
val (Ts',env') = fold_map (prep_typ ctxt) Ts env
handle ERROR msg => cat_error msg
- ("The error(s) above occured in parent statespace specification "
+ ("The error(s) above occurred in parent statespace specification "
^ quote pname);
val err_insts = if length args <> length Ts' then
["number of type instantiation(s) does not match arguments of parent statespace "
@@ -539,7 +554,7 @@
fun prep_comp (n,T) env =
let val (T', env') = prep_typ ctxt T env handle ERROR msg =>
- cat_error msg ("The error(s) above occured in component " ^ quote n)
+ cat_error msg ("The error(s) above occurred in component " ^ quote n)
in ((n,T'), env') end;
val (comps',env') = fold_map prep_comp comps env;
@@ -579,8 +594,8 @@
end
handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name);
-val define_statespace = gen_define_statespace Record.read_typ NONE;
-val define_statespace_i = gen_define_statespace Record.cert_typ;
+val define_statespace = gen_define_statespace read_typ NONE;
+val define_statespace_i = gen_define_statespace cert_typ;
(*** parse/print - translations ***)
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Apr 16 15:49:46 2010 +0200
@@ -682,7 +682,7 @@
(constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
end handle ERROR msg => cat_error msg
- ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
+ ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
" of datatype " ^ quote (Binding.str_of tname));
val (constrs', constr_syntax', sorts') =
--- a/src/HOL/Tools/record.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOL/Tools/record.ML Fri Apr 16 15:49:46 2010 +0200
@@ -54,9 +54,9 @@
val print_records: theory -> unit
val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
- val add_record: bool -> string list * binding -> (typ list * string) option ->
+ val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
(binding * typ * mixfix) list -> theory -> theory
- val add_record_cmd: bool -> string list * binding -> string option ->
+ val add_record_cmd: bool -> (string * string option) list * binding -> string option ->
(binding * string * mixfix) list -> theory -> theory
val setup: theory -> theory
end;
@@ -64,7 +64,8 @@
signature ISO_TUPLE_SUPPORT =
sig
- val add_iso_tuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
+ val add_iso_tuple_type: bstring * (string * sort) list ->
+ typ * typ -> theory -> (term * term) * theory
val mk_cons_tuple: term * term -> term
val dest_cons_tuple: term -> term * term
val iso_tuple_intros_tac: int -> tactic
@@ -742,7 +743,7 @@
val varifyT = varifyT midx;
val vartypes = map varifyT types;
- val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty
+ val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
handle Type.TYPE_MATCH => err "type is no proper record (extension)";
val alphas' =
map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
@@ -872,11 +873,10 @@
apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs;
val (args', more) = split_last args;
val alphavars = map varifyT (but_last alphas);
- val subst = fold (Sign.typ_match thy) (alphavars ~~ args') Vartab.empty;
+ val subst = Type.raw_matches (alphavars, args') Vartab.empty;
val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
in fields'' @ strip_fields more end
- handle Type.TYPE_MATCH => [("", T)]
- | Library.UnequalLengths => [("", T)])
+ handle Type.TYPE_MATCH => [("", T)])
| _ => [("", T)])
| _ => [("", T)])
| _ => [("", T)])
@@ -900,19 +900,18 @@
val midx = maxidx_of_typ T;
val varifyT = varifyT midx;
- fun mk_type_abbr subst name alphas =
- let val abbrT = Type (name, map (fn a => varifyT (TFree (a, HOLogic.typeS))) alphas) in
- Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
- end;
-
- fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
+ fun mk_type_abbr subst name args =
+ let val abbrT = Type (name, map (varifyT o TFree) args)
+ in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
+
+ fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
in
if ! print_record_type_abbr then
(case last_extT T of
SOME (name, _) =>
if name = last_ext then
let val subst = match schemeT T in
- if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, HOLogic.typeS))))
+ if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
then mk_type_abbr subst abbr alphas
else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
@@ -1639,11 +1638,10 @@
val fields_moreTs = fieldTs @ [moreT];
val alphas_zeta = alphas @ [zeta];
- val alphas_zetaTs = map (fn a => TFree (a, HOLogic.typeS)) alphas_zeta;
val ext_binding = Binding.name (suffix extN base_name);
val ext_name = suffix extN name;
- val extT = Type (suffix ext_typeN name, alphas_zetaTs);
+ val extT = Type (suffix ext_typeN name, map TFree alphas_zeta);
val ext_type = fields_moreTs ---> extT;
@@ -1846,10 +1844,8 @@
(* record_definition *)
-fun record_definition (args, binding) parent (parents: parent_info list) raw_fields thy =
+fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
let
- val alphas = map fst args;
-
val name = Sign.full_name thy binding;
val full = Sign.full_name_path thy (Binding.name_of binding); (* FIXME Binding.qualified (!?) *)
@@ -1869,7 +1865,7 @@
val fields = map (apfst full) bfields;
val names = map fst fields;
val types = map snd fields;
- val alphas_fields = fold Term.add_tfree_namesT types [];
+ val alphas_fields = fold Term.add_tfreesT types [];
val alphas_ext = inter (op =) alphas_fields alphas;
val len = length fields;
val variants =
@@ -1885,9 +1881,8 @@
val all_vars = parent_vars @ vars;
val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
-
- val zeta = Name.variant alphas "'z";
- val moreT = TFree (zeta, HOLogic.typeS);
+ val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS);
+ val moreT = TFree zeta;
val more = Free (moreN, moreT);
val full_moreN = full (Binding.name moreN);
val bfields_more = bfields @ [(Binding.name moreN, moreT)];
@@ -1978,8 +1973,8 @@
(*record (scheme) type abbreviation*)
val recordT_specs =
- [(Binding.suffix_name schemeN binding, alphas @ [zeta], rec_schemeT0, NoSyn),
- (binding, alphas, recT0, NoSyn)];
+ [(Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), rec_schemeT0, NoSyn),
+ (binding, map #1 alphas, recT0, NoSyn)];
val ext_defs = ext_def :: map #ext_def parents;
@@ -2349,7 +2344,7 @@
((Binding.name "iffs", iffs), [iff_add])];
val info =
- make_record_info args parent fields extension
+ make_record_info alphas parent fields extension
ext_induct ext_inject ext_surjective ext_split ext_def
sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
@@ -2371,10 +2366,25 @@
(* add_record *)
-(*We do all preparations and error checks here, deferring the real
- work to record_definition.*)
-fun gen_add_record prep_typ prep_raw_parent quiet_mode
- (params, binding) raw_parent raw_fields thy =
+local
+
+fun read_parent NONE ctxt = (NONE, ctxt)
+ | read_parent (SOME raw_T) ctxt =
+ (case ProofContext.read_typ_abbrev ctxt raw_T of
+ Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
+ | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
+
+fun prep_field prep (x, T, mx) = (x, prep T, mx)
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in record field " ^ quote (Binding.str_of x));
+
+fun read_field raw_field ctxt =
+ let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
+ in (field, Variable.declare_typ T ctxt) end;
+
+in
+
+fun add_record quiet_mode (params, binding) raw_parent raw_fields thy =
let
val _ = Theory.requires thy "Record" "record definitions";
val _ =
@@ -2382,40 +2392,19 @@
else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
val ctxt = ProofContext.init thy;
-
-
- (* parents *)
-
- fun prep_inst T = fst (cert_typ ctxt T []);
-
- val parent = Option.map (apfst (map prep_inst) o prep_raw_parent ctxt) raw_parent
- handle ERROR msg => cat_error msg ("The error(s) above in parent record specification");
+ fun cert_typ T = Type.no_tvars (ProofContext.cert_typ ctxt T)
+ handle TYPE (msg, _, _) => error msg;
+
+
+ (* specification *)
+
+ val parent = Option.map (apfst (map cert_typ)) raw_parent
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in parent record specification");
+ val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
val parents = add_parents thy parent [];
- val init_env =
- (case parent of
- NONE => []
- | SOME (types, _) => fold Term.add_tfreesT types []);
-
-
- (* fields *)
-
- fun prep_field (x, raw_T, mx) env =
- let
- val (T, env') =
- prep_typ ctxt raw_T env handle ERROR msg =>
- cat_error msg ("The error(s) above occured in record field " ^ quote (Binding.str_of x));
- in ((x, T, mx), env') end;
-
- val (bfields, envir) = fold_map prep_field raw_fields init_env;
- val envir_names = map fst envir;
-
-
- (* args *)
-
- val defaultS = Sign.defaultS thy;
- val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params;
-
+ val bfields = map (prep_field cert_typ) raw_fields;
(* errors *)
@@ -2424,15 +2413,12 @@
if is_none (get_record thy name) then []
else ["Duplicate definition of record " ^ quote name];
- val err_dup_parms =
- (case duplicates (op =) params of
+ val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
+ val err_extra_frees =
+ (case subtract (op =) params spec_frees of
[] => []
- | dups => ["Duplicate parameter(s) " ^ commas dups]);
-
- val err_extra_frees =
- (case subtract (op =) params envir_names of
- [] => []
- | extras => ["Extra free type variable(s) " ^ commas extras]);
+ | extras => ["Extra free type variable(s) " ^
+ commas (map (Syntax.string_of_typ ctxt o TFree) extras)]);
val err_no_fields = if null bfields then ["No fields present"] else [];
@@ -2445,23 +2431,25 @@
if forall (not_equal moreN o Binding.name_of o #1) bfields then []
else ["Illegal field name " ^ quote moreN];
- val err_dup_sorts =
- (case duplicates (op =) envir_names of
- [] => []
- | dups => ["Inconsistent sort constraints for " ^ commas dups]);
-
val errs =
- err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
- err_dup_fields @ err_bad_fields @ err_dup_sorts;
-
+ err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
val _ = if null errs then () else error (cat_lines errs);
in
- thy |> record_definition (args, binding) parent parents bfields
+ thy |> record_definition (params, binding) parent parents bfields
end
handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
-val add_record = gen_add_record cert_typ (K I);
-val add_record_cmd = gen_add_record read_typ read_raw_parent;
+fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
+ let
+ val ctxt = ProofContext.init thy;
+ val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
+ val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
+ val (parent, ctxt2) = read_parent raw_parent ctxt1;
+ val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
+ val params' = map (ProofContext.check_tfree ctxt3) params;
+ in thy |> add_record quiet_mode (params', binding) parent fields end;
+
+end;
(* setup theory *)
@@ -2479,7 +2467,7 @@
val _ =
OuterSyntax.command "record" "define extensible record" K.thy_decl
- (P.type_args -- P.binding --
+ (P.type_args_constrained -- P.binding --
(P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const_binding)
>> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
--- a/src/HOL/Tools/typecopy.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML Fri Apr 16 15:49:46 2010 +0200
@@ -8,7 +8,7 @@
sig
type info = { vs: (string * sort) list, constr: string, typ: typ,
inject: thm, proj: string * typ, proj_def: thm }
- val typecopy: binding * string list -> typ -> (binding * binding) option
+ val typecopy: binding * (string * sort) list -> typ -> (binding * binding) option
-> theory -> (string * info) * theory
val get_info: theory -> string -> info option
val interpretation: (string -> theory -> theory) -> theory -> theory
@@ -52,8 +52,8 @@
fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
let
val ty = Sign.certify_typ thy raw_ty;
- val vs =
- AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
+ val ctxt = ProofContext.init thy |> Variable.declare_typ ty;
+ val vs = map (ProofContext.check_tfree ctxt) raw_vs;
val tac = Tactic.rtac UNIV_witness 1;
fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })
@@ -80,8 +80,7 @@
end
in
thy
- |> Typedef.add_typedef_global false (SOME raw_tyco)
- (raw_tyco, map (fn (v, _) => (v, dummyS)) vs, NoSyn) (* FIXME keep constraints!? *)
+ |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
(HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
|-> (fn (tyco, info) => add_info tyco info)
end;
--- a/src/HOL/Tools/typedef.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOL/Tools/typedef.ML Fri Apr 16 15:49:46 2010 +0200
@@ -135,9 +135,9 @@
(* rhs *)
- val (_, tmp_lthy) = lthy |> Typedecl.predeclare_constraints (tname, raw_args, mx);
- val set = prep_term tmp_lthy raw_set;
- val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
+ val tmp_ctxt = lthy |> fold (Variable.declare_typ o TFree) raw_args;
+ val set = prep_term tmp_ctxt raw_set;
+ val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
val setT = Term.fastype_of set;
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
@@ -149,7 +149,7 @@
(* lhs *)
- val args = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
+ val args = map (ProofContext.check_tfree tmp_ctxt') raw_args;
val (newT, typedecl_lthy) = lthy
|> Typedecl.typedecl (tname, args, mx)
||> Variable.declare_term set;
--- a/src/HOL/ex/Codegenerator_Candidates.thy Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Fri Apr 16 15:49:46 2010 +0200
@@ -20,8 +20,8 @@
"~~/src/HOL/Number_Theory/Primes"
Product_ord
"~~/src/HOL/ex/Records"
+ RBT
SetsAndFunctions
- Table
While_Combinator
Word
begin
--- a/src/HOLCF/Domain.thy Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOLCF/Domain.thy Fri Apr 16 15:49:46 2010 +0200
@@ -149,8 +149,8 @@
cfcomp2 sfst_defined_iff ssnd_defined_iff
lemmas take_con_rules =
- ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict
- sprod_map_spair' sprod_map_strict u_map_up u_map_strict
+ ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
+ deflation_strict deflation_ID ID1 cfcomp2
use "Tools/cont_consts.ML"
use "Tools/cont_proc.ML"
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Apr 16 15:49:46 2010 +0200
@@ -184,8 +184,7 @@
val rhs = con_app2 con one_rhs args;
val goal = mk_trp (lhs === rhs);
val rules =
- [ax_abs_iso]
- @ @{thms take_con_rules ID1 cfcomp2 deflation_strict}
+ [ax_abs_iso] @ @{thms take_con_rules}
@ take_Suc_thms @ deflation_thms @ deflation_take_thms;
val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
in pg con_appls goal (K tacs) end;
--- a/src/HOLCF/Tools/pcpodef.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML Fri Apr 16 15:49:46 2010 +0200
@@ -169,18 +169,18 @@
val _ = Theory.requires thy "Pcpodef" "pcpodefs";
(*rhs*)
- val (_, tmp_lthy) =
- thy |> Theory.copy |> Theory_Target.init NONE
- |> Typedecl.predeclare_constraints (tname, raw_args, mx);
- val set = prep_term tmp_lthy raw_set;
- val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
+ val tmp_ctxt =
+ ProofContext.init thy
+ |> fold (Variable.declare_typ o TFree) raw_args;
+ val set = prep_term tmp_ctxt raw_set;
+ val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
val setT = Term.fastype_of set;
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_lthy setT));
+ error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
(*lhs*)
- val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
+ val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
val full_tname = Sign.full_name thy tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
--- a/src/HOLCF/Tools/repdef.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML Fri Apr 16 15:49:46 2010 +0200
@@ -64,18 +64,18 @@
val _ = Theory.requires thy "Representable" "repdefs";
(*rhs*)
- val (_, tmp_lthy) =
- thy |> Theory.copy |> Theory_Target.init NONE
- |> Typedecl.predeclare_constraints (tname, raw_args, mx);
- val defl = prep_term tmp_lthy raw_defl;
- val tmp_lthy = tmp_lthy |> Variable.declare_constraints defl;
+ val tmp_ctxt =
+ ProofContext.init thy
+ |> fold (Variable.declare_typ o TFree) raw_args;
+ val defl = prep_term tmp_ctxt raw_defl;
+ val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
val deflT = Term.fastype_of defl;
val _ = if deflT = @{typ "udom alg_defl"} then ()
- else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_lthy deflT));
+ else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
(*lhs*)
- val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy (a, ~1))) raw_args;
+ val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args;
val lhs_sorts = map snd lhs_tfrees;
val full_tname = Sign.full_name thy tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
--- a/src/Pure/General/path.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/General/path.ML Fri Apr 16 15:49:46 2010 +0200
@@ -1,7 +1,8 @@
(* Title: Pure/General/path.ML
Author: Markus Wenzel, TU Muenchen
-Abstract algebra of file paths (external encoding in Unix style).
+Abstract algebra of file paths: basic POSIX notation, extended by
+named roots (e.g. //foo) and variables (e.g. $BAR).
*)
signature PATH =
@@ -10,6 +11,7 @@
val is_current: T -> bool
val current: T
val root: T
+ val named_root: string -> T
val parent: T
val basic: string -> T
val variable: string -> T
@@ -31,10 +33,15 @@
structure Path: PATH =
struct
-
(* path elements *)
-datatype elem = Root | Parent | Basic of string | Variable of string;
+datatype elem =
+ Root of string |
+ Basic of string |
+ Variable of string |
+ Parent;
+
+local
fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
@@ -46,16 +53,18 @@
[] => chs
| bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
+in
+
+val root_elem = Root o implode o check_elem;
val basic_elem = Basic o implode o check_elem;
val variable_elem = Variable o implode o check_elem;
-fun is_var (Variable _) = true
- | is_var _ = false;
+end;
(* type path *)
-datatype T = Path of elem list;
+datatype T = Path of elem list; (*reversed elements*)
fun rep (Path xs) = xs;
@@ -63,13 +72,16 @@
| is_current _ = false;
val current = Path [];
-val root = Path [Root];
-val parent = Path [Parent];
+val root = Path [Root ""];
+fun named_root s = Path [root_elem (explode s)];
fun basic s = Path [basic_elem (explode s)];
fun variable s = Path [variable_elem (explode s)];
+val parent = Path [Parent];
-fun is_absolute (Path (Root :: _)) = true
- | is_absolute _ = false;
+fun is_absolute (Path xs) =
+ (case try List.last xs of
+ SOME (Root _) => true
+ | _ => false);
fun is_basic (Path [Basic _]) = true
| is_basic _ = false;
@@ -77,37 +89,42 @@
(* append and norm *)
-(*append non-normal path (2n arg) to reversed normal one, result is normal*)
-fun rev_app xs [] = rev xs
- | rev_app _ (Root :: ys) = rev_app [Root] ys
- | rev_app (x :: xs) (Parent :: ys) =
- if x = Parent orelse is_var x then rev_app (Parent :: x :: xs) ys
- else if x = Root then rev_app (x :: xs) ys
- else rev_app xs ys
- | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
+fun apply (y as Root _) _ = [y]
+ | apply Parent (xs as (Root _ :: _)) = xs
+ | apply Parent (Basic _ :: rest) = rest
+ | apply y xs = y :: xs;
-fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
+fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs);
fun appends paths = Library.foldl (uncurry append) (current, paths);
val make = appends o map basic;
-fun norm path = rev_app [] path;
+
+fun norm elems = fold_rev apply elems [];
(* implode *)
-fun implode_elem Root = ""
- | implode_elem Parent = ".."
+local
+
+fun implode_elem (Root "") = ""
+ | implode_elem (Root s) = "//" ^ s
| implode_elem (Basic s) = s
- | implode_elem (Variable s) = "$" ^ s;
+ | implode_elem (Variable s) = "$" ^ s
+ | implode_elem Parent = "..";
+
+in
fun implode_path (Path []) = "."
- | implode_path (Path (Root :: xs)) = "/" ^ space_implode "/" (map implode_elem xs)
- | implode_path (Path xs) = space_implode "/" (map implode_elem xs);
+ | implode_path (Path [Root ""]) = "/"
+ | implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs));
+
+end;
(* explode *)
-fun explode_elem "" = Root
- | explode_elem ".." = Parent
+local
+
+fun explode_elem ".." = Parent
| explode_elem "~" = Variable "HOME"
| explode_elem "~~" = Variable "ISABELLE_HOME"
| explode_elem s =
@@ -115,28 +132,35 @@
"$" :: cs => variable_elem cs
| cs => basic_elem cs);
-val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
+val explode_elems =
+ rev o map explode_elem o filter_out (fn c => c = "" orelse c = ".");
+
+in
-fun explode_path str = Path (norm
- (case space_explode "/" str of
- "" :: ss => Root :: explode_elems ss
- | ss => explode_elems ss));
+fun explode_path str =
+ let val (roots, raw_elems) =
+ (case take_prefix (equal "") (space_explode "/" str) |>> length of
+ (0, es) => ([], es)
+ | (1, es) => ([Root ""], es)
+ | (_, []) => ([Root ""], [])
+ | (_, e :: es) => ([root_elem (explode e)], es))
+ in Path (norm (explode_elems raw_elems @ roots)) end;
+
+end;
(* base element *)
-fun split_path f (path as Path xs) =
- (case try split_last xs of
- SOME (prfx, Basic s) => f (prfx, s)
- | _ => error ("Cannot split path into dir/base: " ^ quote (implode_path path)));
+fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)
+ | split_path _ path = error ("Cannot split path into dir/base: " ^ quote (implode_path path));
-val dir = split_path (fn (prfx, _) => Path prfx);
+val dir = split_path #1;
val base = split_path (fn (_, s) => Path [Basic s]);
-fun ext "" path = path
- | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
+fun ext "" = I
+ | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
-val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
+val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
(case take_suffix (fn c => c <> ".") (explode s) of
([], _) => (Path [Basic s], "")
| (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
@@ -144,14 +168,20 @@
(* expand variables *)
+local
+
fun eval (Variable s) =
- (case getenv s of
- "" => error ("Undefined Isabelle environment variable: " ^ quote s)
- | path => rep (explode_path path))
+ (case getenv s of
+ "" => error ("Undefined Isabelle environment variable: " ^ quote s)
+ | path => rep (explode_path path))
| eval x = [x];
+in
+
val expand = rep #> maps eval #> norm #> Path;
+end;
+
(* source position *)
@@ -163,3 +193,4 @@
val explode = explode_path;
end;
+
--- a/src/Pure/Isar/proof_context.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Apr 16 15:49:46 2010 +0200
@@ -62,6 +62,8 @@
val read_const_proper: Proof.context -> bool -> string -> term
val read_const: Proof.context -> bool -> string -> term
val allow_dummies: Proof.context -> Proof.context
+ val check_tvar: Proof.context -> indexname * sort -> indexname * sort
+ val check_tfree: Proof.context -> string * sort -> string * sort
val decode_term: Proof.context -> term -> term
val standard_infer_types: Proof.context -> term list -> term list
val read_term_pattern: Proof.context -> string -> term
@@ -606,19 +608,26 @@
(* types *)
-fun get_sort ctxt def_sort raw_env =
+fun get_sort ctxt raw_env =
let
val tsig = tsig_of ctxt;
fun eq ((xi, S), (xi', S')) =
Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
val env = distinct eq raw_env;
- val _ = (case duplicates (eq_fst (op =)) env of [] => ()
+ val _ =
+ (case duplicates (eq_fst (op =)) env of
+ [] => ()
| dups => error ("Inconsistent sort constraints for type variable(s) "
^ commas_quote (map (Term.string_of_vname' o fst) dups)));
+ fun lookup xi =
+ (case AList.lookup (op =) env xi of
+ NONE => NONE
+ | SOME S => if S = dummyS then NONE else SOME S);
+
fun get xi =
- (case (AList.lookup (op =) env xi, def_sort xi) of
+ (case (lookup xi, Variable.def_sort ctxt xi) of
(NONE, NONE) => Type.defaultS tsig
| (NONE, SOME S) => S
| (SOME S, NONE) => S
@@ -629,6 +638,9 @@
" for type variable " ^ quote (Term.string_of_vname' xi)));
in get end;
+fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
+fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
+
local
fun intern_skolem ctxt def_type x =
@@ -647,7 +659,7 @@
in
fun term_context ctxt =
- {get_sort = get_sort ctxt (Variable.def_sort ctxt),
+ {get_sort = get_sort ctxt,
map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
map_free = intern_skolem ctxt (Variable.def_type ctxt false)};
@@ -731,9 +743,8 @@
fun parse_typ ctxt text =
let
- val get_sort = get_sort ctxt (Variable.def_sort ctxt);
val (syms, pos) = Syntax.parse_token Markup.typ text;
- val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos)
+ val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
in T end;
--- a/src/Pure/Isar/typedecl.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML Fri Apr 16 15:49:46 2010 +0200
@@ -7,8 +7,7 @@
signature TYPEDECL =
sig
val read_constraint: Proof.context -> string option -> sort
- val predeclare_constraints: binding * (string * sort) list * mixfix ->
- local_theory -> string * local_theory
+ val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory
val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory
end;
@@ -16,6 +15,12 @@
structure Typedecl: TYPEDECL =
struct
+(* constraints *)
+
+fun read_constraint _ NONE = dummyS
+ | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
+
+
(* primitives *)
fun object_logic_arity name thy =
@@ -33,26 +38,15 @@
end;
-(* syntactic version -- useful for internalizing additional types/terms beforehand *)
-
-fun read_constraint _ NONE = dummyS
- | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
-
-fun predeclare_constraints (b, raw_args, mx) =
- basic_typedecl (b, length raw_args, mx) ##>
- fold (Variable.declare_constraints o Logic.mk_type o TFree) raw_args;
-
-
-(* regular version -- without dependencies on type parameters of the context *)
+(* regular typedecl -- without dependencies on type parameters of the context *)
fun typedecl (b, raw_args, mx) lthy =
let
fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
- val args = raw_args
- |> map (fn (a, S) => (a, if S = dummyS then ProofContext.default_sort lthy (a, ~1) else S));
- val T = Type (Local_Theory.full_name lthy b, map TFree args);
+ val args = map (TFree o ProofContext.check_tfree lthy) raw_args;
+ val T = Type (Local_Theory.full_name lthy b, args);
val bad_args =
#2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
--- a/src/Pure/ML-Systems/polyml.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Fri Apr 16 15:49:46 2010 +0200
@@ -66,3 +66,6 @@
use_text context (1, "pp") false
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+val ml_make_string =
+ "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
+
--- a/src/Pure/ML-Systems/polyml_common.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML Fri Apr 16 15:49:46 2010 +0200
@@ -55,7 +55,7 @@
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
-(* print depth *)
+(* toplevel printing *)
local
val depth = Unsynchronized.ref 10;
@@ -66,6 +66,8 @@
val error_depth = PolyML.error_depth;
+val ml_make_string = "PolyML.makestring";
+
(** interrupts **)
--- a/src/Pure/ML-Systems/smlnj.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Fri Apr 16 15:49:46 2010 +0200
@@ -61,6 +61,8 @@
Control.Print.printLength := dest_int n);
end;
+val ml_make_string = "(fn _ => \"?\")";
+
(*prompts*)
fun ml_prompts p1 p2 =
--- a/src/Pure/ML/ml_antiquote.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Fri Apr 16 15:49:46 2010 +0200
@@ -59,6 +59,8 @@
structure P = OuterParse;
+val _ = inline "make_string" (Scan.succeed ml_make_string);
+
val _ = value "binding"
(Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
--- a/src/Pure/ML/ml_env.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/ML/ml_env.ML Fri Apr 16 15:49:46 2010 +0200
@@ -9,6 +9,7 @@
val inherit: Context.generic -> Context.generic -> Context.generic
val name_space: ML_Name_Space.T
val local_context: use_context
+ val check_functor: string -> unit
end
structure ML_Env: ML_ENV =
@@ -88,5 +89,11 @@
print = writeln,
error = error};
+val is_functor = is_some o #lookupFunct name_space;
+
+fun check_functor name =
+ if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
+ else error ("Unknown ML functor: " ^ quote name);
+
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Apr 16 15:49:46 2010 +0200
@@ -955,7 +955,7 @@
end)
| _ => raise PGIP "Invalid PGIP packet received")
handle PGIP msg =>
- (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
+ (Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^
(XML.string_of xml));
true))
--- a/src/Pure/System/isabelle_system.scala Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Fri Apr 16 15:49:46 2010 +0200
@@ -88,31 +88,39 @@
/* expand_path */
+ private val Root = new Regex("(//+[^/]*|/)(.*)")
+ private val Only_Root = new Regex("//+[^/]*|/")
+
def expand_path(isabelle_path: String): String =
{
val result_path = new StringBuilder
- def init(path: String)
+ def init(path: String): String =
{
- if (path.startsWith("/")) {
- result_path.clear
- result_path += '/'
+ path match {
+ case Root(root, rest) =>
+ result_path.clear
+ result_path ++= root
+ rest
+ case _ => path
}
}
def append(path: String)
{
- init(path)
- for (p <- path.split("/") if p != "" && p != ".") {
+ val rest = init(path)
+ for (p <- rest.split("/") if p != "" && p != ".") {
if (p == "..") {
val result = result_path.toString
- val i = result.lastIndexOf("/")
- if (result == "")
- result_path ++= ".."
- else if (result.substring(i + 1) == "..")
- result_path ++= "/.."
- else if (i < 1)
- result_path.length = i + 1
- else
- result_path.length = i
+ if (!Only_Root.pattern.matcher(result).matches) {
+ val i = result.lastIndexOf("/")
+ if (result == "")
+ result_path ++= ".."
+ else if (result.substring(i + 1) == "..")
+ result_path ++= "/.."
+ else if (i < 0)
+ result_path.length = 0
+ else
+ result_path.length = i
+ }
}
else {
val len = result_path.length
@@ -122,8 +130,8 @@
}
}
}
- init(isabelle_path)
- for (p <- isabelle_path.split("/")) {
+ val rest = init(isabelle_path)
+ for (p <- rest.split("/")) {
if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
else if (p == "~") append(getenv_strict("HOME"))
else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
--- a/src/Pure/System/standard_system.scala Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/System/standard_system.scala Fri Apr 16 15:49:46 2010 +0200
@@ -162,6 +162,7 @@
/* jvm_path */
private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
+ private val Named_Root = new Regex("//+([^/]*)(.*)")
def jvm_path(posix_path: String): String =
if (Platform.is_windows) {
@@ -171,6 +172,11 @@
case Cygdrive(drive, rest) =>
result_path ++= (drive + ":" + File.separator)
rest
+ case Named_Root(root, rest) =>
+ result_path ++= File.separator
+ result_path ++= File.separator
+ result_path ++= root
+ rest
case path if path.startsWith("/") =>
result_path ++= platform_root
path
--- a/src/Pure/Thy/thy_output.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Apr 16 15:49:46 2010 +0200
@@ -599,7 +599,7 @@
val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
-val _ = ml_text "ML_functor" (K ""); (*no check!*)
+val _ = ml_text "ML_functor" (fn txt => "ML_Env.check_functor " ^ ML_Syntax.print_string txt);
val _ = ml_text "ML_text" (K "");
end;
--- a/src/Pure/sign.ML Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Pure/sign.ML Fri Apr 16 15:49:46 2010 +0200
@@ -346,15 +346,12 @@
(* add type constructors *)
-val type_syntax = Syntax.mark_type oo full_name;
+fun type_syntax thy (b, n, mx) = (Syntax.mark_type (full_name thy b), Syntax.make_type n, mx);
fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' =
- Syntax.update_type_gram true Syntax.mode_default
- (map (fn (a, n, mx) => (type_syntax thy a, Syntax.make_type n, mx)) types) syn;
- val decls = map (fn (a, n, _) => (a, n)) types;
- val tsig' = fold (Type.add_type naming) decls tsig;
+ val syn' = Syntax.update_type_gram true Syntax.mode_default (map (type_syntax thy) types) syn;
+ val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
in (naming, syn', tsig', consts) end);
@@ -373,9 +370,8 @@
let
val ctxt = ProofContext.init thy;
val syn' =
- Syntax.update_type_gram true Syntax.mode_default
- [(type_syntax thy b, Syntax.make_type (length vs), mx)] syn;
- val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
+ Syntax.update_type_gram true Syntax.mode_default [type_syntax thy (b, length vs, mx)] syn;
+ val abbr = (b, vs, parse_typ ctxt rhs)
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
val tsig' = Type.add_abbrev naming abbr tsig;
in (naming, syn', tsig', consts) end);
--- a/src/Tools/jEdit/README_BUILD Fri Apr 16 15:49:13 2010 +0200
+++ b/src/Tools/jEdit/README_BUILD Fri Apr 16 15:49:46 2010 +0200
@@ -15,9 +15,6 @@
* jEdit 4.3.1 (final)
http://www.jedit.org/
-
-
-
Netbeans Project "jEdit": install official sources as ./contrib/jEdit/.
* jEdit plugins: