--- 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 \<forall> that both
produce the Isabelle symbol \<forall> 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".
--- 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 \<le> 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 \<in> sset (smerge ss)"
thus "x \<in> 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 \<in> sset ss" "x \<in> sset s"
thus "x \<in> sset (smerge ss)" using snth_sset_smerge by (auto simp: sset_range)
@@ -480,7 +480,7 @@
"sproduct s1 s2 = smerge (smap (\<lambda>x. smap (Pair x) s2) s1)"
lemma sset_sproduct: "sset (sproduct s1 s2) = sset s1 \<times> 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 *}
--- 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)
--- 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 \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
unfolding fset_rel_def set_rel_def by auto
@@ -881,7 +881,7 @@
Plus: "\<lbrakk>R a b; multiset_rel' R M N\<rbrakk> \<Longrightarrow> multiset_rel' R (M + {#a#}) (N + {#b#})"
lemma multiset_map_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> 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 "\<exists> N1. N = N1 + {#f a#} \<and> mmap f M = N1"
proof-
have "f a \<in># 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 "\<exists> M1 a. M = M1 + {#a#} \<and> f a = b \<and> mmap f M1 = N"
proof-
obtain a where a: "a \<in># 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
--- 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));
--- 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]}],
--- 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)
--- 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;
--- 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);
--- 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;
--- 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
--- 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
--- 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;
--- 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]},
--- 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;
--- 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 =
- ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x)))"
+definition "topological_basis B \<longleftrightarrow>
+ (\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
lemma topological_basis:
- "topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
+ "topological_basis B \<longleftrightarrow> (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
unfolding topological_basis_def
apply safe
apply fastforce
@@ -198,7 +198,7 @@
by (atomize_elim) simp
lemma countable_dense_exists:
- shows "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
+ "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
proof -
let ?f = "(\<lambda>B'. SOME x. x \<in> B')"
have "countable (?f ` B)" using countable_basis by simp
@@ -667,7 +667,7 @@
lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
by (simp add: closedin_subtopology closed_closedin Int_ac)
-lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \<inter> S)"
+lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> 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 \<le> 0 ==> ball x e = {}" by simp
+lemma ball_empty[intro]: "e \<le> 0 \<Longrightarrow> 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\<Colon>euclidean_space"
- assumes "0 < e"
+ assumes "e > 0"
shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e"
proof -
def e' \<equiv> "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 "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>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 \<in> S" "z \<noteq> 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) \<longleftrightarrow> ((\<lambda>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 \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
+ shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (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 ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
+ shows "closed S \<Longrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> 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 ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
+ "(f ---> l) sequentially \<Longrightarrow> ((\<lambda>i. f(i - k)) ---> l) sequentially"
apply (rule topological_tendstoI)
apply (drule (2) topological_tendstoD)
apply (simp only: eventually_sequentially)
- apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
+ apply (subgoal_tac "\<And>N k (n::nat). N + k <= n \<Longrightarrow> N <= n - k")
apply metis
apply arith
done
lemma seq_offset_rev:
- "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
+ "((\<lambda>i. f(i + k)) ---> l) sequentially \<Longrightarrow> (f ---> l) sequentially"
by (rule LIMSEQ_offset) (* FIXME: redundant *)
lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
@@ -2184,7 +2185,7 @@
unfolding open_contains_ball by auto
qed
-lemma open_contains_cball_eq: "open S ==> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"
+lemma open_contains_cball_eq: "open S \<Longrightarrow> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"
by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)
lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
@@ -2196,7 +2197,8 @@
lemma islimpt_ball:
fixes x y :: "'a::{real_normed_vector,perfect_space}"
- shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e" (is "?lhs = ?rhs")
+ shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> 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 "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * 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 "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
@@ -2402,7 +2404,7 @@
using d as(1)[unfolded subset_eq] by blast
have "y - x \<noteq> 0" using `x \<noteq> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> S \<subseteq> T ==> bounded S"
+lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> bounded S"
by (metis bounded_def subset_eq)
-lemma bounded_interior[intro]: "bounded S ==> bounded(interior S)"
+lemma bounded_interior[intro]: "bounded S \<Longrightarrow> bounded(interior S)"
by (metis bounded_subset interior_subset)
lemma bounded_closure[intro]:
@@ -2583,7 +2585,7 @@
lemma bounded_Int[intro]: "bounded S \<or> bounded T \<Longrightarrow> bounded (S \<inter> T)"
by (metis Int_lower1 Int_lower2 bounded_subset)
-lemma bounded_diff[intro]: "bounded S ==> bounded (S - T)"
+lemma bounded_diff[intro]: "bounded S \<Longrightarrow> 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" "\<forall>x\<in>S. norm x \<le> b"
unfolding bounded_pos by auto
@@ -2626,7 +2629,8 @@
lemma bounded_scaling:
fixes S :: "'a::real_normed_vector set"
shows "bounded S \<Longrightarrow> bounded ((\<lambda>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 \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. abs x <= a)"
+ shows "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. abs x \<le> 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 \<Longrightarrow> 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 \<Longrightarrow> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
+ shows "finite S \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
+ shows "finite S \<Longrightarrow> 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 \<subseteq> s"
+ assumes "compact s" and "infinite t" and "t \<subseteq> s"
shows "\<exists>x \<in> s. x islimpt t"
-proof(rule ccontr)
+proof (rule ccontr)
assume "\<not> (\<exists>x \<in> s. x islimpt t)"
then obtain f where f:"\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> 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 \<union> 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 \<subseteq> s"
+ assumes "countably_compact s"
+ and "countable t"
+ and "infinite t"
+ and "t \<subseteq> s"
shows "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t)"
proof (rule ccontr)
def C \<equiv> "(\<lambda>F. interior (F \<union> (- t))) ` {F. finite F \<and> F \<subseteq> t }"
@@ -3445,7 +3453,8 @@
lemma countable_acc_point_imp_seq_compact:
fixes s :: "'a::first_countable_topology set"
- assumes "\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t))"
+ assumes "\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s \<longrightarrow>
+ (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> 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 \<longleftrightarrow> (\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s --> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t)))"
+ shows "seq_compact s \<longleftrightarrow>
+ (\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s --> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> 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 \<longleftrightarrow> bounded s \<and> closed s" (is "?lhs = ?rhs")
+ shows "compact s \<longleftrightarrow> bounded s \<and> closed s"
+ (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
@@ -3707,8 +3718,8 @@
lemma compact_lemma:
fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
assumes "bounded (range f)"
- shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. subseq r \<and>
- (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
+ shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
+ subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
proof safe
fix d :: "'a set"
assume d: "d \<subseteq> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<subseteq> s"
+ shows "compact s \<Longrightarrow> frontier s \<subseteq> 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 "\<forall>n. closed(s n)" "\<forall>n. (s n \<noteq> {})"
- "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)" "bounded(s 0)"
+ assumes "\<forall>n. closed(s n)"
+ and "\<forall>n. (s n \<noteq> {})"
+ and "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)"
+ and "bounded(s 0)"
shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s(n)"
proof -
from assms(2) obtain x where x:"\<forall>n::nat. x n \<in> s n"
@@ -4296,8 +4309,8 @@
lemma uniformly_convergent_eq_cauchy:
fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
shows
- "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e) \<longleftrightarrow>
- (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x --> dist (s m x) (s n x) < e)"
+ "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e) \<longleftrightarrow>
+ (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x \<longrightarrow> 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: "\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) ---> l x) sequentially"
- unfolding convergent_eq_cauchy[THEN sym]
+ unfolding convergent_eq_cauchy[symmetric]
using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) ---> l) sequentially"]
by auto
{
@@ -4358,11 +4371,11 @@
lemma uniformly_cauchy_imp_uniformly_convergent:
fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
- "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n --> dist(s n x)(l x) < e)"
- shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e"
+ and "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n \<longrightarrow> dist(s n x)(l x) < e)"
+ shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
proof -
obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> 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 \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> 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 \<in> f ` (ball x d \<inter> s)"
then have "y \<in> 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 \<in> T` unfolding dist_nz[THEN sym] by auto
+ using d x(1) `f a \<in> T` unfolding dist_nz[symmetric] by auto
qed
}
then show ?rhs
@@ -4548,15 +4561,16 @@
lemma continuous_at_sequentially:
fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
- shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
- --> ((f o x) ---> f a) sequentially)"
+ shows "continuous (at a) f \<longleftrightarrow>
+ (\<forall>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 \<Rightarrow> 'b::topological_space"
shows "continuous_on s f \<longleftrightarrow>
(\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (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 \<in> s. f x \<in> t}"
proof -
have *: "\<forall>x. x \<in> s \<and> f x \<in> t \<longleftrightarrow> x \<in> s \<and> f x \<in> (t \<inter> 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 \<in> s. f x \<in> t}"
proof-
obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> 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 \<in> s. f x \<in> t}"
proof-
obtain T where "closed T" "{x \<in> s. f x \<in> t} = s \<inter> 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:
- "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
+ "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s \<Longrightarrow> closed {x. f x \<in> s}"
using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
lemma continuous_open_vimage: "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
@@ -4926,7 +4944,8 @@
unfolding vimage_def by (rule continuous_closed_preimage_univ)
lemma interior_image_subset:
- assumes "\<forall>x. continuous (at x) f" "inj f"
+ assumes "\<forall>x. continuous (at x) f"
+ and "inj f"
shows "interior (f ` s) \<subseteq> f ` (interior s)"
proof
fix x assume "x \<in> interior (f ` s)"
@@ -4947,12 +4966,12 @@
lemma continuous_closed_in_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
- shows "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
+ shows "continuous_on s f \<Longrightarrow> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
using continuous_closed_in_preimage[of s f "{a}"] by auto
lemma continuous_closed_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
- shows "continuous_on s f \<Longrightarrow> closed s ==> closed {x \<in> s. f x = a}"
+ shows "continuous_on s f \<Longrightarrow> closed s \<Longrightarrow> closed {x \<in> 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) \<subseteq> t"
+ assumes "continuous_on (closure s) f"
+ and "closed t"
+ and "(f ` s) \<subseteq> t"
shows "f ` (closure s) \<subseteq> t"
proof -
have "s \<subseteq> {x \<in> closure s. f x \<in> t}"
@@ -4983,10 +5004,10 @@
assumes "continuous_on (closure s) f"
and "\<forall>y \<in> s. norm(f y) \<le> b"
and "x \<in> (closure s)"
- shows "norm(f x) \<le> b"
+ shows "norm (f x) \<le> b"
proof -
have *: "f ` s \<subseteq> 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 \<noteq> a"
shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"
-proof-
+proof -
obtain U where "open U" and "f x \<in> U" and "a \<notin> U"
using t1_space [OF `f x \<noteq> 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 \<Rightarrow> 'b::t1_space"
- assumes "continuous_on s f" "open s" "x \<in> s" "f x \<noteq> a"
+ assumes "continuous_on s f"
+ and "open s"
+ and "x \<in> s"
+ and "f x \<noteq> a"
shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> 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 :: "_ \<Rightarrow> 'b::t1_space"
shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
openin (subtopology euclidean s) {x \<in> s. f x = a} \<Longrightarrow>
- (\<exists>x \<in> s. f x = a) ==> (\<forall>x \<in> s. f x = a)"
+ (\<exists>x \<in> s. f x = a) \<Longrightarrow> (\<forall>x \<in> 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 \<noteq> 0" "open s"
+ assumes "c \<noteq> 0"
+ and "open s"
shows "open((\<lambda>x. c *\<^sub>R x) ` s)"
proof -
{
@@ -5085,7 +5110,7 @@
and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> 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 \<in> 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 ((\<lambda> x. -x) ` s)"
+ shows "open s \<Longrightarrow> open ((\<lambda> 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((\<lambda>x. a + x) ` s)"
+ assumes "open s"
+ shows "open((\<lambda>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 \<in> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<noteq> {}" "T \<noteq> f ` s" "openin (subtopology euclidean (f ` s)) T" "closedin (subtopology euclidean (f ` s)) T"
+ assume as:
+ "T \<noteq> {}"
+ "T \<noteq> f ` s"
+ "openin (subtopology euclidean (f ` s)) T"
+ "closedin (subtopology euclidean (f ` s)) T"
have "{x \<in> s. f x \<in> T} = {} \<or> {x \<in> s. f x \<in> 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 \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>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 \<noteq> {}"
+ assumes "closed s"
+ and "s \<noteq> {}"
shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a x \<le> dist a y"
proof -
from assms(2) obtain b where "b \<in> s" by auto
@@ -5569,12 +5602,13 @@
lemma compact_negations:
fixes s :: "'a::real_normed_vector set"
assumes "compact s"
- shows "compact ((\<lambda>x. -x) ` s)"
+ shows "compact ((\<lambda>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 \<in> s \<and> y \<in> t}"
proof -
have *: "{x + y | x y. x \<in> s \<and> y \<in> t} = (\<lambda>z. fst z + snd z) ` (s \<times> 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 \<in> s \<and> y \<in> t}"
+ assumes "compact s"
+ and "compact t"
+ shows "compact {x - y | x y. x \<in> s \<and> y \<in> t}"
proof-
have "{x - y | x y. x\<in>s \<and> y \<in> t} = {x + y | x y. x \<in> s \<and> y \<in> (uminus ` t)}"
apply auto
@@ -5630,7 +5666,8 @@
lemma compact_sup_maxdistance:
fixes s :: "'a::metric_space set"
- assumes "compact s" "s \<noteq> {}"
+ assumes "compact s"
+ and "s \<noteq> {}"
shows "\<exists>x\<in>s. \<exists>y\<in>s. \<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
proof -
have "compact (s \<times> s)"
@@ -5688,17 +5725,19 @@
lemma diameter_bounded:
assumes "bounded s"
shows "\<forall>x\<in>s. \<forall>y\<in>s. dist x y \<le> diameter s"
- "\<forall>d>0. d < diameter s \<longrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. dist x y > d)"
+ and "\<forall>d>0. d < diameter s \<longrightarrow> (\<exists>x\<in>s. \<exists>y\<in>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 \<noteq> {}"
+ assumes "compact s"
+ and "s \<noteq> {}"
shows "\<exists>x\<in>s. \<exists>y\<in>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\<in>s" "y\<in>s" and xy: "\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
+ then obtain x y where xys: "x\<in>s" "y\<in>s"
+ and xy: "\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
using compact_sup_maxdistance[OF assms] by auto
then have "diameter s \<le> 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 "\<exists>N. \<forall>n\<ge>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\<noteq>0` by auto
}
then have "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially"
@@ -5795,7 +5834,9 @@
unfolding o_def
by auto
then have "l - l' \<in> t"
- using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda> n. snd (f (r n))"], THEN spec[where x="l - l'"]]
+ using assms(2)[unfolded closed_sequential_limits,
+ THEN spec[where x="\<lambda> n. snd (f (r n))"],
+ THEN spec[where x="l - l'"]]
using f(3)
by auto
then have "l \<in> ?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 \<in> s \<and> y \<in> t}"
proof -
have "{x + y |x y. x \<in> t \<and> y \<in> s} = {x + y |x y. x \<in> s \<and> y \<in> 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 \<in> s \<and> y \<in> t}"
proof -
have "{x + y |x y. x \<in> s \<and> y \<in> uminus ` t} = {x - y |x y. x \<in> s \<and> y \<in> 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 \<in> s \<and> y \<in> t}"
proof -
have "{x + y |x y. x \<in> s \<and> y \<in> uminus ` t} = {x - y |x y. x \<in> s \<and> y \<in> t}"
@@ -5917,7 +5961,8 @@
lemma separate_point_closed:
fixes s :: "'a::heine_borel set"
- assumes "closed s" and "a \<notin> s"
+ assumes "closed s"
+ and "a \<notin> s"
shows "\<exists>d>0. \<forall>x\<in>s. d \<le> 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<..<a} = {}"
+ shows "{a .. a} = {a}"
+ and "{a<..<a} = {}"
unfolding set_eq_iff mem_interval eq_iff [symmetric]
by (auto intro: euclidean_eqI simp: ex_in_conv)
@@ -6173,7 +6219,8 @@
lemma inter_interval:
fixes a :: "'a::ordered_euclidean_space"
- shows "{a .. b} \<inter> {c .. d} = {(\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)}"
+ shows "{a .. b} \<inter> {c .. d} =
+ {(\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>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<..<b}" (is "?L = ?R")
proof(rule subset_antisym)
- show "?R \<subseteq> ?L" using interval_open_subset_closed open_interval
+ show "?R \<subseteq> ?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} \<noteq> UNIV) \<and> ({a<..<b} \<noteq> UNIV)"
+ shows "{a .. b} \<noteq> UNIV \<and> {a<..<b} \<noteq> 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 ==> (\<exists>a b. s \<subseteq> {a<..<b})"
+ shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> {a<..<b})"
by (auto dest!: bounded_subset_open_interval_symmetric)
lemma bounded_subset_closed_interval_symmetric:
fixes s :: "('a::ordered_euclidean_space) set"
- assumes "bounded s" shows "\<exists>a. s \<subseteq> {-a .. a}"
+ assumes "bounded s"
+ shows "\<exists>a. s \<subseteq> {-a .. a}"
proof -
obtain a where "s \<subseteq> {- a<..<a}"
using bounded_subset_open_interval_symmetric[OF assms] by auto
@@ -6477,7 +6526,7 @@
lemma bounded_subset_closed_interval:
fixes s :: "('a::ordered_euclidean_space) set"
- shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> {a .. b})"
+ shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> {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<..<d} \<noteq> {}"
shows "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> {a<..<b} \<inter> {c<..<d} = {}"
- unfolding closure_open_interval[OF assms, THEN sym]
+ unfolding closure_open_interval[OF assms, symmetric]
unfolding open_inter_closure_eq_empty[OF open_interval] ..
@@ -6815,7 +6864,11 @@
text{* Some more convenient intermediate-value theorem formulations. *}
lemma connected_ivt_hyperplane:
- assumes "connected s" "x \<in> s" "y \<in> s" "inner a x \<le> b" "b \<le> inner a y"
+ assumes "connected s"
+ and "x \<in> s"
+ and "y \<in> s"
+ and "inner a x \<le> b"
+ and "b \<le> inner a y"
shows "\<exists>z \<in> s. inner a z = b"
proof (rule ccontr)
assume as:"\<not> (\<exists>z\<in>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 \<inter> ?B = {}" by auto
- moreover have "s \<subseteq> ?A \<union> ?B" using as by auto
- ultimately show False
+ moreover
+ have "?A \<inter> ?B = {}" by auto
+ moreover
+ have "s \<subseteq> ?A \<union> ?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\<in>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':"\<forall>x\<in>t. f (g x) = x" by auto
moreover
@@ -6971,7 +7027,7 @@
then have "x \<in> s"
unfolding g_def
using someI2[of "\<lambda>b. b\<in>s \<and> f b = y" x' "\<lambda>x. x\<in>s"]
- unfolding y(2)[THEN sym] and g_def
+ unfolding y(2)[symmetric] and g_def
by auto
}
ultimately have "x\<in>s \<longleftrightarrow> x \<in> 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:"\<forall>n\<ge>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 \<le> n` N unfolding f.diff[THEN sym] by auto
+ using `N \<le> n` N unfolding f.diff[symmetric] by auto
finally have "norm (x n - x N) < d" using `e>0` by simp
}
then have "\<exists>N. \<forall>n\<ge>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 \<Rightarrow> 'b::euclidean_space"
assumes "0 < e"
and s: "subspace s"
and f: "bounded_linear f"
and normf: "\<forall>x\<in>s. norm(f x) \<ge> 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\<in>s"
and ba: "norm b = norm a"
and b: "\<forall>x\<in>{x \<in> s. norm x = norm a}. norm (f b) \<le> 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\<noteq>0`
- unfolding zero_less_norm_iff[THEN sym]
+ unfolding zero_less_norm_iff[symmetric]
by (simp only: divide_pos_pos)
have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> 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 \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
+ "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
by (simp add: field_simps inverse_eq_divide)
lemma real_le_affinity:
- "0 < (m::'a::linordered_field) ==> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
+ "0 < (m::'a::linordered_field) \<Longrightarrow> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
by (simp add: field_simps inverse_eq_divide)
lemma real_affinity_lt:
- "0 < (m::'a::linordered_field) ==> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
+ "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c < y \<longleftrightarrow> 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 \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
+ "0 < (m::'a::linordered_field) \<Longrightarrow> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
by (simp add: field_simps inverse_eq_divide)
lemma real_affinity_eq:
- "(m::'a::linordered_field) \<noteq> 0 ==> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
+ "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
by (simp add: field_simps inverse_eq_divide)
lemma real_eq_affinity:
- "(m::'a::linordered_field) \<noteq> 0 ==> (y = m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
+ "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c \<longleftrightarrow> 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 "(\<lambda>x. m *\<^sub>R x + c) ` {a .. b} =
- (if {a .. b} = {} then {}
- else (if 0 \<le> 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 \<le> 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 \<le> c" "c \<le> x"
@@ -7389,9 +7448,9 @@
apply (auto intro: order_antisym)
done
}
- moreover case True
- moreover have "c \<in> {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 \<in> {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 \<noteq> {}"
and c: "0 \<le> c" "c < 1"
and f: "(f ` s) \<subseteq> s"
- and lipschitz:"\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
- shows "\<exists>! x\<in>s. (f x = x)"
+ and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
+ shows "\<exists>!x\<in>s. f x = x"
proof -
have "1 - c > 0" using c by auto
--- 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
--- 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
}
}
--- 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"
--- 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);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.complete">
+ <CODE>
+ isabelle.jedit.Isabelle.complete(view);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.control-sub">
<CODE>
isabelle.jedit.Isabelle.control_sub(textArea);
--- 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])
--- 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)
--- 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