author  haftmann 
Wed, 21 Jan 2009 18:37:44 +0100  
changeset 29586  4f9803829625 
parent 29233  ce6d35a0bed6 
child 30729  461ee3e49ad3 
permissions  rwrr 
22657  1 
(* Title: HOL/ex/LocaleTest2.thy 
2 
Author: Clemens Ballarin 

3 
Copyright (c) 2007 by Clemens Ballarin 

4 

5 
More regression tests for locales. 

6 
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

7 
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

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

11 
header {* Test of Locale Interpretation *} 

12 

13 
theory LocaleTest2 

25592  14 
imports Main GCD 
22657  15 
begin 
16 

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

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

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

20 

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

21 

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

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

23 

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

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

25 

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 
subsubsection {* Definitions *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

28 

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

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

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

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

32 
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

33 
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

34 

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

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

36 

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

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

38 
"[ 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

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

40 

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

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

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

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

44 

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

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

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

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

48 

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

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

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

51 
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

52 

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

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

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

55 
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

56 

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

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

58 

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

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

60 
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

61 
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

62 

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

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

64 

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

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

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

67 
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

68 

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

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

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

71 
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

72 

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

73 
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

74 
(\<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

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

76 

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

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

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

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

80 

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

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

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

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

84 

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

85 
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

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

87 
assume inf: "is_inf x y i" 
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 
show ?thesis 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

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

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

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

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

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

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

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

100 
qed 
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 

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

104 
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

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

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

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

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

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

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

111 
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

112 
qed 
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 

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

115 
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

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

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

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

119 
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

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

121 

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

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

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

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

125 

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

126 
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

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

128 
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

129 
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

130 
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

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

132 

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

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

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

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

136 

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

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

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

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

140 

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

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

142 
"[ 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

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

144 

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

145 
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

146 
(\<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

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

148 

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

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

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

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

152 

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

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

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

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

156 

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

157 
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

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

159 
assume sup: "is_sup x y s" 
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 
show ?thesis 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

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

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

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

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

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

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

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

172 
qed 
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 

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

176 
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

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

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

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

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

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

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

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

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

185 
qed 
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 

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

188 
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

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

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

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

192 
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

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

194 

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

195 
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

196 
(\<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

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

198 

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

199 
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

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

201 
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

202 
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

203 
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

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

205 

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

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

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

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

209 

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

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

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

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

213 

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

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

215 
"[ 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

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

217 

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

218 
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

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

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

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

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

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

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

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

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

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

228 
qed 
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 
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

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

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

236 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

254 
qed 
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 

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

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

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

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

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

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

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

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

265 

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

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

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

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

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

270 
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

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

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

273 

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

274 
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

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

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

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

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

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

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

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

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

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

284 
qed 
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 
show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

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

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

292 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

310 
qed 
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 

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

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

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

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

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

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

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

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

321 

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

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

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

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

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

326 
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

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

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

329 

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

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

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

332 
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

333 
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

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

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

336 

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

337 
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

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

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

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

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

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

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

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

345 

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

346 
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

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

348 

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

349 
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

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

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

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

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

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

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

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

357 

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

358 
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

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

360 

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 
text {* Additional theorems *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

363 

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

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

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

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

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

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

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

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

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

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

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

374 

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

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

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

377 

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

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

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

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

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

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

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

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

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

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

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

388 

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

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

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

391 

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 
text {* Naming according to Jacobson I, p.\ 459. *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

394 

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

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

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

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

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

399 

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

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

401 

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

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

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

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

405 
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

406 

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

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

408 

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

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

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

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

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

413 
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

414 
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

415 
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

416 
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

417 
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

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

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

420 

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

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

422 

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

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

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

425 

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

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

427 

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

428 
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

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

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

431 

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

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

433 

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

434 

29223  435 
sublocale dlo < dlat 
28823  436 
proof 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

438 
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

439 
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

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

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

442 
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

443 
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

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

445 

29223  446 
sublocale dlo < ddlat 
28823  447 
proof 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

449 
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

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

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

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

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

454 
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

455 
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

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

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

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

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

460 
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

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

462 
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

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

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

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

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

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

468 

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

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

470 

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

472 
where "(dpo.less (op <=) (x::int) y) = (x < y)" 
24946
a7bcad413799
proper latex antiquotations instead of adhoc escapes;
wenzelm
parents:
23951
diff
changeset

473 
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *} 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

475 
show "dpo (op <= :: [int, int] => bool)" 
28823  476 
proof qed auto 
29226  477 
then interpret int: dpo "op <= :: [int, int] => bool" . 
24946
a7bcad413799
proper latex antiquotations instead of adhoc escapes;
wenzelm
parents:
23951
diff
changeset

478 
txt {* Gives interpreted version of @{text less_def} (without condition). *} 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

482 

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

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

484 
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

485 
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

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

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

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

489 

29233  490 
interpretation int!: dlat "op <= :: [int, int] => bool" 
25284  491 
where meet_eq: "dlat.meet (op <=) (x::int) y = min x y" 
492 
and join_eq: "dlat.join (op <=) (x::int) y = max x y" 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

513 

29233  514 
interpretation int!: dlo "op <= :: [int, int] => bool" 
28823  515 
proof qed arith 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

516 

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

517 
text {* Interpreted theorems from the locales, involving defined terms. *} 
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 
thm int.less_def text {* from dpo *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

523 

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

524 

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

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

526 

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

528 
where "dpo.less (op <=) (x::nat) y = (x < y)" 
24946
a7bcad413799
proper latex antiquotations instead of adhoc escapes;
wenzelm
parents:
23951
diff
changeset

529 
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *} 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

531 
show "dpo (op <= :: [nat, nat] => bool)" 
28823  532 
proof qed auto 
29226  533 
then interpret nat: dpo "op <= :: [nat, nat] => bool" . 
24946
a7bcad413799
proper latex antiquotations instead of adhoc escapes;
wenzelm
parents:
23951
diff
changeset

534 
txt {* Gives interpreted version of @{text less_def} (without condition). *} 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

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

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

540 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

564 

29233  565 
interpretation nat!: dlo "op <= :: [nat, nat] => bool" 
28823  566 
proof qed arith 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

567 

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

568 
text {* Interpreted theorems from the locales, involving defined terms. *} 
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 
thm nat.less_def text {* from dpo *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

574 

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

575 

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

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

577 

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

579 
where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)" 
24946
a7bcad413799
proper latex antiquotations instead of adhoc escapes;
wenzelm
parents:
23951
diff
changeset

580 
txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *} 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

582 
show "dpo (op dvd :: [nat, nat] => bool)" 
28823  583 
proof qed (auto simp: dvd_def) 
29226  584 
then interpret nat_dvd: dpo "op dvd :: [nat, nat] => bool" . 
24946
a7bcad413799
proper latex antiquotations instead of adhoc escapes;
wenzelm
parents:
23951
diff
changeset

585 
txt {* Gives interpreted version of @{text less_def} (without condition). *} 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

586 
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

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

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

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

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

591 

29233  592 
interpretation nat_dvd!: dlat "op dvd :: [nat, nat] => bool" 
27556  593 
where "dlat.meet (op dvd) (x::nat) y = gcd x y" 
594 
and "dlat.join (op dvd) (x::nat) y = lcm x y" 

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

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

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

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

598 
apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def) 
27556  599 
apply (rule_tac x = "gcd x y" in exI) 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

600 
apply auto [1] 
27556  601 
apply (rule_tac x = "lcm x y" in exI) 
23951  602 
apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

606 
conditional in general but unconditional after interpretation. *} 
27556  607 
show "dlat.meet (op dvd) (x::nat) y = gcd x y" 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

611 
by auto 
27556  612 
show "dlat.join (op dvd) (x::nat) y = lcm x y" 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

615 
apply (unfold nat_dvd.is_sup_def) 
23951  616 
by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

618 

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

619 
text {* Interpreted theorems from the locales, involving defined terms. *} 
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 
thm nat_dvd.less_def text {* from dpo *} 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

622 
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

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

624 
thm nat_dvd.meet_left text {* from dlat *} 
27556  625 
lemma "gcd x y dvd x" 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

627 

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

628 

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

629 
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

630 

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

631 
subsubsection {* Locale declarations and lemmas *} 
22657  632 

633 
locale Dsemi = 

634 
fixes prod (infixl "**" 65) 

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

636 

637 
locale Dmonoid = Dsemi + 

638 
fixes one 

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

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

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

641 

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

642 
begin 
22657  643 

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

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

645 
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

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

647 
unit where "unit x = (EX y. x ** y = one & y ** x = one)" 
22657  648 

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

649 
lemma inv_unique: 
22657  650 
assumes eq: "y ** x = one" "x ** y' = one" 
651 
shows "y = y'" 

652 
proof  

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

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

655 
also from eq have "... = y'" by (simp add: l_one) 
22657  656 
finally show ?thesis . 
657 
qed 

658 

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

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

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

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

662 

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

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

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

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

666 

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

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

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

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

670 

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

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

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

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

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

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

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

677 
done 
22657  678 

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

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

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

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

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

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

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

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

686 

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

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

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

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

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

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

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

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

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

695 

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

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

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

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

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

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

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

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

703 
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

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

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

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

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

708 
qed 
22657  709 

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

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

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

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

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

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

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

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

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

718 

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

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

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

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

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

723 
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

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

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

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

727 

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

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

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

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

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

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

733 
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

734 
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

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

736 

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

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

738 

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

739 

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

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

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

742 

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

743 
begin 
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 
lemma l_inv_ex [simp]: 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

748 

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

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

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

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

752 

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

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

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

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

756 

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

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

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

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

760 

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

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

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

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

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

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

767 
qed 
22657  768 

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

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

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

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

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

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

775 
then show "y = z" by simp 
22657  776 
qed simp 
777 

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

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

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

781 
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

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

783 
finally show ?thesis . 
22657  784 
qed 
785 

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

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

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

788 
using unit_inv_inv by simp 
22657  789 

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

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

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

792 
using inv_inj_on_unit by simp 
22657  793 

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

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

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

797 
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

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

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

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

801 

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

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

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

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

805 

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

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

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

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

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

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

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

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

813 

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

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

815 

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

816 

29226  817 
locale Dhom = prod: Dgrp prod one + sum: Dgrp sum zero 
818 
for prod (infixl "**" 65) and one and sum (infixl "+++" 60) and zero + 

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

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

820 
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

821 

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

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

823 

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

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

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

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

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

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

829 
then show ?thesis by (simp del: r_one) 
22657  830 
qed 
831 

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

832 
end 
22657  833 

834 

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

835 
subsubsection {* Interpretation of Functions *} 
22657  836 

29233  837 
interpretation Dfun!: Dmonoid "op o" "id :: 'a => 'a" 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

838 
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

839 
(* and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *) 
22657  840 
proof  
28823  841 
show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc) 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

842 
note Dmonoid = this 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

843 
(* 
29226  844 
from this interpret Dmonoid "op o" "id :: 'a => 'a" . 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

846 
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

847 
apply (unfold Dmonoid.unit_def [OF Dmonoid]) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

851 
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

852 
show "bij f" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

854 
show "inj f" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

857 
assume "f x = f y" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

858 
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

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

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

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

862 
show "surj f" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

865 
from id1 have "(f o g) x = x" by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

866 
then show "f (g x) = x" by simp 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

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

871 
assume bij: "bij f" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

873 
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

874 
by (simp add: bij_def surj_iff inj_iff) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

875 
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

876 
qed 
22657  877 
qed 
878 

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

879 
thm Dmonoid.unit_def Dfun.unit_def 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

880 

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

881 
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

882 

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

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

884 
"(f :: unit => unit) = id" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

886 

29233  887 
interpretation Dfun!: Dgrp "op o" "id :: unit => unit" 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

888 
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

889 
proof  
28823  890 
have "Dmonoid op o (id :: 'a => 'a)" .. 
23919
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

891 
note Dmonoid = this 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

892 

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

893 
show "Dgrp (op o) (id :: unit => unit)" 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

895 
apply (unfold Dmonoid.unit_def [OF Dmonoid]) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

896 
apply (insert unit_id) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

899 
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

900 
apply (unfold Dmonoid.inv_def [OF Dmonoid] inv_def) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

901 
apply (insert unit_id) 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

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

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

905 
apply rule 
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 
done 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

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

909 

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

910 
thm Dfun.unit_l_inv Dfun.l_inv 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

911 

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

912 
thm Dfun.inv_equality 
af871d13e320
interpretation: equations are propositions not pairs of terms;
ballarin
parents:
23219
diff
changeset

913 
thm Dfun.inv_equality 
22657  914 

915 
end 