src/LCF/fix.ML
author nipkow
Tue, 17 Oct 2000 08:00:46 +0200
changeset 10228 e653cb933293
parent 3837 d7f033c74b38
child 17248 81bf91654e73
permissions -rw-r--r--
added intermediate value thms
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
     1
(*  Title:      LCF/fix
660
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
     3
    Author:     Tobias Nipkow
660
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
     4
    Copyright   1992  University of Cambridge
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
     5
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
     6
Fixedpoint theory
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
     7
*)
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
     8
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
signature FIX =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
  val adm_eq: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  val adm_not_eq_tr: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  val adm_not_not: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  val not_eq_TT: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  val not_eq_FF: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  val not_eq_UU: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val induct2: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val induct_tac: string -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val induct2_tac: string*string -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
structure Fix:FIX =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1461
diff changeset
    25
val adm_eq = prove_goal LCF.thy "adm(%x. t(x)=(u(x)::'a::cpo))"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    26
        (fn _ => [rewtac eq_def,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    27
                  REPEAT(rstac[adm_conj,adm_less]1)]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
val adm_not_not = prove_goal LCF.thy "adm(P) ==> adm(%x.~~P(x))"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    30
        (fn prems => [simp_tac (LCF_ss addsimps prems) 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val tac = rtac tr_induct 1 THEN REPEAT(simp_tac LCF_ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
val not_eq_TT = prove_goal LCF.thy "ALL p. ~p=TT <-> (p=FF | p=UU)"
660
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
    36
    (fn _ => [tac]) RS spec;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val not_eq_FF = prove_goal LCF.thy "ALL p. ~p=FF <-> (p=TT | p=UU)"
660
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
    39
    (fn _ => [tac]) RS spec;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val not_eq_UU = prove_goal LCF.thy "ALL p. ~p=UU <-> (p=TT | p=FF)"
660
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
    42
    (fn _ => [tac]) RS spec;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1461
diff changeset
    44
val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr. adm(%x. ~t(x)=p)"
660
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
    45
    (fn _ => [rtac tr_induct 1,
7fe6ec24d842 added header files; deleted commented-out code
lcp
parents: 645
diff changeset
    46
    REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    47
           REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
val adm_lemmas = [adm_not_free,adm_eq,adm_less,adm_not_less,adm_not_eq_tr,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    50
                  adm_conj,adm_disj,adm_imp,adm_all];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
fun induct_tac v i = res_inst_tac[("f",v)] induct i THEN
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    53
                     REPEAT(rstac adm_lemmas i);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
val least_FIX = prove_goal LCF.thy "f(p) = p ==> FIX(f) << p"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    57
        (fn [prem] => [induct_tac "f" 1, rtac minimal 1, strip_tac 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    58
                        stac (prem RS sym) 1, etac less_ap_term 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
val lfp_is_FIX = prove_goal LCF.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    61
        "[| f(p) = p; ALL q. f(q)=q --> p << q |] ==> p = FIX(f)"
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    62
        (fn [prem1,prem2] => [rtac less_anti_sym 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    63
                              rtac (prem2 RS spec RS mp) 1, rtac FIX_eq 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    64
                              rtac least_FIX 1, rtac prem1 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val ffix = read_instantiate [("f","f::?'a=>?'a")] FIX_eq;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
val gfix = read_instantiate [("f","g::?'a=>?'a")] FIX_eq;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
val ss = LCF_ss addsimps [ffix,gfix];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
val FIX_pair = prove_goal LCF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  "<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
  (fn _ => [rtac lfp_is_FIX 1, simp_tac ss 1,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    73
          strip_tac 1, simp_tac (LCF_ss addsimps [PROD_less]) 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    74
          rtac conjI 1, rtac least_FIX 1, etac subst 1, rtac (FST RS sym) 1,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    75
          rtac least_FIX 1, etac subst 1, rtac (SND RS sym) 1]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
val FIX_pair_conj = rewrite_rule (map mk_meta_eq [PROD_eq,FST,SND]) FIX_pair;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
val FIX1 = FIX_pair_conj RS conjunct1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
val FIX2 = FIX_pair_conj RS conjunct2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
val induct2 = prove_goal LCF.thy
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1461
diff changeset
    83
         "[| adm(%p. P(FST(p),SND(p))); P(UU::'a,UU::'b);\
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    84
\            ALL x y. P(x,y) --> P(f(x),g(y)) |] ==> P(FIX(f),FIX(g))"
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    85
        (fn prems => [EVERY1
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    86
        [res_inst_tac [("f","f"),("g","g")] (standard(FIX1 RS ssubst)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    87
         res_inst_tac [("f","f"),("g","g")] (standard(FIX2 RS ssubst)),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    88
         res_inst_tac [("f","%x. <f(FST(x)),g(SND(x))>")] induct,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    89
         rstac prems, simp_tac ss, rstac prems,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    90
         simp_tac (LCF_ss addsimps [expand_all_PROD]), rstac prems]]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
fun induct2_tac (f,g) i = res_inst_tac[("f",f),("g",g)] induct2 i THEN
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 660
diff changeset
    93
                     REPEAT(rstac adm_lemmas i);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
open Fix;