src/HOL/Metis_Examples/Clausify.thy
author blanchet
Thu Apr 14 11:24:05 2011 +0200 (2011-04-14)
changeset 42342 6babd86a54a4
parent 42340 4e4f0665e5be
child 42343 118cc349de35
permissions -rw-r--r--
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@42338
     1
(*  Title:      HOL/Metis_Examples/Clausifier.thy
blanchet@42338
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@42338
     3
blanchet@42338
     4
Testing Metis's clausifier.
blanchet@42338
     5
*)
blanchet@42338
     6
blanchet@42338
     7
theory Clausifier
blanchet@42338
     8
imports Complex_Main
blanchet@42338
     9
begin
blanchet@42338
    10
blanchet@42338
    11
text {* Definitional CNF for goal *}
blanchet@42338
    12
blanchet@42338
    13
(* FIXME: shouldn't need this *)
blanchet@42338
    14
declare [[unify_search_bound = 100]]
blanchet@42338
    15
declare [[unify_trace_bound = 100]]
blanchet@42338
    16
blanchet@42338
    17
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42338
    18
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))"
blanchet@42338
    19
blanchet@42338
    20
declare [[metis_new_skolemizer = false]]
blanchet@42338
    21
blanchet@42338
    22
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>
blanchet@42338
    23
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
    24
by (metis pax)
blanchet@42338
    25
blanchet@42338
    26
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>
blanchet@42338
    27
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
    28
by (metisFT pax)
blanchet@42338
    29
blanchet@42338
    30
declare [[metis_new_skolemizer]]
blanchet@42338
    31
blanchet@42338
    32
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>
blanchet@42338
    33
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
    34
by (metis pax)
blanchet@42338
    35
blanchet@42338
    36
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>
blanchet@42338
    37
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
    38
by (metisFT pax)
blanchet@42338
    39
blanchet@42338
    40
text {* New Skolemizer *}
blanchet@42338
    41
blanchet@42338
    42
declare [[metis_new_skolemizer]]
blanchet@42338
    43
blanchet@42338
    44
lemma
blanchet@42338
    45
  fixes x :: real
blanchet@42342
    46
  assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
blanchet@42338
    47
  shows "lim f \<le> x"
blanchet@42338
    48
by (metis 1 LIMSEQ_le_const2 fn_le)
blanchet@42338
    49
blanchet@42338
    50
definition
blanchet@42338
    51
  bounded :: "'a::metric_space set \<Rightarrow> bool" where
blanchet@42338
    52
  "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
blanchet@42338
    53
blanchet@42338
    54
lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
blanchet@42338
    55
by (metis bounded_def subset_eq)
blanchet@42338
    56
blanchet@42338
    57
lemma
blanchet@42338
    58
  assumes a: "Quotient R Abs Rep"
blanchet@42338
    59
  shows "symp R"
blanchet@42338
    60
using a unfolding Quotient_def using sympI
blanchet@42338
    61
by metisFT
blanchet@42338
    62
blanchet@42338
    63
lemma
blanchet@42338
    64
  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
blanchet@42342
    65
   (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
blanchet@42338
    66
by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
blanchet@42338
    67
blanchet@42342
    68
lemma ex_tl: "EX ys. tl ys = xs"
blanchet@42342
    69
using tl.simps(2) by fast
blanchet@42342
    70
blanchet@42342
    71
lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
blanchet@42342
    72
by (metis ex_tl)
blanchet@42342
    73
blanchet@42338
    74
end