--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Aug 18 13:19:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Aug 18 14:19:23 2014 +0200
@@ -55,6 +55,7 @@
val in_mono_of_bnf: bnf -> thm
val in_rel_of_bnf: bnf -> thm
val inj_map_of_bnf: bnf -> thm
+ val inj_map_strong_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
@@ -73,6 +74,7 @@
val rel_cong_of_bnf: bnf -> thm
val rel_conversep_of_bnf: bnf -> thm
val rel_mono_of_bnf: bnf -> thm
+ val rel_mono_strong0_of_bnf: bnf -> thm
val rel_mono_strong_of_bnf: bnf -> thm
val rel_eq_of_bnf: bnf -> thm
val rel_flip_of_bnf: bnf -> thm
@@ -222,6 +224,7 @@
in_mono: thm lazy,
in_rel: thm lazy,
inj_map: thm lazy,
+ inj_map_strong: thm lazy,
map_comp: thm lazy,
map_cong: thm lazy,
map_id: thm lazy,
@@ -234,6 +237,7 @@
rel_cong: thm lazy,
rel_map: thm list lazy,
rel_mono: thm lazy,
+ rel_mono_strong0: thm lazy,
rel_mono_strong: thm lazy,
rel_Grp: thm lazy,
rel_conversep: thm lazy,
@@ -241,8 +245,9 @@
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
- inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
- rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
+ inj_map inj_map_strong map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
+ rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp
+ rel_conversep rel_OO = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
@@ -252,6 +257,7 @@
in_mono = in_mono,
in_rel = in_rel,
inj_map = inj_map,
+ inj_map_strong = inj_map_strong,
map_comp = map_comp,
map_cong = map_cong,
map_id = map_id,
@@ -264,6 +270,7 @@
rel_cong = rel_cong,
rel_map = rel_map,
rel_mono = rel_mono,
+ rel_mono_strong0 = rel_mono_strong0,
rel_mono_strong = rel_mono_strong,
rel_Grp = rel_Grp,
rel_conversep = rel_conversep,
@@ -279,6 +286,7 @@
in_mono,
in_rel,
inj_map,
+ inj_map_strong,
map_comp,
map_cong,
map_id,
@@ -291,6 +299,7 @@
rel_cong,
rel_map,
rel_mono,
+ rel_mono_strong0,
rel_mono_strong,
rel_Grp,
rel_conversep,
@@ -304,6 +313,7 @@
in_mono = Lazy.map f in_mono,
in_rel = Lazy.map f in_rel,
inj_map = Lazy.map f inj_map,
+ inj_map_strong = Lazy.map f inj_map_strong,
map_comp = Lazy.map f map_comp,
map_cong = Lazy.map f map_cong,
map_id = Lazy.map f map_id,
@@ -316,6 +326,7 @@
rel_cong = Lazy.map f rel_cong,
rel_map = Lazy.map (map f) rel_map,
rel_mono = Lazy.map f rel_mono,
+ rel_mono_strong0 = Lazy.map f rel_mono_strong0,
rel_mono_strong = Lazy.map f rel_mono_strong,
rel_Grp = Lazy.map f rel_Grp,
rel_conversep = Lazy.map f rel_conversep,
@@ -425,6 +436,7 @@
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 inj_map_strong_of_bnf = Lazy.force o #inj_map_strong 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;
@@ -445,6 +457,7 @@
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_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
@@ -598,6 +611,7 @@
val in_monoN = "in_mono";
val in_relN = "in_rel";
val inj_mapN = "inj_map";
+val inj_map_strongN = "inj_map_strong";
val map_id0N = "map_id0";
val map_idN = "map_id";
val map_identN = "map_ident";
@@ -615,6 +629,7 @@
val rel_conversepN = "rel_conversep";
val rel_mapN = "rel_map"
val rel_monoN = "rel_mono"
+val rel_mono_strong0N = "rel_mono_strong0"
val rel_mono_strongN = "rel_mono_strong"
val rel_comppN = "rel_compp";
val rel_compp_GrpN = "rel_compp_Grp";
@@ -652,9 +667,9 @@
(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_transferN, [Lazy.force (#map_transfer facts)]),
+ (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
(rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
(set_map0N, #set_map0 axioms),
(set_bdN, #set_bd axioms)] @
@@ -669,7 +684,9 @@
fun note_unless_dont_note (noted0, lthy0) =
let
val notes =
- [(map_compN, [Lazy.force (#map_comp facts)], []),
+ [(inj_mapN, [Lazy.force (#inj_map facts)], []),
+ (inj_map_strongN, [Lazy.force (#inj_map_strong facts)], []),
+ (map_compN, [Lazy.force (#map_comp facts)], []),
(map_cong0N, [#map_cong0 axioms], []),
(map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
(map_idN, [Lazy.force (#map_id facts)], []),
@@ -948,16 +965,19 @@
fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
val pre_names_lthy = lthy;
- val ((((((((((((((((((fs, gs), hs), is), x), y), zs), ys), As),
+ val (((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), zs), zs'), ys), As),
As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs),
transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
|> mk_Frees "f" (map2 (curry op -->) As' Bs')
+ ||>> mk_Frees "f" (map2 (curry op -->) As' Bs')
||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs)
||>> mk_Frees "h" (map2 (curry op -->) As' Ts)
||>> mk_Frees "i" (map2 (curry op -->) As' Cs)
||>> yield_singleton (mk_Frees "x") CA'
+ ||>> yield_singleton (mk_Frees "x") CA'
||>> yield_singleton (mk_Frees "y") CB'
||>> mk_Frees "z" As'
+ ||>> mk_Frees "z" As'
||>> mk_Frees "y" Bs'
||>> mk_Frees "A" (map HOLogic.mk_setT As')
||>> mk_Frees "A" (map HOLogic.mk_setT As')
@@ -1299,7 +1319,7 @@
val rel_flip = Lazy.lazy mk_rel_flip;
- fun mk_rel_mono_strong () =
+ fun mk_rel_mono_strong0 () =
let
fun mk_prem setA setB R S a b =
HOLogic.mk_Trueprop
@@ -1312,11 +1332,15 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
- (fn {context = ctxt, prems = _} => mk_rel_mono_strong_tac ctxt (Lazy.force in_rel)
+ (fn {context = ctxt, prems = _} => mk_rel_mono_strong0_tac ctxt (Lazy.force in_rel)
(map Lazy.force set_map))
|> Thm.close_derivation
end;
+ val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
+
+ fun mk_rel_mono_strong () = Object_Logic.rulify lthy (Lazy.force rel_mono_strong0)
+
val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
fun mk_rel_map () =
@@ -1334,12 +1358,13 @@
mk_vimage2p (HOLogic.id_const T) f $ P) gs S_AsCs As') $ x $ y];
val goals = map2 mk_goal lhss rhss;
in
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ goals
+ |> map (fn goal => Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_rel_map0_tac ctxt live (Lazy.force rel_OO) (Lazy.force rel_conversep)
- (Lazy.force rel_Grp) (Lazy.force map_id))
- |> Conjunction.elim_balanced (length goals)
- |> map (unfold_thms lthy @{thms vimage2p_def id_apply})
+ (Lazy.force rel_Grp) (Lazy.force map_id)))
+ |> map (unfold_thms lthy @{thms vimage2p_def[of id, unfolded id_apply]
+ vimage2p_def[of _ id, unfolded id_apply]})
|> map Thm.close_derivation
end;
@@ -1364,11 +1389,36 @@
val map_transfer = Lazy.lazy mk_map_transfer;
+ fun mk_inj_map_strong () =
+ let
+ val assms = map5 (fn setA => fn z => fn f => fn z' => fn f' =>
+ fold_rev Logic.all [z, z']
+ (Logic.mk_implies (mk_Trueprop_mem (z, setA $ x),
+ Logic.mk_implies (mk_Trueprop_mem (z', setA $ x'),
+ Logic.mk_implies (mk_Trueprop_eq (f $ z, f' $ z'),
+ mk_Trueprop_eq (z, z')))))) bnf_sets_As zs fs zs' fs';
+ val concl = Logic.mk_implies
+ (mk_Trueprop_eq
+ (Term.list_comb (bnf_map_AsBs, fs) $ x,
+ Term.list_comb (bnf_map_AsBs, fs') $ x'),
+ mk_Trueprop_eq (x, x'));
+ val goal = fold_rev Logic.all (x :: x' :: fs @ fs')
+ (fold_rev (curry Logic.mk_implies) assms concl);
+ in
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ mk_inj_map_strong_tac ctxt (Lazy.force rel_eq) (Lazy.force rel_map)
+ (Lazy.force rel_mono_strong))
+ |> Thm.close_derivation
+ end;
+
+ val inj_map_strong = Lazy.lazy mk_inj_map_strong;
+
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 inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
- rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
+ in_mono in_rel inj_map inj_map_strong map_comp map_cong map_id map_ident0 map_ident
+ map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0
+ 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 Mon Aug 18 13:19:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Aug 18 14:19:23 2014 +0200
@@ -11,6 +11,7 @@
sig
val mk_collect_set_map_tac: thm list -> tactic
val mk_in_mono_tac: int -> tactic
+ val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic
val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic
val mk_map_id: thm -> thm
val mk_map_ident: Proof.context -> thm -> thm
@@ -25,7 +26,7 @@
val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
val mk_rel_mono_tac: thm list -> thm -> tactic
- val mk_rel_mono_strong_tac: Proof.context -> thm -> thm list -> tactic
+ val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
@@ -70,6 +71,17 @@
REPEAT_DETERM_N n o atac))
end;
+fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong =
+ let
+ val rel_eq' = rel_eq RS @{thm predicate2_eqD};
+ val rel_maps' = map (fn thm => thm RS iffD1) rel_maps;
+ in
+ HEADGOAL (dtac (rel_eq' RS iffD2) THEN' rtac (rel_eq' RS iffD1)) THEN
+ EVERY (map (HEADGOAL o dtac) rel_maps') THEN
+ HEADGOAL (etac rel_mono_strong) THEN
+ TRYALL (Goal.assume_rule_tac ctxt)
+ 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 =>
@@ -197,7 +209,7 @@
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,
- REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply,
+ 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],
@@ -211,7 +223,7 @@
in_tac @{thm sndOp_in}] 1
end;
-fun mk_rel_mono_strong_tac ctxt in_rel set_maps =
+fun mk_rel_mono_strong0_tac ctxt in_rel set_maps =
if null set_maps then atac 1
else
unfold_tac ctxt [in_rel] THEN
@@ -252,10 +264,10 @@
let
val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1};
val inserts =
- map (fn set_bd =>
+ map (fn set_bd =>
iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF
[set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]])
- set_bds;
+ set_bds;
in
EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm cprod_cinfinite_bound},
rtac (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac @{thm card_of_Card_order},