# HG changeset patch # User berghofe # Date 1130940322 -3600 # Node ID d1e47ee130705e63734655104e73ba53e4e31676 # Parent 16608ab6ed84c26e21535e3834d0842542eb1a6c Added code for proving that new datatype has finite support. diff -r 16608ab6ed84 -r d1e47ee13070 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Wed Nov 02 14:48:55 2005 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Wed Nov 02 15:05:22 2005 +0100 @@ -1895,6 +1895,29 @@ val case_names_induct = mk_case_names_induct (List.concat descr'); + (**** prove that new datatypes have finite support ****) + + val indnames = DatatypeProp.make_tnames recTs; + + val abs_supp = PureThy.get_thms thy8 (Name "abs_supp"); + val supp_at = PureThy.get_thms thy8 (Name "supp_at"); + + val finite_supp_thms = map (fn atom => + let val atomT = Type (atom, []) + in map standard (List.take + (split_conj_thm (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop + (foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem + (Const ("nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T), + Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT)))) + (indnames ~~ recTs)))) + (fn _ => indtac dt_induct indnames 1 THEN + ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps + (abs_supp @ supp_at @ + PureThy.get_thms thy8 (Name ("fs_" ^ Sign.base_name atom ^ "1")) @ + List.concat supp_thms))))), + length new_type_names)) + end) atoms; + val (thy9, _) = thy8 |> Theory.add_path big_name |> PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>> @@ -1904,7 +1927,14 @@ DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>> DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>> DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>> - DatatypeAux.store_thmss "fresh" new_type_names fresh_thms; + DatatypeAux.store_thmss "fresh" new_type_names fresh_thms |>> + fold (fn (atom, ths) => fn thy => + let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom) + in fold (fn T => AxClass.add_inst_arity_i + (fst (dest_Type T), + replicate (length sorts) [class], [class]) + (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy + end) (atoms ~~ finite_supp_thms); in (thy9, perm_eq_thms)