# HG changeset patch # User blanchet # Date 1392823957 -3600 # Node ID a879f14b6f955e533f2ece9602324495ff5899f2 # Parent a0134252ac29d17d4717e197efbbfc5b86362b2c merged 'List.set' with BNF-generated 'set' diff -r a0134252ac29 -r a879f14b6f95 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Wed Feb 19 22:02:23 2014 +1100 +++ b/src/HOL/Decision_Procs/Cooper.thy Wed Feb 19 16:32:37 2014 +0100 @@ -1674,7 +1674,7 @@ {assume H: "\ (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'="x" and bs="bs"]] + 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"]] have nob: "\ (\j\ {1 ..d}. x = - ?e + j)" by auto from H p have "x + ?e > 0 \ x + ?e \ d" by (simp add: c1) hence "x + ?e \ 1 \ x + ?e \ d" by simp @@ -1694,7 +1694,7 @@ {assume H: "\ (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'="x" and bs="bs"]] + 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"]] have nob: "\ (\j\ {1 ..d}. x = - ?e - 1 + j)" by auto from H p have "x + ?e \ 0 \ x + ?e < d" by (simp add: c1) hence "x + ?e +1 \ 1 \ x + ?e + 1 \ d" by simp diff -r a0134252ac29 -r a879f14b6f95 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Wed Feb 19 22:02:23 2014 +1100 +++ b/src/HOL/Decision_Procs/MIR.thy Wed Feb 19 16:32:37 2014 +0100 @@ -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 set_simps 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 set_simps 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 set_simps) 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 set_simps) 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 a0134252ac29 -r a879f14b6f95 src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Feb 19 22:02:23 2014 +1100 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Feb 19 16:32:37 2014 +0100 @@ -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: set_simps 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 a0134252ac29 -r a879f14b6f95 src/HOL/Library/Permutation.thy --- a/src/HOL/Library/Permutation.thy Wed Feb 19 22:02:23 2014 +1100 +++ b/src/HOL/Library/Permutation.thy Wed Feb 19 16:32:37 2014 +0100 @@ -157,7 +157,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 set_simps(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 a0134252ac29 -r a879f14b6f95 src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Wed Feb 19 22:02:23 2014 +1100 +++ b/src/HOL/Library/RBT_Set.thy Wed Feb 19 16:32:37 2014 +0100 @@ -520,7 +520,7 @@ code_datatype Set Coset -declare set.simps[code] +declare set_simps[code] lemma empty_Set [code]: "Set.empty = Set RBT.empty" diff -r a0134252ac29 -r a879f14b6f95 src/HOL/List.thy --- a/src/HOL/List.thy Wed Feb 19 22:02:23 2014 +1100 +++ b/src/HOL/List.thy Wed Feb 19 16:32:37 2014 +0100 @@ -8,7 +8,7 @@ imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product begin -datatype_new 'a list (map: map rel: list_all2) = +datatype_new (set: 'a) list (map: map rel: list_all2) = =: Nil (defaults tl: "[]") ("[]") | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65) datatype_compat list @@ -51,9 +51,15 @@ "butlast []= []" | "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)" -primrec set :: "'a list \ 'a set" where -"set [] = {}" | -"set (x # xs) = insert x (set 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 definition coset :: "'a list \ 'a set" where [simp]: "coset xs = - set xs" @@ -548,7 +554,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 set_simps(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} @@ -1214,8 +1220,6 @@ subsubsection {* @{const set} *} -declare set.simps [code_post] --"pretty output" - lemma finite_set [iff]: "finite (set xs)" by (induct xs) auto @@ -1284,7 +1288,7 @@ case (snoc a xs) show ?case proof cases - assume "x = a" thus ?case using snoc by (metis List.set.simps(1) emptyE) + assume "x = a" thus ?case using snoc by (metis set_simps(1) emptyE) next assume "x \ a" thus ?case using snoc by fastforce qed @@ -1363,8 +1367,7 @@ by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 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: set_simps(2) [symmetric] simp del: set_simps(2)) lemma card_length: "card (set xs) \ length xs" by (induct xs) (auto simp add: card_insert_if) @@ -6693,7 +6696,7 @@ lemma set_transfer [transfer_rule]: "(list_all2 A ===> set_rel A) set set" - unfolding set_def by transfer_prover + unfolding set_rec[abs_def] by transfer_prover lemma map_rec: "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs" by (induct xs) auto diff -r a0134252ac29 -r a879f14b6f95 src/HOL/MicroJava/Comp/CorrCompTp.thy --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Feb 19 22:02:23 2014 +1100 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Feb 19 16:32:37 2014 +0100 @@ -1394,7 +1394,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 set_simps list.map) apply blast apply (simp (no_asm_simp)) apply simp (* subgoal bc3 = [] *) apply (simp add: comb_nil_def) (* subgoal mt3 = [] \ sttp2 = sttp3 *) @@ -1421,7 +1421,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 set_simps list.map) apply blast apply (simp (no_asm_simp)) apply (drule_tac x=sttp2 in spec, simp) (* subgoal \mt3_rest. \ *) diff -r a0134252ac29 -r a879f14b6f95 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Wed Feb 19 22:02:23 2014 +1100 +++ b/src/HOL/Quotient_Examples/FSet.thy Wed Feb 19 16:32:37 2014 +0100 @@ -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_simps(1) emptyE empty_subsetI) have "\x ys. \\ List.member ys x; xs \ x # ys\ \ thesis" proof - fix x :: 'a diff -r a0134252ac29 -r a879f14b6f95 src/HOL/Quotient_Examples/Lift_FSet.thy --- a/src/HOL/Quotient_Examples/Lift_FSet.thy Wed Feb 19 22:02:23 2014 +1100 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Wed Feb 19 16:32:37 2014 +0100 @@ -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 set_simps(2) [Transfer.transferred] . lemma "fset (fappend xs ys) = fset xs \ fset ys" using set_append [Transfer.transferred] . diff -r a0134252ac29 -r a879f14b6f95 src/HOL/Quotient_Examples/Lift_Set.thy --- a/src/HOL/Quotient_Examples/Lift_Set.thy Wed Feb 19 22:02:23 2014 +1100 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy Wed Feb 19 16:32:37 2014 +0100 @@ -12,18 +12,18 @@ typedef 'a set = "set :: ('a \ bool) set" morphisms member Set - unfolding set_def by auto + unfolding set_def by (rule UNIV_witness) setup_lifting type_definition_set[unfolded set_def] text {* Now, we can employ lift_definition to lift definitions. *} -lift_definition empty :: "'a set" is "bot :: 'a \ bool" done +lift_definition empty :: "'a set" is "bot :: 'a \ bool" . term "Lift_Set.empty" thm Lift_Set.empty_def -lift_definition insert :: "'a => 'a set => 'a set" is "\ x P y. y = x \ P y" done +lift_definition insert :: "'a => 'a set => 'a set" is "\ x P y. y = x \ P y" . term "Lift_Set.insert" thm Lift_Set.insert_def @@ -31,4 +31,3 @@ export_code empty insert in SML end -