author berghofe Tue Jul 18 17:10:22 2006 +0200 (2006-07-18) changeset 20145 922b4e7b8efd parent 20144 2517cd4b1f37 child 20146 d8cf6eb9baf9
Started implementing uniqueness proof for recursion
combinator (still unfinished).
```     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 |>