# HG changeset patch # User blanchet # Date 1278111035 -7200 # Node ID c6161bee84860f4fabb5ddc0df82eaa25380b574 # Parent b4c799bab553bf9c7f2cf4ed8c0b1b1208f3537f 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 "*" diff -r b4c799bab553 -r c6161bee8486 src/HOL/Nitpick.thy --- 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 = (\p. f (fst p) (snd p))" -by (simp add: prod_case_unfold split_def) - lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \ (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 diff -r b4c799bab553 -r c6161bee8486 src/HOL/Nitpick_Examples/Core_Nits.thy --- 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 "(\f x y. (curry o split) f x y) = (\f x y. (\x. x) f x y)" -nitpick [card = 1\12, expect = unknown (*none*)] +nitpick [card = 1\12, expect = none] by auto lemma "(\f p. (split o curry) f p) = (\f p. (\x. x) f p)" -nitpick [card = 1\12, expect = unknown (*none*)] +nitpick [card = 1\12, expect = none] by auto lemma "split (curry f) = f" @@ -61,12 +61,12 @@ by auto lemma "split o curry = (\x. x)" -nitpick [card = 1\12, expect = unknown (*none*)] +nitpick [card = 1\12, expect = none] apply (rule ext)+ by auto lemma "curry o split = (\x. x)" -nitpick [card = 1\12, expect = unknown (*none*)] +nitpick [card = 1\12, expect = none] apply (rule ext)+ by auto diff -r b4c799bab553 -r c6161bee8486 src/HOL/Nitpick_Examples/Datatype_Nits.thy --- 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\9, expect = unknown (*none*)] +nitpick [card = 1\9, expect = none] sorry lemma "fs (Pd ((a, b), (c, d))) = (c, d)" diff -r b4c799bab553 -r c6161bee8486 src/HOL/Product_Type.thy --- 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" diff -r b4c799bab553 -r c6161bee8486 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r b4c799bab553 -r c6161bee8486 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 () => " \ \ " ^ + 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 () => " \ \ " ^ + 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 () => "\ \ " ^ diff -r b4c799bab553 -r c6161bee8486 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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])