# HG changeset patch
# User wenzelm
# Date 1408206707 -7200
# Node ID e6ee35b8f4b5eefc19b3626de2c042a2ee8f84cb
# Parent  3ab5d15fac6bc3139b8a85e5b6840ad23d7a4528
updated to named_theorems;
modernized setup;
tuned;

diff -r 3ab5d15fac6b -r e6ee35b8f4b5 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Sat Aug 16 18:08:55 2014 +0200
+++ b/src/HOL/SMT.thy	Sat Aug 16 18:31:47 2014 +0200
@@ -126,6 +126,7 @@
 ML_file "Tools/SMT/z3_proof_tools.ML"
 ML_file "Tools/SMT/z3_proof_literals.ML"
 ML_file "Tools/SMT/z3_proof_methods.ML"
+named_theorems z3_simp "simplification rules for Z3 proof reconstruction"
 ML_file "Tools/SMT/z3_proof_reconstruction.ML"
 ML_file "Tools/SMT/z3_model.ML"
 ML_file "Tools/SMT/smt_setup_solvers.ML"
@@ -135,7 +136,6 @@
   SMT_Normalize.setup #>
   SMTLIB_Interface.setup #>
   Z3_Interface.setup #>
-  Z3_Proof_Reconstruction.setup #>
   SMT_Setup_Solvers.setup
 *}
 
diff -r 3ab5d15fac6b -r e6ee35b8f4b5 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Aug 16 18:08:55 2014 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Aug 16 18:31:47 2014 +0200
@@ -7,9 +7,7 @@
 signature Z3_PROOF_RECONSTRUCTION =
 sig
   val add_z3_rule: thm -> Context.generic -> Context.generic
-  val reconstruct: Proof.context -> SMT_Translate.recon -> string list ->
-    int list * thm
-  val setup: theory -> theory
+  val reconstruct: Proof.context -> SMT_Translate.recon -> string list -> int list * thm
 end
 
 structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
@@ -23,8 +21,6 @@
 
 (* net of schematic rules *)
 
-val z3_ruleN = "z3_rule"
-
 local
   val description = "declaration of Z3 proof rules"
 
@@ -55,9 +51,9 @@
 fun by_schematic_rule ctxt ct =
   the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
 
-val z3_rules_setup =
-  Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
-  Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
+val _ = Theory.setup
+ (Attrib.setup @{binding z3_rule} (Attrib.add_del add del) description #>
+  Global_Theory.add_thms_dynamic (@{binding z3_rule}, Net.content o Z3_Rules.get))
 
 end
 
@@ -84,8 +80,7 @@
       Pretty.big_list ("Z3 found a proof," ^
         " but proof reconstruction failed at the following subgoal:")
         (pretty_goal ctxt thms (Thm.term_of ct)),
-      Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^
-        " might solve this problem.")])
+      Pretty.str ("Declaring a rule as [z3_rule] might solve this problem.")])
 
     fun apply [] ct = error (try_apply_err ct)
       | apply (prover :: provers) ct =
@@ -671,12 +666,6 @@
      * normal forms for polynoms (integer/real arithmetic)
      * quantifier elimination over linear arithmetic
      * ... ? **)
-structure Z3_Simps = Named_Thms
-(
-  val name = @{binding z3_simp}
-  val description = "simplification rules for Z3 proof reconstruction"
-)
-
 local
   fun spec_meta_eq_of thm =
     (case try (fn th => th RS @{thm spec}) thm of
@@ -880,7 +869,8 @@
     val (asserted, steps, vars, ctxt1) =
       Z3_Proof_Parser.parse ctxt typs terms output
 
-    val simpset = Z3_Proof_Tools.make_simpset ctxt1 (Z3_Simps.get ctxt1)
+    val simpset =
+      Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems z3_simp})
 
     val ((is, rules), cxp as (ctxt2, _)) =
       add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
@@ -895,6 +885,4 @@
 
 end
 
-val setup = z3_rules_setup #> Z3_Simps.setup
-
 end