author nipkow Tue, 22 Sep 2015 17:13:01 +0200 changeset 61229 0b9c45c4af29 parent 61225 1a690dce8cfc child 61230 e367b93f78e5
unified isin-proofs
```--- a/src/HOL/Data_Structures/Isin2.thy	Tue Sep 22 14:31:22 2015 +0200
+++ b/src/HOL/Data_Structures/Isin2.thy	Tue Sep 22 17:13:01 2015 +0200
@@ -13,9 +13,9 @@
"isin (Node _ l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)"

lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
-by (induction t) (auto simp: elems_simps)
+by (induction t) (auto simp: elems_simps1)

lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
-by (induction t) (auto simp: elems_simps dest: sortedD)
+by (induction t) (auto simp: elems_simps2)

end
\ No newline at end of file```
```--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Tue Sep 22 14:31:22 2015 +0200
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Tue Sep 22 17:13:01 2015 +0200
@@ -26,15 +26,26 @@
"sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> elems xs. y < x))"
by(simp add: elems_eq_set Sorted_Less.sorted_snoc_iff)

+text{* The above two rules introduce quantifiers. It turns out
+that in practice this is not a problem because of the simplicity of
+the "isin" functions that implement @{const elems}. Nevertheless
+it is possible to avoid the quantifiers with the help of some rewrite rules: *}
+
lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> y < x"
by (simp add: sorted_Cons_iff)

lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> x < y"
by (simp add: sorted_snoc_iff)

-lemmas elems_simps0 = sorted_lems elems_app
-lemmas elems_simps = elems_simps0 sorted_Cons_iff sorted_snoc_iff
-lemmas sortedD = sorted_ConsD sorted_snocD
+lemma sorted_ConsD2: "sorted (y # xs) \<Longrightarrow> x \<le> y \<Longrightarrow> x \<notin> elems xs"
+using leD sorted_ConsD by blast
+
+lemma sorted_snocD2: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> x \<notin> elems xs"
+using leD sorted_snocD by blast
+
+lemmas elems_simps = sorted_lems elems_app
+lemmas elems_simps1 = elems_simps sorted_Cons_iff sorted_snoc_iff
+lemmas elems_simps2 = elems_simps sorted_ConsD sorted_snocD sorted_ConsD2 sorted_snocD2

subsection \<open>Inserting into an ordered list without duplicates:\<close>```
```--- a/src/HOL/Data_Structures/Tree_Set.thy	Tue Sep 22 14:31:22 2015 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Tue Sep 22 17:13:01 2015 +0200
@@ -35,10 +35,10 @@
subsection "Functional Correctness Proofs"

lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps)
+by (induction t) (auto simp: elems_simps1)

lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps0 dest: sortedD)
+by (induction t) (auto simp: elems_simps2)

lemma inorder_insert:```