no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
authorblanchet
Thu Aug 07 12:17:41 2014 +0200 (2014-08-07)
changeset 57816d8bbb97689d3
parent 57815 f97643a56615
child 57817 dfebc374bd89
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/RBT_Set.thy
src/HOL/List.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/Lift_FSet.thy
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 07 12:17:41 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 07 12:17:41 2014 +0200
     1.3 @@ -2052,7 +2052,7 @@
     1.4      let ?v = "Neg e"
     1.5      have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))"
     1.6        by simp
     1.7 -    from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
     1.8 +    from 7(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
     1.9      have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)"
    1.10        by auto
    1.11      from H p have "x + ?e > 0 \<and> x + ?e \<le> d"
    1.12 @@ -2085,7 +2085,7 @@
    1.13      let ?v = "Sub (C -1) e"
    1.14      have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))"
    1.15        by simp
    1.16 -    from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
    1.17 +    from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
    1.18      have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e - 1 + j)"
    1.19        by auto
    1.20      from H p have "x + ?e \<ge> 0 \<and> x + ?e < d"
     2.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Aug 07 12:17:41 2014 +0200
     2.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Aug 07 12:17:41 2014 +0200
     2.3 @@ -2612,7 +2612,7 @@
     2.4      {assume H: "\<not> real (x-d) + ?e > 0" 
     2.5        let ?v="Neg e"
     2.6        have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
     2.7 -      from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 
     2.8 +      from 7(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 
     2.9        have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x =  - ?e + real j)" by auto 
    2.10        from H p have "real x + ?e > 0 \<and> real x + ?e \<le> real d" by (simp add: c1)
    2.11        hence "real (x + floor ?e) > real (0::int) \<and> real (x + floor ?e) \<le> real d"
    2.12 @@ -2638,7 +2638,7 @@
    2.13      {assume H: "\<not> real (x-d) + ?e \<ge> 0" 
    2.14        let ?v="Sub (C -1) e"
    2.15        have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
    2.16 -      from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 
    2.17 +      from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]] 
    2.18        have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x =  - ?e - 1 + real j)" by auto 
    2.19        from H p have "real x + ?e \<ge> 0 \<and> real x + ?e < real d" by (simp add: c1)
    2.20        hence "real (x + floor ?e) \<ge> real (0::int) \<and> real (x + floor ?e) < real d"
    2.21 @@ -3394,7 +3394,7 @@
    2.22      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
    2.23      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un 
    2.24      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {n .. 0})))"
    2.25 -    by (simp only: set_map set_upto set_simps)
    2.26 +    by (simp only: set_map set_upto list.set)
    2.27    also have "\<dots> =   
    2.28      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
    2.29      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un 
    2.30 @@ -3548,7 +3548,7 @@
    2.31      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
    2.32      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un 
    2.33      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {n .. 0})))"
    2.34 -    by (simp only: set_map set_upto set_simps)
    2.35 +    by (simp only: set_map set_upto list.set)
    2.36    also have "\<dots> =   
    2.37      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
    2.38      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un 
     3.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Aug 07 12:17:41 2014 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Aug 07 12:17:41 2014 +0200
     3.3 @@ -642,7 +642,7 @@
     3.4    with init all_ref_present have q_is_new: "q \<notin> set (p#refs)"
     3.5      by (auto elim!: effect_refE intro!: Ref.noteq_I)
     3.6    from refs_of_p refs_of_q q_is_new have a3: "\<forall>qrs prs. refs_of' h2 q qrs \<and> refs_of' h2 p prs \<longrightarrow> set prs \<inter> set qrs = {}"
     3.7 -    by (fastforce simp only: set_simps dest: refs_of'_is_fun)
     3.8 +    by (fastforce simp only: list.set dest: refs_of'_is_fun)
     3.9    from rev'_invariant [OF effect_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" 
    3.10      unfolding list_of'_def by auto
    3.11    with lookup show ?thesis
     4.1 --- a/src/HOL/Library/Permutation.thy	Thu Aug 07 12:17:41 2014 +0200
     4.2 +++ b/src/HOL/Library/Permutation.thy	Thu Aug 07 12:17:41 2014 +0200
     4.3 @@ -162,7 +162,7 @@
     4.4    apply (case_tac "remdups xs")
     4.5     apply simp_all
     4.6    apply (subgoal_tac "a \<in> set (remdups ys)")
     4.7 -   prefer 2 apply (metis set_simps(2) insert_iff set_remdups)
     4.8 +   prefer 2 apply (metis list.set(2) insert_iff set_remdups)
     4.9    apply (drule split_list) apply (elim exE conjE)
    4.10    apply (drule_tac x = list in spec) apply (erule impE) prefer 2
    4.11     apply (drule_tac x = "ysa @ zs" in spec) apply (erule impE) prefer 2
     5.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Aug 07 12:17:41 2014 +0200
     5.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Aug 07 12:17:41 2014 +0200
     5.3 @@ -522,7 +522,7 @@
     5.4  
     5.5  code_datatype Set Coset
     5.6  
     5.7 -declare set_simps[code]
     5.8 +declare list.set[code] (* needed? *)
     5.9  
    5.10  lemma empty_Set [code]:
    5.11    "Set.empty = Set RBT.empty"
     6.1 --- a/src/HOL/List.thy	Thu Aug 07 12:17:41 2014 +0200
     6.2 +++ b/src/HOL/List.thy	Thu Aug 07 12:17:41 2014 +0200
     6.3 @@ -39,6 +39,8 @@
     6.4  
     6.5  setup {* Sign.parent_path *}
     6.6  
     6.7 +lemmas set_simps = list.set (* legacy *)
     6.8 +
     6.9  syntax
    6.10    -- {* list Enumeration *}
    6.11    "_list" :: "args => 'a list"    ("[(_)]")
    6.12 @@ -54,16 +56,9 @@
    6.13  "last (x # xs) = (if xs = [] then x else last xs)"
    6.14  
    6.15  primrec butlast :: "'a list \<Rightarrow> 'a list" where
    6.16 -"butlast []= []" |
    6.17 +"butlast [] = []" |
    6.18  "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
    6.19  
    6.20 -declare list.set[simp del, code del]
    6.21 -
    6.22 -lemma set_simps[simp, code, code_post]:
    6.23 -  "set [] = {}"
    6.24 -  "set (x # xs) = insert x (set xs)"
    6.25 -by (simp_all add: list.set)
    6.26 -
    6.27  lemma set_rec: "set xs = rec_list {} (\<lambda>x _. insert x) xs"
    6.28    by (induct xs) auto
    6.29  
    6.30 @@ -575,7 +570,7 @@
    6.31  
    6.32  fun simproc ctxt redex =
    6.33    let
    6.34 -    val set_Nil_I = @{thm trans} OF [@{thm set_simps(1)}, @{thm empty_def}]
    6.35 +    val set_Nil_I = @{thm trans} OF [@{thm list.set(1)}, @{thm empty_def}]
    6.36      val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
    6.37      val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
    6.38      val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
    6.39 @@ -1255,6 +1250,8 @@
    6.40  
    6.41  subsubsection {* @{const set} *}
    6.42  
    6.43 +declare list.set[code_post]  --"pretty output"
    6.44 +
    6.45  lemma finite_set [iff]: "finite (set xs)"
    6.46  by (induct xs) auto
    6.47  
    6.48 @@ -1404,7 +1401,7 @@
    6.49  
    6.50  
    6.51  lemma finite_list: "finite A ==> EX xs. set xs = A"
    6.52 -  by (erule finite_induct) (auto simp add: set_simps(2) [symmetric] simp del: set_simps(2))
    6.53 +  by (erule finite_induct) (auto simp add: list.set(2)[symmetric] simp del: list.set(2))
    6.54  
    6.55  lemma card_length: "card (set xs) \<le> length xs"
    6.56  by (induct xs) (auto simp add: card_insert_if)
     7.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Aug 07 12:17:41 2014 +0200
     7.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Aug 07 12:17:41 2014 +0200
     7.3 @@ -1392,7 +1392,7 @@
     7.4  
     7.5    apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
     7.6      apply (rule max_of_list_sublist)
     7.7 -    apply (simp (no_asm_simp) only: set_append set_simps list.map) apply blast
     7.8 +    apply (simp (no_asm_simp) only: set_append list.set list.map) apply blast
     7.9    apply (simp (no_asm_simp))
    7.10    apply simp                    (* subgoal bc3 = [] *)
    7.11    apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
    7.12 @@ -1419,7 +1419,7 @@
    7.13       (* (some) preconditions of  wt_instr_offset *)
    7.14    apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
    7.15    apply (rule max_of_list_sublist)
    7.16 -    apply (simp (no_asm_simp) only: set_append set_simps list.map) apply blast
    7.17 +    apply (simp (no_asm_simp) only: set_append list.set list.map) apply blast
    7.18    apply (simp (no_asm_simp))
    7.19  
    7.20  apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)
     8.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Thu Aug 07 12:17:41 2014 +0200
     8.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Thu Aug 07 12:17:41 2014 +0200
     8.3 @@ -985,7 +985,7 @@
     8.4    have b: "\<And>x' ys'. \<lbrakk>\<not> List.member ys' x'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
     8.5    have c: "xs = [] \<Longrightarrow> thesis" using b 
     8.6      apply(simp)
     8.7 -    by (metis List.set_simps(1) emptyE empty_subsetI)
     8.8 +    by (metis list.set(1) emptyE empty_subsetI)
     8.9    have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
    8.10    proof -
    8.11      fix x :: 'a
     9.1 --- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Thu Aug 07 12:17:41 2014 +0200
     9.2 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Thu Aug 07 12:17:41 2014 +0200
     9.3 @@ -151,7 +151,7 @@
     9.4    using filter_filter [Transfer.transferred] .
     9.5  
     9.6  lemma "fset (fcons x xs) = insert x (fset xs)"
     9.7 -  using set_simps(2) [Transfer.transferred] .
     9.8 +  using list.set(2) [Transfer.transferred] .
     9.9  
    9.10  lemma "fset (fappend xs ys) = fset xs \<union> fset ys"
    9.11    using set_append [Transfer.transferred] .