src/HOL/Tools/simpdata.ML
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 56073 29e308b56d23
child 58839 ccda99401bc8
permissions -rw-r--r--
more qualified names;
     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 Pure.eq},_) $ _ $ _ => 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 (_: Proof.context) 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 (Thm.term_of (Thm.cprem_of st i)))
    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         val mk_simp_implies = fold_rev (fn R => fn S =>
    69           Const (@{const_name HOL.simp_implies}, propT --> propT --> propT) $ R $ S) Ps;
    70       in
    71         Goal.prove_global (Thm.theory_of_thm st) []
    72           [mk_simp_implies @{prop "(x::'a) == y"}]
    73           (mk_simp_implies @{prop "(x::'a) = y"})
    74           (fn {context = ctxt, prems} => EVERY
    75            [rewrite_goals_tac ctxt @{thms simp_implies_def},
    76             REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
    77               map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)])
    78       end
    79   end;
    80 
    81 (*Congruence rules for = (instead of ==)*)
    82 fun mk_meta_cong (_: Proof.context) rl = zero_var_indexes
    83   (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
    84      rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
    85    in mk_meta_eq rl' handle THM _ =>
    86      if can Logic.dest_equals (concl_of rl') then rl'
    87      else error "Conclusion of congruence rules must be =-equality"
    88    end);
    89 
    90 fun mk_atomize pairs =
    91   let
    92     fun atoms thm =
    93       let
    94         fun res th = map (fn rl => th RS rl);   (*exception THM*)
    95         fun res_fixed rls =
    96           if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
    97           else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm];
    98       in
    99         case concl_of thm
   100           of Const (@{const_name Trueprop}, _) $ p => (case head_of p
   101             of Const (a, _) => (case AList.lookup (op =) pairs a
   102               of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm])
   103               | NONE => [thm])
   104             | _ => [thm])
   105           | _ => [thm]
   106       end;
   107   in atoms end;
   108 
   109 fun mksimps pairs (_: Proof.context) =
   110   map_filter (try mk_eq) o mk_atomize pairs o gen_all;
   111 
   112 val simp_legacy_precond =
   113   Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false)
   114 
   115 fun unsafe_solver_tac ctxt =
   116   let
   117     val intros =
   118       if Config.get ctxt simp_legacy_precond then [] else [@{thm conjI}]
   119     val sol_thms =
   120       reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
   121     fun sol_tac i =
   122       FIRST [resolve_tac sol_thms i, atac i , etac @{thm FalseE} i] ORELSE
   123       (match_tac intros THEN_ALL_NEW sol_tac) i
   124   in
   125     (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
   126   end;
   127 
   128 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   129 
   130 
   131 (*No premature instantiation of variables during simplification*)
   132 fun safe_solver_tac ctxt =
   133   (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
   134   FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
   135     eq_assume_tac, ematch_tac @{thms FalseE}];
   136 
   137 val safe_solver = mk_solver "HOL safe" safe_solver_tac;
   138 
   139 structure Splitter = Splitter
   140 (
   141   val thy = @{theory}
   142   val mk_eq = mk_eq
   143   val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
   144   val iffD = @{thm iffD2}
   145   val disjE = @{thm disjE}
   146   val conjE = @{thm conjE}
   147   val exE = @{thm exE}
   148   val contrapos = @{thm contrapos_nn}
   149   val contrapos2 = @{thm contrapos_pp}
   150   val notnotD = @{thm notnotD}
   151 );
   152 
   153 val split_tac = Splitter.split_tac;
   154 val split_inside_tac = Splitter.split_inside_tac;
   155 
   156 
   157 (* integration of simplifier with classical reasoner *)
   158 
   159 structure Clasimp = Clasimp
   160 (
   161   structure Simplifier = Simplifier
   162     and Splitter = Splitter
   163     and Classical  = Classical
   164     and Blast = Blast
   165   val iffD1 = @{thm iffD1}
   166   val iffD2 = @{thm iffD2}
   167   val notE = @{thm notE}
   168 );
   169 open Clasimp;
   170 
   171 val mksimps_pairs =
   172  [(@{const_name HOL.implies}, [@{thm mp}]),
   173   (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
   174   (@{const_name All}, [@{thm spec}]),
   175   (@{const_name True}, []),
   176   (@{const_name False}, []),
   177   (@{const_name If}, [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
   178 
   179 val HOL_basic_ss =
   180   empty_simpset @{context}
   181   setSSolver safe_solver
   182   setSolver unsafe_solver
   183   |> Simplifier.set_subgoaler asm_simp_tac
   184   |> Simplifier.set_mksimps (mksimps mksimps_pairs)
   185   |> Simplifier.set_mkeqTrue mk_eq_True
   186   |> Simplifier.set_mkcong mk_meta_cong
   187   |> simpset_of;
   188 
   189 fun hol_simplify ctxt rews =
   190   Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews);
   191 
   192 fun unfold_tac ctxt ths =
   193   ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths));
   194 
   195 end;
   196 
   197 structure Splitter = Simpdata.Splitter;
   198 structure Clasimp = Simpdata.Clasimp;