# HG changeset patch # User huffman # Date 1117146242 -7200 # Node ID a92ee283393858fc1ef2d1fe69b2bfa4b9049f4a # Parent cdcbf5a7f38df350f06e43e196dae991db482adf Use TypedefPcpo theorem for po instance diff -r cdcbf5a7f38d -r a92ee2833938 src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Fri May 27 00:16:18 2005 +0200 +++ b/src/HOLCF/Cfun.thy Fri May 27 00:24:02 2005 +0200 @@ -8,7 +8,7 @@ header {* The type of continuous functions *} theory Cfun -imports Cont +imports TypedefPcpo begin defaultsort cpo @@ -80,20 +80,8 @@ defs (overloaded) less_cfun_def: "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )" -lemma refl_less_cfun: "(f::'a->'b) << f" -by (unfold less_cfun_def, rule refl_less) - -lemma antisym_less_cfun: - "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2" -by (unfold less_cfun_def, rule Rep_CFun_inject[THEN iffD1], rule antisym_less) - -lemma trans_less_cfun: - "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3" -by (unfold less_cfun_def, rule trans_less) - instance "->" :: (cpo, cpo) po -by intro_classes - (assumption | rule refl_less_cfun antisym_less_cfun trans_less_cfun)+ +by (rule typedef_po [OF type_definition_CFun less_cfun_def]) text {* for compatibility with old HOLCF-Version *} lemma inst_cfun_po: "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)"