adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
authorblanchet
Sat Jul 03 00:50:35 2010 +0200 (2010-07-03)
changeset 37704c6161bee8486
parent 37703 b4c799bab553
child 37705 8e44a83df34a
child 37729 daea77769276
adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Datatype_Nits.thy
src/HOL/Product_Type.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Nitpick.thy	Sat Jul 03 00:49:12 2010 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Sat Jul 03 00:50:35 2010 +0200
     1.3 @@ -69,9 +69,6 @@
     1.4   apply (erule_tac x = y in allE)
     1.5  by (auto simp: mem_def)
     1.6  
     1.7 -lemma split_def [nitpick_def]: "split f = (\<lambda>p. f (fst p) (snd p))"
     1.8 -by (simp add: prod_case_unfold split_def)
     1.9 -
    1.10  lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.11  by simp
    1.12  
    1.13 @@ -252,12 +249,12 @@
    1.14      less_frac less_eq_frac of_frac
    1.15  hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.16      word
    1.17 -hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
    1.18 -    refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    1.19 -    fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
    1.20 -    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    1.21 -    zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    1.22 -    plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    1.23 -    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
    1.24 +hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    1.25 +    wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    1.26 +    The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
    1.27 +    nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    1.28 +    num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
    1.29 +    uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def
    1.30 +    less_eq_frac_def of_frac_def
    1.31  
    1.32  end
     2.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Sat Jul 03 00:49:12 2010 +0200
     2.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Sat Jul 03 00:50:35 2010 +0200
     2.3 @@ -17,11 +17,11 @@
     2.4  subsection {* Curry in a Hurry *}
     2.5  
     2.6  lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
     2.7 -nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
     2.8 +nitpick [card = 1\<midarrow>12, expect = none]
     2.9  by auto
    2.10  
    2.11  lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
    2.12 -nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
    2.13 +nitpick [card = 1\<midarrow>12, expect = none]
    2.14  by auto
    2.15  
    2.16  lemma "split (curry f) = f"
    2.17 @@ -61,12 +61,12 @@
    2.18  by auto
    2.19  
    2.20  lemma "split o curry = (\<lambda>x. x)"
    2.21 -nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
    2.22 +nitpick [card = 1\<midarrow>12, expect = none]
    2.23  apply (rule ext)+
    2.24  by auto
    2.25  
    2.26  lemma "curry o split = (\<lambda>x. x)"
    2.27 -nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
    2.28 +nitpick [card = 1\<midarrow>12, expect = none]
    2.29  apply (rule ext)+
    2.30  by auto
    2.31  
     3.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sat Jul 03 00:49:12 2010 +0200
     3.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sat Jul 03 00:50:35 2010 +0200
     3.3 @@ -69,7 +69,7 @@
     3.4  oops
     3.5  
     3.6  lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
     3.7 -nitpick [card = 1\<midarrow>9, expect = unknown (*none*)]
     3.8 +nitpick [card = 1\<midarrow>9, expect = none]
     3.9  sorry
    3.10  
    3.11  lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
     4.1 --- a/src/HOL/Product_Type.thy	Sat Jul 03 00:49:12 2010 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Sat Jul 03 00:50:35 2010 +0200
     4.3 @@ -158,6 +158,8 @@
     4.4      by (simp add: Pair_def Abs_prod_inject)
     4.5  qed
     4.6  
     4.7 +declare prod.simps(2) [nitpick_simp del]
     4.8 +
     4.9  declare weak_case_cong [cong del]
    4.10  
    4.11  
    4.12 @@ -391,7 +393,7 @@
    4.13  code_const fst and snd
    4.14    (Haskell "fst" and "snd")
    4.15  
    4.16 -lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
    4.17 +lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))"
    4.18    by (simp add: expand_fun_eq split: prod.split)
    4.19  
    4.20  lemma fst_eqD: "fst (x, y) = a ==> x = a"
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jul 03 00:49:12 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jul 03 00:50:35 2010 +0200
     5.3 @@ -876,6 +876,20 @@
     5.4             "") ^ "."
     5.5        end
     5.6  
     5.7 +    val (skipped, the_scopes) =
     5.8 +      all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
     5.9 +                 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    5.10 +                 finitizable_dataTs
    5.11 +    val _ = if skipped > 0 then
    5.12 +              print_m (fn () => "Too many scopes. Skipping " ^
    5.13 +                                string_of_int skipped ^ " scope" ^
    5.14 +                                plural_s skipped ^
    5.15 +                                ". (Consider using \"mono\" or \
    5.16 +                                \\"merge_type_vars\" to prevent this.)")
    5.17 +            else
    5.18 +              ()
    5.19 +    val _ = scopes := the_scopes
    5.20 +
    5.21      fun run_batches _ _ []
    5.22                      (found_really_genuine, max_potential, max_genuine, donno) =
    5.23          if donno > 0 andalso max_genuine > 0 then
    5.24 @@ -888,7 +902,7 @@
    5.25                      " This suggests that the induction hypothesis might be \
    5.26                      \general enough to prove this subgoal."
    5.27                    else
    5.28 -                    "")); "none")
    5.29 +                    "")); if skipped > 0 then "unknown" else "none")
    5.30            else
    5.31              (print_m (fn () =>
    5.32                   "Nitpick could not find a" ^
    5.33 @@ -903,20 +917,6 @@
    5.34            run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
    5.35          end
    5.36  
    5.37 -    val (skipped, the_scopes) =
    5.38 -      all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
    5.39 -                 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    5.40 -                 finitizable_dataTs
    5.41 -    val _ = if skipped > 0 then
    5.42 -              print_m (fn () => "Too many scopes. Skipping " ^
    5.43 -                                string_of_int skipped ^ " scope" ^
    5.44 -                                plural_s skipped ^
    5.45 -                                ". (Consider using \"mono\" or \
    5.46 -                                \\"merge_type_vars\" to prevent this.)")
    5.47 -            else
    5.48 -              ()
    5.49 -    val _ = scopes := the_scopes
    5.50 -
    5.51      val batches = batch_list batch_size (!scopes)
    5.52      val outcome_code =
    5.53        (run_batches 0 (length batches) batches
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Jul 03 00:49:12 2010 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Jul 03 00:50:35 2010 +0200
     6.3 @@ -628,7 +628,9 @@
     6.4        end
     6.5      and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
     6.6                               cset)) =
     6.7 -        (case t of
     6.8 +        (print_g (fn () => "  \<Gamma> \<turnstile> " ^
     6.9 +                           Syntax.string_of_term ctxt t ^ " : _?");
    6.10 +         case t of
    6.11             Const (x as (s, T)) =>
    6.12             (case AList.lookup (op =) consts x of
    6.13                SOME M => (M, accum)
    6.14 @@ -846,48 +848,54 @@
    6.15                Plus => do_term t accum
    6.16              | Minus => consider_general_equals mdata false x t1 t2 accum
    6.17          in
    6.18 -          case t of
    6.19 -            Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
    6.20 -            do_quantifier x s1 T1 t1
    6.21 -          | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
    6.22 -          | @{const Trueprop} $ t1 =>
    6.23 -            let val (m1, accum) = do_formula sn t1 accum in
    6.24 -              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
    6.25 -                     m1), accum)
    6.26 -            end
    6.27 -          | @{const Not} $ t1 =>
    6.28 -            let val (m1, accum) = do_formula (negate sn) t1 accum in
    6.29 -              (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
    6.30 -               accum)
    6.31 -            end
    6.32 -          | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
    6.33 -            do_quantifier x s1 T1 t1
    6.34 -          | Const (x0 as (s0 as @{const_name Ex}, T0))
    6.35 -            $ (t1 as Abs (s1, T1, t1')) =>
    6.36 -            (case sn of
    6.37 -               Plus => do_quantifier x0 s1 T1 t1'
    6.38 -             | Minus =>
    6.39 -               (* FIXME: Move elsewhere *)
    6.40 -               do_term (@{const Not}
    6.41 -                        $ (HOLogic.eq_const (domain_type T0) $ t1
    6.42 -                           $ Abs (Name.uu, T1, @{const False}))) accum)
    6.43 -          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
    6.44 -            do_equals x t1 t2
    6.45 -          | (t0 as Const (s0, _)) $ t1 $ t2 =>
    6.46 -            if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
    6.47 -               s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
    6.48 -              let
    6.49 -                val impl = (s0 = @{const_name "==>"} orelse
    6.50 -                           s0 = @{const_name "op -->"})
    6.51 -                val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
    6.52 -                val (m2, accum) = do_formula sn t2 accum
    6.53 -              in
    6.54 -                (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
    6.55 -                 accum)
    6.56 -              end 
    6.57 -            else
    6.58 -              do_term t accum
    6.59 -          | _ => do_term t accum
    6.60 +          (print_g (fn () => "  \<Gamma> \<turnstile> " ^
    6.61 +                           Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^
    6.62 +                           string_for_sign sn ^ "?");
    6.63 +           case t of
    6.64 +             Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
    6.65 +             do_quantifier x s1 T1 t1
    6.66 +           | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
    6.67 +           | @{const Trueprop} $ t1 =>
    6.68 +             let val (m1, accum) = do_formula sn t1 accum in
    6.69 +               (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
    6.70 +                      m1), accum)
    6.71 +             end
    6.72 +           | @{const Not} $ t1 =>
    6.73 +             let val (m1, accum) = do_formula (negate sn) t1 accum in
    6.74 +               (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
    6.75 +                accum)
    6.76 +             end
    6.77 +           | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
    6.78 +             do_quantifier x s1 T1 t1
    6.79 +           | Const (x0 as (s0 as @{const_name Ex}, T0))
    6.80 +             $ (t1 as Abs (s1, T1, t1')) =>
    6.81 +             (case sn of
    6.82 +                Plus => do_quantifier x0 s1 T1 t1'
    6.83 +              | Minus =>
    6.84 +                (* FIXME: Move elsewhere *)
    6.85 +                do_term (@{const Not}
    6.86 +                         $ (HOLogic.eq_const (domain_type T0) $ t1
    6.87 +                            $ Abs (Name.uu, T1, @{const False}))) accum)
    6.88 +           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
    6.89 +             do_equals x t1 t2
    6.90 +           | Const (@{const_name Let}, _) $ t1 $ t2 =>
    6.91 +             do_formula sn (betapply (t2, t1)) accum
    6.92 +           | (t0 as Const (s0, _)) $ t1 $ t2 =>
    6.93 +             if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
    6.94 +                s0 = @{const_name "op |"} orelse
    6.95 +                s0 = @{const_name "op -->"} then
    6.96 +               let
    6.97 +                 val impl = (s0 = @{const_name "==>"} orelse
    6.98 +                             s0 = @{const_name "op -->"})
    6.99 +                 val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
   6.100 +                 val (m2, accum) = do_formula sn t2 accum
   6.101 +               in
   6.102 +                 (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   6.103 +                  accum)
   6.104 +               end 
   6.105 +             else
   6.106 +               do_term t accum
   6.107 +           | _ => do_term t accum)
   6.108          end
   6.109          |> tap (fn (m, _) =>
   6.110                     print_g (fn () => "\<Gamma> \<turnstile> " ^
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Jul 03 00:49:12 2010 +0200
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Jul 03 00:50:35 2010 +0200
     7.3 @@ -179,7 +179,8 @@
     7.4        let
     7.5          val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
     7.6          val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
     7.7 -        val T = [T1, T2] |> sort Term_Ord.typ_ord |> List.last
     7.8 +        val T = if def then T1
     7.9 +                else [T1, T2] |> sort (int_ord o pairself size_of_typ) |> hd
    7.10        in
    7.11          list_comb (Const (s0, T --> T --> body_type T0),
    7.12                     map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])