# HG changeset patch # User boehmes # Date 1292404368 -3600 # Node ID bb2fa5c13d1a5774bf9fcbe79376e100f8ccccb4 # Parent 2ea84c8535c6c3ba48f202fe8096e28765f64d14 always add pair rules and function update rules automatically (Boogie provides pairs and function update as built-in concepts and does not generate background axioms for them) diff -r 2ea84c8535c6 -r bb2fa5c13d1a src/HOL/Boogie/Tools/boogie_tactics.ML --- a/src/HOL/Boogie/Tools/boogie_tactics.ML Wed Dec 15 10:12:44 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Wed Dec 15 10:12:48 2010 +0100 @@ -28,9 +28,13 @@ let val unfold = Conv.rewrs_conv label_eqs in CONVERSION (Conv.top_sweep_conv (K unfold) ctxt) end +val boogie_rules = + [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] @ + [@{thm fun_upd_same}, @{thm fun_upd_apply}] + fun boogie_tac ctxt rules = unfold_labels_tac ctxt - THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ rules) + THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ boogie_rules @ rules) fun boogie_all_tac ctxt rules = PARALLEL_GOALS (HEADGOAL (boogie_tac ctxt rules))