--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 10 15:48:13 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 10 16:11:01 2014 +0100
@@ -1172,7 +1172,8 @@
val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs;
val cond_ctrs =
fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs [];
- val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
+ val ctr_thms =
+ map (the_default FalseE o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
in SOME (false, rhs, raw_rhs, ctr_thms) end
| NONE =>
let
@@ -1221,13 +1222,13 @@
val (distincts, discIs, sel_splits, sel_split_asms) =
case_thms_of_term lthy bound_Ts raw_rhs;
- val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs
- sel_splits sel_split_asms ms ctr_thms
+ val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs sel_splits
+ sel_split_asms ms ctr_thms
(if exhaustive_code then try the_single nchotomys else NONE)
|> K |> Goal.prove_sorry lthy [] [] raw_goal
|> Thm.close_derivation;
in
- mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
+ mk_primcorec_code_tac lthy distincts sel_splits raw_code_thm
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
|> single
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Fri Jan 10 15:48:13 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Fri Jan 10 16:11:01 2014 +0100
@@ -8,7 +8,7 @@
signature BNF_GFP_REC_SUGAR_TACTICS =
sig
val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
- val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
+ val mk_primcorec_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
val mk_primcorec_ctr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
tactic
@@ -16,8 +16,8 @@
thm list -> tactic
val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic
val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic
- val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
- thm list -> int list -> thm list -> thm option -> tactic
+ val mk_primcorec_raw_code_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
+ int list -> thm list -> thm option -> tactic
val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
end;
@@ -157,7 +157,7 @@
end
| _ => split);
-fun raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
+fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
let
val splits' =
map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
@@ -177,8 +177,7 @@
fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
-fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms fun_ctrs
- nchotomy_opt =
+fun mk_primcorec_raw_code_tac ctxt distincts discIs splits split_asms ms fun_ctrs nchotomy_opt =
let
val n = length ms;
val (ms', fun_ctrs') =
@@ -192,13 +191,12 @@
||> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm])
|> op @));
in
- EVERY (map2 (raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
- ms' fun_ctrs') THEN
+ EVERY (map2 (raw_code_single_tac ctxt distincts discIs splits split_asms) ms' fun_ctrs') THEN
IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)))
end;
-fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw =
+fun mk_primcorec_code_tac ctxt distincts splits raw =
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
(rtac refl ORELSE' atac ORELSE'