1 (* Title: LCF/fix |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1992 University of Cambridge |
|
5 *) |
|
6 |
|
7 val adm_eq = prove_goal (the_context ()) "adm(%x. t(x)=(u(x)::'a::cpo))" |
|
8 (fn _ => [rewtac eq_def, |
|
9 REPEAT(rstac[adm_conj,adm_less]1)]); |
|
10 |
|
11 val adm_not_not = prove_goal (the_context ()) "adm(P) ==> adm(%x.~~P(x))" |
|
12 (fn prems => [simp_tac (LCF_ss addsimps prems) 1]); |
|
13 |
|
14 |
|
15 val tac = rtac tr_induct 1 THEN ALLGOALS (simp_tac LCF_ss); |
|
16 |
|
17 val not_eq_TT = prove_goal (the_context ()) "ALL p. ~p=TT <-> (p=FF | p=UU)" |
|
18 (fn _ => [tac]) RS spec; |
|
19 |
|
20 val not_eq_FF = prove_goal (the_context ()) "ALL p. ~p=FF <-> (p=TT | p=UU)" |
|
21 (fn _ => [tac]) RS spec; |
|
22 |
|
23 val not_eq_UU = prove_goal (the_context ()) "ALL p. ~p=UU <-> (p=TT | p=FF)" |
|
24 (fn _ => [tac]) RS spec; |
|
25 |
|
26 val adm_not_eq_tr = prove_goal (the_context ()) "ALL p::tr. adm(%x. ~t(x)=p)" |
|
27 (fn _ => [rtac tr_induct 1, |
|
28 REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN |
|
29 REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec; |
|
30 |
|
31 val adm_lemmas = [adm_not_free,adm_eq,adm_less,adm_not_less,adm_not_eq_tr, |
|
32 adm_conj,adm_disj,adm_imp,adm_all]; |
|
33 |
|
34 fun induct_tac v i = res_inst_tac[("f",v)] induct i THEN |
|
35 REPEAT(rstac adm_lemmas i); |
|
36 |
|
37 |
|
38 val least_FIX = prove_goal (the_context ()) "f(p) = p ==> FIX(f) << p" |
|
39 (fn [prem] => [induct_tac "f" 1, rtac minimal 1, strip_tac 1, |
|
40 stac (prem RS sym) 1, etac less_ap_term 1]); |
|
41 |
|
42 val lfp_is_FIX = prove_goal (the_context ()) |
|
43 "[| f(p) = p; ALL q. f(q)=q --> p << q |] ==> p = FIX(f)" |
|
44 (fn [prem1,prem2] => [rtac less_anti_sym 1, |
|
45 rtac (prem2 RS spec RS mp) 1, rtac FIX_eq 1, |
|
46 rtac least_FIX 1, rtac prem1 1]); |
|
47 |
|
48 val ffix = read_instantiate [("f","f::?'a=>?'a")] FIX_eq; |
|
49 val gfix = read_instantiate [("f","g::?'a=>?'a")] FIX_eq; |
|
50 val ss = LCF_ss addsimps [ffix,gfix]; |
|
51 |
|
52 val FIX_pair = prove_goal (the_context ()) |
|
53 "<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)" |
|
54 (fn _ => [rtac lfp_is_FIX 1, simp_tac ss 1, |
|
55 strip_tac 1, simp_tac (LCF_ss addsimps [PROD_less]) 1, |
|
56 rtac conjI 1, rtac least_FIX 1, etac subst 1, rtac (FST RS sym) 1, |
|
57 rtac least_FIX 1, etac subst 1, rtac (SND RS sym) 1]); |
|
58 |
|
59 val FIX_pair_conj = rewrite_rule (map mk_meta_eq [PROD_eq,FST,SND]) FIX_pair; |
|
60 |
|
61 val FIX1 = FIX_pair_conj RS conjunct1; |
|
62 val FIX2 = FIX_pair_conj RS conjunct2; |
|
63 |
|
64 val induct2 = prove_goal (the_context ()) |
|
65 "[| adm(%p. P(FST(p),SND(p))); P(UU::'a,UU::'b);\ |
|
66 \ ALL x y. P(x,y) --> P(f(x),g(y)) |] ==> P(FIX(f),FIX(g))" |
|
67 (fn prems => [EVERY1 |
|
68 [res_inst_tac [("f","f"),("g","g")] (standard(FIX1 RS ssubst)), |
|
69 res_inst_tac [("f","f"),("g","g")] (standard(FIX2 RS ssubst)), |
|
70 res_inst_tac [("f","%x. <f(FST(x)),g(SND(x))>")] induct, |
|
71 rstac prems, simp_tac ss, rstac prems, |
|
72 simp_tac (LCF_ss addsimps [expand_all_PROD]), rstac prems]]); |
|
73 |
|
74 fun induct2_tac (f,g) i = res_inst_tac[("f",f),("g",g)] induct2 i THEN |
|
75 REPEAT(rstac adm_lemmas i); |
|