1461

1 
(* Title: LCF/fix

660

2 
ID: $Id$

1461

3 
Author: Tobias Nipkow

660

4 
Copyright 1992 University of Cambridge


5 


6 
Fixedpoint theory


7 
*)


8 

0

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 

3837

25 
val adm_eq = prove_goal LCF.thy "adm(%x. t(x)=(u(x)::'a::cpo))"

1461

26 
(fn _ => [rewtac eq_def,


27 
REPEAT(rstac[adm_conj,adm_less]1)]);

0

28 


29 
val adm_not_not = prove_goal LCF.thy "adm(P) ==> adm(%x.~~P(x))"

1461

30 
(fn prems => [simp_tac (LCF_ss addsimps prems) 1]);

0

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)"

660

36 
(fn _ => [tac]) RS spec;

0

37 


38 
val not_eq_FF = prove_goal LCF.thy "ALL p. ~p=FF <> (p=TT  p=UU)"

660

39 
(fn _ => [tac]) RS spec;

0

40 


41 
val not_eq_UU = prove_goal LCF.thy "ALL p. ~p=UU <> (p=TT  p=FF)"

660

42 
(fn _ => [tac]) RS spec;

0

43 

3837

44 
val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr. adm(%x. ~t(x)=p)"

660

45 
(fn _ => [rtac tr_induct 1,


46 
REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN

1461

47 
REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec;

0

48 


49 
val adm_lemmas = [adm_not_free,adm_eq,adm_less,adm_not_less,adm_not_eq_tr,

1461

50 
adm_conj,adm_disj,adm_imp,adm_all];

0

51 


52 
fun induct_tac v i = res_inst_tac[("f",v)] induct i THEN

1461

53 
REPEAT(rstac adm_lemmas i);

0

54 


55 


56 
val least_FIX = prove_goal LCF.thy "f(p) = p ==> FIX(f) << p"

1461

57 
(fn [prem] => [induct_tac "f" 1, rtac minimal 1, strip_tac 1,


58 
stac (prem RS sym) 1, etac less_ap_term 1]);

0

59 


60 
val lfp_is_FIX = prove_goal LCF.thy

1461

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]);

0

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,

1461

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]);

0

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

3837

83 
"[ adm(%p. P(FST(p),SND(p))); P(UU::'a,UU::'b);\

1461

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]]);

0

91 


92 
fun induct2_tac (f,g) i = res_inst_tac[("f",f),("g",g)] induct2 i THEN

1461

93 
REPEAT(rstac adm_lemmas i);

0

94 


95 
end;


96 


97 
open Fix;
