author  wenzelm 
Sun, 04 Feb 2001 19:31:13 +0100  
changeset 11049  7eef34adb852 
parent 9508  4d01dbf6ded7 
child 11549  e7265e70fd7c 
permissions  rwrr 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

1 
(* Title: HOL/NumberTheory/BijectionRel.thy 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

2 
ID: $Id$ 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

3 
Author: Thomas M. Rasmussen 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

4 
Copyright 2000 University of Cambridge 
9508
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 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

7 
header {* Bijections between sets *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

8 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

9 
theory BijectionRel = Main: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

10 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

11 
text {* 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

12 
Inductive definitions of bijections between two different sets and 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

13 
between the same set. Theorem for relating the two definitions. 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

14 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

15 
\bigskip 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

16 
*} 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

17 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

18 
consts 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

19 
bijR :: "('a => 'b => bool) => ('a set * 'b set) set" 
9508
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 
inductive "bijR P" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

22 
intros 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

23 
empty [simp]: "({}, {}) \<in> bijR P" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

24 
insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

25 
==> (insert a A, insert b B) \<in> bijR P" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

26 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

27 
text {* 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

28 
Add extra condition to @{term insert}: @{term "\<forall>b \<in> B. \<not> P a b"} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

29 
(and similar for @{term A}). 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

30 
*} 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

31 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

32 
constdefs 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

33 
bijP :: "('a => 'a => bool) => 'a set => bool" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

34 
"bijP P F == \<forall>a b. a \<in> F \<and> P a b > b \<in> F" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

35 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

36 
uniqP :: "('a => 'a => bool) => bool" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

37 
"uniqP P == \<forall>a b c d. P a b \<and> P c d > (a = c) = (b = d)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

38 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

39 
symP :: "('a => 'a => bool) => bool" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

40 
"symP P == \<forall>a b. P a b = P b a" 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

41 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

42 
consts 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

43 
bijER :: "('a => 'a => bool) => 'a set set" 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

44 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

45 
inductive "bijER P" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

46 
intros 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

47 
empty [simp]: "{} \<in> bijER P" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

48 
insert1: "P a a ==> a \<notin> A ==> A \<in> bijER P ==> insert a A \<in> bijER P" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

49 
insert2: "P a b ==> a \<noteq> b ==> a \<notin> A ==> b \<notin> A ==> A \<in> bijER P 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

50 
==> insert a (insert b A) \<in> bijER P" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

51 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

52 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

53 
text {* \medskip @{term bijR} *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

54 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

55 
lemma fin_bijRl: "(A, B) \<in> bijR P ==> finite A" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

56 
apply (erule bijR.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

57 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

58 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

59 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

60 
lemma fin_bijRr: "(A, B) \<in> bijR P ==> finite B" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

61 
apply (erule bijR.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

62 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

63 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

64 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

65 
lemma aux_induct: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

66 
"finite F ==> F \<subseteq> A ==> P {} ==> 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

67 
(!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

68 
==> P F" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

69 
proof  
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

70 
case antecedent 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

71 
assume major: "finite F" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

72 
and subs: "F \<subseteq> A" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

73 
show ?thesis 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

74 
apply (rule subs [THEN rev_mp]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

75 
apply (rule major [THEN finite_induct]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

76 
apply (blast intro: antecedent)+ 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

77 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

78 
qed 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

79 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

80 
lemma aux: "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

81 
apply (unfold inj_on_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

82 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

83 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

84 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

85 
lemma aux: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

86 
"\<forall>a. a \<in> A > P a (f a) ==> inj_on f A ==> finite A ==> F <= A 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

87 
==> (F, f ` F) \<in> bijR P" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

88 
apply (rule_tac F = F and A = A in aux_induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

89 
apply (rule finite_subset) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

90 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

91 
apply (rule bijR.insert) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

92 
apply (rule_tac [3] aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

93 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

94 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

95 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

96 
lemma inj_func_bijR: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

97 
"\<forall>a. a \<in> A > P a (f a) ==> inj_on f A ==> finite A 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

98 
==> (A, f ` A) \<in> bijR P" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

99 
apply (rule aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

100 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

101 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

102 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

103 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

104 
text {* \medskip @{term bijER} *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

105 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

106 
lemma fin_bijER: "A \<in> bijER P ==> finite A" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

107 
apply (erule bijER.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

108 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

109 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

110 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

111 
lemma aux1: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

112 
"a \<notin> A ==> a \<notin> B ==> F \<subseteq> insert a A ==> F \<subseteq> insert a B ==> a \<in> F 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

113 
==> \<exists>C. F = insert a C \<and> a \<notin> C \<and> C <= A \<and> C <= B" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

114 
apply (rule_tac x = "F  {a}" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

115 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

116 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

117 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

118 
lemma aux2: "a \<noteq> b ==> a \<notin> A ==> b \<notin> B ==> a \<in> F ==> b \<in> F 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

119 
==> F \<subseteq> insert a A ==> F \<subseteq> insert b B 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

120 
==> \<exists>C. F = insert a (insert b C) \<and> a \<notin> C \<and> b \<notin> C \<and> C \<subseteq> A \<and> C \<subseteq> B" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

121 
apply (rule_tac x = "F  {a, b}" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

122 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

123 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

124 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

125 
lemma aux_uniq: "uniqP P ==> P a b ==> P c d ==> (a = c) = (b = d)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

126 
apply (unfold uniqP_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

127 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

128 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

129 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

130 
lemma aux_sym: "symP P ==> P a b = P b a" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

131 
apply (unfold symP_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

132 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

133 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

134 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

135 
lemma aux_in1: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

136 
"uniqP P ==> b \<notin> C ==> P b b ==> bijP P (insert b C) ==> bijP P C" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

137 
apply (unfold bijP_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

138 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

139 
apply (subgoal_tac "b \<noteq> a") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

140 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

141 
apply clarify 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

142 
apply (simp add: aux_uniq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

143 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

144 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

145 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

146 
lemma aux_in2: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

147 
"symP P ==> uniqP P ==> a \<notin> C ==> b \<notin> C ==> a \<noteq> b ==> P a b 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

148 
==> bijP P (insert a (insert b C)) ==> bijP P C" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

149 
apply (unfold bijP_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

150 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

151 
apply (subgoal_tac "aa \<noteq> a") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

152 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

153 
apply clarify 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

154 
apply (subgoal_tac "aa \<noteq> b") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

155 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

156 
apply clarify 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

157 
apply (simp add: aux_uniq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

158 
apply (subgoal_tac "ba \<noteq> a") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

159 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

160 
apply (subgoal_tac "P a aa") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

161 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

162 
apply (simp add: aux_sym) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

163 
apply (subgoal_tac "b = aa") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

164 
apply (rule_tac [2] iffD1) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

165 
apply (rule_tac [2] a = a and c = a and P = P in aux_uniq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

166 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

167 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

168 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

169 
lemma aux: "\<forall>a b. Q a \<and> P a b > R b ==> P a b ==> Q a ==> R b" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

170 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

171 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

172 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

173 
lemma aux_bij: "bijP P F ==> symP P ==> P a b ==> (a \<in> F) = (b \<in> F)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

174 
apply (unfold bijP_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

175 
apply (rule iffI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

176 
apply (erule_tac [!] aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

177 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

178 
apply (rule iffD2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

179 
apply (rule_tac P = P in aux_sym) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

180 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

181 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

182 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

183 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

184 
lemma aux_bijRER: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

185 
"(A, B) \<in> bijR P ==> uniqP P ==> symP P 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

186 
==> \<forall>F. bijP P F \<and> F \<subseteq> A \<and> F \<subseteq> B > F \<in> bijER P" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

187 
apply (erule bijR.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

188 
apply simp 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

189 
apply (case_tac "a = b") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

190 
apply clarify 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

191 
apply (case_tac "b \<in> F") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

192 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

193 
apply (rotate_tac 1) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

194 
apply (simp add: subset_insert) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

195 
apply (cut_tac F = F and a = b and A = A and B = B in aux1) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

196 
prefer 6 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

197 
apply clarify 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

198 
apply (rule bijER.insert1) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

199 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

200 
apply (subgoal_tac "bijP P C") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

201 
apply simp 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

202 
apply (rule aux_in1) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

203 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

204 
apply clarify 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

205 
apply (case_tac "a \<in> F") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

206 
apply (case_tac [!] "b \<in> F") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

207 
apply (rotate_tac [24] 2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

208 
apply (cut_tac F = F and a = a and b = b and A = A and B = B 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

209 
in aux2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

210 
apply (simp_all add: subset_insert) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

211 
apply clarify 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

212 
apply (rule bijER.insert2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

213 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

214 
apply (subgoal_tac "bijP P C") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

215 
apply simp 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

216 
apply (rule aux_in2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

217 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

218 
apply (subgoal_tac "b \<in> F") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

219 
apply (rule_tac [2] iffD1) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

220 
apply (rule_tac [2] a = a and F = F and P = P in aux_bij) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

221 
apply (simp_all (no_asm_simp)) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

222 
apply (subgoal_tac [2] "a \<in> F") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

223 
apply (rule_tac [3] iffD2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

224 
apply (rule_tac [3] b = b and F = F and P = P in aux_bij) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

225 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

226 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

227 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

228 
lemma bijR_bijER: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

229 
"(A, A) \<in> bijR P ==> 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

230 
bijP P A ==> uniqP P ==> symP P ==> A \<in> bijER P" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

231 
apply (cut_tac A = A and B = A and P = P in aux_bijRER) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

232 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

233 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

234 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

235 
end 