src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 35220 2bcdae5f4fdb
parent 35219 15a5f213ef5b
child 35280 54ab4921f826
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 18 10:38:37 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 18 18:48:07 2010 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4  fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
     1.5      could_exist_alpha_subtype alpha_T T
     1.6    | could_exist_alpha_sub_ctype thy alpha_T T =
     1.7 -    (T = alpha_T orelse is_datatype thy T)
     1.8 +    (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
     1.9  
    1.10  (* ctype -> bool *)
    1.11  fun exists_alpha_sub_ctype CAlpha = true
    1.12 @@ -545,8 +545,9 @@
    1.13    handle List.Empty => initial_gamma
    1.14  
    1.15  (* cdata -> term -> accumulator -> ctype * accumulator *)
    1.16 -fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
    1.17 -                             max_fresh, ...}) =
    1.18 +fun consider_term (cdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
    1.19 +                                          def_table, ...},
    1.20 +                             alpha_T, max_fresh, ...}) =
    1.21    let
    1.22      (* typ -> ctype *)
    1.23      val ctype_for = fresh_ctype_for_type cdata
    1.24 @@ -663,10 +664,6 @@
    1.25                  in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
    1.26                | @{const_name trancl} => do_fragile_set_operation T accum
    1.27                | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
    1.28 -              | @{const_name semilattice_inf_fun_inst.inf_fun} =>
    1.29 -                do_robust_set_operation T accum
    1.30 -              | @{const_name semilattice_sup_fun_inst.sup_fun} =>
    1.31 -                do_robust_set_operation T accum
    1.32                | @{const_name finite} =>
    1.33                  let val C1 = ctype_for (domain_type (domain_type T)) in
    1.34                    (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
    1.35 @@ -710,19 +707,6 @@
    1.36                    (CFun (a_set_C, S Minus,
    1.37                           CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
    1.38                  end
    1.39 -              | @{const_name minus_fun_inst.minus_fun} =>
    1.40 -                let
    1.41 -                  val set_T = domain_type T
    1.42 -                  val left_set_C = ctype_for set_T
    1.43 -                  val right_set_C = ctype_for set_T
    1.44 -                in
    1.45 -                  (CFun (left_set_C, S Minus,
    1.46 -                         CFun (right_set_C, S Minus, left_set_C)),
    1.47 -                   (gamma, cset |> add_ctype_is_right_unique right_set_C
    1.48 -                                |> add_is_sub_ctype right_set_C left_set_C))
    1.49 -                end
    1.50 -              | @{const_name ord_fun_inst.less_eq_fun} =>
    1.51 -                do_fragile_set_operation T accum
    1.52                | @{const_name Tha} =>
    1.53                  let
    1.54                    val a_C = ctype_for (domain_type (domain_type T))
    1.55 @@ -732,24 +716,44 @@
    1.56                  let val dom_C = ctype_for (domain_type T) in
    1.57                    (CFun (dom_C, S Minus, dom_C), accum)
    1.58                  end
    1.59 -              | _ => if is_sel s then
    1.60 -                       if constr_name_for_sel_like s = @{const_name FunBox} then
    1.61 -                         let val dom_C = ctype_for (domain_type T) in
    1.62 -                           (CFun (dom_C, S Minus, dom_C), accum)
    1.63 -                         end
    1.64 -                       else
    1.65 -                         (ctype_for_sel cdata x, accum)
    1.66 -                     else if is_constr thy x then
    1.67 -                       (ctype_for_constr cdata x, accum)
    1.68 -                     else if is_built_in_const true x then
    1.69 -                       case def_of_const thy def_table x of
    1.70 -                         SOME t' => do_term t' accum
    1.71 -                       | NONE => (print_g ("*** built-in " ^ s); unsolvable)
    1.72 -                     else
    1.73 -                       let val C = ctype_for T in
    1.74 -                         (C, ({bounds = bounds, frees = frees,
    1.75 -                               consts = (x, C) :: consts}, cset))
    1.76 -                       end)
    1.77 +              | _ =>
    1.78 +                if s = @{const_name minus_class.minus} andalso
    1.79 +                   is_set_type (domain_type T) then
    1.80 +                  let
    1.81 +                    val set_T = domain_type T
    1.82 +                    val left_set_C = ctype_for set_T
    1.83 +                    val right_set_C = ctype_for set_T
    1.84 +                  in
    1.85 +                    (CFun (left_set_C, S Minus,
    1.86 +                           CFun (right_set_C, S Minus, left_set_C)),
    1.87 +                     (gamma, cset |> add_ctype_is_right_unique right_set_C
    1.88 +                                  |> add_is_sub_ctype right_set_C left_set_C))
    1.89 +                  end
    1.90 +                else if s = @{const_name ord_class.less_eq} andalso
    1.91 +                        is_set_type (domain_type T) then
    1.92 +                  do_fragile_set_operation T accum
    1.93 +                else if (s = @{const_name semilattice_inf_class.inf} orelse
    1.94 +                         s = @{const_name semilattice_sup_class.sup}) andalso
    1.95 +                        is_set_type (domain_type T) then
    1.96 +                  do_robust_set_operation T accum
    1.97 +                else if is_sel s then
    1.98 +                  if constr_name_for_sel_like s = @{const_name FunBox} then
    1.99 +                    let val dom_C = ctype_for (domain_type T) in
   1.100 +                      (CFun (dom_C, S Minus, dom_C), accum)
   1.101 +                    end
   1.102 +                  else
   1.103 +                    (ctype_for_sel cdata x, accum)
   1.104 +                else if is_constr thy stds x then
   1.105 +                  (ctype_for_constr cdata x, accum)
   1.106 +                else if is_built_in_const thy stds fast_descrs x then
   1.107 +                  case def_of_const thy def_table x of
   1.108 +                    SOME t' => do_term t' accum
   1.109 +                  | NONE => (print_g ("*** built-in " ^ s); unsolvable)
   1.110 +                else
   1.111 +                  let val C = ctype_for T in
   1.112 +                    (C, ({bounds = bounds, frees = frees,
   1.113 +                          consts = (x, C) :: consts}, cset))
   1.114 +                  end)
   1.115           | Free (x as (_, T)) =>
   1.116             (case AList.lookup (op =) frees x of
   1.117                SOME C => (C, accum)
   1.118 @@ -881,20 +885,21 @@
   1.119  val bounteous_consts = [@{const_name bisim}]
   1.120  
   1.121  (* term -> bool *)
   1.122 -fun is_harmless_axiom t =
   1.123 -  Term.add_consts t [] |> filter_out (is_built_in_const true)
   1.124 +fun is_harmless_axiom ({thy, stds, fast_descrs, ...} : hol_context) t =
   1.125 +  Term.add_consts t []
   1.126 +  |> filter_out (is_built_in_const thy stds fast_descrs)
   1.127    |> (forall (member (op =) harmless_consts o original_name o fst)
   1.128        orf exists (member (op =) bounteous_consts o fst))
   1.129  
   1.130  (* cdata -> sign -> term -> accumulator -> accumulator *)
   1.131 -fun consider_nondefinitional_axiom cdata sn t =
   1.132 -  not (is_harmless_axiom t) ? consider_general_formula cdata sn t
   1.133 +fun consider_nondefinitional_axiom (cdata as {hol_ctxt, ...}) sn t =
   1.134 +  not (is_harmless_axiom hol_ctxt t) ? consider_general_formula cdata sn t
   1.135  
   1.136  (* cdata -> term -> accumulator -> accumulator *)
   1.137  fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
   1.138    if not (is_constr_pattern_formula thy t) then
   1.139      consider_nondefinitional_axiom cdata Plus t
   1.140 -  else if is_harmless_axiom t then
   1.141 +  else if is_harmless_axiom hol_ctxt t then
   1.142      I
   1.143    else
   1.144      let