# HG changeset patch
# User wenzelm
# Date 1003090109 -7200
# Node ID b6bb7a853dd26238368368f2ade7150fbd97232b
# Parent  1fcf1eb516084b805f80f08fa3600ff9b0058807
moved rulify to ObjectLogic;

diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/HOL/Finite.ML
--- 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";
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/HOL/HOL.thy
--- 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
 
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/HOL/Integ/IntArith.ML
--- 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)";
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/HOL/IsaMakefile
--- 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 \
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/HOL/List.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 **)
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/HOL/ROOT.ML
--- 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";
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/HOL/Set.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;
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/HOL/Tools/inductive_package.ML
--- 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
 
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/HOL/Typedef.thy
--- 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
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/Pure/Isar/attrib.ML
--- 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 *)
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/Pure/object_logic.ML
--- 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 **)
 
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/ZF/ZF.ML
--- 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;
diff -r 1fcf1eb51608 -r b6bb7a853dd2 src/ZF/upair.thy
--- 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