src/HOL/Metis_Examples/Clausify.thy
 changeset 42747 f132d13fcf75 parent 42350 128dc0fa87fc child 42756 6b7ef9b724fd
```     1.1 --- a/src/HOL/Metis_Examples/Clausify.thy	Thu May 12 15:29:19 2011 +0200
1.2 +++ b/src/HOL/Metis_Examples/Clausify.thy	Thu May 12 15:29:19 2011 +0200
1.3 @@ -12,6 +12,37 @@
1.4  declare [[unify_search_bound = 100]]
1.5  declare [[unify_trace_bound = 100]]
1.6
1.7 +sledgehammer_params [prover = e, blocking, timeout = 10]
1.8 +
1.9 +
1.10 +text {* Extensionality *}
1.11 +
1.12 +lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
1.13 +by simp
1.14 +
1.15 +definition inc :: "nat \<Rightarrow> nat" where
1.16 +"inc x = x + 1"
1.17 +
1.18 +lemma "inc \<noteq> (\<lambda>y. 0)"
1.19 +sledgehammer [expect = some] (inc_def plus_1_not_0)
1.20 +by (metis inc_def plus_1_not_0)
1.21 +
1.22 +lemma "inc = (\<lambda>y. y + 1)"
1.23 +sledgehammer [expect = some] (inc_def)
1.24 +by (metis inc_def)
1.25 +
1.26 +lemma "(\<lambda>y. y + 1) = inc"
1.27 +sledgehammer [expect = some] (inc_def)
1.28 +by (metis inc_def)
1.29 +
1.30 +definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
1.31 +"add_swap = (\<lambda>x y. y + x)"
1.32 +
1.33 +lemma "add_swap m n = n + m"
1.34 +sledgehammer [expect = some] (add_swap_def)
1.36 +
1.37 +
1.38  text {* Definitional CNF for facts *}
1.39
1.40  declare [[meson_max_clauses = 10]]
1.41 @@ -83,6 +114,7 @@
1.42         (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
1.43  by (metisFT rax)
1.44
1.45 +
1.46  text {* Definitional CNF for goal *}
1.47
1.48  axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
1.49 @@ -108,6 +140,7 @@
1.50                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
1.51  by (metisFT pax)
1.52
1.53 +
1.54  text {* New Skolemizer *}
1.55
1.56  declare [[metis_new_skolemizer]]
```