wneuper/isa: src/HOL/Tools/Nitpick/nitpick

     1 (*  Title:      HOL/Tools/Nitpick/nitpick_preproc.ML

     2     Author:     Jasmin Blanchette, TU Muenchen

     3     Copyright   2008, 2009, 2010

     5 Nitpick's HOL preprocessor.

     6 *)

     8 signature NITPICK_PREPROC =

     9 sig

    10   type hol_context = Nitpick_HOL.hol_context

    11   val preprocess_formulas :

    12     hol_context -> (typ option * bool option) list

    13     -> (typ option * bool option) list -> term list -> term

    14     -> term list * term list * bool * bool * bool

    15 end;

    17 structure Nitpick_Preproc : NITPICK_PREPROC =

    18 struct

    20 open Nitpick_Util

    21 open Nitpick_HOL

    22 open Nitpick_Mono

    24 fun is_positive_existential polar quant_s =

    25   (polar = Pos andalso quant_s = @{const_name Ex}) orelse

    26   (polar = Neg andalso quant_s <> @{const_name Ex})

    28 val is_descr =

    29   member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The},

    30                  @{const_name safe_Eps}]

    32 (** Binary coding of integers **)

    34 (* If a formula contains a numeral whose absolute value is more than this

    35    threshold, the unary coding is likely not to work well and we prefer the

    36    binary coding. *)

    37 val binary_int_threshold = 3

    39 val may_use_binary_ints =

    40   let

    41     fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =

    42         aux def t1 andalso aux false t2

    43       | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2

    44       | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =

    45         aux def t1 andalso aux false t2

    46       | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2

    47       | aux def (t1 $ t2) = aux def t1 andalso aux def t2

    48       | aux def (t as Const (s, _)) =

    49         (not def orelse t <> @{const Suc}) andalso

    50         not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},

    51                             @{const_name nat_gcd}, @{const_name nat_lcm},

    52                             @{const_name Frac}, @{const_name norm_frac}] s)

    53       | aux def (Abs (_, _, t')) = aux def t'

    54       | aux _ _ = true

    55   in aux end

    56 val should_use_binary_ints =

    57   let

    58     fun aux (t1 $ t2) = aux t1 orelse aux t2

    59       | aux (Const (s, T)) =

    60         ((s = @{const_name times} orelse s = @{const_name div}) andalso

    61          is_integer_type (body_type T)) orelse

    62         (String.isPrefix numeral_prefix s andalso

    63          let val n = the (Int.fromString (unprefix numeral_prefix s)) in

    64            n < ~ binary_int_threshold orelse n > binary_int_threshold

    65          end)

    66       | aux (Abs (_, _, t')) = aux t'

    67       | aux _ = false

    68   in aux end

    70 (** Uncurrying **)

    72 fun add_to_uncurry_table ctxt t =

    73   let

    74     val thy = ProofContext.theory_of ctxt

    75     fun aux (t1 $ t2) args table =

    76         let val table = aux t2 [] table in aux t1 (t2 :: args) table end

    77       | aux (Abs (_, _, t')) _ table = aux t' [] table

    78       | aux (t as Const (x as (s, _))) args table =

    79         if is_built_in_const thy [(NONE, true)] true x orelse

    80            is_constr_like ctxt x orelse

    81            is_sel s orelse s = @{const_name Sigma} then

    82           table

    83         else

    84           Termtab.map_default (t, 65536) (Integer.min (length args)) table

    85       | aux _ _ table = table

    86   in aux t [] end

    88 fun uncurry_prefix_for k j =

    89   uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep

    91 fun uncurry_term table t =

    92   let

    93     fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)

    94       | aux (Abs (s, T, t')) args = s_betapplys [] (Abs (s, T, aux t' []), args)

    95       | aux (t as Const (s, T)) args =

    96         (case Termtab.lookup table t of

    97            SOME n =>

    98            if n >= 2 then

    99              let

   100                val arg_Ts = strip_n_binders n T |> fst

   101                val j =

   102                  if is_iterator_type (hd arg_Ts) then

   103                    1

   104                  else case find_index (not_equal bool_T) arg_Ts of

   105                    ~1 => n

   106                  | j => j

   107                val ((before_args, tuple_args), after_args) =

   108                  args |> chop n |>> chop j

   109                val ((before_arg_Ts, tuple_arg_Ts), rest_T) =

   110                  T |> strip_n_binders n |>> chop j

   111                val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts

   112              in

   113                if n - j < 2 then

   114                  s_betapplys [] (t, args)

   115                else

   116                  s_betapplys []

   117                      (Const (uncurry_prefix_for (n - j) j ^ s,

   118                              before_arg_Ts ---> tuple_T --> rest_T),

   119                       before_args @ [mk_flat_tuple tuple_T tuple_args] @

   120                       after_args)

   121              end

   122            else

   123              s_betapplys [] (t, args)

   124          | NONE => s_betapplys [] (t, args))

   125       | aux t args = s_betapplys [] (t, args)

   126   in aux t [] end

   128 (** Boxing **)

   130 fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, fast_descrs, ...})

   131                              def orig_t =

   132   let

   133     fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =

   134         Type (@{type_name fun}, map box_relational_operator_type Ts)

   135       | box_relational_operator_type (Type (@{type_name prod}, Ts)) =

   136         Type (@{type_name prod}, map (box_type hol_ctxt InPair) Ts)

   137       | box_relational_operator_type T = T

   138     fun add_boxed_types_for_var (z as (_, T)) (T', t') =

   139       case t' of

   140         Var z' => z' = z ? insert (op =) T'

   141       | Const (@{const_name Pair}, _) $ t1 $ t2 =>

   142         (case T' of

   143            Type (_, [T1, T2]) =>

   144            fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]

   145          | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\

   146                             \add_boxed_types_for_var", [T'], []))

   147       | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T

   148     fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =

   149       case t of

   150         @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z

   151       | Const (s0, _) $ t1 $ _ =>

   152         if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then

   153           let

   154             val (t', args) = strip_comb t1

   155             val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')

   156           in

   157             case fold (add_boxed_types_for_var z)

   158                       (fst (strip_n_binders (length args) T') ~~ args) [] of

   159               [T''] => T''

   160             | _ => T

   161           end

   162         else

   163           T

   164       | _ => T

   165     and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =

   166       let

   167         val abs_T' =

   168           if polar = Neut orelse is_positive_existential polar quant_s then

   169             box_type hol_ctxt InFunLHS abs_T

   170           else

   171             abs_T

   172         val body_T = body_type quant_T

   173       in

   174         Const (quant_s, (abs_T' --> body_T) --> body_T)

   175         $ Abs (abs_s, abs_T',

   176                t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)

   177       end

   178     and do_equals new_Ts old_Ts s0 T0 t1 t2 =

   179       let

   180         val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)

   181         val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)

   182         val T = if def then T1

   183                 else [T1, T2] |> sort (int_ord o pairself size_of_typ) |> hd

   184       in

   185         list_comb (Const (s0, T --> T --> body_type T0),

   186                    map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])

   187       end

   188     and do_descr s T =

   189       let val T1 = box_type hol_ctxt InFunLHS (range_type T) in

   190         Const (s, (T1 --> bool_T) --> T1)

   191       end

   192     and do_term new_Ts old_Ts polar t =

   193       case t of

   194         Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>

   195         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1

   196       | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>

   197         do_equals new_Ts old_Ts s0 T0 t1 t2

   198       | @{const "==>"} $ t1 $ t2 =>

   199         @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1

   200         $ do_term new_Ts old_Ts polar t2

   201       | @{const Pure.conjunction} $ t1 $ t2 =>

   202         @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1

   203         $ do_term new_Ts old_Ts polar t2

   204       | @{const Trueprop} $ t1 =>

   205         @{const Trueprop} $ do_term new_Ts old_Ts polar t1

   206       | @{const Not} $ t1 =>

   207         @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1

   208       | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>

   209         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1

   210       | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>

   211         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1

   212       | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>

   213         do_equals new_Ts old_Ts s0 T0 t1 t2

   214       | @{const "op &"} $ t1 $ t2 =>

   215         @{const "op &"} $ do_term new_Ts old_Ts polar t1

   216         $ do_term new_Ts old_Ts polar t2

   217       | @{const "op |"} $ t1 $ t2 =>

   218         @{const "op |"} $ do_term new_Ts old_Ts polar t1

   219         $ do_term new_Ts old_Ts polar t2

   220       | @{const HOL.implies} $ t1 $ t2 =>

   221         @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1

   222         $ do_term new_Ts old_Ts polar t2

   223       | Const (x as (s, T)) =>

   224         if is_descr s then

   225           do_descr s T

   226         else

   227           Const (s, if s = @{const_name converse} orelse

   228                        s = @{const_name trancl} then

   229                       box_relational_operator_type T

   230                     else if String.isPrefix quot_normal_prefix s then

   231                       let val T' = box_type hol_ctxt InFunLHS (domain_type T) in

   232                         T' --> T'

   233                       end

   234                     else if is_built_in_const thy stds fast_descrs x orelse

   235                             s = @{const_name Sigma} then

   236                       T

   237                     else if is_constr_like ctxt x then

   238                       box_type hol_ctxt InConstr T

   239                     else if is_sel s orelse is_rep_fun ctxt x then

   240                       box_type hol_ctxt InSel T

   241                     else

   242                       box_type hol_ctxt InExpr T)

   243       | t1 $ Abs (s, T, t2') =>

   244         let

   245           val t1 = do_term new_Ts old_Ts Neut t1

   246           val T1 = fastype_of1 (new_Ts, t1)

   247           val (s1, Ts1) = dest_Type T1

   248           val T' = hd (snd (dest_Type (hd Ts1)))

   249           val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')

   250           val T2 = fastype_of1 (new_Ts, t2)

   251           val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2

   252         in

   253           s_betapply new_Ts (if s1 = @{type_name fun} then

   254                                t1

   255                              else

   256                                select_nth_constr_arg ctxt stds

   257                                    (@{const_name FunBox},

   258                                     Type (@{type_name fun}, Ts1) --> T1) t1 0

   259                                    (Type (@{type_name fun}, Ts1)), t2)

   260         end

   261       | t1 $ t2 =>

   262         let

   263           val t1 = do_term new_Ts old_Ts Neut t1

   264           val T1 = fastype_of1 (new_Ts, t1)

   265           val (s1, Ts1) = dest_Type T1

   266           val t2 = do_term new_Ts old_Ts Neut t2

   267           val T2 = fastype_of1 (new_Ts, t2)

   268           val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2

   269         in

   270           s_betapply new_Ts (if s1 = @{type_name fun} then

   271                                t1

   272                              else

   273                                select_nth_constr_arg ctxt stds

   274                                    (@{const_name FunBox},

   275                                     Type (@{type_name fun}, Ts1) --> T1) t1 0

   276                                    (Type (@{type_name fun}, Ts1)), t2)

   277         end

   278       | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)

   279       | Var (z as (x, T)) =>

   280         Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z

   281                 else box_type hol_ctxt InExpr T)

   282       | Bound _ => t

   283       | Abs (s, T, t') =>

   284         Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')

   285   in do_term [] [] Pos orig_t end

   287 (** Destruction of constructors **)

   289 val val_var_prefix = nitpick_prefix ^ "v"

   291 fun fresh_value_var Ts k n j t =

   292   Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))

   294 fun has_heavy_bounds_or_vars Ts t =

   295   let

   296     fun aux [] = false

   297       | aux [T] = is_fun_type T orelse is_pair_type T

   298       | aux _ = true

   299   in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end

   301 fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level t

   302                          args seen =

   303   let val t_comb = list_comb (t, args) in

   304     case t of

   305       Const x =>

   306       if not relax andalso is_constr ctxt stds x andalso

   307          not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso

   308          has_heavy_bounds_or_vars Ts t_comb andalso

   309          not (loose_bvar (t_comb, level)) then

   310         let

   311           val (j, seen) = case find_index (curry (op =) t_comb) seen of

   312                             ~1 => (0, t_comb :: seen)

   313                           | j => (j, seen)

   314         in (fresh_value_var Ts k (length seen) j t_comb, seen) end

   315       else

   316         (t_comb, seen)

   317     | _ => (t_comb, seen)

   318   end

   320 fun equations_for_pulled_out_constrs mk_eq Ts k seen =

   321   let val n = length seen in

   322     map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))

   323          (index_seq 0 n) seen

   324   end

   326 fun pull_out_universal_constrs hol_ctxt def t =

   327   let

   328     val k = maxidx_of_term t + 1

   329     fun do_term Ts def t args seen =

   330       case t of

   331         (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>

   332         do_eq_or_imp Ts true def t0 t1 t2 seen

   333       | (t0 as @{const "==>"}) $ t1 $ t2 =>

   334         if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen

   335       | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>

   336         do_eq_or_imp Ts true def t0 t1 t2 seen

   337       | (t0 as @{const HOL.implies}) $ t1 $ t2 =>

   338         do_eq_or_imp Ts false def t0 t1 t2 seen

   339       | Abs (s, T, t') =>

   340         let val (t', seen) = do_term (T :: Ts) def t' [] seen in

   341           (list_comb (Abs (s, T, t'), args), seen)

   342         end

   343       | t1 $ t2 =>

   344         let val (t2, seen) = do_term Ts def t2 [] seen in

   345           do_term Ts def t1 (t2 :: args) seen

   346         end

   347       | _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen

   348     and do_eq_or_imp Ts eq def t0 t1 t2 seen =

   349       let

   350         val (t2, seen) = if eq andalso def then (t2, seen)

   351                          else do_term Ts false t2 [] seen

   352         val (t1, seen) = do_term Ts false t1 [] seen

   353       in (t0 $ t1 $ t2, seen) end

   354     val (concl, seen) = do_term [] def t [] []

   355   in

   356     Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k

   357                                                          seen, concl)

   358   end

   360 fun mk_exists v t =

   361   HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)

   363 fun pull_out_existential_constrs hol_ctxt t =

   364   let

   365     val k = maxidx_of_term t + 1

   366     fun aux Ts num_exists t args seen =

   367       case t of

   368         (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>

   369         let

   370           val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []

   371           val n = length seen'

   372           fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'

   373         in

   374           (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'

   375            |> List.foldl s_conj t1 |> fold mk_exists (vars ())

   376            |> curry3 Abs s1 T1 |> curry (op $) t0, seen)

   377         end

   378       | t1 $ t2 =>

   379         let val (t2, seen) = aux Ts num_exists t2 [] seen in

   380           aux Ts num_exists t1 (t2 :: args) seen

   381         end

   382       | Abs (s, T, t') =>

   383         let

   384           val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)

   385         in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end

   386       | _ =>

   387         if num_exists > 0 then

   388           pull_out_constr_comb hol_ctxt Ts false k num_exists t args seen

   389         else

   390           (list_comb (t, args), seen)

   391   in aux [] 0 t [] [] |> fst end

   393 fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t =

   394   let

   395     val num_occs_of_var =

   396       fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)

   397                     | _ => I) t (K 0)

   398     fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =

   399         aux_eq careful true t0 t1 t2

   400       | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =

   401         t0 $ aux false t1 $ aux careful t2

   402       | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =

   403         aux_eq careful true t0 t1 t2

   404       | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =

   405         t0 $ aux false t1 $ aux careful t2

   406       | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')

   407       | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2

   408       | aux _ t = t

   409     and aux_eq careful pass1 t0 t1 t2 =

   410       ((if careful then

   411           raise SAME ()

   412         else if axiom andalso is_Var t2 andalso

   413                 num_occs_of_var (dest_Var t2) = 1 then

   414           @{const True}

   415         else case strip_comb t2 of

   416           (* The first case is not as general as it could be. *)

   417           (Const (@{const_name PairBox}, _),

   418                   [Const (@{const_name fst}, _) $ Var z1,

   419                    Const (@{const_name snd}, _) $ Var z2]) =>

   420           if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}

   421           else raise SAME ()

   422         | (Const (x as (s, T)), args) =>

   423           let

   424             val (arg_Ts, dataT) = strip_type T

   425             val n = length arg_Ts

   426           in

   427             if length args = n andalso

   428                (is_constr ctxt stds x orelse s = @{const_name Pair} orelse

   429                 x = (@{const_name Suc}, nat_T --> nat_T)) andalso

   430                (not careful orelse not (is_Var t1) orelse

   431                 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then

   432                 s_let "l" (n + 1) dataT bool_T

   433                       (fn t1 => discriminate_value hol_ctxt x t1 ::

   434                                 map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args

   435                                 |> foldr1 s_conj) t1

   436             else

   437               raise SAME ()

   438           end

   439         | _ => raise SAME ())

   440        |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)

   441       handle SAME () => if pass1 then aux_eq careful false t0 t2 t1

   442                         else t0 $ aux false t2 $ aux false t1

   443     and sel_eq x t n nth_T nth_t =

   444       HOLogic.eq_const nth_T $ nth_t

   445                              $ select_nth_constr_arg ctxt stds x t n nth_T

   446       |> aux false

   447   in aux axiom t end

   449 (** Destruction of universal and existential equalities **)

   451 fun curry_assms (@{const "==>"} $ (@{const Trueprop}

   452                                    $ (@{const "op &"} $ t1 $ t2)) $ t3) =

   453     curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))

   454   | curry_assms (@{const "==>"} $ t1 $ t2) =

   455     @{const "==>"} $ curry_assms t1 $ curry_assms t2

   456   | curry_assms t = t

   458 val destroy_universal_equalities =

   459   let

   460     fun aux prems zs t =

   461       case t of

   462         @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2

   463       | _ => Logic.list_implies (rev prems, t)

   464     and aux_implies prems zs t1 t2 =

   465       case t1 of

   466         Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2

   467       | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>

   468         aux_eq prems zs z t' t1 t2

   469       | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>

   470         aux_eq prems zs z t' t1 t2

   471       | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2

   472     and aux_eq prems zs z t' t1 t2 =

   473       if not (member (op =) zs z) andalso

   474          not (exists_subterm (curry (op =) (Var z)) t') then

   475         aux prems zs (subst_free [(Var z, t')] t2)

   476       else

   477         aux (t1 :: prems) (Term.add_vars t1 zs) t2

   478   in aux [] [] end

   480 fun find_bound_assign ctxt stds j =

   481   let

   482     fun do_term _ [] = NONE

   483       | do_term seen (t :: ts) =

   484         let

   485           fun do_eq pass1 t1 t2 =

   486             (if loose_bvar1 (t2, j) then

   487                if pass1 then do_eq false t2 t1 else raise SAME ()

   488              else case t1 of

   489                Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()

   490              | Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>

   491                if j' = j andalso

   492                   s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then

   493                  SOME (construct_value ctxt stds

   494                                        (@{const_name FunBox}, T2 --> T1) [t2],

   495                        ts @ seen)

   496                else

   497                  raise SAME ()

   498              | _ => raise SAME ())

   499             handle SAME () => do_term (t :: seen) ts

   500         in

   501           case t of

   502             Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2

   503           | _ => do_term (t :: seen) ts

   504         end

   505   in do_term end

   507 fun subst_one_bound j arg t =

   508   let

   509     fun aux (Bound i, lev) =

   510         if i < lev then raise SAME ()

   511         else if i = lev then incr_boundvars (lev - j) arg

   512         else Bound (i - 1)

   513       | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))

   514       | aux (f $ t, lev) =

   515         (aux (f, lev) $ (aux (t, lev) handle SAME () => t)

   516          handle SAME () => f $ aux (t, lev))

   517       | aux _ = raise SAME ()

   518   in aux (t, j) handle SAME () => t end

   520 fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) =

   521   let

   522     fun kill [] [] ts = foldr1 s_conj ts

   523       | kill (s :: ss) (T :: Ts) ts =

   524         (case find_bound_assign ctxt stds (length ss) [] ts of

   525            SOME (_, []) => @{const True}

   526          | SOME (arg_t, ts) =>

   527            kill ss Ts (map (subst_one_bound (length ss)

   528                                 (incr_bv (~1, length ss + 1, arg_t))) ts)

   529          | NONE =>

   530            Const (@{const_name Ex}, (T --> bool_T) --> bool_T)

   531            $ Abs (s, T, kill ss Ts ts))

   532       | kill _ _ _ = raise UnequalLengths

   533     fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =

   534         gather (ss @ [s1]) (Ts @ [T1]) t1

   535       | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)

   536       | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2

   537       | gather [] [] t = t

   538       | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t))

   539   in gather [] [] end

   541 (** Skolemization **)

   543 fun skolem_prefix_for k j =

   544   skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep

   546 fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})

   547                             skolem_depth =

   548   let

   549     val incrs = map (Integer.add 1)

   550     fun aux ss Ts js skolemizable polar t =

   551       let

   552         fun do_quantifier quant_s quant_T abs_s abs_T t =

   553           (if not (loose_bvar1 (t, 0)) then

   554              aux ss Ts js skolemizable polar (incr_boundvars ~1 t)

   555            else if is_positive_existential polar quant_s then

   556              let

   557                val j = length (!skolems) + 1

   558                val (js', (ss', Ts')) =

   559                  js ~~ (ss ~~ Ts)

   560                  |> filter (fn (j, _) => loose_bvar1 (t, j + 1))

   561                  |> ListPair.unzip ||> ListPair.unzip

   562              in

   563                if skolemizable andalso length js' <= skolem_depth then

   564                  let

   565                    val sko_s = skolem_prefix_for (length js') j ^ abs_s

   566                    val _ = Unsynchronized.change skolems (cons (sko_s, ss'))

   567                    val sko_t = list_comb (Const (sko_s, rev Ts' ---> abs_T),

   568                                           map Bound (rev js'))

   569                    val abs_t = Abs (abs_s, abs_T,

   570                                     aux ss Ts (incrs js) skolemizable polar t)

   571                  in

   572                    if null js' then

   573                      s_betapply Ts (abs_t, sko_t)

   574                    else

   575                      Const (@{const_name Let}, abs_T --> quant_T) $ sko_t

   576                      $ abs_t

   577                  end

   578                else

   579                  raise SAME ()

   580              end

   581            else

   582              raise SAME ())

   583           handle SAME () =>

   584                  Const (quant_s, quant_T)

   585                  $ Abs (abs_s, abs_T,

   586                         aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)

   587                             (skolemizable andalso

   588                              not (is_higher_order_type abs_T)) polar t)

   589       in

   590         case t of

   591           Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>

   592           do_quantifier s0 T0 s1 T1 t1

   593         | @{const "==>"} $ t1 $ t2 =>

   594           @{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1

   595           $ aux ss Ts js skolemizable polar t2

   596         | @{const Pure.conjunction} $ t1 $ t2 =>

   597           @{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1

   598           $ aux ss Ts js skolemizable polar t2

   599         | @{const Trueprop} $ t1 =>

   600           @{const Trueprop} $ aux ss Ts js skolemizable polar t1

   601         | @{const Not} $ t1 =>

   602           @{const Not} $ aux ss Ts js skolemizable (flip_polarity polar) t1

   603         | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>

   604           do_quantifier s0 T0 s1 T1 t1

   605         | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>

   606           do_quantifier s0 T0 s1 T1 t1

   607         | @{const "op &"} $ t1 $ t2 =>

   608           s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))

   609         | @{const "op |"} $ t1 $ t2 =>

   610           s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))

   611         | @{const HOL.implies} $ t1 $ t2 =>

   612           @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1

   613           $ aux ss Ts js skolemizable polar t2

   614         | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>

   615           t0 $ t1 $ aux ss Ts js skolemizable polar t2

   616         | Const (x as (s, T)) =>

   617           if is_real_inductive_pred hol_ctxt x andalso

   618              not (is_real_equational_fun hol_ctxt x) andalso

   619              not (is_well_founded_inductive_pred hol_ctxt x) then

   620             let

   621               val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)

   622               val (pref, connective) =

   623                 if gfp then (lbfp_prefix, @{const "op |"})

   624                 else (ubfp_prefix, @{const "op &"})

   625               fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x

   626                            |> aux ss Ts js skolemizable polar

   627               fun neg () = Const (pref ^ s, T)

   628             in

   629               case polar |> gfp ? flip_polarity of

   630                 Pos => pos ()

   631               | Neg => neg ()

   632               | Neut =>

   633                 let

   634                   val arg_Ts = binder_types T

   635                   fun app f =

   636                     list_comb (f (), map Bound (length arg_Ts - 1 downto 0))

   637                 in

   638                   List.foldr absdummy (connective $ app pos $ app neg) arg_Ts

   639                 end

   640             end

   641           else

   642             Const x

   643         | t1 $ t2 =>

   644           s_betapply Ts (aux ss Ts js false polar t1,

   645                          aux ss Ts js false Neut t2)

   646         | Abs (s, T, t1) =>

   647           Abs (s, T, aux ss Ts (incrs js) skolemizable polar t1)

   648         | _ => t

   649       end

   650   in aux [] [] [] true Pos end

   652 (** Function specialization **)

   654 fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2

   655   | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1

   656   | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =

   657     snd (strip_comb t1)

   658   | params_in_equation _ = []

   660 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =

   661   let

   662     val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0

   663             + 1

   664     val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t

   665     val fixed_params = filter_indices fixed_js (params_in_equation t)

   666     fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)

   667       | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1

   668       | aux args t =

   669         if t = Const x then

   670           list_comb (Const x', extra_args @ filter_out_indices fixed_js args)

   671         else

   672           let val j = find_index (curry (op =) t) fixed_params in

   673             list_comb (if j >= 0 then nth fixed_args j else t, args)

   674           end

   675   in aux [] t end

   677 fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =

   678   let

   679     fun fun_calls (Abs (_, _, t)) _ = fun_calls t []

   680       | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)

   681       | fun_calls t args =

   682         (case t of

   683            Const (x' as (s', T')) =>

   684            x = x' orelse (case AList.lookup (op =) ersatz_table s' of

   685                             SOME s'' => x = (s'', T')

   686                           | NONE => false)

   687          | _ => false) ? cons args

   688     fun call_sets [] [] vs = [vs]

   689       | call_sets [] uss vs = vs :: call_sets uss [] []

   690       | call_sets ([] :: _) _ _ = []

   691       | call_sets ((t :: ts) :: tss) uss vs =

   692         OrdList.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)

   693     val sets = call_sets (fun_calls t [] []) [] []

   694     val indexed_sets = sets ~~ (index_seq 0 (length sets))

   695   in

   696     fold_rev (fn (set, j) =>

   697                  case set of

   698                    [Var _] => AList.lookup (op =) indexed_sets set = SOME j

   699                               ? cons (j, NONE)

   700                  | [t as Const _] => cons (j, SOME t)

   701                  | [t as Free _] => cons (j, SOME t)

   702                  | _ => I) indexed_sets []

   703   end

   704 fun static_args_in_terms hol_ctxt x =

   705   map (static_args_in_term hol_ctxt x)

   706   #> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))

   708 fun overlapping_indices [] _ = []

   709   | overlapping_indices _ [] = []

   710   | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =

   711     if j1 < j2 then overlapping_indices ps1' ps2

   712     else if j1 > j2 then overlapping_indices ps1 ps2'

   713     else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1

   715 fun is_eligible_arg Ts t =

   716   let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in

   717     null bad_Ts orelse

   718     (is_higher_order_type (fastype_of1 (Ts, t)) andalso

   719      forall (not o is_higher_order_type) bad_Ts)

   720   end

   722 fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep

   724 (* If a constant's definition is picked up deeper than this threshold, we

   725    prevent excessive specialization by not specializing it. *)

   726 val special_max_depth = 20

   728 val bound_var_prefix = "b"

   730 fun special_fun_aconv ((x1, js1, ts1), (x2, js2, ts2)) =

   731   x1 = x2 andalso js1 = js2 andalso length ts1 = length ts2 andalso

   732   forall (op aconv) (ts1 ~~ ts2)

   734 fun specialize_consts_in_term

   735         (hol_ctxt as {ctxt, thy, stds, specialize, fast_descrs, def_table,

   736                       simp_table, special_funs, ...}) def depth t =

   737   if not specialize orelse depth > special_max_depth then

   738     t

   739   else

   740     let

   741       val blacklist =

   742         if def then case term_under_def t of Const x => [x] | _ => [] else []

   743       fun aux args Ts (Const (x as (s, T))) =

   744           ((if not (member (op =) blacklist x) andalso not (null args) andalso

   745                not (String.isPrefix special_prefix s) andalso

   746                not (is_built_in_const thy stds fast_descrs x) andalso

   747                (is_equational_fun_but_no_plain_def hol_ctxt x orelse

   748                 (is_some (def_of_const thy def_table x) andalso

   749                  not (is_of_class_const thy x) andalso

   750                  not (is_constr ctxt stds x) andalso

   751                  not (is_choice_spec_fun hol_ctxt x))) then

   752               let

   753                 val eligible_args = filter (is_eligible_arg Ts o snd)

   754                                            (index_seq 0 (length args) ~~ args)

   755                 val _ = not (null eligible_args) orelse raise SAME ()

   756                 val old_axs = equational_fun_axioms hol_ctxt x

   757                               |> map (destroy_existential_equalities hol_ctxt)

   758                 val static_params = static_args_in_terms hol_ctxt x old_axs

   759                 val fixed_js = overlapping_indices static_params eligible_args

   760                 val _ = not (null fixed_js) orelse raise SAME ()

   761                 val fixed_args = filter_indices fixed_js args

   762                 val vars = fold Term.add_vars fixed_args []

   763                            |> sort (Term_Ord.fast_indexname_ord o pairself fst)

   764                 val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))

   765                                     fixed_args []

   766                                |> sort int_ord

   767                 val live_args = filter_out_indices fixed_js args

   768                 val extra_args = map Var vars @ map Bound bound_js @ live_args

   769                 val extra_Ts = map snd vars @ filter_indices bound_js Ts

   770                 val k = maxidx_of_term t + 1

   771                 fun var_for_bound_no j =

   772                   Var ((bound_var_prefix ^

   773                         nat_subscript (find_index (curry (op =) j) bound_js

   774                                        + 1), k),

   775                        nth Ts j)

   776                 val fixed_args_in_axiom =

   777                   map (curry subst_bounds

   778                              (map var_for_bound_no (index_seq 0 (length Ts))))

   779                       fixed_args

   780               in

   781                 case AList.lookup special_fun_aconv (!special_funs)

   782                                   (x, fixed_js, fixed_args_in_axiom) of

   783                   SOME x' => list_comb (Const x', extra_args)

   784                 | NONE =>

   785                   let

   786                     val extra_args_in_axiom =

   787                       map Var vars @ map var_for_bound_no bound_js

   788                     val x' as (s', _) =

   789                       (special_prefix_for (length (!special_funs) + 1) ^ s,

   790                        extra_Ts @ filter_out_indices fixed_js (binder_types T)

   791                        ---> body_type T)

   792                     val new_axs =

   793                       map (specialize_fun_axiom x x' fixed_js

   794                                fixed_args_in_axiom extra_args_in_axiom) old_axs

   795                     val _ =

   796                       Unsynchronized.change special_funs

   797                           (cons ((x, fixed_js, fixed_args_in_axiom), x'))

   798                     val _ = add_simps simp_table s' new_axs

   799                   in list_comb (Const x', extra_args) end

   800               end

   801             else

   802               raise SAME ())

   803            handle SAME () => list_comb (Const x, args))

   804         | aux args Ts (Abs (s, T, t)) =

   805           list_comb (Abs (s, T, aux [] (T :: Ts) t), args)

   806         | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1

   807         | aux args _ t = list_comb (t, args)

   808     in aux [] [] t end

   810 type special_triple = int list * term list * styp

   812 val cong_var_prefix = "c"

   814 fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) =

   815   let

   816     val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)

   817     val Ts = binder_types T

   818     val max_j = fold (fold Integer.max) [js1, js2] ~1

   819     val (eqs, (args1, args2)) =

   820       fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)

   821                                   (js1 ~~ ts1, js2 ~~ ts2) of

   822                       (SOME t1, SOME t2) => apfst (cons (t1, t2))

   823                     | (SOME t1, NONE) => apsnd (apsnd (cons t1))

   824                     | (NONE, SOME t2) => apsnd (apfst (cons t2))

   825                     | (NONE, NONE) =>

   826                       let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),

   827                                        nth Ts j) in

   828                         apsnd (pairself (cons v))

   829                       end) (max_j downto 0) ([], ([], []))

   830   in

   831     Logic.list_implies (eqs |> filter_out (op aconv) |> distinct (op =)

   832                             |> map Logic.mk_equals,

   833                         Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),

   834                                          list_comb (Const x2, bounds2 @ args2)))

   835   end

   837 fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) ts =

   838   let

   839     val groups =

   840       !special_funs

   841       |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))

   842       |> AList.group (op =)

   843       |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)

   844       |> map (fn (x, zs) =>

   845                  (x, zs |> member (op =) ts (Const x) ? cons ([], [], x)))

   846     fun generality (js, _, _) = ~(length js)

   847     fun is_more_specific (j1, t1, x1) (j2, t2, x2) =

   848       x1 <> x2 andalso length j2 < length j1 andalso

   849       OrdList.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)

   850     fun do_pass_1 _ [] [_] [_] = I

   851       | do_pass_1 T skipped _ [] = do_pass_2 T skipped

   852       | do_pass_1 T skipped all (z :: zs) =

   853         case filter (is_more_specific z) all

   854              |> sort (int_ord o pairself generality) of

   855           [] => do_pass_1 T (z :: skipped) all zs

   856         | (z' :: _) => cons (special_congruence_axiom T z z')

   857                        #> do_pass_1 T skipped all zs

   858     and do_pass_2 _ [] = I

   859       | do_pass_2 T (z :: zs) =

   860         fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs

   861   in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end

   863 (** Axiom selection **)

   865 fun defined_free_by_assumption t =

   866   let

   867     fun do_equals x def =

   868       if exists_subterm (curry (op aconv) (Free x)) def then NONE else SOME x

   869   in

   870     case t of

   871       Const (@{const_name "=="}, _) $ Free x $ def => do_equals x def

   872     | @{const Trueprop} $ (Const (@{const_name "=="}, _) $ Free x $ def) =>

   873       do_equals x def

   874     | _ => NONE

   875   end

   877 fun assumption_exclusively_defines_free assm_ts t =

   878   case defined_free_by_assumption t of

   879     SOME x =>

   880     length (filter ((fn SOME x' => x = x' | NONE => false)

   881                      o defined_free_by_assumption) assm_ts) = 1

   882   | NONE => false

   884 fun all_table_entries table = Symtab.fold (append o snd) table []

   885 fun extra_table table s = Symtab.make [(s, all_table_entries table)]

   887 fun eval_axiom_for_term j t =

   888   Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)

   890 val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)

   892 (* Prevents divergence in case of cyclic or infinite axiom dependencies. *)

   893 val axioms_max_depth = 255

   895 fun axioms_for_term

   896         (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,

   897                       fast_descrs, evals, def_table, nondef_table,

   898                       choice_spec_table, user_nondefs, ...}) assm_ts neg_t =

   899   let

   900     val (def_assm_ts, nondef_assm_ts) =

   901       List.partition (assumption_exclusively_defines_free assm_ts) assm_ts

   902     val def_assm_table = map (`(the o defined_free_by_assumption)) def_assm_ts

   903     type accumulator = styp list * (term list * term list)

   904     fun add_axiom get app def depth t (accum as (seen, axs)) =

   905       let

   906         val t = t |> unfold_defs_in_term hol_ctxt

   907                   |> skolemize_term_and_more hol_ctxt ~1 (* FIXME: why ~1? *)

   908       in

   909         if is_trivial_equation t then

   910           accum

   911         else

   912           let val t' = t |> specialize_consts_in_term hol_ctxt def depth in

   913             if exists (member (op aconv) (get axs)) [t, t'] then accum

   914             else add_axioms_for_term (depth + 1) t' (seen, app (cons t') axs)

   915           end

   916       end

   917     and add_def_axiom depth = add_axiom fst apfst true depth

   918     and add_nondef_axiom depth = add_axiom snd apsnd false depth

   919     and add_maybe_def_axiom depth t =

   920       (if head_of t <> @{const "==>"} then add_def_axiom

   921        else add_nondef_axiom) depth t

   922     and add_eq_axiom depth t =

   923       (if is_constr_pattern_formula ctxt t then add_def_axiom

   924        else add_nondef_axiom) depth t

   925     and add_axioms_for_term depth t (accum as (seen, axs)) =

   926       case t of

   927         t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]

   928       | Const (x as (s, T)) =>

   929         (if member (op aconv) seen t orelse

   930             is_built_in_const thy stds fast_descrs x then

   931            accum

   932          else

   933            let val accum = (t :: seen, axs) in

   934              if depth > axioms_max_depth then

   935                raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\

   936                                 \add_axioms_for_term",

   937                                 "too many nested axioms (" ^

   938                                 string_of_int depth ^ ")")

   939              else if is_of_class_const thy x then

   940                let

   941                  val class = Logic.class_of_const s

   942                  val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),

   943                                                    class)

   944                  val ax1 = try (specialize_type thy x) of_class

   945                  val ax2 = Option.map (specialize_type thy x o snd)

   946                                       (get_class_def thy class)

   947                in

   948                  fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])

   949                       accum

   950                end

   951              else if is_constr ctxt stds x then

   952                accum

   953              else if is_descr (original_name s) then

   954                fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x)

   955                     accum

   956              else if is_equational_fun_but_no_plain_def hol_ctxt x then

   957                fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)

   958                     accum

   959              else if is_choice_spec_fun hol_ctxt x then

   960                fold (add_nondef_axiom depth)

   961                     (nondef_props_for_const thy true choice_spec_table x) accum

   962              else if is_abs_fun ctxt x then

   963                accum |> fold (add_nondef_axiom depth)

   964                              (nondef_props_for_const thy false nondef_table x)

   965                      |> (is_funky_typedef ctxt (range_type T) orelse

   966                          range_type T = nat_T)

   967                         ? fold (add_maybe_def_axiom depth)

   968                                (nondef_props_for_const thy true

   969                                                     (extra_table def_table s) x)

   970              else if is_rep_fun ctxt x then

   971                accum |> fold (add_nondef_axiom depth)

   972                              (nondef_props_for_const thy false nondef_table x)

   973                      |> (is_funky_typedef ctxt (range_type T) orelse

   974                          range_type T = nat_T)

   975                         ? fold (add_maybe_def_axiom depth)

   976                                (nondef_props_for_const thy true

   977                                                     (extra_table def_table s) x)

   978                      |> add_axioms_for_term depth

   979                                             (Const (mate_of_rep_fun ctxt x))

   980                      |> fold (add_def_axiom depth)

   981                              (inverse_axioms_for_rep_fun ctxt x)

   982              else if s = @{const_name TYPE} then

   983                accum

   984              else case def_of_const thy def_table x of

   985                SOME def =>

   986                fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)

   987                     accum

   988              | NONE =>

   989                accum |> user_axioms <> SOME false

   990                         ? fold (add_nondef_axiom depth)

   991                                (nondef_props_for_const thy false nondef_table x)

   992            end)

   993         |> add_axioms_for_type depth T

   994       | Free (x as (_, T)) =>

   995         (if member (op aconv) seen t then

   996            accum

   997          else case AList.lookup (op =) def_assm_table x of

   998            SOME t => add_def_axiom depth t accum

   999          | NONE => accum)

  1000         |> add_axioms_for_type depth T

  1001       | Var (_, T) => add_axioms_for_type depth T accum

  1002       | Bound _ => accum

  1003       | Abs (_, T, t) => accum |> add_axioms_for_term depth t

  1004                                |> add_axioms_for_type depth T

  1005     and add_axioms_for_type depth T =

  1006       case T of

  1007         Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts

  1008       | Type (@{type_name prod}, Ts) => fold (add_axioms_for_type depth) Ts

  1009       | @{typ prop} => I

  1010       | @{typ bool} => I

  1011       | TFree (_, S) => add_axioms_for_sort depth T S

  1012       | TVar (_, S) => add_axioms_for_sort depth T S

  1013       | Type (z as (_, Ts)) =>

  1014         fold (add_axioms_for_type depth) Ts

  1015         #> (if is_pure_typedef ctxt T then

  1016               fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z)

  1017             else if is_quot_type ctxt T then

  1018               fold (add_def_axiom depth)

  1019                    (optimized_quot_type_axioms ctxt stds z)

  1020             else if max_bisim_depth >= 0 andalso is_codatatype ctxt T then

  1021               fold (add_maybe_def_axiom depth)

  1022                    (codatatype_bisim_axioms hol_ctxt T)

  1023             else

  1024               I)

  1025     and add_axioms_for_sort depth T S =

  1026       let

  1027         val supers = Sign.complete_sort thy S

  1028         val class_axioms =

  1029           maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms

  1030                                          handle ERROR _ => [])) supers

  1031         val monomorphic_class_axioms =

  1032           map (fn t => case Term.add_tvars t [] of

  1033                          [] => t

  1034                        | [(x, S)] =>

  1035                          monomorphic_term (Vartab.make [(x, (S, T))]) t

  1036                        | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\

  1037                                           \add_axioms_for_sort", [t]))

  1038               class_axioms

  1039       in fold (add_nondef_axiom depth) monomorphic_class_axioms end

  1040     val (mono_user_nondefs, poly_user_nondefs) =

  1041       List.partition (null o Term.hidden_polymorphism) user_nondefs

  1042     val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))

  1043                            evals

  1044     val (seen, (defs, nondefs)) =

  1045       ([], ([], []))

  1046       |> add_axioms_for_term 1 neg_t

  1047       |> fold_rev (add_nondef_axiom 1) nondef_assm_ts

  1048       |> fold_rev (add_def_axiom 1) eval_axioms

  1049       |> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_user_nondefs

  1050     val defs = defs @ special_congruence_axioms hol_ctxt seen

  1051     val got_all_mono_user_axioms =

  1052       (user_axioms = SOME true orelse null mono_user_nondefs)

  1053   in

  1054     (neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs)

  1055   end

  1057 (** Simplification of constructor/selector terms **)

  1059 fun simplify_constrs_and_sels ctxt t =

  1060   let

  1061     fun is_nth_sel_on t' n (Const (s, _) $ t) =

  1062         (t = t' andalso is_sel_like_and_no_discr s andalso

  1063          sel_no_from_name s = n)

  1064       | is_nth_sel_on _ _ _ = false

  1065     fun do_term (Const (@{const_name Rep_Frac}, _)

  1066                  $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []

  1067       | do_term (Const (@{const_name Abs_Frac}, _)

  1068                  $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []

  1069       | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)

  1070       | do_term (t as Const (x as (s, T))) (args as _ :: _) =

  1071         ((if is_constr_like ctxt x then

  1072             if length args = num_binder_types T then

  1073               case hd args of

  1074                 Const (_, T') $ t' =>

  1075                 if domain_type T' = body_type T andalso

  1076                    forall (uncurry (is_nth_sel_on t'))

  1077                           (index_seq 0 (length args) ~~ args) then

  1078                   t'

  1079                 else

  1080                   raise SAME ()

  1081               | _ => raise SAME ()

  1082             else

  1083               raise SAME ()

  1084           else if is_sel_like_and_no_discr s then

  1085             case strip_comb (hd args) of

  1086               (Const (x' as (s', T')), ts') =>

  1087               if is_constr_like ctxt x' andalso

  1088                  constr_name_for_sel_like s = s' andalso

  1089                  not (exists is_pair_type (binder_types T')) then

  1090                 list_comb (nth ts' (sel_no_from_name s), tl args)

  1091               else

  1092                 raise SAME ()

  1093             | _ => raise SAME ()

  1094           else

  1095             raise SAME ())

  1096          handle SAME () => s_betapplys [] (t, args))

  1097       | do_term (Abs (s, T, t')) args =

  1098         s_betapplys [] (Abs (s, T, do_term t' []), args)

  1099       | do_term t args = s_betapplys [] (t, args)

  1100   in do_term t [] end

  1102 (** Quantifier massaging: Distributing quantifiers **)

  1104 fun distribute_quantifiers t =

  1105   case t of

  1106     (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>

  1107     (case t1 of

  1108        (t10 as @{const "op &"}) $ t11 $ t12 =>

  1109        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))

  1110            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))

  1111      | (t10 as @{const Not}) $ t11 =>

  1112        t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)

  1113                                      $ Abs (s, T1, t11))

  1114      | t1 =>

  1115        if not (loose_bvar1 (t1, 0)) then

  1116          distribute_quantifiers (incr_boundvars ~1 t1)

  1117        else

  1118          t0 $ Abs (s, T1, distribute_quantifiers t1))

  1119   | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>

  1120     (case distribute_quantifiers t1 of

  1121        (t10 as @{const "op |"}) $ t11 $ t12 =>

  1122        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))

  1123            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))

  1124      | (t10 as @{const HOL.implies}) $ t11 $ t12 =>

  1125        t10 $ distribute_quantifiers (Const (@{const_name All}, T0)

  1126                                      $ Abs (s, T1, t11))

  1127            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))

  1128      | (t10 as @{const Not}) $ t11 =>

  1129        t10 $ distribute_quantifiers (Const (@{const_name All}, T0)

  1130                                      $ Abs (s, T1, t11))

  1131      | t1 =>

  1132        if not (loose_bvar1 (t1, 0)) then

  1133          distribute_quantifiers (incr_boundvars ~1 t1)

  1134        else

  1135          t0 $ Abs (s, T1, distribute_quantifiers t1))

  1136   | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2

  1137   | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')

  1138   | _ => t

  1140 (** Quantifier massaging: Pushing quantifiers inward **)

  1142 fun renumber_bounds j n f t =

  1143   case t of

  1144     t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2

  1145   | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')

  1146   | Bound j' =>

  1147     Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')

  1148   | _ => t

  1150 (* Maximum number of quantifiers in a cluster for which the exponential

  1151    algorithm is used. Larger clusters use a heuristic inspired by Claessen &

  1152    Soerensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003

  1153    paper). *)

  1154 val quantifier_cluster_threshold = 7

  1156 val push_quantifiers_inward =

  1157   let

  1158     fun aux quant_s ss Ts t =

  1159       (case t of

  1160          Const (s0, _) $ Abs (s1, T1, t1 as _ $ _) =>

  1161          if s0 = quant_s then

  1162            aux s0 (s1 :: ss) (T1 :: Ts) t1

  1163          else if quant_s = "" andalso

  1164                  (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then

  1165            aux s0 [s1] [T1] t1

  1166          else

  1167            raise SAME ()

  1168        | _ => raise SAME ())

  1169       handle SAME () =>

  1170              case t of

  1171                t1 $ t2 =>

  1172                if quant_s = "" then

  1173                  aux "" [] [] t1 $ aux "" [] [] t2

  1174                else

  1175                  let

  1176                    val typical_card = 4

  1177                    fun big_union proj ps =

  1178                      fold (fold (insert (op =)) o proj) ps []

  1179                    val (ts, connective) = strip_any_connective t

  1180                    val T_costs =

  1181                      map (bounded_card_of_type 65536 typical_card []) Ts

  1182                    val t_costs = map size_of_term ts

  1183                    val num_Ts = length Ts

  1184                    val flip = curry (op -) (num_Ts - 1)

  1185                    val t_boundss = map (map flip o loose_bnos) ts

  1186                    fun merge costly_boundss [] = costly_boundss

  1187                      | merge costly_boundss (j :: js) =

  1188                        let

  1189                          val (yeas, nays) =

  1190                            List.partition (fn (bounds, _) =>

  1191                                               member (op =) bounds j)

  1192                                           costly_boundss

  1193                          val yeas_bounds = big_union fst yeas

  1194                          val yeas_cost = Integer.sum (map snd yeas)

  1195                                          * nth T_costs j

  1196                        in merge ((yeas_bounds, yeas_cost) :: nays) js end

  1197                    val cost = Integer.sum o map snd oo merge

  1198                    fun heuristically_best_permutation _ [] = []

  1199                      | heuristically_best_permutation costly_boundss js =

  1200                        let

  1201                          val (costly_boundss, (j, js)) =

  1202                            js |> map (`(merge costly_boundss o single))

  1203                               |> sort (int_ord

  1204                                        o pairself (Integer.sum o map snd o fst))

  1205                               |> split_list |>> hd ||> pairf hd tl

  1206                        in

  1207                          j :: heuristically_best_permutation costly_boundss js

  1208                        end

  1209                    val js =

  1210                      if length Ts <= quantifier_cluster_threshold then

  1211                        all_permutations (index_seq 0 num_Ts)

  1212                        |> map (`(cost (t_boundss ~~ t_costs)))

  1213                        |> sort (int_ord o pairself fst) |> hd |> snd

  1214                      else

  1215                        heuristically_best_permutation (t_boundss ~~ t_costs)

  1216                                                       (index_seq 0 num_Ts)

  1217                    val back_js = map (fn j => find_index (curry (op =) j) js)

  1218                                      (index_seq 0 num_Ts)

  1219                    val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))

  1220                                 ts

  1221                    fun mk_connection [] =

  1222                        raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\

  1223                                   \mk_connection", "")

  1224                      | mk_connection ts_cum_bounds =

  1225                        ts_cum_bounds |> map fst

  1226                        |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)

  1227                    fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection

  1228                      | build ts_cum_bounds (j :: js) =

  1229                        let

  1230                          val (yeas, nays) =

  1231                            List.partition (fn (_, bounds) =>

  1232                                               member (op =) bounds j)

  1233                                           ts_cum_bounds

  1234                            ||> map (apfst (incr_boundvars ~1))

  1235                        in

  1236                          if null yeas then

  1237                            build nays js

  1238                          else

  1239                            let val T = nth Ts (flip j) in

  1240                              build ((Const (quant_s, (T --> bool_T) --> bool_T)

  1241                                      $ Abs (nth ss (flip j), T,

  1242                                             mk_connection yeas),

  1243                                       big_union snd yeas) :: nays) js

  1244                            end

  1245                        end

  1246                  in build (ts ~~ t_boundss) js end

  1247              | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')

  1248              | _ => t

  1249   in aux "" [] [] end

  1251 (** Inference of finite functions **)

  1253 fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos

  1254                                (nondef_ts, def_ts) =

  1255   if forall (curry (op =) (SOME false) o snd) finitizes then

  1256     (nondef_ts, def_ts)

  1257   else

  1258     let

  1259       val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)

  1260                |> filter_out (fn Type (@{type_name fun_box}, _) => true

  1261                                | @{typ signed_bit} => true

  1262                                | @{typ unsigned_bit} => true

  1263                                | T => is_small_finite_type hol_ctxt T orelse

  1264                                       triple_lookup (type_match thy) monos T

  1265                                       = SOME (SOME false))

  1266     in

  1267       fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts)

  1268     end

  1270 (** Preprocessor entry point **)

  1272 val max_skolem_depth = 3

  1274 fun preprocess_formulas

  1275         (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,

  1276                       ...}) finitizes monos assm_ts neg_t =

  1277   let

  1278     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =

  1279       neg_t |> unfold_defs_in_term hol_ctxt

  1280             |> close_form

  1281             |> skolemize_term_and_more hol_ctxt max_skolem_depth

  1282             |> specialize_consts_in_term hol_ctxt false 0

  1283             |> axioms_for_term hol_ctxt assm_ts

  1284     val binarize =

  1285       is_standard_datatype thy stds nat_T andalso

  1286       case binary_ints of

  1287         SOME false => false

  1288       | _ => forall (may_use_binary_ints false) nondef_ts andalso

  1289              forall (may_use_binary_ints true) def_ts andalso

  1290              (binary_ints = SOME true orelse

  1291               exists should_use_binary_ints (nondef_ts @ def_ts))

  1292     val box = exists (not_equal (SOME false) o snd) boxes

  1293     val table =

  1294       Termtab.empty

  1295       |> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts)

  1296     fun do_rest def =

  1297       binarize ? binarize_nat_and_int_in_term

  1298       #> box ? uncurry_term table

  1299       #> box ? box_fun_and_pair_in_term hol_ctxt def

  1300       #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def

  1301                             #> pull_out_existential_constrs hol_ctxt

  1302                             #> destroy_pulled_out_constrs hol_ctxt def)

  1303       #> curry_assms

  1304       #> destroy_universal_equalities

  1305       #> destroy_existential_equalities hol_ctxt

  1306       #> simplify_constrs_and_sels ctxt

  1307       #> distribute_quantifiers

  1308       #> push_quantifiers_inward

  1309       #> close_form

  1310       #> Term.map_abs_vars shortest_name

  1311     val nondef_ts = map (do_rest false) nondef_ts

  1312     val def_ts = map (do_rest true) def_ts

  1313     val (nondef_ts, def_ts) =

  1314       finitize_all_types_of_funs hol_ctxt binarize finitizes monos

  1315                                  (nondef_ts, def_ts)

  1316   in

  1317     (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)

  1318   end

  1320 end;

author	haftmann
	Thu, 26 Aug 2010 20:51:17 +0200
changeset 39019	e46e7a9cb622
parent 38464	a44d108a8d39
child 39028	848be46708dc
permissions	-rw-r--r--