# HG changeset patch # User blanchet # Date 1377810064 -7200 # Node ID b6c3be86821796a8f65c9535a9a156537dc0b397 # Parent 5e0623448bdba8fca415d8740822863df63a8121 renamed BNF fact diff -r 5e0623448bdb -r b6c3be868217 src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Thu Aug 29 22:56:39 2013 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Thu Aug 29 23:01:04 2013 +0200 @@ -453,12 +453,12 @@ proof (cases "n \ m") case False thus ?thesis unfolding smerge_def by (subst sset_flat) - (auto simp: stream.set_map' in_set_conv_nth simp del: stake.simps + (auto simp: stream.set_map in_set_conv_nth simp del: stake.simps intro!: exI[of _ n, OF disjI2] exI[of _ m, OF mp]) next case True thus ?thesis unfolding smerge_def by (subst sset_flat) - (auto simp: stream.set_map' in_set_conv_nth image_iff simp del: stake.simps snth.simps + (auto simp: stream.set_map in_set_conv_nth image_iff simp del: stake.simps snth.simps intro!: exI[of _ m, OF disjI1] bexI[of _ "ss !! n"] exI[of _ n, OF mp]) qed @@ -467,7 +467,7 @@ fix x assume "x \ sset (smerge ss)" thus "x \ UNION (sset ss) sset" unfolding smerge_def by (subst (asm) sset_flat) - (auto simp: stream.set_map' in_set_conv_nth sset_range simp del: stake.simps, fast+) + (auto simp: stream.set_map in_set_conv_nth sset_range simp del: stake.simps, fast+) next fix s x assume "s \ sset ss" "x \ sset s" thus "x \ sset (smerge ss)" using snth_sset_smerge by (auto simp: sset_range) @@ -480,7 +480,7 @@ "sproduct s1 s2 = smerge (smap (\x. smap (Pair x) s2) s1)" lemma sset_sproduct: "sset (sproduct s1 s2) = sset s1 \ sset s2" - unfolding sproduct_def sset_smerge by (auto simp: stream.set_map') + unfolding sproduct_def sset_smerge by (auto simp: stream.set_map) subsection {* interleave two streams *} diff -r 5e0623448bdb -r b6c3be868217 src/HOL/BNF/Examples/TreeFI.thy --- a/src/HOL/BNF/Examples/TreeFI.thy Thu Aug 29 22:56:39 2013 +0200 +++ b/src/HOL/BNF/Examples/TreeFI.thy Thu Aug 29 23:01:04 2013 +0200 @@ -16,7 +16,7 @@ lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs" unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs -by (auto simp add: listF.set_map') +by (auto simp add: listF.set_map) lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)" by (metis Tree_def treeFI.collapse treeFI.dtor_ctor) diff -r 5e0623448bdb -r b6c3be868217 src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Thu Aug 29 22:56:39 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Thu Aug 29 23:01:04 2013 +0200 @@ -227,7 +227,7 @@ apply transfer apply simp done -lemmas [simp] = fset.map_comp fset.map_id fset.set_map' +lemmas [simp] = fset.map_comp fset.map_id fset.set_map lemma fset_rel_fset: "set_rel \ (fset A1) (fset A2) = fset_rel \ A1 A2" unfolding fset_rel_def set_rel_def by auto @@ -881,7 +881,7 @@ Plus: "\R a b; multiset_rel' R M N\ \ multiset_rel' R (M + {#a#}) (N + {#b#})" lemma multiset_map_Zero_iff[simp]: "mmap f M = {#} \ M = {#}" -by (metis image_is_empty multiset.set_map' set_of_eq_empty_iff) +by (metis image_is_empty multiset.set_map set_of_eq_empty_iff) lemma multiset_map_Zero[simp]: "mmap f {#} = {#}" by simp @@ -1001,7 +1001,7 @@ shows "\ N1. N = N1 + {#f a#} \ mmap f M = N1" proof- have "f a \# N" - using assms multiset.set_map'[of f "M + {#a#}"] by auto + using assms multiset.set_map[of f "M + {#a#}"] by auto then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis have "mmap f M = N1" using assms unfolding N by simp thus ?thesis using N by blast @@ -1012,7 +1012,7 @@ shows "\ M1 a. M = M1 + {#a#} \ f a = b \ mmap f M1 = N" proof- obtain a where a: "a \# M" and fa: "f a = b" - using multiset.set_map'[of f M] unfolding assms + using multiset.set_map[of f M] unfolding assms by (metis image_iff mem_set_of_iff union_single_eq_member) then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis have "mmap f M1 = N" using assms unfolding M fa[symmetric] by simp diff -r 5e0623448bdb -r b6c3be868217 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 22:56:39 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 23:01:04 2013 +0200 @@ -73,7 +73,7 @@ val set_bd_of_bnf: bnf -> thm list val set_defs_of_bnf: bnf -> thm list val set_map0_of_bnf: bnf -> thm list - val set_map'_of_bnf: bnf -> thm list + val set_map_of_bnf: bnf -> thm list val wit_thms_of_bnf: bnf -> thm list val wit_thmss_of_bnf: bnf -> thm list list @@ -195,7 +195,7 @@ map_wppull: thm lazy, rel_eq: thm lazy, rel_flip: thm lazy, - set_map': thm lazy list, + set_map: thm lazy list, rel_cong: thm lazy, rel_mono: thm lazy, rel_mono_strong: thm lazy, @@ -205,7 +205,7 @@ }; fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel - map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map' rel_cong rel_mono + map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, @@ -222,7 +222,7 @@ map_wppull = map_wppull, rel_eq = rel_eq, rel_flip = rel_flip, - set_map' = set_map', + set_map = set_map, rel_cong = rel_cong, rel_mono = rel_mono, rel_mono_strong = rel_mono_strong, @@ -246,7 +246,7 @@ map_wppull, rel_eq, rel_flip, - set_map', + set_map, rel_cong, rel_mono, rel_mono_strong, @@ -268,7 +268,7 @@ map_wppull = Lazy.map f map_wppull, rel_eq = Lazy.map f rel_eq, rel_flip = Lazy.map f rel_flip, - set_map' = map (Lazy.map f) set_map', + set_map = map (Lazy.map f) set_map, rel_cong = Lazy.map f rel_cong, rel_mono = Lazy.map f rel_mono, rel_mono_strong = Lazy.map f rel_mono_strong, @@ -395,7 +395,7 @@ val set_bd_of_bnf = #set_bd o #axioms o rep_bnf; val set_defs_of_bnf = #set_defs o #defs o rep_bnf; val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf; -val set_map'_of_bnf = map Lazy.force o #set_map' o #facts o rep_bnf; +val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf; val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf; val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf; val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf; @@ -519,7 +519,7 @@ val rel_eqN = "rel_eq"; val rel_flipN = "rel_flip"; val set_map0N = "set_map0"; -val set_map'N = "set_map'"; +val set_mapN = "set_map"; val set_bdN = "set_bd"; val rel_GrpN = "rel_Grp"; val rel_conversepN = "rel_conversep"; @@ -583,7 +583,7 @@ (map_idN, [Lazy.force (#map_id facts)], []), (rel_eqN, [Lazy.force (#rel_eq facts)], []), (rel_flipN, [Lazy.force (#rel_flip facts)], []), - (set_map'N, map Lazy.force (#set_map' facts), []), + (set_mapN, map Lazy.force (#set_map facts), []), (rel_OO_GrpN, no_refl [#rel_OO_Grp axioms], []), (rel_GrpN, [Lazy.force (#rel_Grp facts)], []), (rel_conversepN, [Lazy.force (#rel_conversep facts)], []), @@ -1018,7 +1018,7 @@ val map_cong = Lazy.lazy mk_map_cong; - val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map0 axioms); + val set_map = map (fn thm => Lazy.lazy (fn () => mk_set_map thm)) (#set_map0 axioms); fun mk_in_bd () = let @@ -1050,7 +1050,7 @@ Goal.prove_sorry lthy [] [] in_bd_goal (mk_in_bd_tac live surj_imp_ordLeq_inst (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms) - (map Lazy.force set_map') (#set_bd axioms) (#bd_card_order axioms) + (map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms) bd_Card_order bd_Cinfinite bd_Cnotzero) |> Thm.close_derivation end; @@ -1087,7 +1087,7 @@ in Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_wppull_tac (#map_id0 axioms) (#map_cong0 axioms) - (#map_wpull axioms) (Lazy.force map_comp) (map Lazy.force set_map')) + (#map_wpull axioms) (Lazy.force map_comp) (map Lazy.force set_map)) |> Thm.close_derivation end; @@ -1103,7 +1103,7 @@ in Goal.prove_sorry lthy [] [] goal (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id) - (Lazy.force map_comp) (map Lazy.force set_map')) + (Lazy.force map_comp) (map Lazy.force set_map)) |> Thm.close_derivation end; @@ -1155,7 +1155,7 @@ val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs)); val le_thm = Goal.prove_sorry lthy [] [] le_goal (mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms) - (Lazy.force map_comp) (map Lazy.force set_map')) + (Lazy.force map_comp) (map Lazy.force set_map)) |> Thm.close_derivation val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs)); in @@ -1176,7 +1176,7 @@ in Goal.prove_sorry lthy [] [] goal (mk_rel_OO_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms) - (Lazy.force map_wppull) (Lazy.force map_comp) (map Lazy.force set_map')) + (Lazy.force map_wppull) (Lazy.force map_comp) (map Lazy.force set_map)) |> Thm.close_derivation end; @@ -1227,7 +1227,7 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl))) - (mk_rel_mono_strong_tac (Lazy.force in_rel) (map Lazy.force set_map')) + (mk_rel_mono_strong_tac (Lazy.force in_rel) (map Lazy.force set_map)) |> Thm.close_derivation end; @@ -1245,7 +1245,7 @@ Goal.prove_sorry lthy [] [] (fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl) (mk_map_transfer_tac (Lazy.force rel_mono) (Lazy.force in_rel) - (map Lazy.force set_map') (#map_cong0 axioms) (Lazy.force map_comp)) + (map Lazy.force set_map) (#map_cong0 axioms) (Lazy.force map_comp)) |> Thm.close_derivation end; @@ -1254,7 +1254,7 @@ val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def; val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong - in_mono in_rel map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map' + in_mono in_rel map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO; val wits = map2 mk_witness bnf_wits wit_thms; diff -r 5e0623448bdb -r b6c3be868217 src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:56:39 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 23:01:04 2013 +0200 @@ -14,7 +14,7 @@ val mk_map_cong_tac: Proof.context -> thm -> tactic val mk_in_mono_tac: int -> tactic val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic - val mk_set_map': thm -> thm + val mk_set_map: thm -> thm val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic @@ -50,7 +50,7 @@ fun mk_map_cong_tac ctxt cong0 = (hyp_subst_tac ctxt THEN' rtac cong0 THEN' REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1; -fun mk_set_map' set_map0 = set_map0 RS @{thm comp_eq_dest}; +fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest}; fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1 else (rtac subsetI THEN' rtac CollectI) 1 THEN @@ -226,10 +226,10 @@ EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]}, CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_map0s] 1; -fun mk_map_transfer_tac rel_mono in_rel set_map's map_cong0 map_comp +fun mk_map_transfer_tac rel_mono in_rel set_maps map_cong0 map_comp {context = ctxt, prems = _} = let - val n = length set_map's; + val n = length set_maps; in REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN @@ -239,14 +239,14 @@ rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]})) - set_map's, + set_maps, rtac conjI, EVERY' (map (fn convol => rtac (box_equals OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN' REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})]) end; -fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_map's set_bds +fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_maps set_bds bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} = if live = 0 then rtac @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order] @@ -272,7 +272,7 @@ rtac bd_Card_order, rtac @{thm Card_order_csum}, rtac bd_Cnotzero, rtac @{thm csum_Cfinite_cexp_Cinfinite}, rtac (if live = 1 then @{thm card_of_Card_order} else @{thm Card_order_csum}), - CONJ_WRAP_GEN' (rtac @{thm Cfinite_csum}) (K (rtac @{thm Cfinite_cone})) set_map's, + CONJ_WRAP_GEN' (rtac @{thm Cfinite_csum}) (K (rtac @{thm Cfinite_cone})) set_maps, rtac bd'_Cinfinite, rtac @{thm card_of_Card_order}, rtac @{thm Card_order_cexp}, rtac @{thm Cinfinite_cexp}, rtac @{thm ordLeq_csum2}, rtac @{thm Card_order_ctwo}, rtac bd'_Cinfinite, @@ -290,7 +290,7 @@ else REPEAT_DETERM_N (live - 2) o (etac conjE THEN' rotate_tac ~1) THEN' etac conjE, rtac (Drule.rotate_prems 1 @{thm image_eqI}), rtac @{thm SigmaI}, rtac @{thm UNIV_I}, CONJ_WRAP_GEN' (rtac @{thm SigmaI}) - (K (etac @{thm If_the_inv_into_in_Func} THEN' atac)) set_map's, + (K (etac @{thm If_the_inv_into_in_Func} THEN' atac)) set_maps, rtac sym, rtac (Drule.rotate_prems 1 ((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f}, @@ -302,7 +302,7 @@ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, CONJ_WRAP' (fn thm => rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]}) - set_map's, + set_maps, rtac sym, rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]}, map_comp RS sym, map_id])] 1 diff -r 5e0623448bdb -r b6c3be868217 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 22:56:39 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 23:01:04 2013 +0200 @@ -604,7 +604,7 @@ val pre_set_defss = map set_defs_of_bnf pre_bnfs; val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; val nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs; - val nested_set_map's = maps set_map'_of_bnf nested_bnfs; + val nested_set_maps = maps set_map_of_bnf nested_bnfs; val fp_b_names = map base_name_of_typ fpTs; @@ -687,7 +687,7 @@ val thm = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => - mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_map's + mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_maps pre_set_defss) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation; @@ -1170,8 +1170,8 @@ val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_set_defss = map set_defs_of_bnf pre_bnfs; val pre_rel_defs = map rel_def_of_bnf pre_bnfs; - val nesting_set_map's = maps set_map'_of_bnf nesting_bnfs; - val nested_set_map's = maps set_map'_of_bnf nested_bnfs; + val nesting_set_maps = maps set_map_of_bnf nesting_bnfs; + val nested_set_maps = maps set_map_of_bnf nested_bnfs; val live = live_of_bnf any_fp_bnf; val _ = @@ -1330,7 +1330,7 @@ fun mk_set_thm fp_set_thm ctr_def' cxIn = fold_thms lthy [ctr_def'] - (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @ + (unfold_thms lthy (pre_set_defs @ nested_set_maps @ nesting_set_maps @ (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_set) (cterm_instantiate_pos [SOME cxIn] fp_set_thm)) |> singleton (Proof_Context.export names_lthy no_defs_lthy); diff -r 5e0623448bdb -r b6c3be868217 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Aug 29 22:56:39 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Aug 29 23:01:04 2013 +0200 @@ -119,26 +119,26 @@ hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN' (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI}); -fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs = +fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs = HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, - SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_map's @ sum_prod_thms_set0)), + SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_maps @ sum_prod_thms_set0)), solve_prem_prem_tac ctxt]) (rev kks))); -fun mk_induct_discharge_prem_tac ctxt nn n set_map's pre_set_defs m k kks = +fun mk_induct_discharge_prem_tac ctxt nn n set_maps pre_set_defs m k kks = let val r = length kks in HEADGOAL (EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt, REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)]) THEN EVERY [REPEAT_DETERM_N r (HEADGOAL (rotate_tac ~1 THEN' dtac meta_mp THEN' rotate_tac 1) THEN prefer_tac 2), if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, HEADGOAL atac, - mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs] + mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs] end; -fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_map's pre_set_defss = +fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_maps pre_set_defss = let val n = Integer.sum ns in unfold_thms_tac ctxt ctr_defs THEN HEADGOAL (rtac ctor_induct' THEN' inst_as_projs_tac ctxt) THEN - EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_map's) pre_set_defss + EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_maps) pre_set_defss mss (unflat mss (1 upto n)) kkss) end; diff -r 5e0623448bdb -r b6c3be868217 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 22:56:39 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 23:01:04 2013 +0200 @@ -222,7 +222,7 @@ val map_ids = map map_id_of_bnf bnfs; val map_wpulls = map map_wpull_of_bnf bnfs; val set_bdss = map set_bd_of_bnf bnfs; - val set_map'ss = map set_map'_of_bnf bnfs; + val set_mapss = map set_map_of_bnf bnfs; val rel_congs = map rel_cong_of_bnf bnfs; val rel_converseps = map rel_conversep_of_bnf bnfs; val rel_Grps = map rel_Grp_of_bnf bnfs; @@ -809,7 +809,7 @@ Goal.prove_sorry lthy [] [] (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs) (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs))) - (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_map'ss)) + (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_mapss)) |> Thm.close_derivation end; @@ -1209,7 +1209,7 @@ val coalgT_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs))) - (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_map'ss) + (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss) |> Thm.close_derivation; val timer = time (timer "Tree coalgebra"); @@ -1578,7 +1578,7 @@ to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss - set_map'ss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms) + set_mapss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms) |> Thm.close_derivation; val timer = time (timer "Behavioral morphism"); @@ -1617,7 +1617,7 @@ val coalg_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As car_finalAs str_finalAs))) (K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms - set_map'ss coalgT_set_thmss)) + set_mapss coalgT_set_thmss)) |> Thm.close_derivation; val mor_T_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As @@ -2292,7 +2292,7 @@ map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs => singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) - (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_map'ss)) + (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_mapss)) |> Thm.close_derivation) goals ctss hset_rec_0ss' hset_rec_Sucss'; in @@ -2360,7 +2360,7 @@ val thm = singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal - (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_map_thms map_cong0s set_map'ss + (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_map_thms map_cong0s set_mapss set_hset_thmss set_hset_hset_thmsss))) |> Thm.close_derivation in @@ -2396,7 +2396,7 @@ (Logic.mk_implies (wpull_prem, coalg)); in Goal.prove_sorry lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms - set_map'ss pickWP_assms_tacs) + set_mapss pickWP_assms_tacs) |> Thm.close_derivation end; @@ -2447,7 +2447,7 @@ val thms = map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs => singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal - (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_map'ss + (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_mapss map_wpull_thms pickWP_assms_tacs)) |> Thm.close_derivation) ls goals ctss hset_rec_0ss' hset_rec_Sucss'; @@ -2633,7 +2633,7 @@ in map2 (fn goal => fn induct => Goal.prove_sorry lthy [] [] goal - (mk_coind_wit_tac induct dtor_unfold_thms (flat set_map'ss) wit_thms) + (mk_coind_wit_tac induct dtor_unfold_thms (flat set_mapss) wit_thms) |> Thm.close_derivation) goals dtor_hset_induct_thms |> map split_conj_thm @@ -2707,7 +2707,7 @@ dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss)) |> Thm.close_derivation) ks goals in_rels map_comps map_cong0s folded_dtor_map_thms folded_dtor_set_thmss' - dtor_inject_thms dtor_ctor_thms set_map'ss dtor_set_incl_thmss + dtor_inject_thms dtor_ctor_thms set_mapss dtor_set_incl_thmss dtor_set_set_incl_thmsss end; @@ -2802,7 +2802,7 @@ (map6 (mk_helper_coind_concl false) activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds)); val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comps - map_cong0s map_arg_cong_thms set_map'ss dtor_unfold_thms folded_dtor_map_thms; + map_cong0s map_arg_cong_thms set_mapss dtor_unfold_thms folded_dtor_map_thms; fun mk_helper_coind_thms vars concl = Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Jphis @ activeJphis @ vars @ zips) @@ -2831,7 +2831,7 @@ Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Jphis @ activeJphis @ zip_zs @ zips) (Logic.list_implies (helper_prems, concl))) - (mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_map'ss j set_induct) + (mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_mapss j set_induct) |> Thm.close_derivation |> split_conj_thm) mk_helper_ind_concls ls dtor_set_induct_thms diff -r 5e0623448bdb -r b6c3be868217 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 22:56:39 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 23:01:04 2013 +0200 @@ -165,7 +165,7 @@ val map_id0s = map map_id0_of_bnf bnfs; val map_ids = map map_id_of_bnf bnfs; val map_wpulls = map map_wpull_of_bnf bnfs; - val set_map'ss = map set_map'_of_bnf bnfs; + val set_mapss = map set_map_of_bnf bnfs; val timer = time (timer "Extracted terms & thms"); @@ -404,7 +404,7 @@ Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs) (Logic.list_implies (prems, concl))) - (K (mk_mor_comp_tac mor_def set_map'ss map_comp_id_thms)) + (K (mk_mor_comp_tac mor_def set_mapss map_comp_id_thms)) |> Thm.close_derivation end; @@ -422,8 +422,7 @@ Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ inv_fs) (Logic.list_implies (prems, concl))) - (K (mk_mor_inv_tac alg_def mor_def - set_map'ss morE_thms map_comp_id_thms map_cong0L_thms)) + (K (mk_mor_inv_tac alg_def mor_def set_mapss morE_thms map_comp_id_thms map_cong0L_thms)) |> Thm.close_derivation end; @@ -528,7 +527,7 @@ val copy_str_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs) (Logic.list_implies (all_prems, alg))) - (K (mk_copy_str_tac set_map'ss alg_def alg_set_thms)) + (K (mk_copy_str_tac set_mapss alg_def alg_set_thms)) |> Thm.close_derivation; val iso = HOLogic.mk_Trueprop @@ -536,7 +535,7 @@ val copy_alg_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs) (Logic.list_implies (all_prems, iso))) - (K (mk_copy_alg_tac set_map'ss alg_set_thms mor_def iso_alt_thm copy_str_thm)) + (K (mk_copy_alg_tac set_mapss alg_set_thms mor_def iso_alt_thm copy_str_thm)) |> Thm.close_derivation; val ex = HOLogic.mk_Trueprop @@ -883,7 +882,7 @@ Goal.prove_sorry lthy [] [] (fold_rev Logic.all (iidx :: Bs @ ss @ Asuc_fs) (Logic.list_implies (prems, concl))) (K (mk_mor_select_tac mor_def mor_cong_thm mor_comp_thm mor_incl_min_alg_thm alg_def - alg_select_thm alg_set_thms set_map'ss str_init_defs)) + alg_select_thm alg_set_thms set_mapss str_init_defs)) |> Thm.close_derivation end; @@ -1335,7 +1334,7 @@ in (Goal.prove_sorry lthy [] [] (fold_rev Logic.all (phis @ Izs) goal) - (K (mk_ctor_induct_tac lthy m set_map'ss init_induct_thm morE_thms mor_Abs_thm + (K (mk_ctor_induct_tac lthy m set_mapss init_induct_thm morE_thms mor_Abs_thm Rep_inverses Abs_inverses Reps)) |> Thm.close_derivation, rev (Term.add_tfrees goal [])) @@ -1538,7 +1537,7 @@ Goal.prove_sorry lthy [] [] goal (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats))) |> Thm.close_derivation) - set_map'ss) ls simp_goalss setss; + set_mapss) ls simp_goalss setss; in ctor_setss end; @@ -1579,7 +1578,7 @@ (map4 (mk_set_map0 f) fs_maps Izs sets sets'))) fs setss_by_range setss_by_range'; - fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_map'ss ctor_map_thms; + fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_mapss ctor_map_thms; val thms = map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i => singleton (Proof_Context.export names_lthy lthy) @@ -1781,7 +1780,7 @@ ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss)) |> Thm.close_derivation) ks goals in_rels map_comps map_cong0s folded_ctor_map_thms folded_ctor_set_thmss' - ctor_inject_thms ctor_dtor_thms set_map'ss ctor_set_incl_thmss + ctor_inject_thms ctor_dtor_thms set_mapss ctor_set_incl_thmss ctor_set_set_incl_thmsss end; diff -r 5e0623448bdb -r b6c3be868217 src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:56:39 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 23:01:04 2013 +0200 @@ -122,39 +122,39 @@ CONJ_WRAP' (fn thm => (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_ids) 1; -fun mk_mor_comp_tac mor_def set_map's map_comp_ids = +fun mk_mor_comp_tac mor_def set_maps map_comp_ids = let val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac]; - fun mor_tac (set_map', map_comp_id) = + fun mor_tac (set_map, map_comp_id) = EVERY' [rtac ballI, stac o_apply, rtac trans, rtac trans, dtac rev_bspec, atac, etac arg_cong, REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN' CONJ_WRAP' (fn thm => FIRST' [rtac subset_UNIV, (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, - etac bspec, etac set_mp, atac])]) set_map' THEN' + etac bspec, etac set_mp, atac])]) set_map THEN' rtac (map_comp_id RS arg_cong); in (dtac (mor_def RS subst) THEN' dtac (mor_def RS subst) THEN' stac mor_def THEN' REPEAT o etac conjE THEN' rtac conjI THEN' - CONJ_WRAP' (K fbetw_tac) set_map's THEN' - CONJ_WRAP' mor_tac (set_map's ~~ map_comp_ids)) 1 + CONJ_WRAP' (K fbetw_tac) set_maps THEN' + CONJ_WRAP' mor_tac (set_maps ~~ map_comp_ids)) 1 end; -fun mk_mor_inv_tac alg_def mor_def set_map's morEs map_comp_ids map_cong0Ls = +fun mk_mor_inv_tac alg_def mor_def set_maps morEs map_comp_ids map_cong0Ls = let val fbetw_tac = EVERY' [rtac ballI, etac set_mp, etac imageI]; - fun Collect_tac set_map' = + fun Collect_tac set_map = CONJ_WRAP' (fn thm => FIRST' [rtac subset_UNIV, (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans, - etac @{thm image_mono}, atac])]) set_map'; - fun mor_tac (set_map', ((morE, map_comp_id), map_cong0L)) = + etac @{thm image_mono}, atac])]) set_map; + fun mor_tac (set_map, ((morE, map_comp_id), map_cong0L)) = EVERY' [rtac ballI, ftac rev_bspec, atac, REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym, - etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_map', - rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map', + etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_map, + rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map, rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_cong0L RS arg_cong), REPEAT_DETERM_N (length morEs) o (EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])]; @@ -164,8 +164,8 @@ dtac (alg_def RS iffD1) THEN' REPEAT o etac conjE THEN' rtac conjI THEN' - CONJ_WRAP' (K fbetw_tac) set_map's THEN' - CONJ_WRAP' mor_tac (set_map's ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1 + CONJ_WRAP' (K fbetw_tac) set_maps THEN' + CONJ_WRAP' mor_tac (set_maps ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1 end; fun mk_mor_str_tac ks mor_def = @@ -211,7 +211,7 @@ (rtac iffI THEN' if_tac THEN' only_if_tac) 1 end; -fun mk_copy_str_tac set_map's alg_def alg_sets = +fun mk_copy_str_tac set_maps alg_def alg_sets = let val n = length alg_sets; val bij_betw_inv_tac = @@ -225,13 +225,13 @@ EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp, rtac equalityD1, etac @{thm bij_betw_imageE}, rtac imageI, etac thm, REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)]) - (set_map's ~~ alg_sets); + (set_maps ~~ alg_sets); in (rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN' stac alg_def THEN' copy_str_tac) 1 end; -fun mk_copy_alg_tac set_map's alg_sets mor_def iso_alt copy_str = +fun mk_copy_alg_tac set_maps alg_sets mor_def iso_alt copy_str = let val n = length alg_sets; val fbetw_tac = CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets; @@ -243,7 +243,7 @@ CONJ_WRAP' (fn (thms, thm) => EVERY' [rtac ballI, etac CollectE, etac @{thm inverE}, etac thm, REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)]) - (set_map's ~~ alg_sets); + (set_maps ~~ alg_sets); in (rtac (iso_alt RS iffD2) THEN' etac copy_str THEN' REPEAT_DETERM o atac THEN' @@ -390,25 +390,25 @@ EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt] 1 THEN unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1; -fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select - alg_sets set_map's str_init_defs = +fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select alg_sets + set_maps str_init_defs = let val n = length alg_sets; val fbetw_tac = CONJ_WRAP' (K (EVERY' [rtac ballI, etac rev_bspec, etac CollectE, atac])) alg_sets; val mor_tac = CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs; - fun alg_epi_tac ((alg_set, str_init_def), set_map') = + fun alg_epi_tac ((alg_set, str_init_def), set_map) = EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, rtac ballI, ftac (alg_select RS bspec), stac str_init_def, etac alg_set, REPEAT_DETERM o FIRST' [rtac subset_UNIV, - EVERY' [rtac ord_eq_le_trans, resolve_tac set_map', rtac subset_trans, + EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans, etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]]; in (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm o_id}) THEN' rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN' stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' rtac mor_incl_min_alg THEN' - stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_map's)) 1 + stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)) 1 end; fun mk_init_ex_mor_tac Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs @@ -534,21 +534,21 @@ (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN etac fold_unique_mor 1; -fun mk_ctor_induct_tac ctxt m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = +fun mk_ctor_induct_tac ctxt m set_mapss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = let - val n = length set_map'ss; + val n = length set_mapss; val ks = 1 upto n; - fun mk_IH_tac Rep_inv Abs_inv set_map' = + fun mk_IH_tac Rep_inv Abs_inv set_map = DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS subst), etac bspec, - dtac set_rev_mp, rtac equalityD1, rtac set_map', etac imageE, + dtac set_rev_mp, rtac equalityD1, rtac set_map, etac imageE, hyp_subst_tac ctxt, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac]; - fun mk_closed_tac (k, (morE, set_map's)) = + fun mk_closed_tac (k, (morE, set_maps)) = EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI, rtac (mor_Abs RS morE RS arg_cong RS ssubst), atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec}, - EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_map's)), atac]; + EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac]; fun mk_induct_tac (Rep, Rep_inv) = EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RSN (2, bspec))]; @@ -556,7 +556,7 @@ (rtac mp THEN' rtac impI THEN' DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN' rtac init_induct THEN' - DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_map'ss))) 1 + DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_mapss))) 1 end; fun mk_ctor_induct2_tac cTs cts ctor_induct weak_ctor_inducts {context = ctxt, prems = _} = @@ -592,19 +592,19 @@ fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac sym, rtac o_apply] 1; -fun mk_ctor_set_tac set set_map' set_map's = +fun mk_ctor_set_tac set set_map set_maps = let - val n = length set_map's; + val n = length set_maps; fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN' rtac @{thm Union_image_eq}; in EVERY' [rtac (set RS @{thm comp_eq_dest} RS trans), rtac Un_cong, - rtac (trans OF [set_map', trans_fun_cong_image_id_id_apply]), + rtac (trans OF [set_map, trans_fun_cong_image_id_id_apply]), REPEAT_DETERM_N (n - 1) o rtac Un_cong, - EVERY' (map mk_UN set_map's)] 1 + EVERY' (map mk_UN set_maps)] 1 end; -fun mk_set_nat_tac m induct_tac set_map'ss +fun mk_set_nat_tac m induct_tac set_mapss ctor_maps csets ctor_sets i {context = ctxt, prems = _} = let val n = length ctor_maps; @@ -621,7 +621,7 @@ REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]), EVERY' (map useIH (drop m set_nats))]; in - (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_map'ss)) 1 + (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1 end; fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i {context = ctxt, prems = _} =