updated to named_theorems;
authorwenzelm
Sat Aug 16 18:31:47 2014 +0200 (2014-08-16)
changeset 57957e6ee35b8f4b5
parent 57956 3ab5d15fac6b
child 57958 045c96e3edf0
updated to named_theorems;
modernized setup;
tuned;
src/HOL/SMT.thy
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
     1.1 --- a/src/HOL/SMT.thy	Sat Aug 16 18:08:55 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Sat Aug 16 18:31:47 2014 +0200
     1.3 @@ -126,6 +126,7 @@
     1.4  ML_file "Tools/SMT/z3_proof_tools.ML"
     1.5  ML_file "Tools/SMT/z3_proof_literals.ML"
     1.6  ML_file "Tools/SMT/z3_proof_methods.ML"
     1.7 +named_theorems z3_simp "simplification rules for Z3 proof reconstruction"
     1.8  ML_file "Tools/SMT/z3_proof_reconstruction.ML"
     1.9  ML_file "Tools/SMT/z3_model.ML"
    1.10  ML_file "Tools/SMT/smt_setup_solvers.ML"
    1.11 @@ -135,7 +136,6 @@
    1.12    SMT_Normalize.setup #>
    1.13    SMTLIB_Interface.setup #>
    1.14    Z3_Interface.setup #>
    1.15 -  Z3_Proof_Reconstruction.setup #>
    1.16    SMT_Setup_Solvers.setup
    1.17  *}
    1.18  
     2.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Aug 16 18:08:55 2014 +0200
     2.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat Aug 16 18:31:47 2014 +0200
     2.3 @@ -7,9 +7,7 @@
     2.4  signature Z3_PROOF_RECONSTRUCTION =
     2.5  sig
     2.6    val add_z3_rule: thm -> Context.generic -> Context.generic
     2.7 -  val reconstruct: Proof.context -> SMT_Translate.recon -> string list ->
     2.8 -    int list * thm
     2.9 -  val setup: theory -> theory
    2.10 +  val reconstruct: Proof.context -> SMT_Translate.recon -> string list -> int list * thm
    2.11  end
    2.12  
    2.13  structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
    2.14 @@ -23,8 +21,6 @@
    2.15  
    2.16  (* net of schematic rules *)
    2.17  
    2.18 -val z3_ruleN = "z3_rule"
    2.19 -
    2.20  local
    2.21    val description = "declaration of Z3 proof rules"
    2.22  
    2.23 @@ -55,9 +51,9 @@
    2.24  fun by_schematic_rule ctxt ct =
    2.25    the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
    2.26  
    2.27 -val z3_rules_setup =
    2.28 -  Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
    2.29 -  Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
    2.30 +val _ = Theory.setup
    2.31 + (Attrib.setup @{binding z3_rule} (Attrib.add_del add del) description #>
    2.32 +  Global_Theory.add_thms_dynamic (@{binding z3_rule}, Net.content o Z3_Rules.get))
    2.33  
    2.34  end
    2.35  
    2.36 @@ -84,8 +80,7 @@
    2.37        Pretty.big_list ("Z3 found a proof," ^
    2.38          " but proof reconstruction failed at the following subgoal:")
    2.39          (pretty_goal ctxt thms (Thm.term_of ct)),
    2.40 -      Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^
    2.41 -        " might solve this problem.")])
    2.42 +      Pretty.str ("Declaring a rule as [z3_rule] might solve this problem.")])
    2.43  
    2.44      fun apply [] ct = error (try_apply_err ct)
    2.45        | apply (prover :: provers) ct =
    2.46 @@ -671,12 +666,6 @@
    2.47       * normal forms for polynoms (integer/real arithmetic)
    2.48       * quantifier elimination over linear arithmetic
    2.49       * ... ? **)
    2.50 -structure Z3_Simps = Named_Thms
    2.51 -(
    2.52 -  val name = @{binding z3_simp}
    2.53 -  val description = "simplification rules for Z3 proof reconstruction"
    2.54 -)
    2.55 -
    2.56  local
    2.57    fun spec_meta_eq_of thm =
    2.58      (case try (fn th => th RS @{thm spec}) thm of
    2.59 @@ -880,7 +869,8 @@
    2.60      val (asserted, steps, vars, ctxt1) =
    2.61        Z3_Proof_Parser.parse ctxt typs terms output
    2.62  
    2.63 -    val simpset = Z3_Proof_Tools.make_simpset ctxt1 (Z3_Simps.get ctxt1)
    2.64 +    val simpset =
    2.65 +      Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems z3_simp})
    2.66  
    2.67      val ((is, rules), cxp as (ctxt2, _)) =
    2.68        add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
    2.69 @@ -895,6 +885,4 @@
    2.70  
    2.71  end
    2.72  
    2.73 -val setup = z3_rules_setup #> Z3_Simps.setup
    2.74 -
    2.75  end