# HG changeset patch # User huffman # Date 1122395127 -7200 # Node ID 6df23e3180fb62cd34028b12981d35faaca4c474 # Parent d0fdc7b9a33fbb5abdc1f55c61867fef63d6cb44 removed duplicated code; generate new lub and thelub lemmas for new cpo types diff -r d0fdc7b9a33f -r 6df23e3180fb src/HOLCF/pcpodef_package.ML --- a/src/HOLCF/pcpodef_package.ML Tue Jul 26 18:24:29 2005 +0200 +++ b/src/HOLCF/pcpodef_package.ML Tue Jul 26 18:25:27 2005 +0200 @@ -26,7 +26,9 @@ val typedef_po = thm "typedef_po"; val typedef_cpo = thm "typedef_cpo"; -val typedef_pcpo = thm "typedef_pcpo_UU"; +val typedef_pcpo = thm "typedef_pcpo"; +val typedef_lub = thm "typedef_lub"; +val typedef_thelub = thm "typedef_thelub"; val cont_Rep = thm "typedef_cont_Rep"; val cont_Abs = thm "typedef_cont_Abs"; val Rep_strict = thm "typedef_Rep_strict"; @@ -104,6 +106,42 @@ (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1) |> rpair (type_definition, less_definition, set_def)); + fun make_cpo admissible (theory, defs as (type_def, less_def, set_def)) = + let + val admissible' = option_fold_rule set_def admissible; + val cpo_thms = [type_def, less_def, admissible']; + val (theory', _) = + theory + |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.cpo"]) + (Tactic.rtac (typedef_cpo OF cpo_thms) 1) + |> Theory.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), [])]) + |>> Theory.parent_path; + in (theory', defs) end; + + fun make_pcpo UUmem (theory, defs as (type_def, less_def, set_def)) = + let + val UUmem' = option_fold_rule set_def UUmem; + val pcpo_thms = [type_def, less_def, UUmem']; + val (theory', _) = + theory + |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.pcpo"]) + (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1) + |> Theory.add_path name + |> PureThy.add_thms + ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []), + ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []), + ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []), + ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), []) + ]) + |>> Theory.parent_path; + in (theory', defs) end; + fun pcpodef_result (theory, UUmem_admissible) = let val UUmem = UUmem_admissible RS conjunct1; @@ -111,30 +149,9 @@ in theory |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1) - |> (fn (theory', (type_definition, less_definition, set_def)) => - let - val admissible' = option_fold_rule set_def admissible; - val UUmem' = option_fold_rule set_def UUmem; - val cpo_thms = [type_definition, less_definition, admissible']; - val pcpo_thms = [type_definition, less_definition, UUmem']; - val (theory'', _) = - theory' - |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.cpo"]) - (Tactic.rtac (typedef_cpo OF cpo_thms) 1) - |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.pcpo"]) - (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1) - |> Theory.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), []), - ((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []), - ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []), - ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []), - ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), []) - ]) - |>> Theory.parent_path; - in (theory'', type_definition) end) + |> make_cpo admissible + |> make_pcpo UUmem + |> (fn (theory', (type_def, _, _)) => (theory', type_def)) end; fun cpodef_result (theory, nonempty_admissible) = @@ -144,21 +161,8 @@ in theory |> make_po (Tactic.rtac nonempty 1) - |> (fn (theory', (type_definition, less_definition, set_def)) => - let - val admissible' = option_fold_rule set_def admissible; - val cpo_thms = [type_definition, less_definition, admissible']; - val (theory'', _) = - theory' - |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.cpo"]) - (Tactic.rtac (typedef_cpo OF cpo_thms) 1) - |> Theory.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), [])]) - |>> Theory.parent_path; - in (theory'', type_definition) end) + |> make_cpo admissible + |> (fn (theory', (type_def, _, _)) => (theory', type_def)) end; in (goal, if pcpo then pcpodef_result else cpodef_result) end