author | lcp |
Wed, 19 Oct 1994 09:44:31 +0100 | |
changeset 645 | 77474875da92 |
parent 442 | 13ac1fd0a14d |
child 660 | 7fe6ec24d842 |
permissions | -rw-r--r-- |
0 | 1 |
signature FIX = |
2 |
sig |
|
3 |
val adm_eq: thm |
|
4 |
val adm_not_eq_tr: thm |
|
5 |
val adm_not_not: thm |
|
6 |
val not_eq_TT: thm |
|
7 |
val not_eq_FF: thm |
|
8 |
val not_eq_UU: thm |
|
9 |
val induct2: thm |
|
10 |
val induct_tac: string -> int -> tactic |
|
11 |
val induct2_tac: string*string -> int -> tactic |
|
12 |
end; |
|
13 |
||
14 |
structure Fix:FIX = |
|
15 |
struct |
|
16 |
||
442
13ac1fd0a14d
added parentheses made necessary by change of constrain's precedence
clasohm
parents:
231
diff
changeset
|
17 |
val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=(u(x)::'a::cpo))" |
0 | 18 |
(fn _ => [rewrite_goals_tac [eq_def], |
19 |
REPEAT(rstac[adm_conj,adm_less]1)]); |
|
20 |
||
21 |
val adm_not_not = prove_goal LCF.thy "adm(P) ==> adm(%x.~~P(x))" |
|
22 |
(fn prems => [simp_tac (LCF_ss addsimps prems) 1]); |
|
23 |
||
24 |
||
25 |
val tac = rtac tr_induct 1 THEN REPEAT(simp_tac LCF_ss 1); |
|
26 |
||
27 |
val not_eq_TT = prove_goal LCF.thy "ALL p. ~p=TT <-> (p=FF | p=UU)" |
|
28 |
(fn _ => [tac]) RS spec; |
|
29 |
||
30 |
val not_eq_FF = prove_goal LCF.thy "ALL p. ~p=FF <-> (p=TT | p=UU)" |
|
31 |
(fn _ => [tac]) RS spec; |
|
32 |
||
33 |
val not_eq_UU = prove_goal LCF.thy "ALL p. ~p=UU <-> (p=TT | p=FF)" |
|
34 |
(fn _ => [tac]) RS spec; |
|
35 |
||
36 |
val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr.adm(%x. ~t(x)=p)" |
|
37 |
(fn _ => [rtac tr_induct 1, |
|
38 |
REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN |
|
39 |
REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec; |
|
40 |
||
41 |
val adm_lemmas = [adm_not_free,adm_eq,adm_less,adm_not_less,adm_not_eq_tr, |
|
42 |
adm_conj,adm_disj,adm_imp,adm_all]; |
|
43 |
||
44 |
fun induct_tac v i = res_inst_tac[("f",v)] induct i THEN |
|
45 |
REPEAT(rstac adm_lemmas i); |
|
46 |
||
47 |
||
48 |
val least_FIX = prove_goal LCF.thy "f(p) = p ==> FIX(f) << p" |
|
49 |
(fn [prem] => [induct_tac "f" 1, rtac minimal 1, strip_tac 1, |
|
50 |
stac (prem RS sym) 1, etac less_ap_term 1]); |
|
51 |
||
52 |
val lfp_is_FIX = prove_goal LCF.thy |
|
53 |
"[| f(p) = p; ALL q. f(q)=q --> p << q |] ==> p = FIX(f)" |
|
54 |
(fn [prem1,prem2] => [rtac less_anti_sym 1, |
|
645
77474875da92
LCF/fix/lfp_is_FIX: modified proof to suppress deep unification
lcp
parents:
442
diff
changeset
|
55 |
rtac (prem2 RS spec RS mp) 1, rtac FIX_eq 1, |
0 | 56 |
rtac least_FIX 1, rtac prem1 1]); |
57 |
||
58 |
val ffix = read_instantiate [("f","f::?'a=>?'a")] FIX_eq; |
|
59 |
val gfix = read_instantiate [("f","g::?'a=>?'a")] FIX_eq; |
|
60 |
val ss = LCF_ss addsimps [ffix,gfix]; |
|
61 |
||
62 |
(* Do not use prove_goal because the result is ?ed which leads to divergence |
|
63 |
when submitted as an argument to SIMP_THM *) |
|
64 |
(* |
|
65 |
local |
|
231 | 66 |
val thm = trivial(read_cterm(sign_of LCF.thy) |
0 | 67 |
("<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)",propT)); |
68 |
val tac = EVERY1[rtac lfp_is_FIX, simp_tac ss, |
|
69 |
strip_tac, simp_tac (LCF_ss addsimps [PROD_less]), |
|
70 |
rtac conjI, rtac least_FIX, etac subst, rtac (FST RS sym), |
|
71 |
rtac least_FIX, etac subst, rtac (SND RS sym)]; |
|
72 |
in |
|
73 |
val Some(FIX_pair,_) = Sequence.pull(tapply(tac,thm)); |
|
74 |
end; |
|
75 |
||
76 |
val FIX_pair_conj = SIMP_THM (LCF_ss addsimps [PROD_eq]) FIX_pair; |
|
77 |
*) |
|
78 |
val FIX_pair = prove_goal LCF.thy |
|
79 |
"<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)" |
|
80 |
(fn _ => [rtac lfp_is_FIX 1, simp_tac ss 1, |
|
81 |
strip_tac 1, simp_tac (LCF_ss addsimps [PROD_less]) 1, |
|
82 |
rtac conjI 1, rtac least_FIX 1, etac subst 1, rtac (FST RS sym) 1, |
|
83 |
rtac least_FIX 1, etac subst 1, rtac (SND RS sym) 1]); |
|
84 |
||
85 |
val FIX_pair_conj = rewrite_rule (map mk_meta_eq [PROD_eq,FST,SND]) FIX_pair; |
|
86 |
||
87 |
val FIX1 = FIX_pair_conj RS conjunct1; |
|
88 |
val FIX2 = FIX_pair_conj RS conjunct2; |
|
89 |
||
90 |
val induct2 = prove_goal LCF.thy |
|
91 |
"[| adm(%p.P(FST(p),SND(p))); P(UU::'a,UU::'b);\ |
|
92 |
\ ALL x y. P(x,y) --> P(f(x),g(y)) |] ==> P(FIX(f),FIX(g))" |
|
93 |
(fn prems => [EVERY1 |
|
94 |
[res_inst_tac [("f","f"),("g","g")] (standard(FIX1 RS ssubst)), |
|
95 |
res_inst_tac [("f","f"),("g","g")] (standard(FIX2 RS ssubst)), |
|
96 |
res_inst_tac [("f","%x. <f(FST(x)),g(SND(x))>")] induct, |
|
97 |
rstac prems, simp_tac ss, rstac prems, |
|
98 |
simp_tac (LCF_ss addsimps [expand_all_PROD]), rstac prems]]); |
|
99 |
||
100 |
fun induct2_tac (f,g) i = res_inst_tac[("f",f),("g",g)] induct2 i THEN |
|
101 |
REPEAT(rstac adm_lemmas i); |
|
102 |
||
103 |
end; |
|
104 |
||
105 |
open Fix; |