# HG changeset patch
# User nipkow
# Date 1402322910 -7200
# Node ID 159e1b0434959529281b43d730181900ce9cfd45
# Parent  4cf607675df8190b2d4975a25642ed5d63e185db
added List.union

diff -r 4cf607675df8 -r 159e1b043495 src/HOL/List.thy
--- 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)"