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