author | paulson |
Fri, 29 Oct 2004 15:16:02 +0200 | |
changeset 15270 | 8b3f707a78a7 |
parent 5062 | fbdb0b541314 |
child 17456 | bcf7544875b2 |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: CCL/fix |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
For fix.thy. |
|
7 |
*) |
|
8 |
||
9 |
open Fix; |
|
10 |
||
11 |
(*** Fixed Point Induction ***) |
|
12 |
||
13 |
val [base,step,incl] = goalw Fix.thy [INCL_def] |
|
3837 | 14 |
"[| P(bot); !!x. P(x) ==> P(f(x)); INCL(P) |] ==> P(fix(f))"; |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
15 |
by (rtac (incl RS spec RS mp) 1); |
0 | 16 |
by (rtac (Nat_ind RS ballI) 1 THEN atac 1); |
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
17 |
by (ALLGOALS (simp_tac term_ss)); |
0 | 18 |
by (REPEAT (ares_tac [base,step] 1)); |
757 | 19 |
qed "fix_ind"; |
0 | 20 |
|
21 |
(*** Inclusive Predicates ***) |
|
22 |
||
23 |
val prems = goalw Fix.thy [INCL_def] |
|
24 |
"INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
25 |
by (rtac iff_refl 1); |
757 | 26 |
qed "inclXH"; |
0 | 27 |
|
28 |
val prems = goal Fix.thy |
|
3837 | 29 |
"[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))"; |
0 | 30 |
by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1); |
757 | 31 |
qed "inclI"; |
0 | 32 |
|
33 |
val incl::prems = goal Fix.thy |
|
3837 | 34 |
"[| INCL(P); !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))"; |
0 | 35 |
by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] |
36 |
@ prems)) 1); |
|
757 | 37 |
qed "inclD"; |
0 | 38 |
|
39 |
val incl::prems = goal Fix.thy |
|
3837 | 40 |
"[| INCL(P); (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R"; |
0 | 41 |
by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1); |
757 | 42 |
qed "inclE"; |
0 | 43 |
|
44 |
||
45 |
(*** Lemmas for Inclusive Predicates ***) |
|
46 |
||
5062 | 47 |
Goal "INCL(%x.~ a(x) [= t)"; |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
48 |
by (rtac inclI 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
49 |
by (dtac bspec 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
50 |
by (rtac zeroT 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
51 |
by (etac contrapos 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
52 |
by (rtac po_trans 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
53 |
by (assume_tac 2); |
2035 | 54 |
by (stac napplyBzero 1); |
0 | 55 |
by (rtac po_cong 1 THEN rtac po_bot 1); |
757 | 56 |
qed "npo_INCL"; |
0 | 57 |
|
3837 | 58 |
val prems = goal Fix.thy "[| INCL(P); INCL(Q) |] ==> INCL(%x. P(x) & Q(x))"; |
0 | 59 |
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; |
757 | 60 |
qed "conj_INCL"; |
0 | 61 |
|
3837 | 62 |
val prems = goal Fix.thy "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))"; |
0 | 63 |
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; |
757 | 64 |
qed "all_INCL"; |
0 | 65 |
|
3837 | 66 |
val prems = goal Fix.thy "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))"; |
0 | 67 |
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; |
757 | 68 |
qed "ball_INCL"; |
0 | 69 |
|
5062 | 70 |
Goal "INCL(%x. a(x) = (b(x)::'a::prog))"; |
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
71 |
by (simp_tac (term_ss addsimps [eq_iff]) 1); |
0 | 72 |
by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1)); |
757 | 73 |
qed "eq_INCL"; |
0 | 74 |
|
75 |
(*** Derivation of Reachability Condition ***) |
|
76 |
||
77 |
(* Fixed points of idgen *) |
|
78 |
||
5062 | 79 |
Goal "idgen(fix(idgen)) = fix(idgen)"; |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
80 |
by (rtac (fixB RS sym) 1); |
757 | 81 |
qed "fix_idgenfp"; |
0 | 82 |
|
5062 | 83 |
Goalw [idgen_def] "idgen(lam x. x) = lam x. x"; |
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
84 |
by (simp_tac term_ss 1); |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
85 |
by (rtac (term_case RS allI) 1); |
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
86 |
by (ALLGOALS (simp_tac term_ss)); |
757 | 87 |
qed "id_idgenfp"; |
0 | 88 |
|
89 |
(* All fixed points are lam-expressions *) |
|
90 |
||
91 |
val [prem] = goal Fix.thy "idgen(d) = d ==> d = lam x.?f(x)"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
92 |
by (rtac (prem RS subst) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
93 |
by (rewtac idgen_def); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
94 |
by (rtac refl 1); |
757 | 95 |
qed "idgenfp_lam"; |
0 | 96 |
|
97 |
(* Lemmas for rewriting fixed points of idgen *) |
|
98 |
||
99 |
val prems = goalw Fix.thy [idgen_def] |
|
100 |
"[| a = b; a ` t = u |] ==> b ` t = u"; |
|
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
101 |
by (simp_tac (term_ss addsimps (prems RL [sym])) 1); |
757 | 102 |
qed "l_lemma"; |
0 | 103 |
|
104 |
val idgen_lemmas = |
|
105 |
let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s |
|
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
106 |
(fn [prem] => [rtac (prem RS l_lemma) 1,simp_tac term_ss 1]) |
0 | 107 |
in map mk_thm |
108 |
[ "idgen(d) = d ==> d ` bot = bot", |
|
109 |
"idgen(d) = d ==> d ` true = true", |
|
110 |
"idgen(d) = d ==> d ` false = false", |
|
111 |
"idgen(d) = d ==> d ` <a,b> = <d ` a,d ` b>", |
|
3837 | 112 |
"idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)"] |
0 | 113 |
end; |
114 |
||
115 |
(* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points |
|
116 |
of idgen and hence are they same *) |
|
117 |
||
118 |
val [p1,p2,p3] = goal CCL.thy |
|
3837 | 119 |
"[| ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x) |] ==> t [= u"; |
2035 | 120 |
by (stac (p2 RS cond_eta) 1); |
121 |
by (stac (p3 RS cond_eta) 1); |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
122 |
by (rtac (p1 RS (po_lam RS iffD2)) 1); |
757 | 123 |
qed "po_eta"; |
0 | 124 |
|
125 |
val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
126 |
by (rtac (prem RS subst) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
127 |
by (rtac refl 1); |
757 | 128 |
qed "po_eta_lemma"; |
0 | 129 |
|
130 |
val [prem] = goal Fix.thy |
|
131 |
"idgen(d) = d ==> \ |
|
3837 | 132 |
\ {p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)} <= \ |
133 |
\ POgen({p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)})"; |
|
0 | 134 |
by (REPEAT (step_tac term_cs 1)); |
135 |
by (term_case_tac "t" 1); |
|
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
136 |
by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas))))); |
0 | 137 |
by (ALLGOALS (fast_tac set_cs)); |
757 | 138 |
qed "lemma1"; |
0 | 139 |
|
140 |
val [prem] = goal Fix.thy |
|
141 |
"idgen(d) = d ==> fix(idgen) [= d"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
142 |
by (rtac (allI RS po_eta) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
143 |
by (rtac (lemma1 RSN(2,po_coinduct)) 1); |
0 | 144 |
by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); |
757 | 145 |
qed "fix_least_idgen"; |
0 | 146 |
|
147 |
val [prem] = goal Fix.thy |
|
148 |
"idgen(d) = d ==> \ |
|
3837 | 149 |
\ {p. EX a b. p=<a,b> & b = d ` a} <= POgen({p. EX a b. p=<a,b> & b = d ` a})"; |
0 | 150 |
by (REPEAT (step_tac term_cs 1)); |
151 |
by (term_case_tac "a" 1); |
|
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
152 |
by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas))))); |
0 | 153 |
by (ALLGOALS (fast_tac set_cs)); |
757 | 154 |
qed "lemma2"; |
0 | 155 |
|
156 |
val [prem] = goal Fix.thy |
|
3837 | 157 |
"idgen(d) = d ==> lam x. x [= d"; |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
158 |
by (rtac (allI RS po_eta) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
159 |
by (rtac (lemma2 RSN(2,po_coinduct)) 1); |
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
160 |
by (simp_tac term_ss 1); |
0 | 161 |
by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); |
757 | 162 |
qed "id_least_idgen"; |
0 | 163 |
|
5062 | 164 |
Goal "fix(idgen) = lam x. x"; |
0 | 165 |
by (fast_tac (term_cs addIs [eq_iff RS iffD2, |
166 |
id_idgenfp RS fix_least_idgen, |
|
167 |
fix_idgenfp RS id_least_idgen]) 1); |
|
757 | 168 |
qed "reachability"; |
0 | 169 |
|
170 |
(********) |
|
171 |
||
3837 | 172 |
val [prem] = goal Fix.thy "f = lam x. x ==> f`t = t"; |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
173 |
by (rtac (prem RS sym RS subst) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
174 |
by (rtac applyB 1); |
757 | 175 |
qed "id_apply"; |
0 | 176 |
|
177 |
val prems = goal Fix.thy |
|
178 |
"[| P(bot); P(true); P(false); \ |
|
179 |
\ !!x y.[| P(x); P(y) |] ==> P(<x,y>); \ |
|
3837 | 180 |
\ !!u.(!!x. P(u(x))) ==> P(lam x. u(x)); INCL(P) |] ==> \ |
0 | 181 |
\ P(t)"; |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
182 |
by (rtac (reachability RS id_apply RS subst) 1); |
0 | 183 |
by (res_inst_tac [("x","t")] spec 1); |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
184 |
by (rtac fix_ind 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
185 |
by (rewtac idgen_def); |
0 | 186 |
by (REPEAT_SOME (ares_tac [allI])); |
2035 | 187 |
by (stac applyBbot 1); |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
442
diff
changeset
|
188 |
by (resolve_tac prems 1); |
0 | 189 |
br (applyB RS ssubst )1; |
190 |
by (res_inst_tac [("t","xa")] term_case 1); |
|
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
191 |
by (ALLGOALS (simp_tac term_ss)); |
0 | 192 |
by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems)))); |
757 | 193 |
qed "term_ind"; |
0 | 194 |