# HG changeset patch
# User blanchet
# Date 1348404773 -7200
# Node ID fe1deee434b687f44924316ee87eb8cb8927c295
# Parent  898aea2e7a945b49ba453bbd61ed10f0055076e0
generate "rel_as_srel" and "rel_flip" properties

diff -r 898aea2e7a94 -r fe1deee434b6 src/HOL/BNF/BNF_Def.thy
--- a/src/HOL/BNF/BNF_Def.thy	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Sun Sep 23 14:52:53 2012 +0200
@@ -145,7 +145,20 @@
 lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
 unfolding o_def fun_eq_iff by simp
 
+lemma eqset_imp_iff_pair: "A = B \<Longrightarrow> (a, b) \<in> A \<longleftrightarrow> (a, b) \<in> B"
+by (rule eqset_imp_iff)
+
+lemma fun_cong_pair: "f = g \<Longrightarrow> f {(a, b). R a b} = g {(a, b). R a b}"
+by (rule fun_cong)
+
+lemma flip_as_converse: "{(a, b). R b a} = converse {(a, b). R a b}"
+unfolding converse_def mem_Collect_eq prod.cases
+apply (rule arg_cong[of _ _ "\<lambda>x. Collect (prod_case x)"])
+apply (rule ext)+
+apply (unfold conversep_iff)
+by (rule refl)
+
 ML_file "Tools/bnf_def_tactics.ML"
-ML_file"Tools/bnf_def.ML"
+ML_file "Tools/bnf_def.ML"
 
 end
diff -r 898aea2e7a94 -r fe1deee434b6 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -56,7 +56,9 @@
   val map_id_of_bnf: BNF -> thm
   val map_wppull_of_bnf: BNF -> thm
   val map_wpull_of_bnf: BNF -> thm
+  val rel_as_srel_of_bnf: BNF -> thm
   val rel_def_of_bnf: BNF -> thm
+  val rel_flip_of_bnf: BNF -> thm
   val set_bd_of_bnf: BNF -> thm list
   val set_defs_of_bnf: BNF -> thm list
   val set_natural'_of_bnf: BNF -> thm list
@@ -182,6 +184,8 @@
   map_comp': thm lazy,
   map_id': thm lazy,
   map_wppull: thm lazy,
+  rel_as_srel: thm lazy,
+  rel_flip: thm lazy,
   set_natural': thm lazy list,
   srel_cong: thm lazy,
   srel_mono: thm lazy,
@@ -192,8 +196,8 @@
 };
 
 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel
-    map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id srel_Gr srel_converse
-    srel_O = {
+    map_comp' map_id' map_wppull rel_as_srel rel_flip set_natural' srel_cong srel_mono srel_Id
+    srel_Gr srel_converse srel_O = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
   bd_Cnotzero = bd_Cnotzero,
@@ -204,6 +208,8 @@
   map_comp' = map_comp',
   map_id' = map_id',
   map_wppull = map_wppull,
+  rel_as_srel = rel_as_srel,
+  rel_flip = rel_flip,
   set_natural' = set_natural',
   srel_cong = srel_cong,
   srel_mono = srel_mono,
@@ -223,6 +229,8 @@
   map_comp',
   map_id',
   map_wppull,
+  rel_as_srel,
+  rel_flip,
   set_natural',
   srel_cong,
   srel_mono,
@@ -240,6 +248,8 @@
     map_comp' = Lazy.map f map_comp',
     map_id' = Lazy.map f map_id',
     map_wppull = Lazy.map f map_wppull,
+    rel_as_srel = Lazy.map f rel_as_srel,
+    rel_flip = Lazy.map f rel_flip,
     set_natural' = map (Lazy.map f) set_natural',
     srel_cong = Lazy.map f srel_cong,
     srel_mono = Lazy.map f srel_mono,
@@ -358,7 +368,9 @@
 val map_cong_of_bnf = #map_cong o #axioms o rep_bnf;
 val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
 val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
+val rel_as_srel_of_bnf = Lazy.force o #rel_as_srel o #facts o rep_bnf;
 val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
+val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
 val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
 val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
 val set_natural_of_bnf = #set_natural o #axioms o rep_bnf;
@@ -490,15 +502,17 @@
 val map_comp'N = "map_comp'";
 val map_congN = "map_cong";
 val map_wpullN = "map_wpull";
+val rel_as_srelN = "rel_as_srel";
+val rel_flipN = "rel_flip";
+val set_naturalN = "set_natural";
+val set_natural'N = "set_natural'";
+val set_bdN = "set_bd";
 val srel_IdN = "srel_Id";
 val srel_GrN = "srel_Gr";
 val srel_converseN = "srel_converse";
 val srel_monoN = "srel_mono"
 val srel_ON = "srel_comp";
 val srel_O_GrN = "srel_comp_Gr";
-val set_naturalN = "set_natural";
-val set_natural'N = "set_natural'";
-val set_bdN = "set_bd";
 
 datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
 
@@ -695,7 +709,7 @@
       ||>> mk_Frees' "S" setRTs
       ||>> mk_Frees "S" setRTs
       ||>> mk_Frees "T" setRTsBsCs
-      ||>> mk_Frees' "Q" QTs;
+      ||>> mk_Frees' "R" QTs;
 
     (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
     val O_Gr =
@@ -714,11 +728,14 @@
         val y = Free (y_name, U);
       in fold_rev Term.lambda [x, y] (HOLogic.mk_mem (HOLogic.mk_prod (x, y), t)) end;
 
+    val sQs =
+      map3 (fn Q => fn T => fn U =>
+          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs';
+
     val rel_rhs = (case raw_rel_opt of
         NONE =>
         fold_rev absfree Qs' (mk_predicate_of_set (fst x') (fst y')
-          (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, map3 (fn Q => fn T => fn U =>
-          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs')))
+          (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, sQs)))
       | SOME raw_rel => prep_term no_defs_lthy raw_rel);
 
     val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
@@ -1090,11 +1107,36 @@
 
         val in_srel = mk_lazy mk_in_srel;
 
+        val eqset_imp_iff_pair = @{thm eqset_imp_iff_pair};
+        val mem_Collect_etc = @{thms mem_Collect_eq fst_conv snd_conv prod.cases};
+
+        fun mk_rel_as_srel () =
+          unfold_thms lthy mem_Collect_etc
+            (funpow live (fn thm => thm RS @{thm fun_cong_pair}) (bnf_srel_def RS meta_eq_to_obj_eq)
+               RS eqset_imp_iff_pair RS sym)
+          |> Drule.zero_var_indexes;
+
+        val rel_as_srel = mk_lazy mk_rel_as_srel;
+
+        fun mk_rel_flip () =
+          let
+            val srel_converse_thm = Lazy.force srel_converse;
+            val Rs' = Term.add_vars (prop_of srel_converse_thm) [];
+            val cts = map (pairself (certify lthy)) (map Var Rs' ~~ sQs);
+            val srel_converse_thm' = Drule.cterm_instantiate cts srel_converse_thm;
+          in
+            unfold_thms lthy (bnf_srel_def :: @{thm converse_iff} :: mem_Collect_etc)
+              (srel_converse_thm' RS eqset_imp_iff_pair)
+            |> Drule.zero_var_indexes |> Thm.generalize ([], map fst Qs') 1
+          end;
+
+        val rel_flip = mk_lazy mk_rel_flip;
+
         val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def;
 
         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong
-          in_mono in_srel map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id
-          srel_Gr srel_converse srel_O;
+          in_mono in_srel map_comp' map_id' map_wppull rel_as_srel rel_flip set_natural' srel_cong
+          srel_mono srel_Id srel_Gr srel_converse srel_O;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 
@@ -1141,6 +1183,8 @@
                     [(map_comp'N, [Lazy.force (#map_comp' facts)]),
                     (map_congN, [#map_cong axioms]),
                     (map_id'N, [Lazy.force (#map_id' facts)]),
+                    (rel_as_srelN, [Lazy.force (#rel_as_srel facts)]),
+                    (rel_flipN, [Lazy.force (#rel_flip facts)]),
                     (set_natural'N, map Lazy.force (#set_natural' facts)),
                     (srel_O_GrN, srel_O_Grs),
                     (srel_IdN, [Lazy.force (#srel_Id facts)]),