--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Fri Apr 04 15:58:20 2014 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Fri Apr 04 16:43:47 2014 +0200
@@ -516,10 +516,10 @@
{fix z::'a
assume h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z"
from c0 have "norm c > 0" by simp
- from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z*c)"
+ from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z * c)"
by (simp add: field_simps norm_mult)
have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
- from norm_diff_ineq[of "z*c" a ]
+ from norm_diff_ineq[of "z * c" a ]
have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
by (simp add: algebra_simps)
from ath[OF th1 th0] have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
@@ -720,7 +720,7 @@
with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)" unfolding norm_of_real by simp
have ath: "\<And>x (t::real). 0\<le> x \<Longrightarrow> x < t \<Longrightarrow> t\<le>1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1" by arith
- have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
+ have "t * cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult)
from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
by (simp add: inverse_eq_divide field_simps)
@@ -1074,4 +1074,3 @@
shows "poly [:c:] x = y \<longleftrightarrow> c = y" by simp
end
-
--- a/src/HOL/Quickcheck_Narrowing.thy Fri Apr 04 15:58:20 2014 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Fri Apr 04 16:43:47 2014 +0200
@@ -275,6 +275,26 @@
else Code_Evaluation.term_of ((i + 1) div 2))"
by (rule partial_term_of_anything)+
+code_printing constant "Code_Evaluation.term_of :: integer \<Rightarrow> term" \<rightharpoonup> (Haskell_Quickcheck)
+ "(let { t = Typerep.Typerep \"Code'_Numeral.integer\" [];
+ mkFunT s t = Typerep.Typerep \"fun\" [s, t];
+ numT = Typerep.Typerep \"Num.num\" [];
+ mkBit 0 = Generated'_Code.Const \"Num.num.Bit0\" (mkFunT numT numT);
+ mkBit 1 = Generated'_Code.Const \"Num.num.Bit1\" (mkFunT numT numT);
+ mkNumeral 1 = Generated'_Code.Const \"Num.num.One\" numT;
+ mkNumeral i = let { q = i `Prelude.div` 2; r = i `Prelude.mod` 2 }
+ in Generated'_Code.App (mkBit r) (mkNumeral q);
+ mkNumber 0 = Generated'_Code.Const \"Groups.zero'_class.zero\" t;
+ mkNumber 1 = Generated'_Code.Const \"Groups.one'_class.one\" t;
+ mkNumber i = if i > 0 then
+ Generated'_Code.App
+ (Generated'_Code.Const \"Num.numeral'_class.numeral\"
+ (mkFunT numT t))
+ (mkNumeral i)
+ else
+ Generated'_Code.App
+ (Generated'_Code.Const \"Groups.uminus'_class.uminus\" (mkFunT t t))
+ (mkNumber (- i)); } in mkNumber)"
subsection {* The @{text find_unused_assms} command *}
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Apr 04 15:58:20 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Apr 04 16:43:47 2014 +0200
@@ -46,6 +46,7 @@
val spass_input_rule : string
val spass_pre_skolemize_rule : string
val spass_skolemize_rule : string
+ val z3_tptp_core_rule : string
val short_output : bool -> string -> string
val string_of_atp_failure : atp_failure -> string
@@ -75,6 +76,7 @@
val spass_input_rule = "Inp"
val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *)
val spass_skolemize_rule = "__Sko" (* arbitrary *)
+val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *)
exception UNRECOGNIZED_ATP_PROOF of unit
@@ -211,11 +213,13 @@
(**** PARSING OF TSTP FORMAT ****)
-(* Strings enclosed in single quotes (e.g., file names) *)
+(* Strings enclosed in single quotes (e.g., file names), identifiers possibly starting
+ with "$" and possibly with "!" in them (for "z3_tptp"). *)
val scan_general_id =
$$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
- || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
- >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
+ || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o pairself implode))
+ -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o pairself implode)) ""
+ >> op ^
val skip_term =
let
@@ -416,14 +420,14 @@
| Inference_Source (rule, deps) => (((num, []), phi), rule, deps))
fun mk_step () = (name, role_of_tptp_string role, phi, rule, map (rpair []) deps)
in
- (case role_of_tptp_string role of
- Definition =>
- (case phi of
- AAtom (ATerm (("equal", _), _)) =>
- (* Vampire's equality proxy axiom *)
- (name, Definition, phi, rule, map (rpair []) deps)
- | _ => mk_step ())
- | _ => mk_step ())
+ [(case role_of_tptp_string role of
+ Definition =>
+ (case phi of
+ AAtom (ATerm (("equal", _), _)) =>
+ (* Vampire's equality proxy axiom *)
+ (name, Definition, phi, rule, map (rpair []) deps)
+ | _ => mk_step ())
+ | _ => mk_step ())]
end)
(**** PARSING OF SPASS OUTPUT ****)
@@ -464,7 +468,7 @@
-- Scan.option (Scan.this_string "derived from formulae "
|-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
>> (fn ((((num, rule), deps), u), names) =>
- ((num, these names), Unknown, u, rule, map (rpair []) deps))) x
+ [((num, these names), Unknown, u, rule, map (rpair []) deps)])) x
fun parse_spass_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
fun parse_spass_pirate_dependencies x =
@@ -489,23 +493,28 @@
File_Source (_, SOME s) => ([s], spass_input_rule, [])
| Inference_Source (rule, deps) => ([], rule, deps))
in
- ((num, names), Unknown, u, rule, map (rpair []) deps)
+ [((num, names), Unknown, u, rule, map (rpair []) deps)]
end)) x
fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
(* Syntax: <name> *)
-fun parse_satallax_line x =
- (scan_general_id --| Scan.option ($$ " ") >> core_inference satallax_core_rule) x
+fun parse_satallax_core_line x =
+ (scan_general_id --| Scan.option ($$ " ") >> (single o core_inference satallax_core_rule)) x
+
+(* Syntax: SZS core <name> ... <name> *)
+fun parse_z3_tptp_core_line x =
+ (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id)
+ >> map (core_inference z3_tptp_core_rule)) x
fun parse_line problem =
- parse_tstp_line problem || parse_spass_line || parse_spass_pirate_line || parse_satallax_line
+ parse_tstp_line problem || parse_z3_tptp_core_line || parse_spass_line || parse_spass_pirate_line
+ || parse_satallax_core_line
fun parse_proof problem =
strip_spaces_except_between_idents
#> raw_explode
#> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
- (Scan.finite Symbol.stopper
- (Scan.repeat1 (parse_line problem))))
+ (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line problem) >> flat)))
#> fst
fun core_of_agsyhol_proof s =
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Apr 04 15:58:20 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Apr 04 16:43:47 2014 +0200
@@ -620,7 +620,7 @@
val z3_tptp_config : atp_config =
{exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
+ "-core -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
proof_delims = [("SZS status Theorem", "")],
known_failures = known_szs_status_failures,
prem_role = Hypothesis,