src/HOL/NumberTheory/IntFact.ML
 author nipkow Fri, 24 Nov 2000 16:49:27 +0100 changeset 10519 ade64af4c57c parent 10198 2b255b772585 permissions -rw-r--r--
hide many names from Datatype_Universe.
```
(*  Title:	IntPowerFact.ML
ID:         \$Id\$
Author:	Thomas M. Rasmussen

Factorial on integers.
Product of finite set.
Recursively defined set including all Integers from 2 up to a.
*)

(*----  setprod  ----*)

Goalw [setprod_def] "setprod {} = #1";
by (Simp_tac 1);
qed "setprod_empty";

Goalw [setprod_def]
"[| finite A; a ~: A |] ==> setprod (insert a A) = a * setprod A";
export fold_insert]) 1);
qed "setprod_insert";

(*---- IntFact ----*)

val [d22set_eq] = d22set.simps;
Delsimps d22set.simps;

val [prem1,prem2] =
Goal "[| !!a. P {} a; \
\        !!a. [| #1<(a::int); P (d22set (a-#1)) (a-#1) |] \
\             ==> P (d22set a) a |] \
\    ==> P (d22set u) u";
by (rtac d22set.induct 1);
by Safe_tac;
by (case_tac "#1<a" 2);
by (rtac prem2 2);
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [d22set_eq,prem1])));
qed "d22set_induct";

Goal "b:(d22set a) --> #1<b";
by (induct_thm_tac d22set_induct "a" 1);
by (stac d22set_eq 2);
by Auto_tac;
qed_spec_mp "d22set_g_1";

Goal "b:(d22set a) --> b<=a";
by (induct_thm_tac d22set_induct "a" 1);
by (stac d22set_eq 2);
by Auto_tac;
qed_spec_mp "d22set_le";

Goal "a<b ==> b~:(d22set a)";
by (auto_tac (claset() addDs [d22set_le], simpset()));
qed "d22set_le_swap";

Goal "#1<b --> b<=a --> b:(d22set a)";
by (induct_thm_tac d22set.induct "a" 1);
by Auto_tac;
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq])));
qed_spec_mp "d22set_mem";

Goal "finite (d22set a)";
by (induct_thm_tac d22set_induct "a" 1);
by (stac d22set_eq 2);
by Auto_tac;
qed "d22set_fin";

val [zfact_eq] = zfact.simps;
Delsimps zfact.simps;

Goal "setprod(d22set a) = zfact a";
by (induct_thm_tac d22set.induct "a" 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 1);
by (stac d22set_eq 1);
by (stac zfact_eq 1);
by (case_tac "#1<a" 1);
by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 2);
by (asm_full_simp_tac (simpset() addsimps [d22set_fin,d22set_le_swap]) 1);
qed "d22set_prod_zfact";

```