1.1 --- a/NEWS Tue Jun 29 02:18:08 2010 +0100
1.2 +++ b/NEWS Tue Jun 29 07:55:18 2010 +0200
1.3 @@ -21,6 +21,22 @@
1.4 of ML functions, facts etc. involving split have been retained so far,
1.5 though. INCOMPATIBILITY.
1.6
1.7 +* Dropped old infix syntax "mem" for List.member; use "in set"
1.8 +instead. INCOMPATIBILITY.
1.9 +
1.10 +* Refactoring of code-generation specific operations in List.thy
1.11 +
1.12 + constants
1.13 + null ~> List.null
1.14 +
1.15 + facts
1.16 + mem_iff ~> member_def
1.17 + null_empty ~> null_def
1.18 +
1.19 +INCOMPATIBILITY. Note that these were not suppossed to be used
1.20 +regularly unless for striking reasons; their main purpose was code
1.21 +generation.
1.22 +
1.23 * Some previously unqualified names have been qualified:
1.24
1.25 types
2.1 --- a/src/HOL/Auth/Guard/Guard.thy Tue Jun 29 02:18:08 2010 +0100
2.2 +++ b/src/HOL/Auth/Guard/Guard.thy Tue Jun 29 07:55:18 2010 +0200
2.3 @@ -201,14 +201,16 @@
2.4 lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'"
2.5 by (induct l, auto)
2.6
2.7 -lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
2.8 -by (induct l, auto)
2.9 +lemma mem_cnb_minus: "x \<in> set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
2.10 + by (induct l) auto
2.11
2.12 lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
2.13
2.14 -lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
2.15 +lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
2.16 apply (induct l, auto)
2.17 -by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
2.18 +apply (erule_tac l1=l and x1=x in mem_cnb_minus_substI)
2.19 +apply simp
2.20 +done
2.21
2.22 lemma parts_cnb: "Z:parts (set l) ==>
2.23 cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
2.24 @@ -272,7 +274,7 @@
2.25 apply (clarsimp, blast)
2.26 (* K ~:invKey`Ks *)
2.27 apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))")
2.28 -apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
2.29 +apply (drule_tac x="decrypt' l' K Y" in spec, simp)
2.30 apply (subgoal_tac "Crypt K Y:parts (set l)")
2.31 apply (drule parts_cnb, rotate_tac -1, simp)
2.32 apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
3.1 --- a/src/HOL/Auth/Guard/GuardK.thy Tue Jun 29 02:18:08 2010 +0100
3.2 +++ b/src/HOL/Auth/Guard/GuardK.thy Tue Jun 29 07:55:18 2010 +0200
3.3 @@ -197,12 +197,12 @@
3.4 lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'"
3.5 by (induct l, auto)
3.6
3.7 -lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
3.8 +lemma mem_cnb_minus: "x \<in> set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
3.9 by (induct l, auto)
3.10
3.11 lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
3.12
3.13 -lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x"
3.14 +lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
3.15 apply (induct l, auto)
3.16 by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
3.17
3.18 @@ -268,7 +268,7 @@
3.19 apply (clarsimp, blast)
3.20 (* K ~:invKey`Ks *)
3.21 apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))")
3.22 -apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
3.23 +apply (drule_tac x="decrypt' l' K Y" in spec, simp)
3.24 apply (subgoal_tac "Crypt K Y:parts (set l)")
3.25 apply (drule parts_cnb, rotate_tac -1, simp)
3.26 apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
4.1 --- a/src/HOL/Bali/Trans.thy Tue Jun 29 02:18:08 2010 +0100
4.2 +++ b/src/HOL/Bali/Trans.thy Tue Jun 29 07:55:18 2010 +0200
4.3 @@ -10,7 +10,7 @@
4.4 theory Trans imports Evaln begin
4.5
4.6 definition groundVar :: "var \<Rightarrow> bool" where
4.7 -"groundVar v \<equiv> (case v of
4.8 +"groundVar v \<longleftrightarrow> (case v of
4.9 LVar ln \<Rightarrow> True
4.10 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
4.11 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
4.12 @@ -35,19 +35,15 @@
4.13 qed
4.14
4.15 definition groundExprs :: "expr list \<Rightarrow> bool" where
4.16 -"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
4.17 + "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
4.18
4.19 -consts the_val:: "expr \<Rightarrow> val"
4.20 -primrec
4.21 -"the_val (Lit v) = v"
4.22 +primrec the_val:: "expr \<Rightarrow> val" where
4.23 + "the_val (Lit v) = v"
4.24
4.25 -consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
4.26 -primrec
4.27 -"the_var G s (LVar ln) =(lvar ln (store s),s)"
4.28 -the_var_FVar_def:
4.29 -"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
4.30 -the_var_AVar_def:
4.31 -"the_var G s(a.[i]) =avar G (the_val i) (the_val a) s"
4.32 +primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
4.33 + "the_var G s (LVar ln) =(lvar ln (store s),s)"
4.34 +| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
4.35 +| the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s"
4.36
4.37 lemma the_var_FVar_simp[simp]:
4.38 "the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
5.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy Tue Jun 29 02:18:08 2010 +0100
5.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy Tue Jun 29 07:55:18 2010 +0200
5.3 @@ -425,7 +425,7 @@
5.4
5.5 lemma poly_exp_eq_zero:
5.6 "(poly (p %^ n) = poly ([]::('a::idom) list)) = (poly p = poly [] & n \<noteq> 0)"
5.7 -apply (simp only: fun_eq add: all_simps [symmetric])
5.8 +apply (simp only: fun_eq add: HOL.all_simps [symmetric])
5.9 apply (rule arg_cong [where f = All])
5.10 apply (rule ext)
5.11 apply (induct_tac "n")
6.1 --- a/src/HOL/Extraction/Euclid.thy Tue Jun 29 02:18:08 2010 +0100
6.2 +++ b/src/HOL/Extraction/Euclid.thy Tue Jun 29 07:55:18 2010 +0200
6.3 @@ -44,7 +44,7 @@
6.4 done
6.5
6.6 lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
6.7 - by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps)
6.8 + by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
6.9
6.10 lemma not_prime_ex_mk:
6.11 assumes n: "Suc 0 < n"
7.1 --- a/src/HOL/Extraction/Warshall.thy Tue Jun 29 02:18:08 2010 +0100
7.2 +++ b/src/HOL/Extraction/Warshall.thy Tue Jun 29 07:55:18 2010 +0200
7.3 @@ -38,7 +38,7 @@
7.4 "\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
7.5 by (induct ys) simp+
7.6
7.7 -theorem list_all_scoc [simp]: "list_all P (xs @ [x]) = (P x \<and> list_all P xs)"
7.8 +theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \<longleftrightarrow> P x \<and> list_all P xs"
7.9 by (induct xs, simp+, iprover)
7.10
7.11 theorem list_all_lemma:
8.1 --- a/src/HOL/Import/HOL/HOL4Base.thy Tue Jun 29 02:18:08 2010 +0100
8.2 +++ b/src/HOL/Import/HOL/HOL4Base.thy Tue Jun 29 07:55:18 2010 +0200
8.3 @@ -3130,7 +3130,7 @@
8.4 by (import list EVERY_MEM)
8.5
8.6 lemma EXISTS_MEM: "ALL (P::'a::type => bool) l::'a::type list.
8.7 - list_exists P l = (EX e::'a::type. e mem l & P e)"
8.8 + list_ex P l = (EX e::'a::type. e mem l & P e)"
8.9 by (import list EXISTS_MEM)
8.10
8.11 lemma MEM_APPEND: "ALL (e::'a::type) (l1::'a::type list) l2::'a::type list.
8.12 @@ -3138,15 +3138,15 @@
8.13 by (import list MEM_APPEND)
8.14
8.15 lemma EXISTS_APPEND: "ALL (P::'a::type => bool) (l1::'a::type list) l2::'a::type list.
8.16 - list_exists P (l1 @ l2) = (list_exists P l1 | list_exists P l2)"
8.17 + list_ex P (l1 @ l2) = (list_ex P l1 | list_ex P l2)"
8.18 by (import list EXISTS_APPEND)
8.19
8.20 lemma NOT_EVERY: "ALL (P::'a::type => bool) l::'a::type list.
8.21 - (~ list_all P l) = list_exists (Not o P) l"
8.22 + (~ list_all P l) = list_ex (Not o P) l"
8.23 by (import list NOT_EVERY)
8.24
8.25 lemma NOT_EXISTS: "ALL (P::'a::type => bool) l::'a::type list.
8.26 - (~ list_exists P l) = list_all (Not o P) l"
8.27 + (~ list_ex P l) = list_all (Not o P) l"
8.28 by (import list NOT_EXISTS)
8.29
8.30 lemma MEM_MAP: "ALL (l::'a::type list) (f::'a::type => 'b::type) x::'b::type.
8.31 @@ -3220,7 +3220,7 @@
8.32 lemma EXISTS_CONG: "ALL (l1::'a::type list) (l2::'a::type list) (P::'a::type => bool)
8.33 P'::'a::type => bool.
8.34 l1 = l2 & (ALL x::'a::type. x mem l2 --> P x = P' x) -->
8.35 - list_exists P l1 = list_exists P' l2"
8.36 + list_ex P l1 = list_ex P' l2"
8.37 by (import list EXISTS_CONG)
8.38
8.39 lemma EVERY_CONG: "ALL (l1::'a::type list) (l2::'a::type list) (P::'a::type => bool)
8.40 @@ -4598,7 +4598,7 @@
8.41 SCANR f e (x # l) = f x (hd (SCANR f e l)) # SCANR f e l)"
8.42 by (import rich_list SCANR)
8.43
8.44 -lemma IS_EL_DEF: "ALL (x::'a::type) l::'a::type list. x mem l = list_exists (op = x) l"
8.45 +lemma IS_EL_DEF: "ALL (x::'a::type) l::'a::type list. x mem l = list_ex (op = x) l"
8.46 by (import rich_list IS_EL_DEF)
8.47
8.48 definition AND_EL :: "bool list => bool" where
8.49 @@ -4608,9 +4608,9 @@
8.50 by (import rich_list AND_EL_DEF)
8.51
8.52 definition OR_EL :: "bool list => bool" where
8.53 - "OR_EL == list_exists I"
8.54 -
8.55 -lemma OR_EL_DEF: "OR_EL = list_exists I"
8.56 + "OR_EL == list_ex I"
8.57 +
8.58 +lemma OR_EL_DEF: "OR_EL = list_ex I"
8.59 by (import rich_list OR_EL_DEF)
8.60
8.61 consts
8.62 @@ -4937,7 +4937,7 @@
8.63 by (import rich_list ALL_EL_MAP)
8.64
8.65 lemma SOME_EL_SNOC: "ALL (P::'a::type => bool) (x::'a::type) l::'a::type list.
8.66 - list_exists P (SNOC x l) = (P x | list_exists P l)"
8.67 + list_ex P (SNOC x l) = (P x | list_ex P l)"
8.68 by (import rich_list SOME_EL_SNOC)
8.69
8.70 lemma IS_EL_SNOC: "ALL (y::'a::type) (x::'a::type) l::'a::type list.
8.71 @@ -5080,11 +5080,11 @@
8.72 by (import rich_list ALL_EL_FOLDL)
8.73
8.74 lemma SOME_EL_FOLDR: "ALL (P::'a::type => bool) l::'a::type list.
8.75 - list_exists P l = foldr (%x::'a::type. op | (P x)) l False"
8.76 + list_ex P l = foldr (%x::'a::type. op | (P x)) l False"
8.77 by (import rich_list SOME_EL_FOLDR)
8.78
8.79 lemma SOME_EL_FOLDL: "ALL (P::'a::type => bool) l::'a::type list.
8.80 - list_exists P l = foldl (%(l'::bool) x::'a::type. l' | P x) False l"
8.81 + list_ex P l = foldl (%(l'::bool) x::'a::type. l' | P x) False l"
8.82 by (import rich_list SOME_EL_FOLDL)
8.83
8.84 lemma ALL_EL_FOLDR_MAP: "ALL (x::'a::type => bool) xa::'a::type list.
8.85 @@ -5096,11 +5096,11 @@
8.86 by (import rich_list ALL_EL_FOLDL_MAP)
8.87
8.88 lemma SOME_EL_FOLDR_MAP: "ALL (x::'a::type => bool) xa::'a::type list.
8.89 - list_exists x xa = foldr op | (map x xa) False"
8.90 + list_ex x xa = foldr op | (map x xa) False"
8.91 by (import rich_list SOME_EL_FOLDR_MAP)
8.92
8.93 lemma SOME_EL_FOLDL_MAP: "ALL (x::'a::type => bool) xa::'a::type list.
8.94 - list_exists x xa = foldl op | False (map x xa)"
8.95 + list_ex x xa = foldl op | False (map x xa)"
8.96 by (import rich_list SOME_EL_FOLDL_MAP)
8.97
8.98 lemma FOLDR_FILTER: "ALL (f::'a::type => 'a::type => 'a::type) (e::'a::type)
8.99 @@ -5132,12 +5132,12 @@
8.100 by (import rich_list ASSOC_FOLDL_FLAT)
8.101
8.102 lemma SOME_EL_MAP: "ALL (P::'b::type => bool) (f::'a::type => 'b::type) l::'a::type list.
8.103 - list_exists P (map f l) = list_exists (P o f) l"
8.104 + list_ex P (map f l) = list_ex (P o f) l"
8.105 by (import rich_list SOME_EL_MAP)
8.106
8.107 lemma SOME_EL_DISJ: "ALL (P::'a::type => bool) (Q::'a::type => bool) l::'a::type list.
8.108 - list_exists (%x::'a::type. P x | Q x) l =
8.109 - (list_exists P l | list_exists Q l)"
8.110 + list_ex (%x::'a::type. P x | Q x) l =
8.111 + (list_ex P l | list_ex Q l)"
8.112 by (import rich_list SOME_EL_DISJ)
8.113
8.114 lemma IS_EL_FOLDR: "ALL (x::'a::type) xa::'a::type list.
8.115 @@ -5579,7 +5579,7 @@
8.116 by (import rich_list FLAT_FLAT)
8.117
8.118 lemma SOME_EL_REVERSE: "ALL (P::'a::type => bool) l::'a::type list.
8.119 - list_exists P (rev l) = list_exists P l"
8.120 + list_ex P (rev l) = list_ex P l"
8.121 by (import rich_list SOME_EL_REVERSE)
8.122
8.123 lemma ALL_EL_SEG: "ALL (P::'a::type => bool) l::'a::type list.
8.124 @@ -5621,29 +5621,29 @@
8.125
8.126 lemma SOME_EL_SEG: "ALL (m::nat) (k::nat) l::'a::type list.
8.127 m + k <= length l -->
8.128 - (ALL P::'a::type => bool. list_exists P (SEG m k l) --> list_exists P l)"
8.129 + (ALL P::'a::type => bool. list_ex P (SEG m k l) --> list_ex P l)"
8.130 by (import rich_list SOME_EL_SEG)
8.131
8.132 lemma SOME_EL_FIRSTN: "ALL (m::nat) l::'a::type list.
8.133 m <= length l -->
8.134 - (ALL P::'a::type => bool. list_exists P (FIRSTN m l) --> list_exists P l)"
8.135 + (ALL P::'a::type => bool. list_ex P (FIRSTN m l) --> list_ex P l)"
8.136 by (import rich_list SOME_EL_FIRSTN)
8.137
8.138 lemma SOME_EL_BUTFIRSTN: "ALL (m::nat) l::'a::type list.
8.139 m <= length l -->
8.140 (ALL P::'a::type => bool.
8.141 - list_exists P (BUTFIRSTN m l) --> list_exists P l)"
8.142 + list_ex P (BUTFIRSTN m l) --> list_ex P l)"
8.143 by (import rich_list SOME_EL_BUTFIRSTN)
8.144
8.145 lemma SOME_EL_LASTN: "ALL (m::nat) l::'a::type list.
8.146 m <= length l -->
8.147 - (ALL P::'a::type => bool. list_exists P (LASTN m l) --> list_exists P l)"
8.148 + (ALL P::'a::type => bool. list_ex P (LASTN m l) --> list_ex P l)"
8.149 by (import rich_list SOME_EL_LASTN)
8.150
8.151 lemma SOME_EL_BUTLASTN: "ALL (m::nat) l::'a::type list.
8.152 m <= length l -->
8.153 (ALL P::'a::type => bool.
8.154 - list_exists P (BUTLASTN m l) --> list_exists P l)"
8.155 + list_ex P (BUTLASTN m l) --> list_ex P l)"
8.156 by (import rich_list SOME_EL_BUTLASTN)
8.157
8.158 lemma IS_EL_REVERSE: "ALL (x::'a::type) l::'a::type list. x mem rev l = x mem l"
8.159 @@ -5657,7 +5657,7 @@
8.160 n + m <= length l --> (ALL x::'a::type. x mem SEG n m l --> x mem l)"
8.161 by (import rich_list IS_EL_SEG)
8.162
8.163 -lemma IS_EL_SOME_EL: "ALL (x::'a::type) l::'a::type list. x mem l = list_exists (op = x) l"
8.164 +lemma IS_EL_SOME_EL: "ALL (x::'a::type) l::'a::type list. x mem l = list_ex (op = x) l"
8.165 by (import rich_list IS_EL_SOME_EL)
8.166
8.167 lemma IS_EL_FIRSTN: "ALL (x::nat) xa::'a::type list.
9.1 --- a/src/HOL/Import/HOL4Compat.thy Tue Jun 29 02:18:08 2010 +0100
9.2 +++ b/src/HOL/Import/HOL4Compat.thy Tue Jun 29 07:55:18 2010 +0200
9.3 @@ -6,6 +6,7 @@
9.4 imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum
9.5 begin
9.6
9.7 +abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
9.8 no_notation differentiable (infixl "differentiable" 60)
9.9 no_notation sums (infixr "sums" 80)
9.10
9.11 @@ -326,8 +327,8 @@
9.12 qed
9.13 qed
9.14
9.15 -lemma NULL_DEF: "(null [] = True) & (!h t. null (h # t) = False)"
9.16 - by simp
9.17 +lemma NULL_DEF: "(List.null [] = True) & (!h t. List.null (h # t) = False)"
9.18 + by (simp add: null_def)
9.19
9.20 definition sum :: "nat list \<Rightarrow> nat" where
9.21 "sum l == foldr (op +) l 0"
9.22 @@ -347,8 +348,8 @@
9.23 lemma MAP: "(!f. map f [] = []) & (!f h t. map f (h#t) = f h#map f t)"
9.24 by simp
9.25
9.26 -lemma MEM: "(!x. x mem [] = False) & (!x h t. x mem (h#t) = ((x = h) | x mem t))"
9.27 - by auto
9.28 +lemma MEM: "(!x. List.member [] x = False) & (!x h t. List.member (h#t) x = ((x = h) | List.member t x))"
9.29 + by (simp add: member_def)
9.30
9.31 lemma FILTER: "(!P. filter P [] = []) & (!P h t.
9.32 filter P (h#t) = (if P h then h#filter P t else filter P t))"
9.33 @@ -373,15 +374,7 @@
9.34 lemma EVERY_DEF: "(!P. list_all P [] = True) & (!P h t. list_all P (h#t) = (P h & list_all P t))"
9.35 by simp
9.36
9.37 -consts
9.38 - list_exists :: "['a \<Rightarrow> bool,'a list] \<Rightarrow> bool"
9.39 -
9.40 -primrec
9.41 - list_exists_Nil: "list_exists P Nil = False"
9.42 - list_exists_Cons: "list_exists P (x#xs) = (if P x then True else list_exists P xs)"
9.43 -
9.44 -lemma list_exists_DEF: "(!P. list_exists P [] = False) &
9.45 - (!P h t. list_exists P (h#t) = (P h | list_exists P t))"
9.46 +lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
9.47 by simp
9.48
9.49 consts
10.1 --- a/src/HOL/Induct/Term.thy Tue Jun 29 02:18:08 2010 +0100
10.2 +++ b/src/HOL/Induct/Term.thy Tue Jun 29 07:55:18 2010 +0200
10.3 @@ -13,18 +13,12 @@
10.4
10.5 text {* \medskip Substitution function on terms *}
10.6
10.7 -consts
10.8 - subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
10.9 - subst_term_list ::
10.10 - "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
10.11 -
10.12 -primrec
10.13 +primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
10.14 + and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
10.15 "subst_term f (Var a) = f a"
10.16 - "subst_term f (App b ts) = App b (subst_term_list f ts)"
10.17 -
10.18 - "subst_term_list f [] = []"
10.19 - "subst_term_list f (t # ts) =
10.20 - subst_term f t # subst_term_list f ts"
10.21 +| "subst_term f (App b ts) = App b (subst_term_list f ts)"
10.22 +| "subst_term_list f [] = []"
10.23 +| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
10.24
10.25
10.26 text {* \medskip A simple theorem about composition of substitutions *}
10.27 @@ -41,9 +35,9 @@
10.28
10.29 lemma
10.30 assumes var: "!!v. P (Var v)"
10.31 - and app: "!!f ts. list_all P ts ==> P (App f ts)"
10.32 + and app: "!!f ts. (\<forall>t \<in> set ts. P t) ==> P (App f ts)"
10.33 shows term_induct2: "P t"
10.34 - and "list_all P ts"
10.35 + and "\<forall>t \<in> set ts. P t"
10.36 apply (induct t and ts)
10.37 apply (rule var)
10.38 apply (rule app)
11.1 --- a/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Jun 29 02:18:08 2010 +0100
11.2 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Jun 29 07:55:18 2010 +0200
11.3 @@ -10,17 +10,14 @@
11.4 Var 'a
11.5 | App 'b "('a, 'b) term list"
11.6
11.7 -consts
11.8 - subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
11.9 - subst_term_list ::
11.10 - "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
11.11 +primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
11.12 + subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
11.13 + "subst_term f (Var a) = f a"
11.14 +| "subst_term f (App b ts) = App b (subst_term_list f ts)"
11.15 +| "subst_term_list f [] = []"
11.16 +| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
11.17
11.18 -primrec (subst)
11.19 - "subst_term f (Var a) = f a"
11.20 - "subst_term f (App b ts) = App b (subst_term_list f ts)"
11.21 - "subst_term_list f [] = []"
11.22 - "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
11.23 -
11.24 +lemmas subst_simps = subst_term_subst_term_list.simps
11.25
11.26 text {*
11.27 \medskip A simple lemma about composition of substitutions.
11.28 @@ -44,13 +41,13 @@
11.29 next
11.30 fix b ts assume "?Q ts"
11.31 then show "?P (App b ts)"
11.32 - by (simp only: subst.simps)
11.33 + by (simp only: subst_simps)
11.34 next
11.35 show "?Q []" by simp
11.36 next
11.37 fix t ts
11.38 assume "?P t" "?Q ts" then show "?Q (t # ts)"
11.39 - by (simp only: subst.simps)
11.40 + by (simp only: subst_simps)
11.41 qed
11.42 qed
11.43
11.44 @@ -59,18 +56,18 @@
11.45
11.46 theorem term_induct' [case_names Var App]:
11.47 assumes var: "!!a. P (Var a)"
11.48 - and app: "!!b ts. list_all P ts ==> P (App b ts)"
11.49 + and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
11.50 shows "P t"
11.51 proof (induct t)
11.52 fix a show "P (Var a)" by (rule var)
11.53 next
11.54 - fix b t ts assume "list_all P ts"
11.55 + fix b t ts assume "\<forall>t \<in> set ts. P t"
11.56 then show "P (App b ts)" by (rule app)
11.57 next
11.58 - show "list_all P []" by simp
11.59 + show "\<forall>t \<in> set []. P t" by simp
11.60 next
11.61 - fix t ts assume "P t" "list_all P ts"
11.62 - then show "list_all P (t # ts)" by simp
11.63 + fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"
11.64 + then show "\<forall>t' \<in> set (t # ts). P t'" by simp
11.65 qed
11.66
11.67 lemma
12.1 --- a/src/HOL/Library/AssocList.thy Tue Jun 29 02:18:08 2010 +0100
12.2 +++ b/src/HOL/Library/AssocList.thy Tue Jun 29 07:55:18 2010 +0200
12.3 @@ -674,8 +674,8 @@
12.4 by (rule mapping_eqI) simp
12.5
12.6 lemma is_empty_Mapping [code]:
12.7 - "Mapping.is_empty (Mapping xs) \<longleftrightarrow> null xs"
12.8 - by (cases xs) (simp_all add: is_empty_def)
12.9 + "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
12.10 + by (cases xs) (simp_all add: is_empty_def null_def)
12.11
12.12 lemma update_Mapping [code]:
12.13 "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
13.1 --- a/src/HOL/Library/Dlist.thy Tue Jun 29 02:18:08 2010 +0100
13.2 +++ b/src/HOL/Library/Dlist.thy Tue Jun 29 07:55:18 2010 +0200
13.3 @@ -122,7 +122,7 @@
13.4 next
13.5 case (insert x xs)
13.6 then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
13.7 - by (simp_all add: member_def mem_iff)
13.8 + by (simp_all add: member_def List.member_def)
13.9 with insrt have "P (insert x (Dlist xs))" .
13.10 with insert show ?case by (simp add: insert_def distinct_remdups_id)
13.11 qed
13.12 @@ -144,7 +144,7 @@
13.13 case (Cons x xs)
13.14 with dxs distinct have "\<not> member (Dlist xs) x"
13.15 and "dxs = insert x (Dlist xs)"
13.16 - by (simp_all add: member_def mem_iff insert_def distinct_remdups_id)
13.17 + by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
13.18 with insert show P .
13.19 qed
13.20 qed
13.21 @@ -205,7 +205,7 @@
13.22
13.23 lemma is_empty_Set [code]:
13.24 "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
13.25 - by (simp add: null_def null_empty member_set)
13.26 + by (simp add: null_def List.null_def member_set)
13.27
13.28 lemma bot_code [code]:
13.29 "bot = Set empty"
14.1 --- a/src/HOL/Library/Enum.thy Tue Jun 29 02:18:08 2010 +0100
14.2 +++ b/src/HOL/Library/Enum.thy Tue Jun 29 07:55:18 2010 +0200
14.3 @@ -49,8 +49,8 @@
14.4 lemma order_fun [code]:
14.5 fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
14.6 shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
14.7 - and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
14.8 - by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def order_less_le)
14.9 + and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"
14.10 + by (simp_all add: list_all_iff list_ex_iff enum_all expand_fun_eq le_fun_def order_less_le)
14.11
14.12
14.13 subsection {* Quantifiers *}
14.14 @@ -58,8 +58,8 @@
14.15 lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
14.16 by (simp add: list_all_iff enum_all)
14.17
14.18 -lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
14.19 - by (simp add: list_all_iff enum_all)
14.20 +lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
14.21 + by (simp add: list_ex_iff enum_all)
14.22
14.23
14.24 subsection {* Default instances *}
15.1 --- a/src/HOL/Library/Executable_Set.thy Tue Jun 29 02:18:08 2010 +0100
15.2 +++ b/src/HOL/Library/Executable_Set.thy Tue Jun 29 07:55:18 2010 +0200
15.3 @@ -50,9 +50,9 @@
15.4 by simp
15.5
15.6 lemma [code]:
15.7 - "x \<in> Set xs \<longleftrightarrow> member xs x"
15.8 - "x \<in> Coset xs \<longleftrightarrow> \<not> member xs x"
15.9 - by (simp_all add: mem_iff)
15.10 + "x \<in> Set xs \<longleftrightarrow> List.member xs x"
15.11 + "x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x"
15.12 + by (simp_all add: member_def)
15.13
15.14 definition is_empty :: "'a set \<Rightarrow> bool" where
15.15 [simp]: "is_empty A \<longleftrightarrow> A = {}"
15.16 @@ -85,8 +85,8 @@
15.17 *}
15.18
15.19 lemma is_empty_Set [code]:
15.20 - "is_empty (Set xs) \<longleftrightarrow> null xs"
15.21 - by (simp add: empty_null)
15.22 + "is_empty (Set xs) \<longleftrightarrow> List.null xs"
15.23 + by (simp add: null_def)
15.24
15.25 lemma empty_Set [code]:
15.26 "empty = Set []"
15.27 @@ -112,11 +112,11 @@
15.28
15.29 lemma Ball_Set [code]:
15.30 "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
15.31 - by (simp add: ball_set)
15.32 + by (simp add: list_all_iff)
15.33
15.34 lemma Bex_Set [code]:
15.35 "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
15.36 - by (simp add: bex_set)
15.37 + by (simp add: list_ex_iff)
15.38
15.39 lemma card_Set [code]:
15.40 "card (Set xs) = length (remdups xs)"
16.1 --- a/src/HOL/Library/Fset.thy Tue Jun 29 02:18:08 2010 +0100
16.2 +++ b/src/HOL/Library/Fset.thy Tue Jun 29 07:55:18 2010 +0200
16.3 @@ -51,7 +51,7 @@
16.4 lemma member_code [code]:
16.5 "member (Set xs) = List.member xs"
16.6 "member (Coset xs) = Not \<circ> List.member xs"
16.7 - by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def)
16.8 + by (simp_all add: expand_fun_eq member_def fun_Compl_def bool_Compl_def)
16.9
16.10 lemma member_image_UNIV [simp]:
16.11 "member ` UNIV = UNIV"
16.12 @@ -141,7 +141,7 @@
16.13 [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
16.14
16.15 lemma is_empty_Set [code]:
16.16 - "is_empty (Set xs) \<longleftrightarrow> null xs"
16.17 + "is_empty (Set xs) \<longleftrightarrow> List.null xs"
16.18 by (simp add: is_empty_set)
16.19
16.20 lemma empty_Set [code]:
16.21 @@ -188,14 +188,14 @@
16.22
16.23 lemma forall_Set [code]:
16.24 "forall P (Set xs) \<longleftrightarrow> list_all P xs"
16.25 - by (simp add: Set_def ball_set)
16.26 + by (simp add: Set_def list_all_iff)
16.27
16.28 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
16.29 [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
16.30
16.31 lemma exists_Set [code]:
16.32 "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
16.33 - by (simp add: Set_def bex_set)
16.34 + by (simp add: Set_def list_ex_iff)
16.35
16.36 definition card :: "'a fset \<Rightarrow> nat" where
16.37 [simp]: "card A = Finite_Set.card (member A)"
17.1 --- a/src/HOL/Library/More_Set.thy Tue Jun 29 02:18:08 2010 +0100
17.2 +++ b/src/HOL/Library/More_Set.thy Tue Jun 29 07:55:18 2010 +0200
17.3 @@ -37,16 +37,8 @@
17.4 subsection {* Basic set operations *}
17.5
17.6 lemma is_empty_set:
17.7 - "is_empty (set xs) \<longleftrightarrow> null xs"
17.8 - by (simp add: is_empty_def null_empty)
17.9 -
17.10 -lemma ball_set:
17.11 - "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
17.12 - by (rule list_ball_code)
17.13 -
17.14 -lemma bex_set:
17.15 - "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
17.16 - by (rule list_bex_code)
17.17 + "is_empty (set xs) \<longleftrightarrow> List.null xs"
17.18 + by (simp add: is_empty_def null_def)
17.19
17.20 lemma empty_set:
17.21 "{} = set []"
18.1 --- a/src/HOL/Library/Univ_Poly.thy Tue Jun 29 02:18:08 2010 +0100
18.2 +++ b/src/HOL/Library/Univ_Poly.thy Tue Jun 29 07:55:18 2010 +0200
18.3 @@ -407,7 +407,7 @@
18.4
18.5 lemma (in idom) poly_exp_eq_zero[simp]:
18.6 "(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
18.7 -apply (simp only: fun_eq add: all_simps [symmetric])
18.8 +apply (simp only: fun_eq add: HOL.all_simps [symmetric])
18.9 apply (rule arg_cong [where f = All])
18.10 apply (rule ext)
18.11 apply (induct n)
19.1 --- a/src/HOL/Library/positivstellensatz.ML Tue Jun 29 02:18:08 2010 +0100
19.2 +++ b/src/HOL/Library/positivstellensatz.ML Tue Jun 29 07:55:18 2010 +0200
19.3 @@ -228,7 +228,7 @@
19.4 val prenex_simps =
19.5 map (fn th => th RS sym)
19.6 ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @
19.7 - @{thms "all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
19.8 + @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
19.9
19.10 val real_abs_thms1 = @{lemma
19.11 "((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and
20.1 --- a/src/HOL/List.thy Tue Jun 29 02:18:08 2010 +0100
20.2 +++ b/src/HOL/List.thy Tue Jun 29 07:55:18 2010 +0200
20.3 @@ -2352,6 +2352,22 @@
20.4 case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
20.5 qed
20.6
20.7 +lemma rev_foldl_cons [code]:
20.8 + "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
20.9 +proof (induct xs)
20.10 + case Nil then show ?case by simp
20.11 +next
20.12 + case Cons
20.13 + {
20.14 + fix x xs ys
20.15 + have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
20.16 + = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
20.17 + by (induct xs arbitrary: ys) auto
20.18 + }
20.19 + note aux = this
20.20 + show ?case by (induct xs) (auto simp add: Cons aux)
20.21 +qed
20.22 +
20.23
20.24 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
20.25
20.26 @@ -2509,120 +2525,6 @@
20.27 by (simp add: sup_commute)
20.28
20.29
20.30 -subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
20.31 -
20.32 -lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
20.33 -by (induct xs) (simp_all add:add_assoc)
20.34 -
20.35 -lemma listsum_rev [simp]:
20.36 - fixes xs :: "'a\<Colon>comm_monoid_add list"
20.37 - shows "listsum (rev xs) = listsum xs"
20.38 -by (induct xs) (simp_all add:add_ac)
20.39 -
20.40 -lemma listsum_map_remove1:
20.41 -fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
20.42 -shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
20.43 -by (induct xs)(auto simp add:add_ac)
20.44 -
20.45 -lemma list_size_conv_listsum:
20.46 - "list_size f xs = listsum (map f xs) + size xs"
20.47 -by(induct xs) auto
20.48 -
20.49 -lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
20.50 -by (induct xs) auto
20.51 -
20.52 -lemma length_concat: "length (concat xss) = listsum (map length xss)"
20.53 -by (induct xss) simp_all
20.54 -
20.55 -lemma listsum_map_filter:
20.56 - fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
20.57 - assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
20.58 - shows "listsum (map f (filter P xs)) = listsum (map f xs)"
20.59 -using assms by (induct xs) auto
20.60 -
20.61 -text{* For efficient code generation ---
20.62 - @{const listsum} is not tail recursive but @{const foldl} is. *}
20.63 -lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
20.64 -by(simp add:listsum_foldr foldl_foldr1)
20.65 -
20.66 -lemma distinct_listsum_conv_Setsum:
20.67 - "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
20.68 -by (induct xs) simp_all
20.69 -
20.70 -lemma listsum_eq_0_nat_iff_nat[simp]:
20.71 - "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
20.72 -by(simp add: listsum)
20.73 -
20.74 -lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)"
20.75 -apply(induct ns arbitrary: k)
20.76 - apply simp
20.77 -apply(fastsimp simp add:nth_Cons split: nat.split)
20.78 -done
20.79 -
20.80 -lemma listsum_update_nat: "k<size ns \<Longrightarrow>
20.81 - listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"
20.82 -apply(induct ns arbitrary:k)
20.83 - apply (auto split:nat.split)
20.84 -apply(drule elem_le_listsum_nat)
20.85 -apply arith
20.86 -done
20.87 -
20.88 -text{* Some syntactic sugar for summing a function over a list: *}
20.89 -
20.90 -syntax
20.91 - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
20.92 -syntax (xsymbols)
20.93 - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
20.94 -syntax (HTML output)
20.95 - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
20.96 -
20.97 -translations -- {* Beware of argument permutation! *}
20.98 - "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
20.99 - "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
20.100 -
20.101 -lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
20.102 - by (induct xs) (simp_all add: left_distrib)
20.103 -
20.104 -lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
20.105 - by (induct xs) (simp_all add: left_distrib)
20.106 -
20.107 -text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
20.108 -lemma uminus_listsum_map:
20.109 - fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
20.110 - shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
20.111 -by (induct xs) simp_all
20.112 -
20.113 -lemma listsum_addf:
20.114 - fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
20.115 - shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
20.116 -by (induct xs) (simp_all add: algebra_simps)
20.117 -
20.118 -lemma listsum_subtractf:
20.119 - fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
20.120 - shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
20.121 -by (induct xs) simp_all
20.122 -
20.123 -lemma listsum_const_mult:
20.124 - fixes f :: "'a \<Rightarrow> 'b::semiring_0"
20.125 - shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
20.126 -by (induct xs, simp_all add: algebra_simps)
20.127 -
20.128 -lemma listsum_mult_const:
20.129 - fixes f :: "'a \<Rightarrow> 'b::semiring_0"
20.130 - shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
20.131 -by (induct xs, simp_all add: algebra_simps)
20.132 -
20.133 -lemma listsum_abs:
20.134 - fixes xs :: "'a::ordered_ab_group_add_abs list"
20.135 - shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
20.136 -by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
20.137 -
20.138 -lemma listsum_mono:
20.139 - fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"
20.140 - 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)"
20.141 -by (induct xs, simp, simp add: add_mono)
20.142 -
20.143 -
20.144 subsubsection {* @{text upt} *}
20.145
20.146 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
20.147 @@ -2961,6 +2863,137 @@
20.148 qed
20.149
20.150
20.151 +subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
20.152 +
20.153 +lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
20.154 +by (induct xs) (simp_all add:add_assoc)
20.155 +
20.156 +lemma listsum_rev [simp]:
20.157 + fixes xs :: "'a\<Colon>comm_monoid_add list"
20.158 + shows "listsum (rev xs) = listsum xs"
20.159 +by (induct xs) (simp_all add:add_ac)
20.160 +
20.161 +lemma listsum_map_remove1:
20.162 +fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
20.163 +shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
20.164 +by (induct xs)(auto simp add:add_ac)
20.165 +
20.166 +lemma list_size_conv_listsum:
20.167 + "list_size f xs = listsum (map f xs) + size xs"
20.168 +by(induct xs) auto
20.169 +
20.170 +lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
20.171 +by (induct xs) auto
20.172 +
20.173 +lemma length_concat: "length (concat xss) = listsum (map length xss)"
20.174 +by (induct xss) simp_all
20.175 +
20.176 +lemma listsum_map_filter:
20.177 + fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
20.178 + assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
20.179 + shows "listsum (map f (filter P xs)) = listsum (map f xs)"
20.180 +using assms by (induct xs) auto
20.181 +
20.182 +text{* For efficient code generation ---
20.183 + @{const listsum} is not tail recursive but @{const foldl} is. *}
20.184 +lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
20.185 +by(simp add:listsum_foldr foldl_foldr1)
20.186 +
20.187 +lemma distinct_listsum_conv_Setsum:
20.188 + "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
20.189 +by (induct xs) simp_all
20.190 +
20.191 +lemma listsum_eq_0_nat_iff_nat[simp]:
20.192 + "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
20.193 +by(simp add: listsum)
20.194 +
20.195 +lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)"
20.196 +apply(induct ns arbitrary: k)
20.197 + apply simp
20.198 +apply(fastsimp simp add:nth_Cons split: nat.split)
20.199 +done
20.200 +
20.201 +lemma listsum_update_nat: "k<size ns \<Longrightarrow>
20.202 + listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"
20.203 +apply(induct ns arbitrary:k)
20.204 + apply (auto split:nat.split)
20.205 +apply(drule elem_le_listsum_nat)
20.206 +apply arith
20.207 +done
20.208 +
20.209 +text{* Some syntactic sugar for summing a function over a list: *}
20.210 +
20.211 +syntax
20.212 + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
20.213 +syntax (xsymbols)
20.214 + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
20.215 +syntax (HTML output)
20.216 + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
20.217 +
20.218 +translations -- {* Beware of argument permutation! *}
20.219 + "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
20.220 + "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
20.221 +
20.222 +lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
20.223 + by (induct xs) (simp_all add: left_distrib)
20.224 +
20.225 +lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
20.226 + by (induct xs) (simp_all add: left_distrib)
20.227 +
20.228 +text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
20.229 +lemma uminus_listsum_map:
20.230 + fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
20.231 + shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
20.232 +by (induct xs) simp_all
20.233 +
20.234 +lemma listsum_addf:
20.235 + fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
20.236 + shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
20.237 +by (induct xs) (simp_all add: algebra_simps)
20.238 +
20.239 +lemma listsum_subtractf:
20.240 + fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
20.241 + shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
20.242 +by (induct xs) simp_all
20.243 +
20.244 +lemma listsum_const_mult:
20.245 + fixes f :: "'a \<Rightarrow> 'b::semiring_0"
20.246 + shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
20.247 +by (induct xs, simp_all add: algebra_simps)
20.248 +
20.249 +lemma listsum_mult_const:
20.250 + fixes f :: "'a \<Rightarrow> 'b::semiring_0"
20.251 + shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
20.252 +by (induct xs, simp_all add: algebra_simps)
20.253 +
20.254 +lemma listsum_abs:
20.255 + fixes xs :: "'a::ordered_ab_group_add_abs list"
20.256 + shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
20.257 +by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
20.258 +
20.259 +lemma listsum_mono:
20.260 + fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"
20.261 + 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)"
20.262 +by (induct xs, simp, simp add: add_mono)
20.263 +
20.264 +lemma listsum_distinct_conv_setsum_set:
20.265 + "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
20.266 + by (induct xs) simp_all
20.267 +
20.268 +lemma interv_listsum_conv_setsum_set_nat:
20.269 + "listsum (map f [m..<n]) = setsum f (set [m..<n])"
20.270 + by (simp add: listsum_distinct_conv_setsum_set)
20.271 +
20.272 +lemma interv_listsum_conv_setsum_set_int:
20.273 + "listsum (map f [k..l]) = setsum f (set [k..l])"
20.274 + by (simp add: listsum_distinct_conv_setsum_set)
20.275 +
20.276 +text {* General equivalence between @{const listsum} and @{const setsum} *}
20.277 +lemma listsum_setsum_nth:
20.278 + "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
20.279 + using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
20.280 +
20.281 +
20.282 subsubsection {* @{const insert} *}
20.283
20.284 lemma in_set_insert [simp]:
20.285 @@ -4513,9 +4546,266 @@
20.286 *)
20.287
20.288
20.289 -subsection {* Code generator *}
20.290 -
20.291 -subsubsection {* Setup *}
20.292 +subsection {* Code generation *}
20.293 +
20.294 +subsubsection {* Counterparts for set-related operations *}
20.295 +
20.296 +definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
20.297 + [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
20.298 +
20.299 +text {*
20.300 + Only use @{text member} for generating executable code. Otherwise use
20.301 + @{prop "x \<in> set xs"} instead --- it is much easier to reason about.
20.302 +*}
20.303 +
20.304 +lemma member_set:
20.305 + "member = set"
20.306 + by (simp add: expand_fun_eq member_def mem_def)
20.307 +
20.308 +lemma member_rec [code]:
20.309 + "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
20.310 + "member [] y \<longleftrightarrow> False"
20.311 + by (auto simp add: member_def)
20.312 +
20.313 +lemma in_set_member [code_unfold]:
20.314 + "x \<in> set xs \<longleftrightarrow> member xs x"
20.315 + by (simp add: member_def)
20.316 +
20.317 +declare INFI_def [code_unfold]
20.318 +declare SUPR_def [code_unfold]
20.319 +
20.320 +declare set_map [symmetric, code_unfold]
20.321 +
20.322 +definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
20.323 + list_all_iff [code_post]: "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
20.324 +
20.325 +definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
20.326 + list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
20.327 +
20.328 +text {*
20.329 + Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
20.330 + over @{const list_all} and @{const list_ex} in specifications.
20.331 +*}
20.332 +
20.333 +lemma list_all_simps [simp, code]:
20.334 + "list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs"
20.335 + "list_all P [] \<longleftrightarrow> True"
20.336 + by (simp_all add: list_all_iff)
20.337 +
20.338 +lemma list_ex_simps [simp, code]:
20.339 + "list_ex P (x # xs) \<longleftrightarrow> P x \<or> list_ex P xs"
20.340 + "list_ex P [] \<longleftrightarrow> False"
20.341 + by (simp_all add: list_ex_iff)
20.342 +
20.343 +lemma Ball_set_list_all [code_unfold]:
20.344 + "Ball (set xs) P \<longleftrightarrow> list_all P xs"
20.345 + by (simp add: list_all_iff)
20.346 +
20.347 +lemma Bex_set_list_ex [code_unfold]:
20.348 + "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
20.349 + by (simp add: list_ex_iff)
20.350 +
20.351 +lemma list_all_append [simp]:
20.352 + "list_all P (xs @ ys) \<longleftrightarrow> list_all P xs \<and> list_all P ys"
20.353 + by (auto simp add: list_all_iff)
20.354 +
20.355 +lemma list_ex_append [simp]:
20.356 + "list_ex P (xs @ ys) \<longleftrightarrow> list_ex P xs \<or> list_ex P ys"
20.357 + by (auto simp add: list_ex_iff)
20.358 +
20.359 +lemma list_all_rev [simp]:
20.360 + "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
20.361 + by (simp add: list_all_iff)
20.362 +
20.363 +lemma list_ex_rev [simp]:
20.364 + "list_ex P (rev xs) \<longleftrightarrow> list_ex P xs"
20.365 + by (simp add: list_ex_iff)
20.366 +
20.367 +lemma list_all_length:
20.368 + "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
20.369 + by (auto simp add: list_all_iff set_conv_nth)
20.370 +
20.371 +lemma list_ex_length:
20.372 + "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
20.373 + by (auto simp add: list_ex_iff set_conv_nth)
20.374 +
20.375 +lemma list_all_cong [fundef_cong]:
20.376 + "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
20.377 + by (simp add: list_all_iff)
20.378 +
20.379 +lemma list_any_cong [fundef_cong]:
20.380 + "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
20.381 + by (simp add: list_ex_iff)
20.382 +
20.383 +text {* Bounded quantification and summation over nats. *}
20.384 +
20.385 +lemma atMost_upto [code_unfold]:
20.386 + "{..n} = set [0..<Suc n]"
20.387 + by auto
20.388 +
20.389 +lemma atLeast_upt [code_unfold]:
20.390 + "{..<n} = set [0..<n]"
20.391 + by auto
20.392 +
20.393 +lemma greaterThanLessThan_upt [code_unfold]:
20.394 + "{n<..<m} = set [Suc n..<m]"
20.395 + by auto
20.396 +
20.397 +lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
20.398 +
20.399 +lemma greaterThanAtMost_upt [code_unfold]:
20.400 + "{n<..m} = set [Suc n..<Suc m]"
20.401 + by auto
20.402 +
20.403 +lemma atLeastAtMost_upt [code_unfold]:
20.404 + "{n..m} = set [n..<Suc m]"
20.405 + by auto
20.406 +
20.407 +lemma all_nat_less_eq [code_unfold]:
20.408 + "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
20.409 + by auto
20.410 +
20.411 +lemma ex_nat_less_eq [code_unfold]:
20.412 + "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
20.413 + by auto
20.414 +
20.415 +lemma all_nat_less [code_unfold]:
20.416 + "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
20.417 + by auto
20.418 +
20.419 +lemma ex_nat_less [code_unfold]:
20.420 + "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
20.421 + by auto
20.422 +
20.423 +lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
20.424 + "setsum f (set [m..<n]) = listsum (map f [m..<n])"
20.425 + by (simp add: interv_listsum_conv_setsum_set_nat)
20.426 +
20.427 +text {* Summation over ints. *}
20.428 +
20.429 +lemma greaterThanLessThan_upto [code_unfold]:
20.430 + "{i<..<j::int} = set [i+1..j - 1]"
20.431 +by auto
20.432 +
20.433 +lemma atLeastLessThan_upto [code_unfold]:
20.434 + "{i..<j::int} = set [i..j - 1]"
20.435 +by auto
20.436 +
20.437 +lemma greaterThanAtMost_upto [code_unfold]:
20.438 + "{i<..j::int} = set [i+1..j]"
20.439 +by auto
20.440 +
20.441 +lemmas atLeastAtMost_upto [code_unfold] = set_upto [symmetric]
20.442 +
20.443 +lemma setsum_set_upto_conv_listsum_int [code_unfold]:
20.444 + "setsum f (set [i..j::int]) = listsum (map f [i..j])"
20.445 + by (simp add: interv_listsum_conv_setsum_set_int)
20.446 +
20.447 +
20.448 +subsubsection {* Optimizing by rewriting *}
20.449 +
20.450 +definition null :: "'a list \<Rightarrow> bool" where
20.451 + [code_post]: "null xs \<longleftrightarrow> xs = []"
20.452 +
20.453 +text {*
20.454 + Efficient emptyness check is implemented by @{const null}.
20.455 +*}
20.456 +
20.457 +lemma null_rec [code]:
20.458 + "null (x # xs) \<longleftrightarrow> False"
20.459 + "null [] \<longleftrightarrow> True"
20.460 + by (simp_all add: null_def)
20.461 +
20.462 +lemma eq_Nil_null [code_unfold]:
20.463 + "xs = [] \<longleftrightarrow> null xs"
20.464 + by (simp add: null_def)
20.465 +
20.466 +lemma equal_Nil_null [code_unfold]:
20.467 + "eq_class.eq xs [] \<longleftrightarrow> null xs"
20.468 + by (simp add: eq eq_Nil_null)
20.469 +
20.470 +definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
20.471 + [code_post]: "maps f xs = concat (map f xs)"
20.472 +
20.473 +definition map_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
20.474 + [code_post]: "map_filter f xs = map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> None) xs)"
20.475 +
20.476 +text {*
20.477 + Operations @{const maps} and @{const map_filter} avoid
20.478 + intermediate lists on execution -- do not use for proving.
20.479 +*}
20.480 +
20.481 +lemma maps_simps [code]:
20.482 + "maps f (x # xs) = f x @ maps f xs"
20.483 + "maps f [] = []"
20.484 + by (simp_all add: maps_def)
20.485 +
20.486 +lemma map_filter_simps [code]:
20.487 + "map_filter f (x # xs) = (case f x of None \<Rightarrow> map_filter f xs | Some y \<Rightarrow> y # map_filter f xs)"
20.488 + "map_filter f [] = []"
20.489 + by (simp_all add: map_filter_def split: option.split)
20.490 +
20.491 +lemma concat_map_maps [code_unfold]:
20.492 + "concat (map f xs) = maps f xs"
20.493 + by (simp add: maps_def)
20.494 +
20.495 +lemma map_filter_map_filter [code_unfold]:
20.496 + "map f (filter P xs) = map_filter (\<lambda>x. if P x then Some (f x) else None) xs"
20.497 + by (simp add: map_filter_def)
20.498 +
20.499 +text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
20.500 +and similiarly for @{text"\<exists>"}. *}
20.501 +
20.502 +definition all_interval_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
20.503 + "all_interval_nat P i j \<longleftrightarrow> (\<forall>n \<in> {i..<j}. P n)"
20.504 +
20.505 +lemma [code]:
20.506 + "all_interval_nat P i j \<longleftrightarrow> i \<ge> j \<or> P i \<and> all_interval_nat P (Suc i) j"
20.507 +proof -
20.508 + have *: "\<And>n. P i \<Longrightarrow> \<forall>n\<in>{Suc i..<j}. P n \<Longrightarrow> i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n"
20.509 + proof -
20.510 + fix n
20.511 + assume "P i" "\<forall>n\<in>{Suc i..<j}. P n" "i \<le> n" "n < j"
20.512 + then show "P n" by (cases "n = i") simp_all
20.513 + qed
20.514 + show ?thesis by (auto simp add: all_interval_nat_def intro: *)
20.515 +qed
20.516 +
20.517 +lemma list_all_iff_all_interval_nat [code_unfold]:
20.518 + "list_all P [i..<j] \<longleftrightarrow> all_interval_nat P i j"
20.519 + by (simp add: list_all_iff all_interval_nat_def)
20.520 +
20.521 +lemma list_ex_iff_not_all_inverval_nat [code_unfold]:
20.522 + "list_ex P [i..<j] \<longleftrightarrow> \<not> (all_interval_nat (Not \<circ> P) i j)"
20.523 + by (simp add: list_ex_iff all_interval_nat_def)
20.524 +
20.525 +definition all_interval_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
20.526 + "all_interval_int P i j \<longleftrightarrow> (\<forall>k \<in> {i..j}. P k)"
20.527 +
20.528 +lemma [code]:
20.529 + "all_interval_int P i j \<longleftrightarrow> i > j \<or> P i \<and> all_interval_int P (i + 1) j"
20.530 +proof -
20.531 + 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"
20.532 + proof -
20.533 + fix k
20.534 + assume "P i" "\<forall>k\<in>{i+1..j}. P k" "i \<le> k" "k \<le> j"
20.535 + then show "P k" by (cases "k = i") simp_all
20.536 + qed
20.537 + show ?thesis by (auto simp add: all_interval_int_def intro: *)
20.538 +qed
20.539 +
20.540 +lemma list_all_iff_all_interval_int [code_unfold]:
20.541 + "list_all P [i..j] \<longleftrightarrow> all_interval_int P i j"
20.542 + by (simp add: list_all_iff all_interval_int_def)
20.543 +
20.544 +lemma list_ex_iff_not_all_inverval_int [code_unfold]:
20.545 + "list_ex P [i..j] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> P) i j)"
20.546 + by (simp add: list_ex_iff all_interval_int_def)
20.547 +
20.548 +hide_const (open) member null maps map_filter all_interval_nat all_interval_int
20.549 +
20.550 +
20.551 +subsubsection {* Pretty lists *}
20.552
20.553 use "Tools/list_code.ML"
20.554
20.555 @@ -4578,374 +4868,6 @@
20.556 *}
20.557
20.558
20.559 -subsubsection {* Generation of efficient code *}
20.560 -
20.561 -definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
20.562 - mem_iff [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
20.563 -
20.564 -primrec
20.565 - null:: "'a list \<Rightarrow> bool"
20.566 -where
20.567 - "null [] = True"
20.568 - | "null (x#xs) = False"
20.569 -
20.570 -primrec
20.571 - list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
20.572 -where
20.573 - "list_inter [] bs = []"
20.574 - | "list_inter (a#as) bs =
20.575 - (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
20.576 -
20.577 -primrec
20.578 - list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
20.579 -where
20.580 - "list_all P [] = True"
20.581 - | "list_all P (x#xs) = (P x \<and> list_all P xs)"
20.582 -
20.583 -primrec
20.584 - list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
20.585 -where
20.586 - "list_ex P [] = False"
20.587 - | "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
20.588 -
20.589 -primrec
20.590 - filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
20.591 -where
20.592 - "filtermap f [] = []"
20.593 - | "filtermap f (x#xs) =
20.594 - (case f x of None \<Rightarrow> filtermap f xs
20.595 - | Some y \<Rightarrow> y # filtermap f xs)"
20.596 -
20.597 -primrec
20.598 - map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
20.599 -where
20.600 - "map_filter f P [] = []"
20.601 - | "map_filter f P (x#xs) =
20.602 - (if P x then f x # map_filter f P xs else map_filter f P xs)"
20.603 -
20.604 -primrec
20.605 - length_unique :: "'a list \<Rightarrow> nat"
20.606 -where
20.607 - "length_unique [] = 0"
20.608 - | "length_unique (x#xs) =
20.609 - (if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
20.610 -
20.611 -primrec
20.612 - concat_map :: "('a => 'b list) => 'a list => 'b list"
20.613 -where
20.614 - "concat_map f [] = []"
20.615 - | "concat_map f (x#xs) = f x @ concat_map f xs"
20.616 -
20.617 -text {*
20.618 - Only use @{text member} for generating executable code. Otherwise use
20.619 - @{prop "x : set xs"} instead --- it is much easier to reason about.
20.620 - The same is true for @{const list_all} and @{const list_ex}: write
20.621 - @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
20.622 - quantifiers are aleady known to the automatic provers. In fact, the
20.623 - declarations in the code subsection make sure that @{text "\<in>"},
20.624 - @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} are implemented
20.625 - efficiently.
20.626 -
20.627 - Efficient emptyness check is implemented by @{const null}.
20.628 -
20.629 - The functions @{const filtermap} and @{const map_filter} are just
20.630 - there to generate efficient code. Do not use
20.631 - them for modelling and proving.
20.632 -*}
20.633 -
20.634 -lemma rev_foldl_cons [code]:
20.635 - "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
20.636 -proof (induct xs)
20.637 - case Nil then show ?case by simp
20.638 -next
20.639 - case Cons
20.640 - {
20.641 - fix x xs ys
20.642 - have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
20.643 - = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
20.644 - by (induct xs arbitrary: ys) auto
20.645 - }
20.646 - note aux = this
20.647 - show ?case by (induct xs) (auto simp add: Cons aux)
20.648 -qed
20.649 -
20.650 -lemmas in_set_code [code_unfold] = mem_iff [symmetric]
20.651 -
20.652 -lemma member_simps [simp, code]:
20.653 - "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
20.654 - "member [] y \<longleftrightarrow> False"
20.655 - by (auto simp add: mem_iff)
20.656 -
20.657 -lemma member_set:
20.658 - "member = set"
20.659 - by (simp add: expand_fun_eq mem_iff mem_def)
20.660 -
20.661 -abbreviation (input) mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55) where
20.662 - "x mem xs \<equiv> member xs x" -- "for backward compatibility"
20.663 -
20.664 -lemma empty_null:
20.665 - "xs = [] \<longleftrightarrow> null xs"
20.666 -by (cases xs) simp_all
20.667 -
20.668 -lemma [code_unfold]:
20.669 - "eq_class.eq xs [] \<longleftrightarrow> null xs"
20.670 -by (simp add: eq empty_null)
20.671 -
20.672 -lemmas null_empty [code_post] =
20.673 - empty_null [symmetric]
20.674 -
20.675 -lemma list_inter_conv:
20.676 - "set (list_inter xs ys) = set xs \<inter> set ys"
20.677 -by (induct xs) auto
20.678 -
20.679 -lemma list_all_iff [code_post]:
20.680 - "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
20.681 -by (induct xs) auto
20.682 -
20.683 -lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
20.684 -
20.685 -lemma list_all_append [simp]:
20.686 - "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
20.687 -by (induct xs) auto
20.688 -
20.689 -lemma list_all_rev [simp]:
20.690 - "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
20.691 -by (simp add: list_all_iff)
20.692 -
20.693 -lemma list_all_length:
20.694 - "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
20.695 -unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
20.696 -
20.697 -lemma list_all_cong[fundef_cong]:
20.698 - "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
20.699 -by (simp add: list_all_iff)
20.700 -
20.701 -lemma list_ex_iff [code_post]:
20.702 - "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
20.703 -by (induct xs) simp_all
20.704 -
20.705 -lemmas list_bex_code [code_unfold] =
20.706 - list_ex_iff [symmetric]
20.707 -
20.708 -lemma list_ex_length:
20.709 - "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
20.710 -unfolding list_ex_iff set_conv_nth by auto
20.711 -
20.712 -lemma list_ex_cong[fundef_cong]:
20.713 - "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
20.714 -by (simp add: list_ex_iff)
20.715 -
20.716 -lemma filtermap_conv:
20.717 - "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
20.718 -by (induct xs) (simp_all split: option.split)
20.719 -
20.720 -lemma map_filter_conv [simp]:
20.721 - "map_filter f P xs = map f (filter P xs)"
20.722 -by (induct xs) auto
20.723 -
20.724 -lemma length_remdups_length_unique [code_unfold]:
20.725 - "length (remdups xs) = length_unique xs"
20.726 -by (induct xs) simp_all
20.727 -
20.728 -lemma concat_map_code[code_unfold]:
20.729 - "concat(map f xs) = concat_map f xs"
20.730 -by (induct xs) simp_all
20.731 -
20.732 -declare INFI_def [code_unfold]
20.733 -declare SUPR_def [code_unfold]
20.734 -
20.735 -declare set_map [symmetric, code_unfold]
20.736 -
20.737 -hide_const (open) length_unique
20.738 -
20.739 -
20.740 -text {* Code for bounded quantification and summation over nats. *}
20.741 -
20.742 -lemma atMost_upto [code_unfold]:
20.743 - "{..n} = set [0..<Suc n]"
20.744 -by auto
20.745 -
20.746 -lemma atLeast_upt [code_unfold]:
20.747 - "{..<n} = set [0..<n]"
20.748 -by auto
20.749 -
20.750 -lemma greaterThanLessThan_upt [code_unfold]:
20.751 - "{n<..<m} = set [Suc n..<m]"
20.752 -by auto
20.753 -
20.754 -lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
20.755 -
20.756 -lemma greaterThanAtMost_upt [code_unfold]:
20.757 - "{n<..m} = set [Suc n..<Suc m]"
20.758 -by auto
20.759 -
20.760 -lemma atLeastAtMost_upt [code_unfold]:
20.761 - "{n..m} = set [n..<Suc m]"
20.762 -by auto
20.763 -
20.764 -lemma all_nat_less_eq [code_unfold]:
20.765 - "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
20.766 -by auto
20.767 -
20.768 -lemma ex_nat_less_eq [code_unfold]:
20.769 - "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
20.770 -by auto
20.771 -
20.772 -lemma all_nat_less [code_unfold]:
20.773 - "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
20.774 -by auto
20.775 -
20.776 -lemma ex_nat_less [code_unfold]:
20.777 - "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
20.778 -by auto
20.779 -
20.780 -lemma setsum_set_distinct_conv_listsum:
20.781 - "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
20.782 -by (induct xs) simp_all
20.783 -
20.784 -lemma setsum_set_upt_conv_listsum [code_unfold]:
20.785 - "setsum f (set [m..<n]) = listsum (map f [m..<n])"
20.786 -by (rule setsum_set_distinct_conv_listsum) simp
20.787 -
20.788 -text {* General equivalence between @{const listsum} and @{const setsum} *}
20.789 -lemma listsum_setsum_nth:
20.790 - "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
20.791 -using setsum_set_upt_conv_listsum[of "op ! xs" 0 "length xs"]
20.792 -by (simp add: map_nth)
20.793 -
20.794 -text {* Code for summation over ints. *}
20.795 -
20.796 -lemma greaterThanLessThan_upto [code_unfold]:
20.797 - "{i<..<j::int} = set [i+1..j - 1]"
20.798 -by auto
20.799 -
20.800 -lemma atLeastLessThan_upto [code_unfold]:
20.801 - "{i..<j::int} = set [i..j - 1]"
20.802 -by auto
20.803 -
20.804 -lemma greaterThanAtMost_upto [code_unfold]:
20.805 - "{i<..j::int} = set [i+1..j]"
20.806 -by auto
20.807 -
20.808 -lemmas atLeastAtMost_upto [code_unfold] = set_upto[symmetric]
20.809 -
20.810 -lemma setsum_set_upto_conv_listsum [code_unfold]:
20.811 - "setsum f (set [i..j::int]) = listsum (map f [i..j])"
20.812 -by (rule setsum_set_distinct_conv_listsum) simp
20.813 -
20.814 -
20.815 -text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
20.816 -and similiarly for @{text"\<exists>"}. *}
20.817 -
20.818 -function all_from_to_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
20.819 -"all_from_to_nat P i j =
20.820 - (if i < j then if P i then all_from_to_nat P (i+1) j else False
20.821 - else True)"
20.822 -by auto
20.823 -termination
20.824 -by (relation "measure(%(P,i,j). j - i)") auto
20.825 -
20.826 -declare all_from_to_nat.simps[simp del]
20.827 -
20.828 -lemma all_from_to_nat_iff_ball:
20.829 - "all_from_to_nat P i j = (ALL n : {i ..< j}. P n)"
20.830 -proof(induct P i j rule:all_from_to_nat.induct)
20.831 - case (1 P i j)
20.832 - let ?yes = "i < j & P i"
20.833 - show ?case
20.834 - proof (cases)
20.835 - assume ?yes
20.836 - hence "all_from_to_nat P i j = (P i & all_from_to_nat P (i+1) j)"
20.837 - by(simp add: all_from_to_nat.simps)
20.838 - also have "... = (P i & (ALL n : {i+1 ..< j}. P n))" using `?yes` 1 by simp
20.839 - also have "... = (ALL n : {i ..< j}. P n)" (is "?L = ?R")
20.840 - proof
20.841 - assume L: ?L
20.842 - show ?R
20.843 - proof clarify
20.844 - fix n assume n: "n : {i..<j}"
20.845 - show "P n"
20.846 - proof cases
20.847 - assume "n = i" thus "P n" using L by simp
20.848 - next
20.849 - assume "n ~= i"
20.850 - hence "i+1 <= n" using n by auto
20.851 - thus "P n" using L n by simp
20.852 - qed
20.853 - qed
20.854 - next
20.855 - assume R: ?R thus ?L using `?yes` 1 by auto
20.856 - qed
20.857 - finally show ?thesis .
20.858 - next
20.859 - assume "~?yes" thus ?thesis by(auto simp add: all_from_to_nat.simps)
20.860 - qed
20.861 -qed
20.862 -
20.863 -
20.864 -lemma list_all_iff_all_from_to_nat[code_unfold]:
20.865 - "list_all P [i..<j] = all_from_to_nat P i j"
20.866 -by(simp add: all_from_to_nat_iff_ball list_all_iff)
20.867 -
20.868 -lemma list_ex_iff_not_all_from_to_not_nat[code_unfold]:
20.869 - "list_ex P [i..<j] = (~all_from_to_nat (%x. ~P x) i j)"
20.870 -by(simp add: all_from_to_nat_iff_ball list_ex_iff)
20.871 -
20.872 -
20.873 -function all_from_to_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
20.874 -"all_from_to_int P i j =
20.875 - (if i <= j then if P i then all_from_to_int P (i+1) j else False
20.876 - else True)"
20.877 -by auto
20.878 -termination
20.879 -by (relation "measure(%(P,i,j). nat(j - i + 1))") auto
20.880 -
20.881 -declare all_from_to_int.simps[simp del]
20.882 -
20.883 -lemma all_from_to_int_iff_ball:
20.884 - "all_from_to_int P i j = (ALL n : {i .. j}. P n)"
20.885 -proof(induct P i j rule:all_from_to_int.induct)
20.886 - case (1 P i j)
20.887 - let ?yes = "i <= j & P i"
20.888 - show ?case
20.889 - proof (cases)
20.890 - assume ?yes
20.891 - hence "all_from_to_int P i j = (P i & all_from_to_int P (i+1) j)"
20.892 - by(simp add: all_from_to_int.simps)
20.893 - also have "... = (P i & (ALL n : {i+1 .. j}. P n))" using `?yes` 1 by simp
20.894 - also have "... = (ALL n : {i .. j}. P n)" (is "?L = ?R")
20.895 - proof
20.896 - assume L: ?L
20.897 - show ?R
20.898 - proof clarify
20.899 - fix n assume n: "n : {i..j}"
20.900 - show "P n"
20.901 - proof cases
20.902 - assume "n = i" thus "P n" using L by simp
20.903 - next
20.904 - assume "n ~= i"
20.905 - hence "i+1 <= n" using n by auto
20.906 - thus "P n" using L n by simp
20.907 - qed
20.908 - qed
20.909 - next
20.910 - assume R: ?R thus ?L using `?yes` 1 by auto
20.911 - qed
20.912 - finally show ?thesis .
20.913 - next
20.914 - assume "~?yes" thus ?thesis by(auto simp add: all_from_to_int.simps)
20.915 - qed
20.916 -qed
20.917 -
20.918 -lemma list_all_iff_all_from_to_int[code_unfold]:
20.919 - "list_all P [i..j] = all_from_to_int P i j"
20.920 -by(simp add: all_from_to_int_iff_ball list_all_iff)
20.921 -
20.922 -lemma list_ex_iff_not_all_from_to_not_int[code_unfold]:
20.923 - "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
20.924 -by(simp add: all_from_to_int_iff_ball list_ex_iff)
20.925 -
20.926 -
20.927 subsubsection {* Use convenient predefined operations *}
20.928
20.929 code_const "op @"
20.930 @@ -4963,12 +4885,18 @@
20.931 code_const concat
20.932 (Haskell "concat")
20.933
20.934 +code_const List.maps
20.935 + (Haskell "concatMap")
20.936 +
20.937 code_const rev
20.938 (Haskell "reverse")
20.939
20.940 code_const zip
20.941 (Haskell "zip")
20.942
20.943 +code_const List.null
20.944 + (Haskell "null")
20.945 +
20.946 code_const takeWhile
20.947 (Haskell "takeWhile")
20.948
20.949 @@ -4981,4 +4909,10 @@
20.950 code_const last
20.951 (Haskell "last")
20.952
20.953 +code_const list_all
20.954 + (Haskell "all")
20.955 +
20.956 +code_const list_ex
20.957 + (Haskell "any")
20.958 +
20.959 end
21.1 --- a/src/HOL/MicroJava/DFA/LBVComplete.thy Tue Jun 29 02:18:08 2010 +0100
21.2 +++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Tue Jun 29 07:55:18 2010 +0200
21.3 @@ -10,17 +10,17 @@
21.4 begin
21.5
21.6 definition is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" where
21.7 - "is_target step phi pc' \<equiv>
21.8 - \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))"
21.9 + "is_target step phi pc' \<longleftrightarrow>
21.10 + (\<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc)))"
21.11
21.12 definition make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate" where
21.13 - "make_cert step phi B \<equiv>
21.14 + "make_cert step phi B =
21.15 map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"
21.16
21.17 lemma [code]:
21.18 "is_target step phi pc' =
21.19 - list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"
21.20 -by (force simp: list_ex_iff is_target_def mem_iff)
21.21 + list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> List.member (map fst (step pc (phi!pc))) pc') [0..<length phi]"
21.22 +by (force simp: list_ex_iff member_def is_target_def)
21.23
21.24
21.25 locale lbvc = lbv +
22.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Jun 29 02:18:08 2010 +0100
22.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Jun 29 07:55:18 2010 +0200
22.3 @@ -707,7 +707,7 @@
22.4 case False
22.5 have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add: power2_eq_square)
22.6 also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
22.7 - also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
22.8 + also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by (auto simp add: inner_diff_left)
22.9 also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz)
22.10 finally show ?thesis using False x(1) by(auto simp add: real_mult_left_cancel) next
22.11 case True thus ?thesis using assms(1) apply(rule_tac x="(a + b) /2" in bexI) by auto qed qed
23.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Jun 29 02:18:08 2010 +0100
23.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Jun 29 07:55:18 2010 +0200
23.3 @@ -15,7 +15,7 @@
23.4 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
23.5 by auto
23.6
23.7 -abbreviation inner_bullet (infix "\<bullet>" 70) where "x \<bullet> y \<equiv> inner x y"
23.8 +notation inner (infix "\<bullet>" 70)
23.9
23.10 subsection {* A connectedness or intermediate value lemma with several applications. *}
23.11
23.12 @@ -466,8 +466,8 @@
23.13 "orthogonal x a \<Longrightarrow> orthogonal (-x) a"
23.14 "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
23.15 "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
23.16 - unfolding orthogonal_def inner_simps by auto
23.17 -
23.18 + unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto
23.19 +
23.20 end
23.21
23.22 lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
24.1 --- a/src/HOL/NanoJava/Equivalence.thy Tue Jun 29 02:18:08 2010 +0100
24.2 +++ b/src/HOL/NanoJava/Equivalence.thy Tue Jun 29 07:55:18 2010 +0200
24.3 @@ -133,7 +133,7 @@
24.4 apply (clarify intro!: Impl_nvalid_0)
24.5 apply (clarify intro!: Impl_nvalid_Suc)
24.6 apply (drule nvalids_SucD)
24.7 -apply (simp only: all_simps)
24.8 +apply (simp only: HOL.all_simps)
24.9 apply (erule (1) impE)
24.10 apply (drule (2) Impl_sound_lemma)
24.11 apply blast
25.1 --- a/src/HOL/Number_Theory/Primes.thy Tue Jun 29 02:18:08 2010 +0100
25.2 +++ b/src/HOL/Number_Theory/Primes.thy Tue Jun 29 07:55:18 2010 +0200
25.3 @@ -208,22 +208,20 @@
25.4 lemma one_not_prime_int [simp]: "~prime (1::int)"
25.5 by (simp add: prime_int_def)
25.6
25.7 -lemma prime_nat_code[code]:
25.8 - "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
25.9 -apply(simp add: Ball_def)
25.10 +lemma prime_nat_code [code]:
25.11 + "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
25.12 +apply (simp add: Ball_def)
25.13 apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
25.14 done
25.15
25.16 lemma prime_nat_simp:
25.17 - "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
25.18 -apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
25.19 -apply(simp add:nat_number One_nat_def)
25.20 -done
25.21 + "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
25.22 +by (auto simp add: prime_nat_code)
25.23
25.24 -lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard]
25.25 +lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
25.26
25.27 -lemma prime_int_code[code]:
25.28 - "prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R")
25.29 +lemma prime_int_code [code]:
25.30 + "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
25.31 proof
25.32 assume "?L" thus "?R"
25.33 by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
25.34 @@ -232,12 +230,10 @@
25.35 qed
25.36
25.37 lemma prime_int_simp:
25.38 - "prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))"
25.39 -apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto)
25.40 -apply simp
25.41 -done
25.42 + "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
25.43 +by (auto simp add: prime_int_code)
25.44
25.45 -lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
25.46 +lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
25.47
25.48 lemma two_is_prime_nat [simp]: "prime (2::nat)"
25.49 by simp
26.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy Tue Jun 29 02:18:08 2010 +0100
26.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy Tue Jun 29 07:55:18 2010 +0200
26.3 @@ -1174,7 +1174,8 @@
26.4 ultimately show ?case using prime_divprod[OF p] by blast
26.5 qed
26.6
26.7 -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)
26.8 +lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps"
26.9 + by (auto simp add: primefact_def list_all_iff)
26.10
26.11 (* Variant of Lucas theorem. *)
26.12
27.1 --- a/src/HOL/Tools/refute.ML Tue Jun 29 02:18:08 2010 +0100
27.2 +++ b/src/HOL/Tools/refute.ML Tue Jun 29 07:55:18 2010 +0200
27.3 @@ -2234,7 +2234,7 @@
27.4 (* sanity check: every element of terms' must also be *)
27.5 (* present in terms *)
27.6 val _ =
27.7 - if List.all (member (op =) terms) terms' then ()
27.8 + if forall (member (op =) terms) terms' then ()
27.9 else
27.10 raise REFUTE ("IDT_constructor_interpreter",
27.11 "element has disappeared")
27.12 @@ -2957,7 +2957,7 @@
27.13 (* "lfp(f) == Inter({u. f(u) <= u})" *)
27.14 (* interpretation * interpretation -> bool *)
27.15 fun is_subset (Node subs, Node sups) =
27.16 - List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT))
27.17 + forall (fn (sub, sup) => (sub = FF) orelse (sup = TT))
27.18 (subs ~~ sups)
27.19 | is_subset (_, _) =
27.20 raise REFUTE ("lfp_interpreter",
27.21 @@ -3012,7 +3012,7 @@
27.22 (* "gfp(f) == Union({u. u <= f(u)})" *)
27.23 (* interpretation * interpretation -> bool *)
27.24 fun is_subset (Node subs, Node sups) =
27.25 - List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT))
27.26 + forall (fn (sub, sup) => (sub = FF) orelse (sup = TT))
27.27 (subs ~~ sups)
27.28 | is_subset (_, _) =
27.29 raise REFUTE ("gfp_interpreter",
28.1 --- a/src/HOL/Word/WordShift.thy Tue Jun 29 02:18:08 2010 +0100
28.2 +++ b/src/HOL/Word/WordShift.thy Tue Jun 29 07:55:18 2010 +0200
28.3 @@ -988,8 +988,10 @@
28.4 apply (erule bin_nth_uint_imp)+
28.5 done
28.6
28.7 -lemmas test_bit_split =
28.8 - test_bit_split' [THEN mp, simplified all_simps, standard]
28.9 +lemma test_bit_split:
28.10 + "word_split c = (a, b) \<Longrightarrow>
28.11 + (\<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))"
28.12 + by (simp add: test_bit_split')
28.13
28.14 lemma test_bit_split_eq: "word_split c = (a, b) <->
28.15 ((ALL n::nat. b !! n = (n < size b & c !! n)) &
29.1 --- a/src/HOL/ex/Execute_Choice.thy Tue Jun 29 02:18:08 2010 +0100
29.2 +++ b/src/HOL/ex/Execute_Choice.thy Tue Jun 29 07:55:18 2010 +0200
29.3 @@ -66,7 +66,7 @@
29.4 shows [code]: "valuesum (Mapping []) = 0"
29.5 and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in
29.6 the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
29.7 - by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping)
29.8 + by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping null_def)
29.9
29.10 text {*
29.11 As a side effect the precondition disappears (but note this has nothing to do with choice!).
30.1 --- a/src/HOL/ex/Meson_Test.thy Tue Jun 29 02:18:08 2010 +0100
30.2 +++ b/src/HOL/ex/Meson_Test.thy Tue Jun 29 07:55:18 2010 +0200
30.3 @@ -16,7 +16,7 @@
30.4 below and constants declared in HOL!
30.5 *}
30.6
30.7 -hide_const (open) subset member quotient union inter sum
30.8 +hide_const (open) subset quotient union inter sum
30.9
30.10 text {*
30.11 Test data for the MESON proof procedure
31.1 --- a/src/HOL/ex/Recdefs.thy Tue Jun 29 02:18:08 2010 +0100
31.2 +++ b/src/HOL/ex/Recdefs.thy Tue Jun 29 07:55:18 2010 +0200
31.3 @@ -1,5 +1,4 @@
31.4 (* Title: HOL/ex/Recdefs.thy
31.5 - ID: $Id$
31.6 Author: Konrad Slind and Lawrence C Paulson
31.7 Copyright 1996 University of Cambridge
31.8
31.9 @@ -44,7 +43,7 @@
31.10 text {* Not handled automatically: too complicated. *}
31.11 consts variant :: "nat * nat list => nat"
31.12 recdef (permissive) variant "measure (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
31.13 - "variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
31.14 + "variant (x, L) = (if x \<in> set L then variant (Suc x, L) else x)"
31.15
31.16 consts gcd :: "nat * nat => nat"
31.17 recdef gcd "measure (\<lambda>(x, y). x + y)"
32.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy Tue Jun 29 02:18:08 2010 +0100
32.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy Tue Jun 29 07:55:18 2010 +0200
32.3 @@ -86,7 +86,7 @@
32.4 "(mkfin (a>>s)) = (a>>(mkfin s))"
32.5
32.6
32.7 -lemmas [simp del] = ex_simps all_simps split_paired_Ex
32.8 +lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
32.9
32.10 declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
32.11
33.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy Tue Jun 29 02:18:08 2010 +0100
33.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy Tue Jun 29 07:55:18 2010 +0200
33.3 @@ -192,7 +192,7 @@
33.4 "Traces A == (traces A,asig_of A)"
33.5
33.6
33.7 -lemmas [simp del] = ex_simps all_simps split_paired_Ex
33.8 +lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
33.9 declare Let_def [simp]
33.10 declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
33.11
34.1 --- a/src/HOLCF/ex/Focus_ex.thy Tue Jun 29 02:18:08 2010 +0100
34.2 +++ b/src/HOLCF/ex/Focus_ex.thy Tue Jun 29 07:55:18 2010 +0200
34.3 @@ -204,7 +204,7 @@
34.4 done
34.5
34.6 lemma lemma4: "is_g(g) --> def_g(g)"
34.7 -apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps")
34.8 +apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
34.9 addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *})
34.10 apply (rule impI)
34.11 apply (erule exE)