renamed conversions to _conv, tuned
authorkrauss
Mon Jul 14 17:02:55 2008 +0200 (2008-07-14)
changeset 2757169f3981c8ed4
parent 27570 9964e59a688c
child 27572 67cd6ed76446
renamed conversions to _conv, tuned
src/Tools/atomize_elim.ML
     1.1 --- a/src/Tools/atomize_elim.ML	Mon Jul 14 16:13:58 2008 +0200
     1.2 +++ b/src/Tools/atomize_elim.ML	Mon Jul 14 17:02:55 2008 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  sig
     1.5    val declare_atomize_elim : attribute  
     1.6  
     1.7 -  val atomize_elim : Proof.context -> conv
     1.8 -  val full_atomize_elim : Proof.context -> conv
     1.9 +  val atomize_elim_conv : Proof.context -> conv
    1.10 +  val full_atomize_elim_conv : Proof.context -> conv
    1.11  
    1.12    val atomize_elim_tac : Proof.context -> int -> tactic
    1.13  
    1.14 @@ -21,18 +21,12 @@
    1.15  struct
    1.16  
    1.17  (* theory data *)
    1.18 -structure AtomizeElimData = TheoryDataFun
    1.19 -(
    1.20 -  type T = thm list;
    1.21 -  val empty = [];
    1.22 -  val copy = I;
    1.23 -  val extend = I;
    1.24 -  fun merge _ = Thm.merge_thms
    1.25 +structure AtomizeElimData = NamedThmsFun(
    1.26 +  val name = "atomize_elim";
    1.27 +  val description = "atomize_elim rewrite rule";
    1.28  );
    1.29  
    1.30 -val add_elim = AtomizeElimData.map o Thm.add_thm
    1.31 -val declare_atomize_elim = Thm.declaration_attribute (fn th => Context.mapping (add_elim th) I);
    1.32 -
    1.33 +val declare_atomize_elim = AtomizeElimData.add
    1.34  
    1.35  (* More conversions: *)
    1.36  local open Conv in
    1.37 @@ -48,11 +42,11 @@
    1.38  fun rearrange_prems_conv pi ct =
    1.39      let
    1.40        val pi' = 0 :: map (curry op + 1) pi
    1.41 -      val fwd  = trivial ct
    1.42 +      val fwd  = Thm.trivial ct
    1.43                    |> Drule.rearrange_prems pi'
    1.44 -      val back = trivial (snd (Thm.dest_implies (cprop_of fwd)))
    1.45 +      val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd)))
    1.46                    |> Drule.rearrange_prems (invert_perm pi')
    1.47 -    in equal_intr fwd back end
    1.48 +    in Thm.equal_intr fwd back end
    1.49  
    1.50  
    1.51  (* convert !!thesis. (!!x y z. ... => thesis) ==> ... 
    1.52 @@ -63,9 +57,9 @@
    1.53  
    1.54     (EX x y z. ...) | ... | (EX a b c. ...)
    1.55  *)
    1.56 -fun atomize_elim ctxt ct =
    1.57 +fun atomize_elim_conv ctxt ct =
    1.58      (forall_conv (K (prems_conv ~1 ObjectLogic.atomize_prems)) ctxt
    1.59 -    then_conv MetaSimplifier.rewrite true (AtomizeElimData.get (ProofContext.theory_of ctxt))
    1.60 +    then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt)
    1.61      then_conv (fn ct' => if can ObjectLogic.dest_judgment ct'
    1.62                           then all_conv ct'
    1.63                           else raise CTERM ("atomize_elim", [ct', ct])))
    1.64 @@ -76,10 +70,10 @@
    1.65  fun thesis_miniscope_conv inner_cv ctxt =
    1.66      let
    1.67        (* check if the outermost quantifier binds the conclusion *)
    1.68 -      fun is_forall_thesis (Const ("all", _) $ Abs (_, T, b)) =
    1.69 -          exists_subterm (fn Free (n, _) => n = "" | _ => false) 
    1.70 -                         (Logic.strip_assums_concl (subst_bound (Free ("", dummyT), b)))
    1.71 -        | is_forall_thesis _ = false
    1.72 +      fun is_forall_thesis t = 
    1.73 +          case Logic.strip_assums_concl t of
    1.74 +            (_ $ Bound i) => i = length (Logic.strip_params t) - 1
    1.75 +          | _ => false
    1.76  
    1.77        (* move unrelated assumptions out of the quantification *)
    1.78        fun movea_conv ctxt ct =
    1.79 @@ -99,7 +93,7 @@
    1.80  
    1.81        (* move current quantifier to the right *)
    1.82        fun moveq_conv ctxt = 
    1.83 -          (rewr_conv @{thm swap_params} then_conv (forall_conv (uncurry (K moveq_conv)) ctxt))
    1.84 +          (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt))
    1.85            else_conv (movea_conv ctxt)
    1.86  
    1.87        fun ms_conv ctxt ct = 
    1.88 @@ -107,40 +101,40 @@
    1.89            then moveq_conv ctxt ct
    1.90            else (implies_concl_conv (ms_conv ctxt)
    1.91              else_conv
    1.92 -            (forall_conv (uncurry (K ms_conv)) ctxt))
    1.93 +            (forall_conv (ms_conv o snd) ctxt))
    1.94              ct
    1.95      in
    1.96        ms_conv ctxt 
    1.97      end
    1.98  
    1.99 -val full_atomize_elim = thesis_miniscope_conv atomize_elim
   1.100 +val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv
   1.101  
   1.102  end
   1.103  
   1.104  
   1.105 -fun atomize_elim_tac ctxt = CSUBGOAL (fn (csubg, i) =>
   1.106 +fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) =>
   1.107      let
   1.108 -      val _ $ thesis = Logic.strip_assums_concl (term_of csubg)
   1.109 +      val thy = ProofContext.theory_of ctxt
   1.110 +      val _ $ thesis = Logic.strip_assums_concl subg
   1.111                         
   1.112        (* Introduce a quantifier first if the thesis is not bound *)
   1.113        val quantify_thesis = 
   1.114            if is_Bound thesis then all_tac
   1.115            else let
   1.116 -              val cthesis = cterm_of (theory_of_cterm csubg) thesis
   1.117 +              val cthesis = cterm_of thy thesis
   1.118                val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] 
   1.119                           @{thm meta_spec}
   1.120              in
   1.121 -              Thm.compose_no_flatten false (rule, 1) i
   1.122 +              compose_tac (false, rule, 1) i
   1.123              end
   1.124      in
   1.125        quantify_thesis
   1.126 -      THEN (CONVERSION (full_atomize_elim ctxt) i)
   1.127 +      THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
   1.128      end)
   1.129  
   1.130  val setup = Method.add_methods
   1.131    [("atomize_elim", Method.ctxt_args (Method.SIMPLE_METHOD' o atomize_elim_tac),
   1.132      "convert obtains statement to atomic object logic goal")]
   1.133 -  #> Attrib.add_attributes 
   1.134 -      [("atomize_elim", Attrib.no_args declare_atomize_elim, "declaration of atomize_elim rewrite rule")]
   1.135 +  #> AtomizeElimData.setup
   1.136  
   1.137  end