# HG changeset patch
# User blanchet
# Date 1500564523 -3600
# Node ID 88714f2e40e8a7c78b6cb9e4adcee92ee2fc9e9e
# Parent  2562f151541c0177c55462d48e0cd87aca1aa6ee
strengthened tactic

diff -r 2562f151541c -r 88714f2e40e8 src/HOL/BNF_Least_Fixpoint.thy
--- 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"
diff -r 2562f151541c -r 88714f2e40e8 src/HOL/Nat.thy
--- 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>
 
diff -r 2562f151541c -r 88714f2e40e8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- 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
diff -r 2562f151541c -r 88714f2e40e8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- 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;