# HG changeset patch
# User blanchet
# Date 1477694373 -7200
# Node ID 1d85ac286c72237f245dcc2b2ba8a2bf7e858d41
# Parent  582f54f6b29bd06bca6727d26b9b8bb9e481a445
avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar

diff -r 582f54f6b29b -r 1d85ac286c72 src/HOL/Ctr_Sugar.thy
--- a/src/HOL/Ctr_Sugar.thy	Sat Oct 29 00:39:32 2016 +0200
+++ b/src/HOL/Ctr_Sugar.thy	Sat Oct 29 00:39:33 2016 +0200
@@ -42,8 +42,8 @@
 ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
 ML_file "Tools/Ctr_Sugar/ctr_sugar.ML"
 
+text \<open>Coinduction method that avoids some boilerplate compared with coinduct.\<close>
 
-text \<open>Coinduction method that avoids some boilerplate compared to coinduct.\<close>
 ML_file "Tools/coinduction.ML"
 
 end
diff -r 582f54f6b29b -r 1d85ac286c72 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat Oct 29 00:39:32 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat Oct 29 00:39:33 2016 +0200
@@ -785,7 +785,7 @@
         fun prove_split selss goal =
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
-            mk_split_tac ctxt ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss))
+            mk_split_tac ctxt uexhaust_thm case_thms selss inject_thmss distinct_thmsss))
           |> Thm.close_derivation;
 
         fun prove_split_asm asm_goal split_thm =
@@ -805,13 +805,12 @@
             (thm, asm_thm)
           end;
 
-        val (sel_defs, all_sel_thms, sel_thmss, disc_defs, nontriv_disc_defs, disc_thmss,
-             nontriv_disc_thmss, discI_thms, nontriv_discI_thms, distinct_disc_thms,
-             distinct_disc_thmsss, exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms,
-             safe_collapse_thms, expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms,
-             disc_eq_case_thms) =
+        val (sel_defs, all_sel_thms, sel_thmss, nontriv_disc_defs, disc_thmss, nontriv_disc_thmss,
+             discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
+             exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms, safe_collapse_thms,
+             expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms, disc_eq_case_thms) =
           if no_discs_sels then
-            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
+            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
           else
             let
               val udiscs = map (rapp u) discs;
@@ -1049,11 +1048,11 @@
                   |> Conjunction.elim_balanced (length goals)
                 end;
             in
-              (sel_defs, all_sel_thms, sel_thmss, disc_defs, nontriv_disc_defs, disc_thmss,
-               nontriv_disc_thmss, discI_thms, nontriv_discI_thms, distinct_disc_thms,
-               distinct_disc_thmsss, [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms,
-               safe_collapse_thms, [expand_thm], [split_sel_thm], [split_sel_asm_thm],
-               [case_eq_if_thm], disc_eq_case_thms)
+              (sel_defs, all_sel_thms, sel_thmss, nontriv_disc_defs, disc_thmss, nontriv_disc_thmss,
+               discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
+               [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms, safe_collapse_thms,
+               [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm],
+               disc_eq_case_thms)
             end;
 
         val case_distrib_thm =
@@ -1113,8 +1112,7 @@
           |> map (fn (thmN, thms, attrs) =>
             ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
 
-        val (noted, lthy') =
-          lthy
+        val (noted, lthy') = lthy
           |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
           |> fold (Spec_Rules.add Spec_Rules.Equational)
             (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
@@ -1123,14 +1121,15 @@
           |> Local_Theory.declaration {syntax = false, pervasive = true}
             (fn phi => Case_Translation.register
                (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
-          |> Local_Theory.background_theory (fold (fold Code.del_eqn) [nontriv_disc_defs, sel_defs])
+          |> Local_Theory.background_theory
+            (fold (fold Code.del_eqn_silent) [nontriv_disc_defs, sel_defs])
           |> plugins code_plugin ?
-            Local_Theory.declaration {syntax = false, pervasive = false}
-              (fn phi => Context.mapping
-                 (add_ctr_code fcT_name (map (Morphism.typ phi) As)
-                    (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
-                    (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
-                 I)
+             Local_Theory.declaration {syntax = false, pervasive = false}
+               (fn phi => Context.mapping
+                  (add_ctr_code fcT_name (map (Morphism.typ phi) As)
+                     (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
+                     (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
+                  I)
           |> Local_Theory.notes (anonymous_notes @ notes)
           (* for "datatype_realizer.ML": *)
           |>> name_noted_thms fcT_name exhaustN;
diff -r 582f54f6b29b -r 1d85ac286c72 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Oct 29 00:39:32 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Oct 29 00:39:33 2016 +0200
@@ -31,8 +31,8 @@
   val mk_half_distinct_disc_tac: Proof.context -> int -> thm -> thm -> tactic
   val mk_nchotomy_tac: Proof.context -> int -> thm -> tactic
   val mk_other_half_distinct_disc_tac: Proof.context -> thm -> tactic
-  val mk_split_tac: Proof.context -> int list -> thm -> thm list -> thm list list ->
-    thm list list -> thm list list list -> tactic
+  val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list ->
+    thm list list list -> tactic
   val mk_split_asm_tac: Proof.context -> thm -> tactic
   val mk_unique_disc_def_tac: Proof.context -> int -> thm -> tactic
 end;
@@ -180,20 +180,18 @@
           rtac ctxt casex])
       cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
 
-fun mk_split_tac ctxt ms uexhaust cases selss injectss distinctsss =
-  let val depth = fold Integer.max ms 0 in
-    HEADGOAL (rtac ctxt uexhaust) THEN
-    ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
-       simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
-         flat (nth distinctsss (k - 1))) ctxt)) k) THEN
-    ALLGOALS (etac ctxt thin_rl THEN' rtac ctxt iffI THEN'
-      REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN'
-      REPEAT_DETERM o etac ctxt conjE THEN'
-      hyp_subst_tac ctxt THEN' assume_tac ctxt THEN'
-      REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN'
-      REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN'
-      rtac ctxt refl THEN' assume_tac ctxt)
-  end;
+fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
+  HEADGOAL (rtac ctxt uexhaust) THEN
+  ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
+    simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
+      flat (nth distinctsss (k - 1))) ctxt)) k) THEN
+  ALLGOALS (etac ctxt thin_rl THEN' rtac ctxt iffI THEN'
+    REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN'
+    REPEAT_DETERM o etac ctxt conjE THEN'
+    hyp_subst_tac ctxt THEN' assume_tac ctxt THEN'
+    REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN'
+    REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN'
+    rtac ctxt refl THEN' assume_tac ctxt);
 
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
 
diff -r 582f54f6b29b -r 1d85ac286c72 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sat Oct 29 00:39:32 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sat Oct 29 00:39:33 2016 +0200
@@ -406,25 +406,27 @@
   handle Sorts.CLASS_ERROR _ => NONE
 
 fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) config raw_tycos thy =
-  let
-    val algebra = Sign.classes_of thy
-    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos
-    val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
-    fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
-      (Old_Datatype_Aux.interpret_construction descr vs constr)
-    val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] }
-      @ insts_of aux_sort { atyp = K [], dtyp = K o K }
-    val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos
-  in
-    if has_inst then thy
-    else
-      (case perhaps_constrain thy insts vs of
-        SOME constrain =>
-          instantiate config descr
-            (map constrain vs) tycos prfx (names, auxnames)
-              ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
-      | NONE => thy)
-  end
+  (case try (the_descr thy) raw_tycos of
+    NONE => thy
+  | SOME (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =>
+    let
+      val algebra = Sign.classes_of thy
+      val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
+      fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
+        (Old_Datatype_Aux.interpret_construction descr vs constr)
+      val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] }
+        @ insts_of aux_sort { atyp = K [], dtyp = K o K }
+      val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos
+    in
+      if has_inst then thy
+      else
+        (case perhaps_constrain thy insts vs of
+          SOME constrain =>
+            instantiate config descr
+              (map constrain vs) tycos prfx (names, auxnames)
+                ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
+        | NONE => thy)
+    end)
 
 fun ensure_common_sort_datatype (sort, instantiate) =
   ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
diff -r 582f54f6b29b -r 1d85ac286c72 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Oct 29 00:39:32 2016 +0200
+++ b/src/Pure/Isar/code.ML	Sat Oct 29 00:39:33 2016 +0200
@@ -47,6 +47,7 @@
   val add_eqn: kind * bool -> thm -> theory -> theory
   val add_default_eqn_attribute: kind -> attribute
   val add_default_eqn_attrib: kind -> Token.src
+  val del_eqn_silent: thm -> theory -> theory
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
   val del_exception: string -> theory -> theory
@@ -1168,7 +1169,7 @@
     | SOME ((thm, _), SOME tyco) => gen_add_abs_eqn false (thm, tyco) thy
     | NONE => thy;
 
-fun del_eqn thm thy = case mk_eqn Liberal thy (thm, true)
+fun generic_del_eqn strictness thm thy = case mk_eqn strictness thy (thm, true)
  of SOME (thm, _) =>
       let
         fun del_eqn' (Eqns_Default _) = initial_fun_spec
@@ -1180,6 +1181,9 @@
       in change_fun_spec (const_eqn thy thm) del_eqn' thy end
   | NONE => thy;
 
+val del_eqn_silent = generic_del_eqn Silent;
+val del_eqn = generic_del_eqn Liberal;
+
 fun del_eqns c = change_fun_spec c (K None);
 
 fun del_exception c = change_fun_spec c (K (Eqns []));