# HG changeset patch
# User blanchet
# Date 1266069849 -3600
# Node ID c57dba9733918ac7dfed3905abc55c3ae9bd37b2
# Parent  4b198af5beb5bec4548b7e39ebb1275d8fb13bef
more work on Nitpick's support for nonstandard models + fix in model reconstruction

diff -r 4b198af5beb5 -r c57dba973391 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Sat Feb 13 11:56:06 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Sat Feb 13 15:04:09 2010 +0100
@@ -1331,7 +1331,7 @@
 and this time \textit{arith} can finish off the subgoals.
 
 A similar technique can be employed for structural induction. The
-following mini-formalization of full binary trees will serve as illustration:
+following mini formalization of full binary trees will serve as illustration:
 
 \prew
 \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]
@@ -1350,8 +1350,7 @@
 obtained by swapping $a$ and $b$:
 
 \prew
-\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\
-\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
+\textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
 \postw
 
 Nitpick can't find any counterexample, so we proceed with induction
@@ -1370,29 +1369,29 @@
 \prew
 \slshape
 Hint: To check that the induction hypothesis is general enough, try this command:
-\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
+\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_all}].
 \postw
 
 If we follow the hint, we get a ``nonstandard'' counterexample for the step:
 
 \prew
-\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
+\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
 \hbox{}\qquad Free variables: \nopagebreak \\
 \hbox{}\qquad\qquad $a = a_1$ \\
 \hbox{}\qquad\qquad $b = a_2$ \\
 \hbox{}\qquad\qquad $t = \xi_1$ \\
 \hbox{}\qquad\qquad $u = \xi_2$ \\
+\hbox{}\qquad Datatype: \nopagebreak \\
+\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\}$ \\
 \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
 \hbox{}\qquad\qquad $\textit{labels} = \undef
     (\!\begin{aligned}[t]%
-    & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING
-    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt]
-    & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\
+    & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
+    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
 \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
     (\!\begin{aligned}[t]%
     & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
-    & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt]
-    & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount]
+    & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
 The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
 even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
 \postw
@@ -1408,9 +1407,9 @@
 \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
 set of objects over which the induction is performed while doing the step
 in order to test the induction hypothesis's strength.}
-The new trees are so nonstandard that we know nothing about them, except what
-the induction hypothesis states and what can be proved about all trees without
-relying on induction or case distinction. The key observation is,
+Unlike standard trees, these new trees contain cycles. We will see later that
+every property of acyclic trees that can be proved without using induction also
+holds for cyclic trees. Hence,
 %
 \begin{quote}
 \textsl{If the induction
@@ -1418,9 +1417,9 @@
 objects, and Nitpick won't find any nonstandard counterexample.}
 \end{quote}
 %
-But here, Nitpick did find some nonstandard trees $t = \xi_1$
-and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin
-\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
+But here the tool find some nonstandard trees $t = \xi_1$
+and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
+\textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
 Because neither tree contains both $a$ and $b$, the induction hypothesis tells
 us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
 and as a result we know nothing about the labels of the tree
diff -r 4b198af5beb5 -r c57dba973391 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Sat Feb 13 11:56:06 2010 +0100
+++ b/src/HOL/Nitpick.thy	Sat Feb 13 15:04:09 2010 +0100
@@ -37,7 +37,6 @@
            and bisim_iterator_max :: bisim_iterator
            and Quot :: "'a \<Rightarrow> 'b"
            and quot_normal :: "'a \<Rightarrow> 'a"
-           and Silly :: "'a \<Rightarrow> 'b"
            and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
 
 datatype ('a, 'b) pair_box = PairBox 'a 'b
@@ -45,7 +44,6 @@
 
 typedecl unsigned_bit
 typedecl signed_bit
-typedecl \<xi>
 
 datatype 'a word = Word "('a set)"
 
@@ -254,12 +252,12 @@
 setup {* Nitpick_Isar.setup *}
 
 hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
-    bisim_iterator_max Quot quot_normal Silly Tha PairBox FunBox Word refl' wf'
+    bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
     wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
     int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
     plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
     of_frac
-hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit \<xi> word
+hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
 hide (open) fact 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
diff -r 4b198af5beb5 -r c57dba973391 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Feb 13 11:56:06 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Feb 13 15:04:09 2010 +0100
@@ -259,7 +259,7 @@
  (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
 "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
 
-lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
+lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
 nitpick
 proof (induct t)
   case Leaf thus ?case by simp
diff -r 4b198af5beb5 -r c57dba973391 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 13 11:56:06 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 13 15:04:09 2010 +0100
@@ -54,7 +54,7 @@
 val step_mixfix = "_\<^bsub>step\<^esub>"
 val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
 val cyclic_co_val_name = "\<omega>"
-val cyclic_non_std_type_name = "\<xi>"
+val cyclic_type_name = "\<xi>"
 val opt_flag = nitpick_prefix ^ "opt"
 val non_opt_flag = nitpick_prefix ^ "non_opt"
 
@@ -259,14 +259,13 @@
   | mk_tuple _ (t :: _) = t
   | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
 
-(* string * string * string * string -> scope -> nut list -> nut list
-   -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
-   -> int list list -> term *)
-fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
+(* bool -> atom_pool -> string * string * string * string -> scope -> nut list
+   -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
+   -> typ -> rep -> int list list -> term *)
+fun reconstruct_term elaborate pool (maybe_name, base_name, step_name, abs_name)
         ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
          : scope) sel_names rel_table bounds =
   let
-    val pool = Unsynchronized.ref []
     val for_auto = (maybe_name = "")
     (* int list list -> int *)
     fun value_of_bits jss =
@@ -404,8 +403,11 @@
             (* styp -> int list *)
             fun tuples_for_const (s, T) =
               tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
-            (* unit -> indexname * typ *)
-            fun var () = ((nth_atom_name pool "" T j k, 0), T)
+            (* unit -> term *)
+            fun cyclic_atom () =
+              nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
+            fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
+
             val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
                                  constrs
             val real_j = j + offset_of_type ofs T
@@ -432,8 +434,9 @@
             val uncur_arg_Ts = binder_types constr_T
             val maybe_cyclic = co orelse not standard
           in
-            if maybe_cyclic andalso member (op =) seen (T, j) then
-              Var (var ())
+            if maybe_cyclic andalso not (null seen) andalso
+               member (op =) (seen |> elaborate ? (fst o split_last)) (T, j) then
+              cyclic_var ()
             else if constr_s = @{const_name Word} then
               HOLogic.mk_number
                   (if T = @{typ "unsigned_bit word"} then nat_T else int_T)
@@ -476,16 +479,23 @@
                     list_comb (Const constr_x, ts)
               in
                 if maybe_cyclic then
-                  let val var = var () in
-                    if exists_subterm (curry (op =) (Var var)) t then
+                  let val var = cyclic_var () in
+                    if elaborate andalso not standard andalso
+                       length seen = 1 andalso
+                       exists_subterm (fn Const (s, _) =>
+                                          String.isPrefix cyclic_type_name s
+                                        | t' => t' = var) t then
+                      let val atom = cyclic_atom () in
+                        HOLogic.mk_eq (atom, subst_atomic [(var, atom)] t)
+                      end
+                    else if exists_subterm (curry (op =) var) t then
                       if co then
                         Const (@{const_name The}, (T --> bool_T) --> T)
                         $ Abs (cyclic_co_val_name, T,
                                Const (@{const_name "op ="}, T --> T --> bool_T)
-                               $ Bound 0 $ abstract_over (Var var, t))
+                               $ Bound 0 $ abstract_over (var, t))
                       else
-                        nth_atom pool for_auto
-                                 (Type (cyclic_non_std_type_name, [])) j k
+                        cyclic_atom ()
                     else
                       t
                   end
@@ -541,17 +551,15 @@
         raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
                    Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
                    string_of_int (length jss))
-  in
-    polish_funs [] o unbit_and_unbox_term oooo term_for_rep []
-  end
+  in polish_funs [] o unbit_and_unbox_term oooo term_for_rep [] end
 
-(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
-   -> term *)
-fun term_for_name scope sel_names rel_table bounds name =
+(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
+   -> nut -> term *)
+fun term_for_name pool scope sel_names rel_table bounds name =
   let val T = type_of name in
     tuple_list_for_name rel_table bounds name
-    |> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T
-                        (rep_of name)
+    |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table
+                        bounds T T (rep_of name)
   end
 
 (* Proof.context -> (string * string * string * string) * Proof.context *)
@@ -614,6 +622,7 @@
          card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
         formats all_frees free_names sel_names nonsel_names rel_table bounds =
   let
+    val pool = Unsynchronized.ref []
     val (wacky_names as (_, base_name, step_name, _), ctxt) =
       add_wacky_syntax ctxt
     val hol_ctxt =
@@ -633,11 +642,13 @@
     val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
                  bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
                  ofs = ofs}
-    (* typ -> typ -> rep -> int list list -> term *)
-    val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table
-                                        bounds
+    (* bool -> typ -> typ -> rep -> int list list -> term *)
+    fun term_for_rep elaborate =
+      reconstruct_term elaborate pool wacky_names scope sel_names rel_table
+                       bounds
     (* nat -> typ -> nat -> typ *)
-    fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]]
+    fun nth_value_of_type card T n =
+      term_for_rep true T T (Atom (card, 0)) [[n]]
     (* nat -> typ -> typ list *)
     fun all_values_of_type card T =
       index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord
@@ -670,7 +681,7 @@
                    Const (@{const_name undefined}, T')
                  else
                    tuple_list_for_name rel_table bounds name
-                   |> term_for_rep T T' (rep_of name)
+                   |> term_for_rep false T T' (rep_of name)
       in
         Pretty.block (Pretty.breaks
             [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
@@ -763,7 +774,7 @@
     (* nut -> term *)
     fun free_name_assm name =
       HOLogic.mk_eq (Free (nickname_of name, type_of name),
-                     term_for_name scope sel_names rel_table bounds name)
+                     term_for_name pool scope sel_names rel_table bounds name)
     val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
     val model_assms = map free_name_assm free_names
     val assm = foldr1 s_conj (freeT_assms @ model_assms)