mk_atomize: careful matching against rules admits overloading;
authorwenzelm
Sun Nov 12 21:14:49 2006 +0100 (2006-11-12)
changeset 2131326fc3a45547c
parent 21312 1d39091a3208
child 21314 6d709b9bea1a
mk_atomize: careful matching against rules admits overloading;
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Sun Nov 12 19:22:10 2006 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Sun Nov 12 21:14:49 2006 +0100
     1.3 @@ -94,23 +94,27 @@
     1.4       else error "Conclusion of congruence rules must be =-equality"
     1.5     end);
     1.6  
     1.7 -(*
     1.8 -val mk_atomize:      (string * thm list) list -> thm -> thm list
     1.9 -looks too specific to move it somewhere else
    1.10 -*)
    1.11  fun mk_atomize pairs =
    1.12    let
    1.13 -    fun atoms thm = case concl_of thm
    1.14 -     of Const("Trueprop", _) $ p => (case head_of p
    1.15 -        of Const(a, _) => (case AList.lookup (op =) pairs a
    1.16 -           of SOME rls => maps atoms ([thm] RL rls)
    1.17 -            | NONE => [thm])
    1.18 -         | _ => [thm])
    1.19 -      | _ => [thm]
    1.20 +    fun atoms thm =
    1.21 +      let
    1.22 +        fun res th = map (fn rl => th RS rl);   (*exception THM*)
    1.23 +        fun res_fixed rls =
    1.24 +          if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
    1.25 +          else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm];
    1.26 +      in
    1.27 +        case concl_of thm
    1.28 +          of Const ("Trueprop", _) $ p => (case head_of p
    1.29 +            of Const (a, _) => (case AList.lookup (op =) pairs a
    1.30 +              of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm])
    1.31 +              | NONE => [thm])
    1.32 +            | _ => [thm])
    1.33 +          | _ => [thm]
    1.34 +      end;
    1.35    in atoms end;
    1.36  
    1.37  fun mksimps pairs =
    1.38 -  (map_filter (try mk_eq) o mk_atomize pairs o gen_all);
    1.39 +  map_filter (try mk_eq) o mk_atomize pairs o gen_all;
    1.40  
    1.41  fun unsafe_solver_tac prems =
    1.42    (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
    1.43 @@ -142,6 +146,7 @@
    1.44  
    1.45  structure Splitter = SplitterFun(SplitterData);
    1.46  
    1.47 +
    1.48  (* integration of simplifier with classical reasoner *)
    1.49  
    1.50  structure Clasimp = ClasimpFun
    1.51 @@ -174,6 +179,8 @@
    1.52    let val ss0 = Simplifier.clear_ss simpset_basic addsimps ths
    1.53    in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
    1.54  
    1.55 +
    1.56 +
    1.57  (** simprocs **)
    1.58  
    1.59  (* simproc for proving "(y = x) == False" from premise "~(x = y)" *)
    1.60 @@ -199,7 +206,7 @@
    1.61  
    1.62  val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover;
    1.63  
    1.64 -end; (*local*)
    1.65 +end;
    1.66  
    1.67  
    1.68  (* simproc for Let *)
    1.69 @@ -259,7 +266,8 @@
    1.70          | _ => NONE)
    1.71       end)
    1.72  
    1.73 -end; (*local*)
    1.74 +end;
    1.75 +
    1.76  
    1.77  (* generic refutation procedure *)
    1.78  
    1.79 @@ -301,7 +309,7 @@
    1.80              REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
    1.81              SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
    1.82    end;
    1.83 -end; (*local*)
    1.84 +end;
    1.85  
    1.86  val defALL_regroup =
    1.87    Simplifier.simproc (the_context ())
    1.88 @@ -315,4 +323,4 @@
    1.89  val simpset_simprocs = simpset_basic
    1.90    addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc]
    1.91  
    1.92 -end; (*struct*)
    1.93 \ No newline at end of file
    1.94 +end;