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 val fix_ind = result(); |
19 qed "fix_ind"; |
20 |
20 |
21 (*** Inclusive Predicates ***) |
21 (*** Inclusive Predicates ***) |
22 |
22 |
23 val prems = goalw Fix.thy [INCL_def] |
23 val prems = goalw Fix.thy [INCL_def] |
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 val inclXH = result(); |
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 val inclI = result(); |
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 val inclD = result(); |
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 val inclE = result(); |
42 qed "inclE"; |
43 |
43 |
44 |
44 |
45 (*** Lemmas for Inclusive Predicates ***) |
45 (*** Lemmas for Inclusive Predicates ***) |
46 |
46 |
47 goal Fix.thy "INCL(%x.~ a(x) [= t)"; |
47 goal Fix.thy "INCL(%x.~ a(x) [= t)"; |
51 by (etac contrapos 1); |
51 by (etac contrapos 1); |
52 by (rtac po_trans 1); |
52 by (rtac po_trans 1); |
53 by (assume_tac 2); |
53 by (assume_tac 2); |
54 by (rtac (napplyBzero RS ssubst) 1); |
54 by (rtac (napplyBzero RS ssubst) 1); |
55 by (rtac po_cong 1 THEN rtac po_bot 1); |
55 by (rtac po_cong 1 THEN rtac po_bot 1); |
56 val npo_INCL = result(); |
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 val conj_INCL = result(); |
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 val all_INCL = result(); |
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 val ball_INCL = result(); |
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 val eq_INCL = result(); |
73 qed "eq_INCL"; |
74 |
74 |
75 (*** Derivation of Reachability Condition ***) |
75 (*** Derivation of Reachability Condition ***) |
76 |
76 |
77 (* Fixed points of idgen *) |
77 (* Fixed points of idgen *) |
78 |
78 |
79 goal Fix.thy "idgen(fix(idgen)) = fix(idgen)"; |
79 goal Fix.thy "idgen(fix(idgen)) = fix(idgen)"; |
80 by (rtac (fixB RS sym) 1); |
80 by (rtac (fixB RS sym) 1); |
81 val fix_idgenfp = result(); |
81 qed "fix_idgenfp"; |
82 |
82 |
83 goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x"; |
83 goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x"; |
84 by (simp_tac term_ss 1); |
84 by (simp_tac term_ss 1); |
85 by (rtac (term_case RS allI) 1); |
85 by (rtac (term_case RS allI) 1); |
86 by (ALLGOALS (simp_tac term_ss)); |
86 by (ALLGOALS (simp_tac term_ss)); |
87 val id_idgenfp = result(); |
87 qed "id_idgenfp"; |
88 |
88 |
89 (* All fixed points are lam-expressions *) |
89 (* All fixed points are lam-expressions *) |
90 |
90 |
91 val [prem] = goal Fix.thy "idgen(d) = d ==> d = lam x.?f(x)"; |
91 val [prem] = goal Fix.thy "idgen(d) = d ==> d = lam x.?f(x)"; |
92 by (rtac (prem RS subst) 1); |
92 by (rtac (prem RS subst) 1); |
93 by (rewtac idgen_def); |
93 by (rewtac idgen_def); |
94 by (rtac refl 1); |
94 by (rtac refl 1); |
95 val idgenfp_lam = result(); |
95 qed "idgenfp_lam"; |
96 |
96 |
97 (* Lemmas for rewriting fixed points of idgen *) |
97 (* Lemmas for rewriting fixed points of idgen *) |
98 |
98 |
99 val prems = goalw Fix.thy [idgen_def] |
99 val prems = goalw Fix.thy [idgen_def] |
100 "[| a = b; a ` t = u |] ==> b ` t = u"; |
100 "[| a = b; a ` t = u |] ==> b ` t = u"; |
101 by (simp_tac (term_ss addsimps (prems RL [sym])) 1); |
101 by (simp_tac (term_ss addsimps (prems RL [sym])) 1); |
102 val l_lemma= result(); |
102 qed "l_lemma"; |
103 |
103 |
104 val idgen_lemmas = |
104 val idgen_lemmas = |
105 let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s |
105 let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s |
106 (fn [prem] => [rtac (prem RS l_lemma) 1,simp_tac term_ss 1]) |
106 (fn [prem] => [rtac (prem RS l_lemma) 1,simp_tac term_ss 1]) |
107 in map mk_thm |
107 in map mk_thm |
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 (rtac (p2 RS cond_eta RS ssubst) 1); |
120 by (rtac (p2 RS cond_eta RS ssubst) 1); |
121 by (rtac (p3 RS cond_eta RS ssubst) 1); |
121 by (rtac (p3 RS cond_eta RS ssubst) 1); |
122 by (rtac (p1 RS (po_lam RS iffD2)) 1); |
122 by (rtac (p1 RS (po_lam RS iffD2)) 1); |
123 val po_eta = result(); |
123 qed "po_eta"; |
124 |
124 |
125 val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)"; |
125 val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)"; |
126 by (rtac (prem RS subst) 1); |
126 by (rtac (prem RS subst) 1); |
127 by (rtac refl 1); |
127 by (rtac refl 1); |
128 val po_eta_lemma = result(); |
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 val lemma1 = result(); |
138 qed "lemma1"; |
139 |
139 |
140 val [prem] = goal Fix.thy |
140 val [prem] = goal Fix.thy |
141 "idgen(d) = d ==> fix(idgen) [= d"; |
141 "idgen(d) = d ==> fix(idgen) [= d"; |
142 by (rtac (allI RS po_eta) 1); |
142 by (rtac (allI RS po_eta) 1); |
143 by (rtac (lemma1 RSN(2,po_coinduct)) 1); |
143 by (rtac (lemma1 RSN(2,po_coinduct)) 1); |
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 val fix_least_idgen = result(); |
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 val lemma2 = result(); |
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 val id_least_idgen = result(); |
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 val reachability = result(); |
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 val id_apply = result(); |
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) |] ==> \ |