# HG changeset patch
# User desharna
# Date 1405585712 -7200
# Node ID d554b0097ad4d7d1fbf651fd5787cf5a5a6496fe
# Parent  0fb191472e4a85e6cf0c5286c0a9e736aa31cbda
add mk_Trueprop_mem utility function

diff -r 0fb191472e4a -r d554b0097ad4 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Jul 17 10:28:32 2014 +0200
@@ -223,7 +223,7 @@
           val bd' = @{term natLeq};
           val bd_bd' = HOLogic.mk_prod (bd, bd');
           val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
-          val goal = HOLogic.mk_Trueprop (HOLogic.mk_mem (bd_bd', ordIso));
+          val goal = mk_Trueprop_mem (bd_bd', ordIso);
         in
           (bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac)
             |> Thm.close_derivation))
@@ -811,7 +811,7 @@
 
           val Abs_bdT_inj = mk_Abs_inj_thm Abs_bdT_inject;
           val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj Abs_bdT_cases;
-      
+
           val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
           val bd_card_order =
             @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
@@ -862,7 +862,7 @@
       (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
 
     val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds));
-    
+
     val map_def = map_def_of_bnf bnf'';
     val set_defs = set_defs_of_bnf bnf'';
     val rel_def = rel_def_of_bnf bnf'';
diff -r 0fb191472e4a -r d554b0097ad4 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Jul 17 10:28:32 2014 +0200
@@ -981,8 +981,7 @@
 
     fun mk_map_cong_prem x z set f f_copy =
       Logic.all z (Logic.mk_implies
-        (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
-        mk_Trueprop_eq (f $ z, f_copy $ z)));
+        (mk_Trueprop_mem (z, set $ x), mk_Trueprop_eq (f $ z, f_copy $ z)));
 
     val map_cong0_goal =
       let
@@ -1044,7 +1043,7 @@
               else @{term False});
           in
             fold_rev Logic.all (z :: xs)
-              (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set_wit)), concl))
+              (Logic.mk_implies (mk_Trueprop_mem (z, set_wit), concl))
           end;
       in
         map wit_goal (0 upto live - 1)
diff -r 0fb191472e4a -r d554b0097ad4 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 17 10:28:32 2014 +0200
@@ -574,7 +574,7 @@
 
         fun mk_prem_prem xs (xysets, (j, x)) =
           close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
-              HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
+              mk_Trueprop_mem (y, set $ x')) xysets,
             HOLogic.mk_Trueprop (nth ps (j - 1) $ x)));
 
         fun mk_raw_prem phi ctr ctr_Ts ctrXs_Ts =
@@ -1564,7 +1564,7 @@
                                     let
                                       val X = HOLogic.dest_setT (range_type (fastype_of set));
                                       val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt;
-                                      val assm = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ a));
+                                      val assm = mk_Trueprop_mem (x, set $ a);
                                     in
                                       travese_nested_types x ctxt'
                                       |>> map (Logic.mk_implies o pair assm)
@@ -1575,13 +1575,13 @@
                                 end)
                             | T =>
                               if T = A then
-                                ([HOLogic.mk_Trueprop (HOLogic.mk_mem (t, setA $ ta))], ctxt)
+                                ([mk_Trueprop_mem (t, setA $ ta)], ctxt)
                               else
                                 ([], ctxt));
 
                           val (concls, ctxt') =
                             if sel_rangeT = A then
-                              ([HOLogic.mk_Trueprop (HOLogic.mk_mem (selA $ ta, setA $ ta))], ctxt)
+                              ([mk_Trueprop_mem (selA $ ta, setA $ ta)], ctxt)
                             else
                               travese_nested_types (selA $ ta) names_lthy;
                         in
diff -r 0fb191472e4a -r d554b0097ad4 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jul 17 10:28:32 2014 +0200
@@ -326,7 +326,7 @@
     val coalg_set_thmss =
       let
         val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
-        fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
+        fun mk_prem x B = mk_Trueprop_mem (x, B);
         fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B);
         val prems = map2 mk_prem zs Bs;
         val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
@@ -405,7 +405,7 @@
           Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2));
         val image_goals = map3 mk_image_goal fs Bs B's;
         fun mk_elim_goal B mapAsBs f s s' x =
-          Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
+          Logic.list_implies ([prem, mk_Trueprop_mem (x, B)],
             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 =
@@ -1092,8 +1092,8 @@
         val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks;
 
         fun mk_goal i z = Logic.mk_implies
-            (HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z)),
-            HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z)));
+            (mk_Trueprop_mem (kl, mk_Lev ss nat i $ z),
+            mk_Trueprop_mem (kl, mk_Lev ss (mk_size kl) i $ z));
         val goals = map2 mk_goal ks zs;
 
         val length_Levs' = map2 (fn goal => fn length_Lev =>
@@ -1651,7 +1651,7 @@
       ||>> mk_Frees "JR" activeJphiTs;
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
 
-    fun mk_Jrel_DEADID_coinduct_thm () = 
+    fun mk_Jrel_DEADID_coinduct_thm () =
       mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
         Jzs Jz's dtors dtor's (fn {context = ctxt, prems} =>
           (unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
@@ -1697,10 +1697,10 @@
         val set_bss =
           map (flat o map2 (fn B => fn b =>
             if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0;
-    
+
         fun col_bind j = mk_internal_b (colN ^ (if m = 1 then "" else string_of_int j));
         val col_def_bind = rpair [] o Thm.def_binding o col_bind;
-    
+
         fun col_spec j Zero hrec hrec' =
           let
             fun mk_Suc dtor sets z z' =
@@ -1711,13 +1711,13 @@
                 Term.absfree z'
                   (mk_union (set $ (dtor $ z), Library.foldl1 mk_union (map2 mk_UN sets ks)))
               end;
-    
+
             val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec'
               (HOLogic.mk_tuple (map4 mk_Suc dtors FTs_setss Jzs Jzs')));
           in
             mk_rec_nat Zero Suc
           end;
-    
+
         val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) =
           lthy
           |> fold_map4 (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define
@@ -1725,12 +1725,12 @@
             ls Zeros hrecs hrecs'
           |>> apsnd split_list o split_list
           ||> `Local_Theory.restore;
-    
+
         val phi = Proof_Context.export_morphism lthy_old lthy;
-    
+
         val col_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) col_def_frees;
         val cols = map (fst o Term.dest_Const o Morphism.term phi) col_frees;
-    
+
         fun mk_col Ts nat i j T =
           let
             val hrecT = HOLogic.mk_tupleT (map (fn U => U --> HOLogic.mk_setT T) Ts)
@@ -1738,12 +1738,12 @@
           in
             mk_nthN n (Term.list_comb (Const (nth cols (j - 1), colT), [nat])) i
           end;
-    
+
         val col_0ss = mk_rec_simps n @{thm rec_nat_0_imp} col_defs;
         val col_Sucss = mk_rec_simps n @{thm rec_nat_Suc_imp} col_defs;
         val col_0ss' = transpose col_0ss;
         val col_Sucss' = transpose col_Sucss;
-    
+
         fun mk_set Ts i j T =
           Abs (Name.uu, nth Ts (i - 1), mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
             (Term.absfree nat' (mk_col Ts nat i j T $ Bound 1)));
@@ -1835,28 +1835,28 @@
           let
             fun mk_passive_prem set dtor x K =
               Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (K $ x)));
-    
+
             fun mk_active_prem dtor x1 K1 set x2 K2 =
               fold_rev Logic.all [x1, x2]
-                (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (dtor $ x1))),
+                (Logic.mk_implies (mk_Trueprop_mem (x2, set $ (dtor $ x1)),
                   HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
-    
+
             val premss = map2 (fn j => fn Ks =>
               map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @
                 flat (map4 (fn sets => fn s => fn x1 => fn K1 =>
                   map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks))
               ls Kss;
-    
+
             val col_minimal_thms =
               let
                 fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x);
                 fun mk_concl j T Ks = list_all_free Jzs
                   (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs));
                 val concls = map3 mk_concl ls passiveAs Kss;
-    
+
                 val goals = map2 (fn prems => fn concl =>
                   Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
-    
+
                 val ctss =
                   map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
               in
@@ -1868,11 +1868,11 @@
                   |> singleton (Proof_Context.export names_lthy lthy))
                 goals ctss col_0ss' col_Sucss'
               end;
-    
+
             fun mk_conjunct set K x = mk_leq (set $ x) (K $ x);
             fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct sets Ks Jzs);
             val concls = map2 mk_concl Jsetss_by_range Kss;
-    
+
             val goals = map2 (fn prems => fn concl =>
               Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls;
           in
@@ -1889,16 +1889,16 @@
           let
             fun mk_set_incl_Jset dtor x set Jset =
               HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (Jset $ x));
-    
+
             fun mk_set_Jset_incl_Jset dtor x y set Jset1 Jset2 =
-              Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))),
+              Logic.mk_implies (mk_Trueprop_mem (x, set $ (dtor $ y)),
                 HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y)));
-    
+
             val set_incl_Jset_goalss =
               map4 (fn dtor => fn x => fn sets => fn Jsets =>
                 map2 (mk_set_incl_Jset dtor x) (take m sets) Jsets)
               dtors Jzs FTs_setss Jsetss_by_bnf;
-    
+
             (*x(k) : F(i)set(m+k) (dtor(i) y(i)) ==> J(k)set(j) x(k) <= J(i)set(j) y(i)*)
             val set_Jset_incl_Jset_goalsss =
               map4 (fn dtori => fn yi => fn sets => fn Jsetsi =>
@@ -1928,7 +1928,7 @@
               ks goalss)
             set_Jset_incl_Jset_goalsss col_Sucss)
           end;
-    
+
         val set_incl_Jset_thmss' = transpose dtor_Jset_incl_thmss;
         val set_Jset_incl_Jset_thmsss' = transpose (map transpose dtor_set_Jset_incl_thmsss);
         val set_Jset_thmss = map (map (fn thm => thm RS @{thm set_mp})) dtor_Jset_incl_thmss;
@@ -1936,14 +1936,14 @@
           dtor_set_Jset_incl_thmsss;
         val set_Jset_thmss' = transpose set_Jset_thmss;
         val set_Jset_Jset_thmsss' = transpose (map transpose set_Jset_Jset_thmsss);
-    
+
         val dtor_Jset_induct_thms =
           let
             val incls =
               maps (map (fn thm => thm RS @{thm subset_Collect_iff})) dtor_Jset_incl_thmss @
                 @{thms subset_Collect_iff[OF subset_refl]};
 
-            val cTs = map (SOME o certifyT lthy) params';    
+            val cTs = map (SOME o certifyT lthy) params';
             fun mk_induct_tinst phis jsets y y' =
               map4 (fn phi => fn jset => fn Jz => fn Jz' =>
                 SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
@@ -1985,7 +1985,7 @@
               le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss');
 
             val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap));
-            val set_ge_thmss = 
+            val set_ge_thmss =
               map3 (map3 (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
                 Goal.prove_sorry lthy [] [] goal
                   (K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets))
@@ -2225,7 +2225,7 @@
             abs' helper_ind_phiss;
           fun mk_helper_ind_concl ab' z ind_phi set =
             mk_Ball (set $ z) (Term.absfree ab' ind_phi);
-  
+
           val mk_helper_ind_concls =
             map3 (fn ab' => fn ind_phis => fn zip_sets =>
               map3 (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets)
diff -r 0fb191472e4a -r d554b0097ad4 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Jul 17 10:28:32 2014 +0200
@@ -272,7 +272,7 @@
       let
         val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B);
-        fun mk_concl s x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (s $ x, B));
+        fun mk_concl s x B = mk_Trueprop_mem (s $ x, B);
         val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs;
         val concls = map3 mk_concl ss xFs Bs;
         val goals = map2 (fn prems => fn concl =>
@@ -790,7 +790,7 @@
 
     val mor_select_thm =
       let
-        val i_prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (iidx, II));
+        val i_prem = mk_Trueprop_mem (iidx, II);
         val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss active_UNIVs ss Asuc_fs);
         val prems = [i_prem, mor_prem];
         val concl = HOLogic.mk_Trueprop
@@ -1208,7 +1208,7 @@
           let
             fun mk_IH phi set z =
               let
-                val prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x));
+                val prem = mk_Trueprop_mem (z, set $ x);
                 val concl = HOLogic.mk_Trueprop (phi $ z);
               in
                 Logic.all z (Logic.mk_implies (prem, concl))
@@ -1247,8 +1247,8 @@
           let
             fun mk_IH phi set set' z1 z2 =
               let
-                val prem1 = HOLogic.mk_Trueprop (HOLogic.mk_mem (z1, (set $ x)));
-                val prem2 = HOLogic.mk_Trueprop (HOLogic.mk_mem (z2, (set' $ y)));
+                val prem1 = mk_Trueprop_mem (z1, (set $ x));
+                val prem2 = mk_Trueprop_mem (z2, (set' $ y));
                 val concl = HOLogic.mk_Trueprop (phi $ z1 $ z2);
               in
                 fold_rev Logic.all [z1, z2] (Logic.list_implies ([prem1, prem2], concl))
@@ -1383,44 +1383,44 @@
               val (sum_bd0T_params, sum_bd0T_params') = `(map TFree) (Term.add_tfreesT sum_bd0T []);
 
               val sbd0T_bind = mk_internal_b (sum_bdTN ^ "0");
-    
+
               val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) =
                 typedef (sbd0T_bind, sum_bd0T_params', NoSyn)
                   (HOLogic.mk_UNIV sum_bd0T) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
-    
+
               val sbd0T = Type (sbd0T_name, sum_bd0T_params);
               val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T);
-    
+
               val sbd0_bind = mk_internal_b (sum_bdN ^ "0");
               val sbd0_def_bind = (Thm.def_binding sbd0_bind, []);
-    
+
               val sbd0_spec = mk_dir_image sum_bd0 Abs_sbd0T;
-    
+
               val ((sbd0_free, (_, sbd0_def_free)), (lthy, lthy_old)) =
                 lthy
                 |> Local_Theory.define ((sbd0_bind, NoSyn), (sbd0_def_bind, sbd0_spec))
                 ||> `Local_Theory.restore;
-    
+
               val phi = Proof_Context.export_morphism lthy_old lthy;
-    
+
               val sbd0_def = Morphism.thm phi sbd0_def_free RS meta_eq_to_obj_eq;
               val sbd0 = Const (fst (Term.dest_Const (Morphism.term phi sbd0_free)),
                 mk_relT (`I sbd0T));
-    
+
               val Abs_sbd0T_inj = mk_Abs_inj_thm (#Abs_inject sbd0T_loc_info);
               val Abs_sbd0T_bij = mk_Abs_bij_thm lthy Abs_sbd0T_inj (#Abs_cases sbd0T_loc_info);
-    
+
               val sum_Cinfinite = mk_sum_Cinfinite bd0_Cinfinites;
               val sum_Card_order = sum_Cinfinite RS conjunct2;
               val sum_card_order = mk_sum_card_order bd0_card_orders;
-    
+
               val sbd0_ordIso = @{thm ssubst_Pair_rhs} OF
                 [@{thm dir_image} OF [Abs_sbd0T_inj, sum_Card_order], sbd0_def];
               val sbd0_Cinfinite = @{thm Cinfinite_cong} OF [sbd0_ordIso, sum_Cinfinite];
-    
+
               val sbd0_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF
                 [sbd0_def, @{thm card_order_dir_image} OF [Abs_sbd0T_bij, sum_card_order]];
-    
+
               fun mk_set_sbd0 i bd0_Card_order bd0s =
                 map (fn thm => @{thm ordLeq_ordIso_trans} OF
                   [bd0_Card_order RS mk_ordLeq_csum n i thm, sbd0_ordIso]) bd0s;
diff -r 0fb191472e4a -r d554b0097ad4 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Jul 16 17:57:27 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jul 17 10:28:32 2014 +0200
@@ -53,6 +53,7 @@
 
   val mk_IfN: typ -> term list -> term list -> term
   val mk_Trueprop_eq: term * term -> term
+  val mk_Trueprop_mem: term * term -> term
 
   val rapp: term -> term -> term
 
@@ -201,6 +202,7 @@
     Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts;
 
 val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
+val mk_Trueprop_mem = HOLogic.mk_Trueprop o HOLogic.mk_mem;
 
 fun rapp u t = betapply (t, u);