--- 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.
--- 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 *}
--- 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 \<equiv> 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 \<equiv> 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
--- 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 *}
--- 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) \<equiv> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> 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 \<equiv> \<exists>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>* \<equiv> (r\<^sup>+)\<^sup>="
+lemma rtrancl_def [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
by simp
-lemma rtranclp_def [nitpick_def, no_atp]:
+lemma rtranclp_def [nitpick_unfold, no_atp]:
"rtranclp r a b \<equiv> (a = b \<or> 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 \<equiv> 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 \<equiv> 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 \<equiv> if n = 0 then x else f (n - 1)"
apply (rule eq_reflection)
by (case_tac n) auto
--- 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"
--- 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
--- 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
--- 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 \<and> 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 = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
--- 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)
--- 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;
--- 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