# HG changeset patch
# User blanchet
# Date 1444053445 -7200
# Node ID d4ec7594f558f3149bb2203749311cdbee5518bb
# Parent  99b3a17a7eab33a271bfe1add6ffc502341319ce
avoid unsound simplification of (C (s x)) when s is a selector but not C's

diff -r 99b3a17a7eab -r d4ec7594f558 NEWS
--- a/NEWS	Mon Oct 05 13:26:25 2015 +0200
+++ b/NEWS	Mon Oct 05 15:57:25 2015 +0200
@@ -253,6 +253,7 @@
   - Eliminated obsolete "blocking" option and related subcommands.
 
 * Nitpick:
+  - Fixed soundness bug in "destroy_constrs" optimization.
   - Removed "check_potential" and "check_genuine" options.
   - Eliminated obsolete "blocking" option.
 
diff -r 99b3a17a7eab -r d4ec7594f558 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Oct 05 13:26:25 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Oct 05 15:57:25 2015 +0200
@@ -390,12 +390,12 @@
    (@{const_name unknown}, 0),
    (@{const_name is_unknown}, 1),
    (@{const_name safe_The}, 1),
-   (@{const_name Nitpick.Frac}, 0),
-   (@{const_name Nitpick.norm_frac}, 0),
+   (@{const_name Frac}, 0),
+   (@{const_name norm_frac}, 0),
    (@{const_name Suc}, 0),
    (@{const_name nat}, 0),
-   (@{const_name Nitpick.nat_gcd}, 0),
-   (@{const_name Nitpick.nat_lcm}, 0)]
+   (@{const_name nat_gcd}, 0),
+   (@{const_name nat_lcm}, 0)]
 val built_in_typed_consts =
   [((@{const_name zero_class.zero}, nat_T), 0),
    ((@{const_name one_class.one}, nat_T), 0),
@@ -583,9 +583,9 @@
 fun typedef_info ctxt s =
   if is_frac_type ctxt (Type (s, [])) then
     SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
-          Abs_name = @{const_name Nitpick.Abs_Frac},
-          Rep_name = @{const_name Nitpick.Rep_Frac},
-          prop_of_Rep = @{prop "Nitpick.Rep_Frac x \<in> Collect Nitpick.Frac"}
+          Abs_name = @{const_name Abs_Frac},
+          Rep_name = @{const_name Rep_Frac},
+          prop_of_Rep = @{prop "Rep_Frac x \<in> Collect Frac"}
                         |> Logic.varify_global,
           Abs_inverse = NONE, Rep_inverse = NONE}
   else case Typedef.get_info ctxt s of
@@ -859,7 +859,7 @@
 
 fun is_stale_constr ctxt (x as (s, T)) =
   is_registered_type ctxt (body_type T) andalso is_nonfree_constr ctxt x andalso
-  not (s = @{const_name Nitpick.Abs_Frac} orelse is_registered_coconstr ctxt x)
+  not (s = @{const_name Abs_Frac} orelse is_registered_coconstr ctxt x)
 
 fun is_constr ctxt (x as (_, T)) =
   is_nonfree_constr ctxt x andalso
diff -r 99b3a17a7eab -r d4ec7594f558 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Oct 05 13:26:25 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Oct 05 15:57:25 2015 +0200
@@ -579,7 +579,7 @@
                     |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
                     |> dest_n_tuple (length uncur_arg_Ts)
                 val t =
-                  if constr_s = @{const_name Nitpick.Abs_Frac} then
+                  if constr_s = @{const_name Abs_Frac} then
                     case ts of
                       [Const (@{const_name Pair}, _) $ t1 $ t2] =>
                       frac_from_term_pair (body_type T) t1 t2
diff -r 99b3a17a7eab -r d4ec7594f558 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Oct 05 13:26:25 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Oct 05 15:57:25 2015 +0200
@@ -569,8 +569,8 @@
             Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
           else
             do_apply t0 ts
-        | (Const (@{const_name Nitpick.nat_gcd}, T), []) => Cst (Gcd, T, Any)
-        | (Const (@{const_name Nitpick.nat_lcm}, T), []) => Cst (Lcm, T, Any)
+        | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
+        | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
         | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
           if is_built_in_const x then
             let val num_T = domain_type T in
@@ -586,8 +586,8 @@
         | (Const (@{const_name safe_The},
                   Type (@{type_name fun}, [_, T2])), [t1]) =>
           Op1 (SafeThe, T2, Any, sub t1)
-        | (Const (@{const_name Nitpick.Frac}, T), []) => Cst (Fracs, T, Any)
-        | (Const (@{const_name Nitpick.norm_frac}, T), []) =>
+        | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
+        | (Const (@{const_name norm_frac}, T), []) =>
           Cst (NormFrac, T, Any)
         | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
           Cst (NatToInt, T, Any)
diff -r 99b3a17a7eab -r d4ec7594f558 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Oct 05 13:26:25 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Oct 05 15:57:25 2015 +0200
@@ -46,9 +46,9 @@
       | aux def (t as Const (s, _)) =
         (not def orelse t <> @{const Suc}) andalso
         not (member (op =)
-               [@{const_name Nitpick.Abs_Frac}, @{const_name Nitpick.Rep_Frac},
-                @{const_name Nitpick.nat_gcd}, @{const_name Nitpick.nat_lcm},
-                @{const_name Nitpick.Frac}, @{const_name Nitpick.norm_frac}] s)
+               [@{const_name Abs_Frac}, @{const_name Rep_Frac},
+                @{const_name nat_gcd}, @{const_name nat_lcm},
+                @{const_name Frac}, @{const_name norm_frac}] s)
       | aux def (Abs (_, _, t')) = aux def t'
       | aux _ _ = true
   in aux end
@@ -1055,15 +1055,15 @@
 
 fun simplify_constrs_and_sels ctxt t =
   let
-    fun is_nth_sel_on t' n (Const (s, _) $ t) =
+    fun is_nth_sel_on constr_s t' n (Const (s, _) $ t) =
         (t = t' andalso is_sel_like_and_no_discr s andalso
-         sel_no_from_name s = n)
-      | is_nth_sel_on _ _ _ = false
-    fun do_term (Const (@{const_name Nitpick.Rep_Frac}, _)
-                 $ (Const (@{const_name Nitpick.Abs_Frac}, _) $ t1)) [] =
+         constr_name_for_sel_like s = constr_s andalso sel_no_from_name s = n)
+      | is_nth_sel_on _ _ _ _ = false
+    fun do_term (Const (@{const_name Rep_Frac}, _)
+                 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] =
         do_term t1 []
-      | do_term (Const (@{const_name Nitpick.Abs_Frac}, _)
-                 $ (Const (@{const_name Nitpick.Rep_Frac}, _) $ t1)) [] =
+      | do_term (Const (@{const_name Abs_Frac}, _)
+                 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] =
         do_term t1 []
       | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
       | do_term (t as Const (x as (s, T))) (args as _ :: _) =
@@ -1072,7 +1072,7 @@
               case hd args of
                 Const (_, T') $ t' =>
                 if domain_type T' = body_type T andalso
-                   forall (uncurry (is_nth_sel_on t'))
+                   forall (uncurry (is_nth_sel_on s t'))
                           (index_seq 0 (length args) ~~ args) then
                   t'
                 else