isabelle - Proof of existence of prime factorization (Educational) -

i trying write proof of existence of prime factorization of numbers. meant educational, every function defined, try not use isabelle built in functions. here code:

(* addition*) primrec suma::"nat ⇒ nat ⇒ nat" "suma 0 n = 0" | "suma (suc x) n = suc (suma x n)"  primrec pred::"nat ⇒ nat" "pred 0 = 0" | "pred (suc x) = x"  (* substraction *) primrec resta::"nat ⇒ nat ⇒ nat" "resta m 0 = m" | "resta m (suc x) = pred (resta m x)"  primrec mult::"nat ⇒ nat ⇒ nat" "mult 0 m = 0" | "mult (suc x) m = suma m (mult x m)"  lemma less_pred [simp]: "(x < y) ⟶ (pred x < y)" proof (induct x) case 0 show ?case simp next case (suc x) show ?case simp qed  lemma less_n_pred [simp]: "∀n::nat. (n ≠ 0) ⟶ (pred n < n)" proof fix n::nat show "n ≠ 0 ⟶ pred n < n" (induct n) simp_all qed  lemma less_resta [simp]: "(m > 0 ∧ n > 0) ⟶ (resta m n < m)" proof (induct n) case 0 show ?case simp_all next case (suc x) show ?case force qed  fun divi::"nat ⇒ nat ⇒ nat" "divi m n = (if n = 0                 undefined             else               if m = 0                  0                else suc (divi (resta m n) n))"  fun modulo::"nat ⇒ nat ⇒ nat" "modulo m n = (if n = 0                 undefined             else               if m < n                  m                else modulo (resta m n) n)"  definition divide::"nat ⇒ nat ⇒ bool" "divide m n = (modulo n m = 0)"  primrec numto :: "nat ⇒ nat list" "numto 0 = []" | "numto (suc x) = (suc x)#(numto x)"   primrec filter:: "'a list ⇒ ('a ⇒ bool) ⇒ 'a list" "filter [] p = []" | "filter (x#xs) p = (if p x x#(filter xs p) else filter xs p)"  definition divisores::"nat ⇒ nat list" "divisores n = (filter (numto n) (λm. divide m n))"  definition is_prime::"nat ⇒ bool" "is_prime n = (length (divisores n) = 2)"  primrec all_prime::"nat list ⇒ bool" "all_prime [] = true" | "all_prime (x#xs) = (is_prime x ∧ all_prime xs)"  primrec prod_list::"nat list ⇒ nat" "prod_list [] = 1" | "prod_list (x#xs) = mult x (prod_list xs)"  lemma mult_num: "∀n::nat. n>1 ∧ ¬ is_prime n ⟶ (∃x y::nat. x < n ∧ y < n ∧ mult x y = n)" proof fix n::nat (* lemma might useful? *)  theorem exists_prime_factor: "∀n::nat. (n > 1 ⟶ (∃xs::nat list. prod_list xs = n ∧ all_prime xs))" proof   fix n::nat   show "(n > 1 ⟶ (∃xs::nat list. prod_list xs = n ∧ all_prime xs))"   proof (induct n rule: less_induct)  (* how can prove this? *) 

how can prove theorem exists_prime_factor: ∀n::nat. (n > 1 ⟶ (∃xs::nat list. prod_list xs = n ∧ all_prime xs))?

thank in advance help.

one short answer started basic mistake in definition of suma. should (i guess):

primrec suma::"nat ⇒ nat ⇒ nat"   "suma 0 n = n" |   "suma (suc x) n = suc (suma x n)" 

my long answer has how use value, nitpick, , sledgehammer see if you're on right track.

if can't prove something, quick thing try sledgehammer. if sledgehammer returns nothing @ all, it's idea try nitpick.

if nitpick finds counterexample, that's indicator conjecture false, though no guarantee. underspecified definitions due undefined, the, , some can cause that, or not defining cases primrec.

use value quick checks of functions

using value end result of me trying figure things out, without sorting out logic.

value "mult 2 2" (* suc (suc 0) *) 

from there, seeing obvious.

use value see if functions working right, though requires value inputs can simplified code generator.

use nitpick, it's free

for things this, see if sledgehammer can work magic.

first, it's best rid of outer quantifiers, this:

theorem exists_prime_factor:    "n > 1 --> (∃xs::nat list. prod_list xs = n ∧ all_prime xs)"   apply(induct n, auto)   sledgehammer   oops 

when sledgehammer returns nothing @ all, conjecture false, or need out.

nitpick gave me counterexample of n = 2, it's potentially spurious, , you're using undefined in definitions, can mess nitpick.

eventually, ran nitpick on lemma mult_num, , gave me counterexample of n = 4.

one thing try prove negation of theorem, proves theorem false. trying prove this:

theorem   "(x >= 4) | (y >= 4) | ~(mult x y = 4)" 

finally, said, "hmmm, lets try simple":

value "mult 2 2" 

that returning 2, helped me see obvious.

undefined may not think is

i looking things mess nitpick up, 1 of them being use of undefined, such function here:

fun divi::"nat ⇒ nat ⇒ nat"   "divi m n = (if n = 0 undefined                else if m = 0 0                 else suc (divi (resta m n) n))" 

this example of value not going out. can't simplify this:

value "divi 3 0" (* divi (suc (suc (suc 0))) 0  *) 

if follow past discussion of isabelle/hol terminology, experts prefer undefined called underspecified.

here, theorem cannot proved:

theorem "divi n 0 ~= (1::nat)"   apply(induct n, auto) oops 

nitpick finds counterexample:

theorem "divi n 0 ~= (1::nat)"   nitpick (*   nitpick found counterexample:    free variable:     n = 1 *) oops 

but then, it's same counterexample this:

theorem "divi n 0 = (1::nat)"   nitpick oops 

why this? because undefined::nat nat. if never define it, such axiom, can't nat equal to, though has equal unique nat.

how 44?

theorem "(divi n 0 = 44) <-> undefined = (44::nat)"   by(simp) 

it seems there's infinitely small chance n = 1023456.

theorem "(divi n 0 = 1023456) <-> undefined = (1023456::nat)"   by(simp) 

the consequence? there infinitely many jokes made this, of infinitesimal size humor.