# HG changeset patch
# User berghofe
# Date 1142204963 -3600
# Node ID 6bc0dda66f3257b922ce81d9d3a4f9123d219972
# Parent  932a50e2332f5778b2926b44620fe38540398bea
First version of function for defining graph of iteration combinator.

diff -r 932a50e2332f -r 6bc0dda66f32 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Sat Mar 11 21:23:10 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Mar 13 00:09:23 2006 +0100
@@ -1321,8 +1321,110 @@
       PureThy.add_thmss [(("inducts", projections induct), [case_names_induct])] ||>
       Theory.parent_path;
 
+    (**** iteration combinator ****)
+
+    val _ = warning "defining iteration combinator ...";
+
+    val used = foldr add_typ_tfree_names [] recTs;
+    val rec_result_Ts = map TFree (variantlist (replicate (length descr'') "'t", used) ~~
+      replicate (length descr'') HOLogic.typeS);
+
+    val iter_fn_Ts = List.concat (map (fn (i, (_, _, constrs)) =>
+      map (fn (_, cargs) =>
+        let
+          val Ts = map (typ_of_dtyp descr'' sorts') cargs;
+          fun mk_argT (dt, T) =
+            if is_rec_type dt then List.nth (rec_result_Ts, body_index dt)
+            else T;
+          val argTs = map mk_argT (cargs ~~ Ts)
+        in argTs ---> List.nth (rec_result_Ts, i)
+        end) constrs) descr'');
+
+    val permTs = map mk_permT dt_atomTs;
+    val perms = map Free
+      (DatatypeProp.indexify_names (replicate (length permTs) "pi") ~~ permTs);
+
+    val iter_set_Ts = map (fn (T1, T2) => iter_fn_Ts ---> HOLogic.mk_setT
+      (HOLogic.mk_prodT (T1, permTs ---> T2))) (recTs ~~ rec_result_Ts);
+
+    val big_iter_name = big_name ^ "_iter_set";
+    val iter_set_names = map (Sign.full_name (Theory.sign_of thy10))
+      (if length descr'' = 1 then [big_iter_name] else
+        (map ((curry (op ^) (big_iter_name ^ "_")) o string_of_int)
+          (1 upto (length descr''))));
+
+    val iter_fns = map (uncurry (mk_Free "f"))
+      (iter_fn_Ts ~~ (1 upto (length iter_fn_Ts)));
+    val iter_sets = map (fn c => list_comb (Const c, iter_fns))
+      (iter_set_names ~~ iter_set_Ts);
+
+    (* introduction rules for graph of iteration function *)
+
+    fun partition_cargs idxs xs = map (fn (i, j) =>
+      (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
+
+    fun mk_fresh_fun (a, t) = Const ("nominal.fresh_fun",
+      (fastype_of a --> fastype_of t) --> fastype_of t) $ lambda a t;
+
+    fun make_iter_intr T iter_set ((iter_intr_ts, l), ((cname, cargs), idxs)) =
+      let
+        fun mk_prem ((dts, (dt, U)), (j, k, prems, t1s, t2s, atoms)) =
+          let
+            val free1 = mk_Free "x" U (j + length dts);
+            val Us = map snd dts;
+            val xs = Us ~~ (j upto j + length dts - 1);
+            val frees = map (uncurry (mk_Free "x")) xs;
+            val frees' = map (uncurry (mk_Free "x'")) xs;
+            val frees'' = Us ~~ (frees ~~ frees');
+            val pis = map (fn (T, p) =>
+              case filter (equal T o fst) frees'' of
+                [] => p
+              | xs => HOLogic.mk_binop "List.op @" (p,
+                HOLogic.mk_list (HOLogic.mk_prod o snd)
+                  (HOLogic.mk_prodT (T, T)) xs))
+                  (dt_atomTs ~~ perms)
+          in (case dt of
+             DtRec m =>
+               let val free2 = mk_Free "y"
+                 (permTs ---> List.nth (rec_result_Ts, m)) k
+               in (j + length dts + 1, k + 1,
+                   HOLogic.mk_Trueprop
+                     (HOLogic.mk_mem (HOLogic.mk_prod
+                       (free1, free2),
+                         List.nth (iter_sets, m))) :: prems,
+                   frees @ free1 :: t1s,
+                   frees' @ list_comb (free2, pis) :: t2s,
+                   frees' @ atoms)
+               end
+           | _ => (j + length dts + 1, k, prems,
+               frees @ free1 :: t1s,
+               frees' @ foldr (mk_perm []) free1 pis :: t2s,
+               frees' @ atoms))
+          end;
+
+        val Ts = map (typ_of_dtyp descr'' sorts') cargs;
+        val (_, _, prems, t1s, t2s, atoms) = foldr mk_prem (1, 1, [], [], [], [])
+          (partition_cargs idxs (cargs ~~ Ts))
+
+      in (iter_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
+        (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
+          foldr (uncurry lambda)
+            (foldr mk_fresh_fun
+              (list_comb (List.nth (iter_fns, l), t2s)) atoms)
+            perms), iter_set)))], l + 1)
+      end;
+
+    val (iter_intr_ts, _) = Library.foldl (fn (x, (((d, d'), T), iter_set)) =>
+      Library.foldl (make_iter_intr T iter_set) (x, #3 (snd d) ~~ snd d'))
+        (([], 0), descr'' ~~ ndescr ~~ recTs ~~ iter_sets);
+
+    val (thy11, {intrs = iter_intrs, elims = iter_elims, ...}) =
+      setmp InductivePackage.quiet_mode (!quiet_mode)
+        (InductivePackage.add_inductive_i false true big_iter_name false false false
+           iter_sets (map (fn x => (("", x), [])) iter_intr_ts) []) thy10;
+
   in
-    thy10
+    thy11
   end;
 
 val add_nominal_datatype = gen_add_nominal_datatype read_typ true;