# HG changeset patch # User traytel # Date 1377811378 -7200 # Node ID 87866222a7150544322b7251df424e267c3adecf # Parent e414487da3f8e03146d54713a624a6a966309ecc# Parent 84242070e267b1c1393dbb5d1da64eeea8a45a5e merged diff -r e414487da3f8 -r 87866222a715 NEWS --- a/NEWS Thu Aug 29 23:21:48 2013 +0200 +++ b/NEWS Thu Aug 29 23:22:58 2013 +0200 @@ -96,6 +96,9 @@ completed in backslash forms, e.g. \forall or \ that both produce the Isabelle symbol \ in its Unicode rendering. +* Standard jEdit completion via C+b uses action isabelle.complete +with fall-back on complete-word for non-Isabelle buffers. + * Improved support for Linux look-and-feel "GTK+", see also "Utilities / Global Options / Appearance". diff -r e414487da3f8 -r 87866222a715 src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Thu Aug 29 23:22:58 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 e414487da3f8 -r 87866222a715 src/HOL/BNF/Examples/TreeFI.thy --- a/src/HOL/BNF/Examples/TreeFI.thy Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Examples/TreeFI.thy Thu Aug 29 23:22:58 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 e414487da3f8 -r 87866222a715 src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Thu Aug 29 23:22:58 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 e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Thu Aug 29 23:22:58 2013 +0200 @@ -153,16 +153,16 @@ mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer) (map map_id0_of_bnf inners); - fun map_comp_tac _ = - mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer) - (map map_comp_of_bnf inners); + fun map_comp0_tac _ = + mk_comp_map_comp0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer) + (map map_comp0_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) + fun mk_single_set_map0_tac i _ = + mk_comp_set_map0_tac (map_comp0_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); + (map ((fn thms => nth thms i) o set_map0_of_bnf) inners); - val set_map_tacs = map mk_single_set_map_tac (0 upto ilive - 1); + val set_map0_tacs = map mk_single_set_map0_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); @@ -233,7 +233,7 @@ rtac thm 1 end; - val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; @@ -301,12 +301,12 @@ (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd; fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; - fun map_comp_tac {context = ctxt, prems = _} = - unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN + fun map_comp0_tac {context = ctxt, prems = _} = + unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN 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_map_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map_of_bnf bnf)); + val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_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 = @@ -339,7 +339,7 @@ rtac thm 1 end; - val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; @@ -391,17 +391,17 @@ val bd = mk_bd_of_bnf Ds As bnf; fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; - fun map_comp_tac {context = ctxt, prems = _} = - unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN + fun map_comp0_tac {context = ctxt, prems = _} = + unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN 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_map_tacs = + val set_map0_tacs = if Config.get lthy 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_map_of_bnf bnf); + map (fn thm => fn _ => rtac thm 1) (set_map0_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 = @@ -424,7 +424,7 @@ fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm; - val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); @@ -475,10 +475,10 @@ val bd = mk_bd_of_bnf Ds As bnf; fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1; - fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1; + fun map_comp0_tac _ = rtac (map_comp0_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_map_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf)); + val set_map0_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map0_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)); @@ -497,7 +497,7 @@ fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm; - val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac + val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); @@ -630,8 +630,8 @@ (rtac (unfold_all thm) THEN' SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1; - val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf)) - (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf)) + val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf)) + (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map0_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac (map_wpull_of_bnf bnf)) (mk_tac (rel_OO_Grp_of_bnf bnf)); diff -r e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_comp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 23:22:58 2013 +0200 @@ -11,12 +11,12 @@ val mk_comp_bd_card_order_tac: thm list -> thm -> tactic val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic - val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic + val mk_comp_map_comp0_tac: thm -> thm -> thm list -> tactic val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic val mk_comp_map_id0_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_map_tac: thm -> thm -> thm -> thm list -> tactic + val mk_comp_set_map0_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 @@ -62,26 +62,26 @@ EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @ map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1; -fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps = +fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s = EVERY' ([rtac ext, rtac sym, rtac trans_o_apply, - 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; + rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ + map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1; -fun mk_comp_set_map_tac Gmap_comp Gmap_cong0 Gset_map set_maps = +fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s = 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_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ - map (fn thm => rtac (thm RS fun_cong)) set_maps @ - [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, + map (fn thm => rtac (thm RS fun_cong)) set_map0s @ + [rtac (Gset_map0 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_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), + rtac (@{thm image_cong} OF [Gset_map0 RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), rtac @{thm trans[OF comp_eq_dest[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_maps) o EVERY' [rtac @{thm trans[OF image_insert]}, + [REPEAT_DETERM_N (length set_map0s) 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]}], diff -r e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 29 23:22:58 2013 +0200 @@ -50,13 +50,13 @@ val in_cong_of_bnf: bnf -> thm val in_mono_of_bnf: bnf -> thm val in_rel_of_bnf: bnf -> thm - val map_comp'_of_bnf: bnf -> thm + val map_comp0_of_bnf: bnf -> thm val map_comp_of_bnf: bnf -> thm val map_cong0_of_bnf: bnf -> thm val map_cong_of_bnf: bnf -> thm val map_def_of_bnf: bnf -> thm val map_id0_of_bnf: bnf -> thm - val map_id'_of_bnf: bnf -> thm + val map_id_of_bnf: bnf -> thm val map_transfer_of_bnf: bnf -> thm val map_wppull_of_bnf: bnf -> thm val map_wpull_of_bnf: bnf -> thm @@ -72,7 +72,7 @@ val rel_flip_of_bnf: bnf -> thm val set_bd_of_bnf: bnf -> thm list val set_defs_of_bnf: bnf -> thm list - val set_map'_of_bnf: bnf -> thm list + val set_map0_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 @@ -114,9 +114,9 @@ type axioms = { map_id0: thm, - map_comp: thm, + map_comp0: thm, map_cong0: thm, - set_map: thm list, + set_map0: thm list, bd_card_order: thm, bd_cinfinite: thm, set_bd: thm list, @@ -124,8 +124,8 @@ rel_OO_Grp: thm }; -fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) = - {map_id0 = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o, +fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), wpull), rel) = + {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, bd_card_order = c_o, bd_cinfinite = cinf, set_bd = set_bd, map_wpull = wpull, rel_OO_Grp = rel}; fun dest_cons [] = raise List.Empty @@ -144,20 +144,20 @@ ||> the_single |> mk_axioms'; -fun zip_axioms mid mcomp mcong snat bdco bdinf sbd wpull rel = - [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [wpull, rel]; +fun zip_axioms mid mcomp mcong smap bdco bdinf sbd wpull rel = + [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [wpull, rel]; -fun dest_axioms {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, +fun dest_axioms {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd, map_wpull, rel_OO_Grp} = - zip_axioms map_id0 map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull + zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd map_wpull rel_OO_Grp; -fun map_axioms f {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, +fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd, map_wpull, rel_OO_Grp} = {map_id0 = f map_id0, - map_comp = f map_comp, + map_comp0 = f map_comp0, map_cong0 = f map_cong0, - set_map = map f set_map, + set_map0 = map f set_map0, bd_card_order = f bd_card_order, bd_cinfinite = f bd_cinfinite, set_bd = map f set_bd, @@ -188,14 +188,14 @@ in_cong: thm lazy, in_mono: thm lazy, in_rel: thm lazy, - map_comp': thm lazy, + map_comp: thm lazy, map_cong: thm lazy, - map_id': thm lazy, + map_id: thm lazy, map_transfer: thm lazy, 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, @@ -215,14 +215,14 @@ in_cong = in_cong, in_mono = in_mono, in_rel = in_rel, - map_comp' = map_comp', + map_comp = map_comp, map_cong = map_cong, - map_id' = map_id', + map_id = map_id, map_transfer = map_transfer, 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, @@ -239,14 +239,14 @@ in_cong, in_mono, in_rel, - map_comp', + map_comp, map_cong, - map_id', + map_id, map_transfer, map_wppull, rel_eq, rel_flip, - set_map', + set_map, rel_cong, rel_mono, rel_mono_strong, @@ -261,14 +261,14 @@ in_cong = Lazy.map f in_cong, in_mono = Lazy.map f in_mono, in_rel = Lazy.map f in_rel, - map_comp' = Lazy.map f map_comp', + map_comp = Lazy.map f map_comp, map_cong = Lazy.map f map_cong, - map_id' = Lazy.map f map_id', + map_id = Lazy.map f map_id, map_transfer = Lazy.map f map_transfer, 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, @@ -381,9 +381,9 @@ val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf; val map_def_of_bnf = #map_def o #defs o rep_bnf; val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf; -val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf; -val map_comp_of_bnf = #map_comp o #axioms o rep_bnf; -val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf; +val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf; +val map_comp0_of_bnf = #map_comp0 o #axioms o rep_bnf; +val map_comp_of_bnf = Lazy.force o #map_comp o #facts o rep_bnf; val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf; val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf; val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf; @@ -394,8 +394,8 @@ val rel_flip_of_bnf = Lazy.force o #rel_flip 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_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 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 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; @@ -509,17 +509,17 @@ val in_monoN = "in_mono"; val in_relN = "in_rel"; val map_id0N = "map_id0"; -val map_id'N = "map_id'"; +val map_idN = "map_id"; +val map_comp0N = "map_comp0"; val map_compN = "map_comp"; -val map_comp'N = "map_comp'"; val map_cong0N = "map_cong0"; val map_congN = "map_cong"; val map_transferN = "map_transfer"; val map_wpullN = "map_wpull"; val rel_eqN = "rel_eq"; val rel_flipN = "rel_flip"; +val set_map0N = "set_map0"; val set_mapN = "set_map"; -val set_map'N = "set_map'"; val set_bdN = "set_bd"; val rel_GrpN = "rel_Grp"; val rel_conversepN = "rel_conversep"; @@ -558,12 +558,12 @@ (in_bdN, [Lazy.force (#in_bd facts)]), (in_monoN, [Lazy.force (#in_mono facts)]), (in_relN, [Lazy.force (#in_rel facts)]), - (map_compN, [#map_comp axioms]), + (map_comp0N, [#map_comp0 axioms]), (map_id0N, [#map_id0 axioms]), (map_transferN, [Lazy.force (#map_transfer facts)]), (map_wpullN, [#map_wpull axioms]), (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), - (set_mapN, #set_map axioms), + (set_map0N, #set_map0 axioms), (set_bdN, #set_bd axioms)] @ (witNs ~~ wit_thmss_of_bnf bnf) |> map (fn (thmN, thms) => @@ -577,13 +577,13 @@ #> (if fact_policy <> Dont_Note then let val notes = - [(map_comp'N, [Lazy.force (#map_comp' facts)], []), + [(map_compN, [Lazy.force (#map_comp facts)], []), (map_cong0N, [#map_cong0 axioms], []), (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs), - (map_id'N, [Lazy.force (#map_id' facts)], []), + (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)], []), @@ -850,7 +850,7 @@ mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA') end; - val map_comp_goal = + val map_comp0_goal = let val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs); val comp_bnf_map_app = HOLogic.mk_comp @@ -873,7 +873,7 @@ fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq)) end; - val set_maps_goal = + val set_map0s_goal = let fun mk_goal setA setB f = let @@ -922,7 +922,7 @@ val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp)); - val goals = zip_axioms map_id0_goal map_comp_goal map_cong0_goal set_maps_goal + val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal; fun mk_wit_goals (I, wit) = @@ -965,7 +965,7 @@ (*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_map_tac (#set_map axioms))) + Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map0 axioms))) |> Thm.close_derivation end; @@ -1000,8 +1000,8 @@ val in_cong = Lazy.lazy mk_in_cong; - val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id0 axioms)); - val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp axioms)); + val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms)); + val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms)); fun mk_map_cong () = let @@ -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_map axioms); + val set_map = map (fn thm => Lazy.lazy (fn () => mk_set_map thm)) (#set_map0 axioms); fun mk_in_bd () = let @@ -1049,8 +1049,8 @@ in 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) + (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 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; @@ -1102,8 +1102,8 @@ val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs)); 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')) + (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)) |> 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; @@ -1335,12 +1335,12 @@ val _ = Outer_Syntax.improper_command @{command_spec "print_bnfs"} - "print all BNFs (bounded natural functors)" + "print all bounded natural functors" (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of))); val _ = Outer_Syntax.local_theory_to_proof @{command_spec "bnf"} - "register a type as a BNF (bounded natural functor)" + "register a type as a bounded natural functor" ((parse_opt_binding_colon -- Parse.term -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term) diff -r e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 23:22:58 2013 +0200 @@ -9,12 +9,12 @@ signature BNF_DEF_TACTICS = sig val mk_collect_set_map_tac: thm list -> tactic - val mk_map_id': thm -> thm - val mk_map_comp': thm -> thm + val mk_map_id: thm -> thm + val mk_map_comp: thm -> thm 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 @@ -45,12 +45,12 @@ val ord_le_eq_trans = @{thm ord_le_eq_trans}; val conversep_shift = @{thm conversep_le_swap} RS iffD1; -fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply}; -fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp]; +fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply}; +fun mk_map_comp comp = @{thm o_eq_dest_lhs} OF [mk_sym comp]; 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_map = set_map 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 @@ -59,15 +59,15 @@ ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN (etac subset_trans THEN' atac) 1; -fun mk_collect_set_map_tac set_maps = +fun mk_collect_set_map_tac set_map0s = (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN' - EVERY' (map (fn set_map => + EVERY' (map (fn set_map0 => rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' - rtac set_map) set_maps) THEN' + rtac set_map0) set_map0s) THEN' rtac @{thm image_empty}) 1; -fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps = - if null set_maps then +fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_map0s = + if null set_map0s then EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 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, @@ -75,45 +75,45 @@ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac]) - 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_maps) o EVERY' [rtac (o_apply RS trans), + set_map0s, + CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp0 RS trans), rtac (map_comp0 RS trans), + rtac (map_comp0 RS trans RS sym), rtac map_cong0, + REPEAT_DETERM_N (length set_map0s) 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_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id' map_comp set_maps +fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp0 set_map0s {context = ctxt, prems = _} = let - val n = length set_maps; + val n = length set_map0s; val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans); in - if null set_maps then + if null set_map0s then unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN rtac @{thm Grp_UNIV_idI[OF refl]} 1 else EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], - hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0, + hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac], rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac]) - set_maps, + set_map0s, rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE], hyp_subst_tac ctxt, rtac @{thm relcomppI}, rtac @{thm conversepI}, EVERY' (map2 (fn convol => fn map_id0 => - EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]), + EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp0 RS sym, map_id0]), REPEAT_DETERM_N n o rtac (convol RS fun_cong), REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI}, rtac @{thm convol_mem_GrpI}, etac set_mp, atac]) - set_maps]) - @{thms fst_convol snd_convol} [map_id', refl])] 1 + set_map0s]) + @{thms fst_convol snd_convol} [map_id, refl])] 1 end; fun mk_rel_eq_tac n rel_Grp rel_cong map_id0 = @@ -135,15 +135,15 @@ rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1 end; -fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps +fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp0 set_map0s {context = ctxt, prems = _} = let - val n = length set_maps; + val n = length set_map0s; val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN' rtac (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans)); in - if null set_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1 + if null set_map0s then rtac (rel_eq RS @{thm leq_conversepI}) 1 else EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I}, REPEAT_DETERM o @@ -151,9 +151,9 @@ hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm, - rtac (map_comp RS sym), rtac CollectI, + rtac (map_comp0 RS sym), rtac CollectI, CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), - etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 + etac @{thm flip_pred}]) set_map0s]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1 end; fun mk_rel_conversep_tac le_conversep rel_mono = @@ -161,52 +161,52 @@ rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono, REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1; -fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp set_maps +fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp0 set_map0s {context = ctxt, prems = _} = let - val n = length set_maps; + val n = length set_map0s; fun in_tac nthO_in = rtac CollectI THEN' CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans), - rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps; + rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_map0s; val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans) THEN' rtac (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN (2, trans)); in - if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1 + if null set_map0s then rtac (rel_eq RS @{thm eq_OOI}) 1 else EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}], hyp_subst_tac ctxt, rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI}, - rtac trans, rtac map_comp, rtac sym, rtac map_cong0, + rtac trans, rtac map_comp0, rtac sym, rtac map_cong0, REPEAT_DETERM_N n o rtac @{thm fst_fstOp}, in_tac @{thm fstOp_in}, - rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0, + rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst, rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE, etac set_mp, atac], in_tac @{thm fstOp_in}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI}, - rtac trans, rtac map_comp, rtac map_cong0, + rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N n o rtac o_apply, in_tac @{thm sndOp_in}, - rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0, + rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac sym, rtac map_cong0, REPEAT_DETERM_N n o rtac @{thm snd_sndOp}, in_tac @{thm sndOp_in}, rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}], hyp_subst_tac ctxt, rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull, - CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_maps, + CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_map0s, etac allE, etac impE, etac conjI, etac conjI, etac sym, REPEAT_DETERM o eresolve_tac [bexE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI}, EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans, rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm, - rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1 + rtac (map_comp0 RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1 end; fun mk_in_rel_tac rel_OO_Gr {context = ctxt, prems = _} = @@ -216,20 +216,20 @@ REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI}, etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1; -fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} = - if null set_maps then atac 1 +fun mk_rel_mono_strong_tac in_rel set_map0s {context = ctxt, prems = _} = + if null set_map0s then atac 1 else unfold_tac [in_rel] ctxt THEN REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN hyp_subst_tac ctxt 1 THEN - unfold_tac set_maps ctxt THEN + unfold_tac set_map0s ctxt THEN EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]}, - CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1; + 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' + 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,11 +290,11 @@ 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}, - map_comp' RS sym, map_id']) RSN (2, trans))), + map_comp RS sym, map_id]) RSN (2, trans))), REPEAT_DETERM_N (2 * live) o atac, REPEAT_DETERM_N live o rtac (@{thm prod.cases} RS trans), rtac refl, @@ -302,10 +302,10 @@ 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 + map_comp RS sym, map_id])] 1 end; end; diff -r e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 29 23:22:58 2013 +0200 @@ -602,9 +602,9 @@ val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_set_defss = map set_defs_of_bnf pre_bnfs; - val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; - val nested_map_ids'' = 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 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_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; @@ -726,7 +726,7 @@ val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss; val tacss = - map2 (map o mk_iter_tac pre_map_defs (nested_map_ids'' @ nesting_map_ids'') iter_defs) + map2 (map o mk_iter_tac pre_map_defs (nested_map_id's @ nesting_map_id's) iter_defs) ctor_iter_thms ctr_defss; fun prove goal tac = @@ -763,7 +763,7 @@ val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_rel_defs = map rel_def_of_bnf pre_bnfs; - val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; + val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs; val fp_b_names = map base_name_of_typ fpTs; @@ -919,10 +919,10 @@ val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; val unfold_tacss = - map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'') + map3 (map oo mk_coiter_tac unfold_defs nesting_map_id's) (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss; val corec_tacss = - map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'') + map3 (map oo mk_coiter_tac corec_defs nesting_map_id's) (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss; fun prove goal tac = @@ -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 e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Aug 29 23:22:58 2013 +0200 @@ -94,17 +94,17 @@ @{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv split_conv unit_case_Unity} @ sum_prod_thms_map; -fun mk_iter_tac pre_map_defs map_ids'' iter_defs ctor_iter ctr_def ctxt = - unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_ids'' @ +fun mk_iter_tac pre_map_defs map_id's iter_defs ctor_iter ctr_def ctxt = + unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_id's @ iter_unfold_thms) THEN HEADGOAL (rtac refl); val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map; -fun mk_coiter_tac coiter_defs map_ids'' ctor_dtor_coiter pre_map_def ctr_def ctxt = +fun mk_coiter_tac coiter_defs map_id's ctor_dtor_coiter pre_map_def ctr_def ctxt = unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN' asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE - (unfold_thms_tac ctxt (pre_map_def :: map_ids'' @ coiter_unfold_thms) THEN + (unfold_thms_tac ctxt (pre_map_def :: map_id's @ coiter_unfold_thms) THEN HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))); fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt = @@ -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 e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 29 23:22:58 2013 +0200 @@ -219,15 +219,15 @@ val bd_Cinfinites = map bd_Cinfinite_of_bnf bnfs; val bd_Cinfinite = hd bd_Cinfinites; val in_monos = map in_mono_of_bnf bnfs; + val map_comp0s = map map_comp0_of_bnf bnfs; + val sym_map_comps = map mk_sym map_comp0s; val map_comps = map map_comp_of_bnf bnfs; - val sym_map_comps = map mk_sym map_comps; - val map_comp's = map map_comp'_of_bnf bnfs; val map_cong0s = map map_cong0_of_bnf bnfs; val map_id0s = map map_id0_of_bnf bnfs; - val map_id's = map map_id'_of_bnf bnfs; + 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; @@ -242,7 +242,7 @@ (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) = map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*) - fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp = + fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 = let val lhs = Term.list_comb (mapBsCs, all_gs) $ (Term.list_comb (mapAsBs, passive_ids @ fs) $ x); @@ -251,15 +251,15 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs))) - (K (mk_map_comp_id_tac map_comp)) + (K (mk_map_comp_id_tac map_comp0)) |> Thm.close_derivation end; - val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's; + val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps; (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==> map id ... id f(m+1) ... f(m+n) x = x*) - fun mk_map_cong0L x mapAsAs sets map_cong0 map_id' = + fun mk_map_cong0L x mapAsAs sets map_cong0 map_id = let fun mk_prem set f z z' = HOLogic.mk_Trueprop @@ -269,11 +269,11 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal))) - (K (mk_map_cong0L_tac m map_cong0 map_id')) + (K (mk_map_cong0L_tac m map_cong0 map_id)) |> Thm.close_derivation end; - val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's; + val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids; val in_mono'_thms = map (fn thm => (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos; @@ -443,7 +443,7 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl))) - (K (mk_mor_incl_tac mor_def map_id's)) + (K (mk_mor_incl_tac mor_def map_ids)) |> Thm.close_derivation end; @@ -814,7 +814,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_comp's 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; @@ -1210,7 +1210,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 @@ -2098,7 +2098,7 @@ dtor_set_induct_thms, dtor_Jrel_thms, lthy) = if m = 0 then (timer, replicate n DEADID_bnf, - map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_id's), + map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids), replicate n [], [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; @@ -2184,16 +2184,16 @@ val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's; val cTs = map (SOME o certifyT lthy) FTs'; val maps = - map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong0 => + map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 => Goal.prove_sorry lthy [] [] goal - (K (mk_map_tac m n cT unfold map_comp' map_cong0)) + (K (mk_map_tac m n cT unfold map_comp map_cong0)) |> Thm.close_derivation) - goals cTs dtor_unfold_thms map_comp's map_cong0s; + goals cTs dtor_unfold_thms map_comps map_cong0s; in map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps end; - val map_comp_thms = + val map_comp0_thms = let val goal = fold_rev Logic.all (fs @ gs) (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj @@ -2202,7 +2202,7 @@ fs_maps gs_maps fgs_maps))) in split_conj_thm (Goal.prove_sorry lthy [] [] goal - (K (mk_map_comp_tac m n map_thms map_comps map_cong0s dtor_unfold_unique_thm)) + (K (mk_map_comp0_tac m n map_thms map_comp0s map_cong0s dtor_unfold_unique_thm)) |> Thm.close_derivation) end; @@ -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_comp's 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; @@ -2420,11 +2420,11 @@ (Logic.mk_implies (wpull_prem, mor_pick)); in (Goal.prove_sorry lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms - map_comp's pickWP_assms_tacs) |> Thm.close_derivation, + map_comps pickWP_assms_tacs) |> Thm.close_derivation, Goal.prove_sorry lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms - map_comp's pickWP_assms_tacs) |> Thm.close_derivation, + map_comps pickWP_assms_tacs) |> Thm.close_derivation, Goal.prove_sorry lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms - map_comp's) |> Thm.close_derivation) + map_comps) |> Thm.close_derivation) end; val pick_col_thmss = @@ -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'; @@ -2459,10 +2459,10 @@ val map_id0_tacs = map2 (K oo mk_map_id0_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms; - val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms; + val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp0_thms; val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms; val set_nat_tacss = - map2 (map2 (K oo mk_set_map_tac)) hset_defss (transpose col_natural_thmss); + map2 (map2 (K oo mk_set_map0_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)); @@ -2476,7 +2476,7 @@ val rel_OO_Grp_tacs = replicate n (K (rtac refl 1)); - val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss + val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs; val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) = @@ -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 @@ -2699,15 +2699,15 @@ (mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz'))); val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis; in - map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 => + map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 => fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor => - fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss => + fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss => Goal.prove_sorry lthy [] [] goal - (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets - dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss)) + (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets + dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss)) |> Thm.close_derivation) - ks goals in_rels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss' - dtor_inject_thms dtor_ctor_thms set_map'ss dtor_set_incl_thmss + ks goals in_rels map_comps map_cong0s folded_dtor_map_thms folded_dtor_set_thmss' + dtor_inject_thms dtor_ctor_thms set_mapss dtor_set_incl_thmss dtor_set_set_incl_thmsss end; @@ -2801,8 +2801,8 @@ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (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_comp's - map_cong0s map_arg_cong_thms set_map'ss dtor_unfold_thms folded_dtor_map_thms; + val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comps + 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 e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 29 23:22:58 2013 +0200 @@ -52,7 +52,7 @@ val mk_incl_lsbis_tac: int -> int -> thm -> tactic val mk_length_Lev'_tac: thm -> tactic val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic - val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic + val mk_map_comp0_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list -> thm list list -> thm list list list -> tactic val mk_map_id0_tac: thm list -> thm -> thm -> tactic @@ -107,7 +107,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_map_tac: thm -> thm -> tactic + val mk_set_map0_tac: thm -> thm -> tactic val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> tactic val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic @@ -160,12 +160,12 @@ etac bspec THEN' atac) 1; -fun mk_mor_incl_tac mor_def map_id's = +fun mk_mor_incl_tac mor_def map_ids = (stac mor_def THEN' rtac conjI THEN' - CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_id's THEN' + CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN' CONJ_WRAP' (fn thm => - (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_id's) 1; + (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_ids) 1; fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids = let @@ -234,41 +234,41 @@ 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_mapss coalg_setss = +fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_map0ss 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_maps, active_set_maps), coalg_sets))) => + (fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), 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 Un_cong, rtac box_equals, - rtac (nth passive_set_maps (j - 1) RS sym), + rtac (nth passive_set_map0s (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 Un_cong)) - (fn (i, (set_map, coalg_set)) => + (fn (i, (set_map0, 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_map, + etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map0, 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_maps ~~ coalg_sets)))]) - (rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1; + (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))]) + (rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1; -fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comps map_cong0s set_mapss = +fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_map0ss = let val n = length rel_OO_Grps; - val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps); + val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ rel_OO_Grps); - fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) = + fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) = EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i), etac allE, etac allE, etac impE, atac, etac bexE, etac conjE, rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}), rtac @{thm relcomppI}, rtac @{thm conversepI}, EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, - rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm, + rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N m o rtac thm, REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, CONJ_WRAP' (fn (i, thm) => @@ -278,20 +278,20 @@ etac @{thm Collect_split_in_relI[OF Id_onI]}] else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}]) - (1 upto (m + n) ~~ set_maps)]) + (1 upto (m + n) ~~ set_map0s)]) @{thms fst_diag_id snd_diag_id})]; - fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) = + fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) = EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI, etac allE, etac allE, etac impE, atac, dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}), REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @ @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}), hyp_subst_tac ctxt, - rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0, + rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), - atac, rtac trans, rtac map_comp, rtac trans, rtac map_cong0, + atac, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), rtac trans, rtac map_cong0, @@ -304,7 +304,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_maps)]; + (1 upto (m + n) ~~ set_map0s)]; in EVERY' [rtac (bis_def RS trans), rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms, @@ -399,7 +399,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_mapss {context = ctxt, prems = _} = +fun mk_coalgT_tac m defs strT_defs set_map0ss {context = ctxt, prems = _} = let val n = length strT_defs; val ks = 1 upto n; @@ -444,7 +444,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_mapss ~~ strT_defs)) 1 + CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_map0ss ~~ strT_defs)) 1 end; fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss = @@ -685,14 +685,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_mapss coalg_setss + prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_map0ss 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_maps, + ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_map0s, (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, @@ -708,29 +708,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_maps => + EVERY' (map6 (fn i => fn isNode_def => fn set_map0s => 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_map => fn set_rv_Lev => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans), + EVERY' (map2 (fn set_map0 => fn set_rv_Lev => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans), rtac trans_fun_cong_image_id_id_apply, etac set_rv_Lev, TRY o atac, etac conjI, atac]) - (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}, + (take m set_map0s) set_rv_Levs), + CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => + EVERY' [rtac (set_map0 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 ctxt, 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_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, + (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))]) + ks isNode_defs set_map0ss set_rv_Levss set_Levss set_image_Levss), + CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s, (set_rv_Levs, (set_Levs, set_image_Levs)))))) => EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], @@ -739,13 +739,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_map => fn set_rv_Lev => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans), + EVERY' (map2 (fn set_map0 => fn set_rv_Lev => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans), rtac trans_fun_cong_image_id_id_apply, etac set_rv_Lev, TRY o atac, etac conjI, atac]) - (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}, + (take m set_map0s) set_rv_Levs), + CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => + EVERY' [rtac (set_map0 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}], @@ -754,8 +754,8 @@ atac, dtac length_Lev, hyp_subst_tac ctxt, 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_maps ~~ (set_Levs ~~ set_image_Levs))]) - (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_mapss ~~ + (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))]) + (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~ (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))), (**) rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI, @@ -766,12 +766,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_map => fn coalg_set => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans), + EVERY' (map2 (fn set_map0 => fn coalg_set => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans), rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac]) - (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}, + (take m set_map0s) (take m coalg_sets)), + CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => + EVERY' [rtac (set_map0 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, @@ -781,7 +781,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_maps ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))]; + (drop m set_map0s ~~ (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)))))) = @@ -842,7 +842,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_mapss ~~ (coalg_setss ~~ + (set_map0ss ~~ (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)) ~~ @@ -860,22 +860,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_mapss coalgT_setss = +fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss = EVERY' [stac coalg_def, - CONJ_WRAP' (fn ((set_maps, coalgT_sets), (equiv_LSBIS, congruent_str_final)) => + CONJ_WRAP' (fn ((set_map0s, 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_map => fn coalgT_set => - EVERY' [rtac conjI, rtac (set_map RS ord_eq_le_trans), + EVERY' (map2 (fn set_map0 => fn coalgT_set => + EVERY' [rtac conjI, rtac (set_map0 RS ord_eq_le_trans), rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply, etac coalgT_set]) - (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), + (take m set_map0s) (take m coalgT_sets)), + CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) => + EVERY' [rtac (set_map0 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_maps ~~ coalgT_sets))]) - ((set_mapss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1; + (equiv_LSBISs ~~ drop m (set_map0s ~~ coalgT_sets))]) + ((set_map0ss ~~ 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, @@ -1008,9 +1008,9 @@ rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1 end; -fun mk_map_tac m n cT unfold map_comp' map_cong0 = +fun mk_map_tac m n cT unfold map_comp map_cong0 = EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym), - rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong0, + rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0, REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1; @@ -1034,50 +1034,50 @@ EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps), rtac unfold_dtor] 1; -fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique = +fun mk_map_comp0_tac m n maps map_comp0s map_cong0s unfold_unique = EVERY' [rtac unfold_unique, - EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong0 => + EVERY' (map3 (fn map_thm => fn map_comp0 => fn map_cong0 => EVERY' (map rtac ([@{thm o_assoc} RS trans, - @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans, + @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans, @{thm o_assoc} RS trans RS sym, @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans, @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans, - @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans, + @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans, ext, o_apply RS trans, o_apply RS trans RS sym, map_cong0] @ replicate m (@{thm id_o} RS fun_cong) @ replicate n (@{thm o_id} RS fun_cong)))) - maps map_comps map_cong0s)] 1; + maps map_comp0s map_cong0s)] 1; -fun mk_mcong_tac ctxt m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss +fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_hsetss set_hset_hsetsss = let - val n = length map_comp's; + val n = length map_comps; val ks = 1 upto n; in EVERY' ([rtac rev_mp, coinduct_tac] @ - maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets), + maps (fn (((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_hsets), set_hset_hsetss) => [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI, - rtac conjI, rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0, + rtac conjI, rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0, REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply), REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym, - rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0, + rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0, EVERY' (maps (fn set_hset => [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_map, set_hset_hsets) => + CONJ_WRAP' (fn (set_map0, 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_map, + etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map0, 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_maps ~~ set_hset_hsetss)]) - (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~ - map_cong0s ~~ set_mapss ~~ set_hsetss ~~ set_hset_hsetsss) @ + (drop m set_map0s ~~ set_hset_hsetss)]) + (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~ + map_cong0s ~~ set_map0ss ~~ 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, @@ -1089,7 +1089,7 @@ unfold_thms_tac ctxt (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_mapss +fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_map0ss {context = ctxt, prems = _} = let val n = length dtor_maps; @@ -1105,10 +1105,10 @@ CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 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_mapss))] 1 + (rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1 end; -fun mk_set_map_tac hset_def col_natural = +fun mk_set_map0_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; @@ -1158,10 +1158,10 @@ REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq] end; -fun mk_coalg_thePull_tac m coalg_def map_wpulls set_mapss pickWP_assms_tacs +fun mk_coalg_thePull_tac m coalg_def map_wpulls set_map0ss pickWP_assms_tacs {context = ctxt, prems = _} = unfold_thms_tac ctxt [coalg_def] THEN - CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) => + CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_map0s)) => EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}], hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), @@ -1171,46 +1171,46 @@ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV), - CONJ_WRAP' (fn set_map => - EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map, + CONJ_WRAP' (fn set_map0 => + EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map0, rtac trans_fun_cong_image_id_id_apply, atac]) - (drop m set_maps)]) - (map_wpulls ~~ (pickWP_assms_tacs ~~ set_mapss)) 1; + (drop m set_map0s)]) + (map_wpulls ~~ (pickWP_assms_tacs ~~ set_map0ss)) 1; -fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs +fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comp0s pickWP_assms_tacs {context = ctxt, prems = _: thm list} = let - val n = length map_comps; + val n = length map_comp0s; in unfold_thms_tac ctxt [mor_def] THEN EVERY' [rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n), - CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) => + CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp0)) => EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE], hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), - rtac (map_comp RS trans), + rtac (map_comp0 RS trans), SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})), rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac, pickWP_assms_tac]) - (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1 + (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comp0s))] 1 end; val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)}; val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)}; -fun mk_mor_thePull_pick_tac mor_def unfolds map_comps {context = ctxt, prems = _} = +fun mk_mor_thePull_pick_tac mor_def unfolds map_comp0s {context = ctxt, prems = _} = unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN - CONJ_WRAP' (fn (unfold, map_comp) => + CONJ_WRAP' (fn (unfold, map_comp0) => EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE], hyp_subst_tac ctxt, - SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})), + SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp0 :: @{thms comp_def id_def})), rtac refl]) - (unfolds ~~ map_comps) 1; + (unfolds ~~ map_comp0s) 1; -fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_mapss map_wpulls pickWP_assms_tacs +fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_map0ss map_wpulls pickWP_assms_tacs {context = ctxt, prems = _} = let val n = length rec_0s; @@ -1221,7 +1221,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_maps), (map_wpull, pickWP_assms_tac))) => + CONJ_WRAP' (fn (rec_Suc, ((unfold, set_map0s), (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 ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), @@ -1230,16 +1230,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_maps (j - 1), + SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_map0s (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_map) => + CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map0) => EVERY' [rtac @{thm UN_least}, - SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]), + SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map0, @{thm prod.cases}]), etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, etac set_mp, atac]) - (ks ~~ rev (drop m set_maps))]) - (rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1 + (ks ~~ rev (drop m set_map0s))]) + (rec_Sucs ~~ ((unfolds ~~ set_map0ss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1 end; fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick @@ -1287,29 +1287,29 @@ ALLGOALS (TRY o FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) -fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets dtor_inject - dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss = +fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject + dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss = let val m = length dtor_set_incls; val n = length dtor_set_set_inclss; - val (passive_set_maps, active_set_maps) = chop m set_maps; + val (passive_set_map0s, active_set_map0s) = chop m set_map0s; val in_Jrel = nth in_Jrels (i - 1); val if_tac = EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - EVERY' (map2 (fn set_map => fn set_incl => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map, + EVERY' (map2 (fn set_map0 => fn set_incl => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0, rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, etac (set_incl RS @{thm subset_trans})]) - passive_set_maps dtor_set_incls), - CONJ_WRAP' (fn (in_Jrel, (set_map, dtor_set_set_incls)) => - EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI, + passive_set_map0s dtor_set_incls), + CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) => + EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm prod_caseI}, rtac (in_Jrel 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_Jrels ~~ (active_set_maps ~~ dtor_set_set_inclss)), + (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)), CONJ_WRAP' (fn conv => - EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0, + EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac]) @@ -1317,14 +1317,14 @@ val only_if_tac = EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - CONJ_WRAP' (fn (dtor_set, passive_set_map) => + CONJ_WRAP' (fn (dtor_set, passive_set_map0) => EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least}, - rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map, + rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map0, 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_map, in_Jrel) => EVERY' [rtac ord_eq_le_trans, + (fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans, rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]}, - rtac active_set_map, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least}, + rtac active_set_map0, 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]}, REPEAT_DETERM o eresolve_tac (CollectE :: conjE :: @@ -1335,11 +1335,11 @@ TRY o EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt], REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac]) - (rev (active_set_maps ~~ in_Jrels))]) - (dtor_sets ~~ passive_set_maps), + (rev (active_set_map0s ~~ in_Jrels))]) + (dtor_sets ~~ passive_set_map0s), 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, + rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac, dtac @{thm ssubst_mem[OF pair_collapse]}, @@ -1352,61 +1352,61 @@ EVERY' [rtac iffI, if_tac, only_if_tac] 1 end; -fun mk_rel_coinduct_coind_tac m coinduct ks map_comps map_congs map_arg_congs set_mapss +fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps {context = ctxt, prems = _} = let val n = length ks; in EVERY' [DETERM o rtac coinduct, - EVERY' (map7 (fn i => fn map_comp => fn map_cong => fn map_arg_cong => fn set_maps => + EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s => fn dtor_unfold => fn dtor_map => EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE], select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI, rtac conjI, - rtac (map_comp RS trans), rtac (dtor_map RS trans RS sym), - rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp, map_cong]), + rtac (map_comp0 RS trans), rtac (dtor_map RS trans RS sym), + rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp0, map_cong]), REPEAT_DETERM_N m o rtac @{thm trans[OF fun_cong[OF o_id] sym[OF fun_cong[OF id_o]]]}, REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}), - rtac (map_comp RS trans), rtac (map_cong RS trans), + rtac (map_comp0 RS trans), rtac (map_cong RS trans), REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_o]}, REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}), etac (@{thm prod.cases} RS map_arg_cong RS trans), SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}), - CONJ_WRAP' (fn set_map => + CONJ_WRAP' (fn set_map0 => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], - dtac (set_map RS equalityD1 RS set_mp), + dtac (set_map0 RS equalityD1 RS set_mp), REPEAT_DETERM o eresolve_tac (imageE :: conjE :: @{thms iffD1[OF Pair_eq, elim_format]}), hyp_subst_tac ctxt, rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac, rtac (o_apply RS trans), rtac (@{thm surjective_pairing} RS arg_cong)]) - (drop m set_maps)]) - ks map_comps map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1 + (drop m set_map0s)]) + ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps)] 1 end; val split_id_unfolds = @{thms prod.cases image_id id_apply}; -fun mk_rel_coinduct_ind_tac m ks unfolds set_mapss j set_induct {context = ctxt, prems = _} = +fun mk_rel_coinduct_ind_tac m ks unfolds set_map0ss j set_induct {context = ctxt, prems = _} = let val n = length ks; in rtac set_induct 1 THEN - EVERY' (map3 (fn unfold => fn set_maps => fn i => + EVERY' (map3 (fn unfold => fn set_map0s => fn i => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE, select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp], hyp_subst_tac ctxt, - SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_maps (j - 1)] @ split_id_unfolds)), + SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)), rtac subset_refl]) - unfolds set_mapss ks) 1 THEN - EVERY' (map3 (fn unfold => fn set_maps => fn i => - EVERY' (map (fn set_map => + unfolds set_map0ss ks) 1 THEN + EVERY' (map3 (fn unfold => fn set_map0s => fn i => + EVERY' (map (fn set_map0 => EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE, select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt, - SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map] @ split_id_unfolds)), + SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)), etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [allE, mp], rtac conjI, etac Collect_splitD_set_mp, atac, rtac (@{thm surjective_pairing} RS arg_cong)]) - (drop m set_maps))) - unfolds set_mapss ks) 1 + (drop m set_map0s))) + unfolds set_map0ss ks) 1 end; fun mk_rel_coinduct_tac in_rels in_Jrels helper_indss helper_coind1s helper_coind2s diff -r e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 29 23:22:58 2013 +0200 @@ -164,13 +164,13 @@ map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s) set_bd0ss bd0_Card_orders; val in_bds = map in_bd_of_bnf bnfs; - val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs; - val map_comp's = map map_comp'_of_bnf bnfs; + val sym_map_comps = map (fn bnf => map_comp0_of_bnf bnf RS sym) bnfs; + val map_comps = map map_comp_of_bnf bnfs; val map_cong0s = map map_cong0_of_bnf bnfs; val map_id0s = map map_id0_of_bnf bnfs; - val map_id's = map map_id'_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"); @@ -199,7 +199,7 @@ (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) = map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*) - fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp = + fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 = let val lhs = Term.list_comb (mapBsCs, all_gs) $ (Term.list_comb (mapAsBs, passive_ids @ fs) $ x); @@ -208,15 +208,15 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs))) - (K (mk_map_comp_id_tac map_comp)) + (K (mk_map_comp_id_tac map_comp0)) |> Thm.close_derivation end; - val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's; + val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps; (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==> map id ... id f(m+1) ... f(m+n) x = x*) - fun mk_map_cong0L x mapAsAs sets map_cong0 map_id' = + fun mk_map_cong0L x mapAsAs sets map_cong0 map_id = let fun mk_prem set f z z' = HOLogic.mk_Trueprop (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z)))); @@ -225,11 +225,11 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal))) - (K (mk_map_cong0L_tac m map_cong0 map_id')) + (K (mk_map_cong0L_tac m map_cong0 map_id)) |> Thm.close_derivation end; - val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's; + val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids; val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs; val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs; @@ -394,7 +394,7 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl))) - (K (mk_mor_incl_tac mor_def map_id's)) + (K (mk_mor_incl_tac mor_def map_ids)) |> Thm.close_derivation end; @@ -409,7 +409,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; @@ -427,8 +427,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; @@ -533,7 +532,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 @@ -541,7 +540,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 @@ -886,7 +885,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; @@ -1338,7 +1337,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 [])) @@ -1408,7 +1407,7 @@ ctor_Irel_thms, lthy) = if m = 0 then (timer, replicate n DEADID_bnf, - map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's), + map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids), replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; @@ -1541,7 +1540,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; @@ -1560,13 +1559,13 @@ map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) setss_by_bnf; val setss_by_range' = transpose setss_by_bnf'; - val set_map_thmss = + val set_map0_thmss = let - fun mk_set_map f map z set set' = + fun mk_set_map0 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_map f map z set set')); + (Term.absfree (dest_Free z) (mk_set_map0 f map z set set')); val csetss = map (map (certify lthy)) setss_by_range'; @@ -1579,10 +1578,10 @@ val goals = map3 (fn f => fn sets => fn sets' => HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map4 (mk_set_map f) fs_maps Izs sets sets'))) + (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) @@ -1695,10 +1694,10 @@ val timer = time (timer "helpers for BNF properties"); val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_map_unique_thms; - val map_comp_tacs = - map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks; + val map_comp0_tacs = + map2 (K oo mk_map_comp0_tac map_comps 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_map_tac)) (transpose set_map_thmss); + val set_nat_tacss = map (map (K o mk_set_map0_tac)) (transpose set_map0_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); @@ -1706,7 +1705,7 @@ val rel_OO_Grp_tacs = replicate n (K (rtac refl 1)); - val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss + val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs; val ctor_witss = @@ -1776,15 +1775,15 @@ (mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF)); val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis; in - map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 => + map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 => fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor => - fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss => + fn set_map0s => fn ctor_set_incls => fn ctor_set_set_inclss => Goal.prove_sorry lthy [] [] goal - (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets - ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss)) + (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets + ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss)) |> Thm.close_derivation) - ks goals in_rels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss' - ctor_inject_thms ctor_dtor_thms set_map'ss ctor_set_incl_thmss + ks goals in_rels map_comps map_cong0s folded_ctor_map_thms folded_ctor_set_thmss' + ctor_inject_thms ctor_dtor_thms set_mapss ctor_set_incl_thmss ctor_set_set_incl_thmsss end; diff -r e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 23:22:58 2013 +0200 @@ -39,7 +39,7 @@ val mk_least_min_alg_tac: thm -> thm -> tactic val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list list -> thm list list list -> thm list -> tactic - val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic + val mk_map_comp0_tac: thm list -> thm list -> thm -> int -> tactic val mk_map_id0_tac: thm list -> thm -> tactic val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic @@ -72,7 +72,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_map_tac: thm -> tactic + val mk_set_map0_tac: thm -> tactic val mk_set_tac: thm -> tactic val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic val mk_wpull_tac: thm -> tactic @@ -115,46 +115,46 @@ etac bspec THEN' atac) 1; -fun mk_mor_incl_tac mor_def map_id's = +fun mk_mor_incl_tac mor_def map_ids = (stac mor_def THEN' rtac conjI THEN' - CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_id's THEN' + CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN' CONJ_WRAP' (fn thm => - (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_id's) 1; + (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 = _} = @@ -710,21 +710,21 @@ EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id}, rtac (thm RS sym RS arg_cong)]) map_id0s)) 1; -fun mk_map_comp_tac map_comps ctor_maps unique iplus1 = +fun mk_map_comp0_tac map_comp0s ctor_maps unique iplus1 = let val i = iplus1 - 1; val unique' = Thm.permute_prems 0 i unique; - val map_comps' = drop i map_comps @ take i map_comps; + val map_comp0s' = drop i map_comp0s @ take i map_comp0s; val ctor_maps' = drop i ctor_maps @ take i ctor_maps; fun mk_comp comp simp = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply, rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp, rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply]; in - (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' ctor_maps')) 1 + (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1 end; -fun mk_set_map_tac set_nat = +fun mk_set_map0_tac set_nat = EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1; fun mk_bd_card_order_tac bd_card_orders = @@ -746,34 +746,34 @@ EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set, REPEAT_DETERM_N n o etac UnE]))))] 1); -fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets ctor_inject - ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss = +fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject + ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss = let val m = length ctor_set_incls; val n = length ctor_set_set_inclss; - val (passive_set_maps, active_set_maps) = chop m set_maps; + val (passive_set_map0s, active_set_map0s) = chop m set_map0s; val in_Irel = nth in_Irels (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_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - EVERY' (map2 (fn set_map => fn ctor_set_incl => - EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map, + EVERY' (map2 (fn set_map0 => fn ctor_set_incl => + EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0, 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_maps ctor_set_incls), - CONJ_WRAP' (fn (in_Irel, (set_map, ctor_set_set_incls)) => - EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI, + passive_set_map0s ctor_set_incls), + CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) => + EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm prod_caseI}, rtac (in_Irel 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_Irels ~~ (active_set_maps ~~ ctor_set_set_inclss)), + (in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)), CONJ_WRAP' (fn conv => - EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0, + EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map, @@ -782,13 +782,13 @@ val only_if_tac = EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI, - CONJ_WRAP' (fn (ctor_set, passive_set_map) => + CONJ_WRAP' (fn (ctor_set, passive_set_map0) => 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_map, rtac trans_fun_cong_image_id_id_apply, atac, + rtac passive_set_map0, rtac trans_fun_cong_image_id_id_apply, atac, CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) - (fn (active_set_map, in_Irel) => EVERY' [rtac ord_eq_le_trans, - rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map, rtac @{thm UN_least}, + (fn (active_set_map0, in_Irel) => EVERY' [rtac ord_eq_le_trans, + rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map0, rtac @{thm UN_least}, dtac set_rev_mp, etac @{thm image_mono}, etac imageE, dtac @{thm ssubst_mem[OF pair_collapse]}, REPEAT_DETERM o eresolve_tac (CollectE :: conjE :: @@ -798,11 +798,11 @@ TRY o EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt], REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac]) - (rev (active_set_maps ~~ in_Irels))]) - (ctor_sets ~~ passive_set_maps), + (rev (active_set_map0s ~~ in_Irels))]) + (ctor_sets ~~ passive_set_map0s), 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, + rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac, dtac @{thm ssubst_mem[OF pair_collapse]}, diff -r e414487da3f8 -r 87866222a715 src/HOL/BNF/Tools/bnf_tactics.ML --- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 29 23:22:58 2013 +0200 @@ -106,16 +106,16 @@ split_conv}) THEN rtac refl 1; -fun mk_map_comp_id_tac map_comp = - (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1; +fun mk_map_comp_id_tac map_comp0 = + (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1; fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} = EVERY' [rtac mp, rtac map_cong0, CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; -fun mk_map_cong0L_tac passive map_cong0 map_id' = +fun mk_map_cong0L_tac passive map_cong0 map_id = (rtac trans THEN' rtac map_cong0 THEN' EVERY' (replicate passive (rtac refl))) 1 THEN REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN - rtac map_id' 1; + rtac map_id 1; end; diff -r e414487da3f8 -r 87866222a715 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 29 23:21:48 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Aug 29 23:22:58 2013 +0200 @@ -55,11 +55,11 @@ context topological_space begin -definition "topological_basis B = - ((\b\B. open b) \ (\x. open x \ (\B'. B' \ B \ \B' = x)))" +definition "topological_basis B \ + (\b\B. open b) \ (\x. open x \ (\B'. B' \ B \ \B' = x))" lemma topological_basis: - "topological_basis B = (\x. open x \ (\B'. B' \ B \ \B' = x))" + "topological_basis B \ (\x. open x \ (\B'. B' \ B \ \B' = x))" unfolding topological_basis_def apply safe apply fastforce @@ -198,7 +198,7 @@ by (atomize_elim) simp lemma countable_dense_exists: - shows "\D::'a set. countable D \ (\X. open X \ X \ {} \ (\d \ D. d \ X))" + "\D::'a set. countable D \ (\X. open X \ X \ {} \ (\d \ D. d \ X))" proof - let ?f = "(\B'. SOME x. x \ B')" have "countable (?f ` B)" using countable_basis by simp @@ -667,7 +667,7 @@ lemma closedin_closed: "closedin (subtopology euclidean U) S \ (\T. closed T \ S = U \ T)" by (simp add: closedin_subtopology closed_closedin Int_ac) -lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \ S)" +lemma closedin_closed_Int: "closed S \ closedin (subtopology euclidean U) (U \ S)" by (metis closedin_closed) lemma closed_closedin_trans: @@ -818,7 +818,7 @@ apply (metis zero_le_dist order_trans dist_self) done -lemma ball_empty[intro]: "e \ 0 ==> ball x e = {}" by simp +lemma ball_empty[intro]: "e \ 0 \ ball x e = {}" by simp lemma euclidean_dist_l2: fixes x y :: "'a :: euclidean_space" @@ -830,11 +830,11 @@ lemma rational_boxes: fixes x :: "'a\euclidean_space" - assumes "0 < e" + assumes "e > 0" shows "\a b. (\i\Basis. a \ i \ \ \ b \ i \ \ ) \ x \ box a b \ box a b \ ball x e" proof - def e' \ "e / (2 * sqrt (real (DIM ('a))))" - then have e: "0 < e'" + then have e: "e' > 0" using assms by (auto intro!: divide_pos_pos simp: DIM_positive) have "\i. \y. y \ \ \ y < x \ i \ x \ i - y < e'" (is "\i. ?th i") proof @@ -1087,7 +1087,7 @@ by blast let ?m = "min (e/2) (dist x y) " from e2 y(2) have mp: "?m > 0" - by (simp add: dist_nz[THEN sym]) + by (simp add: dist_nz[symmetric]) from C[rule_format, OF mp] obtain z where z: "z \ S" "z \ x" "dist z x < ?m" by blast have th: "dist z y < e" using z y @@ -1754,7 +1754,7 @@ lemma Lim_at_zero: fixes a :: "'a::real_normed_vector" - fixes l :: "'b::topological_space" + and l :: "'b::topological_space" shows "(f ---> l) (at a) \ ((\x. f(a + x)) ---> l) (at 0)" using LIM_offset_zero LIM_offset_zero_cancel .. @@ -1880,7 +1880,8 @@ lemma closure_sequential: fixes l :: "'a::first_countable_topology" - shows "l \ closure S \ (\x. (\n. x n \ S) \ (x ---> l) sequentially)" (is "?lhs = ?rhs") + shows "l \ closure S \ (\x. (\n. x n \ S) \ (x ---> l) sequentially)" + (is "?lhs = ?rhs") proof assume "?lhs" moreover @@ -1917,7 +1918,7 @@ lemma closed_approachable: fixes S :: "'a::metric_space set" - shows "closed S ==> (\e>0. \y\S. dist y x < e) \ x \ S" + shows "closed S \ (\e>0. \y\S. dist y x < e) \ x \ S" by (metis closure_closed closure_approachable) lemma closure_contains_Inf: @@ -2135,17 +2136,17 @@ using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *) lemma seq_offset_neg: - "(f ---> l) sequentially ==> ((\i. f(i - k)) ---> l) sequentially" + "(f ---> l) sequentially \ ((\i. f(i - k)) ---> l) sequentially" apply (rule topological_tendstoI) apply (drule (2) topological_tendstoD) apply (simp only: eventually_sequentially) - apply (subgoal_tac "\N k (n::nat). N + k <= n ==> N <= n - k") + apply (subgoal_tac "\N k (n::nat). N + k <= n \ N <= n - k") apply metis apply arith done lemma seq_offset_rev: - "((\i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially" + "((\i. f(i + k)) ---> l) sequentially \ (f ---> l) sequentially" by (rule LIMSEQ_offset) (* FIXME: redundant *) lemma seq_harmonic: "((\n. inverse (real n)) ---> 0) sequentially" @@ -2184,7 +2185,7 @@ unfolding open_contains_ball by auto qed -lemma open_contains_cball_eq: "open S ==> (\x. x \ S \ (\e>0. cball x e \ S))" +lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\e>0. cball x e \ S))" by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball) lemma mem_interior_cball: "x \ interior S \ (\e>0. cball x e \ S)" @@ -2196,7 +2197,8 @@ lemma islimpt_ball: fixes x y :: "'a::{real_normed_vector,perfect_space}" - shows "y islimpt ball x e \ 0 < e \ y \ cball x e" (is "?lhs = ?rhs") + shows "y islimpt ball x e \ 0 < e \ y \ cball x e" + (is "?lhs = ?rhs") proof assume "?lhs" { @@ -2233,10 +2235,10 @@ case False have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) = norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))" - unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[THEN sym] + unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric] by auto also have "\ = \- 1 + d / (2 * norm (x - y))\ * norm (x - y)" - using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"] + using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"] unfolding scaleR_minus_left scaleR_one by (auto simp add: norm_minus_commute) also have "\ = \- norm (x - y) + d / 2\" @@ -2402,7 +2404,7 @@ using d as(1)[unfolded subset_eq] by blast have "y - x \ 0" using `x \ y` by auto then have **:"d / (2 * norm (y - x)) > 0" - unfolding zero_less_norm_iff[THEN sym] + unfolding zero_less_norm_iff[symmetric] using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x = norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)" @@ -2427,7 +2429,7 @@ lemma frontier_ball: fixes a :: "'a::real_normed_vector" - shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}" + shows "0 < e \ frontier(ball a e) = {x. dist a x = e}" apply (simp add: frontier_def closure_ball interior_open order_less_imp_le) apply (simp add: set_eq_iff) apply arith @@ -2463,7 +2465,7 @@ lemma cball_sing: fixes x :: "'a::metric_space" - shows "e = 0 ==> cball x e = {x}" + shows "e = 0 \ cball x e = {x}" by (auto simp add: set_eq_iff) @@ -2501,10 +2503,10 @@ lemma bounded_empty [simp]: "bounded {}" by (simp add: bounded_def) -lemma bounded_subset: "bounded T \ S \ T ==> bounded S" +lemma bounded_subset: "bounded T \ S \ T \ bounded S" by (metis bounded_def subset_eq) -lemma bounded_interior[intro]: "bounded S ==> bounded(interior S)" +lemma bounded_interior[intro]: "bounded S \ bounded(interior S)" by (metis bounded_subset interior_subset) lemma bounded_closure[intro]: @@ -2583,7 +2585,7 @@ lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)" by (metis Int_lower1 Int_lower2 bounded_subset) -lemma bounded_diff[intro]: "bounded S ==> bounded (S - T)" +lemma bounded_diff[intro]: "bounded S \ bounded (S - T)" by (metis Diff_subset bounded_subset) lemma not_bounded_UNIV[simp, intro]: @@ -2599,8 +2601,9 @@ qed lemma bounded_linear_image: - assumes "bounded S" "bounded_linear f" - shows "bounded(f ` S)" + assumes "bounded S" + and "bounded_linear f" + shows "bounded (f ` S)" proof - from assms(1) obtain b where b:"b>0" "\x\S. norm x \ b" unfolding bounded_pos by auto @@ -2626,7 +2629,8 @@ lemma bounded_scaling: fixes S :: "'a::real_normed_vector set" shows "bounded S \ bounded ((\x. c *\<^sub>R x) ` S)" - apply (rule bounded_linear_image, assumption) + apply (rule bounded_linear_image) + apply assumption apply (rule bounded_linear_scaleR_right) done @@ -2654,7 +2658,7 @@ lemma bounded_real: fixes S :: "real set" - shows "bounded S \ (\a. \x\S. abs x <= a)" + shows "bounded S \ (\a. \x\S. abs x \ a)" by (simp add: bounded_iff) lemma bounded_has_Sup: @@ -2674,7 +2678,7 @@ lemma Sup_insert: fixes S :: "real set" - shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))" + shows "bounded S \ Sup (insert x S) = (if S = {} then x else max x (Sup S))" apply (subst cSup_insert_If) apply (rule bounded_has_Sup(1)[of S, rule_format]) apply (auto simp: sup_max) @@ -2682,7 +2686,7 @@ lemma Sup_insert_finite: fixes S :: "real set" - shows "finite S \ Sup(insert x S) = (if S = {} then x else max x (Sup S))" + shows "finite S \ Sup (insert x S) = (if S = {} then x else max x (Sup S))" apply (rule Sup_insert) apply (rule finite_imp_bounded) apply simp @@ -2707,7 +2711,7 @@ lemma Inf_insert: fixes S :: "real set" - shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" + shows "bounded S \ Inf (insert x S) = (if S = {} then x else min x (Inf S))" apply (subst cInf_insert_if) apply (rule bounded_has_Inf(1)[of S, rule_format]) apply (auto simp: inf_min) @@ -2715,7 +2719,7 @@ lemma Inf_insert_finite: fixes S :: "real set" - shows "finite S \ Inf(insert x S) = (if S = {} then x else min x (Inf S))" + shows "finite S \ Inf (insert x S) = (if S = {} then x else min x (Inf S))" apply (rule Inf_insert) apply (rule finite_imp_bounded) apply simp @@ -2726,9 +2730,9 @@ subsubsection {* Bolzano-Weierstrass property *} lemma heine_borel_imp_bolzano_weierstrass: - assumes "compact s" "infinite t" "t \ s" + assumes "compact s" and "infinite t" and "t \ s" shows "\x \ s. x islimpt t" -proof(rule ccontr) +proof (rule ccontr) assume "\ (\x \ s. x islimpt t)" then obtain f where f:"\x\s. x \ f x \ open (f x) \ (\y\t. y \ f x \ y = x)" unfolding islimpt_def @@ -2981,7 +2985,8 @@ text{* In particular, some common special cases. *} lemma compact_union [intro]: - assumes "compact s" "compact t" + assumes "compact s" + and "compact t" shows " compact (s \ t)" proof (rule compactI) fix f @@ -3411,7 +3416,10 @@ using assms unfolding seq_compact_def by fast lemma countably_compact_imp_acc_point: - assumes "countably_compact s" "countable t" "infinite t" "t \ s" + assumes "countably_compact s" + and "countable t" + and "infinite t" + and "t \ s" shows "\x\s. \U. x\U \ open U \ infinite (U \ t)" proof (rule ccontr) def C \ "(\F. interior (F \ (- t))) ` {F. finite F \ F \ t }" @@ -3445,7 +3453,8 @@ lemma countable_acc_point_imp_seq_compact: fixes s :: "'a::first_countable_topology set" - assumes "\t. infinite t \ countable t \ t \ s \ (\x\s. \U. x\U \ open U \ infinite (U \ t))" + assumes "\t. infinite t \ countable t \ t \ s \ + (\x\s. \U. x\U \ open U \ infinite (U \ t))" shows "seq_compact s" proof - { @@ -3487,7 +3496,8 @@ lemma seq_compact_eq_acc_point: fixes s :: "'a :: first_countable_topology set" - shows "seq_compact s \ (\t. infinite t \ countable t \ t \ s --> (\x\s. \U. x\U \ open U \ infinite (U \ t)))" + shows "seq_compact s \ + (\t. infinite t \ countable t \ t \ s --> (\x\s. \U. x\U \ open U \ infinite (U \ t)))" using countable_acc_point_imp_seq_compact[of s] countably_compact_imp_acc_point[of s] @@ -3670,7 +3680,8 @@ lemma compact_eq_bounded_closed: fixes s :: "'a::heine_borel set" - shows "compact s \ bounded s \ closed s" (is "?lhs = ?rhs") + shows "compact s \ bounded s \ closed s" + (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs @@ -3707,8 +3718,8 @@ lemma compact_lemma: fixes f :: "nat \ 'a::euclidean_space" assumes "bounded (range f)" - shows "\d\Basis. \l::'a. \ r. subseq r \ - (\e>0. eventually (\n. \i\d. dist (f (r n) \ i) (l \ i) < e) sequentially)" + shows "\d\Basis. \l::'a. \ r. + subseq r \ (\e>0. eventually (\n. \i\d. dist (f (r n) \ i) (l \ i) < e) sequentially)" proof safe fix d :: "'a set" assume d: "d \ Basis" @@ -4133,28 +4144,30 @@ lemma compact_frontier_bounded[intro]: fixes s :: "'a::heine_borel set" - shows "bounded s ==> compact(frontier s)" + shows "bounded s \ compact(frontier s)" unfolding frontier_def using compact_eq_bounded_closed by blast lemma compact_frontier[intro]: fixes s :: "'a::heine_borel set" - shows "compact s ==> compact (frontier s)" + shows "compact s \ compact (frontier s)" using compact_eq_bounded_closed compact_frontier_bounded by blast lemma frontier_subset_compact: fixes s :: "'a::heine_borel set" - shows "compact s ==> frontier s \ s" + shows "compact s \ frontier s \ s" using frontier_subset_closed compact_eq_bounded_closed by blast subsection {* Bounded closed nest property (proof does not use Heine-Borel) *} lemma bounded_closed_nest: - assumes "\n. closed(s n)" "\n. (s n \ {})" - "(\m n. m \ n --> s n \ s m)" "bounded(s 0)" + assumes "\n. closed(s n)" + and "\n. (s n \ {})" + and "(\m n. m \ n --> s n \ s m)" + and "bounded(s 0)" shows "\a::'a::heine_borel. \n::nat. a \ s(n)" proof - from assms(2) obtain x where x:"\n::nat. x n \ s n" @@ -4296,8 +4309,8 @@ lemma uniformly_convergent_eq_cauchy: fixes s::"nat \ 'b \ 'a::complete_space" shows - "(\l. \e>0. \N. \n x. N \ n \ P x --> dist(s n x)(l x) < e) \ - (\e>0. \N. \m n x. N \ m \ N \ n \ P x --> dist (s m x) (s n x) < e)" + "(\l. \e>0. \N. \n x. N \ n \ P x \ dist(s n x)(l x) < e) \ + (\e>0. \N. \m n x. N \ m \ N \ n \ P x \ dist (s m x) (s n x) < e)" (is "?lhs = ?rhs") proof assume ?lhs @@ -4328,7 +4341,7 @@ apply auto done then obtain l where l: "\x. P x \ ((\n. s n x) ---> l x) sequentially" - unfolding convergent_eq_cauchy[THEN sym] + unfolding convergent_eq_cauchy[symmetric] using choice[of "\x l. P x \ ((\n. s n x) ---> l) sequentially"] by auto { @@ -4358,11 +4371,11 @@ lemma uniformly_cauchy_imp_uniformly_convergent: fixes s :: "nat \ 'a \ 'b::complete_space" assumes "\e>0.\N. \m (n::nat) x. N \ m \ N \ n \ P x --> dist(s m x)(s n x) < e" - "\x. P x --> (\e>0. \N. \n. N \ n --> dist(s n x)(l x) < e)" - shows "\e>0. \N. \n x. N \ n \ P x --> dist(s n x)(l x) < e" + and "\x. P x --> (\e>0. \N. \n. N \ n \ dist(s n x)(l x) < e)" + shows "\e>0. \N. \n x. N \ n \ P x \ dist(s n x)(l x) < e" proof - obtain l' where l:"\e>0. \N. \n x. N \ n \ P x \ dist (s n x) (l' x) < e" - using assms(1) unfolding uniformly_convergent_eq_cauchy[THEN sym] by auto + using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto moreover { fix x @@ -4383,7 +4396,7 @@ "continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)" unfolding continuous_within and Lim_within apply auto - unfolding dist_nz[THEN sym] + unfolding dist_nz[symmetric] apply (auto del: allE elim!:allE) apply(rule_tac x=d in exI) apply auto @@ -4411,7 +4424,7 @@ assume "y \ f ` (ball x d \ s)" then have "y \ ball (f x) e" using d(2) - unfolding dist_nz[THEN sym] + unfolding dist_nz[symmetric] apply (auto simp add: dist_commute) apply (erule_tac x=xa in ballE) apply auto @@ -4447,7 +4460,7 @@ apply auto apply (erule_tac x=xa in allE) apply (auto simp add: dist_commute dist_nz) - unfolding dist_nz[THEN sym] + unfolding dist_nz[symmetric] apply auto done next @@ -4534,7 +4547,7 @@ proof eventually_elim case (elim n) then show ?case - using d x(1) `f a \ T` unfolding dist_nz[THEN sym] by auto + using d x(1) `f a \ T` unfolding dist_nz[symmetric] by auto qed } then show ?rhs @@ -4548,15 +4561,16 @@ lemma continuous_at_sequentially: fixes f :: "'a::metric_space \ 'b::topological_space" - shows "continuous (at a) f \ (\x. (x ---> a) sequentially - --> ((f o x) ---> f a) sequentially)" + shows "continuous (at a) f \ + (\x. (x ---> a) sequentially --> ((f o x) ---> f a) sequentially)" using continuous_within_sequentially[of a UNIV f] by simp lemma continuous_on_sequentially: fixes f :: "'a::metric_space \ 'b::topological_space" shows "continuous_on s f \ (\x. \a \ s. (\n. x(n) \ s) \ (x ---> a) sequentially - --> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs") + --> ((f o x) ---> f(a)) sequentially)" + (is "?lhs = ?rhs") proof assume ?rhs then show ?lhs @@ -4878,7 +4892,7 @@ qed lemma continuous_closed_in_preimage: - assumes "continuous_on s f" "closed t" + assumes "continuous_on s f" and "closed t" shows "closedin (subtopology euclidean s) {x \ s. f x \ t}" proof - have *: "\x. x \ s \ f x \ t \ x \ s \ f x \ (t \ f ` s)" @@ -4892,7 +4906,9 @@ qed lemma continuous_open_preimage: - assumes "continuous_on s f" "open s" "open t" + assumes "continuous_on s f" + and "open s" + and "open t" shows "open {x \ s. f x \ t}" proof- obtain T where T: "open T" "{x \ s. f x \ t} = s \ T" @@ -4902,7 +4918,9 @@ qed lemma continuous_closed_preimage: - assumes "continuous_on s f" "closed s" "closed t" + assumes "continuous_on s f" + and "closed s" + and "closed t" shows "closed {x \ s. f x \ t}" proof- obtain T where "closed T" "{x \ s. f x \ t} = s \ T" @@ -4916,7 +4934,7 @@ using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto lemma continuous_closed_preimage_univ: - "(\x. continuous (at x) f) \ closed s ==> closed {x. f x \ s}" + "(\x. continuous (at x) f) \ closed s \ closed {x. f x \ s}" using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto lemma continuous_open_vimage: "\x. continuous (at x) f \ open s \ open (f -` s)" @@ -4926,7 +4944,8 @@ unfolding vimage_def by (rule continuous_closed_preimage_univ) lemma interior_image_subset: - assumes "\x. continuous (at x) f" "inj f" + assumes "\x. continuous (at x) f" + and "inj f" shows "interior (f ` s) \ f ` (interior s)" proof fix x assume "x \ interior (f ` s)" @@ -4947,12 +4966,12 @@ lemma continuous_closed_in_preimage_constant: fixes f :: "_ \ 'b::t1_space" - shows "continuous_on s f ==> closedin (subtopology euclidean s) {x \ s. f x = a}" + shows "continuous_on s f \ closedin (subtopology euclidean s) {x \ s. f x = a}" using continuous_closed_in_preimage[of s f "{a}"] by auto lemma continuous_closed_preimage_constant: fixes f :: "_ \ 'b::t1_space" - shows "continuous_on s f \ closed s ==> closed {x \ s. f x = a}" + shows "continuous_on s f \ closed s \ closed {x \ s. f x = a}" using continuous_closed_preimage[of s f "{a}"] by auto lemma continuous_constant_on_closure: @@ -4966,7 +4985,9 @@ by auto lemma image_closure_subset: - assumes "continuous_on (closure s) f" "closed t" "(f ` s) \ t" + assumes "continuous_on (closure s) f" + and "closed t" + and "(f ` s) \ t" shows "f ` (closure s) \ t" proof - have "s \ {x \ closure s. f x \ t}" @@ -4983,10 +5004,10 @@ assumes "continuous_on (closure s) f" and "\y \ s. norm(f y) \ b" and "x \ (closure s)" - shows "norm(f x) \ b" + shows "norm (f x) \ b" proof - have *: "f ` s \ cball 0 b" - using assms(2)[unfolded mem_cball_0[THEN sym]] by auto + using assms(2)[unfolded mem_cball_0[symmetric]] by auto show ?thesis using image_closure_subset[OF assms(1) closed_cball[of 0 b] *] assms(3) unfolding subset_eq @@ -5002,7 +5023,7 @@ assumes "continuous (at x within s) f" and "f x \ a" shows "\e>0. \y \ s. dist x y < e --> f y \ a" -proof- +proof - obtain U where "open U" and "f x \ U" and "a \ U" using t1_space [OF `f x \ a`] by fast have "(f ---> f x) (at x within s)" @@ -5036,7 +5057,10 @@ lemma continuous_on_open_avoid: fixes f :: "'a::metric_space \ 'b::t1_space" - assumes "continuous_on s f" "open s" "x \ s" "f x \ a" + assumes "continuous_on s f" + and "open s" + and "x \ s" + and "f x \ a" shows "\e>0. \y. dist x y < e \ f y \ a" using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)] using continuous_at_avoid[of x f a] assms(4) @@ -5056,7 +5080,7 @@ fixes f :: "_ \ 'b::t1_space" shows "connected s \ continuous_on s f \ openin (subtopology euclidean s) {x \ s. f x = a} \ - (\x \ s. f x = a) ==> (\x \ s. f x = a)" + (\x \ s. f x = a) \ (\x \ s. f x = a)" using continuous_levelset_open_in_cases[of s f ] by meson @@ -5075,7 +5099,8 @@ lemma open_scaling[intro]: fixes s :: "'a::real_normed_vector set" - assumes "c \ 0" "open s" + assumes "c \ 0" + and "open s" shows "open((\x. c *\<^sub>R x) ` s)" proof - { @@ -5085,7 +5110,7 @@ and e:"\x'. dist x' x < e \ x' \ s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]] by auto have "e * abs c > 0" - using assms(1)[unfolded zero_less_abs_iff[THEN sym]] + using assms(1)[unfolded zero_less_abs_iff[symmetric]] using mult_pos_pos[OF `e>0`] by auto moreover @@ -5095,7 +5120,7 @@ then have "norm ((1 / c) *\<^sub>R y - x) < e" unfolding dist_norm using norm_scaleR[of c "(1 / c) *\<^sub>R y - x", unfolded scaleR_right_diff_distrib, unfolded scaleR_scaleR] assms(1) - assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff) + assms(1)[unfolded zero_less_abs_iff[symmetric]] by (simp del:zero_less_abs_iff) then have "y \ op *\<^sub>R c ` s" using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "op *\<^sub>R c"] using e[THEN spec[where x="(1 / c) *\<^sub>R y"]] @@ -5118,13 +5143,14 @@ lemma open_negations: fixes s :: "'a::real_normed_vector set" - shows "open s ==> open ((\ x. -x) ` s)" + shows "open s \ open ((\ x. -x) ` s)" unfolding scaleR_minus1_left [symmetric] by (rule open_scaling, auto) lemma open_translation: fixes s :: "'a::real_normed_vector set" - assumes "open s" shows "open((\x. a + x) ` s)" + assumes "open s" + shows "open((\x. a + x) ` s)" proof - { fix x @@ -5164,7 +5190,7 @@ unfolding subset_eq Ball_def mem_ball dist_norm apply auto apply (erule_tac x="a + xa" in allE) - unfolding ab_group_add_class.diff_diff_eq[THEN sym] + unfolding ab_group_add_class.diff_diff_eq[symmetric] apply auto done then show "x \ op + a ` interior s" @@ -5217,11 +5243,11 @@ done lemma linear_continuous_within: - "bounded_linear f ==> continuous (at x within s) f" + "bounded_linear f \ continuous (at x within s) f" using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto lemma linear_continuous_on: - "bounded_linear f ==> continuous_on s f" + "bounded_linear f \ continuous_on s f" using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto text {* Also bilinear functions, in composition form. *} @@ -5293,12 +5319,17 @@ qed lemma connected_continuous_image: - assumes "continuous_on s f" "connected s" + assumes "continuous_on s f" + and "connected s" shows "connected(f ` s)" proof - { fix T - assume as: "T \ {}" "T \ f ` s" "openin (subtopology euclidean (f ` s)) T" "closedin (subtopology euclidean (f ` s)) T" + assume as: + "T \ {}" + "T \ f ` s" + "openin (subtopology euclidean (f ` s)) T" + "closedin (subtopology euclidean (f ` s)) T" have "{x \ s. f x \ T} = {} \ {x \ s. f x \ T} = s" using assms(1)[unfolded continuous_on_open, THEN spec[where x=T]] using assms(1)[unfolded continuous_on_closed, THEN spec[where x=T]] @@ -5313,7 +5344,8 @@ text {* Continuity implies uniform continuity on a compact domain. *} lemma compact_uniformly_continuous: - assumes f: "continuous_on s f" and s: "compact s" + assumes f: "continuous_on s f" + and s: "compact s" shows "uniformly_continuous_on s f" unfolding uniformly_continuous_on_def proof (cases, safe) @@ -5415,7 +5447,7 @@ shows "continuous (at x) f \ (\e>0. \d>0. \x'. norm(x' - x) < d --> abs(f x' - f x) < e)" unfolding continuous_at unfolding Lim_at - unfolding dist_nz[THEN sym] + unfolding dist_nz[symmetric] unfolding dist_norm apply auto apply (erule_tac x=e in allE) @@ -5454,7 +5486,8 @@ lemma distance_attains_inf: fixes a :: "'a::heine_borel" - assumes "closed s" "s \ {}" + assumes "closed s" + and "s \ {}" shows "\x\s. \y\s. dist a x \ dist a y" proof - from assms(2) obtain b where "b \ s" by auto @@ -5569,12 +5602,13 @@ lemma compact_negations: fixes s :: "'a::real_normed_vector set" assumes "compact s" - shows "compact ((\x. -x) ` s)" + shows "compact ((\x. - x) ` s)" using compact_scaling [OF assms, of "- 1"] by auto lemma compact_sums: fixes s t :: "'a::real_normed_vector set" - assumes "compact s" and "compact t" + assumes "compact s" + and "compact t" shows "compact {x + y | x y. x \ s \ y \ t}" proof - have *: "{x + y | x y. x \ s \ y \ t} = (\z. fst z + snd z) ` (s \ t)" @@ -5591,7 +5625,9 @@ lemma compact_differences: fixes s t :: "'a::real_normed_vector set" - assumes "compact s" "compact t" shows "compact {x - y | x y. x \ s \ y \ t}" + assumes "compact s" + and "compact t" + shows "compact {x - y | x y. x \ s \ y \ t}" proof- have "{x - y | x y. x\s \ y \ t} = {x + y | x y. x \ s \ y \ (uminus ` t)}" apply auto @@ -5630,7 +5666,8 @@ lemma compact_sup_maxdistance: fixes s :: "'a::metric_space set" - assumes "compact s" "s \ {}" + assumes "compact s" + and "s \ {}" shows "\x\s. \y\s. \u\s. \v\s. dist u v \ dist x y" proof - have "compact (s \ s)" @@ -5688,17 +5725,19 @@ lemma diameter_bounded: assumes "bounded s" shows "\x\s. \y\s. dist x y \ diameter s" - "\d>0. d < diameter s \ (\x\s. \y\s. dist x y > d)" + and "\d>0. d < diameter s \ (\x\s. \y\s. dist x y > d)" using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms by auto lemma diameter_compact_attained: - assumes "compact s" "s \ {}" + assumes "compact s" + and "s \ {}" shows "\x\s. \y\s. dist x y = diameter s" proof - have b: "bounded s" using assms(1) by (rule compact_imp_bounded) - then obtain x y where xys: "x\s" "y\s" and xy: "\u\s. \v\s. dist u v \ dist x y" + then obtain x y where xys: "x\s" "y\s" + and xy: "\u\s. \v\s. dist u v \ dist x y" using compact_sup_maxdistance[OF assms] by auto then have "diameter s \ dist x y" unfolding diameter_def @@ -5752,7 +5791,7 @@ using as(2)[unfolded LIMSEQ_def, THEN spec[where x="e * abs c"]] by auto then have "\N. \n\N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e" unfolding dist_norm - unfolding scaleR_right_diff_distrib[THEN sym] + unfolding scaleR_right_diff_distrib[symmetric] using mult_imp_div_pos_less[of "abs c" _ e] `c\0` by auto } then have "((\n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" @@ -5795,7 +5834,9 @@ unfolding o_def by auto then have "l - l' \ t" - using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\ n. snd (f (r n))"], THEN spec[where x="l - l'"]] + using assms(2)[unfolded closed_sequential_limits, + THEN spec[where x="\ n. snd (f (r n))"], + THEN spec[where x="l - l'"]] using f(3) by auto then have "l \ ?S" @@ -5812,7 +5853,8 @@ lemma closed_compact_sums: fixes s t :: "'a::real_normed_vector set" - assumes "closed s" "compact t" + assumes "closed s" + and "compact t" shows "closed {x + y | x y. x \ s \ y \ t}" proof - have "{x + y |x y. x \ t \ y \ s} = {x + y |x y. x \ s \ y \ t}" @@ -5828,7 +5870,8 @@ lemma compact_closed_differences: fixes s t :: "'a::real_normed_vector set" - assumes "compact s" and "closed t" + assumes "compact s" + and "closed t" shows "closed {x - y | x y. x \ s \ y \ t}" proof - have "{x + y |x y. x \ s \ y \ uminus ` t} = {x - y |x y. x \ s \ y \ t}" @@ -5844,7 +5887,8 @@ lemma closed_compact_differences: fixes s t :: "'a::real_normed_vector set" - assumes "closed s" "compact t" + assumes "closed s" + and "compact t" shows "closed {x - y | x y. x \ s \ y \ t}" proof - have "{x + y |x y. x \ s \ y \ uminus ` t} = {x - y |x y. x \ s \ y \ t}" @@ -5917,7 +5961,8 @@ lemma separate_point_closed: fixes s :: "'a::heine_borel set" - assumes "closed s" and "a \ s" + assumes "closed s" + and "a \ s" shows "\d>0. \x\s. d \ dist a x" proof (cases "s = {}") case True @@ -6049,7 +6094,8 @@ lemma interval_sing: fixes a :: "'a::ordered_euclidean_space" - shows "{a .. a} = {a}" and "{a<.. {c .. d} = {(\i\Basis. max (a\i) (c\i) *\<^sub>R i) .. (\i\Basis. min (b\i) (d\i) *\<^sub>R i)}" + shows "{a .. b} \ {c .. d} = + {(\i\Basis. max (a\i) (c\i) *\<^sub>R i) .. (\i\Basis. min (b\i) (d\i) *\<^sub>R i)}" unfolding set_eq_iff and Int_iff and mem_interval by auto @@ -6225,7 +6272,8 @@ fixes a b :: "'a::ordered_euclidean_space" shows "interior {a..b} = {a<.. ?L" using interval_open_subset_closed open_interval + show "?R \ ?L" + using interval_open_subset_closed open_interval by (rule interior_maximal) { fix x @@ -6296,7 +6344,7 @@ lemma not_interval_univ: fixes a :: "'a::ordered_euclidean_space" - shows "({a .. b} \ UNIV) \ ({a<.. UNIV)" + shows "{a .. b} \ UNIV \ {a<.. UNIV" using bounded_interval[of a b] by auto lemma compact_interval: @@ -6462,12 +6510,13 @@ lemma bounded_subset_open_interval: fixes s :: "('a::ordered_euclidean_space) set" - shows "bounded s ==> (\a b. s \ {a<.. (\a b. s \ {a<..a. s \ {-a .. a}" + assumes "bounded s" + shows "\a. s \ {-a .. a}" proof - obtain a where "s \ {- a<.. (\a b. s \ {a .. b})" + shows "bounded s \ \a b. s \ {a .. b}" using bounded_subset_closed_interval_symmetric[of s] by auto lemma frontier_closed_interval: @@ -6503,7 +6552,7 @@ fixes a :: "'a::ordered_euclidean_space" assumes "{c<.. {}" shows "{a<.. {c .. d} = {} \ {a<.. {c<.. s" "y \ s" "inner a x \ b" "b \ inner a y" + assumes "connected s" + and "x \ s" + and "y \ s" + and "inner a x \ b" + and "b \ inner a y" shows "\z \ s. inner a z = b" proof (rule ccontr) assume as:"\ (\z\s. inner a z = b)" @@ -6823,9 +6876,12 @@ let ?B = "{x. inner a x > b}" have "open ?A" "open ?B" using open_halfspace_lt and open_halfspace_gt by auto - moreover have "?A \ ?B = {}" by auto - moreover have "s \ ?A \ ?B" using as by auto - ultimately show False + moreover + have "?A \ ?B = {}" by auto + moreover + have "s \ ?A \ ?B" using as by auto + ultimately + show False using assms(1)[unfolded connected_def not_ex, THEN spec[where x="?A"], THEN spec[where x="?B"]] using assms(2-5) @@ -6951,7 +7007,7 @@ then obtain x where x:"f x = y" "x\s" using assms(3) by auto then have "g (f x) = x" using g by auto - then have "f (g y) = y" unfolding x(1)[THEN sym] by auto + then have "f (g y) = y" unfolding x(1)[symmetric] by auto } then have g':"\x\t. f (g x) = x" by auto moreover @@ -6971,7 +7027,7 @@ then have "x \ s" unfolding g_def using someI2[of "\b. b\s \ f b = y" x' "\x. x\s"] - unfolding y(2)[THEN sym] and g_def + unfolding y(2)[symmetric] and g_def by auto } ultimately have "x\s \ x \ g ` t" .. @@ -7069,9 +7125,11 @@ proof - interpret f: bounded_linear f by fact { - fix d::real assume "d>0" + fix d :: real + assume "d > 0" then obtain N where N:"\n\N. norm (f (x n) - f (x N)) < e * d" - using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] + using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] + and e and mult_pos_pos[of e d] by auto { fix n @@ -7082,7 +7140,7 @@ using normf[THEN bspec[where x="x n - x N"]] by auto also have "norm (f (x n - x N)) < e * d" - using `N \ n` N unfolding f.diff[THEN sym] by auto + using `N \ n` N unfolding f.diff[symmetric] by auto finally have "norm (x n - x N) < d" using `e>0` by simp } then have "\N. \n\N. norm (x n - x N) < d" by auto @@ -7091,13 +7149,13 @@ qed lemma complete_isometric_image: - fixes f :: "'a::euclidean_space => 'b::euclidean_space" + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "0 < e" and s: "subspace s" and f: "bounded_linear f" and normf: "\x\s. norm(f x) \ e * norm(x)" and cs: "complete s" - shows "complete(f ` s)" + shows "complete (f ` s)" proof - { fix g @@ -7156,7 +7214,7 @@ then obtain b where "b\s" and ba: "norm b = norm a" and b: "\x\{x \ s. norm x = norm a}. norm (f b) \ norm (f x)" - unfolding *[THEN sym] unfolding image_iff by auto + unfolding *[symmetric] unfolding image_iff by auto let ?e = "norm (f b) / norm b" have "norm b > 0" using ba and a and norm_ge_zero by auto @@ -7179,7 +7237,7 @@ case False then have *: "0 < norm a / norm x" using `a\0` - unfolding zero_less_norm_iff[THEN sym] + unfolding zero_less_norm_iff[symmetric] by (simp only: divide_pos_pos) have "\c. \x\s. c *\<^sub>R x \ s" using s[unfolded subspace_def] by auto @@ -7203,7 +7261,7 @@ using injective_imp_isometric[OF assms(4,1,2,3)] by auto show ?thesis using complete_isometric_image[OF `e>0` assms(1,2) e] and assms(4) - unfolding complete_eq_closed[THEN sym] by auto + unfolding complete_eq_closed[symmetric] by auto qed @@ -7299,7 +7357,7 @@ qed lemma closed_subspace: - fixes s::"('a::euclidean_space) set" + fixes s :: "'a::euclidean_space set" assumes "subspace s" shows "closed s" proof - @@ -7349,36 +7407,37 @@ subsection {* Affine transformations of intervals *} lemma real_affinity_le: - "0 < (m::'a::linordered_field) ==> (m * x + c \ y \ x \ inverse(m) * y + -(c / m))" + "0 < (m::'a::linordered_field) \ (m * x + c \ y \ x \ inverse(m) * y + -(c / m))" by (simp add: field_simps inverse_eq_divide) lemma real_le_affinity: - "0 < (m::'a::linordered_field) ==> (y \ m * x + c \ inverse(m) * y + -(c / m) \ x)" + "0 < (m::'a::linordered_field) \ (y \ m * x + c \ inverse(m) * y + -(c / m) \ x)" by (simp add: field_simps inverse_eq_divide) lemma real_affinity_lt: - "0 < (m::'a::linordered_field) ==> (m * x + c < y \ x < inverse(m) * y + -(c / m))" + "0 < (m::'a::linordered_field) \ (m * x + c < y \ x < inverse(m) * y + -(c / m))" by (simp add: field_simps inverse_eq_divide) lemma real_lt_affinity: - "0 < (m::'a::linordered_field) ==> (y < m * x + c \ inverse(m) * y + -(c / m) < x)" + "0 < (m::'a::linordered_field) \ (y < m * x + c \ inverse(m) * y + -(c / m) < x)" by (simp add: field_simps inverse_eq_divide) lemma real_affinity_eq: - "(m::'a::linordered_field) \ 0 ==> (m * x + c = y \ x = inverse(m) * y + -(c / m))" + "(m::'a::linordered_field) \ 0 \ (m * x + c = y \ x = inverse(m) * y + -(c / m))" by (simp add: field_simps inverse_eq_divide) lemma real_eq_affinity: - "(m::'a::linordered_field) \ 0 ==> (y = m * x + c \ inverse(m) * y + -(c / m) = x)" + "(m::'a::linordered_field) \ 0 \ (y = m * x + c \ inverse(m) * y + -(c / m) = x)" by (simp add: field_simps inverse_eq_divide) lemma image_affinity_interval: fixes m::real fixes a b c :: "'a::ordered_euclidean_space" shows "(\x. m *\<^sub>R x + c) ` {a .. b} = - (if {a .. b} = {} then {} - else (if 0 \ m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} - else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))" + (if {a .. b} = {} then {} + else (if 0 \ m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} + else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))" proof (cases "m = 0") + case True { fix x assume "x \ c" "c \ x" @@ -7389,9 +7448,9 @@ apply (auto intro: order_antisym) done } - moreover case True - moreover have "c \ {m *\<^sub>R a + c..m *\<^sub>R b + c}" unfolding True by(auto simp add: eucl_le[where 'a='a]) - ultimately show ?thesis by auto + moreover have "c \ {m *\<^sub>R a + c..m *\<^sub>R b + c}" + unfolding True by (auto simp add: eucl_le[where 'a='a]) + ultimately show ?thesis using True by auto next case False { @@ -7441,8 +7500,8 @@ assumes s: "complete s" "s \ {}" and c: "0 \ c" "c < 1" and f: "(f ` s) \ s" - and lipschitz:"\x\s. \y\s. dist (f x) (f y) \ c * dist x y" - shows "\! x\s. (f x = x)" + and lipschitz: "\x\s. \y\s. dist (f x) (f y) \ c * dist x y" + shows "\!x\s. f x = x" proof - have "1 - c > 0" using c by auto diff -r e414487da3f8 -r 87866222a715 src/Pure/General/time.scala --- a/src/Pure/General/time.scala Thu Aug 29 23:21:48 2013 +0200 +++ b/src/Pure/General/time.scala Thu Aug 29 23:22:58 2013 +0200 @@ -30,6 +30,7 @@ def min(t: Time): Time = if (ms < t.ms) this else t def max(t: Time): Time = if (ms > t.ms) this else t + def is_zero: Boolean = ms == 0 def is_relevant: Boolean = ms >= 1 override def hashCode: Int = ms.hashCode diff -r e414487da3f8 -r 87866222a715 src/Pure/Isar/completion.scala --- a/src/Pure/Isar/completion.scala Thu Aug 29 23:21:48 2013 +0200 +++ b/src/Pure/Isar/completion.scala Thu Aug 29 23:22:58 2013 +0200 @@ -13,7 +13,11 @@ { /* items */ - sealed case class Item(original: String, replacement: String, description: String) + sealed case class Item( + original: String, + replacement: String, + description: String, + immediate: Boolean) { override def toString: String = description } @@ -105,9 +109,12 @@ } raw_result match { case Some((word, cs)) => - val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word) + val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs) if (ds.isEmpty) None - else Some((word, ds.map(s => Completion.Item(word, s, s)))) + else { + val immediate = !Completion.is_word(word) + Some((word, ds.map(s => Completion.Item(word, s, s, immediate)))) + } case None => None } } diff -r e414487da3f8 -r 87866222a715 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Thu Aug 29 23:21:48 2013 +0200 +++ b/src/Tools/jEdit/etc/options Thu Aug 29 23:22:58 2013 +0200 @@ -33,12 +33,18 @@ public option jedit_timing_threshold : real = 0.1 -- "default threshold for timing display" + +section "Completion" + public option jedit_completion : bool = true -- "enable completion popup" public option jedit_completion_delay : real = 0.0 -- "delay for completion popup (seconds)" +public option jedit_completion_immediate : bool = false + -- "insert unique completion immediately into buffer (if delay = 0)" + section "Rendering of Document Content" diff -r e414487da3f8 -r 87866222a715 src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Thu Aug 29 23:21:48 2013 +0200 +++ b/src/Tools/jEdit/src/actions.xml Thu Aug 29 23:22:58 2013 +0200 @@ -117,6 +117,11 @@ isabelle.jedit.Isabelle.decrease_font_size(view); + + + isabelle.jedit.Isabelle.complete(view); + + isabelle.jedit.Isabelle.control_sub(textArea); diff -r e414487da3f8 -r 87866222a715 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Thu Aug 29 23:21:48 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Thu Aug 29 23:22:58 2013 +0200 @@ -9,14 +9,15 @@ import isabelle._ -import java.awt.{Font, Point, BorderLayout, Dimension} -import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} +import java.awt.{Color, Font, Point, BorderLayout, Dimension} +import java.awt.event.{InputEvent, KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities} +import javax.swing.border.LineBorder import scala.swing.{ListView, ScrollPane} import scala.swing.event.MouseClicked -import org.gjt.sp.jedit.View +import org.gjt.sp.jedit.{View, Debug} import org.gjt.sp.jedit.textarea.JEditTextArea @@ -66,26 +67,10 @@ class Text_Area private(text_area: JEditTextArea) { - /* popup state */ - private var completion_popup: Option[Completion_Popup] = None - def dismissed(): Boolean = - { - Swing_Thread.require() - completion_popup match { - case Some(completion) => - completion.hide_popup() - completion_popup = None - true - case None => - false - } - } - - - /* insert selected item */ + /* completion action */ private def insert(item: Completion.Item) { @@ -106,8 +91,56 @@ } } + def action(immediate: Boolean) + { + val view = text_area.getView + val layered = view.getLayeredPane + val buffer = text_area.getBuffer + val painter = text_area.getPainter - /* input of key events */ + if (buffer.isEditable) { + Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { + case Some(syntax) => + val caret = text_area.getCaretPosition + val line = buffer.getLineOfOffset(caret) + val start = buffer.getLineStartOffset(line) + val text = buffer.getSegment(start, caret - start) + + syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match { + case Some((_, List(item))) if item.immediate && immediate => + insert(item) + + case Some((original, items)) => + val font = + painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale")) + + val loc1 = text_area.offsetToXY(caret - original.length) + if (loc1 != null) { + val loc2 = + SwingUtilities.convertPoint(painter, + loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) + + val completion = + new Completion_Popup(layered, loc2, font, items) { + override def complete(item: Completion.Item) { insert(item) } + override def propagate(evt: KeyEvent) { + JEdit_Lib.propagate_key(view, evt) + input(evt) + } + override def refocus() { text_area.requestFocus } + } + completion_popup = Some(completion) + completion.show_popup() + } + case None => + } + case None => + } + } + } + + + /* input key events */ def input(evt: KeyEvent) { @@ -116,60 +149,46 @@ if (PIDE.options.bool("jedit_completion")) { if (!evt.isConsumed) { dismissed() - input_delay.invoke() + + val mod = evt.getModifiers + val special = + evt.getKeyChar == '\b' || + // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java + (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 || + (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 && + !Debug.ALT_KEY_PRESSED_DISABLED || + (mod & InputEvent.META_MASK) != 0 + + if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { + input_delay.revoke() + action(PIDE.options.bool("jedit_completion_immediate")) + } + else input_delay.invoke() } } - else { - dismissed() - input_delay.revoke() - } } private val input_delay = - Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) - { - val view = text_area.getView - val layered = view.getLayeredPane - val buffer = text_area.getBuffer - val painter = text_area.getPainter + Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { + action(false) + } - if (buffer.isEditable) { - Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { - case Some(syntax) => - val caret = text_area.getCaretPosition - val line = buffer.getLineOfOffset(caret) - val start = buffer.getLineStartOffset(line) - val text = buffer.getSegment(start, caret - start) - syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match { - case Some((original, items)) => - val font = - painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale")) + /* dismiss popup */ - val loc1 = text_area.offsetToXY(caret - original.length) - if (loc1 != null) { - val loc2 = - SwingUtilities.convertPoint(painter, - loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) + def dismissed(): Boolean = + { + Swing_Thread.require() - val completion = - new Completion_Popup(layered, loc2, font, items) { - override def complete(item: Completion.Item) { insert(item) } - override def propagate(evt: KeyEvent) { - JEdit_Lib.propagate_key(view, evt) - input(evt) - } - override def refocus() { text_area.requestFocus } - } - completion_popup = Some(completion) - completion.show_popup() - } - case None => - } - case None => - } - } + completion_popup match { + case Some(completion) => + completion.hide_popup() + completion_popup = None + true + case None => + false } + } /* activation */ @@ -289,7 +308,7 @@ /* main content */ override def getFocusTraversalKeysEnabled = false - + completion.setBorder(new LineBorder(Color.BLACK)) completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent]) diff -r e414487da3f8 -r 87866222a715 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Thu Aug 29 23:21:48 2013 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Thu Aug 29 23:22:58 2013 +0200 @@ -11,7 +11,7 @@ import org.gjt.sp.jedit.{jEdit, View, Buffer} import org.gjt.sp.jedit.textarea.JEditTextArea -import org.gjt.sp.jedit.gui.DockableWindowManager +import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord} object Isabelle @@ -163,6 +163,17 @@ } + /* completion */ + + def complete(view: View) + { + Completion_Popup.Text_Area(view.getTextArea) match { + case Some(text_area_completion) => text_area_completion.action(true) + case None => CompleteWord.completeWord(view) + } + } + + /* control styles */ def control_sub(text_area: JEditTextArea) diff -r e414487da3f8 -r 87866222a715 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Thu Aug 29 23:21:48 2013 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Thu Aug 29 23:22:58 2013 +0200 @@ -190,6 +190,8 @@ isabelle-sledgehammer.dock-position=bottom isabelle-symbols.dock-position=bottom isabelle-theories.dock-position=right +isabelle.complete.label=Complete text +isabelle.complete.shortcut=C+b isabelle.control-bold.label=Control bold isabelle.control-bold.shortcut=C+e RIGHT isabelle.control-reset.label=Control reset