summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 |