--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Fri Nov 12 17:44:03 2010 +0100
@@ -79,9 +79,9 @@
*}
-boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
+boogie_open "Boogie_Dijkstra"
-declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]]
+declare [[smt_certificates="Boogie_Dijkstra.certs"]]
declare [[smt_fixed=true]]
declare [[smt_oracle=false]]
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Fri Nov 12 17:44:03 2010 +0100
@@ -36,9 +36,9 @@
\end{verbatim}
*}
-boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
+boogie_open "Boogie_Max"
-declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Max.certs"]]
+declare [[smt_certificates="Boogie_Max.certs"]]
declare [[smt_fixed=true]]
declare [[smt_oracle=false]]
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Fri Nov 12 17:44:03 2010 +0100
@@ -36,7 +36,7 @@
\end{verbatim}
*}
-boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
+boogie_open "Boogie_Max"
boogie_status -- {* gives an overview of all verification conditions *}
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy Fri Nov 12 17:44:03 2010 +0100
@@ -44,9 +44,9 @@
\end{verbatim}
*}
-boogie_open (quiet) "~~/src/HOL/Boogie/Examples/VCC_Max"
+boogie_open (quiet) "VCC_Max"
-declare [[smt_certificates="~~/src/HOL/Boogie/Examples/VCC_Max.certs"]]
+declare [[smt_certificates="VCC_Max.certs"]]
declare [[smt_fixed=true]]
declare [[smt_oracle=false]]
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Nov 12 17:44:03 2010 +0100
@@ -16,13 +16,20 @@
fun boogie_open ((quiet, base_name), offsets) thy =
let
- val path = Path.explode (base_name ^ ".b2i")
- val _ = File.exists path orelse
- error ("Unable to find file " ^ quote (Path.implode path))
+ val ext = "b2i"
+ fun add_ext path = path |> snd (Path.split_ext path) <> ext ? Path.ext ext
+ val base_path = add_ext (Path.explode base_name)
+ val path_id = Thy_Load.check_file [Thy_Load.master_directory thy] base_path
+
val _ = Boogie_VCs.is_closed thy orelse
error ("Found the beginning of a new Boogie environment, " ^
"but another Boogie environment is still open.")
- in Boogie_Loader.load_b2i (not quiet) offsets path thy end
+ in
+ thy
+ |> Thy_Load.require base_path
+ |> Boogie_Loader.load_b2i (not quiet) offsets (fst path_id)
+ |> Thy_Load.provide (base_path, path_id)
+ end
datatype vc_opts =
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 12 17:44:03 2010 +0100
@@ -7,7 +7,7 @@
imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function
begin
-declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]]
+declare [[smt_certificates="Integration.certs"]]
declare [[smt_fixed=true]]
declare [[smt_oracle=false]]
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Fri Nov 12 17:44:03 2010 +0100
@@ -9,7 +9,7 @@
begin
declare [[smt_solver=z3, smt_oracle=false]]
-declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Examples.certs"]]
+declare [[smt_certificates="SMT_Examples.certs"]]
declare [[smt_fixed=true]]
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Fri Nov 12 17:44:03 2010 +0100
@@ -9,7 +9,7 @@
begin
declare [[smt_solver=z3, smt_oracle=false]]
-declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Tests.certs"]]
+declare [[smt_certificates="SMT_Tests.certs"]]
declare [[smt_fixed=true]]
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy Fri Nov 12 17:44:03 2010 +0100
@@ -9,7 +9,7 @@
begin
declare [[smt_solver=z3, smt_oracle=true]]
-declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Word_Examples.certs"]]
+declare [[smt_certificates="SMT_Word_Examples.certs"]]
declare [[smt_fixed=true]]
--- a/src/HOL/Tools/SMT/smt_config.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Fri Nov 12 17:44:03 2010 +0100
@@ -173,9 +173,12 @@
val get_certificates_path =
Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
-fun select_certificates name = Certificates.put (
+fun select_certificates name context = context |> Certificates.put (
if name = "" then NONE
- else SOME (Cache_IO.make (Path.explode name)))
+ else
+ Path.explode name
+ |> Path.append (Thy_Load.master_directory (Context.theory_of context))
+ |> SOME o Cache_IO.make)
val certificates_of = Certificates.get o Context.Proof
--- a/src/HOL/Tools/SMT/smt_failure.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_failure.ML Fri Nov 12 17:44:03 2010 +0100
@@ -26,7 +26,9 @@
fun string_of_failure ctxt (Counterexample (real, ex)) =
let
- val msg = (if real then "C" else "Potential c") ^ "ounterexample found"
+ val msg =
+ if real then "Counterexample found (possibly spurious)"
+ else "Potential counterexample found"
in
if null ex then msg
else Pretty.string_of (Pretty.big_list (msg ^ ":")
--- a/src/HOL/Tools/SMT/smt_monomorph.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML Fri Nov 12 17:44:03 2010 +0100
@@ -17,8 +17,7 @@
val ignored = member (op =) [
@{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
- @{const_name HOL.eq}, @{const_name zero_class.zero},
- @{const_name one_class.one}, @{const_name number_of}]
+ @{const_name HOL.eq}]
fun is_const f (n, T) = not (ignored n) andalso f T
fun add_const_if f g (Const c) = if is_const f c then g c else I
--- a/src/HOL/Tools/SMT/smt_real.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML Fri Nov 12 17:44:03 2010 +0100
@@ -78,7 +78,8 @@
local
structure I = Z3_Interface
- fun z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real}
+ fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
+ | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
| z3_mk_builtin_typ _ = NONE
fun z3_mk_builtin_num _ i T =
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Nov 12 17:44:03 2010 +0100
@@ -342,8 +342,12 @@
val str_of = SMT_Failure.string_of_failure ctxt'
fun safe_solve irules =
if pass_exns then SOME (solve irules)
- else (SOME (solve irules) handle SMT_Failure.SMT fail =>
- (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
+ else (SOME (solve irules)
+ handle
+ SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
+ (C.verbose_msg ctxt' (prefix tag o str_of) fail; NONE)
+ | SMT_Failure.SMT fail =>
+ (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
in
safe_solve (map (pair ~1) (rules @ prems))
|> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
--- a/src/HOL/Tools/SMT/z3_interface.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Fri Nov 12 17:44:03 2010 +0100
@@ -155,7 +155,8 @@
(* basic and additional constructors *)
fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}
- | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int}
+ | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
+ | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int} (*FIXME: delete*)
| mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym
fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i)
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Fri Nov 12 17:44:03 2010 +0100
@@ -13,7 +13,7 @@
PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
- CnfStar | Skolemize | ModusPonensOeq | ThLemma
+ CnfStar | Skolemize | ModusPonensOeq | ThLemma of string list
val string_of_rule: rule -> string
(* proof parser *)
@@ -41,7 +41,7 @@
PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
- CnfStar | Skolemize | ModusPonensOeq | ThLemma
+ CnfStar | Skolemize | ModusPonensOeq | ThLemma of string list
val rule_names = Symtab.make [
("true-axiom", TrueAxiom),
@@ -81,11 +81,12 @@
("cnf*", CnfStar),
("sk", Skolemize),
("mp~", ModusPonensOeq),
- ("th-lemma", ThLemma)]
+ ("th-lemma", ThLemma [])]
-fun string_of_rule r =
- let fun eq_rule (s, r') = if r = r' then SOME s else NONE
- in the (Symtab.get_first eq_rule rule_names) end
+fun string_of_rule (ThLemma args) = space_implode " " ("th-lemma" :: args)
+ | string_of_rule r =
+ let fun eq_rule (s, r') = if r = r' then SOME s else NONE
+ in the (Symtab.get_first eq_rule rule_names) end
@@ -271,14 +272,17 @@
fun $$ s = Scan.lift (Scan.$$ s)
fun this s = Scan.lift (Scan.this_string s)
-fun blank st = Scan.lift (Scan.many1 Symbol.is_ascii_blank) st
+val is_blank = Symbol.is_ascii_blank
+fun blank st = Scan.lift (Scan.many1 is_blank) st
fun sep scan = blank |-- scan
fun seps scan = Scan.repeat (sep scan)
fun seps1 scan = Scan.repeat1 (sep scan)
fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan)
-fun par scan = $$ "(" |-- scan --| $$ ")"
-fun bra scan = $$ "[" |-- scan --| $$ "]"
+val lpar = "(" and rpar = ")"
+val lbra = "[" and rbra = "]"
+fun par scan = $$ lpar |-- scan --| $$ rpar
+fun bra scan = $$ lbra |-- scan --| $$ rbra
val digit = (fn
"0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
@@ -368,8 +372,14 @@
Scan.first [bound, quantifier, pattern, application, number, constant] :|--
with_context (pair NONE oo add_expr k)
+fun th_lemma_arg st =
+ Scan.lift (Scan.many1 (not o (is_blank orf equal rbra)) >> implode) st
+
fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn
- (SOME r, _) => Scan.succeed r
+ (SOME (ThLemma _), _) =>
+ let fun stop st = (sep id >> K "" || $$ rbra) st
+ in Scan.repeat (Scan.unless stop (sep th_lemma_arg)) >> ThLemma end
+ | (SOME r, _) => Scan.succeed r
| (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st
fun rule f k =
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Nov 12 17:44:03 2010 +0100
@@ -787,7 +787,7 @@
| (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
(* theory rules *)
- | (P.ThLemma, _) =>
+ | (P.ThLemma _, _) => (* FIXME: use arguments *)
(th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
| (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp)
| (P.RewriteStar, ps) =>
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 12 17:44:03 2010 +0100
@@ -406,7 +406,7 @@
: (Domain_Take_Proofs.iso_info list
* Domain_Take_Proofs.take_induct_info) * theory =
let
- val _ = Theory.requires thy "Representable" "domain isomorphisms";
+ val _ = Theory.requires thy "Domain" "domain isomorphisms";
(* this theory is used just for parsing *)
val tmp_thy = thy |>
--- a/src/HOLCF/Tools/repdef.ML Fri Nov 12 14:51:28 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML Fri Nov 12 17:44:03 2010 +0100
@@ -88,7 +88,7 @@
(thy: theory)
: (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory =
let
- val _ = Theory.requires thy "Representable" "repdefs";
+ val _ = Theory.requires thy "Domain" "repdefs";
(*rhs*)
val tmp_ctxt =