rewrite op = == eq handled by simproc
authorhaftmann
Thu May 14 09:16:34 2009 +0200 (2009-05-14)
changeset 311511c64b0827ee8
parent 31150 03a87478b89e
child 31152 e79d1ff2abc5
rewrite op = == eq handled by simproc
src/HOL/HOL.thy
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/src/HOL/HOL.thy	Thu May 14 09:16:33 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu May 14 09:16:34 2009 +0200
     1.3 @@ -1331,7 +1331,7 @@
     1.4      of Abs (_, _, t') => count_loose t' 0 <= 1
     1.5       | _ => true;
     1.6  in fn _ => fn ss => fn ct => if is_trivial_let (Thm.term_of ct)
     1.7 -  then SOME @{thm Let_def} (*no or one ocurrenc of bound variable*)
     1.8 +  then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
     1.9    else let (*Norbert Schirmer's case*)
    1.10      val ctxt = Simplifier.the_context ss;
    1.11      val thy = ProofContext.theory_of ctxt;
    1.12 @@ -1775,6 +1775,13 @@
    1.13  end
    1.14  *}
    1.15  
    1.16 +subsubsection {* Generic code generator preprocessor setup *}
    1.17 +
    1.18 +setup {*
    1.19 +  Code_Preproc.map_pre (K HOL_basic_ss)
    1.20 +  #> Code_Preproc.map_post (K HOL_basic_ss)
    1.21 +*}
    1.22 +
    1.23  subsubsection {* Equality *}
    1.24  
    1.25  class eq =
    1.26 @@ -1788,7 +1795,7 @@
    1.27  lemma eq_refl: "eq x x \<longleftrightarrow> True"
    1.28    unfolding eq by rule+
    1.29  
    1.30 -lemma equals_eq [code inline]: "(op =) \<equiv> eq"
    1.31 +lemma equals_eq: "(op =) \<equiv> eq"
    1.32    by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    1.33  
    1.34  declare equals_eq [symmetric, code post]
    1.35 @@ -1797,6 +1804,14 @@
    1.36  
    1.37  declare equals_eq [code]
    1.38  
    1.39 +setup {*
    1.40 +  Code_Preproc.map_pre (fn simpset =>
    1.41 +    simpset addsimprocs [Simplifier.simproc_i @{theory} "eq" [@{term "op ="}]
    1.42 +      (fn thy => fn _ => fn t as Const (_, T) => case strip_type T
    1.43 +        of ((T as Type _) :: _, _) => SOME @{thm equals_eq}
    1.44 +         | _ => NONE)])
    1.45 +*}
    1.46 +
    1.47  
    1.48  subsubsection {* Generic code generator foundation *}
    1.49  
    1.50 @@ -1851,18 +1866,17 @@
    1.51    "eq_class.eq TYPE('a) TYPE('a) \<longleftrightarrow> True"
    1.52    by (simp add: eq)
    1.53  
    1.54 -
    1.55  text {* Equality *}
    1.56  
    1.57  declare simp_thms(6) [code nbe]
    1.58  
    1.59 -hide (open) const eq
    1.60 -hide const eq
    1.61 -
    1.62  setup {*
    1.63    Code_Unit.add_const_alias @{thm equals_eq}
    1.64  *}
    1.65  
    1.66 +hide (open) const eq
    1.67 +hide const eq
    1.68 +
    1.69  text {* Cases *}
    1.70  
    1.71  lemma Let_case_cert:
    1.72 @@ -1883,13 +1897,6 @@
    1.73  
    1.74  code_abort undefined
    1.75  
    1.76 -subsubsection {* Generic code generator preprocessor *}
    1.77 -
    1.78 -setup {*
    1.79 -  Code_Preproc.map_pre (K HOL_basic_ss)
    1.80 -  #> Code_Preproc.map_post (K HOL_basic_ss)
    1.81 -*}
    1.82 -
    1.83  subsubsection {* Generic code generator target languages *}
    1.84  
    1.85  text {* type bool *}
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu May 14 09:16:33 2009 +0200
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu May 14 09:16:34 2009 +0200
     2.3 @@ -368,8 +368,7 @@
     2.4        addsimps (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms))
     2.5        addsimprocs [DatatypePackage.distinct_simproc]);
     2.6      fun prove prop = Goal.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
     2.7 -      |> Simpdata.mk_eq
     2.8 -      |> Simplifier.rewrite_rule [@{thm equals_eq}];
     2.9 +      |> Simpdata.mk_eq;
    2.10    in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
    2.11  
    2.12  fun add_equality vs dtcos thy =