9 open Fix; |
9 open Fix; |
10 |
10 |
11 (*** Fixed Point Induction ***) |
11 (*** Fixed Point Induction ***) |
12 |
12 |
13 val [base,step,incl] = goalw Fix.thy [INCL_def] |
13 val [base,step,incl] = goalw Fix.thy [INCL_def] |
14 "[| P(bot); !!x.P(x) ==> P(f(x)); INCL(P) |] ==> P(fix(f))"; |
14 "[| P(bot); !!x. P(x) ==> P(f(x)); INCL(P) |] ==> P(fix(f))"; |
15 by (rtac (incl RS spec RS mp) 1); |
15 by (rtac (incl RS spec RS mp) 1); |
16 by (rtac (Nat_ind RS ballI) 1 THEN atac 1); |
16 by (rtac (Nat_ind RS ballI) 1 THEN atac 1); |
17 by (ALLGOALS (simp_tac term_ss)); |
17 by (ALLGOALS (simp_tac term_ss)); |
18 by (REPEAT (ares_tac [base,step] 1)); |
18 by (REPEAT (ares_tac [base,step] 1)); |
19 qed "fix_ind"; |
19 qed "fix_ind"; |
24 "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))"; |
24 "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))"; |
25 by (rtac iff_refl 1); |
25 by (rtac iff_refl 1); |
26 qed "inclXH"; |
26 qed "inclXH"; |
27 |
27 |
28 val prems = goal Fix.thy |
28 val prems = goal Fix.thy |
29 "[| !!f.ALL n:Nat.P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x.P(x))"; |
29 "[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))"; |
30 by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1); |
30 by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1); |
31 qed "inclI"; |
31 qed "inclI"; |
32 |
32 |
33 val incl::prems = goal Fix.thy |
33 val incl::prems = goal Fix.thy |
34 "[| INCL(P); !!n.n:Nat ==> P(f^n`bot) |] ==> P(fix(f))"; |
34 "[| INCL(P); !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))"; |
35 by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] |
35 by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] |
36 @ prems)) 1); |
36 @ prems)) 1); |
37 qed "inclD"; |
37 qed "inclD"; |
38 |
38 |
39 val incl::prems = goal Fix.thy |
39 val incl::prems = goal Fix.thy |
40 "[| INCL(P); (ALL n:Nat.P(f^n`bot))-->P(fix(f)) ==> R |] ==> R"; |
40 "[| INCL(P); (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R"; |
41 by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1); |
41 by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1); |
42 qed "inclE"; |
42 qed "inclE"; |
43 |
43 |
44 |
44 |
45 (*** Lemmas for Inclusive Predicates ***) |
45 (*** Lemmas for Inclusive Predicates ***) |
53 by (assume_tac 2); |
53 by (assume_tac 2); |
54 by (stac napplyBzero 1); |
54 by (stac napplyBzero 1); |
55 by (rtac po_cong 1 THEN rtac po_bot 1); |
55 by (rtac po_cong 1 THEN rtac po_bot 1); |
56 qed "npo_INCL"; |
56 qed "npo_INCL"; |
57 |
57 |
58 val prems = goal Fix.thy "[| INCL(P); INCL(Q) |] ==> INCL(%x.P(x) & Q(x))"; |
58 val prems = goal Fix.thy "[| INCL(P); INCL(Q) |] ==> INCL(%x. P(x) & Q(x))"; |
59 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; |
59 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; |
60 qed "conj_INCL"; |
60 qed "conj_INCL"; |
61 |
61 |
62 val prems = goal Fix.thy "[| !!a.INCL(P(a)) |] ==> INCL(%x.ALL a.P(a,x))"; |
62 val prems = goal Fix.thy "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))"; |
63 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; |
63 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; |
64 qed "all_INCL"; |
64 qed "all_INCL"; |
65 |
65 |
66 val prems = goal Fix.thy "[| !!a.a:A ==> INCL(P(a)) |] ==> INCL(%x.ALL a:A.P(a,x))"; |
66 val prems = goal Fix.thy "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))"; |
67 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; |
67 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; |
68 qed "ball_INCL"; |
68 qed "ball_INCL"; |
69 |
69 |
70 goal Fix.thy "INCL(%x.a(x) = (b(x)::'a::prog))"; |
70 goal Fix.thy "INCL(%x. a(x) = (b(x)::'a::prog))"; |
71 by (simp_tac (term_ss addsimps [eq_iff]) 1); |
71 by (simp_tac (term_ss addsimps [eq_iff]) 1); |
72 by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1)); |
72 by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1)); |
73 qed "eq_INCL"; |
73 qed "eq_INCL"; |
74 |
74 |
75 (*** Derivation of Reachability Condition ***) |
75 (*** Derivation of Reachability Condition ***) |
107 in map mk_thm |
107 in map mk_thm |
108 [ "idgen(d) = d ==> d ` bot = bot", |
108 [ "idgen(d) = d ==> d ` bot = bot", |
109 "idgen(d) = d ==> d ` true = true", |
109 "idgen(d) = d ==> d ` true = true", |
110 "idgen(d) = d ==> d ` false = false", |
110 "idgen(d) = d ==> d ` false = false", |
111 "idgen(d) = d ==> d ` <a,b> = <d ` a,d ` b>", |
111 "idgen(d) = d ==> d ` <a,b> = <d ` a,d ` b>", |
112 "idgen(d) = d ==> d ` (lam x.f(x)) = lam x.d ` f(x)"] |
112 "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)"] |
113 end; |
113 end; |
114 |
114 |
115 (* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points |
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 *) |
116 of idgen and hence are they same *) |
117 |
117 |
118 val [p1,p2,p3] = goal CCL.thy |
118 val [p1,p2,p3] = goal CCL.thy |
119 "[| ALL x.t ` x [= u ` x; EX f.t=lam x.f(x); EX f.u=lam x.f(x) |] ==> t [= u"; |
119 "[| ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x) |] ==> t [= u"; |
120 by (stac (p2 RS cond_eta) 1); |
120 by (stac (p2 RS cond_eta) 1); |
121 by (stac (p3 RS cond_eta) 1); |
121 by (stac (p3 RS cond_eta) 1); |
122 by (rtac (p1 RS (po_lam RS iffD2)) 1); |
122 by (rtac (p1 RS (po_lam RS iffD2)) 1); |
123 qed "po_eta"; |
123 qed "po_eta"; |
124 |
124 |
127 by (rtac refl 1); |
127 by (rtac refl 1); |
128 qed "po_eta_lemma"; |
128 qed "po_eta_lemma"; |
129 |
129 |
130 val [prem] = goal Fix.thy |
130 val [prem] = goal Fix.thy |
131 "idgen(d) = d ==> \ |
131 "idgen(d) = d ==> \ |
132 \ {p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t & b = d ` t)} <= \ |
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)})"; |
133 \ POgen({p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)})"; |
134 by (REPEAT (step_tac term_cs 1)); |
134 by (REPEAT (step_tac term_cs 1)); |
135 by (term_case_tac "t" 1); |
135 by (term_case_tac "t" 1); |
136 by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas))))); |
136 by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas))))); |
137 by (ALLGOALS (fast_tac set_cs)); |
137 by (ALLGOALS (fast_tac set_cs)); |
138 qed "lemma1"; |
138 qed "lemma1"; |
144 by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); |
144 by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); |
145 qed "fix_least_idgen"; |
145 qed "fix_least_idgen"; |
146 |
146 |
147 val [prem] = goal Fix.thy |
147 val [prem] = goal Fix.thy |
148 "idgen(d) = d ==> \ |
148 "idgen(d) = d ==> \ |
149 \ {p.EX a b.p=<a,b> & b = d ` a} <= POgen({p.EX a b.p=<a,b> & b = d ` a})"; |
149 \ {p. EX a b. p=<a,b> & b = d ` a} <= POgen({p. EX a b. p=<a,b> & b = d ` a})"; |
150 by (REPEAT (step_tac term_cs 1)); |
150 by (REPEAT (step_tac term_cs 1)); |
151 by (term_case_tac "a" 1); |
151 by (term_case_tac "a" 1); |
152 by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas))))); |
152 by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas))))); |
153 by (ALLGOALS (fast_tac set_cs)); |
153 by (ALLGOALS (fast_tac set_cs)); |
154 qed "lemma2"; |
154 qed "lemma2"; |
155 |
155 |
156 val [prem] = goal Fix.thy |
156 val [prem] = goal Fix.thy |
157 "idgen(d) = d ==> lam x.x [= d"; |
157 "idgen(d) = d ==> lam x. x [= d"; |
158 by (rtac (allI RS po_eta) 1); |
158 by (rtac (allI RS po_eta) 1); |
159 by (rtac (lemma2 RSN(2,po_coinduct)) 1); |
159 by (rtac (lemma2 RSN(2,po_coinduct)) 1); |
160 by (simp_tac term_ss 1); |
160 by (simp_tac term_ss 1); |
161 by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); |
161 by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); |
162 qed "id_least_idgen"; |
162 qed "id_least_idgen"; |
163 |
163 |
164 goal Fix.thy "fix(idgen) = lam x.x"; |
164 goal Fix.thy "fix(idgen) = lam x. x"; |
165 by (fast_tac (term_cs addIs [eq_iff RS iffD2, |
165 by (fast_tac (term_cs addIs [eq_iff RS iffD2, |
166 id_idgenfp RS fix_least_idgen, |
166 id_idgenfp RS fix_least_idgen, |
167 fix_idgenfp RS id_least_idgen]) 1); |
167 fix_idgenfp RS id_least_idgen]) 1); |
168 qed "reachability"; |
168 qed "reachability"; |
169 |
169 |
170 (********) |
170 (********) |
171 |
171 |
172 val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t"; |
172 val [prem] = goal Fix.thy "f = lam x. x ==> f`t = t"; |
173 by (rtac (prem RS sym RS subst) 1); |
173 by (rtac (prem RS sym RS subst) 1); |
174 by (rtac applyB 1); |
174 by (rtac applyB 1); |
175 qed "id_apply"; |
175 qed "id_apply"; |
176 |
176 |
177 val prems = goal Fix.thy |
177 val prems = goal Fix.thy |
178 "[| P(bot); P(true); P(false); \ |
178 "[| P(bot); P(true); P(false); \ |
179 \ !!x y.[| P(x); P(y) |] ==> P(<x,y>); \ |
179 \ !!x y.[| P(x); P(y) |] ==> P(<x,y>); \ |
180 \ !!u.(!!x.P(u(x))) ==> P(lam x.u(x)); INCL(P) |] ==> \ |
180 \ !!u.(!!x. P(u(x))) ==> P(lam x. u(x)); INCL(P) |] ==> \ |
181 \ P(t)"; |
181 \ P(t)"; |
182 by (rtac (reachability RS id_apply RS subst) 1); |
182 by (rtac (reachability RS id_apply RS subst) 1); |
183 by (res_inst_tac [("x","t")] spec 1); |
183 by (res_inst_tac [("x","t")] spec 1); |
184 by (rtac fix_ind 1); |
184 by (rtac fix_ind 1); |
185 by (rewtac idgen_def); |
185 by (rewtac idgen_def); |