# HG changeset patch
# User blanchet
# Date 1376671557 -7200
# Node ID dd5ea8a51af08c51fdd248899b19f9e20d0b5375
# Parent  e5fa456890b4bcd7791a752802c590c3a494d415
generalized "mk_permute"

diff -r e5fa456890b4 -r dd5ea8a51af0 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Aug 16 18:36:55 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Aug 16 18:45:57 2013 +0200
@@ -445,8 +445,8 @@
     val live = live_of_bnf bnf;
     val dead = dead_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
-    fun permute xs = mk_permute src dest xs;
-    fun permute_rev xs = mk_permute dest src xs;
+    fun permute xs = mk_permute (op =) src dest xs;
+    fun unpermute xs = mk_permute (op =) dest src xs;
 
     val (Ds, lthy1) = apfst (map TFree)
       (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
@@ -462,10 +462,10 @@
 
     (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
     val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
-      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
+      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0))));
     (*%Q(1) ... Q(n). bnf.rel Q\<sigma>(1) ... Q\<sigma>(n)*)
     val rel = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs))
-      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
+      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0))));
 
     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
     val sets = permute bnf_sets;
@@ -484,7 +484,7 @@
     val in_alt_thm =
       let
         val inx = mk_in Asets sets T;
-        val in_alt = mk_in (permute_rev Asets) bnf_sets T;
+        val in_alt = mk_in (unpermute Asets) bnf_sets T;
         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
       in
         Goal.prove_sorry lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
diff -r e5fa456890b4 -r dd5ea8a51af0 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:36:55 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:45:57 2013 +0200
@@ -49,10 +49,13 @@
   val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
   val splice: 'a list -> 'a list -> 'a list
   val transpose: 'a list list -> 'a list list
-  val sort_like: ('a * 'b -> bool) -> 'b list -> 'c list -> 'a list -> 'c list
   val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
   val pad_list: 'a -> int -> 'a list -> 'a list
 
+  val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list
+  val mk_permute: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list
+  val sort_like: ('a * 'b -> bool) -> 'b list -> 'c list -> 'a list -> 'c list
+
   val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
   val mk_TFrees: int -> Proof.context -> typ list * Proof.context
   val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
@@ -167,9 +170,6 @@
   val fold_thms: Proof.context -> thm list -> thm -> thm
   val unfold_thms: Proof.context -> thm list -> thm -> thm
 
-  val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
-  val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list
-
   val certifyT: Proof.context -> typ -> ctyp
   val certify: Proof.context -> term -> cterm
 
@@ -624,8 +624,6 @@
   let val T = (case xs of [] => defT | (x::_) => fastype_of x);
   in Const (@{const_name collect}, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end;
 
-fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest;
-
 fun rapp u t = betapply (t, u);
 
 val list_all_free =
@@ -722,6 +720,8 @@
   | transpose ([] :: xss) = transpose xss
   | transpose xss = map hd xss :: transpose (map tl xss);
 
+fun mk_permute eq xs xs' ys = map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs';
+
 (*FIXME: merge with mk_permute*)
 fun sort_like eq xs ys = map (fn x => nth ys (find_index (curry eq x) xs));