--- a/NEWS Tue Jun 29 02:18:08 2010 +0100
+++ b/NEWS Tue Jun 29 07:55:18 2010 +0200
@@ -21,6 +21,22 @@
of ML functions, facts etc. involving split have been retained so far,
though. INCOMPATIBILITY.
+* Dropped old infix syntax "mem" for List.member; use "in set"
+instead. INCOMPATIBILITY.
+
+* Refactoring of code-generation specific operations in List.thy
+
+ constants
+ null ~> List.null
+
+ facts
+ mem_iff ~> member_def
+ null_empty ~> null_def
+
+INCOMPATIBILITY. Note that these were not suppossed to be used
+regularly unless for striking reasons; their main purpose was code
+generation.
+
* Some previously unqualified names have been qualified:
types
--- a/src/HOL/Auth/Guard/Guard.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy Tue Jun 29 07:55:18 2010 +0200
@@ -201,14 +201,16 @@
lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'"
by (induct l, auto)
-lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
-by (induct l, auto)
+lemma mem_cnb_minus: "x \<in> set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
+ by (induct l) auto
lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
-lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
+lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
apply (induct l, auto)
-by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
+apply (erule_tac l1=l and x1=x in mem_cnb_minus_substI)
+apply simp
+done
lemma parts_cnb: "Z:parts (set l) ==>
cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
@@ -272,7 +274,7 @@
apply (clarsimp, blast)
(* K ~:invKey`Ks *)
apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))")
-apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
+apply (drule_tac x="decrypt' l' K Y" in spec, simp)
apply (subgoal_tac "Crypt K Y:parts (set l)")
apply (drule parts_cnb, rotate_tac -1, simp)
apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
--- a/src/HOL/Auth/Guard/GuardK.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy Tue Jun 29 07:55:18 2010 +0200
@@ -197,12 +197,12 @@
lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'"
by (induct l, auto)
-lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
+lemma mem_cnb_minus: "x \<in> set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
by (induct l, auto)
lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
-lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
+lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
apply (induct l, auto)
by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
@@ -268,7 +268,7 @@
apply (clarsimp, blast)
(* K ~:invKey`Ks *)
apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))")
-apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
+apply (drule_tac x="decrypt' l' K Y" in spec, simp)
apply (subgoal_tac "Crypt K Y:parts (set l)")
apply (drule parts_cnb, rotate_tac -1, simp)
apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
--- a/src/HOL/Bali/Trans.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Bali/Trans.thy Tue Jun 29 07:55:18 2010 +0200
@@ -10,7 +10,7 @@
theory Trans imports Evaln begin
definition groundVar :: "var \<Rightarrow> bool" where
-"groundVar v \<equiv> (case v of
+"groundVar v \<longleftrightarrow> (case v of
LVar ln \<Rightarrow> True
| {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
| e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
@@ -35,19 +35,15 @@
qed
definition groundExprs :: "expr list \<Rightarrow> bool" where
-"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
+ "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
-consts the_val:: "expr \<Rightarrow> val"
-primrec
-"the_val (Lit v) = v"
+primrec the_val:: "expr \<Rightarrow> val" where
+ "the_val (Lit v) = v"
-consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
-primrec
-"the_var G s (LVar ln) =(lvar ln (store s),s)"
-the_var_FVar_def:
-"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
-the_var_AVar_def:
-"the_var G s(a.[i]) =avar G (the_val i) (the_val a) s"
+primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
+ "the_var G s (LVar ln) =(lvar ln (store s),s)"
+| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
+| the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s"
lemma the_var_FVar_simp[simp]:
"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Tue Jun 29 07:55:18 2010 +0200
@@ -425,7 +425,7 @@
lemma poly_exp_eq_zero:
"(poly (p %^ n) = poly ([]::('a::idom) list)) = (poly p = poly [] & n \<noteq> 0)"
-apply (simp only: fun_eq add: all_simps [symmetric])
+apply (simp only: fun_eq add: HOL.all_simps [symmetric])
apply (rule arg_cong [where f = All])
apply (rule ext)
apply (induct_tac "n")
--- a/src/HOL/Extraction/Euclid.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Extraction/Euclid.thy Tue Jun 29 07:55:18 2010 +0200
@@ -44,7 +44,7 @@
done
lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
- by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps)
+ by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
lemma not_prime_ex_mk:
assumes n: "Suc 0 < n"
--- a/src/HOL/Extraction/Warshall.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Extraction/Warshall.thy Tue Jun 29 07:55:18 2010 +0200
@@ -38,7 +38,7 @@
"\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
by (induct ys) simp+
-theorem list_all_scoc [simp]: "list_all P (xs @ [x]) = (P x \<and> list_all P xs)"
+theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \<longleftrightarrow> P x \<and> list_all P xs"
by (induct xs, simp+, iprover)
theorem list_all_lemma:
--- a/src/HOL/Import/HOL/HOL4Base.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Import/HOL/HOL4Base.thy Tue Jun 29 07:55:18 2010 +0200
@@ -3130,7 +3130,7 @@
by (import list EVERY_MEM)
lemma EXISTS_MEM: "ALL (P::'a::type => bool) l::'a::type list.
- list_exists P l = (EX e::'a::type. e mem l & P e)"
+ list_ex P l = (EX e::'a::type. e mem l & P e)"
by (import list EXISTS_MEM)
lemma MEM_APPEND: "ALL (e::'a::type) (l1::'a::type list) l2::'a::type list.
@@ -3138,15 +3138,15 @@
by (import list MEM_APPEND)
lemma EXISTS_APPEND: "ALL (P::'a::type => bool) (l1::'a::type list) l2::'a::type list.
- list_exists P (l1 @ l2) = (list_exists P l1 | list_exists P l2)"
+ list_ex P (l1 @ l2) = (list_ex P l1 | list_ex P l2)"
by (import list EXISTS_APPEND)
lemma NOT_EVERY: "ALL (P::'a::type => bool) l::'a::type list.
- (~ list_all P l) = list_exists (Not o P) l"
+ (~ list_all P l) = list_ex (Not o P) l"
by (import list NOT_EVERY)
lemma NOT_EXISTS: "ALL (P::'a::type => bool) l::'a::type list.
- (~ list_exists P l) = list_all (Not o P) l"
+ (~ list_ex P l) = list_all (Not o P) l"
by (import list NOT_EXISTS)
lemma MEM_MAP: "ALL (l::'a::type list) (f::'a::type => 'b::type) x::'b::type.
@@ -3220,7 +3220,7 @@
lemma EXISTS_CONG: "ALL (l1::'a::type list) (l2::'a::type list) (P::'a::type => bool)
P'::'a::type => bool.
l1 = l2 & (ALL x::'a::type. x mem l2 --> P x = P' x) -->
- list_exists P l1 = list_exists P' l2"
+ list_ex P l1 = list_ex P' l2"
by (import list EXISTS_CONG)
lemma EVERY_CONG: "ALL (l1::'a::type list) (l2::'a::type list) (P::'a::type => bool)
@@ -4598,7 +4598,7 @@
SCANR f e (x # l) = f x (hd (SCANR f e l)) # SCANR f e l)"
by (import rich_list SCANR)
-lemma IS_EL_DEF: "ALL (x::'a::type) l::'a::type list. x mem l = list_exists (op = x) l"
+lemma IS_EL_DEF: "ALL (x::'a::type) l::'a::type list. x mem l = list_ex (op = x) l"
by (import rich_list IS_EL_DEF)
definition AND_EL :: "bool list => bool" where
@@ -4608,9 +4608,9 @@
by (import rich_list AND_EL_DEF)
definition OR_EL :: "bool list => bool" where
- "OR_EL == list_exists I"
-
-lemma OR_EL_DEF: "OR_EL = list_exists I"
+ "OR_EL == list_ex I"
+
+lemma OR_EL_DEF: "OR_EL = list_ex I"
by (import rich_list OR_EL_DEF)
consts
@@ -4937,7 +4937,7 @@
by (import rich_list ALL_EL_MAP)
lemma SOME_EL_SNOC: "ALL (P::'a::type => bool) (x::'a::type) l::'a::type list.
- list_exists P (SNOC x l) = (P x | list_exists P l)"
+ list_ex P (SNOC x l) = (P x | list_ex P l)"
by (import rich_list SOME_EL_SNOC)
lemma IS_EL_SNOC: "ALL (y::'a::type) (x::'a::type) l::'a::type list.
@@ -5080,11 +5080,11 @@
by (import rich_list ALL_EL_FOLDL)
lemma SOME_EL_FOLDR: "ALL (P::'a::type => bool) l::'a::type list.
- list_exists P l = foldr (%x::'a::type. op | (P x)) l False"
+ list_ex P l = foldr (%x::'a::type. op | (P x)) l False"
by (import rich_list SOME_EL_FOLDR)
lemma SOME_EL_FOLDL: "ALL (P::'a::type => bool) l::'a::type list.
- list_exists P l = foldl (%(l'::bool) x::'a::type. l' | P x) False l"
+ list_ex P l = foldl (%(l'::bool) x::'a::type. l' | P x) False l"
by (import rich_list SOME_EL_FOLDL)
lemma ALL_EL_FOLDR_MAP: "ALL (x::'a::type => bool) xa::'a::type list.
@@ -5096,11 +5096,11 @@
by (import rich_list ALL_EL_FOLDL_MAP)
lemma SOME_EL_FOLDR_MAP: "ALL (x::'a::type => bool) xa::'a::type list.
- list_exists x xa = foldr op | (map x xa) False"
+ list_ex x xa = foldr op | (map x xa) False"
by (import rich_list SOME_EL_FOLDR_MAP)
lemma SOME_EL_FOLDL_MAP: "ALL (x::'a::type => bool) xa::'a::type list.
- list_exists x xa = foldl op | False (map x xa)"
+ list_ex x xa = foldl op | False (map x xa)"
by (import rich_list SOME_EL_FOLDL_MAP)
lemma FOLDR_FILTER: "ALL (f::'a::type => 'a::type => 'a::type) (e::'a::type)
@@ -5132,12 +5132,12 @@
by (import rich_list ASSOC_FOLDL_FLAT)
lemma SOME_EL_MAP: "ALL (P::'b::type => bool) (f::'a::type => 'b::type) l::'a::type list.
- list_exists P (map f l) = list_exists (P o f) l"
+ list_ex P (map f l) = list_ex (P o f) l"
by (import rich_list SOME_EL_MAP)
lemma SOME_EL_DISJ: "ALL (P::'a::type => bool) (Q::'a::type => bool) l::'a::type list.
- list_exists (%x::'a::type. P x | Q x) l =
- (list_exists P l | list_exists Q l)"
+ list_ex (%x::'a::type. P x | Q x) l =
+ (list_ex P l | list_ex Q l)"
by (import rich_list SOME_EL_DISJ)
lemma IS_EL_FOLDR: "ALL (x::'a::type) xa::'a::type list.
@@ -5579,7 +5579,7 @@
by (import rich_list FLAT_FLAT)
lemma SOME_EL_REVERSE: "ALL (P::'a::type => bool) l::'a::type list.
- list_exists P (rev l) = list_exists P l"
+ list_ex P (rev l) = list_ex P l"
by (import rich_list SOME_EL_REVERSE)
lemma ALL_EL_SEG: "ALL (P::'a::type => bool) l::'a::type list.
@@ -5621,29 +5621,29 @@
lemma SOME_EL_SEG: "ALL (m::nat) (k::nat) l::'a::type list.
m + k <= length l -->
- (ALL P::'a::type => bool. list_exists P (SEG m k l) --> list_exists P l)"
+ (ALL P::'a::type => bool. list_ex P (SEG m k l) --> list_ex P l)"
by (import rich_list SOME_EL_SEG)
lemma SOME_EL_FIRSTN: "ALL (m::nat) l::'a::type list.
m <= length l -->
- (ALL P::'a::type => bool. list_exists P (FIRSTN m l) --> list_exists P l)"
+ (ALL P::'a::type => bool. list_ex P (FIRSTN m l) --> list_ex P l)"
by (import rich_list SOME_EL_FIRSTN)
lemma SOME_EL_BUTFIRSTN: "ALL (m::nat) l::'a::type list.
m <= length l -->
(ALL P::'a::type => bool.
- list_exists P (BUTFIRSTN m l) --> list_exists P l)"
+ list_ex P (BUTFIRSTN m l) --> list_ex P l)"
by (import rich_list SOME_EL_BUTFIRSTN)
lemma SOME_EL_LASTN: "ALL (m::nat) l::'a::type list.
m <= length l -->
- (ALL P::'a::type => bool. list_exists P (LASTN m l) --> list_exists P l)"
+ (ALL P::'a::type => bool. list_ex P (LASTN m l) --> list_ex P l)"
by (import rich_list SOME_EL_LASTN)
lemma SOME_EL_BUTLASTN: "ALL (m::nat) l::'a::type list.
m <= length l -->
(ALL P::'a::type => bool.
- list_exists P (BUTLASTN m l) --> list_exists P l)"
+ list_ex P (BUTLASTN m l) --> list_ex P l)"
by (import rich_list SOME_EL_BUTLASTN)
lemma IS_EL_REVERSE: "ALL (x::'a::type) l::'a::type list. x mem rev l = x mem l"
@@ -5657,7 +5657,7 @@
n + m <= length l --> (ALL x::'a::type. x mem SEG n m l --> x mem l)"
by (import rich_list IS_EL_SEG)
-lemma IS_EL_SOME_EL: "ALL (x::'a::type) l::'a::type list. x mem l = list_exists (op = x) l"
+lemma IS_EL_SOME_EL: "ALL (x::'a::type) l::'a::type list. x mem l = list_ex (op = x) l"
by (import rich_list IS_EL_SOME_EL)
lemma IS_EL_FIRSTN: "ALL (x::nat) xa::'a::type list.
--- a/src/HOL/Import/HOL4Compat.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Import/HOL4Compat.thy Tue Jun 29 07:55:18 2010 +0200
@@ -6,6 +6,7 @@
imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum
begin
+abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
no_notation differentiable (infixl "differentiable" 60)
no_notation sums (infixr "sums" 80)
@@ -326,8 +327,8 @@
qed
qed
-lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)"
- by simp
+lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)"
+ by (simp add: null_def)
definition sum :: "nat list \<Rightarrow> nat" where
"sum l == foldr (op +) l 0"
@@ -347,8 +348,8 @@
lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
by simp
-lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))"
- by auto
+lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))"
+ by (simp add: member_def)
lemma FILTER: "(!P. filter P [] = []) & (!P h t.
filter P (h#t) = (if P h then h#filter P t else filter P t))"
@@ -373,15 +374,7 @@
lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
by simp
-consts
- list_exists :: "['a \<Rightarrow> bool,'a list] \<Rightarrow> bool"
-
-primrec
- list_exists_Nil: "list_exists P Nil = False"
- list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)"
-
-lemma list_exists_DEF: "(!P. list_exists P [] = False) &
- (!P h t. list_exists P (h#t) = (P h | list_exists P t))"
+lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
by simp
consts
--- a/src/HOL/Induct/Term.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Induct/Term.thy Tue Jun 29 07:55:18 2010 +0200
@@ -13,18 +13,12 @@
text {* \medskip Substitution function on terms *}
-consts
- subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
- subst_term_list ::
- "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
-
-primrec
+primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
+ and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
"subst_term f (Var a) = f a"
- "subst_term f (App b ts) = App b (subst_term_list f ts)"
-
- "subst_term_list f [] = []"
- "subst_term_list f (t # ts) =
- subst_term f t # subst_term_list f ts"
+| "subst_term f (App b ts) = App b (subst_term_list f ts)"
+| "subst_term_list f [] = []"
+| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
text {* \medskip A simple theorem about composition of substitutions *}
@@ -41,9 +35,9 @@
lemma
assumes var: "!!v. P (Var v)"
- and app: "!!f ts. list_all P ts ==> P (App f ts)"
+ and app: "!!f ts. (\<forall>t \<in> set ts. P t) ==> P (App f ts)"
shows term_induct2: "P t"
- and "list_all P ts"
+ and "\<forall>t \<in> set ts. P t"
apply (induct t and ts)
apply (rule var)
apply (rule app)
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Jun 29 07:55:18 2010 +0200
@@ -10,17 +10,14 @@
Var 'a
| App 'b "('a, 'b) term list"
-consts
- subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
- subst_term_list ::
- "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
+primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
+ subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
+ "subst_term f (Var a) = f a"
+| "subst_term f (App b ts) = App b (subst_term_list f ts)"
+| "subst_term_list f [] = []"
+| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
-primrec (subst)
- "subst_term f (Var a) = f a"
- "subst_term f (App b ts) = App b (subst_term_list f ts)"
- "subst_term_list f [] = []"
- "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
-
+lemmas subst_simps = subst_term_subst_term_list.simps
text {*
\medskip A simple lemma about composition of substitutions.
@@ -44,13 +41,13 @@
next
fix b ts assume "?Q ts"
then show "?P (App b ts)"
- by (simp only: subst.simps)
+ by (simp only: subst_simps)
next
show "?Q []" by simp
next
fix t ts
assume "?P t" "?Q ts" then show "?Q (t # ts)"
- by (simp only: subst.simps)
+ by (simp only: subst_simps)
qed
qed
@@ -59,18 +56,18 @@
theorem term_induct' [case_names Var App]:
assumes var: "!!a. P (Var a)"
- and app: "!!b ts. list_all P ts ==> P (App b ts)"
+ and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
shows "P t"
proof (induct t)
fix a show "P (Var a)" by (rule var)
next
- fix b t ts assume "list_all P ts"
+ fix b t ts assume "\<forall>t \<in> set ts. P t"
then show "P (App b ts)" by (rule app)
next
- show "list_all P []" by simp
+ show "\<forall>t \<in> set []. P t" by simp
next
- fix t ts assume "P t" "list_all P ts"
- then show "list_all P (t # ts)" by simp
+ fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"
+ then show "\<forall>t' \<in> set (t # ts). P t'" by simp
qed
lemma
--- a/src/HOL/Library/AssocList.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Library/AssocList.thy Tue Jun 29 07:55:18 2010 +0200
@@ -674,8 +674,8 @@
by (rule mapping_eqI) simp
lemma is_empty_Mapping [code]:
- "Mapping.is_empty (Mapping xs) \<longleftrightarrow> null xs"
- by (cases xs) (simp_all add: is_empty_def)
+ "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
+ by (cases xs) (simp_all add: is_empty_def null_def)
lemma update_Mapping [code]:
"Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
--- a/src/HOL/Library/Dlist.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Library/Dlist.thy Tue Jun 29 07:55:18 2010 +0200
@@ -122,7 +122,7 @@
next
case (insert x xs)
then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
- by (simp_all add: member_def mem_iff)
+ by (simp_all add: member_def List.member_def)
with insrt have "P (insert x (Dlist xs))" .
with insert show ?case by (simp add: insert_def distinct_remdups_id)
qed
@@ -144,7 +144,7 @@
case (Cons x xs)
with dxs distinct have "\<not> member (Dlist xs) x"
and "dxs = insert x (Dlist xs)"
- by (simp_all add: member_def mem_iff insert_def distinct_remdups_id)
+ by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
with insert show P .
qed
qed
@@ -205,7 +205,7 @@
lemma is_empty_Set [code]:
"Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
- by (simp add: null_def null_empty member_set)
+ by (simp add: null_def List.null_def member_set)
lemma bot_code [code]:
"bot = Set empty"
--- a/src/HOL/Library/Enum.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Library/Enum.thy Tue Jun 29 07:55:18 2010 +0200
@@ -49,8 +49,8 @@
lemma order_fun [code]:
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
- and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
- by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def order_less_le)
+ and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"
+ by (simp_all add: list_all_iff list_ex_iff enum_all expand_fun_eq le_fun_def order_less_le)
subsection {* Quantifiers *}
@@ -58,8 +58,8 @@
lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
by (simp add: list_all_iff enum_all)
-lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
- by (simp add: list_all_iff enum_all)
+lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
+ by (simp add: list_ex_iff enum_all)
subsection {* Default instances *}
--- a/src/HOL/Library/Executable_Set.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Library/Executable_Set.thy Tue Jun 29 07:55:18 2010 +0200
@@ -50,9 +50,9 @@
by simp
lemma [code]:
- "x \<in> Set xs \<longleftrightarrow> member xs x"
- "x \<in> Coset xs \<longleftrightarrow> \<not> member xs x"
- by (simp_all add: mem_iff)
+ "x \<in> Set xs \<longleftrightarrow> List.member xs x"
+ "x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x"
+ by (simp_all add: member_def)
definition is_empty :: "'a set \<Rightarrow> bool" where
[simp]: "is_empty A \<longleftrightarrow> A = {}"
@@ -85,8 +85,8 @@
*}
lemma is_empty_Set [code]:
- "is_empty (Set xs) \<longleftrightarrow> null xs"
- by (simp add: empty_null)
+ "is_empty (Set xs) \<longleftrightarrow> List.null xs"
+ by (simp add: null_def)
lemma empty_Set [code]:
"empty = Set []"
@@ -112,11 +112,11 @@
lemma Ball_Set [code]:
"Ball (Set xs) P \<longleftrightarrow> list_all P xs"
- by (simp add: ball_set)
+ by (simp add: list_all_iff)
lemma Bex_Set [code]:
"Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
- by (simp add: bex_set)
+ by (simp add: list_ex_iff)
lemma card_Set [code]:
"card (Set xs) = length (remdups xs)"
--- a/src/HOL/Library/Fset.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Library/Fset.thy Tue Jun 29 07:55:18 2010 +0200
@@ -51,7 +51,7 @@
lemma member_code [code]:
"member (Set xs) = List.member xs"
"member (Coset xs) = Not \<circ> List.member xs"
- by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def)
+ by (simp_all add: expand_fun_eq member_def fun_Compl_def bool_Compl_def)
lemma member_image_UNIV [simp]:
"member ` UNIV = UNIV"
@@ -141,7 +141,7 @@
[simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
lemma is_empty_Set [code]:
- "is_empty (Set xs) \<longleftrightarrow> null xs"
+ "is_empty (Set xs) \<longleftrightarrow> List.null xs"
by (simp add: is_empty_set)
lemma empty_Set [code]:
@@ -188,14 +188,14 @@
lemma forall_Set [code]:
"forall P (Set xs) \<longleftrightarrow> list_all P xs"
- by (simp add: Set_def ball_set)
+ by (simp add: Set_def list_all_iff)
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
[simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
lemma exists_Set [code]:
"exists P (Set xs) \<longleftrightarrow> list_ex P xs"
- by (simp add: Set_def bex_set)
+ by (simp add: Set_def list_ex_iff)
definition card :: "'a fset \<Rightarrow> nat" where
[simp]: "card A = Finite_Set.card (member A)"
--- a/src/HOL/Library/More_Set.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Library/More_Set.thy Tue Jun 29 07:55:18 2010 +0200
@@ -37,16 +37,8 @@
subsection {* Basic set operations *}
lemma is_empty_set:
- "is_empty (set xs) \<longleftrightarrow> null xs"
- by (simp add: is_empty_def null_empty)
-
-lemma ball_set:
- "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
- by (rule list_ball_code)
-
-lemma bex_set:
- "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
- by (rule list_bex_code)
+ "is_empty (set xs) \<longleftrightarrow> List.null xs"
+ by (simp add: is_empty_def null_def)
lemma empty_set:
"{} = set []"
--- a/src/HOL/Library/Univ_Poly.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Library/Univ_Poly.thy Tue Jun 29 07:55:18 2010 +0200
@@ -407,7 +407,7 @@
lemma (in idom) poly_exp_eq_zero[simp]:
"(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
-apply (simp only: fun_eq add: all_simps [symmetric])
+apply (simp only: fun_eq add: HOL.all_simps [symmetric])
apply (rule arg_cong [where f = All])
apply (rule ext)
apply (induct n)
--- a/src/HOL/Library/positivstellensatz.ML Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Tue Jun 29 07:55:18 2010 +0200
@@ -228,7 +228,7 @@
val prenex_simps =
map (fn th => th RS sym)
([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @
- @{thms "all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
+ @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
val real_abs_thms1 = @{lemma
"((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and
--- a/src/HOL/List.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/List.thy Tue Jun 29 07:55:18 2010 +0200
@@ -2352,6 +2352,22 @@
case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
qed
+lemma rev_foldl_cons [code]:
+ "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
+proof (induct xs)
+ case Nil then show ?case by simp
+next
+ case Cons
+ {
+ fix x xs ys
+ have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
+ = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
+ by (induct xs arbitrary: ys) auto
+ }
+ note aux = this
+ show ?case by (induct xs) (auto simp add: Cons aux)
+qed
+
text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
@@ -2509,120 +2525,6 @@
by (simp add: sup_commute)
-subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
-
-lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
-by (induct xs) (simp_all add:add_assoc)
-
-lemma listsum_rev [simp]:
- fixes xs :: "'a\<Colon>comm_monoid_add list"
- shows "listsum (rev xs) = listsum xs"
-by (induct xs) (simp_all add:add_ac)
-
-lemma listsum_map_remove1:
-fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
-shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
-by (induct xs)(auto simp add:add_ac)
-
-lemma list_size_conv_listsum:
- "list_size f xs = listsum (map f xs) + size xs"
-by(induct xs) auto
-
-lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
-by (induct xs) auto
-
-lemma length_concat: "length (concat xss) = listsum (map length xss)"
-by (induct xss) simp_all
-
-lemma listsum_map_filter:
- fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
- assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
- shows "listsum (map f (filter P xs)) = listsum (map f xs)"
-using assms by (induct xs) auto
-
-text{* For efficient code generation ---
- @{const listsum} is not tail recursive but @{const foldl} is. *}
-lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
-by(simp add:listsum_foldr foldl_foldr1)
-
-lemma distinct_listsum_conv_Setsum:
- "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
-by (induct xs) simp_all
-
-lemma listsum_eq_0_nat_iff_nat[simp]:
- "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
-by(simp add: listsum)
-
-lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)"
-apply(induct ns arbitrary: k)
- apply simp
-apply(fastsimp simp add:nth_Cons split: nat.split)
-done
-
-lemma listsum_update_nat: "k<size ns \<Longrightarrow>
- listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"
-apply(induct ns arbitrary:k)
- apply (auto split:nat.split)
-apply(drule elem_le_listsum_nat)
-apply arith
-done
-
-text{* Some syntactic sugar for summing a function over a list: *}
-
-syntax
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
-syntax (xsymbols)
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
-
-translations -- {* Beware of argument permutation! *}
- "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
- "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
-
-lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
- by (induct xs) (simp_all add: left_distrib)
-
-lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
- by (induct xs) (simp_all add: left_distrib)
-
-text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
-lemma uminus_listsum_map:
- fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
- shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
-by (induct xs) simp_all
-
-lemma listsum_addf:
- fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
- shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
-by (induct xs) (simp_all add: algebra_simps)
-
-lemma listsum_subtractf:
- fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
- shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
-by (induct xs) simp_all
-
-lemma listsum_const_mult:
- fixes f :: "'a \<Rightarrow> 'b::semiring_0"
- shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
-by (induct xs, simp_all add: algebra_simps)
-
-lemma listsum_mult_const:
- fixes f :: "'a \<Rightarrow> 'b::semiring_0"
- shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
-by (induct xs, simp_all add: algebra_simps)
-
-lemma listsum_abs:
- fixes xs :: "'a::ordered_ab_group_add_abs list"
- shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
-by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
-
-lemma listsum_mono:
- fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"
- shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"
-by (induct xs, simp, simp add: add_mono)
-
-
subsubsection {* @{text upt} *}
lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
@@ -2961,6 +2863,137 @@
qed
+subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
+
+lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
+by (induct xs) (simp_all add:add_assoc)
+
+lemma listsum_rev [simp]:
+ fixes xs :: "'a\<Colon>comm_monoid_add list"
+ shows "listsum (rev xs) = listsum xs"
+by (induct xs) (simp_all add:add_ac)
+
+lemma listsum_map_remove1:
+fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
+shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
+by (induct xs)(auto simp add:add_ac)
+
+lemma list_size_conv_listsum:
+ "list_size f xs = listsum (map f xs) + size xs"
+by(induct xs) auto
+
+lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
+by (induct xs) auto
+
+lemma length_concat: "length (concat xss) = listsum (map length xss)"
+by (induct xss) simp_all
+
+lemma listsum_map_filter:
+ fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
+ assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
+ shows "listsum (map f (filter P xs)) = listsum (map f xs)"
+using assms by (induct xs) auto
+
+text{* For efficient code generation ---
+ @{const listsum} is not tail recursive but @{const foldl} is. *}
+lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
+by(simp add:listsum_foldr foldl_foldr1)
+
+lemma distinct_listsum_conv_Setsum:
+ "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
+by (induct xs) simp_all
+
+lemma listsum_eq_0_nat_iff_nat[simp]:
+ "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
+by(simp add: listsum)
+
+lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)"
+apply(induct ns arbitrary: k)
+ apply simp
+apply(fastsimp simp add:nth_Cons split: nat.split)
+done
+
+lemma listsum_update_nat: "k<size ns \<Longrightarrow>
+ listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"
+apply(induct ns arbitrary:k)
+ apply (auto split:nat.split)
+apply(drule elem_le_listsum_nat)
+apply arith
+done
+
+text{* Some syntactic sugar for summing a function over a list: *}
+
+syntax
+ "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
+syntax (xsymbols)
+ "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+syntax (HTML output)
+ "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+
+translations -- {* Beware of argument permutation! *}
+ "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
+ "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
+
+lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
+ by (induct xs) (simp_all add: left_distrib)
+
+lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
+ by (induct xs) (simp_all add: left_distrib)
+
+text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
+lemma uminus_listsum_map:
+ fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
+ shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
+by (induct xs) simp_all
+
+lemma listsum_addf:
+ fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
+ shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
+by (induct xs) (simp_all add: algebra_simps)
+
+lemma listsum_subtractf:
+ fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
+ shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
+by (induct xs) simp_all
+
+lemma listsum_const_mult:
+ fixes f :: "'a \<Rightarrow> 'b::semiring_0"
+ shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
+by (induct xs, simp_all add: algebra_simps)
+
+lemma listsum_mult_const:
+ fixes f :: "'a \<Rightarrow> 'b::semiring_0"
+ shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
+by (induct xs, simp_all add: algebra_simps)
+
+lemma listsum_abs:
+ fixes xs :: "'a::ordered_ab_group_add_abs list"
+ shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
+by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
+
+lemma listsum_mono:
+ fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"
+ shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"
+by (induct xs, simp, simp add: add_mono)
+
+lemma listsum_distinct_conv_setsum_set:
+ "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
+ by (induct xs) simp_all
+
+lemma interv_listsum_conv_setsum_set_nat:
+ "listsum (map f [m..<n]) = setsum f (set [m..<n])"
+ by (simp add: listsum_distinct_conv_setsum_set)
+
+lemma interv_listsum_conv_setsum_set_int:
+ "listsum (map f [k..l]) = setsum f (set [k..l])"
+ by (simp add: listsum_distinct_conv_setsum_set)
+
+text {* General equivalence between @{const listsum} and @{const setsum} *}
+lemma listsum_setsum_nth:
+ "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
+ using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
+
+
subsubsection {* @{const insert} *}
lemma in_set_insert [simp]:
@@ -4513,9 +4546,266 @@
*)
-subsection {* Code generator *}
-
-subsubsection {* Setup *}
+subsection {* Code generation *}
+
+subsubsection {* Counterparts for set-related operations *}
+
+definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
+ [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
+
+text {*
+ Only use @{text member} for generating executable code. Otherwise use
+ @{prop "x \<in> set xs"} instead --- it is much easier to reason about.
+*}
+
+lemma member_set:
+ "member = set"
+ by (simp add: expand_fun_eq member_def mem_def)
+
+lemma member_rec [code]:
+ "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
+ "member [] y \<longleftrightarrow> False"
+ by (auto simp add: member_def)
+
+lemma in_set_member [code_unfold]:
+ "x \<in> set xs \<longleftrightarrow> member xs x"
+ by (simp add: member_def)
+
+declare INFI_def [code_unfold]
+declare SUPR_def [code_unfold]
+
+declare set_map [symmetric, code_unfold]
+
+definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+ list_all_iff [code_post]: "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
+
+definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+ list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
+
+text {*
+ Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
+ over @{const list_all} and @{const list_ex} in specifications.
+*}
+
+lemma list_all_simps [simp, code]:
+ "list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs"
+ "list_all P [] \<longleftrightarrow> True"
+ by (simp_all add: list_all_iff)
+
+lemma list_ex_simps [simp, code]:
+ "list_ex P (x # xs) \<longleftrightarrow> P x \<or> list_ex P xs"
+ "list_ex P [] \<longleftrightarrow> False"
+ by (simp_all add: list_ex_iff)
+
+lemma Ball_set_list_all [code_unfold]:
+ "Ball (set xs) P \<longleftrightarrow> list_all P xs"
+ by (simp add: list_all_iff)
+
+lemma Bex_set_list_ex [code_unfold]:
+ "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
+ by (simp add: list_ex_iff)
+
+lemma list_all_append [simp]:
+ "list_all P (xs @ ys) \<longleftrightarrow> list_all P xs \<and> list_all P ys"
+ by (auto simp add: list_all_iff)
+
+lemma list_ex_append [simp]:
+ "list_ex P (xs @ ys) \<longleftrightarrow> list_ex P xs \<or> list_ex P ys"
+ by (auto simp add: list_ex_iff)
+
+lemma list_all_rev [simp]:
+ "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
+ by (simp add: list_all_iff)
+
+lemma list_ex_rev [simp]:
+ "list_ex P (rev xs) \<longleftrightarrow> list_ex P xs"
+ by (simp add: list_ex_iff)
+
+lemma list_all_length:
+ "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
+ by (auto simp add: list_all_iff set_conv_nth)
+
+lemma list_ex_length:
+ "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
+ by (auto simp add: list_ex_iff set_conv_nth)
+
+lemma list_all_cong [fundef_cong]:
+ "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
+ by (simp add: list_all_iff)
+
+lemma list_any_cong [fundef_cong]:
+ "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
+ by (simp add: list_ex_iff)
+
+text {* Bounded quantification and summation over nats. *}
+
+lemma atMost_upto [code_unfold]:
+ "{..n} = set [0..<Suc n]"
+ by auto
+
+lemma atLeast_upt [code_unfold]:
+ "{..<n} = set [0..<n]"
+ by auto
+
+lemma greaterThanLessThan_upt [code_unfold]:
+ "{n<..<m} = set [Suc n..<m]"
+ by auto
+
+lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
+
+lemma greaterThanAtMost_upt [code_unfold]:
+ "{n<..m} = set [Suc n..<Suc m]"
+ by auto
+
+lemma atLeastAtMost_upt [code_unfold]:
+ "{n..m} = set [n..<Suc m]"
+ by auto
+
+lemma all_nat_less_eq [code_unfold]:
+ "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
+ by auto
+
+lemma ex_nat_less_eq [code_unfold]:
+ "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
+ by auto
+
+lemma all_nat_less [code_unfold]:
+ "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
+ by auto
+
+lemma ex_nat_less [code_unfold]:
+ "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
+ by auto
+
+lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
+ "setsum f (set [m..<n]) = listsum (map f [m..<n])"
+ by (simp add: interv_listsum_conv_setsum_set_nat)
+
+text {* Summation over ints. *}
+
+lemma greaterThanLessThan_upto [code_unfold]:
+ "{i<..<j::int} = set [i+1..j - 1]"
+by auto
+
+lemma atLeastLessThan_upto [code_unfold]:
+ "{i..<j::int} = set [i..j - 1]"
+by auto
+
+lemma greaterThanAtMost_upto [code_unfold]:
+ "{i<..j::int} = set [i+1..j]"
+by auto
+
+lemmas atLeastAtMost_upto [code_unfold] = set_upto [symmetric]
+
+lemma setsum_set_upto_conv_listsum_int [code_unfold]:
+ "setsum f (set [i..j::int]) = listsum (map f [i..j])"
+ by (simp add: interv_listsum_conv_setsum_set_int)
+
+
+subsubsection {* Optimizing by rewriting *}
+
+definition null :: "'a list \<Rightarrow> bool" where
+ [code_post]: "null xs \<longleftrightarrow> xs = []"
+
+text {*
+ Efficient emptyness check is implemented by @{const null}.
+*}
+
+lemma null_rec [code]:
+ "null (x # xs) \<longleftrightarrow> False"
+ "null [] \<longleftrightarrow> True"
+ by (simp_all add: null_def)
+
+lemma eq_Nil_null [code_unfold]:
+ "xs = [] \<longleftrightarrow> null xs"
+ by (simp add: null_def)
+
+lemma equal_Nil_null [code_unfold]:
+ "eq_class.eq xs [] \<longleftrightarrow> null xs"
+ by (simp add: eq eq_Nil_null)
+
+definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
+ [code_post]: "maps f xs = concat (map f xs)"
+
+definition map_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
+ [code_post]: "map_filter f xs = map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> None) xs)"
+
+text {*
+ Operations @{const maps} and @{const map_filter} avoid
+ intermediate lists on execution -- do not use for proving.
+*}
+
+lemma maps_simps [code]:
+ "maps f (x # xs) = f x @ maps f xs"
+ "maps f [] = []"
+ by (simp_all add: maps_def)
+
+lemma map_filter_simps [code]:
+ "map_filter f (x # xs) = (case f x of None \<Rightarrow> map_filter f xs | Some y \<Rightarrow> y # map_filter f xs)"
+ "map_filter f [] = []"
+ by (simp_all add: map_filter_def split: option.split)
+
+lemma concat_map_maps [code_unfold]:
+ "concat (map f xs) = maps f xs"
+ by (simp add: maps_def)
+
+lemma map_filter_map_filter [code_unfold]:
+ "map f (filter P xs) = map_filter (\<lambda>x. if P x then Some (f x) else None) xs"
+ by (simp add: map_filter_def)
+
+text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
+and similiarly for @{text"\<exists>"}. *}
+
+definition all_interval_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+ "all_interval_nat P i j \<longleftrightarrow> (\<forall>n \<in> {i..<j}. P n)"
+
+lemma [code]:
+ "all_interval_nat P i j \<longleftrightarrow> i \<ge> j \<or> P i \<and> all_interval_nat P (Suc i) j"
+proof -
+ have *: "\<And>n. P i \<Longrightarrow> \<forall>n\<in>{Suc i..<j}. P n \<Longrightarrow> i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n"
+ proof -
+ fix n
+ assume "P i" "\<forall>n\<in>{Suc i..<j}. P n" "i \<le> n" "n < j"
+ then show "P n" by (cases "n = i") simp_all
+ qed
+ show ?thesis by (auto simp add: all_interval_nat_def intro: *)
+qed
+
+lemma list_all_iff_all_interval_nat [code_unfold]:
+ "list_all P [i..<j] \<longleftrightarrow> all_interval_nat P i j"
+ by (simp add: list_all_iff all_interval_nat_def)
+
+lemma list_ex_iff_not_all_inverval_nat [code_unfold]:
+ "list_ex P [i..<j] \<longleftrightarrow> \<not> (all_interval_nat (Not \<circ> P) i j)"
+ by (simp add: list_ex_iff all_interval_nat_def)
+
+definition all_interval_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
+ "all_interval_int P i j \<longleftrightarrow> (\<forall>k \<in> {i..j}. P k)"
+
+lemma [code]:
+ "all_interval_int P i j \<longleftrightarrow> i > j \<or> P i \<and> all_interval_int P (i + 1) j"
+proof -
+ have *: "\<And>k. P i \<Longrightarrow> \<forall>k\<in>{i+1..j}. P k \<Longrightarrow> i \<le> k \<Longrightarrow> k \<le> j \<Longrightarrow> P k"
+ proof -
+ fix k
+ assume "P i" "\<forall>k\<in>{i+1..j}. P k" "i \<le> k" "k \<le> j"
+ then show "P k" by (cases "k = i") simp_all
+ qed
+ show ?thesis by (auto simp add: all_interval_int_def intro: *)
+qed
+
+lemma list_all_iff_all_interval_int [code_unfold]:
+ "list_all P [i..j] \<longleftrightarrow> all_interval_int P i j"
+ by (simp add: list_all_iff all_interval_int_def)
+
+lemma list_ex_iff_not_all_inverval_int [code_unfold]:
+ "list_ex P [i..j] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> P) i j)"
+ by (simp add: list_ex_iff all_interval_int_def)
+
+hide_const (open) member null maps map_filter all_interval_nat all_interval_int
+
+
+subsubsection {* Pretty lists *}
use "Tools/list_code.ML"
@@ -4578,374 +4868,6 @@
*}
-subsubsection {* Generation of efficient code *}
-
-definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
- mem_iff [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
-
-primrec
- null:: "'a list \<Rightarrow> bool"
-where
- "null [] = True"
- | "null (x#xs) = False"
-
-primrec
- list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
- "list_inter [] bs = []"
- | "list_inter (a#as) bs =
- (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
-
-primrec
- list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
-where
- "list_all P [] = True"
- | "list_all P (x#xs) = (P x \<and> list_all P xs)"
-
-primrec
- list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
-where
- "list_ex P [] = False"
- | "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
-
-primrec
- filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
-where
- "filtermap f [] = []"
- | "filtermap f (x#xs) =
- (case f x of None \<Rightarrow> filtermap f xs
- | Some y \<Rightarrow> y # filtermap f xs)"
-
-primrec
- map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
-where
- "map_filter f P [] = []"
- | "map_filter f P (x#xs) =
- (if P x then f x # map_filter f P xs else map_filter f P xs)"
-
-primrec
- length_unique :: "'a list \<Rightarrow> nat"
-where
- "length_unique [] = 0"
- | "length_unique (x#xs) =
- (if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
-
-primrec
- concat_map :: "('a => 'b list) => 'a list => 'b list"
-where
- "concat_map f [] = []"
- | "concat_map f (x#xs) = f x @ concat_map f xs"
-
-text {*
- Only use @{text member} for generating executable code. Otherwise use
- @{prop "x : set xs"} instead --- it is much easier to reason about.
- The same is true for @{const list_all} and @{const list_ex}: write
- @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
- quantifiers are aleady known to the automatic provers. In fact, the
- declarations in the code subsection make sure that @{text "\<in>"},
- @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} are implemented
- efficiently.
-
- Efficient emptyness check is implemented by @{const null}.
-
- The functions @{const filtermap} and @{const map_filter} are just
- there to generate efficient code. Do not use
- them for modelling and proving.
-*}
-
-lemma rev_foldl_cons [code]:
- "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
-proof (induct xs)
- case Nil then show ?case by simp
-next
- case Cons
- {
- fix x xs ys
- have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
- = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
- by (induct xs arbitrary: ys) auto
- }
- note aux = this
- show ?case by (induct xs) (auto simp add: Cons aux)
-qed
-
-lemmas in_set_code [code_unfold] = mem_iff [symmetric]
-
-lemma member_simps [simp, code]:
- "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
- "member [] y \<longleftrightarrow> False"
- by (auto simp add: mem_iff)
-
-lemma member_set:
- "member = set"
- by (simp add: expand_fun_eq mem_iff mem_def)
-
-abbreviation (input) mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55) where
- "x mem xs \<equiv> member xs x" -- "for backward compatibility"
-
-lemma empty_null:
- "xs = [] \<longleftrightarrow> null xs"
-by (cases xs) simp_all
-
-lemma [code_unfold]:
- "eq_class.eq xs [] \<longleftrightarrow> null xs"
-by (simp add: eq empty_null)
-
-lemmas null_empty [code_post] =
- empty_null [symmetric]
-
-lemma list_inter_conv:
- "set (list_inter xs ys) = set xs \<inter> set ys"
-by (induct xs) auto
-
-lemma list_all_iff [code_post]:
- "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
-by (induct xs) auto
-
-lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
-
-lemma list_all_append [simp]:
- "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
-by (induct xs) auto
-
-lemma list_all_rev [simp]:
- "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
-by (simp add: list_all_iff)
-
-lemma list_all_length:
- "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
-unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
-
-lemma list_all_cong[fundef_cong]:
- "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
-by (simp add: list_all_iff)
-
-lemma list_ex_iff [code_post]:
- "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
-by (induct xs) simp_all
-
-lemmas list_bex_code [code_unfold] =
- list_ex_iff [symmetric]
-
-lemma list_ex_length:
- "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
-unfolding list_ex_iff set_conv_nth by auto
-
-lemma list_ex_cong[fundef_cong]:
- "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
-by (simp add: list_ex_iff)
-
-lemma filtermap_conv:
- "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
-by (induct xs) (simp_all split: option.split)
-
-lemma map_filter_conv [simp]:
- "map_filter f P xs = map f (filter P xs)"
-by (induct xs) auto
-
-lemma length_remdups_length_unique [code_unfold]:
- "length (remdups xs) = length_unique xs"
-by (induct xs) simp_all
-
-lemma concat_map_code[code_unfold]:
- "concat(map f xs) = concat_map f xs"
-by (induct xs) simp_all
-
-declare INFI_def [code_unfold]
-declare SUPR_def [code_unfold]
-
-declare set_map [symmetric, code_unfold]
-
-hide_const (open) length_unique
-
-
-text {* Code for bounded quantification and summation over nats. *}
-
-lemma atMost_upto [code_unfold]:
- "{..n} = set [0..<Suc n]"
-by auto
-
-lemma atLeast_upt [code_unfold]:
- "{..<n} = set [0..<n]"
-by auto
-
-lemma greaterThanLessThan_upt [code_unfold]:
- "{n<..<m} = set [Suc n..<m]"
-by auto
-
-lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
-
-lemma greaterThanAtMost_upt [code_unfold]:
- "{n<..m} = set [Suc n..<Suc m]"
-by auto
-
-lemma atLeastAtMost_upt [code_unfold]:
- "{n..m} = set [n..<Suc m]"
-by auto
-
-lemma all_nat_less_eq [code_unfold]:
- "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
-by auto
-
-lemma ex_nat_less_eq [code_unfold]:
- "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
-by auto
-
-lemma all_nat_less [code_unfold]:
- "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
-by auto
-
-lemma ex_nat_less [code_unfold]:
- "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
-by auto
-
-lemma setsum_set_distinct_conv_listsum:
- "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
-by (induct xs) simp_all
-
-lemma setsum_set_upt_conv_listsum [code_unfold]:
- "setsum f (set [m..<n]) = listsum (map f [m..<n])"
-by (rule setsum_set_distinct_conv_listsum) simp
-
-text {* General equivalence between @{const listsum} and @{const setsum} *}
-lemma listsum_setsum_nth:
- "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
-using setsum_set_upt_conv_listsum[of "op ! xs" 0 "length xs"]
-by (simp add: map_nth)
-
-text {* Code for summation over ints. *}
-
-lemma greaterThanLessThan_upto [code_unfold]:
- "{i<..<j::int} = set [i+1..j - 1]"
-by auto
-
-lemma atLeastLessThan_upto [code_unfold]:
- "{i..<j::int} = set [i..j - 1]"
-by auto
-
-lemma greaterThanAtMost_upto [code_unfold]:
- "{i<..j::int} = set [i+1..j]"
-by auto
-
-lemmas atLeastAtMost_upto [code_unfold] = set_upto[symmetric]
-
-lemma setsum_set_upto_conv_listsum [code_unfold]:
- "setsum f (set [i..j::int]) = listsum (map f [i..j])"
-by (rule setsum_set_distinct_conv_listsum) simp
-
-
-text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
-and similiarly for @{text"\<exists>"}. *}
-
-function all_from_to_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
-"all_from_to_nat P i j =
- (if i < j then if P i then all_from_to_nat P (i+1) j else False
- else True)"
-by auto
-termination
-by (relation "measure(%(P,i,j). j - i)") auto
-
-declare all_from_to_nat.simps[simp del]
-
-lemma all_from_to_nat_iff_ball:
- "all_from_to_nat P i j = (ALL n : {i ..< j}. P n)"
-proof(induct P i j rule:all_from_to_nat.induct)
- case (1 P i j)
- let ?yes = "i < j & P i"
- show ?case
- proof (cases)
- assume ?yes
- hence "all_from_to_nat P i j = (P i & all_from_to_nat P (i+1) j)"
- by(simp add: all_from_to_nat.simps)
- also have "... = (P i & (ALL n : {i+1 ..< j}. P n))" using `?yes` 1 by simp
- also have "... = (ALL n : {i ..< j}. P n)" (is "?L = ?R")
- proof
- assume L: ?L
- show ?R
- proof clarify
- fix n assume n: "n : {i..<j}"
- show "P n"
- proof cases
- assume "n = i" thus "P n" using L by simp
- next
- assume "n ~= i"
- hence "i+1 <= n" using n by auto
- thus "P n" using L n by simp
- qed
- qed
- next
- assume R: ?R thus ?L using `?yes` 1 by auto
- qed
- finally show ?thesis .
- next
- assume "~?yes" thus ?thesis by(auto simp add: all_from_to_nat.simps)
- qed
-qed
-
-
-lemma list_all_iff_all_from_to_nat[code_unfold]:
- "list_all P [i..<j] = all_from_to_nat P i j"
-by(simp add: all_from_to_nat_iff_ball list_all_iff)
-
-lemma list_ex_iff_not_all_from_to_not_nat[code_unfold]:
- "list_ex P [i..<j] = (~all_from_to_nat (%x. ~P x) i j)"
-by(simp add: all_from_to_nat_iff_ball list_ex_iff)
-
-
-function all_from_to_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
-"all_from_to_int P i j =
- (if i <= j then if P i then all_from_to_int P (i+1) j else False
- else True)"
-by auto
-termination
-by (relation "measure(%(P,i,j). nat(j - i + 1))") auto
-
-declare all_from_to_int.simps[simp del]
-
-lemma all_from_to_int_iff_ball:
- "all_from_to_int P i j = (ALL n : {i .. j}. P n)"
-proof(induct P i j rule:all_from_to_int.induct)
- case (1 P i j)
- let ?yes = "i <= j & P i"
- show ?case
- proof (cases)
- assume ?yes
- hence "all_from_to_int P i j = (P i & all_from_to_int P (i+1) j)"
- by(simp add: all_from_to_int.simps)
- also have "... = (P i & (ALL n : {i+1 .. j}. P n))" using `?yes` 1 by simp
- also have "... = (ALL n : {i .. j}. P n)" (is "?L = ?R")
- proof
- assume L: ?L
- show ?R
- proof clarify
- fix n assume n: "n : {i..j}"
- show "P n"
- proof cases
- assume "n = i" thus "P n" using L by simp
- next
- assume "n ~= i"
- hence "i+1 <= n" using n by auto
- thus "P n" using L n by simp
- qed
- qed
- next
- assume R: ?R thus ?L using `?yes` 1 by auto
- qed
- finally show ?thesis .
- next
- assume "~?yes" thus ?thesis by(auto simp add: all_from_to_int.simps)
- qed
-qed
-
-lemma list_all_iff_all_from_to_int[code_unfold]:
- "list_all P [i..j] = all_from_to_int P i j"
-by(simp add: all_from_to_int_iff_ball list_all_iff)
-
-lemma list_ex_iff_not_all_from_to_not_int[code_unfold]:
- "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
-by(simp add: all_from_to_int_iff_ball list_ex_iff)
-
-
subsubsection {* Use convenient predefined operations *}
code_const "op @"
@@ -4963,12 +4885,18 @@
code_const concat
(Haskell "concat")
+code_const List.maps
+ (Haskell "concatMap")
+
code_const rev
(Haskell "reverse")
code_const zip
(Haskell "zip")
+code_const List.null
+ (Haskell "null")
+
code_const takeWhile
(Haskell "takeWhile")
@@ -4981,4 +4909,10 @@
code_const last
(Haskell "last")
+code_const list_all
+ (Haskell "all")
+
+code_const list_ex
+ (Haskell "any")
+
end
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Tue Jun 29 07:55:18 2010 +0200
@@ -10,17 +10,17 @@
begin
definition is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" where
- "is_target step phi pc' \<equiv>
- \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))"
+ "is_target step phi pc' \<longleftrightarrow>
+ (\<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc)))"
definition make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate" where
- "make_cert step phi B \<equiv>
+ "make_cert step phi B =
map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"
lemma [code]:
"is_target step phi pc' =
- list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"
-by (force simp: list_ex_iff is_target_def mem_iff)
+ list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> List.member (map fst (step pc (phi!pc))) pc') [0..<length phi]"
+by (force simp: list_ex_iff member_def is_target_def)
locale lbvc = lbv +
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Jun 29 07:55:18 2010 +0200
@@ -707,7 +707,7 @@
case False
have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add: power2_eq_square)
also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
- also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
+ also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by (auto simp add: inner_diff_left)
also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz)
finally show ?thesis using False x(1) by(auto simp add: real_mult_left_cancel) next
case True thus ?thesis using assms(1) apply(rule_tac x="(a + b) /2" in bexI) by auto qed qed
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Jun 29 07:55:18 2010 +0200
@@ -15,7 +15,7 @@
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
by auto
-abbreviation inner_bullet (infix "\<bullet>" 70) where "x \<bullet> y \<equiv> inner x y"
+notation inner (infix "\<bullet>" 70)
subsection {* A connectedness or intermediate value lemma with several applications. *}
@@ -466,8 +466,8 @@
"orthogonal x a \<Longrightarrow> orthogonal (-x) a"
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
- unfolding orthogonal_def inner_simps by auto
-
+ unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto
+
end
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
--- a/src/HOL/NanoJava/Equivalence.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy Tue Jun 29 07:55:18 2010 +0200
@@ -133,7 +133,7 @@
apply (clarify intro!: Impl_nvalid_0)
apply (clarify intro!: Impl_nvalid_Suc)
apply (drule nvalids_SucD)
-apply (simp only: all_simps)
+apply (simp only: HOL.all_simps)
apply (erule (1) impE)
apply (drule (2) Impl_sound_lemma)
apply blast
--- a/src/HOL/Number_Theory/Primes.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Number_Theory/Primes.thy Tue Jun 29 07:55:18 2010 +0200
@@ -208,22 +208,20 @@
lemma one_not_prime_int [simp]: "~prime (1::int)"
by (simp add: prime_int_def)
-lemma prime_nat_code[code]:
- "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
-apply(simp add: Ball_def)
+lemma prime_nat_code [code]:
+ "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
+apply (simp add: Ball_def)
apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
done
lemma prime_nat_simp:
- "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
-apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
-apply(simp add:nat_number One_nat_def)
-done
+ "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
+by (auto simp add: prime_nat_code)
-lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard]
+lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
-lemma prime_int_code[code]:
- "prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R")
+lemma prime_int_code [code]:
+ "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
proof
assume "?L" thus "?R"
by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
@@ -232,12 +230,10 @@
qed
lemma prime_int_simp:
- "prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))"
-apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto)
-apply simp
-done
+ "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
+by (auto simp add: prime_int_code)
-lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
+lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
lemma two_is_prime_nat [simp]: "prime (2::nat)"
by simp
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Tue Jun 29 07:55:18 2010 +0200
@@ -1174,7 +1174,8 @@
ultimately show ?case using prime_divprod[OF p] by blast
qed
-lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps" by (auto simp add: primefact_def list_all_iff)
+lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps"
+ by (auto simp add: primefact_def list_all_iff)
(* Variant of Lucas theorem. *)
--- a/src/HOL/Tools/refute.ML Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Tools/refute.ML Tue Jun 29 07:55:18 2010 +0200
@@ -2234,7 +2234,7 @@
(* sanity check: every element of terms' must also be *)
(* present in terms *)
val _ =
- if List.all (member (op =) terms) terms' then ()
+ if forall (member (op =) terms) terms' then ()
else
raise REFUTE ("IDT_constructor_interpreter",
"element has disappeared")
@@ -2957,7 +2957,7 @@
(* "lfp(f) == Inter({u. f(u) <= u})" *)
(* interpretation * interpretation -> bool *)
fun is_subset (Node subs, Node sups) =
- List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT))
+ forall (fn (sub, sup) => (sub = FF) orelse (sup = TT))
(subs ~~ sups)
| is_subset (_, _) =
raise REFUTE ("lfp_interpreter",
@@ -3012,7 +3012,7 @@
(* "gfp(f) == Union({u. u <= f(u)})" *)
(* interpretation * interpretation -> bool *)
fun is_subset (Node subs, Node sups) =
- List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT))
+ forall (fn (sub, sup) => (sub = FF) orelse (sup = TT))
(subs ~~ sups)
| is_subset (_, _) =
raise REFUTE ("gfp_interpreter",
--- a/src/HOL/Word/WordShift.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/Word/WordShift.thy Tue Jun 29 07:55:18 2010 +0200
@@ -988,8 +988,10 @@
apply (erule bin_nth_uint_imp)+
done
-lemmas test_bit_split =
- test_bit_split' [THEN mp, simplified all_simps, standard]
+lemma test_bit_split:
+ "word_split c = (a, b) \<Longrightarrow>
+ (\<forall>n\<Colon>nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> (\<forall>m\<Colon>nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
+ by (simp add: test_bit_split')
lemma test_bit_split_eq: "word_split c = (a, b) <->
((ALL n::nat. b !! n = (n < size b & c !! n)) &
--- a/src/HOL/ex/Execute_Choice.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/ex/Execute_Choice.thy Tue Jun 29 07:55:18 2010 +0200
@@ -66,7 +66,7 @@
shows [code]: "valuesum (Mapping []) = 0"
and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in
the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
- by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping)
+ by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping null_def)
text {*
As a side effect the precondition disappears (but note this has nothing to do with choice!).
--- a/src/HOL/ex/Meson_Test.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/ex/Meson_Test.thy Tue Jun 29 07:55:18 2010 +0200
@@ -16,7 +16,7 @@
below and constants declared in HOL!
*}
-hide_const (open) subset member quotient union inter sum
+hide_const (open) subset quotient union inter sum
text {*
Test data for the MESON proof procedure
--- a/src/HOL/ex/Recdefs.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOL/ex/Recdefs.thy Tue Jun 29 07:55:18 2010 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Recdefs.thy
- ID: $Id$
Author: Konrad Slind and Lawrence C Paulson
Copyright 1996 University of Cambridge
@@ -44,7 +43,7 @@
text {* Not handled automatically: too complicated. *}
consts variant :: "nat * nat list => nat"
recdef (permissive) variant "measure (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
- "variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
+ "variant (x, L) = (if x \<in> set L then variant (Suc x, L) else x)"
consts gcd :: "nat * nat => nat"
recdef gcd "measure (\<lambda>(x, y). x + y)"
--- a/src/HOLCF/IOA/meta_theory/TLS.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy Tue Jun 29 07:55:18 2010 +0200
@@ -86,7 +86,7 @@
"(mkfin (a>>s)) = (a>>(mkfin s))"
-lemmas [simp del] = ex_simps all_simps split_paired_Ex
+lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Tue Jun 29 07:55:18 2010 +0200
@@ -192,7 +192,7 @@
"Traces A == (traces A,asig_of A)"
-lemmas [simp del] = ex_simps all_simps split_paired_Ex
+lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
declare Let_def [simp]
declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
--- a/src/HOLCF/ex/Focus_ex.thy Tue Jun 29 02:18:08 2010 +0100
+++ b/src/HOLCF/ex/Focus_ex.thy Tue Jun 29 07:55:18 2010 +0200
@@ -204,7 +204,7 @@
done
lemma lemma4: "is_g(g) --> def_g(g)"
-apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps")
+apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *})
apply (rule impI)
apply (erule exE)