-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathShweta_FreeGroup.thy
183 lines (172 loc) · 5.15 KB
/
Shweta_FreeGroup.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
theory Shweta_FreeGroup
imports Main "HOL-Library.FuncSet" "HOL-Algebra.Group"
begin
(*From Generators.thy*)
datatype ('a,'b) monoidgentype = C 'a 'b (infix "!" 63)
datatype ('a,'b) groupgentype = P "('a,'b) monoidgentype"
| N "('a,'b) monoidgentype"
type_synonym ('a,'b) word = "(('a,'b) groupgentype) list"
primrec inverse::"('a,'b) groupgentype \<Rightarrow> ('a,'b) groupgentype"
where
"inverse (P x) = (N x)"
|"inverse (N x) = (P x)"
fun reduction:: "('a,'b) word \<Rightarrow> ('a,'b) word"
where
"reduction [] = []"
|"reduction [x] = [x]"
|"reduction (g1#g2#wrd) = (if (g1 = inverse g2)
then reduction wrd
else (g1#(reduction (g2#wrd))))"
fun reduced::"('a,'b) word \<Rightarrow> bool"
where
"reduced [] = True"
|"reduced [g] = True"
|"reduced (g#h#wrd) = (if (g \<noteq> inverse h) then reduced (h#wrd) else False)"
primrec iter::"nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
where
"iter 0 f = (\<lambda> x. x)"
|"iter (Suc n) f = (\<lambda> x. f ((iter n f) x))"
lemma length_reduction : "length (reduction wrd) \<le> length wrd"
proof(induction wrd rule: reduction.induct)
case 1
then show ?case by simp
next
case (2 x)
then show ?case by simp
next
case (3 g1 g2 wrd)
then show ?case
proof(cases "g1 = inverse g2")
case True
then show ?thesis using 3 by force
next
case False
then show ?thesis using 3
by auto
qed
qed
lemma decreasing_length:
assumes "reduction wrd \<noteq> wrd"
shows "length (reduction wrd) < length wrd"
using assms
proof(induction wrd rule: reduction.induct)
case 1
then show ?case by simp
next
case (2 x)
then show ?case by simp
next
case (3 g1 g2 wrd)
then show ?case
proof(cases "g1 = inverse g2")
case True
then have red_inv:"reduction (g1#g2#wrd) = reduction wrd" by auto
then show ?thesis
proof(cases "reduction wrd = wrd")
case True
then have "reduction (g1#g2#wrd) = wrd" using red_inv by auto
then have "length (reduction (g1#g2#wrd)) = length wrd" by auto
then show ?thesis
by simp
next
case False
then have "length (reduction wrd) < length wrd" using 3 True by argo
then show ?thesis using red_inv by force
qed
next
case False
have prem:"reduction (g1#g2#wrd) \<noteq> (g1#g2#wrd)" using 3 by argo
then have "reduction (g1#g2#wrd) = g1#reduction (g2#wrd)" using False by auto
then have "reduction (g2#wrd) \<noteq> g2#wrd" using prem by fastforce
then have "length (g2#wrd) > length (reduction (g2#wrd))" using 3 False by blast
then have "length (g1#g2#wrd) > length (reduction (g1#g2#wrd))" using False by force
then show ?thesis by fast
qed
qed
(*Prove 1. length (reduction (wrd)) = length wrd \<Rightarrow> reduction wrd = wrd*)
lemma assumes "length (reduction (wrd)) = length wrd"
shows "reduction wrd = wrd"
using assms
proof(induction wrd rule: reduction.induct)
case 1
then show ?case
by simp
next
case (2 x)
then show ?case by simp
next
case (3 g1 g2 wrd)
then show ?case
proof(cases "g1 = inverse g2")
case True
then have 1: "reduction (g1#g2#wrd) = reduction (wrd)" by simp
then have "length (reduction (g1#g2#wrd)) = length (reduction (wrd))"
by auto
moreover have "length (wrd) > length (reduction wrd)" using 1
by (metis "3.prems" decreasing_length impossible_Cons nat_le_linear) (*"m \<le> n \<or> n \<le> m", "length xs \<le> length ys \<Longrightarrow> xs = x # ys = False"*)
then show ?thesis using 3 by auto
next
case False
then show ?thesis
using decreasing_length by blast
qed
qed
(*2.reduction wrd = wrd \<Rightarrow> reduced wrd*)
lemma assumes "reduction wrd = wrd"
shows "reduced wrd"
using assms
proof(induction wrd rule:reduction.induct)
case 1
then show ?case by simp
next
case (2 x)
then show ?case by simp
next
case (3 g1 g2 wrd)
then show ?case
proof(cases "g1 \<noteq> inverse g2")
case True
then show ?thesis using 3 by force
next
case False
have "g1 = inverse g2"using False by auto
then have "(g1#g2#wrd) = reduction wrd" using 3
by simp
moreover then have "length (reduction(wrd)) \<le> length wrd"
by (simp add: length_reduction)
moreover then have "length (g1#g2#wrd) > length wrd"
by simp
ultimately show ?thesis by simp
qed
qed
(*3. lemma assumes length wrd = n shows iter (n+k) reduction = iter n reduction*)
lemma assumes "length wrd = n"
shows " iter (n+k) reduction = iter n reduction"
(*if xs@ys is reduced then xs is reduced*)
lemma assumes "reduced (xs@ys)"
shows "reduced xs"
using assms
proof (induction xs rule : reduction.induct)
case 1
then show ?case try
by simp
next
case (2 x)
then show ?case try
by simp
next
case (3 g1 g2 wrd)
then show ?case
proof (cases "g1 = inverse g2")
case True
then show ?thesis
using "3.prems" by force
next
case False
have "reduced ((g2 # wrd) @ ys)"
by (metis "3.prems" append_Cons reduced.simps(3))
then have "reduced (g2#wrd)"
using "3.IH"(2) False by auto
then show ?thesis by (simp add: False)
qed
qed