# HG changeset patch
# User wenzelm
# Date 1289580243 -3600
# Node ID b41c6b5a7a35ee0175bff48e29cfcb8b7ae769e6
# Parent  516a367eb38cf311b281ad0e8224a0f185b6fe31# Parent  0bc83ae22789ef4ea64e3027712f9d30a307f545
merged

diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- 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]]
 
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Boogie/Examples/Boogie_Max.thy
--- 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]]
 
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
--- 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 *}
 
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Boogie/Examples/VCC_Max.thy
--- 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]]
 
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Boogie/Tools/boogie_commands.ML
--- 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 =
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Multivariate_Analysis/Integration.thy
--- 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]]
 
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/SMT_Examples/SMT_Examples.thy
--- 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]]
 
 
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/SMT_Examples/SMT_Tests.thy
--- 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]]
 
 
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/SMT_Examples/SMT_Word_Examples.thy
--- 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]]
 
 
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Tools/SMT/smt_config.ML
--- 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
 
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Tools/SMT/smt_failure.ML
--- 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 ^ ":")
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Tools/SMT/smt_monomorph.ML
--- 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
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Tools/SMT/smt_real.ML
--- 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 =
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Tools/SMT/smt_solver.ML
--- 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)
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Tools/SMT/z3_interface.ML
--- 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)
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Tools/SMT/z3_proof_parser.ML
--- 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 =
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- 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) =>
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- 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 |>
diff -r 0bc83ae22789 -r b41c6b5a7a35 src/HOLCF/Tools/repdef.ML
--- 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 =