src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
changeset 58059 4e477dcd050a
parent 58058 1a0b18176548
child 58957 c9e744ea8a38
equal deleted inserted replaced
58058:1a0b18176548 58059:4e477dcd050a
    50 
    50 
    51 fun by_schematic_rule ctxt ct =
    51 fun by_schematic_rule ctxt ct =
    52   the (Old_Z3_Proof_Tools.net_instance (Old_Z3_Rules.get (Context.Proof ctxt)) ct)
    52   the (Old_Z3_Proof_Tools.net_instance (Old_Z3_Rules.get (Context.Proof ctxt)) ct)
    53 
    53 
    54 val _ = Theory.setup
    54 val _ = Theory.setup
    55  (Attrib.setup @{binding z3_rule} (Attrib.add_del add del) description #>
    55  (Attrib.setup @{binding old_z3_rule} (Attrib.add_del add del) description #>
    56   Global_Theory.add_thms_dynamic (@{binding z3_rule}, Net.content o Old_Z3_Rules.get))
    56   Global_Theory.add_thms_dynamic (@{binding old_z3_rule}, Net.content o Old_Z3_Rules.get))
    57 
    57 
    58 end
    58 end
    59 
    59 
    60 
    60 
    61 
    61 
    78   let
    78   let
    79     fun try_apply_err ct = Pretty.string_of (Pretty.chunks [
    79     fun try_apply_err ct = Pretty.string_of (Pretty.chunks [
    80       Pretty.big_list ("Z3 found a proof," ^
    80       Pretty.big_list ("Z3 found a proof," ^
    81         " but proof reconstruction failed at the following subgoal:")
    81         " but proof reconstruction failed at the following subgoal:")
    82         (pretty_goal ctxt thms (Thm.term_of ct)),
    82         (pretty_goal ctxt thms (Thm.term_of ct)),
    83       Pretty.str ("Declaring a rule as [z3_rule] might solve this problem.")])
    83       Pretty.str ("Declaring a rule as [old_z3_rule] might solve this problem.")])
    84 
    84 
    85     fun apply [] ct = error (try_apply_err ct)
    85     fun apply [] ct = error (try_apply_err ct)
    86       | apply (prover :: provers) ct =
    86       | apply (prover :: provers) ct =
    87           (case try prover ct of
    87           (case try prover ct of
    88             SOME thm => (Old_SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
    88             SOME thm => (Old_SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
   868     val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
   868     val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
   869     val (asserted, steps, vars, ctxt1) =
   869     val (asserted, steps, vars, ctxt1) =
   870       Old_Z3_Proof_Parser.parse ctxt typs terms output
   870       Old_Z3_Proof_Parser.parse ctxt typs terms output
   871 
   871 
   872     val simpset =
   872     val simpset =
   873       Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems z3_simp})
   873       Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems old_z3_simp})
   874 
   874 
   875     val ((is, rules), cxp as (ctxt2, _)) =
   875     val ((is, rules), cxp as (ctxt2, _)) =
   876       add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
   876       add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
   877   in
   877   in
   878     if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI})
   878     if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI})