# HG changeset patch
# User blanchet
# Date 1411126024 -7200
# Node ID ee1f45ca0d73fe0f706f87e28959fe8620d06211
# Parent  4d408eb71301608e299191ebb6f17d8608fe533c
made new 'primrec' bootstrapping-capable

diff -r 4d408eb71301 -r ee1f45ca0d73 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Nat.thy	Fri Sep 19 13:27:04 2014 +0200
@@ -152,6 +152,31 @@
   nat_exhaust
   nat_induct0
 
+ML {*
+val nat_basic_lfp_sugar =
+  let
+    val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global @{theory} @{type_name nat});
+    val recx = Logic.varify_types_global @{term rec_nat};
+    val C = body_type (fastype_of recx);
+  in
+    {T = HOLogic.natT, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[HOLogic.natT, C]]],
+     ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms nat.rec}}
+  end;
+*}
+
+setup {*
+let
+  fun basic_lfp_sugars_of _ [@{typ nat}] _ _ ctxt =
+      ([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, ctxt)
+    | basic_lfp_sugars_of bs arg_Ts callers callssss ctxt =
+      BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt;
+in
+  BNF_LFP_Rec_Sugar.register_lfp_rec_extension
+    {nested_simps = [], is_new_datatype = K (K true), basic_lfp_sugars_of = basic_lfp_sugars_of,
+     rewrite_nested_rec_call = NONE}
+end
+*}
+
 text {* Injectiveness and distinctness lemmas *}
 
 lemma inj_Suc[simp]: "inj_on Suc N"
diff -r 4d408eb71301 -r ee1f45ca0d73 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Product_Type.thy	Fri Sep 19 13:27:04 2014 +0200
@@ -1342,6 +1342,7 @@
         end
     | _ => NONE)
 *}
+
 ML_file "Tools/inductive_set.ML"
 
 
diff -r 4d408eb71301 -r ee1f45ca0d73 src/HOL/Quickcheck_Random.thy
--- a/src/HOL/Quickcheck_Random.thy	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Quickcheck_Random.thy	Fri Sep 19 13:27:04 2014 +0200
@@ -168,7 +168,7 @@
 instantiation set :: (random) random
 begin
 
-primrec random_aux_set
+fun random_aux_set
 where
   "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
 | "random_aux_set (Code_Numeral.Suc i) j =
diff -r 4d408eb71301 -r ee1f45ca0d73 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
@@ -39,16 +39,20 @@
   type lfp_rec_extension =
     {nested_simps: thm list,
      is_new_datatype: Proof.context -> string -> bool,
-     get_basic_lfp_sugars: binding list -> typ list -> term list ->
+     basic_lfp_sugars_of: binding list -> typ list -> term list ->
        (term * term list list) list list -> local_theory ->
        typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * Token.src list
        * bool * local_theory,
-     rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
-       term -> term -> term -> term};
+     rewrite_nested_rec_call: (Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
+       term -> term -> term -> term) option};
 
   exception PRIMREC of string * term list;
 
   val register_lfp_rec_extension: lfp_rec_extension -> theory -> theory
+  val default_basic_lfp_sugars_of: binding list -> typ list -> term list ->
+    (term * term list list) list list -> local_theory ->
+    typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * Token.src list * bool
+    * local_theory
   val rec_specs_of: binding list -> typ list -> typ list -> term list ->
     (term * term list list) list list -> local_theory ->
     (bool * rec_spec list * typ list * thm * thm list * Token.src list) * local_theory
@@ -115,12 +119,12 @@
 type lfp_rec_extension =
   {nested_simps: thm list,
    is_new_datatype: Proof.context -> string -> bool,
-   get_basic_lfp_sugars: binding list -> typ list -> term list ->
+   basic_lfp_sugars_of: binding list -> typ list -> term list ->
      (term * term list list) list list -> local_theory ->
      typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * Token.src list * bool
      * local_theory,
-   rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
-     term -> term -> term -> term};
+   rewrite_nested_rec_call: (Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
+     term -> term -> term -> term) option};
 
 structure Data = Theory_Data
 (
@@ -140,16 +144,35 @@
 fun is_new_datatype ctxt =
   (case Data.get (Proof_Context.theory_of ctxt) of
     SOME {is_new_datatype, ...} => is_new_datatype ctxt
-  | NONE => K false);
+  | NONE => K true);
+
+fun default_basic_lfp_sugars_of _ [Type (arg_T_name, _)] _ _ ctxt =
+    let
+      val ctr_sugar as {T, ctrs, casex, case_thms, ...} =
+        (case ctr_sugar_of ctxt arg_T_name of
+          SOME ctr_sugar => ctr_sugar
+        | NONE => error ("Unsupported type " ^ quote arg_T_name ^ " at this stage"));
+
+      val C = body_type (fastype_of casex);
+      val fun_arg_Tsss = map (map single o binder_types o fastype_of) ctrs;
 
-fun get_basic_lfp_sugars bs arg_Ts callers callssss lthy =
+      val basic_lfp_sugar =
+        {T = T, fp_res_index = 0, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
+         recx = casex, rec_thms = case_thms};
+    in
+      ([], [0], [basic_lfp_sugar], [], [], TrueI, [], false, ctxt)
+    end
+  | default_basic_lfp_sugars_of _ _ _ _ _ = error "Unsupported mutual recursion at this stage";
+
+fun basic_lfp_sugars_of bs arg_Ts callers callssss lthy =
   (case Data.get (Proof_Context.theory_of lthy) of
-    SOME {get_basic_lfp_sugars, ...} => get_basic_lfp_sugars bs arg_Ts callers callssss lthy
-  | NONE => error "Functionality not loaded yet");
+    SOME {basic_lfp_sugars_of, ...} => basic_lfp_sugars_of
+  | NONE => default_basic_lfp_sugars_of) bs arg_Ts callers callssss lthy;
 
 fun rewrite_nested_rec_call ctxt =
   (case Data.get (Proof_Context.theory_of ctxt) of
-    SOME {rewrite_nested_rec_call, ...} => rewrite_nested_rec_call ctxt);
+    SOME {rewrite_nested_rec_call = SOME f, ...} => f ctxt
+  | _ => error "Unsupported nested recursion");
 
 fun rec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
   let
@@ -157,7 +180,7 @@
 
     val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_ident0s, fp_nesting_map_comps,
          common_induct, induct_attrs, n2m, lthy) =
-      get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
+      basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0;
 
     val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
 
diff -r 4d408eb71301 -r ee1f45ca0d73 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Sep 19 13:27:04 2014 +0200
@@ -16,46 +16,51 @@
 open BNF_FP_N2M_Sugar
 open BNF_LFP_Rec_Sugar
 
+(* FIXME: remove "nat" cases throughout once it is registered as a datatype *)
+
 val nested_simps = @{thms o_def[abs_def] id_def split fst_conv snd_conv};
 
-fun is_new_datatype ctxt s =
-  (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
+fun is_new_datatype _ @{type_name nat} = true
+  | is_new_datatype ctxt s =
+    (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
 
 fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_sugar, co_rec = recx,
     co_rec_thms = rec_thms, ...} : fp_sugar) =
   {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
    recx = recx, rec_thms = rec_thms};
 
-fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
-  let
-    val ((missing_arg_Ts, perm0_kks,
-          fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
-          (lfp_sugar_thms, _)), lthy) =
-      nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
+fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy =
+    ([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, lthy)
+  | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 =
+    let
+      val ((missing_arg_Ts, perm0_kks,
+            fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
+            (lfp_sugar_thms, _)), lthy) =
+        nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
 
-    val induct_attrs = (case lfp_sugar_thms of SOME ((_, _, attrs), _) => attrs | NONE => []);
+      val induct_attrs = (case lfp_sugar_thms of SOME ((_, _, attrs), _) => attrs | NONE => []);
 
-    val Ts = map #T fp_sugars;
-    val Xs = map #X fp_sugars;
-    val Cs = map (body_type o fastype_of o #co_rec) fp_sugars;
-    val Xs_TCs = Xs ~~ (Ts ~~ Cs);
+      val Ts = map #T fp_sugars;
+      val Xs = map #X fp_sugars;
+      val Cs = map (body_type o fastype_of o #co_rec) fp_sugars;
+      val Xs_TCs = Xs ~~ (Ts ~~ Cs);
 
-    fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)]
-      | zip_recT U =
-        (case AList.lookup (op =) Xs_TCs U of
-          SOME (T, C) => [T, C]
-        | NONE => [U]);
+      fun zip_XrecT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_XrecT) Us)]
+        | zip_XrecT U =
+          (case AList.lookup (op =) Xs_TCs U of
+            SOME (T, C) => [T, C]
+          | NONE => [U]);
 
-    val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
-    val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss;
+      val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
+      val fun_arg_Tssss = map (map (map zip_XrecT)) ctrXs_Tsss;
 
-    val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
-    val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
-  in
-    (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
-     fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs,
-     is_some lfp_sugar_thms, lthy)
-  end;
+      val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
+      val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
+    in
+      (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
+       fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs,
+       is_some lfp_sugar_thms, lthy)
+    end;
 
 exception NO_MAP of term;
 
@@ -162,6 +167,7 @@
 
 val _ = Theory.setup (register_lfp_rec_extension
   {nested_simps = nested_simps, is_new_datatype = is_new_datatype,
-   get_basic_lfp_sugars = get_basic_lfp_sugars, rewrite_nested_rec_call = rewrite_nested_rec_call});
+   basic_lfp_sugars_of = basic_lfp_sugars_of,
+   rewrite_nested_rec_call = SOME rewrite_nested_rec_call});
 
 end;