--- a/src/HOL/Finite.ML Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/Finite.ML Sun Oct 14 22:08:29 2001 +0200
@@ -598,7 +598,7 @@
Goal "[| (A, x) : foldSet f e; (A, y) : foldSet f e |] ==> y=x";
-by (blast_tac (claset() addIs [rulify lemma]) 1);
+by (blast_tac (claset() addIs [ObjectLogic.rulify lemma]) 1);
qed "foldSet_determ";
Goalw [fold_def] "(A,y) : foldSet f e ==> fold f e A = y";
--- a/src/HOL/HOL.thy Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/HOL.thy Sun Oct 14 22:08:29 2001 +0200
@@ -237,6 +237,7 @@
use "cladata.ML"
setup hypsubst_setup
+declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify]
setup Classical.setup
setup clasetup
--- a/src/HOL/Integ/IntArith.ML Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/Integ/IntArith.ML Sun Oct 14 22:08:29 2001 +0200
@@ -38,7 +38,7 @@
by(blast_tac (claset() addIs [le_SucI]) 1);
val lemma = result();
-bind_thm("nat0_intermed_int_val", rulify_no_asm lemma);
+bind_thm("nat0_intermed_int_val", ObjectLogic.rulify_no_asm lemma);
Goal "[| !i. m <= i & i < n --> abs(f(i + 1::nat) - f i) <= Numeral1; m < n; \
\ f m <= k; k <= f n |] ==> ? i. m <= i & i <= n & f i = (k::int)";
--- a/src/HOL/IsaMakefile Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/IsaMakefile Sun Oct 14 22:08:29 2001 +0200
@@ -73,9 +73,9 @@
$(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
- $(SRC)/Provers/make_elim.ML $(SRC)/Provers/rulify.ML \
- $(SRC)/Provers/simplifier.ML $(SRC)/Provers/split_paired_all.ML \
- $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
+ $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
+ $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
+ $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
$(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
$(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML Calculation.thy \
Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
--- a/src/HOL/List.ML Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/List.ML Sun Oct 14 22:08:29 2001 +0200
@@ -413,7 +413,7 @@
by Auto_tac;
qed "rev_exhaust_aux";
-bind_thm ("rev_exhaust", Rulify.rulify rev_exhaust_aux);
+bind_thm ("rev_exhaust", ObjectLogic.rulify rev_exhaust_aux);
(** set **)
--- a/src/HOL/ROOT.ML Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/ROOT.ML Sun Oct 14 22:08:29 2001 +0200
@@ -20,7 +20,6 @@
use "~~/src/Provers/split_paired_all.ML";
use "~~/src/Provers/splitter.ML";
use "~~/src/Provers/hypsubst.ML";
-use "~~/src/Provers/rulify.ML";
use "~~/src/Provers/induct_method.ML";
use "~~/src/Provers/make_elim.ML";
use "~~/src/Provers/classical.ML";
--- a/src/HOL/Set.ML Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/Set.ML Sun Oct 14 22:08:29 2001 +0200
@@ -840,23 +840,6 @@
by (Blast_tac 1);
qed "psubset_imp_ex_mem";
-
-(* rulify setup *)
-
Goal "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)";
by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
qed "atomize_ball";
-
-local
- val ss = HOL_basic_ss addsimps
- [Drule.norm_hhf_eq, Thm.symmetric atomize_ball, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
-in
-
-structure Rulify = RulifyFun
- (val make_meta = Simplifier.simplify ss
- val full_make_meta = Simplifier.full_simplify ss);
-
-structure BasicRulify: BASIC_RULIFY = Rulify;
-open BasicRulify;
-
-end;
--- a/src/HOL/Tools/inductive_package.ML Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML Sun Oct 14 22:08:29 2001 +0200
@@ -295,7 +295,7 @@
val all_not_allowed =
"Introduction rule must not have a leading \"!!\" quantifier";
-val atomize_cterm = full_rewrite_cterm inductive_atomize;
+val atomize_cterm = rewrite_cterm true inductive_atomize;
in
--- a/src/HOL/Typedef.thy Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/Typedef.thy Sun Oct 14 22:08:29 2001 +0200
@@ -8,6 +8,9 @@
theory Typedef = Set
files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"):
+(*belongs to theory Set*)
+declare atomize_ball [symmetric, rulify]
+
(* Courtesy of Stephan Merz *)
lemma Least_mono:
"mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
@@ -20,10 +23,6 @@
done
-(*belongs to theory Set*)
-setup Rulify.setup
-
-
subsection {* HOL type definitions *}
constdefs
--- a/src/Pure/Isar/attrib.ML Sun Oct 14 22:07:01 2001 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Oct 14 22:08:29 2001 +0200
@@ -278,6 +278,13 @@
fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x;
+(* rule_format *)
+
+fun rule_format_att x = syntax
+ (Scan.lift (Args.parens (Args.$$$ "no_asm")
+ >> K ObjectLogic.rule_format_no_asm || Scan.succeed ObjectLogic.rule_format)) x;
+
+
(* misc rules *)
fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
@@ -288,6 +295,7 @@
fun exported_local x = no_args (Drule.rule_attribute Proof.export_thm) x;
+
(** theory setup **)
(* pure_attributes *)
@@ -309,8 +317,11 @@
("case_names", (case_names, case_names), "named rule cases"),
("params", (params, params), "named rule parameters"),
("exported", (exported_global, exported_local), "theorem exported from context"),
- ("atomize", (no_args ObjectLogic.atomize, no_args undef_local_attribute),
- "declaration of atomize rule")];
+ ("atomize", (no_args ObjectLogic.declare_atomize, no_args undef_local_attribute),
+ "declaration of atomize rule"),
+ ("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute),
+ "declaration of rulify rule"),
+ ("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")];
(* setup *)
--- a/src/Pure/object_logic.ML Sun Oct 14 22:07:01 2001 +0200
+++ b/src/Pure/object_logic.ML Sun Oct 14 22:08:29 2001 +0200
@@ -14,9 +14,14 @@
val is_judgment: Sign.sg -> term -> bool
val drop_judgment: Sign.sg -> term -> term
val fixed_judgment: Sign.sg -> string -> term
- val atomize: theory attribute
+ val declare_atomize: theory attribute
+ val declare_rulify: theory attribute
val atomize_tac: int -> tactic
val atomize_goal: int -> thm -> thm
+ val rulify: thm -> thm
+ val rulify_no_asm: thm -> thm
+ val rule_format: 'a attribute
+ val rule_format_no_asm: 'a attribute
val setup: (theory -> theory) list
end;
@@ -31,9 +36,9 @@
structure ObjectLogicDataArgs =
struct
val name = "Pure/object-logic";
- type T = string option * thm list;
+ type T = string option * (thm list * thm list);
- val empty = (None, []);
+ val empty = (None, ([], [Drule.norm_hhf_eq]));
val copy = I;
val prep_ext = I;
@@ -41,8 +46,9 @@
if x = y then Some x else error "Attempt to merge different object-logics"
| merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
- fun merge ((judgment1, atomize1), (judgment2, atomize2)) =
- (merge_judgment (judgment1, judgment2), Drule.merge_rules (atomize1, atomize2));
+ fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
+ (merge_judgment (judgment1, judgment2),
+ (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
fun print _ _ = ();
end;
@@ -72,7 +78,6 @@
end;
-
(* term operations *)
fun judgment_name sg =
@@ -99,32 +104,49 @@
-(** atomize meta-level connectives **)
+(** treatment of meta-level connectives **)
(* maintain rules *)
-val get_atomize_sg = #2 o ObjectLogicData.get_sg;
+val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
+val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
-val add_atomize = ObjectLogicData.map o Library.apsnd o Drule.add_rules;
-fun atomize (thy, th) = (add_atomize [th] thy, th);
+val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules;
+val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules;
+
+fun declare_atomize (thy, th) = (add_atomize [th] thy, th);
+fun declare_rulify (thy, th) = (add_rulify [th] thy, th);
-(* tactics *)
+(* atomize *)
fun rewrite_prems_tac rews i = PRIMITIVE (MetaSimplifier.fconv_rule
(MetaSimplifier.goals_conv (Library.equal i)
(MetaSimplifier.forall_conv
- (MetaSimplifier.goals_conv (K true) (Tactic.full_rewrite rews)))));
+ (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews)))));
fun atomize_tac i st =
if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then
- (rewrite_prems_tac (get_atomize_sg (Thm.sign_of_thm st)) i) st
+ (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
else all_tac st;
fun atomize_goal i st =
(case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');
+(* rulify *)
+
+fun gen_rulify full thm =
+ Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
+ |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
+
+val rulify = gen_rulify true;
+val rulify_no_asm = gen_rulify false;
+
+fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
+fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
+
+
(** theory setup **)
--- a/src/ZF/ZF.ML Sun Oct 14 22:07:01 2001 +0200
+++ b/src/ZF/ZF.ML Sun Oct 14 22:08:29 2001 +0200
@@ -510,23 +510,6 @@
by (Blast_tac 1);
qed "Union_in_Pow";
-
-(* update rulify setup -- include bounded All *)
-
Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))";
by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
qed "atomize_ball";
-
-local
- val ss = FOL_basic_ss addsimps
- [Drule.norm_hhf_eq, Thm.symmetric atomize_ball, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
-in
-
-structure Rulify = RulifyFun
- (val make_meta = Simplifier.simplify ss
- val full_make_meta = Simplifier.full_simplify ss);
-
-structure BasicRulify: BASIC_RULIFY = Rulify;
-open BasicRulify;
-
-end;
--- a/src/ZF/upair.thy Sun Oct 14 22:07:01 2001 +0200
+++ b/src/ZF/upair.thy Sun Oct 14 22:08:29 2001 +0200
@@ -8,6 +8,6 @@
files "Tools/typechk":
setup TypeCheck.setup
-setup Rulify.setup
+declare atomize_ball [symmetric, rulify]
end