--- a/src/HOL/Refute.thy Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Refute.thy Mon Dec 14 12:31:00 2009 +0100
@@ -61,7 +61,8 @@
(* ------------------------------------------------------------------------- *)
(* PARAMETERS *)
(* *)
-(* The following global parameters are currently supported (and required): *)
+(* The following global parameters are currently supported (and required, *)
+(* except for "expect"): *)
(* *)
(* Name Type Description *)
(* *)
@@ -75,6 +76,10 @@
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *)
(* This value is ignored under some ML compilers. *)
(* "satsolver" string Name of the SAT solver to be used. *)
+(* "no_assms" bool If "true", assumptions in structured proofs are *)
+(* not considered. *)
+(* "expect" string Expected result ("genuine", "potential", "none", or *)
+(* "unknown"). *)
(* *)
(* See 'HOL/SAT.thy' for default values. *)
(* *)
--- a/src/HOL/SAT.thy Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/SAT.thy Mon Dec 14 12:31:00 2009 +0100
@@ -23,7 +23,8 @@
maxsize=8,
maxvars=10000,
maxtime=60,
- satsolver="auto"]
+ satsolver="auto",
+ no_assms="false"]
ML {* structure sat = SATFunc(cnf) *}
--- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Mon Dec 14 12:31:00 2009 +0100
@@ -996,7 +996,7 @@
(* bool -> Time.time option -> int -> int -> problem list -> outcome *)
fun solve_any_problem overlord deadline max_threads max_solutions problems =
let
- val j = find_index (equal True o #formula) problems
+ val j = find_index (curry (op =) True o #formula) problems
val indexed_problems = if j >= 0 then
[(j, nth problems j)]
else
--- a/src/HOL/Tools/Nitpick/minipick.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/Nitpick/minipick.ML Mon Dec 14 12:31:00 2009 +0100
@@ -232,7 +232,7 @@
| Const (@{const_name snd}, _) => raise SAME ()
| Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
| Free (x as (_, T)) =>
- Rel (arity_of RRep card T, find_index (equal x) frees)
+ Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
| Term.Var _ => raise NOT_SUPPORTED "schematic variables"
| Bound j => raise SAME ()
| Abs (_, T, t') =>
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 14 12:31:00 2009 +0100
@@ -133,7 +133,7 @@
[Pretty.str (s ^ plural_s_for_list ts ^ ":"),
Pretty.indent indent_size (Pretty.chunks
(map2 (fn j => fn t =>
- Pretty.block [t |> shorten_const_names_in_term
+ Pretty.block [t |> shorten_names_in_term
|> Syntax.pretty_term ctxt,
Pretty.str (if j = 1 then "." else ";")])
(length ts downto 1) ts))]
@@ -315,7 +315,7 @@
(core_u :: def_us @ nondef_us)
*)
- val unique_scope = forall (equal 1 o length o snd) cards_assigns
+ val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
(* typ -> bool *)
fun is_free_type_monotonic T =
unique_scope orelse
@@ -331,7 +331,7 @@
orelse is_number_type thy T
orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
fun is_datatype_shallow T =
- not (exists (equal T o domain_type o type_of) sel_names)
+ not (exists (curry (op =) T o domain_type o type_of) sel_names)
val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
|> sort TermOrd.typ_ord
val (all_dataTs, all_free_Ts) =
@@ -375,8 +375,9 @@
val need_incremental = Int.max (max_potential, max_genuine) >= 2
val effective_sat_solver =
if sat_solver <> "smart" then
- if need_incremental andalso
- not (sat_solver mem Kodkod_SAT.configured_sat_solvers true) then
+ if need_incremental
+ andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
+ sat_solver) then
(print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
\be used instead of " ^ quote sat_solver ^ "."));
"SAT4J")
@@ -418,7 +419,7 @@
val main_j0 = offset_of_type ofs bool_T
val (nat_card, nat_j0) = spec_of_type scope nat_T
val (int_card, int_j0) = spec_of_type scope int_T
- val _ = forall (equal main_j0) [nat_j0, int_j0]
+ val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0)
orelse raise BAD ("Nitpick.pick_them_nits_in_term.\
\problem_for_scope", "bad offsets")
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0
@@ -663,7 +664,8 @@
let
val num_genuine = take max_potential lib_ps
|> map (print_and_check false)
- |> filter (equal (SOME true)) |> length
+ |> filter (curry (op =) (SOME true))
+ |> length
val max_genuine = max_genuine - num_genuine
val max_potential = max_potential
- (length lib_ps - num_genuine)
@@ -859,8 +861,8 @@
error "Nitpick was interrupted."
(* Proof.state -> params -> bool -> term -> string * Proof.state *)
-fun pick_nits_in_term state (params as {debug, timeout, expect, ...})
- auto orig_assm_ts orig_t =
+fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto
+ orig_assm_ts orig_t =
if getenv "KODKODI" = "" then
(if auto then ()
else warning (Pretty.string_of (plazy install_kodkodi_message));
@@ -878,7 +880,7 @@
end
(* Proof.state -> params -> thm -> int -> string * Proof.state *)
-fun pick_nits_in_subgoal state params auto subgoal =
+fun pick_nits_in_subgoal state params auto i =
let
val ctxt = Proof.context_of state
val t = state |> Proof.raw_goal |> #goal |> prop_of
@@ -888,7 +890,7 @@
else
let
val assms = map term_of (Assumption.all_assms_of ctxt)
- val (t, frees) = Logic.goal_params t subgoal
+ val (t, frees) = Logic.goal_params t i
in pick_nits_in_term state params auto assms (subst_bounds (frees, t)) end
end
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Dec 14 12:31:00 2009 +0100
@@ -52,9 +52,9 @@
val unbox_type : typ -> typ
val string_for_type : Proof.context -> typ -> string
val prefix_name : string -> string -> string
+ val shortest_name : string -> string
val short_name : string -> string
- val short_const_name : string -> string
- val shorten_const_names_in_term : term -> term
+ val shorten_names_in_term : term -> term
val type_match : theory -> typ * typ -> bool
val const_match : theory -> styp * styp -> bool
val term_match : theory -> term * term -> bool
@@ -197,12 +197,14 @@
(* term * term -> term *)
fun s_conj (t1, @{const True}) = t1
| s_conj (@{const True}, t2) = t2
- | s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False}
- else HOLogic.mk_conj (t1, t2)
+ | s_conj (t1, t2) =
+ if t1 = @{const False} orelse t2 = @{const False} then @{const False}
+ else HOLogic.mk_conj (t1, t2)
fun s_disj (t1, @{const False}) = t1
| s_disj (@{const False}, t2) = t2
- | s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True}
- else HOLogic.mk_disj (t1, t2)
+ | 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)
@@ -213,7 +215,7 @@
| strip_connective _ t = [t]
(* term -> term list * term *)
fun strip_any_connective (t as (t0 $ t1 $ t2)) =
- if t0 mem [@{const "op &"}, @{const "op |"}] then
+ if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
(strip_connective t0 t, t0)
else
([t], @{const Not})
@@ -347,19 +349,24 @@
(* string -> string -> string *)
val prefix_name = Long_Name.qualify o Long_Name.base_name
(* string -> string *)
-fun short_name s = List.last (space_explode "." s) handle List.Empty => ""
+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 short_name
+val shorten_abs_vars = Term.map_abs_vars shortest_name
(* string -> string *)
-fun short_const_name s =
+fun short_name s =
case space_explode name_sep s of
[_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
- | ss => map short_name ss |> space_implode "_"
+ | ss => map shortest_name ss |> space_implode "_"
+(* typ -> typ *)
+fun shorten_names_in_type (Type (s, Ts)) =
+ Type (short_name s, map shorten_names_in_type Ts)
+ | shorten_names_in_type T = T
(* term -> term *)
-val shorten_const_names_in_term =
- map_aterms (fn Const (s, T) => Const (short_const_name s, T) | t => t)
+val shorten_names_in_term =
+ map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
+ #> map_types shorten_names_in_type
(* theory -> typ * typ -> bool *)
fun type_match thy (T1, T2) =
@@ -371,7 +378,7 @@
(* theory -> term * term -> bool *)
fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
| term_match thy (Free (s1, T1), Free (s2, T2)) =
- const_match thy ((short_name s1, T1), (short_name s2, T2))
+ const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
| term_match thy (t1, t2) = t1 aconv t2
(* typ -> bool *)
@@ -391,7 +398,7 @@
fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
| is_gfp_iterator_type _ = false
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
-val is_boolean_type = equal prop_T orf equal bool_T
+fun is_boolean_type T = (T = prop_T orelse T = bool_T)
val is_integer_type =
member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
val is_record_type = not o null o Record.dest_recTs
@@ -458,6 +465,14 @@
| NONE => case T of Type (s, Ts) => Type (s, map subst Ts) | _ => T
in subst T end
+(* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
+ e.g., by adding a field to "Datatype_Aux.info". *)
+(* string -> bool *)
+val is_basic_datatype =
+ member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
+ @{type_name nat}, @{type_name int},
+ "Code_Numeral.code_numeral"]
+
(* theory -> typ -> typ -> typ -> typ *)
fun instantiate_type thy T1 T1' T2 =
Same.commit (Envir.subst_type_same
@@ -486,8 +501,11 @@
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
val (co_s, co_Ts) = dest_Type co_T
val _ =
- if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then ()
- else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
+ if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts)
+ andalso co_s <> "fun" andalso not (is_basic_datatype co_s) then
+ ()
+ else
+ raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
codatatypes
in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
@@ -516,12 +534,6 @@
Rep_inverse = SOME Rep_inverse}
| NONE => NONE
-(* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
- e.g., by adding a field to "Datatype_Aux.info". *)
-(* string -> bool *)
-fun is_basic_datatype s =
- s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},
- @{type_name nat}, @{type_name int}, "Code_Numeral.code_numeral"]
(* theory -> string -> bool *)
val is_typedef = is_some oo typedef_info
val is_real_datatype = is_some oo Datatype.get_info
@@ -568,14 +580,15 @@
val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
(* theory -> string -> typ -> int *)
fun no_of_record_field thy s T1 =
- find_index (equal s o fst) (Record.get_extT_fields thy T1 ||> single |> op @)
+ find_index (curry (op =) s o fst)
+ (Record.get_extT_fields thy T1 ||> single |> op @)
(* theory -> styp -> bool *)
fun is_record_get thy (s, Type ("fun", [T1, _])) =
- exists (equal s o fst) (all_record_fields thy T1)
+ exists (curry (op =) s o fst) (all_record_fields thy T1)
| is_record_get _ _ = false
fun is_record_update thy (s, T) =
String.isSuffix Record.updateN s andalso
- exists (equal (unsuffix Record.updateN s) o fst)
+ exists (curry (op =) (unsuffix Record.updateN s) o fst)
(all_record_fields thy (body_type T))
handle TYPE _ => false
fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
@@ -608,11 +621,11 @@
end
handle TYPE ("dest_Type", _, _) => false
fun is_constr_like thy (s, T) =
- s mem [@{const_name FunBox}, @{const_name PairBox}] orelse
+ s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse
let val (x as (s, T)) = (s, unbox_type T) in
Refute.is_IDT_constructor thy x orelse is_record_constr x
orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
- orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}]
+ orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep}
orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
orelse is_coconstr thy x
end
@@ -644,10 +657,11 @@
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
case T of
Type ("fun", _) =>
- boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T))
+ (boxy = InPair orelse boxy = InFunLHS)
+ andalso not (is_boolean_type (body_type T))
| Type ("*", Ts) =>
- boxy mem [InPair, InFunRHS1, InFunRHS2]
- orelse (boxy mem [InExpr, InFunLHS]
+ 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))
| _ => false
@@ -660,7 +674,7 @@
and box_type ext_ctxt boxy T =
case T of
Type (z as ("fun", [T1, T2])) =>
- if not (boxy mem [InConstr, InSel])
+ if boxy <> InConstr andalso boxy <> InSel
andalso should_box_type ext_ctxt boxy z then
Type (@{type_name fun_box},
[box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
@@ -672,8 +686,8 @@
Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
else
Type ("*", map (box_type ext_ctxt
- (if boxy mem [InConstr, InSel] then boxy
- else InPair)) Ts)
+ (if boxy = InConstr orelse boxy = InSel then boxy
+ else InPair)) Ts)
| _ => T
(* styp -> styp *)
@@ -922,7 +936,7 @@
let
(* typ list -> typ -> int *)
fun aux avoid T =
- (if T mem avoid then
+ (if member (op =) avoid T then
0
else case T of
Type ("fun", [T1, T2]) =>
@@ -957,7 +971,7 @@
|> map (Integer.prod o map (aux (T :: avoid)) o binder_types
o snd)
in
- if exists (equal 0) constr_cards then 0
+ if exists (curry (op =) 0) constr_cards then 0
else Integer.sum constr_cards
end)
| _ => raise SAME ())
@@ -989,8 +1003,8 @@
(* theory -> string -> bool *)
fun is_funky_typedef_name thy s =
- s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
- @{type_name int}]
+ member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
+ @{type_name int}] s
orelse is_frac_type thy (Type (s, []))
(* theory -> term -> bool *)
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
@@ -1063,10 +1077,11 @@
val (built_in_nondefs, user_nondefs) =
List.partition (is_typedef_axiom thy false) user_nondefs
|>> append built_in_nondefs
- val defs = (thy |> PureThy.all_thms_of
- |> filter (equal Thm.definitionK o Thm.get_kind o snd)
- |> map (prop_of o snd) |> filter is_plain_definition) @
- user_defs @ built_in_defs
+ val defs =
+ (thy |> PureThy.all_thms_of
+ |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
+ |> map (prop_of o snd) |> filter is_plain_definition) @
+ user_defs @ built_in_defs
in (defs, built_in_nondefs, user_nondefs) end
(* bool -> styp -> int option *)
@@ -1111,7 +1126,7 @@
else
these (Symtab.lookup table s)
|> map_filter (try (Refute.specialize_type thy x))
- |> filter (equal (Const x) o term_under_def)
+ |> filter (curry (op =) (Const x) o term_under_def)
(* theory -> term -> term option *)
fun normalized_rhs_of thy t =
@@ -1152,7 +1167,8 @@
(* term -> bool *)
fun is_good_arg (Bound _) = true
| is_good_arg (Const (s, _)) =
- s mem [@{const_name True}, @{const_name False}, @{const_name undefined}]
+ s = @{const_name True} orelse s = @{const_name False}
+ orelse s = @{const_name undefined}
| is_good_arg _ = false
in
case t |> strip_abs_body |> strip_comb of
@@ -1598,9 +1614,9 @@
let
val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
- val (main, side) = List.partition (exists_Const (equal x)) prems
+ val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
(* term -> bool *)
- val is_good_head = equal (Const x) o head_of
+ val is_good_head = curry (op =) (Const x) o head_of
in
if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
end
@@ -1693,7 +1709,7 @@
(x as (s, _)) =
case triple_lookup (const_match thy) wfs x of
SOME (SOME b) => b
- | _ => s mem [@{const_name Nats}, @{const_name fold_graph'}]
+ | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'}
orelse case AList.lookup (op =) (!wf_cache) x of
SOME (_, wf) => wf
| NONE =>
@@ -1730,7 +1746,7 @@
| do_disjunct j t =
case num_occs_of_bound_in_term j t of
0 => true
- | 1 => exists (equal (Bound j) o head_of) (conjuncts t)
+ | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t)
| _ => false
(* term -> bool *)
fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
@@ -1774,7 +1790,7 @@
t
end
val (nonrecs, recs) =
- List.partition (equal 0 o num_occs_of_bound_in_term j)
+ List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
(disjuncts body)
val base_body = nonrecs |> List.foldl s_disj @{const False}
val step_body = recs |> map (repair_rec j)
@@ -1923,7 +1939,7 @@
| Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
| Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
| Type (_, Ts) =>
- if T mem @{typ prop} :: @{typ bool} :: @{typ unit} :: accum then
+ if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
accum
else
T :: accum
@@ -1962,7 +1978,7 @@
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 (equal t_comb) seen of
+ 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
@@ -2046,7 +2062,7 @@
(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 mem [@{const_name Pair}]
+ andalso (is_constr thy x orelse s = @{const_name Pair}
orelse x = dest_Const @{const Suc})
andalso (not careful orelse not (is_Var t1)
orelse String.isPrefix val_var_prefix
@@ -2141,7 +2157,8 @@
(* term list -> (indexname * typ) list -> indexname * typ -> term -> term
-> term -> term *)
and aux_eq prems zs z t' t1 t2 =
- if not (z mem zs) andalso not (exists_subterm (equal (Var z)) t') then
+ 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
@@ -2299,8 +2316,8 @@
(t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
aux s0 (s1 :: ss) (T1 :: Ts) t1
- else if quant_s = ""
- andalso s0 mem [@{const_name All}, @{const_name Ex}] then
+ else if quant_s = "" andalso (s0 = @{const_name All}
+ orelse s0 = @{const_name Ex}) then
aux s0 [s1] [T1] t1
else
raise SAME ()
@@ -2330,7 +2347,8 @@
| cost boundss_cum_costs (j :: js) =
let
val (yeas, nays) =
- List.partition (fn (bounds, _) => j mem bounds)
+ List.partition (fn (bounds, _) =>
+ member (op =) bounds j)
boundss_cum_costs
val yeas_bounds = big_union fst yeas
val yeas_cost = Integer.sum (map snd yeas)
@@ -2339,7 +2357,7 @@
val js = all_permutations (index_seq 0 num_Ts)
|> map (`(cost (t_boundss ~~ t_costs)))
|> sort (int_ord o pairself fst) |> hd |> snd
- val back_js = map (fn j => find_index (equal j) js)
+ 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
@@ -2355,7 +2373,8 @@
| build ts_cum_bounds (j :: js) =
let
val (yeas, nays) =
- List.partition (fn (_, bounds) => j mem bounds)
+ List.partition (fn (_, bounds) =>
+ member (op =) bounds j)
ts_cum_bounds
||> map (apfst (incr_boundvars ~1))
in
@@ -2548,7 +2567,7 @@
if t = Const x then
list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
else
- let val j = find_index (equal t) fixed_params in
+ 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
@@ -2582,7 +2601,7 @@
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 (x mem blacklist) andalso not (null args)
+ ((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
@@ -2607,7 +2626,8 @@
(* int -> term *)
fun var_for_bound_no j =
Var ((bound_var_prefix ^
- nat_subscript (find_index (equal j) bound_js + 1), k),
+ nat_subscript (find_index (curry (op =) j) bound_js
+ + 1), k),
nth Ts j)
val fixed_args_in_axiom =
map (curry subst_bounds
@@ -2739,7 +2759,8 @@
\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 mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then
+ 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
@@ -2770,13 +2791,13 @@
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 (equal (Var z)) t' ? insert (op =) 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 mem [@{const_name "=="}, @{const_name "op ="}] then
+ 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')
@@ -2855,7 +2876,8 @@
| Const (s as @{const_name Eps}, T) => do_description_operator s T
| Const (s as @{const_name Tha}, T) => do_description_operator s T
| Const (x as (s, T)) =>
- Const (s, if s mem [@{const_name converse}, @{const_name trancl}] then
+ 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
@@ -2954,7 +2976,7 @@
|> 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 |> (x mem xs) ? cons ([], [], x)))
+ |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
(* special -> int *)
fun generality (js, _, _) = ~(length js)
(* special -> special -> bool *)
@@ -3022,7 +3044,7 @@
case t of
t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
| Const (x as (s, T)) =>
- (if x mem xs orelse is_built_in_const fast_descrs x then
+ (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
@@ -3175,7 +3197,7 @@
val T = unbox_type T
val format = format |> filter (curry (op <) 0)
in
- if forall (equal 1) format then
+ if forall (curry (op =) 1) format then
T
else
let
@@ -3226,7 +3248,8 @@
SOME t => do_term t
| NONE =>
Var (nth missing_vars
- (find_index (equal j) missing_js)))
+ (find_index (curry (op =) j)
+ missing_js)))
Ts (0 upto max_j)
val t = do_const x' |> fst
val format =
@@ -3300,7 +3323,7 @@
(t, format_term_type thy def_table formats t)
end)
|>> map_types (typ_subst [(@{typ bisim_iterator}, nat_T)] o unbox_type)
- |>> shorten_const_names_in_term |>> shorten_abs_vars
+ |>> shorten_names_in_term |>> shorten_abs_vars
in do_const end
(* styp -> string *)
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Dec 14 12:31:00 2009 +0100
@@ -105,7 +105,7 @@
fun is_known_raw_param s =
AList.defined (op =) default_default_params s
orelse AList.defined (op =) negated_params s
- orelse s mem ["max", "eval", "expect"]
+ orelse s = "max" orelse s = "eval" orelse s = "expect"
orelse exists (fn p => String.isPrefix (p ^ " ") s)
["card", "max", "iter", "box", "dont_box", "mono", "non_mono",
"wf", "non_wf", "format"]
@@ -409,7 +409,7 @@
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
-fun pick_nits override_params auto subgoal state =
+fun pick_nits override_params auto i state =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
@@ -423,26 +423,25 @@
|> (if auto then perhaps o try
else if debug then fn f => fn x => f x
else handle_exceptions ctxt)
- (fn (_, state) => pick_nits_in_subgoal state params auto subgoal
- |>> equal "genuine")
+ (fn (_, state) => pick_nits_in_subgoal state params auto i
+ |>> curry (op =) "genuine")
in
if auto orelse blocking then go ()
else (Toplevel.thread true (fn () => (go (); ())); (false, state))
end
-(* (TableFun().key * string list) list option * int option
- -> Toplevel.transition -> Toplevel.transition *)
-fun nitpick_trans (opt_params, opt_subgoal) =
+(* raw_param list option * int option -> Toplevel.transition
+ -> Toplevel.transition *)
+fun nitpick_trans (opt_params, opt_i) =
Toplevel.keep (K ()
- o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
+ o snd o pick_nits (these opt_params) false (the_default 1 opt_i)
o Toplevel.proof_of)
(* raw_param -> string *)
fun string_for_raw_param (name, value) =
name ^ " = " ^ stringify_raw_param_value value
-(* (TableFun().key * string) list option -> Toplevel.transition
- -> Toplevel.transition *)
+(* raw_param list option -> Toplevel.transition -> Toplevel.transition *)
fun nitpick_params_trans opt_params =
Toplevel.theory
(fold set_default_raw_param (these opt_params)
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Dec 14 12:31:00 2009 +0100
@@ -82,7 +82,7 @@
(* Proof.context -> bool -> string -> typ -> rep -> string *)
fun bound_comment ctxt debug nick T R =
- short_const_name nick ^
+ short_name nick ^
(if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
else "") ^ " : " ^ string_for_rep R
@@ -725,7 +725,7 @@
(* nfa_table -> typ -> typ -> Kodkod.rel_expr list *)
fun direct_path_rel_exprs nfa start final =
case AList.lookup (op =) nfa final of
- SOME trans => map fst (filter (equal start o snd) trans)
+ SOME trans => map fst (filter (curry (op =) start o snd) trans)
| NONE => []
(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> Kodkod.rel_expr *)
and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final =
@@ -1031,7 +1031,7 @@
fold (kk_or o (kk_no o to_r)) opt_arg_us
(kk_rel_eq (to_rep min_R u1) (to_rep min_R u2))
else
- kk_no (kk_difference (to_rep min_R u1) (to_rep min_R u2))
+ kk_subset (to_rep min_R u1) (to_rep min_R u2)
end)
| Op2 (Eq, T, R, u1, u2) =>
(case min_rep (rep_of u1) (rep_of u2) of
@@ -1067,7 +1067,7 @@
kk_subset (kk_product r1 r2) Kodkod.Iden
else if not both_opt then
(r1, r2) |> is_opt_rep (rep_of u2) ? swap
- |> uncurry kk_difference |> kk_no
+ |-> kk_subset
else
raise SAME ()
else
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Dec 14 12:31:00 2009 +0100
@@ -60,7 +60,7 @@
? prefix "\<^isub>,"
(* string -> typ -> int -> string *)
fun atom_name prefix (T as Type (s, _)) j =
- prefix ^ substring (short_name s, 0, 1) ^ atom_suffix s j
+ prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j
| atom_name prefix (T as TFree (s, _)) j =
prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
| atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
@@ -125,7 +125,8 @@
$ aux T1 T2 ps $ t1 $ t2
in aux T1 T2 o rev end
(* term -> bool *)
-fun is_plain_fun (Const (s, _)) = s mem [@{const_name undefined}, non_opt_name]
+fun is_plain_fun (Const (s, _)) =
+ (s = @{const_name undefined} orelse s = non_opt_name)
| is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
is_plain_fun t0
| is_plain_fun _ = false
@@ -350,7 +351,8 @@
val real_j = j + offset_of_type ofs T
val constr_x as (constr_s, constr_T) =
get_first (fn (jss, {const, ...}) =>
- if [real_j] mem jss then SOME const else NONE)
+ if member (op =) jss [real_j] then SOME const
+ 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)
@@ -369,7 +371,7 @@
else NONE)) sel_jsss
val uncur_arg_Ts = binder_types constr_T
in
- if co andalso (T, j) mem seen then
+ if co andalso member (op =) seen (T, j) then
Var (var ())
else
let
@@ -408,7 +410,7 @@
in
if co then
let val var = var () in
- if exists_subterm (equal (Var var)) t then
+ if exists_subterm (curry (op =) (Var var)) t then
Const (@{const_name The}, (T --> bool_T) --> T)
$ Abs ("\<omega>", T,
Const (@{const_name "op ="}, [T, T] ---> bool_T)
@@ -449,7 +451,8 @@
val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
val ts2 =
map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
- [[int_for_bool (js mem jss)]]) jss1
+ [[int_for_bool (member (op =) jss js)]])
+ jss1
in make_fun false T1 T2 T' ts1 ts2 end
| term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
let
@@ -517,7 +520,7 @@
let
val ((head1, args1), (head2, args2)) =
pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
- val max_depth = max_depth - (if T mem coTs then 1 else 0)
+ val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
in
head1 = head2
andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
@@ -639,10 +642,12 @@
val (eval_names, noneval_nonskolem_nonsel_names) =
List.partition (String.isPrefix eval_prefix o nickname_of)
nonskolem_nonsel_names
- ||> filter_out (equal @{const_name bisim_iterator_max} o nickname_of)
+ ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
+ o nickname_of)
val free_names =
map (fn x as (s, T) =>
- case filter (equal x o pairf nickname_of (unbox_type o type_of))
+ case filter (curry (op =) x
+ o pairf nickname_of (unbox_type o type_of))
free_names of
[name] => name
| [] => FreeName (s, T, Any)
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 14 12:31:00 2009 +0100
@@ -101,7 +101,7 @@
string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2
| CPair (C1, C2) => aux (prec + 1) C1 ^ " \<times> " ^ aux prec C2
| CType (s, []) =>
- if s mem [@{type_name prop}, @{type_name bool}] then "o" else s
+ if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s
| CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s
| CRec (s, _) => "[" ^ s ^ "]") ^
(if need_parens then ")" else "")
@@ -125,9 +125,10 @@
andalso exists (could_exist_alpha_subtype alpha_T) Ts)
| could_exist_alpha_subtype alpha_T T = (T = alpha_T)
(* theory -> typ -> typ -> bool *)
-fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) =
- could_exist_alpha_subtype alpha_T
- | could_exist_alpha_sub_ctype thy alpha_T = equal alpha_T orf is_datatype thy
+fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
+ could_exist_alpha_subtype alpha_T T
+ | could_exist_alpha_sub_ctype thy alpha_T T =
+ (T = alpha_T orelse is_datatype thy T)
(* ctype -> bool *)
fun exists_alpha_sub_ctype CAlpha = true
@@ -164,7 +165,7 @@
| repair_ctype cache seen (CRec (z as (s, _))) =
case AList.lookup (op =) cache z |> the of
CRec _ => CType (s, [])
- | C => if C mem seen then CType (s, [])
+ | C => if member (op =) seen C then CType (s, [])
else repair_ctype cache (C :: seen) C
(* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *)
@@ -490,7 +491,7 @@
(* literal list -> unit *)
fun print_solution lits =
- let val (pos, neg) = List.partition (equal Pos o snd) lits in
+ let val (pos, neg) = List.partition (curry (op =) Pos o snd) lits in
print_g ("*** Solution:\n" ^
"+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
"-: " ^ commas (map (string_for_var o fst) neg))
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Dec 14 12:31:00 2009 +0100
@@ -716,16 +716,16 @@
else if is_rep_fun thy x then
Func oo best_non_opt_symmetric_reps_for_fun_type
else if all_precise orelse is_skolem_name v
- orelse original_name s
- mem [@{const_name undefined_fast_The},
- @{const_name undefined_fast_Eps},
- @{const_name bisim},
- @{const_name bisim_iterator_max}] then
+ orelse member (op =) [@{const_name undefined_fast_The},
+ @{const_name undefined_fast_Eps},
+ @{const_name bisim},
+ @{const_name bisim_iterator_max}]
+ (original_name s) then
best_non_opt_set_rep_for_type
- else if original_name s
- mem [@{const_name set}, @{const_name distinct},
- @{const_name ord_class.less},
- @{const_name ord_class.less_eq}] then
+ else if member (op =) [@{const_name set}, @{const_name distinct},
+ @{const_name ord_class.less},
+ @{const_name ord_class.less_eq}]
+ (original_name s) then
best_set_rep_for_type
else
best_opt_set_rep_for_type) scope T
@@ -934,20 +934,21 @@
Cst (NormFrac, T, Func (R1, Func (R1, Opt (Struct [R1, R1]))))
end
| Cst (cst, T, _) =>
- if cst mem [Unknown, Unrep] then
+ if cst = Unknown orelse cst = Unrep then
case (is_boolean_type T, polar) of
(true, Pos) => Cst (False, T, Formula Pos)
| (true, Neg) => Cst (True, T, Formula Neg)
| _ => Cst (cst, T, best_opt_set_rep_for_type scope T)
- else if cst mem [Add, Subtract, Multiply, Divide, Modulo, Gcd,
- Lcm] then
+ else if member (op =) [Add, Subtract, Multiply, Divide, Modulo, Gcd,
+ Lcm] cst then
let
val T1 = domain_type T
val R1 = Atom (spec_of_type scope T1)
val total =
- T1 = nat_T andalso cst mem [Subtract, Divide, Modulo, Gcd]
+ T1 = nat_T andalso (cst = Subtract orelse cst = Divide
+ orelse cst = Modulo orelse cst = Gcd)
in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
- else if cst mem [NatToInt, IntToNat] then
+ else if cst = NatToInt orelse cst = IntToNat then
let
val (nat_card, nat_j0) = spec_of_type scope nat_T
val (int_card, int_j0) = spec_of_type scope int_T
@@ -1113,7 +1114,7 @@
in s_op2 Lambda T R u1' u2' end
| R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
| Op2 (oper, T, _, u1, u2) =>
- if oper mem [All, Exist] then
+ if oper = All orelse oper = Exist then
let
val table' = fold (choose_rep_for_bound_var scope) (untuple I u1)
table
@@ -1140,7 +1141,7 @@
end
end
end
- else if oper mem [Or, And] then
+ else if oper = Or orelse oper = And then
let
val u1' = gsub def polar u1
val u2' = gsub def polar u2
@@ -1159,7 +1160,7 @@
raise SAME ())
handle SAME () => s_op2 oper T (Formula polar) u1' u2'
end
- else if oper mem [The, Eps] then
+ else if oper = The orelse oper = Eps then
let
val u1' = sub u1
val opt1 = is_opt_rep (rep_of u1')
@@ -1210,7 +1211,7 @@
let
val Rs = map (best_one_rep_for_type scope o type_of) us
val us = map sub us
- val R = if forall (equal Unit) Rs then Unit else Struct Rs
+ val R = if forall (curry (op =) Unit) Rs then Unit else Struct Rs
val R' = (exists (is_opt_rep o rep_of) us ? opt_rep ofs T) R
in s_tuple T R' us end
| Construct (us', T, _, us) =>
@@ -1331,7 +1332,7 @@
Cst _ => u
| Op1 (oper, T, R, u1) => Op1 (oper, T, R, rename_vars_in_nut pool table u1)
| Op2 (oper, T, R, u1, u2) =>
- if oper mem [All, Exist, Lambda] then
+ if oper = All orelse oper = Exist orelse oper = Lambda then
let
val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1)
([], pool, table)
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Dec 14 12:31:00 2009 +0100
@@ -85,12 +85,12 @@
(* dtype_spec list -> typ -> dtype_spec option *)
fun datatype_spec (dtypes : dtype_spec list) T =
- List.find (equal T o #typ) dtypes
+ List.find (curry (op =) T o #typ) dtypes
(* dtype_spec list -> styp -> constr_spec *)
fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
| constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) =
- case List.find (equal (s, body_type T) o (apsnd body_type o #const))
+ case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const))
constrs of
SOME c => c
| NONE => constr_spec dtypes x
@@ -125,7 +125,7 @@
bisim_depth, datatypes, ...} : scope) =
let
val (iter_asgns, card_asgns) =
- card_assigns |> filter_out (equal @{typ bisim_iterator} o fst)
+ card_assigns |> filter_out (curry (op =) @{typ bisim_iterator} o fst)
|> List.partition (is_fp_iterator_type o fst)
val (unimportant_card_asgns, important_card_asgns) =
card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
@@ -262,14 +262,14 @@
(* int list -> int *)
fun cost_with_monos [] = 0
| cost_with_monos (k :: ks) =
- if k < sync_threshold andalso forall (equal k) ks then
+ if k < sync_threshold andalso forall (curry (op =) k) ks then
k - sync_threshold
else
k * (k + 1) div 2 + Integer.sum ks
fun cost_without_monos [] = 0
| cost_without_monos [k] = k
| cost_without_monos (_ :: k :: ks) =
- if k < sync_threshold andalso forall (equal k) ks then
+ if k < sync_threshold andalso forall (curry (op =) k) ks then
k - sync_threshold
else
Integer.sum (k :: ks)
@@ -282,7 +282,7 @@
(* typ -> bool *)
fun is_self_recursive_constr_type T =
- exists (exists_subtype (equal (body_type T))) (binder_types T)
+ exists (exists_subtype (curry (op =) (body_type T))) (binder_types T)
(* (styp * int) list -> styp -> int *)
fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x)
@@ -436,12 +436,12 @@
fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
(desc as (card_asgns, _)) (T, card) =
let
- val shallow = T mem shallow_dataTs
+ val shallow = member (op =) shallow_dataTs T
val co = is_codatatype thy T
val xs = boxed_datatype_constrs ext_ctxt T
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
- List.partition (equal true) self_recs |> pairself length
+ List.partition (curry (op =) true) self_recs |> pairself length
val precise = (card = bounded_precise_card_of_type ext_ctxt (card + 1) 0
card_asgns T)
(* int -> int *)
--- a/src/HOL/Tools/refute.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/refute.ML Mon Dec 14 12:31:00 2009 +0100
@@ -45,13 +45,16 @@
val get_default_params : theory -> (string * string) list
val actual_params : theory -> (string * string) list -> params
- val find_model : theory -> params -> term -> bool -> unit
+ val find_model : theory -> params -> term list -> term -> bool -> unit
(* tries to find a model for a formula: *)
- val satisfy_term : theory -> (string * string) list -> term -> unit
+ val satisfy_term :
+ theory -> (string * string) list -> term list -> term -> unit
(* tries to find a model that refutes a formula: *)
- val refute_term : theory -> (string * string) list -> term -> unit
- val refute_goal : theory -> (string * string) list -> thm -> int -> unit
+ val refute_term :
+ theory -> (string * string) list -> term list -> term -> unit
+ val refute_goal :
+ Proof.context -> (string * string) list -> thm -> int -> unit
val setup : theory -> theory
@@ -153,8 +156,10 @@
(* formula. *)
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *)
(* "satsolver" string SAT solver to be used. *)
+(* "no_assms" bool If "true", assumptions in structured proofs are *)
+(* not considered. *)
(* "expect" string Expected result ("genuine", "potential", "none", or *)
-(* "unknown") *)
+(* "unknown"). *)
(* ------------------------------------------------------------------------- *)
type params =
@@ -165,6 +170,7 @@
maxvars : int,
maxtime : int,
satsolver: string,
+ no_assms : bool,
expect : string
};
@@ -360,6 +366,15 @@
fun actual_params thy override =
let
+ (* (string * string) list * string -> bool *)
+ fun read_bool (parms, name) =
+ case AList.lookup (op =) parms name of
+ SOME "true" => true
+ | SOME "false" => false
+ | SOME s => error ("parameter " ^ quote name ^
+ " (value is " ^ quote s ^ ") must be \"true\" or \"false\"")
+ | NONE => error ("parameter " ^ quote name ^
+ " must be assigned a value")
(* (string * string) list * string -> int *)
fun read_int (parms, name) =
case AList.lookup (op =) parms name of
@@ -385,6 +400,7 @@
val maxtime = read_int (allparams, "maxtime")
(* string *)
val satsolver = read_string (allparams, "satsolver")
+ val no_assms = read_bool (allparams, "no_assms")
val expect = the_default "" (AList.lookup (op =) allparams "expect")
(* all remaining parameters of the form "string=int" are collected in *)
(* 'sizes' *)
@@ -395,10 +411,10 @@
(fn (name, value) => Option.map (pair name) (Int.fromString value))
(filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
andalso name<>"maxvars" andalso name<>"maxtime"
- andalso name<>"satsolver") allparams)
+ andalso name<>"satsolver" andalso name<>"no_assms") allparams)
in
{sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars,
- maxtime=maxtime, satsolver=satsolver, expect=expect}
+ maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect}
end;
@@ -1118,6 +1134,7 @@
(* the model to the user by calling 'print_model' *)
(* thy : the current theory *)
(* {...} : parameters that control the translation/model generation *)
+(* assm_ts : assumptions to be considered unless "no_assms" is specified *)
(* t : term to be translated into a propositional formula *)
(* negate : if true, find a model that makes 't' false (rather than true) *)
(* ------------------------------------------------------------------------- *)
@@ -1125,7 +1142,7 @@
(* theory -> params -> Term.term -> bool -> unit *)
fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver,
- expect} t negate =
+ no_assms, expect} assm_ts t negate =
let
(* string -> unit *)
fun check_expect outcome_code =
@@ -1135,6 +1152,9 @@
fun wrapper () =
let
val timer = Timer.startRealTimer ()
+ val t = if no_assms then t
+ else if negate then Logic.list_implies (assm_ts, t)
+ else Logic.mk_conjunction_list (t :: assm_ts)
val u = unfold_defs thy t
val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
val axioms = collect_axioms thy u
@@ -1270,10 +1290,10 @@
(* parameters *)
(* ------------------------------------------------------------------------- *)
- (* theory -> (string * string) list -> Term.term -> unit *)
+ (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
- fun satisfy_term thy params t =
- find_model thy (actual_params thy params) t false;
+ fun satisfy_term thy params assm_ts t =
+ find_model thy (actual_params thy params) assm_ts t false;
(* ------------------------------------------------------------------------- *)
(* refute_term: calls 'find_model' to find a model that refutes 't' *)
@@ -1281,9 +1301,9 @@
(* parameters *)
(* ------------------------------------------------------------------------- *)
- (* theory -> (string * string) list -> Term.term -> unit *)
+ (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
- fun refute_term thy params t =
+ fun refute_term thy params assm_ts t =
let
(* disallow schematic type variables, since we cannot properly negate *)
(* terms containing them (their logical meaning is that there EXISTS a *)
@@ -1332,15 +1352,29 @@
val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure)
val subst_t = Term.subst_bounds (map Free frees, strip_t)
in
- find_model thy (actual_params thy params) subst_t true
+ find_model thy (actual_params thy params) assm_ts subst_t true
+ handle REFUTE (s, s') => error ("REFUTE " ^ s ^ " " ^ s') (* ### *)
end;
(* ------------------------------------------------------------------------- *)
(* refute_goal *)
(* ------------------------------------------------------------------------- *)
- fun refute_goal thy params st i =
- refute_term thy params (Logic.get_goal (Thm.prop_of st) i);
+ fun refute_goal ctxt params th i =
+ let
+ val t = th |> prop_of
+ in
+ if Logic.count_prems t = 0 then
+ priority "No subgoal!"
+ else
+ let
+ val assms = map term_of (Assumption.all_assms_of ctxt)
+ val (t, frees) = Logic.goal_params t i
+ in
+ refute_term (ProofContext.theory_of ctxt) params assms
+ (subst_bounds (frees, t))
+ end
+ end
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/refute_isar.ML Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Tools/refute_isar.ML Mon Dec 14 12:31:00 2009 +0100
@@ -12,8 +12,9 @@
(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
-val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
-
+val scan_parm =
+ OuterParse.name
+ -- (Scan.optional (OuterParse.$$$ "=" |-- OuterParse.name) "true")
val scan_parms = Scan.optional
(OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
@@ -27,9 +28,9 @@
(fn (parms, i) =>
Toplevel.keep (fn state =>
let
- val thy = Toplevel.theory_of state;
+ val ctxt = Toplevel.context_of state;
val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
- in Refute.refute_goal thy parms st i end)));
+ in Refute.refute_goal ctxt parms st i end)));
(* 'refute_params' command *)
--- a/src/HOL/ex/Refute_Examples.thy Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/ex/Refute_Examples.thy Mon Dec 14 12:31:00 2009 +0100
@@ -1516,6 +1516,17 @@
refute
oops
+text {* Structured proofs *}
+
+lemma "x = y"
+proof cases
+ assume "x = y"
+ show ?thesis
+ refute
+ refute [no_assms]
+ refute [no_assms = false]
+oops
+
refute_params [satsolver="auto"]
end