# HG changeset patch # User bulwahn # Date 1258089871 -3600 # Node ID feaf3627a844096d59508fbf71cbe009e5a15fa3 # Parent d7836058f52b5b32772f6df9717f921a6a8f2975# Parent 555e5358b8c9bc5939628895ba6333a6810c296d merged diff -r d7836058f52b -r feaf3627a844 src/HOL/Nominal/nominal_datatype.ML --- 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)) diff -r d7836058f52b -r feaf3627a844 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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)) diff -r d7836058f52b -r feaf3627a844 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- 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') [] diff -r d7836058f52b -r feaf3627a844 src/HOL/Tools/Function/function_core.ML --- 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 diff -r d7836058f52b -r feaf3627a844 src/HOL/Tools/Function/mutual.ML --- 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 diff -r d7836058f52b -r feaf3627a844 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- 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) => diff -r d7836058f52b -r feaf3627a844 src/HOL/Tools/inductive.ML --- 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) diff -r d7836058f52b -r feaf3627a844 src/HOL/Tools/inductive_set.ML --- 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)))))) diff -r d7836058f52b -r feaf3627a844 src/HOL/Tools/recdef.ML --- 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; diff -r d7836058f52b -r feaf3627a844 src/HOLCF/Tools/pcpodef.ML --- 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; diff -r d7836058f52b -r feaf3627a844 src/Pure/General/markup.ML --- 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 *) diff -r d7836058f52b -r feaf3627a844 src/Pure/Isar/expression.ML --- 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 []; diff -r d7836058f52b -r feaf3627a844 src/Pure/Isar/locale.ML --- 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], [])])]; diff -r d7836058f52b -r feaf3627a844 src/Pure/Isar/proof_context.ML --- 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 diff -r d7836058f52b -r feaf3627a844 src/Pure/Isar/proof_display.ML --- 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 diff -r d7836058f52b -r feaf3627a844 src/Pure/Isar/specification.ML --- 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) diff -r d7836058f52b -r feaf3627a844 src/Pure/Thy/thm_deps.ML --- 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 => diff -r d7836058f52b -r feaf3627a844 src/Pure/drule.ML --- 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; diff -r d7836058f52b -r feaf3627a844 src/Pure/more_thm.ML --- 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);