src/HOL/Lfp.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10202 9e8b4bebc940
child 14169 0590de71a016
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9422
4b6bc2b347e5 avoid referencing thy value;
wenzelm
parents: 5316
diff changeset
     1
(*  Title:      HOL/Lfp.ML
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
9422
4b6bc2b347e5 avoid referencing thy value;
wenzelm
parents: 5316
diff changeset
     6
The Knaster-Tarski Theorem.
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
(*** Proof of Knaster-Tarski Theorem ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
(* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    13
Goalw [lfp_def] "f(A) <= A ==> lfp(f) <= A";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
by (rtac (CollectI RS Inter_lower) 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    15
by (assume_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
qed "lfp_lowerbound";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    18
val prems = Goalw [lfp_def]
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
    "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
by (etac CollectD 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
qed "lfp_greatest";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    24
Goal "mono(f) ==> f(lfp(f)) <= lfp(f)";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    25
by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    26
            etac monoD, rtac lfp_lowerbound, atac, atac]);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    27
qed "lfp_lemma2";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    28
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    29
Goal "mono(f) ==> lfp(f) <= f(lfp(f))";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    30
by (EVERY1 [rtac lfp_lowerbound, rtac monoD, assume_tac,
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    31
            etac lfp_lemma2]);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    32
qed "lfp_lemma3";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    33
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    34
Goal "mono(f) ==> lfp(f) = f(lfp(f))";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    35
by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
10186
499637e8f2c6 *** empty log message ***
nipkow
parents: 10067
diff changeset
    36
qed "lfp_unfold";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    37
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
(*** General induction rule for least fixed points ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    39
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    40
val [lfp,mono,indhyp] = Goal
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    41
    "[| a: lfp(f);  mono(f);                            \
3842
b55686a7b22c fixed dots;
wenzelm
parents: 1873
diff changeset
    42
\       !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)   \
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
\    |] ==> P(a)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    44
by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
by (EVERY1 [rtac Int_greatest, rtac subset_trans, 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    47
            rtac (Int_lower1 RS (mono RS monoD)),
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    48
            rtac (mono RS lfp_lemma2),
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    49
            rtac (CollectI RS subsetI), rtac indhyp, atac]);
10202
9e8b4bebc940 induct -> lfp_induct
nipkow
parents: 10186
diff changeset
    50
qed "lfp_induct";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
10202
9e8b4bebc940 induct -> lfp_induct
nipkow
parents: 10186
diff changeset
    52
bind_thm ("lfp_induct2",
9e8b4bebc940 induct -> lfp_induct
nipkow
parents: 10186
diff changeset
    53
  split_rule (read_instantiate [("a","(a,b)")] lfp_induct));
1114
c8dfb56a7e95 Prod is now a parent of Lfp.
nipkow
parents: 923
diff changeset
    54
1125
13a3df2adbe5 Added Park induction to Lfp.
nipkow
parents: 1114
diff changeset
    55
10202
9e8b4bebc940 induct -> lfp_induct
nipkow
parents: 10186
diff changeset
    56
(** Definition forms of lfp_unfold and lfp_induct, to control unfolding **)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    57
10067
ab03cfd6be3a tidied, removing obsolete "goal" commands
paulson
parents: 9422
diff changeset
    58
Goal "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
10186
499637e8f2c6 *** empty log message ***
nipkow
parents: 10067
diff changeset
    59
by (auto_tac (claset() addSIs [lfp_unfold], simpset()));  
499637e8f2c6 *** empty log message ***
nipkow
parents: 10067
diff changeset
    60
qed "def_lfp_unfold";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    61
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    62
val rew::prems = Goal
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    63
    "[| A == lfp(f);  mono(f);   a:A;                   \
3842
b55686a7b22c fixed dots;
wenzelm
parents: 1873
diff changeset
    64
\       !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)        \
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
\    |] ==> P(a)";
10202
9e8b4bebc940 induct -> lfp_induct
nipkow
parents: 10186
diff changeset
    66
by (EVERY1 [rtac lfp_induct,        (*backtracking to force correct induction*)
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    67
            REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
10202
9e8b4bebc940 induct -> lfp_induct
nipkow
parents: 10186
diff changeset
    68
qed "def_lfp_induct";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    69
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    70
(*Monotonicity of lfp!*)
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    71
val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    72
by (rtac (lfp_lowerbound RS lfp_greatest) 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    73
by (etac (prem RS subset_trans) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    74
qed "lfp_mono";