isabelle: src/HOL/NumberTheory/BijectionRel.ML@50be659d4222 (annotated)

9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	1	(* Title: BijectionRel.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	Inductive definitions of bijections between two different sets and
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	7	between the same set.
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	8	Theorem for relating the two definitions
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	(*** bijR ***)
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	Addsimps [bijR.empty];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	15
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	16	Goal "(A,B) : (bijR P) ==> finite A";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	17	by (etac bijR.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	18	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	19	qed "fin_bijRl";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	20
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	21	Goal "(A,B) : (bijR P) ==> finite B";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	22	by (etac bijR.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	23	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	24	qed "fin_bijRr";
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	val major::subs::prems =
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	27	Goal "[\| finite F; F <= A; P({}); \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	28	\ !!F a. [\| F <= A; a:A; a ~: F; P(F) \|] ==> P(insert a F) \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	29	\ ==> P(F)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	30	by (rtac (subs RS rev_mp) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	31	by (rtac (major RS finite_induct) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	32	by (ALLGOALS (blast_tac (claset() addIs prems)));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	33	val lemma_induct = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	34
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	35	Goalw [inj_on_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	36	"[\| A <= B; a ~: A ; a : B; inj_on f B \|] ==> (f a) ~: f``A";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	37	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	38	val lemma = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	39
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	40	Goal "[\| ALL a. a:A --> P a (f a); inj_on f A; finite A; F <= A \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	41	\ ==> (F,f``F) : bijR P";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	42	by (res_inst_tac [("F","F"),("A","A")] lemma_induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	43	by (rtac finite_subset 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	44	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	45	by (rtac bijR.insert 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	46	by (rtac lemma 3);
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	val lemma = result();
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 "[\| ALL a. a:A --> P a (f a); inj_on f A; finite A \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	51	\ ==> (A,f``A) : bijR P";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	52	by (rtac lemma 1);
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 "inj_func_bijR";
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
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	57	(*** bijER ***)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	58
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	59	Addsimps [bijER.empty];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	60
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	61	Goal "A : bijER P ==> finite A";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	62	by (etac bijER.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	63	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	64	qed "fin_bijER";
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 "[\| a ~: A; a ~: B; F <= insert a A; F <= insert a B; a : F \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	67	\ ==> (EX C. F = insert a C & a ~: C & C <= A & C <= B)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	68	by (res_inst_tac [("x","F-{a}")] exI 1);
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	val lemma1 = result();
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	Goal "[\| a ~= b; a ~: A; b ~: B; a : F; b : F; \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	73	\ F <= insert a A; F <= insert b B \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	74	\ ==> (EX C. F = insert a (insert b C) & a ~: C & b ~: C & \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	75	\ C <= A & C <= B)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	76	by (res_inst_tac [("x","F-{a,b}")] exI 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	77	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	78	val lemma2 = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	79
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	80	Goalw [uniqP_def] "[\| uniqP P; P a b; P c d \|] ==> (a=c) = (b=d)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	81	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	82	val lemma_uniq = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	83
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	84	Goalw [symP_def] "symP P ==> (P a b) = (P b a)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	85	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	86	val lemma_sym = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	87
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	88	Goalw [bijP_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	89	"[\| uniqP P; b ~: C; P b b; bijP P (insert b C) \|] ==> bijP P C";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	90	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	91	by (subgoal_tac "b~=a" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	92	by (Clarify_tac 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	93	by (asm_full_simp_tac (simpset() addsimps [lemma_uniq]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	94	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	95	val lemma_in1 = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	96
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	97	Goalw [bijP_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	98	"[\| symP P; uniqP P; a ~: C; b ~: C; a ~= b; P a b; \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	99	\ bijP P (insert a (insert b C)) \|] ==> bijP P C";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	100	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	101	by (subgoal_tac "aa~=a" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	102	by (Clarify_tac 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	103	by (subgoal_tac "aa~=b" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	104	by (Clarify_tac 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	105	by (asm_full_simp_tac (simpset() addsimps [lemma_uniq]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	106	by (subgoal_tac "ba~=a" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	107	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	108	by (subgoal_tac "P a aa" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	109	by (asm_simp_tac (simpset() addsimps [lemma_sym]) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	110	by (subgoal_tac "b=aa" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	111	by (rtac iffD1 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	112	by (res_inst_tac [("a","a"),("c","a"),("P","P")] lemma_uniq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	113	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	114	val lemma_in2 = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	115
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	116	Goal "[\| ALL a b. Q a & P a b --> R b; P a b; Q a \|] ==> R b";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	117	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	118	val lemma = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	119
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	120	Goalw [bijP_def] "[\| bijP P F; symP P; P a b \|] ==> (a:F) = (b:F)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	121	by (rtac iffI 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	122	by (ALLGOALS (etac lemma));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	123	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	124	by (rtac iffD2 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	125	by (res_inst_tac [("P","P")] lemma_sym 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	126	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	127	val lemma_bij = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	128
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	129	Goal "[\| (A,B) : bijR P; uniqP P; symP P \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	130	\ ==> (ALL F. (bijP P F) & F<=A & F<=B --> F : bijER P)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	131	by (etac bijR.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	132	by (Simp_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	133	by (case_tac "a=b" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	134	by (Clarify_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	135	by (case_tac "b:F" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	136	by (rotate_tac ~1 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	137	by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	138	by (cut_inst_tac [("F","F"),("a","b"),("A","A"),("B","B")] lemma1 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	139	by (Clarify_tac 6);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	140	by (rtac bijER.insert1 6);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	141	by (ALLGOALS Asm_full_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	142	by (subgoal_tac "bijP P C" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	143	by (Asm_full_simp_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	144	by (rtac lemma_in1 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	145	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	146	by (Clarify_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	147	by (case_tac "a:F" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	148	by (ALLGOALS (case_tac "b:F"));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	149	by (rotate_tac ~2 4);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	150	by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 4);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	151	by (rotate_tac ~2 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	152	by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	153	by (rotate_tac ~2 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	154	by (asm_full_simp_tac (simpset() addsimps [subset_insert]) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	155	by (cut_inst_tac [("F","F"),("a","a"),("b","b"),("A","A"),("B","B")]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	156	lemma2 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	157	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	158	by (Clarify_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	159	by (rtac bijER.insert2 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	160	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	161	by (subgoal_tac "bijP P C" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	162	by (Asm_full_simp_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	163	by (rtac lemma_in2 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	164	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	165	by (subgoal_tac "b:F" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	166	by (rtac iffD1 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	167	by (res_inst_tac [("a","a"),("F","F"),("P","P")] lemma_bij 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	168	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	169	by (subgoal_tac "a:F" 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	170	by (rtac iffD2 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	171	by (res_inst_tac [("b","b"),("F","F"),("P","P")] lemma_bij 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	172	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	173	val lemma_bijRER = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	174
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	175	Goal "[\| (A,A) : bijR P; (bijP P A); uniqP P; symP P \|] ==> A : bijER P";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	176	by (cut_inst_tac [("A","A"),("B","A"),("P","P")] lemma_bijRER 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	177	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	178	qed "bijR_bijER";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	179
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	180
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	181
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	182

author	wenzelm
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 9508	4d01dbf6ded7
child 10834	a7897aebbffc
permissions	-rw-r--r--