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