--- a/src/HOLCF/Tools/pcpodef.ML Thu Nov 12 20:33:26 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML Thu Nov 12 14:31:29 2009 -0800
@@ -7,14 +7,31 @@
signature PCPODEF =
sig
+ type cpo_info =
+ { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
+ lub: thm, thelub: thm, compact: thm }
+ type pcpo_info =
+ { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
+ Rep_defined: thm, Abs_defined: thm }
+
+ val add_podef: bool -> binding option -> binding * string list * mixfix ->
+ term -> (binding * binding) option -> tactic -> theory ->
+ (Typedef.info * thm) * theory
+ val add_cpodef: bool -> binding option -> binding * string list * mixfix ->
+ term -> (binding * binding) option -> tactic * tactic -> theory ->
+ (Typedef.info * cpo_info) * theory
+ val add_pcpodef: bool -> binding option -> binding * string list * mixfix ->
+ term -> (binding * binding) option -> tactic * tactic -> theory ->
+ (Typedef.info * cpo_info * pcpo_info) * theory
+
+ val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
+ * (binding * binding) option -> theory -> Proof.state
+ val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
+ * (binding * binding) option -> theory -> Proof.state
val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
* (binding * binding) option -> theory -> Proof.state
val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
* (binding * binding) option -> theory -> Proof.state
- val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
- * (binding * binding) option -> theory -> Proof.state
- val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
- * (binding * binding) option -> theory -> Proof.state
end;
structure Pcpodef :> PCPODEF =
@@ -22,22 +39,124 @@
(** type definitions **)
-(* prepare_cpodef *)
+type cpo_info =
+ { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
+ lub: thm, thelub: thm, compact: thm }
-fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
+type pcpo_info =
+ { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
+ Rep_defined: thm, Abs_defined: thm }
+
+(* building terms *)
fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
-fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
+fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
+
+(* manipulating theorems *)
+
+fun fold_adm_mem thm NONE = thm
+ | fold_adm_mem thm (SOME set_def) =
+ let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
+ in rule OF [set_def, thm] end;
+
+fun fold_UU_mem thm NONE = thm
+ | fold_UU_mem thm (SOME set_def) =
+ let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
+ in rule OF [set_def, thm] end;
+
+(* proving class instances *)
+
+fun prove_cpo
+ (name: binding)
+ (newT: typ)
+ (Rep_name: binding, Abs_name: binding)
+ (type_definition: thm) (* type_definition Rep Abs A *)
+ (set_def: thm option) (* A == set *)
+ (below_def: thm) (* op << == %x y. Rep x << Rep y *)
+ (admissible: thm) (* adm (%x. x : set) *)
+ (thy: theory)
+ =
+ let
+ val admissible' = fold_adm_mem admissible set_def;
+ val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
+ val (full_tname, Ts) = dest_Type newT;
+ val lhs_sorts = map (snd o dest_TFree) Ts;
+ val thy2 =
+ thy
+ |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
+ (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
+ val cpo_thms' = map (Thm.transfer thy2) cpo_thms;
+ fun make thm = Drule.standard (thm OF cpo_thms');
+ val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) =
+ thy2
+ |> Sign.add_path (Binding.name_of name)
+ |> PureThy.add_thms
+ ([((Binding.prefix_name "adm_" name, admissible'), []),
+ ((Binding.prefix_name "cont_" Rep_name, make @{thm typedef_cont_Rep}), []),
+ ((Binding.prefix_name "cont_" Abs_name, make @{thm typedef_cont_Abs}), []),
+ ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []),
+ ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []),
+ ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])])
+ ||> Sign.parent_path;
+ val cpo_info : cpo_info =
+ { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
+ cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact };
+ in
+ (cpo_info, thy3)
+ end;
+
+fun prove_pcpo
+ (name: binding)
+ (newT: typ)
+ (Rep_name: binding, Abs_name: binding)
+ (type_definition: thm) (* type_definition Rep Abs A *)
+ (set_def: thm option) (* A == set *)
+ (below_def: thm) (* op << == %x y. Rep x << Rep y *)
+ (UU_mem: thm) (* UU : set *)
+ (thy: theory)
+ =
+ let
+ val UU_mem' = fold_UU_mem UU_mem set_def;
+ val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
+ val (full_tname, Ts) = dest_Type newT;
+ val lhs_sorts = map (snd o dest_TFree) Ts;
+ val thy2 = thy
+ |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
+ (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
+ val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms;
+ fun make thm = Drule.standard (thm OF pcpo_thms');
+ val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff,
+ Rep_defined, Abs_defined], thy3) =
+ thy2
+ |> Sign.add_path (Binding.name_of name)
+ |> PureThy.add_thms
+ ([((Binding.suffix_name "_strict" Rep_name, make @{thm typedef_Rep_strict}), []),
+ ((Binding.suffix_name "_strict" Abs_name, make @{thm typedef_Abs_strict}), []),
+ ((Binding.suffix_name "_strict_iff" Rep_name, make @{thm typedef_Rep_strict_iff}), []),
+ ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []),
+ ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []),
+ ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])])
+ ||> Sign.parent_path;
+ val pcpo_info =
+ { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
+ Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,
+ Rep_defined = Rep_defined, Abs_defined = Abs_defined };
+ in
+ (pcpo_info, thy3)
+ end;
+
+(* prepare_cpodef *)
+
+fun declare_type_name a =
+ Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
+
+fun prepare prep_term _ name (t, vs, mx) raw_set opt_morphs thy =
let
val _ = Theory.requires thy "Pcpodef" "pcpodefs";
val ctxt = ProofContext.init thy;
- val full = Sign.full_name thy;
- val full_name = full name;
- val bname = Binding.name_of name;
-
(*rhs*)
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
val setT = Term.fastype_of set;
@@ -45,129 +164,171 @@
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
- (*goal*)
- val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
+ (*lhs*)
+ val defS = Sign.defaultS thy;
+ val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
+ val lhs_sorts = map snd lhs_tfrees;
+ val tname = Binding.map_name (Syntax.type_name mx) t;
+ val full_tname = Sign.full_name thy tname;
+ val newT = Type (full_tname, map TFree lhs_tfrees);
+
+ val morphs = opt_morphs
+ |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
+ in
+ (newT, oldT, set, morphs, lhs_sorts)
+ end
+
+fun add_podef def opt_name typ set opt_morphs tac thy =
+ let
+ val name = the_default (#1 typ) opt_name;
+ val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy
+ |> Typedef.add_typedef def opt_name typ set opt_morphs tac;
+ val oldT = #rep_type info;
+ val newT = #abs_type info;
+ val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
+
+ val RepC = Const (Rep_name, newT --> oldT);
+ val below_def = Logic.mk_equals (below_const newT,
+ Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
+ val lthy3 = thy2
+ |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
+ val below_def' = Syntax.check_term lthy3 below_def;
+ val ((_, (_, below_definition')), lthy4) = lthy3
+ |> Specification.definition (NONE,
+ ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
+ val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
+ val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
+ val thy5 = lthy4
+ |> Class.prove_instantiation_instance
+ (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
+ |> LocalTheory.exit_global;
+ in ((info, below_definition), thy5) end;
+
+fun prepare_cpodef
+ (prep_term: Proof.context -> 'a -> term)
+ (def: bool)
+ (name: binding)
+ (typ: binding * string list * mixfix)
+ (raw_set: 'a)
+ (opt_morphs: (binding * binding) option)
+ (thy: theory)
+ : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
+ let
+ val (newT, oldT, set, morphs as (Rep_name, Abs_name), lhs_sorts) =
+ prepare prep_term def name typ raw_set opt_morphs thy;
+
val goal_nonempty =
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
val goal_admissible =
HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
- (*lhs*)
- val defS = Sign.defaultS thy;
- val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
- val lhs_sorts = map snd lhs_tfrees;
-
- val tname = Binding.map_name (Syntax.type_name mx) t;
- val full_tname = full tname;
- val newT = Type (full_tname, map TFree lhs_tfrees);
-
- val (Rep_name, Abs_name) =
- (case opt_morphs of
- NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
- | SOME morphs => morphs);
- val RepC = Const (full Rep_name, newT --> oldT);
- fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
- val below_def = Logic.mk_equals (belowC newT,
- Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
-
- fun make_po tac thy1 =
+ fun cpodef_result nonempty admissible thy =
let
- val ((_, {type_definition, set_def, ...}), thy2) = thy1
- |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
- val lthy3 = thy2
- |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
- val below_def' = Syntax.check_term lthy3 below_def;
- val ((_, (_, below_definition')), lthy4) = lthy3
- |> Specification.definition (NONE,
- ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
- val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
- val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
- val thy5 = lthy4
- |> Class.prove_instantiation_instance
- (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
- |> LocalTheory.exit_global;
- in ((type_definition, below_definition, set_def), thy5) end;
-
- fun make_cpo admissible (type_def, below_def, set_def) theory =
- let
- (* FIXME fold_rule might fold user input inintentionally *)
- val admissible' = fold_rule (the_list set_def) admissible;
- val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
- val theory' = theory
- |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
- (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
- val cpo_thms' = map (Thm.transfer theory') cpo_thms;
+ val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
+ |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
+ val (cpo_info, thy3) = thy2
+ |> prove_cpo name newT morphs type_definition set_def below_def admissible;
in
- theory'
- |> Sign.add_path (Binding.name_of name)
- |> PureThy.add_thms
- ([((Binding.prefix_name "adm_" name, admissible'), []),
- ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
- ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
- ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
- ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
- ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
- |> snd
- |> Sign.parent_path
+ ((info, cpo_info), thy3)
end;
-
- fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
- let
- (* FIXME fold_rule might fold user input inintentionally *)
- val UU_mem' = fold_rule (the_list set_def) UU_mem;
- val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
- val theory' = theory
- |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
- (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
- val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
- in
- theory'
- |> Sign.add_path (Binding.name_of name)
- |> PureThy.add_thms
- ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
- ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
- ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
- ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
- ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
- ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
- |> snd
- |> Sign.parent_path
- end;
-
- fun pcpodef_result UU_mem admissible =
- make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
- #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
-
- fun cpodef_result nonempty admissible =
- make_po (Tactic.rtac nonempty 1)
- #-> make_cpo admissible;
in
- if pcpo
- then (goal_UU_mem, goal_admissible, pcpodef_result)
- else (goal_nonempty, goal_admissible, cpodef_result)
+ (goal_nonempty, goal_admissible, cpodef_result)
end
handle ERROR msg =>
cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
+fun prepare_pcpodef
+ (prep_term: Proof.context -> 'a -> term)
+ (def: bool)
+ (name: binding)
+ (typ: binding * string list * mixfix)
+ (raw_set: 'a)
+ (opt_morphs: (binding * binding) option)
+ (thy: theory)
+ : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
+ let
+ val (newT, oldT, set, morphs as (Rep_name, Abs_name), lhs_sorts) =
+ prepare prep_term def name typ raw_set opt_morphs thy;
+
+ val goal_UU_mem =
+ HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
+
+ val goal_admissible =
+ HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+
+ fun pcpodef_result UU_mem admissible thy =
+ let
+ val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
+ val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
+ |> add_podef def (SOME name) typ set opt_morphs tac;
+ val (cpo_info, thy3) = thy2
+ |> prove_cpo name newT morphs type_definition set_def below_def admissible;
+ val (pcpo_info, thy4) = thy3
+ |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem;
+ in
+ ((info, cpo_info, pcpo_info), thy4)
+ end;
+ in
+ (goal_UU_mem, goal_admissible, pcpodef_result)
+ end
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name));
+
+
+(* tactic interface *)
+
+fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
+ let
+ val name = the_default (#1 typ) opt_name;
+ val (goal1, goal2, cpodef_result) =
+ prepare_cpodef Syntax.check_term def name typ set opt_morphs thy;
+ val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
+ handle ERROR msg => cat_error msg
+ ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
+ val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
+ handle ERROR msg => cat_error msg
+ ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
+ in cpodef_result thm1 thm2 thy end;
+
+fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
+ let
+ val name = the_default (#1 typ) opt_name;
+ val (goal1, goal2, pcpodef_result) =
+ prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy;
+ val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
+ handle ERROR msg => cat_error msg
+ ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
+ val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
+ handle ERROR msg => cat_error msg
+ ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
+ in pcpodef_result thm1 thm2 thy end;
+
(* proof interface *)
local
-fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
+fun gen_cpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy =
let
val (goal1, goal2, make_result) =
- prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
- fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
+ prepare_cpodef prep_term def name typ set opt_morphs thy;
+ fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
+ in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
+
+fun gen_pcpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy =
+ let
+ val (goal1, goal2, make_result) =
+ prepare_pcpodef prep_term def name typ set opt_morphs thy;
+ fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
in
-fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
-fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
+fun cpodef_proof x = gen_cpodef_proof Syntax.check_term x;
+fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term x;
-fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
-fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
+fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term x;
+fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term x;
end;