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