10 keywords "smt_status" :: diag |
10 keywords "smt_status" :: diag |
11 begin |
11 begin |
12 |
12 |
13 subsection \<open>A skolemization tactic and proof method\<close> |
13 subsection \<open>A skolemization tactic and proof method\<close> |
14 |
14 |
15 lemma choices: |
15 lemma ex_iff_push: "(\<exists>y. P \<longleftrightarrow> Q y) \<longleftrightarrow> (P \<longrightarrow> (\<exists>y. Q y)) \<and> ((\<forall>y. Q y) \<longrightarrow> P)" |
16 "\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)" |
16 by metis |
17 "\<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)" |
|
18 "\<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)" |
|
19 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow> |
|
20 \<exists>f fa fb fc fd. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x)" |
|
21 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow> |
|
22 \<exists>f fa fb fc fd fe. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" |
|
23 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow> |
|
24 \<exists>f fa fb fc fd fe ff. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" |
|
25 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow> |
|
26 \<exists>f fa fb fc fd fe ff fg. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" |
|
27 by metis+ |
|
28 |
|
29 lemma bchoices: |
|
30 "\<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)" |
|
31 "\<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)" |
|
32 "\<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)" |
|
33 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow> |
|
34 \<exists>f fa fb fc fd. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x)" |
|
35 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow> |
|
36 \<exists>f fa fb fc fd fe. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" |
|
37 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow> |
|
38 \<exists>f fa fb fc fd fe ff. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" |
|
39 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow> |
|
40 \<exists>f fa fb fc fd fe ff fg. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" |
|
41 by metis+ |
|
42 |
17 |
43 ML \<open> |
18 ML \<open> |
44 fun moura_tac ctxt = |
19 fun moura_tac ctxt = |
45 Atomize_Elim.atomize_elim_tac ctxt THEN' |
20 TRY o Atomize_Elim.atomize_elim_tac ctxt THEN' |
46 SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN |
21 REPEAT o EqSubst.eqsubst_tac ctxt [0] |
47 ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs) |
22 @{thms choice_iff[symmetric] bchoice_iff[symmetric]} THEN' |
48 ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE' |
23 TRY o Simplifier.asm_full_simp_tac |
49 blast_tac ctxt)) |
24 (clear_simpset ctxt addsimps @{thms all_simps ex_simps ex_iff_push}) THEN_ALL_NEW |
|
25 Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs) |
|
26 ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] |
50 \<close> |
27 \<close> |
51 |
28 |
52 method_setup moura = \<open> |
29 method_setup moura = \<open> |
53 Scan.succeed (SIMPLE_METHOD' o moura_tac) |
30 Scan.succeed (SIMPLE_METHOD' o moura_tac) |
54 \<close> "solve skolemization goals, especially those arising from Z3 proofs" |
31 \<close> "solve skolemization goals, especially those arising from Z3 proofs" |
55 |
32 |
56 hide_fact (open) choices bchoices |
33 hide_fact (open) ex_iff_push |
57 |
34 |
58 |
35 |
59 subsection \<open>Triggers for quantifier instantiation\<close> |
36 subsection \<open>Triggers for quantifier instantiation\<close> |
60 |
37 |
61 text \<open> |
38 text \<open> |