src/HOL/Nominal/nominal_package.ML
changeset 18066 d1e47ee13070
parent 18054 2493cb9f5ede
child 18067 8b9848d150ba
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Nov 02 14:48:55 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Nov 02 15:05:22 2005 +0100
     1.3 @@ -1895,6 +1895,29 @@
     1.4  
     1.5      val case_names_induct = mk_case_names_induct (List.concat descr');
     1.6  
     1.7 +    (**** prove that new datatypes have finite support ****)
     1.8 +
     1.9 +    val indnames = DatatypeProp.make_tnames recTs;
    1.10 +
    1.11 +    val abs_supp = PureThy.get_thms thy8 (Name "abs_supp");
    1.12 +    val supp_at = PureThy.get_thms thy8 (Name "supp_at");
    1.13 +
    1.14 +    val finite_supp_thms = map (fn atom =>
    1.15 +      let val atomT = Type (atom, [])
    1.16 +      in map standard (List.take
    1.17 +        (split_conj_thm (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop
    1.18 +           (foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem
    1.19 +             (Const ("nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
    1.20 +              Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT))))
    1.21 +               (indnames ~~ recTs))))
    1.22 +           (fn _ => indtac dt_induct indnames 1 THEN
    1.23 +            ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
    1.24 +              (abs_supp @ supp_at @
    1.25 +               PureThy.get_thms thy8 (Name ("fs_" ^ Sign.base_name atom ^ "1")) @
    1.26 +               List.concat supp_thms))))),
    1.27 +         length new_type_names))
    1.28 +      end) atoms;
    1.29 +
    1.30      val (thy9, _) = thy8 |>
    1.31        Theory.add_path big_name |>
    1.32        PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>>
    1.33 @@ -1904,7 +1927,14 @@
    1.34        DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>>
    1.35        DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>>
    1.36        DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>>
    1.37 -      DatatypeAux.store_thmss "fresh" new_type_names fresh_thms;
    1.38 +      DatatypeAux.store_thmss "fresh" new_type_names fresh_thms |>>
    1.39 +      fold (fn (atom, ths) => fn thy =>
    1.40 +        let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
    1.41 +        in fold (fn T => AxClass.add_inst_arity_i
    1.42 +            (fst (dest_Type T),
    1.43 +              replicate (length sorts) [class], [class])
    1.44 +            (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
    1.45 +        end) (atoms ~~ finite_supp_thms);
    1.46  
    1.47    in
    1.48      (thy9, perm_eq_thms)