src/HOL/BNF/Tools/bnf_comp.ML

 
 (* TODO: Replace by "BNF_Defs.defs list" *)
 type unfold_set = {
   map_unfolds: thm list,
   set_unfoldss: thm list list,
-  rel_unfolds: thm list,
-  srel_unfolds: thm list
+  rel_unfolds: thm list
 };
 
-val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = [], srel_unfolds = []};
+val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
 
 fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
 fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
 
-fun add_to_unfolds map sets rel srel
-  {map_unfolds, set_unfoldss, rel_unfolds, srel_unfolds} =
+fun add_to_unfolds map sets rel
+  {map_unfolds, set_unfoldss, rel_unfolds} =
   {map_unfolds = add_to_thms map_unfolds map,
     set_unfoldss = adds_to_thms set_unfoldss sets,
-    rel_unfolds = add_to_thms rel_unfolds rel,
-    srel_unfolds = add_to_thms srel_unfolds srel};
+    rel_unfolds = add_to_thms rel_unfolds rel};
 
 fun add_bnf_to_unfolds bnf =
-  add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf)
-    (srel_def_of_bnf bnf);
+  add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf);
 
 val bdTN = "bdT";
 
 fun mk_killN n = "_kill" ^ string_of_int n;
 fun mk_liftN n = "_lift" ^ string_of_int n;

         (map bd_Cinfinite_of_bnf inners) (bd_Card_order_of_bnf outer);
 
     fun map_wpull_tac _ =
       mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
 
-    fun srel_O_Gr_tac _ =
+    fun rel_OO_Grp_tac _ =
       let
-        val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*)
-        val outer_srel_Gr = srel_Gr_of_bnf outer RS sym;
-        val outer_srel_cong = srel_cong_of_bnf outer;
+        val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
+        val outer_rel_cong = rel_cong_of_bnf outer;
         val thm =
-          (trans OF [in_alt_thm RS @{thm O_Gr_cong},
-             trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
-               [trans OF [outer_srel_Gr RS @{thm arg_cong[of _ _ converse]},
-                 srel_converse_of_bnf outer RS sym], outer_srel_Gr],
-               trans OF [srel_O_of_bnf outer RS sym, outer_srel_cong OF
-                 (map (fn bnf => srel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
-          |> unfold_thms lthy (basic_thms @ srel_def_of_bnf outer :: map srel_def_of_bnf inners);
+          (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
+             trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
+               [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
+                 rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
+               trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF
+                 (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym)
+          (*|> unfold_thms lthy (rel_def_of_bnf outer :: map rel_def_of_bnf inners)*);
       in
-        unfold_thms_tac lthy basic_thms THEN rtac thm 1
+        rtac thm 1
       end;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
-      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
 
     val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
 
     val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
       (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))

     fun in_bd_tac _ =
       mk_kill_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf)
         (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
-    fun srel_O_Gr_tac _ =
+    fun rel_OO_Grp_tac _ =
       let
-        val srel_Gr = srel_Gr_of_bnf bnf RS sym
+        val rel_Grp = rel_Grp_of_bnf bnf RS sym
         val thm =
-          (trans OF [in_alt_thm RS @{thm O_Gr_cong},
-            trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
-              [trans OF [srel_Gr RS @{thm arg_cong[of _ _ converse]},
-                srel_converse_of_bnf bnf RS sym], srel_Gr],
-              trans OF [srel_O_of_bnf bnf RS sym, srel_cong_of_bnf bnf OF
-                (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
-                 replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
-          |> unfold_thms lthy (srel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
+          (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
+            trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
+              [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]},
+                rel_conversep_of_bnf bnf RS sym], rel_Grp],
+              trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
+                (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
+                 replicate (live - n) @{thm Grp_fst_snd})]]] RS sym)
+          (*|> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv})*);
       in
         rtac thm 1
       end;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
-      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
 
     val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
 
     val wits = map (fn t => fold absfree (Term.add_frees t []) t)
       (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits);

       end;
 
     fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
-    fun srel_O_Gr_tac _ =
-      mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
+    fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
-      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 

 
     fun in_bd_tac _ =
       mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
-    fun srel_O_Gr_tac _ =
-      mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
+    fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
-      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 

       (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
 
     val map_unfolds = #map_unfolds unfold_set;
     val set_unfoldss = #set_unfoldss unfold_set;
     val rel_unfolds = #rel_unfolds unfold_set;
-    val srel_unfolds = #srel_unfolds unfold_set;
 
     val expand_maps =
       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
     val expand_sets =
       fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
     val expand_rels =
       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
     val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
     val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
     val unfold_rels = unfold_thms lthy rel_unfolds;
-    val unfold_srels = unfold_thms lthy srel_unfolds;
-    val unfold_all = unfold_sets o unfold_maps o unfold_rels o unfold_srels;
+    val unfold_all = unfold_sets o unfold_maps o unfold_rels;
     val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
     val bnf_sets = map (expand_maps o expand_sets)
       (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
     val bnf_bd = mk_bd_of_bnf Ds As bnf;
     val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf);

 
     val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
       (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
       (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
       (mk_tac (map_wpull_of_bnf bnf))
-      (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
+      (mk_tac (unfold_thms lthy [rel_def_of_bnf bnf] (rel_OO_Grp_of_bnf bnf)));
 
     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
     fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));