src/HOL/Lfp.ML
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 5316 7a8975451a89
child 9422 4b6bc2b347e5
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
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
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
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
open Lfp;
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
(*** Proof of Knaster-Tarski Theorem ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
(* 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
    14
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    15
Goalw [lfp_def] "f(A) <= A ==> lfp(f) <= A";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
by (rtac (CollectI RS Inter_lower) 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    17
by (assume_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
qed "lfp_lowerbound";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    20
val prems = Goalw [lfp_def]
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
    "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
by (etac CollectD 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
qed "lfp_greatest";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    25
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    26
Goal "mono(f) ==> f(lfp(f)) <= lfp(f)";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    27
by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    28
            etac monoD, rtac lfp_lowerbound, atac, atac]);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
qed "lfp_lemma2";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    31
Goal "mono(f) ==> lfp(f) <= f(lfp(f))";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    32
by (EVERY1 [rtac lfp_lowerbound, rtac monoD, assume_tac,
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    33
            etac lfp_lemma2]);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    34
qed "lfp_lemma3";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    35
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    36
Goal "mono(f) ==> lfp(f) = f(lfp(f))";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    37
by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
qed "lfp_Tarski";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    39
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    40
(*** General induction rule for least fixed points ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    42
val [lfp,mono,indhyp] = Goal
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    43
    "[| a: lfp(f);  mono(f);                            \
3842
b55686a7b22c fixed dots;
wenzelm
parents: 1873
diff changeset
    44
\       !!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
    45
\    |] ==> P(a)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
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
    47
by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
by (EVERY1 [rtac Int_greatest, rtac subset_trans, 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    49
            rtac (Int_lower1 RS (mono RS monoD)),
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    50
            rtac (mono RS lfp_lemma2),
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    51
            rtac (CollectI RS subsetI), rtac indhyp, atac]);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    52
qed "induct";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    53
5098
48e70d9fe05f Removed structure Prod_Syntax.
berghofe
parents: 3842
diff changeset
    54
bind_thm ("induct2",
48e70d9fe05f Removed structure Prod_Syntax.
berghofe
parents: 3842
diff changeset
    55
  split_rule (read_instantiate [("a","(a,b)")] induct));
1114
c8dfb56a7e95 Prod is now a parent of Lfp.
nipkow
parents: 923
diff changeset
    56
1125
13a3df2adbe5 Added Park induction to Lfp.
nipkow
parents: 1114
diff changeset
    57
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    58
(** Definition forms of lfp_Tarski and induct, to control unfolding **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    59
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    60
val [rew,mono] = goal Lfp.thy "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    61
by (rewtac rew);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    62
by (rtac (mono RS lfp_Tarski) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    63
qed "def_lfp_Tarski";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    64
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    65
val rew::prems = Goal
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    66
    "[| A == lfp(f);  mono(f);   a:A;                   \
3842
b55686a7b22c fixed dots;
wenzelm
parents: 1873
diff changeset
    67
\       !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)        \
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    68
\    |] ==> P(a)";
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    69
by (EVERY1 [rtac induct,        (*backtracking to force correct induction*)
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    70
            REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    71
qed "def_induct";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    72
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    73
(*Monotonicity of lfp!*)
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5098
diff changeset
    74
val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    75
by (rtac (lfp_lowerbound RS lfp_greatest) 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
    76
by (etac (prem RS subset_trans) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
qed "lfp_mono";