--- a/CONTRIBUTORS Fri Nov 13 11:33:33 2009 +0000
+++ b/CONTRIBUTORS Fri Nov 13 11:34:05 2009 +0000
@@ -6,6 +6,10 @@
Contributions to this Isabelle version
--------------------------------------
+
+* November 2009: Stefan Berghofer, Lukas Bulwahn, TUM
+ A tabled implementation of the reflexive transitive closure
+
* November 2009: Lukas Bulwahn, TUM
Predicate Compiler: a compiler for inductive predicates to equational specfications
--- a/NEWS Fri Nov 13 11:33:33 2009 +0000
+++ b/NEWS Fri Nov 13 11:34:05 2009 +0000
@@ -37,6 +37,8 @@
*** HOL ***
+* A tabled implementation of the reflexive transitive closure
+
* New commands "code_pred" and "values" to invoke the predicate compiler
and to enumerate values of inductive predicates.
--- a/src/HOL/IsaMakefile Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/IsaMakefile Fri Nov 13 11:34:05 2009 +0000
@@ -382,8 +382,9 @@
Library/Order_Relation.thy Library/Nested_Environment.thy \
Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML \
Library/Library/document/root.tex Library/Library/document/root.bib \
- Library/While_Combinator.thy Library/Product_ord.thy \
- Library/Char_nat.thy Library/Char_ord.thy Library/Option_ord.thy \
+ Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
+ Library/Product_ord.thy Library/Char_nat.thy \
+ Library/Char_ord.thy Library/Option_ord.thy \
Library/Sublist_Order.thy Library/List_lexord.thy \
Library/Coinductive_List.thy Library/AssocList.thy \
Library/Formal_Power_Series.thy Library/Binomial.thy \
--- a/src/HOL/Library/Library.thy Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Library/Library.thy Fri Nov 13 11:34:05 2009 +0000
@@ -51,6 +51,7 @@
SML_Quickcheck
State_Monad
Sum_Of_Squares
+ Transitive_Closure_Table
Univ_Poly
While_Combinator
Word
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri Nov 13 11:34:05 2009 +0000
@@ -0,0 +1,230 @@
+(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
+
+header {* A tabled implementation of the reflexive transitive closure *}
+
+theory Transitive_Closure_Table
+imports Main
+begin
+
+inductive rtrancl_path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ base: "rtrancl_path r x [] x"
+| step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z"
+
+lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\<exists>xs. rtrancl_path r x xs y)"
+proof
+ assume "r\<^sup>*\<^sup>* x y"
+ then show "\<exists>xs. rtrancl_path r x xs y"
+ proof (induct rule: converse_rtranclp_induct)
+ case 1
+ have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
+ then show ?case ..
+ next
+ case (2 x z)
+ from `\<exists>xs. rtrancl_path r z xs y`
+ obtain xs where "rtrancl_path r z xs y" ..
+ with `r x z` have "rtrancl_path r x (z # xs) y"
+ by (rule rtrancl_path.step)
+ then show ?case ..
+ qed
+next
+ assume "\<exists>xs. rtrancl_path r x xs y"
+ then obtain xs where "rtrancl_path r x xs y" ..
+ then show "r\<^sup>*\<^sup>* x y"
+ proof induct
+ case (base x)
+ show ?case by (rule rtranclp.rtrancl_refl)
+ next
+ case (step x y ys z)
+ from `r x y` `r\<^sup>*\<^sup>* y z` show ?case
+ by (rule converse_rtranclp_into_rtranclp)
+ qed
+qed
+
+lemma rtrancl_path_trans:
+ assumes xy: "rtrancl_path r x xs y"
+ and yz: "rtrancl_path r y ys z"
+ shows "rtrancl_path r x (xs @ ys) z" using xy yz
+proof (induct arbitrary: z)
+ case (base x)
+ then show ?case by simp
+next
+ case (step x y xs)
+ then have "rtrancl_path r y (xs @ ys) z"
+ by simp
+ with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"
+ by (rule rtrancl_path.step)
+ then show ?case by simp
+qed
+
+lemma rtrancl_path_appendE:
+ assumes xz: "rtrancl_path r x (xs @ y # ys) z"
+ obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz
+proof (induct xs arbitrary: x)
+ case Nil
+ then have "rtrancl_path r x (y # ys) z" by simp
+ then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
+ by cases auto
+ from xy have "rtrancl_path r x [y] y"
+ by (rule rtrancl_path.step [OF _ rtrancl_path.base])
+ then have "rtrancl_path r x ([] @ [y]) y" by simp
+ then show ?thesis using yz by (rule Nil)
+next
+ case (Cons a as)
+ then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
+ then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
+ by cases auto
+ show ?thesis
+ proof (rule Cons(1) [OF _ az])
+ assume "rtrancl_path r y ys z"
+ assume "rtrancl_path r a (as @ [y]) y"
+ with xa have "rtrancl_path r x (a # (as @ [y])) y"
+ by (rule rtrancl_path.step)
+ then have "rtrancl_path r x ((a # as) @ [y]) y"
+ by simp
+ then show ?thesis using `rtrancl_path r y ys z`
+ by (rule Cons(2))
+ qed
+qed
+
+lemma rtrancl_path_distinct:
+ assumes xy: "rtrancl_path r x xs y"
+ obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy
+proof (induct xs rule: measure_induct_rule [of length])
+ case (less xs)
+ show ?case
+ proof (cases "distinct (x # xs)")
+ case True
+ with `rtrancl_path r x xs y` show ?thesis by (rule less)
+ next
+ case False
+ then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
+ by (rule not_distinct_decomp)
+ then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
+ by iprover
+ show ?thesis
+ proof (cases as)
+ case Nil
+ with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
+ by auto
+ from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
+ by (auto elim: rtrancl_path_appendE)
+ from xs have "length cs < length xs" by simp
+ then show ?thesis
+ by (rule less(1)) (iprover intro: cs less(2))+
+ next
+ case (Cons d ds)
+ with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
+ by auto
+ with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
+ and ay: "rtrancl_path r a (bs @ a # cs) y"
+ by (auto elim: rtrancl_path_appendE)
+ from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
+ with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
+ by (rule rtrancl_path_trans)
+ from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
+ then show ?thesis
+ by (rule less(1)) (iprover intro: xy less(2))+
+ qed
+ qed
+qed
+
+inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ base: "rtrancl_tab r xs x x"
+| step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z"
+
+lemma rtrancl_path_imp_rtrancl_tab:
+ assumes path: "rtrancl_path r x xs y"
+ and x: "distinct (x # xs)"
+ and ys: "({x} \<union> set xs) \<inter> set ys = {}"
+ shows "rtrancl_tab r ys x y" using path x ys
+proof (induct arbitrary: ys)
+ case base
+ show ?case by (rule rtrancl_tab.base)
+next
+ case (step x y zs z)
+ then have "x \<notin> set ys" by auto
+ from step have "distinct (y # zs)" by simp
+ moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"
+ by auto
+ ultimately have "rtrancl_tab r (x # ys) y z"
+ by (rule step)
+ with `x \<notin> set ys` `r x y`
+ show ?case by (rule rtrancl_tab.step)
+qed
+
+lemma rtrancl_tab_imp_rtrancl_path:
+ assumes tab: "rtrancl_tab r ys x y"
+ obtains xs where "rtrancl_path r x xs y" using tab
+proof induct
+ case base
+ from rtrancl_path.base show ?case by (rule base)
+next
+ case step show ?case by (iprover intro: step rtrancl_path.step)
+qed
+
+lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y"
+proof
+ assume "r\<^sup>*\<^sup>* x y"
+ then obtain xs where "rtrancl_path r x xs y"
+ by (auto simp add: rtranclp_eq_rtrancl_path)
+ then obtain xs' where xs': "rtrancl_path r x xs' y"
+ and distinct: "distinct (x # xs')"
+ by (rule rtrancl_path_distinct)
+ have "({x} \<union> set xs') \<inter> set [] = {}" by simp
+ with xs' distinct show "rtrancl_tab r [] x y"
+ by (rule rtrancl_path_imp_rtrancl_tab)
+next
+ assume "rtrancl_tab r [] x y"
+ then obtain xs where "rtrancl_path r x xs y"
+ by (rule rtrancl_tab_imp_rtrancl_path)
+ then show "r\<^sup>*\<^sup>* x y"
+ by (auto simp add: rtranclp_eq_rtrancl_path)
+qed
+
+declare rtranclp_eq_rtrancl_tab_nil [code_unfold]
+
+declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
+
+code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp
+
+subsection {* A simple example *}
+
+datatype ty = A | B | C
+
+inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
+where
+ "test A B"
+| "test B A"
+| "test B C"
+
+subsubsection {* Invoking with the SML code generator *}
+
+code_module Test
+contains
+test1 = "test\<^sup>*\<^sup>* A C"
+test2 = "test\<^sup>*\<^sup>* C A"
+test3 = "test\<^sup>*\<^sup>* A _"
+test4 = "test\<^sup>*\<^sup>* _ C"
+
+ML "Test.test1"
+ML "Test.test2"
+ML "DSeq.list_of Test.test3"
+ML "DSeq.list_of Test.test4"
+
+subsubsection {* Invoking with the predicate compiler and the generic code generator *}
+
+code_pred test .
+
+values "{x. test\<^sup>*\<^sup>* A C}"
+values "{x. test\<^sup>*\<^sup>* C A}"
+values "{x. test\<^sup>*\<^sup>* A x}"
+values "{x. test\<^sup>*\<^sup>* x C}"
+
+hide const test
+
+end
+
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Function/function_core.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Function/mutual.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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_core.ML Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 13 11:34:05 2009 +0000
@@ -1047,7 +1047,6 @@
let
val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
p ^ " violates mode " ^ string_of_mode thy p m)
- val _ = tracing (string_of_clause thy p (nth rs i))
in () end
else ()
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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/Predicate_Compile/predicate_compile_quickcheck.ML Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Nov 13 11:34:05 2009 +0000
@@ -23,6 +23,8 @@
val options = Options {
expected_modes = NONE,
+ proposed_modes = [],
+ proposed_names = [],
show_steps = true,
show_intermediate_results = true,
show_proof_trace = false,
--- a/src/HOL/Tools/inductive.ML Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/inductive.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/inductive_set.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/recdef.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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/HOL/Tools/res_atp.ML Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/res_atp.ML Fri Nov 13 11:34:05 2009 +0000
@@ -352,20 +352,32 @@
filter (not o known) c_clauses
end;
-fun valid_facts facts =
- Facts.fold_static (fn (name, ths) =>
- if Facts.is_concealed facts name orelse
- (run_blacklist_filter andalso is_package_def name) then I
- else
- let val xname = Facts.extern facts name in
- if Name_Space.is_hidden xname then I
- else cons (xname, filter_out Res_Axioms.bad_for_atp ths)
- end) facts [];
-
fun all_valid_thms ctxt =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
val local_facts = ProofContext.facts_of ctxt;
+ val full_space =
+ Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
+
+ fun valid_facts facts =
+ (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
+ let
+ fun check_thms a =
+ (case try (ProofContext.get_thms ctxt) a of
+ NONE => false
+ | SOME ths1 => Thm.eq_thms (ths0, ths1));
+
+ val name1 = Facts.extern facts name;
+ val name2 = Name_Space.extern full_space name;
+ val ths = filter_out Res_Axioms.bad_for_atp ths0;
+ in
+ if Facts.is_concealed facts name orelse null ths orelse
+ run_blacklist_filter andalso is_package_def name then I
+ else
+ (case find_first check_thms [name1, name2, name] of
+ NONE => I
+ | SOME a => cons (a, ths))
+ end);
in valid_facts global_facts @ valid_facts local_facts end;
fun multi_name a th (n, pairs) =
--- a/src/HOL/ex/ROOT.ML Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/ex/ROOT.ML Fri Nov 13 11:34:05 2009 +0000
@@ -13,7 +13,8 @@
"Codegenerator_Pretty_Test",
"NormalForm",
"Predicate_Compile",
- "Predicate_Compile_ex"
+ "Predicate_Compile_ex",
+ "Predicate_Compile_Quickcheck"
];
use_thys [
--- a/src/HOLCF/Tools/pcpodef.ML Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOLCF/Tools/pcpodef.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/General/markup.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Isar/expression.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Isar/locale.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Isar/proof_context.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Isar/proof_display.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Isar/specification.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Thy/thm_deps.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/drule.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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 Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/more_thm.ML Fri Nov 13 11:34:05 2009 +0000
@@ -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);