# HG changeset patch
# User krauss
# Date 1216047775 -7200
# Node ID 69f3981c8ed4aeca227b18baeb7eb747a76eb0a7
# Parent  9964e59a688c630c9f9c275166d36afe39a4cea7
renamed conversions to _conv, tuned

diff -r 9964e59a688c -r 69f3981c8ed4 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Mon Jul 14 16:13:58 2008 +0200
+++ b/src/Tools/atomize_elim.ML	Mon Jul 14 17:02:55 2008 +0200
@@ -9,8 +9,8 @@
 sig
   val declare_atomize_elim : attribute  
 
-  val atomize_elim : Proof.context -> conv
-  val full_atomize_elim : Proof.context -> conv
+  val atomize_elim_conv : Proof.context -> conv
+  val full_atomize_elim_conv : Proof.context -> conv
 
   val atomize_elim_tac : Proof.context -> int -> tactic
 
@@ -21,18 +21,12 @@
 struct
 
 (* theory data *)
-structure AtomizeElimData = TheoryDataFun
-(
-  type T = thm list;
-  val empty = [];
-  val copy = I;
-  val extend = I;
-  fun merge _ = Thm.merge_thms
+structure AtomizeElimData = NamedThmsFun(
+  val name = "atomize_elim";
+  val description = "atomize_elim rewrite rule";
 );
 
-val add_elim = AtomizeElimData.map o Thm.add_thm
-val declare_atomize_elim = Thm.declaration_attribute (fn th => Context.mapping (add_elim th) I);
-
+val declare_atomize_elim = AtomizeElimData.add
 
 (* More conversions: *)
 local open Conv in
@@ -48,11 +42,11 @@
 fun rearrange_prems_conv pi ct =
     let
       val pi' = 0 :: map (curry op + 1) pi
-      val fwd  = trivial ct
+      val fwd  = Thm.trivial ct
                   |> Drule.rearrange_prems pi'
-      val back = trivial (snd (Thm.dest_implies (cprop_of fwd)))
+      val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd)))
                   |> Drule.rearrange_prems (invert_perm pi')
-    in equal_intr fwd back end
+    in Thm.equal_intr fwd back end
 
 
 (* convert !!thesis. (!!x y z. ... => thesis) ==> ... 
@@ -63,9 +57,9 @@
 
    (EX x y z. ...) | ... | (EX a b c. ...)
 *)
-fun atomize_elim ctxt ct =
+fun atomize_elim_conv ctxt ct =
     (forall_conv (K (prems_conv ~1 ObjectLogic.atomize_prems)) ctxt
-    then_conv MetaSimplifier.rewrite true (AtomizeElimData.get (ProofContext.theory_of ctxt))
+    then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt)
     then_conv (fn ct' => if can ObjectLogic.dest_judgment ct'
                          then all_conv ct'
                          else raise CTERM ("atomize_elim", [ct', ct])))
@@ -76,10 +70,10 @@
 fun thesis_miniscope_conv inner_cv ctxt =
     let
       (* check if the outermost quantifier binds the conclusion *)
-      fun is_forall_thesis (Const ("all", _) $ Abs (_, T, b)) =
-          exists_subterm (fn Free (n, _) => n = "" | _ => false) 
-                         (Logic.strip_assums_concl (subst_bound (Free ("", dummyT), b)))
-        | is_forall_thesis _ = false
+      fun is_forall_thesis t = 
+          case Logic.strip_assums_concl t of
+            (_ $ Bound i) => i = length (Logic.strip_params t) - 1
+          | _ => false
 
       (* move unrelated assumptions out of the quantification *)
       fun movea_conv ctxt ct =
@@ -99,7 +93,7 @@
 
       (* move current quantifier to the right *)
       fun moveq_conv ctxt = 
-          (rewr_conv @{thm swap_params} then_conv (forall_conv (uncurry (K moveq_conv)) ctxt))
+          (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt))
           else_conv (movea_conv ctxt)
 
       fun ms_conv ctxt ct = 
@@ -107,40 +101,40 @@
           then moveq_conv ctxt ct
           else (implies_concl_conv (ms_conv ctxt)
             else_conv
-            (forall_conv (uncurry (K ms_conv)) ctxt))
+            (forall_conv (ms_conv o snd) ctxt))
             ct
     in
       ms_conv ctxt 
     end
 
-val full_atomize_elim = thesis_miniscope_conv atomize_elim
+val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv
 
 end
 
 
-fun atomize_elim_tac ctxt = CSUBGOAL (fn (csubg, i) =>
+fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) =>
     let
-      val _ $ thesis = Logic.strip_assums_concl (term_of csubg)
+      val thy = ProofContext.theory_of ctxt
+      val _ $ thesis = Logic.strip_assums_concl subg
                        
       (* Introduce a quantifier first if the thesis is not bound *)
       val quantify_thesis = 
           if is_Bound thesis then all_tac
           else let
-              val cthesis = cterm_of (theory_of_cterm csubg) thesis
+              val cthesis = cterm_of thy thesis
               val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] 
                          @{thm meta_spec}
             in
-              Thm.compose_no_flatten false (rule, 1) i
+              compose_tac (false, rule, 1) i
             end
     in
       quantify_thesis
-      THEN (CONVERSION (full_atomize_elim ctxt) i)
+      THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
     end)
 
 val setup = Method.add_methods
   [("atomize_elim", Method.ctxt_args (Method.SIMPLE_METHOD' o atomize_elim_tac),
     "convert obtains statement to atomic object logic goal")]
-  #> Attrib.add_attributes 
-      [("atomize_elim", Attrib.no_args declare_atomize_elim, "declaration of atomize_elim rewrite rule")]
+  #> AtomizeElimData.setup
 
 end