src/HOL/Metis_Examples/Tarski.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47040 78e88d26f19d
child 50705 0e943b33d907
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:
41141
ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents: 38991
diff changeset
     1
(*  Title:      HOL/Metis_Examples/Tarski.thy
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
     2
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
41144
509e51b7509a example tuning
blanchet
parents: 41141
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     4
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
     5
Metis example featuring the full theorem of Tarski.
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     6
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     7
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
     8
header {* Metis Example Featuring the Full Theorem of Tarski *}
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     9
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 26806
diff changeset
    10
theory Tarski
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 41144
diff changeset
    11
imports Main "~~/src/HOL/Library/FuncSet"
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 26806
diff changeset
    12
begin
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    13
42103
6066a35f6678 Metis examples use the new Skolemizer to test it
blanchet
parents: 41413
diff changeset
    14
declare [[metis_new_skolemizer]]
6066a35f6678 Metis examples use the new Skolemizer to test it
blanchet
parents: 41413
diff changeset
    15
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    16
(*Many of these higher-order problems appear to be impossible using the
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    17
current linkup. They often seem to need either higher-order unification
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    18
or explicit reasoning about connectives such as conjunction. The numerous
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    19
set comprehensions are to blame.*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    20
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    21
record 'a potype =
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    22
  pset  :: "'a set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    23
  order :: "('a * 'a) set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    24
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    25
definition monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    26
  "monotone f A r == \<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    27
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    28
definition least :: "['a => bool, 'a potype] => 'a" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    29
  "least P po == @ x. x: pset po & P x &
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    30
                       (\<forall>y \<in> pset po. P y --> (x,y): order po)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    31
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    32
definition greatest :: "['a => bool, 'a potype] => 'a" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    33
  "greatest P po == @ x. x: pset po & P x &
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    34
                          (\<forall>y \<in> pset po. P y --> (y,x): order po)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    35
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    36
definition lub  :: "['a set, 'a potype] => 'a" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    37
  "lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    38
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    39
definition glb  :: "['a set, 'a potype] => 'a" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    40
  "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    41
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    42
definition isLub :: "['a set, 'a potype, 'a] => bool" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    43
  "isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    44
                   (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    45
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    46
definition isGlb :: "['a set, 'a potype, 'a] => bool" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    47
  "isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    48
                 (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    49
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    50
definition "fix"    :: "[('a => 'a), 'a set] => 'a set" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    51
  "fix f A  == {x. x: A & f x = x}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    52
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    53
definition interval :: "[('a*'a) set,'a, 'a ] => 'a set" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    54
  "interval r a b == {x. (a,x): r & (x,b): r}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    55
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    56
definition Bot :: "'a potype => 'a" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    57
  "Bot po == least (%x. True) po"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    58
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    59
definition Top :: "'a potype => 'a" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    60
  "Top po == greatest (%x. True) po"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    61
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    62
definition PartialOrder :: "('a potype) set" where
30198
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
    63
  "PartialOrder == {P. refl_on (pset P) (order P) & antisym (order P) &
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    64
                       trans (order P)}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    65
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    66
definition CompleteLattice :: "('a potype) set" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    67
  "CompleteLattice == {cl. cl: PartialOrder &
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    68
                        (\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) &
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    69
                        (\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    70
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    71
definition induced :: "['a set, ('a * 'a) set] => ('a *'a)set" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    72
  "induced A r == {(a,b). a : A & b: A & (a,b): r}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    73
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    74
definition sublattice :: "('a potype * 'a set)set" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    75
  "sublattice ==
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    76
      SIGMA cl: CompleteLattice.
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    77
          {S. S \<subseteq> pset cl &
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    78
           (| pset = S, order = induced S (order cl) |): CompleteLattice }"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    79
35054
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 33027
diff changeset
    80
abbreviation
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 33027
diff changeset
    81
  sublattice_syntax :: "['a set, 'a potype] => bool" ("_ <<= _" [51, 50] 50)
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 33027
diff changeset
    82
  where "S <<= cl \<equiv> S : sublattice `` {cl}"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    83
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35054
diff changeset
    84
definition dual :: "'a potype => 'a potype" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    85
  "dual po == (| pset = pset po, order = converse (order po) |)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    86
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
    87
locale PO =
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    88
  fixes cl :: "'a potype"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    89
    and A  :: "'a set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    90
    and r  :: "('a * 'a) set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    91
  assumes cl_po:  "cl : PartialOrder"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    92
  defines A_def: "A == pset cl"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    93
     and  r_def: "r == order cl"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    94
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
    95
locale CL = PO +
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    96
  assumes cl_co:  "cl : CompleteLattice"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    97
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
    98
definition CLF_set :: "('a potype * ('a => 'a)) set" where
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
    99
  "CLF_set = (SIGMA cl: CompleteLattice.
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   100
            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   101
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   102
locale CLF = CL +
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   103
  fixes f :: "'a => 'a"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   104
    and P :: "'a set"
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   105
  assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF``{cl}"*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   106
  defines P_def: "P == fix f A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   107
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   108
locale Tarski = CLF +
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   109
  fixes Y     :: "'a set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   110
    and intY1 :: "'a set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   111
    and v     :: "'a"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   112
  assumes
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   113
    Y_ss: "Y \<subseteq> P"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   114
  defines
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   115
    intY1_def: "intY1 == interval r (lub Y cl) (Top cl)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   116
    and v_def: "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r &
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   117
                             x: intY1}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   118
                      (| pset=intY1, order=induced intY1 r|)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   119
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   120
subsection {* Partial Order *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   121
30198
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
   122
lemma (in PO) PO_imp_refl_on: "refl_on A r"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   123
apply (insert cl_po)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   124
apply (simp add: PartialOrder_def A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   125
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   126
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   127
lemma (in PO) PO_imp_sym: "antisym r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   128
apply (insert cl_po)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   129
apply (simp add: PartialOrder_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   130
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   131
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   132
lemma (in PO) PO_imp_trans: "trans r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   133
apply (insert cl_po)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   134
apply (simp add: PartialOrder_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   135
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   136
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   137
lemma (in PO) reflE: "x \<in> A ==> (x, x) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   138
apply (insert cl_po)
30198
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
   139
apply (simp add: PartialOrder_def refl_on_def A_def r_def)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   140
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   141
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   142
lemma (in PO) antisymE: "[| (a, b) \<in> r; (b, a) \<in> r |] ==> a = b"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   143
apply (insert cl_po)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   144
apply (simp add: PartialOrder_def antisym_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   145
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   146
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   147
lemma (in PO) transE: "[| (a, b) \<in> r; (b, c) \<in> r|] ==> (a,c) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   148
apply (insert cl_po)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   149
apply (simp add: PartialOrder_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   150
apply (unfold trans_def, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   151
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   152
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   153
lemma (in PO) monotoneE:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   154
     "[| monotone f A r;  x \<in> A; y \<in> A; (x, y) \<in> r |] ==> (f x, f y) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   155
by (simp add: monotone_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   156
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   157
lemma (in PO) po_subset_po:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   158
     "S \<subseteq> A ==> (| pset = S, order = induced S r |) \<in> PartialOrder"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   159
apply (simp (no_asm) add: PartialOrder_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   160
apply auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   161
-- {* refl *}
30198
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
   162
apply (simp add: refl_on_def induced_def)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   163
apply (blast intro: reflE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   164
-- {* antisym *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   165
apply (simp add: antisym_def induced_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   166
apply (blast intro: antisymE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   167
-- {* trans *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   168
apply (simp add: trans_def induced_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   169
apply (blast intro: transE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   170
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   171
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   172
lemma (in PO) indE: "[| (x, y) \<in> induced S r; S \<subseteq> A |] ==> (x, y) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   173
by (simp add: add: induced_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   174
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   175
lemma (in PO) indI: "[| (x, y) \<in> r; x \<in> S; y \<in> S |] ==> (x, y) \<in> induced S r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   176
by (simp add: add: induced_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   177
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   178
lemma (in CL) CL_imp_ex_isLub: "S \<subseteq> A ==> \<exists>L. isLub S cl L"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   179
apply (insert cl_co)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   180
apply (simp add: CompleteLattice_def A_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   181
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   182
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   183
declare (in CL) cl_co [simp]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   184
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   185
lemma isLub_lub: "(\<exists>L. isLub S cl L) = isLub S cl (lub S cl)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   186
by (simp add: lub_def least_def isLub_def some_eq_ex [symmetric])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   187
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   188
lemma isGlb_glb: "(\<exists>G. isGlb S cl G) = isGlb S cl (glb S cl)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   189
by (simp add: glb_def greatest_def isGlb_def some_eq_ex [symmetric])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   190
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   191
lemma isGlb_dual_isLub: "isGlb S cl = isLub S (dual cl)"
46752
e9e7209eb375 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents: 45970
diff changeset
   192
by (simp add: isLub_def isGlb_def dual_def converse_unfold)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   193
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   194
lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)"
46752
e9e7209eb375 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents: 45970
diff changeset
   195
by (simp add: isLub_def isGlb_def dual_def converse_unfold)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   196
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   197
lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   198
apply (insert cl_po)
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45705
diff changeset
   199
apply (simp add: PartialOrder_def dual_def)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   200
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   201
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   202
lemma Rdual:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   203
     "\<forall>S. (S \<subseteq> A -->( \<exists>L. isLub S (| pset = A, order = r|) L))
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   204
      ==> \<forall>S. (S \<subseteq> A --> (\<exists>G. isGlb S (| pset = A, order = r|) G))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   205
apply safe
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   206
apply (rule_tac x = "lub {y. y \<in> A & (\<forall>k \<in> S. (y, k) \<in> r)}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   207
                      (|pset = A, order = r|) " in exI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   208
apply (drule_tac x = "{y. y \<in> A & (\<forall>k \<in> S. (y,k) \<in> r) }" in spec)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   209
apply (drule mp, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   210
apply (simp add: isLub_lub isGlb_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   211
apply (simp add: isLub_def, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   212
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   213
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   214
lemma lub_dual_glb: "lub S cl = glb S (dual cl)"
46752
e9e7209eb375 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents: 45970
diff changeset
   215
by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   216
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   217
lemma glb_dual_lub: "glb S cl = lub S (dual cl)"
46752
e9e7209eb375 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents: 45970
diff changeset
   218
by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   219
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   220
lemma CL_subset_PO: "CompleteLattice \<subseteq> PartialOrder"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   221
by (simp add: PartialOrder_def CompleteLattice_def, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   222
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   223
lemmas CL_imp_PO = CL_subset_PO [THEN subsetD]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   224
30198
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
   225
declare PO.PO_imp_refl_on  [OF PO.intro [OF CL_imp_PO], simp]
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   226
declare PO.PO_imp_sym   [OF PO.intro [OF CL_imp_PO], simp]
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   227
declare PO.PO_imp_trans [OF PO.intro [OF CL_imp_PO], simp]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   228
30198
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
   229
lemma (in CL) CO_refl_on: "refl_on A r"
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
   230
by (rule PO_imp_refl_on)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   231
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   232
lemma (in CL) CO_antisym: "antisym r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   233
by (rule PO_imp_sym)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   234
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   235
lemma (in CL) CO_trans: "trans r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   236
by (rule PO_imp_trans)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   237
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   238
lemma CompleteLatticeI:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   239
     "[| po \<in> PartialOrder; (\<forall>S. S \<subseteq> pset po --> (\<exists>L. isLub S po L));
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   240
         (\<forall>S. S \<subseteq> pset po --> (\<exists>G. isGlb S po G))|]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   241
      ==> po \<in> CompleteLattice"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   242
apply (unfold CompleteLattice_def, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   243
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   244
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   245
lemma (in CL) CL_dualCL: "dual cl \<in> CompleteLattice"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   246
apply (insert cl_co)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   247
apply (simp add: CompleteLattice_def dual_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   248
apply (fold dual_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   249
apply (simp add: isLub_dual_isGlb [symmetric] isGlb_dual_isLub [symmetric]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   250
                 dualPO)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   251
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   252
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   253
lemma (in PO) dualA_iff: "pset (dual cl) = pset cl"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   254
by (simp add: dual_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   255
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   256
lemma (in PO) dualr_iff: "((x, y) \<in> (order(dual cl))) = ((y, x) \<in> order cl)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   257
by (simp add: dual_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   258
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   259
lemma (in PO) monotone_dual:
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   260
     "monotone f (pset cl) (order cl)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   261
     ==> monotone f (pset (dual cl)) (order(dual cl))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   262
by (simp add: monotone_def dualA_iff dualr_iff)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   263
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   264
lemma (in PO) interval_dual:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   265
     "[| x \<in> A; y \<in> A|] ==> interval r x y = interval (order(dual cl)) y x"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   266
apply (simp add: interval_def dualr_iff)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   267
apply (fold r_def, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   268
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   269
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   270
lemma (in PO) interval_not_empty:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   271
     "[| trans r; interval r a b \<noteq> {} |] ==> (a, b) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   272
apply (simp add: interval_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   273
apply (unfold trans_def, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   274
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   275
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   276
lemma (in PO) interval_imp_mem: "x \<in> interval r a b ==> (a, x) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   277
by (simp add: interval_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   278
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   279
lemma (in PO) left_in_interval:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   280
     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] ==> a \<in> interval r a b"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   281
apply (simp (no_asm_simp) add: interval_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   282
apply (simp add: PO_imp_trans interval_not_empty)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   283
apply (simp add: reflE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   284
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   285
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   286
lemma (in PO) right_in_interval:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   287
     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] ==> b \<in> interval r a b"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   288
apply (simp (no_asm_simp) add: interval_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   289
apply (simp add: PO_imp_trans interval_not_empty)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   290
apply (simp add: reflE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   291
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   292
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   293
subsection {* sublattice *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   294
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   295
lemma (in PO) sublattice_imp_CL:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   296
     "S <<= cl  ==> (| pset = S, order = induced S r |) \<in> CompleteLattice"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   297
by (simp add: sublattice_def CompleteLattice_def A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   298
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   299
lemma (in CL) sublatticeI:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   300
     "[| S \<subseteq> A; (| pset = S, order = induced S r |) \<in> CompleteLattice |]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   301
      ==> S <<= cl"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   302
by (simp add: sublattice_def A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   303
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   304
subsection {* lub *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   305
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   306
lemma (in CL) lub_unique: "[| S \<subseteq> A; isLub S cl x; isLub S cl L|] ==> x = L"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   307
apply (rule antisymE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   308
apply (auto simp add: isLub_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   309
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   310
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   311
lemma (in CL) lub_upper: "[|S \<subseteq> A; x \<in> S|] ==> (x, lub S cl) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   312
apply (rule CL_imp_ex_isLub [THEN exE], assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   313
apply (unfold lub_def least_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   314
apply (rule some_equality [THEN ssubst])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   315
  apply (simp add: isLub_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   316
 apply (simp add: lub_unique A_def isLub_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   317
apply (simp add: isLub_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   318
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   319
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   320
lemma (in CL) lub_least:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   321
     "[| S \<subseteq> A; L \<in> A; \<forall>x \<in> S. (x,L) \<in> r |] ==> (lub S cl, L) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   322
apply (rule CL_imp_ex_isLub [THEN exE], assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   323
apply (unfold lub_def least_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   324
apply (rule_tac s=x in some_equality [THEN ssubst])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   325
  apply (simp add: isLub_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   326
 apply (simp add: lub_unique A_def isLub_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   327
apply (simp add: isLub_def r_def A_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   328
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   329
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   330
lemma (in CL) lub_in_lattice: "S \<subseteq> A ==> lub S cl \<in> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   331
apply (rule CL_imp_ex_isLub [THEN exE], assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   332
apply (unfold lub_def least_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   333
apply (subst some_equality)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   334
apply (simp add: isLub_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   335
prefer 2 apply (simp add: isLub_def A_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   336
apply (simp add: lub_unique A_def isLub_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   337
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   338
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   339
lemma (in CL) lubI:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   340
     "[| S \<subseteq> A; L \<in> A; \<forall>x \<in> S. (x,L) \<in> r;
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   341
         \<forall>z \<in> A. (\<forall>y \<in> S. (y,z) \<in> r) --> (L,z) \<in> r |] ==> L = lub S cl"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   342
apply (rule lub_unique, assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   343
apply (simp add: isLub_def A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   344
apply (unfold isLub_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   345
apply (rule conjI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   346
apply (fold A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   347
apply (rule lub_in_lattice, assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   348
apply (simp add: lub_upper lub_least)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   349
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   350
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   351
lemma (in CL) lubIa: "[| S \<subseteq> A; isLub S cl L |] ==> L = lub S cl"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   352
by (simp add: lubI isLub_def A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   353
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   354
lemma (in CL) isLub_in_lattice: "isLub S cl L ==> L \<in> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   355
by (simp add: isLub_def  A_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   356
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   357
lemma (in CL) isLub_upper: "[|isLub S cl L; y \<in> S|] ==> (y, L) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   358
by (simp add: isLub_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   359
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   360
lemma (in CL) isLub_least:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   361
     "[| isLub S cl L; z \<in> A; \<forall>y \<in> S. (y, z) \<in> r|] ==> (L, z) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   362
by (simp add: isLub_def A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   363
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   364
lemma (in CL) isLubI:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   365
     "[| L \<in> A; \<forall>y \<in> S. (y, L) \<in> r;
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   366
         (\<forall>z \<in> A. (\<forall>y \<in> S. (y, z):r) --> (L, z) \<in> r)|] ==> isLub S cl L"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   367
by (simp add: isLub_def A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   368
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   369
subsection {* glb *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   370
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   371
lemma (in CL) glb_in_lattice: "S \<subseteq> A ==> glb S cl \<in> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   372
apply (subst glb_dual_lub)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   373
apply (simp add: A_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   374
apply (rule dualA_iff [THEN subst])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   375
apply (rule CL.lub_in_lattice)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   376
apply (rule CL.intro)
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   377
apply (rule PO.intro)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   378
apply (rule dualPO)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   379
apply (rule CL_axioms.intro)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   380
apply (rule CL_dualCL)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   381
apply (simp add: dualA_iff)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   382
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   383
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   384
lemma (in CL) glb_lower: "[|S \<subseteq> A; x \<in> S|] ==> (glb S cl, x) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   385
apply (subst glb_dual_lub)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   386
apply (simp add: r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   387
apply (rule dualr_iff [THEN subst])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   388
apply (rule CL.lub_upper)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   389
apply (rule CL.intro)
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   390
apply (rule PO.intro)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   391
apply (rule dualPO)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   392
apply (rule CL_axioms.intro)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   393
apply (rule CL_dualCL)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   394
apply (simp add: dualA_iff A_def, assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   395
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   396
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   397
text {*
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   398
  Reduce the sublattice property by using substructural properties;
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   399
  abandoned see @{text "Tarski_4.ML"}.
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   400
*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   401
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   402
declare (in CLF) f_cl [simp]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   403
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   404
lemma (in CLF) [simp]:
42762
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   405
    "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   406
proof -
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   407
  have "\<forall>u v. (v, u) \<in> CLF_set \<longrightarrow> u \<in> {R \<in> pset v \<rightarrow> pset v. monotone R (pset v) (order v)}"
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   408
    unfolding CLF_set_def using SigmaE2 by blast
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   409
  hence F1: "\<forall>u v. (v, u) \<in> CLF_set \<longrightarrow> u \<in> pset v \<rightarrow> pset v \<and> monotone u (pset v) (order v)"
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   410
    using CollectE by blast
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   411
  hence "Tarski.monotone f (pset cl) (order cl)" by (metis f_cl)
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   412
  hence "(cl, f) \<in> CLF_set \<and> Tarski.monotone f (pset cl) (order cl)"
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   413
    by (metis f_cl)
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   414
  thus "f \<in> pset cl \<rightarrow> pset cl \<and> Tarski.monotone f (pset cl) (order cl)"
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   415
    using F1 by metis
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   416
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   417
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   418
lemma (in CLF) f_in_funcset: "f \<in> A -> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   419
by (simp add: A_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   420
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   421
lemma (in CLF) monotone_f: "monotone f A r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   422
by (simp add: A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   423
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   424
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   425
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   426
declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp]
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   427
42762
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   428
lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   429
apply (simp del: dualA_iff)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   430
apply (simp)
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   431
done
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   432
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   433
declare (in CLF) CLF_set_def[simp del] CL_dualCL[simp del] monotone_dual[simp del]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   434
          dualA_iff[simp del]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   435
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   436
subsection {* fixed points *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   437
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   438
lemma fix_subset: "fix f A \<subseteq> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   439
by (simp add: fix_def, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   440
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   441
lemma fix_imp_eq: "x \<in> fix f A ==> f x = x"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   442
by (simp add: fix_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   443
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   444
lemma fixf_subset:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   445
     "[| A \<subseteq> B; x \<in> fix (%y: A. f y) A |] ==> x \<in> fix f B"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   446
by (simp add: fix_def, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   447
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   448
subsection {* lemmas for Tarski, lub *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   450
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   451
blanchet
parents: 43197
diff changeset
   452
declare CL.lub_least[intro] CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro] PO.transE[intro] PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro]
blanchet
parents: 43197
diff changeset
   453
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   454
lemma (in CLF) lubH_le_flubH:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   455
     "H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   456
apply (rule lub_least, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   457
apply (rule f_in_funcset [THEN funcset_mem])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   458
apply (rule lub_in_lattice, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   459
-- {* @{text "\<forall>x:H. (x, f (lub H r)) \<in> r"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   460
apply (rule ballI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   461
(*never proved, 2007-01-22*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   462
apply (rule transE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   463
-- {* instantiates @{text "(x, ?z) \<in> order cl to (x, f x)"}, *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   464
-- {* because of the def of @{text H} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   465
apply fast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   466
-- {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   467
apply (rule_tac f = "f" in monotoneE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   468
apply (rule monotone_f, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   469
apply (rule lub_in_lattice, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   470
apply (rule lub_upper, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   471
apply assumption
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   472
done
45705
blanchet
parents: 43197
diff changeset
   473
blanchet
parents: 43197
diff changeset
   474
declare CL.lub_least[rule del] CLF.f_in_funcset[rule del]
blanchet
parents: 43197
diff changeset
   475
        funcset_mem[rule del] CL.lub_in_lattice[rule del]
blanchet
parents: 43197
diff changeset
   476
        PO.transE[rule del] PO.monotoneE[rule del]
blanchet
parents: 43197
diff changeset
   477
        CLF.monotone_f[rule del] CL.lub_upper[rule del]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   478
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   479
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   480
blanchet
parents: 43197
diff changeset
   481
declare CLF.f_in_funcset[intro] funcset_mem[intro] CL.lub_in_lattice[intro]
blanchet
parents: 43197
diff changeset
   482
     PO.monotoneE[intro] CLF.monotone_f[intro] CL.lub_upper[intro]
blanchet
parents: 43197
diff changeset
   483
     CLF.lubH_le_flubH[simp]
blanchet
parents: 43197
diff changeset
   484
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   485
lemma (in CLF) flubH_le_lubH:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   486
     "[|  H = {x. (x, f x) \<in> r & x \<in> A} |] ==> (f (lub H cl), lub H cl) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   487
apply (rule lub_upper, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   488
apply (rule_tac t = "H" in ssubst, assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   489
apply (rule CollectI)
47040
78e88d26f19d tune Metis example
blanchet
parents: 46752
diff changeset
   490
by (metis (lifting) CO_refl_on lubH_le_flubH monotone_def monotone_f refl_onD1 refl_onD2)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   491
45705
blanchet
parents: 43197
diff changeset
   492
declare CLF.f_in_funcset[rule del] funcset_mem[rule del]
blanchet
parents: 43197
diff changeset
   493
        CL.lub_in_lattice[rule del] PO.monotoneE[rule del]
blanchet
parents: 43197
diff changeset
   494
        CLF.monotone_f[rule del] CL.lub_upper[rule del]
blanchet
parents: 43197
diff changeset
   495
        CLF.lubH_le_flubH[simp del]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   496
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   497
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   498
37622
b3f572839570 no setup is necessary anymore
blanchet
parents: 36554
diff changeset
   499
(* Single-step version fails. The conjecture clauses refer to local abstraction
b3f572839570 no setup is necessary anymore
blanchet
parents: 36554
diff changeset
   500
functions (Frees). *)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   501
lemma (in CLF) lubH_is_fixp:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   502
     "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   503
apply (simp add: fix_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   504
apply (rule conjI)
36554
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   505
proof -
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   506
  assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}"
42762
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   507
  have F1: "\<forall>u v. v \<inter> u \<subseteq> u" by (metis Int_commute Int_lower1)
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   508
  have "{R. (R, f R) \<in> r} \<inter> {R. R \<in> A} = H" using A1 by (metis Collect_conj_eq)
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   509
  hence "H \<subseteq> {R. R \<in> A}" using F1 by metis
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   510
  hence "H \<subseteq> A" by (metis Collect_mem_eq)
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   511
  hence "lub H cl \<in> A" by (metis lub_in_lattice)
0b3c3cf28218 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
blanchet
parents: 42103
diff changeset
   512
  thus "lub {x. (x, f x) \<in> r \<and> x \<in> A} cl \<in> A" using A1 by metis
36554
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   513
next
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   514
  assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}"
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45705
diff changeset
   515
  have F1: "\<forall>v. {R. R \<in> v} = v" by (metis Collect_mem_eq)
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45705
diff changeset
   516
  have F2: "\<forall>w u. {R. R \<in> u \<and> R \<in> w} = u \<inter> w"
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45705
diff changeset
   517
    by (metis Collect_conj_eq Collect_mem_eq)
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45705
diff changeset
   518
  have F3: "\<forall>x v. {R. v R \<in> x} = v -` x" by (metis vimage_def)
36554
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   519
  hence F4: "A \<inter> (\<lambda>R. (R, f R)) -` r = H" using A1 by auto
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45705
diff changeset
   520
  hence F5: "(f (lub H cl), lub H cl) \<in> r" 
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45705
diff changeset
   521
    by (metis A1 flubH_le_lubH)
36554
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   522
  have F6: "(lub H cl, f (lub H cl)) \<in> r"
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45705
diff changeset
   523
    by (metis A1 lubH_le_flubH)
36554
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   524
  have "(lub H cl, f (lub H cl)) \<in> r \<longrightarrow> f (lub H cl) = lub H cl"
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   525
    using F5 by (metis antisymE)
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   526
  hence "f (lub H cl) = lub H cl" using F6 by metis
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   527
  thus "H = {x. (x, f x) \<in> r \<and> x \<in> A}
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   528
        \<Longrightarrow> f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) =
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   529
           lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45705
diff changeset
   530
    by metis
24827
646bdc51eb7d combinator translation
paulson
parents: 24545
diff changeset
   531
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   532
25710
4cdf7de81e1b Replaced refs by config params; finer critical section in mets method
paulson
parents: 24855
diff changeset
   533
lemma (in CLF) (*lubH_is_fixp:*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   534
     "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   535
apply (simp add: fix_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   536
apply (rule conjI)
30198
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
   537
apply (metis CO_refl_on lubH_le_flubH refl_onD1)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   538
apply (metis antisymE flubH_le_lubH lubH_le_flubH)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   539
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   540
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   541
lemma (in CLF) fix_in_H:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   542
     "[| H = {x. (x, f x) \<in> r & x \<in> A};  x \<in> P |] ==> x \<in> H"
30198
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
   543
by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl_on
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   544
                    fix_subset [of f A, THEN subsetD])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   545
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   546
lemma (in CLF) fixf_le_lubH:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   547
     "H = {x. (x, f x) \<in> r & x \<in> A} ==> \<forall>x \<in> fix f A. (x, lub H cl) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   548
apply (rule ballI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   549
apply (rule lub_upper, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   550
apply (rule fix_in_H)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   551
apply (simp_all add: P_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   552
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   553
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   554
lemma (in CLF) lubH_least_fixf:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   555
     "H = {x. (x, f x) \<in> r & x \<in> A}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   556
      ==> \<forall>L. (\<forall>y \<in> fix f A. (y,L) \<in> r) --> (lub H cl, L) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   557
apply (metis P_def lubH_is_fixp)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   558
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   559
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   560
subsection {* Tarski fixpoint theorem 1, first part *}
45705
blanchet
parents: 43197
diff changeset
   561
blanchet
parents: 43197
diff changeset
   562
declare CL.lubI[intro] fix_subset[intro] CL.lub_in_lattice[intro]
blanchet
parents: 43197
diff changeset
   563
        CLF.fixf_le_lubH[simp] CLF.lubH_least_fixf[simp]
blanchet
parents: 43197
diff changeset
   564
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   565
lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   566
(*sledgehammer;*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   567
apply (rule sym)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   568
apply (simp add: P_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   569
apply (rule lubI)
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   570
apply (metis P_def fix_subset)
24827
646bdc51eb7d combinator translation
paulson
parents: 24545
diff changeset
   571
apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def)
47040
78e88d26f19d tune Metis example
blanchet
parents: 46752
diff changeset
   572
apply (metis P_def fixf_le_lubH)
78e88d26f19d tune Metis example
blanchet
parents: 46752
diff changeset
   573
by (metis P_def lubH_least_fixf)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   574
45705
blanchet
parents: 43197
diff changeset
   575
declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del]
blanchet
parents: 43197
diff changeset
   576
        CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   577
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   578
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   579
blanchet
parents: 43197
diff changeset
   580
declare glb_dual_lub[simp] PO.dualA_iff[intro] CLF.lubH_is_fixp[intro]
blanchet
parents: 43197
diff changeset
   581
        PO.dualPO[intro] CL.CL_dualCL[intro] PO.dualr_iff[simp]
blanchet
parents: 43197
diff changeset
   582
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   583
lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \<in> r & x \<in> A} ==> glb H cl \<in> P"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   584
  -- {* Tarski for glb *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   585
(*sledgehammer;*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   586
apply (simp add: glb_dual_lub P_def A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   587
apply (rule dualA_iff [THEN subst])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   588
apply (rule CLF.lubH_is_fixp)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   589
apply (rule CLF.intro)
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   590
apply (rule CL.intro)
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   591
apply (rule PO.intro)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   592
apply (rule dualPO)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   593
apply (rule CL_axioms.intro)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   594
apply (rule CL_dualCL)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   595
apply (rule CLF_axioms.intro)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   596
apply (rule CLF_dual)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   597
apply (simp add: dualr_iff dualA_iff)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   598
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   599
45705
blanchet
parents: 43197
diff changeset
   600
declare glb_dual_lub[simp del] PO.dualA_iff[rule del] CLF.lubH_is_fixp[rule del]
blanchet
parents: 43197
diff changeset
   601
        PO.dualPO[rule del] CL.CL_dualCL[rule del] PO.dualr_iff[simp del]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   602
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   603
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   604
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   605
lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   606
(*sledgehammer;*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   607
apply (simp add: glb_dual_lub P_def A_def r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   608
apply (rule dualA_iff [THEN subst])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   609
(*never proved, 2007-01-22*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   610
(*sledgehammer;*)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   611
apply (simp add: CLF.T_thm_1_lub [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro,
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   612
  OF dualPO CL_dualCL] dualPO CL_dualCL CLF_dual dualr_iff)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   613
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   614
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   615
subsection {* interval *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   616
45705
blanchet
parents: 43197
diff changeset
   617
declare (in CLF) CO_refl_on[simp] refl_on_def [simp]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   618
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   619
lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
30198
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
   620
by (metis CO_refl_on refl_onD1)
45705
blanchet
parents: 43197
diff changeset
   621
blanchet
parents: 43197
diff changeset
   622
declare (in CLF) CO_refl_on[simp del]  refl_on_def [simp del]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   623
45705
blanchet
parents: 43197
diff changeset
   624
declare (in CLF) rel_imp_elem[intro]
blanchet
parents: 43197
diff changeset
   625
declare interval_def [simp]
blanchet
parents: 43197
diff changeset
   626
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   627
lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
30198
922f944f03b2 name changes
nipkow
parents: 28592
diff changeset
   628
by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   629
45705
blanchet
parents: 43197
diff changeset
   630
declare (in CLF) rel_imp_elem[rule del]
blanchet
parents: 43197
diff changeset
   631
declare interval_def [simp del]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   632
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   633
lemma (in CLF) intervalI:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   634
     "[| (a, x) \<in> r; (x, b) \<in> r |] ==> x \<in> interval r a b"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   635
by (simp add: interval_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   636
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   637
lemma (in CLF) interval_lemma1:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   638
     "[| S \<subseteq> interval r a b; x \<in> S |] ==> (a, x) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   639
by (unfold interval_def, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   640
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   641
lemma (in CLF) interval_lemma2:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   642
     "[| S \<subseteq> interval r a b; x \<in> S |] ==> (x, b) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   643
by (unfold interval_def, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   644
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   645
lemma (in CLF) a_less_lub:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   646
     "[| S \<subseteq> A; S \<noteq> {};
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   647
         \<forall>x \<in> S. (a,x) \<in> r; \<forall>y \<in> S. (y, L) \<in> r |] ==> (a,L) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   648
by (blast intro: transE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   649
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   650
lemma (in CLF) glb_less_b:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   651
     "[| S \<subseteq> A; S \<noteq> {};
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   652
         \<forall>x \<in> S. (x,b) \<in> r; \<forall>y \<in> S. (G, y) \<in> r |] ==> (G,b) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   653
by (blast intro: transE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   654
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   655
lemma (in CLF) S_intv_cl:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   656
     "[| a \<in> A; b \<in> A; S \<subseteq> interval r a b |]==> S \<subseteq> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   657
by (simp add: subset_trans [OF _ interval_subset])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   658
45705
blanchet
parents: 43197
diff changeset
   659
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   660
lemma (in CLF) L_in_interval:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   661
     "[| a \<in> A; b \<in> A; S \<subseteq> interval r a b;
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   662
         S \<noteq> {}; isLub S cl L; interval r a b \<noteq> {} |] ==> L \<in> interval r a b"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   663
(*WON'T TERMINATE
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   664
apply (metis CO_trans intervalI interval_lemma1 interval_lemma2 isLub_least isLub_upper subset_empty subset_iff trans_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   665
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   666
apply (rule intervalI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   667
apply (rule a_less_lub)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   668
prefer 2 apply assumption
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   669
apply (simp add: S_intv_cl)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   670
apply (rule ballI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   671
apply (simp add: interval_lemma1)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   672
apply (simp add: isLub_upper)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   673
-- {* @{text "(L, b) \<in> r"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   674
apply (simp add: isLub_least interval_lemma2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   675
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   676
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   677
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   678
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   679
lemma (in CLF) G_in_interval:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   680
     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G;
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   681
         S \<noteq> {} |] ==> G \<in> interval r a b"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   682
apply (simp add: interval_dual)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   683
apply (simp add: CLF.L_in_interval [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   684
                 dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   685
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   686
45705
blanchet
parents: 43197
diff changeset
   687
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   688
lemma (in CLF) intervalPO:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   689
     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   690
      ==> (| pset = interval r a b, order = induced (interval r a b) r |)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   691
          \<in> PartialOrder"
36554
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   692
proof -
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   693
  assume A1: "a \<in> A"
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   694
  assume "b \<in> A"
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   695
  hence "\<forall>u. u \<in> A \<longrightarrow> interval r u b \<subseteq> A" by (metis interval_subset)
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   696
  hence "interval r a b \<subseteq> A" using A1 by metis
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   697
  hence "interval r a b \<subseteq> A" by metis
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
   698
  thus ?thesis by (metis po_subset_po)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   699
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   700
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   701
lemma (in CLF) intv_CL_lub:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   702
 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   703
  ==> \<forall>S. S \<subseteq> interval r a b -->
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   704
          (\<exists>L. isLub S (| pset = interval r a b,
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   705
                          order = induced (interval r a b) r |)  L)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   706
apply (intro strip)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   707
apply (frule S_intv_cl [THEN CL_imp_ex_isLub])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   708
prefer 2 apply assumption
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   709
apply assumption
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   710
apply (erule exE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   711
-- {* define the lub for the interval as *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   712
apply (rule_tac x = "if S = {} then a else L" in exI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   713
apply (simp (no_asm_simp) add: isLub_def split del: split_if)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   714
apply (intro impI conjI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   715
-- {* @{text "(if S = {} then a else L) \<in> interval r a b"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   716
apply (simp add: CL_imp_PO L_in_interval)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   717
apply (simp add: left_in_interval)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   718
-- {* lub prop 1 *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   719
apply (case_tac "S = {}")
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   720
-- {* @{text "S = {}, y \<in> S = False => everything"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   721
apply fast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   722
-- {* @{text "S \<noteq> {}"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   723
apply simp
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   724
-- {* @{text "\<forall>y:S. (y, L) \<in> induced (interval r a b) r"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   725
apply (rule ballI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   726
apply (simp add: induced_def  L_in_interval)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   727
apply (rule conjI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   728
apply (rule subsetD)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   729
apply (simp add: S_intv_cl, assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   730
apply (simp add: isLub_upper)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   731
-- {* @{text "\<forall>z:interval r a b. (\<forall>y:S. (y, z) \<in> induced (interval r a b) r \<longrightarrow> (if S = {} then a else L, z) \<in> induced (interval r a b) r"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   732
apply (rule ballI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   733
apply (rule impI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   734
apply (case_tac "S = {}")
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   735
-- {* @{text "S = {}"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   736
apply simp
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   737
apply (simp add: induced_def  interval_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   738
apply (rule conjI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   739
apply (rule reflE, assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   740
apply (rule interval_not_empty)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   741
apply (rule CO_trans)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   742
apply (simp add: interval_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   743
-- {* @{text "S \<noteq> {}"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   744
apply simp
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   745
apply (simp add: induced_def  L_in_interval)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   746
apply (rule isLub_least, assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   747
apply (rule subsetD)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   748
prefer 2 apply assumption
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   749
apply (simp add: S_intv_cl, fast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   750
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   751
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   752
lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   753
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   754
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   755
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   756
lemma (in CLF) interval_is_sublattice:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   757
     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   758
        ==> interval r a b <<= cl"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   759
(*sledgehammer *)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   760
apply (rule sublatticeI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   761
apply (simp add: interval_subset)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   762
(*never proved, 2007-01-22*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   763
(*sledgehammer *)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   764
apply (rule CompleteLatticeI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   765
apply (simp add: intervalPO)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   766
 apply (simp add: intv_CL_lub)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   767
apply (simp add: intv_CL_glb)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   768
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   769
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   770
lemmas (in CLF) interv_is_compl_latt =
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   771
    interval_is_sublattice [THEN sublattice_imp_CL]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   772
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   773
subsection {* Top and Bottom *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   774
lemma (in CLF) Top_dual_Bot: "Top cl = Bot (dual cl)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   775
by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   776
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   777
lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   778
by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   779
45705
blanchet
parents: 43197
diff changeset
   780
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   781
lemma (in CLF) Bot_in_lattice: "Bot cl \<in> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   782
(*sledgehammer; *)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   783
apply (simp add: Bot_def least_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   784
apply (rule_tac a="glb A cl" in someI2)
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   785
apply (simp_all add: glb_in_lattice glb_lower
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   786
                     r_def [symmetric] A_def [symmetric])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   787
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   788
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   789
(*first proved 2007-01-25 after relaxing relevance*)
45705
blanchet
parents: 43197
diff changeset
   790
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   791
lemma (in CLF) Top_in_lattice: "Top cl \<in> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   792
(*sledgehammer;*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   793
apply (simp add: Top_dual_Bot A_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   794
(*first proved 2007-01-25 after relaxing relevance*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   795
(*sledgehammer*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   796
apply (rule dualA_iff [THEN subst])
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   797
apply (blast intro!: CLF.Bot_in_lattice [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] dualPO CL_dualCL CLF_dual)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   798
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   799
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   800
lemma (in CLF) Top_prop: "x \<in> A ==> (x, Top cl) \<in> r"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   801
apply (simp add: Top_def greatest_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   802
apply (rule_tac a="lub A cl" in someI2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   803
apply (rule someI2)
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   804
apply (simp_all add: lub_in_lattice lub_upper
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   805
                     r_def [symmetric] A_def [symmetric])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   806
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   807
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   808
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   809
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   810
lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r"
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   811
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   812
apply (simp add: Bot_dual_Top r_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   813
apply (rule dualr_iff [THEN subst])
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   814
apply (simp add: CLF.Top_prop [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   815
                 dualA_iff A_def dualPO CL_dualCL CLF_dual)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   816
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   817
45705
blanchet
parents: 43197
diff changeset
   818
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   819
lemma (in CLF) Top_intv_not_empty: "x \<in> A  ==> interval r x (Top cl) \<noteq> {}"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   820
apply (metis Top_in_lattice Top_prop empty_iff intervalI reflE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   821
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   822
45705
blanchet
parents: 43197
diff changeset
   823
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   824
lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   825
apply (metis Bot_prop ex_in_conv intervalI reflE rel_imp_elem)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   826
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   827
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   828
subsection {* fixed points form a partial order *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   829
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   830
lemma (in CLF) fixf_po: "(| pset = P, order = induced P r|) \<in> PartialOrder"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   831
by (simp add: P_def fix_subset po_subset_po)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   832
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   833
(*first proved 2007-01-25 after relaxing relevance*)
45705
blanchet
parents: 43197
diff changeset
   834
blanchet
parents: 43197
diff changeset
   835
declare (in Tarski) P_def[simp] Y_ss [simp]
blanchet
parents: 43197
diff changeset
   836
declare fix_subset [intro] subset_trans [intro]
blanchet
parents: 43197
diff changeset
   837
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   838
lemma (in Tarski) Y_subset_A: "Y \<subseteq> A"
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   839
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   840
apply (rule subset_trans [OF _ fix_subset])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   841
apply (rule Y_ss [simplified P_def])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   842
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   843
45705
blanchet
parents: 43197
diff changeset
   844
declare (in Tarski) P_def[simp del] Y_ss [simp del]
blanchet
parents: 43197
diff changeset
   845
declare fix_subset [rule del] subset_trans [rule del]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   846
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   847
lemma (in Tarski) lubY_in_A: "lub Y cl \<in> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   848
  by (rule Y_subset_A [THEN lub_in_lattice])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   849
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   850
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   851
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   852
lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \<in> r"
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   853
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   854
apply (rule lub_least)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   855
apply (rule Y_subset_A)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   856
apply (rule f_in_funcset [THEN funcset_mem])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   857
apply (rule lubY_in_A)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   858
-- {* @{text "Y \<subseteq> P ==> f x = x"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   859
apply (rule ballI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   860
(*sledgehammer *)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   861
apply (rule_tac t = "x" in fix_imp_eq [THEN subst])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   862
apply (erule Y_ss [simplified P_def, THEN subsetD])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   863
-- {* @{text "reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r"} by monotonicity *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   864
(*sledgehammer*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   865
apply (rule_tac f = "f" in monotoneE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   866
apply (rule monotone_f)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   867
apply (simp add: Y_subset_A [THEN subsetD])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   868
apply (rule lubY_in_A)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   869
apply (simp add: lub_upper Y_subset_A)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   870
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   871
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   872
(*first proved 2007-01-25 after relaxing relevance*)
45705
blanchet
parents: 43197
diff changeset
   873
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   874
lemma (in Tarski) intY1_subset: "intY1 \<subseteq> A"
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   875
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   876
apply (unfold intY1_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   877
apply (rule interval_subset)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   878
apply (rule lubY_in_A)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   879
apply (rule Top_in_lattice)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   880
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   881
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   882
lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   883
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   884
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   885
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   886
lemma (in Tarski) intY1_f_closed: "x \<in> intY1 \<Longrightarrow> f x \<in> intY1"
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   887
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   888
apply (simp add: intY1_def  interval_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   889
apply (rule conjI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   890
apply (rule transE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   891
apply (rule lubY_le_flubY)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   892
-- {* @{text "(f (lub Y cl), f x) \<in> r"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   893
(*sledgehammer [has been proved before now...]*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   894
apply (rule_tac f=f in monotoneE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   895
apply (rule monotone_f)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   896
apply (rule lubY_in_A)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   897
apply (simp add: intY1_def interval_def  intY1_elem)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   898
apply (simp add: intY1_def  interval_def)
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   899
-- {* @{text "(f x, Top cl) \<in> r"} *}
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   900
apply (rule Top_prop)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   901
apply (rule f_in_funcset [THEN funcset_mem])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   902
apply (simp add: intY1_def interval_def  intY1_elem)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   903
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   904
45705
blanchet
parents: 43197
diff changeset
   905
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 26806
diff changeset
   906
lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
9f90ac19e32b established Plain theory and image
haftmann
parents: 26806
diff changeset
   907
apply (rule restrict_in_funcset)
9f90ac19e32b established Plain theory and image
haftmann
parents: 26806
diff changeset
   908
apply (metis intY1_f_closed restrict_in_funcset)
9f90ac19e32b established Plain theory and image
haftmann
parents: 26806
diff changeset
   909
done
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   910
45705
blanchet
parents: 43197
diff changeset
   911
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   912
lemma (in Tarski) intY1_mono:
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   913
     "monotone (%x: intY1. f x) intY1 (induced intY1 r)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   914
(*sledgehammer *)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   915
apply (auto simp add: monotone_def induced_def intY1_f_closed)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   916
apply (blast intro: intY1_elem monotone_f [THEN monotoneE])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   917
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   918
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   919
(*proof requires relaxing relevance: 2007-01-25*)
45705
blanchet
parents: 43197
diff changeset
   920
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   921
lemma (in Tarski) intY1_is_cl:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   922
    "(| pset = intY1, order = induced intY1 r |) \<in> CompleteLattice"
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   923
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   924
apply (unfold intY1_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   925
apply (rule interv_is_compl_latt)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   926
apply (rule lubY_in_A)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   927
apply (rule Top_in_lattice)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   928
apply (rule Top_intv_not_empty)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   929
apply (rule lubY_in_A)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   930
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   931
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   932
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   933
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   934
lemma (in Tarski) v_in_P: "v \<in> P"
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   935
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   936
apply (unfold P_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   937
apply (rule_tac A = "intY1" in fixf_subset)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   938
apply (rule intY1_subset)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   939
apply (simp add: CLF.glbH_is_fixp [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified]
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   940
                 v_def CL_imp_PO intY1_is_cl CLF_set_def intY1_func intY1_mono)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   941
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   942
45705
blanchet
parents: 43197
diff changeset
   943
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   944
lemma (in Tarski) z_in_interval:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   945
     "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] ==> z \<in> intY1"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   946
(*sledgehammer *)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   947
apply (unfold intY1_def P_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   948
apply (rule intervalI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   949
prefer 2
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   950
 apply (erule fix_subset [THEN subsetD, THEN Top_prop])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   951
apply (rule lub_least)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   952
apply (rule Y_subset_A)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   953
apply (fast elim!: fix_subset [THEN subsetD])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   954
apply (simp add: induced_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   955
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   956
45705
blanchet
parents: 43197
diff changeset
   957
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   958
lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |]
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   959
      ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r"
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26483
diff changeset
   960
apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   961
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   962
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   963
(*never proved, 2007-01-22*)
45705
blanchet
parents: 43197
diff changeset
   964
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   965
lemma (in Tarski) tarski_full_lemma:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   966
     "\<exists>L. isLub Y (| pset = P, order = induced P r |) L"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   967
apply (rule_tac x = "v" in exI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   968
apply (simp add: isLub_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   969
-- {* @{text "v \<in> P"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   970
apply (simp add: v_in_P)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   971
apply (rule conjI)
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   972
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   973
-- {* @{text v} is lub *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   974
-- {* @{text "1. \<forall>y:Y. (y, v) \<in> induced P r"} *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   975
apply (rule ballI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   976
apply (simp add: induced_def subsetD v_in_P)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   977
apply (rule conjI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   978
apply (erule Y_ss [THEN subsetD])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   979
apply (rule_tac b = "lub Y cl" in transE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   980
apply (rule lub_upper)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   981
apply (rule Y_subset_A, assumption)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   982
apply (rule_tac b = "Top cl" in interval_imp_mem)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   983
apply (simp add: v_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   984
apply (fold intY1_def)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   985
apply (rule CL.glb_in_lattice [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified])
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   986
 apply (simp add: CL_imp_PO intY1_is_cl, force)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   987
-- {* @{text v} is LEAST ub *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   988
apply clarify
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   989
apply (rule indI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   990
  prefer 3 apply assumption
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   991
 prefer 2 apply (simp add: v_in_P)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   992
apply (unfold v_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   993
(*never proved, 2007-01-22*)
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   994
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   995
apply (rule indE)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   996
apply (rule_tac [2] intY1_subset)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   997
(*never proved, 2007-01-22*)
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
   998
(*sledgehammer*)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
   999
apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified])
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1000
  apply (simp add: CL_imp_PO intY1_is_cl)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1001
 apply force
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1002
apply (simp add: induced_def intY1_f_closed z_in_interval)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1003
apply (simp add: P_def fix_imp_eq [of _ f A] reflE
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1004
                 fix_subset [of f A, THEN subsetD])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1005
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1006
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1007
lemma CompleteLatticeI_simp:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1008
     "[| (| pset = A, order = r |) \<in> PartialOrder;
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1009
         \<forall>S. S \<subseteq> A --> (\<exists>L. isLub S (| pset = A, order = r |)  L) |]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1010
    ==> (| pset = A, order = r |) \<in> CompleteLattice"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1011
by (simp add: CompleteLatticeI Rdual)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1012
45705
blanchet
parents: 43197
diff changeset
  1013
(*never proved, 2007-01-22*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1014
45705
blanchet
parents: 43197
diff changeset
  1015
declare (in CLF) fixf_po[intro] P_def [simp] A_def [simp] r_def [simp]
blanchet
parents: 43197
diff changeset
  1016
             Tarski.tarski_full_lemma [intro] cl_po [intro] cl_co [intro]
blanchet
parents: 43197
diff changeset
  1017
             CompleteLatticeI_simp [intro]
blanchet
parents: 43197
diff changeset
  1018
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1019
theorem (in CLF) Tarski_full:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1020
     "(| pset = P, order = induced P r|) \<in> CompleteLattice"
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
  1021
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1022
apply (rule CompleteLatticeI_simp)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1023
apply (rule fixf_po, clarify)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1024
(*never proved, 2007-01-22*)
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42762
diff changeset
  1025
(*sledgehammer*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1026
apply (simp add: P_def A_def r_def)
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
  1027
apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro,
8cedebf55539 dropped locale (open)
haftmann
parents: 27368
diff changeset
  1028
  OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1029
done
36554
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
  1030
2673979cb54d more neg_clausify proofs that get replaced by direct proofs
blanchet
parents: 35416
diff changeset
  1031
declare (in CLF) fixf_po [rule del] P_def [simp del] A_def [simp del] r_def [simp del]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1032
         Tarski.tarski_full_lemma [rule del] cl_po [rule del] cl_co [rule del]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1033
         CompleteLatticeI_simp [rule del]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1034
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
  1035
end