author  ballarin 
Mon, 23 Jul 2007 13:48:30 +0200  
changeset 23919  af871d13e320 
parent 23219  87ad6e8a5f2c 
child 23951  b188cac107ad 
permissions  rwrr 
22657  1 
(* Title: HOL/ex/LocaleTest2.thy 
2 
ID: $Id$ 

3 
Author: Clemens Ballarin 

4 
Copyright (c) 2007 by Clemens Ballarin 

5 

6 
More regression tests for locales. 

7 
Definitions are less natural in FOL, since there is no selection operator. 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

8 
Hence we do them here in HOL, not in the main test suite for locales, 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

9 
which is FOL/ex/LocaleTest.thy 
22657  10 
*) 
11 

12 
header {* Test of Locale Interpretation *} 

13 

14 
theory LocaleTest2 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

15 
imports GCD 
22657  16 
begin 
17 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

18 
section {* Interpretation of Defined Concepts *} 
22657  19 

20 
text {* Naming convention for global objects: prefixes D and d *} 

21 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

22 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

23 
subsection {* Lattices *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

24 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

25 
text {* Much of the lattice proofs are from HOL/Lattice. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

26 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

27 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

28 
subsubsection {* Definitions *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

29 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

30 
locale dpo = 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

31 
fixes le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>" 50) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

32 
assumes refl [intro, simp]: "x \<sqsubseteq> x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

33 
and anti_sym [intro]: "[ x \<sqsubseteq> y; y \<sqsubseteq> x ] ==> x = y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

34 
and trans [trans]: "[ x \<sqsubseteq> y; y \<sqsubseteq> z ] ==> x \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

35 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

36 
begin 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

37 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

38 
theorem circular: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

39 
"[ x \<sqsubseteq> y; y \<sqsubseteq> z; z \<sqsubseteq> x ] ==> x = y & y = z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

40 
by (blast intro: trans) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

41 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

42 
definition 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

43 
less :: "['a, 'a] => bool" (infixl "\<sqsubset>" 50) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

44 
where "(x \<sqsubset> y) = (x \<sqsubseteq> y & x ~= y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

45 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

46 
theorem abs_test: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

47 
"op \<sqsubset> = (%x y. x \<sqsubset> y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

48 
by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

49 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

50 
definition 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

51 
is_inf :: "['a, 'a, 'a] => bool" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

52 
where "is_inf x y i = (i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

53 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

54 
definition 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

55 
is_sup :: "['a, 'a, 'a] => bool" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

56 
where "is_sup x y s = (x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z))" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

57 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

58 
end 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

59 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

60 
locale dlat = dpo + 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

61 
assumes ex_inf: "EX inf. dpo.is_inf le x y inf" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

62 
and ex_sup: "EX sup. dpo.is_sup le x y sup" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

63 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

64 
begin 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

65 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

66 
definition 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

67 
meet :: "['a, 'a] => 'a" (infixl "\<sqinter>" 70) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

68 
where "x \<sqinter> y = (THE inf. is_inf x y inf)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

69 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

70 
definition 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

71 
join :: "['a, 'a] => 'a" (infixl "\<squnion>" 65) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

72 
where "x \<squnion> y = (THE sup. is_sup x y sup)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

73 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

74 
lemma is_infI [intro?]: "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

75 
(\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> is_inf x y i" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

76 
by (unfold is_inf_def) blast 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

77 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

78 
lemma is_inf_lower [elim?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

79 
"is_inf x y i \<Longrightarrow> (i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

80 
by (unfold is_inf_def) blast 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

81 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

82 
lemma is_inf_greatest [elim?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

83 
"is_inf x y i \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

84 
by (unfold is_inf_def) blast 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

85 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

86 
theorem is_inf_uniq: "is_inf x y i \<Longrightarrow> is_inf x y i' \<Longrightarrow> i = i'" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

87 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

88 
assume inf: "is_inf x y i" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

89 
assume inf': "is_inf x y i'" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

90 
show ?thesis 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

91 
proof (rule anti_sym) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

92 
from inf' show "i \<sqsubseteq> i'" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

93 
proof (rule is_inf_greatest) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

94 
from inf show "i \<sqsubseteq> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

95 
from inf show "i \<sqsubseteq> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

96 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

97 
from inf show "i' \<sqsubseteq> i" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

98 
proof (rule is_inf_greatest) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

99 
from inf' show "i' \<sqsubseteq> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

100 
from inf' show "i' \<sqsubseteq> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

101 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

102 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

103 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

104 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

105 
theorem is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

106 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

107 
assume "x \<sqsubseteq> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

108 
show ?thesis 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

109 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

110 
show "x \<sqsubseteq> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

111 
show "x \<sqsubseteq> y" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

112 
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

113 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

114 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

115 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

116 
lemma meet_equality [elim?]: "is_inf x y i \<Longrightarrow> x \<sqinter> y = i" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

117 
proof (unfold meet_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

118 
assume "is_inf x y i" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

119 
then show "(THE i. is_inf x y i) = i" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

120 
by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y i`]) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

121 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

122 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

123 
lemma meetI [intro?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

124 
"i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> x \<sqinter> y = i" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

125 
by (rule meet_equality, rule is_infI) blast+ 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

126 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

127 
lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

128 
proof (unfold meet_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

129 
from ex_inf obtain i where "is_inf x y i" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

130 
then show "is_inf x y (THE i. is_inf x y i)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

131 
by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y i`]) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

132 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

133 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

134 
lemma meet_left [intro?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

135 
"x \<sqinter> y \<sqsubseteq> x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

136 
by (rule is_inf_lower) (rule is_inf_meet) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

137 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

138 
lemma meet_right [intro?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

139 
"x \<sqinter> y \<sqsubseteq> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

140 
by (rule is_inf_lower) (rule is_inf_meet) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

141 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

142 
lemma meet_le [intro?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

143 
"[ z \<sqsubseteq> x; z \<sqsubseteq> y ] ==> z \<sqsubseteq> x \<sqinter> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

144 
by (rule is_inf_greatest) (rule is_inf_meet) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

145 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

146 
lemma is_supI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

147 
(\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> is_sup x y s" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

148 
by (unfold is_sup_def) blast 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

149 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

150 
lemma is_sup_least [elim?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

151 
"is_sup x y s \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

152 
by (unfold is_sup_def) blast 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

153 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

154 
lemma is_sup_upper [elim?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

155 
"is_sup x y s \<Longrightarrow> (x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> C) \<Longrightarrow> C" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

156 
by (unfold is_sup_def) blast 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

157 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

158 
theorem is_sup_uniq: "is_sup x y s \<Longrightarrow> is_sup x y s' \<Longrightarrow> s = s'" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

159 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

160 
assume sup: "is_sup x y s" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

161 
assume sup': "is_sup x y s'" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

162 
show ?thesis 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

163 
proof (rule anti_sym) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

164 
from sup show "s \<sqsubseteq> s'" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

165 
proof (rule is_sup_least) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

166 
from sup' show "x \<sqsubseteq> s'" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

167 
from sup' show "y \<sqsubseteq> s'" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

168 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

169 
from sup' show "s' \<sqsubseteq> s" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

170 
proof (rule is_sup_least) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

171 
from sup show "x \<sqsubseteq> s" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

172 
from sup show "y \<sqsubseteq> s" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

173 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

174 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

175 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

176 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

177 
theorem is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

178 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

179 
assume "x \<sqsubseteq> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

180 
show ?thesis 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

181 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

182 
show "x \<sqsubseteq> y" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

183 
show "y \<sqsubseteq> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

184 
fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

185 
show "y \<sqsubseteq> z" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

186 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

187 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

188 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

189 
lemma join_equality [elim?]: "is_sup x y s \<Longrightarrow> x \<squnion> y = s" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

190 
proof (unfold join_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

191 
assume "is_sup x y s" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

192 
then show "(THE s. is_sup x y s) = s" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

193 
by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y s`]) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

194 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

195 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

196 
lemma joinI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

197 
(\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = s" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

198 
by (rule join_equality, rule is_supI) blast+ 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

199 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

200 
lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

201 
proof (unfold join_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

202 
from ex_sup obtain s where "is_sup x y s" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

203 
then show "is_sup x y (THE s. is_sup x y s)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

204 
by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y s`]) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

205 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

206 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

207 
lemma join_left [intro?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

208 
"x \<sqsubseteq> x \<squnion> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

209 
by (rule is_sup_upper) (rule is_sup_join) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

210 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

211 
lemma join_right [intro?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

212 
"y \<sqsubseteq> x \<squnion> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

213 
by (rule is_sup_upper) (rule is_sup_join) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

214 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

215 
lemma join_le [intro?]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

216 
"[ x \<sqsubseteq> z; y \<sqsubseteq> z ] ==> x \<squnion> y \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

217 
by (rule is_sup_least) (rule is_sup_join) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

218 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

219 
theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

220 
proof (rule meetI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

221 
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

222 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

223 
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

224 
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

225 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

226 
have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

227 
also have "\<dots> \<sqsubseteq> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

228 
finally show ?thesis . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

229 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

230 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

231 
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

232 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

233 
have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

234 
also have "\<dots> \<sqsubseteq> z" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

235 
finally show ?thesis . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

236 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

237 
fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

238 
show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

239 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

240 
show "w \<sqsubseteq> x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

241 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

242 
have "w \<sqsubseteq> x \<sqinter> y" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

243 
also have "\<dots> \<sqsubseteq> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

244 
finally show ?thesis . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

245 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

246 
show "w \<sqsubseteq> y \<sqinter> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

247 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

248 
show "w \<sqsubseteq> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

249 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

250 
have "w \<sqsubseteq> x \<sqinter> y" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

251 
also have "\<dots> \<sqsubseteq> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

252 
finally show ?thesis . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

253 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

254 
show "w \<sqsubseteq> z" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

255 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

256 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

257 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

258 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

259 
theorem meet_commute: "x \<sqinter> y = y \<sqinter> x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

260 
proof (rule meetI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

261 
show "y \<sqinter> x \<sqsubseteq> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

262 
show "y \<sqinter> x \<sqsubseteq> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

263 
fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

264 
then show "z \<sqsubseteq> y \<sqinter> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

265 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

266 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

267 
theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

268 
proof (rule meetI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

269 
show "x \<sqsubseteq> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

270 
show "x \<sqsubseteq> x \<squnion> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

271 
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

272 
show "z \<sqsubseteq> x" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

273 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

274 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

275 
theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

276 
proof (rule joinI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

277 
show "x \<squnion> y \<sqsubseteq> x \<squnion> (y \<squnion> z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

278 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

279 
show "x \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

280 
show "y \<sqsubseteq> x \<squnion> (y \<squnion> z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

281 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

282 
have "y \<sqsubseteq> y \<squnion> z" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

283 
also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

284 
finally show ?thesis . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

285 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

286 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

287 
show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

288 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

289 
have "z \<sqsubseteq> y \<squnion> z" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

290 
also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

291 
finally show ?thesis . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

292 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

293 
fix w assume "x \<squnion> y \<sqsubseteq> w" and "z \<sqsubseteq> w" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

294 
show "x \<squnion> (y \<squnion> z) \<sqsubseteq> w" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

295 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

296 
show "x \<sqsubseteq> w" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

297 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

298 
have "x \<sqsubseteq> x \<squnion> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

299 
also have "\<dots> \<sqsubseteq> w" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

300 
finally show ?thesis . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

301 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

302 
show "y \<squnion> z \<sqsubseteq> w" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

303 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

304 
show "y \<sqsubseteq> w" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

305 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

306 
have "y \<sqsubseteq> x \<squnion> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

307 
also have "... \<sqsubseteq> w" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

308 
finally show ?thesis . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

309 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

310 
show "z \<sqsubseteq> w" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

311 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

312 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

313 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

314 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

315 
theorem join_commute: "x \<squnion> y = y \<squnion> x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

316 
proof (rule joinI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

317 
show "x \<sqsubseteq> y \<squnion> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

318 
show "y \<sqsubseteq> y \<squnion> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

319 
fix z assume "y \<sqsubseteq> z" and "x \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

320 
then show "y \<squnion> x \<sqsubseteq> z" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

321 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

322 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

323 
theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

324 
proof (rule joinI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

325 
show "x \<sqsubseteq> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

326 
show "x \<sqinter> y \<sqsubseteq> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

327 
fix z assume "x \<sqsubseteq> z" and "x \<sqinter> y \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

328 
show "x \<sqsubseteq> z" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

329 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

330 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

331 
theorem meet_idem: "x \<sqinter> x = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

332 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

333 
have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

334 
also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

335 
finally show ?thesis . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

336 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

337 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

338 
theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

339 
proof (rule meetI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

340 
assume "x \<sqsubseteq> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

341 
show "x \<sqsubseteq> x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

342 
show "x \<sqsubseteq> y" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

343 
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

344 
show "z \<sqsubseteq> x" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

345 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

346 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

347 
theorem meet_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

348 
by (drule meet_related) (simp add: meet_commute) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

349 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

350 
theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

351 
proof (rule joinI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

352 
assume "x \<sqsubseteq> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

353 
show "y \<sqsubseteq> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

354 
show "x \<sqsubseteq> y" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

355 
fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

356 
show "y \<sqsubseteq> z" by fact 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

357 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

358 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

359 
theorem join_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

360 
by (drule join_related) (simp add: join_commute) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

361 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

362 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

363 
text {* Additional theorems *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

364 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

365 
theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

366 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

367 
assume "x \<sqsubseteq> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

368 
then have "is_inf x y x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

369 
then show "x \<sqinter> y = x" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

370 
next 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

371 
have "x \<sqinter> y \<sqsubseteq> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

372 
also assume "x \<sqinter> y = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

373 
finally show "x \<sqsubseteq> y" . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

374 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

375 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

376 
theorem meet_connection2: "(x \<sqsubseteq> y) = (y \<sqinter> x = x)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

377 
using meet_commute meet_connection by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

378 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

379 
theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

380 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

381 
assume "x \<sqsubseteq> y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

382 
then have "is_sup x y y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

383 
then show "x \<squnion> y = y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

384 
next 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

385 
have "x \<sqsubseteq> x \<squnion> y" .. 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

386 
also assume "x \<squnion> y = y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

387 
finally show "x \<sqsubseteq> y" . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

388 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

389 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

390 
theorem join_connection2: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

391 
using join_commute join_connection by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

392 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

393 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

394 
text {* Naming according to Jacobson I, p.\ 459. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

395 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

396 
lemmas L1 = join_commute meet_commute 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

397 
lemmas L2 = join_assoc meet_assoc 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

398 
(*lemmas L3 = join_idem meet_idem*) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

399 
lemmas L4 = join_meet_absorb meet_join_absorb 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

400 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

401 
end 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

402 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

403 
locale ddlat = dlat + 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

404 
assumes meet_distr: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

405 
"dlat.meet le x (dlat.join le y z) = 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

406 
dlat.join le (dlat.meet le x y) (dlat.meet le x z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

407 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

408 
begin 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

409 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

410 
lemma join_distr: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

411 
"x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

412 
txt {* Jacobson I, p.\ 462 *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

413 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

414 
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by (simp add: L4) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

415 
also have "... = x \<squnion> ((x \<sqinter> z) \<squnion> (y \<sqinter> z))" by (simp add: L2) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

416 
also have "... = x \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 meet_distr) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

417 
also have "... = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 L4) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

418 
also have "... = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by (simp add: meet_distr) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

419 
finally show ?thesis . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

420 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

421 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

422 
end 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

423 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

424 
locale dlo = dpo + 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

425 
assumes total: "x \<sqsubseteq> y  y \<sqsubseteq> x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

426 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

427 
begin 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

428 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

429 
lemma less_total: "x \<sqsubset> y  x = y  y \<sqsubset> x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

430 
using total 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

431 
by (unfold less_def) blast 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

432 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

433 
end 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

434 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

435 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

436 
interpretation dlo < dlat 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

437 
(* TODO: definition syntax is unavailable *) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

438 
proof unfold_locales 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

439 
fix x y 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

440 
from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

441 
then show "EX inf. is_inf x y inf" by blast 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

442 
next 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

443 
fix x y 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

444 
from total have "is_sup x y (if x \<sqsubseteq> y then y else x)" by (auto simp: is_sup_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

445 
then show "EX sup. is_sup x y sup" by blast 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

446 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

447 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

448 
interpretation dlo < ddlat 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

449 
proof unfold_locales 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

450 
fix x y z 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

451 
show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r") 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

452 
txt {* Jacobson I, p.\ 462 *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

453 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

454 
{ assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

455 
from c have "?l = y \<squnion> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

456 
by (metis c (*join_commute*) join_connection2 join_related2 (*meet_commute*) meet_connection meet_related2 total) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

457 
also from c have "... = ?r" by (metis (*c*) (*join_commute*) meet_related2) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

458 
finally have "?l = ?r" . } 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

459 
moreover 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

460 
{ assume c: "x \<sqsubseteq> y  x \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

461 
from c have "?l = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

462 
by (metis (*anti_sym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

463 
also from c have "... = ?r" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

464 
by (metis join_commute join_related2 meet_connection meet_related2 total) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

465 
finally have "?l = ?r" . } 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

466 
moreover note total 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

467 
ultimately show ?thesis by blast 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

468 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

469 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

470 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

471 
subsubsection {* Total order @{text "<="} on @{typ int} *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

472 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

473 
interpretation int: dpo ["op <= :: [int, int] => bool"] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

474 
where "(dpo.less (op <=) (x::int) y) = (x < y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

475 
txt {* We give interpretation for less, but not is\_inf and is\_sub. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

476 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

477 
show "dpo (op <= :: [int, int] => bool)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

478 
by unfold_locales auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

479 
then interpret int: dpo ["op <= :: [int, int] => bool"] . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

480 
txt {* Gives interpreted version of less\_def (without condition). *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

481 
show "(dpo.less (op <=) (x::int) y) = (x < y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

482 
by (unfold int.less_def) auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

483 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

484 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

485 
thm int.circular 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

486 
lemma "\<lbrakk> (x::int) \<le> y; y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> x = y \<and> y = z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

487 
apply (rule int.circular) apply assumption apply assumption apply assumption done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

488 
thm int.abs_test 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

489 
lemma "(op < :: [int, int] => bool) = op <" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

490 
apply (rule int.abs_test) done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

491 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

492 
interpretation int: dlat ["op <= :: [int, int] => bool"] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

493 
where "dlat.meet (op <=) (x::int) y = min x y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

494 
and "dlat.join (op <=) (x::int) y = max x y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

495 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

496 
show "dlat (op <= :: [int, int] => bool)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

497 
apply unfold_locales 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

498 
apply (unfold int.is_inf_def int.is_sup_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

499 
apply arith+ 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

500 
done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

501 
then interpret int: dlat ["op <= :: [int, int] => bool"] . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

502 
txt {* Interpretation to ease use of definitions, which are 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

503 
conditional in general but unconditional after interpretation. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

504 
show "dlat.meet (op <=) (x::int) y = min x y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

505 
apply (unfold int.meet_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

506 
apply (rule the_equality) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

507 
apply (unfold int.is_inf_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

508 
by auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

509 
show "dlat.join (op <=) (x::int) y = max x y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

510 
apply (unfold int.join_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

511 
apply (rule the_equality) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

512 
apply (unfold int.is_sup_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

513 
by auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

514 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

515 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

516 
interpretation int: dlo ["op <= :: [int, int] => bool"] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

517 
by unfold_locales arith 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

518 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

519 
text {* Interpreted theorems from the locales, involving defined terms. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

520 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

521 
thm int.less_def text {* from dpo *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

522 
thm int.meet_left text {* from dlat *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

523 
thm int.meet_distr text {* from ddlat *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

524 
thm int.less_total text {* from dlo *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

525 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

526 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

527 
subsubsection {* Total order @{text "<="} on @{typ nat} *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

528 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

529 
interpretation nat: dpo ["op <= :: [nat, nat] => bool"] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

530 
where "dpo.less (op <=) (x::nat) y = (x < y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

531 
txt {* We give interpretation for less, but not is\_inf and is\_sub. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

532 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

533 
show "dpo (op <= :: [nat, nat] => bool)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

534 
by unfold_locales auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

535 
then interpret nat: dpo ["op <= :: [nat, nat] => bool"] . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

536 
txt {* Gives interpreted version of less\_def (without condition). *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

537 
show "dpo.less (op <=) (x::nat) y = (x < y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

538 
apply (unfold nat.less_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

539 
apply auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

540 
done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

541 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

542 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

543 
interpretation nat: dlat ["op <= :: [nat, nat] => bool"] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

544 
where "dlat.meet (op <=) (x::nat) y = min x y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

545 
and "dlat.join (op <=) (x::nat) y = max x y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

546 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

547 
show "dlat (op <= :: [nat, nat] => bool)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

548 
apply unfold_locales 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

549 
apply (unfold nat.is_inf_def nat.is_sup_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

550 
apply arith+ 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

551 
done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

552 
then interpret nat: dlat ["op <= :: [nat, nat] => bool"] . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

553 
txt {* Interpretation to ease use of definitions, which are 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

554 
conditional in general but unconditional after interpretation. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

555 
show "dlat.meet (op <=) (x::nat) y = min x y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

556 
apply (unfold nat.meet_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

557 
apply (rule the_equality) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

558 
apply (unfold nat.is_inf_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

559 
by auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

560 
show "dlat.join (op <=) (x::nat) y = max x y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

561 
apply (unfold nat.join_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

562 
apply (rule the_equality) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

563 
apply (unfold nat.is_sup_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

564 
by auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

565 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

566 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

567 
interpretation nat: dlo ["op <= :: [nat, nat] => bool"] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

568 
by unfold_locales arith 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

569 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

570 
text {* Interpreted theorems from the locales, involving defined terms. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

571 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

572 
thm nat.less_def text {* from dpo *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

573 
thm nat.meet_left text {* from dlat *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

574 
thm nat.meet_distr text {* from ddlat *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

575 
thm nat.less_total text {* from ldo *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

576 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

577 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

578 
subsubsection {* Lattice @{text "dvd"} on @{typ nat} *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

579 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

580 
interpretation nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

581 
where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

582 
txt {* We give interpretation for less, but not is\_inf and is\_sub. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

583 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

584 
show "dpo (op dvd :: [nat, nat] => bool)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

585 
by unfold_locales (auto simp: dvd_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

586 
then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

587 
txt {* Gives interpreted version of less\_def (without condition). *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

588 
show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

589 
apply (unfold nat_dvd.less_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

590 
apply auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

591 
done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

592 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

593 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

594 
interpretation nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

595 
where "dlat.meet (op dvd) (x::nat) y = gcd (x, y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

596 
and "dlat.join (op dvd) (x::nat) y = lcm (x, y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

597 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

598 
show "dlat (op dvd :: [nat, nat] => bool)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

599 
apply unfold_locales 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

600 
apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

601 
apply (rule_tac x = "gcd (x, y)" in exI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

602 
apply auto [1] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

603 
apply (rule_tac x = "lcm (x, y)" in exI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

604 
apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_lowest) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

605 
done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

606 
then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

607 
txt {* Interpretation to ease use of definitions, which are 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

608 
conditional in general but unconditional after interpretation. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

609 
show "dlat.meet (op dvd) (x::nat) y = gcd (x, y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

610 
apply (unfold nat_dvd.meet_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

611 
apply (rule the_equality) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

612 
apply (unfold nat_dvd.is_inf_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

613 
by auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

614 
show "dlat.join (op dvd) (x::nat) y = lcm (x, y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

615 
apply (unfold nat_dvd.join_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

616 
apply (rule the_equality) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

617 
apply (unfold nat_dvd.is_sup_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

618 
by (auto intro: lcm_dvd1 lcm_dvd2 lcm_lowest) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

619 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

620 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

621 
text {* Interpreted theorems from the locales, involving defined terms. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

622 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

623 
thm nat_dvd.less_def text {* from dpo *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

624 
lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

625 
apply (rule nat_dvd.less_def) done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

626 
thm nat_dvd.meet_left text {* from dlat *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

627 
lemma "gcd (x, y) dvd x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

628 
apply (rule nat_dvd.meet_left) done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

629 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

630 
print_interps dpo 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

631 
print_interps dlat 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

632 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

633 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

634 
subsection {* Group example with defined operations @{text inv} and @{text unit} *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

635 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

636 
subsubsection {* Locale declarations and lemmas *} 
22657  637 

638 
locale Dsemi = 

639 
fixes prod (infixl "**" 65) 

640 
assumes assoc: "(x ** y) ** z = x ** (y ** z)" 

641 

642 
locale Dmonoid = Dsemi + 

643 
fixes one 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

644 
assumes l_one [simp]: "one ** x = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

645 
and r_one [simp]: "x ** one = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

646 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

647 
begin 
22657  648 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

649 
definition 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

650 
inv where "inv x = (THE y. x ** y = one & y ** x = one)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

651 
definition 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

652 
unit where "unit x = (EX y. x ** y = one & y ** x = one)" 
22657  653 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

654 
lemma inv_unique: 
22657  655 
assumes eq: "y ** x = one" "x ** y' = one" 
656 
shows "y = y'" 

657 
proof  

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

658 
from eq have "y = y ** (x ** y')" by (simp add: r_one) 
22657  659 
also have "... = (y ** x) ** y'" by (simp add: assoc) 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

660 
also from eq have "... = y'" by (simp add: l_one) 
22657  661 
finally show ?thesis . 
662 
qed 

663 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

664 
lemma unit_one [intro, simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

665 
"unit one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

666 
by (unfold unit_def) auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

667 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

668 
lemma unit_l_inv_ex: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

669 
"unit x ==> \<exists>y. y ** x = one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

670 
by (unfold unit_def) auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

671 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

672 
lemma unit_r_inv_ex: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

673 
"unit x ==> \<exists>y. x ** y = one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

674 
by (unfold unit_def) auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

675 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

676 
lemma unit_l_inv: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

677 
"unit x ==> inv x ** x = one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

678 
apply (simp add: unit_def inv_def) apply (erule exE) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

679 
apply (rule theI2, fast) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

680 
apply (rule inv_unique) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

681 
apply fast+ 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

682 
done 
22657  683 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

684 
lemma unit_r_inv: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

685 
"unit x ==> x ** inv x = one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

686 
apply (simp add: unit_def inv_def) apply (erule exE) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

687 
apply (rule theI2, fast) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

688 
apply (rule inv_unique) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

689 
apply fast+ 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

690 
done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

691 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

692 
lemma unit_inv_unit [intro, simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

693 
"unit x ==> unit (inv x)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

694 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

695 
assume x: "unit x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

696 
show "unit (inv x)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

697 
by (auto simp add: unit_def 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

698 
intro: unit_l_inv unit_r_inv x) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

699 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

700 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

701 
lemma unit_l_cancel [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

702 
"unit x ==> (x ** y = x ** z) = (y = z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

703 
proof 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

704 
assume eq: "x ** y = x ** z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

705 
and G: "unit x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

706 
then have "(inv x ** x) ** y = (inv x ** x) ** z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

707 
by (simp add: assoc) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

708 
with G show "y = z" by (simp add: unit_l_inv) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

709 
next 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

710 
assume eq: "y = z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

711 
and G: "unit x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

712 
then show "x ** y = x ** z" by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

713 
qed 
22657  714 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

715 
lemma unit_inv_inv [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

716 
"unit x ==> inv (inv x) = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

717 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

718 
assume x: "unit x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

719 
then have "inv x ** inv (inv x) = inv x ** x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

720 
by (simp add: unit_l_inv unit_r_inv) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

721 
with x show ?thesis by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

722 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

723 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

724 
lemma inv_inj_on_unit: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

725 
"inj_on inv {x. unit x}" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

726 
proof (rule inj_onI, simp) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

727 
fix x y 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

728 
assume G: "unit x" "unit y" and eq: "inv x = inv y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

729 
then have "inv (inv x) = inv (inv y)" by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

730 
with G show "x = y" by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

731 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

732 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

733 
lemma unit_inv_comm: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

734 
assumes inv: "x ** y = one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

735 
and G: "unit x" "unit y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

736 
shows "y ** x = one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

737 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

738 
from G have "x ** y ** x = x ** one" by (auto simp add: inv) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

739 
with G show ?thesis by (simp del: r_one add: assoc) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

740 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

741 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

742 
end 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

743 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

744 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

745 
locale Dgrp = Dmonoid + 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

746 
assumes unit [intro, simp]: "Dmonoid.unit (op **) one x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

747 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

748 
begin 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

749 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

750 
lemma l_inv_ex [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

751 
"\<exists>y. y ** x = one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

752 
using unit_l_inv_ex by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

753 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

754 
lemma r_inv_ex [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

755 
"\<exists>y. x ** y = one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

756 
using unit_r_inv_ex by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

757 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

758 
lemma l_inv [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

759 
"inv x ** x = one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

760 
using unit_l_inv by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

761 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

762 
lemma l_cancel [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

763 
"(x ** y = x ** z) = (y = z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

764 
using unit_l_inv by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

765 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

766 
lemma r_inv [simp]: 
22657  767 
"x ** inv x = one" 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

768 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

769 
have "inv x ** (x ** inv x) = inv x ** one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

770 
by (simp add: assoc [symmetric] l_inv) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

771 
then show ?thesis by (simp del: r_one) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

772 
qed 
22657  773 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

774 
lemma r_cancel [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

775 
"(y ** x = z ** x) = (y = z)" 
22657  776 
proof 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

777 
assume eq: "y ** x = z ** x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

778 
then have "y ** (x ** inv x) = z ** (x ** inv x)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

779 
by (simp add: assoc [symmetric] del: r_inv) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

780 
then show "y = z" by simp 
22657  781 
qed simp 
782 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

783 
lemma inv_one [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

784 
"inv one = one" 
22657  785 
proof  
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

786 
have "inv one = one ** (inv one)" by (simp del: r_inv) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

787 
moreover have "... = one" by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

788 
finally show ?thesis . 
22657  789 
qed 
790 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

791 
lemma inv_inv [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

792 
"inv (inv x) = x" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

793 
using unit_inv_inv by simp 
22657  794 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

795 
lemma inv_inj: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

796 
"inj_on inv UNIV" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

797 
using inv_inj_on_unit by simp 
22657  798 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

799 
lemma inv_mult_group: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

800 
"inv (x ** y) = inv y ** inv x" 
22657  801 
proof  
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

802 
have "inv (x ** y) ** (x ** y) = (inv y ** inv x) ** (x ** y)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

803 
by (simp add: assoc l_inv) (simp add: assoc [symmetric]) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

804 
then show ?thesis by (simp del: l_inv) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

805 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

806 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

807 
lemma inv_comm: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

808 
"x ** y = one ==> y ** x = one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

809 
by (rule unit_inv_comm) auto 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

810 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

811 
lemma inv_equality: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

812 
"y ** x = one ==> inv x = y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

813 
apply (simp add: inv_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

814 
apply (rule the_equality) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

815 
apply (simp add: inv_comm [of y x]) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

816 
apply (rule r_cancel [THEN iffD1], auto) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

817 
done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

818 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

819 
end 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

820 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

821 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

822 
locale Dhom = Dgrp prod (infixl "**" 65) one + Dgrp sum (infixl "+++" 60) zero + 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

823 
fixes hom 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

824 
assumes hom_mult [simp]: "hom (x ** y) = hom x +++ hom y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

825 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

826 
begin 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

827 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

828 
lemma hom_one [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

829 
"hom one = zero" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

830 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

831 
have "hom one +++ zero = hom one +++ hom one" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

832 
by (simp add: hom_mult [symmetric] del: hom_mult) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

833 
then show ?thesis by (simp del: r_one) 
22657  834 
qed 
835 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

836 
end 
22657  837 

838 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

839 
subsubsection {* Interpretation of Functions *} 
22657  840 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

841 
interpretation Dfun: Dmonoid ["op o" "id :: 'a => 'a"] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

842 
where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

843 
(* and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *) 
22657  844 
proof  
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

845 
show "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

846 
note Dmonoid = this 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

847 
(* 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

848 
from this interpret Dmonoid ["op o" "id :: 'a => 'a"] . 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

849 
*) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

850 
show "Dmonoid.unit (op o) (id :: 'a => 'a) f = bij f" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

851 
apply (unfold Dmonoid.unit_def [OF Dmonoid]) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

852 
apply rule apply clarify 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

853 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

854 
fix f g 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

855 
assume id1: "f o g = id" and id2: "g o f = id" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

856 
show "bij f" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

857 
proof (rule bijI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

858 
show "inj f" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

859 
proof (rule inj_onI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

860 
fix x y 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

861 
assume "f x = f y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

862 
then have "(g o f) x = (g o f) y" by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

863 
with id2 show "x = y" by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

864 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

865 
next 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

866 
show "surj f" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

867 
proof (rule surjI) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

868 
fix x 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

869 
from id1 have "(f o g) x = x" by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

870 
then show "f (g x) = x" by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

871 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

872 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

873 
next 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

874 
fix f 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

875 
assume bij: "bij f" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

876 
then 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

877 
have inv: "f o Hilbert_Choice.inv f = id & Hilbert_Choice.inv f o f = id" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

878 
by (simp add: bij_def surj_iff inj_iff) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

879 
show "EX g. f o g = id & g o f = id" by rule (rule inv) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

880 
qed 
22657  881 
qed 
882 

23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

883 
thm Dmonoid.unit_def Dfun.unit_def 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

884 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

885 
thm Dmonoid.inv_inj_on_unit Dfun.inv_inj_on_unit 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

886 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

887 
lemma unit_id: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

888 
"(f :: unit => unit) = id" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

889 
by rule simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

890 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

891 
interpretation Dfun: Dgrp ["op o" "id :: unit => unit"] 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

892 
where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

893 
proof  
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

894 
have "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

895 
note Dmonoid = this 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

896 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

897 
show "Dgrp (op o) (id :: unit => unit)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

898 
apply unfold_locales 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

899 
apply (unfold Dmonoid.unit_def [OF Dmonoid]) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

900 
apply (insert unit_id) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

901 
apply simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

902 
done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

903 
show "Dmonoid.inv (op o) id f = inv (f :: unit => unit)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

904 
apply (unfold Dmonoid.inv_def [OF Dmonoid] inv_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

905 
apply (insert unit_id) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

906 
apply simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

907 
apply (rule the_equality) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

908 
apply rule 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

909 
apply rule 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

910 
apply simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

911 
done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

912 
qed 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

913 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

914 
thm Dfun.unit_l_inv Dfun.l_inv 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

915 

af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

916 
thm Dfun.inv_equality 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

917 
thm Dfun.inv_equality 
22657  918 

919 
end 