src/HolSmt/Z3_ProofReplay.sml

10   fun profile name f x =
754       (state, profile "rewrite(01)(proforma)"
759     (state, profile "rewrite(02)(cache)" (state_inst_cached_thm state) t)
763     profile "rewrite(04)(conj/disj)" (fn () =>
765         (state, profile "rewrite(04.1)(conj)" rewrite_conj (l, r))
767         (state, profile "rewrite(04.2)(disj)" rewrite_disj (l, r))
773     (state, profile "rewrite(05)(nnf)" rewrite_nnf (l, r))
780     (state, profile "rewrite(06)(all_distinct)" rewrite_all_distinct (l, r))
784       val thm = profile "rewrite(07)(SIMP_PROVE_UPDATE)" SIMP_PROVE_UPDATE t
787         profile "rewrite(08)(WORD_DP)" (wordsLib.WORD_DP
793         profile "rewrite(09)(WORD_ARITH_CONV)" (fn () =>
798         profile "rewrite(10)(BBLAST)" blastLib.BBLAST_PROVE t
802           profile "rewrite(11.1)(REAL_ARITH)" realLib.REAL_ARITH t
804           profile "rewrite(11.2)(ARITH_PROVE)" intLib.ARITH_PROVE t
820       profile ("th_lemma[" ^ name ^ "](1)(proforma)")
824         profile ("th_lemma[" ^ name ^ "](2)(cache)")
840           profile "th_lemma[arith](3.1)(real)" realLib.REAL_ARITH t'
842           profile "th_lemma[arith](3.2)(int)" intLib.ARITH_PROVE t'
852       val thm = profile "th_lemma[array](3)(SIMP_PROVE_UPDATE)"
875         val thm = profile "th_lemma[bv](3)(WORD_BIT_EQ)" (fn () =>
881           profile "th_lemma[bv](4)(COND_BBLAST)" Tactical.prove (t,
882             Tactical.THEN (profile "th_lemma[bv](4.1)(COND_REWRITE_TAC)"
883               COND_REWRITE_TAC, profile "th_lemma[bv](4.2)(BBLAST_TAC)"
932     val (state, thm) = profile name z3_rule_fn (state, concl)
935     val _ = profile "check_thm" check_thm (name, thm, concl)
949           val (state, thm) = profile name z3_rule_fn (state, thm, concl)
953           val _ = profile "check_thm" check_thm (name, thm, concl)
968             val (state, thm) = profile name z3_rule_fn
974             val _ = profile "check_thm" check_thm (name, thm, concl)
988       val (state, thm) = profile name z3_rule_fn (state, acc, concl)
992       val _ = profile "check_thm" check_thm (name, thm, concl)
1099     val _ = profile "check_proof(hypcheck)" HOLset.isSubset (Thm.hypset thm,