src/HOL/Power.thy
changeset 63040 eb4ddd18d635
parent 62481 b5d8e57826df
child 63417 c184ec919c70
equal deleted inserted replaced
63039:1a20fd9cf281 63040:eb4ddd18d635
    88   "(times x ^^ f x) = times (x ^ f x)"
    88   "(times x ^^ f x) = times (x ^ f x)"
    89 proof (induct "f x" arbitrary: f)
    89 proof (induct "f x" arbitrary: f)
    90   case 0 then show ?case by (simp add: fun_eq_iff)
    90   case 0 then show ?case by (simp add: fun_eq_iff)
    91 next
    91 next
    92   case (Suc n)
    92   case (Suc n)
    93   def g \<equiv> "\<lambda>x. f x - 1"
    93   define g where "g x = f x - 1" for x
    94   with Suc have "n = g x" by simp
    94   with Suc have "n = g x" by simp
    95   with Suc have "times x ^^ g x = times (x ^ g x)" by simp
    95   with Suc have "times x ^^ g x = times (x ^ g x)" by simp
    96   moreover from Suc g_def have "f x = g x + 1" by simp
    96   moreover from Suc g_def have "f x = g x + 1" by simp
    97   ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc)
    97   ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc)
    98 qed
    98 qed