src/HOL/Metis_Examples/Clausification.thy
changeset 50705 0e943b33d907
parent 50696 85f944352d55
child 55417 01fbfb60c33e
     1.1 --- a/src/HOL/Metis_Examples/Clausification.thy	Thu Jan 03 17:10:12 2013 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Clausification.thy	Thu Jan 03 17:28:55 2013 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     1.5  qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
     1.6  
     1.7 -declare [[metis_new_skolemizer = false]]
     1.8 +declare [[metis_new_skolem = false]]
     1.9  
    1.10  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    1.11  by (metis qax)
    1.12 @@ -32,7 +32,7 @@
    1.13  lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    1.14  by (metis (full_types) qax)
    1.15  
    1.16 -declare [[metis_new_skolemizer]]
    1.17 +declare [[metis_new_skolem]]
    1.18  
    1.19  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    1.20  by (metis qax)
    1.21 @@ -54,7 +54,7 @@
    1.22        (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
    1.23        (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
    1.24  
    1.25 -declare [[metis_new_skolemizer = false]]
    1.26 +declare [[metis_new_skolem = false]]
    1.27  
    1.28  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    1.29  by (metis rax)
    1.30 @@ -62,7 +62,7 @@
    1.31  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    1.32  by (metis (full_types) rax)
    1.33  
    1.34 -declare [[metis_new_skolemizer]]
    1.35 +declare [[metis_new_skolem]]
    1.36  
    1.37  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    1.38  by (metis rax)
    1.39 @@ -88,7 +88,7 @@
    1.40  axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    1.41  pax: "\<exists>b. \<forall>a. (p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b)"
    1.42  
    1.43 -declare [[metis_new_skolemizer = false]]
    1.44 +declare [[metis_new_skolem = false]]
    1.45  
    1.46  lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
    1.47                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    1.48 @@ -98,7 +98,7 @@
    1.49                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    1.50  by (metis (full_types) pax)
    1.51  
    1.52 -declare [[metis_new_skolemizer]]
    1.53 +declare [[metis_new_skolem]]
    1.54  
    1.55  lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
    1.56                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    1.57 @@ -111,7 +111,7 @@
    1.58  
    1.59  text {* New Skolemizer *}
    1.60  
    1.61 -declare [[metis_new_skolemizer]]
    1.62 +declare [[metis_new_skolem]]
    1.63  
    1.64  lemma
    1.65    fixes x :: real