--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 09 16:08:30 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 10 11:38:53 2014 +0200
@@ -193,12 +193,13 @@
conflict with variable constraints in the goal. At least, type inference often fails
otherwise. See also "axiom_inference" in "Metis_Reconstruct". *)
val var_index = if textual then 0 else 1
+
fun do_term extra_ts opt_T u =
(case u of
ATerm ((s, tys), us) =>
- if s = ""
- then error "Isar proof reconstruction failed because the ATP proof \
- \contains unparsable material."
+ if s = "" then
+ error "Isar proof reconstruction failed because the ATP proof contains unparsable \
+ \material."
else if String.isPrefix native_type_prefix s then
@{const True} (* ignore TPTP type information *)
else if s = tptp_equal then
@@ -221,10 +222,8 @@
else if s' = app_op_name then
let val extra_t = do_term [] NONE (List.last us) in
do_term (extra_t :: extra_ts)
- (case opt_T of
- SOME T => SOME (slack_fastype_of extra_t --> T)
- | NONE => NONE)
- (nth us (length us - 2))
+ (case opt_T of SOME T => SOME (slack_fastype_of extra_t --> T) | NONE => NONE)
+ (nth us (length us - 2))
end
else if s' = type_guard_name then
@{const True} (* ignore type predicates *)
@@ -238,18 +237,15 @@
val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us
val T =
(if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then
- if new_skolem then
- SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
- else if textual then
- try (Sign.const_instance thy) (s', Ts)
- else
- NONE
+ if new_skolem then SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
+ else if textual then try (Sign.const_instance thy) (s', Ts)
+ else NONE
else
NONE)
|> (fn SOME T => T
| NONE =>
map slack_fastype_of term_ts --->
- the_default (Type_Infer.anyT @{sort type}) opt_T)
+ the_default (Type_Infer.anyT @{sort type}) opt_T)
val t =
if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
else Const (unproxify_const s', T)
@@ -261,8 +257,8 @@
"Variable.variant_frees". This does not hold in general but should hold for
ATP-generated Skolem function names, since these end with a digit and
"variant_frees" appends letters. *)
- fun fresh_up s =
- [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
+ fun fresh_up s = [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
+
val term_ts =
map (do_term [] NONE) us
(* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jun 09 16:08:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 10 11:38:53 2014 +0200
@@ -183,6 +183,8 @@
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
val simp_attrs = @{attributes [simp]};
+fun is_triv_eq t = op aconv (HOLogic.dest_eq t) handle TERM _ => false;
+
val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
fun flat_corec_predss_getterss qss gss = maps (op @) (qss ~~ gss);
@@ -1189,20 +1191,13 @@
val selssA = map (map (mk_disc_or_sel ADs)) selss;
val disc_sel_pairs = flat (map2 (map o pair) discsA selssA);
- fun is_t_eq_t T t term =
- let
- val (head, tail) = Term.strip_comb term;
- in
- head aconv HOLogic.eq_const T andalso forall (fn u => u = t) tail
- end;
-
val disc_map_iff_thms =
let
val discsB = map (mk_disc_or_sel BDs) discs;
val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discsA;
fun mk_goal (discA_t, discB) =
- if head_of discA_t aconv @{const Not} orelse is_t_eq_t TA ta discA_t then
+ if head_of discA_t aconv HOLogic.Not orelse is_triv_eq discA_t then
NONE
else
SOME (mk_Trueprop_eq
@@ -1210,7 +1205,8 @@
val goals = map_filter mk_goal (discsA_t ~~ discsB);
in
- if null goals then []
+ if null goals then
+ []
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
@@ -1224,7 +1220,7 @@
let
fun mk_goal (discA, selA) =
let
- val premise = Term.betapply (discA, ta);
+ val prem = Term.betapply (discA, ta);
val selB = mk_disc_or_sel BDs selA;
val lhs = selB $ (Term.list_comb (map_term, fs) $ ta);
val lhsT = fastype_of lhs;
@@ -1234,14 +1230,15 @@
val rhs = (case map_rhs of
Const (@{const_name id}, _) => selA $ ta
| _ => map_rhs $ (selA $ ta));
- val conclusion = mk_Trueprop_eq (lhs, rhs);
+ val concl = mk_Trueprop_eq (lhs, rhs);
in
- if is_t_eq_t TA ta premise then conclusion
- else Logic.mk_implies (HOLogic.mk_Trueprop premise, conclusion)
+ if is_triv_eq prem then concl
+ else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl)
end;
val goals = map mk_goal disc_sel_pairs;
in
- if null goals then []
+ if null goals then
+ []
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
@@ -1250,14 +1247,17 @@
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
end;
+
val sel_set_thms =
let
val setsA = map (mk_set ADs) (sets_of_bnf fp_bnf);
+
fun mk_goal discA selA setA ctxt =
let
- val premise = Term.betapply (discA, ta);
+ val prem = Term.betapply (discA, ta);
val sel_rangeT = range_type (fastype_of selA);
val A = HOLogic.dest_setT (range_type (fastype_of setA));
+
fun travese_nested_types t ctxt =
(case fastype_of t of
Type (type_name, xs) =>
@@ -1284,23 +1284,27 @@
([HOLogic.mk_Trueprop (HOLogic.mk_mem (t, setA $ ta))], ctxt)
else
([], ctxt));
- val (conclusions, ctxt') =
+
+ val (concls, ctxt') =
if sel_rangeT = A then
([HOLogic.mk_Trueprop (HOLogic.mk_mem (selA $ ta, setA $ ta))], ctxt)
else
travese_nested_types (selA $ ta) names_lthy;
in
if exists_subtype_in [A] sel_rangeT then
- if is_t_eq_t TA ta premise then (conclusions, ctxt')
+ if is_triv_eq prem then
+ (concls, ctxt')
else
- (map (Logic.mk_implies o pair (HOLogic.mk_Trueprop premise))
- conclusions, ctxt')
- else ([], ctxt)
+ (map (Logic.mk_implies o pair (HOLogic.mk_Trueprop prem)) concls,
+ ctxt')
+ else
+ ([], ctxt)
end;
val (goals, names_lthy) = apfst (flat o flat) (fold_map (fn (disc, sel) =>
fold_map (mk_goal disc sel) setsA) disc_sel_pairs names_lthy);
in
- if null goals then []
+ if null goals then
+ []
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
--- a/src/HOL/Tools/SMT2/smt2_config.ML Mon Jun 09 16:08:30 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_config.ML Tue Jun 10 11:38:53 2014 +0200
@@ -99,9 +99,9 @@
fun warn_solver (Context.Proof ctxt) name =
if Context_Position.is_visible ctxt then
- warning ("The SMT solver " ^ quote name ^ " is not installed.")
+ warning ("The SMT solver " ^ quote name ^ " is not installed")
else ()
- | warn_solver _ _ = ();
+ | warn_solver _ _ = ()
fun select_solver name context =
let