# HG changeset patch # User blanchet # Date 1402393133 -7200 # Node ID 472360558b225a8ab6bfc3d82b77ef253f4a887a # Parent 159e1b0434959529281b43d730181900ce9cfd45 tuning diff -r 159e1b043495 -r 472360558b22 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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 diff -r 159e1b043495 -r 472360558b22 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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 = _} => diff -r 159e1b043495 -r 472360558b22 src/HOL/Tools/SMT2/smt2_config.ML --- 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