src/HOL/Metis_Examples/Clausification.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47308 9caab698dbe4
child 50696 85f944352d55
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42756
diff changeset
     1
(*  Title:      HOL/Metis_Examples/Clausification.thy
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
     3
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42756
diff changeset
     4
Example that exercises Metis's Clausifier.
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
     5
*)
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
     6
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42756
diff changeset
     7
header {* Example that Exercises Metis's Clausifier *}
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42756
diff changeset
     8
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42756
diff changeset
     9
theory Clausification
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    10
imports Complex_Main
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    11
begin
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    12
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    13
(* FIXME: shouldn't need this *)
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    14
declare [[unify_search_bound = 100]]
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    15
declare [[unify_trace_bound = 100]]
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    16
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42350
diff changeset
    17
42345
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    18
text {* Definitional CNF for facts *}
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    19
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    20
declare [[meson_max_clauses = 10]]
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    21
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    22
axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    23
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)"
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    24
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    25
declare [[metis_new_skolemizer = false]]
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    26
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    27
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    28
by (metis qax)
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    29
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    30
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43197
diff changeset
    31
by (metis (full_types) qax)
42345
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    32
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    33
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)"
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    34
by (metis qax)
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    35
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    36
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)"
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43197
diff changeset
    37
by (metis (full_types) qax)
42345
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    38
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    39
declare [[metis_new_skolemizer]]
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    40
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    41
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    42
by (metis qax)
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    43
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    44
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43197
diff changeset
    45
by (metis (full_types) qax)
42345
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    46
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    47
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)"
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    48
by (metis qax)
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    49
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    50
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)"
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43197
diff changeset
    51
by (metis (full_types) qax)
42345
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    52
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    53
declare [[meson_max_clauses = 60]]
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    54
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    55
axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    56
rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    57
      (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    58
      (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    59
      (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    60
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    61
declare [[metis_new_skolemizer = false]]
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    62
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    63
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    64
by (metis rax)
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    65
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    66
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43197
diff changeset
    67
by (metis (full_types) rax)
42345
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    68
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    69
declare [[metis_new_skolemizer]]
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    70
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    71
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    72
by (metis rax)
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    73
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    74
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43197
diff changeset
    75
by (metis (full_types) rax)
42345
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    76
42350
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    77
lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    78
       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    79
       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    80
       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    81
by (metis rax)
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    82
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    83
lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    84
       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    85
       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    86
       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43197
diff changeset
    87
by (metis (full_types) rax)
42350
128dc0fa87fc more clausification tests
blanchet
parents: 42345
diff changeset
    88
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42350
diff changeset
    89
42345
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    90
text {* Definitional CNF for goal *}
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    91
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    92
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
42345
5ecd55993606 added examples of definitional CNF facts
blanchet
parents: 42343
diff changeset
    93
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)"
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    94
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    95
declare [[metis_new_skolemizer = false]]
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    96
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    97
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>
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    98
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
    99
by (metis pax)
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   100
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   101
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>
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   102
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43197
diff changeset
   103
by (metis (full_types) pax)
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   104
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   105
declare [[metis_new_skolemizer]]
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   106
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   107
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>
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   108
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   109
by (metis pax)
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   110
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   111
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>
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   112
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43197
diff changeset
   113
by (metis (full_types) pax)
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   114
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42350
diff changeset
   115
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   116
text {* New Skolemizer *}
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   117
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   118
declare [[metis_new_skolemizer]]
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   119
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   120
lemma
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   121
  fixes x :: real
42342
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42340
diff changeset
   122
  assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   123
  shows "lim f \<le> x"
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   124
by (metis 1 LIMSEQ_le_const2 fn_le)
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   125
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   126
definition
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   127
  bounded :: "'a::metric_space set \<Rightarrow> bool" where
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   128
  "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   129
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   130
lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   131
by (metis bounded_def subset_eq)
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   132
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   133
lemma
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 43228
diff changeset
   134
  assumes a: "Quotient R Abs Rep T"
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   135
  shows "symp R"
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   136
using a unfolding Quotient_def using sympI
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43197
diff changeset
   137
by (metis (full_types))
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   138
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   139
lemma
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   140
  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
42342
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42340
diff changeset
   141
   (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   142
by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   143
42342
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42340
diff changeset
   144
lemma ex_tl: "EX ys. tl ys = xs"
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42340
diff changeset
   145
using tl.simps(2) by fast
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42340
diff changeset
   146
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42340
diff changeset
   147
lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42340
diff changeset
   148
by (metis ex_tl)
6babd86a54a4 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents: 42340
diff changeset
   149
42338
802f2fe7a0c9 started clausifier examples
blanchet
parents:
diff changeset
   150
end