src/HOL/BNF/Tools/bnf_lfp.ML

       end;
 
     val alg_set_thms =
       let
         val alg_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
-        fun mk_prem x set B = HOLogic.mk_Trueprop (mk_subset (set $ x) B);
+        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));
         val premss = map2 ((fn x => fn sets =>  map2 (mk_prem x) sets (As @ Bs))) xFs setssAs;
         val concls = map3 mk_concl ss xFs Bs;
         val goals = map3 (fn x => fn prems => fn concl =>
           fold_rev Logic.all (x :: As @ Bs @ ss)

 
     val (mor_image_thms, morE_thms) =
       let
         val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
         fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
-          (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_subset (mk_image f $ B1) B2)));
+          (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_prem sets x T = HOLogic.mk_Trueprop
           (HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
         fun mk_elim_goal sets mapAsBs f s s' x T =
           fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)

         (map prove image_goals, map prove elim_goals)
       end;
 
     val mor_incl_thm =
       let
-        val prems = map2 (HOLogic.mk_Trueprop oo mk_subset) Bs Bs_copy;
+        val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
           (K (mk_mor_incl_tac mor_def map_id's))

         |> Thm.close_derivation
       end;
 
     val mor_inv_thm =
       let
-        fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_subset (mk_image inv_f $ B') B,
+        fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_leq (mk_image inv_f $ B') B,
           HOLogic.mk_conj (mk_inver inv_f f B, mk_inver f inv_f B'));
         val prems = map HOLogic.mk_Trueprop
           ([mk_mor Bs ss B's s's fs,
           mk_alg passive_UNIVs Bs ss,
           mk_alg passive_UNIVs B's s's] @

               sum_Card_order sum_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
               suc_bd_Asuc_bd Asuc_bd_Cinfinite)))
           |> Thm.close_derivation;
 
         val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
-        val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_subset min_algss Bs);
+        val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
         val least_cT = certifyT lthy suc_bdT;
         val least_ct = certify lthy (Term.absfree idx' least_conjunction);
 
         val least = singleton (Proof_Context.export names_lthy lthy)
           (Goal.prove_sorry lthy [] []

           |> Thm.close_derivation;
 
         val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
         fun mk_least_thm min_alg B def = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss)
-            (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_subset min_alg B))))
+            (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B))))
           (K (mk_least_min_alg_tac def least_min_algs_thm))
           |> Thm.close_derivation;
 
         val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
 

         val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose set_bd_thmss);
         val in_bd_tacs = map2 (K oo mk_in_bd_tac sum_Card_order suc_bd_Cnotzero)
           in_incl_min_alg_thms card_of_min_alg_thms;
         val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
 
-        val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
+        val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
 
         val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
-          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
+          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_OO_Grp_tacs;
 
         val ctor_witss =
           let
             val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf
               (replicate (nwits_of_bnf bnf) Ds)

         val fold_sets = fold_thms lthy (maps (fn bnf =>
           map (fn thm => thm RS meta_eq_to_obj_eq) (set_defs_of_bnf bnf)) Ibnfs);
 
         val timer = time (timer "registered new datatypes as BNFs");
 
-        val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
-        val Isrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Ibnfs;
         val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
         val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
 
-        val IsrelRs = map (fn Isrel => Term.list_comb (Isrel, IRs)) Isrels;
-        val srelRs = map (fn srel => Term.list_comb (srel, IRs @ IsrelRs)) srels;
-        val Irelphis = map (fn Isrel => Term.list_comb (Isrel, Iphis)) Irels;
-        val relphis = map (fn srel => Term.list_comb (srel, Iphis @ Irelphis)) rels;
-
-        val in_srels = map in_srel_of_bnf bnfs;
-        val in_Isrels = map in_srel_of_bnf Ibnfs;
-        val srel_defs = map srel_def_of_bnf bnfs;
-        val Isrel_defs = map srel_def_of_bnf Ibnfs;
+        val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels;
+        val relphis = map (fn rel => Term.list_comb (rel, Iphis @ Irelphis)) rels;
+
+        val in_rels = map in_rel_of_bnf bnfs;
+        val in_Irels = map in_rel_of_bnf Ibnfs;
+        val rel_defs = map rel_def_of_bnf bnfs;
         val Irel_defs = map rel_def_of_bnf Ibnfs;
 
         val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
         val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
         val folded_ctor_map_thms = map fold_maps ctor_map_thms;
         val folded_ctor_set_thmss = map (map fold_sets) ctor_set_thmss;
         val folded_ctor_set_thmss' = transpose folded_ctor_set_thmss;
 
-        val ctor_Isrel_thms =
+        val ctor_Irel_thms =
           let
-            fun mk_goal xF yF ctor ctor' IsrelR srelR = fold_rev Logic.all (xF :: yF :: IRs)
-              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IsrelR),
-                  HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), srelR)));
-            val goals = map6 mk_goal xFs yFs ctors ctor's IsrelRs srelRs;
+            fun mk_goal xF yF ctor ctor' Irelphi relphi = fold_rev Logic.all (xF :: yF :: Iphis)
+              (mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF));
+            val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
           in
-            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
+            map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
               fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
               fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss =>
               Goal.prove_sorry lthy [] [] goal
-               (K (mk_ctor_srel_tac lthy in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
+               (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets
                  ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
               |> Thm.close_derivation)
-            ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
+            ks goals in_rels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
               ctor_inject_thms ctor_dtor_thms set_map'ss ctor_set_incl_thmss
               ctor_set_set_incl_thmsss
-          end;
-
-        val ctor_Irel_thms =
-          let
-            fun mk_goal xF yF ctor ctor' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
-              (mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF));
-            val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
-          in
-            map3 (fn goal => fn srel_def => fn ctor_Isrel =>
-              Goal.prove_sorry lthy [] [] goal
-                (mk_ctor_or_dtor_rel_tac srel_def Irel_defs Isrel_defs ctor_Isrel)
-              |> Thm.close_derivation)
-            goals srel_defs ctor_Isrel_thms
           end;
 
         val timer = time (timer "additional properties");
 
         val ls' = if m = 1 then [0] else ls

         val Ibnf_notes =
           [(ctor_mapN, map single folded_ctor_map_thms),
           (ctor_relN, map single ctor_Irel_thms),
           (ctor_set_inclN, ctor_set_incl_thmss),
           (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @
-          (if note_all then
-             [(ctor_srelN, map single ctor_Isrel_thms)]
-           else
-             []) @
           map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_ctor_set_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)