equal
deleted
inserted
replaced
63 val less_anti_sym = prove_goal thy "[| x << y; y << x |] ==> x=y" |
63 val less_anti_sym = prove_goal thy "[| x << y; y << x |] ==> x=y" |
64 (fn prems => [rewrite_goals_tac[eq_def], |
64 (fn prems => [rewrite_goals_tac[eq_def], |
65 REPEAT(rstac(conjI::prems)1)]); |
65 REPEAT(rstac(conjI::prems)1)]); |
66 |
66 |
67 val ext = prove_goal thy |
67 val ext = prove_goal thy |
68 "(!!x::'a::cpo. f(x)=g(x)::'b::cpo) ==> (%x.f(x))=(%x.g(x))" |
68 "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))" |
69 (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI, |
69 (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI, |
70 prem RS eq_imp_less1, |
70 prem RS eq_imp_less1, |
71 prem RS eq_imp_less2]1)]); |
71 prem RS eq_imp_less2]1)]); |
72 |
72 |
73 val cong = prove_goal thy "[| f=g; x=y |] ==> f(x)=g(y)" |
73 val cong = prove_goal thy "[| f=g; x=y |] ==> f(x)=g(y)" |