Added premises concerning finite support of recursion results to FCBs.
authorberghofe
Thu Aug 24 15:20:43 2006 +0200 (2006-08-24)
changeset 20411dd8a1cda2eaf
parent 20410 4bd5cd97c547
child 20412 40757f475eb0
Added premises concerning finite support of recursion results to FCBs.
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Aug 23 23:40:47 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Aug 24 15:20:43 2006 +0200
     1.3 @@ -1391,6 +1391,7 @@
     1.4          val Ts = map (typ_of_dtyp descr'' sorts') cargs;
     1.5          val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
     1.6          val frees' = partition_cargs idxs frees;
     1.7 +        val atomTs = distinct op = (maps (map snd o fst) frees');
     1.8          val recs = List.mapPartial
     1.9            (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE)
    1.10            (partition_cargs idxs cargs ~~ frees');
    1.11 @@ -1409,6 +1410,10 @@
    1.12          val prems4 = map (fn ((i, _), y) =>
    1.13            HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees'');
    1.14          val prems5 = mk_fresh3 (recs ~~ frees'') frees';
    1.15 +        val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
    1.16 +          (HOLogic.mk_mem (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y,
    1.17 +             Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT)))))
    1.18 +               frees'') atomTs;
    1.19          val result = list_comb (List.nth (rec_fns, l), map Free (frees @ frees''));
    1.20          val result_freshs = map (fn p as (_, T) =>
    1.21            Const ("Nominal.fresh", T --> fastype_of result --> HOLogic.boolT) $
    1.22 @@ -1422,7 +1427,7 @@
    1.23           rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
    1.24           if null result_freshs then rec_prems'
    1.25           else rec_prems' @ [list_all_free (frees @ frees'',
    1.26 -           Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ [P],
    1.27 +           Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ prems6 @ [P],
    1.28               HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj result_freshs)))],
    1.29           rec_eq_prems @ [List.concat prems2 @ prems3],
    1.30           l + 1)
    1.31 @@ -1864,6 +1869,8 @@
    1.32                             [resolve_tac fcbs 1,
    1.33                              REPEAT_DETERM (resolve_tac
    1.34                                (fresh_prems @ rec_freshs1 @ rec_freshs2) 1),
    1.35 +                            REPEAT_DETERM (resolve_tac (maps snd rec_fin_supp_thms') 1
    1.36 +                              THEN resolve_tac rec_prems 1),
    1.37                              resolve_tac P_ind_ths 1,
    1.38                              REPEAT_DETERM (resolve_tac (P_ths @ rec_prems) 1)]);
    1.39