# HG changeset patch # User blanchet # Date 1392190556 -3600 # Node ID f33235c7a93e80e417581c8de109bc6994dbd381 # Parent f3353672399936e246d1b23c04a1d4d8f4c63177 tuned code diff -r f33536723999 -r f33235c7a93e src/HOL/Tools/Datatype/rep_datatype.ML --- a/src/HOL/Tools/Datatype/rep_datatype.ML Wed Feb 12 08:35:56 2014 +0100 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Wed Feb 12 08:35:56 2014 +0100 @@ -292,44 +292,45 @@ (* define case combinators via primrec combinators *) - val (case_defs, thy2) = - fold (fn ((((i, (_, _, constrs)), T), name), recname) => fn (defs, thy) => + fun def_case ((((i, (_, _, constrs)), T), name), recname) (defs, thy) = + let + val (fns1, fns2) = split_list (map (fn ((_, cargs), j) => let - val (fns1, fns2) = split_list (map (fn ((_, cargs), j) => - let - val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs; - val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs); - val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts'); - val frees = take (length cargs) frees'; - val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j; - in - (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees))) - end) (constrs ~~ (1 upto length constrs))); + val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs; + val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs); + val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts'); + val frees = take (length cargs) frees'; + val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j; + in + (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees))) + end) (constrs ~~ (1 upto length constrs))); - val caseT = map (snd o dest_Free) fns1 @ [T] ---> T'; - val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns); - val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T'); - val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn); - val def = - (Binding.name (Thm.def_name (Long_Name.base_name name)), - Logic.mk_equals (Const (name, caseT), - fold_rev lambda fns1 - (list_comb (reccomb, - flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns))))); - val ([def_thm], thy') = - thy - |> Sign.declare_const_global decl |> snd - |> (Global_Theory.add_defs false o map Thm.no_attributes) [def]; + val caseT = map (snd o dest_Free) fns1 @ [T] ---> T'; + val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns); + val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T'); + val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn); + val def = + (Binding.name (Thm.def_name (Long_Name.base_name name)), + Logic.mk_equals (Const (name, caseT), + fold_rev lambda fns1 + (list_comb (reccomb, + flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns))))); + val ([def_thm], thy') = + thy + |> Sign.declare_const_global decl |> snd + |> (Global_Theory.add_defs false o map Thm.no_attributes) [def]; + in (defs @ [def_thm], thy') end; - in (defs @ [def_thm], thy') end) - (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) ([], thy1); + val (case_defs, thy2) = + fold def_case (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) + ([], thy1); + + fun prove_case _ t = + Goal.prove_sorry_global thy2 [] [] t (fn {context = ctxt, ...} => + EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]); val case_thms = - (map o map) (fn t => - Goal.prove_sorry_global thy2 [] [] t - (fn {context = ctxt, ...} => - EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])) - (Datatype_Prop.make_cases case_names descr thy2); + map2 (map o prove_case) new_type_names (Datatype_Prop.make_cases case_names descr thy2); in thy2 |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)