62 |
62 |
63 (* Do not use prove_goal because the result is ?ed which leads to divergence |
63 (* Do not use prove_goal because the result is ?ed which leads to divergence |
64 when submitted as an argument to SIMP_THM *) |
64 when submitted as an argument to SIMP_THM *) |
65 (* |
65 (* |
66 local |
66 local |
67 val thm = trivial(Sign.read_cterm(sign_of LCF.thy) |
67 val thm = trivial(read_cterm(sign_of LCF.thy) |
68 ("<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)",propT)); |
68 ("<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)",propT)); |
69 val tac = EVERY1[rtac lfp_is_FIX, simp_tac ss, |
69 val tac = EVERY1[rtac lfp_is_FIX, simp_tac ss, |
70 strip_tac, simp_tac (LCF_ss addsimps [PROD_less]), |
70 strip_tac, simp_tac (LCF_ss addsimps [PROD_less]), |
71 rtac conjI, rtac least_FIX, etac subst, rtac (FST RS sym), |
71 rtac conjI, rtac least_FIX, etac subst, rtac (FST RS sym), |
72 rtac least_FIX, etac subst, rtac (SND RS sym)]; |
72 rtac least_FIX, etac subst, rtac (SND RS sym)]; |