1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jan 14 17:06:35 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Jan 20 10:38:06 2010 +0100
1.3 @@ -82,6 +82,7 @@
1.4 val dest_n_tuple : int -> term -> term list
1.5 val instantiate_type : theory -> typ -> typ -> typ -> typ
1.6 val is_real_datatype : theory -> string -> bool
1.7 + val is_quot_type : theory -> typ -> bool
1.8 val is_codatatype : theory -> typ -> bool
1.9 val is_pure_typedef : theory -> typ -> bool
1.10 val is_univ_typedef : theory -> typ -> bool
1.11 @@ -91,6 +92,8 @@
1.12 val is_record_update : theory -> styp -> bool
1.13 val is_abs_fun : theory -> styp -> bool
1.14 val is_rep_fun : theory -> styp -> bool
1.15 + val is_quot_abs_fun : Proof.context -> styp -> bool
1.16 + val is_quot_rep_fun : Proof.context -> styp -> bool
1.17 val is_constr : theory -> styp -> bool
1.18 val is_stale_constr : theory -> styp -> bool
1.19 val is_sel : string -> bool
1.20 @@ -325,6 +328,8 @@
1.21 (@{const_name uminus_int_inst.uminus_int}, 0),
1.22 (@{const_name ord_int_inst.less_int}, 2),
1.23 (@{const_name ord_int_inst.less_eq_int}, 2),
1.24 + (@{const_name unknown}, 0),
1.25 + (@{const_name is_unknown}, 1),
1.26 (@{const_name Tha}, 1),
1.27 (@{const_name Frac}, 0),
1.28 (@{const_name norm_frac}, 0)]
1.29 @@ -506,8 +511,8 @@
1.30 val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
1.31 val (co_s, co_Ts) = dest_Type co_T
1.32 val _ =
1.33 - if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts)
1.34 - andalso co_s <> "fun" andalso not (is_basic_datatype co_s) then
1.35 + if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
1.36 + co_s <> "fun" andalso not (is_basic_datatype co_s) then
1.37 ()
1.38 else
1.39 raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
1.40 @@ -543,14 +548,16 @@
1.41 val is_typedef = is_some oo typedef_info
1.42 val is_real_datatype = is_some oo Datatype.get_info
1.43 (* theory -> typ -> bool *)
1.44 +fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* ### *)
1.45 + | is_quot_type _ _ = false
1.46 fun is_codatatype thy (T as Type (s, _)) =
1.47 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
1.48 |> Option.map snd |> these))
1.49 | is_codatatype _ _ = false
1.50 fun is_pure_typedef thy (T as Type (s, _)) =
1.51 is_typedef thy s andalso
1.52 - not (is_real_datatype thy s orelse is_codatatype thy T
1.53 - orelse is_record_type T orelse is_integer_type T)
1.54 + not (is_real_datatype thy s orelse is_quot_type thy T orelse
1.55 + is_codatatype thy T orelse is_record_type T orelse is_integer_type T)
1.56 | is_pure_typedef _ _ = false
1.57 fun is_univ_typedef thy (Type (s, _)) =
1.58 (case typedef_info thy s of
1.59 @@ -564,8 +571,9 @@
1.60 | NONE => false)
1.61 | is_univ_typedef _ _ = false
1.62 fun is_datatype thy (T as Type (s, _)) =
1.63 - (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind})
1.64 - andalso not (is_basic_datatype s)
1.65 + (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
1.66 + is_quot_type thy T) andalso
1.67 + not (is_basic_datatype s)
1.68 | is_datatype _ _ = false
1.69
1.70 (* theory -> typ -> (string * typ) list * (string * typ) *)
1.71 @@ -606,6 +614,11 @@
1.72 SOME {Rep_name, ...} => s = Rep_name
1.73 | NONE => false)
1.74 | is_rep_fun _ _ = false
1.75 +(* Proof.context -> styp -> bool *)
1.76 +fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* ### *)
1.77 + | is_quot_abs_fun _ _ = false
1.78 +fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* ### *)
1.79 + | is_quot_rep_fun _ _ = false
1.80
1.81 (* theory -> styp -> styp *)
1.82 fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
1.83 @@ -613,6 +626,15 @@
1.84 SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
1.85 | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
1.86 | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
1.87 +(* theory -> typ -> typ *)
1.88 +fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"}
1.89 + | rep_type_for_quot_type _ T =
1.90 + raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
1.91 +(* theory -> typ -> term *)
1.92 +fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) =
1.93 + Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"})
1.94 + | equiv_relation_for_quot_type _ T =
1.95 + raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
1.96
1.97 (* theory -> styp -> bool *)
1.98 fun is_coconstr thy (s, T) =
1.99 @@ -628,19 +650,20 @@
1.100 fun is_constr_like thy (s, T) =
1.101 s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse
1.102 let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
1.103 - Refute.is_IDT_constructor thy x orelse is_record_constr x
1.104 - orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
1.105 - orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep}
1.106 - orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
1.107 - orelse is_coconstr thy x
1.108 + Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
1.109 + (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
1.110 + s = @{const_name Quot} orelse
1.111 + s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep} orelse
1.112 + x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
1.113 + is_coconstr thy x
1.114 end
1.115 fun is_stale_constr thy (x as (_, T)) =
1.116 - is_codatatype thy (body_type T) andalso is_constr_like thy x
1.117 - andalso not (is_coconstr thy x)
1.118 + is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
1.119 + not (is_coconstr thy x)
1.120 fun is_constr thy (x as (_, T)) =
1.121 - is_constr_like thy x
1.122 - andalso not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T)))))
1.123 - andalso not (is_stale_constr thy x)
1.124 + is_constr_like thy x andalso
1.125 + not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso
1.126 + not (is_stale_constr thy x)
1.127 (* string -> bool *)
1.128 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
1.129 val is_sel_like_and_no_discr =
1.130 @@ -662,13 +685,13 @@
1.131 fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
1.132 case T of
1.133 Type ("fun", _) =>
1.134 - (boxy = InPair orelse boxy = InFunLHS)
1.135 - andalso not (is_boolean_type (body_type T))
1.136 + (boxy = InPair orelse boxy = InFunLHS) andalso
1.137 + not (is_boolean_type (body_type T))
1.138 | Type ("*", Ts) =>
1.139 - boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2
1.140 - orelse ((boxy = InExpr orelse boxy = InFunLHS)
1.141 - andalso exists (is_boxing_worth_it ext_ctxt InPair)
1.142 - (map (box_type ext_ctxt InPair) Ts))
1.143 + boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
1.144 + ((boxy = InExpr orelse boxy = InFunLHS) andalso
1.145 + exists (is_boxing_worth_it ext_ctxt InPair)
1.146 + (map (box_type ext_ctxt InPair) Ts))
1.147 | _ => false
1.148 (* extended_context -> boxability -> string * typ list -> string *)
1.149 and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
1.150 @@ -679,8 +702,8 @@
1.151 and box_type ext_ctxt boxy T =
1.152 case T of
1.153 Type (z as ("fun", [T1, T2])) =>
1.154 - if boxy <> InConstr andalso boxy <> InSel
1.155 - andalso should_box_type ext_ctxt boxy z then
1.156 + if boxy <> InConstr andalso boxy <> InSel andalso
1.157 + should_box_type ext_ctxt boxy z then
1.158 Type (@{type_name fun_box},
1.159 [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
1.160 else
1.161 @@ -778,6 +801,8 @@
1.162 val T' = (Record.get_extT_fields thy T
1.163 |> apsnd single |> uncurry append |> map snd) ---> T
1.164 in [(s', T')] end
1.165 + else if is_quot_type thy T then
1.166 + [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
1.167 else case typedef_info thy s of
1.168 SOME {abs_type, rep_type, Abs_name, ...} =>
1.169 [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
1.170 @@ -871,10 +896,10 @@
1.171 let val args = map Envir.eta_contract args in
1.172 case hd args of
1.173 Const (x' as (s', _)) $ t =>
1.174 - if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s
1.175 - andalso forall (fn (n, t') =>
1.176 - select_nth_constr_arg thy x t n dummyT = t')
1.177 - (index_seq 0 (length args) ~~ args) then
1.178 + if is_sel_like_and_no_discr s' andalso
1.179 + constr_name_for_sel_like s' = s andalso
1.180 + forall (fn (n, t') => select_nth_constr_arg thy x t n dummyT = t')
1.181 + (index_seq 0 (length args) ~~ args) then
1.182 t
1.183 else
1.184 list_comb (Const x, args)
1.185 @@ -1011,8 +1036,8 @@
1.186 (* theory -> string -> bool *)
1.187 fun is_funky_typedef_name thy s =
1.188 member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
1.189 - @{type_name int}] s
1.190 - orelse is_frac_type thy (Type (s, []))
1.191 + @{type_name int}] s orelse
1.192 + is_frac_type thy (Type (s, []))
1.193 (* theory -> term -> bool *)
1.194 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
1.195 | is_funky_typedef _ _ = false
1.196 @@ -1055,8 +1080,8 @@
1.197 (* term -> bool *)
1.198 fun do_lhs t1 =
1.199 case strip_comb t1 of
1.200 - (Const _, args) => forall is_Var args
1.201 - andalso not (has_duplicates (op =) args)
1.202 + (Const _, args) =>
1.203 + forall is_Var args andalso not (has_duplicates (op =) args)
1.204 | _ => false
1.205 fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
1.206 | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
1.207 @@ -1174,8 +1199,8 @@
1.208 (* term -> bool *)
1.209 fun is_good_arg (Bound _) = true
1.210 | is_good_arg (Const (s, _)) =
1.211 - s = @{const_name True} orelse s = @{const_name False}
1.212 - orelse s = @{const_name undefined}
1.213 + s = @{const_name True} orelse s = @{const_name False} orelse
1.214 + s = @{const_name undefined}
1.215 | is_good_arg _ = false
1.216 in
1.217 case t |> strip_abs_body |> strip_comb of
1.218 @@ -1289,9 +1314,17 @@
1.219 fun nondef_props_for_const thy slack table (x as (s, _)) =
1.220 these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
1.221
1.222 +(* theory -> styp -> term list *)
1.223 +fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
1.224 + let val abs_T = domain_type T in
1.225 + typedef_info thy (fst (dest_Type abs_T)) |> the
1.226 + |> pairf #Abs_inverse #Rep_inverse
1.227 + |> pairself (Refute.specialize_type thy x o prop_of o the)
1.228 + ||> single |> op ::
1.229 + end
1.230 (* theory -> styp list -> term list *)
1.231 -fun optimized_typedef_axioms thy (abs_s, abs_Ts) =
1.232 - let val abs_T = Type (abs_s, abs_Ts) in
1.233 +fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
1.234 + let val abs_T = Type abs_z in
1.235 if is_univ_typedef thy abs_T then
1.236 []
1.237 else case typedef_info thy abs_s of
1.238 @@ -1313,13 +1346,31 @@
1.239 end
1.240 | NONE => []
1.241 end
1.242 -(* theory -> styp -> term list *)
1.243 -fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
1.244 - let val abs_T = domain_type T in
1.245 - typedef_info thy (fst (dest_Type abs_T)) |> the
1.246 - |> pairf #Abs_inverse #Rep_inverse
1.247 - |> pairself (Refute.specialize_type thy x o prop_of o the)
1.248 - ||> single |> op ::
1.249 +fun optimized_quot_type_axioms thy abs_z =
1.250 + let
1.251 + val abs_T = Type abs_z
1.252 + val rep_T = rep_type_for_quot_type thy abs_T
1.253 + val equiv_rel = equiv_relation_for_quot_type thy abs_T
1.254 + val a_var = Var (("a", 0), abs_T)
1.255 + val x_var = Var (("x", 0), rep_T)
1.256 + val y_var = Var (("y", 0), rep_T)
1.257 + val x = (@{const_name Quot}, rep_T --> abs_T)
1.258 + val sel_a_t = select_nth_constr_arg thy x a_var 0 rep_T
1.259 + val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
1.260 + val normal_x = normal_t $ x_var
1.261 + val normal_y = normal_t $ y_var
1.262 + val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
1.263 + in
1.264 + [Logic.mk_equals (sel_a_t, normal_t $ sel_a_t),
1.265 + Logic.list_implies
1.266 + ([@{const Not} $ (HOLogic.mk_eq (x_var, y_var)),
1.267 + @{const Not} $ (is_unknown_t $ normal_x),
1.268 + @{const Not} $ (is_unknown_t $ normal_y),
1.269 + equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
1.270 + Logic.mk_equals (normal_x, normal_y)),
1.271 + @{const "==>"}
1.272 + $ (HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)))
1.273 + $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
1.274 end
1.275
1.276 (* theory -> int * styp -> term *)
1.277 @@ -1402,8 +1453,8 @@
1.278 (* extended_context -> styp -> bool *)
1.279 fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
1.280 : extended_context) x =
1.281 - not (null (def_props_for_const thy fast_descrs intro_table x))
1.282 - andalso fixpoint_kind_of_const thy def_table x <> NoFp
1.283 + not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
1.284 + fixpoint_kind_of_const thy def_table x <> NoFp
1.285 fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
1.286 : extended_context) x =
1.287 exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
1.288 @@ -1489,10 +1540,9 @@
1.289 (t1 |> HOLogic.dest_list |> distinctness_formula T'
1.290 handle TERM _ => do_const depth Ts t x [t1])
1.291 | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
1.292 - if is_ground_term t1
1.293 - andalso exists (Pattern.matches thy o rpair t1)
1.294 - (Inttab.lookup_list ground_thm_table
1.295 - (hash_term t1)) then
1.296 + if is_ground_term t1 andalso
1.297 + exists (Pattern.matches thy o rpair t1)
1.298 + (Inttab.lookup_list ground_thm_table (hash_term t1)) then
1.299 do_term depth Ts t2
1.300 else
1.301 do_const depth Ts t x [t1, t2, t3]
1.302 @@ -1534,8 +1584,24 @@
1.303 if is_constr thy x then
1.304 (Const x, ts)
1.305 else if is_stale_constr thy x then
1.306 - raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
1.307 + raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
1.308 \(\"" ^ s ^ "\")")
1.309 + else if is_quot_abs_fun thy x then
1.310 + let
1.311 + val rep_T = domain_type T
1.312 + val abs_T = range_type T
1.313 + in
1.314 + (Abs (Name.uu, rep_T,
1.315 + Const (@{const_name Quot}, rep_T --> abs_T)
1.316 + $ (Const (@{const_name quot_normal},
1.317 + rep_T --> rep_T) $ Bound 0)), ts)
1.318 + end
1.319 + else if is_quot_rep_fun thy x then
1.320 + let
1.321 + val abs_T = domain_type T
1.322 + val rep_T = range_type T
1.323 + val x' = (@{const_name Quot}, rep_T --> abs_T)
1.324 + in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end
1.325 else if is_record_get thy x then
1.326 case length ts of
1.327 0 => (do_term depth Ts (eta_expand Ts t 1), [])
1.328 @@ -1691,8 +1757,8 @@
1.329 else
1.330 ()
1.331 in
1.332 - if tac_timeout = (!cached_timeout)
1.333 - andalso length (!cached_wf_props) < max_cached_wfs then
1.334 + if tac_timeout = (!cached_timeout) andalso
1.335 + length (!cached_wf_props) < max_cached_wfs then
1.336 ()
1.337 else
1.338 (cached_wf_props := []; cached_timeout := tac_timeout);
1.339 @@ -1716,8 +1782,8 @@
1.340 (x as (s, _)) =
1.341 case triple_lookup (const_match thy) wfs x of
1.342 SOME (SOME b) => b
1.343 - | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'}
1.344 - orelse case AList.lookup (op =) (!wf_cache) x of
1.345 + | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
1.346 + case AList.lookup (op =) (!wf_cache) x of
1.347 SOME (_, wf) => wf
1.348 | NONE =>
1.349 let
1.350 @@ -1859,8 +1925,8 @@
1.351 in
1.352 if is_equational_fun ext_ctxt x' then
1.353 unrolled_const (* already done *)
1.354 - else if not gfp andalso is_linear_inductive_pred_def def
1.355 - andalso star_linear_preds then
1.356 + else if not gfp andalso is_linear_inductive_pred_def def andalso
1.357 + star_linear_preds then
1.358 starred_linear_pred_const ext_ctxt x def
1.359 else
1.360 let
1.361 @@ -1980,10 +2046,10 @@
1.362 let val t_comb = list_comb (t, args) in
1.363 case t of
1.364 Const x =>
1.365 - if not relax andalso is_constr thy x
1.366 - andalso not (is_fun_type (fastype_of1 (Ts, t_comb)))
1.367 - andalso has_heavy_bounds_or_vars Ts level t_comb
1.368 - andalso not (loose_bvar (t_comb, level)) then
1.369 + if not relax andalso is_constr thy x andalso
1.370 + not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
1.371 + has_heavy_bounds_or_vars Ts level t_comb andalso
1.372 + not (loose_bvar (t_comb, level)) then
1.373 let
1.374 val (j, seen) = case find_index (curry (op =) t_comb) seen of
1.375 ~1 => (0, t_comb :: seen)
1.376 @@ -2062,18 +2128,17 @@
1.377 and aux_eq careful pass1 t0 t1 t2 =
1.378 (if careful then
1.379 raise SAME ()
1.380 - else if axiom andalso is_Var t2
1.381 - andalso num_occs_of_var (dest_Var t2) = 1 then
1.382 + else if axiom andalso is_Var t2 andalso
1.383 + num_occs_of_var (dest_Var t2) = 1 then
1.384 @{const True}
1.385 else case strip_comb t2 of
1.386 (Const (x as (s, T)), args) =>
1.387 let val arg_Ts = binder_types T in
1.388 - if length arg_Ts = length args
1.389 - andalso (is_constr thy x orelse s = @{const_name Pair}
1.390 - orelse x = (@{const_name Suc}, nat_T --> nat_T))
1.391 - andalso (not careful orelse not (is_Var t1)
1.392 - orelse String.isPrefix val_var_prefix
1.393 - (fst (fst (dest_Var t1)))) then
1.394 + if length arg_Ts = length args andalso
1.395 + (is_constr thy x orelse s = @{const_name Pair} orelse
1.396 + x = (@{const_name Suc}, nat_T --> nat_T)) andalso
1.397 + (not careful orelse not (is_Var t1) orelse
1.398 + String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
1.399 discriminate_value ext_ctxt x t1 ::
1.400 map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
1.401 |> foldr1 s_conj
1.402 @@ -2095,8 +2160,8 @@
1.403 let
1.404 (* term -> int -> term *)
1.405 fun is_nth_sel_on t' n (Const (s, _) $ t) =
1.406 - (t = t' andalso is_sel_like_and_no_discr s
1.407 - andalso sel_no_from_name s = n)
1.408 + (t = t' andalso is_sel_like_and_no_discr s andalso
1.409 + sel_no_from_name s = n)
1.410 | is_nth_sel_on _ _ _ = false
1.411 (* term -> term list -> term *)
1.412 fun do_term (Const (@{const_name Rep_Frac}, _)
1.413 @@ -2109,9 +2174,9 @@
1.414 if length args = num_binder_types T then
1.415 case hd args of
1.416 Const (x' as (_, T')) $ t' =>
1.417 - if domain_type T' = body_type T
1.418 - andalso forall (uncurry (is_nth_sel_on t'))
1.419 - (index_seq 0 (length args) ~~ args) then
1.420 + if domain_type T' = body_type T andalso
1.421 + forall (uncurry (is_nth_sel_on t'))
1.422 + (index_seq 0 (length args) ~~ args) then
1.423 t'
1.424 else
1.425 raise SAME ()
1.426 @@ -2121,9 +2186,9 @@
1.427 else if is_sel_like_and_no_discr s then
1.428 case strip_comb (hd args) of
1.429 (Const (x' as (s', T')), ts') =>
1.430 - if is_constr_like thy x'
1.431 - andalso constr_name_for_sel_like s = s'
1.432 - andalso not (exists is_pair_type (binder_types T')) then
1.433 + if is_constr_like thy x' andalso
1.434 + constr_name_for_sel_like s = s' andalso
1.435 + not (exists is_pair_type (binder_types T')) then
1.436 list_comb (nth ts' (sel_no_from_name s), tl args)
1.437 else
1.438 raise SAME ()
1.439 @@ -2164,8 +2229,8 @@
1.440 (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
1.441 -> term -> term *)
1.442 and aux_eq prems zs z t' t1 t2 =
1.443 - if not (member (op =) zs z)
1.444 - andalso not (exists_subterm (curry (op =) (Var z)) t') then
1.445 + if not (member (op =) zs z) andalso
1.446 + not (exists_subterm (curry (op =) (Var z)) t') then
1.447 aux prems zs (subst_free [(Var z, t')] t2)
1.448 else
1.449 aux (t1 :: prems) (Term.add_vars t1 zs) t2
1.450 @@ -2323,8 +2388,8 @@
1.451 (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
1.452 if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
1.453 aux s0 (s1 :: ss) (T1 :: Ts) t1
1.454 - else if quant_s = "" andalso (s0 = @{const_name All}
1.455 - orelse s0 = @{const_name Ex}) then
1.456 + else if quant_s = "" andalso
1.457 + (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
1.458 aux s0 [s1] [T1] t1
1.459 else
1.460 raise SAME ()
1.461 @@ -2402,8 +2467,8 @@
1.462
1.463 (* polarity -> string -> bool *)
1.464 fun is_positive_existential polar quant_s =
1.465 - (polar = Pos andalso quant_s = @{const_name Ex})
1.466 - orelse (polar = Neg andalso quant_s <> @{const_name Ex})
1.467 + (polar = Pos andalso quant_s = @{const_name Ex}) orelse
1.468 + (polar = Neg andalso quant_s <> @{const_name Ex})
1.469
1.470 (* extended_context -> int -> term -> term *)
1.471 fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
1.472 @@ -2418,8 +2483,8 @@
1.473 fun do_quantifier quant_s quant_T abs_s abs_T t =
1.474 if not (loose_bvar1 (t, 0)) then
1.475 aux ss Ts js depth polar (incr_boundvars ~1 t)
1.476 - else if depth <= skolem_depth
1.477 - andalso is_positive_existential polar quant_s then
1.478 + else if depth <= skolem_depth andalso
1.479 + is_positive_existential polar quant_s then
1.480 let
1.481 val j = length (!skolems) + 1
1.482 val sko_s = skolem_prefix_for (length js) j ^ abs_s
1.483 @@ -2469,8 +2534,8 @@
1.484 | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
1.485 t0 $ t1 $ aux ss Ts js depth polar t2
1.486 | Const (x as (s, T)) =>
1.487 - if is_inductive_pred ext_ctxt x
1.488 - andalso not (is_well_founded_inductive_pred ext_ctxt x) then
1.489 + if is_inductive_pred ext_ctxt x andalso
1.490 + not (is_well_founded_inductive_pred ext_ctxt x) then
1.491 let
1.492 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
1.493 val (pref, connective, set_oper) =
1.494 @@ -2582,9 +2647,9 @@
1.495 (* typ list -> term -> bool *)
1.496 fun is_eligible_arg Ts t =
1.497 let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
1.498 - null bad_Ts
1.499 - orelse (is_higher_order_type (fastype_of1 (Ts, t))
1.500 - andalso forall (not o is_higher_order_type) bad_Ts)
1.501 + null bad_Ts orelse
1.502 + (is_higher_order_type (fastype_of1 (Ts, t)) andalso
1.503 + forall (not o is_higher_order_type) bad_Ts)
1.504 end
1.505
1.506 (* (int * term option) list -> (int * term) list -> int list *)
1.507 @@ -2608,9 +2673,9 @@
1.508 else case term_under_def t of Const x => [x] | _ => []
1.509 (* term list -> typ list -> term -> term *)
1.510 fun aux args Ts (Const (x as (s, T))) =
1.511 - ((if not (member (op =) blacklist x) andalso not (null args)
1.512 - andalso not (String.isPrefix special_prefix s)
1.513 - andalso is_equational_fun ext_ctxt x then
1.514 + ((if not (member (op =) blacklist x) andalso not (null args) andalso
1.515 + not (String.isPrefix special_prefix s) andalso
1.516 + is_equational_fun ext_ctxt x then
1.517 let
1.518 val eligible_args = filter (is_eligible_arg Ts o snd)
1.519 (index_seq 0 (length args) ~~ args)
1.520 @@ -2678,8 +2743,8 @@
1.521 let val table = aux t2 [] table in aux t1 (t2 :: args) table end
1.522 | aux (Abs (_, _, t')) _ table = aux t' [] table
1.523 | aux (t as Const (x as (s, _))) args table =
1.524 - if is_built_in_const true x orelse is_constr_like thy x orelse is_sel s
1.525 - orelse s = @{const_name Sigma} then
1.526 + if is_built_in_const true x orelse is_constr_like thy x orelse
1.527 + is_sel s orelse s = @{const_name Sigma} then
1.528 table
1.529 else
1.530 Termtab.map_default (t, 65536) (curry Int.min (length args)) table
1.531 @@ -2699,8 +2764,8 @@
1.532 let
1.533 val (arg_Ts, rest_T) = strip_n_binders n T
1.534 val j =
1.535 - if hd arg_Ts = @{typ bisim_iterator}
1.536 - orelse is_fp_iterator_type (hd arg_Ts) then
1.537 + if hd arg_Ts = @{typ bisim_iterator} orelse
1.538 + is_fp_iterator_type (hd arg_Ts) then
1.539 1
1.540 else case find_index (not_equal bool_T) arg_Ts of
1.541 ~1 => n
1.542 @@ -2766,8 +2831,8 @@
1.543 \coerce_term", [t']))
1.544 | (Type (new_s, new_Ts as [new_T1, new_T2]),
1.545 Type (old_s, old_Ts as [old_T1, old_T2])) =>
1.546 - if old_s = @{type_name fun_box} orelse old_s = @{type_name pair_box}
1.547 - orelse old_s = "*" then
1.548 + if old_s = @{type_name fun_box} orelse
1.549 + old_s = @{type_name pair_box} orelse old_s = "*" then
1.550 case constr_expand ext_ctxt old_T t of
1.551 Const (@{const_name FunBox}, _) $ t1 =>
1.552 if new_s = "fun" then
1.553 @@ -2881,13 +2946,17 @@
1.554 $ do_term new_Ts old_Ts polar t2
1.555 | Const (s as @{const_name The}, T) => do_description_operator s T
1.556 | Const (s as @{const_name Eps}, T) => do_description_operator s T
1.557 + | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
1.558 + let val T' = box_type ext_ctxt InFunRHS1 T2 in
1.559 + Const (@{const_name quot_normal}, T' --> T')
1.560 + end
1.561 | Const (s as @{const_name Tha}, T) => do_description_operator s T
1.562 | Const (x as (s, T)) =>
1.563 - Const (s, if s = @{const_name converse}
1.564 - orelse s = @{const_name trancl} then
1.565 + Const (s, if s = @{const_name converse} orelse
1.566 + s = @{const_name trancl} then
1.567 box_relational_operator_type T
1.568 - else if is_built_in_const fast_descrs x
1.569 - orelse s = @{const_name Sigma} then
1.570 + else if is_built_in_const fast_descrs x orelse
1.571 + s = @{const_name Sigma} then
1.572 T
1.573 else if is_constr_like thy x then
1.574 box_type ext_ctxt InConstr T
1.575 @@ -2972,7 +3041,7 @@
1.576 |> map Logic.mk_equals,
1.577 Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
1.578 list_comb (Const x2, bounds2 @ args2)))
1.579 - |> Refute.close_form
1.580 + |> Refute.close_form (* TODO: needed? *)
1.581 end
1.582
1.583 (* extended_context -> styp list -> term list *)
1.584 @@ -3078,23 +3147,29 @@
1.585 fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
1.586 accum
1.587 else if is_abs_fun thy x then
1.588 - accum |> fold (add_nondef_axiom depth)
1.589 - (nondef_props_for_const thy false nondef_table x)
1.590 - |> is_funky_typedef thy (range_type T)
1.591 - ? fold (add_maybe_def_axiom depth)
1.592 - (nondef_props_for_const thy true
1.593 + if is_quot_type thy (range_type T) then
1.594 + raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
1.595 + else
1.596 + accum |> fold (add_nondef_axiom depth)
1.597 + (nondef_props_for_const thy false nondef_table x)
1.598 + |> is_funky_typedef thy (range_type T)
1.599 + ? fold (add_maybe_def_axiom depth)
1.600 + (nondef_props_for_const thy true
1.601 (extra_table def_table s) x)
1.602 else if is_rep_fun thy x then
1.603 - accum |> fold (add_nondef_axiom depth)
1.604 - (nondef_props_for_const thy false nondef_table x)
1.605 - |> is_funky_typedef thy (range_type T)
1.606 - ? fold (add_maybe_def_axiom depth)
1.607 - (nondef_props_for_const thy true
1.608 + if is_quot_type thy (domain_type T) then
1.609 + raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
1.610 + else
1.611 + accum |> fold (add_nondef_axiom depth)
1.612 + (nondef_props_for_const thy false nondef_table x)
1.613 + |> is_funky_typedef thy (range_type T)
1.614 + ? fold (add_maybe_def_axiom depth)
1.615 + (nondef_props_for_const thy true
1.616 (extra_table def_table s) x)
1.617 - |> add_axioms_for_term depth
1.618 - (Const (mate_of_rep_fun thy x))
1.619 - |> fold (add_def_axiom depth)
1.620 - (inverse_axioms_for_rep_fun thy x)
1.621 + |> add_axioms_for_term depth
1.622 + (Const (mate_of_rep_fun thy x))
1.623 + |> fold (add_def_axiom depth)
1.624 + (inverse_axioms_for_rep_fun thy x)
1.625 else
1.626 accum |> user_axioms <> SOME false
1.627 ? fold (add_nondef_axiom depth)
1.628 @@ -3116,10 +3191,12 @@
1.629 | @{typ unit} => I
1.630 | TFree (_, S) => add_axioms_for_sort depth T S
1.631 | TVar (_, S) => add_axioms_for_sort depth T S
1.632 - | Type (z as (_, Ts)) =>
1.633 + | Type (z as (s, Ts)) =>
1.634 fold (add_axioms_for_type depth) Ts
1.635 #> (if is_pure_typedef thy T then
1.636 fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
1.637 + else if is_quot_type thy T then
1.638 + fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
1.639 else if max_bisim_depth >= 0 andalso is_codatatype thy T then
1.640 fold (add_maybe_def_axiom depth)
1.641 (codatatype_bisim_axioms ext_ctxt T)
1.642 @@ -3364,11 +3441,11 @@
1.643 member (op =) [@{const_name times_nat_inst.times_nat},
1.644 @{const_name div_nat_inst.div_nat},
1.645 @{const_name times_int_inst.times_int},
1.646 - @{const_name div_int_inst.div_int}] s
1.647 - orelse (String.isPrefix numeral_prefix s andalso
1.648 - let val n = the (Int.fromString (unprefix numeral_prefix s)) in
1.649 - n <= ~ binary_int_threshold orelse n >= binary_int_threshold
1.650 - end)
1.651 + @{const_name div_int_inst.div_int}] s orelse
1.652 + (String.isPrefix numeral_prefix s andalso
1.653 + let val n = the (Int.fromString (unprefix numeral_prefix s)) in
1.654 + n <= ~ binary_int_threshold orelse n >= binary_int_threshold
1.655 + end)
1.656 | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
1.657 | should_use_binary_ints _ = false
1.658
1.659 @@ -3398,8 +3475,8 @@
1.660 SOME false => false
1.661 | _ =>
1.662 forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
1.663 - (binary_ints = SOME true
1.664 - orelse exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
1.665 + (binary_ints = SOME true orelse
1.666 + exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
1.667 val box = exists (not_equal (SOME false) o snd) boxes
1.668 val table =
1.669 Termtab.empty |> uncurry