equal
deleted
inserted
replaced
322 fun quot_normal_name_for_type ctxt T = |
322 fun quot_normal_name_for_type ctxt T = |
323 quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T) |
323 quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T) |
324 |
324 |
325 val strip_first_name_sep = |
325 val strip_first_name_sep = |
326 Substring.full #> Substring.position name_sep ##> Substring.triml 1 |
326 Substring.full #> Substring.position name_sep ##> Substring.triml 1 |
327 #> pairself Substring.string |
327 #> apply2 Substring.string |
328 |
328 |
329 fun original_name s = |
329 fun original_name s = |
330 if String.isPrefix nitpick_prefix s then |
330 if String.isPrefix nitpick_prefix s then |
331 case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2 |
331 case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2 |
332 else |
332 else |
458 |
458 |
459 fun strict_type_match thy (T1, T2) = |
459 fun strict_type_match thy (T1, T2) = |
460 (Sign.typ_match thy (T2, T1) Vartab.empty; true) |
460 (Sign.typ_match thy (T2, T1) Vartab.empty; true) |
461 handle Type.TYPE_MATCH => false |
461 handle Type.TYPE_MATCH => false |
462 |
462 |
463 fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type |
463 fun type_match thy = strict_type_match thy o apply2 unarize_unbox_etc_type |
464 |
464 |
465 fun const_match thy ((s1, T1), (s2, T2)) = |
465 fun const_match thy ((s1, T1), (s2, T2)) = |
466 s1 = s2 andalso type_match thy (T1, T2) |
466 s1 = s2 andalso type_match thy (T1, T2) |
467 |
467 |
468 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2) |
468 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2) |
1327 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 |
1327 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 |
1328 | is_ground_term (Const _) = true |
1328 | is_ground_term (Const _) = true |
1329 | is_ground_term _ = false |
1329 | is_ground_term _ = false |
1330 |
1330 |
1331 fun special_bounds ts = |
1331 fun special_bounds ts = |
1332 fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst) |
1332 fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o apply2 fst) |
1333 |
1333 |
1334 fun is_funky_typedef_name ctxt s = |
1334 fun is_funky_typedef_name ctxt s = |
1335 member (op =) [@{type_name unit}, @{type_name prod}, @{type_name set}, |
1335 member (op =) [@{type_name unit}, @{type_name prod}, @{type_name set}, |
1336 @{type_name Sum_Type.sum}, @{type_name int}] s orelse |
1336 @{type_name Sum_Type.sum}, @{type_name int}] s orelse |
1337 is_frac_type ctxt (Type (s, [])) |
1337 is_frac_type ctxt (Type (s, [])) |
1348 |> Ord_List.make fast_string_ord |
1348 |> Ord_List.make fast_string_ord |
1349 in |
1349 in |
1350 Theory.nodes_of thy |
1350 Theory.nodes_of thy |
1351 |> maps Thm.axioms_of |
1351 |> maps Thm.axioms_of |
1352 |> map (apsnd (subst_atomic subst o prop_of)) |
1352 |> map (apsnd (subst_atomic subst o prop_of)) |
1353 |> sort (fast_string_ord o pairself fst) |
1353 |> sort (fast_string_ord o apply2 fst) |
1354 |> Ord_List.inter (fast_string_ord o apsnd fst) def_names |
1354 |> Ord_List.inter (fast_string_ord o apsnd fst) def_names |
1355 |> map snd |
1355 |> map snd |
1356 end |
1356 end |
1357 |
1357 |
1358 (* Ideally we would check against "Complex_Main", not "Hilbert_Choice", but any |
1358 (* Ideally we would check against "Complex_Main", not "Hilbert_Choice", but any |
1605 (constr_case_body ctxt (dataT :: Ts) |
1605 (constr_case_body ctxt (dataT :: Ts) |
1606 (incr_boundvars 1 func_t, x), |
1606 (incr_boundvars 1 func_t, x), |
1607 discriminate_value hol_ctxt x (Bound 0))) |
1607 discriminate_value hol_ctxt x (Bound 0))) |
1608 |> AList.group (op aconv) |
1608 |> AList.group (op aconv) |
1609 |> map (apsnd (List.foldl s_disj @{const False})) |
1609 |> map (apsnd (List.foldl s_disj @{const False})) |
1610 |> sort (int_ord o pairself (size_of_term o snd)) |
1610 |> sort (int_ord o apply2 (size_of_term o snd)) |
1611 |> rev |
1611 |> rev |
1612 in |
1612 in |
1613 if res_T = bool_T then |
1613 if res_T = bool_T then |
1614 if forall (member (op =) [@{const False}, @{const True}] o fst) cases then |
1614 if forall (member (op =) [@{const False}, @{const True}] o fst) cases then |
1615 case cases of |
1615 case cases of |
1725 (Inttab.lookup_list ground_thm_table (hash_term t1)) then |
1725 (Inttab.lookup_list ground_thm_table (hash_term t1)) then |
1726 do_term depth Ts t2 |
1726 do_term depth Ts t2 |
1727 else |
1727 else |
1728 do_const depth Ts t x [t1, t2, t3] |
1728 do_const depth Ts t x [t1, t2, t3] |
1729 | Const (@{const_name Let}, _) $ t1 $ t2 => |
1729 | Const (@{const_name Let}, _) $ t1 $ t2 => |
1730 s_betapply Ts (pairself (do_term depth Ts) (t2, t1)) |
1730 s_betapply Ts (apply2 (do_term depth Ts) (t2, t1)) |
1731 | Const x => do_const depth Ts t x [] |
1731 | Const x => do_const depth Ts t x [] |
1732 | t1 $ t2 => |
1732 | t1 $ t2 => |
1733 (case strip_comb t of |
1733 (case strip_comb t of |
1734 (Const x, ts) => do_const depth Ts t x ts |
1734 (Const x, ts) => do_const depth Ts t x ts |
1735 | _ => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)) |
1735 | _ => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)) |
1977 val thy = Proof_Context.theory_of ctxt |
1977 val thy = Proof_Context.theory_of ctxt |
1978 val abs_T = domain_type T |
1978 val abs_T = domain_type T |
1979 in |
1979 in |
1980 typedef_info ctxt (fst (dest_Type abs_T)) |> the |
1980 typedef_info ctxt (fst (dest_Type abs_T)) |> the |
1981 |> pairf #Abs_inverse #Rep_inverse |
1981 |> pairf #Abs_inverse #Rep_inverse |
1982 |> pairself (specialize_type thy x o prop_of o the) |
1982 |> apply2 (specialize_type thy x o prop_of o the) |
1983 ||> single |> op :: |
1983 ||> single |> op :: |
1984 end |
1984 end |
1985 |
1985 |
1986 fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) = |
1986 fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) = |
1987 let |
1987 let |
2087 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb |
2087 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb |
2088 |
2088 |
2089 fun wf_constraint_for rel side concl main = |
2089 fun wf_constraint_for rel side concl main = |
2090 let |
2090 let |
2091 val core = HOLogic.mk_mem (HOLogic.mk_prod |
2091 val core = HOLogic.mk_mem (HOLogic.mk_prod |
2092 (pairself tuple_for_args (main, concl)), Var rel) |
2092 (apply2 tuple_for_args (main, concl)), Var rel) |
2093 val t = List.foldl HOLogic.mk_imp core side |
2093 val t = List.foldl HOLogic.mk_imp core side |
2094 val vars = filter_out (curry (op =) rel) (Term.add_vars t []) |
2094 val vars = filter_out (curry (op =) rel) (Term.add_vars t []) |
2095 in |
2095 in |
2096 Library.foldl (fn (t', ((x, j), T)) => |
2096 Library.foldl (fn (t', ((x, j), T)) => |
2097 HOLogic.all_const T |
2097 HOLogic.all_const T |
2180 fold_rev (Term.abs o pair "c") arg_Ts |
2180 fold_rev (Term.abs o pair "c") arg_Ts |
2181 (incr_boundvars n t $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0))) |
2181 (incr_boundvars n t $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0))) |
2182 end |
2182 end |
2183 |
2183 |
2184 fun num_occs_of_bound_in_term j (t1 $ t2) = |
2184 fun num_occs_of_bound_in_term j (t1 $ t2) = |
2185 op + (pairself (num_occs_of_bound_in_term j) (t1, t2)) |
2185 op + (apply2 (num_occs_of_bound_in_term j) (t1, t2)) |
2186 | num_occs_of_bound_in_term j (Abs (_, _, t')) = |
2186 | num_occs_of_bound_in_term j (Abs (_, _, t')) = |
2187 num_occs_of_bound_in_term (j + 1) t' |
2187 num_occs_of_bound_in_term (j + 1) t' |
2188 | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0 |
2188 | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0 |
2189 | num_occs_of_bound_in_term _ _ = 0 |
2189 | num_occs_of_bound_in_term _ _ = 0 |
2190 |
2190 |
2395 SOME _ => I |
2395 SOME _ => I |
2396 | NONE => |
2396 | NONE => |
2397 filter_out (fn (S', _) => Sign.subsort thy (S, S')) |
2397 filter_out (fn (S', _) => Sign.subsort thy (S, S')) |
2398 #> cons (S, s)) |
2398 #> cons (S, s)) |
2399 val tfrees = [] |> fold Term.add_tfrees ts |
2399 val tfrees = [] |> fold Term.add_tfrees ts |
2400 |> sort (string_ord o pairself fst) |
2400 |> sort (string_ord o apply2 fst) |
2401 in [] |> fold add tfrees |> rev end |
2401 in [] |> fold add tfrees |> rev end |
2402 |
2402 |
2403 fun merge_type_vars_in_term thy merge_type_vars table = |
2403 fun merge_type_vars_in_term thy merge_type_vars table = |
2404 merge_type_vars |
2404 merge_type_vars |
2405 ? map_types (map_atyps |
2405 ? map_types (map_atyps |