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.35 +by (metis 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]]