src/HOL/Tools/Nitpick/nitpick_nut.ML

     Not |
     Finite |
     Converse |
     Closure |
     SingletonSet |
+    IsUnknown |
     Tha |
     First |
     Second |
     Cast
 

   Not |
   Finite |
   Converse |
   Closure |
   SingletonSet |
+  IsUnknown |
   Tha |
   First |
   Second |
   Cast
 

 fun string_for_op1 Not = "Not"
   | string_for_op1 Finite = "Finite"
   | string_for_op1 Converse = "Converse"
   | string_for_op1 Closure = "Closure"
   | string_for_op1 SingletonSet = "SingletonSet"
+  | string_for_op1 IsUnknown = "IsUnknown"
   | string_for_op1 Tha = "Tha"
   | string_for_op1 First = "First"
   | string_for_op1 Second = "Second"
   | string_for_op1 Cast = "Cast"
 

         | (Const (@{const_name Let}, T), [t1, Abs (s, T', t2)]) =>
           Op3 (Let, nth_range_type 2 T, Any, BoundName (length Ts, T', Any, s),
                sub t1, sub_abs s T' t2)
         | (t0 as Const (@{const_name Let}, T), [t1, t2]) =>
           sub (t0 $ t1 $ eta_expand Ts t2 1)
-        | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
         | (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any)
         | (Const (@{const_name Pair}, T), [t1, t2]) =>
           Tuple (nth_range_type 2 T, Any, map sub [t1, t2])
         | (Const (@{const_name fst}, T), [t1]) =>
           Op1 (First, range_type T, Any, sub t1)

           end
         | (Const (@{const_name ord_int_inst.less_int}, T), [t1, t2]) =>
           Op2 (Less, bool_T, Any, sub t1, sub t2)
         | (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) =>
           Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
+        | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
+        | (Const (@{const_name is_unknown}, T), [t1]) =>
+          Op1 (IsUnknown, bool_T, Any, sub t1)
         | (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
           Op1 (Tha, T2, Any, sub t1)
         | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
         | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
         | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>

     val x as (s, T) = (nickname_of v, type_of v)
     val R = (if is_abs_fun thy x then
                rep_for_abs_fun
              else if is_rep_fun thy x then
                Func oo best_non_opt_symmetric_reps_for_fun_type
-             else if all_exact orelse is_skolem_name v
-                     orelse member (op =) [@{const_name undefined_fast_The},
-                                           @{const_name undefined_fast_Eps},
-                                           @{const_name bisim},
-                                           @{const_name bisim_iterator_max}]
-                                          (original_name s) then
+             else if all_exact orelse is_skolem_name v orelse
+                    member (op =) [@{const_name undefined_fast_The},
+                                   @{const_name undefined_fast_Eps},
+                                   @{const_name bisim},
+                                   @{const_name bisim_iterator_max}]
+                           (original_name s) then
                best_non_opt_set_rep_for_type
              else if member (op =) [@{const_name set}, @{const_name distinct},
                                     @{const_name ord_class.less},
                                     @{const_name ord_class.less_eq}]
                                    (original_name s) then

    -> nut list * rep NameTable.table *)
 fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n
                                       (vs, table) =
   let
     val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
-    val R' = if n = ~1 orelse is_word_type (body_type T)
-                orelse (is_fun_type (range_type T')
-                        andalso is_boolean_type (body_type T')) then
+    val R' = if n = ~1 orelse is_word_type (body_type T) orelse
+                (is_fun_type (range_type T') andalso
+                 is_boolean_type (body_type T')) then
                best_non_opt_set_rep_for_type scope T'
              else
                best_opt_set_rep_for_type scope T' |> unopt_rep
     val v = ConstName (s', T', R')
   in (v :: vs, NameTable.update (v, R') table) end

 (* nut -> nut *)
 fun optimize_unit u =
   if rep_of u = Unit then Cst (Unity, type_of u, Unit) else u
 (* typ -> rep -> nut *)
 fun unknown_boolean T R =
-  Cst (case R of
-         Formula Pos => False
-       | Formula Neg => True
-       | _ => Unknown, T, R)
+  Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
+       T, R)
 
 (* op1 -> typ -> rep -> nut -> nut *)
 fun s_op1 oper T R u1 =
   ((if oper = Not then
       if is_Cst True u1 then Cst (False, T, R)

           else if member (op =) [Add, Subtract, Multiply, Divide, Gcd, Lcm]
                          cst then
             let
               val T1 = domain_type T
               val R1 = Atom (spec_of_type scope T1)
-              val total = T1 = nat_T
-                          andalso (cst = Subtract orelse cst = Divide
-                                   orelse cst = Gcd)
+              val total = T1 = nat_T andalso
+                          (cst = Subtract orelse cst = Divide orelse cst = Gcd)
             in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
           else if cst = NatToInt orelse cst = IntToNat then
             let
               val (dom_card, dom_j0) = spec_of_type scope (domain_type T)
               val (ran_card, ran_j0) = spec_of_type scope (range_type T)
-              val total = not (is_word_type (domain_type T))
-                          andalso (if cst = NatToInt then
-                                    max_int_for_card ran_card >= dom_card + 1
-                                  else
-                                    max_int_for_card dom_card < ran_card)
+              val total = not (is_word_type (domain_type T)) andalso
+                          (if cst = NatToInt then
+                             max_int_for_card ran_card >= dom_card + 1
+                           else
+                             max_int_for_card dom_card < ran_card)
             in
               Cst (cst, T, Func (Atom (dom_card, dom_j0),
                                  Atom (ran_card, ran_j0) |> not total ? Opt))
             end
           else

           (case gsub def (flip_polarity polar) u1 of
              Op2 (Triad, T, R, u11, u12) =>
              triad (s_op1 Not T (Formula Pos) u12)
                    (s_op1 Not T (Formula Neg) u11)
            | u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
+        | Op1 (IsUnknown, T, _, u1) =>
+          let val u1 = sub u1 in
+            if is_opt_rep (rep_of u1) then Op1 (IsUnknown, T, Formula Neut, u1)
+            else Cst (False, T, Formula Neut)
+          end
         | Op1 (oper, T, _, u1) =>
           let
             val u1 = sub u1
             val R1 = rep_of u1
             val R = case oper of

             fun hybrid_case u =
               (* hackish optimization *)
               if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
               else opt_opt_case ()
           in
-            if liberal orelse polar = Neg
-               orelse is_concrete_type datatypes (type_of u1) then
+            if liberal orelse polar = Neg orelse
+               is_concrete_type datatypes (type_of u1) then
               case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
                 (true, true) => opt_opt_case ()
               | (true, false) => hybrid_case u1'
               | (false, true) => hybrid_case u2'
               | (false, false) => non_opt_case ()

              let
                val table' = NameTable.update (u1, R1) table
                val u1' = aux table' false Neut u1
                val u2' = aux table' false Neut u2
                val R =
-                 if is_opt_rep (rep_of u2')
-                    orelse (range_type T = bool_T andalso
-                            not (is_Cst False
-                                        (unrepify_nut_in_nut table false Neut
-                                                             u1 u2
-                                         |> optimize_nut))) then
+                 if is_opt_rep (rep_of u2') orelse
+                    (range_type T = bool_T andalso
+                     not (is_Cst False (unrepify_nut_in_nut table false Neut
+                                                            u1 u2
+                                        |> optimize_nut))) then
                    opt_rep ofs T R
                  else
                    unopt_rep R
              in s_op2 Lambda T R u1' u2' end
            | R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))

             in
               if polar = Neut andalso is_opt_rep (rep_of u2') then
                 triad_fn (fn polar => gsub def polar u)
               else
                 let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
-                  if def
-                     orelse (liberal andalso (polar = Pos) = (oper = All))
-                     orelse is_complete_type datatypes (type_of u1) then
+                  if def orelse
+                     (liberal andalso (polar = Pos) = (oper = All)) orelse
+                     is_complete_type datatypes (type_of u1) then
                     quant_u
                   else
                     let
                       val connective = if oper = All then And else Or
                       val unrepified_u = unrepify_nut_in_nut table def polar

               constr_spec datatypes (original_name (nickname_of (hd us')), T)
             val opt = exists is_opt_rep Rs orelse not total
           in Construct (map sub us', T, R |> opt ? Opt, us) end
         | _ =>
           let val u = modify_name_rep u (the_name table u) in
-            if polar = Neut orelse not (is_boolean_type (type_of u))
-               orelse not (is_opt_rep (rep_of u)) then
+            if polar = Neut orelse not (is_boolean_type (type_of u)) orelse
+               not (is_opt_rep (rep_of u)) then
               u
             else
               s_op1 Cast (type_of u) (Formula polar) u
           end
       end