Theory IntFact

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory IntFact = IntPrimes:

```(*  Title:      HOL/NumberTheory/IntFact.thy
ID:         \$Id: IntFact.thy,v 1.10 2003/12/03 09:49:35 paulson Exp \$
Author:     Thomas M. Rasmussen
*)

header {* Factorial on integers *}

theory IntFact = IntPrimes:

text {*
Factorial on integers and recursively defined set including all
Integers from @{text 2} up to @{text a}.  Plus definition of product
of finite set.

\bigskip
*}

consts
zfact :: "int => int"
ssetprod :: "int set => int"
d22set :: "int => int set"

recdef zfact  "measure ((λn. nat n) :: int => nat)"
"zfact n = (if n ≤ 0 then 1 else n * zfact (n - 1))"

defs
ssetprod_def: "ssetprod A == (if finite A then fold (op *) 1 A else 1)"

recdef d22set  "measure ((λa. nat a) :: int => nat)"
"d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"

text {* \medskip @{term ssetprod} --- product of finite set *}

lemma ssetprod_empty [simp]: "ssetprod {} = 1"
done

lemma ssetprod_insert [simp]:
"finite A ==> a ∉ A ==> ssetprod (insert a A) = a * ssetprod A"
by (simp add: ssetprod_def mult_left_commute LC.fold_insert [OF LC.intro])

text {*
\medskip @{term d22set} --- recursively defined set including all
integers from @{text 2} up to @{text a}
*}

declare d22set.simps [simp del]

lemma d22set_induct:
"(!!a. P {} a) ==>
(!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1)
==> P (d22set a) a)
==> P (d22set u) u"
proof -
case rule_context
show ?thesis
apply (rule d22set.induct)
apply safe
apply (case_tac [2] "1 < a")
apply (rule_tac [2] rule_context)
apply (simp_all (no_asm_simp))
apply (simp_all (no_asm_simp) add: d22set.simps rule_context)
done
qed

lemma d22set_g_1 [rule_format]: "b ∈ d22set a --> 1 < b"
apply (induct a rule: d22set_induct)
prefer 2
apply (subst d22set.simps)
apply auto
done

lemma d22set_le [rule_format]: "b ∈ d22set a --> b ≤ a"
apply (induct a rule: d22set_induct)
prefer 2
apply (subst d22set.simps)
apply auto
done

lemma d22set_le_swap: "a < b ==> b ∉ d22set a"
apply (auto dest: d22set_le)
done

lemma d22set_mem [rule_format]: "1 < b --> b ≤ a --> b ∈ d22set a"
apply (induct a rule: d22set.induct)
apply auto
done

lemma d22set_fin: "finite (d22set a)"
apply (induct a rule: d22set_induct)
prefer 2
apply (subst d22set.simps)
apply auto
done

declare zfact.simps [simp del]

lemma d22set_prod_zfact: "ssetprod (d22set a) = zfact a"
apply (induct a rule: d22set.induct)
apply safe
apply (subst d22set.simps)
apply (subst zfact.simps)
apply (case_tac "1 < a")
prefer 2
done

end
```

lemma ssetprod_empty:

`  ssetprod {} = 1`

lemma ssetprod_insert:

`  [| finite A; a ∉ A |] ==> ssetprod (insert a A) = a * ssetprod A`

lemma d22set_induct:

```  [| !!a. P {} a;
!!a. [| 1 < a; P (d22set (a - 1)) (a - 1) |] ==> P (d22set a) a |]
==> P (d22set u) u```

lemma d22set_g_1:

`  b ∈ d22set a ==> 1 < b`

lemma d22set_le:

`  b ∈ d22set a ==> b ≤ a`

lemma d22set_le_swap:

`  a < b ==> b ∉ d22set a`

lemma d22set_mem:

`  [| 1 < b; b ≤ a |] ==> b ∈ d22set a`

lemma d22set_fin:

`  finite (d22set a)`

lemma d22set_prod_zfact:

`  ssetprod (d22set a) = zfact a`