--- a/src/HOL/BNF/BNF_Def.thy Thu Sep 12 11:23:49 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy Thu Sep 12 11:23:49 2013 +0200
@@ -89,6 +89,9 @@
lemma eq_OOI: "R = op = \<Longrightarrow> R = R OO R"
by auto
+lemma OO_Grp_alt: "(Grp A f)^--1 OO Grp A g = (\<lambda>x y. \<exists>z. z \<in> A \<and> f z = x \<and> g z = y)"
+ unfolding Grp_def by auto
+
lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f"
unfolding Grp_def by auto
--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Sep 12 11:23:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Sep 12 11:23:49 2013 +0200
@@ -770,7 +770,7 @@
val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
val pre_names_lthy = lthy;
- val (((((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), ys), As),
+ val ((((((((((((((((((((((((fs, gs), hs), x), y), zs), ys), As),
As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
|> mk_Frees "f" (map2 (curry op -->) As' Bs')
@@ -778,7 +778,6 @@
||>> mk_Frees "h" (map2 (curry op -->) As' Ts)
||>> yield_singleton (mk_Frees "x") CA'
||>> yield_singleton (mk_Frees "y") CB'
- ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs'
||>> mk_Frees "z" As'
||>> mk_Frees "y" Bs'
||>> mk_Frees "A" (map HOLogic.mk_setT As')
@@ -1093,7 +1092,8 @@
val map_wppull = Lazy.lazy mk_map_wppull;
- val rel_OO_Grps = no_refl [#rel_OO_Grp axioms];
+ val rel_OO_Grp = #rel_OO_Grp axioms;
+ val rel_OO_Grps = no_refl [rel_OO_Grp];
fun mk_rel_Grp () =
let
@@ -1182,23 +1182,7 @@
val rel_OO = Lazy.lazy mk_rel_OO;
- fun mk_in_rel () =
- let
- val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs';
- val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
- val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
- val map_fst_eq = HOLogic.mk_eq (map1 $ z, x);
- val map_snd_eq = HOLogic.mk_eq (map2 $ z, y);
- val lhs = Term.list_comb (rel, Rs) $ x $ y;
- val rhs =
- HOLogic.mk_exists (fst z', snd z', HOLogic.mk_conj (HOLogic.mk_mem (z, bnf_in),
- HOLogic.mk_conj (map_fst_eq, map_snd_eq)));
- val goal =
- fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
- in
- Goal.prove_sorry lthy [] [] goal (mk_in_rel_tac (the_single rel_OO_Grps))
- |> Thm.close_derivation
- end;
+ fun mk_in_rel () = trans OF [rel_OO_Grp, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD};
val in_rel = Lazy.lazy mk_in_rel;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Sep 12 11:23:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Sep 12 11:23:49 2013 +0200
@@ -21,7 +21,6 @@
val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic
val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_in_rel_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
val mk_rel_conversep_tac: thm -> thm -> tactic
val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
@@ -209,13 +208,6 @@
rtac (map_comp0 RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
end;
-fun mk_in_rel_tac rel_OO_Gr {context = ctxt, prems = _} =
- EVERY' [rtac (rel_OO_Gr RS fun_cong RS fun_cong RS trans), rtac iffI,
- REPEAT_DETERM o eresolve_tac [@{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
- hyp_subst_tac ctxt, rtac exI, rtac conjI, atac, rtac conjI, rtac refl, rtac refl,
- REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI},
- etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1;
-
fun mk_rel_mono_strong_tac in_rel set_map0s {context = ctxt, prems = _} =
if null set_map0s then atac 1
else