equal
deleted
inserted
replaced
52 Goal |
52 Goal |
53 "[| mono f; finite U; f U = U |] \ |
53 "[| mono f; finite U; f U = U |] \ |
54 \ ==> lfp f = fst(while (%(A,fA). A~=fA) (%(A,fA). (fA, f fA)) ({},f{}))"; |
54 \ ==> lfp f = fst(while (%(A,fA). A~=fA) (%(A,fA). (fA, f fA)) ({},f{}))"; |
55 by(res_inst_tac [("P","%(A,B).(A <= U & B = f A & A <= B & B <= lfp f)")] |
55 by(res_inst_tac [("P","%(A,B).(A <= U & B = f A & A <= B & B <= lfp f)")] |
56 while_rule 1); |
56 while_rule 1); |
57 by(stac lfp_Tarski 1); |
57 by(stac lfp_unfold 1); |
58 ba 1; |
58 ba 1; |
59 by(Clarsimp_tac 1); |
59 by(Clarsimp_tac 1); |
60 by(blast_tac (claset() addDs [monoD]) 1); |
60 by(blast_tac (claset() addDs [monoD]) 1); |
61 by(fast_tac (claset() addSIs [lfp_lowerbound] addss simpset()) 1); |
61 by(fast_tac (claset() addSIs [lfp_lowerbound] addss simpset()) 1); |
62 by(res_inst_tac [("r","((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) Int \ |
62 by(res_inst_tac [("r","((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) Int \ |
65 by(blast_tac (claset() addIs |
65 by(blast_tac (claset() addIs |
66 [wf_finite_psubset,Int_lower2 RSN (2,wf_subset)]) 1); |
66 [wf_finite_psubset,Int_lower2 RSN (2,wf_subset)]) 1); |
67 by(clarsimp_tac (claset(),simpset() addsimps |
67 by(clarsimp_tac (claset(),simpset() addsimps |
68 [inv_image_def,finite_psubset_def,order_less_le]) 1); |
68 [inv_image_def,finite_psubset_def,order_less_le]) 1); |
69 by(blast_tac (claset() addSIs [finite_Diff] addDs [monoD]) 1); |
69 by(blast_tac (claset() addSIs [finite_Diff] addDs [monoD]) 1); |
70 by(stac lfp_Tarski 1); |
70 by(stac lfp_unfold 1); |
71 ba 1; |
71 ba 1; |
72 by(asm_simp_tac (simpset() addsimps [monoD]) 1); |
72 by(asm_simp_tac (simpset() addsimps [monoD]) 1); |
73 qed "lfp_conv_while"; |
73 qed "lfp_conv_while"; |
74 |
74 |
75 (*** An example; requires integers |
75 (*** An example; requires integers |