src/HolSmt/Z3_ProofReplay.sml

72       thm_cache = Net.insert (Thm.concl thm, thm) (#thm_cache s)
77       (fn thm => Drule.INST_TY_TERM (Term.match_term (Thm.concl thm) t) thm)
128         val lit = Thm.concl th
145     val clause = Thm.concl (List.hd thms)
225       (dict, Thm.concl th, th)) (Redblackmap.mkDict Term.compare) conj_ths
252     fun disjuncts dict (thmfun, concl) =
254       val (l, r) = boolSyntax.dest_disj concl  (* may fail *)
259     handle Feedback.HOL_ERR _ =>  (* 'concl' is not a disjunction *)
261         (* |- concl ==> disjunction *)
262         val th = Thm.DISCH concl (thmfun (Thm.ASSUME concl))
263         (* ~disjunction |- ~concl *)
265         val th = Thm.MP (Thm.SPEC (boolSyntax.dest_neg concl) NOT_NOT_ELIM) th
267         val t = Thm.concl th
280             val dict = Redblackmap.insert (dict, Thm.concl th1, th1)
288               Redblackmap.insert (dict, Thm.concl th1, th1)
303               Redblackmap.insert (dict, Thm.concl th1, th1)
341         (Thm.concl th1))
349       if boolSyntax.rhs (Thm.concl th2) = boolSyntax.T then
374         (boolSyntax.rhs (Thm.concl th1))
377       val something = boolSyntax.rhs (Thm.concl th2)
380       val rhs = boolSyntax.rhs (Thm.concl th3)
431     val l'_eq_r' = Drule.CONJUNCTS_AC (boolSyntax.rhs (Thm.concl l_eq_l'),
432       boolSyntax.rhs (Thm.concl r_eq_r'))
563         (boolSyntax.rhs (Thm.concl all_distinct_th), r))
597     (state, Thm.MP (Thm.SPEC (Thm.concl thm) VALID_IFF_TRUE) thm)
615           val concl = Thm.concl th
619             if concl = boolSyntax.F then
623               (* [...] |- ~neg_lit \/ concl *)
624               Thm.MP (Drule.SPECL [neg_lit, concl] IMP_DISJ_1) th1
626             if concl = boolSyntax.F then
630               (* [...] |- lit \/ concl *)
631               Thm.MP (Drule.SPECL [lit, concl] IMP_DISJ_2) th1
658       (fn thm => (boolSyntax.dest_eq (Thm.concl thm), thm)) thms
685           val l' = Lib.snd (boolSyntax.dest_eq (Thm.concl th1))
704     val disj = boolSyntax.dest_neg (Thm.concl thm)
724     val (P, _) = boolSyntax.dest_eq (Thm.concl thm)
740     val (_, intermediate_rhs) = boolSyntax.dest_eq (Thm.concl thm)
817     val t' = boolSyntax.list_mk_imp (List.map Thm.concl thms, t)
916   fun check_thm (name, thm, concl) =
917     if Thm.concl thm <> concl then
919         (Thm.concl thm) ^ ", expected: " ^ Hol_pp.term_to_string concl)
928       (concl : Term.term)
932     val (state, thm) = profile name z3_rule_fn (state, concl)
934         raise ERR name (Hol_pp.term_to_string concl)
935     val _ = profile "check_thm" check_thm (name, thm, concl)
943       (pt : proofterm, concl : Term.term)
949           val (state, thm) = profile name z3_rule_fn (state, thm, concl)
952                 Hol_pp.term_to_string concl)
953           val _ = profile "check_thm" check_thm (name, thm, concl)
961       (pt1 : proofterm, pt2 : proofterm, concl : Term.term)
969               (state, thm1, thm2, concl)
973                     Hol_pp.term_to_string concl)
974             val _ = profile "check_thm" check_thm (name, thm, concl)
982       ([] : proofterm list, concl : Term.term)
988       val (state, thm) = profile name z3_rule_fn (state, acc, concl)
991             Hol_pp.thm_to_string acc) ^ "], " ^ Hol_pp.term_to_string concl)
992       val _ = profile "check_thm" check_thm (name, thm, concl)
999       (pt :: pts : proofterm list, concl : Term.term)
1004       list_prems state_proof name z3_rule_fn (pts, concl) continuation
1094     val _ = Thm.concl thm = boolSyntax.F orelse