# HG changeset patch
# User wenzelm
# Date 1138465739 -3600
# Node ID c13136d648e22a2c3bb68f7251af4a85d1ce745e
# Parent  126049347167c13630643054b3c77905384522f1
removed unatomize;
added versions of meta_rewrite, unfold, fold;

diff -r 126049347167 -r c13136d648e2 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sat Jan 28 17:28:58 2006 +0100
+++ b/src/Pure/Isar/object_logic.ML	Sat Jan 28 17:28:59 2006 +0100
@@ -22,23 +22,27 @@
   val atomize_tac: int -> tactic
   val full_atomize_tac: int -> tactic
   val atomize_goal: int -> thm -> thm
-  val unatomize_term: theory -> term -> term
-  val unatomize_tac: int -> tactic
   val rulify_term: theory -> term -> term
   val rulify_tac: int -> tactic
   val rulify: thm -> thm
   val rulify_no_asm: thm -> thm
   val rule_format: attribute
   val rule_format_no_asm: attribute
+  val meta_rewrite_cterm: cterm -> thm
+  val meta_rewrite_thm: thm -> thm
+  val meta_rewrite_tac: int -> tactic
+  val unfold: thm list -> thm -> thm
+  val unfold_goals: thm list -> thm -> thm
+  val unfold_tac: thm list -> tactic
+  val fold: thm list -> thm -> thm
+  val fold_tac: thm list -> tactic
 end;
 
 structure ObjectLogic: OBJECT_LOGIC =
 struct
 
 
-(** object-logic theory data **)
-
-(* data kind 'Pure/object-logic' *)
+(** theory data **)
 
 structure ObjectLogicData = TheoryDataFun
 (struct
@@ -66,7 +70,7 @@
 
 (** generic treatment of judgments -- with a single argument only **)
 
-(* add_judgment(_i) *)
+(* add judgment *)
 
 local
 
@@ -125,7 +129,6 @@
 (* maintain rules *)
 
 val get_atomize = #1 o #2 o ObjectLogicData.get;
-val get_unatomize = map Thm.symmetric o get_atomize;
 val get_rulify = #2 o #2 o ObjectLogicData.get;
 
 val declare_atomize =
@@ -162,12 +165,6 @@
   (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st');
 
 
-(* unatomize -- not necessarily the same as rulify *)
-
-fun unatomize_term thy = MetaSimplifier.rewrite_term thy (get_unatomize thy) [];
-fun unatomize_tac i st = rewrite_goal_tac (get_unatomize (Thm.theory_of_thm st)) i st;
-
-
 (* rulify *)
 
 fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) [];
@@ -184,4 +181,36 @@
 fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x;
 
 
+(* handle object-level equalities *)
+
+local
+
+val equals_ss =
+  MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
+    addeqcongs [Drule.equals_cong];    (*protect meta-level equality*)
+
+fun rewrite rules =
+  MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE)) (equals_ss addsimps rules);
+
+in
+
+fun meta_rewrite_cterm ct =
+  let val thy = Thm.theory_of_cterm ct in
+    Thm.transitive
+      (rewrite (get_rulify thy) ct)
+      (rewrite (map Thm.symmetric (get_atomize thy)) ct)    (*produce meta-level equality*)
+  end;
+
+val meta_rewrite_thm = Drule.fconv_rule meta_rewrite_cterm;
+fun meta_rewrite_tac i =
+  PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) meta_rewrite_cterm));
+
+val unfold       = Tactic.rewrite_rule       o map meta_rewrite_thm;
+val unfold_goals = Tactic.rewrite_goals_rule o map meta_rewrite_thm;
+val unfold_tac   = Tactic.rewrite_goals_tac  o map meta_rewrite_thm;
+val fold         = Tactic.fold_rule          o map meta_rewrite_thm;
+val fold_tac     = Tactic.fold_goals_tac     o map meta_rewrite_thm;
+
 end;
+
+end;