renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
authorblanchet
Mon Feb 21 10:44:19 2011 +0100 (2011-02-21)
changeset 41792ff3cb0c418b7
parent 41791 01d722707a36
child 41793 c7a2669ae75d
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
NEWS
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/HOL.thy
src/HOL/Nitpick.thy
src/HOL/Product_Type.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
src/HOL/Relation.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/inductive.ML
src/HOL/Transitive_Closure.thy
     1.1 --- a/NEWS	Mon Feb 21 10:42:29 2011 +0100
     1.2 +++ b/NEWS	Mon Feb 21 10:44:19 2011 +0100
     1.3 @@ -19,8 +19,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Nitpick:
     1.8 +  - Renamed attribute: nitpick_def ~> nitpick_unfold.
     1.9 +    INCOMPATIBILITY.
    1.10 +
    1.11  * Sledgehammer:
    1.12 -    sledgehammer available_provers ~> sledgehammer supported_provers
    1.13 +  - sledgehammer available_provers ~> sledgehammer supported_provers
    1.14      INCOMPATIBILITY.
    1.15  
    1.16  
     2.1 --- a/src/HOL/Divides.thy	Mon Feb 21 10:42:29 2011 +0100
     2.2 +++ b/src/HOL/Divides.thy	Mon Feb 21 10:44:19 2011 +0100
     2.3 @@ -2470,9 +2470,7 @@
     2.4      in subst [OF mod_div_equality [of _ n]])
     2.5     arith
     2.6  
     2.7 -lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
     2.8 -                       mod_div_equality' [THEN eq_reflection]
     2.9 -                       zmod_zdiv_equality' [THEN eq_reflection]
    2.10 +lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'
    2.11  
    2.12  
    2.13  subsubsection {* Code generation *}
     3.1 --- a/src/HOL/GCD.thy	Mon Feb 21 10:42:29 2011 +0100
     3.2 +++ b/src/HOL/GCD.thy	Mon Feb 21 10:44:19 2011 +0100
     3.3 @@ -1722,12 +1722,11 @@
     3.4  
     3.5  text{* Nitpick: *}
     3.6  
     3.7 -lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
     3.8 -apply (rule eq_reflection)
     3.9 -apply (induct x y rule: nat_gcd.induct)
    3.10 -by (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
    3.11 +lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
    3.12 +by (induct x y rule: nat_gcd.induct)
    3.13 +   (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
    3.14  
    3.15 -lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \<equiv> Nitpick.nat_lcm x y"
    3.16 +lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
    3.17  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
    3.18  
    3.19  end
     4.1 --- a/src/HOL/HOL.thy	Mon Feb 21 10:42:29 2011 +0100
     4.2 +++ b/src/HOL/HOL.thy	Mon Feb 21 10:44:19 2011 +0100
     4.3 @@ -1111,7 +1111,8 @@
     4.4  lemma if_eq_cancel: "(if x = y then y else x) = x"
     4.5  by (simplesubst split_if, blast)
     4.6  
     4.7 -lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
     4.8 +lemma if_bool_eq_conj:
     4.9 +"(if P then Q else R) = ((P-->Q) & (~P-->R))"
    4.10    -- {* This form is useful for expanding @{text "if"}s on the RIGHT of the @{text "==>"} symbol. *}
    4.11    by (rule split_if)
    4.12  
    4.13 @@ -1990,9 +1991,9 @@
    4.14  subsubsection {* Nitpick setup *}
    4.15  
    4.16  ML {*
    4.17 -structure Nitpick_Defs = Named_Thms
    4.18 +structure Nitpick_Unfolds = Named_Thms
    4.19  (
    4.20 -  val name = "nitpick_def"
    4.21 +  val name = "nitpick_unfold"
    4.22    val description = "alternative definitions of constants as needed by Nitpick"
    4.23  )
    4.24  structure Nitpick_Simps = Named_Thms
    4.25 @@ -2013,12 +2014,15 @@
    4.26  *}
    4.27  
    4.28  setup {*
    4.29 -  Nitpick_Defs.setup
    4.30 +  Nitpick_Unfolds.setup
    4.31    #> Nitpick_Simps.setup
    4.32    #> Nitpick_Psimps.setup
    4.33    #> Nitpick_Choice_Specs.setup
    4.34  *}
    4.35  
    4.36 +declare if_bool_eq_conj [nitpick_unfold, no_atp]
    4.37 +        if_bool_eq_disj [no_atp]
    4.38 +
    4.39  
    4.40  subsection {* Preprocessing for the predicate compiler *}
    4.41  
     5.1 --- a/src/HOL/Nitpick.thy	Mon Feb 21 10:42:29 2011 +0100
     5.2 +++ b/src/HOL/Nitpick.thy	Mon Feb 21 10:44:19 2011 +0100
     5.3 @@ -47,11 +47,7 @@
     5.4  Alternative definitions.
     5.5  *}
     5.6  
     5.7 -lemma If_def [nitpick_def, no_atp]:
     5.8 -"(if P then Q else R) \<equiv> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R)"
     5.9 -by (rule eq_reflection) (rule if_bool_eq_conj)
    5.10 -
    5.11 -lemma Ex1_def [nitpick_def, no_atp]:
    5.12 +lemma Ex1_def [nitpick_unfold, no_atp]:
    5.13  "Ex1 P \<equiv> \<exists>x. P = {x}"
    5.14  apply (rule eq_reflection)
    5.15  apply (simp add: Ex1_def set_eq_iff)
    5.16 @@ -64,14 +60,14 @@
    5.17   apply (erule_tac x = y in allE)
    5.18  by (auto simp: mem_def)
    5.19  
    5.20 -lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    5.21 +lemma rtrancl_def [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    5.22  by simp
    5.23  
    5.24 -lemma rtranclp_def [nitpick_def, no_atp]:
    5.25 +lemma rtranclp_def [nitpick_unfold, no_atp]:
    5.26  "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
    5.27  by (rule eq_reflection) (auto dest: rtranclpD)
    5.28  
    5.29 -lemma tranclp_def [nitpick_def, no_atp]:
    5.30 +lemma tranclp_def [nitpick_unfold, no_atp]:
    5.31  "tranclp r a b \<equiv> trancl (split r) (a, b)"
    5.32  by (simp add: trancl_def Collect_def mem_def)
    5.33  
    5.34 @@ -119,7 +115,7 @@
    5.35  apply (erule contrapos_np)
    5.36  by (rule someI)
    5.37  
    5.38 -lemma unit_case_def [nitpick_def, no_atp]:
    5.39 +lemma unit_case_def [nitpick_unfold, no_atp]:
    5.40  "unit_case x u \<equiv> x"
    5.41  apply (subgoal_tac "u = ()")
    5.42   apply (simp only: unit.cases)
    5.43 @@ -127,7 +123,7 @@
    5.44  
    5.45  declare unit.cases [nitpick_simp del]
    5.46  
    5.47 -lemma nat_case_def [nitpick_def, no_atp]:
    5.48 +lemma nat_case_def [nitpick_unfold, no_atp]:
    5.49  "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
    5.50  apply (rule eq_reflection)
    5.51  by (case_tac n) auto
     6.1 --- a/src/HOL/Product_Type.thy	Mon Feb 21 10:42:29 2011 +0100
     6.2 +++ b/src/HOL/Product_Type.thy	Mon Feb 21 10:44:19 2011 +0100
     6.3 @@ -392,7 +392,7 @@
     6.4  code_const fst and snd
     6.5    (Haskell "fst" and "snd")
     6.6  
     6.7 -lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))"
     6.8 +lemma prod_case_unfold [nitpick_unfold]: "prod_case = (%c p. c (fst p) (snd p))"
     6.9    by (simp add: fun_eq_iff split: prod.split)
    6.10  
    6.11  lemma fst_eqD: "fst (x, y) = a ==> x = a"
     7.1 --- a/src/HOL/Rat.thy	Mon Feb 21 10:42:29 2011 +0100
     7.2 +++ b/src/HOL/Rat.thy	Mon Feb 21 10:44:19 2011 +0100
     7.3 @@ -1199,7 +1199,7 @@
     7.4      (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})]
     7.5  *}
     7.6  
     7.7 -lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
     7.8 +lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat
     7.9    number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_rat
    7.10    ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
    7.11    uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
     8.1 --- a/src/HOL/RealDef.thy	Mon Feb 21 10:42:29 2011 +0100
     8.2 +++ b/src/HOL/RealDef.thy	Mon Feb 21 10:44:19 2011 +0100
     8.3 @@ -1829,7 +1829,7 @@
     8.4      (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
     8.5  *}
     8.6  
     8.7 -lemmas [nitpick_def] = inverse_real_inst.inverse_real
     8.8 +lemmas [nitpick_unfold] = inverse_real_inst.inverse_real
     8.9      number_real_inst.number_of_real one_real_inst.one_real
    8.10      ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real
    8.11      times_real_inst.times_real uminus_real_inst.uminus_real
     9.1 --- a/src/HOL/Relation.thy	Mon Feb 21 10:42:29 2011 +0100
     9.2 +++ b/src/HOL/Relation.thy	Mon Feb 21 10:44:19 2011 +0100
     9.3 @@ -132,7 +132,7 @@
     9.4  lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
     9.5  by blast
     9.6  
     9.7 -lemma Id_on_def'[nitpick_def, code]:
     9.8 +lemma Id_on_def' [nitpick_unfold, code]:
     9.9    "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \<and> A x)"
    9.10  by (auto simp add: fun_eq_iff
    9.11    elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def])
    9.12 @@ -227,7 +227,7 @@
    9.13  lemma refl_on_Id_on: "refl_on A (Id_on A)"
    9.14  by (rule refl_onI [OF Id_on_subset_Times Id_onI])
    9.15  
    9.16 -lemma refl_on_def'[nitpick_def, code]:
    9.17 +lemma refl_on_def' [nitpick_unfold, code]:
    9.18    "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
    9.19  by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
    9.20  
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 10:42:29 2011 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 10:44:19 2011 +0100
    10.3 @@ -1850,7 +1850,7 @@
    10.4         |> AList.group (op =) |> Symtab.make
    10.5  
    10.6  fun const_def_tables ctxt subst ts =
    10.7 -  (def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst,
    10.8 +  (def_table_for (map prop_of o Nitpick_Unfolds.get) ctxt subst,
    10.9     fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
   10.10          (map pair_for_prop ts) Symtab.empty)
   10.11  
    11.1 --- a/src/HOL/Tools/inductive.ML	Mon Feb 21 10:42:29 2011 +0100
    11.2 +++ b/src/HOL/Tools/inductive.ML	Mon Feb 21 10:44:19 2011 +0100
    11.3 @@ -774,7 +774,7 @@
    11.4        |> Local_Theory.conceal
    11.5        |> Local_Theory.define
    11.6          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    11.7 -         ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
    11.8 +         ((Binding.empty, [Attrib.internal (K Nitpick_Unfolds.add)]),
    11.9           fold_rev lambda params
   11.10             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
   11.11        ||> Local_Theory.restore_naming lthy;
    12.1 --- a/src/HOL/Transitive_Closure.thy	Mon Feb 21 10:42:29 2011 +0100
    12.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Feb 21 10:44:19 2011 +0100
    12.3 @@ -33,10 +33,10 @@
    12.4      r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
    12.5    | trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+"
    12.6  
    12.7 -declare rtrancl_def [nitpick_def del]
    12.8 -        rtranclp_def [nitpick_def del]
    12.9 -        trancl_def [nitpick_def del]
   12.10 -        tranclp_def [nitpick_def del]
   12.11 +declare rtrancl_def [nitpick_unfold del]
   12.12 +        rtranclp_def [nitpick_unfold del]
   12.13 +        trancl_def [nitpick_unfold del]
   12.14 +        tranclp_def [nitpick_unfold del]
   12.15  
   12.16  notation
   12.17    rtranclp  ("(_^**)" [1000] 1000) and