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 "*"
--- a/src/HOL/Nitpick.thy Sat Jul 03 00:49:12 2010 +0200
+++ b/src/HOL/Nitpick.thy Sat Jul 03 00:50:35 2010 +0200
@@ -69,9 +69,6 @@
apply (erule_tac x = y in allE)
by (auto simp: mem_def)
-lemma split_def [nitpick_def]: "split f = (\<lambda>p. f (fst p) (snd p))"
-by (simp add: prod_case_unfold split_def)
-
lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
by simp
@@ -252,12 +249,12 @@
less_frac less_eq_frac of_frac
hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
word
-hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
- refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
- fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
- list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
- zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
- plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
- inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
+hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
+ wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
+ The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
+ nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
+ num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
+ uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def
+ less_eq_frac_def of_frac_def
end
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Sat Jul 03 00:49:12 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Sat Jul 03 00:50:35 2010 +0200
@@ -17,11 +17,11 @@
subsection {* Curry in a Hurry *}
lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
-nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
-nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "split (curry f) = f"
@@ -61,12 +61,12 @@
by auto
lemma "split o curry = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
+nitpick [card = 1\<midarrow>12, expect = none]
apply (rule ext)+
by auto
lemma "curry o split = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
+nitpick [card = 1\<midarrow>12, expect = none]
apply (rule ext)+
by auto
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sat Jul 03 00:49:12 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sat Jul 03 00:50:35 2010 +0200
@@ -69,7 +69,7 @@
oops
lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
-nitpick [card = 1\<midarrow>9, expect = unknown (*none*)]
+nitpick [card = 1\<midarrow>9, expect = none]
sorry
lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
--- a/src/HOL/Product_Type.thy Sat Jul 03 00:49:12 2010 +0200
+++ b/src/HOL/Product_Type.thy Sat Jul 03 00:50:35 2010 +0200
@@ -158,6 +158,8 @@
by (simp add: Pair_def Abs_prod_inject)
qed
+declare prod.simps(2) [nitpick_simp del]
+
declare weak_case_cong [cong del]
@@ -391,7 +393,7 @@
code_const fst and snd
(Haskell "fst" and "snd")
-lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
+lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))"
by (simp add: expand_fun_eq split: prod.split)
lemma fst_eqD: "fst (x, y) = a ==> x = a"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Jul 03 00:49:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Jul 03 00:50:35 2010 +0200
@@ -876,6 +876,20 @@
"") ^ "."
end
+ val (skipped, the_scopes) =
+ all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
+ bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
+ finitizable_dataTs
+ val _ = if skipped > 0 then
+ print_m (fn () => "Too many scopes. Skipping " ^
+ string_of_int skipped ^ " scope" ^
+ plural_s skipped ^
+ ". (Consider using \"mono\" or \
+ \\"merge_type_vars\" to prevent this.)")
+ else
+ ()
+ val _ = scopes := the_scopes
+
fun run_batches _ _ []
(found_really_genuine, max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
@@ -888,7 +902,7 @@
" This suggests that the induction hypothesis might be \
\general enough to prove this subgoal."
else
- "")); "none")
+ "")); if skipped > 0 then "unknown" else "none")
else
(print_m (fn () =>
"Nitpick could not find a" ^
@@ -903,20 +917,6 @@
run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
end
- val (skipped, the_scopes) =
- all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
- bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
- finitizable_dataTs
- val _ = if skipped > 0 then
- print_m (fn () => "Too many scopes. Skipping " ^
- string_of_int skipped ^ " scope" ^
- plural_s skipped ^
- ". (Consider using \"mono\" or \
- \\"merge_type_vars\" to prevent this.)")
- else
- ()
- val _ = scopes := the_scopes
-
val batches = batch_list batch_size (!scopes)
val outcome_code =
(run_batches 0 (length batches) batches
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Jul 03 00:49:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Jul 03 00:50:35 2010 +0200
@@ -628,7 +628,9 @@
end
and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
cset)) =
- (case t of
+ (print_g (fn () => " \<Gamma> \<turnstile> " ^
+ Syntax.string_of_term ctxt t ^ " : _?");
+ case t of
Const (x as (s, T)) =>
(case AList.lookup (op =) consts x of
SOME M => (M, accum)
@@ -846,48 +848,54 @@
Plus => do_term t accum
| Minus => consider_general_equals mdata false x t1 t2 accum
in
- case t of
- Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
- do_quantifier x s1 T1 t1
- | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
- | @{const Trueprop} $ t1 =>
- let val (m1, accum) = do_formula sn t1 accum in
- (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
- m1), accum)
- end
- | @{const Not} $ t1 =>
- let val (m1, accum) = do_formula (negate sn) t1 accum in
- (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
- accum)
- end
- | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
- do_quantifier x s1 T1 t1
- | Const (x0 as (s0 as @{const_name Ex}, T0))
- $ (t1 as Abs (s1, T1, t1')) =>
- (case sn of
- Plus => do_quantifier x0 s1 T1 t1'
- | Minus =>
- (* FIXME: Move elsewhere *)
- do_term (@{const Not}
- $ (HOLogic.eq_const (domain_type T0) $ t1
- $ Abs (Name.uu, T1, @{const False}))) accum)
- | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
- do_equals x t1 t2
- | (t0 as Const (s0, _)) $ t1 $ t2 =>
- if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
- s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
- let
- val impl = (s0 = @{const_name "==>"} orelse
- s0 = @{const_name "op -->"})
- val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
- val (m2, accum) = do_formula sn t2 accum
- in
- (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
- accum)
- end
- else
- do_term t accum
- | _ => do_term t accum
+ (print_g (fn () => " \<Gamma> \<turnstile> " ^
+ Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^
+ string_for_sign sn ^ "?");
+ case t of
+ Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
+ do_quantifier x s1 T1 t1
+ | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
+ | @{const Trueprop} $ t1 =>
+ let val (m1, accum) = do_formula sn t1 accum in
+ (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
+ m1), accum)
+ end
+ | @{const Not} $ t1 =>
+ let val (m1, accum) = do_formula (negate sn) t1 accum in
+ (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
+ accum)
+ end
+ | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
+ do_quantifier x s1 T1 t1
+ | Const (x0 as (s0 as @{const_name Ex}, T0))
+ $ (t1 as Abs (s1, T1, t1')) =>
+ (case sn of
+ Plus => do_quantifier x0 s1 T1 t1'
+ | Minus =>
+ (* FIXME: Move elsewhere *)
+ do_term (@{const Not}
+ $ (HOLogic.eq_const (domain_type T0) $ t1
+ $ Abs (Name.uu, T1, @{const False}))) accum)
+ | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ do_equals x t1 t2
+ | Const (@{const_name Let}, _) $ t1 $ t2 =>
+ do_formula sn (betapply (t2, t1)) accum
+ | (t0 as Const (s0, _)) $ t1 $ t2 =>
+ if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
+ s0 = @{const_name "op |"} orelse
+ s0 = @{const_name "op -->"} then
+ let
+ val impl = (s0 = @{const_name "==>"} orelse
+ s0 = @{const_name "op -->"})
+ val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
+ val (m2, accum) = do_formula sn t2 accum
+ in
+ (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
+ accum)
+ end
+ else
+ do_term t accum
+ | _ => do_term t accum)
end
|> tap (fn (m, _) =>
print_g (fn () => "\<Gamma> \<turnstile> " ^
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Jul 03 00:49:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Jul 03 00:50:35 2010 +0200
@@ -179,7 +179,8 @@
let
val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
- val T = [T1, T2] |> sort Term_Ord.typ_ord |> List.last
+ val T = if def then T1
+ else [T1, T2] |> sort (int_ord o pairself size_of_typ) |> hd
in
list_comb (Const (s0, T --> T --> body_type T0),
map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])