src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49123 263b0e330d8b
parent 49121 9e0acaa470ab
child 49124 968e1b7de057
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 13:05:07 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 13:06:41 2012 +0200
     1.3 @@ -237,7 +237,7 @@
     1.4            Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
     1.5        in
     1.6          Skip_Proof.prove lthy [] []
     1.7 -          (fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
     1.8 +          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
     1.9            (K (mk_map_comp_id_tac map_comp))
    1.10          |> Thm.close_derivation
    1.11        end;
    1.12 @@ -252,8 +252,7 @@
    1.13            HOLogic.mk_Trueprop
    1.14              (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
    1.15          val prems = map4 mk_prem (drop m sets) self_fs zs zs';
    1.16 -        val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.17 -         (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x))
    1.18 +        val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
    1.19        in
    1.20          Skip_Proof.prove lthy [] []
    1.21            (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
    1.22 @@ -268,11 +267,10 @@
    1.23  
    1.24      val map_arg_cong_thms =
    1.25        let
    1.26 -        val prems = map2 (fn x => fn y =>
    1.27 -          HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))) xFs xFs_copy;
    1.28 +        val prems = map2 (curry mk_Trueprop_eq) xFs xFs_copy;
    1.29          val maps = map (fn map => Term.list_comb (map, all_fs)) mapsAsBs;
    1.30 -        val concls = map3 (fn x => fn y => fn map =>
    1.31 -          HOLogic.mk_Trueprop (HOLogic.mk_eq (map $ x, map $ y))) xFs xFs_copy maps;
    1.32 +        val concls =
    1.33 +          map3 (fn x => fn y => fn map => mk_Trueprop_eq (map $ x, map $ y)) xFs xFs_copy maps;
    1.34          val goals =
    1.35            map4 (fn prem => fn concl => fn x => fn y =>
    1.36              fold_rev Logic.all (x :: y :: all_fs) (Logic.mk_implies (prem, concl)))
    1.37 @@ -302,7 +300,7 @@
    1.38          val lhs = Term.list_comb (Free (coalg_name, coalgT), As @ Bs @ ss);
    1.39          val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
    1.40        in
    1.41 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    1.42 +        mk_Trueprop_eq (lhs, rhs)
    1.43        end;
    1.44  
    1.45      val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
    1.46 @@ -386,7 +384,7 @@
    1.47            (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
    1.48             Library.foldr1 HOLogic.mk_conj (map7 mk_mor Bs mapsAsBs fs ss s's zs zs'))
    1.49        in
    1.50 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    1.51 +        mk_Trueprop_eq (lhs, rhs)
    1.52        end;
    1.53  
    1.54      val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
    1.55 @@ -419,8 +417,7 @@
    1.56          fun mk_elim_goal B mapAsBs f s s' x =
    1.57            fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
    1.58              (Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
    1.59 -              HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.60 -               (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)))));
    1.61 +              mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x))));
    1.62          val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs;
    1.63          fun prove goal =
    1.64            Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def))
    1.65 @@ -480,8 +477,7 @@
    1.66          val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
    1.67          val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
    1.68        in
    1.69 -        Skip_Proof.prove lthy [] []
    1.70 -          (fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
    1.71 +        Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
    1.72            (K (mk_mor_UNIV_tac morE_thms mor_def))
    1.73          |> Thm.close_derivation
    1.74        end;
    1.75 @@ -535,7 +531,7 @@
    1.76          val lhs = Term.list_comb (Free (hset_rec_name j, hsetT), ss);
    1.77          val rhs = mk_nat_rec Zero Suc;
    1.78        in
    1.79 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    1.80 +        mk_Trueprop_eq (lhs, rhs)
    1.81        end;
    1.82  
    1.83      val ((hset_rec_frees, (_, hset_rec_def_frees)), (lthy, lthy_old)) =
    1.84 @@ -586,7 +582,7 @@
    1.85          val rhs = mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
    1.86            (Term.absfree nat' (mk_hset_rec ss nat i j T $ z));
    1.87        in
    1.88 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    1.89 +        mk_Trueprop_eq (lhs, rhs)
    1.90        end;
    1.91  
    1.92      val ((hset_frees, (_, hset_def_frees)), (lthy, lthy_old)) =
    1.93 @@ -767,8 +763,8 @@
    1.94  
    1.95          fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
    1.96  
    1.97 -        fun mk_concl j T i f x = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.98 -          (mk_hset s's i j T $ (f $ x), mk_hset ss i j T $ x));
    1.99 +        fun mk_concl j T i f x =
   1.100 +          mk_Trueprop_eq (mk_hset s's i j T $ (f $ x), mk_hset ss i j T $ x);
   1.101  
   1.102          val goalss = map2 (fn j => fn T => map4 (fn i => fn f => fn x => fn B =>
   1.103            fold_rev Logic.all (x :: As @ Bs @ ss @ B's @ s's @ fs)
   1.104 @@ -812,7 +808,7 @@
   1.105            (bis_le, Library.foldr1 HOLogic.mk_conj
   1.106              (map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
   1.107        in
   1.108 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.109 +        mk_Trueprop_eq (lhs, rhs)
   1.110        end;
   1.111  
   1.112      val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
   1.113 @@ -861,7 +857,7 @@
   1.114        in
   1.115          Skip_Proof.prove lthy [] []
   1.116            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
   1.117 -            (HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_bis As Bs ss B's s's Rs, rhs))))
   1.118 +            (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
   1.119            (K (mk_bis_rel_tac m bis_def rel_defs map_comp's map_congs set_natural'ss))
   1.120          |> Thm.close_derivation
   1.121        end;
   1.122 @@ -947,7 +943,7 @@
   1.123          val lhs = Term.list_comb (Free (lsbis_name i, mk_lsbisT RT), As @ Bs @ ss);
   1.124          val rhs = mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i));
   1.125        in
   1.126 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.127 +        mk_Trueprop_eq (lhs, rhs)
   1.128        end;
   1.129  
   1.130      val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
   1.131 @@ -1166,7 +1162,7 @@
   1.132            (Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
   1.133            map2 mk_subset passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
   1.134        in
   1.135 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.136 +        mk_Trueprop_eq (lhs, rhs)
   1.137        end;
   1.138  
   1.139      val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
   1.140 @@ -1221,7 +1217,7 @@
   1.141            (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
   1.142              HOLogic.mk_conj (isTree, mk_isNode As (HOLogic.mk_list sum_sbdT []) i))));
   1.143        in
   1.144 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.145 +        mk_Trueprop_eq (lhs, rhs)
   1.146        end;
   1.147  
   1.148      val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
   1.149 @@ -1261,7 +1257,7 @@
   1.150          val rhs = HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
   1.151            (mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))));
   1.152        in
   1.153 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.154 +        mk_Trueprop_eq (lhs, rhs)
   1.155        end;
   1.156  
   1.157      val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
   1.158 @@ -1452,7 +1448,7 @@
   1.159          val lhs = Term.list_comb (Free (Lev_name, LevT), ss);
   1.160          val rhs = mk_nat_rec Zero Suc;
   1.161        in
   1.162 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.163 +        mk_Trueprop_eq (lhs, rhs)
   1.164        end;
   1.165  
   1.166      val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
   1.167 @@ -1498,7 +1494,7 @@
   1.168          val lhs = Term.list_comb (Free (rv_name, rvT), ss);
   1.169          val rhs = mk_list_rec Nil Cons;
   1.170        in
   1.171 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.172 +        mk_Trueprop_eq (lhs, rhs)
   1.173        end;
   1.174  
   1.175      val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
   1.176 @@ -1547,7 +1543,7 @@
   1.177          val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
   1.178            (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
   1.179        in
   1.180 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.181 +        mk_Trueprop_eq (lhs, rhs)
   1.182        end;
   1.183  
   1.184      val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
   1.185 @@ -1900,7 +1896,7 @@
   1.186            (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $
   1.187              (str $ (rep $ Jz)));
   1.188        in
   1.189 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.190 +        mk_Trueprop_eq (lhs, rhs)
   1.191        end;
   1.192  
   1.193      val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) =
   1.194 @@ -1953,7 +1949,7 @@
   1.195          val lhs = Term.list_comb (Free (coiter_name i, coiterT), ss);
   1.196          val rhs = Term.absfree z' (abs $ (f $ z));
   1.197        in
   1.198 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.199 +        mk_Trueprop_eq (lhs, rhs)
   1.200        end;
   1.201  
   1.202      val ((coiter_frees, (_, coiter_def_frees)), (lthy, lthy_old)) =
   1.203 @@ -2067,7 +2063,7 @@
   1.204          val lhs = Free (fld_name i, fldT);
   1.205          val rhs = mk_coiter Ts map_unfs i;
   1.206        in
   1.207 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.208 +        mk_Trueprop_eq (lhs, rhs)
   1.209        end;
   1.210  
   1.211      val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
   1.212 @@ -2090,8 +2086,7 @@
   1.213  
   1.214      val unf_o_fld_thms =
   1.215        let
   1.216 -        fun mk_goal unf fld FT =
   1.217 -          HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT));
   1.218 +        fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT);
   1.219          val goals = map3 mk_goal unfs flds FTs;
   1.220        in
   1.221          map5 (fn goal => fn fld_def => fn coiter => fn map_comp_id => fn map_congL =>
   1.222 @@ -2148,7 +2143,7 @@
   1.223          val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
   1.224          val rhs = HOLogic.mk_comp (mk_coiter Ts maps i, Inr_const T AT);
   1.225        in
   1.226 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.227 +        mk_Trueprop_eq (lhs, rhs)
   1.228        end;
   1.229  
   1.230      val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
   1.231 @@ -2176,7 +2171,7 @@
   1.232              val lhs = unf $ (mk_corec corec_ss i $ z);
   1.233              val rhs = Term.list_comb (corec_map, passive_ids @ sum_cases) $ (corec_s $ z);
   1.234            in
   1.235 -            fold_rev Logic.all (z :: corec_ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
   1.236 +            fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs))
   1.237            end;
   1.238          val goals = map5 mk_goal ks corec_ss corec_maps_rev unfs zs;
   1.239        in
   1.240 @@ -2382,8 +2377,8 @@
   1.241          val (map_simp_thms, map_thms) =
   1.242            let
   1.243              fun mk_goal fs_map map unf unf' = fold_rev Logic.all fs
   1.244 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf', fs_map),
   1.245 -                HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf))));
   1.246 +              (mk_Trueprop_eq (HOLogic.mk_comp (unf', fs_map),
   1.247 +                HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf)));
   1.248              val goals = map4 mk_goal fs_maps map_FTFT's unfs unf's;
   1.249              val cTs = map (SOME o certifyT lthy) FTs';
   1.250              val maps =
   1.251 @@ -2412,8 +2407,8 @@
   1.252          val (map_unique_thms, map_unique_thm) =
   1.253            let
   1.254              fun mk_prem u map unf unf' =
   1.255 -              HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf', u),
   1.256 -                HOLogic.mk_comp (Term.list_comb (map, fs @ us), unf)));
   1.257 +              mk_Trueprop_eq (HOLogic.mk_comp (unf', u),
   1.258 +                HOLogic.mk_comp (Term.list_comb (map, fs @ us), unf));
   1.259              val prems = map4 mk_prem us map_FTFT's unfs unf's;
   1.260              val goal =
   1.261                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   1.262 @@ -2915,9 +2910,8 @@
   1.263          val Jrel_unfold_thms =
   1.264            let
   1.265              fun mk_goal Jz Jz' unf unf' JrelR relR = fold_rev Logic.all (Jz :: Jz' :: JRs)
   1.266 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.267 -                (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
   1.268 -                  HOLogic.mk_mem (HOLogic.mk_prod (unf $ Jz, unf' $ Jz'), relR))));
   1.269 +              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
   1.270 +                  HOLogic.mk_mem (HOLogic.mk_prod (unf $ Jz, unf' $ Jz'), relR)));
   1.271              val goals = map6 mk_goal Jzs Jz's unfs unf's JrelRs relRs;
   1.272            in
   1.273              map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
   1.274 @@ -2934,8 +2928,7 @@
   1.275          val Jpred_unfold_thms =
   1.276            let
   1.277              fun mk_goal Jz Jz' unf unf' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
   1.278 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.279 -                (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz'))));
   1.280 +              (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz')));
   1.281              val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis;
   1.282            in
   1.283              map3 (fn goal => fn pred_def => fn Jrel_unfold =>