# HG changeset patch # User wenzelm # Date 1222521636 -7200 # Node ID 73b380ba174373a48efa24de73e94ae442d52c78 # Parent f66ca5b982b4c081ce778a4857ba5c16f3d180f3 proper transfer of theorems that involve classes being instantiated here; diff -r f66ca5b982b4 -r 73b380ba1743 src/HOLCF/Tools/pcpodef_package.ML --- a/src/HOLCF/Tools/pcpodef_package.ML Sat Sep 27 14:26:06 2008 +0200 +++ b/src/HOLCF/Tools/pcpodef_package.ML Sat Sep 27 15:20:36 2008 +0200 @@ -107,19 +107,21 @@ fun make_cpo admissible (type_def, less_def, set_def) theory = let val admissible' = fold_rule (the_list set_def) admissible; - val cpo_thms = [type_def, less_def, admissible']; + val cpo_thms = map (Thm.transfer theory) [type_def, less_def, admissible']; + val theory' = theory + |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"]) + (Tactic.rtac (typedef_cpo OF cpo_thms) 1); + val cpo_thms' = map (Thm.transfer theory') cpo_thms; in - theory - |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"]) - (Tactic.rtac (typedef_cpo OF cpo_thms) 1) + theory' |> Sign.add_path name |> PureThy.add_thms ([(("adm_" ^ name, admissible'), []), - (("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []), - (("cont_" ^ Abs_name, cont_Abs OF cpo_thms), []), - (("lub_" ^ name, typedef_lub OF cpo_thms), []), - (("thelub_" ^ name, typedef_thelub OF cpo_thms), []), - (("compact_" ^ name, typedef_compact OF cpo_thms), [])]) + (("cont_" ^ Rep_name, cont_Rep OF cpo_thms'), []), + (("cont_" ^ Abs_name, cont_Abs OF cpo_thms'), []), + (("lub_" ^ name, typedef_lub OF cpo_thms'), []), + (("thelub_" ^ name, typedef_thelub OF cpo_thms'), []), + (("compact_" ^ name, typedef_compact OF cpo_thms'), [])]) |> snd |> Sign.parent_path end; @@ -127,19 +129,21 @@ fun make_pcpo UUmem (type_def, less_def, set_def) theory = let val UUmem' = fold_rule (the_list set_def) UUmem; - val pcpo_thms = [type_def, less_def, UUmem']; + val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UUmem']; + val theory' = theory + |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"]) + (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1); + val pcpo_thms' = map (Thm.transfer theory') pcpo_thms; in - theory - |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"]) - (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1) + theory' |> Sign.add_path name |> PureThy.add_thms - ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []), - ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []), - ((Rep_name ^ "_strict_iff", Rep_strict_iff OF pcpo_thms), []), - ((Abs_name ^ "_strict_iff", Abs_strict_iff OF pcpo_thms), []), - ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []), - ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), []) + ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms'), []), + ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms'), []), + ((Rep_name ^ "_strict_iff", Rep_strict_iff OF pcpo_thms'), []), + ((Abs_name ^ "_strict_iff", Abs_strict_iff OF pcpo_thms'), []), + ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms'), []), + ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms'), []) ]) |> snd |> Sign.parent_path