src/HOL/HOL.thy
changeset 31024 0fdf666e08bf
parent 30980 fe0855471964
child 31125 80218ee73167
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 29 13:36:29 2009 -0700
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 29 17:15:01 2009 -0700
     1.3 @@ -1568,6 +1568,56 @@
     1.4  setup Coherent.setup
     1.5  
     1.6  
     1.7 +subsubsection {* Reorienting equalities *}
     1.8 +
     1.9 +ML {*
    1.10 +signature REORIENT_PROC =
    1.11 +sig
    1.12 +  val init : theory -> theory
    1.13 +  val add : (term -> bool) -> theory -> theory
    1.14 +  val proc : morphism -> simpset -> cterm -> thm option
    1.15 +end;
    1.16 +
    1.17 +structure ReorientProc : REORIENT_PROC =
    1.18 +struct
    1.19 +  structure Data = TheoryDataFun
    1.20 +  (
    1.21 +    type T = term -> bool;
    1.22 +    val empty = (fn _ => false);
    1.23 +    val copy = I;
    1.24 +    val extend = I;
    1.25 +    fun merge _ (m1, m2) = (fn t => m1 t orelse m2 t);
    1.26 +  )
    1.27 +
    1.28 +  val init = Data.init;
    1.29 +  fun add m = Data.map (fn matches => fn t => matches t orelse m t);
    1.30 +  val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
    1.31 +  fun proc phi ss ct =
    1.32 +    let
    1.33 +      val ctxt = Simplifier.the_context ss;
    1.34 +      val thy = ProofContext.theory_of ctxt;
    1.35 +      val matches = Data.get thy;
    1.36 +    in
    1.37 +      case Thm.term_of ct of
    1.38 +        (_ $ t $ u) => if matches u then NONE else SOME meta_reorient
    1.39 +      | _ => NONE
    1.40 +    end;
    1.41 +end;
    1.42 +*}
    1.43 +
    1.44 +setup ReorientProc.init
    1.45 +
    1.46 +setup {*
    1.47 +  ReorientProc.add
    1.48 +    (fn Const(@{const_name HOL.zero}, _) => true
    1.49 +      | Const(@{const_name HOL.one}, _) => true
    1.50 +      | _ => false)
    1.51 +*}
    1.52 +
    1.53 +simproc_setup reorient_zero ("0 = x") = ReorientProc.proc
    1.54 +simproc_setup reorient_one ("1 = x") = ReorientProc.proc
    1.55 +
    1.56 +
    1.57  subsection {* Other simple lemmas and lemma duplicates *}
    1.58  
    1.59  lemma Let_0 [simp]: "Let 0 f = f 0"