--- a/src/HOL/List.thy Mon Jun 09 12:36:22 2014 +0200
+++ b/src/HOL/List.thy Mon Jun 09 16:08:30 2014 +0200
@@ -174,8 +174,11 @@
definition insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"insert x xs = (if x \<in> set xs then xs else x # xs)"
-hide_const (open) insert
-hide_fact (open) insert_def
+definition union :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"union = fold insert"
+
+hide_const (open) insert union
+hide_fact (open) insert_def union_def
primrec find :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" where
"find _ [] = None" |
@@ -295,6 +298,7 @@
@{lemma "remdups_adj [2,2,3,1,1::nat,2,1] = [2,3,1,2,1]" by simp}\\
@{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\
@{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\
+@{lemma "List.union [2,3,4] [0::int,1,2] = [4,3,0,1,2]" by (simp add: List.insert_def List.union_def)}\\
@{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\
@{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\
@{lemma "List.extract (%i::int. i>0) [0,0] = None" by(simp add: extract_def)}\\
@@ -3611,7 +3615,7 @@
by (auto simp add: List.insert_def)
lemma distinct_insert [simp]:
- "distinct xs \<Longrightarrow> distinct (List.insert x xs)"
+ "distinct (List.insert x xs) = distinct xs"
by (simp add: List.insert_def)
lemma insert_remdups:
@@ -3619,6 +3623,18 @@
by (simp add: List.insert_def)
+subsubsection {* @{const List.union} *}
+
+text{* This is all one should need to know about union: *}
+lemma set_union[simp]: "set (List.union xs ys) = set xs \<union> set ys"
+unfolding List.union_def
+by(induct xs arbitrary: ys) simp_all
+
+lemma distinct_union[simp]: "distinct(List.union xs ys) = distinct ys"
+unfolding List.union_def
+by(induct xs arbitrary: ys) simp_all
+
+
subsubsection {* @{const List.find} *}
lemma find_None_iff: "List.find P xs = None \<longleftrightarrow> \<not> (\<exists>x. x \<in> set xs \<and> P x)"