src/HOL/ex/Tarski.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9969 4753185f1dd2
child 10797 028d22926a41
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7085
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
     1
(*  Title:      HOL/ex/Tarski
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
     2
    ID:         $Id$
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
     3
    Author:     Florian Kammueller, Cambridge University Computer Laboratory
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
     5
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
     6
Minimal version of lattice theory plus the full theorem of Tarski:
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
     7
   The fixedpoints of a complete lattice themselves form a complete lattice.
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
     8
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
     9
Illustrates first-class theories, using the Sigma representation of structures
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    10
*)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    11
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    12
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    13
(* abbreviate commonly used tactic application *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    14
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    15
fun afs thms = (asm_full_simp_tac (simpset() addsimps thms));
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    16
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    17
(* Partial Order *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    18
Open_locale "PO";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    19
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    20
val simp_PO = simplify (simpset() addsimps [PartialOrder_def]) (thm "cl_po");
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    21
Addsimps [simp_PO, thm "cl_po"];
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    22
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    23
val PO_simp = [thm "A_def", thm "r_def"];
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    24
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    25
Goal "refl A r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    26
by (simp_tac (simpset() addsimps PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    27
qed "PartialOrderE1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    28
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    29
Goal "antisym r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    30
by (simp_tac (simpset() addsimps PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    31
qed "PartialOrderE2";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    32
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    33
Goal "trans r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    34
by (simp_tac (simpset() addsimps PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    35
qed "PartialOrderE3";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    36
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    37
Goal "[| refl A r; x: A|] ==> (x, x): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    38
by (afs [refl_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    39
qed "reflE";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    40
(* Interesting: A and r don't get bound because the proof doesn't use
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    41
   locale rules 
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    42
val reflE = "[| refl ?A ?r; ?x : ?A |] ==> (?x, ?x) : ?r" *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    43
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    44
Goal "[| antisym r; (a, b): r; (b, a): r |] ==> a = b";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    45
by (afs [antisym_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    46
qed "antisymE";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    47
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    48
Goalw [trans_def] "[| trans r; (a, b): r; (b, c): r|] ==> (a,c): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    49
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    50
qed "transE";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    51
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    52
Goal "[| monotone f A r;  x: A; y: A; (x, y): r |] ==> (f x, f y): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    53
by (afs [monotone_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    54
qed "monotoneE";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    55
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    56
Goal "S <= A ==> (| pset = S, order = induced S r |): PartialOrder";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    57
by (simp_tac (simpset() addsimps [PartialOrder_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    58
by (Step_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    59
(* refl *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    60
by (afs [refl_def,induced_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    61
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    62
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    63
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    64
by (rtac reflE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    65
by (rtac PartialOrderE1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    66
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    67
(* antisym *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    68
by (afs [antisym_def,induced_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    69
by (Step_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    70
by (rtac antisymE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    71
by (assume_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    72
by (assume_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    73
by (rtac PartialOrderE2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    74
(* trans *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    75
by (afs [trans_def,induced_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    76
by (Step_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    77
by (rtac transE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    78
by (assume_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    79
by (assume_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    80
by (rtac PartialOrderE3 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    81
qed "po_subset_po";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    82
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    83
Goal "[| (x, y): induced S r; S <= A |] ==> (x, y): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    84
by (afs [induced_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    85
qed "indE";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    86
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    87
Goal "[| (x, y): r; x: S; y: S |] ==> (x, y): induced S r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    88
by (afs [induced_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    89
qed "indI";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    90
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    91
(* with locales *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    92
Open_locale "CL";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    93
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    94
Delsimps [simp_PO, thm "cl_po"];
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    95
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    96
val simp_CL = simplify (simpset() addsimps [CompleteLattice_def]) 
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    97
                       (thm "cl_co");
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    98
Addsimps [simp_CL, thm "cl_co"];
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
    99
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   100
Goalw [Ex_def] "(EX L. islub S cl L) = islub S cl (lub S cl)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   101
by (simp_tac (simpset() addsimps [lub_def, least_def, islub_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   102
qed "islub_lub";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   103
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   104
Goalw [Ex_def] "(EX G. isglb S cl G) = isglb S cl (glb S cl)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   105
by (simp_tac (simpset() addsimps [glb_def, greatest_def, isglb_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   106
qed "isglb_glb";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   107
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   108
Goal "isglb S cl = islub S (dual cl)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   109
by (afs [islub_def,isglb_def,dual_def,converse_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   110
qed "isglb_dual_islub";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   111
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   112
Goal "islub S cl = isglb S (dual cl)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   113
by (afs [islub_def,isglb_def,dual_def,converse_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   114
qed "islub_dual_isglb";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   115
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   116
Goal "dual cl : PartialOrder";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   117
by (simp_tac (simpset() addsimps [PartialOrder_def, dual_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   118
by (afs [simp_PO,refl_converse,trans_converse,antisym_converse] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   119
qed "dualPO";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   120
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   121
Goal "! S. (S <= A -->( ? L. islub S (| pset = A, order = r|) L)) \
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   122
\     ==> ! S. (S <= A --> (? G. isglb S (| pset = A, order = r|) G))";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   123
by (Step_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   124
by (res_inst_tac
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   125
    [("x"," lub {y. y: A & (! k: S. (y, k): r)}(|pset = A, order = r|)")] 
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   126
    exI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   127
by (dres_inst_tac [("x","{y. y: A & (! k: S. (y,k): r)}")] spec 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   128
by (dtac mp 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   129
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   130
by (afs [islub_lub, isglb_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   131
by (afs [islub_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   132
by (Blast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   133
qed "Rdual";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   134
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   135
Goal "lub S cl = glb S (dual cl)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   136
by (afs [lub_def,glb_def,least_def,greatest_def,dual_def,converse_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   137
qed "lub_dual_glb";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   138
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   139
Goal "glb S cl = lub S (dual cl)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   140
by (afs [lub_def,glb_def,least_def,greatest_def,dual_def,converse_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   141
qed "glb_dual_lub";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   142
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   143
Goal "CompleteLattice <= PartialOrder";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   144
by (simp_tac (simpset() addsimps [PartialOrder_def, CompleteLattice_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   145
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   146
qed "CL_subset_PO";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   147
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   148
val CompleteLatticeE1 = CL_subset_PO RS subsetD;
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   149
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   150
Goal "! S.  S <= A --> (? L. islub S cl L)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   151
by (simp_tac (simpset() addsimps PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   152
qed "CompleteLatticeE2";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   153
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   154
Goal "! S.  S <= A --> (? G. isglb S cl G)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   155
by (simp_tac (simpset() addsimps PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   156
qed "CompleteLatticeE3";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   157
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   158
Addsimps [CompleteLatticeE1 RS (export simp_PO)];
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   159
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   160
Goal "refl A r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   161
by (simp_tac (simpset() addsimps PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   162
qed "CompleteLatticeE11";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   163
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   164
Goal "antisym r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   165
by (simp_tac (simpset() addsimps PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   166
qed "CompleteLatticeE12";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   167
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   168
Goal "trans r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   169
by (afs (PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   170
qed "CompleteLatticeE13";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   171
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   172
Goal "[| po : PartialOrder; (! S. S <= po.<A> --> (? L. islub S po L));\
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   173
\  (! S. S <= po.<A> --> (? G. isglb S po G))|] ==> po: CompleteLattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   174
by (afs [CompleteLattice_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   175
qed "CompleteLatticeI";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   176
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   177
Goal "dual cl : CompleteLattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   178
by (simp_tac (simpset() addsimps [CompleteLattice_def,dual_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   179
by (fold_goals_tac [dual_def]);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   180
by (simp_tac (simpset() addsimps [islub_dual_isglb RS sym,
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   181
				  isglb_dual_islub RS sym,
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   182
				  export dualPO]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   183
qed "CL_dualCL";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   184
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   185
Goal "(dual cl.<A>) = cl.<A>";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   186
by (simp_tac (simpset() addsimps [dual_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   187
qed "dualA_iff";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   188
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   189
Goal "((x, y): (dual cl.<r>)) = ((y, x): cl.<r>)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   190
by (simp_tac (simpset() addsimps [dual_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   191
qed "dualr_iff";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   192
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   193
Goal "monotone f (cl.<A>) (cl.<r>) ==> monotone f (dual cl.<A>) (dual cl.<r>)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   194
by (afs [monotone_def,dualA_iff,dualr_iff] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   195
qed "monotone_dual";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   196
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   197
Goal "[| x: A; y: A|] ==> interval r x y = interval (dual cl.<r>) y x";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   198
by (simp_tac (simpset() addsimps [interval_def,dualr_iff]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   199
by (fold_goals_tac [thm "r_def"]);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   200
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   201
qed "interval_dual";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   202
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   203
Goal "[| trans r; interval r a b ~= {} |] ==> (a, b): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   204
by (afs [interval_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   205
by (rewtac trans_def);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   206
by (Blast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   207
qed "interval_not_empty";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   208
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   209
Goal "x: interval r a b ==> (a, x): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   210
by (afs [interval_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   211
qed "intervalE1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   212
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   213
Goal "[| a: A; b: A; interval r a b ~= {} |] ==> a: interval r a b";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   214
by (simp_tac (simpset() addsimps [interval_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   215
by (afs [PartialOrderE3,interval_not_empty] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   216
by (afs [PartialOrderE1 RS reflE] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   217
qed "left_in_interval";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   218
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   219
Goal "[| a: A; b: A; interval r a b ~= {} |] ==> b: interval r a b";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   220
by (simp_tac (simpset() addsimps [interval_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   221
by (afs [PartialOrderE3,interval_not_empty] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   222
by (afs [PartialOrderE1 RS reflE] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   223
qed "right_in_interval";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   224
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   225
Goal "[| (| pset = A, order = r |) : PartialOrder;\
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   226
\        ! S. S <= A --> (? L. islub S (| pset = A, order = r |)  L) |] \
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   227
\   ==> (| pset = A, order = r |) : CompleteLattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   228
by (afs [CompleteLatticeI, Rdual] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   229
qed "CompleteLatticeI_simp";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   230
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   231
(* sublattice *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   232
Goal "S <<= cl ==> S <= A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   233
by (afs [sublattice_def, CompleteLattice_def, thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   234
qed "sublatticeE1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   235
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   236
Goal "S <<= cl  ==> (| pset = S, order = induced S r |) : CompleteLattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   237
by (afs ([sublattice_def, CompleteLattice_def] @ PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   238
qed "sublatticeE2";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   239
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   240
Goal "[| S <= A; (| pset = S, order = induced S r |) : CompleteLattice |] ==> S <<= cl";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   241
by (afs ([sublattice_def] @ PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   242
qed "sublatticeI";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   243
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   244
(* lub *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   245
Goal "[| S <= A; islub S cl x; islub S cl L|] ==> x = L";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   246
by (rtac antisymE 1); 
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   247
by (rtac CompleteLatticeE12 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   248
by (rewtac islub_def);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   249
by (rotate_tac ~1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   250
by (etac conjE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   251
by (dtac conjunct2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   252
by (dtac conjunct1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   253
by (dtac conjunct2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   254
by (rotate_tac ~1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   255
by (dres_inst_tac [("x","L")] bspec 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   256
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   257
by (fold_goals_tac [thm "r_def"]);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   258
by (etac mp 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   259
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   260
(* (L, x) : (cl .<r>) *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   261
by (rotate_tac ~1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   262
by (etac conjE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   263
by (rotate_tac ~1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   264
by (dtac conjunct2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   265
by (dtac bspec 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   266
by (etac conjunct1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   267
by (etac mp 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   268
by (etac (conjunct2 RS conjunct1) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   269
qed "lub_unique";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   270
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   271
Goal "[| S <= A |] ==> ! x: S. (x,lub S cl): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   272
by (rtac exE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   273
by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   274
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   275
by (rewrite_goals_tac [lub_def,least_def]);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 8703
diff changeset
   276
by (stac some_equality 1);
7085
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   277
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   278
by (afs [islub_def] 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   279
by (etac conjunct2 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   280
by (afs [islub_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   281
by (rtac lub_unique 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   282
by (afs [thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   283
by (afs [islub_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   284
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   285
by (afs [islub_def,thm "r_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   286
qed "lubE1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   287
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   288
Goal "[| S <= A; L: A; ! x: S. (x,L): r |] ==> (lub S cl, L): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   289
by (rtac exE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   290
by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   291
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   292
by (rewrite_goals_tac [lub_def,least_def]);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 8703
diff changeset
   293
by (stac some_equality 1);
7085
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   294
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   295
by (afs [islub_def] 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   296
by (etac conjunct2 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   297
by (afs [islub_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   298
by (rtac lub_unique 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   299
by (afs [thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   300
by (afs [islub_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   301
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   302
by (afs [islub_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   303
by (dtac conjunct2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   304
by (dtac conjunct2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   305
by (rotate_tac 3 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   306
by (dtac bspec 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   307
by (fold_goals_tac [thm "r_def"]);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   308
by (etac mp 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   309
by (afs [thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   310
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   311
qed "lubE2";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   312
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   313
Goal "[| S <= A |] ==> lub S cl : A";  
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   314
by (rtac exE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   315
by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   316
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   317
by (rewrite_goals_tac [lub_def,least_def]);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 8703
diff changeset
   318
by (stac some_equality 1);
7085
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   319
by (afs [islub_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   320
by (afs [islub_def, thm "A_def"] 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   321
by (rtac lub_unique 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   322
by (afs [thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   323
by (afs [islub_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   324
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   325
qed "lub_in_lattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   326
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   327
Goal "[| S <= A; L: A; ! x: S. (x,L): r;\
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   328
\ ! z: A. (! y: S. (y,z): r) --> (L,z): r |] ==> L = lub S cl";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   329
by (rtac lub_unique 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   330
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   331
by (afs ([islub_def] @ PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   332
by (rewtac islub_def);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   333
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   334
by (fold_goals_tac PO_simp);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   335
by (rtac lub_in_lattice 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   336
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   337
by (afs [lubE1, lubE2] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   338
qed "lubI";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   339
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   340
Goal "[| S <= A; islub S cl L |] ==> L = lub S cl";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   341
by (afs ([lubI, islub_def] @ PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   342
qed "lubIa";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   343
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   344
Goal "islub S cl L ==> L : A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   345
by (afs [islub_def, thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   346
qed "islub_in_lattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   347
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   348
Goal "islub S cl L ==> ! y: S. (y, L): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   349
by (afs [islub_def, thm "r_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   350
qed "islubE1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   351
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   352
Goal "[| islub S cl L; \
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   353
\      z: A; ! y: S. (y, z): r|] ==> (L, z): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   354
by (afs ([islub_def] @ PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   355
qed "islubE2";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   356
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   357
Goal "[| S <= A |] ==> ? L. islub S cl L";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   358
by (afs [thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   359
qed "islubE";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   360
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   361
Goal "[| L: A; ! y: S. (y, L): r; \
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   362
\     (!z: A. (! y: S. (y, z):r) --> (L, z): r)|] ==> islub S cl L";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   363
by (afs ([islub_def] @ PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   364
qed "islubI";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   365
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   366
(* glb *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   367
Goal "S <= A ==> glb S cl : A";  
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   368
by (stac glb_dual_lub 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   369
by (afs [thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   370
by (rtac (dualA_iff RS subst) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   371
by (rtac (export lub_in_lattice) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   372
by (rtac CL_dualCL 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   373
by (afs [dualA_iff] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   374
qed "glb_in_lattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   375
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   376
Goal "S <= A ==> ! x: S. (glb S cl, x): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   377
by (stac glb_dual_lub 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   378
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   379
by (afs [thm "r_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   380
by (rtac (dualr_iff RS subst) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   381
by (rtac (export lubE1 RS bspec) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   382
by (rtac CL_dualCL 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   383
by (afs [dualA_iff, thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   384
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   385
qed "glbE1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   386
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   387
(* Reduce the sublattice property by using substructural properties! *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   388
(* abandoned see Tarski_4.ML *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   389
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   390
Open_locale "CLF";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   391
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   392
val simp_CLF = simplify (simpset() addsimps [CLF_def]) (thm "f_cl");
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   393
Addsimps [simp_CLF, thm "f_cl"];
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   394
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   395
Goal "f : A funcset A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   396
by (simp_tac (simpset() addsimps [thm "A_def"]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   397
qed "CLF_E1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   398
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   399
Goal "monotone f A r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   400
by (simp_tac (simpset() addsimps PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   401
qed "CLF_E2";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   402
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   403
Goal "f : CLF ^^ {cl} ==> f : CLF ^^ {dual cl}";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   404
by (afs [CLF_def, CL_dualCL, monotone_dual] 1); 
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   405
by (afs [dualA_iff] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   406
qed "CLF_dual";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   407
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   408
(* fixed points *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   409
Goal "P <= A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   410
by (simp_tac (simpset() addsimps [thm "P_def", fix_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   411
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   412
qed "fixfE1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   413
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   414
Goal "x: P ==> f x = x";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   415
by (afs [thm "P_def", fix_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   416
qed "fixfE2";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   417
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   418
Goal "[| A <= B; x: fix (lam y: A. f y) A |] ==> x: fix f B";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   419
by (forward_tac [export fixfE2] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   420
by (dtac ((export fixfE1) RS subsetD) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   421
by (afs [fix_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   422
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   423
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   424
by (res_inst_tac [("P","% y. f x = y")] subst 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   425
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   426
by (rtac sym 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   427
by (etac restrict_apply1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   428
qed "fixf_subset";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   429
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   430
(* lemmas for Tarski, lub *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   431
Goal "H = {x. (x, f x) : r & x : A} ==> (lub H cl, f (lub H cl)) : r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   432
by (rtac lubE2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   433
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   434
by (rtac (CLF_E1 RS funcset_mem) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   435
by (rtac lub_in_lattice 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   436
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   437
(* ! x:H. (x, f (lub H r)) : r *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   438
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   439
by (rtac transE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   440
by (rtac CompleteLatticeE13 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   441
(* instantiates (x, ???z): cl.<r> to (x, f x), because of the def of H *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   442
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   443
(* so it remains to show (f x, f (lub H cl)) : r *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   444
by (res_inst_tac [("f","f")] monotoneE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   445
by (rtac CLF_E2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   446
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   447
by (rtac lub_in_lattice 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   448
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   449
by (rtac (lubE1 RS bspec) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   450
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   451
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   452
qed "lubH_le_flubH";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   453
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   454
Goal "[|  H = {x. (x, f x) : r & x : A} |] ==> (f (lub H cl), lub H cl) : r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   455
by (rtac (lubE1 RS bspec) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   456
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   457
by (res_inst_tac [("t","H")] ssubst 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   458
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   459
by (rtac CollectI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   460
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   461
by (rtac (CLF_E1 RS funcset_mem) 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   462
by (rtac lub_in_lattice 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   463
by (Fast_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   464
by (res_inst_tac [("f","f")] monotoneE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   465
by (rtac CLF_E2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   466
by (afs [lubH_le_flubH] 3);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   467
by (rtac (CLF_E1 RS funcset_mem) 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   468
by (rtac lub_in_lattice 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   469
by (Fast_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   470
by (rtac lub_in_lattice 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   471
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   472
qed "flubH_le_lubH";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   473
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   474
Goal "H = {x. (x, f x): r & x : A} ==> lub H cl : P";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   475
by (simp_tac (simpset() addsimps [thm "P_def", fix_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   476
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   477
by (rtac lub_in_lattice 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   478
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   479
by (rtac antisymE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   480
by (rtac CompleteLatticeE12 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   481
by (afs [flubH_le_lubH] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   482
by (afs [lubH_le_flubH] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   483
qed "lubH_is_fixp";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   484
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   485
Goal "[| H = {x. (x, f x) : r & x : A};  x: P |] ==> x: H";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   486
by (etac ssubst 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   487
by (Simp_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   488
by (rtac conjI 1);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7085
diff changeset
   489
by (ftac fixfE2 1);
7085
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   490
by (etac ssubst 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   491
by (rtac reflE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   492
by (rtac CompleteLatticeE11 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   493
by (etac (fixfE1 RS subsetD) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   494
by (etac (fixfE1 RS subsetD) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   495
qed "fix_in_H";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   496
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   497
Goal "H = {x. (x, f x) : r & x : A} ==> ! x: P. (x, lub H cl) : r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   498
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   499
by (rtac (lubE1 RS bspec) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   500
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   501
by (rtac fix_in_H 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   502
by (REPEAT (atac 1));
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   503
qed "fixf_le_lubH";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   504
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   505
Goal "H = {x. (x, f x) : r & x : A} ==> ! L. (! y: P. (y,L): r) --> (lub H cl, L): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   506
by (rtac allI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   507
by (rtac impI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   508
by (etac bspec 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   509
by (rtac lubH_is_fixp 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   510
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   511
qed "lubH_least_fixf";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   512
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   513
(* Tarski fixpoint theorem 1, first part *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   514
Goal "lub P cl = lub {x. (x, f x) : r & x : A} cl";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   515
by (rtac sym 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   516
by (rtac lubI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   517
by (rtac fixfE1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   518
by (rtac lub_in_lattice 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   519
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   520
by (afs [fixf_le_lubH] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   521
by (afs [lubH_least_fixf] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   522
qed "T_thm_1_lub";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   523
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   524
(* Tarski for glb *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   525
Goal "H = {x. (f x, x): r & x : A} ==> glb H cl : P";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   526
by (full_simp_tac 
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   527
    (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   528
by (rtac (dualA_iff RS subst) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   529
by (rtac (CL_dualCL RS (export lubH_is_fixp)) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   530
by (rtac (thm "f_cl" RS CLF_dual) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   531
by (afs [dualr_iff, dualA_iff] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   532
qed "glbH_is_fixp";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   533
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   534
Goal "glb P cl = glb {x. (f x, x): r & x : A} cl";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   535
by (simp_tac (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   536
by (rtac (dualA_iff RS subst) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   537
by (rtac (CL_dualCL RS (export T_thm_1_lub) RS ssubst) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   538
by (rtac (thm "f_cl" RS CLF_dual) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   539
by (afs [dualr_iff] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   540
qed "T_thm_1_glb";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   541
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   542
(* interval *)
8703
816d8f6513be Times -> <*>
nipkow
parents: 7499
diff changeset
   543
Goal "refl A r ==> r <= A <*> A";
7085
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   544
by (afs [refl_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   545
qed "reflE1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   546
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   547
Goal "(x, y): r ==> x: A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   548
by (rtac SigmaD1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   549
by (rtac (reflE1 RS subsetD) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   550
by (rtac CompleteLatticeE11 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   551
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   552
qed "rel_imp_elem";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   553
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   554
Goal "[| a: A; b: A |] ==> interval r a b <= A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   555
by (simp_tac (simpset() addsimps [interval_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   556
by (rtac subsetI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   557
by (rtac rel_imp_elem 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   558
by (dtac CollectD 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   559
by (etac conjunct2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   560
qed "interval_subset";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   561
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   562
Goal "[| (a, x): r; (x, b): r |] ==> x: interval r a b";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   563
by (afs [interval_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   564
qed "intervalI";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   565
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   566
Goalw [interval_def] "[| S <= interval r a b; x: S |] ==> (a, x): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   567
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   568
qed "interval_lemma1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   569
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   570
Goalw [interval_def] "[| S <= interval r a b; x: S |] ==> (x, b): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   571
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   572
qed "interval_lemma2";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   573
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   574
Goal "[| S <= A; S ~= {};\
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   575
\        ! x: S. (a,x): r; ! y: S. (y, L): r |] ==> (a,L): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   576
by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   577
qed "a_less_lub";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   578
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   579
Goal "[| S <= A; S ~= {};\
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   580
\        ! x: S. (x,b): r; ! y: S. (G, y): r |] ==> (G,b): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   581
by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   582
qed "glb_less_b";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   583
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   584
Goal "[| a : A; b : A; S <= interval r a b |]==> S <= A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   585
by (afs [interval_subset RSN(2, subset_trans)] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   586
qed "S_intv_cl";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   587
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   588
Goal "[| a : A; b: A; S <= interval r a b; \
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   589
\      S ~= {}; islub S cl L; interval r a b ~= {} |] ==> L : interval r a b";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   590
by (rtac intervalI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   591
by (rtac a_less_lub 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   592
by (assume_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   593
by (afs [S_intv_cl] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   594
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   595
by (afs [interval_lemma1] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   596
by (afs [islubE1] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   597
(* (L, b) : r *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   598
by (rtac islubE2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   599
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   600
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   601
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   602
by (afs [interval_lemma2] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   603
qed "L_in_interval";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   604
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   605
Goal "[| a : A; b : A; interval r a b ~= {}; S <= interval r a b; isglb S cl G; \
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   606
\      S ~= {} |]   ==> G : interval r a b";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   607
by (afs [interval_dual] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   608
by (rtac (export L_in_interval) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   609
by (rtac dualPO 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   610
by (afs [dualA_iff, thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   611
by (afs [dualA_iff, thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   612
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   613
by (afs [isglb_dual_islub] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   614
by (afs [isglb_dual_islub] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   615
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   616
qed "G_in_interval";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   617
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   618
Goal "[| a: A; b: A; interval r a b ~= {} |]\
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   619
\  ==> (| pset = interval r a b, order = induced (interval r a b) r |) : PartialOrder";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   620
by (rtac po_subset_po 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   621
by (afs [interval_subset] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   622
qed "intervalPO";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   623
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   624
Goal "[| a : A; b : A;\
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   625
\   interval r a b ~= {} |] ==> ! S. S <= interval r a b -->\
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   626
\         (? L. islub S (| pset = interval r a b, order = induced (interval r a b) r |)  L)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   627
by (strip_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   628
by (forward_tac [S_intv_cl RS islubE] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   629
by (assume_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   630
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   631
by (etac exE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   632
(* define the lub for the interval as: *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   633
by (res_inst_tac [("x","if S = {} then a else L")] exI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   634
by (rtac (export islubI) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   635
(* (if S = {} then a else L) : interval r a b *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   636
by (asm_full_simp_tac
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   637
    (simpset() addsimps [CompleteLatticeE1,L_in_interval]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   638
by (afs [left_in_interval] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   639
(* lub prop 1 *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   640
by (case_tac "S = {}" 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   641
(* S = {}, y: S = False => everything *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   642
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   643
(* S ~= {} *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   644
by (Asm_full_simp_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   645
(* ! y:S. (y, L) : induced (interval r a b) r *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   646
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   647
by (afs [induced_def, L_in_interval] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   648
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   649
by (rtac subsetD 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   650
by (afs [S_intv_cl] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   651
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   652
by (afs [islubE1] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   653
(* ! z:interval r a b. (! y:S. (y, z) : induced (interval r a b) r -->
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   654
      (if S = {} then a else L, z) : induced (interval r a b) r *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   655
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   656
by (rtac impI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   657
by (case_tac "S = {}" 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   658
(* S = {} *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   659
by (Asm_full_simp_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   660
by (afs [induced_def, interval_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   661
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   662
by (rtac reflE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   663
by (rtac CompleteLatticeE11 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   664
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   665
by (rtac interval_not_empty 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   666
by (rtac CompleteLatticeE13 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   667
by (afs [interval_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   668
(* S ~= {} *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   669
by (Asm_full_simp_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   670
by (afs [induced_def, L_in_interval] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   671
by (rtac islubE2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   672
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   673
by (rtac subsetD 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   674
by (assume_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   675
by (afs [S_intv_cl] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   676
by (Fast_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   677
qed "intv_CL_lub";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   678
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   679
val intv_CL_glb = intv_CL_lub RS Rdual;
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   680
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   681
Goal "[| a: A; b: A; interval r a b ~= {} |]\
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   682
\       ==> interval r a b <<= cl";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   683
by (rtac sublatticeI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   684
by (afs [interval_subset] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   685
by (rtac CompleteLatticeI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   686
by (afs [intervalPO] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   687
by (afs [intv_CL_lub] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   688
by (afs [intv_CL_glb] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   689
qed "interval_is_sublattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   690
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   691
val interv_is_compl_latt = interval_is_sublattice RS sublatticeE2;
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   692
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   693
(* Top and Bottom *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   694
Goal "Top cl = Bot (dual cl)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   695
by (afs [Top_def,Bot_def,least_def,greatest_def,dualA_iff, dualr_iff] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   696
qed "Top_dual_Bot";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   697
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   698
Goal "Bot cl = Top (dual cl)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   699
by (afs [Top_def,Bot_def,least_def,greatest_def,dualA_iff, dualr_iff] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   700
qed "Bot_dual_Top";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   701
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   702
Goal "Bot cl: A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   703
by (simp_tac (simpset() addsimps [Bot_def,least_def]) 1);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 8703
diff changeset
   704
by (rtac someI2 1);
7085
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   705
by (fold_goals_tac [thm "A_def"]);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   706
by (etac conjunct1 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   707
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   708
by (rtac glb_in_lattice 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   709
by (rtac subset_refl 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   710
by (fold_goals_tac [thm "r_def"]);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   711
by (afs [glbE1] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   712
qed "Bot_in_lattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   713
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   714
Goal "Top cl: A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   715
by (simp_tac (simpset() addsimps [Top_dual_Bot, thm "A_def"]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   716
by (rtac (dualA_iff RS subst) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   717
by (afs [export Bot_in_lattice,CL_dualCL] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   718
qed "Top_in_lattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   719
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   720
Goal "x: A ==> (x, Top cl): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   721
by (simp_tac (simpset() addsimps [Top_def,greatest_def]) 1);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 8703
diff changeset
   722
by (rtac someI2 1);
7085
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   723
by (fold_goals_tac [thm "r_def", thm "A_def"]);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   724
by (Fast_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   725
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   726
by (rtac lubE1 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   727
by (afs [lub_in_lattice] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   728
by (rtac subset_refl 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   729
qed "Top_prop";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   730
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   731
Goal "x: A ==> (Bot cl, x): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   732
by (simp_tac (simpset() addsimps [Bot_dual_Top, thm "r_def"]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   733
by (rtac (dualr_iff RS subst) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   734
by (rtac (export Top_prop) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   735
by (rtac CL_dualCL 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   736
by (afs [dualA_iff, thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   737
qed "Bot_prop";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   738
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   739
Goal "x: A  ==> interval r x (Top cl) ~= {}";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   740
by (rtac notI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   741
by (dres_inst_tac [("a","Top cl")] equals0D 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   742
by (afs [interval_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   743
by (afs [refl_def,Top_in_lattice,Top_prop] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   744
qed "Top_intv_not_empty";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   745
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   746
Goal "x: A ==> interval r (Bot cl) x ~= {}";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   747
by (simp_tac (simpset() addsimps [Bot_dual_Top]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   748
by (stac interval_dual 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   749
by (assume_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   750
by (afs [thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   751
by (rtac (dualA_iff RS subst) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   752
by (rtac (export Top_in_lattice) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   753
by (rtac CL_dualCL 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   754
by (afs [export Top_intv_not_empty,CL_dualCL,dualA_iff, thm "A_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   755
qed "Bot_intv_not_empty";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   756
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   757
(* fixed points form a partial order *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   758
Goal "(| pset = P, order = induced P r|) : PartialOrder";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   759
by (rtac po_subset_po 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   760
by (rtac fixfE1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   761
qed "fixf_po";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   762
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   763
Open_locale "Tarski";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   764
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   765
Goal "Y <= A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   766
by (rtac (fixfE1 RSN(2,subset_trans)) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   767
by (rtac (thm "Y_ss") 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   768
qed "Y_subset_A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   769
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   770
Goal "lub Y cl : A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   771
by (afs [Y_subset_A RS lub_in_lattice] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   772
qed "lubY_in_A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   773
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   774
Goal "(lub Y cl, f (lub Y cl)): r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   775
by (rtac lubE2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   776
by (rtac Y_subset_A 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   777
by (rtac (CLF_E1 RS funcset_mem) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   778
by (rtac lubY_in_A 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   779
(* Y <= P ==> f x = x *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   780
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   781
by (res_inst_tac [("t","x")] (fixfE2 RS subst) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   782
by (etac (thm "Y_ss" RS subsetD) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   783
(* reduce (f x, f (lub Y cl)) : r to (x, lub Y cl): r by monotonicity *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   784
by (res_inst_tac [("f","f")] monotoneE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   785
by (rtac CLF_E2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   786
by (afs [Y_subset_A RS subsetD] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   787
by (rtac lubY_in_A 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   788
by (afs [lubE1, Y_subset_A] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   789
qed "lubY_le_flubY";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   790
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   791
Goalw [thm "intY1_def"] "intY1 <= A";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   792
by (rtac interval_subset 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   793
by (rtac lubY_in_A 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   794
by (rtac Top_in_lattice 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   795
qed "intY1_subset";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   796
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   797
val intY1_elem = intY1_subset RS subsetD;
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   798
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   799
Goal "(lam x: intY1. f x): intY1 funcset intY1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   800
by (rtac restrictI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   801
by (afs [thm "intY1_def", interval_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   802
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   803
by (rtac transE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   804
by (rtac CompleteLatticeE13 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   805
by (rtac lubY_le_flubY 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   806
(* (f (lub Y cl), f x) : r *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   807
by (res_inst_tac [("f","f")]monotoneE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   808
by (rtac CLF_E2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   809
by (rtac lubY_in_A 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   810
by (afs [thm "intY1_def",interval_def, intY1_elem] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   811
by (afs [thm "intY1_def", interval_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   812
(* (f x, Top cl) : r *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   813
by (rtac Top_prop 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   814
by (rtac (CLF_E1 RS funcset_mem) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   815
by (afs [thm "intY1_def",interval_def, intY1_elem] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   816
qed "intY1_func";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   817
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   818
Goal "monotone (lam x: intY1. f x) intY1 (induced intY1 r)";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   819
by (simp_tac (simpset() addsimps [monotone_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   820
by (Clarify_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   821
by (simp_tac (simpset() addsimps [induced_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   822
by (afs [intY1_func RS funcset_mem] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   823
by (afs [restrict_apply1] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   824
by (res_inst_tac [("f","f")] monotoneE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   825
by (rtac CLF_E2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   826
by (etac (intY1_subset RS subsetD) 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   827
by (etac (intY1_subset RS subsetD) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   828
by (afs [induced_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   829
qed "intY1_mono";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   830
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   831
Goalw [thm "intY1_def"]
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   832
    "(| pset = intY1, order = induced intY1 r |): CompleteLattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   833
by (rtac interv_is_compl_latt 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   834
by (rtac lubY_in_A 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   835
by (rtac Top_in_lattice 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   836
by (rtac Top_intv_not_empty 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   837
by (rtac lubY_in_A 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   838
qed "intY1_is_cl";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   839
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   840
Goalw  [thm "P_def"] "v : P";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   841
by (res_inst_tac [("A","intY1")] fixf_subset 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   842
by (rtac intY1_subset 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   843
by (rewrite_goals_tac [thm "v_def"]);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   844
by (rtac (simplify (simpset()) (intY1_is_cl RS export glbH_is_fixp)) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   845
by (afs [CLF_def, intY1_is_cl, intY1_func, intY1_mono] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   846
by (Simp_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   847
qed "v_in_P";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   848
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   849
Goalw [thm "intY1_def"]
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   850
     "[| z : P; ! y:Y. (y, z) : induced P r |] ==> z : intY1";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   851
by (rtac intervalI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   852
by (etac (fixfE1 RS subsetD RS Top_prop) 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   853
by (rtac lubE2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   854
by (rtac Y_subset_A 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   855
by (fast_tac (claset() addSEs [fixfE1 RS subsetD]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   856
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   857
by (dtac bspec 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   858
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   859
by (afs [induced_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   860
qed "z_in_interval";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   861
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   862
Goal "[| z : P; ! y:Y. (y, z) : induced P r |]\
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   863
\     ==> ((lam x: intY1. f x) z, z) : induced intY1 r";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   864
by (afs [induced_def,intY1_func RS funcset_mem, z_in_interval] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   865
by (rtac (z_in_interval RS restrict_apply1 RS ssubst) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   866
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   867
by (afs [induced_def] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   868
by (afs [fixfE2] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   869
by (rtac reflE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   870
by (rtac CompleteLatticeE11 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   871
by (etac (fixfE1 RS subsetD) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   872
qed "f'z_in_int_rel";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   873
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   874
Goal "? L. islub Y (| pset = P, order = induced P r |) L";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   875
by (res_inst_tac [("x","v")] exI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   876
by (simp_tac (simpset() addsimps [islub_def]) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   877
(* v : P *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   878
by (afs [v_in_P] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   879
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   880
(* v is lub *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   881
(*  1. ! y:Y. (y, v) : induced P r *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   882
by (rtac ballI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   883
by (afs [induced_def, subsetD, v_in_P] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   884
by (rtac conjI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   885
by (etac (thm "Y_ss" RS subsetD) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   886
by (res_inst_tac [("b","lub Y cl")] transE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   887
by (rtac CompleteLatticeE13 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   888
by (rtac (lubE1 RS bspec) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   889
by (rtac Y_subset_A 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   890
by (assume_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   891
by (res_inst_tac [("b","Top cl")] intervalE1 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   892
by (afs [thm "v_def"] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   893
by (fold_goals_tac [thm "intY1_def"]);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   894
by (rtac (simplify (simpset()) (intY1_is_cl RS export glb_in_lattice)) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   895
by (Simp_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   896
by (rtac subsetI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   897
by (dtac CollectD 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   898
by (etac conjunct2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   899
(* v is LEAST ub *)
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   900
by (Clarify_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   901
by (rtac indI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   902
by (afs [v_in_P] 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   903
by (assume_tac 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   904
by (rewrite_goals_tac [thm "v_def"]);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   905
by (rtac indE 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   906
by (rtac intY1_subset 2);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   907
by (rtac (simplify (simpset()) (intY1_is_cl RS export (glbE1 RS bspec))) 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   908
by (Simp_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   909
by (rtac subsetI 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   910
by (dtac CollectD 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   911
by (etac conjunct2 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   912
by (afs [f'z_in_int_rel, z_in_interval] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   913
qed "tarski_full_lemma";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   914
val Tarski_full_lemma = Export tarski_full_lemma;
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   915
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   916
Close_locale "Tarski";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   917
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   918
Goal "(| pset = P, order = induced P r|) : CompleteLattice";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   919
by (rtac CompleteLatticeI_simp 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   920
by (afs [fixf_po] 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   921
by (Clarify_tac 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   922
by (etac Tarski_full_lemma 1);
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   923
qed "Tarski_full";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   924
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   925
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   926
Close_locale "CLF";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   927
Close_locale "CL";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   928
Close_locale "PO";
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   929
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   930
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents:
diff changeset
   931