--- a/src/Doc/ProgProve/Bool_nat_list.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Fri Feb 14 07:53:45 2014 +0100
@@ -394,8 +394,8 @@
and the \indexed{@{const map}}{map} function that applies a function to all elements of a list:
\begin{isabelle}
\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\
-@{text"\""}@{thm map.simps(1)}@{text"\" |"}\\
-@{text"\""}@{thm map.simps(2)}@{text"\""}
+@{text"\""}@{thm list.map(1)}@{text"\" |"}\\
+@{text"\""}@{thm list.map(2)}@{text"\""}
\end{isabelle}
\ifsem
--- a/src/HOL/HOLCF/Library/List_Cpo.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy Fri Feb 14 07:53:45 2014 +0100
@@ -242,7 +242,7 @@
using f
apply (simp add: prod_cont_iff)
apply (rule cont_apply [OF g])
-apply (rule list_contI, rule map.simps, simp, simp, simp)
+apply (rule list_contI, rule list.map, simp, simp, simp)
apply (induct_tac y, simp, simp)
done
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Fri Feb 14 07:53:45 2014 +0100
@@ -669,7 +669,7 @@
apply force
apply(rule conjI,simp add:lift_def)
apply(subgoal_tac "lift Q (Some P2, ta) =(Some (Seq P2 Q), ta)")
- apply(simp add:Cons_lift del:map.simps)
+ apply(simp add:Cons_lift del:list.map)
apply(rule nth_tl_if)
apply force
apply simp+
@@ -733,11 +733,11 @@
apply clarify
apply(case_tac xs,simp add:cp_def)
apply clarify
- apply (simp del:map.simps)
+ apply (simp del:list.map)
apply (rename_tac list)
apply(subgoal_tac "(map (lift Q) ((a, b) # list))\<noteq>[]")
apply(drule last_conv_nth)
- apply (simp del:map.simps)
+ apply (simp del:list.map)
apply(simp only:last_lift_not_None)
apply simp
--{* @{text "\<exists>i<length x. fst (x ! i) = Some Q"} *}
@@ -857,7 +857,7 @@
apply clarify
apply(erule_tac x="Suc i" in allE)
apply simp
- apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
+ apply(simp add:Cons_lift_append nth_append snd_lift del:list.map)
apply(erule mp)
apply(erule etranE,simp)
apply(case_tac "fst(((Some P, s) # xs) ! i)")
@@ -916,8 +916,8 @@
--{* WhileOne *}
apply(thin_tac "P = While b P \<longrightarrow> ?Q")
apply(rule ctran_in_comm,simp)
-apply(simp add:Cons_lift del:map.simps)
-apply(simp add:comm_def del:map.simps)
+apply(simp add:Cons_lift del:list.map)
+apply(simp add:comm_def del:list.map)
apply(rule conjI)
apply clarify
apply(case_tac "fst(((Some P, sa) # xs) ! i)")
@@ -926,20 +926,20 @@
apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
apply simp
apply simp
- apply(simp add:snd_lift del:map.simps)
+ apply(simp add:snd_lift del:list.map)
apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
apply(erule_tac x=sa in allE)
apply(drule_tac c="(Some P, sa) # xs" in subsetD)
- apply (simp add:assum_def del:map.simps)
+ apply (simp add:assum_def del:list.map)
apply clarify
- apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:map.simps)
+ apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:list.map)
apply(erule mp)
apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
apply(erule etranE,simp add:lift_def)
apply(rule Env)
apply(erule etranE,simp add:lift_def)
apply(rule Env)
- apply (simp add:comm_def del:map.simps)
+ apply (simp add:comm_def del:list.map)
apply clarify
apply(erule allE,erule impE,assumption)
apply(erule mp)
@@ -953,7 +953,7 @@
apply clarify
apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
apply(drule last_conv_nth)
- apply (simp del:map.simps)
+ apply (simp del:list.map)
apply(simp only:last_lift_not_None)
apply simp
--{* WhileMore *}
@@ -966,32 +966,32 @@
apply(erule assum_after_body)
apply (simp del:last.simps)+
--{* lo de antes. *}
-apply(simp add:comm_def del:map.simps last.simps)
+apply(simp add:comm_def del:list.map last.simps)
apply(rule conjI)
apply clarify
apply(simp only:Cons_lift_append)
apply(case_tac "i<length xs")
- apply(simp add:nth_append del:map.simps last.simps)
+ apply(simp add:nth_append del:list.map last.simps)
apply(case_tac "fst(((Some P, sa) # xs) ! i)")
apply(case_tac "((Some P, sa) # xs) ! i")
apply (simp add:lift_def del:last.simps)
apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t)
apply simp
apply simp
- apply(simp add:snd_lift del:map.simps last.simps)
+ apply(simp add:snd_lift del:list.map last.simps)
apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> ?P i")
apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
apply(erule_tac x=sa in allE)
apply(drule_tac c="(Some P, sa) # xs" in subsetD)
- apply (simp add:assum_def del:map.simps last.simps)
+ apply (simp add:assum_def del:list.map last.simps)
apply clarify
- apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:map.simps last.simps, erule mp)
+ apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:list.map last.simps, erule mp)
apply(case_tac "fst(((Some P, sa) # xs) ! ia)")
apply(erule etranE,simp add:lift_def)
apply(rule Env)
apply(erule etranE,simp add:lift_def)
apply(rule Env)
- apply (simp add:comm_def del:map.simps)
+ apply (simp add:comm_def del:list.map)
apply clarify
apply(erule allE,erule impE,assumption)
apply(erule mp)
@@ -1007,7 +1007,7 @@
apply arith
apply(erule_tac x="i-length xs" in allE,clarify)
apply(case_tac "i=length xs")
- apply (simp add:nth_append snd_lift del:map.simps last.simps)
+ apply (simp add:nth_append snd_lift del:list.map last.simps)
apply(simp add:last_length del:last.simps)
apply(erule mp)
apply(case_tac "last((Some P, sa) # xs)")
@@ -1015,7 +1015,7 @@
--{* @{text "i>length xs"} *}
apply(case_tac "i-length xs")
apply arith
-apply(simp add:nth_append del:map.simps last.simps)
+apply(simp add:nth_append del:list.map last.simps)
apply(rotate_tac -3)
apply(subgoal_tac "i- Suc (length xs)=nat")
prefer 2
@@ -1024,20 +1024,20 @@
--{* last=None *}
apply clarify
apply(case_tac ys)
- apply(simp add:Cons_lift del:map.simps last.simps)
+ apply(simp add:Cons_lift del:list.map last.simps)
apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]")
apply(drule last_conv_nth)
- apply (simp del:map.simps)
+ apply (simp del:list.map)
apply(simp only:last_lift_not_None)
apply simp
apply(subgoal_tac "((Some (Seq P (While b P)), sa) # map (lift (While b P)) xs @ ys)\<noteq>[]")
apply(drule last_conv_nth)
- apply (simp del:map.simps last.simps)
+ apply (simp del:list.map last.simps)
apply(simp add:nth_append del:last.simps)
apply(rename_tac a list)
apply(subgoal_tac "((Some (While b P), snd (last ((Some P, sa) # xs))) # a # list)\<noteq>[]")
apply(drule last_conv_nth)
- apply (simp del:map.simps last.simps)
+ apply (simp del:list.map last.simps)
apply simp
apply simp
done
--- a/src/HOL/List.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/List.thy Fri Feb 14 07:53:45 2014 +0100
@@ -8,7 +8,7 @@
imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
begin
-datatype_new 'a list =
+datatype_new 'a list (map: map rel: rel) =
=: Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
@@ -59,10 +59,6 @@
definition coset :: "'a list \<Rightarrow> 'a set" where
[simp]: "coset xs = - set xs"
-primrec map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
-"map f [] = []" |
-"map f (x # xs) = f x # map f xs"
-
primrec append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
append_Nil: "[] @ ys = ys" |
append_Cons: "(x#xs) @ ys = x # xs @ ys"
@@ -5164,7 +5160,7 @@
lemma lists_image: "lists (f`A) = map f ` lists A"
proof -
{ fix xs have "\<forall>x\<in>set xs. x \<in> f ` A \<Longrightarrow> xs \<in> map f ` lists A"
- by (induct xs) (auto simp del: map.simps simp add: map.simps[symmetric] intro!: imageI) }
+ by (induct xs) (auto simp del: list.map simp add: list.map[symmetric] intro!: imageI) }
then show ?thesis by auto
qed
@@ -6710,9 +6706,12 @@
"(list_all2 A ===> set_rel A) set set"
unfolding set_def by transfer_prover
+lemma map_rec: "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs"
+ by (induct xs) auto
+
lemma map_transfer [transfer_rule]:
"((A ===> B) ===> list_all2 A ===> list_all2 B) map map"
- unfolding List.map_def by transfer_prover
+ unfolding map_rec[abs_def] by transfer_prover
lemma append_transfer [transfer_rule]:
"(list_all2 A ===> list_all2 A ===> list_all2 A) append append"
--- a/src/HOL/Metis_Examples/Abstraction.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy Fri Feb 14 07:53:45 2014 +0100
@@ -138,14 +138,14 @@
lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)"
apply (induct xs)
- apply (metis map.simps(1) zip_Nil)
+ apply (metis list.map(1) zip_Nil)
by auto
lemma
"map (\<lambda>w. (w -> w, w \<times> w)) xs =
zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)"
apply (induct xs)
- apply (metis map.simps(1) zip_Nil)
+ apply (metis list.map(1) zip_Nil)
by auto
lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A"
--- a/src/HOL/Metis_Examples/Binary_Tree.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy Fri Feb 14 07:53:45 2014 +0100
@@ -130,14 +130,14 @@
lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
apply (induct t)
- apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
+ apply (metis bt_map.simps(1) list.map(1) preorder.simps(1))
by simp
lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
proof (induct t)
case Lf thus ?case
proof -
- have "map f [] = []" by (metis map.simps(1))
+ have "map f [] = []" by (metis list.map(1))
hence "map f [] = inorder Lf" by (metis inorder.simps(1))
hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1))
thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1))
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Fri Feb 14 07:53:45 2014 +0100
@@ -76,13 +76,13 @@
by (metis_exhaust last.simps One_nat_def)
lemma "map Suc [0] = [Suc 0]"
-by (metis_exhaust map.simps)
+by (metis_exhaust list.map)
lemma "map Suc [1 + 1] = [Suc 2]"
-by (metis_exhaust map.simps nat_1_add_1)
+by (metis_exhaust list.map nat_1_add_1)
lemma "map Suc [2] = [Suc (1 + 1)]"
-by (metis_exhaust map.simps nat_1_add_1)
+by (metis_exhaust list.map nat_1_add_1)
definition "null xs = (xs = [])"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Feb 14 07:53:45 2014 +0100
@@ -80,7 +80,7 @@
apply (rule allI)
apply (drule_tac x="a # ys" in spec)
apply (simp only: rev.simps append_assoc append_Cons append_Nil
- map.simps map_of.simps map_upds_Cons list.sel)
+ list.map map_of.simps map_upds_Cons list.sel)
done
lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))"
@@ -132,7 +132,7 @@
apply (case_tac "vname = This")
apply (simp add: inited_LT_def)
apply (simp add: inited_LT_def)
-apply (simp (no_asm_simp) only: map_map [symmetric] map_append [symmetric] map.simps [symmetric])
+apply (simp (no_asm_simp) only: map_map [symmetric] map_append [symmetric] list.map [symmetric])
apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)")
apply (simp (no_asm_simp) only: List.nth_map ok_val.simps)
apply (subgoal_tac "map_of lvars = map_of (map (\<lambda> p. (fst p, snd p)) lvars)")
@@ -166,7 +166,7 @@
lemma inited_LT_at_index_no_err: " i < length (inited_LT C pTs lvars)
\<Longrightarrow> inited_LT C pTs lvars ! i \<noteq> Err"
apply (simp only: inited_LT_def)
-apply (simp only: map_map [symmetric] map_append [symmetric] map.simps [symmetric] length_map)
+apply (simp only: map_map [symmetric] map_append [symmetric] list.map [symmetric] length_map)
apply (simp only: nth_map)
apply simp
done
@@ -1394,7 +1394,7 @@
apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
apply (rule max_of_list_sublist)
- apply (simp (no_asm_simp) only: set_append set.simps map.simps) apply blast
+ apply (simp (no_asm_simp) only: set_append set.simps list.map) apply blast
apply (simp (no_asm_simp))
apply simp (* subgoal bc3 = [] *)
apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
@@ -1421,7 +1421,7 @@
(* (some) preconditions of wt_instr_offset *)
apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
apply (rule max_of_list_sublist)
- apply (simp (no_asm_simp) only: set_append set.simps map.simps) apply blast
+ apply (simp (no_asm_simp) only: set_append set.simps list.map) apply blast
apply (simp (no_asm_simp))
apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Fri Feb 14 07:53:45 2014 +0100
@@ -481,7 +481,7 @@
lemma "le = op \<le> \<Longrightarrow> le (3::int) 42" by smt
-lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps)
+lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt list.map)
lemma "(ALL x. P x) | ~ All P" by smt
--- a/src/HOL/Statespace/state_fun.ML Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Statespace/state_fun.ML Fri Feb 14 07:53:45 2014 +0100
@@ -340,7 +340,7 @@
fun is_datatype thy = is_some o Datatype.get_info thy;
-fun mk_map "List.list" = Syntax.const "List.map"
+fun mk_map @{type_name List.list} = Syntax.const @{const_name List.map}
| mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
fun gen_constr_destr comp prfx thy (Type (T, [])) =
--- a/src/HOL/Word/WordBitwise.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Word/WordBitwise.thy Fri Feb 14 07:53:45 2014 +0100
@@ -593,7 +593,7 @@
@{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size}
addsimprocs [word_len_simproc],
put_simpset no_split_ss @{context} addsimps
- @{thms list.simps split_conv replicate.simps map.simps
+ @{thms list.simps split_conv replicate.simps list.map
zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil
foldr.simps map2_Cons map2_Nil takefill_Suc_Cons
takefill_Suc_Nil takefill.Z rbl_succ2_simps