--- a/src/HOL/BNF_Def.thy Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/BNF_Def.thy Wed Apr 23 10:23:26 2014 +0200
@@ -14,19 +14,19 @@
"bnf" :: thy_goal
begin
-lemma collect_comp: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
+lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
by (rule ext) (auto simp only: comp_apply collect_def)
definition convol ("<_ , _>") where
"<f , g> \<equiv> %a. (f a, g a)"
lemma fst_convol:
-"fst o <f , g> = f"
+"fst \<circ> <f , g> = f"
apply(rule ext)
unfolding convol_def by simp
lemma snd_convol:
-"snd o <f , g> = g"
+"snd \<circ> <f , g> = g"
apply(rule ext)
unfolding convol_def by simp
@@ -97,10 +97,10 @@
"csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
-lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
+lemma snd_fst_flip: "snd xy = (fst \<circ> (%(x, y). (y, x))) xy"
by (simp split: prod.split)
-lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy"
+lemma fst_snd_flip: "fst xy = (snd \<circ> (%(x, y). (y, x))) xy"
by (simp split: prod.split)
lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
@@ -134,16 +134,19 @@
lemma If_the_inv_into_f_f:
"\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow>
- ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
+ ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<circ> g) i = id i"
unfolding Func_def by (auto elim: the_inv_into_f_f)
+lemma the_inv_f_o_f_id: "inj f \<Longrightarrow> (the_inv f \<circ> f) z = id z"
+ by (simp add: the_inv_f_f)
+
lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
unfolding vimage2p_def by -
lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
unfolding rel_fun_def vimage2p_def by auto
-lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
+lemma convol_image_vimage2p: "<f \<circ> fst, g \<circ> snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
unfolding vimage2p_def convol_def by auto
lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 10:23:26 2014 +0200
@@ -53,6 +53,7 @@
val in_cong_of_bnf: bnf -> thm
val in_mono_of_bnf: bnf -> thm
val in_rel_of_bnf: bnf -> thm
+ val inj_map_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
@@ -217,6 +218,7 @@
in_cong: thm lazy,
in_mono: thm lazy,
in_rel: thm lazy,
+ inj_map: thm lazy,
map_comp: thm lazy,
map_cong: thm lazy,
map_id: thm lazy,
@@ -233,7 +235,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 rel_eq rel_flip set_map rel_cong rel_mono
+ inj_map map_comp map_cong map_id map_transfer 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,
@@ -243,6 +245,7 @@
in_cong = in_cong,
in_mono = in_mono,
in_rel = in_rel,
+ inj_map = inj_map,
map_comp = map_comp,
map_cong = map_cong,
map_id = map_id,
@@ -266,6 +269,7 @@
in_cong,
in_mono,
in_rel,
+ inj_map,
map_comp,
map_cong,
map_id,
@@ -287,6 +291,7 @@
in_cong = Lazy.map f in_cong,
in_mono = Lazy.map f in_mono,
in_rel = Lazy.map f in_rel,
+ inj_map = Lazy.map f inj_map,
map_comp = Lazy.map f map_comp,
map_cong = Lazy.map f map_cong,
map_id = Lazy.map f map_id,
@@ -404,6 +409,7 @@
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;
val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
+val inj_map_of_bnf = Lazy.force o #inj_map 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;
@@ -572,6 +578,7 @@
val in_bdN = "in_bd";
val in_monoN = "in_mono";
val in_relN = "in_rel";
+val inj_mapN = "inj_map";
val map_id0N = "map_id0";
val map_idN = "map_id";
val map_comp0N = "map_comp0";
@@ -624,6 +631,7 @@
(in_bdN, [Lazy.force (#in_bd facts)]),
(in_monoN, [Lazy.force (#in_mono facts)]),
(in_relN, [Lazy.force (#in_rel facts)]),
+ (inj_mapN, [Lazy.force (#inj_map facts)]),
(map_comp0N, [#map_comp0 axioms]),
(map_id0N, [#map_id0 axioms]),
(map_transferN, [Lazy.force (#map_transfer facts)]),
@@ -1103,6 +1111,19 @@
val map_cong = Lazy.lazy mk_map_cong;
+ fun mk_inj_map () =
+ let
+ val prems = map (HOLogic.mk_Trueprop o mk_inj) fs;
+ val concl = HOLogic.mk_Trueprop (mk_inj (Term.list_comb (bnf_map_AsBs, fs)));
+ val goal = fold_rev Logic.all fs (Logic.list_implies (prems, concl));
+ in
+ Goal.prove_sorry lthy [] [] goal (fn _ => mk_inj_map_tac live (Lazy.force map_id)
+ (Lazy.force map_comp) (#map_cong0 axioms) (Lazy.force map_cong))
+ |> Thm.close_derivation
+ end;
+
+ val inj_map = Lazy.lazy mk_inj_map;
+
val set_map = map (fn thm => Lazy.lazy (fn () => mk_set_map thm)) (#set_map0 axioms);
val wit_thms =
@@ -1289,7 +1310,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 rel_eq rel_flip set_map
+ in_mono in_rel inj_map map_comp map_cong map_id map_transfer 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;
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Apr 23 10:23:26 2014 +0200
@@ -9,10 +9,11 @@
signature BNF_DEF_TACTICS =
sig
val mk_collect_set_map_tac: thm list -> tactic
+ val mk_in_mono_tac: int -> tactic
+ val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic
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_set_map: thm -> thm
val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic
@@ -55,6 +56,16 @@
((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
(etac subset_trans THEN' atac) 1;
+fun mk_inj_map_tac n map_id map_comp map_cong0 map_cong =
+ let
+ val map_cong' = map_cong OF (asm_rl :: replicate n refl);
+ val map_cong0' = map_cong0 OF (replicate n @{thm the_inv_f_o_f_id});
+ in
+ HEADGOAL (rtac @{thm injI} THEN' etac (map_cong' RS box_equals) THEN'
+ REPEAT_DETERM_N 2 o (rtac (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN'
+ REPEAT_DETERM_N n o atac))
+ end;
+
fun mk_collect_set_map_tac set_map0s =
(rtac (@{thm collect_comp} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
EVERY' (map (fn set_map0 =>
--- a/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 23 10:23:26 2014 +0200
@@ -101,6 +101,7 @@
val mk_rel_fun: term -> term -> term
val mk_image: term -> term
val mk_in: term list -> term list -> typ -> term
+ val mk_inj: term -> term
val mk_leq: term -> term -> term
val mk_ordLeq: term -> term -> term
val mk_rel_comp: term * term -> term
@@ -470,6 +471,12 @@
else HOLogic.mk_UNIV T
end;
+fun mk_inj t =
+ let val T as Type (@{type_name fun}, [domT, ranT]) = fastype_of t in
+ Const (@{const_name inj_on}, T --> HOLogic.mk_setT domT --> HOLogic.boolT) $ t
+ $ HOLogic.mk_UNIV domT
+ end;
+
fun mk_leq t1 t2 =
Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;