merge
authorblanchet
Tue, 24 Nov 2009 10:33:21 +0100
changeset 33880 6cc01403f78a
parent 33879 8dfc55999130 (diff)
parent 33875 e5e7faaed7ad (current diff)
child 33881 d8958955ecb5
merge
--- a/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 22:59:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 24 10:33:21 2009 +0100
@@ -10,8 +10,8 @@
   * Optimized Kodkod encoding of datatypes whose constructors don't appear in
     the formula to falsify
   * Added support for codatatype view of datatypes
-  * Fixed soundness bugs related to sets, sets of sets, and (co)inductive
-    predicates
+  * Fixed soundness bugs related to sets, sets of sets, (co)inductive
+    predicates, typedefs, and "finite"
   * Fixed monotonicity check
   * Fixed error when processing definitions
   * Fixed error in "star_linear_preds" optimization
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 23 22:59:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Nov 24 10:33:21 2009 +0100
@@ -251,7 +251,7 @@
     val intro_table = inductive_intro_table ctxt def_table
     val ground_thm_table = ground_theorem_table thy
     val ersatz_table = ersatz_table thy
-    val (ext_ctxt as {skolems, special_funs, wf_cache, ...}) =
+    val (ext_ctxt as {wf_cache, ...}) =
       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
        user_axioms = user_axioms, debug = debug, wfs = wfs,
        destroy_constrs = destroy_constrs, specialize = specialize,
@@ -296,11 +296,9 @@
             handle TYPE (_, Ts, ts) =>
                    raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
 
-    val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
-    val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
-                     def_ts
-    val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
-                        nondef_ts
+    val core_u = nut_from_term ext_ctxt Eq core_t
+    val def_us = map (nut_from_term ext_ctxt DefEq) def_ts
+    val nondef_us = map (nut_from_term ext_ctxt Eq) nondef_ts
     val (free_names, const_names) =
       fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
     val (sel_names, nonsel_names) =
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 22:59:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 24 10:33:21 2009 +0100
@@ -496,7 +496,7 @@
 type typedef_info =
   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
    set_def: thm option, prop_of_Rep: thm, set_name: string,
-   Rep_inverse: thm option}
+   Abs_inverse: thm option, Rep_inverse: thm option}
 
 (* theory -> string -> typedef_info *)
 fun typedef_info thy s =
@@ -505,13 +505,14 @@
           Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
           set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
                           |> Logic.varify,
-          set_name = @{const_name Frac}, Rep_inverse = NONE}
+          set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   else case Typedef.get_info thy s of
-    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Rep_inverse,
-          ...} =>
+    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
+          Rep_inverse, ...} =>
     SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
           Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
-          set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}
+          set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
+          Rep_inverse = SOME Rep_inverse}
   | NONE => NONE
 
 (* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
@@ -1288,11 +1289,13 @@
       end
     | NONE => []
   end
-(* theory -> styp -> term *)
-fun inverse_axiom_for_rep_fun thy (x as (_, T)) =
+(* theory -> styp -> term list *)
+fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
   let val abs_T = domain_type T in
-    typedef_info thy (fst (dest_Type abs_T)) |> the |> #Rep_inverse |> the
-    |> prop_of |> Refute.specialize_type thy x
+    typedef_info thy (fst (dest_Type abs_T)) |> the
+    |> pairf #Abs_inverse #Rep_inverse
+    |> pairself (Refute.specialize_type thy x o prop_of o the)
+    ||> single |> op ::
   end
 
 (* theory -> int * styp -> term *)
@@ -1493,14 +1496,7 @@
         let
           val (const, ts) =
             if is_built_in_const fast_descrs x then
-              if s = @{const_name finite} then
-                if is_finite_type ext_ctxt (domain_type T) then
-                  (Abs ("A", domain_type T, @{const True}), ts)
-                else case ts of
-                  [Const (@{const_name top}, _)] => (@{const False}, [])
-                | _ => (Const x, ts)
-              else
-                (Const x, ts)
+              (Const x, ts)
             else case AList.lookup (op =) case_names s of
               SOME n =>
               let
@@ -2475,7 +2471,7 @@
                        list_comb (f (),
                                   map Bound (length trunk_arg_Ts - 1 downto 0))
                    in
-                     List.foldl absdummy
+                     List.foldr absdummy
                                 (Const (set_oper, [set_T, set_T] ---> set_T)
                                         $ app pos $ app neg) trunk_arg_Ts
                    end
@@ -3063,8 +3059,8 @@
                                                     (extra_table def_table s) x)
                      |> add_axioms_for_term depth
                                             (Const (mate_of_rep_fun thy x))
-                     |> add_maybe_def_axiom depth
-                                            (inverse_axiom_for_rep_fun thy x)
+                     |> fold (add_def_axiom depth)
+                             (inverse_axioms_for_rep_fun thy x)
              else
                accum |> user_axioms <> SOME false
                         ? fold (add_nondef_axiom depth)
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 23 22:59:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Nov 24 10:33:21 2009 +0100
@@ -106,7 +106,7 @@
   val name_ord : (nut * nut) -> order
   val the_name : 'a NameTable.table -> nut -> 'a
   val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
-  val nut_from_term : theory -> bool -> special_fun list -> op2 -> term -> nut
+  val nut_from_term : extended_context -> op2 -> term -> nut
   val choose_reps_for_free_vars :
     scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
   val choose_reps_for_consts :
@@ -464,8 +464,8 @@
 fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
   | factorize z = [z]
 
-(* theory -> bool -> special_fun list -> op2 -> term -> nut *)
-fun nut_from_term thy fast_descrs special_funs eq =
+(* extended_context -> op2 -> term -> nut *)
+fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
   let
     (* string list -> typ list -> term -> nut *)
     fun aux eq ss Ts t =
@@ -596,7 +596,11 @@
           Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
         | (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
         | (Const (@{const_name finite}, T), [t1]) =>
-          Op1 (Finite, bool_T, Any, sub t1)
+          (if is_finite_type ext_ctxt (domain_type T) then
+             Cst (True, bool_T, Any)
+           else case t1 of
+             Const (@{const_name top}, _) => Cst (False, bool_T, Any)
+           | _ => Op1 (Finite, bool_T, Any, sub t1))
         | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
         | (Const (@{const_name zero_nat_inst.zero_nat}, T), []) =>
           Cst (Num 0, T, Any)
@@ -678,7 +682,7 @@
              | NONE => if null ts then ConstName (s, T, Any)
                        else do_apply t0 ts)
         | (Free (s, T), []) => FreeName (s, T, Any)
-        | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term", [t])
+        | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
         | (Bound j, []) =>
           BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j)
         | (Abs (s, T, t1), []) =>
--- a/src/HOL/Transitive_Closure.thy	Mon Nov 23 22:59:48 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy	Tue Nov 24 10:33:21 2009 +0100
@@ -33,6 +33,11 @@
     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]
+
 notation
   rtranclp  ("(_^**)" [1000] 1000) and
   tranclp  ("(_^++)" [1000] 1000)