# HG changeset patch # User blanchet # Date 1366818442 -7200 # Node ID f19a4d0ab1bf261116a7bb79c4f39db283748a4d # Parent 224b6eb2313a6ff2e0eb081498623aad6e10a13f renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Wed Apr 24 17:47:22 2013 +0200 @@ -442,12 +442,12 @@ proof (cases "n \ m") case False thus ?thesis unfolding smerge_def by (subst stream_set_flat) - (auto simp: stream.set_natural' 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 stream_set_flat) - (auto simp: stream.set_natural' 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 @@ -456,7 +456,7 @@ fix x assume "x \ stream_set (smerge ss)" thus "x \ UNION (stream_set ss) stream_set" unfolding smerge_def by (subst (asm) stream_set_flat) - (auto simp: stream.set_natural' in_set_conv_nth stream_set_range simp del: stake.simps, fast+) + (auto simp: stream.set_map' in_set_conv_nth stream_set_range simp del: stake.simps, fast+) next fix s x assume "s \ stream_set ss" "x \ stream_set s" thus "x \ stream_set (smerge ss)" using snth_stream_set_smerge by (auto simp: stream_set_range) @@ -469,7 +469,7 @@ "sproduct s1 s2 = smerge (stream_map (\x. stream_map (Pair x) s2) s1)" lemma stream_set_sproduct: "stream_set (sproduct s1 s2) = stream_set s1 \ stream_set s2" - unfolding sproduct_def stream_set_smerge by (auto simp: stream.set_natural') + unfolding sproduct_def stream_set_smerge by (auto simp: stream.set_map') subsection {* interleave two streams *} diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Examples/TreeFI.thy --- a/src/HOL/BNF/Examples/TreeFI.thy Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Examples/TreeFI.thy Wed Apr 24 17:47:22 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_natural') +by (auto simp add: listF.set_map') lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)" unfolding lab_def sub_def treeFI_case_def diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Wed Apr 24 17:47:22 2013 +0200 @@ -353,7 +353,7 @@ apply transfer apply simp done -lemmas [simp] = fset.map_comp' fset.map_id' fset.set_natural' +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 @@ -422,7 +422,7 @@ "{(x, y). R x y} \ A \ B = {(x, y). R x y \ x \ A \ y \ B}" by auto -lemma rcset_natural': "rcset (cIm f x) = f ` rcset x" +lemma rcset_map': "rcset (cIm f x) = f ` rcset x" unfolding cIm_def[abs_def] by simp definition cset_rel :: "('a \ 'b \ bool) \ 'a cset \ 'b cset \ bool" where @@ -455,9 +455,9 @@ assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold apply (simp add: subset_eq Ball_def) apply (rule conjI) - apply (clarsimp, metis (lifting, no_types) rcset_natural' image_iff surjective_pairing) + apply (clarsimp, metis (lifting, no_types) rcset_map' image_iff surjective_pairing) apply (clarsimp) - by (metis Domain.intros Range.simps rcset_natural' fst_eq_Domain snd_eq_Range) + by (metis Domain.intros Range.simps rcset_map' fst_eq_Domain snd_eq_Range) qed bnf_def cIm [rcset] "\_::'a cset. natLeq" ["cEmp"] cset_rel @@ -1151,7 +1151,7 @@ Plus: "\R a b; multiset_rel' R M N\ \ multiset_rel' R (M + {#a#}) (N + {#b#})" lemma multiset_map_Zero_iff[simp]: "multiset_map f M = {#} \ M = {#}" -by (metis image_is_empty multiset.set_natural' set_of_eq_empty_iff) +by (metis image_is_empty multiset.set_map' set_of_eq_empty_iff) lemma multiset_map_Zero[simp]: "multiset_map f {#} = {#}" by simp @@ -1287,7 +1287,7 @@ shows "\ N1. N = N1 + {#f a#} \ multiset_map f M = N1" proof- have "f a \# N" - using assms multiset.set_natural'[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 "multiset_map f M = N1" using assms unfolding N by simp thus ?thesis using N by blast @@ -1298,7 +1298,7 @@ shows "\ M1 a. M = M1 + {#a#} \ f a = b \ multiset_map f M1 = N" proof- obtain a where a: "a \# M" and fa: "f a = b" - using multiset.set_natural'[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 "multiset_map f M1 = N" using assms unfolding M fa[symmetric] by simp diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Apr 24 17:47:22 2013 +0200 @@ -157,12 +157,12 @@ mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer) (map map_comp_of_bnf inners); - fun mk_single_set_natural_tac i _ = - mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer) - (collect_set_natural_of_bnf outer) - (map ((fn thms => nth thms i) o set_natural_of_bnf) inners); + fun mk_single_set_map_tac i _ = + mk_comp_set_map_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer) + (collect_set_map_of_bnf outer) + (map ((fn thms => nth thms i) o set_map_of_bnf) inners); - val set_natural_tacs = map mk_single_set_natural_tac (0 upto ilive - 1); + val set_map_tacs = map mk_single_set_map_tac (0 upto ilive - 1); fun bd_card_order_tac _ = mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer); @@ -177,7 +177,7 @@ map (fn goal => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => - mk_comp_set_alt_tac ctxt (collect_set_natural_of_bnf outer)) + mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer)) |> Thm.close_derivation) (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt); @@ -238,7 +238,7 @@ unfold_thms_tac lthy basic_thms THEN rtac thm 1 end; - val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac + val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; @@ -257,7 +257,7 @@ |> map (fn (frees, t) => fold absfree frees t); fun wit_tac {context = ctxt, prems = _} = - mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer) + mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer) (maps wit_thms_of_bnf inners); val (bnf', lthy') = @@ -311,7 +311,7 @@ rtac refl 1; fun map_cong0_tac {context = ctxt, prems = _} = mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf); - val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf)); + val set_map_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map_of_bnf bnf)); fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf); fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf); val set_bd_tacs = @@ -348,7 +348,7 @@ rtac thm 1 end; - val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac + val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; @@ -405,12 +405,12 @@ rtac refl 1; fun map_cong0_tac {context = ctxt, prems = _} = rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); - val set_natural_tacs = + val set_map_tacs = if ! quick_and_dirty then replicate (n + live) (K all_tac) else replicate n (K empty_natural_tac) @ - map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf); + map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf); fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; val set_bd_tacs = @@ -435,7 +435,7 @@ fun srel_O_Gr_tac _ = mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm; - val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac + val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); @@ -490,7 +490,7 @@ fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1; fun map_cong0_tac {context = ctxt, prems = _} = rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); - val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf)); + val set_map_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf)); fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf)); @@ -512,7 +512,7 @@ fun srel_O_Gr_tac _ = mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm; - val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac + val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); @@ -653,7 +653,7 @@ SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1; val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf)) - (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf)) + (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd) (mk_tac (map_wpull_of_bnf bnf)) (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf))); diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Tools/bnf_comp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Apr 24 17:47:22 2013 +0200 @@ -17,7 +17,7 @@ val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic val mk_comp_set_alt_tac: Proof.context -> thm -> tactic val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic - val mk_comp_set_natural_tac: thm -> thm -> thm -> thm list -> tactic + val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic val mk_kill_bd_card_order_tac: int -> thm -> tactic @@ -64,9 +64,9 @@ (* Composition *) -fun mk_comp_set_alt_tac ctxt collect_set_natural = +fun mk_comp_set_alt_tac ctxt collect_set_map = unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN - unfold_thms_tac ctxt [collect_set_natural RS sym] THEN + unfold_thms_tac ctxt [collect_set_map RS sym] THEN rtac refl 1; fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids = @@ -78,21 +78,21 @@ rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ map (fn thm => rtac (thm RS sym RS fun_cong)) map_comps) 1; -fun mk_comp_set_natural_tac Gmap_comp Gmap_cong0 Gset_natural set_naturals = +fun mk_comp_set_map_tac Gmap_comp Gmap_cong0 Gset_map set_maps = EVERY' ([rtac ext] @ replicate 3 (rtac trans_o_apply) @ [rtac (arg_cong_Union RS trans), rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans), rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ - map (fn thm => rtac (thm RS fun_cong)) set_naturals @ - [rtac (Gset_natural RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, + map (fn thm => rtac (thm RS fun_cong)) set_maps @ + [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply, - rtac (@{thm image_cong} OF [Gset_natural RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), + rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), rtac @{thm trans[OF pointfreeE[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]}, rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ - [REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac @{thm trans[OF image_insert]}, + [REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]}, rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply, rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]}, rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}], @@ -217,9 +217,9 @@ val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def Union_image_insert Union_image_empty}; -fun mk_comp_wit_tac ctxt Gwit_thms collect_set_natural Fwit_thms = +fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms = ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN - unfold_thms_tac ctxt (collect_set_natural :: comp_wit_thms) THEN + unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN REPEAT_DETERM ( atac 1 ORELSE REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Apr 24 17:47:22 2013 +0200 @@ -45,7 +45,7 @@ val bd_Cnotzero_of_bnf: BNF -> thm val bd_card_order_of_bnf: BNF -> thm val bd_cinfinite_of_bnf: BNF -> thm - val collect_set_natural_of_bnf: BNF -> thm + val collect_set_map_of_bnf: BNF -> thm val in_bd_of_bnf: BNF -> thm val in_cong_of_bnf: BNF -> thm val in_mono_of_bnf: BNF -> thm @@ -65,8 +65,8 @@ val rel_srel_of_bnf: BNF -> thm val set_bd_of_bnf: BNF -> thm list val set_defs_of_bnf: BNF -> thm list - val set_natural'_of_bnf: BNF -> thm list - val set_natural_of_bnf: BNF -> thm list + val set_map'_of_bnf: BNF -> thm list + val set_map_of_bnf: BNF -> thm list val srel_def_of_bnf: BNF -> thm val srel_Gr_of_bnf: BNF -> thm val srel_Id_of_bnf: BNF -> thm @@ -111,7 +111,7 @@ map_id: thm, map_comp: thm, map_cong0: thm, - set_natural: thm list, + set_map: thm list, bd_card_order: thm, bd_cinfinite: thm, set_bd: thm list, @@ -121,7 +121,7 @@ }; fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), srel) = - {map_id = id, map_comp = comp, map_cong0 = cong, set_natural = nat, bd_card_order = c_o, + {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o, bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, srel_O_Gr = srel}; fun dest_cons [] = raise Empty @@ -144,17 +144,17 @@ fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull srel = [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, srel]; -fun dest_axioms {map_id, map_comp, map_cong0, set_natural, bd_card_order, bd_cinfinite, set_bd, - in_bd, map_wpull, srel_O_Gr} = - zip_axioms map_id map_comp map_cong0 set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull +fun dest_axioms {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, in_bd, + map_wpull, srel_O_Gr} = + zip_axioms map_id map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd in_bd map_wpull srel_O_Gr; -fun map_axioms f {map_id, map_comp, map_cong0, set_natural, bd_card_order, bd_cinfinite, set_bd, +fun map_axioms f {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, in_bd, map_wpull, srel_O_Gr} = {map_id = f map_id, map_comp = f map_comp, map_cong0 = f map_cong0, - set_natural = map f set_natural, + set_map = map f set_map, bd_card_order = f bd_card_order, bd_cinfinite = f bd_cinfinite, set_bd = map f set_bd, @@ -182,7 +182,7 @@ bd_Card_order: thm, bd_Cinfinite: thm, bd_Cnotzero: thm, - collect_set_natural: thm lazy, + collect_set_map: thm lazy, in_cong: thm lazy, in_mono: thm lazy, in_srel: thm lazy, @@ -193,7 +193,7 @@ rel_eq: thm lazy, rel_flip: thm lazy, rel_srel: thm lazy, - set_natural': thm lazy list, + set_map': thm lazy list, srel_cong: thm lazy, srel_mono: thm lazy, srel_Id: thm lazy, @@ -202,13 +202,13 @@ srel_O: thm lazy }; -fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel - map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_natural' srel_cong srel_mono +fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono in_srel + map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_map' srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, bd_Cnotzero = bd_Cnotzero, - collect_set_natural = collect_set_natural, + collect_set_map = collect_set_map, in_cong = in_cong, in_mono = in_mono, in_srel = in_srel, @@ -219,7 +219,7 @@ rel_eq = rel_eq, rel_flip = rel_flip, rel_srel = rel_srel, - set_natural' = set_natural', + set_map' = set_map', srel_cong = srel_cong, srel_mono = srel_mono, srel_Id = srel_Id, @@ -231,7 +231,7 @@ bd_Card_order, bd_Cinfinite, bd_Cnotzero, - collect_set_natural, + collect_set_map, in_cong, in_mono, in_srel, @@ -242,7 +242,7 @@ rel_eq, rel_flip, rel_srel, - set_natural', + set_map', srel_cong, srel_mono, srel_Id, @@ -252,7 +252,7 @@ {bd_Card_order = f bd_Card_order, bd_Cinfinite = f bd_Cinfinite, bd_Cnotzero = f bd_Cnotzero, - collect_set_natural = Lazy.map f collect_set_natural, + collect_set_map = Lazy.map f collect_set_map, in_cong = Lazy.map f in_cong, in_mono = Lazy.map f in_mono, in_srel = Lazy.map f in_srel, @@ -263,7 +263,7 @@ rel_eq = Lazy.map f rel_eq, rel_flip = Lazy.map f rel_flip, rel_srel = Lazy.map f rel_srel, - set_natural' = map (Lazy.map f) set_natural', + set_map' = map (Lazy.map f) set_map', srel_cong = Lazy.map f srel_cong, srel_mono = Lazy.map f srel_mono, srel_Id = Lazy.map f srel_Id, @@ -368,7 +368,7 @@ val bd_Card_order_of_bnf = #bd_Card_order o #facts o rep_bnf; val bd_Cinfinite_of_bnf = #bd_Cinfinite o #facts o rep_bnf; val bd_Cnotzero_of_bnf = #bd_Cnotzero o #facts o rep_bnf; -val collect_set_natural_of_bnf = Lazy.force o #collect_set_natural o #facts o rep_bnf; +val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf; val in_bd_of_bnf = #in_bd o #axioms o rep_bnf; val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf; val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf; @@ -388,8 +388,8 @@ val rel_srel_of_bnf = Lazy.force o #rel_srel o #facts o rep_bnf; 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_natural_of_bnf = #set_natural o #axioms o rep_bnf; -val set_natural'_of_bnf = map Lazy.force o #set_natural' o #facts o rep_bnf; +val set_map_of_bnf = #set_map o #axioms o rep_bnf; +val set_map'_of_bnf = map Lazy.force o #set_map' o #facts o rep_bnf; val srel_cong_of_bnf = Lazy.force o #srel_cong o #facts o rep_bnf; val srel_mono_of_bnf = Lazy.force o #srel_mono o #facts o rep_bnf; val srel_def_of_bnf = #srel_def o #defs o rep_bnf; @@ -507,7 +507,7 @@ val bd_Card_orderN = "bd_Card_order"; val bd_CinfiniteN = "bd_Cinfinite"; val bd_CnotzeroN = "bd_Cnotzero"; -val collect_set_naturalN = "collect_set_natural"; +val collect_set_mapN = "collect_set_map"; val in_bdN = "in_bd"; val in_monoN = "in_mono"; val in_srelN = "in_srel"; @@ -521,8 +521,8 @@ val rel_eqN = "rel_eq"; val rel_flipN = "rel_flip"; val rel_srelN = "rel_srel"; -val set_naturalN = "set_natural"; -val set_natural'N = "set_natural'"; +val set_mapN = "set_map"; +val set_map'N = "set_map'"; val set_bdN = "set_bd"; val srel_IdN = "srel_Id"; val srel_GrN = "srel_Gr"; @@ -835,7 +835,7 @@ fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq)) end; - val set_naturals_goal = + val set_maps_goal = let fun mk_goal setA setB f = let @@ -897,8 +897,8 @@ val srel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (srel, Rs), O_Gr)); - val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_naturals_goal - card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal; + val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_maps_goal card_order_bd_goal + cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal; fun mk_wit_goals (I, wit) = let @@ -928,7 +928,7 @@ val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order]; val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero}; - fun mk_collect_set_natural () = + fun mk_collect_set_map () = let val defT = mk_bnf_T Ts CA --> HOLogic.mk_setT T; val collect_map = HOLogic.mk_comp @@ -940,11 +940,11 @@ (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*) val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect)); in - Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_natural_tac (#set_natural axioms))) + Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map axioms))) |> Thm.close_derivation end; - val collect_set_natural = Lazy.lazy mk_collect_set_natural; + val collect_set_map = Lazy.lazy mk_collect_set_map; fun mk_in_mono () = let @@ -992,8 +992,7 @@ val map_cong = Lazy.lazy mk_map_cong; - val set_natural' = - map (fn thm => Lazy.lazy (fn () => mk_set_natural' thm)) (#set_natural axioms); + val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map axioms); fun mk_map_wppull () = let @@ -1027,7 +1026,7 @@ in Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong0 axioms) - (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_natural')) + (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_map')) |> Thm.close_derivation end; @@ -1043,7 +1042,7 @@ in Goal.prove_sorry lthy [] [] goal (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id') - (Lazy.force map_comp') (map Lazy.force set_natural')) + (Lazy.force map_comp') (map Lazy.force set_map')) |> Thm.close_derivation end; @@ -1096,7 +1095,7 @@ val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs)); val le_thm = Goal.prove_sorry lthy [] [] le_goal (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms) - (Lazy.force map_comp') (map Lazy.force set_natural')) + (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 @@ -1116,7 +1115,7 @@ in Goal.prove_sorry lthy [] [] goal (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms) - (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural')) + (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_map')) |> Thm.close_derivation end; @@ -1176,9 +1175,9 @@ val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def; - val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong - in_mono in_srel map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel - set_natural' srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O; + val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono + in_srel map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_map' + srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O; val wits = map2 mk_witness bnf_wits wit_thms; @@ -1200,14 +1199,14 @@ (bd_Card_orderN, [#bd_Card_order facts]), (bd_CinfiniteN, [#bd_Cinfinite facts]), (bd_CnotzeroN, [#bd_Cnotzero facts]), - (collect_set_naturalN, [Lazy.force (#collect_set_natural facts)]), + (collect_set_mapN, [Lazy.force (#collect_set_map facts)]), (in_bdN, [#in_bd axioms]), (in_monoN, [Lazy.force (#in_mono facts)]), (in_srelN, [Lazy.force (#in_srel facts)]), (map_compN, [#map_comp axioms]), (map_idN, [#map_id axioms]), (map_wpullN, [#map_wpull axioms]), - (set_naturalN, #set_natural axioms), + (set_mapN, #set_map axioms), (set_bdN, #set_bd axioms)] @ (witNs ~~ wit_thms) |> map (fn (thmN, thms) => @@ -1228,7 +1227,7 @@ (rel_eqN, [Lazy.force (#rel_eq facts)], []), (rel_flipN, [Lazy.force (#rel_flip facts)], []), (rel_srelN, [Lazy.force (#rel_srel facts)], []), - (set_natural'N, map Lazy.force (#set_natural' facts), []), + (set_map'N, map Lazy.force (#set_map' facts), []), (srel_O_GrN, srel_O_Grs, []), (srel_IdN, [Lazy.force (#srel_Id facts)], []), (srel_GrN, [Lazy.force (#srel_Gr facts)], []), diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Wed Apr 24 17:47:22 2013 +0200 @@ -8,13 +8,13 @@ signature BNF_DEF_TACTICS = sig - val mk_collect_set_natural_tac: thm list -> tactic + val mk_collect_set_map_tac: thm list -> tactic val mk_map_id': thm -> thm val mk_map_comp': thm -> thm val mk_map_cong_tac: thm -> tactic val mk_in_mono_tac: int -> tactic val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic - val mk_set_natural': thm -> thm + val mk_set_map': thm -> thm val mk_srel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic @@ -39,7 +39,7 @@ fun mk_map_cong_tac cong0 = (hyp_subst_tac THEN' rtac cong0 THEN' REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1; -fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE}; +fun mk_set_map' set_map = set_map RS @{thm pointfreeE}; fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1 else (rtac subsetI THEN' rtac CollectI) 1 THEN @@ -48,15 +48,15 @@ ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN (etac subset_trans THEN' atac) 1; -fun mk_collect_set_natural_tac set_naturals = +fun mk_collect_set_map_tac set_maps = (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN' - EVERY' (map (fn set_natural => + EVERY' (map (fn set_map => rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' - rtac set_natural) set_naturals) THEN' + rtac set_map) set_maps) THEN' rtac @{thm image_empty}) 1; -fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_naturals = - if null set_naturals then +fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_maps = + if null set_maps then EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull, @@ -64,19 +64,19 @@ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) - set_naturals, + set_maps, CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans), rtac (map_comp RS trans RS sym), rtac map_cong0, - REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans), + REPEAT_DETERM_N (length set_maps) o EVERY' [rtac (o_apply RS trans), rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm, rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1; -fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_naturals +fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_maps {context = ctxt, prems = _} = let - val n = length set_naturals; + val n = length set_maps; in - if null set_naturals then + if null set_maps then unfold_thms_tac ctxt srel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1 else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN EVERY' [rtac equalityI, rtac subsetI, @@ -93,7 +93,7 @@ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, - stac @{thm fst_conv}, atac]) set_naturals, + stac @{thm fst_conv}, atac]) set_maps, rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE], REPEAT_DETERM o dtac Pair_eqD, REPEAT_DETERM o etac conjE, hyp_subst_tac, @@ -108,7 +108,7 @@ CONJ_WRAP' (fn thm => EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI}, rtac @{thm convol_memI[of id _ "%x. x", OF id_apply refl]}, etac set_mp, atac]) - set_naturals]) + set_maps]) @{thms fst_convol snd_convol} [map_id', refl])] 1 end; @@ -125,12 +125,12 @@ rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac, rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1; -fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_naturals +fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_maps {context = ctxt, prems = _} = let - val n = length set_naturals; + val n = length set_maps; in - if null set_naturals then + if null set_maps then unfold_thms_tac ctxt [srel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1 else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN EVERY' [rtac @{thm subrelI}, @@ -143,22 +143,22 @@ rtac map_cong0, REPEAT_DETERM_N n o rtac thm, rtac (map_comp RS sym), rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), - etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 + etac @{thm flip_rel}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 end; fun mk_srel_converse_tac le_converse = EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift}, rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1; -fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_naturals +fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_maps {context = ctxt, prems = _} = let - val n = length set_naturals; + val n = length set_maps; fun in_tac nthO_in = rtac CollectI THEN' CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), - rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals; + rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps; in - if null set_naturals then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 + if null set_maps then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1 else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN EVERY' [rtac equalityI, rtac @{thm subrelI}, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}], @@ -190,7 +190,7 @@ REPEAT_DETERM o dtac Pair_eqD, REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, - CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals, + CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_maps, etac allE, etac impE, etac conjI, etac conjI, atac, REPEAT_DETERM o eresolve_tac [bexE, conjE], rtac @{thm relcompI}, rtac @{thm converseI}, diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Apr 24 17:47:22 2013 +0200 @@ -287,8 +287,8 @@ val nested_map_comp's = map map_comp'_of_bnf nested_bnfs; val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs; val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs; - val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs; - val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs; + val nested_set_map's = maps set_map'_of_bnf nested_bnfs; + val nesting_set_map's = maps set_map'_of_bnf nesting_bnfs; val live = live_of_bnf any_fp_bnf; @@ -548,7 +548,7 @@ fun mk_set_thm fp_set_thm ctr_def' cxIn = fold_thms lthy [ctr_def'] - (unfold_thms lthy (pre_set_defs @ nested_set_natural's @ nesting_set_natural's @ + (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @ (if lfp 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); @@ -814,8 +814,8 @@ 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_natural's pre_set_defss) + mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_map's + pre_set_defss) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation; in diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Wed Apr 24 17:47:22 2013 +0200 @@ -133,26 +133,26 @@ hyp_subst_tac 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_natural's pre_set_defs = +fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs = 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_natural's @ sum_prod_thms_set0)), + SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_map's @ sum_prod_thms_set0)), solve_prem_prem_tac]) (rev kks)) 1; -fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks = +fun mk_induct_discharge_prem_tac ctxt nn n set_map's pre_set_defs m k kks = let val r = length kks in EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac, REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN EVERY [REPEAT_DETERM_N r (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2), if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1, - mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs] + mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs] end; -fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_natural's pre_set_defss = +fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_map's pre_set_defss = let val n = Integer.sum ns in unfold_thms_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_as_projs_tac ctxt 1 THEN - EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's) - pre_set_defss mss (unflat mss (1 upto n)) kkss) + EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_map's) pre_set_defss + mss (unflat mss (1 upto n)) kkss) end; fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels = diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Apr 24 17:47:22 2013 +0200 @@ -227,7 +227,7 @@ val map_id's = 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_natural'ss = map set_natural'_of_bnf bnfs; + val set_map'ss = map set_map'_of_bnf bnfs; val srel_congs = map srel_cong_of_bnf bnfs; val srel_converses = map srel_converse_of_bnf bnfs; val srel_defs = map srel_def_of_bnf bnfs; @@ -762,7 +762,7 @@ singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal (K (mk_mor_hset_rec_tac m n cts j hset_rec_0s hset_rec_Sucs - morE_thms set_natural'ss coalg_set_thmss))) + morE_thms set_map'ss coalg_set_thmss))) |> Thm.close_derivation) ls goals ctss hset_rec_0ss' hset_rec_Sucss' end; @@ -866,7 +866,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_srel_tac m bis_def srel_O_Grs map_comp's map_cong0s set_natural'ss)) + (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_cong0s set_map'ss)) |> Thm.close_derivation end; @@ -1284,7 +1284,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_natural'ss) + (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_map'ss) |> Thm.close_derivation; val card_of_carT_thms = @@ -1323,14 +1323,13 @@ val goalss = map3 (fn carT => fn strT => fn sets => map3 (mk_goal carT strT) (drop m sets) kks ks) carTAs strTAs tree_setss; in - map6 (fn i => fn goals => - fn carT_def => fn strT_def => fn isNode_def => fn set_naturals => - map2 (fn goal => fn set_natural => + map6 (fn i => fn goals => fn carT_def => fn strT_def => fn isNode_def => fn set_maps => + map2 (fn goal => fn set_map => Goal.prove_sorry lthy [] [] goal - (mk_carT_set_tac n i carT_def strT_def isNode_def set_natural) + (mk_carT_set_tac n i carT_def strT_def isNode_def set_map) |> Thm.close_derivation) - goals (drop m set_naturals)) - ks goalss carT_defs strT_defs isNode_defs set_natural'ss + goals (drop m set_maps)) + ks goalss carT_defs strT_defs isNode_defs set_map'ss end; val carT_set_thmss' = transpose carT_set_thmss; @@ -1372,7 +1371,7 @@ (K (mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs set_incl_hsets set_hset_incl_hsetss coalg_set_thmss' carT_set_thmss' - coalgT_thm set_natural'ss))) + coalgT_thm set_map'ss))) |> Thm.close_derivation) ls goals ctss set_incl_hset_thmss' set_hset_incl_hset_thmsss'' end; @@ -1770,7 +1769,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_natural'ss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms) + set_map'ss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms) |> Thm.close_derivation; val timer = time (timer "Behavioral morphism"); @@ -1809,7 +1808,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_natural'ss coalgT_set_thmss)) + set_map'ss coalgT_set_thmss)) |> Thm.close_derivation; val mor_T_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As @@ -2517,7 +2516,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_natural'ss)) + (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_map'ss)) |> Thm.close_derivation) goals ctss hset_rec_0ss' hset_rec_Sucss'; in @@ -2585,7 +2584,7 @@ val thm = singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal - (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_natural'ss + (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_map'ss set_hset_thmss set_hset_hset_thmsss))) |> Thm.close_derivation in @@ -2621,7 +2620,7 @@ (Logic.mk_implies (wpull_prem, coalg)); in Goal.prove_sorry lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms - set_natural'ss pickWP_assms_tacs) + set_map'ss pickWP_assms_tacs) |> Thm.close_derivation end; @@ -2672,7 +2671,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_natural'ss + (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_map'ss map_wpull_thms pickWP_assms_tacs)) |> Thm.close_derivation) ls goals ctss hset_rec_0ss' hset_rec_Sucss'; @@ -2687,7 +2686,7 @@ val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms; val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; val set_nat_tacss = - map2 (map2 (K oo mk_set_natural_tac)) hset_defss (transpose col_natural_thmss); + map2 (map2 (K oo mk_set_map_tac)) hset_defss (transpose col_natural_thmss); val bd_co_tacs = replicate n (K (mk_bd_card_order_tac sbd_card_order)); val bd_cinf_tacs = replicate n (K (mk_bd_cinfinite_tac sbd_Cinfinite)); @@ -2866,7 +2865,7 @@ in map2 (fn goal => fn induct => Goal.prove_sorry lthy [] [] goal - (mk_coind_wit_tac induct dtor_unfold_thms (flat set_natural'ss) wit_thms) + (mk_coind_wit_tac induct dtor_unfold_thms (flat set_map'ss) wit_thms) |> Thm.close_derivation) goals dtor_hset_induct_thms |> map split_conj_thm @@ -2943,13 +2942,13 @@ in map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 => fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor => - fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss => + fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss => Goal.prove_sorry lthy [] [] goal (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets - dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss)) + dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss)) |> Thm.close_derivation) ks goals in_srels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss' - dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss + dtor_inject_thms dtor_ctor_thms set_map'ss dtor_set_incl_thmss dtor_set_set_incl_thmsss end; diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Apr 24 17:47:22 2013 +0200 @@ -110,7 +110,7 @@ val mk_set_incl_hin_tac: thm list -> tactic val mk_set_incl_hset_tac: thm -> thm -> tactic val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic - val mk_set_natural_tac: thm -> thm -> tactic + val mk_set_map_tac: thm -> thm -> tactic val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> tactic val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list -> @@ -230,38 +230,38 @@ EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI, REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1 -fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_naturalss coalg_setss = +fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_mapss coalg_setss = EVERY' [rtac (Drule.instantiate' [] cts nat_induct), REPEAT_DETERM o rtac allI, CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s, REPEAT_DETERM o rtac allI, CONJ_WRAP' - (fn (rec_Suc, (morE, ((passive_set_naturals, active_set_naturals), coalg_sets))) => + (fn (rec_Suc, (morE, ((passive_set_maps, active_set_maps), coalg_sets))) => EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym), if m = 0 then K all_tac else EVERY' [rtac @{thm Un_cong}, rtac box_equals, - rtac (nth passive_set_naturals (j - 1) RS sym), + rtac (nth passive_set_maps (j - 1) RS sym), rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac], CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong})) - (fn (i, (set_natural, coalg_set)) => + (fn (i, (set_map, coalg_set)) => EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})), - etac (morE RS sym RS arg_cong RS trans), atac, rtac set_natural, + etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map, rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}), ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i), REPEAT_DETERM o etac allE, atac, atac]) - (rev ((1 upto n) ~~ (active_set_naturals ~~ coalg_sets)))]) - (rec_Sucs ~~ (morEs ~~ (map (chop m) set_naturalss ~~ map (drop m) coalg_setss)))] 1; + (rev ((1 upto n) ~~ (active_set_maps ~~ coalg_sets)))]) + (rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1; fun mk_mor_hset_tac hset_def mor_hset_rec = EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec, atac, atac, rtac (hset_def RS sym)] 1 -fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_naturalss = +fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_mapss = let val n = length srel_O_Grs; - val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_naturalss ~~ srel_O_Grs); + val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ srel_O_Grs); - fun mk_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) = + fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), srel_O_Gr) = EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i), etac allE, etac allE, etac impE, atac, etac bexE, etac conjE, rtac (srel_O_Gr RS equalityD2 RS set_mp), @@ -275,12 +275,12 @@ etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm Id_onI}] else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, rtac trans_fun_cong_image_id_id_apply, atac]) - (1 upto (m + n) ~~ set_naturals), + (1 upto (m + n) ~~ set_maps), rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm, REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac]) @{thms fst_diag_id snd_diag_id})]; - fun mk_only_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) = + fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), srel_O_Gr) = EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI, etac allE, etac allE, etac impE, atac, dtac (srel_O_Gr RS equalityD1 RS set_mp), @@ -306,7 +306,7 @@ rtac @{thm Id_on_fst}, etac set_mp, atac] else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, rtac trans_fun_cong_image_id_id_apply, atac]) - (1 upto (m + n) ~~ set_naturals)]; + (1 upto (m + n) ~~ set_maps)]; in EVERY' [rtac (bis_def RS trans), rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms, @@ -401,7 +401,7 @@ rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis, etac @{thm relcompI}, atac] 1; -fun mk_coalgT_tac m defs strT_defs set_naturalss {context = ctxt, prems = _} = +fun mk_coalgT_tac m defs strT_defs set_mapss {context = ctxt, prems = _} = let val n = length strT_defs; val ks = 1 upto n; @@ -446,7 +446,7 @@ rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)]; in unfold_thms_tac ctxt defs THEN - CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1 + CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1 end; fun mk_card_of_carT_tac m isNode_defs sbd_sbd @@ -539,7 +539,7 @@ atac] 1 end; -fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}= +fun mk_carT_set_tac n i carT_def strT_def isNode_def set_map {context = ctxt, prems = _}= EVERY' [dtac (carT_def RS equalityD1 RS set_mp), REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], dtac Pair_eqD, @@ -550,20 +550,20 @@ rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans), fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt, - rtac set_natural, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI, + rtac set_map, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI, etac @{thm prefCl_Succ}, atac] 1; fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs - set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_naturalss = + set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_mapss = let - val set_naturals = map (fn xs => nth xs (j - 1)) set_naturalss; + val set_maps = map (fn xs => nth xs (j - 1)) set_mapss; val ks = 1 upto n; - fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_natural)))) = + fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_map)))) = CONJ_WRAP' (fn (i', (carT_def, isNode_def)) => rtac impI THEN' etac conjE THEN' (if i = i' then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset, rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans), - rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)), + rtac (Thm.permute_prems 0 1 (set_map RS box_equals)), rtac (trans OF [@{thm image_id} RS fun_cong, id_apply]), rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] else EVERY' [dtac (carT_def RS equalityD1 RS set_mp), @@ -585,7 +585,7 @@ EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}), REPEAT_DETERM o rtac allI, rtac impI, CONJ_WRAP' base_tac - (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_naturals)))), + (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_maps)))), REPEAT_DETERM o rtac allI, rtac impI, REPEAT_DETERM o eresolve_tac [allE, impE], etac @{thm ShiftI}, CONJ_WRAP' (fn i => dtac (mk_conjunctN n i) THEN' rtac (mk_sumEN n) THEN' @@ -840,14 +840,14 @@ fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's - prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_naturalss coalg_setss + prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_mapss coalg_setss map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} = let val n = length beh_defs; val ks = 1 upto n; fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd, - ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_naturals, + ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_maps, (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) = EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI, @@ -863,29 +863,29 @@ rtac conjI, rtac ballI, etac @{thm UN_E}, rtac conjI, if n = 1 then K all_tac else rtac (mk_sumEN n), - EVERY' (map6 (fn i => fn isNode_def => fn set_naturals => + EVERY' (map6 (fn i => fn isNode_def => fn set_maps => fn set_rv_Levs => fn set_Levs => fn set_image_Levs => EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst), rtac exI, rtac conjI, (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev' else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN' etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)), - EVERY' (map2 (fn set_natural => fn set_rv_Lev => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans), + EVERY' (map2 (fn set_map => fn set_rv_Lev => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans), rtac trans_fun_cong_image_id_id_apply, etac set_rv_Lev, TRY o atac, etac conjI, atac]) - (take m set_naturals) set_rv_Levs), - CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) => - EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI}, + (take m set_maps) set_rv_Levs), + CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) => + EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev, if n = 1 then rtac refl else atac, atac, rtac subsetI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev', etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]}, if n = 1 then rtac refl else atac]) - (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))]) - ks isNode_defs set_naturalss set_rv_Levss set_Levss set_image_Levss), - CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_naturals, + (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))]) + ks isNode_defs set_mapss set_rv_Levss set_Levss set_image_Levss), + CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_maps, (set_rv_Levs, (set_Levs, set_image_Levs)))))) => EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], @@ -894,13 +894,13 @@ (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev' else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN' etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)), - EVERY' (map2 (fn set_natural => fn set_rv_Lev => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans), + EVERY' (map2 (fn set_map => fn set_rv_Lev => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans), rtac trans_fun_cong_image_id_id_apply, etac set_rv_Lev, TRY o atac, etac conjI, atac]) - (take m set_naturals) set_rv_Levs), - CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) => - EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI}, + (take m set_maps) set_rv_Levs), + CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) => + EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev, if n = 1 then rtac refl else atac, atac, rtac subsetI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], @@ -909,8 +909,8 @@ atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev', etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]}, if n = 1 then rtac refl else atac]) - (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))]) - (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_naturalss ~~ + (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))]) + (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_mapss ~~ (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))), (**) rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI, @@ -921,12 +921,12 @@ CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), if n = 1 then rtac refl else rtac (mk_sum_casesN n i), - EVERY' (map2 (fn set_natural => fn coalg_set => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans), + EVERY' (map2 (fn set_map => fn coalg_set => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans), rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac]) - (take m set_naturals) (take m coalg_sets)), - CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) => - EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI}, + (take m set_maps) (take m coalg_sets)), + CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) => + EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev, rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil, atac, rtac subsetI, @@ -936,7 +936,7 @@ etac @{thm set_mp[OF equalityD1[OF arg_cong[OF trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]}, rtac rv_Nil]) - (drop m set_naturals ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))]; + (drop m set_maps ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))]; fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)), ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) = @@ -997,7 +997,7 @@ CONJ_WRAP' fbetw_tac (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~ ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~ - (set_naturalss ~~ (coalg_setss ~~ + (set_mapss ~~ (coalg_setss ~~ (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN' CONJ_WRAP' mor_tac (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~ @@ -1015,22 +1015,22 @@ equiv_LSBISs), rtac sym, rtac (o_apply RS trans), etac (sym RS arg_cong RS trans), rtac map_comp_id] 1; -fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_naturalss coalgT_setss = +fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_mapss coalgT_setss = EVERY' [stac coalg_def, - CONJ_WRAP' (fn ((set_naturals, coalgT_sets), (equiv_LSBIS, congruent_str_final)) => + CONJ_WRAP' (fn ((set_maps, coalgT_sets), (equiv_LSBIS, congruent_str_final)) => EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final, rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI, - EVERY' (map2 (fn set_natural => fn coalgT_set => - EVERY' [rtac conjI, rtac (set_natural RS ord_eq_le_trans), + EVERY' (map2 (fn set_map => fn coalgT_set => + EVERY' [rtac conjI, rtac (set_map RS ord_eq_le_trans), rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply, etac coalgT_set]) - (take m set_naturals) (take m coalgT_sets)), - CONJ_WRAP' (fn (equiv_LSBIS, (set_natural, coalgT_set)) => - EVERY' [rtac (set_natural RS ord_eq_le_trans), + (take m set_maps) (take m coalgT_sets)), + CONJ_WRAP' (fn (equiv_LSBIS, (set_map, coalgT_set)) => + EVERY' [rtac (set_map RS ord_eq_le_trans), rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set]) - (equiv_LSBISs ~~ drop m (set_naturals ~~ coalgT_sets))]) - ((set_naturalss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1; + (equiv_LSBISs ~~ drop m (set_maps ~~ coalgT_sets))]) + ((set_mapss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1; fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs = EVERY' [stac mor_def, rtac conjI, @@ -1225,7 +1225,7 @@ replicate n (@{thm o_id} RS fun_cong)))) maps map_comps map_cong0s)] 1; -fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_naturalss set_hsetss +fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss set_hset_hsetsss = let val n = length map_comp's; @@ -1233,7 +1233,7 @@ in EVERY' ([rtac rev_mp, coinduct_tac] @ - maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_naturals), set_hsets), + maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets), set_hset_hsetss) => [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI, rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0, @@ -1244,16 +1244,16 @@ [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE, REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets), REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym, - CONJ_WRAP' (fn (set_natural, set_hset_hsets) => + CONJ_WRAP' (fn (set_map, set_hset_hsets) => EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD}, - etac set_rev_mp, rtac ord_eq_le_trans, rtac set_natural, + etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE, REPEAT_DETERM o etac conjE, CONJ_WRAP' (fn set_hset_hset => EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets]) - (drop m set_naturals ~~ set_hset_hsetss)]) + (drop m set_maps ~~ set_hset_hsetss)]) (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~ - map_cong0s ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @ + map_cong0s ~~ set_mapss ~~ set_hsetss ~~ set_hset_hsetsss) @ [rtac impI, CONJ_WRAP' (fn k => EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI, @@ -1265,7 +1265,7 @@ unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN ALLGOALS (etac sym); -fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_naturalss +fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss {context = ctxt, prems = _} = let val n = length dtor_maps; @@ -1281,10 +1281,10 @@ CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong})) (fn i => EVERY' [rtac @{thm UN_cong[OF refl]}, REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)]) - (rec_Sucs ~~ (dtor_maps ~~ set_naturalss))] 1 + (rec_Sucs ~~ (dtor_maps ~~ set_mapss))] 1 end; -fun mk_set_natural_tac hset_def col_natural = +fun mk_set_map_tac hset_def col_natural = EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym, (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans), (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1; @@ -1370,10 +1370,10 @@ REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq] end; -fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs +fun mk_coalg_thePull_tac m coalg_def map_wpulls set_mapss pickWP_assms_tacs {context = ctxt, prems = _} = unfold_thms_tac ctxt [coalg_def] THEN - CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) => + CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) => EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}], hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), @@ -1383,11 +1383,11 @@ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV), - CONJ_WRAP' (fn set_natural => - EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_natural, + CONJ_WRAP' (fn set_map => + EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map, rtac trans_fun_cong_image_id_id_apply, atac]) - (drop m set_naturals)]) - (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1; + (drop m set_maps)]) + (map_wpulls ~~ (pickWP_assms_tacs ~~ set_mapss)) 1; fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs {context = ctxt, prems = _: thm list} = @@ -1422,7 +1422,7 @@ rtac refl]) (unfolds ~~ map_comps) 1; -fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_naturalss map_wpulls pickWP_assms_tacs +fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_mapss map_wpulls pickWP_assms_tacs {context = ctxt, prems = _} = let val n = length rec_0s; @@ -1433,7 +1433,7 @@ CONJ_WRAP' (fn thm => EVERY' [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s, REPEAT_DETERM o rtac allI, - CONJ_WRAP' (fn (rec_Suc, ((unfold, set_naturals), (map_wpull, pickWP_assms_tac))) => + CONJ_WRAP' (fn (rec_Suc, ((unfold, set_maps), (map_wpull, pickWP_assms_tac))) => EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}], hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), @@ -1442,16 +1442,16 @@ rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac ord_eq_le_trans, rtac rec_Suc, rtac @{thm Un_least}, - SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_naturals (j - 1), + SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_maps (j - 1), @{thm prod.cases}]), etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply, - CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) => + CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map) => EVERY' [rtac @{thm UN_least}, - SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_natural, @{thm prod.cases}]), + SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]), etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, etac set_mp, atac]) - (ks ~~ rev (drop m set_naturals))]) - (rec_Sucs ~~ ((unfolds ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1 + (ks ~~ rev (drop m set_maps))]) + (rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1 end; fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick @@ -1500,26 +1500,26 @@ FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor - set_naturals dtor_set_incls dtor_set_set_inclss = + set_maps dtor_set_incls dtor_set_set_inclss = let val m = length dtor_set_incls; val n = length dtor_set_set_inclss; - val (passive_set_naturals, active_set_naturals) = chop m set_naturals; + val (passive_set_maps, active_set_maps) = chop m set_maps; val in_Jsrel = nth in_Jsrels (i - 1); val if_tac = EVERY' [dtac (in_Jsrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - EVERY' (map2 (fn set_natural => fn set_incl => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural, + EVERY' (map2 (fn set_map => fn set_incl => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map, rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, etac (set_incl RS @{thm subset_trans})]) - passive_set_naturals dtor_set_incls), - CONJ_WRAP' (fn (in_Jsrel, (set_natural, dtor_set_set_incls)) => - EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI}, + passive_set_maps dtor_set_incls), + CONJ_WRAP' (fn (in_Jsrel, (set_map, dtor_set_set_incls)) => + EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls, rtac conjI, rtac refl, rtac refl]) - (in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)), + (in_Jsrels ~~ (active_set_maps ~~ dtor_set_set_inclss)), CONJ_WRAP' (fn conv => EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, @@ -1529,21 +1529,21 @@ val only_if_tac = EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - CONJ_WRAP' (fn (dtor_set, passive_set_natural) => + CONJ_WRAP' (fn (dtor_set, passive_set_map) => EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least}, - rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural, + rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map, rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) - (fn (active_set_natural, in_Jsrel) => EVERY' [rtac ord_eq_le_trans, + (fn (active_set_map, in_Jsrel) => EVERY' [rtac ord_eq_le_trans, rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]}, - rtac active_set_natural, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least}, + rtac active_set_map, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least}, dtac set_rev_mp, etac @{thm image_mono}, etac imageE, dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac]) - (rev (active_set_naturals ~~ in_Jsrels))]) - (dtor_sets ~~ passive_set_naturals), + (rev (active_set_maps ~~ in_Jsrels))]) + (dtor_sets ~~ passive_set_maps), rtac conjI, REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map, rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans, diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed Apr 24 17:47:22 2013 +0200 @@ -149,7 +149,7 @@ val map_id's = 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_natural'ss = map set_natural'_of_bnf bnfs; + val set_map'ss = map set_map'_of_bnf bnfs; val timer = time (timer "Extracted terms & thms"); @@ -388,7 +388,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_natural'ss map_comp_id_thms)) + (K (mk_mor_comp_tac mor_def set_map'ss map_comp_id_thms)) |> Thm.close_derivation end; @@ -407,7 +407,7 @@ (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_natural'ss morE_thms map_comp_id_thms map_cong0L_thms)) + set_map'ss morE_thms map_comp_id_thms map_cong0L_thms)) |> Thm.close_derivation end; @@ -512,7 +512,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_natural'ss alg_def alg_set_thms)) + (K (mk_copy_str_tac set_map'ss alg_def alg_set_thms)) |> Thm.close_derivation; val iso = HOLogic.mk_Trueprop @@ -520,7 +520,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_natural'ss alg_set_thms mor_def iso_alt_thm copy_str_thm)) + (K (mk_copy_alg_tac set_map'ss alg_set_thms mor_def iso_alt_thm copy_str_thm)) |> Thm.close_derivation; val ex = HOLogic.mk_Trueprop @@ -871,7 +871,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_natural'ss str_init_defs)) + alg_select_thm alg_set_thms set_map'ss str_init_defs)) |> Thm.close_derivation end; @@ -1318,7 +1318,7 @@ in (Goal.prove_sorry lthy [] [] (fold_rev Logic.all (phis @ Izs) goal) - (K (mk_ctor_induct_tac m set_natural'ss init_induct_thm morE_thms mor_Abs_thm + (K (mk_ctor_induct_tac m set_map'ss init_induct_thm morE_thms mor_Abs_thm Rep_inverses Abs_inverses Reps)) |> Thm.close_derivation, rev (Term.add_tfrees goal [])) @@ -1509,7 +1509,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_natural'ss) ls simp_goalss setss; + set_map'ss) ls simp_goalss setss; in ctor_setss end; @@ -1528,13 +1528,13 @@ map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) setss_by_bnf; val setss_by_range' = transpose setss_by_bnf'; - val set_natural_thmss = + val set_map_thmss = let - fun mk_set_natural f map z set set' = + fun mk_set_map f map z set set' = HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z)); fun mk_cphi f map z set set' = certify lthy - (Term.absfree (dest_Free z) (mk_set_natural f map z set set')); + (Term.absfree (dest_Free z) (mk_set_map f map z set set')); val csetss = map (map (certify lthy)) setss_by_range'; @@ -1547,10 +1547,10 @@ val goals = map3 (fn f => fn sets => fn sets' => HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map4 (mk_set_natural f) fs_maps Izs sets sets'))) + (map4 (mk_set_map 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_natural'ss ctor_map_thms; + fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_map'ss ctor_map_thms; val thms = map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i => singleton (Proof_Context.export names_lthy lthy) @@ -1693,7 +1693,7 @@ val map_comp_tacs = map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks; val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; - val set_nat_tacss = map (map (K o mk_set_natural_tac)) (transpose set_natural_thmss); + val set_nat_tacss = map (map (K o mk_set_map_tac)) (transpose set_map_thmss); val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders)); val bd_cinf_tacs = replicate n (K (rtac (bd_Cinfinite RS conjunct1) 1)); val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose set_bd_thmss); @@ -1780,13 +1780,13 @@ in map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 => fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor => - fn set_naturals => fn ctor_set_incls => fn ctor_set_set_inclss => + fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss => Goal.prove_sorry lthy [] [] goal (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets - ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss)) + ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss)) |> Thm.close_derivation) ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss' - ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss + ctor_inject_thms ctor_dtor_thms set_map'ss ctor_set_incl_thmss ctor_set_set_incl_thmsss end; diff -r 224b6eb2313a -r f19a4d0ab1bf src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Apr 24 17:03:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Apr 24 17:47:22 2013 +0200 @@ -71,7 +71,7 @@ {prems: 'a, context: Proof.context} -> tactic val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list -> thm list -> int -> {prems: 'a, context: Proof.context} -> tactic - val mk_set_natural_tac: thm -> tactic + val mk_set_map_tac: thm -> tactic val mk_set_tac: thm -> tactic val mk_wit_tac: int -> thm list -> thm list -> tactic val mk_wpull_tac: thm -> tactic @@ -119,39 +119,39 @@ CONJ_WRAP' (fn thm => (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_id's) 1; -fun mk_mor_comp_tac mor_def set_natural's map_comp_ids = +fun mk_mor_comp_tac mor_def set_map's map_comp_ids = let val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac]; - fun mor_tac (set_natural', map_comp_id) = + fun mor_tac (set_map', map_comp_id) = EVERY' [rtac ballI, stac o_apply, rtac trans, rtac trans, dtac @{thm 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_natural' 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_natural's THEN' - CONJ_WRAP' mor_tac (set_natural's ~~ map_comp_ids)) 1 + CONJ_WRAP' (K fbetw_tac) set_map's THEN' + CONJ_WRAP' mor_tac (set_map's ~~ map_comp_ids)) 1 end; -fun mk_mor_inv_tac alg_def mor_def set_natural's morEs map_comp_ids map_cong0Ls = +fun mk_mor_inv_tac alg_def mor_def set_map's morEs map_comp_ids map_cong0Ls = let val fbetw_tac = EVERY' [rtac ballI, etac set_mp, etac imageI]; - fun Collect_tac set_natural' = + 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_natural'; - fun mor_tac (set_natural', ((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 @{thm 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_natural', - rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_natural', + 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])]; @@ -161,8 +161,8 @@ dtac (alg_def RS iffD1) THEN' REPEAT o etac conjE THEN' rtac conjI THEN' - CONJ_WRAP' (K fbetw_tac) set_natural's THEN' - CONJ_WRAP' mor_tac (set_natural's ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1 + CONJ_WRAP' (K fbetw_tac) set_map's THEN' + CONJ_WRAP' mor_tac (set_map's ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1 end; fun mk_mor_str_tac ks mor_def = @@ -208,7 +208,7 @@ (rtac iffI THEN' if_tac THEN' only_if_tac) 1 end; -fun mk_copy_str_tac set_natural's alg_def alg_sets = +fun mk_copy_str_tac set_map's alg_def alg_sets = let val n = length alg_sets; val bij_betw_inv_tac = @@ -222,13 +222,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_natural's ~~ alg_sets); + (set_map's ~~ 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_natural's alg_sets mor_def iso_alt copy_str = +fun mk_copy_alg_tac set_map's 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; @@ -240,7 +240,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_natural's ~~ alg_sets); + (set_map's ~~ alg_sets); in (rtac (iso_alt RS @{thm ssubst[of _ _ "%x. x"]}) THEN' etac copy_str THEN' REPEAT_DETERM o atac THEN' @@ -389,24 +389,24 @@ 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_natural's str_init_defs = + alg_sets set_map's str_init_defs = let val n = length alg_sets; val fbetw_tac = CONJ_WRAP' (K (EVERY' [rtac ballI, etac @{thm 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_natural') = + 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_natural', 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_natural's)) 1 + stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_map's)) 1 end; fun mk_init_ex_mor_tac Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs @@ -532,21 +532,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 m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = +fun mk_ctor_induct_tac m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps = let - val n = length set_natural'ss; + val n = length set_map'ss; val ks = 1 upto n; - fun mk_IH_tac Rep_inv Abs_inv set_natural' = + 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_natural', etac imageE, + dtac set_rev_mp, rtac equalityD1, rtac set_map', etac imageE, hyp_subst_tac, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac]; - fun mk_closed_tac (k, (morE, set_natural's)) = + fun mk_closed_tac (k, (morE, set_map's)) = 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_natural's)), atac]; + EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_map's)), atac]; fun mk_induct_tac (Rep, Rep_inv) = EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RSN (2, bspec))]; @@ -554,7 +554,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_natural'ss))) 1 + DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_map'ss))) 1 end; fun mk_ctor_induct2_tac cTs cts ctor_induct weak_ctor_inducts {context = ctxt, prems = _} = @@ -599,19 +599,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_natural' set_natural's = +fun mk_ctor_set_tac set set_map' set_map's = let - val n = length set_natural's; + val n = length set_map's; 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 pointfreeE} RS trans), rtac @{thm Un_cong}, - rtac (trans OF [set_natural', 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 @{thm Un_cong}, - EVERY' (map mk_UN set_natural's)] 1 + EVERY' (map mk_UN set_map's)] 1 end; -fun mk_set_nat_tac m induct_tac set_natural'ss +fun mk_set_nat_tac m induct_tac set_map'ss ctor_maps csets ctor_sets i {context = ctxt, prems = _} = let val n = length ctor_maps; @@ -628,7 +628,7 @@ REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms 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_natural'ss)) 1 + (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_map'ss)) 1 end; fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i {context = ctxt, prems = _} = @@ -747,7 +747,7 @@ (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' ctor_maps')) 1 end; -fun mk_set_natural_tac set_nat = +fun mk_set_map_tac set_nat = EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1; fun mk_in_bd_tac sum_Card_order sucbd_Cnotzero incl card_of_min_alg = @@ -776,31 +776,31 @@ REPEAT_DETERM_N n o etac UnE]))))] 1); fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject - ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss = + ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss = let val m = length ctor_set_incls; val n = length ctor_set_set_inclss; - val (passive_set_naturals, active_set_naturals) = chop m set_naturals; + val (passive_set_maps, active_set_maps) = chop m set_maps; val in_Isrel = nth in_Isrels (i - 1); val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans; val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans; val if_tac = EVERY' [dtac (in_Isrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - EVERY' (map2 (fn set_natural => fn ctor_set_incl => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural, + EVERY' (map2 (fn set_map => fn ctor_set_incl => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map, rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor]) - passive_set_naturals ctor_set_incls), - CONJ_WRAP' (fn (in_Isrel, (set_natural, ctor_set_set_incls)) => - EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI}, + passive_set_maps ctor_set_incls), + CONJ_WRAP' (fn (in_Isrel, (set_map, ctor_set_set_incls)) => + EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor])) ctor_set_set_incls, rtac conjI, rtac refl, rtac refl]) - (in_Isrels ~~ (active_set_naturals ~~ ctor_set_set_inclss)), + (in_Isrels ~~ (active_set_maps ~~ ctor_set_set_inclss)), CONJ_WRAP' (fn conv => EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, @@ -811,20 +811,20 @@ val only_if_tac = EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - CONJ_WRAP' (fn (ctor_set, passive_set_natural) => + CONJ_WRAP' (fn (ctor_set, passive_set_map) => EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least}, rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]}, - rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply, atac, + rtac passive_set_map, rtac trans_fun_cong_image_id_id_apply, atac, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) - (fn (active_set_natural, in_Isrel) => EVERY' [rtac ord_eq_le_trans, - rtac @{thm UN_cong[OF _ refl]}, rtac active_set_natural, rtac @{thm UN_least}, + (fn (active_set_map, in_Isrel) => EVERY' [rtac ord_eq_le_trans, + rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map, rtac @{thm UN_least}, dtac set_rev_mp, etac @{thm image_mono}, etac imageE, dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac]) - (rev (active_set_naturals ~~ in_Isrels))]) - (ctor_sets ~~ passive_set_naturals), + (rev (active_set_maps ~~ in_Isrels))]) + (ctor_sets ~~ passive_set_maps), rtac conjI, REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2), rtac trans, rtac map_comp, rtac trans, rtac map_cong0,