author  paulson 
Mon, 23 Sep 1996 18:18:18 +0200  
changeset 2010  0a22b9d63a18 
parent 1461  6bcb44e4d6e5 
child 3837  d7f033c74b38 
permissions  rwrr 
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 

442
13ac1fd0a14d
added parentheses made necessary by change of constrain's precedence
clasohm
parents:
231
diff
changeset

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 

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 

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

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; 