reimplement reorientation simproc using theory data
authorhuffman
Wed Apr 29 17:15:01 2009 -0700 (2009-04-29)
changeset 310240fdf666e08bf
parent 31023 d027411c9a38
child 31025 6d2188134536
reimplement reorientation simproc using theory data
src/HOL/HOL.thy
src/HOL/Int.thy
src/HOL/Nat.thy
src/HOL/Tools/int_arith.ML
src/HOLCF/Pcpo.thy
     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"
     2.1 --- a/src/HOL/Int.thy	Wed Apr 29 13:36:29 2009 -0700
     2.2 +++ b/src/HOL/Int.thy	Wed Apr 29 17:15:01 2009 -0700
     2.3 @@ -1518,6 +1518,13 @@
     2.4  use "Tools/int_arith.ML"
     2.5  declaration {* K Int_Arith.setup *}
     2.6  
     2.7 +setup {*
     2.8 +  ReorientProc.add
     2.9 +    (fn Const(@{const_name number_of}, _) $ _ => true | _ => false)
    2.10 +*}
    2.11 +
    2.12 +simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc
    2.13 +
    2.14  
    2.15  subsection{*Lemmas About Small Numerals*}
    2.16  
     3.1 --- a/src/HOL/Nat.thy	Wed Apr 29 13:36:29 2009 -0700
     3.2 +++ b/src/HOL/Nat.thy	Wed Apr 29 17:15:01 2009 -0700
     3.3 @@ -1274,10 +1274,10 @@
     3.4  text{*Special cases where either operand is zero*}
     3.5  
     3.6  lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
     3.7 -  by (rule of_nat_eq_iff [of 0, simplified])
     3.8 +  by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
     3.9  
    3.10  lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
    3.11 -  by (rule of_nat_eq_iff [of _ 0, simplified])
    3.12 +  by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
    3.13  
    3.14  lemma inj_of_nat: "inj of_nat"
    3.15    by (simp add: inj_on_def)
     4.1 --- a/src/HOL/Tools/int_arith.ML	Wed Apr 29 13:36:29 2009 -0700
     4.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Apr 29 17:15:01 2009 -0700
     4.3 @@ -6,27 +6,6 @@
     4.4  structure Int_Numeral_Simprocs =
     4.5  struct
     4.6  
     4.7 -(*reorientation simprules using ==, for the following simproc*)
     4.8 -val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
     4.9 -val meta_one_reorient = @{thm one_reorient} RS eq_reflection
    4.10 -val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
    4.11 -
    4.12 -(*reorientation simplification procedure: reorients (polymorphic) 
    4.13 -  0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
    4.14 -fun reorient_proc sg _ (_ $ t $ u) =
    4.15 -  case u of
    4.16 -      Const(@{const_name HOL.zero}, _) => NONE
    4.17 -    | Const(@{const_name HOL.one}, _) => NONE
    4.18 -    | Const(@{const_name Int.number_of}, _) $ _ => NONE
    4.19 -    | _ => SOME (case t of
    4.20 -        Const(@{const_name HOL.zero}, _) => meta_zero_reorient
    4.21 -      | Const(@{const_name HOL.one}, _) => meta_one_reorient
    4.22 -      | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
    4.23 -
    4.24 -val reorient_simproc = 
    4.25 -  Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
    4.26 -
    4.27 -
    4.28  (** Utilities **)
    4.29  
    4.30  fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
    4.31 @@ -383,7 +362,6 @@
    4.32  
    4.33  end;
    4.34  
    4.35 -Addsimprocs [Int_Numeral_Simprocs.reorient_simproc];
    4.36  Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
    4.37  Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
    4.38  Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
     5.1 --- a/src/HOLCF/Pcpo.thy	Wed Apr 29 13:36:29 2009 -0700
     5.2 +++ b/src/HOLCF/Pcpo.thy	Wed Apr 29 17:15:01 2009 -0700
     5.3 @@ -193,26 +193,14 @@
     5.4  lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
     5.5  by (rule UU_least [THEN spec])
     5.6  
     5.7 -lemma UU_reorient: "(\<bottom> = x) = (x = \<bottom>)"
     5.8 -by auto
     5.9 +text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
    5.10  
    5.11 -ML {*
    5.12 -local
    5.13 -  val meta_UU_reorient = thm "UU_reorient" RS eq_reflection;
    5.14 -  fun reorient_proc sg _ (_ $ t $ u) =
    5.15 -    case u of
    5.16 -        Const("Pcpo.UU",_) => NONE
    5.17 -      | Const("HOL.zero", _) => NONE
    5.18 -      | Const("HOL.one", _) => NONE
    5.19 -      | Const("Numeral.number_of", _) $ _ => NONE
    5.20 -      | _ => SOME meta_UU_reorient;
    5.21 -in
    5.22 -  val UU_reorient_simproc = 
    5.23 -    Simplifier.simproc (the_context ()) "UU_reorient_simproc" ["UU=x"] reorient_proc
    5.24 -end;
    5.25 +setup {*
    5.26 +  ReorientProc.add
    5.27 +    (fn Const(@{const_name UU}, _) => true | _ => false)
    5.28 +*}
    5.29  
    5.30 -Addsimprocs [UU_reorient_simproc];
    5.31 -*}
    5.32 +simproc_setup reorient_bottom ("\<bottom> = x") = ReorientProc.proc
    5.33  
    5.34  text {* useful lemmas about @{term \<bottom>} *}
    5.35