author berghofe Mon Jun 12 00:36:52 2006 +0200 (2006-06-12) changeset 19851 10162c01bd78 parent 19850 29c125556d86 child 19852 b06db8e4476b
Completely rewrote code for defining graph of recursion combinator.
```     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Sun Jun 11 22:45:53 2006 +0200
1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Jun 12 00:36:52 2006 +0200
1.3 @@ -1078,6 +1078,19 @@
1.4      fun make_pred fsT i T =
1.5        Free (List.nth (pnames, i), fsT --> T --> HOLogic.boolT);
1.6
1.7 +    fun mk_fresh1 xs [] = []
1.8 +      | mk_fresh1 xs ((y as (_, T)) :: ys) = map (fn x => HOLogic.mk_Trueprop
1.9 +            (HOLogic.mk_not (HOLogic.mk_eq (Free y, Free x))))
1.10 +              (filter (fn (_, U) => T = U) (rev xs)) @
1.11 +          mk_fresh1 (y :: xs) ys;
1.12 +
1.13 +    fun mk_fresh2 xss [] = []
1.14 +      | mk_fresh2 xss ((p as (ys, _)) :: yss) = List.concat (map (fn y as (_, T) =>
1.15 +            map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop
1.16 +              (Const ("Nominal.fresh", T --> U --> HOLogic.boolT) \$ Free y \$ Free x))
1.17 +                (rev xss @ yss)) ys) @
1.18 +          mk_fresh2 (p :: xss) yss;
1.19 +
1.20      fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
1.21        let
1.22          val recs = List.filter is_rec_type cargs;
1.23 @@ -1097,19 +1110,6 @@
1.24              (make_pred fsT (body_index dt) U \$ Bound l \$ app_bnds (Free (s, T)) l))
1.25            end;
1.26
1.27 -        fun mk_fresh1 xs [] = []
1.28 -          | mk_fresh1 xs ((y as (_, T)):: ys) = map (fn x => HOLogic.mk_Trueprop
1.29 -                (HOLogic.mk_not (HOLogic.mk_eq (Free y, Free x))))
1.30 -                  (filter (fn (_, U) => T = U) (rev xs)) @
1.31 -              mk_fresh1 (y :: xs) ys;
1.32 -
1.33 -        fun mk_fresh2 xss [] = []
1.34 -          | mk_fresh2 xss ((p as (ys, _)) :: yss) = List.concat (map (fn y as (_, T) =>
1.35 -                map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop
1.36 -                  (Const ("Nominal.fresh", T --> U --> HOLogic.boolT) \$ Free y \$ Free x))
1.37 -                    (rev xss @ yss)) ys) @
1.38 -              mk_fresh2 (p :: xss) yss;
1.39 -
1.40          val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
1.41          val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
1.42              (f T (Free p) (Free z))) (List.concat (map fst frees')) @
1.43 @@ -1345,12 +1345,8 @@
1.44
1.45      val (rec_result_Ts, rec_fn_Ts) = DatatypeProp.make_primrec_Ts descr' sorts' used;
1.46
1.47 -    val permTs = map mk_permT dt_atomTs;
1.48 -    val perms = map Free
1.49 -      (DatatypeProp.indexify_names (replicate (length permTs) "pi") ~~ permTs);
1.50 -
1.51      val rec_set_Ts = map (fn (T1, T2) => rec_fn_Ts ---> HOLogic.mk_setT
1.52 -      (HOLogic.mk_prodT (T1, permTs ---> T2))) (recTs ~~ rec_result_Ts);
1.53 +      (HOLogic.mk_prodT (T1, T2))) (recTs ~~ rec_result_Ts);
1.54
1.55      val big_rec_name = big_name ^ "_rec_set";
1.56      val rec_set_names = map (Sign.full_name (Theory.sign_of thy10))
1.57 @@ -1365,57 +1361,30 @@
1.58
1.59      (* introduction rules for graph of recursion function *)
1.60
1.61 -    fun mk_fresh_fun (a, t) = Const ("Nominal.fresh_fun",
1.62 -      (fastype_of a --> fastype_of t) --> fastype_of t) \$ lambda a t;
1.63 -
1.64      fun make_rec_intr T rec_set ((rec_intr_ts, l), ((cname, cargs), idxs)) =
1.65        let
1.66 -        fun mk_prem ((dts, (dt, U)), (j, k, prems, t1s, t2s, t3s, atoms)) =
1.67 -          let
1.68 -            val free1 = mk_Free "x" U (j + length dts);
1.69 -            val Us = map snd dts;
1.70 -            val xs = Us ~~ (j upto j + length dts - 1);
1.71 -            val frees = map (uncurry (mk_Free "x")) xs;
1.72 -            val frees' = map (uncurry (mk_Free "x'")) xs;
1.73 -            val frees'' = Us ~~ (frees ~~ frees');
1.74 -            val pis = map (fn (T, p) =>
1.75 -              case filter (equal T o fst) frees'' of
1.76 -                [] => p
1.77 -              | xs => HOLogic.mk_binop "List.op @" (p,
1.78 -                HOLogic.mk_list (HOLogic.mk_prod o snd)
1.79 -                  (HOLogic.mk_prodT (T, T)) xs))
1.80 -                  (dt_atomTs ~~ perms)
1.81 -          in (case dt of
1.82 -             DtRec m =>
1.83 -               let val free2 = mk_Free "y"
1.84 -                 (permTs ---> List.nth (rec_result_Ts, m)) k
1.85 -               in (j + length dts + 1, k + 1,
1.86 -                   HOLogic.mk_Trueprop
1.87 -                     (HOLogic.mk_mem (HOLogic.mk_prod
1.88 -                       (free1, free2),
1.89 -                         List.nth (rec_sets, m))) :: prems,
1.90 -                   frees @ free1 :: t1s,
1.91 -                   frees' @ foldr (mk_perm []) free1 pis :: t2s,
1.92 -                   list_comb (free2, pis) :: t3s,
1.93 -                   frees' @ atoms)
1.94 -               end
1.95 -           | _ => (j + length dts + 1, k, prems,
1.96 -               frees @ free1 :: t1s,
1.97 -               frees' @ foldr (mk_perm []) free1 pis :: t2s,
1.98 -               t3s,
1.99 -               frees' @ atoms))
1.100 -          end;
1.101 -
1.102          val Ts = map (typ_of_dtyp descr'' sorts') cargs;
1.103 -        val (_, _, prems, t1s, t2s, t3s, atoms) = foldr mk_prem (1, 1, [], [], [], [], [])
1.104 -          (partition_cargs idxs (cargs ~~ Ts))
1.105 -
1.106 -      in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
1.107 -        (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
1.108 -          foldr (uncurry lambda)
1.109 -            (foldr mk_fresh_fun
1.110 -              (list_comb (List.nth (rec_fns, l), t2s @ t3s)) atoms)
1.111 -            perms), rec_set)))], l + 1)
1.112 +        val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
1.113 +        val frees' = partition_cargs idxs frees;
1.114 +        val recs = List.mapPartial
1.115 +          (fn ((_, DtRec i), (_, x)) => SOME (i, x) | _ => NONE)
1.116 +          (partition_cargs idxs cargs ~~ frees');
1.117 +        val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
1.118 +          map (fn (i, _) => List.nth (rec_result_Ts, i)) recs;
1.119 +        val prems = map (fn ((i, x), y) => HOLogic.mk_Trueprop
1.120 +          (HOLogic.mk_mem (HOLogic.mk_prod (Free x, Free y),
1.121 +             List.nth (rec_sets, i)))) (recs ~~ frees'');
1.122 +        val prems' =
1.123 +          List.concat (map (fn p as (_, T) => map (fn f => HOLogic.mk_Trueprop
1.124 +            (Const ("Nominal.fresh", T --> fastype_of f --> HOLogic.boolT) \$
1.125 +              Free p \$ f)) rec_fns) (List.concat (map fst frees'))) @
1.126 +          mk_fresh1 [] (List.concat (map fst frees')) @
1.127 +          mk_fresh2 [] frees'
1.128 +      in (rec_intr_ts @ [Logic.list_implies (prems' @ prems,
1.129 +        HOLogic.mk_Trueprop (HOLogic.mk_mem
1.130 +          (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), map Free frees),
1.131 +            list_comb (List.nth (rec_fns, l), map Free (frees @ frees''))),
1.132 +             rec_set)))], l + 1)
1.133        end;
1.134
1.135      val (rec_intr_ts, _) = Library.foldl (fn (x, (((d, d'), T), rec_set)) =>
```