'(*' Comment ' from Isabelle2021-1 src/HOL/Power.thy; BSD license ' Comment '*)' Comment '\n\n' Text.Whitespace '(*' Comment ' Title: HOL/Power.thy\n Author: Lawrence C Paulson, Cambridge University Computer Laboratory\n Copyright 1997 University of Cambridge\n' Comment '*)' Comment '\n\n' Text.Whitespace 'section' Generic.Subheading ' ' Text.Whitespace '‹' Literal.String 'Exponentiation' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'theory' Keyword ' ' Text.Whitespace 'Power' Name '\n ' Text.Whitespace 'imports' Keyword.Pseudo ' ' Text.Whitespace 'Num' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'subsection' Generic.Subheading ' ' Text.Whitespace '‹' Literal.String 'Powers for Arbitrary Monoids' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'class' Keyword ' ' Text.Whitespace 'power' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'one' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'times' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'primrec' Keyword ' ' Text.Whitespace 'power' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace '"' Literal.String "'a ⇒ nat ⇒ 'a" Literal.String '"' Literal.String ' ' Text.Whitespace '(' Operator 'infixr' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String '^' Literal.String '"' Literal.String ' ' Text.Whitespace '80' Name ')' Operator '\n ' Text.Whitespace 'where' Keyword.Pseudo '\n ' Text.Whitespace 'power_0' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ 0 = 1' Literal.String '"' Literal.String '\n ' Text.Whitespace '|' Operator ' ' Text.Whitespace 'power_Suc' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ Suc n = a * a ^ n' Literal.String '"' Literal.String '\n\n' Text.Whitespace 'notation' Keyword ' ' Text.Whitespace '(' Operator 'latex' Name ' ' Text.Whitespace 'output' Keyword.Pseudo ')' Operator '\n ' Text.Whitespace 'power' Name ' ' Text.Whitespace '(' Operator '"' Literal.String '(_⇗_⇖)' Literal.String '"' Literal.String ' ' Text.Whitespace '[' Operator '1000' Name ']' Operator ' ' Text.Whitespace '1000' Name ')' Operator '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'Special syntax for squares.' Literal.String '›' Literal.String '\n' Text.Whitespace 'abbreviation' Keyword ' ' Text.Whitespace 'power2' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace '"' Literal.String "'a ⇒ 'a" Literal.String '"' Literal.String ' ' Text.Whitespace '(' Operator '"' Literal.String '(_⇧2)' Literal.String '"' Literal.String ' ' Text.Whitespace '[' Operator '1000' Name ']' Operator ' ' Text.Whitespace '999' Name ')' Operator '\n ' Text.Whitespace 'where' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'x⇧2 ≡ x ^ 2' Literal.String '"' Literal.String '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword '\n ' Text.Whitespace 'includes' Keyword.Pseudo ' ' Text.Whitespace 'lifting_syntax' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_transfer' Name ' ' Text.Whitespace '[' Operator 'transfer_rule' Name ']' Operator ':' Operator '\n ' Text.Whitespace '‹' Literal.String '(R ===> (=) ===> R) (^) (^)' Literal.String '›' Literal.String '\n ' Text.Whitespace 'if' Keyword.Pseudo ' ' Text.Whitespace '[' Operator 'transfer_rule' Name ']' Operator ':' Operator ' ' Text.Whitespace '‹' Literal.String 'R 1 1' Literal.String '›' Literal.String '\n ' Text.Whitespace '‹' Literal.String '(R ===> R ===> R) (' Literal.String '*' Literal.String ') (' Literal.String '*' Literal.String ')' Literal.String '›' Literal.String '\n ' Text.Whitespace 'for' Keyword.Pseudo ' ' Text.Whitespace 'R' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace '‹' Literal.String "'a::power ⇒ 'b::power ⇒ bool" Literal.String '›' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'power_def' Name ' ' Text.Whitespace '[' Operator 'abs_def' Name ']' Operator ')' Operator ' ' Text.Whitespace 'transfer_prover' Name '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'monoid_mult' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'subclass' Keyword.Namespace ' ' Text.Whitespace 'power' Name ' ' Text.Whitespace '.' Operator.Word '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_one' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '1 ^ n = 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'simp_all' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_one_right' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ 1 = a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_Suc0_right' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ Suc 0 = a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_commutes' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ n * a = a * a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'mult.assoc' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_Suc2' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ Suc n = a ^ n * a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_commutes' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_add' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ (m + n) = a ^ m * a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'm' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'algebra_simps' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_mult' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ (m * n) = (a ^ m) ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_add' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_even_eq' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ (2 * n) = (a ^ n)⇧2' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'subst' Name ' ' Text.Whitespace 'mult.commute' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_mult' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_odd_eq' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ Suc (2*n) = a * (a ^ n)⇧2' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_even_eq' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_numeral_even' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'numeral_Bit0' Name ' ' Text.Whitespace 'power_add' Name ' ' Text.Whitespace 'Let_def' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_numeral_odd' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'numeral_Bit1' Name ' ' Text.Whitespace 'One_nat_def' Name ' ' Text.Whitespace 'add_Suc_right' Name ' ' Text.Whitespace 'add_0_right' Name '\n ' Text.Whitespace 'power_Suc' Name ' ' Text.Whitespace 'power_add' Name ' ' Text.Whitespace 'Let_def' Name ' ' Text.Whitespace 'mult.assoc' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_eq_square' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a⇧2 = a * a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'numeral_2_eq_2' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power3_eq_cube' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ 3 = a * a * a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'numeral_3_eq_3' Name ' ' Text.Whitespace 'mult.assoc' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power4_eq_xxxx' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x^4 = x * x * x * x' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'mult.assoc' Name ' ' Text.Whitespace 'power_numeral_even' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'funpow_times_power' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '(times x ^^ f x) = times (x ^ f x)' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace '"' Literal.String 'f x' Literal.String '"' Literal.String ' ' Text.Whitespace 'arbitrary' Name ':' Operator ' ' Text.Whitespace 'f' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'fun_eq_iff' Name ')' Operator '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'define' Name ' ' Text.Whitespace 'g' Name ' ' Text.Whitespace 'where' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'g x = f x - 1' Literal.String '"' Literal.String ' ' Text.Whitespace 'for' Keyword.Pseudo ' ' Text.Whitespace 'x' Name '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace 'Suc' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'n = g x' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace 'Suc' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'times x ^^ g x = times (x ^ g x)' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'moreover' Keyword ' ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'Suc' Name ' ' Text.Whitespace 'g_def' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'f x = g x + 1' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'ultimately' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_add' Name ' ' Text.Whitespace 'funpow_add' Name ' ' Text.Whitespace 'fun_eq_iff' Name ' ' Text.Whitespace 'mult.assoc' Name ')' Operator '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_commuting_commutes' Name ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'x * y = y * x' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'x ^ n * y = y * x ^n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'x ^ Suc n * y = x ^ n * y * x' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'subst' Name ' ' Text.Whitespace 'power_Suc2' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'assms' Name ' ' Text.Whitespace 'ac_simps' Name ')' Operator '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '… = y * x ^ Suc n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'Suc' Name ' ' Text.Whitespace 'power_Suc2' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'ac_simps' Name ')' Operator '\n ' Text.Whitespace 'finally' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace '.' Operator.Word '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_minus_mult' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < n ⟹ a ^ (n - 1) * a = a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_commutes' Name ' ' Text.Whitespace 'split' Name ':' Operator ' ' Text.Whitespace 'nat_diff_split' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'left_right_inverse_power' Name ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'x * y = 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'x ^ n * y ^ n = 1' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'moreover' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'x ^ Suc n * y ^ Suc n = x^n * (x * y) * y^n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_Suc2' Name '[' Operator 'symmetric' Name ']' Operator ' ' Text.Whitespace 'mult.assoc' Name '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n ' Text.Whitespace 'ultimately' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'assms' Name ')' Operator '\n' Text.Whitespace 'qed' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'comm_monoid_mult' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_mult_distrib' Name ' ' Text.Whitespace '[' Operator 'algebra_simps' Name ',' Operator ' ' Text.Whitespace 'algebra_split_simps' Name ',' Operator ' ' Text.Whitespace 'field_simps' Name ',' Operator ' ' Text.Whitespace 'field_split_simps' Name ',' Operator ' ' Text.Whitespace 'divide_simps' Name ']' Operator ':' Operator '\n ' Text.Whitespace '"' Literal.String '(a * b) ^ n = (a ^ n) * (b ^ n)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induction' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'ac_simps' Name ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'Extract constant factors from powers.' Literal.String '›' Literal.String '\n' Text.Whitespace 'declare' Keyword ' ' Text.Whitespace 'power_mult_distrib' Name ' ' Text.Whitespace '[' Operator 'where' Keyword.Pseudo ' ' Text.Whitespace 'a' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace '"' Literal.String 'numeral w' Literal.String '"' Literal.String ' ' Text.Whitespace 'for' Keyword.Pseudo ' ' Text.Whitespace 'w' Name ',' Operator ' ' Text.Whitespace 'simp' Name ']' Operator '\n' Text.Whitespace 'declare' Keyword ' ' Text.Whitespace 'power_mult_distrib' Name ' ' Text.Whitespace '[' Operator 'where' Keyword.Pseudo ' ' Text.Whitespace 'b' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace '"' Literal.String 'numeral w' Literal.String '"' Literal.String ' ' Text.Whitespace 'for' Keyword.Pseudo ' ' Text.Whitespace 'w' Name ',' Operator ' ' Text.Whitespace 'simp' Name ']' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_add_numeral' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'a^numeral m * a^numeral n = a^numeral (m + n)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'for' Keyword.Pseudo ' ' Text.Whitespace 'a' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace '"' Literal.String "'a::monoid_mult" Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_add' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_add_numeral2' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b' Literal.String '"' Literal.String '\n ' Text.Whitespace 'for' Keyword.Pseudo ' ' Text.Whitespace 'a' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace '"' Literal.String "'a::monoid_mult" Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'mult.assoc' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_mult_numeral' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(a^numeral m)^numeral n = a^numeral (m * n)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'for' Keyword.Pseudo ' ' Text.Whitespace 'a' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace '"' Literal.String "'a::monoid_mult" Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'numeral_mult' Name ' ' Text.Whitespace 'power_mult' Name ')' Operator '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'semiring_numeral' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'numeral_sqr' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'numeral (Num.sqr k) = numeral k * numeral k' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'sqr_conv_mult' Name ' ' Text.Whitespace 'numeral_mult' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'numeral_pow' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'numeral (Num.pow k l) = numeral k ^ numeral l' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'l' Name ')' Operator '\n ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'numeral_class.numeral.simps' Name ' ' Text.Whitespace 'pow.simps' Name '\n ' Text.Whitespace 'numeral_sqr' Name ' ' Text.Whitespace 'numeral_mult' Name ' ' Text.Whitespace 'power_add' Name ' ' Text.Whitespace 'power_one_right' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_numeral' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'numeral k ^ numeral l = numeral (Num.pow k l)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'numeral_pow' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'semiring_1' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'of_nat_power' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'of_nat (m ^ n) = of_nat m ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'simp_all' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'zero_power' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < n ⟹ 0 ^ n = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'simp_all' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_zero_numeral' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ^ numeral k = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'numeral_eq_Suc' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'zero_power2' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0⇧2 = 0' Literal.String '"' Literal.String ' ' Text.Whitespace '(*' Comment ' delete? ' Comment '*)' Comment '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'power_zero_numeral' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'one_power2' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '1⇧2 = 1' Literal.String '"' Literal.String ' ' Text.Whitespace '(*' Comment ' delete? ' Comment '*)' Comment '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'power_one' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_0_Suc' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ^ Suc n = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'It looks plausible as a simprule, but its effect can be strange.' Literal.String '›' Literal.String '\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_0_left' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ^ n = (if n = 0 then 1 else 0)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'simp_all' Name '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'semiring_char_0' Name ' ' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'numeral_power_eq_of_nat_cancel_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace '"' Literal.String 'numeral x ^ n = of_nat y ⟷ numeral x ^ n = y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'of_nat_eq_iff' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'fastforce' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'real_of_nat_eq_numeral_power_cancel_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace '"' Literal.String 'of_nat y = numeral x ^ n ⟷ y = numeral x ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'numeral_power_eq_of_nat_cancel_iff' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'x' Name ' ' Text.Whitespace 'n' Name ' ' Text.Whitespace 'y' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'metis' Name ' ' Text.Whitespace '(' Operator 'mono_tags' Name ')' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'of_nat_eq_of_nat_power_cancel_iff' Name '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(of_nat b) ^ w = of_nat x ⟷ b ^ w = x' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'metis' Name ' ' Text.Whitespace 'of_nat_power' Name ' ' Text.Whitespace 'of_nat_eq_iff' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'of_nat_power_eq_of_nat_cancel_iff' Name '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'of_nat x = (of_nat b) ^ w ⟷ x = b ^ w' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'metis' Name ' ' Text.Whitespace 'of_nat_eq_of_nat_power_cancel_iff' Name ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'comm_semiring_1' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'The divides relation.' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'le_imp_power_dvd' Name ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'm ≤ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'a ^ m dvd a ^ n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword '\n ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'assms' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'a ^ n = a ^ (m + (n - m))' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '… = a ^ m * a ^ (n - m)' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'power_add' Name ')' Operator '\n ' Text.Whitespace 'finally' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '"' Literal.String 'a ^ n = a ^ m * a ^ (n - m)' Literal.String '"' Literal.String ' ' Text.Whitespace '.' Operator.Word '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_le_dvd' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ n dvd b ⟹ m ≤ n ⟹ a ^ m dvd b' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'dvd_trans' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace 'le_imp_power_dvd' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'dvd_power_same' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x dvd y ⟹ x ^ n dvd y ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'mult_dvd_mono' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'dvd_power_le' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x dvd y ⟹ m ≥ n ⟹ x ^ n dvd y ^ m' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'power_le_dvd' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace 'dvd_power_same' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'dvd_power' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace 'fixes' Keyword.Pseudo ' ' Text.Whitespace 'n' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace 'nat' Name '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'n > 0 ∨ x = 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'x dvd (x ^ n)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'assms' Name '\n' Text.Whitespace 'proof' Keyword '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '"' Literal.String '0 < n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'x ^ n = x ^ Suc (n - 1)' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '"' Literal.String 'x dvd (x ^ n)' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '"' Literal.String 'x = 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '"' Literal.String 'x dvd (x ^ n)' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'semiring_1_no_zero_divisors' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'subclass' Keyword.Namespace ' ' Text.Whitespace 'power' Name ' ' Text.Whitespace '.' Operator.Word '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_eq_0_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ n = 0 ⟷ a = 0 ∧ n > 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'auto' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_not_zero' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ≠ 0 ⟹ a ^ n ≠ 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'auto' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'zero_eq_power2' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'a⇧2 = 0 ⟷ a = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'power2_eq_square' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'ring_1' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_minus' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '(- a) ^ n = (- 1) ^ n * a ^ n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'del' Name ':' Operator ' ' Text.Whitespace 'power_Suc' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_Suc2' Name ' ' Text.Whitespace 'mult.assoc' Name ')' Operator '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace "power_minus'" Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'NO_MATCH 1 x ⟹ (-x) ^ n = (-1)^n * x ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'power_minus' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_minus_Bit0' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'k' Name ',' Operator ' ' Text.Whitespace 'simp_all' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'numeral_class.numeral.simps' Name ' ' Text.Whitespace 'power_add' Name '\n ' Text.Whitespace 'power_one_right' Name ' ' Text.Whitespace 'mult_minus_left' Name ' ' Text.Whitespace 'mult_minus_right' Name ' ' Text.Whitespace 'minus_minus' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_minus_Bit1' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'eval_nat_numeral' Name '(' Operator '3' Name ')' Operator ' ' Text.Whitespace 'power_Suc' Name ' ' Text.Whitespace 'power_minus_Bit0' Name ' ' Text.Whitespace 'mult_minus_left' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_minus' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(- a)⇧2 = a⇧2' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'fact' Name ' ' Text.Whitespace 'power_minus_Bit0' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_minus1_even' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(- 1) ^ (2*n) = 1' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_add' Name ' ' Text.Whitespace 'power2_eq_square' Name ')' Operator '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_minus1_odd' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '(- 1) ^ Suc (2*n) = -1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_minus_even' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(-a) ^ (2*n) = a ^ (2*n)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_minus' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'a' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'ring_1_no_zero_divisors' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_eq_1_iff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a⇧2 = 1 ⟷ a = 1 ∨ a = - 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'square_eq_1_iff' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'a' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power2_eq_square' Name ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'idom' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_eq_iff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x⇧2 = y⇧2 ⟷ x = y ∨ x = - y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'power2_eq_square' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'square_eq_iff' Name ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'semidom_divide' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_diff' Name ':' Operator '\n ' Text.Whitespace '"' Literal.String 'a ^ (m - n) = (a ^ m) div (a ^ n)' Literal.String '"' Literal.String ' ' Text.Whitespace 'if' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'a ≠ 0' Literal.String '"' Literal.String ' ' Text.Whitespace 'and' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'n ≤ m' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '-' Operator '\n ' Text.Whitespace 'define' Name ' ' Text.Whitespace 'q' Name ' ' Text.Whitespace 'where' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'q = m - n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace '‹' Literal.String 'n ≤ m' Literal.String '›' Literal.String ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'm = q + n' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace '‹' Literal.String 'a ≠ 0' Literal.String '›' Literal.String ' ' Text.Whitespace 'q_def' Name ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_add' Name ')' Operator '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'algebraic_semidom' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'div_power' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'b dvd a ⟹ (a div b) ^ n = a ^ n div b ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'div_mult_div_if_dvd' Name ' ' Text.Whitespace 'dvd_power_same' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'is_unit_power_iff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'is_unit (a ^ n) ⟷ is_unit a ∨ n = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'is_unit_mult_iff' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'dvd_power_iff' Name ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'x ≠ 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'x ^ m dvd x ^ n ⟷ is_unit x ∨ m ≤ n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '*' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x ^ m dvd x ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace '{' Operator.Word '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '"' Literal.String 'm > n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'note' Keyword ' ' Text.Whitespace '*' Name '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'x ^ n = x ^ n * 1' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace '‹' Literal.String 'm > n' Literal.String '›' Literal.String ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'm = n + (m - n)' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'x ^ … = x ^ n * x ^ (m - n)' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'power_add' Name ')' Operator '\n ' Text.Whitespace 'finally' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'x ^ (m - n) dvd 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'subst' Name ' ' Text.Whitespace '(' Operator 'asm' Name ')' Operator ' ' Text.Whitespace 'dvd_times_left_cancel_iff' Name ')' Operator ' ' Text.Whitespace '(' Operator 'insert' Name ' ' Text.Whitespace 'assms' Name ',' Operator ' ' Text.Whitespace 'simp_all' Name ')' Operator '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace '‹' Literal.String 'm > n' Literal.String '›' Literal.String ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'is_unit x' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'is_unit_power_iff' Name ')' Operator '\n ' Text.Whitespace '}' Operator.Word '\n ' Text.Whitespace 'thus' Keyword ' ' Text.Whitespace '"' Literal.String 'is_unit x ∨ m ≤ n' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'force' Name '\n' Text.Whitespace 'qed' Keyword ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'intro' Name ':' Operator ' ' Text.Whitespace 'unit_imp_dvd' Name ' ' Text.Whitespace 'simp' Name ':' Operator ' ' Text.Whitespace 'is_unit_power_iff' Name ' ' Text.Whitespace 'le_imp_power_dvd' Name ')' Operator '\n\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'normalization_semidom_multiplicative' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'normalize_power' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'normalize (a ^ n) = normalize a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'normalize_mult' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'unit_factor_power' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'unit_factor (a ^ n) = unit_factor a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'unit_factor_mult' Name ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'division_ring' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'Perhaps these should be simprules.' Literal.String '›' Literal.String '\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_inverse' Name ' ' Text.Whitespace '[' Operator 'field_simps' Name ',' Operator ' ' Text.Whitespace 'field_split_simps' Name ',' Operator ' ' Text.Whitespace 'divide_simps' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'inverse a ^ n = inverse (a ^ n)' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace '"' Literal.String 'a = 0' Literal.String '"' Literal.String ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace 'True' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_0_left' Name ')' Operator '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace 'False' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'inverse (a ^ n) = inverse a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'nonzero_inverse_mult_distrib' Name ' ' Text.Whitespace 'power_commutes' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_one_over' Name ' ' Text.Whitespace '[' Operator 'field_simps' Name ',' Operator ' ' Text.Whitespace 'field_split_simps' Name ',' Operator ' ' Text.Whitespace 'divide_simps' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(1 / a) ^ n = 1 / a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_inverse' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'a' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'divide_inverse' Name ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'field' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_divide' Name ' ' Text.Whitespace '[' Operator 'field_simps' Name ',' Operator ' ' Text.Whitespace 'field_split_simps' Name ',' Operator ' ' Text.Whitespace 'divide_simps' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(a / b) ^ n = a ^ n / b ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'simp_all' Name '\n\n' Text.Whitespace 'end' Keyword '\n\n\n' Text.Whitespace 'subsection' Generic.Subheading ' ' Text.Whitespace '‹' Literal.String 'Exponentiation on ordered types' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'linordered_semidom' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'zero_less_power' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < a ⟹ 0 < a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'simp_all' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'zero_le_power' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ≤ a ⟹ 0 ≤ a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'simp_all' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_mono' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ≤ b ⟹ 0 ≤ a ⟹ a ^ n ≤ b ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'intro' Name ':' Operator ' ' Text.Whitespace 'mult_mono' Name ' ' Text.Whitespace 'order_trans' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace '0' Name ' ' Text.Whitespace 'a' Name ' ' Text.Whitespace 'b' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'one_le_power' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '1 ≤ a ⟹ 1 ≤ a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_mono' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace '1' Name ' ' Text.Whitespace 'a' Name ' ' Text.Whitespace 'n' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_le_one' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ≤ a ⟹ a ≤ 1 ⟹ a ^ n ≤ 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_mono' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'a' Name ' ' Text.Whitespace '1' Name ' ' Text.Whitespace 'n' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_gt1_lemma' Name ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace 'gt1' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '1 < a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String '1 < a * a ^ n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '-' Operator '\n ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'gt1' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '0 ≤ a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'fact' Name ' ' Text.Whitespace 'order_trans' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace 'zero_le_one' Name ' ' Text.Whitespace 'less_imp_le' Name ']' Operator ')' Operator '\n ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'gt1' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '1 * 1 < a * 1' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'gt1' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '… ≤ a * a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'mult_mono' Name ' ' Text.Whitespace '‹' Literal.String '0 ≤ a' Literal.String '›' Literal.String ' ' Text.Whitespace 'one_le_power' Name ' ' Text.Whitespace 'order_less_imp_le' Name ' ' Text.Whitespace 'zero_le_one' Name ' ' Text.Whitespace 'order_refl' Name ')' Operator '\n ' Text.Whitespace 'finally' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_gt1' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '1 < a ⟹ 1 < a ^ Suc n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_gt1_lemma' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'one_less_power' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '1 < a ⟹ 0 < n ⟹ 1 < a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_gt1_lemma' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_le_imp_le_exp' Name ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace 'gt1' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '1 < a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'a ^ m ≤ a ^ n ⟹ m ≤ n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'm' Name ' ' Text.Whitespace 'arbitrary' Name ':' Operator ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'm' Name ')' Operator '\n ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace 'Suc' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'a * a ^ m ≤ 1' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace 'gt1' Name ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'force' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'power_gt1_lemma' Name ' ' Text.Whitespace 'not_less' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n ' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace 'Suc.prems' Name ' ' Text.Whitespace 'Suc.hyps' Name ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'force' Name ' ' Text.Whitespace 'dest' Name ':' Operator ' ' Text.Whitespace 'mult_left_le_imp_le' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'less_trans' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace 'zero_less_one' Name ' ' Text.Whitespace 'gt1' Name ']' Operator ')' Operator '\n ' Text.Whitespace 'qed' Keyword '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'of_nat_zero_less_power_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'of_nat x ^ n > 0 ⟷ x > 0 ∨ n = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'auto' Name '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'Surely we can strengthen this? It holds for ' Literal.String '‹' Literal.String '0' Literal.String.Symbol '‹' Literal.String '00⟧ ⟹ a ^ n ≤ b ^ n ⟷ a ≤ b' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_mono' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'a' Name ' ' Text.Whitespace 'b' Name ']' Operator ' ' Text.Whitespace 'power_strict_mono' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'b' Name ' ' Text.Whitespace 'a' Name ']' Operator ' ' Text.Whitespace 'not_le' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'auto' Name '\n\n' Text.Whitespace 'text' Keyword '‹' Literal.String 'Lemma for ' Literal.String '‹' Literal.String 'power_strict_decreasing' Literal.String '›' Literal.String '›' Literal.String '\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_Suc_less' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < a ⟹ a < 1 ⟹ a * a ^ n < a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ':' Operator ' ' Text.Whitespace 'mult_strict_left_mono' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_strict_decreasing' Name ' ' Text.Whitespace '[' Operator 'rule_format' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'n < N ⟹ 0 < a ⟹ a < 1 ⟶ a ^ N < a ^ n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'N' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'N' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_Suc_less' Name ' ' Text.Whitespace 'less_Suc_eq' Name ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'subgoal_tac' Name ' ' Text.Whitespace '"' Literal.String 'a * a^N < 1 * a^n' Literal.String '"' Literal.String ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'mult_strict_mono' Name ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace 'auto' Name '\n ' Text.Whitespace 'done' Keyword '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'Proof resembles that of ' Literal.String '‹' Literal.String 'power_strict_decreasing' Literal.String '›' Literal.String '.' Literal.String '›' Literal.String '\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_decreasing' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'n ≤ N ⟹ 0 ≤ a ⟹ a ≤ 1 ⟹ a ^ N ≤ a ^ n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'N' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'N' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'le_Suc_eq' Name ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'subgoal_tac' Name ' ' Text.Whitespace '"' Literal.String 'a * a^N ≤ 1 * a^n' Literal.String '"' Literal.String ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'mult_mono' Name ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace 'auto' Name '\n ' Text.Whitespace 'done' Keyword '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_decreasing_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '⟦0 < b; b < 1⟧ ⟹ b ^ m ≤ b ^ n ⟷ n ≤ m' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_strict_decreasing' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'm' Name ' ' Text.Whitespace 'n' Name ' ' Text.Whitespace 'b' Name ']' Operator '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'intro' Name ':' Operator ' ' Text.Whitespace 'power_decreasing' Name ' ' Text.Whitespace 'ccontr' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_strict_decreasing_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '⟦0 < b; b < 1⟧ ⟹ b ^ m < b ^ n ⟷ n < m' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_decreasing_iff' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'b' Name ' ' Text.Whitespace 'm' Name ' ' Text.Whitespace 'n' Name ']' Operator ' ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'le_less' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'dest' Name ':' Operator ' ' Text.Whitespace 'power_strict_decreasing' Name ' ' Text.Whitespace 'le_neq_implies_less' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_Suc_less_one' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < a ⟹ a < 1 ⟹ a ^ Suc n < 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_strict_decreasing' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace '0' Name ' ' Text.Whitespace '"' Literal.String 'Suc n' Literal.String '"' Literal.String ' ' Text.Whitespace 'a' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'Proof again resembles that of ' Literal.String '‹' Literal.String 'power_strict_decreasing' Literal.String '›' Literal.String '.' Literal.String '›' Literal.String '\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_increasing' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'n ≤ N ⟹ 1 ≤ a ⟹ a ^ n ≤ a ^ N' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'N' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'N' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'le_Suc_eq' Name ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'subgoal_tac' Name ' ' Text.Whitespace '"' Literal.String '1 * a^n ≤ a * a^N' Literal.String '"' Literal.String ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'mult_mono' Name ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'order_trans' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace 'zero_le_one' Name ']' Operator ')' Operator '\n ' Text.Whitespace 'done' Keyword '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'Lemma for ' Literal.String '‹' Literal.String 'power_strict_increasing' Literal.String '›' Literal.String '.' Literal.String '›' Literal.String '\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_less_power_Suc' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '1 < a ⟹ a ^ n < a * a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ':' Operator ' ' Text.Whitespace 'mult_strict_left_mono' Name ' ' Text.Whitespace 'less_trans' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace 'zero_less_one' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_strict_increasing' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'n < N ⟹ 1 < a ⟹ a ^ n < a ^ N' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'N' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'N' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_less_power_Suc' Name ' ' Text.Whitespace 'less_Suc_eq' Name ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'subgoal_tac' Name ' ' Text.Whitespace '"' Literal.String '1 * a^n < a * a^N' Literal.String '"' Literal.String ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'mult_strict_mono' Name ')' Operator '\n ' Text.Whitespace 'apply' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'less_trans' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace 'zero_less_one' Name ']' Operator ' ' Text.Whitespace 'less_imp_le' Name ')' Operator '\n ' Text.Whitespace 'done' Keyword '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_increasing_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '1 < b ⟹ b ^ x ≤ b ^ y ⟷ x ≤ y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'blast' Name ' ' Text.Whitespace 'intro' Name ':' Operator ' ' Text.Whitespace 'power_le_imp_le_exp' Name ' ' Text.Whitespace 'power_increasing' Name ' ' Text.Whitespace 'less_imp_le' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_strict_increasing_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '1 < b ⟹ b ^ x < b ^ y ⟷ x < y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'blast' Name ' ' Text.Whitespace 'intro' Name ':' Operator ' ' Text.Whitespace 'power_less_imp_less_exp' Name ' ' Text.Whitespace 'power_strict_increasing' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_le_imp_le_base' Name ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace 'le' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ Suc n ≤ b ^ Suc n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'and' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String '0 ≤ b' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'a ≤ b' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'ccontr' Name ')' Operator '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '"' Literal.String '¬ ?thesis' Literal.String '"' Literal.String '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'b < a' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'linorder_not_le' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'b ^ Suc n < a ^ Suc n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'assms' Name '(' Operator '2' Name ')' Operator ' ' Text.Whitespace 'power_strict_mono' Name ')' Operator '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace 'le' Name ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace 'False' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'linorder_not_less' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_less_imp_less_base' Name ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace 'less' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ n < b ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace 'nonneg' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ≤ b' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'a < b' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'contrapos_pp' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace 'less' Name ']' Operator ')' Operator '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '"' Literal.String '¬ ?thesis' Literal.String '"' Literal.String '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'b ≤ a' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'linorder_not_less' Name ')' Operator '\n ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'this' Name ' ' Text.Whitespace 'nonneg' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'b ^ n ≤ a ^ n' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'power_mono' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '"' Literal.String '¬ a ^ n < b ^ n' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'linorder_not_less' Name ')' Operator '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_inject_base' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ Suc n = b ^ Suc n ⟹ 0 ≤ a ⟹ 0 ≤ b ⟹ a = b' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'blast' Name ' ' Text.Whitespace 'intro' Name ':' Operator ' ' Text.Whitespace 'power_le_imp_le_base' Name ' ' Text.Whitespace 'order.antisym' Name ' ' Text.Whitespace 'eq_refl' Name ' ' Text.Whitespace 'sym' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_eq_imp_eq_base' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a ^ n = b ^ n ⟹ 0 ≤ a ⟹ 0 ≤ b ⟹ 0 < n ⟹ a = b' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'del' Name ':' Operator ' ' Text.Whitespace 'power_Suc' Name ',' Operator ' ' Text.Whitespace 'rule' Name ' ' Text.Whitespace 'power_inject_base' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_eq_iff_eq_base' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < n ⟹ 0 ≤ a ⟹ 0 ≤ b ⟹ a ^ n = b ^ n ⟷ a = b' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_eq_imp_eq_base' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'a' Name ' ' Text.Whitespace 'n' Name ' ' Text.Whitespace 'b' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'auto' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_le_imp_le' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x⇧2 ≤ y⇧2 ⟹ 0 ≤ y ⟹ x ≤ y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'numeral_2_eq_2' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'power_le_imp_le_base' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_less_imp_less' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x⇧2 < y⇧2 ⟹ 0 ≤ y ⟹ x < y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'power_less_imp_less_base' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_eq_imp_eq' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x⇧2 = y⇧2 ⟹ 0 ≤ x ⟹ 0 ≤ y ⟹ x = y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'numeral_2_eq_2' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'erule' Name ' ' Text.Whitespace '(' Operator '2' Name ')' Operator ' ' Text.Whitespace 'power_eq_imp_eq_base' Name ')' Operator ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_Suc_le_self' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ≤ a ⟹ a ≤ 1 ⟹ a ^ Suc n ≤ a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_decreasing' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace '1' Name ' ' Text.Whitespace '"' Literal.String 'Suc n' Literal.String '"' Literal.String ' ' Text.Whitespace 'a' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_eq_iff_nonneg' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String '0 ≤ x' Literal.String '"' Literal.String ' ' Text.Whitespace '"' Literal.String '0 ≤ y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String '(x ^ 2 = y ^ 2) ⟷ x = y' Literal.String '"' Literal.String '\n' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'assms' Name ' ' Text.Whitespace 'power2_eq_imp_eq' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'blast' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'of_nat_less_numeral_power_cancel_iff' Name '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace '"' Literal.String 'of_nat x < numeral i ^ n ⟷ x < numeral i ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'of_nat_less_iff' Name '[' Operator 'of' Name ' ' Text.Whitespace 'x' Name ' ' Text.Whitespace '"' Literal.String 'numeral i ^ n' Literal.String '"' Literal.String ',' Operator ' ' Text.Whitespace 'unfolded' Name ' ' Text.Whitespace 'of_nat_numeral' Name ' ' Text.Whitespace 'of_nat_power' Name ']' Operator ' ' Text.Whitespace '.' Operator.Word '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'of_nat_le_numeral_power_cancel_iff' Name '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace '"' Literal.String 'of_nat x ≤ numeral i ^ n ⟷ x ≤ numeral i ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'of_nat_le_iff' Name '[' Operator 'of' Name ' ' Text.Whitespace 'x' Name ' ' Text.Whitespace '"' Literal.String 'numeral i ^ n' Literal.String '"' Literal.String ',' Operator ' ' Text.Whitespace 'unfolded' Name ' ' Text.Whitespace 'of_nat_numeral' Name ' ' Text.Whitespace 'of_nat_power' Name ']' Operator ' ' Text.Whitespace '.' Operator.Word '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'numeral_power_less_of_nat_cancel_iff' Name '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace '"' Literal.String 'numeral i ^ n < of_nat x ⟷ numeral i ^ n < x' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'of_nat_less_iff' Name '[' Operator 'of' Name ' ' Text.Whitespace '"' Literal.String 'numeral i ^ n' Literal.String '"' Literal.String ' ' Text.Whitespace 'x' Name ',' Operator ' ' Text.Whitespace 'unfolded' Name ' ' Text.Whitespace 'of_nat_numeral' Name ' ' Text.Whitespace 'of_nat_power' Name ']' Operator ' ' Text.Whitespace '.' Operator.Word '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'numeral_power_le_of_nat_cancel_iff' Name '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace '"' Literal.String 'numeral i ^ n ≤ of_nat x ⟷ numeral i ^ n ≤ x' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'of_nat_le_iff' Name '[' Operator 'of' Name ' ' Text.Whitespace '"' Literal.String 'numeral i ^ n' Literal.String '"' Literal.String ' ' Text.Whitespace 'x' Name ',' Operator ' ' Text.Whitespace 'unfolded' Name ' ' Text.Whitespace 'of_nat_numeral' Name ' ' Text.Whitespace 'of_nat_power' Name ']' Operator ' ' Text.Whitespace '.' Operator.Word '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'of_nat_le_of_nat_power_cancel_iff' Name '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(of_nat b) ^ w ≤ of_nat x ⟷ b ^ w ≤ x' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'metis' Name ' ' Text.Whitespace 'of_nat_le_iff' Name ' ' Text.Whitespace 'of_nat_power' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'of_nat_power_le_of_nat_cancel_iff' Name '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'of_nat x ≤ (of_nat b) ^ w ⟷ x ≤ b ^ w' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'metis' Name ' ' Text.Whitespace 'of_nat_le_iff' Name ' ' Text.Whitespace 'of_nat_power' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'of_nat_less_of_nat_power_cancel_iff' Name '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(of_nat b) ^ w < of_nat x ⟷ b ^ w < x' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'metis' Name ' ' Text.Whitespace 'of_nat_less_iff' Name ' ' Text.Whitespace 'of_nat_power' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'of_nat_power_less_of_nat_cancel_iff' Name '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'of_nat x < (of_nat b) ^ w ⟷ x < b ^ w' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'metis' Name ' ' Text.Whitespace 'of_nat_less_iff' Name ' ' Text.Whitespace 'of_nat_power' Name ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'Some @' Literal.String '{' Literal.String 'typ nat' Literal.String '}' Literal.String '-specific lemmas:' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'mono_ge2_power_minus_self' Name ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'k ≥ 2' Literal.String '"' Literal.String ' ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'mono (λm. k ^ m - m)' Literal.String '"' Literal.String '\n' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'mono_iff_le_Suc' Name '\n' Text.Whitespace 'proof' Keyword '\n ' Text.Whitespace 'fix' Keyword ' ' Text.Whitespace 'n' Name '\n ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'k ^ n < k ^ Suc n' Literal.String '"' Literal.String ' ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_strict_increasing_iff' Name '[' Operator 'of' Name ' ' Text.Whitespace 'k' Name ' ' Text.Whitespace '"' Literal.String 'n' Literal.String '"' Literal.String ' ' Text.Whitespace '"' Literal.String 'Suc n' Literal.String '"' Literal.String ']' Operator ' ' Text.Whitespace 'assms' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'linarith' Name '\n ' Text.Whitespace 'thus' Keyword ' ' Text.Whitespace '"' Literal.String 'k ^ n - n ≤ k ^ Suc n - Suc n' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'linarith' Name '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'self_le_ge2_pow' Name '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'k ≥ 2' Literal.String '"' Literal.String ' ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'm ≤ k ^ m' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induction' Name ' ' Text.Whitespace 'm' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'm' Name ')' Operator '\n ' Text.Whitespace 'hence' Keyword ' ' Text.Whitespace '"' Literal.String 'Suc m ≤ Suc (k ^ m)' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '... ≤ k^m + k^m' Literal.String '"' Literal.String ' ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'one_le_power' Name '[' Operator 'of' Name ' ' Text.Whitespace 'k' Name ' ' Text.Whitespace 'm' Name ']' Operator ' ' Text.Whitespace 'assms' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'linarith' Name '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '... ≤ k * k^m' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'metis' Name ' ' Text.Whitespace 'mult_2' Name ' ' Text.Whitespace 'mult_le_mono1' Name '[' Operator 'OF' Name ' ' Text.Whitespace 'assms' Name ']' Operator ')' Operator '\n ' Text.Whitespace 'finally' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'diff_le_diff_pow' Name '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'k ≥ 2' Literal.String '"' Literal.String ' ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'm - n ≤ k ^ m - k ^ n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace '"' Literal.String 'n ≤ m' Literal.String '"' Literal.String ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace 'True' Name '\n ' Text.Whitespace 'thus' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'monoD' Name '[' Operator 'OF' Name ' ' Text.Whitespace 'mono_ge2_power_minus_self' Name '[' Operator 'OF' Name ' ' Text.Whitespace 'assms' Name ']' Operator ' ' Text.Whitespace 'True' Name ']' Operator ' ' Text.Whitespace 'self_le_ge2_pow' Name '[' Operator 'OF' Name ' ' Text.Whitespace 'assms' Name ',' Operator ' ' Text.Whitespace 'of' Name ' ' Text.Whitespace 'm' Name ']' Operator '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'le_diff_conv' Name ' ' Text.Whitespace 'le_diff_conv2' Name ')' Operator '\n' Text.Whitespace 'qed' Keyword ' ' Text.Whitespace 'auto' Name '\n\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'linordered_ring_strict' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'sum_squares_eq_zero_iff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x * x + y * y = 0 ⟷ x = 0 ∧ y = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'add_nonneg_eq_0_iff' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'sum_squares_le_zero_iff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x * x + y * y ≤ 0 ⟷ x = 0 ∧ y = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'le_less' Name ' ' Text.Whitespace 'not_sum_squares_lt_zero' Name ' ' Text.Whitespace 'sum_squares_eq_zero_iff' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'sum_squares_gt_zero_iff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < x * x + y * y ⟷ x ≠ 0 ∨ y ≠ 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'not_le' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ' ' Text.Whitespace 'sum_squares_le_zero_iff' Name ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'linordered_idom' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'zero_le_power2' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ≤ a⇧2' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power2_eq_square' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'zero_less_power2' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < a⇧2 ⟷ a ≠ 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'force' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power2_eq_square' Name ' ' Text.Whitespace 'zero_less_mult_iff' Name ' ' Text.Whitespace 'linorder_neq_iff' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_less_0' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '¬ a⇧2 < 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'force' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power2_eq_square' Name ' ' Text.Whitespace 'mult_less_0_iff' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_abs' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '¦a ^ n¦ = ¦a¦ ^ n' Literal.String '"' Literal.String ' ' Text.Whitespace '―' Name ' ' Text.Whitespace '‹' Literal.String 'FIXME simp?' Literal.String '›' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'abs_mult' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_sgn' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'sgn (a ^ n) = sgn a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace '(' Operator 'simp_all' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'sgn_mult' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'abs_power_minus' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '¦(- a) ^ n¦ = ¦a ^ n¦' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_abs' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'zero_less_power_abs_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < ¦a¦ ^ n ⟷ a ≠ 0 ∨ n = 0' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace 'Suc' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ':' Operator ' ' Text.Whitespace 'zero_less_mult_iff' Name ')' Operator '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'zero_le_power_abs' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ≤ ¦a¦ ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'zero_le_power' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace 'abs_ge_zero' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_less_eq_zero_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'a⇧2 ≤ 0 ⟷ a = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'le_less' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'abs_power2' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '¦a⇧2¦ = a⇧2' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power2_eq_square' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_abs' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '¦a¦⇧2 = a⇧2' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power2_eq_square' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'odd_power_less_zero' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'a < 0 ⟹ a ^ Suc (2 * n) < 0' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'ac_simps' Name ' ' Text.Whitespace 'power_add' Name ' ' Text.Whitespace 'power2_eq_square' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'del' Name ':' Operator ' ' Text.Whitespace 'power_Suc' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'Suc' Name ' ' Text.Whitespace 'mult_less_0_iff' Name ' ' Text.Whitespace 'mult_neg_neg' Name ')' Operator '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'odd_0_le_power_imp_0_le' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ≤ a ^ Suc (2 * n) ⟹ 0 ≤ a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'odd_power_less_zero' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'a' Name ' ' Text.Whitespace 'n' Name ']' Operator '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'force' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'linorder_not_less' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace "zero_le_even_power'" Name '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ≤ a ^ (2 * n)' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'n' Name ')' Operator '\n ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'a ^ (2 * Suc n) = (a*a) * a ^ (2*n)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'ac_simps' Name ' ' Text.Whitespace 'power_add' Name ' ' Text.Whitespace 'power2_eq_square' Name ')' Operator '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'Suc' Name ' ' Text.Whitespace 'zero_le_mult_iff' Name ')' Operator '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'sum_power2_ge_zero' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 ≤ x⇧2 + y⇧2' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'intro' Name ' ' Text.Whitespace 'add_nonneg_nonneg' Name ' ' Text.Whitespace 'zero_le_power2' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'not_sum_power2_lt_zero' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '¬ x⇧2 + y⇧2 < 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'not_less' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'sum_power2_ge_zero' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'sum_power2_eq_zero_iff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x⇧2 + y⇧2 = 0 ⟷ x = 0 ∧ y = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'power2_eq_square' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'add_nonneg_eq_0_iff' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'sum_power2_le_zero_iff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x⇧2 + y⇧2 ≤ 0 ⟷ x = 0 ∧ y = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'le_less' Name ' ' Text.Whitespace 'sum_power2_eq_zero_iff' Name ' ' Text.Whitespace 'not_sum_power2_lt_zero' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'sum_power2_gt_zero_iff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < x⇧2 + y⇧2 ⟷ x ≠ 0 ∨ y ≠ 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'not_le' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'sum_power2_le_zero_iff' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'abs_le_square_iff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '¦x¦ ≤ ¦y¦ ⟷ x⇧2 ≤ y⇧2' Literal.String '"' Literal.String '\n ' Text.Whitespace '(' Operator 'is' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String '?lhs ⟷ ?rhs' Literal.String '"' Literal.String ')' Operator '\n' Text.Whitespace 'proof' Keyword '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '?' Operator 'lhs' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '¦x¦⇧2 ≤ ¦y¦⇧2' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'power_mono' Name ')' Operator ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'rhs' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '?' Operator 'rhs' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'lhs' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'intro' Name '!' Operator ':' Operator ' ' Text.Whitespace 'power2_le_imp_le' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace '_' Operator ' ' Text.Whitespace 'abs_ge_zero' Name ']' Operator ')' Operator '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_le_iff_abs_le' Name ':' Operator '\n ' Text.Whitespace '"' Literal.String 'y ≥ 0 ⟹ x⇧2 ≤ y⇧2 ⟷ ¦x¦ ≤ y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'metis' Name ' ' Text.Whitespace 'abs_le_square_iff' Name ' ' Text.Whitespace 'abs_of_nonneg' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'abs_square_le_1' Name ':' Operator '"' Literal.String 'x⇧2 ≤ 1 ⟷ ¦x¦ ≤ 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'abs_le_square_iff' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'x' Name ' ' Text.Whitespace '1' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'abs_square_eq_1' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x⇧2 = 1 ⟷ ¦x¦ = 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'abs_if' Name ' ' Text.Whitespace 'power2_eq_1_iff' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'abs_square_less_1' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'x⇧2 < 1 ⟷ ¦x¦ < 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'abs_square_eq_1' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'x' Name ']' Operator ' ' Text.Whitespace 'abs_square_le_1' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'x' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'le_less' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'square_le_1' Name ':' Operator '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String '- 1 ≤ x' Literal.String '"' Literal.String ' ' Text.Whitespace '"' Literal.String 'x ≤ 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'x⇧2 ≤ 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'assms' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'metis' Name ' ' Text.Whitespace 'add.inverse_inverse' Name ' ' Text.Whitespace 'linear' Name ' ' Text.Whitespace 'mult_le_one' Name ' ' Text.Whitespace 'neg_equal_0_iff_equal' Name ' ' Text.Whitespace 'neg_le_iff_le' Name ' ' Text.Whitespace 'power2_eq_square' Name ' ' Text.Whitespace 'power_minus_Bit0' Name ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n\n' Text.Whitespace 'subsection' Generic.Subheading ' ' Text.Whitespace '‹' Literal.String 'Miscellaneous rules' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace '(' Operator 'in' Keyword.Pseudo ' ' Text.Whitespace 'linordered_semidom' Name ')' Operator ' ' Text.Whitespace 'self_le_power' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '1 ≤ a ⟹ 0 < n ⟹ a ≤ a ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'power_increasing' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace '1' Name ' ' Text.Whitespace 'n' Name ' ' Text.Whitespace 'a' Name ']' Operator ' ' Text.Whitespace 'power_one_right' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'a' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'auto' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace '(' Operator 'in' Keyword.Pseudo ' ' Text.Whitespace 'power' Name ')' Operator ' ' Text.Whitespace 'power_eq_if' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))' Literal.String '"' Literal.String '\n ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'One_nat_def' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace 'm' Name ')' Operator ' ' Text.Whitespace 'simp_all' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace '(' Operator 'in' Keyword.Pseudo ' ' Text.Whitespace 'comm_semiring_1' Name ')' Operator ' ' Text.Whitespace 'power2_sum' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '(x + y)⇧2 = x⇧2 + y⇧2 + 2 * x * y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'algebra_simps' Name ' ' Text.Whitespace 'power2_eq_square' Name ' ' Text.Whitespace 'mult_2_right' Name ')' Operator '\n\n' Text.Whitespace 'context' Keyword ' ' Text.Whitespace 'comm_ring_1' Name '\n' Text.Whitespace 'begin' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_diff' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '(x - y)⇧2 = x⇧2 + y⇧2 - 2 * x * y' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'algebra_simps' Name ' ' Text.Whitespace 'power2_eq_square' Name ' ' Text.Whitespace 'mult_2_right' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_commute' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '(x - y)⇧2 = (y - x)⇧2' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'algebra_simps' Name ' ' Text.Whitespace 'power2_eq_square' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'minus_power_mult_self' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '(- a) ^ n * (- a) ^ n = a ^ (2 * n)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_mult_distrib' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power2_eq_square' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ' ' Text.Whitespace 'power_mult' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'minus_one_mult_self' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(- 1) ^ n * (- 1) ^ n = 1' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'minus_power_mult_self' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace '1' Name ' ' Text.Whitespace 'n' Name ']' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'left_minus_one_mult_self' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String '(- 1) ^ n * ((- 1) ^ n * a) = a' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'mult.assoc' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'end' Keyword '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String 'Simprules for comparisons where common factors can be cancelled.' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'lemmas' Keyword ' ' Text.Whitespace 'zero_compare_simps' Name ' ' Text.Whitespace '=' Operator '\n ' Text.Whitespace 'add_strict_increasing' Name ' ' Text.Whitespace 'add_strict_increasing2' Name ' ' Text.Whitespace 'add_increasing' Name '\n ' Text.Whitespace 'zero_le_mult_iff' Name ' ' Text.Whitespace 'zero_le_divide_iff' Name '\n ' Text.Whitespace 'zero_less_mult_iff' Name ' ' Text.Whitespace 'zero_less_divide_iff' Name '\n ' Text.Whitespace 'mult_le_0_iff' Name ' ' Text.Whitespace 'divide_le_0_iff' Name '\n ' Text.Whitespace 'mult_less_0_iff' Name ' ' Text.Whitespace 'divide_less_0_iff' Name '\n ' Text.Whitespace 'zero_le_power2' Name ' ' Text.Whitespace 'power2_less_0' Name '\n\n\n' Text.Whitespace 'subsection' Generic.Subheading ' ' Text.Whitespace '‹' Literal.String 'Exponentiation for the Natural Numbers' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'nat_one_le_power' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'Suc 0 ≤ i ⟹ Suc 0 ≤ i ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'one_le_power' Name ' ' Text.Whitespace '[' Operator 'of' Name ' ' Text.Whitespace 'i' Name ' ' Text.Whitespace 'n' Name ',' Operator ' ' Text.Whitespace 'unfolded' Name ' ' Text.Whitespace 'One_nat_def' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'nat_zero_less_power_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'x ^ n > 0 ⟷ x > 0 ∨ n = 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'for' Keyword.Pseudo ' ' Text.Whitespace 'x' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace 'nat' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'n' Name ')' Operator ' ' Text.Whitespace 'auto' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'nat_power_eq_Suc_0_iff' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'x ^ m = Suc 0 ⟷ m = 0 ∨ x = Suc 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'm' Name ')' Operator ' ' Text.Whitespace 'auto' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_Suc_0' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'Suc 0 ^ n = Suc 0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'text' Keyword ' ' Text.Whitespace '‹' Literal.String '\n Valid for the naturals, but what if ' Literal.String '‹' Literal.String '0 < i < 1' Literal.String '›' Literal.String '? Premises cannot be\n weakened: consider the case where ' Literal.String '‹' Literal.String 'i = 0' Literal.String '›' Literal.String ', ' Literal.String '‹' Literal.String 'm = 1' Literal.String '›' Literal.String ' and ' Literal.String '‹' Literal.String 'n = 0' Literal.String '›' Literal.String '.\n' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'nat_power_less_imp_less' Name ':' Operator '\n ' Text.Whitespace 'fixes' Keyword.Pseudo ' ' Text.Whitespace 'i' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace 'nat' Name '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace 'nonneg' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '0 < i' Literal.String '"' Literal.String '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace 'less' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'i ^ m < i ^ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'm < n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace '"' Literal.String 'i = 1' Literal.String '"' Literal.String ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace 'True' Name '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace 'less' Name ' ' Text.Whitespace 'power_one' Name ' ' Text.Whitespace '[' Operator 'where' Keyword.Pseudo ' ' Text.Whitespace "'a" Name.Type ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'nat' Name ']' Operator ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace 'False' Name '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace 'nonneg' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '1 < i' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'auto' Name '\n ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'power_strict_increasing_iff' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace 'this' Name ']' Operator ' ' Text.Whitespace 'less' Name ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name ' ' Text.Whitespace '..' Operator.Word '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_gt_expt' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'n > Suc 0 ⟹ n^k > k' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'induction' Name ' ' Text.Whitespace 'k' Name ')' Operator ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'simp' Name ':' Operator ' ' Text.Whitespace 'less_trans_Suc' Name ' ' Text.Whitespace 'n_less_m_mult_n' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'less_exp' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator '\n ' Text.Whitespace '‹' Literal.String 'n < 2 ^ n' Literal.String '›' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_gt_expt' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power_dvd_imp_le' Name ':' Operator '\n ' Text.Whitespace 'fixes' Keyword.Pseudo ' ' Text.Whitespace 'i' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace 'nat' Name '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'i ^ m dvd i ^ n' Literal.String '"' Literal.String ' ' Text.Whitespace '"' Literal.String '1 < i' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'm ≤ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'assms' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'intro' Name ':' Operator ' ' Text.Whitespace 'power_le_imp_le_exp' Name ' ' Text.Whitespace '[' Operator 'OF' Name ' ' Text.Whitespace '‹' Literal.String '1 < i' Literal.String '›' Literal.String ' ' Text.Whitespace 'dvd_imp_le' Name ']' Operator ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'dvd_power_iff_le' Name ':' Operator '\n ' Text.Whitespace 'fixes' Keyword.Pseudo ' ' Text.Whitespace 'k' Name '::' Operator 'nat' Name '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String '2 ≤ k ⟹ ((k ^ m) dvd (k ^ n) ⟷ m ≤ n)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'le_imp_power_dvd' Name ' ' Text.Whitespace 'power_dvd_imp_le' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'force' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_nat_le_eq_le' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'm⇧2 ≤ n⇧2 ⟷ m ≤ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'for' Keyword.Pseudo ' ' Text.Whitespace 'm' Name ' ' Text.Whitespace 'n' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace 'nat' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'auto' Name ' ' Text.Whitespace 'intro' Name ':' Operator ' ' Text.Whitespace 'power2_le_imp_le' Name ' ' Text.Whitespace 'power_mono' Name ')' Operator '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'power2_nat_le_imp_le' Name ':' Operator '\n ' Text.Whitespace 'fixes' Keyword.Pseudo ' ' Text.Whitespace 'm' Name ' ' Text.Whitespace 'n' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace 'nat' Name '\n ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'm⇧2 ≤ n' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'm ≤ n' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace 'm' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'k' Name ')' Operator '\n ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name '\n ' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'ccontr' Name ')' Operator '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '"' Literal.String '¬ ?thesis' Literal.String '"' Literal.String '\n ' Text.Whitespace 'then' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'n < m' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace 'assms' Name ' ' Text.Whitespace 'Suc' Name ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace 'False' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power2_eq_square' Name ')' Operator '\n ' Text.Whitespace 'qed' Keyword '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'ex_power_ivl1' Name ':' Operator ' ' Text.Whitespace 'fixes' Keyword.Pseudo ' ' Text.Whitespace 'b' Name ' ' Text.Whitespace 'k' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace 'nat' Name ' ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'b ≥ 2' Literal.String '"' Literal.String '\n' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'k ≥ 1 ⟹ ∃n. b^n ≤ k ∧ k < b^(n+1)' Literal.String '"' Literal.String ' ' Text.Whitespace '(' Operator 'is' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String '_ ⟹ ∃n. ?P k n' Literal.String '"' Literal.String ')' Operator '\n' Text.Whitespace 'proof' Keyword '(' Operator 'induction' Name ' ' Text.Whitespace 'k' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '0' Name ' ' Text.Whitespace 'thus' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'Suc' Name ' ' Text.Whitespace 'k' Name ')' Operator '\n ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace 'cases' Name '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '"' Literal.String 'k=0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'hence' Keyword ' ' Text.Whitespace '"' Literal.String '?P (Suc k) 0' Literal.String '"' Literal.String ' ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'assms' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'thus' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace '..' Operator.Word '\n ' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'assume' Keyword ' ' Text.Whitespace '"' Literal.String 'k≠0' Literal.String '"' Literal.String '\n ' Text.Whitespace 'with' Keyword ' ' Text.Whitespace 'Suc' Name ' ' Text.Whitespace 'obtain' Keyword ' ' Text.Whitespace 'n' Name ' ' Text.Whitespace 'where' Keyword.Pseudo ' ' Text.Whitespace 'IH' Name ':' Operator ' ' Text.Whitespace '"' Literal.String '?P k n' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'auto' Name '\n ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword '\n ' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'cases' Name ' ' Text.Whitespace '"' Literal.String 'k = b^(n+1) - 1' Literal.String '"' Literal.String ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace 'True' Name '\n ' Text.Whitespace 'hence' Keyword ' ' Text.Whitespace '"' Literal.String '?P (Suc k) (n+1)' Literal.String '"' Literal.String ' ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'assms' Name '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'power_less_power_Suc' Name ')' Operator '\n ' Text.Whitespace 'thus' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name ' ' Text.Whitespace '..' Operator.Word '\n ' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace 'False' Name '\n ' Text.Whitespace 'hence' Keyword ' ' Text.Whitespace '"' Literal.String '?P (Suc k) n' Literal.String '"' Literal.String ' ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'IH' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'auto' Name '\n ' Text.Whitespace 'thus' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name ' ' Text.Whitespace '..' Operator.Word '\n ' Text.Whitespace 'qed' Keyword '\n ' Text.Whitespace 'qed' Keyword '\n' Text.Whitespace 'qed' Keyword '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'ex_power_ivl2' Name ':' Operator ' ' Text.Whitespace 'fixes' Keyword.Pseudo ' ' Text.Whitespace 'b' Name ' ' Text.Whitespace 'k' Name ' ' Text.Whitespace '::' Operator ' ' Text.Whitespace 'nat' Name ' ' Text.Whitespace 'assumes' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'b ≥ 2' Literal.String '"' Literal.String ' ' Text.Whitespace '"' Literal.String 'k ≥ 2' Literal.String '"' Literal.String '\n ' Text.Whitespace 'shows' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String '∃n. b^n < k ∧ k ≤ b^(n+1)' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '-' Operator '\n ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '1 ≤ k - 1' Literal.String '"' Literal.String ' ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'assms' Name '(' Operator '2' Name ')' Operator ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'arith' Name '\n ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'ex_power_ivl1' Name '[' Operator 'OF' Name ' ' Text.Whitespace 'assms' Name '(' Operator '1' Name ')' Operator ' ' Text.Whitespace 'this' Name ']' Operator '\n ' Text.Whitespace 'obtain' Keyword ' ' Text.Whitespace 'n' Name ' ' Text.Whitespace 'where' Keyword.Pseudo ' ' Text.Whitespace '"' Literal.String 'b ^ n ≤ k - 1 ∧ k - 1 < b ^ (n + 1)' Literal.String '"' Literal.String ' ' Text.Whitespace '..' Operator.Word '\n ' Text.Whitespace 'hence' Keyword ' ' Text.Whitespace '"' Literal.String 'b^n < k ∧ k ≤ b^(n+1)' Literal.String '"' Literal.String ' ' Text.Whitespace 'using' Keyword ' ' Text.Whitespace 'assms' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'auto' Name '\n ' Text.Whitespace 'thus' Keyword ' ' Text.Whitespace '?' Operator 'thesis' Name ' ' Text.Whitespace '..' Operator.Word '\n' Text.Whitespace 'qed' Keyword '\n\n\n' Text.Whitespace 'subsubsection' Generic.Subheading ' ' Text.Whitespace '‹' Literal.String 'Cardinality of the Powerset' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'card_UNIV_bool' Name ' ' Text.Whitespace '[' Operator 'simp' Name ']' Operator ':' Operator ' ' Text.Whitespace '"' Literal.String 'card (UNIV :: bool set) = 2' Literal.String '"' Literal.String '\n ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'UNIV_bool' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n\n' Text.Whitespace 'lemma' Keyword.Namespace ' ' Text.Whitespace 'card_Pow' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'finite A ⟹ card (Pow A) = 2 ^ card A' Literal.String '"' Literal.String '\n' Text.Whitespace 'proof' Keyword ' ' Text.Whitespace '(' Operator 'induct' Name ' ' Text.Whitespace 'rule' Name ':' Operator ' ' Text.Whitespace 'finite_induct' Name ')' Operator '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace 'empty' Name '\n ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n' Text.Whitespace 'next' Keyword '\n ' Text.Whitespace 'case' Keyword ' ' Text.Whitespace '(' Operator 'insert' Name ' ' Text.Whitespace 'x' Name ' ' Text.Whitespace 'A' Name ')' Operator '\n ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace '‹' Literal.String 'x ∉ A' Literal.String '›' Literal.String ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace 'disjoint' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'Pow A ∩ insert x ` Pow A = {}' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'blast' Name '\n ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace '‹' Literal.String 'x ∉ A' Literal.String '›' Literal.String ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace 'inj_on' Name ':' Operator ' ' Text.Whitespace '"' Literal.String 'inj_on (insert x) (Pow A)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'unfolding' Keyword ' ' Text.Whitespace 'inj_on_def' Name ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'auto' Name '\n\n ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'card (Pow (insert x A)) = card (Pow A ∪ insert x ` Pow A)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'only' Name ':' Operator ' ' Text.Whitespace 'Pow_insert' Name ')' Operator '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '… = card (Pow A) + card (insert x ` Pow A)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'card_Un_disjoint' Name ')' Operator ' ' Text.Whitespace '(' Operator 'use' Name ' ' Text.Whitespace '‹' Literal.String 'finite A' Literal.String '›' Literal.String ' ' Text.Whitespace 'disjoint' Name ' ' Text.Whitespace 'in' Keyword.Pseudo ' ' Text.Whitespace 'simp_all' Name ')' Operator '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'inj_on' Name ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'card (insert x ` Pow A) = card (Pow A)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'card_image' Name ')' Operator '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '… + … = 2 * …' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'simp' Name ' ' Text.Whitespace 'add' Name ':' Operator ' ' Text.Whitespace 'mult_2' Name ')' Operator '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'insert' Name '(' Operator '3' Name ')' Operator ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String '… = 2 ^ Suc (card A)' Literal.String '"' Literal.String ' ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace 'simp' Name '\n ' Text.Whitespace 'also' Keyword ' ' Text.Whitespace 'from' Keyword ' ' Text.Whitespace 'insert' Name '(' Operator '1' Name ',' Operator '2' Name ')' Operator ' ' Text.Whitespace 'have' Keyword ' ' Text.Whitespace '"' Literal.String 'Suc (card A) = card (insert x A)' Literal.String '"' Literal.String '\n ' Text.Whitespace 'by' Keyword ' ' Text.Whitespace '(' Operator 'rule' Name ' ' Text.Whitespace 'card_insert_disjoint' Name ' ' Text.Whitespace '[' Operator 'symmetric' Name ']' Operator ')' Operator '\n ' Text.Whitespace 'finally' Keyword ' ' Text.Whitespace 'show' Keyword ' ' Text.Whitespace '?' Operator 'case' Keyword ' ' Text.Whitespace '.' Operator.Word '\n' Text.Whitespace 'qed' Keyword '\n\n\n' Text.Whitespace 'subsection' Generic.Subheading ' ' Text.Whitespace '‹' Literal.String 'Code generator tweak' Literal.String '›' Literal.String '\n\n' Text.Whitespace 'code_identifier' Keyword '\n ' Text.Whitespace 'code_module' Keyword.Pseudo ' ' Text.Whitespace 'Power' Name ' ' Text.Whitespace '⇀' Name ' ' Text.Whitespace '(' Operator 'SML' Name ')' Operator ' ' Text.Whitespace 'Arith' Name ' ' Text.Whitespace 'and' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'OCaml' Name ')' Operator ' ' Text.Whitespace 'Arith' Name ' ' Text.Whitespace 'and' Keyword.Pseudo ' ' Text.Whitespace '(' Operator 'Haskell' Name ')' Operator ' ' Text.Whitespace 'Arith' Name '\n\n' Text.Whitespace 'end' Keyword '\n' Text.Whitespace