src/HOL/Metis_Examples/Clausification.thy
changeset 43228 2ed2f092e990
parent 43197 c71657bbdbc0
child 47308 9caab698dbe4
     1.1 --- a/src/HOL/Metis_Examples/Clausification.thy	Tue Jun 07 07:57:24 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Clausification.thy	Tue Jun 07 08:52:35 2011 +0200
     1.3 @@ -28,13 +28,13 @@
     1.4  by (metis qax)
     1.5  
     1.6  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
     1.7 -by (metisFT qax)
     1.8 +by (metis (full_types) qax)
     1.9  
    1.10  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.11  by (metis qax)
    1.12  
    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 (metisFT qax)
    1.15 +by (metis (full_types) qax)
    1.16  
    1.17  declare [[metis_new_skolemizer]]
    1.18  
    1.19 @@ -42,13 +42,13 @@
    1.20  by (metis qax)
    1.21  
    1.22  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    1.23 -by (metisFT qax)
    1.24 +by (metis (full_types) qax)
    1.25  
    1.26  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.27  by (metis qax)
    1.28  
    1.29  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.30 -by (metisFT qax)
    1.31 +by (metis (full_types) qax)
    1.32  
    1.33  declare [[meson_max_clauses = 60]]
    1.34  
    1.35 @@ -64,7 +64,7 @@
    1.36  by (metis rax)
    1.37  
    1.38  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    1.39 -by (metisFT rax)
    1.40 +by (metis (full_types) rax)
    1.41  
    1.42  declare [[metis_new_skolemizer]]
    1.43  
    1.44 @@ -72,7 +72,7 @@
    1.45  by (metis rax)
    1.46  
    1.47  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    1.48 -by (metisFT rax)
    1.49 +by (metis (full_types) rax)
    1.50  
    1.51  lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
    1.52         (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
    1.53 @@ -84,7 +84,7 @@
    1.54         (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
    1.55         (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
    1.56         (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
    1.57 -by (metisFT rax)
    1.58 +by (metis (full_types) rax)
    1.59  
    1.60  
    1.61  text {* Definitional CNF for goal *}
    1.62 @@ -100,7 +100,7 @@
    1.63  
    1.64  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.65                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    1.66 -by (metisFT pax)
    1.67 +by (metis (full_types) pax)
    1.68  
    1.69  declare [[metis_new_skolemizer]]
    1.70  
    1.71 @@ -110,7 +110,7 @@
    1.72  
    1.73  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.74                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    1.75 -by (metisFT pax)
    1.76 +by (metis (full_types) pax)
    1.77  
    1.78  
    1.79  text {* New Skolemizer *}
    1.80 @@ -134,7 +134,7 @@
    1.81    assumes a: "Quotient R Abs Rep"
    1.82    shows "symp R"
    1.83  using a unfolding Quotient_def using sympI
    1.84 -by metisFT
    1.85 +by (metis (full_types))
    1.86  
    1.87  lemma
    1.88    "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>