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_term :

    12     hol_context -> term -> ((term list * term list) * (bool * bool)) * term

    13 end

    15 structure Nitpick_Preproc : NITPICK_PREPROC =

    16 struct

    18 open Nitpick_Util

    19 open Nitpick_HOL

    21 (* polarity -> string -> bool *)

    22 fun is_positive_existential polar quant_s =

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

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

    26 (** Binary coding of integers **)

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

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

    30    binary coding. *)

    31 val binary_int_threshold = 3

    33 (* term -> bool *)

    34 fun may_use_binary_ints (t1 $ t2) =

    35     may_use_binary_ints t1 andalso may_use_binary_ints t2

    36   | may_use_binary_ints (t as Const (s, _)) =

    37     t <> @{const Suc} andalso

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

    39                         @{const_name nat_gcd}, @{const_name nat_lcm},

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

    41   | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'

    42   | may_use_binary_ints _ = true

    43 fun should_use_binary_ints (t1 $ t2) =

    44     should_use_binary_ints t1 orelse should_use_binary_ints t2

    45   | should_use_binary_ints (Const (s, _)) =

    46     member (op =) [@{const_name times_nat_inst.times_nat},

    47                    @{const_name div_nat_inst.div_nat},

    48                    @{const_name times_int_inst.times_int},

    49                    @{const_name div_int_inst.div_int}] s orelse

    50     (String.isPrefix numeral_prefix s andalso

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

    52        n < ~ binary_int_threshold orelse n > binary_int_threshold

    53      end)

    54   | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'

    55   | should_use_binary_ints _ = false

    57 (* typ -> typ *)

    58 fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}

    59   | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}

    60   | binarize_nat_and_int_in_type (Type (s, Ts)) =

    61     Type (s, map binarize_nat_and_int_in_type Ts)

    62   | binarize_nat_and_int_in_type T = T

    63 (* term -> term *)

    64 val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type

    66 (** Uncurrying **)

    68 (* theory -> term -> int Termtab.tab -> int Termtab.tab *)

    69 fun add_to_uncurry_table thy t =

    70   let

    71     (* term -> term list -> int Termtab.tab -> int Termtab.tab *)

    72     fun aux (t1 $ t2) args table =

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

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

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

    76         if is_built_in_const true x orelse is_constr_like thy x orelse

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

    78           table

    79         else

    80           Termtab.map_default (t, 65536) (curry Int.min (length args)) table

    81       | aux _ _ table = table

    82   in aux t [] end

    84 (* int -> int -> string *)

    85 fun uncurry_prefix_for k j =

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

    88 (* int Termtab.tab term -> term *)

    89 fun uncurry_term table t =

    90   let

    91     (* term -> term list -> term *)

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

    93       | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)

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

    95         (case Termtab.lookup table t of

    96            SOME n =>

    97            if n >= 2 then

    98              let

    99                val (arg_Ts, rest_T) = strip_n_binders n T

   100                val j =

   101                  if hd arg_Ts = @{typ bisim_iterator} orelse

   102                     is_fp_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                  betapplys (t, args)

   115                else

   116                  betapplys (Const (uncurry_prefix_for (n - j) j ^ s,

   117                                    before_arg_Ts ---> tuple_T --> rest_T),

   118                             before_args @ [mk_flat_tuple tuple_T tuple_args] @

   119                             after_args)

   120              end

   121            else

   122              betapplys (t, args)

   123          | NONE => betapplys (t, args))

   124       | aux t args = betapplys (t, args)

   125   in aux t [] end

   127 (** Boxing **)

   129 (* hol_context -> typ -> term -> term *)

   130 fun constr_expand (hol_ctxt as {thy, ...}) T t =

   131   (case head_of t of

   132      Const x => if is_constr_like thy x then t else raise SAME ()

   133    | _ => raise SAME ())

   134   handle SAME () =>

   135          let

   136            val x' as (_, T') =

   137              if is_pair_type T then

   138                let val (T1, T2) = HOLogic.dest_prodT T in

   139                  (@{const_name Pair}, T1 --> T2 --> T)

   140                end

   141              else

   142                datatype_constrs hol_ctxt T |> hd

   143            val arg_Ts = binder_types T'

   144          in

   145            list_comb (Const x', map2 (select_nth_constr_arg thy x' t)

   146                                      (index_seq 0 (length arg_Ts)) arg_Ts)

   147          end

   149 (* hol_context -> bool -> term -> term *)

   150 fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t =

   151   let

   152     (* typ -> typ *)

   153     fun box_relational_operator_type (Type ("fun", Ts)) =

   154         Type ("fun", map box_relational_operator_type Ts)

   155       | box_relational_operator_type (Type ("*", Ts)) =

   156         Type ("*", map (box_type hol_ctxt InPair) Ts)

   157       | box_relational_operator_type T = T

   158     (* (term -> term) -> int -> term -> term *)

   159     fun coerce_bound_no f j t =

   160       case t of

   161         t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2

   162       | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')

   163       | Bound j' => if j' = j then f t else t

   164       | _ => t

   165     (* typ -> typ -> term -> term *)

   166     fun coerce_bound_0_in_term new_T old_T =

   167       old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0

   168     (* typ list -> typ -> term -> term *)

   169     and coerce_term Ts new_T old_T t =

   170       if old_T = new_T then

   171         t

   172       else

   173         case (new_T, old_T) of

   174           (Type (new_s, new_Ts as [new_T1, new_T2]),

   175            Type ("fun", [old_T1, old_T2])) =>

   176           (case eta_expand Ts t 1 of

   177              Abs (s, _, t') =>

   178              Abs (s, new_T1,

   179                   t' |> coerce_bound_0_in_term new_T1 old_T1

   180                      |> coerce_term (new_T1 :: Ts) new_T2 old_T2)

   181              |> Envir.eta_contract

   182              |> new_s <> "fun"

   183                 ? construct_value thy (@{const_name FunBox},

   184                                        Type ("fun", new_Ts) --> new_T) o single

   185            | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\

   186                                \coerce_term", [t']))

   187         | (Type (new_s, new_Ts as [new_T1, new_T2]),

   188            Type (old_s, old_Ts as [old_T1, old_T2])) =>

   189           if old_s = @{type_name fun_box} orelse

   190              old_s = @{type_name pair_box} orelse old_s = "*" then

   191             case constr_expand hol_ctxt old_T t of

   192               Const (@{const_name FunBox}, _) $ t1 =>

   193               if new_s = "fun" then

   194                 coerce_term Ts new_T (Type ("fun", old_Ts)) t1

   195               else

   196                 construct_value thy

   197                     (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)

   198                      [coerce_term Ts (Type ("fun", new_Ts))

   199                                   (Type ("fun", old_Ts)) t1]

   200             | Const _ $ t1 $ t2 =>

   201               construct_value thy

   202                   (if new_s = "*" then @{const_name Pair}

   203                    else @{const_name PairBox}, new_Ts ---> new_T)

   204                   [coerce_term Ts new_T1 old_T1 t1,

   205                    coerce_term Ts new_T2 old_T2 t2]

   206             | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\

   207                                 \coerce_term", [t'])

   208           else

   209             raise TYPE ("coerce_term", [new_T, old_T], [t])

   210         | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])

   211     (* indexname * typ -> typ * term -> typ option list -> typ option list *)

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

   213       case t' of

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

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

   216         (case T' of

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

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

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

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

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

   222     (* typ list -> typ list -> term -> indexname * typ -> typ *)

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

   224       case t of

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

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

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

   228           let

   229             val (t', args) = strip_comb t1

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

   231           in

   232             case fold (add_boxed_types_for_var z)

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

   234               [T''] => T''

   235             | _ => T

   236           end

   237         else

   238           T

   239       | _ => T

   240     (* typ list -> typ list -> polarity -> string -> typ -> string -> typ

   241        -> term -> term *)

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

   243       let

   244         val abs_T' =

   245           if polar = Neut orelse is_positive_existential polar quant_s then

   246             box_type hol_ctxt InFunLHS abs_T

   247           else

   248             abs_T

   249         val body_T = body_type quant_T

   250       in

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

   252         $ Abs (abs_s, abs_T',

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

   254       end

   255     (* typ list -> typ list -> string -> typ -> term -> term -> term *)

   256     and do_equals new_Ts old_Ts s0 T0 t1 t2 =

   257       let

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

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

   260         val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last

   261       in

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

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

   264       end

   265     (* string -> typ -> term *)

   266     and do_description_operator s T =

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

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

   269       end

   270     (* typ list -> typ list -> polarity -> term -> term *)

   271     and do_term new_Ts old_Ts polar t =

   272       case t of

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

   274         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1

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

   276         do_equals new_Ts old_Ts s0 T0 t1 t2

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

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

   279         $ do_term new_Ts old_Ts polar t2

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

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

   282         $ do_term new_Ts old_Ts polar t2

   283       | @{const Trueprop} $ t1 =>

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

   285       | @{const Not} $ t1 =>

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

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

   288         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1

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

   290         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1

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

   292         do_equals new_Ts old_Ts s0 T0 t1 t2

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

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

   295         $ do_term new_Ts old_Ts polar t2

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

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

   298         $ do_term new_Ts old_Ts polar t2

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

   300         @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1

   301         $ do_term new_Ts old_Ts polar t2

   302       | Const (s as @{const_name The}, T) => do_description_operator s T

   303       | Const (s as @{const_name Eps}, T) => do_description_operator s T

   304       | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>

   305         let val T' = box_type hol_ctxt InSel T2 in

   306           Const (@{const_name quot_normal}, T' --> T')

   307         end

   308       | Const (s as @{const_name Tha}, T) => do_description_operator s T

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

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

   311                      s = @{const_name trancl} then

   312                     box_relational_operator_type T

   313                   else if is_built_in_const fast_descrs x orelse

   314                           s = @{const_name Sigma} then

   315                     T

   316                   else if is_constr_like thy x then

   317                     box_type hol_ctxt InConstr T

   318                   else if is_sel s

   319                        orelse is_rep_fun thy x then

   320                     box_type hol_ctxt InSel T

   321                   else

   322                     box_type hol_ctxt InExpr T)

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

   324         let

   325           val t1 = do_term new_Ts old_Ts Neut t1

   326           val T1 = fastype_of1 (new_Ts, t1)

   327           val (s1, Ts1) = dest_Type T1

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

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

   330           val T2 = fastype_of1 (new_Ts, t2)

   331           val t2 = coerce_term new_Ts (hd Ts1) T2 t2

   332         in

   333           betapply (if s1 = "fun" then

   334                       t1

   335                     else

   336                       select_nth_constr_arg thy

   337                           (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0

   338                           (Type ("fun", Ts1)), t2)

   339         end

   340       | t1 $ t2 =>

   341         let

   342           val t1 = do_term new_Ts old_Ts Neut t1

   343           val T1 = fastype_of1 (new_Ts, t1)

   344           val (s1, Ts1) = dest_Type T1

   345           val t2 = do_term new_Ts old_Ts Neut t2

   346           val T2 = fastype_of1 (new_Ts, t2)

   347           val t2 = coerce_term new_Ts (hd Ts1) T2 t2

   348         in

   349           betapply (if s1 = "fun" then

   350                       t1

   351                     else

   352                       select_nth_constr_arg thy

   353                           (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0

   354                           (Type ("fun", Ts1)), t2)

   355         end

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

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

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

   359                 else box_type hol_ctxt InExpr T)

   360       | Bound _ => t

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

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

   363   in do_term [] [] Pos orig_t end

   365 (** Destruction of constructors **)

   367 val val_var_prefix = nitpick_prefix ^ "v"

   369 (* typ list -> int -> int -> int -> term -> term *)

   370 fun fresh_value_var Ts k n j t =

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

   373 (* typ list -> int -> term -> bool *)

   374 fun has_heavy_bounds_or_vars Ts level t =

   375   let

   376     (* typ list -> bool *)

   377     fun aux [] = false

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

   379       | aux _ = true

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

   382 (* theory -> typ list -> bool -> int -> int -> term -> term list -> term list

   383    -> term * term list *)

   384 fun pull_out_constr_comb thy Ts relax k level t args seen =

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

   386     case t of

   387       Const x =>

   388       if not relax andalso is_constr thy x andalso

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

   390          has_heavy_bounds_or_vars Ts level t_comb andalso

   391          not (loose_bvar (t_comb, level)) then

   392         let

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

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

   395                           | j => (j, seen)

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

   397       else

   398         (t_comb, seen)

   399     | _ => (t_comb, seen)

   400   end

   402 (* (term -> term) -> typ list -> int -> term list -> term list *)

   403 fun equations_for_pulled_out_constrs mk_eq Ts k seen =

   404   let val n = length seen in

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

   406          (index_seq 0 n) seen

   407   end

   409 (* theory -> bool -> term -> term *)

   410 fun pull_out_universal_constrs thy def t =

   411   let

   412     val k = maxidx_of_term t + 1

   413     (* typ list -> bool -> term -> term list -> term list -> term * term list *)

   414     fun do_term Ts def t args seen =

   415       case t of

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

   417         do_eq_or_imp Ts true def t0 t1 t2 seen

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

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

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

   421         do_eq_or_imp Ts true def t0 t1 t2 seen

   422       | (t0 as @{const "op -->"}) $ t1 $ t2 =>

   423         do_eq_or_imp Ts false def t0 t1 t2 seen

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

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

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

   427         end

   428       | t1 $ t2 =>

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

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

   431         end

   432       | _ => pull_out_constr_comb thy Ts def k 0 t args seen

   433     (* typ list -> bool -> bool -> term -> term -> term -> term list

   434        -> term * term list *)

   435     and do_eq_or_imp Ts eq def t0 t1 t2 seen =

   436       let

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

   438                          else do_term Ts false t2 [] seen

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

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

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

   442   in

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

   444                                                          seen, concl)

   445   end

   447 (* term -> term -> term *)

   448 fun mk_exists v t =

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

   451 (* theory -> term -> term *)

   452 fun pull_out_existential_constrs thy t =

   453   let

   454     val k = maxidx_of_term t + 1

   455     (* typ list -> int -> term -> term list -> term list -> term * term list *)

   456     fun aux Ts num_exists t args seen =

   457       case t of

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

   459         let

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

   461           val n = length seen'

   462           (* unit -> term list *)

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

   464         in

   465           (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'

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

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

   468         end

   469       | t1 $ t2 =>

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

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

   472         end

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

   474         let

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

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

   477       | _ =>

   478         if num_exists > 0 then

   479           pull_out_constr_comb thy Ts false k num_exists t args seen

   480         else

   481           (list_comb (t, args), seen)

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

   484 (* hol_context -> bool -> term -> term *)

   485 fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t =

   486   let

   487     (* styp -> int *)

   488     val num_occs_of_var =

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

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

   491     (* bool -> term -> term *)

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

   493         aux_eq careful true t0 t1 t2

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

   495         t0 $ aux false t1 $ aux careful t2

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

   497         aux_eq careful true t0 t1 t2

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

   499         t0 $ aux false t1 $ aux careful t2

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

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

   502       | aux _ t = t

   503     (* bool -> bool -> term -> term -> term -> term *)

   504     and aux_eq careful pass1 t0 t1 t2 =

   505       ((if careful then

   506           raise SAME ()

   507         else if axiom andalso is_Var t2 andalso

   508                 num_occs_of_var (dest_Var t2) = 1 then

   509           @{const True}

   510         else case strip_comb t2 of

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

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

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

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

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

   516           else raise SAME ()

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

   518           let val arg_Ts = binder_types T in

   519             if length arg_Ts = length args andalso

   520                (is_constr thy x orelse s = @{const_name Pair} orelse

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

   522                (not careful orelse not (is_Var t1) orelse

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

   524               discriminate_value hol_ctxt x t1 ::

   525               map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args

   526               |> foldr1 s_conj

   527             else

   528               raise SAME ()

   529           end

   530         | _ => raise SAME ())

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

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

   533                         else t0 $ aux false t2 $ aux false t1

   534     (* styp -> term -> int -> typ -> term -> term *)

   535     and sel_eq x t n nth_T nth_t =

   536       HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T

   537       |> aux false

   538   in aux axiom t end

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

   542 (* term -> term *)

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

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

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

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

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

   548   | curry_assms t = t

   550 (* term -> term *)

   551 val destroy_universal_equalities =

   552   let

   553     (* term list -> (indexname * typ) list -> term -> term *)

   554     fun aux prems zs t =

   555       case t of

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

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

   558     (* term list -> (indexname * typ) list -> term -> term -> term *)

   559     and aux_implies prems zs t1 t2 =

   560       case t1 of

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

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

   563         aux_eq prems zs z t' t1 t2

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

   565         aux_eq prems zs z t' t1 t2

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

   567     (* term list -> (indexname * typ) list -> indexname * typ -> term -> term

   568        -> term -> term *)

   569     and aux_eq prems zs z t' t1 t2 =

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

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

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

   573       else

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

   575   in aux [] [] end

   577 (* theory -> int -> term list -> term list -> (term * term list) option *)

   578 fun find_bound_assign _ _ _ [] = NONE

   579   | find_bound_assign thy j seen (t :: ts) =

   580     let

   581       (* bool -> term -> term -> (term * term list) option *)

   582       fun aux pass1 t1 t2 =

   583         (if loose_bvar1 (t2, j) then

   584            if pass1 then aux false t2 t1 else raise SAME ()

   585          else case t1 of

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

   587          | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>

   588            if j' = j andalso

   589               s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then

   590              SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],

   591                    ts @ seen)

   592            else

   593              raise SAME ()

   594          | _ => raise SAME ())

   595         handle SAME () => find_bound_assign thy j (t :: seen) ts

   596     in

   597       case t of

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

   599       | _ => find_bound_assign thy j (t :: seen) ts

   600     end

   602 (* int -> term -> term -> term *)

   603 fun subst_one_bound j arg t =

   604   let

   605     fun aux (Bound i, lev) =

   606         if i < lev then raise SAME ()

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

   608         else Bound (i - 1)

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

   610       | aux (f $ t, lev) =

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

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

   613       | aux _ = raise SAME ()

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

   616 (* theory -> term -> term *)

   617 fun destroy_existential_equalities thy =

   618   let

   619     (* string list -> typ list -> term list -> term *)

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

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

   622         (case find_bound_assign thy (length ss) [] ts of

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

   624          | SOME (arg_t, ts) =>

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

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

   627          | NONE =>

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

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

   630       | kill _ _ _ = raise UnequalLengths

   631     (* string list -> typ list -> term -> term *)

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

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

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

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

   636       | gather [] [] t = t

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

   638   in gather [] [] end

   640 (** Skolemization **)

   642 (* int -> int -> string *)

   643 fun skolem_prefix_for k j =

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

   646 (* hol_context -> int -> term -> term *)

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

   648                             skolem_depth =

   649   let

   650     (* int list -> int list *)

   651     val incrs = map (Integer.add 1)

   652     (* string list -> typ list -> int list -> int -> polarity -> term -> term *)

   653     fun aux ss Ts js depth polar t =

   654       let

   655         (* string -> typ -> string -> typ -> term -> term *)

   656         fun do_quantifier quant_s quant_T abs_s abs_T t =

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

   658             aux ss Ts js depth polar (incr_boundvars ~1 t)

   659           else if depth <= skolem_depth andalso

   660                   is_positive_existential polar quant_s then

   661             let

   662               val j = length (!skolems) + 1

   663               val sko_s = skolem_prefix_for (length js) j ^ abs_s

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

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

   666                                      map Bound (rev js))

   667               val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)

   668             in

   669               if null js then betapply (abs_t, sko_t)

   670               else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t

   671             end

   672           else

   673             Const (quant_s, quant_T)

   674             $ Abs (abs_s, abs_T,

   675                    if is_higher_order_type abs_T then

   676                      t

   677                    else

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

   679                          (depth + 1) polar t)

   680       in

   681         case t of

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

   683           do_quantifier s0 T0 s1 T1 t1

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

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

   686           $ aux ss Ts js depth polar t2

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

   688           @{const Pure.conjunction} $ aux ss Ts js depth polar t1

   689           $ aux ss Ts js depth polar t2

   690         | @{const Trueprop} $ t1 =>

   691           @{const Trueprop} $ aux ss Ts js depth polar t1

   692         | @{const Not} $ t1 =>

   693           @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1

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

   695           do_quantifier s0 T0 s1 T1 t1

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

   697           do_quantifier s0 T0 s1 T1 t1

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

   699           @{const "op &"} $ aux ss Ts js depth polar t1

   700           $ aux ss Ts js depth polar t2

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

   702           @{const "op |"} $ aux ss Ts js depth polar t1

   703           $ aux ss Ts js depth polar t2

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

   705           @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1

   706           $ aux ss Ts js depth polar t2

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

   708           t0 $ t1 $ aux ss Ts js depth polar t2

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

   710           if is_inductive_pred hol_ctxt x andalso

   711              not (is_well_founded_inductive_pred hol_ctxt x) then

   712             let

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

   714               val (pref, connective, set_oper) =

   715                 if gfp then

   716                   (lbfp_prefix,

   717                    @{const "op |"},

   718                    @{const_name upper_semilattice_fun_inst.sup_fun})

   719                 else

   720                   (ubfp_prefix,

   721                    @{const "op &"},

   722                    @{const_name lower_semilattice_fun_inst.inf_fun})

   723               (* unit -> term *)

   724               fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x

   725                            |> aux ss Ts js depth polar

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

   727             in

   728               (case polar |> gfp ? flip_polarity of

   729                  Pos => pos ()

   730                | Neg => neg ()

   731                | Neut =>

   732                  if is_fun_type T then

   733                    let

   734                      val ((trunk_arg_Ts, rump_arg_T), body_T) =

   735                        T |> strip_type |>> split_last

   736                      val set_T = rump_arg_T --> body_T

   737                      (* (unit -> term) -> term *)

   738                      fun app f =

   739                        list_comb (f (),

   740                                   map Bound (length trunk_arg_Ts - 1 downto 0))

   741                    in

   742                      List.foldr absdummy

   743                                 (Const (set_oper, set_T --> set_T --> set_T)

   744                                         $ app pos $ app neg) trunk_arg_Ts

   745                    end

   746                  else

   747                    connective $ pos () $ neg ())

   748             end

   749           else

   750             Const x

   751         | t1 $ t2 =>

   752           betapply (aux ss Ts [] (skolem_depth + 1) polar t1,

   753                     aux ss Ts [] depth Neut t2)

   754         | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)

   755         | _ => t

   756       end

   757   in aux [] [] [] 0 Pos end

   759 (** Function specialization **)

   761 (* term -> term list *)

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

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

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

   765     snd (strip_comb t1)

   766   | params_in_equation _ = []

   768 (* styp -> styp -> int list -> term list -> term list -> term -> term *)

   769 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =

   770   let

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

   772             + 1

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

   774     val fixed_params = filter_indices fixed_js (params_in_equation t)

   775     (* term list -> term -> term *)

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

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

   778       | aux args t =

   779         if t = Const x then

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

   781         else

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

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

   784           end

   785   in aux [] t end

   787 (* hol_context -> styp -> (int * term option) list *)

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

   789   let

   790     (* term -> term list -> term list -> term list list *)

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

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

   793       | fun_calls t args =

   794         (case t of

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

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

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

   798                           | NONE => false)

   799          | _ => false) ? cons args

   800     (* term list list -> term list list -> term list -> term list list *)

   801     fun call_sets [] [] vs = [vs]

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

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

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

   805         OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)

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

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

   808   in

   809     fold_rev (fn (set, j) =>

   810                  case set of

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

   812                               ? cons (j, NONE)

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

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

   815                  | _ => I) indexed_sets []

   816   end

   817 (* hol_context -> styp -> term list -> (int * term option) list *)

   818 fun static_args_in_terms hol_ctxt x =

   819   map (static_args_in_term hol_ctxt x)

   820   #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))

   822 (* (int * term option) list -> (int * term) list -> int list *)

   823 fun overlapping_indices [] _ = []

   824   | overlapping_indices _ [] = []

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

   826     if j1 < j2 then overlapping_indices ps1' ps2

   827     else if j1 > j2 then overlapping_indices ps1 ps2'

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

   830 (* typ list -> term -> bool *)

   831 fun is_eligible_arg Ts t =

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

   833     null bad_Ts orelse

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

   835      forall (not o is_higher_order_type) bad_Ts)

   836   end

   838 (* int -> string *)

   839 fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep

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

   842    prevent excessive specialization by not specializing it. *)

   843 val special_max_depth = 20

   845 val bound_var_prefix = "b"

   847 (* hol_context -> int -> term -> term *)

   848 fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table,

   849                                             special_funs, ...}) depth t =

   850   if not specialize orelse depth > special_max_depth then

   851     t

   852   else

   853     let

   854       val blacklist = if depth = 0 then []

   855                       else case term_under_def t of Const x => [x] | _ => []

   856       (* term list -> typ list -> term -> term *)

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

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

   859                not (String.isPrefix special_prefix s) andalso

   860                is_equational_fun hol_ctxt x then

   861               let

   862                 val eligible_args = filter (is_eligible_arg Ts o snd)

   863                                            (index_seq 0 (length args) ~~ args)

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

   865                 val old_axs = equational_fun_axioms hol_ctxt x

   866                               |> map (destroy_existential_equalities thy)

   867                 val static_params = static_args_in_terms hol_ctxt x old_axs

   868                 val fixed_js = overlapping_indices static_params eligible_args

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

   870                 val fixed_args = filter_indices fixed_js args

   871                 val vars = fold Term.add_vars fixed_args []

   872                            |> sort (TermOrd.fast_indexname_ord o pairself fst)

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

   874                                     fixed_args []

   875                                |> sort int_ord

   876                 val live_args = filter_out_indices fixed_js args

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

   878                 val extra_Ts = map snd vars @ filter_indices bound_js Ts

   879                 val k = maxidx_of_term t + 1

   880                 (* int -> term *)

   881                 fun var_for_bound_no j =

   882                   Var ((bound_var_prefix ^

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

   884                                        + 1), k),

   885                        nth Ts j)

   886                 val fixed_args_in_axiom =

   887                   map (curry subst_bounds

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

   889                       fixed_args

   890               in

   891                 case AList.lookup (op =) (!special_funs)

   892                                   (x, fixed_js, fixed_args_in_axiom) of

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

   894                 | NONE =>

   895                   let

   896                     val extra_args_in_axiom =

   897                       map Var vars @ map var_for_bound_no bound_js

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

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

   900                        extra_Ts @ filter_out_indices fixed_js (binder_types T)

   901                        ---> body_type T)

   902                     val new_axs =

   903                       map (specialize_fun_axiom x x' fixed_js

   904                                fixed_args_in_axiom extra_args_in_axiom) old_axs

   905                     val _ =

   906                       Unsynchronized.change special_funs

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

   908                     val _ = add_simps simp_table s' new_axs

   909                   in list_comb (Const x', extra_args) end

   910               end

   911             else

   912               raise SAME ())

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

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

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

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

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

   918     in aux [] [] t end

   920 type special_triple = int list * term list * styp

   922 val cong_var_prefix = "c"

   924 (* styp -> special_triple -> special_triple -> term *)

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

   926   let

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

   928     val Ts = binder_types T

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

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

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

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

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

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

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

   936                     | (NONE, NONE) =>

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

   938                                        nth Ts j) in

   939                         apsnd (pairself (cons v))

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

   941   in

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

   943                             |> map Logic.mk_equals,

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

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

   946     |> close_form (* TODO: needed? *)

   947   end

   949 (* hol_context -> styp list -> term list *)

   950 fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =

   951   let

   952     val groups =

   953       !special_funs

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

   955       |> AList.group (op =)

   956       |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)

   957       |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))

   958     (* special_triple -> int *)

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

   960     (* special_triple -> special_triple -> bool *)

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

   962       x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)

   963                                       (j2 ~~ t2, j1 ~~ t1)

   964     (* styp -> special_triple list -> special_triple list -> special_triple list

   965        -> term list -> term list *)

   966     fun do_pass_1 _ [] [_] [_] = I

   967       | do_pass_1 x skipped _ [] = do_pass_2 x skipped

   968       | do_pass_1 x skipped all (z :: zs) =

   969         case filter (is_more_specific z) all

   970              |> sort (int_ord o pairself generality) of

   971           [] => do_pass_1 x (z :: skipped) all zs

   972         | (z' :: _) => cons (special_congruence_axiom x z z')

   973                        #> do_pass_1 x skipped all zs

   974     (* styp -> special_triple list -> term list -> term list *)

   975     and do_pass_2 _ [] = I

   976       | do_pass_2 x (z :: zs) =

   977         fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs

   978   in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end

   980 (** Axiom selection **)

   982 (* Similar to "Refute.specialize_type" but returns all matches rather than only

   983    the first (preorder) match. *)

   984 (* theory -> styp -> term -> term list *)

   985 fun multi_specialize_type thy slack (x as (s, T)) t =

   986   let

   987     (* term -> (typ * term) list -> (typ * term) list *)

   988     fun aux (Const (s', T')) ys =

   989         if s = s' then

   990           ys |> (if AList.defined (op =) ys T' then

   991                    I

   992                  else

   993                   cons (T', Refute.monomorphic_term

   994                                 (Sign.typ_match thy (T', T) Vartab.empty) t)

   995                   handle Type.TYPE_MATCH => I

   996                        | Refute.REFUTE _ =>

   997                          if slack then

   998                            I

   999                          else

  1000                            raise NOT_SUPPORTED ("too much polymorphism in \

  1001                                                 \axiom involving " ^ quote s))

  1002         else

  1003           ys

  1004       | aux _ ys = ys

  1005   in map snd (fold_aterms aux t []) end

  1007 (* theory -> bool -> const_table -> styp -> term list *)

  1008 fun nondef_props_for_const thy slack table (x as (s, _)) =

  1009   these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)

  1011 (* 'a Symtab.table -> 'a list *)

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

  1013 (* const_table -> string -> const_table *)

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

  1016 (* int -> term -> term *)

  1017 fun eval_axiom_for_term j t =

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

  1020 (* term -> bool *)

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

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

  1024 val axioms_max_depth = 255

  1026 (* hol_context -> term -> (term list * term list) * (bool * bool) *)

  1027 fun axioms_for_term

  1028         (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,

  1029                       def_table, nondef_table, user_nondefs, ...}) t =

  1030   let

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

  1032     (* (term list * term list -> term list)

  1033        -> ((term list -> term list) -> term list * term list

  1034            -> term list * term list)

  1035        -> int -> term -> accumulator -> accumulator *)

  1036     fun add_axiom get app depth t (accum as (xs, axs)) =

  1037       let

  1038         val t = t |> unfold_defs_in_term hol_ctxt

  1039                   |> skolemize_term_and_more hol_ctxt ~1

  1040       in

  1041         if is_trivial_equation t then

  1042           accum

  1043         else

  1044           let val t' = t |> specialize_consts_in_term hol_ctxt depth in

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

  1046             else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)

  1047           end

  1048       end

  1049     (* int -> term -> accumulator -> accumulator *)

  1050     and add_def_axiom depth = add_axiom fst apfst depth

  1051     and add_nondef_axiom depth = add_axiom snd apsnd depth

  1052     and add_maybe_def_axiom depth t =

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

  1054        else add_nondef_axiom) depth t

  1055     and add_eq_axiom depth t =

  1056       (if is_constr_pattern_formula thy t then add_def_axiom

  1057        else add_nondef_axiom) depth t

  1058     (* int -> term -> accumulator -> accumulator *)

  1059     and add_axioms_for_term depth t (accum as (xs, axs)) =

  1060       case t of

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

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

  1063         (if member (op =) xs x orelse is_built_in_const fast_descrs x then

  1064            accum

  1065          else

  1066            let val accum as (xs, _) = (x :: xs, axs) in

  1067              if depth > axioms_max_depth then

  1068                raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\

  1069                                 \add_axioms_for_term",

  1070                                 "too many nested axioms (" ^

  1071                                 string_of_int depth ^ ")")

  1072              else if Refute.is_const_of_class thy x then

  1073                let

  1074                  val class = Logic.class_of_const s

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

  1076                                                    class)

  1077                  val ax1 = try (Refute.specialize_type thy x) of_class

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

  1079                                       (Refute.get_classdef thy class)

  1080                in

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

  1082                       accum

  1083                end

  1084              else if is_constr thy x then

  1085                accum

  1086              else if is_equational_fun hol_ctxt x then

  1087                fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)

  1088                     accum

  1089              else if is_abs_fun thy x then

  1090                if is_quot_type thy (range_type T) then

  1091                  raise NOT_SUPPORTED "\"Abs_\" function of quotient type"

  1092                else

  1093                  accum |> fold (add_nondef_axiom depth)

  1094                                (nondef_props_for_const thy false nondef_table x)

  1095                        |> is_funky_typedef thy (range_type T)

  1096                           ? fold (add_maybe_def_axiom depth)

  1097                                  (nondef_props_for_const thy true

  1098                                                     (extra_table def_table s) x)

  1099              else if is_rep_fun thy x then

  1100                if is_quot_type thy (domain_type T) then

  1101                  raise NOT_SUPPORTED "\"Rep_\" function of quotient type"

  1102                else

  1103                  accum |> fold (add_nondef_axiom depth)

  1104                                (nondef_props_for_const thy false nondef_table x)

  1105                        |> is_funky_typedef thy (range_type T)

  1106                           ? fold (add_maybe_def_axiom depth)

  1107                                  (nondef_props_for_const thy true

  1108                                                     (extra_table def_table s) x)

  1109                        |> add_axioms_for_term depth

  1110                                               (Const (mate_of_rep_fun thy x))

  1111                        |> fold (add_def_axiom depth)

  1112                                (inverse_axioms_for_rep_fun thy x)

  1113              else

  1114                accum |> user_axioms <> SOME false

  1115                         ? fold (add_nondef_axiom depth)

  1116                                (nondef_props_for_const thy false nondef_table x)

  1117            end)

  1118         |> add_axioms_for_type depth T

  1119       | Free (_, T) => add_axioms_for_type depth T accum

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

  1121       | Bound _ => accum

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

  1123                                |> add_axioms_for_type depth T

  1124     (* int -> typ -> accumulator -> accumulator *)

  1125     and add_axioms_for_type depth T =

  1126       case T of

  1127         Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts

  1128       | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts

  1129       | @{typ prop} => I

  1130       | @{typ bool} => I

  1131       | @{typ unit} => I

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

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

  1134       | Type (z as (s, Ts)) =>

  1135         fold (add_axioms_for_type depth) Ts

  1136         #> (if is_pure_typedef thy T then

  1137               fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)

  1138             else if is_quot_type thy T then

  1139               fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)

  1140             else if max_bisim_depth >= 0 andalso is_codatatype thy T then

  1141               fold (add_maybe_def_axiom depth)

  1142                    (codatatype_bisim_axioms hol_ctxt T)

  1143             else

  1144               I)

  1145     (* int -> typ -> sort -> accumulator -> accumulator *)

  1146     and add_axioms_for_sort depth T S =

  1147       let

  1148         val supers = Sign.complete_sort thy S

  1149         val class_axioms =

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

  1151                                          handle ERROR _ => [])) supers

  1152         val monomorphic_class_axioms =

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

  1154                          [] => t

  1155                        | [(x, S)] =>

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

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

  1158                                           \add_axioms_for_sort", [t]))

  1159               class_axioms

  1160       in fold (add_nondef_axiom depth) monomorphic_class_axioms end

  1161     val (mono_user_nondefs, poly_user_nondefs) =

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

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

  1164                            evals

  1165     val (xs, (defs, nondefs)) =

  1166       ([], ([], [])) |> add_axioms_for_term 1 t

  1167                      |> fold_rev (add_def_axiom 1) eval_axioms

  1168                      |> user_axioms = SOME true

  1169                         ? fold (add_nondef_axiom 1) mono_user_nondefs

  1170     val defs = defs @ special_congruence_axioms hol_ctxt xs

  1171   in

  1172     ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,

  1173                        null poly_user_nondefs))

  1174   end

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

  1178 (* theory -> term -> term *)

  1179 fun simplify_constrs_and_sels thy t =

  1180   let

  1181     (* term -> int -> term *)

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

  1183         (t = t' andalso is_sel_like_and_no_discr s andalso

  1184          sel_no_from_name s = n)

  1185       | is_nth_sel_on _ _ _ = false

  1186     (* term -> term list -> term *)

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

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

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

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

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

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

  1193         ((if is_constr_like thy x then

  1194             if length args = num_binder_types T then

  1195               case hd args of

  1196                 Const (x' as (_, T')) $ t' =>

  1197                 if domain_type T' = body_type T andalso

  1198                    forall (uncurry (is_nth_sel_on t'))

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

  1200                   t'

  1201                 else

  1202                   raise SAME ()

  1203               | _ => raise SAME ()

  1204             else

  1205               raise SAME ()

  1206           else if is_sel_like_and_no_discr s then

  1207             case strip_comb (hd args) of

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

  1209               if is_constr_like thy x' andalso

  1210                  constr_name_for_sel_like s = s' andalso

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

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

  1213               else

  1214                 raise SAME ()

  1215             | _ => raise SAME ()

  1216           else

  1217             raise SAME ())

  1218          handle SAME () => betapplys (t, args))

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

  1220         betapplys (Abs (s, T, do_term t' []), args)

  1221       | do_term t args = betapplys (t, args)

  1222   in do_term t [] end

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

  1226 (* term -> term *)

  1227 fun distribute_quantifiers t =

  1228   case t of

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

  1230     (case t1 of

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

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

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

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

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

  1236                                      $ Abs (s, T1, t11))

  1237      | t1 =>

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

  1239          distribute_quantifiers (incr_boundvars ~1 t1)

  1240        else

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

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

  1243     (case distribute_quantifiers t1 of

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

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

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

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

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

  1249                                      $ Abs (s, T1, t11))

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

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

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

  1253                                      $ Abs (s, T1, t11))

  1254      | t1 =>

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

  1256          distribute_quantifiers (incr_boundvars ~1 t1)

  1257        else

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

  1259   | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2

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

  1261   | _ => t

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

  1265 (* int -> int -> (int -> int) -> term -> term *)

  1266 fun renumber_bounds j n f t =

  1267   case t of

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

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

  1270   | Bound j' =>

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

  1272   | _ => t

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

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

  1276    Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003

  1277    paper). *)

  1278 val quantifier_cluster_threshold = 7

  1280 (* theory -> term -> term *)

  1281 fun push_quantifiers_inward thy =

  1282   let

  1283     (* string -> string list -> typ list -> term -> term *)

  1284     fun aux quant_s ss Ts t =

  1285       (case t of

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

  1287          if s0 = quant_s then

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

  1289          else if quant_s = "" andalso

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

  1291            aux s0 [s1] [T1] t1

  1292          else

  1293            raise SAME ()

  1294        | _ => raise SAME ())

  1295       handle SAME () =>

  1296              case t of

  1297                t1 $ t2 =>

  1298                if quant_s = "" then

  1299                  aux "" [] [] t1 $ aux "" [] [] t2

  1300                else

  1301                  let

  1302                    val typical_card = 4

  1303                    (* ('a -> ''b list) -> 'a list -> ''b list *)

  1304                    fun big_union proj ps =

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

  1306                    val (ts, connective) = strip_any_connective t

  1307                    val T_costs =

  1308                      map (bounded_card_of_type 65536 typical_card []) Ts

  1309                    val t_costs = map size_of_term ts

  1310                    val num_Ts = length Ts

  1311                    (* int -> int *)

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

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

  1314                    (* (int list * int) list -> int list

  1315                       -> (int list * int) list *)

  1316                    fun merge costly_boundss [] = costly_boundss

  1317                      | merge costly_boundss (j :: js) =

  1318                        let

  1319                          val (yeas, nays) =

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

  1321                                               member (op =) bounds j)

  1322                                           costly_boundss

  1323                          val yeas_bounds = big_union fst yeas

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

  1325                                          * nth T_costs j

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

  1327                    (* (int list * int) list -> int list -> int *)

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

  1329                    (* (int list * int) list -> int list -> int list *)

  1330                    fun heuristically_best_permutation _ [] = []

  1331                      | heuristically_best_permutation costly_boundss js =

  1332                        let

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

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

  1335                               |> sort (int_ord

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

  1337                               |> split_list |>> hd ||> pairf hd tl

  1338                        in

  1339                          j :: heuristically_best_permutation costly_boundss js

  1340                        end

  1341                    val js =

  1342                      if length Ts <= quantifier_cluster_threshold then

  1343                        all_permutations (index_seq 0 num_Ts)

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

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

  1346                      else

  1347                        heuristically_best_permutation (t_boundss ~~ t_costs)

  1348                                                       (index_seq 0 num_Ts)

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

  1350                                      (index_seq 0 num_Ts)

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

  1352                                 ts

  1353                    (* (term * int list) list -> term *)

  1354                    fun mk_connection [] =

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

  1356                                   \mk_connection", "")

  1357                      | mk_connection ts_cum_bounds =

  1358                        ts_cum_bounds |> map fst

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

  1360                    (* (term * int list) list -> int list -> term *)

  1361                    fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection

  1362                      | build ts_cum_bounds (j :: js) =

  1363                        let

  1364                          val (yeas, nays) =

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

  1366                                               member (op =) bounds j)

  1367                                           ts_cum_bounds

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

  1369                        in

  1370                          if null yeas then

  1371                            build nays js

  1372                          else

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

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

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

  1376                                             mk_connection yeas),

  1377                                       big_union snd yeas) :: nays) js

  1378                            end

  1379                        end

  1380                  in build (ts ~~ t_boundss) js end

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

  1382              | _ => t

  1383   in aux "" [] [] end

  1385 (** Preprocessor entry point **)

  1387 (* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)

  1388 fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,

  1389                                   skolemize, uncurry, ...}) t =

  1390   let

  1391     val skolem_depth = if skolemize then 4 else ~1

  1392     val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),

  1393          core_t) = t |> unfold_defs_in_term hol_ctxt

  1394                      |> close_form

  1395                      |> skolemize_term_and_more hol_ctxt skolem_depth

  1396                      |> specialize_consts_in_term hol_ctxt 0

  1397                      |> `(axioms_for_term hol_ctxt)

  1398     val binarize =

  1399       case binary_ints of

  1400         SOME false => false

  1401       | _ =>

  1402         forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso

  1403         (binary_ints = SOME true orelse

  1404          exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))

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

  1406     val table =

  1407       Termtab.empty |> uncurry

  1408         ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)

  1409     (* bool -> bool -> term -> term *)

  1410     fun do_rest def core =

  1411       binarize ? binarize_nat_and_int_in_term

  1412       #> uncurry ? uncurry_term table

  1413       #> box ? box_fun_and_pair_in_term hol_ctxt def

  1414       #> destroy_constrs ? (pull_out_universal_constrs thy def

  1415                             #> pull_out_existential_constrs thy

  1416                             #> destroy_pulled_out_constrs hol_ctxt def)

  1417       #> curry_assms

  1418       #> destroy_universal_equalities

  1419       #> destroy_existential_equalities thy

  1420       #> simplify_constrs_and_sels thy

  1421       #> distribute_quantifiers

  1422       #> push_quantifiers_inward thy

  1423       #> close_form

  1424       #> Term.map_abs_vars shortest_name

  1425   in

  1426     (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),

  1427       (got_all_mono_user_axioms, no_poly_user_axioms)),

  1428      do_rest false true core_t)

  1429   end

  1431 end;

author	blanchet
	Tue, 09 Feb 2010 16:07:51 +0100
changeset 35075	6fd1052fe463
parent 35067	96136eb6218f
child 35076	592edca1dfb3
permissions	-rw-r--r--