1.1 --- a/doc-src/Nitpick/nitpick.tex	Sat Feb 13 11:56:06 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Sat Feb 13 15:04:09 2010 +0100
     1.3 @@ -1331,7 +1331,7 @@
     1.4  and this time \textit{arith} can finish off the subgoals.
     1.5  
     1.6  A similar technique can be employed for structural induction. The
     1.7 -following mini-formalization of full binary trees will serve as illustration:
     1.8 +following mini formalization of full binary trees will serve as illustration:
     1.9  
    1.10  \prew
    1.11  \textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
    1.12 @@ -1350,8 +1350,7 @@
    1.13  obtained by swapping $a$ and $b$:
    1.14  
    1.15  \prew
    1.16 -\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\
    1.17 -\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
    1.18 +\textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
    1.19  \postw
    1.20  
    1.21  Nitpick can't find any counterexample, so we proceed with induction
    1.22 @@ -1370,29 +1369,29 @@
    1.23  \prew
    1.24  \slshape
    1.25  Hint: To check that the induction hypothesis is general enough, try this command:
    1.26 -\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
    1.27 +\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_all}].
    1.28  \postw
    1.29  
    1.30  If we follow the hint, we get a ``nonstandard'' counterexample for the step:
    1.31  
    1.32  \prew
    1.33 -\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
    1.34 +\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
    1.35  \hbox{}\qquad Free variables: \nopagebreak \\
    1.36  \hbox{}\qquad\qquad $a = a_1$ \\
    1.37  \hbox{}\qquad\qquad $b = a_2$ \\
    1.38  \hbox{}\qquad\qquad $t = \xi_1$ \\
    1.39  \hbox{}\qquad\qquad $u = \xi_2$ \\
    1.40 +\hbox{}\qquad Datatype: \nopagebreak \\
    1.41 +\hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\
    1.42  \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
    1.43  \hbox{}\qquad\qquad $\textit{labels} = \undef
    1.44      (\!\begin{aligned}[t]%
    1.45 -    & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING
    1.46 -    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt]
    1.47 -    & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\
    1.48 +    & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
    1.49 +    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
    1.50  \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
    1.51      (\!\begin{aligned}[t]%
    1.52      & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
    1.53 -    & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt]
    1.54 -    & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount]
    1.55 +    & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
    1.56  The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
    1.57  even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
    1.58  \postw
    1.59 @@ -1408,9 +1407,9 @@
    1.60  \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
    1.61  set of objects over which the induction is performed while doing the step
    1.62  in order to test the induction hypothesis's strength.}
    1.63 -The new trees are so nonstandard that we know nothing about them, except what
    1.64 -the induction hypothesis states and what can be proved about all trees without
    1.65 -relying on induction or case distinction. The key observation is,
    1.66 +Unlike standard trees, these new trees contain cycles. We will see later that
    1.67 +every property of acyclic trees that can be proved without using induction also
    1.68 +holds for cyclic trees. Hence,
    1.69  %
    1.70  \begin{quote}
    1.71  \textsl{If the induction
    1.72 @@ -1418,9 +1417,9 @@
    1.73  objects, and Nitpick won't find any nonstandard counterexample.}
    1.74  \end{quote}
    1.75  %
    1.76 -But here, Nitpick did find some nonstandard trees $t = \xi_1$
    1.77 -and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin
    1.78 -\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
    1.79 +But here the tool find some nonstandard trees $t = \xi_1$
    1.80 +and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
    1.81 +\textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
    1.82  Because neither tree contains both $a$ and $b$, the induction hypothesis tells
    1.83  us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
    1.84  and as a result we know nothing about the labels of the tree

     2.1 --- a/src/HOL/Nitpick.thy	Sat Feb 13 11:56:06 2010 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Sat Feb 13 15:04:09 2010 +0100
     2.3 @@ -37,7 +37,6 @@
     2.4             and bisim_iterator_max :: bisim_iterator
     2.5             and Quot :: "'a \<Rightarrow> 'b"
     2.6             and quot_normal :: "'a \<Rightarrow> 'a"
     2.7 -           and Silly :: "'a \<Rightarrow> 'b"
     2.8             and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     2.9  
    2.10  datatype ('a, 'b) pair_box = PairBox 'a 'b
    2.11 @@ -45,7 +44,6 @@
    2.12  
    2.13  typedecl unsigned_bit
    2.14  typedecl signed_bit
    2.15 -typedecl \<xi>
    2.16  
    2.17  datatype 'a word = Word "('a set)"
    2.18  
    2.19 @@ -254,12 +252,12 @@
    2.20  setup {* Nitpick_Isar.setup *}
    2.21  
    2.22  hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    2.23 -    bisim_iterator_max Quot quot_normal Silly Tha PairBox FunBox Word refl' wf'
    2.24 +    bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
    2.25      wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
    2.26      int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
    2.27      plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
    2.28      of_frac
    2.29 -hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit \<xi> word
    2.30 +hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
    2.31  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    2.32      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    2.33      The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def

     3.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Feb 13 11:56:06 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Feb 13 15:04:09 2010 +0100
     3.3 @@ -259,7 +259,7 @@
     3.4   (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
     3.5  "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
     3.6  
     3.7 -lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
     3.8 +lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
     3.9  nitpick
    3.10  proof (induct t)
    3.11    case Leaf thus ?case by simp

     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 13 11:56:06 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 13 15:04:09 2010 +0100
     4.3 @@ -54,7 +54,7 @@
     4.4  val step_mixfix = "_\<^bsub>step\<^esub>"
     4.5  val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
     4.6  val cyclic_co_val_name = "\<omega>"
     4.7 -val cyclic_non_std_type_name = "\<xi>"
     4.8 +val cyclic_type_name = "\<xi>"
     4.9  val opt_flag = nitpick_prefix ^ "opt"
    4.10  val non_opt_flag = nitpick_prefix ^ "non_opt"
    4.11  
    4.12 @@ -259,14 +259,13 @@
    4.13    | mk_tuple _ (t :: _) = t
    4.14    | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
    4.15  
    4.16 -(* string * string * string * string -> scope -> nut list -> nut list
    4.17 -   -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
    4.18 -   -> int list list -> term *)
    4.19 -fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
    4.20 +(* bool -> atom_pool -> string * string * string * string -> scope -> nut list
    4.21 +   -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
    4.22 +   -> typ -> rep -> int list list -> term *)
    4.23 +fun reconstruct_term elaborate pool (maybe_name, base_name, step_name, abs_name)
    4.24          ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
    4.25           : scope) sel_names rel_table bounds =
    4.26    let
    4.27 -    val pool = Unsynchronized.ref []
    4.28      val for_auto = (maybe_name = "")
    4.29      (* int list list -> int *)
    4.30      fun value_of_bits jss =
    4.31 @@ -404,8 +403,11 @@
    4.32              (* styp -> int list *)
    4.33              fun tuples_for_const (s, T) =
    4.34                tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
    4.35 -            (* unit -> indexname * typ *)
    4.36 -            fun var () = ((nth_atom_name pool "" T j k, 0), T)
    4.37 +            (* unit -> term *)
    4.38 +            fun cyclic_atom () =
    4.39 +              nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
    4.40 +            fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
    4.41 +
    4.42              val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
    4.43                                   constrs
    4.44              val real_j = j + offset_of_type ofs T
    4.45 @@ -432,8 +434,9 @@
    4.46              val uncur_arg_Ts = binder_types constr_T
    4.47              val maybe_cyclic = co orelse not standard
    4.48            in
    4.49 -            if maybe_cyclic andalso member (op =) seen (T, j) then
    4.50 -              Var (var ())
    4.51 +            if maybe_cyclic andalso not (null seen) andalso
    4.52 +               member (op =) (seen |> elaborate ? (fst o split_last)) (T, j) then
    4.53 +              cyclic_var ()
    4.54              else if constr_s = @{const_name Word} then
    4.55                HOLogic.mk_number
    4.56                    (if T = @{typ "unsigned_bit word"} then nat_T else int_T)
    4.57 @@ -476,16 +479,23 @@
    4.58                      list_comb (Const constr_x, ts)
    4.59                in
    4.60                  if maybe_cyclic then
    4.61 -                  let val var = var () in
    4.62 -                    if exists_subterm (curry (op =) (Var var)) t then
    4.63 +                  let val var = cyclic_var () in
    4.64 +                    if elaborate andalso not standard andalso
    4.65 +                       length seen = 1 andalso
    4.66 +                       exists_subterm (fn Const (s, _) =>
    4.67 +                                          String.isPrefix cyclic_type_name s
    4.68 +                                        | t' => t' = var) t then
    4.69 +                      let val atom = cyclic_atom () in
    4.70 +                        HOLogic.mk_eq (atom, subst_atomic [(var, atom)] t)
    4.71 +                      end
    4.72 +                    else if exists_subterm (curry (op =) var) t then
    4.73                        if co then
    4.74                          Const (@{const_name The}, (T --> bool_T) --> T)
    4.75                          $ Abs (cyclic_co_val_name, T,
    4.76                                 Const (@{const_name "op ="}, T --> T --> bool_T)
    4.77 -                               $ Bound 0 $ abstract_over (Var var, t))
    4.78 +                               $ Bound 0 $ abstract_over (var, t))
    4.79                        else
    4.80 -                        nth_atom pool for_auto
    4.81 -                                 (Type (cyclic_non_std_type_name, [])) j k
    4.82 +                        cyclic_atom ()
    4.83                      else
    4.84                        t
    4.85                    end
    4.86 @@ -541,17 +551,15 @@
    4.87          raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
    4.88                     Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
    4.89                     string_of_int (length jss))
    4.90 -  in
    4.91 -    polish_funs [] o unbit_and_unbox_term oooo term_for_rep []
    4.92 -  end
    4.93 +  in polish_funs [] o unbit_and_unbox_term oooo term_for_rep [] end
    4.94  
    4.95 -(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
    4.96 -   -> term *)
    4.97 -fun term_for_name scope sel_names rel_table bounds name =
    4.98 +(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
    4.99 +   -> nut -> term *)
   4.100 +fun term_for_name pool scope sel_names rel_table bounds name =
   4.101    let val T = type_of name in
   4.102      tuple_list_for_name rel_table bounds name
   4.103 -    |> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T
   4.104 -                        (rep_of name)
   4.105 +    |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table
   4.106 +                        bounds T T (rep_of name)
   4.107    end
   4.108  
   4.109  (* Proof.context -> (string * string * string * string) * Proof.context *)
   4.110 @@ -614,6 +622,7 @@
   4.111           card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
   4.112          formats all_frees free_names sel_names nonsel_names rel_table bounds =
   4.113    let
   4.114 +    val pool = Unsynchronized.ref []
   4.115      val (wacky_names as (_, base_name, step_name, _), ctxt) =
   4.116        add_wacky_syntax ctxt
   4.117      val hol_ctxt =
   4.118 @@ -633,11 +642,13 @@
   4.119      val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
   4.120                   bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
   4.121                   ofs = ofs}
   4.122 -    (* typ -> typ -> rep -> int list list -> term *)
   4.123 -    val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table
   4.124 -                                        bounds
   4.125 +    (* bool -> typ -> typ -> rep -> int list list -> term *)
   4.126 +    fun term_for_rep elaborate =
   4.127 +      reconstruct_term elaborate pool wacky_names scope sel_names rel_table
   4.128 +                       bounds
   4.129      (* nat -> typ -> nat -> typ *)
   4.130 -    fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]]
   4.131 +    fun nth_value_of_type card T n =
   4.132 +      term_for_rep true T T (Atom (card, 0)) [[n]]
   4.133      (* nat -> typ -> typ list *)
   4.134      fun all_values_of_type card T =
   4.135        index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord
   4.136 @@ -670,7 +681,7 @@
   4.137                     Const (@{const_name undefined}, T')
   4.138                   else
   4.139                     tuple_list_for_name rel_table bounds name
   4.140 -                   |> term_for_rep T T' (rep_of name)
   4.141 +                   |> term_for_rep false T T' (rep_of name)
   4.142        in
   4.143          Pretty.block (Pretty.breaks
   4.144              [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
   4.145 @@ -763,7 +774,7 @@
   4.146      (* nut -> term *)
   4.147      fun free_name_assm name =
   4.148        HOLogic.mk_eq (Free (nickname_of name, type_of name),
   4.149 -                     term_for_name scope sel_names rel_table bounds name)
   4.150 +                     term_for_name pool scope sel_names rel_table bounds name)
   4.151      val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
   4.152      val model_assms = map free_name_assm free_names
   4.153      val assm = foldr1 s_conj (freeT_assms @ model_assms)