src/HOL/Nominal/nominal_package.ML
changeset 19851 10162c01bd78
parent 19833 3a3f591c838d
child 19874 cc4b2b882e4c
     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)) =>