--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Wed Dec 18 22:55:20 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Wed Dec 18 22:55:43 2013 +0100
@@ -488,6 +488,8 @@
ctr: term,
sel: term,
rhs_term: term,
+ maybe_ctr_rhs: term option,
+ maybe_code_rhs: term option,
user_eqn: term
};
@@ -557,8 +559,8 @@
}, matchedsss')
end;
-fun dissect_coeqn_sel fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn'
- maybe_of_spec eqn =
+fun dissect_coeqn_sel fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) maybe_ctr_rhs
+ maybe_code_rhs eqn' maybe_of_spec eqn =
let
val (lhs, rhs) = HOLogic.dest_eq eqn
handle TERM _ =>
@@ -584,6 +586,8 @@
ctr = ctr,
sel = sel,
rhs_term = rhs,
+ maybe_ctr_rhs = maybe_ctr_rhs,
+ maybe_code_rhs = maybe_code_rhs,
user_eqn = user_eqn
}
end;
@@ -616,7 +620,8 @@
*)
val eqns_data_sel =
- map (dissect_coeqn_sel fun_names basic_ctr_specss eqn' (SOME ctr)) sel_concls;
+ map (dissect_coeqn_sel fun_names basic_ctr_specss
+ (SOME (abstract (List.rev fun_args) rhs)) maybe_code_rhs eqn' (SOME ctr)) sel_concls;
in
(the_list maybe_eqn_data_disc @ eqns_data_sel, matchedsss')
end;
@@ -670,7 +675,7 @@
dissect_coeqn_disc seq fun_names basic_ctr_specss NONE NONE prems concl matchedsss
|>> single
else if member (op =) sels head then
- ([dissect_coeqn_sel fun_names basic_ctr_specss eqn' maybe_of_spec concl], matchedsss)
+ ([dissect_coeqn_sel fun_names basic_ctr_specss NONE NONE eqn' maybe_of_spec concl], matchedsss)
else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso
member (op =) ctrs (head_of (unfold_let (the maybe_rhs))) then
dissect_coeqn_ctr seq fun_names basic_ctr_specss eqn' NONE prems concl matchedsss
@@ -765,7 +770,9 @@
val ctr_specss = map #ctr_specs corec_specs;
val corec_args = hd corecs
|> fst o split_last o binder_types o fastype_of
- |> map (Const o pair @{const_name undefined})
+ |> map (fn T => if range_type T = @{typ bool}
+ then Abs (Name.uu_, domain_type T, @{term False})
+ else Const (@{const_name undefined}, T))
|> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
|> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss;
fun currys [] t = t
@@ -805,6 +812,7 @@
|> 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 maybe_sel_eqn = find_first (equal (Binding.name_of fun_binding) o #fun_name) sel_eqns;
val extra_disc_eqn = {
fun_name = Binding.name_of fun_binding,
fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))),
@@ -814,8 +822,8 @@
disc = #disc (nth ctr_specs n),
prems = maps (s_not_conj o #prems) disc_eqns,
auto_gen = true,
- maybe_ctr_rhs = NONE,
- maybe_code_rhs = NONE,
+ maybe_ctr_rhs = Option.map #maybe_ctr_rhs maybe_sel_eqn |> the_default NONE,
+ maybe_code_rhs = Option.map #maybe_ctr_rhs maybe_sel_eqn |> the_default NONE,
user_eqn = undef_const};
in
chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
@@ -922,8 +930,8 @@
let
val def_thms = map (snd o snd) def_thms';
- val maybe_exh_thms = if exhaustive andalso is_none maybe_tac then
- map SOME (hd thmss'') else map (K NONE) def_thms;
+ val maybe_exh_thms = if not exhaustive then map (K NONE) def_thms else
+ map SOME (if is_none maybe_tac then hd thmss'' else exh_taut_thms);
val thmss' = if exhaustive andalso is_none maybe_tac then tl thmss'' else thmss'';
val exclss' = map (op ~~) (goal_idxss ~~ thmss');
@@ -1000,7 +1008,7 @@
(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,
#maybe_ctr_rhs x))
- ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], NONE))
+ ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #maybe_ctr_rhs x))
|> the o merge_options;
val m = length prems;
val t = (if is_some maybe_rhs then the maybe_rhs else
@@ -1030,7 +1038,7 @@
(find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns)
|>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x))
- ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, NONE))
+ ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #maybe_code_rhs x))
|> merge_options;
in
(case maybe_fun_data of
@@ -1070,6 +1078,8 @@
in
let
val rhs = (if exhaustive
+ orelse map_filter (try (fst o the)) maybe_ctr_conds_argss
+ |> forall (equal [])
orelse forall is_some maybe_ctr_conds_argss
andalso exists #auto_gen disc_eqns then
split_last (map_filter I maybe_ctr_conds_argss) ||> snd