--- a/doc-src/Nitpick/nitpick.tex Thu Feb 04 14:45:08 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Fri Feb 05 11:15:16 2010 +0100
@@ -1694,7 +1694,7 @@
``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
+{\slshape Nitpick found no counterexample.}
\postw
Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
@@ -1756,7 +1756,7 @@
\prew
\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
+{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
\postw
Insertion should transform the set of elements represented by the tree in the
@@ -1766,14 +1766,14 @@
\textbf{theorem} \textit{dataset\_insort}:\kern.4em
``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 5 of 8 scopes.}
+{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
\postw
-We could continue like this and sketch a complete theory of AA trees without
-performing a single proof. Once the definitions and main theorems are in place
-and have been thoroughly tested using Nitpick, we could start working on the
-proofs. Developing theories this way usually saves time, because faulty theorems
-and definitions are discovered much earlier in the process.
+We could continue like this and sketch a complete theory of AA trees. Once the
+definitions and main theorems are in place and have been thoroughly tested using
+Nitpick, we could start working on the proofs. Developing theories this way
+usually saves time, because faulty theorems and definitions are discovered much
+earlier in the process.
\section{Option Reference}
\label{option-reference}
--- a/src/HOL/IsaMakefile Thu Feb 04 14:45:08 2010 +0100
+++ b/src/HOL/IsaMakefile Fri Feb 05 11:15:16 2010 +0100
@@ -206,6 +206,7 @@
Tools/Nitpick/nitpick_mono.ML \
Tools/Nitpick/nitpick_nut.ML \
Tools/Nitpick/nitpick_peephole.ML \
+ Tools/Nitpick/nitpick_preproc.ML \
Tools/Nitpick/nitpick_rep.ML \
Tools/Nitpick/nitpick_scope.ML \
Tools/Nitpick/nitpick_tests.ML \
--- a/src/HOL/Nitpick.thy Thu Feb 04 14:45:08 2010 +0100
+++ b/src/HOL/Nitpick.thy Fri Feb 05 11:15:16 2010 +0100
@@ -13,6 +13,7 @@
("Tools/Nitpick/kodkod_sat.ML")
("Tools/Nitpick/nitpick_util.ML")
("Tools/Nitpick/nitpick_hol.ML")
+ ("Tools/Nitpick/nitpick_preproc.ML")
("Tools/Nitpick/nitpick_mono.ML")
("Tools/Nitpick/nitpick_scope.ML")
("Tools/Nitpick/nitpick_peephole.ML")
@@ -237,6 +238,7 @@
use "Tools/Nitpick/kodkod_sat.ML"
use "Tools/Nitpick/nitpick_util.ML"
use "Tools/Nitpick/nitpick_hol.ML"
+use "Tools/Nitpick/nitpick_preproc.ML"
use "Tools/Nitpick/nitpick_mono.ML"
use "Tools/Nitpick/nitpick_scope.ML"
use "Tools/Nitpick/nitpick_peephole.ML"
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Feb 04 14:45:08 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Feb 05 11:15:16 2010 +0100
@@ -16,7 +16,7 @@
val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1
val def_table = Nitpick_HOL.const_def_table @{context} defs
-val ext_ctxt : Nitpick_HOL.extended_context =
+val hol_ctxt : Nitpick_HOL.hol_context =
{thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
binary_ints = SOME false, destroy_constrs = false, specialize = false,
@@ -29,7 +29,7 @@
special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
(* term -> bool *)
-val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a}
+val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt @{typ 'a}
Nitpick_Mono.Plus [] []
fun is_const t =
let val T = fastype_of t in
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 04 14:45:08 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 05 11:15:16 2010 +0100
@@ -69,6 +69,7 @@
open Nitpick_Util
open Nitpick_HOL
+open Nitpick_Preproc
open Nitpick_Mono
open Nitpick_Scope
open Nitpick_Peephole
@@ -273,7 +274,7 @@
val intro_table = inductive_intro_table ctxt def_table
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table thy
- val (ext_ctxt as {wf_cache, ...}) =
+ val (hol_ctxt as {wf_cache, ...}) =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
binary_ints = binary_ints, destroy_constrs = destroy_constrs,
@@ -292,7 +293,7 @@
val _ = null (Term.add_tvars assms_t []) orelse
raise NOT_SUPPORTED "schematic type variables"
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
- core_t) = preprocess_term ext_ctxt assms_t
+ core_t) = preprocess_term hol_ctxt assms_t
val got_all_user_axioms =
got_all_mono_user_axioms andalso no_poly_user_axioms
@@ -319,9 +320,9 @@
handle TYPE (_, Ts, ts) =>
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
- val core_u = nut_from_term ext_ctxt Eq core_t
- val def_us = map (nut_from_term ext_ctxt DefEq) def_ts
- val nondef_us = map (nut_from_term ext_ctxt Eq) nondef_ts
+ val core_u = nut_from_term hol_ctxt Eq core_t
+ val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
+ val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
val (free_names, const_names) =
fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
val (sel_names, nonsel_names) =
@@ -344,12 +345,12 @@
case triple_lookup (type_match thy) monos T of
SOME (SOME b) => b
| _ => is_type_always_monotonic T orelse
- formulas_monotonic ext_ctxt T Plus def_ts nondef_ts core_t
+ formulas_monotonic hol_ctxt T Plus def_ts nondef_ts core_t
fun is_deep_datatype T =
is_datatype thy T andalso
(is_word_type T orelse
exists (curry (op =) T o domain_type o type_of) sel_names)
- val all_Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
+ val all_Ts = ground_types_in_terms hol_ctxt (core_t :: def_ts @ nondef_ts)
|> sort TermOrd.typ_ord
val _ = if verbose andalso binary_ints = SOME true andalso
exists (member (op =) [nat_T, int_T]) all_Ts then
@@ -522,7 +523,7 @@
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
- val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk
+ val dtype_axioms = declarative_axioms_for_datatypes hol_ctxt bits ofs kk
rel_table datatypes
val declarative_axioms = plain_axioms @ dtype_axioms
val univ_card = univ_card nat_card int_card main_j0
@@ -553,7 +554,7 @@
if loc = "Nitpick_Kodkod.check_arity" andalso
not (Typtab.is_empty ofs) then
problem_for_scope liberal
- {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
+ {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth,
datatypes = datatypes, ofs = Typtab.empty}
else if loc = "Nitpick.pick_them_nits_in_term.\
@@ -891,7 +892,7 @@
end
val (skipped, the_scopes) =
- all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
+ all_scopes hol_ctxt sym_break cards_assigns maxes_assigns iters_assigns
bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
val _ = if skipped > 0 then
print_m (fn () => "Too many scopes. Skipping " ^
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 04 14:45:08 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 05 11:15:16 2010 +0100
@@ -13,7 +13,7 @@
type unrolled = styp * styp
type wf_cache = (styp * (bool * bool)) list
- type extended_context = {
+ type hol_context = {
thy: theory,
ctxt: Proof.context,
max_bisim_depth: int,
@@ -46,12 +46,24 @@
wf_cache: wf_cache Unsynchronized.ref,
constr_cache: (typ * styp list) list Unsynchronized.ref}
+ datatype fixpoint_kind = Lfp | Gfp | NoFp
+ datatype boxability =
+ InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
+
val name_sep : string
val numeral_prefix : string
+ val ubfp_prefix : string
+ val lbfp_prefix : string
val skolem_prefix : string
+ val special_prefix : string
+ val uncurry_prefix : string
val eval_prefix : string
val original_name : string -> string
val s_conj : term * term -> term
+ val s_disj : term * term -> term
+ val strip_any_connective : term -> term list * term
+ val conjuncts_of : term -> term list
+ val disjuncts_of : term -> term list
val unbit_and_unbox_type : typ -> typ
val string_for_type : Proof.context -> typ -> string
val prefix_name : string -> string -> string
@@ -76,6 +88,7 @@
val is_record_type : typ -> bool
val is_number_type : theory -> typ -> bool
val const_for_iterator_type : typ -> styp
+ val strip_n_binders : int -> typ -> typ list * typ
val nth_range_type : int -> typ -> typ
val num_factors_in_type : typ -> int
val num_binder_types : typ -> int
@@ -96,15 +109,18 @@
val is_rep_fun : theory -> styp -> bool
val is_quot_abs_fun : Proof.context -> styp -> bool
val is_quot_rep_fun : Proof.context -> styp -> bool
+ val mate_of_rep_fun : theory -> styp -> styp
+ val is_constr_like : theory -> styp -> bool
+ val is_stale_constr : theory -> styp -> bool
val is_constr : theory -> styp -> bool
- val is_stale_constr : theory -> styp -> bool
val is_sel : string -> bool
val is_sel_like_and_no_discr : string -> bool
+ val box_type : hol_context -> boxability -> typ -> typ
val discr_for_constr : styp -> styp
val num_sels_for_constr_type : typ -> int
val nth_sel_name_for_constr_name : string -> int -> string
val nth_sel_for_constr : styp -> int -> styp
- val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp
+ val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
val sel_no_from_name : string -> int
val eta_expand : typ list -> term -> int -> term
val extensionalize : term -> term
@@ -113,19 +129,25 @@
val unregister_frac_type : string -> theory -> theory
val register_codatatype : typ -> string -> styp list -> theory -> theory
val unregister_codatatype : typ -> theory -> theory
- val datatype_constrs : extended_context -> typ -> styp list
- val boxed_datatype_constrs : extended_context -> typ -> styp list
- val num_datatype_constrs : extended_context -> typ -> int
+ val datatype_constrs : hol_context -> typ -> styp list
+ val boxed_datatype_constrs : hol_context -> typ -> styp list
+ val num_datatype_constrs : hol_context -> typ -> int
val constr_name_for_sel_like : string -> string
- val boxed_constr_for_sel : extended_context -> styp -> styp
+ val boxed_constr_for_sel : hol_context -> styp -> styp
+ val discriminate_value : hol_context -> styp -> term -> term
+ val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
+ val construct_value : theory -> styp -> term list -> term
val card_of_type : (typ * int) list -> typ -> int
val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
val bounded_exact_card_of_type :
- extended_context -> int -> int -> (typ * int) list -> typ -> int
- val is_finite_type : extended_context -> typ -> bool
+ hol_context -> int -> int -> (typ * int) list -> typ -> int
+ val is_finite_type : hol_context -> typ -> bool
+ val special_bounds : term list -> (indexname * typ) list
+ val is_funky_typedef : theory -> typ -> bool
val all_axioms_of : theory -> term list * term list * term list
val arity_of_built_in_const : bool -> styp -> int option
val is_built_in_const : bool -> styp -> bool
+ val term_under_def : term -> term
val case_const_names : theory -> (string * int) list
val const_def_table : Proof.context -> term list -> const_table
val const_nondef_table : term list -> const_table
@@ -134,22 +156,33 @@
val inductive_intro_table : Proof.context -> const_table -> const_table
val ground_theorem_table : theory -> term list Inttab.table
val ersatz_table : theory -> (string * string) list
+ val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
+ val inverse_axioms_for_rep_fun : theory -> styp -> term list
+ val optimized_typedef_axioms : theory -> string * typ list -> term list
+ val optimized_quot_type_axioms : theory -> string * typ list -> term list
val def_of_const : theory -> const_table -> styp -> term option
- val is_inductive_pred : extended_context -> styp -> bool
+ val fixpoint_kind_of_const :
+ theory -> const_table -> string * typ -> fixpoint_kind
+ val is_inductive_pred : hol_context -> styp -> bool
+ val is_equational_fun : hol_context -> styp -> bool
val is_constr_pattern_lhs : theory -> term -> bool
val is_constr_pattern_formula : theory -> term -> bool
+ val unfold_defs_in_term : hol_context -> term -> term
+ val codatatype_bisim_axioms : hol_context -> typ -> term list
+ val is_well_founded_inductive_pred : hol_context -> styp -> bool
+ val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
+ val equational_fun_axioms : hol_context -> styp -> term list
+ val is_equational_fun_surely_complete : hol_context -> styp -> bool
val merge_type_vars_in_terms : term list -> term list
- val ground_types_in_type : extended_context -> typ -> typ list
- val ground_types_in_terms : extended_context -> term list -> typ list
+ val ground_types_in_type : hol_context -> typ -> typ list
+ val ground_types_in_terms : hol_context -> term list -> typ list
val format_type : int list -> int list -> typ -> typ
val format_term_type :
theory -> const_table -> (term option * int list) list -> term -> typ
val user_friendly_const :
- extended_context -> string * string -> (term option * int list) list
+ hol_context -> string * string -> (term option * int list) list
-> styp -> term * typ
val assign_operator_for_const : styp -> string
- val preprocess_term :
- extended_context -> term -> ((term list * term list) * (bool * bool)) * term
end;
structure Nitpick_HOL : NITPICK_HOL =
@@ -162,7 +195,7 @@
type unrolled = styp * styp
type wf_cache = (styp * (bool * bool)) list
-type extended_context = {
+type hol_context = {
thy: theory,
ctxt: Proof.context,
max_bisim_depth: int,
@@ -195,6 +228,10 @@
wf_cache: wf_cache Unsynchronized.ref,
constr_cache: (typ * styp list) list Unsynchronized.ref}
+datatype fixpoint_kind = Lfp | Gfp | NoFp
+datatype boxability =
+ InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
+
structure Data = Theory_Data(
type T = {frac_types: (string * (string * string) list) list,
codatatypes: (string * (string * styp list)) list}
@@ -222,20 +259,11 @@
val special_prefix = nitpick_prefix ^ "sp"
val uncurry_prefix = nitpick_prefix ^ "unc"
val eval_prefix = nitpick_prefix ^ "eval"
-val bound_var_prefix = "b"
-val cong_var_prefix = "c"
val iter_var_prefix = "i"
-val val_var_prefix = nitpick_prefix ^ "v"
val arg_var_prefix = "x"
(* int -> string *)
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
-fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
-(* int -> int -> string *)
-fun skolem_prefix_for k j =
- skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
-fun uncurry_prefix_for k j =
- uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
(* string -> string * string *)
val strip_first_name_sep =
@@ -260,9 +288,6 @@
| s_disj (t1, t2) =
if t1 = @{const True} orelse t2 = @{const True} then @{const True}
else HOLogic.mk_disj (t1, t2)
-(* term -> term -> term *)
-fun mk_exists v t =
- HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
(* term -> term -> term list *)
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
@@ -276,8 +301,8 @@
([t], @{const Not})
| strip_any_connective t = ([t], @{const Not})
(* term -> term list *)
-val conjuncts = strip_connective @{const "op &"}
-val disjuncts = strip_connective @{const "op |"}
+val conjuncts_of = strip_connective @{const "op &"}
+val disjuncts_of = strip_connective @{const "op |"}
(* When you add constants to these lists, make sure to handle them in
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
@@ -373,8 +398,6 @@
fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
(* string -> term -> term *)
val prefix_abs_vars = Term.map_abs_vars o prefix_name
-(* term -> term *)
-val shorten_abs_vars = Term.map_abs_vars shortest_name
(* string -> string *)
fun short_name s =
case space_explode name_sep s of
@@ -441,7 +464,7 @@
| const_for_iterator_type T =
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
-(* int -> typ -> typ * typ *)
+(* int -> typ -> typ list * typ *)
fun strip_n_binders 0 T = ([], T)
| strip_n_binders n (Type ("fun", [T1, T2])) =
strip_n_binders (n - 1) T2 |>> cons T1
@@ -552,7 +575,7 @@
val is_real_datatype = is_some oo Datatype.get_info
(* theory -> typ -> bool *)
fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
- | is_quot_type _ (Type ("FSet.fset", _)) = true (* FIXME *)
+ | is_quot_type _ (Type ("FSet.fset", _)) = true
| is_quot_type _ _ = false
fun is_codatatype thy (T as Type (s, _)) =
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
@@ -619,11 +642,11 @@
| NONE => false)
| is_rep_fun _ _ = false
(* Proof.context -> styp -> bool *)
-fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* FIXME *)
- | is_quot_abs_fun _ ("FSet.abs_fset", _) = true (* FIXME *)
+fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true
+ | is_quot_abs_fun _ ("FSet.abs_fset", _) = true
| is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* FIXME *)
- | is_quot_rep_fun _ ("FSet.rep_fset", _) = true (* FIXME *)
+fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true
+ | is_quot_rep_fun _ ("FSet.rep_fset", _) = true
| is_quot_rep_fun _ _ = false
(* theory -> styp -> styp *)
@@ -682,9 +705,6 @@
String.isPrefix sel_prefix
orf (member (op =) [@{const_name fst}, @{const_name snd}])
-datatype boxability =
- InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
-
(* boxability -> boxability *)
fun in_fun_lhs_for InConstr = InSel
| in_fun_lhs_for _ = InFunLHS
@@ -693,8 +713,8 @@
| in_fun_rhs_for InFunRHS1 = InFunRHS2
| in_fun_rhs_for _ = InFunRHS1
-(* extended_context -> boxability -> typ -> bool *)
-fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
+(* hol_context -> boxability -> typ -> bool *)
+fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
case T of
Type ("fun", _) =>
(boxy = InPair orelse boxy = InFunLHS) andalso
@@ -702,31 +722,31 @@
| Type ("*", Ts) =>
boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
((boxy = InExpr orelse boxy = InFunLHS) andalso
- exists (is_boxing_worth_it ext_ctxt InPair)
- (map (box_type ext_ctxt InPair) Ts))
+ exists (is_boxing_worth_it hol_ctxt InPair)
+ (map (box_type hol_ctxt InPair) Ts))
| _ => false
-(* extended_context -> boxability -> string * typ list -> string *)
-and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
+(* hol_context -> boxability -> string * typ list -> string *)
+and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
case triple_lookup (type_match thy) boxes (Type z) of
SOME (SOME box_me) => box_me
- | _ => is_boxing_worth_it ext_ctxt boxy (Type z)
-(* extended_context -> boxability -> typ -> typ *)
-and box_type ext_ctxt boxy T =
+ | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
+(* hol_context -> boxability -> typ -> typ *)
+and box_type hol_ctxt boxy T =
case T of
Type (z as ("fun", [T1, T2])) =>
if boxy <> InConstr andalso boxy <> InSel andalso
- should_box_type ext_ctxt boxy z then
+ should_box_type hol_ctxt boxy z then
Type (@{type_name fun_box},
- [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
+ [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
else
- box_type ext_ctxt (in_fun_lhs_for boxy) T1
- --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
+ box_type hol_ctxt (in_fun_lhs_for boxy) T1
+ --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
| Type (z as ("*", Ts)) =>
if boxy <> InConstr andalso boxy <> InSel
- andalso should_box_type ext_ctxt boxy z then
- Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
+ andalso should_box_type hol_ctxt boxy z then
+ Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
else
- Type ("*", map (box_type ext_ctxt
+ Type ("*", map (box_type hol_ctxt
(if boxy = InConstr orelse boxy = InSel then boxy
else InPair)) Ts)
| _ => T
@@ -747,9 +767,9 @@
| nth_sel_for_constr (s, T) n =
(nth_sel_name_for_constr_name s n,
body_type T --> nth (maybe_curried_binder_types T) n)
-(* extended_context -> styp -> int -> styp *)
-fun boxed_nth_sel_for_constr ext_ctxt =
- apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr
+(* hol_context -> styp -> int -> styp *)
+fun boxed_nth_sel_for_constr hol_ctxt =
+ apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr
(* string -> int *)
fun sel_no_from_name s =
@@ -791,8 +811,8 @@
fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
fun suc_const T = Const (@{const_name Suc}, T --> T)
-(* extended_context -> typ -> styp list *)
-fun uncached_datatype_constrs ({thy, stds, ...} : extended_context)
+(* hol_context -> typ -> styp list *)
+fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
(T as Type (s, Ts)) =
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
@@ -829,49 +849,49 @@
else
[])
| uncached_datatype_constrs _ _ = []
-(* extended_context -> typ -> styp list *)
-fun datatype_constrs (ext_ctxt as {constr_cache, ...}) T =
+(* hol_context -> typ -> styp list *)
+fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
case AList.lookup (op =) (!constr_cache) T of
SOME xs => xs
| NONE =>
- let val xs = uncached_datatype_constrs ext_ctxt T in
+ let val xs = uncached_datatype_constrs hol_ctxt T in
(Unsynchronized.change constr_cache (cons (T, xs)); xs)
end
-fun boxed_datatype_constrs ext_ctxt =
- map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
-(* extended_context -> typ -> int *)
+fun boxed_datatype_constrs hol_ctxt =
+ map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
+(* hol_context -> typ -> int *)
val num_datatype_constrs = length oo datatype_constrs
(* string -> string *)
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
| constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
| constr_name_for_sel_like s' = original_name s'
-(* extended_context -> styp -> styp *)
-fun boxed_constr_for_sel ext_ctxt (s', T') =
+(* hol_context -> styp -> styp *)
+fun boxed_constr_for_sel hol_ctxt (s', T') =
let val s = constr_name_for_sel_like s' in
- AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
+ AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s
|> the |> pair s
end
-(* extended_context -> styp -> term *)
-fun discr_term_for_constr ext_ctxt (x as (s, T)) =
+(* hol_context -> styp -> term *)
+fun discr_term_for_constr hol_ctxt (x as (s, T)) =
let val dataT = body_type T in
if s = @{const_name Suc} then
Abs (Name.uu, dataT,
@{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
- else if num_datatype_constrs ext_ctxt dataT >= 2 then
+ else if num_datatype_constrs hol_ctxt dataT >= 2 then
Const (discr_for_constr x)
else
Abs (Name.uu, dataT, @{const True})
end
-(* extended_context -> styp -> term -> term *)
-fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
+(* hol_context -> styp -> term -> term *)
+fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t =
case strip_comb t of
(Const x', args) =>
if x = x' then @{const True}
else if is_constr_like thy x' then @{const False}
- else betapply (discr_term_for_constr ext_ctxt x, t)
- | _ => betapply (discr_term_for_constr ext_ctxt x, t)
+ else betapply (discr_term_for_constr hol_ctxt x, t)
+ | _ => betapply (discr_term_for_constr hol_ctxt x, t)
(* styp -> term -> term *)
fun nth_arg_sel_term_for_constr (x as (s, T)) n =
@@ -920,26 +940,6 @@
| _ => list_comb (Const x, args)
end
-(* extended_context -> typ -> term -> term *)
-fun constr_expand (ext_ctxt as {thy, ...}) T t =
- (case head_of t of
- Const x => if is_constr_like thy x then t else raise SAME ()
- | _ => raise SAME ())
- handle SAME () =>
- let
- val x' as (_, T') =
- if is_pair_type T then
- let val (T1, T2) = HOLogic.dest_prodT T in
- (@{const_name Pair}, T1 --> T2 --> T)
- end
- else
- datatype_constrs ext_ctxt T |> hd
- val arg_Ts = binder_types T'
- in
- list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
- (index_seq 0 (length arg_Ts)) arg_Ts)
- end
-
(* (typ * int) list -> typ -> int *)
fun card_of_type assigns (Type ("fun", [T1, T2])) =
reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
@@ -975,8 +975,8 @@
card_of_type assigns T
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
default_card)
-(* extended_context -> int -> (typ * int) list -> typ -> int *)
-fun bounded_exact_card_of_type ext_ctxt max default_card assigns T =
+(* hol_context -> int -> (typ * int) list -> typ -> int *)
+fun bounded_exact_card_of_type hol_ctxt max default_card assigns T =
let
(* typ list -> typ -> int *)
fun aux avoid T =
@@ -1006,13 +1006,13 @@
| @{typ bool} => 2
| @{typ unit} => 1
| Type _ =>
- (case datatype_constrs ext_ctxt T of
+ (case datatype_constrs hol_ctxt T of
[] => if is_integer_type T orelse is_bit_type T then 0
else raise SAME ()
| constrs =>
let
val constr_cards =
- datatype_constrs ext_ctxt T
+ datatype_constrs hol_ctxt T
|> map (Integer.prod o map (aux (T :: avoid)) o binder_types
o snd)
in
@@ -1024,9 +1024,9 @@
AList.lookup (op =) assigns T |> the_default default_card
in Int.min (max, aux [] T) end
-(* extended_context -> typ -> bool *)
-fun is_finite_type ext_ctxt =
- not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 []
+(* hol_context -> typ -> bool *)
+fun is_finite_type hol_ctxt =
+ not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
(* term -> bool *)
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
@@ -1052,7 +1052,7 @@
member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
@{type_name int}] s orelse
is_frac_type thy (Type (s, []))
-(* theory -> term -> bool *)
+(* theory -> typ -> bool *)
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
| is_funky_typedef _ _ = false
(* term -> bool *)
@@ -1199,8 +1199,6 @@
|> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
handle List.Empty => NONE
-datatype fixpoint_kind = Lfp | Gfp | NoFp
-
(* term -> fixpoint_kind *)
fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
| fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
@@ -1299,35 +1297,6 @@
Unsynchronized.change simp_table
(Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
-(* Similar to "Refute.specialize_type" but returns all matches rather than only
- the first (preorder) match. *)
-(* theory -> styp -> term -> term list *)
-fun multi_specialize_type thy slack (x as (s, T)) t =
- let
- (* term -> (typ * term) list -> (typ * term) list *)
- fun aux (Const (s', T')) ys =
- if s = s' then
- ys |> (if AList.defined (op =) ys T' then
- I
- else
- cons (T', Refute.monomorphic_term
- (Sign.typ_match thy (T', T) Vartab.empty) t)
- handle Type.TYPE_MATCH => I
- | Refute.REFUTE _ =>
- if slack then
- I
- else
- raise NOT_SUPPORTED ("too much polymorphism in \
- \axiom involving " ^ quote s))
- else
- ys
- | aux _ ys = ys
- in map snd (fold_aterms aux t []) end
-
-(* theory -> bool -> const_table -> styp -> term list *)
-fun nondef_props_for_const thy slack table (x as (s, _)) =
- these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
-
(* theory -> styp -> term list *)
fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
let val abs_T = domain_type T in
@@ -1336,7 +1305,7 @@
|> pairself (Refute.specialize_type thy x o prop_of o the)
||> single |> op ::
end
-(* theory -> styp list -> term list *)
+(* theory -> string * typ list -> term list *)
fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
let val abs_T = Type abs_z in
if is_univ_typedef thy abs_T then
@@ -1392,15 +1361,15 @@
list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
(index_seq 0 (length arg_Ts)) arg_Ts)
end
-(* extended_context -> typ -> int * styp -> term -> term *)
-fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
+(* hol_context -> typ -> int * styp -> term -> term *)
+fun add_constr_case (hol_ctxt as {thy, ...}) res_T (j, x) res_t =
Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
- $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
+ $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy (j, x)
$ res_t
-(* extended_context -> typ -> typ -> term *)
-fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
+(* hol_context -> typ -> typ -> term *)
+fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
let
- val xs = datatype_constrs ext_ctxt dataT
+ val xs = datatype_constrs hol_ctxt dataT
val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
in
@@ -1409,19 +1378,19 @@
val (xs'', x) = split_last xs'
in
constr_case_body thy (1, x)
- |> fold_rev (add_constr_case ext_ctxt res_T)
+ |> fold_rev (add_constr_case hol_ctxt res_T)
(length xs' downto 2 ~~ xs'')
end
else
Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
- |> fold_rev (add_constr_case ext_ctxt res_T)
+ |> fold_rev (add_constr_case hol_ctxt res_T)
(length xs' downto 1 ~~ xs'))
|> fold_rev (curry absdummy) (func_Ts @ [dataT])
end
-(* extended_context -> string -> typ -> typ -> term -> term *)
-fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
- let val constr_x = hd (datatype_constrs ext_ctxt rec_T) in
+(* hol_context -> string -> typ -> typ -> term -> term *)
+fun optimized_record_get (hol_ctxt as {thy, ...}) s rec_T res_T t =
+ let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
case no_of_record_field thy s rec_T of
~1 => (case rec_T of
Type (_, Ts as _ :: _) =>
@@ -1430,16 +1399,16 @@
val j = num_record_fields thy rec_T - 1
in
select_nth_constr_arg thy constr_x t j res_T
- |> optimized_record_get ext_ctxt s rec_T' res_T
+ |> optimized_record_get hol_ctxt s rec_T' res_T
end
| _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
[]))
| j => select_nth_constr_arg thy constr_x t j res_T
end
-(* extended_context -> string -> typ -> term -> term -> term *)
-fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
+(* hol_context -> string -> typ -> term -> term -> term *)
+fun optimized_record_update (hol_ctxt as {thy, ...}) s rec_T fun_t rec_t =
let
- val constr_x as (_, constr_T) = hd (datatype_constrs ext_ctxt rec_T)
+ val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
val Ts = binder_types constr_T
val n = length Ts
val special_j = no_of_record_field thy s rec_T
@@ -1450,7 +1419,7 @@
if j = special_j then
betapply (fun_t, t)
else if j = n - 1 andalso special_j = ~1 then
- optimized_record_update ext_ctxt s
+ optimized_record_update hol_ctxt s
(rec_T |> dest_Type |> snd |> List.last) fun_t t
else
t
@@ -1473,19 +1442,19 @@
fixpoint_kind_of_rhs (the (def_of_const thy table x))
handle Option.Option => NoFp
-(* extended_context -> styp -> bool *)
+(* hol_context -> styp -> bool *)
fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
- : extended_context) x =
+ : hol_context) x =
not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
fixpoint_kind_of_const thy def_table x <> NoFp
fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
- : extended_context) x =
+ : hol_context) x =
exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
[!simp_table, psimp_table]
-fun is_inductive_pred ext_ctxt =
- is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)
-fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =
- (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
+fun is_inductive_pred hol_ctxt =
+ is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
+fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
+ (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
andf (not o has_trivial_definition thy def_table)
@@ -1522,11 +1491,11 @@
SOME t' => is_constr_pattern_lhs thy t'
| NONE => false
+(* Prevents divergence in case of cyclic or infinite definition dependencies. *)
val unfold_max_depth = 255
-val axioms_max_depth = 255
-(* extended_context -> term -> term *)
-fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
+(* hol_context -> term -> term *)
+fun unfold_defs_in_term (hol_ctxt as {thy, destroy_constrs, fast_descrs,
case_names, def_table, ground_thm_table,
ersatz_table, ...}) =
let
@@ -1600,7 +1569,7 @@
val (dataT, res_T) = nth_range_type n T
|> pairf domain_type range_type
in
- (optimized_case_def ext_ctxt dataT res_T
+ (optimized_case_def hol_ctxt dataT res_T
|> do_term (depth + 1) Ts, ts)
end
| _ =>
@@ -1628,11 +1597,11 @@
else if is_record_get thy x then
case length ts of
0 => (do_term depth Ts (eta_expand Ts t 1), [])
- | _ => (optimized_record_get ext_ctxt s (domain_type T)
+ | _ => (optimized_record_get hol_ctxt s (domain_type T)
(range_type T) (do_term depth Ts (hd ts)), tl ts)
else if is_record_update thy x then
case length ts of
- 2 => (optimized_record_update ext_ctxt
+ 2 => (optimized_record_update hol_ctxt
(unsuffix Record.updateN s) (nth_range_type 2 T)
(do_term depth Ts (hd ts))
(do_term depth Ts (nth ts 1)), [])
@@ -1645,7 +1614,7 @@
else
(Const x, ts)
end
- else if is_equational_fun ext_ctxt x then
+ else if is_equational_fun hol_ctxt x then
(Const x, ts)
else case def_of_const thy def_table x of
SOME def =>
@@ -1662,10 +1631,10 @@
in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
in do_term 0 [] end
-(* extended_context -> typ -> term list *)
-fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
+(* hol_context -> typ -> term list *)
+fun codatatype_bisim_axioms (hol_ctxt as {thy, ...}) T =
let
- val xs = datatype_constrs ext_ctxt T
+ val xs = datatype_constrs hol_ctxt T
val set_T = T --> bool_T
val iter_T = @{typ bisim_iterator}
val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
@@ -1688,14 +1657,14 @@
let
val arg_Ts = binder_types T
val core_t =
- discriminate_value ext_ctxt x y_var ::
+ discriminate_value hol_ctxt x y_var ::
map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
|> foldr1 s_conj
in List.foldr absdummy core_t arg_Ts end
in
[HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
$ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
- $ (betapplys (optimized_case_def ext_ctxt T bool_T,
+ $ (betapplys (optimized_case_def hol_ctxt T bool_T,
map case_func xs @ [x_var]))),
HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
$ (Const (@{const_name insert}, T --> set_T --> set_T)
@@ -1754,10 +1723,10 @@
val termination_tacs = [Lexicographic_Order.lex_order_tac true,
ScnpReconstruct.sizechange_tac]
-(* extended_context -> const_table -> styp -> bool *)
+(* hol_context -> const_table -> styp -> bool *)
fun uncached_is_well_founded_inductive_pred
({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
- : extended_context) (x as (_, T)) =
+ : hol_context) (x as (_, T)) =
case def_props_for_const thy fast_descrs intro_table x of
[] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
[Const x])
@@ -1797,11 +1766,11 @@
handle List.Empty => false
| NO_TRIPLE () => false
-(* The type constraint below is a workaround for a Poly/ML bug. *)
+(* The type constraint below is a workaround for a Poly/ML crash. *)
-(* extended_context -> styp -> bool *)
+(* hol_context -> styp -> bool *)
fun is_well_founded_inductive_pred
- (ext_ctxt as {thy, wfs, def_table, wf_cache, ...} : extended_context)
+ (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
(x as (s, _)) =
case triple_lookup (const_match thy) wfs x of
SOME (SOME b) => b
@@ -1811,7 +1780,7 @@
| NONE =>
let
val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
- val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
+ val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
in
Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
end
@@ -1842,14 +1811,14 @@
| do_disjunct j t =
case num_occs_of_bound_in_term j t of
0 => true
- | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t)
+ | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
| _ => false
(* term -> bool *)
fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
let val (xs, body) = strip_abs t2 in
case length xs of
1 => false
- | n => forall (do_disjunct (n - 1)) (disjuncts body)
+ | n => forall (do_disjunct (n - 1)) (disjuncts_of body)
end
| do_lfp_def _ = false
in do_lfp_def o strip_abs_body end
@@ -1887,7 +1856,7 @@
end
val (nonrecs, recs) =
List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
- (disjuncts body)
+ (disjuncts_of body)
val base_body = nonrecs |> List.foldl s_disj @{const False}
val step_body = recs |> map (repair_rec j)
|> List.foldl s_disj @{const False}
@@ -1901,8 +1870,8 @@
raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
in aux end
-(* extended_context -> styp -> term -> term *)
-fun starred_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T))
+(* hol_context -> styp -> term -> term *)
+fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (x as (s, T))
def =
let
val j = maxidx_of_term def + 1
@@ -1933,11 +1902,11 @@
$ list_comb (Const step_x, outer_bounds)))
$ list_comb (Const base_x, outer_bounds)
|> ap_curry tuple_arg_Ts tuple_T bool_T)
- |> unfold_defs_in_term ext_ctxt
+ |> unfold_defs_in_term hol_ctxt
end
-(* extended_context -> bool -> styp -> term *)
-fun unrolled_inductive_pred_const (ext_ctxt as {thy, star_linear_preds,
+(* hol_context -> bool -> styp -> term *)
+fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
def_table, simp_table, ...})
gfp (x as (s, T)) =
let
@@ -1946,11 +1915,11 @@
val unrolled_const = Const x' $ zero_const iter_T
val def = the (def_of_const thy def_table x)
in
- if is_equational_fun ext_ctxt x' then
+ if is_equational_fun hol_ctxt x' then
unrolled_const (* already done *)
else if not gfp andalso is_linear_inductive_pred_def def andalso
star_linear_preds then
- starred_linear_pred_const ext_ctxt x def
+ starred_linear_pred_const hol_ctxt x def
else
let
val j = maxidx_of_term def + 1
@@ -1973,8 +1942,8 @@
in unrolled_const end
end
-(* extended_context -> styp -> term *)
-fun raw_inductive_pred_axiom ({thy, def_table, ...} : extended_context) x =
+(* hol_context -> styp -> term *)
+fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
let
val def = the (def_of_const thy def_table x)
val (outer, fp_app) = strip_abs def
@@ -1992,24 +1961,29 @@
HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
|> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
end
-fun inductive_pred_axiom ext_ctxt (x as (s, T)) =
+fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
let val x' = (after_name_sep s, T) in
- raw_inductive_pred_axiom ext_ctxt x' |> subst_atomic [(Const x', Const x)]
+ raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)]
end
else
- raw_inductive_pred_axiom ext_ctxt x
+ raw_inductive_pred_axiom hol_ctxt x
-(* extended_context -> styp -> term list *)
-fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
+(* hol_context -> styp -> term list *)
+fun raw_equational_fun_axioms (hol_ctxt as {thy, fast_descrs, simp_table,
psimp_table, ...}) (x as (s, _)) =
case def_props_for_const thy fast_descrs (!simp_table) x of
[] => (case def_props_for_const thy fast_descrs psimp_table x of
- [] => [inductive_pred_axiom ext_ctxt x]
+ [] => [inductive_pred_axiom hol_ctxt x]
| psimps => psimps)
| simps => simps
-
val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
+(* hol_context -> styp -> bool *)
+fun is_equational_fun_surely_complete hol_ctxt x =
+ case raw_equational_fun_axioms hol_ctxt x of
+ [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
+ strip_comb t1 |> snd |> forall is_Var
+ | _ => false
(* term list -> term list *)
fun merge_type_vars_in_terms ts =
@@ -2028,1261 +2002,27 @@
| coalesce T = T
in map (map_types (map_atyps coalesce)) ts end
-(* extended_context -> typ -> typ list -> typ list *)
-fun add_ground_types ext_ctxt T accum =
+(* hol_context -> typ -> typ list -> typ list *)
+fun add_ground_types hol_ctxt T accum =
case T of
- Type ("fun", Ts) => fold (add_ground_types ext_ctxt) Ts accum
- | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
- | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
+ Type ("fun", Ts) => fold (add_ground_types hol_ctxt) Ts accum
+ | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
+ | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
| Type (_, Ts) =>
if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
accum
else
T :: accum
- |> fold (add_ground_types ext_ctxt)
- (case boxed_datatype_constrs ext_ctxt T of
+ |> fold (add_ground_types hol_ctxt)
+ (case boxed_datatype_constrs hol_ctxt T of
[] => Ts
| xs => map snd xs)
| _ => insert (op =) T accum
-(* extended_context -> typ -> typ list *)
-fun ground_types_in_type ext_ctxt T = add_ground_types ext_ctxt T []
-(* extended_context -> term list -> typ list *)
-fun ground_types_in_terms ext_ctxt ts =
- fold (fold_types (add_ground_types ext_ctxt)) ts []
-
-(* typ list -> int -> term -> bool *)
-fun has_heavy_bounds_or_vars Ts level t =
- let
- (* typ list -> bool *)
- fun aux [] = false
- | aux [T] = is_fun_type T orelse is_pair_type T
- | aux _ = true
- in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
-
-(* typ list -> int -> int -> int -> term -> term *)
-fun fresh_value_var Ts k n j t =
- Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
-
-(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
- -> term * term list *)
-fun pull_out_constr_comb thy Ts relax k level t args seen =
- let val t_comb = list_comb (t, args) in
- case t of
- Const x =>
- if not relax andalso is_constr thy x andalso
- not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
- has_heavy_bounds_or_vars Ts level t_comb andalso
- not (loose_bvar (t_comb, level)) then
- let
- val (j, seen) = case find_index (curry (op =) t_comb) seen of
- ~1 => (0, t_comb :: seen)
- | j => (j, seen)
- in (fresh_value_var Ts k (length seen) j t_comb, seen) end
- else
- (t_comb, seen)
- | _ => (t_comb, seen)
- end
-
-(* (term -> term) -> typ list -> int -> term list -> term list *)
-fun equations_for_pulled_out_constrs mk_eq Ts k seen =
- let val n = length seen in
- map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
- (index_seq 0 n) seen
- end
-
-(* theory -> bool -> term -> term *)
-fun pull_out_universal_constrs thy def t =
- let
- val k = maxidx_of_term t + 1
- (* typ list -> bool -> term -> term list -> term list -> term * term list *)
- fun do_term Ts def t args seen =
- case t of
- (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
- do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as @{const "==>"}) $ t1 $ t2 =>
- if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
- | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
- do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as @{const "op -->"}) $ t1 $ t2 =>
- do_eq_or_imp Ts false def t0 t1 t2 seen
- | Abs (s, T, t') =>
- let val (t', seen) = do_term (T :: Ts) def t' [] seen in
- (list_comb (Abs (s, T, t'), args), seen)
- end
- | t1 $ t2 =>
- let val (t2, seen) = do_term Ts def t2 [] seen in
- do_term Ts def t1 (t2 :: args) seen
- end
- | _ => pull_out_constr_comb thy Ts def k 0 t args seen
- (* typ list -> bool -> bool -> term -> term -> term -> term list
- -> term * term list *)
- and do_eq_or_imp Ts eq def t0 t1 t2 seen =
- let
- val (t2, seen) = if eq andalso def then (t2, seen)
- else do_term Ts false t2 [] seen
- val (t1, seen) = do_term Ts false t1 [] seen
- in (t0 $ t1 $ t2, seen) end
- val (concl, seen) = do_term [] def t [] []
- in
- Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
- seen, concl)
- end
-
-(* extended_context -> bool -> term -> term *)
-fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
- let
- (* styp -> int *)
- val num_occs_of_var =
- fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
- | _ => I) t (K 0)
- (* bool -> term -> term *)
- fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
- aux_eq careful true t0 t1 t2
- | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
- t0 $ aux false t1 $ aux careful t2
- | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
- aux_eq careful true t0 t1 t2
- | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
- t0 $ aux false t1 $ aux careful t2
- | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
- | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
- | aux _ t = t
- (* bool -> bool -> term -> term -> term -> term *)
- and aux_eq careful pass1 t0 t1 t2 =
- ((if careful then
- raise SAME ()
- else if axiom andalso is_Var t2 andalso
- num_occs_of_var (dest_Var t2) = 1 then
- @{const True}
- else case strip_comb t2 of
- (* The first case is not as general as it could be. *)
- (Const (@{const_name PairBox}, _),
- [Const (@{const_name fst}, _) $ Var z1,
- Const (@{const_name snd}, _) $ Var z2]) =>
- if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
- else raise SAME ()
- | (Const (x as (s, T)), args) =>
- let val arg_Ts = binder_types T in
- if length arg_Ts = length args andalso
- (is_constr thy x orelse s = @{const_name Pair} orelse
- x = (@{const_name Suc}, nat_T --> nat_T)) andalso
- (not careful orelse not (is_Var t1) orelse
- String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
- discriminate_value ext_ctxt x t1 ::
- map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
- |> foldr1 s_conj
- else
- raise SAME ()
- end
- | _ => raise SAME ())
- |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
- handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
- else t0 $ aux false t2 $ aux false t1
- (* styp -> term -> int -> typ -> term -> term *)
- and sel_eq x t n nth_T nth_t =
- HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
- |> aux false
- in aux axiom t end
-
-(* theory -> term -> term *)
-fun simplify_constrs_and_sels thy t =
- let
- (* term -> int -> term *)
- fun is_nth_sel_on t' n (Const (s, _) $ t) =
- (t = t' andalso is_sel_like_and_no_discr s andalso
- sel_no_from_name s = n)
- | is_nth_sel_on _ _ _ = false
- (* term -> term list -> term *)
- fun do_term (Const (@{const_name Rep_Frac}, _)
- $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
- | do_term (Const (@{const_name Abs_Frac}, _)
- $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
- | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
- | do_term (t as Const (x as (s, T))) (args as _ :: _) =
- ((if is_constr_like thy x then
- if length args = num_binder_types T then
- case hd args of
- Const (x' as (_, T')) $ t' =>
- if domain_type T' = body_type T andalso
- forall (uncurry (is_nth_sel_on t'))
- (index_seq 0 (length args) ~~ args) then
- t'
- else
- raise SAME ()
- | _ => raise SAME ()
- else
- raise SAME ()
- else if is_sel_like_and_no_discr s then
- case strip_comb (hd args) of
- (Const (x' as (s', T')), ts') =>
- if is_constr_like thy x' andalso
- constr_name_for_sel_like s = s' andalso
- not (exists is_pair_type (binder_types T')) then
- list_comb (nth ts' (sel_no_from_name s), tl args)
- else
- raise SAME ()
- | _ => raise SAME ()
- else
- raise SAME ())
- handle SAME () => betapplys (t, args))
- | do_term (Abs (s, T, t')) args =
- betapplys (Abs (s, T, do_term t' []), args)
- | do_term t args = betapplys (t, args)
- in do_term t [] end
-
-(* term -> term *)
-fun curry_assms (@{const "==>"} $ (@{const Trueprop}
- $ (@{const "op &"} $ t1 $ t2)) $ t3) =
- curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
- | curry_assms (@{const "==>"} $ t1 $ t2) =
- @{const "==>"} $ curry_assms t1 $ curry_assms t2
- | curry_assms t = t
-
-(* term -> term *)
-val destroy_universal_equalities =
- let
- (* term list -> (indexname * typ) list -> term -> term *)
- fun aux prems zs t =
- case t of
- @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
- | _ => Logic.list_implies (rev prems, t)
- (* term list -> (indexname * typ) list -> term -> term -> term *)
- and aux_implies prems zs t1 t2 =
- case t1 of
- Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
- | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
- aux_eq prems zs z t' t1 t2
- | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
- aux_eq prems zs z t' t1 t2
- | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
- (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
- -> term -> term *)
- and aux_eq prems zs z t' t1 t2 =
- if not (member (op =) zs z) andalso
- not (exists_subterm (curry (op =) (Var z)) t') then
- aux prems zs (subst_free [(Var z, t')] t2)
- else
- aux (t1 :: prems) (Term.add_vars t1 zs) t2
- in aux [] [] end
-
-(* theory -> term -> term *)
-fun pull_out_existential_constrs thy t =
- let
- val k = maxidx_of_term t + 1
- (* typ list -> int -> term -> term list -> term list -> term * term list *)
- fun aux Ts num_exists t args seen =
- case t of
- (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
- let
- val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
- val n = length seen'
- (* unit -> term list *)
- fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
- in
- (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
- |> List.foldl s_conj t1 |> fold mk_exists (vars ())
- |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
- end
- | t1 $ t2 =>
- let val (t2, seen) = aux Ts num_exists t2 [] seen in
- aux Ts num_exists t1 (t2 :: args) seen
- end
- | Abs (s, T, t') =>
- let
- val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
- in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
- | _ =>
- if num_exists > 0 then
- pull_out_constr_comb thy Ts false k num_exists t args seen
- else
- (list_comb (t, args), seen)
- in aux [] 0 t [] [] |> fst end
-
-(* theory -> int -> term list -> term list -> (term * term list) option *)
-fun find_bound_assign _ _ _ [] = NONE
- | find_bound_assign thy j seen (t :: ts) =
- let
- (* bool -> term -> term -> (term * term list) option *)
- fun aux pass1 t1 t2 =
- (if loose_bvar1 (t2, j) then
- if pass1 then aux false t2 t1 else raise SAME ()
- else case t1 of
- Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
- | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
- if j' = j andalso s = sel_prefix_for 0 ^ @{const_name FunBox} then
- SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
- ts @ seen)
- else
- raise SAME ()
- | _ => raise SAME ())
- handle SAME () => find_bound_assign thy j (t :: seen) ts
- in
- case t of
- Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
- | _ => find_bound_assign thy j (t :: seen) ts
- end
-
-(* int -> term -> term -> term *)
-fun subst_one_bound j arg t =
- let
- fun aux (Bound i, lev) =
- if i < lev then raise SAME ()
- else if i = lev then incr_boundvars (lev - j) arg
- else Bound (i - 1)
- | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
- | aux (f $ t, lev) =
- (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
- handle SAME () => f $ aux (t, lev))
- | aux _ = raise SAME ()
- in aux (t, j) handle SAME () => t end
-
-(* theory -> term -> term *)
-fun destroy_existential_equalities thy =
- let
- (* string list -> typ list -> term list -> term *)
- fun kill [] [] ts = foldr1 s_conj ts
- | kill (s :: ss) (T :: Ts) ts =
- (case find_bound_assign thy (length ss) [] ts of
- SOME (_, []) => @{const True}
- | SOME (arg_t, ts) =>
- kill ss Ts (map (subst_one_bound (length ss)
- (incr_bv (~1, length ss + 1, arg_t))) ts)
- | NONE =>
- Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
- $ Abs (s, T, kill ss Ts ts))
- | kill _ _ _ = raise UnequalLengths
- (* string list -> typ list -> term -> term *)
- fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
- gather (ss @ [s1]) (Ts @ [T1]) t1
- | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
- | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
- | gather [] [] t = t
- | gather ss Ts t = kill ss Ts (conjuncts (gather [] [] t))
- in gather [] [] end
-
-(* term -> term *)
-fun distribute_quantifiers t =
- case t of
- (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
- (case t1 of
- (t10 as @{const "op &"}) $ t11 $ t12 =>
- t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
- $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as @{const Not}) $ t11 =>
- t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
- $ Abs (s, T1, t11))
- | t1 =>
- if not (loose_bvar1 (t1, 0)) then
- distribute_quantifiers (incr_boundvars ~1 t1)
- else
- t0 $ Abs (s, T1, distribute_quantifiers t1))
- | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
- (case distribute_quantifiers t1 of
- (t10 as @{const "op |"}) $ t11 $ t12 =>
- t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
- $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as @{const "op -->"}) $ t11 $ t12 =>
- t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
- $ Abs (s, T1, t11))
- $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as @{const Not}) $ t11 =>
- t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
- $ Abs (s, T1, t11))
- | t1 =>
- if not (loose_bvar1 (t1, 0)) then
- distribute_quantifiers (incr_boundvars ~1 t1)
- else
- t0 $ Abs (s, T1, distribute_quantifiers t1))
- | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
- | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
- | _ => t
-
-(* int -> int -> (int -> int) -> term -> term *)
-fun renumber_bounds j n f t =
- case t of
- t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
- | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
- | Bound j' =>
- Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
- | _ => t
-
-val quantifier_cluster_threshold = 7
-
-(* theory -> term -> term *)
-fun push_quantifiers_inward thy =
- let
- (* string -> string list -> typ list -> term -> term *)
- fun aux quant_s ss Ts t =
- (case t of
- (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
- if s0 = quant_s then
- aux s0 (s1 :: ss) (T1 :: Ts) t1
- else if quant_s = "" andalso
- (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
- aux s0 [s1] [T1] t1
- else
- raise SAME ()
- | _ => raise SAME ())
- handle SAME () =>
- case t of
- t1 $ t2 =>
- if quant_s = "" then
- aux "" [] [] t1 $ aux "" [] [] t2
- else
- let
- val typical_card = 4
- (* ('a -> ''b list) -> 'a list -> ''b list *)
- fun big_union proj ps =
- fold (fold (insert (op =)) o proj) ps []
- val (ts, connective) = strip_any_connective t
- val T_costs =
- map (bounded_card_of_type 65536 typical_card []) Ts
- val t_costs = map size_of_term ts
- val num_Ts = length Ts
- (* int -> int *)
- val flip = curry (op -) (num_Ts - 1)
- val t_boundss = map (map flip o loose_bnos) ts
- (* (int list * int) list -> int list
- -> (int list * int) list *)
- fun merge costly_boundss [] = costly_boundss
- | merge costly_boundss (j :: js) =
- let
- val (yeas, nays) =
- List.partition (fn (bounds, _) =>
- member (op =) bounds j)
- costly_boundss
- val yeas_bounds = big_union fst yeas
- val yeas_cost = Integer.sum (map snd yeas)
- * nth T_costs j
- in merge ((yeas_bounds, yeas_cost) :: nays) js end
- (* (int list * int) list -> int list -> int *)
- val cost = Integer.sum o map snd oo merge
- (* Inspired by Claessen & Sörensson's polynomial binary
- splitting heuristic (p. 5 of their MODEL 2003 paper). *)
- (* (int list * int) list -> int list -> int list *)
- fun heuristically_best_permutation _ [] = []
- | heuristically_best_permutation costly_boundss js =
- let
- val (costly_boundss, (j, js)) =
- js |> map (`(merge costly_boundss o single))
- |> sort (int_ord
- o pairself (Integer.sum o map snd o fst))
- |> split_list |>> hd ||> pairf hd tl
- in
- j :: heuristically_best_permutation costly_boundss js
- end
- val js =
- if length Ts <= quantifier_cluster_threshold then
- all_permutations (index_seq 0 num_Ts)
- |> map (`(cost (t_boundss ~~ t_costs)))
- |> sort (int_ord o pairself fst) |> hd |> snd
- else
- heuristically_best_permutation (t_boundss ~~ t_costs)
- (index_seq 0 num_Ts)
- val back_js = map (fn j => find_index (curry (op =) j) js)
- (index_seq 0 num_Ts)
- val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
- ts
- (* (term * int list) list -> term *)
- fun mk_connection [] =
- raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
- \mk_connection", "")
- | mk_connection ts_cum_bounds =
- ts_cum_bounds |> map fst
- |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
- (* (term * int list) list -> int list -> term *)
- fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
- | build ts_cum_bounds (j :: js) =
- let
- val (yeas, nays) =
- List.partition (fn (_, bounds) =>
- member (op =) bounds j)
- ts_cum_bounds
- ||> map (apfst (incr_boundvars ~1))
- in
- if null yeas then
- build nays js
- else
- let val T = nth Ts (flip j) in
- build ((Const (quant_s, (T --> bool_T) --> bool_T)
- $ Abs (nth ss (flip j), T,
- mk_connection yeas),
- big_union snd yeas) :: nays) js
- end
- end
- in build (ts ~~ t_boundss) js end
- | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
- | _ => t
- in aux "" [] [] end
-
-(* polarity -> string -> bool *)
-fun is_positive_existential polar quant_s =
- (polar = Pos andalso quant_s = @{const_name Ex}) orelse
- (polar = Neg andalso quant_s <> @{const_name Ex})
-
-(* extended_context -> int -> term -> term *)
-fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
- skolem_depth =
- let
- (* int list -> int list *)
- val incrs = map (Integer.add 1)
- (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
- fun aux ss Ts js depth polar t =
- let
- (* string -> typ -> string -> typ -> term -> term *)
- fun do_quantifier quant_s quant_T abs_s abs_T t =
- if not (loose_bvar1 (t, 0)) then
- aux ss Ts js depth polar (incr_boundvars ~1 t)
- else if depth <= skolem_depth andalso
- is_positive_existential polar quant_s then
- let
- val j = length (!skolems) + 1
- val sko_s = skolem_prefix_for (length js) j ^ abs_s
- val _ = Unsynchronized.change skolems (cons (sko_s, ss))
- val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
- map Bound (rev js))
- val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
- in
- if null js then betapply (abs_t, sko_t)
- else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
- end
- else
- Const (quant_s, quant_T)
- $ Abs (abs_s, abs_T,
- if is_higher_order_type abs_T then
- t
- else
- aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
- (depth + 1) polar t)
- in
- case t of
- Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier s0 T0 s1 T1 t1
- | @{const "==>"} $ t1 $ t2 =>
- @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
- $ aux ss Ts js depth polar t2
- | @{const Pure.conjunction} $ t1 $ t2 =>
- @{const Pure.conjunction} $ aux ss Ts js depth polar t1
- $ aux ss Ts js depth polar t2
- | @{const Trueprop} $ t1 =>
- @{const Trueprop} $ aux ss Ts js depth polar t1
- | @{const Not} $ t1 =>
- @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
- | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier s0 T0 s1 T1 t1
- | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier s0 T0 s1 T1 t1
- | @{const "op &"} $ t1 $ t2 =>
- @{const "op &"} $ aux ss Ts js depth polar t1
- $ aux ss Ts js depth polar t2
- | @{const "op |"} $ t1 $ t2 =>
- @{const "op |"} $ aux ss Ts js depth polar t1
- $ aux ss Ts js depth polar t2
- | @{const "op -->"} $ t1 $ t2 =>
- @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
- $ aux ss Ts js depth polar t2
- | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
- t0 $ t1 $ aux ss Ts js depth polar t2
- | Const (x as (s, T)) =>
- if is_inductive_pred ext_ctxt x andalso
- not (is_well_founded_inductive_pred ext_ctxt x) then
- let
- val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
- val (pref, connective, set_oper) =
- if gfp then
- (lbfp_prefix,
- @{const "op |"},
- @{const_name upper_semilattice_fun_inst.sup_fun})
- else
- (ubfp_prefix,
- @{const "op &"},
- @{const_name lower_semilattice_fun_inst.inf_fun})
- (* unit -> term *)
- fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x
- |> aux ss Ts js depth polar
- fun neg () = Const (pref ^ s, T)
- in
- (case polar |> gfp ? flip_polarity of
- Pos => pos ()
- | Neg => neg ()
- | Neut =>
- if is_fun_type T then
- let
- val ((trunk_arg_Ts, rump_arg_T), body_T) =
- T |> strip_type |>> split_last
- val set_T = rump_arg_T --> body_T
- (* (unit -> term) -> term *)
- fun app f =
- list_comb (f (),
- map Bound (length trunk_arg_Ts - 1 downto 0))
- in
- List.foldr absdummy
- (Const (set_oper, set_T --> set_T --> set_T)
- $ app pos $ app neg) trunk_arg_Ts
- end
- else
- connective $ pos () $ neg ())
- end
- else
- Const x
- | t1 $ t2 =>
- betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
- aux ss Ts [] depth Neut t2)
- | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
- | _ => t
- end
- in aux [] [] [] 0 Pos end
-
-(* extended_context -> styp -> (int * term option) list *)
-fun static_args_in_term ({ersatz_table, ...} : extended_context) x t =
- let
- (* term -> term list -> term list -> term list list *)
- fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
- | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
- | fun_calls t args =
- (case t of
- Const (x' as (s', T')) =>
- x = x' orelse (case AList.lookup (op =) ersatz_table s' of
- SOME s'' => x = (s'', T')
- | NONE => false)
- | _ => false) ? cons args
- (* term list list -> term list list -> term list -> term list list *)
- fun call_sets [] [] vs = [vs]
- | call_sets [] uss vs = vs :: call_sets uss [] []
- | call_sets ([] :: _) _ _ = []
- | call_sets ((t :: ts) :: tss) uss vs =
- OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
- val sets = call_sets (fun_calls t [] []) [] []
- val indexed_sets = sets ~~ (index_seq 0 (length sets))
- in
- fold_rev (fn (set, j) =>
- case set of
- [Var _] => AList.lookup (op =) indexed_sets set = SOME j
- ? cons (j, NONE)
- | [t as Const _] => cons (j, SOME t)
- | [t as Free _] => cons (j, SOME t)
- | _ => I) indexed_sets []
- end
-(* extended_context -> styp -> term list -> (int * term option) list *)
-fun static_args_in_terms ext_ctxt x =
- map (static_args_in_term ext_ctxt x)
- #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
-
-(* term -> term list *)
-fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
- | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
- | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
- snd (strip_comb t1)
- | params_in_equation _ = []
-
-(* styp -> styp -> int list -> term list -> term list -> term -> term *)
-fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
- let
- val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
- + 1
- val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
- val fixed_params = filter_indices fixed_js (params_in_equation t)
- (* term list -> term -> term *)
- fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
- | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
- | aux args t =
- if t = Const x then
- list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
- else
- let val j = find_index (curry (op =) t) fixed_params in
- list_comb (if j >= 0 then nth fixed_args j else t, args)
- end
- in aux [] t end
-
-(* typ list -> term -> bool *)
-fun is_eligible_arg Ts t =
- let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
- null bad_Ts orelse
- (is_higher_order_type (fastype_of1 (Ts, t)) andalso
- forall (not o is_higher_order_type) bad_Ts)
- end
-
-(* (int * term option) list -> (int * term) list -> int list *)
-fun overlapping_indices [] _ = []
- | overlapping_indices _ [] = []
- | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
- if j1 < j2 then overlapping_indices ps1' ps2
- else if j1 > j2 then overlapping_indices ps1 ps2'
- else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
-
-val special_depth = 20
-
-(* extended_context -> int -> term -> term *)
-fun specialize_consts_in_term (ext_ctxt as {thy, specialize, simp_table,
- special_funs, ...}) depth t =
- if not specialize orelse depth > special_depth then
- t
- else
- let
- val blacklist = if depth = 0 then []
- else case term_under_def t of Const x => [x] | _ => []
- (* term list -> typ list -> term -> term *)
- fun aux args Ts (Const (x as (s, T))) =
- ((if not (member (op =) blacklist x) andalso not (null args) andalso
- not (String.isPrefix special_prefix s) andalso
- is_equational_fun ext_ctxt x then
- let
- val eligible_args = filter (is_eligible_arg Ts o snd)
- (index_seq 0 (length args) ~~ args)
- val _ = not (null eligible_args) orelse raise SAME ()
- val old_axs = equational_fun_axioms ext_ctxt x
- |> map (destroy_existential_equalities thy)
- val static_params = static_args_in_terms ext_ctxt x old_axs
- val fixed_js = overlapping_indices static_params eligible_args
- val _ = not (null fixed_js) orelse raise SAME ()
- val fixed_args = filter_indices fixed_js args
- val vars = fold Term.add_vars fixed_args []
- |> sort (TermOrd.fast_indexname_ord o pairself fst)
- val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
- fixed_args []
- |> sort int_ord
- val live_args = filter_out_indices fixed_js args
- val extra_args = map Var vars @ map Bound bound_js @ live_args
- val extra_Ts = map snd vars @ filter_indices bound_js Ts
- val k = maxidx_of_term t + 1
- (* int -> term *)
- fun var_for_bound_no j =
- Var ((bound_var_prefix ^
- nat_subscript (find_index (curry (op =) j) bound_js
- + 1), k),
- nth Ts j)
- val fixed_args_in_axiom =
- map (curry subst_bounds
- (map var_for_bound_no (index_seq 0 (length Ts))))
- fixed_args
- in
- case AList.lookup (op =) (!special_funs)
- (x, fixed_js, fixed_args_in_axiom) of
- SOME x' => list_comb (Const x', extra_args)
- | NONE =>
- let
- val extra_args_in_axiom =
- map Var vars @ map var_for_bound_no bound_js
- val x' as (s', _) =
- (special_prefix_for (length (!special_funs) + 1) ^ s,
- extra_Ts @ filter_out_indices fixed_js (binder_types T)
- ---> body_type T)
- val new_axs =
- map (specialize_fun_axiom x x' fixed_js
- fixed_args_in_axiom extra_args_in_axiom) old_axs
- val _ =
- Unsynchronized.change special_funs
- (cons ((x, fixed_js, fixed_args_in_axiom), x'))
- val _ = add_simps simp_table s' new_axs
- in list_comb (Const x', extra_args) end
- end
- else
- raise SAME ())
- handle SAME () => list_comb (Const x, args))
- | aux args Ts (Abs (s, T, t)) =
- list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
- | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
- | aux args _ t = list_comb (t, args)
- in aux [] [] t end
-
-(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
-fun add_to_uncurry_table thy t =
- let
- (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
- fun aux (t1 $ t2) args table =
- let val table = aux t2 [] table in aux t1 (t2 :: args) table end
- | aux (Abs (_, _, t')) _ table = aux t' [] table
- | aux (t as Const (x as (s, _))) args table =
- if is_built_in_const true x orelse is_constr_like thy x orelse
- is_sel s orelse s = @{const_name Sigma} then
- table
- else
- Termtab.map_default (t, 65536) (curry Int.min (length args)) table
- | aux _ _ table = table
- in aux t [] end
-
-(* int Termtab.tab term -> term *)
-fun uncurry_term table t =
- let
- (* term -> term list -> term *)
- fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
- | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
- | aux (t as Const (s, T)) args =
- (case Termtab.lookup table t of
- SOME n =>
- if n >= 2 then
- let
- val (arg_Ts, rest_T) = strip_n_binders n T
- val j =
- if hd arg_Ts = @{typ bisim_iterator} orelse
- is_fp_iterator_type (hd arg_Ts) then
- 1
- else case find_index (not_equal bool_T) arg_Ts of
- ~1 => n
- | j => j
- val ((before_args, tuple_args), after_args) =
- args |> chop n |>> chop j
- val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
- T |> strip_n_binders n |>> chop j
- val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
- in
- if n - j < 2 then
- betapplys (t, args)
- else
- betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
- before_arg_Ts ---> tuple_T --> rest_T),
- before_args @ [mk_flat_tuple tuple_T tuple_args] @
- after_args)
- end
- else
- betapplys (t, args)
- | NONE => betapplys (t, args))
- | aux t args = betapplys (t, args)
- in aux t [] end
-
-(* (term -> term) -> int -> term -> term *)
-fun coerce_bound_no f j t =
- case t of
- t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
- | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
- | Bound j' => if j' = j then f t else t
- | _ => t
-
-(* extended_context -> bool -> term -> term *)
-fun box_fun_and_pair_in_term (ext_ctxt as {thy, fast_descrs, ...}) def orig_t =
- let
- (* typ -> typ *)
- fun box_relational_operator_type (Type ("fun", Ts)) =
- Type ("fun", map box_relational_operator_type Ts)
- | box_relational_operator_type (Type ("*", Ts)) =
- Type ("*", map (box_type ext_ctxt InPair) Ts)
- | box_relational_operator_type T = T
- (* typ -> typ -> term -> term *)
- fun coerce_bound_0_in_term new_T old_T =
- old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
- (* typ list -> typ -> term -> term *)
- and coerce_term Ts new_T old_T t =
- if old_T = new_T then
- t
- else
- case (new_T, old_T) of
- (Type (new_s, new_Ts as [new_T1, new_T2]),
- Type ("fun", [old_T1, old_T2])) =>
- (case eta_expand Ts t 1 of
- Abs (s, _, t') =>
- Abs (s, new_T1,
- t' |> coerce_bound_0_in_term new_T1 old_T1
- |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
- |> Envir.eta_contract
- |> new_s <> "fun"
- ? construct_value thy (@{const_name FunBox},
- Type ("fun", new_Ts) --> new_T) o single
- | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
- \coerce_term", [t']))
- | (Type (new_s, new_Ts as [new_T1, new_T2]),
- Type (old_s, old_Ts as [old_T1, old_T2])) =>
- if old_s = @{type_name fun_box} orelse
- old_s = @{type_name pair_box} orelse old_s = "*" then
- case constr_expand ext_ctxt old_T t of
- Const (@{const_name FunBox}, _) $ t1 =>
- if new_s = "fun" then
- coerce_term Ts new_T (Type ("fun", old_Ts)) t1
- else
- construct_value thy
- (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
- [coerce_term Ts (Type ("fun", new_Ts))
- (Type ("fun", old_Ts)) t1]
- | Const _ $ t1 $ t2 =>
- construct_value thy
- (if new_s = "*" then @{const_name Pair}
- else @{const_name PairBox}, new_Ts ---> new_T)
- [coerce_term Ts new_T1 old_T1 t1,
- coerce_term Ts new_T2 old_T2 t2]
- | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
- \coerce_term", [t'])
- else
- raise TYPE ("coerce_term", [new_T, old_T], [t])
- | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
- (* indexname * typ -> typ * term -> typ option list -> typ option list *)
- fun add_boxed_types_for_var (z as (_, T)) (T', t') =
- case t' of
- Var z' => z' = z ? insert (op =) T'
- | Const (@{const_name Pair}, _) $ t1 $ t2 =>
- (case T' of
- Type (_, [T1, T2]) =>
- fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
- | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
- \add_boxed_types_for_var", [T'], []))
- | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
- (* typ list -> typ list -> term -> indexname * typ -> typ *)
- fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
- case t of
- @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
- | Const (s0, _) $ t1 $ _ =>
- if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
- let
- val (t', args) = strip_comb t1
- val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
- in
- case fold (add_boxed_types_for_var z)
- (fst (strip_n_binders (length args) T') ~~ args) [] of
- [T''] => T''
- | _ => T
- end
- else
- T
- | _ => T
- (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
- -> term -> term *)
- and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
- let
- val abs_T' =
- if polar = Neut orelse is_positive_existential polar quant_s then
- box_type ext_ctxt InFunLHS abs_T
- else
- abs_T
- val body_T = body_type quant_T
- in
- Const (quant_s, (abs_T' --> body_T) --> body_T)
- $ Abs (abs_s, abs_T',
- t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
- end
- (* typ list -> typ list -> string -> typ -> term -> term -> term *)
- and do_equals new_Ts old_Ts s0 T0 t1 t2 =
- let
- val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
- val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
- val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
- in
- list_comb (Const (s0, T --> T --> body_type T0),
- map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
- end
- (* string -> typ -> term *)
- and do_description_operator s T =
- let val T1 = box_type ext_ctxt InFunLHS (range_type T) in
- Const (s, (T1 --> bool_T) --> T1)
- end
- (* typ list -> typ list -> polarity -> term -> term *)
- and do_term new_Ts old_Ts polar t =
- case t of
- Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
- | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
- do_equals new_Ts old_Ts s0 T0 t1 t2
- | @{const "==>"} $ t1 $ t2 =>
- @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
- $ do_term new_Ts old_Ts polar t2
- | @{const Pure.conjunction} $ t1 $ t2 =>
- @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | @{const Trueprop} $ t1 =>
- @{const Trueprop} $ do_term new_Ts old_Ts polar t1
- | @{const Not} $ t1 =>
- @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
- | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
- | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
- do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
- | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
- do_equals new_Ts old_Ts s0 T0 t1 t2
- | @{const "op &"} $ t1 $ t2 =>
- @{const "op &"} $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | @{const "op |"} $ t1 $ t2 =>
- @{const "op |"} $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | @{const "op -->"} $ t1 $ t2 =>
- @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
- $ do_term new_Ts old_Ts polar t2
- | Const (s as @{const_name The}, T) => do_description_operator s T
- | Const (s as @{const_name Eps}, T) => do_description_operator s T
- | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
- let val T' = box_type ext_ctxt InSel T2 in
- Const (@{const_name quot_normal}, T' --> T')
- end
- | Const (s as @{const_name Tha}, T) => do_description_operator s T
- | Const (x as (s, T)) =>
- Const (s, if s = @{const_name converse} orelse
- s = @{const_name trancl} then
- box_relational_operator_type T
- else if is_built_in_const fast_descrs x orelse
- s = @{const_name Sigma} then
- T
- else if is_constr_like thy x then
- box_type ext_ctxt InConstr T
- else if is_sel s
- orelse is_rep_fun thy x then
- box_type ext_ctxt InSel T
- else
- box_type ext_ctxt InExpr T)
- | t1 $ Abs (s, T, t2') =>
- let
- val t1 = do_term new_Ts old_Ts Neut t1
- val T1 = fastype_of1 (new_Ts, t1)
- val (s1, Ts1) = dest_Type T1
- val T' = hd (snd (dest_Type (hd Ts1)))
- val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
- val T2 = fastype_of1 (new_Ts, t2)
- val t2 = coerce_term new_Ts (hd Ts1) T2 t2
- in
- betapply (if s1 = "fun" then
- t1
- else
- select_nth_constr_arg thy
- (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
- (Type ("fun", Ts1)), t2)
- end
- | t1 $ t2 =>
- let
- val t1 = do_term new_Ts old_Ts Neut t1
- val T1 = fastype_of1 (new_Ts, t1)
- val (s1, Ts1) = dest_Type T1
- val t2 = do_term new_Ts old_Ts Neut t2
- val T2 = fastype_of1 (new_Ts, t2)
- val t2 = coerce_term new_Ts (hd Ts1) T2 t2
- in
- betapply (if s1 = "fun" then
- t1
- else
- select_nth_constr_arg thy
- (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
- (Type ("fun", Ts1)), t2)
- end
- | Free (s, T) => Free (s, box_type ext_ctxt InExpr T)
- | Var (z as (x, T)) =>
- Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
- else box_type ext_ctxt InExpr T)
- | Bound _ => t
- | Abs (s, T, t') =>
- Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
- in do_term [] [] Pos orig_t end
-
-(* int -> term -> term *)
-fun eval_axiom_for_term j t =
- Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
-
-(* extended_context -> styp -> bool *)
-fun is_equational_fun_surely_complete ext_ctxt x =
- case raw_equational_fun_axioms ext_ctxt x of
- [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
- strip_comb t1 |> snd |> forall is_Var
- | _ => false
-
-type special = int list * term list * styp
-
-(* styp -> special -> special -> term *)
-fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
- let
- val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
- val Ts = binder_types T
- val max_j = fold (fold Integer.max) [js1, js2] ~1
- val (eqs, (args1, args2)) =
- fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
- (js1 ~~ ts1, js2 ~~ ts2) of
- (SOME t1, SOME t2) => apfst (cons (t1, t2))
- | (SOME t1, NONE) => apsnd (apsnd (cons t1))
- | (NONE, SOME t2) => apsnd (apfst (cons t2))
- | (NONE, NONE) =>
- let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
- nth Ts j) in
- apsnd (pairself (cons v))
- end) (max_j downto 0) ([], ([], []))
- in
- Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
- |> map Logic.mk_equals,
- Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
- list_comb (Const x2, bounds2 @ args2)))
- |> Refute.close_form (* TODO: needed? *)
- end
-
-(* extended_context -> styp list -> term list *)
-fun special_congruence_axioms (ext_ctxt as {special_funs, ...}) xs =
- let
- val groups =
- !special_funs
- |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
- |> AList.group (op =)
- |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
- |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
- (* special -> int *)
- fun generality (js, _, _) = ~(length js)
- (* special -> special -> bool *)
- fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
- x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
- (j2 ~~ t2, j1 ~~ t1)
- (* styp -> special list -> special list -> special list -> term list
- -> term list *)
- fun do_pass_1 _ [] [_] [_] = I
- | do_pass_1 x skipped _ [] = do_pass_2 x skipped
- | do_pass_1 x skipped all (z :: zs) =
- case filter (is_more_specific z) all
- |> sort (int_ord o pairself generality) of
- [] => do_pass_1 x (z :: skipped) all zs
- | (z' :: _) => cons (special_congruence_axiom x z z')
- #> do_pass_1 x skipped all zs
- (* styp -> special list -> term list -> term list *)
- and do_pass_2 _ [] = I
- | do_pass_2 x (z :: zs) =
- fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
- in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
-
-(* term -> bool *)
-val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
-
-(* 'a Symtab.table -> 'a list *)
-fun all_table_entries table = Symtab.fold (append o snd) table []
-(* const_table -> string -> const_table *)
-fun extra_table table s = Symtab.make [(s, all_table_entries table)]
-
-(* extended_context -> term -> (term list * term list) * (bool * bool) *)
-fun axioms_for_term
- (ext_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
- def_table, nondef_table, user_nondefs, ...}) t =
- let
- type accumulator = styp list * (term list * term list)
- (* (term list * term list -> term list)
- -> ((term list -> term list) -> term list * term list
- -> term list * term list)
- -> int -> term -> accumulator -> accumulator *)
- fun add_axiom get app depth t (accum as (xs, axs)) =
- let
- val t = t |> unfold_defs_in_term ext_ctxt
- |> skolemize_term_and_more ext_ctxt ~1
- in
- if is_trivial_equation t then
- accum
- else
- let val t' = t |> specialize_consts_in_term ext_ctxt depth in
- if exists (member (op aconv) (get axs)) [t, t'] then accum
- else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
- end
- end
- (* int -> term -> accumulator -> accumulator *)
- and add_def_axiom depth = add_axiom fst apfst depth
- and add_nondef_axiom depth = add_axiom snd apsnd depth
- and add_maybe_def_axiom depth t =
- (if head_of t <> @{const "==>"} then add_def_axiom
- else add_nondef_axiom) depth t
- and add_eq_axiom depth t =
- (if is_constr_pattern_formula thy t then add_def_axiom
- else add_nondef_axiom) depth t
- (* int -> term -> accumulator -> accumulator *)
- and add_axioms_for_term depth t (accum as (xs, axs)) =
- case t of
- t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
- | Const (x as (s, T)) =>
- (if member (op =) xs x orelse is_built_in_const fast_descrs x then
- accum
- else
- let val accum as (xs, _) = (x :: xs, axs) in
- if depth > axioms_max_depth then
- raise TOO_LARGE ("Nitpick_HOL.axioms_for_term.\
- \add_axioms_for_term",
- "too many nested axioms (" ^
- string_of_int depth ^ ")")
- else if Refute.is_const_of_class thy x then
- let
- val class = Logic.class_of_const s
- val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
- class)
- val ax1 = try (Refute.specialize_type thy x) of_class
- val ax2 = Option.map (Refute.specialize_type thy x o snd)
- (Refute.get_classdef thy class)
- in
- fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
- accum
- end
- else if is_constr thy x then
- accum
- else if is_equational_fun ext_ctxt x then
- fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
- accum
- else if is_abs_fun thy x then
- if is_quot_type thy (range_type T) then
- raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
- else
- accum |> fold (add_nondef_axiom depth)
- (nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
- ? fold (add_maybe_def_axiom depth)
- (nondef_props_for_const thy true
- (extra_table def_table s) x)
- else if is_rep_fun thy x then
- if is_quot_type thy (domain_type T) then
- raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
- else
- accum |> fold (add_nondef_axiom depth)
- (nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
- ? fold (add_maybe_def_axiom depth)
- (nondef_props_for_const thy true
- (extra_table def_table s) x)
- |> add_axioms_for_term depth
- (Const (mate_of_rep_fun thy x))
- |> fold (add_def_axiom depth)
- (inverse_axioms_for_rep_fun thy x)
- else
- accum |> user_axioms <> SOME false
- ? fold (add_nondef_axiom depth)
- (nondef_props_for_const thy false nondef_table x)
- end)
- |> add_axioms_for_type depth T
- | Free (_, T) => add_axioms_for_type depth T accum
- | Var (_, T) => add_axioms_for_type depth T accum
- | Bound _ => accum
- | Abs (_, T, t) => accum |> add_axioms_for_term depth t
- |> add_axioms_for_type depth T
- (* int -> typ -> accumulator -> accumulator *)
- and add_axioms_for_type depth T =
- case T of
- Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
- | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
- | @{typ prop} => I
- | @{typ bool} => I
- | @{typ unit} => I
- | TFree (_, S) => add_axioms_for_sort depth T S
- | TVar (_, S) => add_axioms_for_sort depth T S
- | Type (z as (s, Ts)) =>
- fold (add_axioms_for_type depth) Ts
- #> (if is_pure_typedef thy T then
- fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
- else if is_quot_type thy T then
- fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
- else if max_bisim_depth >= 0 andalso is_codatatype thy T then
- fold (add_maybe_def_axiom depth)
- (codatatype_bisim_axioms ext_ctxt T)
- else
- I)
- (* int -> typ -> sort -> accumulator -> accumulator *)
- and add_axioms_for_sort depth T S =
- let
- val supers = Sign.complete_sort thy S
- val class_axioms =
- maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
- handle ERROR _ => [])) supers
- val monomorphic_class_axioms =
- map (fn t => case Term.add_tvars t [] of
- [] => t
- | [(x, S)] =>
- Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
- | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
- \add_axioms_for_sort", [t]))
- class_axioms
- in fold (add_nondef_axiom depth) monomorphic_class_axioms end
- val (mono_user_nondefs, poly_user_nondefs) =
- List.partition (null o Term.hidden_polymorphism) user_nondefs
- val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
- evals
- val (xs, (defs, nondefs)) =
- ([], ([], [])) |> add_axioms_for_term 1 t
- |> fold_rev (add_def_axiom 1) eval_axioms
- |> user_axioms = SOME true
- ? fold (add_nondef_axiom 1) mono_user_nondefs
- val defs = defs @ special_congruence_axioms ext_ctxt xs
- in
- ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
- null poly_user_nondefs))
- end
+(* hol_context -> typ -> typ list *)
+fun ground_types_in_type hol_ctxt T = add_ground_types hol_ctxt T []
+(* hol_context -> term list -> typ list *)
+fun ground_types_in_terms hol_ctxt ts =
+ fold (fold_types (add_ground_types hol_ctxt)) ts []
(* theory -> const_table -> styp -> int list *)
fun const_format thy def_table (x as (s, T)) =
@@ -3356,10 +2096,10 @@
|> map (rev o filter_out (member (op =) js))
|> filter_out null |> map length |> rev
-(* extended_context -> string * string -> (term option * int list) list
+(* hol_context -> string * string -> (term option * int list) list
-> styp -> term * typ *)
fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
- : extended_context) (base_name, step_name) formats =
+ : hol_context) (base_name, step_name) formats =
let
val default_format = the (AList.lookup (op =) formats NONE)
(* styp -> term * typ *)
@@ -3460,7 +2200,7 @@
(t, format_term_type thy def_table formats t)
end)
|>> map_types unbit_and_unbox_type
- |>> shorten_names_in_term |>> shorten_abs_vars
+ |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
in do_const end
(* styp -> string *)
@@ -3474,84 +2214,4 @@
else
"="
-val binary_int_threshold = 4
-
-(* term -> bool *)
-fun may_use_binary_ints (t1 $ t2) =
- may_use_binary_ints t1 andalso may_use_binary_ints t2
- | may_use_binary_ints (t as Const (s, _)) =
- t <> @{const Suc} andalso
- not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
- @{const_name nat_gcd}, @{const_name nat_lcm},
- @{const_name Frac}, @{const_name norm_frac}] s)
- | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
- | may_use_binary_ints _ = true
-fun should_use_binary_ints (t1 $ t2) =
- should_use_binary_ints t1 orelse should_use_binary_ints t2
- | should_use_binary_ints (Const (s, _)) =
- member (op =) [@{const_name times_nat_inst.times_nat},
- @{const_name div_nat_inst.div_nat},
- @{const_name times_int_inst.times_int},
- @{const_name div_int_inst.div_int}] s orelse
- (String.isPrefix numeral_prefix s andalso
- let val n = the (Int.fromString (unprefix numeral_prefix s)) in
- n <= ~ binary_int_threshold orelse n >= binary_int_threshold
- end)
- | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
- | should_use_binary_ints _ = false
-
-(* typ -> typ *)
-fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
- | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
- | binarize_nat_and_int_in_type (Type (s, Ts)) =
- Type (s, map binarize_nat_and_int_in_type Ts)
- | binarize_nat_and_int_in_type T = T
-(* term -> term *)
-val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
-
-(* extended_context -> term
- -> ((term list * term list) * (bool * bool)) * term *)
-fun preprocess_term (ext_ctxt as {thy, binary_ints, destroy_constrs, boxes,
- skolemize, uncurry, ...}) t =
- let
- val skolem_depth = if skolemize then 4 else ~1
- val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
- core_t) = t |> unfold_defs_in_term ext_ctxt
- |> Refute.close_form
- |> skolemize_term_and_more ext_ctxt skolem_depth
- |> specialize_consts_in_term ext_ctxt 0
- |> `(axioms_for_term ext_ctxt)
- val binarize =
- case binary_ints of
- SOME false => false
- | _ =>
- forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
- (binary_ints = SOME true orelse
- exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
- val box = exists (not_equal (SOME false) o snd) boxes
- val table =
- Termtab.empty |> uncurry
- ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
- (* bool -> bool -> term -> term *)
- fun do_rest def core =
- binarize ? binarize_nat_and_int_in_term
- #> uncurry ? uncurry_term table
- #> box ? box_fun_and_pair_in_term ext_ctxt def
- #> destroy_constrs ? (pull_out_universal_constrs thy def
- #> pull_out_existential_constrs thy
- #> destroy_pulled_out_constrs ext_ctxt def)
- #> curry_assms
- #> destroy_universal_equalities
- #> destroy_existential_equalities thy
- #> simplify_constrs_and_sels thy
- #> distribute_quantifiers
- #> push_quantifiers_inward thy
- #> not core ? Refute.close_form
- #> shorten_abs_vars
- in
- (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
- (got_all_mono_user_axioms, no_poly_user_axioms)),
- do_rest false true core_t)
- end
-
end;
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 04 14:45:08 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Feb 05 11:15:16 2010 +0100
@@ -7,7 +7,7 @@
signature NITPICK_KODKOD =
sig
- type extended_context = Nitpick_HOL.extended_context
+ type hol_context = Nitpick_HOL.hol_context
type dtype_spec = Nitpick_Scope.dtype_spec
type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
type nut = Nitpick_Nut.nut
@@ -33,7 +33,7 @@
val merge_bounds : Kodkod.bound list -> Kodkod.bound list
val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
val declarative_axioms_for_datatypes :
- extended_context -> int -> int Typtab.table -> kodkod_constrs
+ hol_context -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
val kodkod_formula_from_nut :
int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
@@ -316,7 +316,15 @@
if R2 = Formula Neut then
[ts] |> not exclusive ? cons (KK.TupleSet [])
else
- [KK.TupleSet [], KK.TupleProduct (ts, upper_bound_for_rep R2)]
+ [KK.TupleSet [],
+ if exclusive andalso T1 = T2 andalso epsilon > delta then
+ index_seq delta (epsilon - delta)
+ |> map (fn j =>
+ KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
+ KK.TupleAtomSeq (j, j0)))
+ |> foldl1 KK.TupleUnion
+ else
+ KK.TupleProduct (ts, upper_bound_for_rep R2)]
end)
end
| bound_for_sel_rel _ _ _ u =
@@ -732,12 +740,12 @@
(* nut NameTable.table -> styp -> KK.rel_expr *)
fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> styp -> int -> nfa_transition list *)
-fun nfa_transitions_for_sel ext_ctxt ({kk_project, ...} : kodkod_constrs)
+fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs)
rel_table (dtypes : dtype_spec list) constr_x n =
let
- val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt constr_x n
+ val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n
val (r, R, arity) = const_triple rel_table x
val type_schema = type_schema_of_rep T R
in
@@ -746,17 +754,17 @@
else SOME (kk_project r (map KK.Num [0, j]), T))
(index_seq 1 (arity - 1) ~~ tl type_schema)
end
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> styp -> nfa_transition list *)
-fun nfa_transitions_for_constr ext_ctxt kk rel_table dtypes (x as (_, T)) =
- maps (nfa_transitions_for_sel ext_ctxt kk rel_table dtypes x)
+fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) =
+ maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x)
(index_seq 0 (num_sels_for_constr_type T))
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> dtype_spec -> nfa_entry option *)
fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
| nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
- | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
- SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
+ | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
+ SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
o #const) constrs)
val empty_rel = KK.Product (KK.None, KK.None)
@@ -812,23 +820,23 @@
fun acyclicity_axiom_for_datatype dtypes kk nfa start =
#kk_no kk (#kk_intersect kk
(loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> KK.formula list *)
-fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes =
- map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes
+fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
+ map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
|> strongly_connected_sub_nfas
|> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst)
nfa)
-(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
- -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
-fun sel_axiom_for_sel ext_ctxt j0
+(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
+ -> constr_spec -> int -> KK.formula *)
+fun sel_axiom_for_sel hol_ctxt j0
(kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
kk_join, ...}) rel_table dom_r
({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
n =
let
- val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt const n
+ val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n
val (r, R, arity) = const_triple rel_table x
val R2 = dest_Func R |> snd
val z = (epsilon - delta, delta + j0)
@@ -842,9 +850,9 @@
(kk_n_ary_function kk R2 r') (kk_no r'))
end
end
-(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
+(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
-> constr_spec -> KK.formula list *)
-fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table
+fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table
(constr as {const, delta, epsilon, explicit_max, ...}) =
let
val honors_explicit_max =
@@ -866,19 +874,19 @@
" too small for \"max\"")
in
max_axiom ::
- map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr)
+ map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr)
(index_seq 0 (num_sels_for_constr_type (snd const)))
end
end
-(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
+(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
-> dtype_spec -> KK.formula list *)
-fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table
+fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table
({constrs, ...} : dtype_spec) =
- maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs
+ maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
-> KK.formula list *)
-fun uniqueness_axiom_for_constr ext_ctxt
+fun uniqueness_axiom_for_constr hol_ctxt
({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
: kodkod_constrs) rel_table ({const, ...} : constr_spec) =
let
@@ -887,7 +895,7 @@
kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
val num_sels = num_sels_for_constr_type (snd const)
val triples = map (const_triple rel_table
- o boxed_nth_sel_for_constr ext_ctxt const)
+ o boxed_nth_sel_for_constr hol_ctxt const)
(~1 upto num_sels - 1)
val j0 = case triples |> hd |> #2 of
Func (Atom (_, j0), _) => j0
@@ -903,11 +911,11 @@
(fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
end
-(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
+(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
-> KK.formula list *)
-fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table
+fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table
({constrs, ...} : dtype_spec) =
- map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs
+ map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs
(* constr_spec -> int *)
fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
@@ -924,31 +932,31 @@
kk_disjoint_sets kk rs]
end
-(* extended_context -> int -> int Typtab.table -> kodkod_constrs
+(* hol_context -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec -> KK.formula list *)
fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
- | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
+ | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table
(dtype as {typ, ...}) =
let val j0 = offset_of_type ofs typ in
- sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @
- uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
+ sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @
+ uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @
partition_axioms_for_datatype j0 kk rel_table dtype
end
-(* extended_context -> int -> int Typtab.table -> kodkod_constrs
+(* hol_context -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> KK.formula list *)
-fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes =
- acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @
- maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes
+fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes =
+ acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
+ maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
fun kodkod_formula_from_nut bits ofs liberal
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
- kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,
- kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference,
- kk_intersect, kk_product, kk_join, kk_closure, kk_comprehension,
- kk_project, kk_project_seq, kk_not3, kk_nat_less, kk_int_less,
- ...}) u =
+ kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
+ kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
+ kk_difference, kk_intersect, kk_product, kk_join, kk_closure,
+ kk_comprehension, kk_project, kk_project_seq, kk_not3,
+ kk_nat_less, kk_int_less, ...}) u =
let
val main_j0 = offset_of_type ofs bool_T
val bool_j0 = main_j0
@@ -1108,7 +1116,7 @@
else
if is_lone_rep min_R then
if arity_of_rep min_R = 1 then
- kk_subset (kk_product r1 r2) KK.Iden
+ kk_lone (kk_union r1 r2)
else if not both_opt then
(r1, r2) |> is_opt_rep (rep_of u2) ? swap
|-> kk_subset
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 04 14:45:08 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Feb 05 11:15:16 2010 +0100
@@ -251,7 +251,7 @@
-> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
-> int list list -> term *)
fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
- ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
+ ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
: scope) sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
@@ -400,7 +400,7 @@
else NONE)
(discr_jsss ~~ constrs) |> the
val arg_Ts = curried_binder_types constr_T
- val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x)
+ val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x)
(index_seq 0 (length arg_Ts))
val sel_Rs =
map (fn x => get_first
@@ -586,7 +586,7 @@
-> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
-> Pretty.T * bool *)
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
- ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
+ ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
user_axioms, debug, binary_ints, destroy_constrs,
specialize, skolemize, star_linear_preds, uncurry,
fast_descrs, tac_timeout, evals, case_names, def_table,
@@ -598,7 +598,7 @@
let
val (wacky_names as (_, base_name, step_name, _), ctxt) =
add_wacky_syntax ctxt
- val ext_ctxt =
+ val hol_ctxt =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
binary_ints = binary_ints, destroy_constrs = destroy_constrs,
@@ -612,7 +612,7 @@
ersatz_table = ersatz_table, skolems = skolems,
special_funs = special_funs, unrolled_preds = unrolled_preds,
wf_cache = wf_cache, constr_cache = constr_cache}
- val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
+ val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
ofs = ofs}
(* typ -> typ -> rep -> int list list -> term *)
@@ -644,7 +644,7 @@
end
| ConstName (s, T, _) =>
(assign_operator_for_const (s, T),
- user_friendly_const ext_ctxt (base_name, step_name) formats (s, T),
+ user_friendly_const hol_ctxt (base_name, step_name) formats (s, T),
T)
| _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
\pretty_for_assign", [name])
@@ -724,7 +724,7 @@
(* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
-> KK.raw_bound list -> term -> bool option *)
-fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, debug, ...},
+fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...},
card_assigns, ...})
auto_timeout free_names sel_names rel_table bounds prop =
let
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 04 14:45:08 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Feb 05 11:15:16 2010 +0100
@@ -8,10 +8,10 @@
signature NITPICK_MONO =
sig
datatype sign = Plus | Minus
- type extended_context = Nitpick_HOL.extended_context
+ type hol_context = Nitpick_HOL.hol_context
val formulas_monotonic :
- extended_context -> typ -> sign -> term list -> term list -> term -> bool
+ hol_context -> typ -> sign -> term list -> term list -> term -> bool
end;
structure Nitpick_Mono : NITPICK_MONO =
@@ -35,7 +35,7 @@
CRec of string * typ list
type cdata =
- {ext_ctxt: extended_context,
+ {hol_ctxt: hol_context,
alpha_T: typ,
max_fresh: int Unsynchronized.ref,
datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
@@ -114,9 +114,9 @@
| flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
| flatten_ctype C = [C]
-(* extended_context -> typ -> cdata *)
-fun initial_cdata ext_ctxt alpha_T =
- ({ext_ctxt = ext_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
+(* hol_context -> typ -> cdata *)
+fun initial_cdata hol_ctxt alpha_T =
+ ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
datatype_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []} : cdata)
@@ -188,7 +188,7 @@
in List.app repair_one (!constr_cache) end
(* cdata -> typ -> ctype *)
-fun fresh_ctype_for_type ({ext_ctxt as {thy, ...}, alpha_T, max_fresh,
+fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, alpha_T, max_fresh,
datatype_cache, constr_cache, ...} : cdata) =
let
(* typ -> typ -> ctype *)
@@ -217,7 +217,7 @@
| NONE =>
let
val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
- val xs = datatype_constrs ext_ctxt T
+ val xs = datatype_constrs hol_ctxt T
val (all_Cs, constr_Cs) =
fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
let
@@ -264,7 +264,7 @@
end
(* cdata -> styp -> ctype *)
-fun ctype_for_constr (cdata as {ext_ctxt as {thy, ...}, alpha_T, constr_cache,
+fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache,
...}) (x as (_, T)) =
if could_exist_alpha_sub_ctype thy alpha_T T then
case AList.lookup (op =) (!constr_cache) x of
@@ -278,8 +278,8 @@
AList.lookup (op =) (!constr_cache) x |> the)
else
fresh_ctype_for_type cdata T
-fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) =
- x |> boxed_constr_for_sel ext_ctxt |> ctype_for_constr cdata
+fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
+ x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
|> sel_ctype_from_constr_ctype s
(* literal list -> ctype -> ctype *)
@@ -549,7 +549,7 @@
handle List.Empty => initial_gamma
(* cdata -> term -> accumulator -> ctype * accumulator *)
-fun consider_term (cdata as {ext_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
+fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
max_fresh, ...}) =
let
(* typ -> ctype *)
@@ -806,7 +806,7 @@
in do_term end
(* cdata -> sign -> term -> accumulator -> accumulator *)
-fun consider_general_formula (cdata as {ext_ctxt as {ctxt, ...}, ...}) =
+fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) =
let
(* typ -> ctype *)
val ctype_for = fresh_ctype_for_type cdata
@@ -895,7 +895,7 @@
not (is_harmless_axiom t) ? consider_general_formula cdata sn t
(* cdata -> term -> accumulator -> accumulator *)
-fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t =
+fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
if not (is_constr_pattern_formula thy t) then
consider_nondefinitional_axiom cdata Plus t
else if is_harmless_axiom t then
@@ -945,13 +945,13 @@
map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
|> cat_lines |> print_g
-(* extended_context -> typ -> sign -> term list -> term list -> term -> bool *)
-fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
+(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
+fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
core_t =
let
val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
Syntax.string_of_typ ctxt alpha_T)
- val cdata as {max_fresh, ...} = initial_cdata ext_ctxt alpha_T
+ val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
val (gamma, cset) =
(initial_gamma, slack)
|> fold (consider_definitional_axiom cdata) def_ts
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Feb 04 14:45:08 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Feb 05 11:15:16 2010 +0100
@@ -8,7 +8,7 @@
signature NITPICK_NUT =
sig
type special_fun = Nitpick_HOL.special_fun
- type extended_context = Nitpick_HOL.extended_context
+ type hol_context = Nitpick_HOL.hol_context
type scope = Nitpick_Scope.scope
type name_pool = Nitpick_Peephole.name_pool
type rep = Nitpick_Rep.rep
@@ -106,7 +106,7 @@
val name_ord : (nut * nut) -> order
val the_name : 'a NameTable.table -> nut -> 'a
val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
- val nut_from_term : extended_context -> op2 -> term -> nut
+ val nut_from_term : hol_context -> op2 -> term -> nut
val choose_reps_for_free_vars :
scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
val choose_reps_for_consts :
@@ -466,8 +466,8 @@
fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
-(* extended_context -> op2 -> term -> nut *)
-fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
+(* hol_context -> op2 -> term -> nut *)
+fun nut_from_term (hol_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
let
(* string list -> typ list -> term -> nut *)
fun aux eq ss Ts t =
@@ -597,7 +597,7 @@
Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
| (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
| (Const (@{const_name finite}, T), [t1]) =>
- (if is_finite_type ext_ctxt (domain_type T) then
+ (if is_finite_type hol_ctxt (domain_type T) then
Cst (True, bool_T, Any)
else case t1 of
Const (@{const_name top}, _) => Cst (False, bool_T, Any)
@@ -712,7 +712,7 @@
in (v :: vs, NameTable.update (v, R) table) end
(* scope -> bool -> nut -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes,
+fun choose_rep_for_const (scope as {hol_ctxt as {thy, ctxt, ...}, datatypes,
ofs, ...}) all_exact v (vs, table) =
let
val x as (s, T) = (nickname_of v, type_of v)
@@ -747,10 +747,10 @@
(* scope -> styp -> int -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n
+fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, ...}) (x as (_, T)) n
(vs, table) =
let
- val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
+ val (s', T') = boxed_nth_sel_for_constr hol_ctxt x n
val R' = if n = ~1 orelse is_word_type (body_type T) orelse
(is_fun_type (range_type T') andalso
is_boolean_type (body_type T')) then
@@ -890,7 +890,7 @@
| untuple f u = if rep_of u = Unit then [] else [f u]
(* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
-fun choose_reps_in_nut (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns,
+fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
bits, datatypes, ofs, ...})
liberal table def =
let
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Feb 05 11:15:16 2010 +0100
@@ -0,0 +1,1431 @@
+(* Title: HOL/Tools/Nitpick/nitpick_preproc.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2008, 2009, 2010
+
+Nitpick's HOL preprocessor.
+*)
+
+signature NITPICK_PREPROC =
+sig
+ type hol_context = Nitpick_HOL.hol_context
+ val preprocess_term :
+ hol_context -> term -> ((term list * term list) * (bool * bool)) * term
+end
+
+structure Nitpick_Preproc : NITPICK_PREPROC =
+struct
+
+open Nitpick_Util
+open Nitpick_HOL
+
+(* polarity -> string -> bool *)
+fun is_positive_existential polar quant_s =
+ (polar = Pos andalso quant_s = @{const_name Ex}) orelse
+ (polar = Neg andalso quant_s <> @{const_name Ex})
+
+(** Binary coding of integers **)
+
+(* If a formula contains a numeral whose absolute value is more than this
+ threshold, the unary coding is likely not to work well and we prefer the
+ binary coding. *)
+val binary_int_threshold = 3
+
+(* term -> bool *)
+fun may_use_binary_ints (t1 $ t2) =
+ may_use_binary_ints t1 andalso may_use_binary_ints t2
+ | may_use_binary_ints (t as Const (s, _)) =
+ t <> @{const Suc} andalso
+ not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
+ @{const_name nat_gcd}, @{const_name nat_lcm},
+ @{const_name Frac}, @{const_name norm_frac}] s)
+ | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
+ | may_use_binary_ints _ = true
+fun should_use_binary_ints (t1 $ t2) =
+ should_use_binary_ints t1 orelse should_use_binary_ints t2
+ | should_use_binary_ints (Const (s, _)) =
+ member (op =) [@{const_name times_nat_inst.times_nat},
+ @{const_name div_nat_inst.div_nat},
+ @{const_name times_int_inst.times_int},
+ @{const_name div_int_inst.div_int}] s orelse
+ (String.isPrefix numeral_prefix s andalso
+ let val n = the (Int.fromString (unprefix numeral_prefix s)) in
+ n < ~ binary_int_threshold orelse n > binary_int_threshold
+ end)
+ | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
+ | should_use_binary_ints _ = false
+
+(* typ -> typ *)
+fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
+ | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
+ | binarize_nat_and_int_in_type (Type (s, Ts)) =
+ Type (s, map binarize_nat_and_int_in_type Ts)
+ | binarize_nat_and_int_in_type T = T
+(* term -> term *)
+val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
+
+(** Uncurrying **)
+
+(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
+fun add_to_uncurry_table thy t =
+ let
+ (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
+ fun aux (t1 $ t2) args table =
+ let val table = aux t2 [] table in aux t1 (t2 :: args) table end
+ | aux (Abs (_, _, t')) _ table = aux t' [] table
+ | aux (t as Const (x as (s, _))) args table =
+ if is_built_in_const true x orelse is_constr_like thy x orelse
+ is_sel s orelse s = @{const_name Sigma} then
+ table
+ else
+ Termtab.map_default (t, 65536) (curry Int.min (length args)) table
+ | aux _ _ table = table
+ in aux t [] end
+
+(* int -> int -> string *)
+fun uncurry_prefix_for k j =
+ uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
+
+(* int Termtab.tab term -> term *)
+fun uncurry_term table t =
+ let
+ (* term -> term list -> term *)
+ fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
+ | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
+ | aux (t as Const (s, T)) args =
+ (case Termtab.lookup table t of
+ SOME n =>
+ if n >= 2 then
+ let
+ val (arg_Ts, rest_T) = strip_n_binders n T
+ val j =
+ if hd arg_Ts = @{typ bisim_iterator} orelse
+ is_fp_iterator_type (hd arg_Ts) then
+ 1
+ else case find_index (not_equal bool_T) arg_Ts of
+ ~1 => n
+ | j => j
+ val ((before_args, tuple_args), after_args) =
+ args |> chop n |>> chop j
+ val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
+ T |> strip_n_binders n |>> chop j
+ val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
+ in
+ if n - j < 2 then
+ betapplys (t, args)
+ else
+ betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
+ before_arg_Ts ---> tuple_T --> rest_T),
+ before_args @ [mk_flat_tuple tuple_T tuple_args] @
+ after_args)
+ end
+ else
+ betapplys (t, args)
+ | NONE => betapplys (t, args))
+ | aux t args = betapplys (t, args)
+ in aux t [] end
+
+(** Boxing **)
+
+(* hol_context -> typ -> term -> term *)
+fun constr_expand (hol_ctxt as {thy, ...}) T t =
+ (case head_of t of
+ Const x => if is_constr_like thy x then t else raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () =>
+ let
+ val x' as (_, T') =
+ if is_pair_type T then
+ let val (T1, T2) = HOLogic.dest_prodT T in
+ (@{const_name Pair}, T1 --> T2 --> T)
+ end
+ else
+ datatype_constrs hol_ctxt T |> hd
+ val arg_Ts = binder_types T'
+ in
+ list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
+ (index_seq 0 (length arg_Ts)) arg_Ts)
+ end
+
+(* hol_context -> bool -> term -> term *)
+fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t =
+ let
+ (* typ -> typ *)
+ fun box_relational_operator_type (Type ("fun", Ts)) =
+ Type ("fun", map box_relational_operator_type Ts)
+ | box_relational_operator_type (Type ("*", Ts)) =
+ Type ("*", map (box_type hol_ctxt InPair) Ts)
+ | box_relational_operator_type T = T
+ (* (term -> term) -> int -> term -> term *)
+ fun coerce_bound_no f j t =
+ case t of
+ t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
+ | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
+ | Bound j' => if j' = j then f t else t
+ | _ => t
+ (* typ -> typ -> term -> term *)
+ fun coerce_bound_0_in_term new_T old_T =
+ old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
+ (* typ list -> typ -> term -> term *)
+ and coerce_term Ts new_T old_T t =
+ if old_T = new_T then
+ t
+ else
+ case (new_T, old_T) of
+ (Type (new_s, new_Ts as [new_T1, new_T2]),
+ Type ("fun", [old_T1, old_T2])) =>
+ (case eta_expand Ts t 1 of
+ Abs (s, _, t') =>
+ Abs (s, new_T1,
+ t' |> coerce_bound_0_in_term new_T1 old_T1
+ |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
+ |> Envir.eta_contract
+ |> new_s <> "fun"
+ ? construct_value thy (@{const_name FunBox},
+ Type ("fun", new_Ts) --> new_T) o single
+ | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
+ \coerce_term", [t']))
+ | (Type (new_s, new_Ts as [new_T1, new_T2]),
+ Type (old_s, old_Ts as [old_T1, old_T2])) =>
+ if old_s = @{type_name fun_box} orelse
+ old_s = @{type_name pair_box} orelse old_s = "*" then
+ case constr_expand hol_ctxt old_T t of
+ Const (@{const_name FunBox}, _) $ t1 =>
+ if new_s = "fun" then
+ coerce_term Ts new_T (Type ("fun", old_Ts)) t1
+ else
+ construct_value thy
+ (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
+ [coerce_term Ts (Type ("fun", new_Ts))
+ (Type ("fun", old_Ts)) t1]
+ | Const _ $ t1 $ t2 =>
+ construct_value thy
+ (if new_s = "*" then @{const_name Pair}
+ else @{const_name PairBox}, new_Ts ---> new_T)
+ [coerce_term Ts new_T1 old_T1 t1,
+ coerce_term Ts new_T2 old_T2 t2]
+ | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
+ \coerce_term", [t'])
+ else
+ raise TYPE ("coerce_term", [new_T, old_T], [t])
+ | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
+ (* indexname * typ -> typ * term -> typ option list -> typ option list *)
+ fun add_boxed_types_for_var (z as (_, T)) (T', t') =
+ case t' of
+ Var z' => z' = z ? insert (op =) T'
+ | Const (@{const_name Pair}, _) $ t1 $ t2 =>
+ (case T' of
+ Type (_, [T1, T2]) =>
+ fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
+ | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\
+ \add_boxed_types_for_var", [T'], []))
+ | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
+ (* typ list -> typ list -> term -> indexname * typ -> typ *)
+ fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
+ case t of
+ @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
+ | Const (s0, _) $ t1 $ _ =>
+ if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
+ let
+ val (t', args) = strip_comb t1
+ val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
+ in
+ case fold (add_boxed_types_for_var z)
+ (fst (strip_n_binders (length args) T') ~~ args) [] of
+ [T''] => T''
+ | _ => T
+ end
+ else
+ T
+ | _ => T
+ (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
+ -> term -> term *)
+ and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
+ let
+ val abs_T' =
+ if polar = Neut orelse is_positive_existential polar quant_s then
+ box_type hol_ctxt InFunLHS abs_T
+ else
+ abs_T
+ val body_T = body_type quant_T
+ in
+ Const (quant_s, (abs_T' --> body_T) --> body_T)
+ $ Abs (abs_s, abs_T',
+ t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
+ end
+ (* typ list -> typ list -> string -> typ -> term -> term -> term *)
+ and do_equals new_Ts old_Ts s0 T0 t1 t2 =
+ let
+ val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
+ val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
+ val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
+ in
+ list_comb (Const (s0, T --> T --> body_type T0),
+ map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
+ end
+ (* string -> typ -> term *)
+ and do_description_operator s T =
+ let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
+ Const (s, (T1 --> bool_T) --> T1)
+ end
+ (* typ list -> typ list -> polarity -> term -> term *)
+ and do_term new_Ts old_Ts polar t =
+ case t of
+ Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
+ | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
+ do_equals new_Ts old_Ts s0 T0 t1 t2
+ | @{const "==>"} $ t1 $ t2 =>
+ @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ $ do_term new_Ts old_Ts polar t2
+ | @{const Pure.conjunction} $ t1 $ t2 =>
+ @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
+ $ do_term new_Ts old_Ts polar t2
+ | @{const Trueprop} $ t1 =>
+ @{const Trueprop} $ do_term new_Ts old_Ts polar t1
+ | @{const Not} $ t1 =>
+ @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
+ | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
+ | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
+ do_equals new_Ts old_Ts s0 T0 t1 t2
+ | @{const "op &"} $ t1 $ t2 =>
+ @{const "op &"} $ do_term new_Ts old_Ts polar t1
+ $ do_term new_Ts old_Ts polar t2
+ | @{const "op |"} $ t1 $ t2 =>
+ @{const "op |"} $ do_term new_Ts old_Ts polar t1
+ $ do_term new_Ts old_Ts polar t2
+ | @{const "op -->"} $ t1 $ t2 =>
+ @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ $ do_term new_Ts old_Ts polar t2
+ | Const (s as @{const_name The}, T) => do_description_operator s T
+ | Const (s as @{const_name Eps}, T) => do_description_operator s T
+ | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
+ let val T' = box_type hol_ctxt InSel T2 in
+ Const (@{const_name quot_normal}, T' --> T')
+ end
+ | Const (s as @{const_name Tha}, T) => do_description_operator s T
+ | Const (x as (s, T)) =>
+ Const (s, if s = @{const_name converse} orelse
+ s = @{const_name trancl} then
+ box_relational_operator_type T
+ else if is_built_in_const fast_descrs x orelse
+ s = @{const_name Sigma} then
+ T
+ else if is_constr_like thy x then
+ box_type hol_ctxt InConstr T
+ else if is_sel s
+ orelse is_rep_fun thy x then
+ box_type hol_ctxt InSel T
+ else
+ box_type hol_ctxt InExpr T)
+ | t1 $ Abs (s, T, t2') =>
+ let
+ val t1 = do_term new_Ts old_Ts Neut t1
+ val T1 = fastype_of1 (new_Ts, t1)
+ val (s1, Ts1) = dest_Type T1
+ val T' = hd (snd (dest_Type (hd Ts1)))
+ val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
+ val T2 = fastype_of1 (new_Ts, t2)
+ val t2 = coerce_term new_Ts (hd Ts1) T2 t2
+ in
+ betapply (if s1 = "fun" then
+ t1
+ else
+ select_nth_constr_arg thy
+ (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
+ (Type ("fun", Ts1)), t2)
+ end
+ | t1 $ t2 =>
+ let
+ val t1 = do_term new_Ts old_Ts Neut t1
+ val T1 = fastype_of1 (new_Ts, t1)
+ val (s1, Ts1) = dest_Type T1
+ val t2 = do_term new_Ts old_Ts Neut t2
+ val T2 = fastype_of1 (new_Ts, t2)
+ val t2 = coerce_term new_Ts (hd Ts1) T2 t2
+ in
+ betapply (if s1 = "fun" then
+ t1
+ else
+ select_nth_constr_arg thy
+ (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
+ (Type ("fun", Ts1)), t2)
+ end
+ | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
+ | Var (z as (x, T)) =>
+ Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
+ else box_type hol_ctxt InExpr T)
+ | Bound _ => t
+ | Abs (s, T, t') =>
+ Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
+ in do_term [] [] Pos orig_t end
+
+(** Destruction of constructors **)
+
+val val_var_prefix = nitpick_prefix ^ "v"
+
+(* typ list -> int -> int -> int -> term -> term *)
+fun fresh_value_var Ts k n j t =
+ Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
+
+(* typ list -> int -> term -> bool *)
+fun has_heavy_bounds_or_vars Ts level t =
+ let
+ (* typ list -> bool *)
+ fun aux [] = false
+ | aux [T] = is_fun_type T orelse is_pair_type T
+ | aux _ = true
+ in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
+
+(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
+ -> term * term list *)
+fun pull_out_constr_comb thy Ts relax k level t args seen =
+ let val t_comb = list_comb (t, args) in
+ case t of
+ Const x =>
+ if not relax andalso is_constr thy x andalso
+ not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
+ has_heavy_bounds_or_vars Ts level t_comb andalso
+ not (loose_bvar (t_comb, level)) then
+ let
+ val (j, seen) = case find_index (curry (op =) t_comb) seen of
+ ~1 => (0, t_comb :: seen)
+ | j => (j, seen)
+ in (fresh_value_var Ts k (length seen) j t_comb, seen) end
+ else
+ (t_comb, seen)
+ | _ => (t_comb, seen)
+ end
+
+(* (term -> term) -> typ list -> int -> term list -> term list *)
+fun equations_for_pulled_out_constrs mk_eq Ts k seen =
+ let val n = length seen in
+ map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
+ (index_seq 0 n) seen
+ end
+
+(* theory -> bool -> term -> term *)
+fun pull_out_universal_constrs thy def t =
+ let
+ val k = maxidx_of_term t + 1
+ (* typ list -> bool -> term -> term list -> term list -> term * term list *)
+ fun do_term Ts def t args seen =
+ case t of
+ (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
+ do_eq_or_imp Ts true def t0 t1 t2 seen
+ | (t0 as @{const "==>"}) $ t1 $ t2 =>
+ if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
+ | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ do_eq_or_imp Ts true def t0 t1 t2 seen
+ | (t0 as @{const "op -->"}) $ t1 $ t2 =>
+ do_eq_or_imp Ts false def t0 t1 t2 seen
+ | Abs (s, T, t') =>
+ let val (t', seen) = do_term (T :: Ts) def t' [] seen in
+ (list_comb (Abs (s, T, t'), args), seen)
+ end
+ | t1 $ t2 =>
+ let val (t2, seen) = do_term Ts def t2 [] seen in
+ do_term Ts def t1 (t2 :: args) seen
+ end
+ | _ => pull_out_constr_comb thy Ts def k 0 t args seen
+ (* typ list -> bool -> bool -> term -> term -> term -> term list
+ -> term * term list *)
+ and do_eq_or_imp Ts eq def t0 t1 t2 seen =
+ let
+ val (t2, seen) = if eq andalso def then (t2, seen)
+ else do_term Ts false t2 [] seen
+ val (t1, seen) = do_term Ts false t1 [] seen
+ in (t0 $ t1 $ t2, seen) end
+ val (concl, seen) = do_term [] def t [] []
+ in
+ Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
+ seen, concl)
+ end
+
+(* term -> term -> term *)
+fun mk_exists v t =
+ HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
+
+(* theory -> term -> term *)
+fun pull_out_existential_constrs thy t =
+ let
+ val k = maxidx_of_term t + 1
+ (* typ list -> int -> term -> term list -> term list -> term * term list *)
+ fun aux Ts num_exists t args seen =
+ case t of
+ (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
+ let
+ val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
+ val n = length seen'
+ (* unit -> term list *)
+ fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
+ in
+ (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
+ |> List.foldl s_conj t1 |> fold mk_exists (vars ())
+ |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
+ end
+ | t1 $ t2 =>
+ let val (t2, seen) = aux Ts num_exists t2 [] seen in
+ aux Ts num_exists t1 (t2 :: args) seen
+ end
+ | Abs (s, T, t') =>
+ let
+ val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
+ in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
+ | _ =>
+ if num_exists > 0 then
+ pull_out_constr_comb thy Ts false k num_exists t args seen
+ else
+ (list_comb (t, args), seen)
+ in aux [] 0 t [] [] |> fst end
+
+(* hol_context -> bool -> term -> term *)
+fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t =
+ let
+ (* styp -> int *)
+ val num_occs_of_var =
+ fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
+ | _ => I) t (K 0)
+ (* bool -> term -> term *)
+ fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
+ aux_eq careful true t0 t1 t2
+ | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
+ t0 $ aux false t1 $ aux careful t2
+ | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
+ aux_eq careful true t0 t1 t2
+ | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
+ t0 $ aux false t1 $ aux careful t2
+ | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
+ | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
+ | aux _ t = t
+ (* bool -> bool -> term -> term -> term -> term *)
+ and aux_eq careful pass1 t0 t1 t2 =
+ ((if careful then
+ raise SAME ()
+ else if axiom andalso is_Var t2 andalso
+ num_occs_of_var (dest_Var t2) = 1 then
+ @{const True}
+ else case strip_comb t2 of
+ (* The first case is not as general as it could be. *)
+ (Const (@{const_name PairBox}, _),
+ [Const (@{const_name fst}, _) $ Var z1,
+ Const (@{const_name snd}, _) $ Var z2]) =>
+ if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
+ else raise SAME ()
+ | (Const (x as (s, T)), args) =>
+ let val arg_Ts = binder_types T in
+ if length arg_Ts = length args andalso
+ (is_constr thy x orelse s = @{const_name Pair} orelse
+ x = (@{const_name Suc}, nat_T --> nat_T)) andalso
+ (not careful orelse not (is_Var t1) orelse
+ String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
+ discriminate_value hol_ctxt x t1 ::
+ map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
+ |> foldr1 s_conj
+ else
+ raise SAME ()
+ end
+ | _ => raise SAME ())
+ |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
+ handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
+ else t0 $ aux false t2 $ aux false t1
+ (* styp -> term -> int -> typ -> term -> term *)
+ and sel_eq x t n nth_T nth_t =
+ HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
+ |> aux false
+ in aux axiom t end
+
+(** Destruction of universal and existential equalities **)
+
+(* term -> term *)
+fun curry_assms (@{const "==>"} $ (@{const Trueprop}
+ $ (@{const "op &"} $ t1 $ t2)) $ t3) =
+ curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
+ | curry_assms (@{const "==>"} $ t1 $ t2) =
+ @{const "==>"} $ curry_assms t1 $ curry_assms t2
+ | curry_assms t = t
+
+(* term -> term *)
+val destroy_universal_equalities =
+ let
+ (* term list -> (indexname * typ) list -> term -> term *)
+ fun aux prems zs t =
+ case t of
+ @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
+ | _ => Logic.list_implies (rev prems, t)
+ (* term list -> (indexname * typ) list -> term -> term -> term *)
+ and aux_implies prems zs t1 t2 =
+ case t1 of
+ Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
+ | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
+ aux_eq prems zs z t' t1 t2
+ | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
+ aux_eq prems zs z t' t1 t2
+ | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
+ (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
+ -> term -> term *)
+ and aux_eq prems zs z t' t1 t2 =
+ if not (member (op =) zs z) andalso
+ not (exists_subterm (curry (op =) (Var z)) t') then
+ aux prems zs (subst_free [(Var z, t')] t2)
+ else
+ aux (t1 :: prems) (Term.add_vars t1 zs) t2
+ in aux [] [] end
+
+(* theory -> int -> term list -> term list -> (term * term list) option *)
+fun find_bound_assign _ _ _ [] = NONE
+ | find_bound_assign thy j seen (t :: ts) =
+ let
+ (* bool -> term -> term -> (term * term list) option *)
+ fun aux pass1 t1 t2 =
+ (if loose_bvar1 (t2, j) then
+ if pass1 then aux false t2 t1 else raise SAME ()
+ else case t1 of
+ Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
+ | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
+ if j' = j andalso
+ s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
+ SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
+ ts @ seen)
+ else
+ raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () => find_bound_assign thy j (t :: seen) ts
+ in
+ case t of
+ Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
+ | _ => find_bound_assign thy j (t :: seen) ts
+ end
+
+(* int -> term -> term -> term *)
+fun subst_one_bound j arg t =
+ let
+ fun aux (Bound i, lev) =
+ if i < lev then raise SAME ()
+ else if i = lev then incr_boundvars (lev - j) arg
+ else Bound (i - 1)
+ | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
+ | aux (f $ t, lev) =
+ (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
+ handle SAME () => f $ aux (t, lev))
+ | aux _ = raise SAME ()
+ in aux (t, j) handle SAME () => t end
+
+(* theory -> term -> term *)
+fun destroy_existential_equalities thy =
+ let
+ (* string list -> typ list -> term list -> term *)
+ fun kill [] [] ts = foldr1 s_conj ts
+ | kill (s :: ss) (T :: Ts) ts =
+ (case find_bound_assign thy (length ss) [] ts of
+ SOME (_, []) => @{const True}
+ | SOME (arg_t, ts) =>
+ kill ss Ts (map (subst_one_bound (length ss)
+ (incr_bv (~1, length ss + 1, arg_t))) ts)
+ | NONE =>
+ Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
+ $ Abs (s, T, kill ss Ts ts))
+ | kill _ _ _ = raise UnequalLengths
+ (* string list -> typ list -> term -> term *)
+ fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
+ gather (ss @ [s1]) (Ts @ [T1]) t1
+ | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
+ | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
+ | gather [] [] t = t
+ | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t))
+ in gather [] [] end
+
+(** Skolemization **)
+
+(* int -> int -> string *)
+fun skolem_prefix_for k j =
+ skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
+
+(* hol_context -> int -> term -> term *)
+fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})
+ skolem_depth =
+ let
+ (* int list -> int list *)
+ val incrs = map (Integer.add 1)
+ (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
+ fun aux ss Ts js depth polar t =
+ let
+ (* string -> typ -> string -> typ -> term -> term *)
+ fun do_quantifier quant_s quant_T abs_s abs_T t =
+ if not (loose_bvar1 (t, 0)) then
+ aux ss Ts js depth polar (incr_boundvars ~1 t)
+ else if depth <= skolem_depth andalso
+ is_positive_existential polar quant_s then
+ let
+ val j = length (!skolems) + 1
+ val sko_s = skolem_prefix_for (length js) j ^ abs_s
+ val _ = Unsynchronized.change skolems (cons (sko_s, ss))
+ val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
+ map Bound (rev js))
+ val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
+ in
+ if null js then betapply (abs_t, sko_t)
+ else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
+ end
+ else
+ Const (quant_s, quant_T)
+ $ Abs (abs_s, abs_T,
+ if is_higher_order_type abs_T then
+ t
+ else
+ aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
+ (depth + 1) polar t)
+ in
+ case t of
+ Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier s0 T0 s1 T1 t1
+ | @{const "==>"} $ t1 $ t2 =>
+ @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
+ $ aux ss Ts js depth polar t2
+ | @{const Pure.conjunction} $ t1 $ t2 =>
+ @{const Pure.conjunction} $ aux ss Ts js depth polar t1
+ $ aux ss Ts js depth polar t2
+ | @{const Trueprop} $ t1 =>
+ @{const Trueprop} $ aux ss Ts js depth polar t1
+ | @{const Not} $ t1 =>
+ @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
+ | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier s0 T0 s1 T1 t1
+ | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
+ do_quantifier s0 T0 s1 T1 t1
+ | @{const "op &"} $ t1 $ t2 =>
+ @{const "op &"} $ aux ss Ts js depth polar t1
+ $ aux ss Ts js depth polar t2
+ | @{const "op |"} $ t1 $ t2 =>
+ @{const "op |"} $ aux ss Ts js depth polar t1
+ $ aux ss Ts js depth polar t2
+ | @{const "op -->"} $ t1 $ t2 =>
+ @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
+ $ aux ss Ts js depth polar t2
+ | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
+ t0 $ t1 $ aux ss Ts js depth polar t2
+ | Const (x as (s, T)) =>
+ if is_inductive_pred hol_ctxt x andalso
+ not (is_well_founded_inductive_pred hol_ctxt x) then
+ let
+ val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
+ val (pref, connective, set_oper) =
+ if gfp then
+ (lbfp_prefix,
+ @{const "op |"},
+ @{const_name upper_semilattice_fun_inst.sup_fun})
+ else
+ (ubfp_prefix,
+ @{const "op &"},
+ @{const_name lower_semilattice_fun_inst.inf_fun})
+ (* unit -> term *)
+ fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
+ |> aux ss Ts js depth polar
+ fun neg () = Const (pref ^ s, T)
+ in
+ (case polar |> gfp ? flip_polarity of
+ Pos => pos ()
+ | Neg => neg ()
+ | Neut =>
+ if is_fun_type T then
+ let
+ val ((trunk_arg_Ts, rump_arg_T), body_T) =
+ T |> strip_type |>> split_last
+ val set_T = rump_arg_T --> body_T
+ (* (unit -> term) -> term *)
+ fun app f =
+ list_comb (f (),
+ map Bound (length trunk_arg_Ts - 1 downto 0))
+ in
+ List.foldr absdummy
+ (Const (set_oper, set_T --> set_T --> set_T)
+ $ app pos $ app neg) trunk_arg_Ts
+ end
+ else
+ connective $ pos () $ neg ())
+ end
+ else
+ Const x
+ | t1 $ t2 =>
+ betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
+ aux ss Ts [] depth Neut t2)
+ | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
+ | _ => t
+ end
+ in aux [] [] [] 0 Pos end
+
+(** Function specialization **)
+
+(* term -> term list *)
+fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
+ | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
+ | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
+ snd (strip_comb t1)
+ | params_in_equation _ = []
+
+(* styp -> styp -> int list -> term list -> term list -> term -> term *)
+fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
+ let
+ val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
+ + 1
+ val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
+ val fixed_params = filter_indices fixed_js (params_in_equation t)
+ (* term list -> term -> term *)
+ fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
+ | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
+ | aux args t =
+ if t = Const x then
+ list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
+ else
+ let val j = find_index (curry (op =) t) fixed_params in
+ list_comb (if j >= 0 then nth fixed_args j else t, args)
+ end
+ in aux [] t end
+
+(* hol_context -> styp -> (int * term option) list *)
+fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =
+ let
+ (* term -> term list -> term list -> term list list *)
+ fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
+ | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
+ | fun_calls t args =
+ (case t of
+ Const (x' as (s', T')) =>
+ x = x' orelse (case AList.lookup (op =) ersatz_table s' of
+ SOME s'' => x = (s'', T')
+ | NONE => false)
+ | _ => false) ? cons args
+ (* term list list -> term list list -> term list -> term list list *)
+ fun call_sets [] [] vs = [vs]
+ | call_sets [] uss vs = vs :: call_sets uss [] []
+ | call_sets ([] :: _) _ _ = []
+ | call_sets ((t :: ts) :: tss) uss vs =
+ OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
+ val sets = call_sets (fun_calls t [] []) [] []
+ val indexed_sets = sets ~~ (index_seq 0 (length sets))
+ in
+ fold_rev (fn (set, j) =>
+ case set of
+ [Var _] => AList.lookup (op =) indexed_sets set = SOME j
+ ? cons (j, NONE)
+ | [t as Const _] => cons (j, SOME t)
+ | [t as Free _] => cons (j, SOME t)
+ | _ => I) indexed_sets []
+ end
+(* hol_context -> styp -> term list -> (int * term option) list *)
+fun static_args_in_terms hol_ctxt x =
+ map (static_args_in_term hol_ctxt x)
+ #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
+
+(* (int * term option) list -> (int * term) list -> int list *)
+fun overlapping_indices [] _ = []
+ | overlapping_indices _ [] = []
+ | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
+ if j1 < j2 then overlapping_indices ps1' ps2
+ else if j1 > j2 then overlapping_indices ps1 ps2'
+ else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
+
+(* typ list -> term -> bool *)
+fun is_eligible_arg Ts t =
+ let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
+ null bad_Ts orelse
+ (is_higher_order_type (fastype_of1 (Ts, t)) andalso
+ forall (not o is_higher_order_type) bad_Ts)
+ end
+
+(* int -> string *)
+fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
+
+(* If a constant's definition is picked up deeper than this threshold, we
+ prevent excessive specialization by not specializing it. *)
+val special_max_depth = 20
+
+val bound_var_prefix = "b"
+
+(* hol_context -> int -> term -> term *)
+fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table,
+ special_funs, ...}) depth t =
+ if not specialize orelse depth > special_max_depth then
+ t
+ else
+ let
+ val blacklist = if depth = 0 then []
+ else case term_under_def t of Const x => [x] | _ => []
+ (* term list -> typ list -> term -> term *)
+ fun aux args Ts (Const (x as (s, T))) =
+ ((if not (member (op =) blacklist x) andalso not (null args) andalso
+ not (String.isPrefix special_prefix s) andalso
+ is_equational_fun hol_ctxt x then
+ let
+ val eligible_args = filter (is_eligible_arg Ts o snd)
+ (index_seq 0 (length args) ~~ args)
+ val _ = not (null eligible_args) orelse raise SAME ()
+ val old_axs = equational_fun_axioms hol_ctxt x
+ |> map (destroy_existential_equalities thy)
+ val static_params = static_args_in_terms hol_ctxt x old_axs
+ val fixed_js = overlapping_indices static_params eligible_args
+ val _ = not (null fixed_js) orelse raise SAME ()
+ val fixed_args = filter_indices fixed_js args
+ val vars = fold Term.add_vars fixed_args []
+ |> sort (TermOrd.fast_indexname_ord o pairself fst)
+ val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
+ fixed_args []
+ |> sort int_ord
+ val live_args = filter_out_indices fixed_js args
+ val extra_args = map Var vars @ map Bound bound_js @ live_args
+ val extra_Ts = map snd vars @ filter_indices bound_js Ts
+ val k = maxidx_of_term t + 1
+ (* int -> term *)
+ fun var_for_bound_no j =
+ Var ((bound_var_prefix ^
+ nat_subscript (find_index (curry (op =) j) bound_js
+ + 1), k),
+ nth Ts j)
+ val fixed_args_in_axiom =
+ map (curry subst_bounds
+ (map var_for_bound_no (index_seq 0 (length Ts))))
+ fixed_args
+ in
+ case AList.lookup (op =) (!special_funs)
+ (x, fixed_js, fixed_args_in_axiom) of
+ SOME x' => list_comb (Const x', extra_args)
+ | NONE =>
+ let
+ val extra_args_in_axiom =
+ map Var vars @ map var_for_bound_no bound_js
+ val x' as (s', _) =
+ (special_prefix_for (length (!special_funs) + 1) ^ s,
+ extra_Ts @ filter_out_indices fixed_js (binder_types T)
+ ---> body_type T)
+ val new_axs =
+ map (specialize_fun_axiom x x' fixed_js
+ fixed_args_in_axiom extra_args_in_axiom) old_axs
+ val _ =
+ Unsynchronized.change special_funs
+ (cons ((x, fixed_js, fixed_args_in_axiom), x'))
+ val _ = add_simps simp_table s' new_axs
+ in list_comb (Const x', extra_args) end
+ end
+ else
+ raise SAME ())
+ handle SAME () => list_comb (Const x, args))
+ | aux args Ts (Abs (s, T, t)) =
+ list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
+ | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
+ | aux args _ t = list_comb (t, args)
+ in aux [] [] t end
+
+type special_triple = int list * term list * styp
+
+val cong_var_prefix = "c"
+
+(* styp -> special_triple -> special_triple -> term *)
+fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
+ let
+ val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
+ val Ts = binder_types T
+ val max_j = fold (fold Integer.max) [js1, js2] ~1
+ val (eqs, (args1, args2)) =
+ fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
+ (js1 ~~ ts1, js2 ~~ ts2) of
+ (SOME t1, SOME t2) => apfst (cons (t1, t2))
+ | (SOME t1, NONE) => apsnd (apsnd (cons t1))
+ | (NONE, SOME t2) => apsnd (apfst (cons t2))
+ | (NONE, NONE) =>
+ let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
+ nth Ts j) in
+ apsnd (pairself (cons v))
+ end) (max_j downto 0) ([], ([], []))
+ in
+ Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
+ |> map Logic.mk_equals,
+ Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
+ list_comb (Const x2, bounds2 @ args2)))
+ |> Refute.close_form (* TODO: needed? *)
+ end
+
+(* hol_context -> styp list -> term list *)
+fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =
+ let
+ val groups =
+ !special_funs
+ |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
+ |> AList.group (op =)
+ |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
+ |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
+ (* special_triple -> int *)
+ fun generality (js, _, _) = ~(length js)
+ (* special_triple -> special_triple -> bool *)
+ fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
+ x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
+ (j2 ~~ t2, j1 ~~ t1)
+ (* styp -> special_triple list -> special_triple list -> special_triple list
+ -> term list -> term list *)
+ fun do_pass_1 _ [] [_] [_] = I
+ | do_pass_1 x skipped _ [] = do_pass_2 x skipped
+ | do_pass_1 x skipped all (z :: zs) =
+ case filter (is_more_specific z) all
+ |> sort (int_ord o pairself generality) of
+ [] => do_pass_1 x (z :: skipped) all zs
+ | (z' :: _) => cons (special_congruence_axiom x z z')
+ #> do_pass_1 x skipped all zs
+ (* styp -> special_triple list -> term list -> term list *)
+ and do_pass_2 _ [] = I
+ | do_pass_2 x (z :: zs) =
+ fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
+ in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
+
+(** Axiom selection **)
+
+(* Similar to "Refute.specialize_type" but returns all matches rather than only
+ the first (preorder) match. *)
+(* theory -> styp -> term -> term list *)
+fun multi_specialize_type thy slack (x as (s, T)) t =
+ let
+ (* term -> (typ * term) list -> (typ * term) list *)
+ fun aux (Const (s', T')) ys =
+ if s = s' then
+ ys |> (if AList.defined (op =) ys T' then
+ I
+ else
+ cons (T', Refute.monomorphic_term
+ (Sign.typ_match thy (T', T) Vartab.empty) t)
+ handle Type.TYPE_MATCH => I
+ | Refute.REFUTE _ =>
+ if slack then
+ I
+ else
+ raise NOT_SUPPORTED ("too much polymorphism in \
+ \axiom involving " ^ quote s))
+ else
+ ys
+ | aux _ ys = ys
+ in map snd (fold_aterms aux t []) end
+
+(* theory -> bool -> const_table -> styp -> term list *)
+fun nondef_props_for_const thy slack table (x as (s, _)) =
+ these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
+
+(* 'a Symtab.table -> 'a list *)
+fun all_table_entries table = Symtab.fold (append o snd) table []
+(* const_table -> string -> const_table *)
+fun extra_table table s = Symtab.make [(s, all_table_entries table)]
+
+(* int -> term -> term *)
+fun eval_axiom_for_term j t =
+ Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
+
+(* term -> bool *)
+val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
+
+(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
+val axioms_max_depth = 255
+
+(* hol_context -> term -> (term list * term list) * (bool * bool) *)
+fun axioms_for_term
+ (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
+ def_table, nondef_table, user_nondefs, ...}) t =
+ let
+ type accumulator = styp list * (term list * term list)
+ (* (term list * term list -> term list)
+ -> ((term list -> term list) -> term list * term list
+ -> term list * term list)
+ -> int -> term -> accumulator -> accumulator *)
+ fun add_axiom get app depth t (accum as (xs, axs)) =
+ let
+ val t = t |> unfold_defs_in_term hol_ctxt
+ |> skolemize_term_and_more hol_ctxt ~1
+ in
+ if is_trivial_equation t then
+ accum
+ else
+ let val t' = t |> specialize_consts_in_term hol_ctxt depth in
+ if exists (member (op aconv) (get axs)) [t, t'] then accum
+ else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
+ end
+ end
+ (* int -> term -> accumulator -> accumulator *)
+ and add_def_axiom depth = add_axiom fst apfst depth
+ and add_nondef_axiom depth = add_axiom snd apsnd depth
+ and add_maybe_def_axiom depth t =
+ (if head_of t <> @{const "==>"} then add_def_axiom
+ else add_nondef_axiom) depth t
+ and add_eq_axiom depth t =
+ (if is_constr_pattern_formula thy t then add_def_axiom
+ else add_nondef_axiom) depth t
+ (* int -> term -> accumulator -> accumulator *)
+ and add_axioms_for_term depth t (accum as (xs, axs)) =
+ case t of
+ t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
+ | Const (x as (s, T)) =>
+ (if member (op =) xs x orelse is_built_in_const fast_descrs x then
+ accum
+ else
+ let val accum as (xs, _) = (x :: xs, axs) in
+ if depth > axioms_max_depth then
+ raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
+ \add_axioms_for_term",
+ "too many nested axioms (" ^
+ string_of_int depth ^ ")")
+ else if Refute.is_const_of_class thy x then
+ let
+ val class = Logic.class_of_const s
+ val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
+ class)
+ val ax1 = try (Refute.specialize_type thy x) of_class
+ val ax2 = Option.map (Refute.specialize_type thy x o snd)
+ (Refute.get_classdef thy class)
+ in
+ fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
+ accum
+ end
+ else if is_constr thy x then
+ accum
+ else if is_equational_fun hol_ctxt x then
+ fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
+ accum
+ else if is_abs_fun thy x then
+ if is_quot_type thy (range_type T) then
+ raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
+ else
+ accum |> fold (add_nondef_axiom depth)
+ (nondef_props_for_const thy false nondef_table x)
+ |> is_funky_typedef thy (range_type T)
+ ? fold (add_maybe_def_axiom depth)
+ (nondef_props_for_const thy true
+ (extra_table def_table s) x)
+ else if is_rep_fun thy x then
+ if is_quot_type thy (domain_type T) then
+ raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
+ else
+ accum |> fold (add_nondef_axiom depth)
+ (nondef_props_for_const thy false nondef_table x)
+ |> is_funky_typedef thy (range_type T)
+ ? fold (add_maybe_def_axiom depth)
+ (nondef_props_for_const thy true
+ (extra_table def_table s) x)
+ |> add_axioms_for_term depth
+ (Const (mate_of_rep_fun thy x))
+ |> fold (add_def_axiom depth)
+ (inverse_axioms_for_rep_fun thy x)
+ else
+ accum |> user_axioms <> SOME false
+ ? fold (add_nondef_axiom depth)
+ (nondef_props_for_const thy false nondef_table x)
+ end)
+ |> add_axioms_for_type depth T
+ | Free (_, T) => add_axioms_for_type depth T accum
+ | Var (_, T) => add_axioms_for_type depth T accum
+ | Bound _ => accum
+ | Abs (_, T, t) => accum |> add_axioms_for_term depth t
+ |> add_axioms_for_type depth T
+ (* int -> typ -> accumulator -> accumulator *)
+ and add_axioms_for_type depth T =
+ case T of
+ Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
+ | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
+ | @{typ prop} => I
+ | @{typ bool} => I
+ | @{typ unit} => I
+ | TFree (_, S) => add_axioms_for_sort depth T S
+ | TVar (_, S) => add_axioms_for_sort depth T S
+ | Type (z as (s, Ts)) =>
+ fold (add_axioms_for_type depth) Ts
+ #> (if is_pure_typedef thy T then
+ fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
+ else if is_quot_type thy T then
+ fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
+ else if max_bisim_depth >= 0 andalso is_codatatype thy T then
+ fold (add_maybe_def_axiom depth)
+ (codatatype_bisim_axioms hol_ctxt T)
+ else
+ I)
+ (* int -> typ -> sort -> accumulator -> accumulator *)
+ and add_axioms_for_sort depth T S =
+ let
+ val supers = Sign.complete_sort thy S
+ val class_axioms =
+ maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
+ handle ERROR _ => [])) supers
+ val monomorphic_class_axioms =
+ map (fn t => case Term.add_tvars t [] of
+ [] => t
+ | [(x, S)] =>
+ Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
+ | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
+ \add_axioms_for_sort", [t]))
+ class_axioms
+ in fold (add_nondef_axiom depth) monomorphic_class_axioms end
+ val (mono_user_nondefs, poly_user_nondefs) =
+ List.partition (null o Term.hidden_polymorphism) user_nondefs
+ val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
+ evals
+ val (xs, (defs, nondefs)) =
+ ([], ([], [])) |> add_axioms_for_term 1 t
+ |> fold_rev (add_def_axiom 1) eval_axioms
+ |> user_axioms = SOME true
+ ? fold (add_nondef_axiom 1) mono_user_nondefs
+ val defs = defs @ special_congruence_axioms hol_ctxt xs
+ in
+ ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
+ null poly_user_nondefs))
+ end
+
+(** Simplification of constructor/selector terms **)
+
+(* theory -> term -> term *)
+fun simplify_constrs_and_sels thy t =
+ let
+ (* term -> int -> term *)
+ fun is_nth_sel_on t' n (Const (s, _) $ t) =
+ (t = t' andalso is_sel_like_and_no_discr s andalso
+ sel_no_from_name s = n)
+ | is_nth_sel_on _ _ _ = false
+ (* term -> term list -> term *)
+ fun do_term (Const (@{const_name Rep_Frac}, _)
+ $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
+ | do_term (Const (@{const_name Abs_Frac}, _)
+ $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
+ | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
+ | do_term (t as Const (x as (s, T))) (args as _ :: _) =
+ ((if is_constr_like thy x then
+ if length args = num_binder_types T then
+ case hd args of
+ Const (x' as (_, T')) $ t' =>
+ if domain_type T' = body_type T andalso
+ forall (uncurry (is_nth_sel_on t'))
+ (index_seq 0 (length args) ~~ args) then
+ t'
+ else
+ raise SAME ()
+ | _ => raise SAME ()
+ else
+ raise SAME ()
+ else if is_sel_like_and_no_discr s then
+ case strip_comb (hd args) of
+ (Const (x' as (s', T')), ts') =>
+ if is_constr_like thy x' andalso
+ constr_name_for_sel_like s = s' andalso
+ not (exists is_pair_type (binder_types T')) then
+ list_comb (nth ts' (sel_no_from_name s), tl args)
+ else
+ raise SAME ()
+ | _ => raise SAME ()
+ else
+ raise SAME ())
+ handle SAME () => betapplys (t, args))
+ | do_term (Abs (s, T, t')) args =
+ betapplys (Abs (s, T, do_term t' []), args)
+ | do_term t args = betapplys (t, args)
+ in do_term t [] end
+
+(** Quantifier massaging: Distributing quantifiers **)
+
+(* term -> term *)
+fun distribute_quantifiers t =
+ case t of
+ (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
+ (case t1 of
+ (t10 as @{const "op &"}) $ t11 $ t12 =>
+ t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
+ $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
+ | (t10 as @{const Not}) $ t11 =>
+ t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
+ $ Abs (s, T1, t11))
+ | t1 =>
+ if not (loose_bvar1 (t1, 0)) then
+ distribute_quantifiers (incr_boundvars ~1 t1)
+ else
+ t0 $ Abs (s, T1, distribute_quantifiers t1))
+ | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
+ (case distribute_quantifiers t1 of
+ (t10 as @{const "op |"}) $ t11 $ t12 =>
+ t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
+ $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
+ | (t10 as @{const "op -->"}) $ t11 $ t12 =>
+ t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
+ $ Abs (s, T1, t11))
+ $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
+ | (t10 as @{const Not}) $ t11 =>
+ t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
+ $ Abs (s, T1, t11))
+ | t1 =>
+ if not (loose_bvar1 (t1, 0)) then
+ distribute_quantifiers (incr_boundvars ~1 t1)
+ else
+ t0 $ Abs (s, T1, distribute_quantifiers t1))
+ | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
+ | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
+ | _ => t
+
+(** Quantifier massaging: Pushing quantifiers inward **)
+
+(* int -> int -> (int -> int) -> term -> term *)
+fun renumber_bounds j n f t =
+ case t of
+ t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
+ | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
+ | Bound j' =>
+ Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
+ | _ => t
+
+(* Maximum number of quantifiers in a cluster for which the exponential
+ algorithm is used. Larger clusters use a heuristic inspired by Claessen &
+ Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
+ paper). *)
+val quantifier_cluster_threshold = 7
+
+(* theory -> term -> term *)
+fun push_quantifiers_inward thy =
+ let
+ (* string -> string list -> typ list -> term -> term *)
+ fun aux quant_s ss Ts t =
+ (case t of
+ (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
+ if s0 = quant_s then
+ aux s0 (s1 :: ss) (T1 :: Ts) t1
+ else if quant_s = "" andalso
+ (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
+ aux s0 [s1] [T1] t1
+ else
+ raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () =>
+ case t of
+ t1 $ t2 =>
+ if quant_s = "" then
+ aux "" [] [] t1 $ aux "" [] [] t2
+ else
+ let
+ val typical_card = 4
+ (* ('a -> ''b list) -> 'a list -> ''b list *)
+ fun big_union proj ps =
+ fold (fold (insert (op =)) o proj) ps []
+ val (ts, connective) = strip_any_connective t
+ val T_costs =
+ map (bounded_card_of_type 65536 typical_card []) Ts
+ val t_costs = map size_of_term ts
+ val num_Ts = length Ts
+ (* int -> int *)
+ val flip = curry (op -) (num_Ts - 1)
+ val t_boundss = map (map flip o loose_bnos) ts
+ (* (int list * int) list -> int list
+ -> (int list * int) list *)
+ fun merge costly_boundss [] = costly_boundss
+ | merge costly_boundss (j :: js) =
+ let
+ val (yeas, nays) =
+ List.partition (fn (bounds, _) =>
+ member (op =) bounds j)
+ costly_boundss
+ val yeas_bounds = big_union fst yeas
+ val yeas_cost = Integer.sum (map snd yeas)
+ * nth T_costs j
+ in merge ((yeas_bounds, yeas_cost) :: nays) js end
+ (* (int list * int) list -> int list -> int *)
+ val cost = Integer.sum o map snd oo merge
+ (* (int list * int) list -> int list -> int list *)
+ fun heuristically_best_permutation _ [] = []
+ | heuristically_best_permutation costly_boundss js =
+ let
+ val (costly_boundss, (j, js)) =
+ js |> map (`(merge costly_boundss o single))
+ |> sort (int_ord
+ o pairself (Integer.sum o map snd o fst))
+ |> split_list |>> hd ||> pairf hd tl
+ in
+ j :: heuristically_best_permutation costly_boundss js
+ end
+ val js =
+ if length Ts <= quantifier_cluster_threshold then
+ all_permutations (index_seq 0 num_Ts)
+ |> map (`(cost (t_boundss ~~ t_costs)))
+ |> sort (int_ord o pairself fst) |> hd |> snd
+ else
+ heuristically_best_permutation (t_boundss ~~ t_costs)
+ (index_seq 0 num_Ts)
+ val back_js = map (fn j => find_index (curry (op =) j) js)
+ (index_seq 0 num_Ts)
+ val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
+ ts
+ (* (term * int list) list -> term *)
+ fun mk_connection [] =
+ raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\
+ \mk_connection", "")
+ | mk_connection ts_cum_bounds =
+ ts_cum_bounds |> map fst
+ |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
+ (* (term * int list) list -> int list -> term *)
+ fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
+ | build ts_cum_bounds (j :: js) =
+ let
+ val (yeas, nays) =
+ List.partition (fn (_, bounds) =>
+ member (op =) bounds j)
+ ts_cum_bounds
+ ||> map (apfst (incr_boundvars ~1))
+ in
+ if null yeas then
+ build nays js
+ else
+ let val T = nth Ts (flip j) in
+ build ((Const (quant_s, (T --> bool_T) --> bool_T)
+ $ Abs (nth ss (flip j), T,
+ mk_connection yeas),
+ big_union snd yeas) :: nays) js
+ end
+ end
+ in build (ts ~~ t_boundss) js end
+ | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
+ | _ => t
+ in aux "" [] [] end
+
+(** Preprocessor entry point **)
+
+(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)
+fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
+ skolemize, uncurry, ...}) t =
+ let
+ val skolem_depth = if skolemize then 4 else ~1
+ val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
+ core_t) = t |> unfold_defs_in_term hol_ctxt
+ |> Refute.close_form
+ |> skolemize_term_and_more hol_ctxt skolem_depth
+ |> specialize_consts_in_term hol_ctxt 0
+ |> `(axioms_for_term hol_ctxt)
+ val binarize =
+ case binary_ints of
+ SOME false => false
+ | _ =>
+ forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
+ (binary_ints = SOME true orelse
+ exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+ val box = exists (not_equal (SOME false) o snd) boxes
+ val table =
+ Termtab.empty |> uncurry
+ ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
+ (* bool -> bool -> term -> term *)
+ fun do_rest def core =
+ binarize ? binarize_nat_and_int_in_term
+ #> uncurry ? uncurry_term table
+ #> box ? box_fun_and_pair_in_term hol_ctxt def
+ #> destroy_constrs ? (pull_out_universal_constrs thy def
+ #> pull_out_existential_constrs thy
+ #> destroy_pulled_out_constrs hol_ctxt def)
+ #> curry_assms
+ #> destroy_universal_equalities
+ #> destroy_existential_equalities thy
+ #> simplify_constrs_and_sels thy
+ #> distribute_quantifiers
+ #> push_quantifiers_inward thy
+ #> not core ? Refute.close_form
+ #> Term.map_abs_vars shortest_name
+ in
+ (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
+ (got_all_mono_user_axioms, no_poly_user_axioms)),
+ do_rest false true core_t)
+ end
+
+end;
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 04 14:45:08 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Feb 05 11:15:16 2010 +0100
@@ -8,7 +8,7 @@
signature NITPICK_SCOPE =
sig
type styp = Nitpick_Util.styp
- type extended_context = Nitpick_HOL.extended_context
+ type hol_context = Nitpick_HOL.hol_context
type constr_spec = {
const: styp,
@@ -28,7 +28,7 @@
constrs: constr_spec list}
type scope = {
- ext_ctxt: extended_context,
+ hol_ctxt: hol_context,
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
@@ -47,7 +47,7 @@
val scopes_equivalent : scope -> scope -> bool
val scope_less_eq : scope -> scope -> bool
val all_scopes :
- extended_context -> int -> (typ option * int list) list
+ hol_context -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list
-> int list -> int list -> typ list -> typ list -> typ list
-> int * scope list
@@ -77,7 +77,7 @@
constrs: constr_spec list}
type scope = {
- ext_ctxt: extended_context,
+ hol_ctxt: hol_context,
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
@@ -131,7 +131,7 @@
(* (string -> string) -> scope
-> string list * string list * string list * string list * string list *)
-fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
+fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
bits, bisim_depth, datatypes, ...} : scope) =
let
val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
@@ -240,10 +240,9 @@
val max_bits = 31 (* Kodkod limit *)
-(* extended_context -> (typ option * int list) list
- -> (styp option * int list) list -> (styp option * int list) list -> int list
- -> int list -> typ -> block *)
-fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns
+(* hol_context -> (typ option * int list) list -> (styp option * int list) list
+ -> (styp option * int list) list -> int list -> int list -> typ -> block *)
+fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
iters_assigns bitss bisim_depths T =
if T = @{typ unsigned_bit} then
[(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
@@ -261,18 +260,18 @@
(const_for_iterator_type T)))]
else
(Card T, lookup_type_ints_assign thy cards_assigns T) ::
- (case datatype_constrs ext_ctxt T of
+ (case datatype_constrs hol_ctxt T of
[_] => []
| constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
-(* extended_context -> (typ option * int list) list
- -> (styp option * int list) list -> (styp option * int list) list -> int list
- -> int list -> typ list -> typ list -> block list *)
-fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns bitss
+(* hol_context -> (typ option * int list) list -> (styp option * int list) list
+ -> (styp option * int list) list -> int list -> int list -> typ list
+ -> typ list -> block list *)
+fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
bisim_depths mono_Ts nonmono_Ts =
let
(* typ -> block *)
- val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns
+ val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
iters_assigns bitss bisim_depths
val mono_block = maps block_for mono_Ts
val nonmono_blocks = map block_for nonmono_Ts
@@ -313,10 +312,10 @@
type scope_desc = (typ * int) list * (styp * int) list
-(* extended_context -> scope_desc -> typ * int -> bool *)
-fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns)
+(* hol_context -> scope_desc -> typ * int -> bool *)
+fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
(T, k) =
- case datatype_constrs ext_ctxt T of
+ case datatype_constrs hol_ctxt T of
[] => false
| xs =>
let
@@ -329,20 +328,20 @@
| effective_max card max = Int.min (card, max)
val max = map2 effective_max dom_cards maxes |> Integer.sum
in max < k end
-(* extended_context -> (typ * int) list -> (typ * int) list
- -> (styp * int) list -> bool *)
-fun is_surely_inconsistent_scope_description ext_ctxt seen rest max_assigns =
- exists (is_surely_inconsistent_card_assign ext_ctxt
+(* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
+ -> bool *)
+fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
+ exists (is_surely_inconsistent_card_assign hol_ctxt
(seen @ rest, max_assigns)) seen
-(* extended_context -> scope_desc -> (typ * int) list option *)
-fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) =
+(* hol_context -> scope_desc -> (typ * int) list option *)
+fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
let
(* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
fun aux seen [] = SOME seen
| aux seen ((T, 0) :: _) = NONE
| aux seen ((T, k) :: rest) =
- (if is_surely_inconsistent_scope_description ext_ctxt ((T, k) :: seen)
+ (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
rest max_assigns then
raise SAME ()
else
@@ -374,12 +373,12 @@
(* block -> scope_desc *)
fun scope_descriptor_from_block block =
fold_rev add_row_to_scope_descriptor block ([], [])
-(* extended_context -> block list -> int list -> scope_desc option *)
-fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
+(* hol_context -> block list -> int list -> scope_desc option *)
+fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
let
val (card_assigns, max_assigns) =
maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
- val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns)
+ val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
|> the
in
SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
@@ -427,15 +426,21 @@
{delta = delta, epsilon = delta, exclusive = true, total = false}
end
else if not co andalso num_self_recs > 0 then
- if not self_rec andalso num_non_self_recs = 1 andalso
- domain_card 2 card_assigns T = 1 then
- {delta = 0, epsilon = 1,
- exclusive = (s = @{const_name Nil} andalso length constrs = 2),
- total = true}
- else if s = @{const_name Cons} andalso length constrs = 2 then
- {delta = 1, epsilon = card, exclusive = true, total = false}
- else
- {delta = 0, epsilon = card, exclusive = false, total = false}
+ (if num_self_recs = 1 andalso num_non_self_recs = 1 then
+ if self_rec then
+ case constrs of
+ [{delta = 0, epsilon = 1, exclusive = true, ...}] =>
+ {delta = 1, epsilon = card, exclusive = true, total = false}
+ | _ => raise SAME ()
+ else
+ if domain_card 2 card_assigns T = 1 then
+ {delta = 0, epsilon = 1, exclusive = true, total = true}
+ else
+ raise SAME ()
+ else
+ raise SAME ())
+ handle SAME () =>
+ {delta = 0, epsilon = card, exclusive = false, total = false}
else if card = sum_dom_cards (card + 1) then
let val delta = next_delta () in
{delta = delta, epsilon = delta + domain_card card card_assigns T,
@@ -449,31 +454,32 @@
explicit_max = max, total = total} :: constrs
end
-(* extended_context -> (typ * int) list -> typ -> bool *)
-fun has_exact_card ext_ctxt card_assigns T =
+(* hol_context -> (typ * int) list -> typ -> bool *)
+fun has_exact_card hol_ctxt card_assigns T =
let val card = card_of_type card_assigns T in
- card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T
+ card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
end
-(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
-fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) deep_dataTs
+(* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
+fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
(desc as (card_assigns, _)) (T, card) =
let
val deep = member (op =) deep_dataTs T
val co = is_codatatype thy T
- val xs = boxed_datatype_constrs ext_ctxt T
+ val xs = boxed_datatype_constrs hol_ctxt T
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
List.partition I self_recs |> pairself length
- val complete = has_exact_card ext_ctxt card_assigns T
+ val complete = has_exact_card hol_ctxt card_assigns T
val concrete = xs |> maps (binder_types o snd) |> maps binder_types
- |> forall (has_exact_card ext_ctxt card_assigns)
+ |> forall (has_exact_card hol_ctxt card_assigns)
(* int -> int *)
fun sum_dom_cards max =
map (domain_card max card_assigns o snd) xs |> Integer.sum
val constrs =
fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
- num_non_self_recs) (self_recs ~~ xs) []
+ num_non_self_recs)
+ (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
in
{typ = T, card = card, co = co, complete = complete, concrete = concrete,
deep = deep, constrs = constrs}
@@ -487,12 +493,12 @@
min_bits_for_nat_value (fold Integer.max
(map snd card_assigns @ map snd max_assigns) 0)
-(* extended_context -> int -> typ list -> scope_desc -> scope *)
-fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break deep_dataTs
+(* hol_context -> int -> typ list -> scope_desc -> scope *)
+fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
(desc as (card_assigns, _)) =
let
val datatypes =
- map (datatype_spec_from_scope_descriptor ext_ctxt deep_dataTs desc)
+ map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
(filter (is_datatype thy o fst) card_assigns)
val bits = card_of_type card_assigns @{typ signed_bit} - 1
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
@@ -500,7 +506,7 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
in
- {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes,
+ {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
bits = bits, bisim_depth = bisim_depth,
ofs = if sym_break <= 0 then Typtab.empty
else offset_table_for_card_assigns thy card_assigns datatypes}
@@ -521,26 +527,26 @@
val max_scopes = 4096
val distinct_threshold = 512
-(* extended_context -> int -> (typ option * int list) list
+(* hol_context -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list -> int list
-> typ list -> typ list -> typ list -> int * scope list *)
-fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
+fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
let
val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
cards_assigns
- val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns
+ val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
iters_assigns bitss bisim_depths mono_Ts
nonmono_Ts
val ranks = map rank_of_block blocks
val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
val head = take max_scopes all
- val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
+ val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
head
in
(length all - length head,
descs |> length descs <= distinct_threshold ? distinct (op =)
- |> map (scope_from_descriptor ext_ctxt sym_break deep_dataTs))
+ |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))
end
end;