src/HOL/Tools/SMT2/z3_new_replay_methods.ML
author boehmes
Sat, 31 May 2014 22:59:54 +0200
changeset 57145 7292a7258750
parent 57144 1d12e22e7caf
child 57220 853557cf2efa
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56090
34bd10a9a2ad adapted to renamed ML files
blanchet
parents: 56089
diff changeset
     1
(*  Title:      HOL/Tools/SMT2/z3_new_replay_methods.ML
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     4
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     5
Proof methods for replaying Z3 proofs.
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     6
*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     7
56090
34bd10a9a2ad adapted to renamed ML files
blanchet
parents: 56089
diff changeset
     8
signature Z3_NEW_REPLAY_METHODS =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     9
sig
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    10
  (*abstraction*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    11
  type abs_context = int * term Termtab.table
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    12
  type 'a abstracter = term -> abs_context -> 'a * abs_context
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    13
  val add_arith_abstracter: (term abstracter -> term option abstracter) ->
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    14
    Context.generic -> Context.generic
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    15
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    16
  (*theory lemma methods*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    17
  type th_lemma_method = Proof.context -> thm list -> term -> thm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    18
  val add_th_lemma_method: string * th_lemma_method -> Context.generic ->
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    19
    Context.generic
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    20
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    21
  (*methods for Z3 proof rules*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    22
  type z3_method = Proof.context -> thm list -> term -> thm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    23
  val true_axiom: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    24
  val mp: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    25
  val refl: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    26
  val symm: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    27
  val trans: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    28
  val cong: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    29
  val quant_intro: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    30
  val distrib: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    31
  val and_elim: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    32
  val not_or_elim: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    33
  val rewrite: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    34
  val rewrite_star: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    35
  val pull_quant: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    36
  val push_quant: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    37
  val elim_unused: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    38
  val dest_eq_res: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    39
  val quant_inst: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    40
  val lemma: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    41
  val unit_res: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    42
  val iff_true: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    43
  val iff_false: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    44
  val comm: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    45
  val def_axiom: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    46
  val apply_def: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    47
  val iff_oeq: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    48
  val nnf_pos: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    49
  val nnf_neg: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    50
  val mp_oeq: z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    51
  val th_lemma: string -> z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    52
  val is_assumption: Z3_New_Proof.z3_rule -> bool
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    53
  val method_for: Z3_New_Proof.z3_rule -> z3_method
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    54
end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    55
56090
34bd10a9a2ad adapted to renamed ML files
blanchet
parents: 56089
diff changeset
    56
structure Z3_New_Replay_Methods: Z3_NEW_REPLAY_METHODS =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    57
struct
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    58
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    59
type z3_method = Proof.context -> thm list -> term -> thm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    60
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    61
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    62
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    63
(* utility functions *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    64
56816
2f3756ccba41 use internal proof-producing SAT solver for more efficient SMT proof replay
boehmes
parents: 56090
diff changeset
    65
fun trace ctxt f = SMT2_Config.trace_msg ctxt f ()
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    66
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    67
fun pretty_thm ctxt thm = Syntax.pretty_term ctxt (Thm.concl_of thm)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    68
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    69
fun pretty_goal ctxt msg rule thms t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    70
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    71
    val full_msg = msg ^ ": " ^ quote (Z3_New_Proof.string_of_rule rule)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    72
    val assms =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    73
      if null thms then []
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    74
      else [Pretty.big_list "assumptions:" (map (pretty_thm ctxt) thms)]
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    75
    val concl = Pretty.big_list "proposition:" [Syntax.pretty_term ctxt t]
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    76
  in Pretty.big_list full_msg (assms @ [concl]) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    77
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    78
fun replay_error ctxt msg rule thms t = error (Pretty.string_of (pretty_goal ctxt msg rule thms t))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    79
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    80
fun replay_rule_error ctxt = replay_error ctxt "Failed to replay Z3 proof step"
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    81
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    82
fun trace_goal ctxt rule thms t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    83
  trace ctxt (fn () => Pretty.string_of (pretty_goal ctxt "Goal" rule thms t))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    84
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    85
fun as_prop (t as Const (@{const_name Trueprop}, _) $ _) = t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    86
  | as_prop t = HOLogic.mk_Trueprop t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    87
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    88
fun dest_prop (Const (@{const_name Trueprop}, _) $ t) = t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    89
  | dest_prop t = t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    90
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    91
fun dest_thm thm = dest_prop (Thm.concl_of thm)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    92
56090
34bd10a9a2ad adapted to renamed ML files
blanchet
parents: 56089
diff changeset
    93
fun certify_prop ctxt t = SMT2_Util.certify ctxt (as_prop t)
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    94
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    95
fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    96
  | try_provers ctxt rule ((name, prover) :: named_provers) thms t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    97
      (case (trace ctxt (K ("Trying prover " ^ quote name)); try prover t) of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    98
        SOME thm => thm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    99
      | NONE => try_provers ctxt rule named_provers thms t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   100
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   101
fun match ctxt pat t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   102
  (Vartab.empty, Vartab.empty)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   103
  |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   104
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   105
fun gen_certify_inst sel mk cert ctxt thm t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   106
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   107
    val inst = match ctxt (dest_thm thm) (dest_prop t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   108
    fun cert_inst (ix, (a, b)) = (cert (mk (ix, a)), cert b)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   109
  in Vartab.fold (cons o cert_inst) (sel inst) [] end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   110
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   111
fun match_instantiateT ctxt t thm =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   112
  if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   113
    let val certT = Thm.ctyp_of (Proof_Context.theory_of ctxt)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   114
    in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   115
  else thm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   116
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   117
fun match_instantiate ctxt t thm =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   118
  let
56090
34bd10a9a2ad adapted to renamed ML files
blanchet
parents: 56089
diff changeset
   119
    val cert = SMT2_Util.certify ctxt
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   120
    val thm' = match_instantiateT ctxt t thm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   121
  in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   122
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   123
fun apply_rule ctxt t =
56090
34bd10a9a2ad adapted to renamed ML files
blanchet
parents: 56089
diff changeset
   124
  (case Z3_New_Replay_Rules.apply ctxt (certify_prop ctxt t) of
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   125
    SOME thm => thm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   126
  | NONE => raise Fail "apply_rule")
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   127
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   128
fun discharge _ [] thm = thm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   129
  | discharge i (rule :: rules) thm = discharge (i + Thm.nprems_of rule) rules (rule RSN (i, thm))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   130
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   131
fun by_tac ctxt thms ns ts t tac =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   132
  Goal.prove ctxt [] (map as_prop ts) (as_prop t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   133
    (fn {context, prems} => HEADGOAL (tac context prems))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   134
  |> Drule.generalize ([], ns)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   135
  |> discharge 1 thms
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   136
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   137
fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   138
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   139
fun prop_tac ctxt prems =
56816
2f3756ccba41 use internal proof-producing SAT solver for more efficient SMT proof replay
boehmes
parents: 56090
diff changeset
   140
  Method.insert_tac prems
2f3756ccba41 use internal proof-producing SAT solver for more efficient SMT proof replay
boehmes
parents: 56090
diff changeset
   141
  THEN' SUBGOAL (fn (prop, i) =>
2f3756ccba41 use internal proof-producing SAT solver for more efficient SMT proof replay
boehmes
parents: 56090
diff changeset
   142
    if Term.size_of_term prop > 100 then SAT.satx_tac ctxt i
2f3756ccba41 use internal proof-producing SAT solver for more efficient SMT proof replay
boehmes
parents: 56090
diff changeset
   143
    else (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) i)
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   144
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   145
fun quant_tac ctxt = Blast.blast_tac ctxt
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   146
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   147
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   148
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   149
(* plug-ins *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   150
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   151
type abs_context = int * term Termtab.table
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   152
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   153
type 'a abstracter = term -> abs_context -> 'a * abs_context
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   154
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   155
type th_lemma_method = Proof.context -> thm list -> term -> thm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   156
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   157
fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   158
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   159
structure Plugins = Generic_Data
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   160
(
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   161
  type T =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   162
    (int * (term abstracter -> term option abstracter)) list *
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   163
    th_lemma_method Symtab.table
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   164
  val empty = ([], Symtab.empty)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   165
  val extend = I
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   166
  fun merge ((abss1, ths1), (abss2, ths2)) = (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   167
    Ord_List.merge id_ord (abss1, abss2),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   168
    Symtab.merge (K true) (ths1, ths2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   169
)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   170
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   171
fun add_arith_abstracter abs = Plugins.map (apfst (Ord_List.insert id_ord (serial (), abs)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   172
fun get_arith_abstracters ctxt = map snd (fst (Plugins.get (Context.Proof ctxt)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   173
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   174
fun add_th_lemma_method method = Plugins.map (apsnd (Symtab.update_new method))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   175
fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   176
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   177
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   178
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   179
(* abstraction *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   180
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   181
fun prove_abstract ctxt thms t tac f =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   182
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   183
    val ((prems, concl), (_, ts)) = f (1, Termtab.empty)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   184
    val ns = Termtab.fold (fn (_, v) => cons (fst (Term.dest_Free v))) ts []
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   185
  in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   186
    by_tac ctxt [] ns prems concl tac
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   187
    |> match_instantiate ctxt t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   188
    |> discharge 1 thms
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   189
  end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   190
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   191
fun prove_abstract' ctxt t tac f =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   192
  prove_abstract ctxt [] t tac (f #>> pair [])
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   193
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   194
fun lookup_term (_, terms) t = Termtab.lookup terms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   195
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   196
fun abstract_sub t f cx =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   197
  (case lookup_term cx t of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   198
    SOME v => (v, cx)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   199
  | NONE => f cx)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   200
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   201
fun mk_fresh_free t (i, terms) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   202
  let val v = Free ("t" ^ string_of_int i, fastype_of t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   203
  in (v, (i + 1, Termtab.update (t, v) terms)) end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   204
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   205
fun apply_abstracters _ [] _ cx = (NONE, cx)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   206
  | apply_abstracters abs (abstracter :: abstracters) t cx =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   207
      (case abstracter abs t cx of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   208
        (NONE, _) => apply_abstracters abs abstracters t cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   209
      | x as (SOME _, _) => x)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   210
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   211
fun abstract_term (t as _ $ _) = abstract_sub t (mk_fresh_free t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   212
  | abstract_term (t as Abs _) = abstract_sub t (mk_fresh_free t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   213
  | abstract_term t = pair t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   214
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   215
fun abstract_bin abs f t t1 t2 = abstract_sub t (abs t1 ##>> abs t2 #>> f)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   216
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   217
fun abstract_ter abs f t t1 t2 t3 =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   218
  abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Parse.triple1 #> f))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   219
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   220
fun abstract_lit (@{const HOL.Not} $ t) = abstract_term t #>> HOLogic.mk_not
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   221
  | abstract_lit t = abstract_term t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   222
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   223
fun abstract_not abs (t as @{const HOL.Not} $ t1) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   224
      abstract_sub t (abs t1 #>> HOLogic.mk_not)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   225
  | abstract_not _ t = abstract_lit t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   226
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   227
fun abstract_conj (t as @{const HOL.conj} $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   228
      abstract_bin abstract_conj HOLogic.mk_conj t t1 t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   229
  | abstract_conj t = abstract_lit t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   230
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   231
fun abstract_disj (t as @{const HOL.disj} $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   232
      abstract_bin abstract_disj HOLogic.mk_disj t t1 t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   233
  | abstract_disj t = abstract_lit t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   234
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   235
fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   236
      abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   237
  | abstract_prop (t as @{const HOL.disj} $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   238
      abstract_bin abstract_prop HOLogic.mk_disj t t1 t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   239
  | abstract_prop (t as @{const HOL.conj} $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   240
      abstract_bin abstract_prop HOLogic.mk_conj t t1 t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   241
  | abstract_prop (t as @{const HOL.implies} $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   242
      abstract_bin abstract_prop HOLogic.mk_imp t t1 t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   243
  | abstract_prop (t as @{term "HOL.eq :: bool => _"} $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   244
      abstract_bin abstract_prop HOLogic.mk_eq t t1 t2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   245
  | abstract_prop t = abstract_not abstract_prop t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   246
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   247
fun abstract_arith ctxt u =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   248
  let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   249
    fun abs (t as (c as Const _) $ Abs (s, T, t')) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   250
          abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   251
      | abs (t as (c as Const (@{const_name If}, _)) $ t1 $ t2 $ t3) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   252
          abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   253
      | abs (t as @{const HOL.Not} $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   254
      | abs (t as @{const HOL.disj} $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   255
          abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   256
      | abs (t as (c as Const (@{const_name uminus_class.uminus}, _)) $ t1) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   257
          abstract_sub t (abs t1 #>> (fn u => c $ u))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   258
      | abs (t as (c as Const (@{const_name plus_class.plus}, _)) $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   259
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   260
      | abs (t as (c as Const (@{const_name minus_class.minus}, _)) $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   261
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   262
      | abs (t as (c as Const (@{const_name times_class.times}, _)) $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   263
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   264
      | abs (t as (c as Const (@{const_name z3div}, _)) $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   265
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   266
      | abs (t as (c as Const (@{const_name z3mod}, _)) $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   267
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   268
      | abs (t as (c as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   269
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   270
      | abs (t as (c as Const (@{const_name ord_class.less}, _)) $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   271
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   272
      | abs (t as (c as Const (@{const_name ord_class.less_eq}, _)) $ t1 $ t2) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   273
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   274
      | abs t = abstract_sub t (fn cx =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   275
          if can HOLogic.dest_number t then (t, cx)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   276
          else
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   277
            (case apply_abstracters abs (get_arith_abstracters ctxt) t cx of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   278
              (SOME u, cx') => (u, cx')
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   279
            | (NONE, _) => abstract_term t cx))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   280
  in abs u end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   281
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   282
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   283
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   284
(* truth axiom *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   285
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   286
fun true_axiom _ _ _ = @{thm TrueI}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   287
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   288
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   289
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   290
(* modus ponens *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   291
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   292
fun mp _ [p, p_eq_q] _ = discharge 1 [p_eq_q, p] iffD1
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   293
  | mp ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Modus_Ponens thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   294
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   295
val mp_oeq = mp
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   296
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   297
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   298
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   299
(* reflexivity *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   300
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   301
fun refl ctxt _ t = match_instantiate ctxt t @{thm refl}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   302
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   303
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   304
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   305
(* symmetry *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   306
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   307
fun symm _ [thm] _ = thm RS @{thm sym}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   308
  | symm ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Reflexivity thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   309
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   310
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   311
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   312
(* transitivity *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   313
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   314
fun trans _ [thm1, thm2] _ = thm1 RSN (1, thm2 RSN (2, @{thm trans}))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   315
  | trans ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Transitivity thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   316
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   317
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   318
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   319
(* congruence *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   320
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   321
fun ctac prems i st = st |> (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   322
  resolve_tac (@{thm refl} :: prems) i
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   323
  ORELSE (cong_tac i THEN ctac prems (i + 1) THEN ctac prems i))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   324
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   325
fun cong_basic ctxt thms t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   326
  let val st = Thm.trivial (certify_prop ctxt t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   327
  in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   328
    (case Seq.pull (ctac thms 1 st) of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   329
      SOME (thm, _) => thm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   330
    | NONE => raise THM ("cong", 0, thms @ [st]))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   331
  end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   332
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   333
val cong_dest_rules = @{lemma
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   334
  "(~ P | Q) & (P | ~ Q) ==> P = Q"
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   335
  "(P | ~ Q) & (~ P | Q) ==> P = Q"
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   336
  by fast+}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   337
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   338
fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   339
  Method.insert_tac thms
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   340
  THEN' (Classical.fast_tac ctxt'
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   341
    ORELSE' dresolve_tac cong_dest_rules
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   342
    THEN' Classical.fast_tac ctxt'))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   343
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   344
fun cong ctxt thms = try_provers ctxt Z3_New_Proof.Monotonicity [
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   345
  ("basic", cong_basic ctxt thms),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   346
  ("full", cong_full ctxt thms)] thms
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   347
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   348
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   349
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   350
(* quantifier introduction *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   351
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   352
val quant_intro_rules = @{lemma
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   353
  "(!!x. P x = Q x) ==> (ALL x. P x) = (ALL x. Q x)"
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   354
  "(!!x. P x = Q x) ==> (EX x. P x) = (EX x. Q x)"
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   355
  "(!!x. (~ P x) = Q x) ==> (~ (EX x. P x)) = (ALL x. Q x)"
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   356
  "(!!x. (~ P x) = Q x) ==> (~ (ALL x. P x)) = (EX x. Q x)"
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   357
  by fast+}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   358
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   359
fun quant_intro ctxt [thm] t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   360
    prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac (thm :: quant_intro_rules))))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   361
  | quant_intro ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Quant_Intro thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   362
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   363
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   364
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   365
(* distributivity of conjunctions and disjunctions *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   366
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   367
(* TODO: there are no tests with this proof rule *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   368
fun distrib ctxt _ t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   369
  prove_abstract' ctxt t prop_tac (abstract_prop (dest_prop t))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   370
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   371
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   372
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   373
(* elimination of conjunctions *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   374
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   375
fun and_elim ctxt [thm] t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   376
      prove_abstract ctxt [thm] t prop_tac (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   377
        abstract_lit (dest_prop t) ##>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   378
        abstract_conj (dest_thm thm) #>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   379
        apfst single o swap)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   380
  | and_elim ctxt thms t = replay_rule_error ctxt Z3_New_Proof.And_Elim thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   381
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   382
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   383
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   384
(* elimination of negated disjunctions *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   385
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   386
fun not_or_elim ctxt [thm] t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   387
      prove_abstract ctxt [thm] t prop_tac (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   388
        abstract_lit (dest_prop t) ##>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   389
        abstract_not abstract_disj (dest_thm thm) #>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   390
        apfst single o swap)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   391
  | not_or_elim ctxt thms t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   392
      replay_rule_error ctxt Z3_New_Proof.Not_Or_Elim thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   393
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   394
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   395
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   396
(* rewriting *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   397
57144
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   398
local
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   399
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   400
fun dest_all (Const (@{const_name HOL.All}, _) $ Abs (_, T, t)) nctxt =
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   401
      let
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   402
        val (n, nctxt') = Name.variant "" nctxt
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   403
        val f = Free (n, T)
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   404
        val t' = Term.subst_bound (f, t)
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   405
      in dest_all t' nctxt' |>> cons f end
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   406
  | dest_all t _ = ([], t)
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   407
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   408
fun dest_alls t =
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   409
  let
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   410
    val nctxt = Name.make_context (Term.add_free_names t [])
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   411
    val (lhs, rhs) = HOLogic.dest_eq (dest_prop t)
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   412
    val (ls, lhs') = dest_all lhs nctxt
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   413
    val (rs, rhs') = dest_all rhs nctxt
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   414
  in
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   415
    if eq_list (op aconv) (ls, rs) then SOME (ls, (HOLogic.mk_eq (lhs', rhs')))
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   416
    else NONE
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   417
  end
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   418
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   419
fun forall_intr ctxt t thm =
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   420
  let val ct = Thm.cterm_of (Proof_Context.theory_of ctxt) t
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   421
  in Thm.forall_intr ct thm COMP_INCR @{thm iff_allI} end
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   422
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   423
in
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   424
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   425
fun focus_eq f ctxt t =
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   426
  (case dest_alls t of
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   427
    NONE => f ctxt t
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   428
  | SOME (vs, t') => fold (forall_intr ctxt) vs (f ctxt t'))
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   429
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   430
end
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   431
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   432
fun abstract_eq f (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   433
      f t1 ##>> f t2 #>> HOLogic.mk_eq
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   434
  | abstract_eq _ t = abstract_term t
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   435
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   436
fun prove_prop_rewrite ctxt t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   437
  prove_abstract' ctxt t prop_tac (
57145
boehmes
parents: 57144
diff changeset
   438
    abstract_eq abstract_prop (dest_prop t))
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   439
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   440
fun arith_rewrite_tac ctxt _ =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   441
  TRY o Simplifier.simp_tac ctxt
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   442
  THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   443
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   444
fun prove_arith_rewrite ctxt t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   445
  prove_abstract' ctxt t arith_rewrite_tac (
57144
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   446
    abstract_eq (abstract_arith ctxt) (dest_prop t))
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   447
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   448
fun rewrite ctxt _ = try_provers ctxt Z3_New_Proof.Rewrite [
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   449
  ("rules", apply_rule ctxt),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   450
  ("prop_rewrite", prove_prop_rewrite ctxt),
57144
1d12e22e7caf more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents: 56816
diff changeset
   451
  ("arith_rewrite", focus_eq prove_arith_rewrite ctxt)] []
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   452
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   453
fun rewrite_star ctxt = rewrite ctxt
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   454
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   455
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   456
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   457
(* pulling quantifiers *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   458
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   459
fun pull_quant ctxt _ t = prove ctxt t quant_tac
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   460
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   461
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   462
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   463
(* pushing quantifiers *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   464
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   465
fun push_quant _ _ _ = raise Fail "unsupported" (* FIXME *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   466
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   467
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   468
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   469
(* elimination of unused bound variables *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   470
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   471
val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   472
val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   473
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   474
fun elim_unused_tac i st = (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   475
  match_tac [@{thm refl}]
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   476
  ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   477
  ORELSE' (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   478
    match_tac [@{thm iff_allI}, @{thm iff_exI}]
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   479
    THEN' elim_unused_tac)) i st
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   480
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   481
fun elim_unused ctxt _ t = prove ctxt t (fn _ => elim_unused_tac)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   482
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   483
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   484
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   485
(* destructive equality resolution *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   486
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   487
fun dest_eq_res _ _ _ = raise Fail "dest_eq_res" (* FIXME *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   488
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   489
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   490
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   491
(* quantifier instantiation *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   492
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   493
val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   494
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   495
fun quant_inst ctxt _ t = prove ctxt t (fn _ => 
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   496
  REPEAT_ALL_NEW (rtac quant_inst_rule)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   497
  THEN' rtac @{thm excluded_middle})
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   498
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   499
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   500
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   501
(* propositional lemma *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   502
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   503
exception LEMMA of unit
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   504
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   505
val intro_hyp_rule1 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   506
val intro_hyp_rule2 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   507
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   508
fun norm_lemma thm =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   509
  (thm COMP_INCR intro_hyp_rule1)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   510
  handle THM _ => thm COMP_INCR intro_hyp_rule2
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   511
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   512
fun negated_prop (@{const HOL.Not} $ t) = HOLogic.mk_Trueprop t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   513
  | negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   514
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   515
fun intro_hyps tab (t as @{const HOL.disj} $ t1 $ t2) cx =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   516
      lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   517
  | intro_hyps tab t cx =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   518
      lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   519
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   520
and lookup_intro_hyps tab t f (cx as (thm, terms)) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   521
  (case Termtab.lookup tab (negated_prop t) of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   522
    NONE => f cx
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   523
  | SOME hyp => (norm_lemma (Thm.implies_intr hyp thm), t :: terms))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   524
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   525
fun lemma ctxt (thms as [thm]) t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   526
    (let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   527
       val tab = Termtab.make (map (`Thm.term_of) (#hyps (Thm.crep_thm thm)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   528
       val (thm', terms) = intro_hyps tab (dest_prop t) (thm, [])
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   529
     in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   530
       prove_abstract ctxt [thm'] t prop_tac (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   531
         fold (snd oo abstract_lit) terms #>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   532
         abstract_disj (dest_thm thm') #>> single ##>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   533
         abstract_disj (dest_prop t))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   534
     end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   535
     handle LEMMA () => replay_error ctxt "Bad proof state" Z3_New_Proof.Lemma thms t)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   536
  | lemma ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Lemma thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   537
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   538
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   539
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   540
(* unit resolution *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   541
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   542
fun abstract_unit (t as (@{const HOL.Not} $ (@{const HOL.disj} $ t1 $ t2))) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   543
      abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   544
        HOLogic.mk_not o HOLogic.mk_disj)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   545
  | abstract_unit (t as (@{const HOL.disj} $ t1 $ t2)) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   546
      abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   547
        HOLogic.mk_disj)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   548
  | abstract_unit t = abstract_lit t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   549
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   550
fun unit_res ctxt thms t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   551
  prove_abstract ctxt thms t prop_tac (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   552
    fold_map (abstract_unit o dest_thm) thms ##>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   553
    abstract_unit (dest_prop t) #>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   554
    (fn (prems, concl) => (prems, concl)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   555
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   556
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   557
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   558
(* iff-true *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   559
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   560
val iff_true_rule = @{lemma "P ==> P = True" by fast}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   561
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   562
fun iff_true _ [thm] _ = thm RS iff_true_rule
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   563
  | iff_true ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Iff_True thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   564
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   565
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   566
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   567
(* iff-false *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   568
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   569
val iff_false_rule = @{lemma "~P ==> P = False" by fast}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   570
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   571
fun iff_false _ [thm] _ = thm RS iff_false_rule
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   572
  | iff_false ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Iff_False thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   573
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   574
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   575
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   576
(* commutativity *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   577
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   578
fun comm ctxt _ t = match_instantiate ctxt t @{thm eq_commute}
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   579
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   580
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   581
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   582
(* definitional axioms *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   583
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   584
fun def_axiom_disj ctxt t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   585
  (case dest_prop t of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   586
    @{const HOL.disj} $ u1 $ u2 =>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   587
      prove_abstract' ctxt t prop_tac (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   588
        abstract_prop u2 ##>> abstract_prop u1 #>> HOLogic.mk_disj o swap)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   589
  | u => prove_abstract' ctxt t prop_tac (abstract_prop u))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   590
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   591
fun def_axiom ctxt _ = try_provers ctxt Z3_New_Proof.Def_Axiom [
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   592
  ("rules", apply_rule ctxt),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   593
  ("disj", def_axiom_disj ctxt)] []
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   594
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   595
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   596
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   597
(* application of definitions *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   598
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   599
fun apply_def _ [thm] _ = thm (* TODO: cover also the missing cases *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   600
  | apply_def ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Apply_Def thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   601
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   602
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   603
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   604
(* iff-oeq *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   605
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   606
fun iff_oeq _ _ _ = raise Fail "iff_oeq" (* FIXME *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   607
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   608
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   609
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   610
(* negation normal form *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   611
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   612
fun nnf_prop ctxt thms t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   613
  prove_abstract ctxt thms t prop_tac (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   614
    fold_map (abstract_prop o dest_thm) thms ##>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   615
    abstract_prop (dest_prop t))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   616
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   617
fun nnf ctxt rule thms = try_provers ctxt rule [
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   618
  ("prop", nnf_prop ctxt thms),
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   619
  ("quant", quant_intro ctxt [hd thms])] thms
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   620
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   621
fun nnf_pos ctxt = nnf ctxt Z3_New_Proof.Nnf_Pos
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   622
fun nnf_neg ctxt = nnf ctxt Z3_New_Proof.Nnf_Neg
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   623
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   624
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   625
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   626
(* theory lemmas *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   627
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   628
fun arith_th_lemma_tac ctxt prems =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   629
  Method.insert_tac prems
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   630
  THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms z3div_def z3mod_def})
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   631
  THEN' Arith_Data.arith_tac ctxt
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   632
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   633
fun arith_th_lemma ctxt thms t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   634
  prove_abstract ctxt thms t arith_th_lemma_tac (
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   635
    fold_map (abstract_arith ctxt o dest_thm) thms ##>>
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   636
    abstract_arith ctxt (dest_prop t))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   637
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   638
val _ = Theory.setup (Context.theory_map (add_th_lemma_method ("arith", arith_th_lemma)))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   639
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   640
fun th_lemma name ctxt thms =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   641
  (case Symtab.lookup (get_th_lemma_method ctxt) name of
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   642
    SOME method => method ctxt thms
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   643
  | NONE => replay_error ctxt "Bad theory" (Z3_New_Proof.Th_Lemma name) thms)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   644
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   645
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   646
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   647
(* mapping of rules to methods *)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   648
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   649
fun is_assumption Z3_New_Proof.Asserted = true
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   650
  | is_assumption Z3_New_Proof.Goal = true
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   651
  | is_assumption Z3_New_Proof.Hypothesis = true
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   652
  | is_assumption Z3_New_Proof.Intro_Def = true
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   653
  | is_assumption Z3_New_Proof.Skolemize = true
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   654
  | is_assumption _ = false
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   655
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   656
fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   657
fun assumed rule ctxt = replay_error ctxt "Assumed" rule
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   658
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   659
fun choose Z3_New_Proof.True_Axiom = true_axiom
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   660
  | choose (r as Z3_New_Proof.Asserted) = assumed r
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   661
  | choose (r as Z3_New_Proof.Goal) = assumed r
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   662
  | choose Z3_New_Proof.Modus_Ponens = mp
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   663
  | choose Z3_New_Proof.Reflexivity = refl
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   664
  | choose Z3_New_Proof.Symmetry = symm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   665
  | choose Z3_New_Proof.Transitivity = trans
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   666
  | choose (r as Z3_New_Proof.Transitivity_Star) = unsupported r
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   667
  | choose Z3_New_Proof.Monotonicity = cong
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   668
  | choose Z3_New_Proof.Quant_Intro = quant_intro
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   669
  | choose Z3_New_Proof.Distributivity = distrib
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   670
  | choose Z3_New_Proof.And_Elim = and_elim
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   671
  | choose Z3_New_Proof.Not_Or_Elim = not_or_elim
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   672
  | choose Z3_New_Proof.Rewrite = rewrite
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   673
  | choose Z3_New_Proof.Rewrite_Star = rewrite_star
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   674
  | choose Z3_New_Proof.Pull_Quant = pull_quant
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   675
  | choose (r as Z3_New_Proof.Pull_Quant_Star) = unsupported r
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   676
  | choose Z3_New_Proof.Push_Quant = push_quant
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   677
  | choose Z3_New_Proof.Elim_Unused_Vars = elim_unused
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   678
  | choose Z3_New_Proof.Dest_Eq_Res = dest_eq_res
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   679
  | choose Z3_New_Proof.Quant_Inst = quant_inst
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   680
  | choose (r as Z3_New_Proof.Hypothesis) = assumed r
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   681
  | choose Z3_New_Proof.Lemma = lemma
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   682
  | choose Z3_New_Proof.Unit_Resolution = unit_res
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   683
  | choose Z3_New_Proof.Iff_True = iff_true
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   684
  | choose Z3_New_Proof.Iff_False = iff_false
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   685
  | choose Z3_New_Proof.Commutativity = comm
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   686
  | choose Z3_New_Proof.Def_Axiom = def_axiom
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   687
  | choose (r as Z3_New_Proof.Intro_Def) = assumed r
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   688
  | choose Z3_New_Proof.Apply_Def = apply_def
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   689
  | choose Z3_New_Proof.Iff_Oeq = iff_oeq
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   690
  | choose Z3_New_Proof.Nnf_Pos = nnf_pos
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   691
  | choose Z3_New_Proof.Nnf_Neg = nnf_neg
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   692
  | choose (r as Z3_New_Proof.Nnf_Star) = unsupported r
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   693
  | choose (r as Z3_New_Proof.Cnf_Star) = unsupported r
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   694
  | choose (r as Z3_New_Proof.Skolemize) = assumed r
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   695
  | choose Z3_New_Proof.Modus_Ponens_Oeq = mp_oeq
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   696
  | choose (Z3_New_Proof.Th_Lemma name) = th_lemma name
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   697
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   698
fun with_tracing rule method ctxt thms t =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   699
  let val _ = trace_goal ctxt rule thms t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   700
  in method ctxt thms t end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   701
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   702
fun method_for rule = with_tracing rule (choose rule)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   703
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   704
end