made new 'primrec' bootstrapping-capable
authorblanchet
Fri Sep 19 13:27:04 2014 +0200 (2014-09-19)
changeset 58389ee1f45ca0d73
parent 58388 4d408eb71301
child 58390 b74d8470b98e
made new 'primrec' bootstrapping-capable
src/HOL/Nat.thy
src/HOL/Product_Type.thy
src/HOL/Quickcheck_Random.thy
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
     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"
     2.1 --- a/src/HOL/Product_Type.thy	Fri Sep 19 13:27:04 2014 +0200
     2.2 +++ b/src/HOL/Product_Type.thy	Fri Sep 19 13:27:04 2014 +0200
     2.3 @@ -1342,6 +1342,7 @@
     2.4          end
     2.5      | _ => NONE)
     2.6  *}
     2.7 +
     2.8  ML_file "Tools/inductive_set.ML"
     2.9  
    2.10  
     3.1 --- a/src/HOL/Quickcheck_Random.thy	Fri Sep 19 13:27:04 2014 +0200
     3.2 +++ b/src/HOL/Quickcheck_Random.thy	Fri Sep 19 13:27:04 2014 +0200
     3.3 @@ -168,7 +168,7 @@
     3.4  instantiation set :: (random) random
     3.5  begin
     3.6  
     3.7 -primrec random_aux_set
     3.8 +fun random_aux_set
     3.9  where
    3.10    "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
    3.11  | "random_aux_set (Code_Numeral.Suc i) j =
     4.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
     4.3 @@ -39,16 +39,20 @@
     4.4    type lfp_rec_extension =
     4.5      {nested_simps: thm list,
     4.6       is_new_datatype: Proof.context -> string -> bool,
     4.7 -     get_basic_lfp_sugars: binding list -> typ list -> term list ->
     4.8 +     basic_lfp_sugars_of: binding list -> typ list -> term list ->
     4.9         (term * term list list) list list -> local_theory ->
    4.10         typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * Token.src list
    4.11         * bool * local_theory,
    4.12 -     rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
    4.13 -       term -> term -> term -> term};
    4.14 +     rewrite_nested_rec_call: (Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
    4.15 +       term -> term -> term -> term) option};
    4.16  
    4.17    exception PRIMREC of string * term list;
    4.18  
    4.19    val register_lfp_rec_extension: lfp_rec_extension -> theory -> theory
    4.20 +  val default_basic_lfp_sugars_of: binding list -> typ list -> term list ->
    4.21 +    (term * term list list) list list -> local_theory ->
    4.22 +    typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * Token.src list * bool
    4.23 +    * local_theory
    4.24    val rec_specs_of: binding list -> typ list -> typ list -> term list ->
    4.25      (term * term list list) list list -> local_theory ->
    4.26      (bool * rec_spec list * typ list * thm * thm list * Token.src list) * local_theory
    4.27 @@ -115,12 +119,12 @@
    4.28  type lfp_rec_extension =
    4.29    {nested_simps: thm list,
    4.30     is_new_datatype: Proof.context -> string -> bool,
    4.31 -   get_basic_lfp_sugars: binding list -> typ list -> term list ->
    4.32 +   basic_lfp_sugars_of: binding list -> typ list -> term list ->
    4.33       (term * term list list) list list -> local_theory ->
    4.34       typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * Token.src list * bool
    4.35       * local_theory,
    4.36 -   rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
    4.37 -     term -> term -> term -> term};
    4.38 +   rewrite_nested_rec_call: (Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
    4.39 +     term -> term -> term -> term) option};
    4.40  
    4.41  structure Data = Theory_Data
    4.42  (
    4.43 @@ -140,16 +144,35 @@
    4.44  fun is_new_datatype ctxt =
    4.45    (case Data.get (Proof_Context.theory_of ctxt) of
    4.46      SOME {is_new_datatype, ...} => is_new_datatype ctxt
    4.47 -  | NONE => K false);
    4.48 +  | NONE => K true);
    4.49 +
    4.50 +fun default_basic_lfp_sugars_of _ [Type (arg_T_name, _)] _ _ ctxt =
    4.51 +    let
    4.52 +      val ctr_sugar as {T, ctrs, casex, case_thms, ...} =
    4.53 +        (case ctr_sugar_of ctxt arg_T_name of
    4.54 +          SOME ctr_sugar => ctr_sugar
    4.55 +        | NONE => error ("Unsupported type " ^ quote arg_T_name ^ " at this stage"));
    4.56 +
    4.57 +      val C = body_type (fastype_of casex);
    4.58 +      val fun_arg_Tsss = map (map single o binder_types o fastype_of) ctrs;
    4.59  
    4.60 -fun get_basic_lfp_sugars bs arg_Ts callers callssss lthy =
    4.61 +      val basic_lfp_sugar =
    4.62 +        {T = T, fp_res_index = 0, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
    4.63 +         recx = casex, rec_thms = case_thms};
    4.64 +    in
    4.65 +      ([], [0], [basic_lfp_sugar], [], [], TrueI, [], false, ctxt)
    4.66 +    end
    4.67 +  | default_basic_lfp_sugars_of _ _ _ _ _ = error "Unsupported mutual recursion at this stage";
    4.68 +
    4.69 +fun basic_lfp_sugars_of bs arg_Ts callers callssss lthy =
    4.70    (case Data.get (Proof_Context.theory_of lthy) of
    4.71 -    SOME {get_basic_lfp_sugars, ...} => get_basic_lfp_sugars bs arg_Ts callers callssss lthy
    4.72 -  | NONE => error "Functionality not loaded yet");
    4.73 +    SOME {basic_lfp_sugars_of, ...} => basic_lfp_sugars_of
    4.74 +  | NONE => default_basic_lfp_sugars_of) bs arg_Ts callers callssss lthy;
    4.75  
    4.76  fun rewrite_nested_rec_call ctxt =
    4.77    (case Data.get (Proof_Context.theory_of ctxt) of
    4.78 -    SOME {rewrite_nested_rec_call, ...} => rewrite_nested_rec_call ctxt);
    4.79 +    SOME {rewrite_nested_rec_call = SOME f, ...} => f ctxt
    4.80 +  | _ => error "Unsupported nested recursion");
    4.81  
    4.82  fun rec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
    4.83    let
    4.84 @@ -157,7 +180,7 @@
    4.85  
    4.86      val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_ident0s, fp_nesting_map_comps,
    4.87           common_induct, induct_attrs, n2m, lthy) =
    4.88 -      get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
    4.89 +      basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0;
    4.90  
    4.91      val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
    4.92  
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 19 13:27:04 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 19 13:27:04 2014 +0200
     5.3 @@ -16,46 +16,51 @@
     5.4  open BNF_FP_N2M_Sugar
     5.5  open BNF_LFP_Rec_Sugar
     5.6  
     5.7 +(* FIXME: remove "nat" cases throughout once it is registered as a datatype *)
     5.8 +
     5.9  val nested_simps = @{thms o_def[abs_def] id_def split fst_conv snd_conv};
    5.10  
    5.11 -fun is_new_datatype ctxt s =
    5.12 -  (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
    5.13 +fun is_new_datatype _ @{type_name nat} = true
    5.14 +  | is_new_datatype ctxt s =
    5.15 +    (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
    5.16  
    5.17  fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_sugar, co_rec = recx,
    5.18      co_rec_thms = rec_thms, ...} : fp_sugar) =
    5.19    {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
    5.20     recx = recx, rec_thms = rec_thms};
    5.21  
    5.22 -fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
    5.23 -  let
    5.24 -    val ((missing_arg_Ts, perm0_kks,
    5.25 -          fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
    5.26 -          (lfp_sugar_thms, _)), lthy) =
    5.27 -      nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
    5.28 +fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy =
    5.29 +    ([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, lthy)
    5.30 +  | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 =
    5.31 +    let
    5.32 +      val ((missing_arg_Ts, perm0_kks,
    5.33 +            fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
    5.34 +            (lfp_sugar_thms, _)), lthy) =
    5.35 +        nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
    5.36  
    5.37 -    val induct_attrs = (case lfp_sugar_thms of SOME ((_, _, attrs), _) => attrs | NONE => []);
    5.38 +      val induct_attrs = (case lfp_sugar_thms of SOME ((_, _, attrs), _) => attrs | NONE => []);
    5.39  
    5.40 -    val Ts = map #T fp_sugars;
    5.41 -    val Xs = map #X fp_sugars;
    5.42 -    val Cs = map (body_type o fastype_of o #co_rec) fp_sugars;
    5.43 -    val Xs_TCs = Xs ~~ (Ts ~~ Cs);
    5.44 +      val Ts = map #T fp_sugars;
    5.45 +      val Xs = map #X fp_sugars;
    5.46 +      val Cs = map (body_type o fastype_of o #co_rec) fp_sugars;
    5.47 +      val Xs_TCs = Xs ~~ (Ts ~~ Cs);
    5.48  
    5.49 -    fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)]
    5.50 -      | zip_recT U =
    5.51 -        (case AList.lookup (op =) Xs_TCs U of
    5.52 -          SOME (T, C) => [T, C]
    5.53 -        | NONE => [U]);
    5.54 +      fun zip_XrecT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_XrecT) Us)]
    5.55 +        | zip_XrecT U =
    5.56 +          (case AList.lookup (op =) Xs_TCs U of
    5.57 +            SOME (T, C) => [T, C]
    5.58 +          | NONE => [U]);
    5.59  
    5.60 -    val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
    5.61 -    val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss;
    5.62 +      val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
    5.63 +      val fun_arg_Tssss = map (map (map zip_XrecT)) ctrXs_Tsss;
    5.64  
    5.65 -    val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
    5.66 -    val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
    5.67 -  in
    5.68 -    (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
    5.69 -     fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs,
    5.70 -     is_some lfp_sugar_thms, lthy)
    5.71 -  end;
    5.72 +      val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
    5.73 +      val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
    5.74 +    in
    5.75 +      (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
    5.76 +       fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs,
    5.77 +       is_some lfp_sugar_thms, lthy)
    5.78 +    end;
    5.79  
    5.80  exception NO_MAP of term;
    5.81  
    5.82 @@ -162,6 +167,7 @@
    5.83  
    5.84  val _ = Theory.setup (register_lfp_rec_extension
    5.85    {nested_simps = nested_simps, is_new_datatype = is_new_datatype,
    5.86 -   get_basic_lfp_sugars = get_basic_lfp_sugars, rewrite_nested_rec_call = rewrite_nested_rec_call});
    5.87 +   basic_lfp_sugars_of = basic_lfp_sugars_of,
    5.88 +   rewrite_nested_rec_call = SOME rewrite_nested_rec_call});
    5.89  
    5.90  end;