Created
November 8, 2017 19:37
-
-
Save DengYiping/9d4b4a43b1d64e7239eb912134e869c1 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| theory ExponentialDiophantine | |
| imports Main Nat Int Complex Real HOL | |
| begin | |
| (* | |
| * second order recurrence function | |
| * the first argument is the index | |
| * the second argument is the b in the recurrence | |
| *) | |
| fun Abn :: "nat \<Rightarrow> int \<Rightarrow> int" where | |
| Abn_base0: "Abn 0 b = 0" | |
| | Abn_base1: "Abn (Suc 0) b = 1" | |
| | Abn_recur: "Abn n b = b * (Abn (n -1) b) - (Abn (n - 2) b)" | |
| lemma recur_non_negativity_monotone: | |
| fixes b :: int and n :: nat | |
| assumes "b \<ge> 2" | |
| shows "0 \<le> Abn n b \<and> Abn n b \<le> Abn (Suc n) b" | |
| proof(induction n) | |
| case 0 | |
| then show ?case by(simp) | |
| next | |
| case (Suc n) | |
| from assms have step1:"b - 1 \<ge> 1" by(simp) | |
| from Suc.IH have non_zero_property:"0 \<le> ((Abn (Suc n) b)::int)" by(simp) | |
| from step1 have ineq1:"1 \<le> (Abn (Suc n) b) \<Longrightarrow> (b - 1) * (Abn (Suc n) b) \<ge> 1 * (Abn (Suc n) b)" by(simp) | |
| have ineq2:"(Abn (Suc n) b) = (0::int) \<Longrightarrow> (b - 1) * (Abn (Suc n) b) \<ge> 1 * (Abn (Suc n) b)" by(simp) | |
| from ineq1 ineq2 have ineq3:"1 \<le> (Abn (Suc n) b) \<or> (Abn (Suc n) b) = 0 \<Longrightarrow> (b - 1) * (Abn (Suc n) b) \<ge> 1 * (Abn (Suc n) b)" by(auto) | |
| have ineq4:"1 \<le> (Abn (Suc n) b) \<or> (Abn (Suc n) b) = 0 \<Longrightarrow> 0 \<le> (Abn (Suc n) b)" by(force) | |
| from ineq3 ineq4 non_zero_property have multi_property:"(b - 1) * (Abn (Suc n) b) \<ge> (Abn (Suc n) b)" by(force) | |
| from multi_property Suc.IH have not_expanded:"(b - 1) * (Abn (Suc n) b) \<ge> Abn n b" by(simp) | |
| from not_expanded have last:"b * (Abn (Suc n) b) - Abn n b \<ge> Abn (Suc n) b" by(simp add:algebra_simps) | |
| from last non_zero_property show ?case by(auto) | |
| qed | |
| end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment