src/HOL/Library/Extended.thy
changeset 55124 ffabc0a5853e
parent 54489 03ff4d1e6784
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/Library/Extended.thy	Thu Jan 23 14:26:16 2014 +0100
     1.2 +++ b/src/HOL/Library/Extended.thy	Thu Jan 23 14:33:54 2014 +0100
     1.3 @@ -77,12 +77,16 @@
     1.4  instance ..
     1.5  end
     1.6  
     1.7 +declare zero_extended_def[symmetric, code_post]
     1.8 +
     1.9  instantiation extended :: (one)one
    1.10  begin
    1.11  definition "1 = Fin(1::'a)"
    1.12  instance ..
    1.13  end
    1.14  
    1.15 +declare one_extended_def[symmetric, code_post]
    1.16 +
    1.17  instantiation extended :: (plus)plus
    1.18  begin
    1.19  
    1.20 @@ -155,13 +159,13 @@
    1.21  
    1.22  instance extended :: ("{ab_semigroup_add,one}")numeral ..
    1.23  
    1.24 -lemma Fin_numeral: "Fin(numeral w) = numeral w"
    1.25 +lemma Fin_numeral[code_post]: "Fin(numeral w) = numeral w"
    1.26    apply (induct w rule: num_induct)
    1.27    apply (simp only: numeral_One one_extended_def)
    1.28    apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
    1.29    done
    1.30  
    1.31 -lemma Fin_neg_numeral: "Fin (- numeral w) = - numeral w"
    1.32 +lemma Fin_neg_numeral[code_post]: "Fin (- numeral w) = - numeral w"
    1.33  by (simp only: Fin_numeral uminus_extended.simps[symmetric])
    1.34  
    1.35