Additional freshness constraints for FCB.
authorberghofe
Mon Jul 31 14:08:42 2006 +0200 (2006-07-31)
changeset 202671154363129be
parent 20266 6fb734789818
child 20268 1fe9aed8fcac
Additional freshness constraints for FCB.
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Sun Jul 30 21:28:59 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Jul 31 14:08:42 2006 +0200
     1.3 @@ -136,6 +136,8 @@
     1.4    ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
     1.5    |> map (standard #> RuleCases.save rule);
     1.6  
     1.7 +val supp_prod = thm "supp_prod";
     1.8 +
     1.9  fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
    1.10    let
    1.11      (* this theory is used just for parsing *)
    1.12 @@ -1376,6 +1378,14 @@
    1.13      val rec_preds = map (fn (a, T) =>
    1.14        Free (a, T --> HOLogic.boolT)) (pnames ~~ rec_result_Ts);
    1.15  
    1.16 +    fun mk_fresh3 rs [] = []
    1.17 +      | mk_fresh3 rs ((p as (ys, z)) :: yss) = List.concat (map (fn y as (_, T) =>
    1.18 +            List.mapPartial (fn ((_, (_, x)), r as (_, U)) => if z = x then NONE
    1.19 +              else SOME (HOLogic.mk_Trueprop
    1.20 +                (Const ("Nominal.fresh", T --> U --> HOLogic.boolT) $ Free y $ Free r)))
    1.21 +                  rs) ys) @
    1.22 +          mk_fresh3 rs yss;
    1.23 +
    1.24      fun make_rec_intr T p rec_set
    1.25            ((rec_intr_ts, rec_prems, rec_prems', l), ((cname, cargs), idxs)) =
    1.26        let
    1.27 @@ -1399,6 +1409,7 @@
    1.28            mk_fresh2 [] frees';
    1.29          val prems4 = map (fn ((i, _), y) =>
    1.30            HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees'');
    1.31 +        val prems5 = mk_fresh3 (recs ~~ frees'') frees';
    1.32          val result = list_comb (List.nth (rec_fns, l), map Free (frees @ frees''));
    1.33          val rec_freshs = map (fn p as (_, T) =>
    1.34            Const ("Nominal.fresh", T --> fastype_of result --> HOLogic.boolT) $
    1.35 @@ -1412,7 +1423,7 @@
    1.36           rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
    1.37           if null rec_freshs then rec_prems'
    1.38           else rec_prems' @ [list_all_free (frees @ frees'',
    1.39 -           Logic.list_implies (List.nth (prems2, l) @ prems3 @ [P],
    1.40 +           Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ [P],
    1.41               HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_freshs)))],
    1.42           l + 1)
    1.43        end;
    1.44 @@ -1503,6 +1514,8 @@
    1.45      val fun_tupleT = fastype_of fun_tuple;
    1.46      val rec_unique_frees =
    1.47        DatatypeProp.indexify_names (replicate (length recTs) "x") ~~ recTs;
    1.48 +    val rec_unique_frees' =
    1.49 +      DatatypeProp.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
    1.50      val rec_unique_concls = map (fn ((x as (_, T), U), R) =>
    1.51          Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $
    1.52            Abs ("y", U, HOLogic.mk_mem (HOLogic.pair_const T U $ Free x $ Bound 0, R)))
    1.53 @@ -1522,10 +1535,31 @@
    1.54      val rec_unique = map standard (split_conj_thm (Goal.prove_global thy11 []
    1.55        (fresh_prems @ rec_prems @ rec_prems')
    1.56        (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls))
    1.57 -      (fn ths => EVERY
    1.58 -         [rtac induct_aux_rec 1,
    1.59 -          print_tac "after application of induction theorem",
    1.60 -          setmp quick_and_dirty true (SkipProof.cheat_tac thy11) (** FIXME !! **)])));
    1.61 +      (fn ths =>
    1.62 +         let
    1.63 +           val k = length rec_fns;
    1.64 +           val (finite_thss, ths1) = funpow (length dt_atomTs) (fn (xss, ys) =>
    1.65 +             apfst (curry op @ xss o single) (chop k ys)) ([], ths);
    1.66 +           val (P_ind_ths, ths2) = chop k ths1;
    1.67 +           val P_ths = map (fn th => th RS mp) (split_conj_thm
    1.68 +             (Goal.prove (Context.init_proof thy11)
    1.69 +               (map fst (rec_unique_frees @ rec_unique_frees')) []
    1.70 +               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.71 +                  (map (fn (((x, y), S), P) => HOLogic.mk_imp (HOLogic.mk_mem
    1.72 +                    (HOLogic.mk_prod (Free x, Free y), S), P $ (Free y)))
    1.73 +                      (rec_unique_frees ~~ rec_unique_frees' ~~ rec_sets ~~ rec_preds))))
    1.74 +               (fn _ =>
    1.75 +                  rtac rec_induct 1 THEN
    1.76 +                  REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))))
    1.77 +         in EVERY
    1.78 +           ([rtac induct_aux_rec 1] @
    1.79 +            List.concat (map (fn finite_ths =>
    1.80 +              [cut_facts_tac finite_ths 1,
    1.81 +               asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1]) finite_thss) @
    1.82 +            [ALLGOALS (full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff])),
    1.83 +             print_tac "after application of induction theorem",
    1.84 +             setmp quick_and_dirty true (SkipProof.cheat_tac thy11) (** FIXME !! **)])
    1.85 +         end)));
    1.86      
    1.87      (* FIXME: theorems are stored in database for testing only *)
    1.88      val (_, thy12) = thy11 |>