improved ML interface to pcpodef
authorhuffman
Thu Nov 12 14:31:11 2009 -0800 (2009-11-12)
changeset 33646d2f3104ca3d2
parent 33645 562635ab559b
child 33647 053ac8080c11
improved ML interface to pcpodef
src/HOLCF/Tools/pcpodef.ML
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Wed Nov 11 10:15:32 2009 -0800
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Thu Nov 12 14:31:11 2009 -0800
     1.3 @@ -7,18 +7,31 @@
     1.4  
     1.5  signature PCPODEF =
     1.6  sig
     1.7 +  type cpo_info =
     1.8 +    { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
     1.9 +      lub: thm, thelub: thm, compact: thm }
    1.10 +  type pcpo_info =
    1.11 +    { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
    1.12 +      Rep_defined: thm, Abs_defined: thm }
    1.13 +
    1.14 +  val add_podef: bool -> binding option -> binding * string list * mixfix ->
    1.15 +    term -> (binding * binding) option -> tactic -> theory ->
    1.16 +    (Typedef.info * thm) * theory
    1.17 +  val add_cpodef: bool -> binding option -> binding * string list * mixfix ->
    1.18 +    term -> (binding * binding) option -> tactic * tactic -> theory ->
    1.19 +    (Typedef.info * cpo_info) * theory
    1.20    val add_pcpodef: bool -> binding option -> binding * string list * mixfix ->
    1.21 -    term -> (binding * binding) option -> tactic -> theory -> theory
    1.22 -  val add_cpodef: bool -> binding option -> binding * string list * mixfix ->
    1.23 -    term -> (binding * binding) option -> tactic -> theory -> theory
    1.24 +    term -> (binding * binding) option -> tactic * tactic -> theory ->
    1.25 +    (Typedef.info * cpo_info * pcpo_info) * theory
    1.26 +
    1.27 +  val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    1.28 +    * (binding * binding) option -> theory -> Proof.state
    1.29 +  val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
    1.30 +    * (binding * binding) option -> theory -> Proof.state
    1.31    val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    1.32      * (binding * binding) option -> theory -> Proof.state
    1.33    val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
    1.34      * (binding * binding) option -> theory -> Proof.state
    1.35 -  val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    1.36 -    * (binding * binding) option -> theory -> Proof.state
    1.37 -  val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
    1.38 -    * (binding * binding) option -> theory -> Proof.state
    1.39  end;
    1.40  
    1.41  structure Pcpodef :> PCPODEF =
    1.42 @@ -26,22 +39,124 @@
    1.43  
    1.44  (** type definitions **)
    1.45  
    1.46 -(* prepare_cpodef *)
    1.47 +type cpo_info =
    1.48 +  { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
    1.49 +    lub: thm, thelub: thm, compact: thm }
    1.50  
    1.51 -fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
    1.52 +type pcpo_info =
    1.53 +  { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
    1.54 +    Rep_defined: thm, Abs_defined: thm }
    1.55 +
    1.56 +(* building terms *)
    1.57  
    1.58  fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
    1.59  fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
    1.60  
    1.61 -fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
    1.62 +fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
    1.63 +
    1.64 +(* manipulating theorems *)
    1.65 +
    1.66 +fun fold_adm_mem thm NONE = thm
    1.67 +  | fold_adm_mem thm (SOME set_def) =
    1.68 +    let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
    1.69 +    in rule OF [set_def, thm] end;
    1.70 +
    1.71 +fun fold_UU_mem thm NONE = thm
    1.72 +  | fold_UU_mem thm (SOME set_def) =
    1.73 +    let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
    1.74 +    in rule OF [set_def, thm] end;
    1.75 +
    1.76 +(* proving class instances *)
    1.77 +
    1.78 +fun prove_cpo
    1.79 +      (name: binding)
    1.80 +      (newT: typ)
    1.81 +      (Rep_name: binding, Abs_name: binding)
    1.82 +      (type_definition: thm)  (* type_definition Rep Abs A *)
    1.83 +      (set_def: thm option)   (* A == set *)
    1.84 +      (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
    1.85 +      (admissible: thm)       (* adm (%x. x : set) *)
    1.86 +      (thy: theory)
    1.87 +    =
    1.88 +  let
    1.89 +    val admissible' = fold_adm_mem admissible set_def;
    1.90 +    val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
    1.91 +    val (full_tname, Ts) = dest_Type newT;
    1.92 +    val lhs_sorts = map (snd o dest_TFree) Ts;
    1.93 +    val thy2 =
    1.94 +      thy
    1.95 +      |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
    1.96 +          (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
    1.97 +    val cpo_thms' = map (Thm.transfer thy2) cpo_thms;
    1.98 +    fun make thm = Drule.standard (thm OF cpo_thms');
    1.99 +    val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) =
   1.100 +      thy2
   1.101 +      |> Sign.add_path (Binding.name_of name)
   1.102 +      |> PureThy.add_thms
   1.103 +        ([((Binding.prefix_name "adm_" name, admissible'), []),
   1.104 +          ((Binding.prefix_name "cont_" Rep_name, make @{thm typedef_cont_Rep}), []),
   1.105 +          ((Binding.prefix_name "cont_" Abs_name, make @{thm typedef_cont_Abs}), []),
   1.106 +          ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []),
   1.107 +          ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []),
   1.108 +          ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])])
   1.109 +      ||> Sign.parent_path;
   1.110 +    val cpo_info : cpo_info =
   1.111 +      { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
   1.112 +        cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact };
   1.113 +  in
   1.114 +    (cpo_info, thy3)
   1.115 +  end;
   1.116 +
   1.117 +fun prove_pcpo
   1.118 +      (name: binding)
   1.119 +      (newT: typ)
   1.120 +      (Rep_name: binding, Abs_name: binding)
   1.121 +      (type_definition: thm)  (* type_definition Rep Abs A *)
   1.122 +      (set_def: thm option)   (* A == set *)
   1.123 +      (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
   1.124 +      (UU_mem: thm)           (* UU : set *)
   1.125 +      (thy: theory)
   1.126 +    =
   1.127 +  let
   1.128 +    val UU_mem' = fold_UU_mem UU_mem set_def;
   1.129 +    val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
   1.130 +    val (full_tname, Ts) = dest_Type newT;
   1.131 +    val lhs_sorts = map (snd o dest_TFree) Ts;
   1.132 +    val thy2 = thy
   1.133 +      |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
   1.134 +        (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
   1.135 +    val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms;
   1.136 +    fun make thm = Drule.standard (thm OF pcpo_thms');
   1.137 +    val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff,
   1.138 +          Rep_defined, Abs_defined], thy3) =
   1.139 +      thy2
   1.140 +      |> Sign.add_path (Binding.name_of name)
   1.141 +      |> PureThy.add_thms
   1.142 +        ([((Binding.suffix_name "_strict" Rep_name, make @{thm typedef_Rep_strict}), []),
   1.143 +          ((Binding.suffix_name "_strict" Abs_name, make @{thm typedef_Abs_strict}), []),
   1.144 +          ((Binding.suffix_name "_strict_iff" Rep_name, make @{thm typedef_Rep_strict_iff}), []),
   1.145 +          ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []),
   1.146 +          ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []),
   1.147 +          ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])])
   1.148 +      ||> Sign.parent_path;
   1.149 +    val pcpo_info =
   1.150 +      { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
   1.151 +        Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,
   1.152 +        Rep_defined = Rep_defined, Abs_defined = Abs_defined };
   1.153 +  in
   1.154 +    (pcpo_info, thy3)
   1.155 +  end;
   1.156 +
   1.157 +(* prepare_cpodef *)
   1.158 +
   1.159 +fun declare_type_name a =
   1.160 +  Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
   1.161 +
   1.162 +fun prepare prep_term _ name (t, vs, mx) raw_set opt_morphs thy =
   1.163    let
   1.164      val _ = Theory.requires thy "Pcpodef" "pcpodefs";
   1.165      val ctxt = ProofContext.init thy;
   1.166  
   1.167 -    val full = Sign.full_name thy;
   1.168 -    val full_name = full name;
   1.169 -    val bname = Binding.name_of name;
   1.170 -
   1.171      (*rhs*)
   1.172      val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
   1.173      val setT = Term.fastype_of set;
   1.174 @@ -49,155 +164,171 @@
   1.175      val oldT = HOLogic.dest_setT setT handle TYPE _ =>
   1.176        error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
   1.177  
   1.178 -    (*goal*)
   1.179 -    val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
   1.180 +    (*lhs*)
   1.181 +    val defS = Sign.defaultS thy;
   1.182 +    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
   1.183 +    val lhs_sorts = map snd lhs_tfrees;
   1.184 +    val tname = Binding.map_name (Syntax.type_name mx) t;
   1.185 +    val full_tname = Sign.full_name thy tname;
   1.186 +    val newT = Type (full_tname, map TFree lhs_tfrees);
   1.187 +
   1.188 +    val morphs = opt_morphs
   1.189 +      |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
   1.190 +  in
   1.191 +    (newT, oldT, set, morphs, lhs_sorts)
   1.192 +  end
   1.193 +
   1.194 +fun add_podef def opt_name typ set opt_morphs tac thy =
   1.195 +  let
   1.196 +    val name = the_default (#1 typ) opt_name;
   1.197 +    val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy
   1.198 +      |> Typedef.add_typedef def opt_name typ set opt_morphs tac;
   1.199 +    val oldT = #rep_type info;
   1.200 +    val newT = #abs_type info;
   1.201 +    val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
   1.202 +
   1.203 +    val RepC = Const (Rep_name, newT --> oldT);
   1.204 +    val below_def = Logic.mk_equals (below_const newT,
   1.205 +      Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
   1.206 +    val lthy3 = thy2
   1.207 +      |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
   1.208 +    val below_def' = Syntax.check_term lthy3 below_def;
   1.209 +    val ((_, (_, below_definition')), lthy4) = lthy3
   1.210 +      |> Specification.definition (NONE,
   1.211 +          ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
   1.212 +    val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
   1.213 +    val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
   1.214 +    val thy5 = lthy4
   1.215 +      |> Class.prove_instantiation_instance
   1.216 +          (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
   1.217 +      |> LocalTheory.exit_global;
   1.218 +  in ((info, below_definition), thy5) end;
   1.219 +
   1.220 +fun prepare_cpodef
   1.221 +      (prep_term: Proof.context -> 'a -> term)
   1.222 +      (def: bool)
   1.223 +      (name: binding)
   1.224 +      (typ: binding * string list * mixfix)
   1.225 +      (raw_set: 'a)
   1.226 +      (opt_morphs: (binding * binding) option)
   1.227 +      (thy: theory)
   1.228 +    : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
   1.229 +  let
   1.230 +    val (newT, oldT, set, morphs as (Rep_name, Abs_name), lhs_sorts) =
   1.231 +      prepare prep_term def name typ raw_set opt_morphs thy;
   1.232 +
   1.233      val goal_nonempty =
   1.234        HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
   1.235      val goal_admissible =
   1.236        HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
   1.237  
   1.238 -    (*lhs*)
   1.239 -    val defS = Sign.defaultS thy;
   1.240 -    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
   1.241 -    val lhs_sorts = map snd lhs_tfrees;
   1.242 -
   1.243 -    val tname = Binding.map_name (Syntax.type_name mx) t;
   1.244 -    val full_tname = full tname;
   1.245 -    val newT = Type (full_tname, map TFree lhs_tfrees);
   1.246 -
   1.247 -    val (Rep_name, Abs_name) =
   1.248 -      (case opt_morphs of
   1.249 -        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
   1.250 -      | SOME morphs => morphs);
   1.251 -    val RepC = Const (full Rep_name, newT --> oldT);
   1.252 -    fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
   1.253 -    val below_def = Logic.mk_equals (belowC newT,
   1.254 -      Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
   1.255 -
   1.256 -    fun make_po tac thy1 =
   1.257 +    fun cpodef_result nonempty admissible thy =
   1.258        let
   1.259 -        val ((_, {type_definition, set_def, ...}), thy2) = thy1
   1.260 -          |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
   1.261 -        val lthy3 = thy2
   1.262 -          |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
   1.263 -        val below_def' = Syntax.check_term lthy3 below_def;
   1.264 -        val ((_, (_, below_definition')), lthy4) = lthy3
   1.265 -          |> Specification.definition (NONE,
   1.266 -              ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
   1.267 -        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
   1.268 -        val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
   1.269 -        val thy5 = lthy4
   1.270 -          |> Class.prove_instantiation_instance
   1.271 -              (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
   1.272 -          |> LocalTheory.exit_global;
   1.273 -      in ((type_definition, below_definition, set_def), thy5) end;
   1.274 -
   1.275 -    fun make_cpo admissible (type_def, below_def, set_def) theory =
   1.276 -      let
   1.277 -        (* FIXME fold_rule might fold user input inintentionally *)
   1.278 -        val admissible' = fold_rule (the_list set_def) admissible;
   1.279 -        val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
   1.280 -        val theory' = theory
   1.281 -          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
   1.282 -            (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
   1.283 -        val cpo_thms' = map (Thm.transfer theory') cpo_thms;
   1.284 -        fun make thm = Drule.standard (thm OF cpo_thms');
   1.285 +        val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
   1.286 +          |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
   1.287 +        val (cpo_info, thy3) = thy2
   1.288 +          |> prove_cpo name newT morphs type_definition set_def below_def admissible;
   1.289        in
   1.290 -        theory'
   1.291 -        |> Sign.add_path (Binding.name_of name)
   1.292 -        |> PureThy.add_thms
   1.293 -          ([((Binding.prefix_name "adm_" name, admissible'), []),
   1.294 -            ((Binding.prefix_name "cont_" Rep_name, make @{thm typedef_cont_Rep}), []),
   1.295 -            ((Binding.prefix_name "cont_" Abs_name, make @{thm typedef_cont_Abs}), []),
   1.296 -            ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []),
   1.297 -            ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []),
   1.298 -            ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])])
   1.299 -        |> snd
   1.300 -        |> Sign.parent_path
   1.301 +        ((info, cpo_info), thy3)
   1.302        end;
   1.303 -
   1.304 -    fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
   1.305 -      let
   1.306 -        (* FIXME fold_rule might fold user input inintentionally *)
   1.307 -        val UU_mem' = fold_rule (the_list set_def) UU_mem;
   1.308 -        val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
   1.309 -        val theory' = theory
   1.310 -          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
   1.311 -            (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
   1.312 -        val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
   1.313 -        fun make thm = Drule.standard (thm OF pcpo_thms');
   1.314 -      in
   1.315 -        theory'
   1.316 -        |> Sign.add_path (Binding.name_of name)
   1.317 -        |> PureThy.add_thms
   1.318 -          ([((Binding.suffix_name "_strict" Rep_name, make @{thm typedef_Rep_strict}), []),
   1.319 -            ((Binding.suffix_name "_strict" Abs_name, make @{thm typedef_Abs_strict}), []),
   1.320 -            ((Binding.suffix_name "_strict_iff" Rep_name, make @{thm typedef_Rep_strict_iff}), []),
   1.321 -            ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []),
   1.322 -            ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []),
   1.323 -            ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])])
   1.324 -        |> snd
   1.325 -        |> Sign.parent_path
   1.326 -      end;
   1.327 -
   1.328 -    fun pcpodef_result UU_mem admissible =
   1.329 -      make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
   1.330 -      #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
   1.331 -
   1.332 -    fun cpodef_result nonempty admissible =
   1.333 -      make_po (Tactic.rtac nonempty 1)
   1.334 -      #-> make_cpo admissible;
   1.335    in
   1.336 -    if pcpo
   1.337 -    then (goal_UU_mem, goal_admissible, pcpodef_result)
   1.338 -    else (goal_nonempty, goal_admissible, cpodef_result)
   1.339 +    (goal_nonempty, goal_admissible, cpodef_result)
   1.340    end
   1.341    handle ERROR msg =>
   1.342      cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
   1.343  
   1.344 +fun prepare_pcpodef
   1.345 +      (prep_term: Proof.context -> 'a -> term)
   1.346 +      (def: bool)
   1.347 +      (name: binding)
   1.348 +      (typ: binding * string list * mixfix)
   1.349 +      (raw_set: 'a)
   1.350 +      (opt_morphs: (binding * binding) option)
   1.351 +      (thy: theory)
   1.352 +    : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
   1.353 +  let
   1.354 +    val (newT, oldT, set, morphs as (Rep_name, Abs_name), lhs_sorts) =
   1.355 +      prepare prep_term def name typ raw_set opt_morphs thy;
   1.356 +
   1.357 +    val goal_UU_mem =
   1.358 +      HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
   1.359 +
   1.360 +    val goal_admissible =
   1.361 +      HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
   1.362 +
   1.363 +    fun pcpodef_result UU_mem admissible thy =
   1.364 +      let
   1.365 +        val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
   1.366 +        val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
   1.367 +          |> add_podef def (SOME name) typ set opt_morphs tac;
   1.368 +        val (cpo_info, thy3) = thy2
   1.369 +          |> prove_cpo name newT morphs type_definition set_def below_def admissible;
   1.370 +        val (pcpo_info, thy4) = thy3
   1.371 +          |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem;
   1.372 +      in
   1.373 +        ((info, cpo_info, pcpo_info), thy4)
   1.374 +      end;
   1.375 +  in
   1.376 +    (goal_UU_mem, goal_admissible, pcpodef_result)
   1.377 +  end
   1.378 +  handle ERROR msg =>
   1.379 +    cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name));
   1.380 +
   1.381  
   1.382  (* tactic interface *)
   1.383  
   1.384 -local
   1.385 +fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
   1.386 +  let
   1.387 +    val name = the_default (#1 typ) opt_name;
   1.388 +    val (goal1, goal2, cpodef_result) =
   1.389 +      prepare_cpodef Syntax.check_term def name typ set opt_morphs thy;
   1.390 +    val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
   1.391 +      handle ERROR msg => cat_error msg
   1.392 +        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
   1.393 +    val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
   1.394 +      handle ERROR msg => cat_error msg
   1.395 +        ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
   1.396 +  in cpodef_result thm1 thm2 thy end;
   1.397  
   1.398 -fun gen_add_pcpodef pcpo def opt_name typ set opt_morphs tac thy =
   1.399 +fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
   1.400    let
   1.401      val name = the_default (#1 typ) opt_name;
   1.402      val (goal1, goal2, pcpodef_result) =
   1.403 -      prepare_pcpodef Syntax.check_term pcpo def name typ set opt_morphs thy;
   1.404 -    val thm1 = Goal.prove_global thy [] [] goal1 (K tac)
   1.405 +      prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy;
   1.406 +    val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
   1.407        handle ERROR msg => cat_error msg
   1.408          ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
   1.409 -    val thm2 = Goal.prove_global thy [] [] goal2 (K tac)
   1.410 +    val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
   1.411        handle ERROR msg => cat_error msg
   1.412          ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
   1.413    in pcpodef_result thm1 thm2 thy end;
   1.414  
   1.415 -in
   1.416 -
   1.417 -val add_pcpodef = gen_add_pcpodef true;
   1.418 -val add_cpodef = gen_add_pcpodef false;
   1.419 -
   1.420 -end;
   1.421  
   1.422  (* proof interface *)
   1.423  
   1.424  local
   1.425  
   1.426 -fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
   1.427 +fun gen_cpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy =
   1.428    let
   1.429      val (goal1, goal2, make_result) =
   1.430 -      prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
   1.431 -    fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
   1.432 +      prepare_cpodef prep_term def name typ set opt_morphs thy;
   1.433 +    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
   1.434 +  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
   1.435 +
   1.436 +fun gen_pcpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy =
   1.437 +  let
   1.438 +    val (goal1, goal2, make_result) =
   1.439 +      prepare_pcpodef prep_term def name typ set opt_morphs thy;
   1.440 +    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
   1.441    in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
   1.442  
   1.443  in
   1.444  
   1.445 -fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
   1.446 -fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
   1.447 +fun cpodef_proof x = gen_cpodef_proof Syntax.check_term x;
   1.448 +fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term x;
   1.449  
   1.450 -fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
   1.451 -fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
   1.452 +fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term x;
   1.453 +fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term x;
   1.454  
   1.455  end;
   1.456