# HG changeset patch # User blanchet # Date 1298281459 -3600 # Node ID ff3cb0c418b7d45552a7c734e140edf2db8a4f3c # Parent 01d722707a361678b834c2648fd516b1a1a94771 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics diff -r 01d722707a36 -r ff3cb0c418b7 NEWS --- a/NEWS Mon Feb 21 10:42:29 2011 +0100 +++ b/NEWS Mon Feb 21 10:44:19 2011 +0100 @@ -19,8 +19,12 @@ *** HOL *** +* Nitpick: + - Renamed attribute: nitpick_def ~> nitpick_unfold. + INCOMPATIBILITY. + * Sledgehammer: - sledgehammer available_provers ~> sledgehammer supported_provers + - sledgehammer available_provers ~> sledgehammer supported_provers INCOMPATIBILITY. diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/Divides.thy Mon Feb 21 10:44:19 2011 +0100 @@ -2470,9 +2470,7 @@ in subst [OF mod_div_equality [of _ n]]) arith -lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection] - mod_div_equality' [THEN eq_reflection] - zmod_zdiv_equality' [THEN eq_reflection] +lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality' subsubsection {* Code generation *} diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/GCD.thy Mon Feb 21 10:44:19 2011 +0100 @@ -1722,12 +1722,11 @@ text{* Nitpick: *} -lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \ Nitpick.nat_gcd x y" -apply (rule eq_reflection) -apply (induct x y rule: nat_gcd.induct) -by (simp add: gcd_nat.simps Nitpick.nat_gcd.simps) +lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y" +by (induct x y rule: nat_gcd.induct) + (simp add: gcd_nat.simps Nitpick.nat_gcd.simps) -lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \ Nitpick.nat_lcm x y" +lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y" by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd) end diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/HOL.thy Mon Feb 21 10:44:19 2011 +0100 @@ -1111,7 +1111,8 @@ lemma if_eq_cancel: "(if x = y then y else x) = x" by (simplesubst split_if, blast) -lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))" +lemma if_bool_eq_conj: +"(if P then Q else R) = ((P-->Q) & (~P-->R))" -- {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *} by (rule split_if) @@ -1990,9 +1991,9 @@ subsubsection {* Nitpick setup *} ML {* -structure Nitpick_Defs = Named_Thms +structure Nitpick_Unfolds = Named_Thms ( - val name = "nitpick_def" + val name = "nitpick_unfold" val description = "alternative definitions of constants as needed by Nitpick" ) structure Nitpick_Simps = Named_Thms @@ -2013,12 +2014,15 @@ *} setup {* - Nitpick_Defs.setup + Nitpick_Unfolds.setup #> Nitpick_Simps.setup #> Nitpick_Psimps.setup #> Nitpick_Choice_Specs.setup *} +declare if_bool_eq_conj [nitpick_unfold, no_atp] + if_bool_eq_disj [no_atp] + subsection {* Preprocessing for the predicate compiler *} diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/Nitpick.thy Mon Feb 21 10:44:19 2011 +0100 @@ -47,11 +47,7 @@ Alternative definitions. *} -lemma If_def [nitpick_def, no_atp]: -"(if P then Q else R) \ (P \ Q) \ (\ P \ R)" -by (rule eq_reflection) (rule if_bool_eq_conj) - -lemma Ex1_def [nitpick_def, no_atp]: +lemma Ex1_def [nitpick_unfold, no_atp]: "Ex1 P \ \x. P = {x}" apply (rule eq_reflection) apply (simp add: Ex1_def set_eq_iff) @@ -64,14 +60,14 @@ apply (erule_tac x = y in allE) by (auto simp: mem_def) -lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \ (r\<^sup>+)\<^sup>=" +lemma rtrancl_def [nitpick_unfold, no_atp]: "r\<^sup>* \ (r\<^sup>+)\<^sup>=" by simp -lemma rtranclp_def [nitpick_def, no_atp]: +lemma rtranclp_def [nitpick_unfold, no_atp]: "rtranclp r a b \ (a = b \ tranclp r a b)" by (rule eq_reflection) (auto dest: rtranclpD) -lemma tranclp_def [nitpick_def, no_atp]: +lemma tranclp_def [nitpick_unfold, no_atp]: "tranclp r a b \ trancl (split r) (a, b)" by (simp add: trancl_def Collect_def mem_def) @@ -119,7 +115,7 @@ apply (erule contrapos_np) by (rule someI) -lemma unit_case_def [nitpick_def, no_atp]: +lemma unit_case_def [nitpick_unfold, no_atp]: "unit_case x u \ x" apply (subgoal_tac "u = ()") apply (simp only: unit.cases) @@ -127,7 +123,7 @@ declare unit.cases [nitpick_simp del] -lemma nat_case_def [nitpick_def, no_atp]: +lemma nat_case_def [nitpick_unfold, no_atp]: "nat_case x f n \ if n = 0 then x else f (n - 1)" apply (rule eq_reflection) by (case_tac n) auto diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/Product_Type.thy Mon Feb 21 10:44:19 2011 +0100 @@ -392,7 +392,7 @@ code_const fst and snd (Haskell "fst" and "snd") -lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))" +lemma prod_case_unfold [nitpick_unfold]: "prod_case = (%c p. c (fst p) (snd p))" by (simp add: fun_eq_iff split: prod.split) lemma fst_eqD: "fst (x, y) = a ==> x = a" diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/Rat.thy Mon Feb 21 10:44:19 2011 +0100 @@ -1199,7 +1199,7 @@ (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})] *} -lemmas [nitpick_def] = inverse_rat_inst.inverse_rat +lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_rat ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/RealDef.thy Mon Feb 21 10:44:19 2011 +0100 @@ -1829,7 +1829,7 @@ (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})] *} -lemmas [nitpick_def] = inverse_real_inst.inverse_real +lemmas [nitpick_unfold] = inverse_real_inst.inverse_real number_real_inst.number_of_real one_real_inst.one_real ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real times_real_inst.times_real uminus_real_inst.uminus_real diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/Relation.thy Mon Feb 21 10:44:19 2011 +0100 @@ -132,7 +132,7 @@ lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)" by blast -lemma Id_on_def'[nitpick_def, code]: +lemma Id_on_def' [nitpick_unfold, code]: "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \ A x)" by (auto simp add: fun_eq_iff elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def]) @@ -227,7 +227,7 @@ lemma refl_on_Id_on: "refl_on A (Id_on A)" by (rule refl_onI [OF Id_on_subset_Times Id_onI]) -lemma refl_on_def'[nitpick_def, code]: +lemma refl_on_def' [nitpick_unfold, code]: "refl_on A r = ((\(x, y) \ r. x : A \ y : A) \ (\x \ A. (x, x) : r))" by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 21 10:44:19 2011 +0100 @@ -1850,7 +1850,7 @@ |> AList.group (op =) |> Symtab.make fun const_def_tables ctxt subst ts = - (def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst, + (def_table_for (map prop_of o Nitpick_Unfolds.get) ctxt subst, fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) (map pair_for_prop ts) Symtab.empty) diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/Tools/inductive.ML Mon Feb 21 10:44:19 2011 +0100 @@ -774,7 +774,7 @@ |> Local_Theory.conceal |> Local_Theory.define ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), - ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]), + ((Binding.empty, [Attrib.internal (K Nitpick_Unfolds.add)]), fold_rev lambda params (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) ||> Local_Theory.restore_naming lthy; diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Mon Feb 21 10:42:29 2011 +0100 +++ b/src/HOL/Transitive_Closure.thy Mon Feb 21 10:44:19 2011 +0100 @@ -33,10 +33,10 @@ r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+" | trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+" -declare rtrancl_def [nitpick_def del] - rtranclp_def [nitpick_def del] - trancl_def [nitpick_def del] - tranclp_def [nitpick_def del] +declare rtrancl_def [nitpick_unfold del] + rtranclp_def [nitpick_unfold del] + trancl_def [nitpick_unfold del] + tranclp_def [nitpick_unfold del] notation rtranclp ("(_^**)" [1000] 1000) and