simplified derivation of in_rel
authortraytel
Thu Sep 12 11:23:49 2013 +0200 (2013-09-12)
changeset 5356192bcac4f9ac9
parent 53560 4b5f42cfa244
child 53562 9d8764624487
simplified derivation of in_rel
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_def_tactics.ML
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:23:49 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:23:49 2013 +0200
     1.3 @@ -89,6 +89,9 @@
     1.4  lemma eq_OOI: "R = op = \<Longrightarrow> R = R OO R"
     1.5    by auto
     1.6  
     1.7 +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)"
     1.8 +  unfolding Grp_def by auto
     1.9 +
    1.10  lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f"
    1.11  unfolding Grp_def by auto
    1.12  
     2.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Sep 12 11:23:49 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Sep 12 11:23:49 2013 +0200
     2.3 @@ -770,7 +770,7 @@
     2.4      val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
     2.5  
     2.6      val pre_names_lthy = lthy;
     2.7 -    val (((((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), ys), As),
     2.8 +    val ((((((((((((((((((((((((fs, gs), hs), x), y), zs), ys), As),
     2.9        As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
    2.10        transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
    2.11        |> mk_Frees "f" (map2 (curry op -->) As' Bs')
    2.12 @@ -778,7 +778,6 @@
    2.13        ||>> mk_Frees "h" (map2 (curry op -->) As' Ts)
    2.14        ||>> yield_singleton (mk_Frees "x") CA'
    2.15        ||>> yield_singleton (mk_Frees "y") CB'
    2.16 -      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs'
    2.17        ||>> mk_Frees "z" As'
    2.18        ||>> mk_Frees "y" Bs'
    2.19        ||>> mk_Frees "A" (map HOLogic.mk_setT As')
    2.20 @@ -1093,7 +1092,8 @@
    2.21  
    2.22          val map_wppull = Lazy.lazy mk_map_wppull;
    2.23  
    2.24 -        val rel_OO_Grps = no_refl [#rel_OO_Grp axioms];
    2.25 +        val rel_OO_Grp = #rel_OO_Grp axioms;
    2.26 +        val rel_OO_Grps = no_refl [rel_OO_Grp];
    2.27  
    2.28          fun mk_rel_Grp () =
    2.29            let
    2.30 @@ -1182,23 +1182,7 @@
    2.31  
    2.32          val rel_OO = Lazy.lazy mk_rel_OO;
    2.33  
    2.34 -        fun mk_in_rel () =
    2.35 -          let
    2.36 -            val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs';
    2.37 -            val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
    2.38 -            val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
    2.39 -            val map_fst_eq = HOLogic.mk_eq (map1 $ z, x);
    2.40 -            val map_snd_eq = HOLogic.mk_eq (map2 $ z, y);
    2.41 -            val lhs = Term.list_comb (rel, Rs) $ x $ y;
    2.42 -            val rhs =
    2.43 -              HOLogic.mk_exists (fst z', snd z', HOLogic.mk_conj (HOLogic.mk_mem (z, bnf_in),
    2.44 -                HOLogic.mk_conj (map_fst_eq, map_snd_eq)));
    2.45 -            val goal =
    2.46 -              fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
    2.47 -          in
    2.48 -            Goal.prove_sorry lthy [] [] goal (mk_in_rel_tac (the_single rel_OO_Grps))
    2.49 -            |> Thm.close_derivation
    2.50 -          end;
    2.51 +        fun mk_in_rel () = trans OF [rel_OO_Grp, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD};
    2.52  
    2.53          val in_rel = Lazy.lazy mk_in_rel;
    2.54  
     3.1 --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Sep 12 11:23:49 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Sep 12 11:23:49 2013 +0200
     3.3 @@ -21,7 +21,6 @@
     3.4    val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic
     3.5    val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
     3.6      {prems: thm list, context: Proof.context} -> tactic
     3.7 -  val mk_in_rel_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
     3.8    val mk_rel_conversep_tac: thm -> thm -> tactic
     3.9    val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
    3.10      {prems: thm list, context: Proof.context} -> tactic
    3.11 @@ -209,13 +208,6 @@
    3.12            rtac (map_comp0 RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
    3.13    end;
    3.14  
    3.15 -fun mk_in_rel_tac rel_OO_Gr {context = ctxt, prems = _} =
    3.16 -  EVERY' [rtac (rel_OO_Gr RS fun_cong RS fun_cong RS trans), rtac iffI,
    3.17 -    REPEAT_DETERM o eresolve_tac [@{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
    3.18 -    hyp_subst_tac ctxt, rtac exI, rtac conjI, atac, rtac conjI, rtac refl, rtac refl,
    3.19 -    REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI},
    3.20 -    etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1;
    3.21 -
    3.22  fun mk_rel_mono_strong_tac in_rel set_map0s {context = ctxt, prems = _} =
    3.23    if null set_map0s then atac 1
    3.24    else