# HG changeset patch
# User blanchet
# Date 1411993950 -7200
# Node ID 62bc7c79212bf72737a05afc257a98554667d576
# Parent  9953ab32d9c24ea66729c8c8ce4a820f355c5f06
made 'moura' tactic more powerful

diff -r 9953ab32d9c2 -r 62bc7c79212b src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Mon Sep 29 12:30:12 2014 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Sep 29 14:32:30 2014 +0200
@@ -111,19 +111,6 @@
 qed
 
 
-subsection {* A skolemization tactic and proof method *}
-
-ML {*
-fun moura_tac ctxt =
-  Atomize_Elim.atomize_elim_tac ctxt THEN'
-  SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice bchoice}) THEN ALLGOALS (blast_tac ctxt));
-*}
-
-method_setup moura = {*
- Scan.succeed (SIMPLE_METHOD' o moura_tac)
-*} "solve skolemization goals, especially those arising from Z3 proofs"
-
-
 subsection {*Function Inverse*}
 
 lemma inv_def: "inv f = (%y. SOME x. f x = y)"
diff -r 9953ab32d9c2 -r 62bc7c79212b src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Sep 29 12:30:12 2014 +0200
+++ b/src/HOL/SMT.thy	Mon Sep 29 14:32:30 2014 +0200
@@ -9,6 +9,34 @@
 keywords "smt_status" :: diag
 begin
 
+subsection {* A skolemization tactic and proof method *}
+
+lemma choices:
+  "\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)"
+  "\<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)"
+  "\<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)"
+  by metis+
+
+lemma bchoices:
+  "\<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)"
+  "\<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)"
+  "\<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)"
+  by metis+
+
+ML {*
+fun moura_tac ctxt =
+  Atomize_Elim.atomize_elim_tac ctxt THEN'
+  SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN
+    ALLGOALS (blast_tac ctxt));
+*}
+
+method_setup moura = {*
+ Scan.succeed (SIMPLE_METHOD' o moura_tac)
+*} "solve skolemization goals, especially those arising from Z3 proofs"
+
+hide_fact (open) choices bchoices
+
+
 subsection {* Triggers for quantifier instantiation *}
 
 text {*
diff -r 9953ab32d9c2 -r 62bc7c79212b src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Mon Sep 29 12:30:12 2014 +0200
+++ b/src/HOL/Sledgehammer.thy	Mon Sep 29 14:32:30 2014 +0200
@@ -12,7 +12,7 @@
 begin
 
 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
-by (erule contrapos_nn) (rule arg_cong)
+  by (erule contrapos_nn) (rule arg_cong)
 
 ML_file "Tools/Sledgehammer/async_manager.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_util.ML"