src/Tools/atomize_elim.ML
changeset 57948 75724d71013c
parent 54742 7a86358a3c0b
child 57949 b203a7644bf1
     1.1 --- a/src/Tools/atomize_elim.ML	Sat Aug 16 12:15:56 2014 +0200
     1.2 +++ b/src/Tools/atomize_elim.ML	Sat Aug 16 13:23:50 2014 +0200
     1.3 @@ -6,17 +6,13 @@
     1.4  
     1.5  signature ATOMIZE_ELIM =
     1.6  sig
     1.7 -  val declare_atomize_elim : attribute  
     1.8 -
     1.9 +  val declare_atomize_elim : attribute
    1.10    val atomize_elim_conv : Proof.context -> conv
    1.11    val full_atomize_elim_conv : Proof.context -> conv
    1.12 -
    1.13    val atomize_elim_tac : Proof.context -> int -> tactic
    1.14 -
    1.15 -  val setup : theory -> theory
    1.16  end
    1.17  
    1.18 -structure AtomizeElim : ATOMIZE_ELIM =
    1.19 +structure Atomize_Elim : ATOMIZE_ELIM =
    1.20  struct
    1.21  
    1.22  (* theory data *)
    1.23 @@ -27,6 +23,8 @@
    1.24    val description = "atomize_elim rewrite rule";
    1.25  );
    1.26  
    1.27 +val _ = Theory.setup AtomizeElimData.setup;
    1.28 +
    1.29  val declare_atomize_elim = AtomizeElimData.add
    1.30  
    1.31  (* More conversions: *)
    1.32 @@ -50,7 +48,7 @@
    1.33      in Thm.equal_intr fwd back end
    1.34  
    1.35  
    1.36 -(* convert !!thesis. (!!x y z. ... => thesis) ==> ... 
    1.37 +(* convert !!thesis. (!!x y z. ... => thesis) ==> ...
    1.38                       ==> (!!a b c. ... => thesis)
    1.39                       ==> thesis
    1.40  
    1.41 @@ -71,7 +69,7 @@
    1.42  fun thesis_miniscope_conv inner_cv ctxt =
    1.43      let
    1.44        (* check if the outermost quantifier binds the conclusion *)
    1.45 -      fun is_forall_thesis t = 
    1.46 +      fun is_forall_thesis t =
    1.47            case Logic.strip_assums_concl t of
    1.48              (_ $ Bound i) => i = length (Logic.strip_params t) - 1
    1.49            | _ => false
    1.50 @@ -93,11 +91,11 @@
    1.51            end
    1.52  
    1.53        (* move current quantifier to the right *)
    1.54 -      fun moveq_conv ctxt = 
    1.55 +      fun moveq_conv ctxt =
    1.56            (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt))
    1.57            else_conv (movea_conv ctxt)
    1.58  
    1.59 -      fun ms_conv ctxt ct = 
    1.60 +      fun ms_conv ctxt ct =
    1.61            if is_forall_thesis (term_of ct)
    1.62            then moveq_conv ctxt ct
    1.63            else (implies_concl_conv (ms_conv ctxt)
    1.64 @@ -105,7 +103,7 @@
    1.65              (forall_conv (ms_conv o snd) ctxt))
    1.66              ct
    1.67      in
    1.68 -      ms_conv ctxt 
    1.69 +      ms_conv ctxt
    1.70      end
    1.71  
    1.72  val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv
    1.73 @@ -117,13 +115,13 @@
    1.74      let
    1.75        val thy = Proof_Context.theory_of ctxt
    1.76        val _ $ thesis = Logic.strip_assums_concl subg
    1.77 -                       
    1.78 +
    1.79        (* Introduce a quantifier first if the thesis is not bound *)
    1.80 -      val quantify_thesis = 
    1.81 +      val quantify_thesis =
    1.82            if is_Bound thesis then all_tac
    1.83            else let
    1.84                val cthesis = cterm_of thy thesis
    1.85 -              val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] 
    1.86 +              val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis]
    1.87                           @{thm meta_spec}
    1.88              in
    1.89                compose_tac (false, rule, 1) i
    1.90 @@ -133,9 +131,9 @@
    1.91        THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
    1.92      end)
    1.93  
    1.94 -val setup =
    1.95 -  Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
    1.96 -    "convert obtains statement to atomic object logic goal"
    1.97 -  #> AtomizeElimData.setup
    1.98 +val _ =
    1.99 +  Theory.setup
   1.100 +    (Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
   1.101 +      "convert obtains statement to atomic object logic goal")
   1.102  
   1.103  end