1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Nov 29 14:24:21 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Sun Dec 01 19:32:57 2013 +0100
     1.3 @@ -904,16 +904,28 @@
     1.4      val exclss'' = exclss' |> map (map (fn (idx, t) =>
     1.5        (idx, (Option.map (Goal.prove lthy [] [] t #> Thm.close_derivation) (excl_tac idx), t))));
     1.6      val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
     1.7 -    val (goal_idxss, goalss) = exclss''
     1.8 +    val (goal_idxss, goalss') = exclss''
     1.9        |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
    1.10        |> split_list o map split_list;
    1.11  
    1.12 -    val exhaustive_props = map (mk_disjs o map (mk_conjs o #prems)) disc_eqnss;
    1.13 +    val exh_props = if not exhaustive then [] else
    1.14 +      map (HOLogic.mk_Trueprop o mk_disjs o map (mk_conjs o #prems)) disc_eqnss
    1.15 +      |> map2 ((fn {fun_args, ...} =>
    1.16 +        curry Logic.list_all (map dest_Free fun_args)) o hd) disc_eqnss;
    1.17 +    val exh_taut_thms = if exhaustive andalso is_some maybe_tac then
    1.18 +        map (fn t => Goal.prove lthy [] [] t (the maybe_tac) |> Thm.close_derivation) exh_props
    1.19 +      else [];
    1.20 +    val goalss = if exhaustive andalso is_none maybe_tac then
    1.21 +      map (rpair []) exh_props :: goalss' else goalss';
    1.22  
    1.23 -    fun prove thmss' def_thms' lthy =
    1.24 +    fun prove thmss'' def_thms' lthy =
    1.25        let
    1.26          val def_thms = map (snd o snd) def_thms';
    1.27  
    1.28 +        val maybe_exh_thms = if exhaustive andalso is_none maybe_tac then
    1.29 +          map SOME (hd thmss'') else map (K NONE) def_thms;
    1.30 +        val thmss' = if exhaustive andalso is_none maybe_tac then tl thmss'' else thmss'';
    1.31 +
    1.32          val exclss' = map (op ~~) (goal_idxss ~~ thmss');
    1.33          fun mk_exclsss excls n =
    1.34            (excls, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1))
    1.35 @@ -1012,7 +1024,7 @@
    1.36                  |> single
    1.37              end;
    1.38  
    1.39 -        fun prove_code disc_eqns sel_eqns ctr_alist ctr_specs =
    1.40 +        fun prove_code disc_eqns sel_eqns maybe_exh ctr_alist ctr_specs =
    1.41            let
    1.42              val fun_data =
    1.43                (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
    1.44 @@ -1057,12 +1069,15 @@
    1.45                      in
    1.46                        if exists is_none maybe_ctr_conds_argss then NONE else
    1.47                          let
    1.48 -                          val rhs = fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t)
    1.49 -                            maybe_ctr_conds_argss
    1.50 -                            (Const (@{const_name Code.abort}, @{typ String.literal} -->
    1.51 -                                (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
    1.52 -                              HOLogic.mk_literal fun_name $
    1.53 -                              absdummy @{typ unit} (incr_boundvars 1 lhs));
    1.54 +                          val rhs = (if exhaustive then
    1.55 +                              split_last maybe_ctr_conds_argss ||> snd o the
    1.56 +                            else
    1.57 +                              Const (@{const_name Code.abort}, @{typ String.literal} -->
    1.58 +                                  (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
    1.59 +                                HOLogic.mk_literal fun_name $
    1.60 +                                absdummy @{typ unit} (incr_boundvars 1 lhs)
    1.61 +                              |> pair maybe_ctr_conds_argss)
    1.62 +                            |-> fold_rev (fn SOME (prems, u) => fn t => mk_If (s_conjs prems) u t)
    1.63                          in SOME (rhs, rhs, map snd ctr_alist) end
    1.64                      end);
    1.65                in
    1.66 @@ -1080,8 +1095,8 @@
    1.67                      val (distincts, discIs, sel_splits, sel_split_asms) =
    1.68                        case_thms_of_term lthy bound_Ts raw_rhs;
    1.69  
    1.70 -                    val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
    1.71 -                        sel_split_asms ms ctr_thms
    1.72 +                    val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs
    1.73 +                        sel_splits sel_split_asms ms ctr_thms maybe_exh
    1.74                        |> K |> Goal.prove lthy [] [] raw_t
    1.75                        |> Thm.close_derivation;
    1.76                    in
    1.77 @@ -1102,7 +1117,7 @@
    1.78            ctr_specss;
    1.79          val ctr_thmss = map (map snd) ctr_alists;
    1.80  
    1.81 -        val code_thmss = map4 prove_code disc_eqnss sel_eqnss ctr_alists ctr_specss;
    1.82 +        val code_thmss = map5 prove_code disc_eqnss sel_eqnss maybe_exh_thms ctr_alists ctr_specss;
    1.83  
    1.84          val simp_thmss = map2 append disc_thmss sel_thmss
    1.85  

     2.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Nov 29 14:24:21 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Sun Dec 01 19:32:57 2013 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4    val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     2.5      tactic
     2.6    val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
     2.7 -    thm list -> int list -> thm list -> tactic
     2.8 +    thm list -> int list -> thm list -> thm option -> tactic
     2.9    val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
    2.10      thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
    2.11  end;
    2.12 @@ -116,7 +116,8 @@
    2.13         (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
    2.14    end;
    2.15  
    2.16 -fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs =
    2.17 +(* TODO: implement "exhaustive" (maybe_exh) *)
    2.18 +fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs maybe_exh =
    2.19    EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) ms
    2.20      f_ctrs) THEN
    2.21    IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN