src/HOL/Num.thy
changeset 55415 05f5fdb8d093
parent 54489 03ff4d1e6784
child 55534 b18bdcbda41b
     1.1 --- a/src/HOL/Num.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Num.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -1050,24 +1050,24 @@
     1.4    "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
     1.5    by (simp add: numeral_eq_Suc)
     1.6  
     1.7 -text {* For @{term nat_case} and @{term nat_rec}. *}
     1.8 +text {* For @{term case_nat} and @{term rec_nat}. *}
     1.9  
    1.10 -lemma nat_case_numeral [simp]:
    1.11 -  "nat_case a f (numeral v) = (let pv = pred_numeral v in f pv)"
    1.12 +lemma case_nat_numeral [simp]:
    1.13 +  "case_nat a f (numeral v) = (let pv = pred_numeral v in f pv)"
    1.14    by (simp add: numeral_eq_Suc)
    1.15  
    1.16 -lemma nat_case_add_eq_if [simp]:
    1.17 -  "nat_case a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
    1.18 +lemma case_nat_add_eq_if [simp]:
    1.19 +  "case_nat a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
    1.20    by (simp add: numeral_eq_Suc)
    1.21  
    1.22 -lemma nat_rec_numeral [simp]:
    1.23 -  "nat_rec a f (numeral v) =
    1.24 -    (let pv = pred_numeral v in f pv (nat_rec a f pv))"
    1.25 +lemma rec_nat_numeral [simp]:
    1.26 +  "rec_nat a f (numeral v) =
    1.27 +    (let pv = pred_numeral v in f pv (rec_nat a f pv))"
    1.28    by (simp add: numeral_eq_Suc Let_def)
    1.29  
    1.30 -lemma nat_rec_add_eq_if [simp]:
    1.31 -  "nat_rec a f (numeral v + n) =
    1.32 -    (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))"
    1.33 +lemma rec_nat_add_eq_if [simp]:
    1.34 +  "rec_nat a f (numeral v + n) =
    1.35 +    (let pv = pred_numeral v in f (pv + n) (rec_nat a f (pv + n)))"
    1.36    by (simp add: numeral_eq_Suc Let_def)
    1.37  
    1.38  text {* Case analysis on @{term "n < 2"} *}