--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Jul 20 14:05:29 2017 +0100
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Jul 20 16:28:43 2017 +0100
@@ -193,6 +193,9 @@
lemmas all_mem_range = all_mem_range1 all_mem_range2 all_mem_range3 all_mem_range4 all_mem_range5
all_mem_range6 all_mem_range7 all_mem_range8
+lemma pred_fun_True_id: "NO_MATCH id p \<Longrightarrow> pred_fun (\<lambda>x. True) p f = pred_fun (\<lambda>x. True) id (p \<circ> f)"
+ unfolding fun.pred_map unfolding comp_def id_def ..
+
ML_file "Tools/BNF/bnf_lfp_util.ML"
ML_file "Tools/BNF/bnf_lfp_tactics.ML"
ML_file "Tools/BNF/bnf_lfp.ML"
--- a/src/HOL/Nat.thy Thu Jul 20 14:05:29 2017 +0100
+++ b/src/HOL/Nat.thy Thu Jul 20 16:28:43 2017 +0100
@@ -163,8 +163,8 @@
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}
+ {nested_simps = [], special_endgame_tac = K (K (K (K no_tac))), is_new_datatype = K (K true),
+ basic_lfp_sugars_of = basic_lfp_sugars_of, rewrite_nested_rec_call = NONE}
end
\<close>
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Jul 20 14:05:29 2017 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Jul 20 16:28:43 2017 +0100
@@ -42,6 +42,7 @@
type lfp_rec_extension =
{nested_simps: thm list,
+ special_endgame_tac: Proof.context -> thm list -> thm list -> thm list -> tactic,
is_new_datatype: Proof.context -> string -> bool,
basic_lfp_sugars_of: binding list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
@@ -129,6 +130,7 @@
type lfp_rec_extension =
{nested_simps: thm list,
+ special_endgame_tac: Proof.context -> thm list -> thm list -> thm list -> tactic,
is_new_datatype: Proof.context -> string -> bool,
basic_lfp_sugars_of: binding list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
@@ -152,6 +154,11 @@
SOME {nested_simps, ...} => nested_simps
| NONE => []);
+fun special_endgame_tac ctxt =
+ (case Data.get (Proof_Context.theory_of ctxt) of
+ SOME {special_endgame_tac, ...} => special_endgame_tac ctxt
+ | NONE => K (K (K no_tac)));
+
fun is_new_datatype ctxt =
(case Data.get (Proof_Context.theory_of ctxt) of
SOME {is_new_datatype, ...} => is_new_datatype ctxt
@@ -488,11 +495,10 @@
fp_nesting_pred_maps fun_defs recx =
unfold_thms_tac ctxt fun_defs THEN
HEADGOAL (rtac ctxt (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
- unfold_thms_tac ctxt (fp_nesting_map_ident0s @ fp_nesting_map_comps @ fp_nesting_pred_maps) THEN
- REPEAT_DETERM (CHANGED (unfold_thms_tac ctxt (fp_nesting_map_ident0s @ fp_nesting_map_comps @
- fp_nesting_pred_maps) THEN
- unfold_thms_tac ctxt (nested_simps ctxt))) THEN
- HEADGOAL (rtac ctxt refl);
+ unfold_thms_tac ctxt (nested_simps ctxt @ fp_nesting_map_ident0s @ fp_nesting_map_comps @
+ fp_nesting_pred_maps) THEN
+ REPEAT_DETERM (HEADGOAL (rtac ctxt refl) ORELSE
+ special_endgame_tac ctxt fp_nesting_map_ident0s fp_nesting_map_comps fp_nesting_pred_maps);
fun prepare_primrec plugins nonexhaustives transfers fixes specs lthy0 =
let
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Jul 20 14:05:29 2017 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Jul 20 16:28:43 2017 +0100
@@ -16,6 +16,7 @@
struct
open BNF_Util
+open BNF_Tactics
open BNF_Def
open BNF_FP_Util
open BNF_FP_Def_Sugar
@@ -26,6 +27,15 @@
val nested_simps = @{thms o_def[abs_def] id_def split fst_conv snd_conv};
+fun special_endgame_tac ctxt fp_nesting_map_ident0s fp_nesting_map_comps fp_nesting_pred_maps =
+ ALLGOALS (CONVERSION Thm.eta_long_conversion) THEN
+ HEADGOAL (simp_tac (ss_only @{thms pred_fun_True_id} ctxt
+ addsimprocs [@{simproc NO_MATCH}])) THEN
+ unfold_thms_tac ctxt (nested_simps @
+ map (unfold_thms ctxt @{thms id_def}) (fp_nesting_map_ident0s @ fp_nesting_map_comps @
+ fp_nesting_pred_maps)) THEN
+ ALLGOALS (rtac ctxt refl);
+
fun is_new_datatype _ @{type_name nat} = true
| is_new_datatype ctxt s =
(case fp_sugar_of ctxt s of
@@ -176,8 +186,8 @@
massage_nested_rec_call ctxt has_call (rewrite_map_fun ctxt get_ctr_pos) (fst_const o fst);
val _ = Theory.setup (register_lfp_rec_extension
- {nested_simps = nested_simps, is_new_datatype = is_new_datatype,
- basic_lfp_sugars_of = basic_lfp_sugars_of,
+ {nested_simps = nested_simps, special_endgame_tac = special_endgame_tac,
+ is_new_datatype = is_new_datatype, basic_lfp_sugars_of = basic_lfp_sugars_of,
rewrite_nested_rec_call = SOME rewrite_nested_rec_call});
end;