src/HOL/Nat.thy
changeset 58389 ee1f45ca0d73
parent 58377 c6f93b8d2d8e
child 58647 fce800afeec7
     1.1 --- a/src/HOL/Nat.thy	Fri Sep 19 13:27:04 2014 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Sep 19 13:27:04 2014 +0200
     1.3 @@ -152,6 +152,31 @@
     1.4    nat_exhaust
     1.5    nat_induct0
     1.6  
     1.7 +ML {*
     1.8 +val nat_basic_lfp_sugar =
     1.9 +  let
    1.10 +    val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global @{theory} @{type_name nat});
    1.11 +    val recx = Logic.varify_types_global @{term rec_nat};
    1.12 +    val C = body_type (fastype_of recx);
    1.13 +  in
    1.14 +    {T = HOLogic.natT, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[HOLogic.natT, C]]],
    1.15 +     ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms nat.rec}}
    1.16 +  end;
    1.17 +*}
    1.18 +
    1.19 +setup {*
    1.20 +let
    1.21 +  fun basic_lfp_sugars_of _ [@{typ nat}] _ _ ctxt =
    1.22 +      ([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, ctxt)
    1.23 +    | basic_lfp_sugars_of bs arg_Ts callers callssss ctxt =
    1.24 +      BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt;
    1.25 +in
    1.26 +  BNF_LFP_Rec_Sugar.register_lfp_rec_extension
    1.27 +    {nested_simps = [], is_new_datatype = K (K true), basic_lfp_sugars_of = basic_lfp_sugars_of,
    1.28 +     rewrite_nested_rec_call = NONE}
    1.29 +end
    1.30 +*}
    1.31 +
    1.32  text {* Injectiveness and distinctness lemmas *}
    1.33  
    1.34  lemma inj_Suc[simp]: "inj_on Suc N"