src/HOL/ex/Tarski.thy
author paulson
Wed, 08 May 2002 09:08:16 +0200
changeset 13115 0a6fbdedcde2
parent 12459 6978ab7cac64
child 13383 041d78bf9403
permissions -rw-r--r--
Tidied and converted to Isar by lcp
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/Tarski
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
     3
    Author:     Florian Kammueller, Cambridge University Computer Laboratory
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
     5
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
     6
Minimal version of lattice theory plus the full theorem of Tarski:
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
     7
   The fixedpoints of a complete lattice themselves form a complete lattice.
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
     8
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
     9
Illustrates first-class theories, using the Sigma representation of structures
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    10
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    11
Tidied and converted to Isar by lcp
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    12
*)
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    13
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    14
theory Tarski = Main:
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    15
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    16
record 'a potype = 
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    17
  pset  :: "'a set"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    18
  order :: "('a * 'a) set"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    19
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    20
syntax
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    21
  "@pset"  :: "'a potype => 'a set"            ("_ .<A>"  [90] 90)
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    22
  "@order" :: "'a potype => ('a *'a)set"       ("_ .<r>"  [90] 90) 
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    23
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    24
translations
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    25
  "po.<A>" == "pset po"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    26
  "po.<r>" == "order po"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    27
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    28
constdefs
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    29
  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    30
    "monotone f A r == \<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    31
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    32
  least :: "['a => bool, 'a potype] => 'a"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    33
   "least P po == @ x. x: po.<A> & P x &
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    34
                       (\<forall>y \<in> po.<A>. P y --> (x,y): po.<r>)"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    35
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    36
  greatest :: "['a => bool, 'a potype] => 'a"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    37
   "greatest P po == @ x. x: po.<A> & P x &
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    38
                          (\<forall>y \<in> po.<A>. P y --> (y,x): po.<r>)"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    39
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    40
  lub  :: "['a set, 'a potype] => 'a"
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    41
   "lub S po == least (%x. \<forall>y\<in>S. (y,x): po.<r>) po"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    42
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    43
  glb  :: "['a set, 'a potype] => 'a"
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    44
   "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): po.<r>) po"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    45
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    46
  isLub :: "['a set, 'a potype, 'a] => bool"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    47
   "isLub S po == %L. (L: po.<A> & (\<forall>y\<in>S. (y,L): po.<r>) &
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    48
                      (\<forall>z\<in>po.<A>. (\<forall>y\<in>S. (y,z): po.<r>) --> (L,z): po.<r>))"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    49
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    50
  isGlb :: "['a set, 'a potype, 'a] => bool"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    51
   "isGlb S po == %G. (G: po.<A> & (\<forall>y\<in>S. (G,y): po.<r>) &
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    52
                     (\<forall>z \<in> po.<A>. (\<forall>y\<in>S. (z,y): po.<r>) --> (z,G): po.<r>))"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    53
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    54
  "fix"    :: "[('a => 'a), 'a set] => 'a set"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    55
   "fix f A  == {x. x: A & f x = x}"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    56
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    57
  interval :: "[('a*'a) set,'a, 'a ] => 'a set"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    58
   "interval r a b == {x. (a,x): r & (x,b): r}"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    59
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    60
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    61
constdefs
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    62
  Bot :: "'a potype => 'a"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    63
   "Bot po == least (%x. True) po"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    64
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    65
  Top :: "'a potype => 'a"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    66
   "Top po == greatest (%x. True) po"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    67
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    68
  PartialOrder :: "('a potype) set"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    69
   "PartialOrder == {P. refl (P.<A>) (P.<r>) & antisym (P.<r>) &
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    70
		        trans (P.<r>)}"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    71
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    72
  CompleteLattice :: "('a potype) set"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    73
   "CompleteLattice == {cl. cl: PartialOrder & 
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    74
			(\<forall>S. S <= cl.<A> --> (\<exists>L. isLub S cl L)) &
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
    75
			(\<forall>S. S <= cl.<A> --> (\<exists>G. isGlb S cl G))}"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    76
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    77
  CLF :: "('a potype * ('a => 'a)) set"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    78
   "CLF == SIGMA cl: CompleteLattice.
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    79
             {f. f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)}"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    80
  
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    81
  induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    82
   "induced A r == {(a,b). a : A & b: A & (a,b): r}"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    83
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    84
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    85
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    86
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    87
constdefs
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    88
  sublattice :: "('a potype * 'a set)set"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    89
   "sublattice == 
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    90
      SIGMA cl: CompleteLattice.
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    91
          {S. S <= cl.<A> &
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    92
	   (| pset = S, order = induced S (cl.<r>) |): CompleteLattice }"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    93
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    94
syntax
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    95
  "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    96
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    97
translations
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
    98
  "S <<= cl" == "S : sublattice `` {cl}"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
    99
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   100
constdefs
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   101
  dual :: "'a potype => 'a potype"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   102
   "dual po == (| pset = po.<A>, order = converse (po.<r>) |)"
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   103
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   104
locale PO = 
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   105
  fixes cl :: "'a potype"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   106
    and A  :: "'a set"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   107
    and r  :: "('a * 'a) set"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   108
  assumes cl_po:  "cl : PartialOrder"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   109
  defines A_def: "A == cl.<A>"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   110
     and  r_def: "r == cl.<r>"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   111
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   112
locale CL = PO +
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   113
  assumes cl_co:  "cl : CompleteLattice"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   114
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   115
locale CLF = CL +
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   116
  fixes f :: "'a => 'a"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   117
    and P :: "'a set"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   118
  assumes f_cl:  "(cl,f) : CLF" (*was the equivalent "f : CLF``{cl}"*)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   119
  defines P_def: "P == fix f A"
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   120
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   121
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   122
locale Tarski = CLF + 
13115
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   123
  fixes Y     :: "'a set"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   124
    and intY1 :: "'a set"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   125
    and v     :: "'a"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   126
  assumes
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   127
    Y_ss: "Y <= P"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   128
  defines
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   129
    intY1_def: "intY1 == interval r (lub Y cl) (Top cl)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   130
    and v_def: "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r & 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   131
                             x: intY1}
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   132
		      (| pset=intY1, order=induced intY1 r|)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   133
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   134
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   135
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   136
(* Partial Order *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   137
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   138
lemma (in PO) PO_imp_refl: "refl A r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   139
apply (insert cl_po) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   140
apply (simp add: PartialOrder_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   141
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   142
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   143
lemma (in PO) PO_imp_sym: "antisym r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   144
apply (insert cl_po) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   145
apply (simp add: PartialOrder_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   146
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   147
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   148
lemma (in PO) PO_imp_trans: "trans r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   149
apply (insert cl_po) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   150
apply (simp add: PartialOrder_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   151
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   152
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   153
lemma (in PO) reflE: "[| refl A r; x \<in> A|] ==> (x, x) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   154
apply (insert cl_po) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   155
apply (simp add: PartialOrder_def refl_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   156
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   157
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   158
lemma (in PO) antisymE: "[| antisym r; (a, b) \<in> r; (b, a) \<in> r |] ==> a = b"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   159
apply (insert cl_po) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   160
apply (simp add: PartialOrder_def antisym_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   161
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   162
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   163
lemma (in PO) transE: "[| trans r; (a, b) \<in> r; (b, c) \<in> r|] ==> (a,c) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   164
apply (insert cl_po) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   165
apply (simp add: PartialOrder_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   166
apply (unfold trans_def, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   167
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   168
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   169
lemma (in PO) monotoneE:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   170
     "[| monotone f A r;  x \<in> A; y \<in> A; (x, y) \<in> r |] ==> (f x, f y) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   171
by (simp add: monotone_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   172
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   173
lemma (in PO) po_subset_po:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   174
     "S <= A ==> (| pset = S, order = induced S r |) \<in> PartialOrder"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   175
apply (simp (no_asm) add: PartialOrder_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   176
apply auto
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   177
(* refl *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   178
apply (simp add: refl_def induced_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   179
apply (blast intro: PO_imp_refl [THEN reflE])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   180
(* antisym *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   181
apply (simp add: antisym_def induced_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   182
apply (blast intro: PO_imp_sym [THEN antisymE])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   183
(* trans *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   184
apply (simp add: trans_def induced_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   185
apply (blast intro: PO_imp_trans [THEN transE])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   186
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   187
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   188
lemma (in PO) indE: "[| (x, y) \<in> induced S r; S <= A |] ==> (x, y) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   189
by (simp add: add: induced_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   190
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   191
lemma (in PO) indI: "[| (x, y) \<in> r; x \<in> S; y \<in> S |] ==> (x, y) \<in> induced S r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   192
by (simp add: add: induced_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   193
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   194
lemma (in CL) CL_imp_ex_isLub: "S <= A ==> \<exists>L. isLub S cl L" 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   195
apply (insert cl_co) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   196
apply (simp add: CompleteLattice_def A_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   197
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   198
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   199
declare (in CL) cl_co [simp]
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   200
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   201
lemma isLub_lub: "(\<exists>L. isLub S cl L) = isLub S cl (lub S cl)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   202
by (simp add: lub_def least_def isLub_def some_eq_ex [symmetric])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   203
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   204
lemma isGlb_glb: "(\<exists>G. isGlb S cl G) = isGlb S cl (glb S cl)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   205
by (simp add: glb_def greatest_def isGlb_def some_eq_ex [symmetric])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   206
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   207
lemma isGlb_dual_isLub: "isGlb S cl = isLub S (dual cl)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   208
by (simp add: isLub_def isGlb_def dual_def converse_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   209
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   210
lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   211
by (simp add: isLub_def isGlb_def dual_def converse_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   212
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   213
lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   214
apply (insert cl_po) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   215
apply (simp add: PartialOrder_def dual_def refl_converse 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   216
                 trans_converse antisym_converse)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   217
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   218
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   219
lemma Rdual:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   220
     "\<forall>S. (S <= A -->( \<exists>L. isLub S (| pset = A, order = r|) L))  
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   221
      ==> \<forall>S. (S <= A --> (\<exists>G. isGlb S (| pset = A, order = r|) G))"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   222
apply safe
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   223
apply (rule_tac x = "lub {y. y \<in> A & (\<forall>k \<in> S. (y, k) \<in> r)}
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   224
                      (|pset = A, order = r|) " in exI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   225
apply (drule_tac x = "{y. y \<in> A & (\<forall>k \<in> S. (y,k) \<in> r) }" in spec)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   226
apply (drule mp, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   227
apply (simp add: isLub_lub isGlb_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   228
apply (simp add: isLub_def, blast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   229
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   230
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   231
lemma lub_dual_glb: "lub S cl = glb S (dual cl)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   232
by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   233
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   234
lemma glb_dual_lub: "glb S cl = lub S (dual cl)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   235
by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   236
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   237
lemma CL_subset_PO: "CompleteLattice <= PartialOrder"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   238
by (simp add: PartialOrder_def CompleteLattice_def, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   239
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   240
lemmas CL_imp_PO = CL_subset_PO [THEN subsetD]
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   241
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   242
declare CL_imp_PO [THEN Tarski.PO_imp_refl, simp]
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   243
declare CL_imp_PO [THEN Tarski.PO_imp_sym, simp]
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   244
declare CL_imp_PO [THEN Tarski.PO_imp_trans, simp]
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   245
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   246
lemma (in CL) CO_refl: "refl A r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   247
by (rule PO_imp_refl)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   248
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   249
lemma (in CL) CO_antisym: "antisym r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   250
by (rule PO_imp_sym)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   251
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   252
lemma (in CL) CO_trans: "trans r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   253
by (rule PO_imp_trans)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   254
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   255
lemma CompleteLatticeI:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   256
     "[| po \<in> PartialOrder; (\<forall>S. S <= po.<A> --> (\<exists>L. isLub S po L)); 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   257
         (\<forall>S. S <= po.<A> --> (\<exists>G. isGlb S po G))|] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   258
      ==> po \<in> CompleteLattice"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   259
apply (unfold CompleteLattice_def, blast) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   260
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   261
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   262
lemma (in CL) CL_dualCL: "dual cl \<in> CompleteLattice"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   263
apply (insert cl_co) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   264
apply (simp add: CompleteLattice_def dual_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   265
apply (fold dual_def) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   266
apply (simp add: isLub_dual_isGlb [symmetric] isGlb_dual_isLub [symmetric] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   267
                 dualPO)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   268
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   269
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   270
lemma (in PO) dualA_iff: "(dual cl.<A>) = cl.<A>"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   271
by (simp add: dual_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   272
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   273
lemma (in PO) dualr_iff: "((x, y) \<in> (dual cl.<r>)) = ((y, x) \<in> cl.<r>)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   274
by (simp add: dual_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   275
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   276
lemma (in PO) monotone_dual:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   277
     "monotone f (cl.<A>) (cl.<r>) ==> monotone f (dual cl.<A>) (dual cl.<r>)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   278
apply (simp add: monotone_def dualA_iff dualr_iff)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   279
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   280
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   281
lemma (in PO) interval_dual:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   282
     "[| x \<in> A; y \<in> A|] ==> interval r x y = interval (dual cl.<r>) y x"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   283
apply (simp add: interval_def dualr_iff)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   284
apply (fold r_def, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   285
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   286
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   287
lemma (in PO) interval_not_empty:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   288
     "[| trans r; interval r a b \<noteq> {} |] ==> (a, b) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   289
apply (simp add: interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   290
apply (unfold trans_def, blast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   291
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   292
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   293
lemma (in PO) interval_imp_mem: "x \<in> interval r a b ==> (a, x) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   294
by (simp add: interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   295
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   296
lemma (in PO) left_in_interval:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   297
     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] ==> a \<in> interval r a b"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   298
apply (simp (no_asm_simp) add: interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   299
apply (simp add: PO_imp_trans interval_not_empty)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   300
apply (simp add: PO_imp_refl [THEN reflE])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   301
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   302
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   303
lemma (in PO) right_in_interval:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   304
     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] ==> b \<in> interval r a b"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   305
apply (simp (no_asm_simp) add: interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   306
apply (simp add: PO_imp_trans interval_not_empty)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   307
apply (simp add: PO_imp_refl [THEN reflE])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   308
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   309
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   310
(* sublattice *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   311
lemma (in PO) sublattice_imp_CL:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   312
     "S <<= cl  ==> (| pset = S, order = induced S r |) \<in> CompleteLattice"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   313
by (simp add: sublattice_def CompleteLattice_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   314
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   315
lemma (in CL) sublatticeI:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   316
     "[| S <= A; (| pset = S, order = induced S r |) \<in> CompleteLattice |] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   317
      ==> S <<= cl"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   318
by (simp add: sublattice_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   319
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   320
(* lub *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   321
lemma (in CL) lub_unique: "[| S <= A; isLub S cl x; isLub S cl L|] ==> x = L"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   322
apply (rule antisymE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   323
apply (rule CO_antisym)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   324
apply (auto simp add: isLub_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   325
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   326
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   327
lemma (in CL) lub_upper: "[|S <= A; x \<in> S|] ==> (x, lub S cl) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   328
apply (rule CL_imp_ex_isLub [THEN exE], assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   329
apply (unfold lub_def least_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   330
apply (rule some_equality [THEN ssubst])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   331
  apply (simp add: isLub_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   332
 apply (simp add: lub_unique A_def isLub_def) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   333
apply (simp add: isLub_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   334
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   335
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   336
lemma (in CL) lub_least:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   337
     "[| S <= A; L \<in> A; \<forall>x \<in> S. (x,L) \<in> r |] ==> (lub S cl, L) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   338
apply (rule CL_imp_ex_isLub [THEN exE], assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   339
apply (unfold lub_def least_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   340
apply (rule_tac s=x in some_equality [THEN ssubst])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   341
  apply (simp add: isLub_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   342
 apply (simp add: lub_unique A_def isLub_def) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   343
apply (simp add: isLub_def r_def A_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   344
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   345
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   346
lemma (in CL) lub_in_lattice: "S <= A ==> lub S cl \<in> A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   347
apply (rule CL_imp_ex_isLub [THEN exE], assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   348
apply (unfold lub_def least_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   349
apply (subst some_equality)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   350
apply (simp add: isLub_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   351
prefer 2 apply (simp add: isLub_def A_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   352
apply (simp add: lub_unique A_def isLub_def) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   353
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   354
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   355
lemma (in CL) lubI:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   356
     "[| S <= A; L \<in> A; \<forall>x \<in> S. (x,L) \<in> r; 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   357
         \<forall>z \<in> A. (\<forall>y \<in> S. (y,z) \<in> r) --> (L,z) \<in> r |] ==> L = lub S cl"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   358
apply (rule lub_unique, assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   359
apply (simp add: isLub_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   360
apply (unfold isLub_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   361
apply (rule conjI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   362
apply (fold A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   363
apply (rule lub_in_lattice, assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   364
apply (simp add: lub_upper lub_least)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   365
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   366
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   367
lemma (in CL) lubIa: "[| S <= A; isLub S cl L |] ==> L = lub S cl"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   368
by (simp add: lubI isLub_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   369
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   370
lemma (in CL) isLub_in_lattice: "isLub S cl L ==> L \<in> A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   371
by (simp add: isLub_def  A_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   372
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   373
lemma (in CL) isLub_upper: "[|isLub S cl L; y \<in> S|] ==> (y, L) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   374
by (simp add: isLub_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   375
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   376
lemma (in CL) isLub_least:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   377
     "[| isLub S cl L; z \<in> A; \<forall>y \<in> S. (y, z) \<in> r|] ==> (L, z) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   378
by (simp add: isLub_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   379
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   380
lemma (in CL) isLubI:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   381
     "[| L \<in> A; \<forall>y \<in> S. (y, L) \<in> r;  
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   382
         (\<forall>z \<in> A. (\<forall>y \<in> S. (y, z):r) --> (L, z) \<in> r)|] ==> isLub S cl L"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   383
by (simp add: isLub_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   384
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   385
(* glb *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   386
lemma (in CL) glb_in_lattice: "S <= A ==> glb S cl \<in> A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   387
apply (subst glb_dual_lub)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   388
apply (simp add: A_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   389
apply (rule dualA_iff [THEN subst])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   390
apply (rule Tarski.lub_in_lattice)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   391
apply (rule dualPO) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   392
apply (rule CL_dualCL)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   393
apply (simp add: dualA_iff)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   394
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   395
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   396
lemma (in CL) glb_lower: "[|S <= A; x \<in> S|] ==> (glb S cl, x) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   397
apply (subst glb_dual_lub)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   398
apply (simp add: r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   399
apply (rule dualr_iff [THEN subst])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   400
apply (rule Tarski.lub_upper [rule_format])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   401
apply (rule dualPO) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   402
apply (rule CL_dualCL)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   403
apply (simp add: dualA_iff A_def, assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   404
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   405
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   406
(* Reduce the sublattice property by using substructural properties*)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   407
(* abandoned see Tarski_4.ML *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   408
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   409
lemma (in CLF) [simp]:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   410
    "f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   411
apply (insert f_cl) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   412
apply (simp add: CLF_def) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   413
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   414
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   415
declare (in CLF) f_cl [simp]
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   416
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   417
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   418
lemma (in CLF) f_in_funcset: "f \<in> A funcset A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   419
by (simp add: A_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   420
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   421
lemma (in CLF) monotone_f: "monotone f A r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   422
by (simp add: A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   423
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   424
lemma (in CLF) CLF_dual: "(cl,f) \<in> CLF ==> (dual cl, f) \<in> CLF"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   425
apply (simp add: CLF_def  CL_dualCL monotone_dual)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   426
apply (simp add: dualA_iff)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   427
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   428
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   429
(* fixed points *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   430
lemma fix_subset: "fix f A <= A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   431
by (simp add: fix_def, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   432
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   433
lemma fix_imp_eq: "x \<in> fix f A ==> f x = x"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   434
by (simp add: fix_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   435
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   436
lemma fixf_subset:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   437
     "[| A <= B; x \<in> fix (%y: A. f y) A |] ==> x \<in> fix f B"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   438
apply (simp add: fix_def, auto) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   439
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   440
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   441
(* lemmas for Tarski, lub *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   442
lemma (in CLF) lubH_le_flubH:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   443
     "H = {x. (x, f x) \<in> r & x \<in> A} ==> (lub H cl, f (lub H cl)) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   444
apply (rule lub_least, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   445
apply (rule f_in_funcset [THEN funcset_mem])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   446
apply (rule lub_in_lattice, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   447
(* \<forall>x:H. (x, f (lub H r)) \<in> r *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   448
apply (rule ballI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   449
apply (rule transE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   450
apply (rule CO_trans)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   451
(* instantiates (x, ???z) \<in> cl.<r> to (x, f x), because of the def of H *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   452
apply fast
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   453
(* so it remains to show (f x, f (lub H cl)) \<in> r *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   454
apply (rule_tac f = "f" in monotoneE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   455
apply (rule monotone_f, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   456
apply (rule lub_in_lattice, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   457
apply (rule lub_upper, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   458
apply assumption
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   459
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   460
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   461
lemma (in CLF) flubH_le_lubH:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   462
     "[|  H = {x. (x, f x) \<in> r & x \<in> A} |] ==> (f (lub H cl), lub H cl) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   463
apply (rule lub_upper, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   464
apply (rule_tac t = "H" in ssubst, assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   465
apply (rule CollectI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   466
apply (rule conjI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   467
apply (rule_tac [2] f_in_funcset [THEN funcset_mem])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   468
apply (rule_tac [2] lub_in_lattice)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   469
prefer 2 apply fast
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   470
apply (rule_tac f = "f" in monotoneE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   471
apply (rule monotone_f)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   472
  apply (blast intro: lub_in_lattice) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   473
 apply (blast intro: lub_in_lattice f_in_funcset [THEN funcset_mem]) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   474
apply (simp add: lubH_le_flubH)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   475
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   476
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   477
lemma (in CLF) lubH_is_fixp:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   478
     "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   479
apply (simp add: fix_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   480
apply (rule conjI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   481
apply (rule lub_in_lattice, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   482
apply (rule antisymE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   483
apply (rule CO_antisym)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   484
apply (simp add: flubH_le_lubH)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   485
apply (simp add: lubH_le_flubH)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   486
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   487
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   488
lemma (in CLF) fix_in_H:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   489
     "[| H = {x. (x, f x) \<in> r & x \<in> A};  x \<in> P |] ==> x \<in> H"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   490
by (simp add: P_def fix_imp_eq [of _ f A] reflE CO_refl 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   491
                    fix_subset [of f A, THEN subsetD]) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   492
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   493
lemma (in CLF) fixf_le_lubH:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   494
     "H = {x. (x, f x) \<in> r & x \<in> A} ==> \<forall>x \<in> fix f A. (x, lub H cl) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   495
apply (rule ballI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   496
apply (rule lub_upper, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   497
apply (rule fix_in_H)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   498
apply (simp_all add: P_def) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   499
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   500
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   501
lemma (in CLF) lubH_least_fixf:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   502
     "H = {x. (x, f x) \<in> r & x \<in> A} 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   503
      ==> \<forall>L. (\<forall>y \<in> fix f A. (y,L) \<in> r) --> (lub H cl, L) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   504
apply (rule allI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   505
apply (rule impI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   506
apply (erule bspec)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   507
apply (rule lubH_is_fixp, assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   508
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   509
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   510
(* Tarski fixpoint theorem 1, first part *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   511
lemma (in CLF) T_thm_1_lub: "lub P cl = lub {x. (x, f x) \<in> r & x \<in> A} cl"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   512
apply (rule sym)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   513
apply (simp add: P_def) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   514
apply (rule lubI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   515
apply (rule fix_subset)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   516
apply (rule lub_in_lattice, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   517
apply (simp add: fixf_le_lubH)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   518
apply (simp add: lubH_least_fixf)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   519
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   520
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   521
(* Tarski for glb *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   522
lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \<in> r & x \<in> A} ==> glb H cl \<in> P"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   523
apply (simp add: glb_dual_lub P_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   524
apply (rule dualA_iff [THEN subst])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   525
apply (rule Tarski.lubH_is_fixp)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   526
apply (rule dualPO) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   527
apply (rule CL_dualCL)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   528
apply (rule f_cl [THEN CLF_dual])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   529
apply (simp add: dualr_iff dualA_iff)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   530
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   531
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   532
lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   533
apply (simp add: glb_dual_lub P_def A_def r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   534
apply (rule dualA_iff [THEN subst])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   535
apply (simp add: Tarski.T_thm_1_lub [of _ f, OF dualPO CL_dualCL] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   536
                 dualPO CL_dualCL CLF_dual dualr_iff)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   537
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   538
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   539
(* interval *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   540
lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   541
apply (insert CO_refl) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   542
apply (simp add: refl_def, blast) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   543
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   544
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   545
lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b <= A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   546
apply (simp add: interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   547
apply (blast intro: rel_imp_elem)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   548
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   549
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   550
lemma (in CLF) intervalI:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   551
     "[| (a, x) \<in> r; (x, b) \<in> r |] ==> x \<in> interval r a b"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   552
apply (simp add: interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   553
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   554
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   555
lemma (in CLF) interval_lemma1:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   556
     "[| S <= interval r a b; x \<in> S |] ==> (a, x) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   557
apply (unfold interval_def, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   558
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   559
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   560
lemma (in CLF) interval_lemma2:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   561
     "[| S <= interval r a b; x \<in> S |] ==> (x, b) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   562
apply (unfold interval_def, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   563
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   564
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   565
lemma (in CLF) a_less_lub:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   566
     "[| S <= A; S \<noteq> {}; 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   567
         \<forall>x \<in> S. (a,x) \<in> r; \<forall>y \<in> S. (y, L) \<in> r |] ==> (a,L) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   568
by (blast intro: transE PO_imp_trans)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   569
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   570
lemma (in CLF) glb_less_b:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   571
     "[| S <= A; S \<noteq> {}; 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   572
         \<forall>x \<in> S. (x,b) \<in> r; \<forall>y \<in> S. (G, y) \<in> r |] ==> (G,b) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   573
by (blast intro: transE PO_imp_trans)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   574
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   575
lemma (in CLF) S_intv_cl:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   576
     "[| a \<in> A; b \<in> A; S <= interval r a b |]==> S <= A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   577
by (simp add: subset_trans [OF _ interval_subset])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   578
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   579
lemma (in CLF) L_in_interval:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   580
     "[| a \<in> A; b \<in> A; S <= interval r a b;  
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   581
         S \<noteq> {}; isLub S cl L; interval r a b \<noteq> {} |] ==> L \<in> interval r a b"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   582
apply (rule intervalI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   583
apply (rule a_less_lub)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   584
prefer 2 apply assumption
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   585
apply (simp add: S_intv_cl)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   586
apply (rule ballI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   587
apply (simp add: interval_lemma1)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   588
apply (simp add: isLub_upper)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   589
(* (L, b) \<in> r *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   590
apply (simp add: isLub_least interval_lemma2)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   591
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   592
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   593
lemma (in CLF) G_in_interval:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   594
     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S <= interval r a b; isGlb S cl G;
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   595
         S \<noteq> {} |] ==> G \<in> interval r a b"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   596
apply (simp add: interval_dual)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   597
apply (simp add: Tarski.L_in_interval [of _ f] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   598
                 dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   599
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   600
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   601
lemma (in CLF) intervalPO:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   602
     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   603
      ==> (| pset = interval r a b, order = induced (interval r a b) r |)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   604
          \<in> PartialOrder"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   605
apply (rule po_subset_po)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   606
apply (simp add: interval_subset)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   607
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   608
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   609
lemma (in CLF) intv_CL_lub:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   610
 "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   611
  ==> \<forall>S. S <= interval r a b --> 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   612
          (\<exists>L. isLub S (| pset = interval r a b, 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   613
                          order = induced (interval r a b) r |)  L)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   614
apply (intro strip)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   615
apply (frule S_intv_cl [THEN CL_imp_ex_isLub])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   616
prefer 2 apply assumption
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   617
apply assumption
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   618
apply (erule exE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   619
(* define the lub for the interval as *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   620
apply (rule_tac x = "if S = {} then a else L" in exI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   621
apply (simp (no_asm_simp) add: isLub_def split del: split_if)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   622
apply (intro impI conjI) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   623
(* (if S = {} then a else L) \<in> interval r a b *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   624
apply (simp add: CL_imp_PO L_in_interval)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   625
apply (simp add: left_in_interval)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   626
(* lub prop 1 *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   627
apply (case_tac "S = {}")
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   628
(* S = {}, y \<in> S = False => everything *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   629
apply fast
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   630
(* S \<noteq> {} *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   631
apply simp
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   632
(* \<forall>y:S. (y, L) \<in> induced (interval r a b) r *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   633
apply (rule ballI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   634
apply (simp add: induced_def  L_in_interval)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   635
apply (rule conjI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   636
apply (rule subsetD)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   637
apply (simp add: S_intv_cl, assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   638
apply (simp add: isLub_upper)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   639
(* \<forall>z:interval r a b. (\<forall>y:S. (y, z) \<in> induced (interval r a b) r -->
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   640
      (if S = {} then a else L, z) \<in> induced (interval r a b) r *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   641
apply (rule ballI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   642
apply (rule impI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   643
apply (case_tac "S = {}")
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   644
(* S = {} *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   645
apply simp
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   646
apply (simp add: induced_def  interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   647
apply (rule conjI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   648
apply (rule reflE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   649
apply (rule CO_refl, assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   650
apply (rule interval_not_empty)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   651
apply (rule CO_trans)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   652
apply (simp add: interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   653
(* S \<noteq> {} *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   654
apply simp
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   655
apply (simp add: induced_def  L_in_interval)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   656
apply (rule isLub_least, assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   657
apply (rule subsetD)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   658
prefer 2 apply assumption
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   659
apply (simp add: S_intv_cl, fast)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   660
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   661
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   662
lemmas (in CLF) intv_CL_glb = intv_CL_lub [THEN Rdual]
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   663
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   664
lemma (in CLF) interval_is_sublattice:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   665
     "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   666
        ==> interval r a b <<= cl"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   667
apply (rule sublatticeI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   668
apply (simp add: interval_subset)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   669
apply (rule CompleteLatticeI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   670
apply (simp add: intervalPO)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   671
 apply (simp add: intv_CL_lub)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   672
apply (simp add: intv_CL_glb)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   673
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   674
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   675
lemmas (in CLF) interv_is_compl_latt = 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   676
    interval_is_sublattice [THEN sublattice_imp_CL]
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   677
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   678
(* Top and Bottom *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   679
lemma (in CLF) Top_dual_Bot: "Top cl = Bot (dual cl)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   680
by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   681
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   682
lemma (in CLF) Bot_dual_Top: "Bot cl = Top (dual cl)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   683
by (simp add: Top_def Bot_def least_def greatest_def dualA_iff dualr_iff)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   684
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   685
lemma (in CLF) Bot_in_lattice: "Bot cl \<in> A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   686
apply (simp add: Bot_def least_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   687
apply (rule someI2)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   688
apply (fold A_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   689
apply (erule_tac [2] conjunct1)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   690
apply (rule conjI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   691
apply (rule glb_in_lattice)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   692
apply (rule subset_refl)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   693
apply (fold r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   694
apply (simp add: glb_lower)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   695
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   696
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   697
lemma (in CLF) Top_in_lattice: "Top cl \<in> A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   698
apply (simp add: Top_dual_Bot A_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   699
apply (rule dualA_iff [THEN subst])  
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   700
apply (blast intro!: Tarski.Bot_in_lattice dualPO CL_dualCL CLF_dual f_cl) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   701
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   702
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   703
lemma (in CLF) Top_prop: "x \<in> A ==> (x, Top cl) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   704
apply (simp add: Top_def greatest_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   705
apply (rule someI2)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   706
apply (fold r_def  A_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   707
prefer 2 apply fast
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   708
apply (intro conjI ballI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   709
apply (rule_tac [2] lub_upper)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   710
apply (auto simp add: lub_in_lattice)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   711
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   712
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   713
lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   714
apply (simp add: Bot_dual_Top r_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   715
apply (rule dualr_iff [THEN subst])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   716
apply (simp add: Tarski.Top_prop [of _ f] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   717
                 dualA_iff A_def dualPO CL_dualCL CLF_dual)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   718
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   719
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   720
lemma (in CLF) Top_intv_not_empty: "x \<in> A  ==> interval r x (Top cl) \<noteq> {}"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   721
apply (rule notI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   722
apply (drule_tac a = "Top cl" in equals0D)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   723
apply (simp add: interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   724
apply (simp add: refl_def Top_in_lattice Top_prop)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   725
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   726
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   727
lemma (in CLF) Bot_intv_not_empty: "x \<in> A ==> interval r (Bot cl) x \<noteq> {}"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   728
apply (simp add: Bot_dual_Top)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   729
apply (subst interval_dual)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   730
prefer 2 apply assumption
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   731
apply (simp add: A_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   732
apply (rule dualA_iff [THEN subst])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   733
apply (blast intro!: Tarski.Top_in_lattice
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   734
                 f_cl dualPO CL_dualCL CLF_dual)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   735
apply (simp add: Tarski.Top_intv_not_empty [of _ f] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   736
                 dualA_iff A_def dualPO CL_dualCL CLF_dual)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   737
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   738
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   739
(* fixed points form a partial order *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   740
lemma (in CLF) fixf_po: "(| pset = P, order = induced P r|) \<in> PartialOrder"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   741
by (simp add: P_def fix_subset po_subset_po)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   742
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   743
lemma (in Tarski) Y_subset_A: "Y <= A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   744
apply (rule subset_trans [OF _ fix_subset])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   745
apply (rule Y_ss [simplified P_def])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   746
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   747
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   748
lemma (in Tarski) lubY_in_A: "lub Y cl \<in> A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   749
by (simp add: Y_subset_A [THEN lub_in_lattice])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   750
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   751
lemma (in Tarski) lubY_le_flubY: "(lub Y cl, f (lub Y cl)) \<in> r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   752
apply (rule lub_least)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   753
apply (rule Y_subset_A)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   754
apply (rule f_in_funcset [THEN funcset_mem])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   755
apply (rule lubY_in_A)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   756
(* Y <= P ==> f x = x *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   757
apply (rule ballI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   758
apply (rule_tac t = "x" in fix_imp_eq [THEN subst])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   759
apply (erule Y_ss [simplified P_def, THEN subsetD])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   760
(* reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r by monotonicity *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   761
apply (rule_tac f = "f" in monotoneE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   762
apply (rule monotone_f)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   763
apply (simp add: Y_subset_A [THEN subsetD])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   764
apply (rule lubY_in_A)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   765
apply (simp add: lub_upper Y_subset_A)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   766
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   767
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   768
lemma (in Tarski) intY1_subset: "intY1 <= A"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   769
apply (unfold intY1_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   770
apply (rule interval_subset)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   771
apply (rule lubY_in_A)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   772
apply (rule Top_in_lattice)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   773
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   774
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   775
lemmas (in Tarski) intY1_elem = intY1_subset [THEN subsetD]
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   776
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   777
lemma (in Tarski) intY1_f_closed: "x \<in> intY1 \<Longrightarrow> f x \<in> intY1"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   778
apply (simp add: intY1_def  interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   779
apply (rule conjI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   780
apply (rule transE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   781
apply (rule CO_trans)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   782
apply (rule lubY_le_flubY)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   783
(* (f (lub Y cl), f x) \<in> r *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   784
apply (rule_tac f=f in monotoneE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   785
apply (rule monotone_f)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   786
apply (rule lubY_in_A)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   787
apply (simp add: intY1_def interval_def  intY1_elem)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   788
apply (simp add: intY1_def  interval_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   789
(* (f x, Top cl) \<in> r *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   790
apply (rule Top_prop)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   791
apply (rule f_in_funcset [THEN funcset_mem])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   792
apply (simp add: intY1_def interval_def  intY1_elem)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   793
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   794
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   795
lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 funcset intY1"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   796
apply (rule restrictI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   797
apply (erule intY1_f_closed)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   798
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   799
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   800
lemma (in Tarski) intY1_mono:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   801
     "monotone (%x: intY1. f x) intY1 (induced intY1 r)"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   802
apply (auto simp add: monotone_def induced_def intY1_f_closed)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   803
apply (blast intro: intY1_elem monotone_f [THEN monotoneE])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   804
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   805
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   806
lemma (in Tarski) intY1_is_cl: 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   807
    "(| pset = intY1, order = induced intY1 r |) \<in> CompleteLattice"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   808
apply (unfold intY1_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   809
apply (rule interv_is_compl_latt)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   810
apply (rule lubY_in_A)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   811
apply (rule Top_in_lattice)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   812
apply (rule Top_intv_not_empty)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   813
apply (rule lubY_in_A)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   814
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   815
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   816
lemma (in Tarski) v_in_P: "v \<in> P"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   817
apply (unfold P_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   818
apply (rule_tac A = "intY1" in fixf_subset)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   819
apply (rule intY1_subset)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   820
apply (simp add: Tarski.glbH_is_fixp [OF _ intY1_is_cl, simplified]
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   821
                 v_def CL_imp_PO intY1_is_cl CLF_def intY1_func intY1_mono)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   822
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   823
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   824
lemma (in Tarski) z_in_interval: 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   825
     "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] ==> z \<in> intY1"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   826
apply (unfold intY1_def P_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   827
apply (rule intervalI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   828
prefer 2 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   829
 apply (erule fix_subset [THEN subsetD, THEN Top_prop])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   830
apply (rule lub_least)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   831
apply (rule Y_subset_A)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   832
apply (fast elim!: fix_subset [THEN subsetD])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   833
apply (simp add: induced_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   834
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   835
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   836
lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   837
      ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   838
apply (simp add: induced_def  intY1_f_closed z_in_interval P_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   839
apply (simp add: fix_imp_eq [of _ f A] fix_subset [of f A, THEN subsetD] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   840
                 CO_refl [THEN reflE])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   841
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   842
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   843
lemma (in Tarski) tarski_full_lemma:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   844
     "\<exists>L. isLub Y (| pset = P, order = induced P r |) L"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   845
apply (rule_tac x = "v" in exI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   846
apply (simp add: isLub_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   847
(* v \<in> P *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   848
apply (simp add: v_in_P)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   849
apply (rule conjI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   850
(* v is lub *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   851
(*  1. \<forall>y:Y. (y, v) \<in> induced P r *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   852
apply (rule ballI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   853
apply (simp add: induced_def subsetD v_in_P)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   854
apply (rule conjI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   855
apply (erule Y_ss [THEN subsetD])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   856
apply (rule_tac b = "lub Y cl" in transE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   857
apply (rule CO_trans)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   858
apply (rule lub_upper)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   859
apply (rule Y_subset_A, assumption)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   860
apply (rule_tac b = "Top cl" in interval_imp_mem)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   861
apply (simp add: v_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   862
apply (fold intY1_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   863
apply (rule Tarski.glb_in_lattice [OF _ intY1_is_cl, simplified])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   864
 apply (simp add: CL_imp_PO intY1_is_cl, force)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   865
(* v is LEAST ub *)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   866
apply clarify
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   867
apply (rule indI)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   868
  prefer 3 apply assumption
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   869
 prefer 2 apply (simp add: v_in_P)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   870
apply (unfold v_def)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   871
apply (rule indE)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   872
apply (rule_tac [2] intY1_subset)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   873
apply (rule Tarski.glb_lower [OF _ intY1_is_cl, simplified])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   874
  apply (simp add: CL_imp_PO intY1_is_cl) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   875
 apply force
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   876
apply (simp add: induced_def intY1_f_closed z_in_interval)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   877
apply (simp add: P_def fix_imp_eq [of _ f A] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   878
                 fix_subset [of f A, THEN subsetD] 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   879
                 CO_refl [THEN reflE])
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   880
done
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   881
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   882
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   883
lemma CompleteLatticeI_simp:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   884
     "[| (| pset = A, order = r |) \<in> PartialOrder; 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   885
         \<forall>S. S <= A --> (\<exists>L. isLub S (| pset = A, order = r |)  L) |]  
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   886
    ==> (| pset = A, order = r |) \<in> CompleteLattice"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   887
by (simp add: CompleteLatticeI Rdual)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   888
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   889
theorem (in CLF) Tarski_full:
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   890
     "(| pset = P, order = induced P r|) \<in> CompleteLattice"
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   891
apply (rule CompleteLatticeI_simp)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   892
apply (rule fixf_po, clarify)
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   893
apply (simp add: P_def A_def r_def) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   894
apply (blast intro!: Tarski.tarski_full_lemma cl_po cl_co f_cl) 
0a6fbdedcde2 Tidied and converted to Isar by lcp
paulson
parents: 12459
diff changeset
   895
done
7112
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   896
b142788d79e8 back again, supposedly with correct perms;
wenzelm
parents:
diff changeset
   897
end