merged 'List.set' with BNF-generated 'set'
authorblanchet
Wed Feb 19 16:32:37 2014 +0100 (2014-02-19)
changeset 55584a879f14b6f95
parent 55583 a0134252ac29
child 55585 014138b356c4
merged 'List.set' with BNF-generated 'set'
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
src/HOL/Quotient_Examples/Lift_Set.thy
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Wed Feb 19 22:02:23 2014 +1100
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Feb 19 16:32:37 2014 +0100
     1.3 @@ -1674,7 +1674,7 @@
     1.4    {assume H: "\<not> (x-d) + ?e > 0"
     1.5      let ?v="Neg e"
     1.6      have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" 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 set_simps 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)" by auto
    1.10      from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
    1.11      hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d"  by simp
    1.12 @@ -1694,7 +1694,7 @@
    1.13      {assume H: "\<not> (x-d) + ?e \<ge> 0"
    1.14        let ?v="Sub (C -1) e"
    1.15        have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" 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 set_simps 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)" by auto
    1.19        from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
    1.20        hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"  by simp
     2.1 --- a/src/HOL/Decision_Procs/MIR.thy	Wed Feb 19 22:02:23 2014 +1100
     2.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Wed Feb 19 16:32:37 2014 +0100
     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 set_simps 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 set_simps 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 set_simps)
    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 set_simps)
    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	Wed Feb 19 22:02:23 2014 +1100
     3.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Feb 19 16:32:37 2014 +0100
     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: set_simps 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	Wed Feb 19 22:02:23 2014 +1100
     4.2 +++ b/src/HOL/Library/Permutation.thy	Wed Feb 19 16:32:37 2014 +0100
     4.3 @@ -157,7 +157,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 set_simps(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	Wed Feb 19 22:02:23 2014 +1100
     5.2 +++ b/src/HOL/Library/RBT_Set.thy	Wed Feb 19 16:32:37 2014 +0100
     5.3 @@ -520,7 +520,7 @@
     5.4  
     5.5  code_datatype Set Coset
     5.6  
     5.7 -declare set.simps[code]
     5.8 +declare set_simps[code]
     5.9  
    5.10  lemma empty_Set [code]:
    5.11    "Set.empty = Set RBT.empty"
     6.1 --- a/src/HOL/List.thy	Wed Feb 19 22:02:23 2014 +1100
     6.2 +++ b/src/HOL/List.thy	Wed Feb 19 16:32:37 2014 +0100
     6.3 @@ -8,7 +8,7 @@
     6.4  imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
     6.5  begin
     6.6  
     6.7 -datatype_new 'a list (map: map rel: list_all2) =
     6.8 +datatype_new (set: 'a) list (map: map rel: list_all2) =
     6.9      =: Nil (defaults tl: "[]")  ("[]")
    6.10    | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
    6.11  datatype_compat list
    6.12 @@ -51,9 +51,15 @@
    6.13  "butlast []= []" |
    6.14  "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
    6.15  
    6.16 -primrec set :: "'a list \<Rightarrow> 'a set" where
    6.17 -"set [] = {}" |
    6.18 -"set (x # xs) = insert x (set xs)"
    6.19 +declare list.set[simp del, code del]
    6.20 +
    6.21 +lemma set_simps[simp, code, code_post]:
    6.22 +  "set [] = {}"
    6.23 +  "set (x # xs) = insert x (set xs)"
    6.24 +by (simp_all add: list.set)
    6.25 +
    6.26 +lemma set_rec: "set xs = rec_list {} (\<lambda>x _. insert x) xs"
    6.27 +  by (induct xs) auto
    6.28  
    6.29  definition coset :: "'a list \<Rightarrow> 'a set" where
    6.30  [simp]: "coset xs = - set xs"
    6.31 @@ -548,7 +554,7 @@
    6.32  
    6.33  fun simproc ctxt redex =
    6.34    let
    6.35 -    val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
    6.36 +    val set_Nil_I = @{thm trans} OF [@{thm set_simps(1)}, @{thm empty_def}]
    6.37      val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
    6.38      val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
    6.39      val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
    6.40 @@ -1214,8 +1220,6 @@
    6.41  
    6.42  subsubsection {* @{const set} *}
    6.43  
    6.44 -declare set.simps [code_post]  --"pretty output"
    6.45 -
    6.46  lemma finite_set [iff]: "finite (set xs)"
    6.47  by (induct xs) auto
    6.48  
    6.49 @@ -1284,7 +1288,7 @@
    6.50    case (snoc a xs)
    6.51    show ?case
    6.52    proof cases
    6.53 -    assume "x = a" thus ?case using snoc by (metis List.set.simps(1) emptyE)
    6.54 +    assume "x = a" thus ?case using snoc by (metis set_simps(1) emptyE)
    6.55    next
    6.56      assume "x \<noteq> a" thus ?case using snoc by fastforce
    6.57    qed
    6.58 @@ -1363,8 +1367,7 @@
    6.59  by (metis split_list_last_prop [where P=P] in_set_conv_decomp)
    6.60  
    6.61  lemma finite_list: "finite A ==> EX xs. set xs = A"
    6.62 -  by (erule finite_induct)
    6.63 -    (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))
    6.64 +  by (erule finite_induct) (auto simp add: set_simps(2) [symmetric] simp del: set_simps(2))
    6.65  
    6.66  lemma card_length: "card (set xs) \<le> length xs"
    6.67  by (induct xs) (auto simp add: card_insert_if)
    6.68 @@ -6693,7 +6696,7 @@
    6.69  
    6.70  lemma set_transfer [transfer_rule]:
    6.71    "(list_all2 A ===> set_rel A) set set"
    6.72 -  unfolding set_def by transfer_prover
    6.73 +  unfolding set_rec[abs_def] by transfer_prover
    6.74  
    6.75  lemma map_rec: "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs"
    6.76    by (induct xs) auto
     7.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Feb 19 22:02:23 2014 +1100
     7.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Feb 19 16:32:37 2014 +0100
     7.3 @@ -1394,7 +1394,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 set_simps 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 @@ -1421,7 +1421,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 set_simps 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	Wed Feb 19 22:02:23 2014 +1100
     8.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Wed Feb 19 16:32:37 2014 +0100
     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_simps(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	Wed Feb 19 22:02:23 2014 +1100
     9.2 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Feb 19 16:32:37 2014 +0100
     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 set_simps(2) [Transfer.transferred] .
     9.9  
    9.10  lemma "fset (fappend xs ys) = fset xs \<union> fset ys"
    9.11    using set_append [Transfer.transferred] .
    10.1 --- a/src/HOL/Quotient_Examples/Lift_Set.thy	Wed Feb 19 22:02:23 2014 +1100
    10.2 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Wed Feb 19 16:32:37 2014 +0100
    10.3 @@ -12,18 +12,18 @@
    10.4  
    10.5  typedef 'a set = "set :: ('a \<Rightarrow> bool) set"
    10.6    morphisms member Set
    10.7 -  unfolding set_def by auto
    10.8 +  unfolding set_def by (rule UNIV_witness)
    10.9  
   10.10  setup_lifting type_definition_set[unfolded set_def]
   10.11  
   10.12  text {* Now, we can employ lift_definition to lift definitions. *}
   10.13  
   10.14 -lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" done
   10.15 +lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" .
   10.16  
   10.17  term "Lift_Set.empty"
   10.18  thm Lift_Set.empty_def
   10.19  
   10.20 -lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" done 
   10.21 +lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" . 
   10.22  
   10.23  term "Lift_Set.insert"
   10.24  thm Lift_Set.insert_def
   10.25 @@ -31,4 +31,3 @@
   10.26  export_code empty insert in SML
   10.27  
   10.28  end
   10.29 -