# HG changeset patch # User wenzelm # Date 1396622627 -7200 # Node ID 3610e0a7693cfc59c5405755fb5f5c8ad2fb1c96 # Parent 9cb137ec6ec8f6aa449436fc167752b0539e2e3e# Parent 8e7ebc4b30f16ef620c300c3da1e514b2320658c merged; diff -r 8e7ebc4b30f1 -r 3610e0a7693c src/HOL/Library/Fundamental_Theorem_Algebra.thy --- 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: "(\d\ + norm a) / norm c \ norm z" from c0 have "norm c > 0" by simp - from h c0 have th0: "\d\ + norm a \ norm (z*c)" + from h c0 have th0: "\d\ + norm a \ norm (z * c)" by (simp add: field_simps norm_mult) have ath: "\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) \ norm (a + z * c) + norm a" by (simp add: algebra_simps) from ath[OF th1 th0] have "d \ 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)) \ \1 - t^k\ + cmod (?w^k * ?w * poly s ?w)" unfolding norm_of_real by simp have ath: "\x (t::real). 0\ x \ x < t \ t\1 \ \1 - t\ + x < 1" by arith - have "t *cmod w \ 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto + have "t * cmod w \ 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto then have tw: "cmod ?w \ 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 \ c = y" by simp end - diff -r 8e7ebc4b30f1 -r 3610e0a7693c src/HOL/Quickcheck_Narrowing.thy --- 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 \ term" \ (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 *} diff -r 8e7ebc4b30f1 -r 3610e0a7693c src/HOL/Tools/ATP/atp_proof.ML --- 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: *) -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 ... *) +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 = diff -r 8e7ebc4b30f1 -r 3610e0a7693c src/HOL/Tools/ATP/atp_systems.ML --- 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,