--- a/src/HOL/Nominal/nominal_datatype.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Nov 13 06:24:31 2009 +0100
@@ -569,7 +569,7 @@
thy3
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = false, verbose = false, kind = Thm.internalK,
+ {quiet_mode = false, verbose = false, kind = "",
alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
@@ -1513,7 +1513,7 @@
thy10
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = "",
alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Nov 13 06:24:31 2009 +0100
@@ -156,7 +156,7 @@
thy0
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = "",
alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Nov 13 06:24:31 2009 +0100
@@ -175,7 +175,7 @@
thy1
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = "",
alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
--- a/src/HOL/Tools/Function/function_core.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Fri Nov 13 06:24:31 2009 +0100
@@ -460,7 +460,7 @@
|> Inductive.add_inductive_i
{quiet_mode = true,
verbose = ! trace,
- kind = Thm.internalK,
+ kind = "",
alt_name = Binding.empty,
coind = false,
no_elim = false,
@@ -519,7 +519,7 @@
$ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
|> Syntax.check_term lthy
in
- LocalTheory.define Thm.internalK
+ LocalTheory.define ""
((Binding.name (function_name fname), mixfix),
((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
end
--- a/src/HOL/Tools/Function/mutual.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Fri Nov 13 06:24:31 2009 +0100
@@ -146,7 +146,7 @@
fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
let
val ((f, (_, f_defthm)), lthy') =
- LocalTheory.define Thm.internalK
+ LocalTheory.define ""
((Binding.name fname, mixfix),
((Binding.conceal (Binding.name (fname ^ "_def")), []),
Term.subst_bound (fsum, f_def))) lthy
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Nov 13 06:24:31 2009 +0100
@@ -355,7 +355,7 @@
thy
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = false, verbose = false, kind = Thm.internalK,
+ {quiet_mode = false, verbose = false, kind = "",
alt_name = Binding.empty, coind = false, no_elim = false,
no_ind = false, skip_mono = false, fork_mono = false}
(map (fn (s, T) =>
--- a/src/HOL/Tools/inductive.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Nov 13 06:24:31 2009 +0100
@@ -663,7 +663,7 @@
val ((rec_const, (_, fp_def)), lthy') = lthy
|> LocalTheory.conceal
- |> LocalTheory.define Thm.internalK
+ |> LocalTheory.define ""
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
fold_rev lambda params
@@ -686,13 +686,13 @@
end) (cnames_syn ~~ cs);
val (consts_defs, lthy'') = lthy'
|> LocalTheory.conceal
- |> fold_map (LocalTheory.define Thm.internalK) specs
+ |> fold_map (LocalTheory.define "") specs
||> LocalTheory.restore_naming lthy';
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
val ((_, [mono']), lthy''') =
- LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
+ LocalTheory.note "" (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
list_comb (rec_const, params), preds, argTs, bs, xs)
--- a/src/HOL/Tools/inductive_set.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML Fri Nov 13 06:24:31 2009 +0100
@@ -485,7 +485,7 @@
(* define inductive sets using previously defined predicates *)
val (defs, lthy2) = lthy1
|> LocalTheory.conceal (* FIXME ?? *)
- |> fold_map (LocalTheory.define Thm.internalK)
+ |> fold_map (LocalTheory.define "")
(map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
fold_rev lambda params (HOLogic.Collect_const U $
HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
--- a/src/HOL/Tools/recdef.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/HOL/Tools/recdef.ML Fri Nov 13 06:24:31 2009 +0100
@@ -263,7 +263,7 @@
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in
- Specification.theorem Thm.internalK NONE (K I)
+ Specification.theorem "" NONE (K I)
(Binding.conceal (Binding.name bname), atts) []
(Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
end;
--- a/src/HOLCF/Tools/pcpodef.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML Fri Nov 13 06:24:31 2009 +0100
@@ -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;
--- a/src/Pure/General/markup.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/Pure/General/markup.ML Fri Nov 13 06:24:31 2009 +0100
@@ -14,7 +14,6 @@
val name: string -> T -> T
val bindingN: string val binding: string -> T
val kindN: string
- val internalK: string
val entityN: string val entity: string -> T
val defN: string
val refN: string
@@ -154,8 +153,6 @@
val kindN = "kind";
-val internalK = "internal";
-
(* formal entities *)
--- a/src/Pure/Isar/expression.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/Pure/Isar/expression.ML Fri Nov 13 06:24:31 2009 +0100
@@ -682,7 +682,7 @@
val (_, thy'') =
thy'
|> Sign.mandatory_path (Binding.name_of abinding)
- |> PureThy.note_thmss Thm.internalK
+ |> PureThy.note_thmss ""
[((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
||> Sign.restore_naming thy';
in (SOME statement, SOME intro, axioms, thy'') end;
@@ -696,7 +696,7 @@
val (_, thy'''') =
thy'''
|> Sign.mandatory_path (Binding.name_of binding)
- |> PureThy.note_thmss Thm.internalK
+ |> PureThy.note_thmss ""
[((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
((Binding.conceal (Binding.name axiomsN), []),
[(map (Drule.standard o Element.conclude_witness) axioms, [])])]
@@ -713,7 +713,7 @@
fold_map (fn (a, spec) => fn axs =>
let val (ps, qs) = chop (length spec) axs
in ((a, [(ps, [])]), qs) end) asms axms
- |> apfst (curry Notes Thm.assumptionK)
+ |> apfst (curry Notes "")
| assumes_to_notes e axms = (e, axms);
fun defines_to_notes thy (Defines defs) =
@@ -755,7 +755,7 @@
val notes =
if is_some asm then
- [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
+ [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
[([Assumption.assume (cterm_of thy' (the asm))],
[(Attrib.internal o K) Locale.witness_add])])])]
else [];
--- a/src/Pure/Isar/locale.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/Pure/Isar/locale.ML Fri Nov 13 06:24:31 2009 +0100
@@ -518,7 +518,7 @@
fun add_decls add loc decl =
ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
- add_thmss loc Thm.internalK
+ add_thmss loc ""
[((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
[([Drule.dummy_thm], [])])];
--- a/src/Pure/Isar/proof_context.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Nov 13 06:24:31 2009 +0100
@@ -1126,7 +1126,7 @@
in
ctxt2
|> auto_bind_facts (flat propss)
- |> note_thmss Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
+ |> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss)
end;
in
--- a/src/Pure/Isar/proof_display.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML Fri Nov 13 06:24:31 2009 +0100
@@ -91,7 +91,7 @@
in
fun print_results do_print ctxt ((kind, name), facts) =
- if not do_print orelse kind = "" orelse kind = Thm.internalK then ()
+ if not do_print orelse kind = "" then ()
else if name = "" then
Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
else Pretty.writeln
--- a/src/Pure/Isar/specification.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/Pure/Isar/specification.ML Fri Nov 13 06:24:31 2009 +0100
@@ -172,7 +172,7 @@
#>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
(*facts*)
- val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
+ val (facts, thy') = axioms_thy |> PureThy.note_thmss ""
(Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
val _ =
@@ -329,8 +329,9 @@
val (facts, goal_ctxt) = elems_ctxt
|> (snd o ProofContext.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (obtains ~~ propp)
- |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
- [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
+ |-> (fn ths =>
+ ProofContext.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
+ #2 #> pair ths);
in ((prems, stmt, SOME facts), goal_ctxt) end);
structure TheoremHook = Generic_Data
@@ -372,8 +373,7 @@
end;
in
goal_ctxt
- |> ProofContext.note_thmss Thm.assumptionK
- [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
+ |> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem_i before_qed after_qed' (map snd stmt)
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
--- a/src/Pure/Thy/thm_deps.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/Pure/Thy/thm_deps.ML Fri Nov 13 06:24:31 2009 +0100
@@ -79,9 +79,7 @@
NONE => I
| SOME grp => Inttab.update (grp, ()))) thms Inttab.empty;
val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') =>
- if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
- (Thm.get_kind th) andalso not concealed andalso is_unused (a, th)
- then
+ if not concealed andalso is_unused (a, th) then
(case group of
NONE => ((a, th) :: thms, grps')
| SOME grp =>
--- a/src/Pure/drule.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/Pure/drule.ML Fri Nov 13 06:24:31 2009 +0100
@@ -710,13 +710,11 @@
val protectI =
store_thm (Binding.conceal (Binding.name "protectI"))
- (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
+ (standard (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)));
val protectD =
store_thm (Binding.conceal (Binding.name "protectD"))
- (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim prop_def (Thm.assume (protect A)))));
+ (standard (Thm.equal_elim prop_def (Thm.assume (protect A))));
val protect_cong =
store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
@@ -734,8 +732,7 @@
val termI =
store_thm (Binding.conceal (Binding.name "termI"))
- (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
+ (standard (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))));
fun mk_term ct =
let
@@ -764,15 +761,14 @@
val sort_constraintI =
store_thm (Binding.conceal (Binding.name "sort_constraintI"))
- (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T))));
+ (standard (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T)));
val sort_constraint_eq =
store_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
- (Thm.kind_rule Thm.internalK (standard
+ (standard
(Thm.equal_intr
(Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
- (implies_intr_list [A, C] (Thm.assume A)))));
+ (implies_intr_list [A, C] (Thm.assume A))));
end;
--- a/src/Pure/more_thm.ML Thu Nov 12 21:14:42 2009 +0100
+++ b/src/Pure/more_thm.ML Fri Nov 13 06:24:31 2009 +0100
@@ -84,14 +84,11 @@
val has_name_hint: thm -> bool
val get_name_hint: thm -> string
val put_name_hint: string -> thm -> thm
- val axiomK: string
- val assumptionK: string
val definitionK: string
val theoremK: string
val generatedK : string
val lemmaK: string
val corollaryK: string
- val internalK: string
val get_kind: thm -> string
val kind_rule: string -> thm -> thm
val kind: string -> attribute
@@ -414,14 +411,11 @@
(* theorem kinds *)
-val axiomK = "axiom";
-val assumptionK = "assumption";
val definitionK = "definition";
val theoremK = "theorem";
val generatedK = "generatedK"
val lemmaK = "lemma";
val corollaryK = "corollary";
-val internalK = Markup.internalK;
fun get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);