author  wenzelm 
Tue, 27 Aug 2002 11:03:05 +0200  
changeset 13524  604d0f3622d6 
parent 11549  e7265e70fd7c 
child 13630  a013a9dd370f 
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  
11549  70 
case rule_context 
11049
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]) 
11549  76 
apply (blast intro: rule_context)+ 
11049
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 

13524  80 
lemma inj_func_bijR_aux1: 
81 
"A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A" 

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

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

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

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

85 

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

87 
"\<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

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

89 
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

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

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

92 
apply (rule bijR.insert) 
13524  93 
apply (rule_tac [3] inj_func_bijR_aux1) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

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

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

96 

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

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

98 
"\<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

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

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

102 
done 
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 

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

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

106 

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

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

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

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

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

111 

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

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

113 
"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

114 
==> \<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

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

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

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

118 

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

119 
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

120 
==> 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

121 
==> \<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

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

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

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

125 

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

126 
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

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

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

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

130 

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

131 
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

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

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

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

135 

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

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

137 
"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

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

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

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

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

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

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

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

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

146 

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

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

148 
"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

149 
==> 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

166 
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

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

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

169 

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

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

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

173 

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

174 
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

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

176 
apply (rule iffI) 
13524  177 
apply (erule_tac [!] aux_foo) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

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

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

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

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

182 
done 
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 

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

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

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

187 
==> \<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

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

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

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

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

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

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

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

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

196 
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

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

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

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

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

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

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

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

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

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

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

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

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

209 
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

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

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

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

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

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

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

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

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

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

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

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

221 
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

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

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

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

225 
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

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

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

228 

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

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

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

231 
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

232 
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

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

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

235 

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

236 
end 