generate more theorems (e.g. for types with only one constructor)

--- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 18 18:11:32 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 19 00:32:33 2013 +0200
@@ -1624,13 +1624,15 @@
 appears directly to the right of the equal sign:
 *}
 
-    primcorec_notyet literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
+    primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
       "literate f x = LCons x (literate f (f x))"
+    .
 
 text {* \blankline *}
 
-    primcorec_notyet siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
+    primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
       "siterate f x = SCons x (siterate f (f x))"
+    .
 
 text {*
 \noindent
@@ -1648,7 +1650,6 @@
 (*<*)
     locale dummy_dest_view
     begin
-end
 (*>*)
     primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
       "\<not> lnull (literate _ x)" |
@@ -1663,7 +1664,7 @@
       "stl (siterate f x) = siterate f (f x)"
     .
 (*<*)
-(*    end*)
+    end
 (*>*)
 
 text {*
@@ -1680,8 +1681,9 @@
 element in a stream:
 *}
 
-    primcorec_notyet every_snd :: "'a stream \<Rightarrow> 'a stream" where
+    primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
       "every_snd s = SCons (shd s) (stl (stl s))"
+    .
 
 text {*
 \noindent
@@ -1735,8 +1737,9 @@
 Corecursion is useful to specify not only functions but also infinite objects:
 *}
 
-    primcorec_notyet infty :: enat where
+    primcorec infty :: enat where
       "infty = ESuc infty"
+    .
 
 text {*
 \noindent
@@ -1818,12 +1821,13 @@
 datatypes is anything but surprising. Following the constructor view:
 *}
 
-    primcorec_notyet
+    primcorec
       even_infty :: even_enat and
       odd_infty :: odd_enat
     where
       "even_infty = Even_ESuc odd_infty" |
       "odd_infty = Odd_ESuc even_infty"
+    .
 
 text {*
 And following the destructor view:
@@ -1856,13 +1860,15 @@
 tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}):
 *}
 
-    primcorec_notyet iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
+    primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
       "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))"
+    .
 
 text {* \blankline *}
 
-    primcorec_notyet iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
+    primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
       "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fmap (iterate\<^sub>i\<^sub>s f) (f x))"
+    .
 
 text {*
 Again, let us not forget our destructor-oriented passengers. Here is the first
@@ -1889,8 +1895,9 @@
 function translates a DFA into a @{type state_machine}:
 *}
 
-    primcorec_notyet of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine" where
+    primcorec of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine" where
       "of_dfa \<delta> F q = State_Machine (q \<in> F) (of_dfa \<delta> F o \<delta> q)"
+    .
 
 
 subsubsection {* Nested-as-Mutual Corecursion

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 18 18:11:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 00:32:33 2013 +0200
@@ -661,15 +661,17 @@
     |> rpair exclss'
   end;
 
-fun mk_real_disc_eqns fun_binding arg_Ts {ctr_specs, ...} disc_eqns =
+fun mk_real_disc_eqns fun_binding arg_Ts {ctr_specs, ...} sel_eqns disc_eqns =
   if length disc_eqns <> length ctr_specs - 1 then disc_eqns else
     let
       val n = 0 upto length ctr_specs
         |> the o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns));
+      val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns)
+        |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options;
       val extra_disc_eqn = {
         fun_name = Binding.name_of fun_binding,
         fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))),
-        fun_args = the_default (map (curry Free Name.uu) arg_Ts) (try (#fun_args o hd) disc_eqns),
+        fun_args = fun_args,
         ctr = #ctr (nth ctr_specs n),
         ctr_no = n,
         disc = #disc (nth ctr_specs n),
@@ -718,7 +720,7 @@
 
     val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
     val arg_Tss = map (binder_types o snd o fst) fixes;
-    val disc_eqnss = map4 mk_real_disc_eqns bs arg_Tss corec_specs disc_eqnss';
+    val disc_eqnss = map5 mk_real_disc_eqns bs arg_Tss corec_specs sel_eqnss disc_eqnss';
     val (defs, exclss') =
       co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
 
@@ -744,13 +746,12 @@
 
         fun prove_disc {ctr_specs, ...} exclsss
             {fun_name, fun_T, fun_args, ctr_no, prems, user_eqn, ...} =
-          if user_eqn = undef_const then [] else
+          if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then [] else
             let
-              val disc_corec = nth ctr_specs ctr_no |> #disc_corec;
+              val {disc_corec, ...} = nth ctr_specs ctr_no;
               val k = 1 + ctr_no;
               val m = length prems;
               val t =
-                (* FIXME use applied_fun from dissect_\<dots> instead? *)
                 list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0))
                 |> curry betapply (#disc (nth ctr_specs ctr_no)) (*###*)
                 |> HOLogic.mk_Trueprop
@@ -790,22 +791,24 @@
 
         fun prove_ctr (_, disc_thms) (_, sel_thms') disc_eqns sel_eqns
             {ctr, disc, sels, collapse, ...} =
+let val _ = tracing ("disc = " ^ @{make_string} disc); in
           if not (exists (equal ctr o #ctr) disc_eqns)
-andalso (warning ("no disc_eqn for ctr " ^ Syntax.string_of_term lthy ctr); true)
-            orelse (* don't try to prove theorems where some sel_eqns are missing *)
+              andalso not (exists (equal ctr o #ctr) sel_eqns)
+andalso (warning ("no eqns for ctr " ^ Syntax.string_of_term lthy ctr); true)
+            orelse (* don't try to prove theorems when some sel_eqns are missing *)
               filter (equal ctr o #ctr) sel_eqns
               |> fst o finds ((op =) o apsnd #sel) sels
               |> exists (null o snd)
 andalso (warning ("sel_eqn(s) missing for ctr " ^ Syntax.string_of_term lthy ctr); true)
-            orelse
-              #user_eqn (the (find_first (equal ctr o #ctr) disc_eqns)) = undef_const
-andalso (warning ("auto-generated disc_eqn for ctr " ^ Syntax.string_of_term lthy ctr); true)
           then [] else
             let
 val _ = tracing ("ctr = " ^ Syntax.string_of_term lthy ctr);
-val _ = tracing ("disc = " ^ Syntax.string_of_term lthy (#disc (the (find_first (equal ctr o #ctr) disc_eqns))));
-              val {fun_name, fun_T, fun_args, prems, ...} =
-                the (find_first (equal ctr o #ctr) disc_eqns);
+val _ = tracing (the_default "NO disc_eqn" (Option.map (curry (op ^) "disc = " o Syntax.string_of_term lthy o #disc) (find_first (equal ctr o #ctr) disc_eqns)));
+              val (fun_name, fun_T, fun_args, prems) =
+                (find_first (equal ctr o #ctr) disc_eqns, find_first (equal ctr o #ctr) sel_eqns)
+                |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x))
+                ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, []))
+                |> the o merge_options;
               val m = length prems;
               val t = sel_eqns
                 |> fst o finds ((op =) o apsnd #sel) sels
@@ -816,17 +819,19 @@
                 |> HOLogic.mk_Trueprop
                 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
                 |> curry Logic.list_all (map dest_Free fun_args);
-              val disc_thm = the_default TrueI (AList.lookup (op =) disc_thms disc);
+              val maybe_disc_thm = AList.lookup (op =) disc_thms disc;
               val sel_thms = map snd (filter (member (op =) sels o fst) sel_thms');
 val _ = tracing ("t = " ^ Syntax.string_of_term lthy t);
 val _ = tracing ("m = " ^ @{make_string} m);
 val _ = tracing ("collapse = " ^ @{make_string} collapse);
-val _ = tracing ("disc_thm = " ^ @{make_string} disc_thm);
+val _ = tracing ("maybe_disc_thm = " ^ @{make_string} maybe_disc_thm);
 val _ = tracing ("sel_thms = " ^ @{make_string} sel_thms);
             in
-              mk_primcorec_ctr_of_dtr_tac lthy m collapse disc_thm sel_thms
+              mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms
               |> K |> Goal.prove lthy [] [] t
               |> single
+(*handle ERROR x => (warning x; []))*)
+end
           end;
 
         val (disc_notes, disc_thmss) =

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 18:11:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 19 00:32:33 2013 +0200
@@ -10,7 +10,7 @@
   val mk_primcorec_assumption_tac: Proof.context -> tactic
   val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic
   val mk_primcorec_code_of_ctr_tac: Proof.context -> int list -> thm list -> tactic
-  val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
+  val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
   val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
     thm list list list -> thm list -> thm list -> thm list -> tactic
   val mk_primcorec_disc_of_ctr_tac: thm -> thm -> tactic;
@@ -63,9 +63,9 @@
     if_cancel[of _ False] o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
   HEADGOAL (rtac refl);
 
-fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc_f sel_fs =
+fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
   HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'
-    rtac disc_f THEN' REPEAT_DETERM_N m o atac) THEN
+    (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
   unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
 
 fun mk_primcorec_disc_of_ctr_tac discI f_ctr =