isabelle: src/HOL/NumberTheory/IntFact.ML@819ee80305a8 (annotated)

9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	1	(* Title: IntPowerFact.ML
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	2	ID: $Id$
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	3	Author: Thomas M. Rasmussen
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	4	Copyright 2000 University of Cambridge
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	5
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	6	Factorial on integers.
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	7	Product of finite set.
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	8	Recursively defined set including all Integers from 2 up to a.
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	9	*)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	10
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	11
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	12	(---- setprod ----)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	13
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	14	Goalw [setprod_def] "setprod {} = #1";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	15	by (Simp_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	16	qed "setprod_empty";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	17	Addsimps [setprod_empty];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	18
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	19	Goalw [setprod_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	20	"[\| finite A; a ~: A \|] ==> setprod (insert a A) = a * setprod A";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	21	by (asm_simp_tac (simpset() addsimps [zmult_left_commute,
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	22	export fold_insert]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	23	qed "setprod_insert";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	24	Addsimps [setprod_insert];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	25
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	26	(---- IntFact ----)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	27
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	28	val [d22set_eq] = d22set.simps;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	29	Delsimps d22set.simps;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	30
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	31	val [prem1,prem2] =
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	32	Goal "[\| !!a. P {} a; \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	33	\ !!a. [\| #1<(a::int); P (d22set (a-#1)) (a-#1) \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	34	\ ==> P (d22set a) a \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	35	\ ==> P (d22set u) u";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	36	by (rtac d22set.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	37	by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	38	by (case_tac "#1<a" 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	39	by (rtac prem2 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	40	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	41	by (ALLGOALS (asm_simp_tac (simpset() addsimps [d22set_eq,prem1])));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	42	qed "d22set_induct";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	43
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	44	Goal "b:(d22set a) --> #1<b";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9736 diff changeset	45	by (induct_thm_tac d22set_induct "a" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	46	by (stac d22set_eq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	47	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	48	qed_spec_mp "d22set_g_1";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	49
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	50	Goal "b:(d22set a) --> b<=a";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9736 diff changeset	51	by (induct_thm_tac d22set_induct "a" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	52	by (stac d22set_eq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	53	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	54	qed_spec_mp "d22set_le";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	55
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	56	Goal "a<b ==> b~:(d22set a)";
10198 2b255b772585 tidied paulson parents: 9747 diff changeset	57	by (auto_tac (claset() addDs [d22set_le], simpset()));
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	58	qed "d22set_le_swap";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	59
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	60	Goal "#1<b --> b<=a --> b:(d22set a)";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9736 diff changeset	61	by (induct_thm_tac d22set.induct "a" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	62	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	63	by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq])));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	64	qed_spec_mp "d22set_mem";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	65
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	66	Goal "finite (d22set a)";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9736 diff changeset	67	by (induct_thm_tac d22set_induct "a" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	68	by (stac d22set_eq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	69	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	70	qed "d22set_fin";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	71
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	72	val [zfact_eq] = zfact.simps;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	73	Delsimps zfact.simps;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	74
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	75	Goal "setprod(d22set a) = zfact a";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9736 diff changeset	76	by (induct_thm_tac d22set.induct "a" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	77	by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	78	by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	79	by (stac d22set_eq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	80	by (stac zfact_eq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	81	by (case_tac "#1<a" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	82	by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	83	by (asm_full_simp_tac (simpset() addsimps [d22set_fin,d22set_le_swap]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	84	qed "d22set_prod_zfact";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	85

author	nipkow
	Thu, 21 Dec 2000 19:19:18 +0100
changeset 10724	819ee80305a8
parent 10198	2b255b772585
permissions	-rw-r--r--