--- 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: "\<not> (x-d) + ?e > 0"
let ?v="Neg e"
have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
- 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"]]
+ 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"]]
have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)" by auto
from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d" by simp
@@ -1694,7 +1694,7 @@
{assume H: "\<not> (x-d) + ?e \<ge> 0"
let ?v="Sub (C -1) e"
have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
- 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"]]
+ 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"]]
have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e - 1 + j)" by auto
from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d" by simp
--- 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: "\<not> real (x-d) + ?e > 0"
let ?v="Neg e"
have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
- 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"]]
+ 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"]]
have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x = - ?e + real j)" by auto
from H p have "real x + ?e > 0 \<and> real x + ?e \<le> real d" by (simp add: c1)
hence "real (x + floor ?e) > real (0::int) \<and> real (x + floor ?e) \<le> real d"
@@ -2638,7 +2638,7 @@
{assume H: "\<not> real (x-d) + ?e \<ge> 0"
let ?v="Sub (C -1) e"
have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
- 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"]]
+ 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"]]
have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x = - ?e - 1 + real j)" by auto
from H p have "real x + ?e \<ge> 0 \<and> real x + ?e < real d" by (simp add: c1)
hence "real (x + floor ?e) \<ge> real (0::int) \<and> real (x + floor ?e) < real d"
@@ -3394,7 +3394,7 @@
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (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 "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
(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
@@ -3548,7 +3548,7 @@
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (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 "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
(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
--- 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 \<notin> set (p#refs)"
by (auto elim!: effect_refE intro!: Ref.noteq_I)
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 = {}"
- 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
--- 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 \<in> 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
--- 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"
--- 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 \<Rightarrow> '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 {} (\<lambda>x _. insert x) xs"
+ by (induct xs) auto
definition coset :: "'a list \<Rightarrow> '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 \<noteq> 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) \<le> 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
--- 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 = [] \<and> 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 \<exists>mt3_rest. \<dots> *)
--- 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: "\<And>x' ys'. \<lbrakk>\<not> List.member ys' x'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
have c: "xs = [] \<Longrightarrow> thesis" using b
apply(simp)
- by (metis List.set.simps(1) emptyE empty_subsetI)
+ by (metis List.set_simps(1) emptyE empty_subsetI)
have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
proof -
fix x :: 'a
--- 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 \<union> fset ys"
using set_append [Transfer.transferred] .
--- 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 \<Rightarrow> 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 \<Rightarrow> bool" done
+lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" .
term "Lift_Set.empty"
thm Lift_Set.empty_def
-lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" done
+lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" .
term "Lift_Set.insert"
thm Lift_Set.insert_def
@@ -31,4 +31,3 @@
export_code empty insert in SML
end
-