src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33571 3655e51f9958
parent 33557 107f3df799f6
child 33578 0c3ba1e010d2
equal deleted inserted replaced
33570:14f2880e7ccf 33571:3655e51f9958
   311    (@{const_name plus_int_inst.plus_int}, 0),
   311    (@{const_name plus_int_inst.plus_int}, 0),
   312    (@{const_name minus_int_inst.minus_int}, 0),
   312    (@{const_name minus_int_inst.minus_int}, 0),
   313    (@{const_name times_int_inst.times_int}, 0),
   313    (@{const_name times_int_inst.times_int}, 0),
   314    (@{const_name div_int_inst.div_int}, 0),
   314    (@{const_name div_int_inst.div_int}, 0),
   315    (@{const_name div_int_inst.mod_int}, 0),
   315    (@{const_name div_int_inst.mod_int}, 0),
   316    (@{const_name uminus_int_inst.uminus_int}, 0), (* FIXME: needed? *)
   316    (@{const_name uminus_int_inst.uminus_int}, 0),
   317    (@{const_name ord_int_inst.less_int}, 2),
   317    (@{const_name ord_int_inst.less_int}, 2),
   318    (@{const_name ord_int_inst.less_eq_int}, 2),
   318    (@{const_name ord_int_inst.less_eq_int}, 2),
   319    (@{const_name Tha}, 1),
   319    (@{const_name Tha}, 1),
   320    (@{const_name Frac}, 0),
   320    (@{const_name Frac}, 0),
   321    (@{const_name norm_frac}, 0)]
   321    (@{const_name norm_frac}, 0)]
   964   fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
   964   fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
   965 
   965 
   966 (* indexname * typ -> term -> term *)
   966 (* indexname * typ -> term -> term *)
   967 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
   967 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
   968 
   968 
       
   969 (* theory -> string -> bool *)
       
   970 fun is_funky_typedef_name thy s =
       
   971   s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
       
   972          @{type_name int}]
       
   973   orelse is_frac_type thy (Type (s, []))
       
   974 (* theory -> term -> bool *)
       
   975 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
       
   976   | is_funky_typedef _ _ = false
   969 (* term -> bool *)
   977 (* term -> bool *)
   970 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
   978 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
   971                          $ Const (@{const_name TYPE}, _)) = true
   979                          $ Const (@{const_name TYPE}, _)) = true
   972   | is_arity_type_axiom _ = false
   980   | is_arity_type_axiom _ = false
   973 (* theory -> bool -> term -> bool *)
   981 (* theory -> bool -> term -> bool *)
   974 fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
   982 fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
   975     is_typedef_axiom thy boring t2
   983     is_typedef_axiom thy boring t2
   976   | is_typedef_axiom thy boring
   984   | is_typedef_axiom thy boring
   977         (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
   985         (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
   978          $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
   986          $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
   979     boring <> (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]
   987     boring <> is_funky_typedef_name thy s andalso is_typedef thy s
   980                orelse is_frac_type thy (Type (s, [])))
       
   981     andalso is_typedef thy s
       
   982   | is_typedef_axiom _ _ _ = false
   988   | is_typedef_axiom _ _ _ = false
   983 
   989 
   984 (* Distinguishes between (1) constant definition axioms, (2) type arity and
   990 (* Distinguishes between (1) constant definition axioms, (2) type arity and
   985    typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
   991    typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
   986    Typedef axioms are uninteresting to Nitpick, because it can retrieve them
   992    Typedef axioms are uninteresting to Nitpick, because it can retrieve them
  2541                                             special_funs, ...}) depth t =
  2547                                             special_funs, ...}) depth t =
  2542   if not specialize orelse depth > special_depth then
  2548   if not specialize orelse depth > special_depth then
  2543     t
  2549     t
  2544   else
  2550   else
  2545     let
  2551     let
  2546       (* FIXME: strong enough in the face of user-defined axioms? *)
       
  2547       val blacklist = if depth = 0 then []
  2552       val blacklist = if depth = 0 then []
  2548                       else case term_under_def t of Const x => [x] | _ => []
  2553                       else case term_under_def t of Const x => [x] | _ => []
  2549       (* term list -> typ list -> term -> term *)
  2554       (* term list -> typ list -> term -> term *)
  2550       fun aux args Ts (Const (x as (s, T))) =
  2555       fun aux args Ts (Const (x as (s, T))) =
  2551           ((if not (x mem blacklist) andalso not (null args)
  2556           ((if not (x mem blacklist) andalso not (null args)
  3007                fold (add_def_axiom depth) (equational_fun_axioms ext_ctxt x)
  3012                fold (add_def_axiom depth) (equational_fun_axioms ext_ctxt x)
  3008                     accum
  3013                     accum
  3009              else if is_abs_fun thy x then
  3014              else if is_abs_fun thy x then
  3010                accum |> fold (add_nondef_axiom depth)
  3015                accum |> fold (add_nondef_axiom depth)
  3011                              (nondef_props_for_const thy false nondef_table x)
  3016                              (nondef_props_for_const thy false nondef_table x)
  3012                      |> fold (add_def_axiom depth)
  3017                      |> is_funky_typedef thy (range_type T)
  3013                              (nondef_props_for_const thy true
  3018                         ? fold (add_def_axiom depth)
       
  3019                                (nondef_props_for_const thy true
  3014                                                     (extra_table def_table s) x)
  3020                                                     (extra_table def_table s) x)
  3015              else if is_rep_fun thy x then
  3021              else if is_rep_fun thy x then
  3016                accum |> fold (add_nondef_axiom depth)
  3022                accum |> fold (add_nondef_axiom depth)
  3017                              (nondef_props_for_const thy false nondef_table x)
  3023                              (nondef_props_for_const thy false nondef_table x)
  3018                      |> fold (add_def_axiom depth)
  3024                      |> is_funky_typedef thy (range_type T)
  3019                              (nondef_props_for_const thy true
  3025                         ? fold (add_def_axiom depth)
       
  3026                                (nondef_props_for_const thy true
  3020                                                     (extra_table def_table s) x)
  3027                                                     (extra_table def_table s) x)
  3021                      |> add_axioms_for_term depth
  3028                      |> add_axioms_for_term depth
  3022                                             (Const (mate_of_rep_fun thy x))
  3029                                             (Const (mate_of_rep_fun thy x))
  3023                      |> add_def_axiom depth (inverse_axiom_for_rep_fun thy x)
  3030                      |> add_def_axiom depth (inverse_axiom_for_rep_fun thy x)
  3024              else
  3031              else