src/HOL/Nominal/nominal_package.ML
changeset 19985 d39c554cf750
parent 19874 cc4b2b882e4c
child 20046 9c8909fc5865
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Jul 04 14:47:01 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Jul 04 15:20:43 2006 +0200
     1.3 @@ -1343,7 +1343,19 @@
     1.4  
     1.5      val used = foldr add_typ_tfree_names [] recTs;
     1.6  
     1.7 -    val (rec_result_Ts, rec_fn_Ts) = DatatypeProp.make_primrec_Ts descr' sorts' used;
     1.8 +    val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts' used;
     1.9 +
    1.10 +    val rec_sort = if null dt_atomTs then HOLogic.typeS else 
    1.11 +      let val names = map (Sign.base_name o fst o dest_Type) dt_atomTs
    1.12 +      in Sign.certify_sort thy10 (map (Sign.intern_class thy10)
    1.13 +        (map (fn s => "pt_" ^ s) names @
    1.14 +         List.concat (map (fn s => List.mapPartial (fn s' =>
    1.15 +           if s = s' then NONE
    1.16 +           else SOME ("cp_" ^ s ^ "_" ^ s')) names) names)))
    1.17 +      end;
    1.18 +
    1.19 +    val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
    1.20 +    val rec_fn_Ts = map (typ_subst_atomic (rec_result_Ts' ~~ rec_result_Ts)) rec_fn_Ts';
    1.21  
    1.22      val rec_set_Ts = map (fn (T1, T2) => rec_fn_Ts ---> HOLogic.mk_setT
    1.23        (HOLogic.mk_prodT (T1, T2))) (recTs ~~ rec_result_Ts);
    1.24 @@ -1391,13 +1403,83 @@
    1.25        Library.foldl (make_rec_intr T rec_set) (x, #3 (snd d) ~~ snd d'))
    1.26          (([], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_sets);
    1.27  
    1.28 -    val (thy11, {intrs = rec_intrs, elims = rec_elims, ...}) =
    1.29 +    val (thy11, {intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}) =
    1.30        setmp InductivePackage.quiet_mode (!quiet_mode)
    1.31          (InductivePackage.add_inductive_i false true big_rec_name false false false
    1.32             rec_sets (map (fn x => (("", x), [])) rec_intr_ts) []) thy10;
    1.33  
    1.34 +    (** equivariance **)
    1.35 +
    1.36 +    val fresh_bij = PureThy.get_thms thy11 (Name "fresh_bij");
    1.37 +    val perm_bij = PureThy.get_thms thy11 (Name "perm_bij");
    1.38 +
    1.39 +    val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
    1.40 +      let
    1.41 +        val permT = mk_permT aT;
    1.42 +        val pi = Free ("pi", permT);
    1.43 +        val rec_fns_pi = map (curry (mk_perm []) pi o uncurry (mk_Free "f"))
    1.44 +          (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
    1.45 +        val rec_sets_pi = map (fn c => list_comb (Const c, rec_fns_pi))
    1.46 +          (rec_set_names ~~ rec_set_Ts);
    1.47 +        val ps = map (fn ((((T, U), R), R'), i) =>
    1.48 +          let
    1.49 +            val x = Free ("x" ^ string_of_int i, T);
    1.50 +            val y = Free ("y" ^ string_of_int i, U)
    1.51 +          in
    1.52 +            (HOLogic.mk_mem (HOLogic.mk_prod (x, y), R),
    1.53 +             HOLogic.mk_mem (HOLogic.mk_prod (mk_perm [] (pi, x), mk_perm [] (pi, y)), R'))
    1.54 +          end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
    1.55 +        val ths = map (fn th => standard (th RS mp)) (split_conj_thm
    1.56 +          (Goal.prove thy11 [] []
    1.57 +            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps)))
    1.58 +            (fn _ => rtac rec_induct 1 THEN REPEAT
    1.59 +               (NominalPermeq.perm_simp_tac (simpset_of thy11) 1 THEN
    1.60 +                (resolve_tac rec_intrs THEN_ALL_NEW
    1.61 +                 asm_simp_tac (HOL_ss addsimps (fresh_bij @ perm_bij))) 1))))
    1.62 +        val ths' = map (fn ((P, Q), th) => standard
    1.63 +          (Goal.prove thy11 [] []
    1.64 +            (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P))
    1.65 +            (fn _ => dtac (Thm.instantiate ([],
    1.66 +                 [(cterm_of thy11 (Var (("pi", 0), permT)),
    1.67 +                   cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
    1.68 +               NominalPermeq.perm_simp_tac HOL_ss 1))) (ps ~~ ths)
    1.69 +      in (ths, ths') end) dt_atomTs);
    1.70 +
    1.71 +    (** finite support **)
    1.72 +
    1.73 +    val rec_fin_supp_thms = map (fn aT =>
    1.74 +      let
    1.75 +        val name = Sign.base_name (fst (dest_Type aT));
    1.76 +        val fs_name = PureThy.get_thm thy11 (Name ("fs_" ^ name ^ "1"));
    1.77 +        val aset = HOLogic.mk_setT aT;
    1.78 +        val finites = Const ("Finite_Set.Finites", HOLogic.mk_setT aset);
    1.79 +        val fins = map (fn (f, T) => HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.80 +          (Const ("Nominal.supp", T --> aset) $ f, finites)))
    1.81 +            (rec_fns ~~ rec_fn_Ts)
    1.82 +      in
    1.83 +        map (fn th => standard (th RS mp)) (split_conj_thm
    1.84 +          (Goal.prove thy11 [] fins
    1.85 +            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.86 +              (map (fn (((T, U), R), i) =>
    1.87 +                 let
    1.88 +                   val x = Free ("x" ^ string_of_int i, T);
    1.89 +                   val y = Free ("y" ^ string_of_int i, U)
    1.90 +                 in
    1.91 +                   HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (x, y), R),
    1.92 +                     HOLogic.mk_mem (Const ("Nominal.supp", U --> aset) $ y, finites))
    1.93 +                 end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ (1 upto length recTs)))))
    1.94 +            (fn fins => (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
    1.95 +               (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
    1.96 +      end) dt_atomTs;
    1.97 +
    1.98 +    (* FIXME: theorems are stored in database for testing only *)
    1.99 +    val (_, thy12) = PureThy.add_thmss
   1.100 +      [(("rec_equiv", List.concat rec_equiv_thms), []),
   1.101 +       (("rec_equiv'", List.concat rec_equiv_thms'), []),
   1.102 +       (("rec_fin_supp", List.concat rec_fin_supp_thms), [])] thy11;
   1.103 +
   1.104    in
   1.105 -    thy11
   1.106 +    thy12
   1.107    end;
   1.108  
   1.109  val add_nominal_datatype = gen_add_nominal_datatype read_typ true;