src/HOL/Tools/simpdata.ML
author wenzelm
Wed Jun 29 21:34:16 2011 +0200 (2011-06-29)
changeset 43597 b4a093e755db
parent 43596 78211f66cf8d
child 45620 f2a587696afb
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      HOL/Tools/simpdata.ML
     2     Author:     Tobias Nipkow
     3     Copyright   1991  University of Cambridge
     4 
     5 Instantiation of the generic simplifier for HOL.
     6 *)
     7 
     8 (** tools setup **)
     9 
    10 structure Quantifier1 = Quantifier1
    11 (
    12   (*abstract syntax*)
    13   fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
    14     | dest_eq _ = NONE;
    15   fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
    16     | dest_conj _ = NONE;
    17   fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
    18     | dest_imp _ = NONE;
    19   val conj = HOLogic.conj
    20   val imp  = HOLogic.imp
    21   (*rules*)
    22   val iff_reflection = @{thm eq_reflection}
    23   val iffI = @{thm iffI}
    24   val iff_trans = @{thm trans}
    25   val conjI= @{thm conjI}
    26   val conjE= @{thm conjE}
    27   val impI = @{thm impI}
    28   val mp   = @{thm mp}
    29   val uncurry = @{thm uncurry}
    30   val exI  = @{thm exI}
    31   val exE  = @{thm exE}
    32   val iff_allI = @{thm iff_allI}
    33   val iff_exI = @{thm iff_exI}
    34   val all_comm = @{thm all_comm}
    35   val ex_comm = @{thm ex_comm}
    36 );
    37 
    38 structure Simpdata =
    39 struct
    40 
    41 fun mk_meta_eq r = r RS @{thm eq_reflection};
    42 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
    43 
    44 fun mk_eq th = case concl_of th
    45   (*expects Trueprop if not == *)
    46   of Const (@{const_name "=="},_) $ _ $ _ => th
    47    | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
    48    | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
    49    | _ => th RS @{thm Eq_TrueI}
    50 
    51 fun mk_eq_True (_: simpset) r =
    52   SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE;
    53 
    54 (* Produce theorems of the form
    55   (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
    56 *)
    57 
    58 fun lift_meta_eq_to_obj_eq i st =
    59   let
    60     fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ P $ Q) = 1 + count_imp Q
    61       | count_imp _ = 0;
    62     val j = count_imp (Logic.strip_assums_concl (nth (prems_of st) (i - 1)))
    63   in
    64     if j = 0 then @{thm meta_eq_to_obj_eq}
    65     else
    66       let
    67         val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
    68         fun mk_simp_implies Q = fold_rev (fn R => fn S =>
    69           Const (@{const_name HOL.simp_implies}, propT --> propT --> propT) $ R $ S) Ps Q
    70         val aT = TFree ("'a", HOLogic.typeS);
    71         val x = Free ("x", aT);
    72         val y = Free ("y", aT)
    73       in
    74         Goal.prove_global (Thm.theory_of_thm st) []
    75           [mk_simp_implies (Logic.mk_equals (x, y))]
    76           (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
    77           (fn {prems, ...} => EVERY
    78            [rewrite_goals_tac @{thms simp_implies_def},
    79             REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
    80               map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
    81       end
    82   end;
    83 
    84 (*Congruence rules for = (instead of ==)*)
    85 fun mk_meta_cong (_: simpset) rl = zero_var_indexes
    86   (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
    87      rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
    88    in mk_meta_eq rl' handle THM _ =>
    89      if can Logic.dest_equals (concl_of rl') then rl'
    90      else error "Conclusion of congruence rules must be =-equality"
    91    end);
    92 
    93 fun mk_atomize pairs =
    94   let
    95     fun atoms thm =
    96       let
    97         fun res th = map (fn rl => th RS rl);   (*exception THM*)
    98         fun res_fixed rls =
    99           if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
   100           else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm];
   101       in
   102         case concl_of thm
   103           of Const (@{const_name Trueprop}, _) $ p => (case head_of p
   104             of Const (a, _) => (case AList.lookup (op =) pairs a
   105               of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm])
   106               | NONE => [thm])
   107             | _ => [thm])
   108           | _ => [thm]
   109       end;
   110   in atoms end;
   111 
   112 fun mksimps pairs (_: simpset) =
   113   map_filter (try mk_eq) o mk_atomize pairs o gen_all;
   114 
   115 fun unsafe_solver_tac ss =
   116   (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
   117   FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
   118     atac, etac @{thm FalseE}];
   119 
   120 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   121 
   122 
   123 (*No premature instantiation of variables during simplification*)
   124 fun safe_solver_tac ss =
   125   (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
   126   FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
   127     eq_assume_tac, ematch_tac @{thms FalseE}];
   128 
   129 val safe_solver = mk_solver "HOL safe" safe_solver_tac;
   130 
   131 structure Splitter = Splitter
   132 (
   133   val thy = @{theory}
   134   val mk_eq = mk_eq
   135   val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
   136   val iffD = @{thm iffD2}
   137   val disjE = @{thm disjE}
   138   val conjE = @{thm conjE}
   139   val exE = @{thm exE}
   140   val contrapos = @{thm contrapos_nn}
   141   val contrapos2 = @{thm contrapos_pp}
   142   val notnotD = @{thm notnotD}
   143 );
   144 
   145 val split_tac = Splitter.split_tac;
   146 val split_inside_tac = Splitter.split_inside_tac;
   147 
   148 val op addsplits = Splitter.addsplits;
   149 val op delsplits = Splitter.delsplits;
   150 
   151 
   152 (* integration of simplifier with classical reasoner *)
   153 
   154 structure Clasimp = Clasimp
   155 (
   156   structure Simplifier = Simplifier
   157     and Splitter = Splitter
   158     and Classical  = Classical
   159     and Blast = Blast
   160   val iffD1 = @{thm iffD1}
   161   val iffD2 = @{thm iffD2}
   162   val notE = @{thm notE}
   163 );
   164 open Clasimp;
   165 
   166 val mksimps_pairs =
   167  [(@{const_name HOL.implies}, [@{thm mp}]),
   168   (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
   169   (@{const_name All}, [@{thm spec}]),
   170   (@{const_name True}, []),
   171   (@{const_name False}, []),
   172   (@{const_name If}, [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
   173 
   174 val HOL_basic_ss =
   175   Simplifier.global_context @{theory} empty_ss
   176     setsubgoaler asm_simp_tac
   177     setSSolver safe_solver
   178     setSolver unsafe_solver
   179     setmksimps (mksimps mksimps_pairs)
   180     setmkeqTrue mk_eq_True
   181     setmkcong mk_meta_cong;
   182 
   183 fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
   184 
   185 fun unfold_tac ths =
   186   let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
   187   in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
   188 
   189 end;
   190 
   191 structure Splitter = Simpdata.Splitter;
   192 structure Clasimp = Simpdata.Clasimp;