# HG changeset patch
# User blanchet
# Date 1281111090 -7200
# Node ID f418654504508d1dcce1ed4e4798e2aa64628612
# Parent  f26d590dce0fb1e0533148ff64588ad62f2a9e88
added support for partial quotient types;
previously Nitpick was unsound for these

diff -r f26d590dce0f -r f41865450450 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 06 17:23:11 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 06 18:11:30 2010 +0200
@@ -771,9 +771,16 @@
   end
 fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
     let
-      val {qtyp, equiv_rel, ...} = Quotient_Info.quotdata_lookup thy s
+      val {qtyp, equiv_rel, equiv_thm, ...} =
+        Quotient_Info.quotdata_lookup thy s
+      val partial =
+        case prop_of equiv_thm of
+          @{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false
+        | @{const Trueprop} $ (Const (@{const_name part_equivp}, _) $ _) => true
+        | _ => raise NOT_SUPPORTED "Ill-formed quotient type equivalence \
+                                   \relation theorem"
       val Ts' = qtyp |> dest_Type |> snd
-    in subst_atomic_types (Ts' ~~ Ts) equiv_rel end
+    in (subst_atomic_types (Ts' ~~ Ts) equiv_rel, partial) end
   | equiv_relation_for_quot_type _ T =
     raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
 
@@ -1758,7 +1765,8 @@
                       val abs_T = domain_type T
                       val rep_T = domain_type (range_type T)
                       val (rep_fun, _) = quot_rep_of depth Ts abs_T rep_T []
-                      val equiv_rel = equiv_relation_for_quot_type thy abs_T
+                      val (equiv_rel, _) =
+                        equiv_relation_for_quot_type thy abs_T
                     in
                       (Abs (Name.uu, abs_T, equiv_rel $ (rep_fun $ Bound 0)),
                        ts)
@@ -1921,7 +1929,7 @@
     val thy = ProofContext.theory_of ctxt
     val abs_T = Type abs_z
     val rep_T = rep_type_for_quot_type thy abs_T
-    val equiv_rel = equiv_relation_for_quot_type thy abs_T
+    val (equiv_rel, partial) = equiv_relation_for_quot_type thy abs_T
     val a_var = Var (("a", 0), abs_T)
     val x_var = Var (("x", 0), rep_T)
     val y_var = Var (("y", 0), rep_T)
@@ -1943,6 +1951,7 @@
          ([HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)),
            HOLogic.mk_Trueprop (@{const Not} $ HOLogic.mk_eq (normal_x, x_var))],
           HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
+    |> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
   end
 
 fun codatatype_bisim_axioms (hol_ctxt as {thy, ctxt, stds, ...}) T =