# HG changeset patch # User blanchet # Date 1392360825 -3600 # Node ID 0d31c05462863dc5e047899576c7467d30e47aeb # Parent 56fa33537869c9ec91bf14c7262e30bda92ef64b merged 'List.map' and 'List.list.map' diff -r 56fa33537869 -r 0d31c0546286 src/Doc/ProgProve/Bool_nat_list.thy --- 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 \ 'b) \ 'a list \ '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 diff -r 56fa33537869 -r 0d31c0546286 src/HOL/HOLCF/Library/List_Cpo.thy --- 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 diff -r 56fa33537869 -r 0d31c0546286 src/HOL/Hoare_Parallel/RG_Hoare.thy --- 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))\[]") 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 "\i ?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\ 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))\[]") 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 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 " \i. i < length ys \ ?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))\[]") 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)\[]") 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)\[]") apply(drule last_conv_nth) - apply (simp del:map.simps last.simps) + apply (simp del:list.map last.simps) apply simp apply simp done diff -r 56fa33537869 -r 0d31c0546286 src/HOL/List.thy --- 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 \ 'a set" where [simp]: "coset xs = - set xs" -primrec map :: "('a \ 'b) \ 'a list \ 'b list" where -"map f [] = []" | -"map f (x # xs) = f x # map f xs" - primrec append :: "'a list \ 'a list \ '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 "\x\set xs. x \ f ` A \ xs \ 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" diff -r 56fa33537869 -r 0d31c0546286 src/HOL/Metis_Examples/Abstraction.thy --- 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 (\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 (\w. (w -> w, w \ w)) xs = zip (map (\w. w -> w) xs) (map (\w. w \ w) xs)" apply (induct xs) - apply (metis map.simps(1) zip_Nil) + apply (metis list.map(1) zip_Nil) by auto lemma "(\x. Suc (f x)) ` {x. even x} \ A \ \x. even x --> Suc (f x) \ A" diff -r 56fa33537869 -r 0d31c0546286 src/HOL/Metis_Examples/Binary_Tree.thy --- 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)) diff -r 56fa33537869 -r 0d31c0546286 src/HOL/Metis_Examples/Type_Encodings.thy --- 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 = [])" diff -r 56fa33537869 -r 0d31c0546286 src/HOL/MicroJava/Comp/CorrCompTp.thy --- 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) [\] (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 (\z. z \ 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 (\ p. (fst p, snd p)) lvars)") @@ -166,7 +166,7 @@ lemma inited_LT_at_index_no_err: " i < length (inited_LT C pTs lvars) \ inited_LT C pTs lvars ! i \ 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 = [] \ 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 \mt3_rest. \ *) diff -r 56fa33537869 -r 0d31c0546286 src/HOL/SMT_Examples/SMT_Examples.thy --- 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 (3::int) 42" by smt -lemma "map (\i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps) +lemma "map (\i::nat. i + 1) [0, 1] = [1, 2]" by (smt list.map) lemma "(ALL x. P x) | ~ All P" by smt diff -r 56fa33537869 -r 0d31c0546286 src/HOL/Statespace/state_fun.ML --- 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, [])) = diff -r 56fa33537869 -r 0d31c0546286 src/HOL/Word/WordBitwise.thy --- 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