merged
authornipkow
Fri Mar 23 11:39:41 2018 +0100 (14 months ago)
changeset 679307dff1186daf3
parent 67928 7f5b1b6f7f40
parent 67929 30486b96274d
child 67931 f7917c15b566
merged
     1.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Fri Mar 23 10:52:00 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Fri Mar 23 11:39:41 2018 +0100
     1.3 @@ -150,13 +150,9 @@
     1.4  
     1.5  subsubsection "Proofs for isin"
     1.6  
     1.7 -lemma
     1.8 -  "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
     1.9 -by(induction h arbitrary: t) (fastforce simp: elems_simps1 split: if_splits)+
    1.10 -
    1.11 -lemma isin_set: "t \<in> T h \<Longrightarrow>
    1.12 -  sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
    1.13 -by(induction h arbitrary: t) (auto simp: elems_simps2 split: if_splits)
    1.14 +lemma isin_set:
    1.15 +  "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))"
    1.16 +by(induction h arbitrary: t) (fastforce simp: isin_simps split: if_splits)+
    1.17  
    1.18  subsubsection "Proofs for insertion"
    1.19  
     2.1 --- a/src/HOL/Data_Structures/Isin2.thy	Fri Mar 23 10:52:00 2018 +0100
     2.2 +++ b/src/HOL/Data_Structures/Isin2.thy	Fri Mar 23 11:39:41 2018 +0100
     2.3 @@ -17,10 +17,7 @@
     2.4       EQ \<Rightarrow> True |
     2.5       GT \<Rightarrow> isin r x)"
     2.6  
     2.7 -lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
     2.8 -by (induction t) (auto simp: elems_simps1)
     2.9 -
    2.10 -lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
    2.11 -by (induction t) (auto simp: elems_simps2)
    2.12 +lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))"
    2.13 +by (induction t) (auto simp: isin_simps)
    2.14  
    2.15  end
     3.1 --- a/src/HOL/Data_Structures/List_Ins_Del.thy	Fri Mar 23 10:52:00 2018 +0100
     3.2 +++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Fri Mar 23 11:39:41 2018 +0100
     3.3 @@ -8,38 +8,29 @@
     3.4  
     3.5  subsection \<open>Elements in a list\<close>
     3.6  
     3.7 -fun elems :: "'a list \<Rightarrow> 'a set" where
     3.8 -"elems [] = {}" |
     3.9 -"elems (x#xs) = Set.insert x (elems xs)"
    3.10 -
    3.11 -lemma elems_app: "elems (xs @ ys) = (elems xs \<union> elems ys)"
    3.12 -by (induction xs) auto
    3.13 -
    3.14 -lemma elems_eq_set: "elems xs = set xs"
    3.15 -by (induction xs) auto
    3.16 -
    3.17  lemma sorted_Cons_iff:
    3.18 -  "sorted(x # xs) = ((\<forall>y \<in> elems xs. x < y) \<and> sorted xs)"
    3.19 -by(simp add: elems_eq_set sorted_wrt_Cons)
    3.20 +  "sorted(x # xs) = ((\<forall>y \<in> set xs. x < y) \<and> sorted xs)"
    3.21 +by(simp add: sorted_wrt_Cons)
    3.22  
    3.23  lemma sorted_snoc_iff:
    3.24 -  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> elems xs. y < x))"
    3.25 -by(simp add: elems_eq_set sorted_wrt_append)
    3.26 -
    3.27 +  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> set xs. y < x))"
    3.28 +by(simp add: sorted_wrt_append)
    3.29 +(*
    3.30  text\<open>The above two rules introduce quantifiers. It turns out
    3.31  that in practice this is not a problem because of the simplicity of
    3.32 -the "isin" functions that implement @{const elems}. Nevertheless
    3.33 +the "isin" functions that implement @{const set}. Nevertheless
    3.34  it is possible to avoid the quantifiers with the help of some rewrite rules:\<close>
    3.35  
    3.36 -lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<le> y \<Longrightarrow> x \<notin> elems xs"
    3.37 +lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<le> y \<Longrightarrow> x \<notin> set xs"
    3.38  by (auto simp: sorted_Cons_iff)
    3.39  
    3.40 -lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> x \<notin> elems xs"
    3.41 +lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> x \<notin> set xs"
    3.42  by (auto simp: sorted_snoc_iff)
    3.43  
    3.44 -lemmas elems_simps = sorted_lems elems_app
    3.45 -lemmas elems_simps1 = elems_simps sorted_Cons_iff sorted_snoc_iff
    3.46 -lemmas elems_simps2 = elems_simps sorted_ConsD sorted_snocD
    3.47 +lemmas isin_simps2 = sorted_lems sorted_ConsD sorted_snocD
    3.48 +*)
    3.49 +
    3.50 +lemmas isin_simps = sorted_lems sorted_Cons_iff sorted_snoc_iff
    3.51  
    3.52  
    3.53  subsection \<open>Inserting into an ordered list without duplicates:\<close>
    3.54 @@ -49,7 +40,7 @@
    3.55  "ins_list x (a#xs) =
    3.56    (if x < a then x#a#xs else if x=a then a#xs else a # ins_list x xs)"
    3.57  
    3.58 -lemma set_ins_list: "elems (ins_list x xs) = insert x (elems xs)"
    3.59 +lemma set_ins_list: "set (ins_list x xs) = insert x (set xs)"
    3.60  by(induction xs) auto
    3.61  
    3.62  lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
    3.63 @@ -93,16 +84,12 @@
    3.64  "del_list x [] = []" |
    3.65  "del_list x (a#xs) = (if x=a then xs else a # del_list x xs)"
    3.66  
    3.67 -lemma del_list_idem: "x \<notin> elems xs \<Longrightarrow> del_list x xs = xs"
    3.68 +lemma del_list_idem: "x \<notin> set xs \<Longrightarrow> del_list x xs = xs"
    3.69  by (induct xs) simp_all
    3.70  
    3.71 -lemma elems_del_list_eq:
    3.72 -  "distinct xs \<Longrightarrow> elems (del_list x xs) = elems xs - {x}"
    3.73 -apply(induct xs)
    3.74 - apply simp
    3.75 -apply (simp add: elems_eq_set)
    3.76 -apply blast
    3.77 -done
    3.78 +lemma set_del_list_eq:
    3.79 +  "distinct xs \<Longrightarrow> set (del_list x xs) = set xs - {x}"
    3.80 +by(induct xs) auto
    3.81  
    3.82  lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)"
    3.83  apply(induction xs rule: induct_list012)
    3.84 @@ -112,7 +99,7 @@
    3.85  lemma del_list_sorted: "sorted (xs @ a # ys) \<Longrightarrow>
    3.86    del_list x (xs @ a # ys) = (if x < a then del_list x xs @ a # ys else xs @ del_list x (a # ys))"
    3.87  by(induction xs)
    3.88 -  (fastforce simp: sorted_lems sorted_Cons_iff elems_eq_set intro!: del_list_idem)+
    3.89 +  (fastforce simp: sorted_lems sorted_Cons_iff intro!: del_list_idem)+
    3.90  
    3.91  text\<open>In principle, @{thm del_list_sorted} suffices, but the following
    3.92  corollaries speed up proofs.\<close>
     4.1 --- a/src/HOL/Data_Structures/Set_by_Ordered.thy	Fri Mar 23 10:52:00 2018 +0100
     4.2 +++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Fri Mar 23 11:39:41 2018 +0100
     4.3 @@ -30,7 +30,7 @@
     4.4  fixes inv :: "'t \<Rightarrow> bool"
     4.5  assumes empty: "inorder empty = []"
     4.6  assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
     4.7 -  isin t x = (x \<in> elems (inorder t))"
     4.8 +  isin t x = (x \<in> set (inorder t))"
     4.9  assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    4.10    inorder(insert x t) = ins_list x (inorder t)"
    4.11  assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
    4.12 @@ -41,7 +41,7 @@
    4.13  begin
    4.14  
    4.15  sublocale Set
    4.16 -  empty insert delete isin "elems o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
    4.17 +  empty insert delete isin "set o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
    4.18  proof(standard, goal_cases)
    4.19    case 1 show ?case by (auto simp: empty)
    4.20  next
    4.21 @@ -50,7 +50,7 @@
    4.22    case 3 thus ?case by(simp add: insert set_ins_list)
    4.23  next
    4.24    case (4 s x) thus ?case
    4.25 -    using delete[OF 4, of x] by (auto simp: distinct_if_sorted elems_del_list_eq)
    4.26 +    using delete[OF 4, of x] by (auto simp: distinct_if_sorted set_del_list_eq)
    4.27  next
    4.28    case 5 thus ?case by(simp add: empty inv_empty)
    4.29  next
     5.1 --- a/src/HOL/Data_Structures/Tree234_Set.thy	Fri Mar 23 10:52:00 2018 +0100
     5.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Fri Mar 23 11:39:41 2018 +0100
     5.3 @@ -202,11 +202,8 @@
     5.4  
     5.5  subsubsection \<open>Functional correctness of isin:\<close>
     5.6  
     5.7 -lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
     5.8 -by (induction t) (auto simp: elems_simps1 ball_Un)
     5.9 -
    5.10 -lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
    5.11 -by (induction t) (auto simp: elems_simps2 split!: if_splits)
    5.12 +lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))"
    5.13 +by (induction t) (auto simp: isin_simps ball_Un)
    5.14  
    5.15  
    5.16  subsubsection \<open>Functional correctness of insert:\<close>
     6.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Fri Mar 23 10:52:00 2018 +0100
     6.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Fri Mar 23 11:39:41 2018 +0100
     6.3 @@ -142,11 +142,8 @@
     6.4  
     6.5  subsubsection "Proofs for isin"
     6.6  
     6.7 -lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
     6.8 -by (induction t) (auto simp: elems_simps1 ball_Un)
     6.9 -
    6.10 -lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
    6.11 -by (induction t) (auto simp: elems_simps2)
    6.12 +lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))"
    6.13 +by (induction t) (auto simp: isin_simps ball_Un)
    6.14  
    6.15  
    6.16  subsubsection "Proofs for insert"
     7.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Fri Mar 23 10:52:00 2018 +0100
     7.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Fri Mar 23 11:39:41 2018 +0100
     7.3 @@ -42,12 +42,8 @@
     7.4  
     7.5  subsection "Functional Correctness Proofs"
     7.6  
     7.7 -lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
     7.8 -by (induction t) (auto simp: elems_simps1)
     7.9 -
    7.10 -lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
    7.11 -by (induction t) (auto simp: elems_simps2)
    7.12 -
    7.13 +lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))"
    7.14 +by (induction t) (auto simp: isin_simps)
    7.15  
    7.16  lemma inorder_insert:
    7.17    "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"