# HG changeset patch # User blanchet # Date 1407406661 -7200 # Node ID d8bbb97689d3d2235ba51d8005e1d2e538f5a8d8 # Parent f97643a566153b6c01d773d931987f8ffc241ddd no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property diff -r f97643a56615 -r d8bbb97689d3 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Thu Aug 07 12:17:41 2014 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Thu Aug 07 12:17:41 2014 +0200 @@ -2052,7 +2052,7 @@ let ?v = "Neg e" have vb: "?v \ set (\ (Gt (CN 0 c e)))" by simp - from 7(5)[simplified simp_thms Inum.simps \.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] + from 7(5)[simplified simp_thms Inum.simps \.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] have nob: "\ (\j\ {1 ..d}. x = - ?e + j)" by auto from H p have "x + ?e > 0 \ x + ?e \ d" @@ -2085,7 +2085,7 @@ let ?v = "Sub (C -1) e" have vb: "?v \ set (\ (Ge (CN 0 c e)))" by simp - from 8(5)[simplified simp_thms Inum.simps \.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] + from 8(5)[simplified simp_thms Inum.simps \.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] have nob: "\ (\j\ {1 ..d}. x = - ?e - 1 + j)" by auto from H p have "x + ?e \ 0 \ x + ?e < d" diff -r f97643a56615 -r d8bbb97689d3 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Thu Aug 07 12:17:41 2014 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Aug 07 12:17:41 2014 +0200 @@ -2612,7 +2612,7 @@ {assume H: "\ real (x-d) + ?e > 0" let ?v="Neg e" have vb: "?v \ set (\ (Gt (CN 0 c e)))" by simp - from 7(5)[simplified simp_thms Inum.simps \.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] + from 7(5)[simplified simp_thms Inum.simps \.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] have nob: "\ (\ j\ {1 ..d}. real x = - ?e + real j)" by auto from H p have "real x + ?e > 0 \ real x + ?e \ real d" by (simp add: c1) hence "real (x + floor ?e) > real (0::int) \ real (x + floor ?e) \ real d" @@ -2638,7 +2638,7 @@ {assume H: "\ real (x-d) + ?e \ 0" let ?v="Sub (C -1) e" have vb: "?v \ set (\ (Ge (CN 0 c e)))" by simp - from 8(5)[simplified simp_thms Inum.simps \.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] + from 8(5)[simplified simp_thms Inum.simps \.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] have nob: "\ (\ j\ {1 ..d}. real x = - ?e - 1 + real j)" by auto from H p have "real x + ?e \ 0 \ real x + ?e < real d" by (simp add: c1) hence "real (x + floor ?e) \ real (0::int) \ real (x + floor ?e) < real d" @@ -3394,7 +3394,7 @@ ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). {(p,0,Floor s)})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). (?f(p,n,s)) ` {n .. 0})))" - by (simp only: set_map set_upto set_simps) + by (simp only: set_map set_upto list.set) also have "\ = ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). {(p,0,Floor s)})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {0 .. n}})) Un @@ -3548,7 +3548,7 @@ ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). {(p,0,Floor s)})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). (?f(p,n,s)) ` {n .. 0})))" - by (simp only: set_map set_upto set_simps) + by (simp only: set_map set_upto list.set) also have "\ = ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). {(p,0,Floor s)})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {0 .. n}})) Un diff -r f97643a56615 -r d8bbb97689d3 src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Aug 07 12:17:41 2014 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Aug 07 12:17:41 2014 +0200 @@ -642,7 +642,7 @@ with init all_ref_present have q_is_new: "q \ set (p#refs)" by (auto elim!: effect_refE intro!: Ref.noteq_I) from refs_of_p refs_of_q q_is_new have a3: "\qrs prs. refs_of' h2 q qrs \ refs_of' h2 p prs \ set prs \ set qrs = {}" - by (fastforce simp only: set_simps dest: refs_of'_is_fun) + by (fastforce simp only: list.set dest: refs_of'_is_fun) from rev'_invariant [OF effect_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" unfolding list_of'_def by auto with lookup show ?thesis diff -r f97643a56615 -r d8bbb97689d3 src/HOL/Library/Permutation.thy --- a/src/HOL/Library/Permutation.thy Thu Aug 07 12:17:41 2014 +0200 +++ b/src/HOL/Library/Permutation.thy Thu Aug 07 12:17:41 2014 +0200 @@ -162,7 +162,7 @@ apply (case_tac "remdups xs") apply simp_all apply (subgoal_tac "a \ set (remdups ys)") - prefer 2 apply (metis set_simps(2) insert_iff set_remdups) + prefer 2 apply (metis list.set(2) insert_iff set_remdups) apply (drule split_list) apply (elim exE conjE) apply (drule_tac x = list in spec) apply (erule impE) prefer 2 apply (drule_tac x = "ysa @ zs" in spec) apply (erule impE) prefer 2 diff -r f97643a56615 -r d8bbb97689d3 src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Thu Aug 07 12:17:41 2014 +0200 +++ b/src/HOL/Library/RBT_Set.thy Thu Aug 07 12:17:41 2014 +0200 @@ -522,7 +522,7 @@ code_datatype Set Coset -declare set_simps[code] +declare list.set[code] (* needed? *) lemma empty_Set [code]: "Set.empty = Set RBT.empty" diff -r f97643a56615 -r d8bbb97689d3 src/HOL/List.thy --- a/src/HOL/List.thy Thu Aug 07 12:17:41 2014 +0200 +++ b/src/HOL/List.thy Thu Aug 07 12:17:41 2014 +0200 @@ -39,6 +39,8 @@ setup {* Sign.parent_path *} +lemmas set_simps = list.set (* legacy *) + syntax -- {* list Enumeration *} "_list" :: "args => 'a list" ("[(_)]") @@ -54,16 +56,9 @@ "last (x # xs) = (if xs = [] then x else last xs)" primrec butlast :: "'a list \ 'a list" where -"butlast []= []" | +"butlast [] = []" | "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)" -declare list.set[simp del, code del] - -lemma set_simps[simp, code, code_post]: - "set [] = {}" - "set (x # xs) = insert x (set xs)" -by (simp_all add: list.set) - lemma set_rec: "set xs = rec_list {} (\x _. insert x) xs" by (induct xs) auto @@ -575,7 +570,7 @@ fun simproc ctxt redex = let - val set_Nil_I = @{thm trans} OF [@{thm set_simps(1)}, @{thm empty_def}] + val set_Nil_I = @{thm trans} OF [@{thm list.set(1)}, @{thm empty_def}] val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp} val del_refl_eq = @{lemma "(t = t & P) == P" by simp} @@ -1255,6 +1250,8 @@ subsubsection {* @{const set} *} +declare list.set[code_post] --"pretty output" + lemma finite_set [iff]: "finite (set xs)" by (induct xs) auto @@ -1404,7 +1401,7 @@ lemma finite_list: "finite A ==> EX xs. set xs = A" - by (erule finite_induct) (auto simp add: set_simps(2) [symmetric] simp del: set_simps(2)) + by (erule finite_induct) (auto simp add: list.set(2)[symmetric] simp del: list.set(2)) lemma card_length: "card (set xs) \ length xs" by (induct xs) (auto simp add: card_insert_if) diff -r f97643a56615 -r d8bbb97689d3 src/HOL/MicroJava/Comp/CorrCompTp.thy --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Aug 07 12:17:41 2014 +0200 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Aug 07 12:17:41 2014 +0200 @@ -1392,7 +1392,7 @@ apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append) apply (rule max_of_list_sublist) - apply (simp (no_asm_simp) only: set_append set_simps list.map) apply blast + apply (simp (no_asm_simp) only: set_append list.set list.map) apply blast apply (simp (no_asm_simp)) apply simp (* subgoal bc3 = [] *) apply (simp add: comb_nil_def) (* subgoal mt3 = [] \ sttp2 = sttp3 *) @@ -1419,7 +1419,7 @@ (* (some) preconditions of wt_instr_offset *) apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append) apply (rule max_of_list_sublist) - apply (simp (no_asm_simp) only: set_append set_simps list.map) apply blast + apply (simp (no_asm_simp) only: set_append list.set list.map) apply blast apply (simp (no_asm_simp)) apply (drule_tac x=sttp2 in spec, simp) (* subgoal \mt3_rest. \ *) diff -r f97643a56615 -r d8bbb97689d3 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Thu Aug 07 12:17:41 2014 +0200 +++ b/src/HOL/Quotient_Examples/FSet.thy Thu Aug 07 12:17:41 2014 +0200 @@ -985,7 +985,7 @@ have b: "\x' ys'. \\ List.member ys' x'; a # xs \ x' # ys'\ \ thesis" by fact have c: "xs = [] \ thesis" using b apply(simp) - by (metis List.set_simps(1) emptyE empty_subsetI) + by (metis list.set(1) emptyE empty_subsetI) have "\x ys. \\ List.member ys x; xs \ x # ys\ \ thesis" proof - fix x :: 'a diff -r f97643a56615 -r d8bbb97689d3 src/HOL/Quotient_Examples/Lift_FSet.thy --- a/src/HOL/Quotient_Examples/Lift_FSet.thy Thu Aug 07 12:17:41 2014 +0200 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Thu Aug 07 12:17:41 2014 +0200 @@ -151,7 +151,7 @@ using filter_filter [Transfer.transferred] . lemma "fset (fcons x xs) = insert x (fset xs)" - using set_simps(2) [Transfer.transferred] . + using list.set(2) [Transfer.transferred] . lemma "fset (fappend xs ys) = fset xs \ fset ys" using set_append [Transfer.transferred] .