src/HOL/SMT.thy
changeset 58481 62bc7c79212b
parent 58441 c1b489999de9
child 58598 d9892c88cb56
     1.1 --- a/src/HOL/SMT.thy	Mon Sep 29 12:30:12 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Mon Sep 29 14:32:30 2014 +0200
     1.3 @@ -9,6 +9,34 @@
     1.4  keywords "smt_status" :: diag
     1.5  begin
     1.6  
     1.7 +subsection {* A skolemization tactic and proof method *}
     1.8 +
     1.9 +lemma choices:
    1.10 +  "\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)"
    1.11 +  "\<And>Q. \<forall>x. \<exists>y ya yb. Q x y ya yb \<Longrightarrow> \<exists>f fa fb. \<forall>x. Q x (f x) (fa x) (fb x)"
    1.12 +  "\<And>Q. \<forall>x. \<exists>y ya yb yc. Q x y ya yb yc \<Longrightarrow> \<exists>f fa fb fc. \<forall>x. Q x (f x) (fa x) (fb x) (fc x)"
    1.13 +  by metis+
    1.14 +
    1.15 +lemma bchoices:
    1.16 +  "\<And>Q. \<forall>x \<in> S. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x \<in> S. Q x (f x) (fa x)"
    1.17 +  "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb. Q x y ya yb \<Longrightarrow> \<exists>f fa fb. \<forall>x \<in> S. Q x (f x) (fa x) (fb x)"
    1.18 +  "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc. Q x y ya yb yc \<Longrightarrow> \<exists>f fa fb fc. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x)"
    1.19 +  by metis+
    1.20 +
    1.21 +ML {*
    1.22 +fun moura_tac ctxt =
    1.23 +  Atomize_Elim.atomize_elim_tac ctxt THEN'
    1.24 +  SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN
    1.25 +    ALLGOALS (blast_tac ctxt));
    1.26 +*}
    1.27 +
    1.28 +method_setup moura = {*
    1.29 + Scan.succeed (SIMPLE_METHOD' o moura_tac)
    1.30 +*} "solve skolemization goals, especially those arising from Z3 proofs"
    1.31 +
    1.32 +hide_fact (open) choices bchoices
    1.33 +
    1.34 +
    1.35  subsection {* Triggers for quantifier instantiation *}
    1.36  
    1.37  text {*