made 'moura' tactic more powerful
authorblanchet
Mon Sep 29 14:32:30 2014 +0200 (2014-09-29)
changeset 5848162bc7c79212b
parent 58480 9953ab32d9c2
child 58482 7836013951e6
made 'moura' tactic more powerful
src/HOL/Hilbert_Choice.thy
src/HOL/SMT.thy
src/HOL/Sledgehammer.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Sep 29 12:30:12 2014 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Sep 29 14:32:30 2014 +0200
     1.3 @@ -111,19 +111,6 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -subsection {* A skolemization tactic and proof method *}
     1.8 -
     1.9 -ML {*
    1.10 -fun moura_tac ctxt =
    1.11 -  Atomize_Elim.atomize_elim_tac ctxt THEN'
    1.12 -  SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice bchoice}) THEN ALLGOALS (blast_tac ctxt));
    1.13 -*}
    1.14 -
    1.15 -method_setup moura = {*
    1.16 - Scan.succeed (SIMPLE_METHOD' o moura_tac)
    1.17 -*} "solve skolemization goals, especially those arising from Z3 proofs"
    1.18 -
    1.19 -
    1.20  subsection {*Function Inverse*}
    1.21  
    1.22  lemma inv_def: "inv f = (%y. SOME x. f x = y)"
     2.1 --- a/src/HOL/SMT.thy	Mon Sep 29 12:30:12 2014 +0200
     2.2 +++ b/src/HOL/SMT.thy	Mon Sep 29 14:32:30 2014 +0200
     2.3 @@ -9,6 +9,34 @@
     2.4  keywords "smt_status" :: diag
     2.5  begin
     2.6  
     2.7 +subsection {* A skolemization tactic and proof method *}
     2.8 +
     2.9 +lemma choices:
    2.10 +  "\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)"
    2.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)"
    2.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)"
    2.13 +  by metis+
    2.14 +
    2.15 +lemma bchoices:
    2.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)"
    2.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)"
    2.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)"
    2.19 +  by metis+
    2.20 +
    2.21 +ML {*
    2.22 +fun moura_tac ctxt =
    2.23 +  Atomize_Elim.atomize_elim_tac ctxt THEN'
    2.24 +  SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN
    2.25 +    ALLGOALS (blast_tac ctxt));
    2.26 +*}
    2.27 +
    2.28 +method_setup moura = {*
    2.29 + Scan.succeed (SIMPLE_METHOD' o moura_tac)
    2.30 +*} "solve skolemization goals, especially those arising from Z3 proofs"
    2.31 +
    2.32 +hide_fact (open) choices bchoices
    2.33 +
    2.34 +
    2.35  subsection {* Triggers for quantifier instantiation *}
    2.36  
    2.37  text {*
     3.1 --- a/src/HOL/Sledgehammer.thy	Mon Sep 29 12:30:12 2014 +0200
     3.2 +++ b/src/HOL/Sledgehammer.thy	Mon Sep 29 14:32:30 2014 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4  begin
     3.5  
     3.6  lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
     3.7 -by (erule contrapos_nn) (rule arg_cong)
     3.8 +  by (erule contrapos_nn) (rule arg_cong)
     3.9  
    3.10  ML_file "Tools/Sledgehammer/async_manager.ML"
    3.11  ML_file "Tools/Sledgehammer/sledgehammer_util.ML"