# HG changeset patch
# User blanchet
# Date 1346756801 -7200
# Node ID 263b0e330d8bce0def42f68f524b61b97b97182c
# Parent  83515378d4d752cbeba084e2536ca704f6e5f464
more work on sugar + simplify Trueprop + eq idiom everywhere

diff -r 83515378d4d7 -r 263b0e330d8b src/HOL/Codatatype/Codatatype.thy
--- a/src/HOL/Codatatype/Codatatype.thy	Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Codatatype.thy	Tue Sep 04 13:06:41 2012 +0200
@@ -16,6 +16,7 @@
 and
   "codata" :: thy_decl
 uses
+  "Tools/bnf_fp_sugar_tactics.ML"
   "Tools/bnf_fp_sugar.ML"
 begin
 
diff -r 83515378d4d7 -r 263b0e330d8b src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Tue Sep 04 13:06:41 2012 +0200
@@ -223,9 +223,7 @@
         let
           val comp_in = mk_in Asets comp_sets CCA;
           val comp_in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
-          val goal =
-            fold_rev Logic.all Asets
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq (comp_in, comp_in_alt)));
+          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (comp_in, comp_in_alt));
         in
           Skip_Proof.prove lthy [] [] goal
             (fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms)
@@ -346,8 +344,7 @@
         let
           val killN_in = mk_in Asets killN_sets T;
           val killN_in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
-          val goal =
-            fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (killN_in, killN_in_alt)));
+          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (killN_in, killN_in_alt));
         in
           Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
         end;
@@ -455,8 +452,7 @@
         let
           val liftN_in = mk_in Asets liftN_sets T;
           val liftN_in_alt = mk_in (drop n Asets) bnf_sets T;
-          val goal =
-            fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (liftN_in, liftN_in_alt)))
+          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (liftN_in, liftN_in_alt));
         in
           Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
         end;
@@ -541,9 +537,7 @@
         let
           val permute_in = mk_in Asets permute_sets T;
           val permute_in_alt = mk_in (permute_rev Asets) bnf_sets T;
-          val goal =
-            fold_rev Logic.all Asets
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq (permute_in, permute_in_alt)));
+          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (permute_in, permute_in_alt));
         in
           Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
           |> Thm.close_derivation
diff -r 83515378d4d7 -r 263b0e330d8b src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 04 13:06:41 2012 +0200
@@ -721,8 +721,7 @@
           (Term.list_comb (bnf_map_BsCs, gs),
            Term.list_comb (bnf_map_AsBs, fs));
       in
-        fold_rev Logic.all (fs @ gs)
-          (HOLogic.mk_Trueprop (HOLogic.mk_eq (bnf_map_app_comp, comp_bnf_map_app)))
+        fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
       end;
 
     val goal_map_cong =
@@ -730,7 +729,7 @@
         fun mk_prem z set f f_copy =
           Logic.all z (Logic.mk_implies
             (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
-            HOLogic.mk_Trueprop (HOLogic.mk_eq (f $ z, f_copy $ z))));
+            mk_Trueprop_eq (f $ z, f_copy $ z)));
         val prems = map4 mk_prem zs bnf_sets_As fs fs_copy;
         val eq = HOLogic.mk_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
           Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
@@ -747,8 +746,7 @@
               HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs));
             val image_comp_set = HOLogic.mk_comp (mk_image f, setA);
           in
-            fold_rev Logic.all fs
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq (set_comp_map, image_comp_set)))
+            fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set))
           end;
       in
         map3 mk_goal bnf_sets_As bnf_sets_Bs fs
@@ -845,9 +843,7 @@
               (map2 (fn h => fn set => HOLogic.mk_comp (mk_image h, set)) hs bnf_sets_As)
               defT;
             (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
-            val goal =
-              fold_rev Logic.all hs
-                (HOLogic.mk_Trueprop (HOLogic.mk_eq (collect_map, image_collect)));
+            val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
           in
             Skip_Proof.prove lthy [] [] goal
               (fn {context = ctxt, ...} => mk_collect_set_natural_tac ctxt (#set_natural axioms))
@@ -990,8 +986,7 @@
           let
             val lhs = Term.list_comb (relAsBs, map2 mk_Gr As fs);
             val rhs = mk_Gr (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
-            val goal = fold_rev Logic.all (As @ fs)
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
+            val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
           in
             Skip_Proof.prove lthy [] [] goal
               (mk_rel_Gr_tac bnf_rel_def (#map_id axioms) (#map_cong axioms)
@@ -1052,7 +1047,7 @@
               (mk_rel_converse_le_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
                 (Lazy.force map_comp') (map Lazy.force set_natural'))
               |> Thm.close_derivation
-            val goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
+            val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
           in
             Skip_Proof.prove lthy [] [] goal (fn _ => mk_rel_converse_tac le_thm)
             |> Thm.close_derivation
@@ -1066,8 +1061,7 @@
             val relBsCs = mk_bnf_rel setRTsBsCs CB' CC';
             val lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_comp) Rs Ss);
             val rhs = mk_rel_comp (Term.list_comb (relAsBs, Rs), Term.list_comb (relBsCs, Ss));
-            val goal =
-              fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
+            val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
           in
             Skip_Proof.prove lthy [] [] goal
               (mk_rel_O_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
@@ -1089,7 +1083,7 @@
               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) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
+              fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
           in
             Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac bnf_rel_def (length bnf_sets))
             |> Thm.close_derivation
diff -r 83515378d4d7 -r 263b0e330d8b src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 13:06:41 2012 +0200
@@ -17,6 +17,7 @@
 open BNF_FP_Util
 open BNF_LFP
 open BNF_GFP
+open BNF_FP_Sugar_Tactics
 
 fun cannot_merge_types () = error "Mutually recursive (co)datatypes must have same type parameters";
 
@@ -142,10 +143,22 @@
         val phi = Proof_Context.export_morphism lthy lthy';
 
         val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
+        val ctrs = map (Morphism.term phi) raw_ctrs;
+        val caseof = Morphism.term phi raw_caseof;
 
-        val ctrs = map (Morphism.term phi) raw_ctrs;
-
-        val caseof = Morphism.term phi raw_caseof;
+        val fld_iff_unf_thm =
+          let
+            val fld = @{term "undefined::'a=>'b"};
+            val unf = @{term True};
+            val (T, T') = dest_funT (fastype_of fld);
+            val fld_unf = TrueI;
+            val unf_fld = TrueI;
+            val goal = @{term True};
+          in
+            Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+              mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [T, T']) (certify lthy fld)
+                (certify lthy unf) fld_unf unf_fld)
+          end;
 
         (* ### *)
         fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
diff -r 83515378d4d7 -r 263b0e330d8b src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 13:06:41 2012 +0200
@@ -0,0 +1,26 @@
+(*  Title:      HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012
+
+Tactics for the LFP/GFP sugar.
+*)
+
+signature BNF_FP_SUGAR_TACTICS =
+sig
+  val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
+    -> tactic
+end;
+
+structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
+struct
+
+open BNF_Util
+
+fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
+  (rtac iffI THEN'
+   EVERY' (map3 (fn cTs => fn cx => fn th =>
+     dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
+     SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
+     atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
+
+end;
diff -r 83515378d4d7 -r 263b0e330d8b src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 13:06:41 2012 +0200
@@ -237,7 +237,7 @@
           Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
       in
         Skip_Proof.prove lthy [] []
-          (fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
+          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
           (K (mk_map_comp_id_tac map_comp))
         |> Thm.close_derivation
       end;
@@ -252,8 +252,7 @@
           HOLogic.mk_Trueprop
             (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
         val prems = map4 mk_prem (drop m sets) self_fs zs zs';
-        val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x))
+        val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
       in
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
@@ -268,11 +267,10 @@
 
     val map_arg_cong_thms =
       let
-        val prems = map2 (fn x => fn y =>
-          HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))) xFs xFs_copy;
+        val prems = map2 (curry mk_Trueprop_eq) xFs xFs_copy;
         val maps = map (fn map => Term.list_comb (map, all_fs)) mapsAsBs;
-        val concls = map3 (fn x => fn y => fn map =>
-          HOLogic.mk_Trueprop (HOLogic.mk_eq (map $ x, map $ y))) xFs xFs_copy maps;
+        val concls =
+          map3 (fn x => fn y => fn map => mk_Trueprop_eq (map $ x, map $ y)) xFs xFs_copy maps;
         val goals =
           map4 (fn prem => fn concl => fn x => fn y =>
             fold_rev Logic.all (x :: y :: all_fs) (Logic.mk_implies (prem, concl)))
@@ -302,7 +300,7 @@
         val lhs = Term.list_comb (Free (coalg_name, coalgT), As @ Bs @ ss);
         val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
@@ -386,7 +384,7 @@
           (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
            Library.foldr1 HOLogic.mk_conj (map7 mk_mor Bs mapsAsBs fs ss s's zs zs'))
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
@@ -419,8 +417,7 @@
         fun mk_elim_goal B mapAsBs f s s' x =
           fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
             (Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
-              HOLogic.mk_Trueprop (HOLogic.mk_eq
-               (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)))));
+              mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x))));
         val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs;
         fun prove goal =
           Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def))
@@ -480,8 +477,7 @@
         val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
         val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
       in
-        Skip_Proof.prove lthy [] []
-          (fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
+        Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
           (K (mk_mor_UNIV_tac morE_thms mor_def))
         |> Thm.close_derivation
       end;
@@ -535,7 +531,7 @@
         val lhs = Term.list_comb (Free (hset_rec_name j, hsetT), ss);
         val rhs = mk_nat_rec Zero Suc;
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((hset_rec_frees, (_, hset_rec_def_frees)), (lthy, lthy_old)) =
@@ -586,7 +582,7 @@
         val rhs = mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
           (Term.absfree nat' (mk_hset_rec ss nat i j T $ z));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((hset_frees, (_, hset_def_frees)), (lthy, lthy_old)) =
@@ -767,8 +763,8 @@
 
         fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
 
-        fun mk_concl j T i f x = HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (mk_hset s's i j T $ (f $ x), mk_hset ss i j T $ x));
+        fun mk_concl j T i f x =
+          mk_Trueprop_eq (mk_hset s's i j T $ (f $ x), mk_hset ss i j T $ x);
 
         val goalss = map2 (fn j => fn T => map4 (fn i => fn f => fn x => fn B =>
           fold_rev Logic.all (x :: As @ Bs @ ss @ B's @ s's @ fs)
@@ -812,7 +808,7 @@
           (bis_le, Library.foldr1 HOLogic.mk_conj
             (map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
@@ -861,7 +857,7 @@
       in
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
-            (HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_bis As Bs ss B's s's Rs, rhs))))
+            (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
           (K (mk_bis_rel_tac m bis_def rel_defs map_comp's map_congs set_natural'ss))
         |> Thm.close_derivation
       end;
@@ -947,7 +943,7 @@
         val lhs = Term.list_comb (Free (lsbis_name i, mk_lsbisT RT), As @ Bs @ ss);
         val rhs = mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
@@ -1166,7 +1162,7 @@
           (Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
           map2 mk_subset passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
@@ -1221,7 +1217,7 @@
           (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
             HOLogic.mk_conj (isTree, mk_isNode As (HOLogic.mk_list sum_sbdT []) i))));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
@@ -1261,7 +1257,7 @@
         val rhs = HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
           (mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
@@ -1452,7 +1448,7 @@
         val lhs = Term.list_comb (Free (Lev_name, LevT), ss);
         val rhs = mk_nat_rec Zero Suc;
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
@@ -1498,7 +1494,7 @@
         val lhs = Term.list_comb (Free (rv_name, rvT), ss);
         val rhs = mk_list_rec Nil Cons;
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
@@ -1547,7 +1543,7 @@
         val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
           (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
@@ -1900,7 +1896,7 @@
           (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $
             (str $ (rep $ Jz)));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) =
@@ -1953,7 +1949,7 @@
         val lhs = Term.list_comb (Free (coiter_name i, coiterT), ss);
         val rhs = Term.absfree z' (abs $ (f $ z));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((coiter_frees, (_, coiter_def_frees)), (lthy, lthy_old)) =
@@ -2067,7 +2063,7 @@
         val lhs = Free (fld_name i, fldT);
         val rhs = mk_coiter Ts map_unfs i;
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
@@ -2090,8 +2086,7 @@
 
     val unf_o_fld_thms =
       let
-        fun mk_goal unf fld FT =
-          HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT));
+        fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT);
         val goals = map3 mk_goal unfs flds FTs;
       in
         map5 (fn goal => fn fld_def => fn coiter => fn map_comp_id => fn map_congL =>
@@ -2148,7 +2143,7 @@
         val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
         val rhs = HOLogic.mk_comp (mk_coiter Ts maps i, Inr_const T AT);
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
@@ -2176,7 +2171,7 @@
             val lhs = unf $ (mk_corec corec_ss i $ z);
             val rhs = Term.list_comb (corec_map, passive_ids @ sum_cases) $ (corec_s $ z);
           in
-            fold_rev Logic.all (z :: corec_ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
+            fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs))
           end;
         val goals = map5 mk_goal ks corec_ss corec_maps_rev unfs zs;
       in
@@ -2382,8 +2377,8 @@
         val (map_simp_thms, map_thms) =
           let
             fun mk_goal fs_map map unf unf' = fold_rev Logic.all fs
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf', fs_map),
-                HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf))));
+              (mk_Trueprop_eq (HOLogic.mk_comp (unf', fs_map),
+                HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf)));
             val goals = map4 mk_goal fs_maps map_FTFT's unfs unf's;
             val cTs = map (SOME o certifyT lthy) FTs';
             val maps =
@@ -2412,8 +2407,8 @@
         val (map_unique_thms, map_unique_thm) =
           let
             fun mk_prem u map unf unf' =
-              HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf', u),
-                HOLogic.mk_comp (Term.list_comb (map, fs @ us), unf)));
+              mk_Trueprop_eq (HOLogic.mk_comp (unf', u),
+                HOLogic.mk_comp (Term.list_comb (map, fs @ us), unf));
             val prems = map4 mk_prem us map_FTFT's unfs unf's;
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -2915,9 +2910,8 @@
         val Jrel_unfold_thms =
           let
             fun mk_goal Jz Jz' unf unf' JrelR relR = fold_rev Logic.all (Jz :: Jz' :: JRs)
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq
-                (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
-                  HOLogic.mk_mem (HOLogic.mk_prod (unf $ Jz, unf' $ Jz'), relR))));
+              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
+                  HOLogic.mk_mem (HOLogic.mk_prod (unf $ Jz, unf' $ Jz'), relR)));
             val goals = map6 mk_goal Jzs Jz's unfs unf's JrelRs relRs;
           in
             map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
@@ -2934,8 +2928,7 @@
         val Jpred_unfold_thms =
           let
             fun mk_goal Jz Jz' unf unf' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq
-                (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz'))));
+              (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz')));
             val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis;
           in
             map3 (fn goal => fn pred_def => fn Jrel_unfold =>
diff -r 83515378d4d7 -r 263b0e330d8b src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 13:06:41 2012 +0200
@@ -170,7 +170,7 @@
           take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
       in
         Skip_Proof.prove lthy [] []
-          (fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
+          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
           (K (mk_map_comp_id_tac map_comp))
         |> Thm.close_derivation
       end;
@@ -184,8 +184,7 @@
         fun mk_prem set f z z' = HOLogic.mk_Trueprop
           (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
         val prems = map4 mk_prem (drop m sets) self_fs zs zs';
-        val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x))
+        val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
       in
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
@@ -217,7 +216,7 @@
         val lhs = Term.list_comb (Free (alg_name, algT), As @ Bs @ ss);
         val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
@@ -312,7 +311,7 @@
           Library.foldr1 HOLogic.mk_conj
             (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
@@ -345,8 +344,7 @@
         fun mk_elim_goal sets mapAsBs f s s' x T =
           fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
             (Logic.list_implies ([prem, mk_elim_prem sets x T],
-              HOLogic.mk_Trueprop (HOLogic.mk_eq (f $ (s $ x),
-                s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x])))));
+              mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x]))));
         val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
         fun prove goal =
           Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
@@ -445,8 +443,7 @@
         val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
         val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
       in
-        Skip_Proof.prove lthy [] []
-          (fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
+        Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
           (K (mk_mor_UNIV_tac m morE_thms mor_def))
         |> Thm.close_derivation
       end;
@@ -472,9 +469,9 @@
         val prems = map HOLogic.mk_Trueprop
          [mk_alg passive_UNIVs Bs ss,
          mk_alg passive_UNIVs B's s's]
-        val concl = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_iso Bs ss B's s's fs inv_fs,
+        val concl = mk_Trueprop_eq (mk_iso Bs ss B's s's fs inv_fs,
           HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
-            Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's))));
+            Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
       in
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs) (Logic.list_implies (prems, concl)))
@@ -698,7 +695,7 @@
         val rhs = mk_UNION (field_suc_bd)
           (Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
@@ -818,7 +815,7 @@
         val lhs = Term.list_comb (Free (str_init_name i, str_initT), [init_xF, iidx]);
         val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF);
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
@@ -1006,7 +1003,7 @@
         val rhs = Term.absfree x' (abs $ (str $
           (Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x)));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
@@ -1066,7 +1063,7 @@
         val lhs = Term.list_comb (Free (iter_name i, iterT), ss);
         val rhs = mk_nthN n iter i;
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((iter_frees, (_, iter_def_frees)), (lthy, lthy_old)) =
@@ -1151,7 +1148,7 @@
         val lhs = Free (unf_name i, unfT);
         val rhs = mk_iter Ts map_flds i;
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) =
@@ -1174,8 +1171,7 @@
 
     val unf_o_fld_thms =
       let
-        fun mk_goal unf fld FT =
-          HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT));
+        fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT);
         val goals = map3 mk_goal unfs flds FTs;
       in
         map5 (fn goal => fn unf_def => fn iter => fn map_comp_id => fn map_congL =>
@@ -1228,7 +1224,7 @@
         val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss);
         val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_iter Ts maps i);
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
@@ -1255,7 +1251,7 @@
             val lhs = mk_rec rec_ss i $ (fld $ x);
             val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x);
           in
-            fold_rev Logic.all (x :: rec_ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
+            fold_rev Logic.all (x :: rec_ss) (mk_Trueprop_eq (lhs, rhs))
           end;
         val goals = map5 mk_goal ks rec_ss rec_maps_rev flds xFs;
       in
@@ -1400,8 +1396,8 @@
         val (map_simp_thms, map_thms) =
           let
             fun mk_goal fs_map map fld fld' = fold_rev Logic.all fs
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (fs_map, fld),
-                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps)))));
+              (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, fld),
+                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps))));
             val goals = map4 mk_goal fs_maps map_FTFT's flds fld's;
             val maps =
               map4 (fn goal => fn iter => fn map_comp_id => fn map_cong =>
@@ -1415,8 +1411,8 @@
         val (map_unique_thms, map_unique_thm) =
           let
             fun mk_prem u map fld fld' =
-              HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (u, fld),
-                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ us))));
+              mk_Trueprop_eq (HOLogic.mk_comp (u, fld),
+                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ us)));
             val prems = map4 mk_prem us map_FTFT's flds fld's;
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -1460,8 +1456,8 @@
         val (set_simp_thmss, set_thmss) =
           let
             fun mk_goal sets fld set col map =
-              HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (set, fld),
-                HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets))));
+              mk_Trueprop_eq (HOLogic.mk_comp (set, fld),
+                HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
             val goalss =
               map3 (fn sets => map4 (mk_goal sets) flds sets) setss_by_range colss map_setss;
             val setss = map (map2 (fn iter => fn goal =>
@@ -1469,9 +1465,9 @@
               iter_thms) goalss;
 
             fun mk_simp_goal pas_set act_sets sets fld z set =
-              Logic.all z (HOLogic.mk_Trueprop (HOLogic.mk_eq (set $ (fld $ z),
+              Logic.all z (mk_Trueprop_eq (set $ (fld $ z),
                 mk_union (pas_set $ z,
-                  Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)))));
+                  Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))));
             val simp_goalss =
               map2 (fn i => fn sets =>
                 map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
@@ -1743,9 +1739,8 @@
         val Irel_unfold_thms =
           let
             fun mk_goal xF yF fld fld' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs)
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq
-                (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
-                  HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR))));
+              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
+                  HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR)));
             val goals = map6 mk_goal xFs yFs flds fld's IrelRs relRs;
           in
             map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
@@ -1762,8 +1757,7 @@
         val Ipred_unfold_thms =
           let
             fun mk_goal xF yF fld fld' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq
-                (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF)));
+              (mk_Trueprop_eq (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF));
             val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis;
           in
             map3 (fn goal => fn pred_def => fn Irel_unfold =>
diff -r 83515378d4d7 -r 263b0e330d8b src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Tue Sep 04 13:06:41 2012 +0200
@@ -69,6 +69,7 @@
   val mk_Card_order: term -> term
   val mk_Field: term -> term
   val mk_Gr: term -> term -> term
+  val mk_Trueprop_eq: term * term -> term
   val mk_UNION: term -> term -> term
   val mk_Union: typ -> term
   val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term
@@ -302,6 +303,8 @@
 
 (** Operators **)
 
+val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
+
 fun mk_converse R =
   let
     val RT = dest_relT (fastype_of R);
diff -r 83515378d4d7 -r 263b0e330d8b src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:05:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:06:41 2012 +0200
@@ -51,8 +51,6 @@
 
 fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
 
-val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
-
 fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
 
 fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs;