1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Jul 18 16:15:47 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Jul 18 17:10:22 2006 +0200
     1.3 @@ -1373,35 +1373,54 @@
     1.4  
     1.5      (* introduction rules for graph of recursion function *)
     1.6  
     1.7 -    fun make_rec_intr T rec_set ((rec_intr_ts, l), ((cname, cargs), idxs)) =
     1.8 +    val rec_preds = map (fn (a, T) =>
     1.9 +      Free (a, T --> HOLogic.boolT)) (pnames ~~ rec_result_Ts);
    1.10 +
    1.11 +    fun make_rec_intr T p rec_set
    1.12 +          ((rec_intr_ts, rec_prems, rec_prems', l), ((cname, cargs), idxs)) =
    1.13        let
    1.14          val Ts = map (typ_of_dtyp descr'' sorts') cargs;
    1.15          val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
    1.16          val frees' = partition_cargs idxs frees;
    1.17          val recs = List.mapPartial
    1.18 -          (fn ((_, DtRec i), (_, x)) => SOME (i, x) | _ => NONE)
    1.19 +          (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE)
    1.20            (partition_cargs idxs cargs ~~ frees');
    1.21          val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
    1.22            map (fn (i, _) => List.nth (rec_result_Ts, i)) recs;
    1.23 -        val prems = map (fn ((i, x), y) => HOLogic.mk_Trueprop
    1.24 +        val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop
    1.25            (HOLogic.mk_mem (HOLogic.mk_prod (Free x, Free y),
    1.26               List.nth (rec_sets, i)))) (recs ~~ frees'');
    1.27 -        val prems' =
    1.28 -          List.concat (map (fn p as (_, T) => map (fn f => HOLogic.mk_Trueprop
    1.29 +        val prems2 =
    1.30 +          map (fn f => map (fn p as (_, T) => HOLogic.mk_Trueprop
    1.31              (Const ("Nominal.fresh", T --> fastype_of f --> HOLogic.boolT) $
    1.32 -              Free p $ f)) rec_fns) (List.concat (map fst frees'))) @
    1.33 +              Free p $ f)) (List.concat (map fst frees'))) rec_fns;
    1.34 +        val prems3 =
    1.35            mk_fresh1 [] (List.concat (map fst frees')) @
    1.36 -          mk_fresh2 [] frees'
    1.37 -      in (rec_intr_ts @ [Logic.list_implies (prems' @ prems,
    1.38 -        HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.39 -          (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), map Free frees),
    1.40 -            list_comb (List.nth (rec_fns, l), map Free (frees @ frees''))),
    1.41 -             rec_set)))], l + 1)
    1.42 +          mk_fresh2 [] frees';
    1.43 +        val prems4 = map (fn ((i, _), y) =>
    1.44 +          HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees'');
    1.45 +        val result = list_comb (List.nth (rec_fns, l), map Free (frees @ frees''));
    1.46 +        val rec_freshs = map (fn p as (_, T) =>
    1.47 +          Const ("Nominal.fresh", T --> fastype_of result --> HOLogic.boolT) $
    1.48 +            Free p $ result) (List.concat (map (fst o snd) recs));
    1.49 +        val P = HOLogic.mk_Trueprop (p $ result)
    1.50 +      in
    1.51 +        (rec_intr_ts @ [Logic.list_implies (List.concat prems2 @ prems3 @ prems1,
    1.52 +           HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.53 +             (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), map Free frees),
    1.54 +               result), rec_set)))],
    1.55 +         rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
    1.56 +         if null rec_freshs then rec_prems'
    1.57 +         else rec_prems' @ [list_all_free (frees @ frees'',
    1.58 +           Logic.list_implies (List.nth (prems2, l) @ prems3 @ [P],
    1.59 +             HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_freshs)))],
    1.60 +         l + 1)
    1.61        end;
    1.62  
    1.63 -    val (rec_intr_ts, _) = Library.foldl (fn (x, (((d, d'), T), rec_set)) =>
    1.64 -      Library.foldl (make_rec_intr T rec_set) (x, #3 (snd d) ~~ snd d'))
    1.65 -        (([], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_sets);
    1.66 +    val (rec_intr_ts, rec_prems, rec_prems', _) =
    1.67 +      Library.foldl (fn (x, ((((d, d'), T), p), rec_set)) =>
    1.68 +        Library.foldl (make_rec_intr T p rec_set) (x, #3 (snd d) ~~ snd d'))
    1.69 +          (([], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets);
    1.70  
    1.71      val (thy11, {intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}) =
    1.72        setmp InductivePackage.quiet_mode (!quiet_mode)
    1.73 @@ -1472,11 +1491,51 @@
    1.74                 (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
    1.75        end) dt_atomTs;
    1.76  
    1.77 +    (** uniqueness **)
    1.78 +
    1.79 +    val fresh_prems = List.concat (map (fn aT =>
    1.80 +      map (fn (f, T) => HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.81 +        (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f,
    1.82 +         Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT)))))
    1.83 +           (rec_fns ~~ rec_fn_Ts)) dt_atomTs);
    1.84 +
    1.85 +    val fun_tuple = foldr1 HOLogic.mk_prod rec_fns;
    1.86 +    val fun_tupleT = fastype_of fun_tuple;
    1.87 +    val rec_unique_frees =
    1.88 +      DatatypeProp.indexify_names (replicate (length recTs) "x") ~~ recTs;
    1.89 +    val rec_unique_concls = map (fn ((x as (_, T), U), R) =>
    1.90 +        Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $
    1.91 +          Abs ("y", U, HOLogic.mk_mem (HOLogic.pair_const T U $ Free x $ Bound 0, R)))
    1.92 +      (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
    1.93 +    val induct_aux_rec = Drule.cterm_instantiate
    1.94 +      (map (pairself (cterm_of thy11))
    1.95 +         (map (fn (aT, f) => (Logic.varify f, Abs ("z", HOLogic.unitT,
    1.96 +            Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
    1.97 +              fresh_fs @
    1.98 +          map (fn (((P, T), (x, U)), Q) =>
    1.99 +           (Var ((P, 0), HOLogic.unitT --> Logic.varifyT T --> HOLogic.boolT),
   1.100 +            Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
   1.101 +              (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
   1.102 +          map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T)))
   1.103 +            rec_unique_frees)) induct_aux;
   1.104 +
   1.105 +    val rec_unique = map standard (split_conj_thm (Goal.prove_global thy11 []
   1.106 +      (fresh_prems @ rec_prems @ rec_prems')
   1.107 +      (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls))
   1.108 +      (fn ths => EVERY
   1.109 +         [rtac induct_aux_rec 1,
   1.110 +          print_tac "after application of induction theorem",
   1.111 +          setmp quick_and_dirty true (SkipProof.cheat_tac thy11) (** FIXME !! **)])));
   1.112 +    
   1.113      (* FIXME: theorems are stored in database for testing only *)
   1.114 -    val (_, thy12) = PureThy.add_thmss
   1.115 -      [(("rec_equiv", List.concat rec_equiv_thms), []),
   1.116 -       (("rec_equiv'", List.concat rec_equiv_thms'), []),
   1.117 -       (("rec_fin_supp", List.concat rec_fin_supp_thms), [])] thy11;
   1.118 +    val (_, thy12) = thy11 |>
   1.119 +      Theory.add_path big_name |>
   1.120 +      PureThy.add_thmss
   1.121 +        [(("rec_equiv", List.concat rec_equiv_thms), []),
   1.122 +         (("rec_equiv'", List.concat rec_equiv_thms'), []),
   1.123 +         (("rec_fin_supp", List.concat rec_fin_supp_thms), []),
   1.124 +         (("rec_unique", rec_unique), [])] ||>
   1.125 +      Theory.parent_path;
   1.126  
   1.127    in
   1.128      thy12