modernized module name and setup;
authorwenzelm
Sat Aug 16 13:23:50 2014 +0200 (2014-08-16)
changeset 5794875724d71013c
parent 57947 189d421ca72d
child 57949 b203a7644bf1
modernized module name and setup;
src/FOL/IFOL.thy
src/HOL/HOL.thy
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
src/Tools/atomize_elim.ML
     1.1 --- a/src/FOL/IFOL.thy	Sat Aug 16 12:15:56 2014 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Sat Aug 16 13:23:50 2014 +0200
     1.3 @@ -710,16 +710,14 @@
     1.4  
     1.5  subsection {* Atomizing elimination rules *}
     1.6  
     1.7 -setup AtomizeElim.setup
     1.8 -
     1.9  lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)"
    1.10 -by rule iprover+
    1.11 +  by rule iprover+
    1.12  
    1.13  lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
    1.14 -by rule iprover+
    1.15 +  by rule iprover+
    1.16  
    1.17  lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
    1.18 -by rule iprover+
    1.19 +  by rule iprover+
    1.20  
    1.21  lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" ..
    1.22  
     2.1 --- a/src/HOL/HOL.thy	Sat Aug 16 12:15:56 2014 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sat Aug 16 13:23:50 2014 +0200
     2.3 @@ -763,8 +763,6 @@
     2.4  
     2.5  subsubsection {* Atomizing elimination rules *}
     2.6  
     2.7 -setup AtomizeElim.setup
     2.8 -
     2.9  lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)"
    2.10    by rule iprover+
    2.11  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Aug 16 12:15:56 2014 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Aug 16 13:23:50 2014 +0200
     3.3 @@ -129,7 +129,7 @@
     3.4      | Blast_Method => blast_tac ctxt
     3.5      | Auto_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
     3.6      | Auto_Choice_Method =>
     3.7 -      AtomizeElim.atomize_elim_tac ctxt THEN'
     3.8 +      Atomize_Elim.atomize_elim_tac ctxt THEN'
     3.9        SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt addSIs @{thms choice}))
    3.10      | Force_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
    3.11      | Linarith_Method =>
     4.1 --- a/src/Tools/atomize_elim.ML	Sat Aug 16 12:15:56 2014 +0200
     4.2 +++ b/src/Tools/atomize_elim.ML	Sat Aug 16 13:23:50 2014 +0200
     4.3 @@ -6,17 +6,13 @@
     4.4  
     4.5  signature ATOMIZE_ELIM =
     4.6  sig
     4.7 -  val declare_atomize_elim : attribute  
     4.8 -
     4.9 +  val declare_atomize_elim : attribute
    4.10    val atomize_elim_conv : Proof.context -> conv
    4.11    val full_atomize_elim_conv : Proof.context -> conv
    4.12 -
    4.13    val atomize_elim_tac : Proof.context -> int -> tactic
    4.14 -
    4.15 -  val setup : theory -> theory
    4.16  end
    4.17  
    4.18 -structure AtomizeElim : ATOMIZE_ELIM =
    4.19 +structure Atomize_Elim : ATOMIZE_ELIM =
    4.20  struct
    4.21  
    4.22  (* theory data *)
    4.23 @@ -27,6 +23,8 @@
    4.24    val description = "atomize_elim rewrite rule";
    4.25  );
    4.26  
    4.27 +val _ = Theory.setup AtomizeElimData.setup;
    4.28 +
    4.29  val declare_atomize_elim = AtomizeElimData.add
    4.30  
    4.31  (* More conversions: *)
    4.32 @@ -50,7 +48,7 @@
    4.33      in Thm.equal_intr fwd back end
    4.34  
    4.35  
    4.36 -(* convert !!thesis. (!!x y z. ... => thesis) ==> ... 
    4.37 +(* convert !!thesis. (!!x y z. ... => thesis) ==> ...
    4.38                       ==> (!!a b c. ... => thesis)
    4.39                       ==> thesis
    4.40  
    4.41 @@ -71,7 +69,7 @@
    4.42  fun thesis_miniscope_conv inner_cv ctxt =
    4.43      let
    4.44        (* check if the outermost quantifier binds the conclusion *)
    4.45 -      fun is_forall_thesis t = 
    4.46 +      fun is_forall_thesis t =
    4.47            case Logic.strip_assums_concl t of
    4.48              (_ $ Bound i) => i = length (Logic.strip_params t) - 1
    4.49            | _ => false
    4.50 @@ -93,11 +91,11 @@
    4.51            end
    4.52  
    4.53        (* move current quantifier to the right *)
    4.54 -      fun moveq_conv ctxt = 
    4.55 +      fun moveq_conv ctxt =
    4.56            (rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt))
    4.57            else_conv (movea_conv ctxt)
    4.58  
    4.59 -      fun ms_conv ctxt ct = 
    4.60 +      fun ms_conv ctxt ct =
    4.61            if is_forall_thesis (term_of ct)
    4.62            then moveq_conv ctxt ct
    4.63            else (implies_concl_conv (ms_conv ctxt)
    4.64 @@ -105,7 +103,7 @@
    4.65              (forall_conv (ms_conv o snd) ctxt))
    4.66              ct
    4.67      in
    4.68 -      ms_conv ctxt 
    4.69 +      ms_conv ctxt
    4.70      end
    4.71  
    4.72  val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv
    4.73 @@ -117,13 +115,13 @@
    4.74      let
    4.75        val thy = Proof_Context.theory_of ctxt
    4.76        val _ $ thesis = Logic.strip_assums_concl subg
    4.77 -                       
    4.78 +
    4.79        (* Introduce a quantifier first if the thesis is not bound *)
    4.80 -      val quantify_thesis = 
    4.81 +      val quantify_thesis =
    4.82            if is_Bound thesis then all_tac
    4.83            else let
    4.84                val cthesis = cterm_of thy thesis
    4.85 -              val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] 
    4.86 +              val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis]
    4.87                           @{thm meta_spec}
    4.88              in
    4.89                compose_tac (false, rule, 1) i
    4.90 @@ -133,9 +131,9 @@
    4.91        THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
    4.92      end)
    4.93  
    4.94 -val setup =
    4.95 -  Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
    4.96 -    "convert obtains statement to atomic object logic goal"
    4.97 -  #> AtomizeElimData.setup
    4.98 +val _ =
    4.99 +  Theory.setup
   4.100 +    (Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
   4.101 +      "convert obtains statement to atomic object logic goal")
   4.102  
   4.103  end