-
Notifications
You must be signed in to change notification settings - Fork 0
/
Embedded_Algebras.thy
1775 lines (1580 loc) · 78.1 KB
/
Embedded_Algebras.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
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* Title: HOL/Algebra/Embedded_Algebras.thy
Author: Paulo Emílio de Vilhena
*)
theory Embedded_Algebras
imports Subrings Generated_Groups
begin
section \<open>Definitions\<close>
locale embedded_algebra =
K?: subfield K R + R?: ring R for K :: "'a set" and R :: "('a, 'b) ring_scheme" (structure)
definition (in ring) line_extension :: "'a set \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
where "line_extension K a E = (K #> a) <+>\<^bsub>R\<^esub> E"
fun (in ring) Span :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a set"
where "Span K Us = foldr (line_extension K) Us { \<zero> }"
fun (in ring) combine :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a"
where
"combine (k # Ks) (u # Us) = (k \<otimes> u) \<oplus> (combine Ks Us)"
| "combine Ks Us = \<zero>"
inductive (in ring) independent :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool"
where
li_Nil [simp, intro]: "independent K []"
| li_Cons: "\<lbrakk> u \<in> carrier R; u \<notin> Span K Us; independent K Us \<rbrakk> \<Longrightarrow> independent K (u # Us)"
inductive (in ring) dimension :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
where
zero_dim [simp, intro]: "dimension 0 K { \<zero> }"
| Suc_dim: "\<lbrakk> v \<in> carrier R; v \<notin> E; dimension n K E \<rbrakk> \<Longrightarrow> dimension (Suc n) K (line_extension K v E)"
subsubsection \<open>Syntactic Definitions\<close>
abbreviation (in ring) dependent :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool"
where "dependent K U \<equiv> \<not> independent K U"
definition over :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" (infixl "over" 65)
where "f over a = f a"
context ring
begin
subsection \<open>Basic Properties - First Part\<close>
lemma line_extension_consistent:
assumes "subring K R" shows "ring.line_extension (R \<lparr> carrier := K \<rparr>) = line_extension"
unfolding ring.line_extension_def[OF subring_is_ring[OF assms]] line_extension_def
by (simp add: set_add_def set_mult_def)
lemma Span_consistent:
assumes "subring K R" shows "ring.Span (R \<lparr> carrier := K \<rparr>) = Span"
unfolding ring.Span.simps[OF subring_is_ring[OF assms]] Span.simps
line_extension_consistent[OF assms] by simp
lemma combine_in_carrier [simp, intro]:
"\<lbrakk> set Ks \<subseteq> carrier R; set Us \<subseteq> carrier R \<rbrakk> \<Longrightarrow> combine Ks Us \<in> carrier R"
by (induct Ks Us rule: combine.induct) (auto)
lemma combine_r_distr:
"\<lbrakk> set Ks \<subseteq> carrier R; set Us \<subseteq> carrier R \<rbrakk> \<Longrightarrow>
k \<in> carrier R \<Longrightarrow> k \<otimes> (combine Ks Us) = combine (map ((\<otimes>) k) Ks) Us"
by (induct Ks Us rule: combine.induct) (auto simp add: m_assoc r_distr)
lemma combine_l_distr:
"\<lbrakk> set Ks \<subseteq> carrier R; set Us \<subseteq> carrier R \<rbrakk> \<Longrightarrow>
u \<in> carrier R \<Longrightarrow> (combine Ks Us) \<otimes> u = combine Ks (map (\<lambda>u'. u' \<otimes> u) Us)"
by (induct Ks Us rule: combine.induct) (auto simp add: m_assoc l_distr)
lemma combine_eq_foldr:
"combine Ks Us = foldr (\<lambda>(k, u). \<lambda>l. (k \<otimes> u) \<oplus> l) (zip Ks Us) \<zero>"
by (induct Ks Us rule: combine.induct) (auto)
lemma combine_replicate:
"set Us \<subseteq> carrier R \<Longrightarrow> combine (replicate (length Us) \<zero>) Us = \<zero>"
by (induct Us) (auto)
lemma combine_take:
"combine (take (length Us) Ks) Us = combine Ks Us"
by (induct Us arbitrary: Ks)
(auto, metis combine.simps(1) list.exhaust take.simps(1) take_Suc_Cons)
lemma combine_append_zero:
"set Us \<subseteq> carrier R \<Longrightarrow> combine (Ks @ [ \<zero> ]) Us = combine Ks Us"
proof (induct Ks arbitrary: Us)
case Nil thus ?case by (induct Us) (auto)
next
case Cons thus ?case by (cases Us) (auto)
qed
lemma combine_prepend_replicate:
"\<lbrakk> set Ks \<subseteq> carrier R; set Us \<subseteq> carrier R \<rbrakk> \<Longrightarrow>
combine ((replicate n \<zero>) @ Ks) Us = combine Ks (drop n Us)"
proof (induct n arbitrary: Us, simp)
case (Suc n) thus ?case
by (cases Us) (auto, meson combine_in_carrier ring_simprules(8) set_drop_subset subset_trans)
qed
lemma combine_append_replicate:
"set Us \<subseteq> carrier R \<Longrightarrow> combine (Ks @ (replicate n \<zero>)) Us = combine Ks Us"
by (induct n) (auto, metis append.assoc combine_append_zero replicate_append_same)
lemma combine_append:
assumes "length Ks = length Us"
and "set Ks \<subseteq> carrier R" "set Us \<subseteq> carrier R"
and "set Ks' \<subseteq> carrier R" "set Vs \<subseteq> carrier R"
shows "(combine Ks Us) \<oplus> (combine Ks' Vs) = combine (Ks @ Ks') (Us @ Vs)"
using assms
proof (induct Ks arbitrary: Us)
case Nil thus ?case by auto
next
case (Cons k Ks)
then obtain u Us' where Us: "Us = u # Us'"
by (metis length_Suc_conv)
hence u: "u \<in> carrier R" and Us': "set Us' \<subseteq> carrier R"
using Cons(4) by auto
then show ?case
using combine_in_carrier[OF _ Us', of Ks] Cons
combine_in_carrier[OF Cons(5-6)] unfolding Us
by (auto, simp add: add.m_assoc)
qed
lemma combine_add:
assumes "length Ks = length Us" and "length Ks' = length Us"
and "set Ks \<subseteq> carrier R" "set Ks' \<subseteq> carrier R" "set Us \<subseteq> carrier R"
shows "(combine Ks Us) \<oplus> (combine Ks' Us) = combine (map2 (\<oplus>) Ks Ks') Us"
using assms
proof (induct Us arbitrary: Ks Ks')
case Nil thus ?case by simp
next
case (Cons u Us)
then obtain c c' Cs Cs' where Ks: "Ks = c # Cs" and Ks': "Ks' = c' # Cs'"
by (metis length_Suc_conv)
hence in_carrier:
"c \<in> carrier R" "set Cs \<subseteq> carrier R"
"c' \<in> carrier R" "set Cs' \<subseteq> carrier R"
"u \<in> carrier R" "set Us \<subseteq> carrier R"
using Cons(4-6) by auto
hence lc_in_carrier: "combine Cs Us \<in> carrier R" "combine Cs' Us \<in> carrier R"
using combine_in_carrier by auto
have "combine Ks (u # Us) \<oplus> combine Ks' (u # Us) =
((c \<otimes> u) \<oplus> combine Cs Us) \<oplus> ((c' \<otimes> u) \<oplus> combine Cs' Us)"
unfolding Ks Ks' by auto
also have " ... = ((c \<oplus> c') \<otimes> u \<oplus> (combine Cs Us \<oplus> combine Cs' Us))"
using lc_in_carrier in_carrier(1,3,5) by (simp add: l_distr ring_simprules(7,22))
also have " ... = combine (map2 (\<oplus>) Ks Ks') (u # Us)"
using Cons unfolding Ks Ks' by auto
finally show ?case .
qed
lemma combine_normalize:
assumes "set Ks \<subseteq> carrier R" "set Us \<subseteq> carrier R" "combine Ks Us = a"
obtains Ks'
where "set (take (length Us) Ks) \<subseteq> set Ks'" "set Ks' \<subseteq> set (take (length Us) Ks) \<union> { \<zero> }"
and "length Ks' = length Us" "combine Ks' Us = a"
proof -
define Ks'
where "Ks' = (if length Ks \<le> length Us
then Ks @ (replicate (length Us - length Ks) \<zero>) else take (length Us) Ks)"
hence "set (take (length Us) Ks) \<subseteq> set Ks'" "set Ks' \<subseteq> set (take (length Us) Ks) \<union> { \<zero> }"
"length Ks' = length Us" "a = combine Ks' Us"
using combine_append_replicate[OF assms(2)] combine_take assms(3) by auto
thus thesis
using that by blast
qed
lemma line_extension_mem_iff: "u \<in> line_extension K a E \<longleftrightarrow> (\<exists>k \<in> K. \<exists>v \<in> E. u = k \<otimes> a \<oplus> v)"
unfolding line_extension_def set_add_def'[of R "K #> a" E] unfolding r_coset_def by blast
lemma line_extension_in_carrier:
assumes "K \<subseteq> carrier R" "a \<in> carrier R" "E \<subseteq> carrier R"
shows "line_extension K a E \<subseteq> carrier R"
using set_add_closed[OF r_coset_subset_G[OF assms(1-2)] assms(3)]
by (simp add: line_extension_def)
lemma Span_in_carrier:
assumes "K \<subseteq> carrier R" "set Us \<subseteq> carrier R"
shows "Span K Us \<subseteq> carrier R"
using assms by (induct Us) (auto simp add: line_extension_in_carrier)
subsection \<open>Some Basic Properties of Linear Independence\<close>
lemma independent_in_carrier: "independent K Us \<Longrightarrow> set Us \<subseteq> carrier R"
by (induct Us rule: independent.induct) (simp_all)
lemma independent_backwards:
"independent K (u # Us) \<Longrightarrow> u \<notin> Span K Us"
"independent K (u # Us) \<Longrightarrow> independent K Us"
"independent K (u # Us) \<Longrightarrow> u \<in> carrier R"
by (cases rule: independent.cases, auto)+
lemma dimension_independent [intro]: "independent K Us \<Longrightarrow> dimension (length Us) K (Span K Us)"
proof (induct Us)
case Nil thus ?case by simp
next
case Cons thus ?case
using Suc_dim independent_backwards[OF Cons(2)] by auto
qed
text \<open>Now, we fix K, a subfield of the ring. Many lemmas would also be true for weaker
structures, but our interest is to work with subfields, so generalization could
be the subject of a future work.\<close>
context
fixes K :: "'a set" assumes K: "subfield K R"
begin
subsection \<open>Basic Properties - Second Part\<close>
lemmas subring_props [simp] =
subringE[OF subfieldE(1)[OF K]]
lemma line_extension_is_subgroup:
assumes "subgroup E (add_monoid R)" "a \<in> carrier R"
shows "subgroup (line_extension K a E) (add_monoid R)"
proof (rule add.subgroupI)
show "line_extension K a E \<subseteq> carrier R"
by (simp add: assms add.subgroupE(1) line_extension_def r_coset_subset_G set_add_closed)
next
have "\<zero> = \<zero> \<otimes> a \<oplus> \<zero>"
using assms(2) by simp
hence "\<zero> \<in> line_extension K a E"
using line_extension_mem_iff subgroup.one_closed[OF assms(1)] by auto
thus "line_extension K a E \<noteq> {}" by auto
next
fix u1 u2
assume "u1 \<in> line_extension K a E" and "u2 \<in> line_extension K a E"
then obtain k1 k2 v1 v2
where u1: "k1 \<in> K" "v1 \<in> E" "u1 = (k1 \<otimes> a) \<oplus> v1"
and u2: "k2 \<in> K" "v2 \<in> E" "u2 = (k2 \<otimes> a) \<oplus> v2"
and in_carr: "k1 \<in> carrier R" "v1 \<in> carrier R" "k2 \<in> carrier R" "v2 \<in> carrier R"
using line_extension_mem_iff by (meson add.subgroupE(1)[OF assms(1)] subring_props(1) subsetCE)
hence "u1 \<oplus> u2 = ((k1 \<oplus> k2) \<otimes> a) \<oplus> (v1 \<oplus> v2)"
using assms(2) by algebra
moreover have "k1 \<oplus> k2 \<in> K" and "v1 \<oplus> v2 \<in> E"
using add.subgroupE(4)[OF assms(1)] u1 u2 by auto
ultimately show "u1 \<oplus> u2 \<in> line_extension K a E"
using line_extension_mem_iff by auto
have "\<ominus> u1 = ((\<ominus> k1) \<otimes> a) \<oplus> (\<ominus> v1)"
using in_carr(1-2) u1(3) assms(2) by algebra
moreover have "\<ominus> k1 \<in> K" and "\<ominus> v1 \<in> E"
using add.subgroupE(3)[OF assms(1)] u1 by auto
ultimately show "(\<ominus> u1) \<in> line_extension K a E"
using line_extension_mem_iff by auto
qed
corollary Span_is_add_subgroup:
"set Us \<subseteq> carrier R \<Longrightarrow> subgroup (Span K Us) (add_monoid R)"
using line_extension_is_subgroup add.normal_invE(1)[OF add.one_is_normal] by (induct Us) (auto)
lemma line_extension_smult_closed:
assumes "\<And>k v. \<lbrakk> k \<in> K; v \<in> E \<rbrakk> \<Longrightarrow> k \<otimes> v \<in> E" and "E \<subseteq> carrier R" "a \<in> carrier R"
shows "\<And>k u. \<lbrakk> k \<in> K; u \<in> line_extension K a E \<rbrakk> \<Longrightarrow> k \<otimes> u \<in> line_extension K a E"
proof -
fix k u assume A: "k \<in> K" "u \<in> line_extension K a E"
then obtain k' v'
where u: "k' \<in> K" "v' \<in> E" "u = k' \<otimes> a \<oplus> v'"
and in_carr: "k \<in> carrier R" "k' \<in> carrier R" "v' \<in> carrier R"
using line_extension_mem_iff assms(2) by (meson subring_props(1) subsetCE)
hence "k \<otimes> u = (k \<otimes> k') \<otimes> a \<oplus> (k \<otimes> v')"
using assms(3) by algebra
thus "k \<otimes> u \<in> line_extension K a E"
using assms(1)[OF A(1) u(2)] line_extension_mem_iff u(1) A(1) by auto
qed
lemma Span_subgroup_props [simp]:
assumes "set Us \<subseteq> carrier R"
shows "Span K Us \<subseteq> carrier R"
and "\<zero> \<in> Span K Us"
and "\<And>v1 v2. \<lbrakk> v1 \<in> Span K Us; v2 \<in> Span K Us \<rbrakk> \<Longrightarrow> (v1 \<oplus> v2) \<in> Span K Us"
and "\<And>v. v \<in> Span K Us \<Longrightarrow> (\<ominus> v) \<in> Span K Us"
using add.subgroupE subgroup.one_closed[of _ "add_monoid R"]
Span_is_add_subgroup[OF assms(1)] by auto
lemma Span_smult_closed [simp]:
assumes "set Us \<subseteq> carrier R"
shows "\<And>k v. \<lbrakk> k \<in> K; v \<in> Span K Us \<rbrakk> \<Longrightarrow> k \<otimes> v \<in> Span K Us"
using assms
proof (induct Us)
case Nil thus ?case
using r_null subring_props(1) by (auto, blast)
next
case Cons thus ?case
using Span_subgroup_props(1) line_extension_smult_closed by auto
qed
lemma Span_m_inv_simprule [simp]:
assumes "set Us \<subseteq> carrier R"
shows "\<lbrakk> k \<in> K - { \<zero> }; a \<in> carrier R \<rbrakk> \<Longrightarrow> k \<otimes> a \<in> Span K Us \<Longrightarrow> a \<in> Span K Us"
proof -
assume k: "k \<in> K - { \<zero> }" and a: "a \<in> carrier R" and ka: "k \<otimes> a \<in> Span K Us"
have inv_k: "inv k \<in> K" "inv k \<otimes> k = \<one>"
using subfield_m_inv[OF K k] by simp+
hence "inv k \<otimes> (k \<otimes> a) \<in> Span K Us"
using Span_smult_closed[OF assms _ ka] by simp
thus ?thesis
using inv_k subring_props(1)a k by (smt DiffD1 l_one m_assoc set_rev_mp)
qed
subsection \<open>Span as Linear Combinations\<close>
text \<open>We show that Span is the set of linear combinations\<close>
lemma line_extension_of_combine_set:
assumes "u \<in> carrier R"
shows "line_extension K u { combine Ks Us | Ks. set Ks \<subseteq> K } =
{ combine Ks (u # Us) | Ks. set Ks \<subseteq> K }"
(is "?line_extension = ?combinations")
proof
show "?line_extension \<subseteq> ?combinations"
proof
fix v assume "v \<in> ?line_extension"
then obtain k Ks
where "k \<in> K" "set Ks \<subseteq> K" and "v = combine (k # Ks) (u # Us)"
using line_extension_mem_iff by auto
thus "v \<in> ?combinations"
by (metis (mono_tags, lifting) insert_subset list.simps(15) mem_Collect_eq)
qed
next
show "?combinations \<subseteq> ?line_extension"
proof
fix v assume "v \<in> ?combinations"
then obtain Ks where v: "set Ks \<subseteq> K" "v = combine Ks (u # Us)"
by auto
thus "v \<in> ?line_extension"
proof (cases Ks)
case Cons thus ?thesis
using v line_extension_mem_iff by auto
next
case Nil
hence "v = \<zero>"
using v by simp
moreover have "combine [] Us = \<zero>" by simp
hence "\<zero> \<in> { combine Ks Us | Ks. set Ks \<subseteq> K }"
by (metis (mono_tags, lifting) local.Nil mem_Collect_eq v(1))
hence "(\<zero> \<otimes> u) \<oplus> \<zero> \<in> ?line_extension"
using line_extension_mem_iff subring_props(2) by blast
hence "\<zero> \<in> ?line_extension"
using assms by auto
ultimately show ?thesis by auto
qed
qed
qed
lemma Span_eq_combine_set:
assumes "set Us \<subseteq> carrier R" shows "Span K Us = { combine Ks Us | Ks. set Ks \<subseteq> K }"
using assms line_extension_of_combine_set
by (induct Us) (auto, metis empty_set empty_subsetI)
lemma line_extension_of_combine_set_length_version:
assumes "u \<in> carrier R"
shows "line_extension K u { combine Ks Us | Ks. length Ks = length Us \<and> set Ks \<subseteq> K } =
{ combine Ks (u # Us) | Ks. length Ks = length (u # Us) \<and> set Ks \<subseteq> K }"
(is "?line_extension = ?combinations")
proof
show "?line_extension \<subseteq> ?combinations"
proof
fix v assume "v \<in> ?line_extension"
then obtain k Ks
where "v = combine (k # Ks) (u # Us)" "length (k # Ks) = length (u # Us)" "set (k # Ks) \<subseteq> K"
using line_extension_mem_iff by auto
thus "v \<in> ?combinations" by blast
qed
next
show "?combinations \<subseteq> ?line_extension"
proof
fix c assume "c \<in> ?combinations"
then obtain Ks where c: "c = combine Ks (u # Us)" "length Ks = length (u # Us)" "set Ks \<subseteq> K"
by blast
then obtain k Ks' where k: "Ks = k # Ks'"
by (metis length_Suc_conv)
thus "c \<in> ?line_extension"
using c line_extension_mem_iff unfolding k by auto
qed
qed
lemma Span_eq_combine_set_length_version:
assumes "set Us \<subseteq> carrier R"
shows "Span K Us = { combine Ks Us | Ks. length Ks = length Us \<and> set Ks \<subseteq> K }"
using assms line_extension_of_combine_set_length_version by (induct Us) (auto)
subsubsection \<open>Corollaries\<close>
corollary Span_mem_iff_length_version:
assumes "set Us \<subseteq> carrier R"
shows "a \<in> Span K Us \<longleftrightarrow> (\<exists>Ks. set Ks \<subseteq> K \<and> length Ks = length Us \<and> a = combine Ks Us)"
using Span_eq_combine_set_length_version[OF assms] by blast
corollary Span_mem_imp_non_trivial_combine:
assumes "set Us \<subseteq> carrier R" and "a \<in> Span K Us"
obtains k Ks
where "k \<in> K - { \<zero> }" "set Ks \<subseteq> K" "length Ks = length Us" "combine (k # Ks) (a # Us) = \<zero>"
proof -
obtain Ks where Ks: "set Ks \<subseteq> K" "length Ks = length Us" "a = combine Ks Us"
using Span_mem_iff_length_version[OF assms(1)] assms(2) by auto
hence "((\<ominus> \<one>) \<otimes> a) \<oplus> a = combine ((\<ominus> \<one>) # Ks) (a # Us)"
by auto
moreover have "((\<ominus> \<one>) \<otimes> a) \<oplus> a = \<zero>"
using assms(2) Span_subgroup_props(1)[OF assms(1)] l_minus l_neg by auto
moreover have "\<ominus> \<one> \<noteq> \<zero>"
using subfieldE(6)[OF K] l_neg by force
ultimately show ?thesis
using that subring_props(3,5) Ks(1-2) by (force simp del: combine.simps)
qed
corollary Span_mem_iff:
assumes "set Us \<subseteq> carrier R" and "a \<in> carrier R"
shows "a \<in> Span K Us \<longleftrightarrow> (\<exists>k \<in> K - { \<zero> }. \<exists>Ks. set Ks \<subseteq> K \<and> combine (k # Ks) (a # Us) = \<zero>)"
(is "?in_Span \<longleftrightarrow> ?exists_combine")
proof
assume "?in_Span"
then obtain Ks where Ks: "set Ks \<subseteq> K" "a = combine Ks Us"
using Span_eq_combine_set[OF assms(1)] by auto
hence "((\<ominus> \<one>) \<otimes> a) \<oplus> a = combine ((\<ominus> \<one>) # Ks) (a # Us)"
by auto
moreover have "((\<ominus> \<one>) \<otimes> a) \<oplus> a = \<zero>"
using assms(2) l_minus l_neg by auto
moreover have "\<ominus> \<one> \<noteq> \<zero>"
using subfieldE(6)[OF K] l_neg by force
ultimately show "?exists_combine"
using subring_props(3,5) Ks(1) by (force simp del: combine.simps)
next
assume "?exists_combine"
then obtain k Ks
where k: "k \<in> K" "k \<noteq> \<zero>" and Ks: "set Ks \<subseteq> K" and a: "(k \<otimes> a) \<oplus> combine Ks Us = \<zero>"
by auto
hence "combine Ks Us \<in> Span K Us"
using Span_eq_combine_set[OF assms(1)] by auto
hence "k \<otimes> a \<in> Span K Us"
using Span_subgroup_props[OF assms(1)] k Ks a
by (metis (no_types, lifting) assms(2) contra_subsetD m_closed minus_equality subring_props(1))
thus "?in_Span"
using Span_m_inv_simprule[OF assms(1) _ assms(2), of k] k by auto
qed
subsection \<open>Span as the minimal subgroup that contains @{term"K <#> (set Us)"}\<close>
text \<open>Now we show the link between Span and Group.generate\<close>
lemma mono_Span:
assumes "set Us \<subseteq> carrier R" and "u \<in> carrier R"
shows "Span K Us \<subseteq> Span K (u # Us)"
proof
fix v assume v: "v \<in> Span K Us"
hence "(\<zero> \<otimes> u) \<oplus> v \<in> Span K (u # Us)"
using line_extension_mem_iff by auto
thus "v \<in> Span K (u # Us)"
using Span_subgroup_props(1)[OF assms(1)] assms(2) v
by (auto simp del: Span.simps)
qed
lemma Span_min:
assumes "set Us \<subseteq> carrier R" and "subgroup E (add_monoid R)"
shows "K <#> (set Us) \<subseteq> E \<Longrightarrow> Span K Us \<subseteq> E"
proof -
assume "K <#> (set Us) \<subseteq> E" show "Span K Us \<subseteq> E"
proof
fix v assume "v \<in> Span K Us"
then obtain Ks where v: "set Ks \<subseteq> K" "v = combine Ks Us"
using Span_eq_combine_set[OF assms(1)] by auto
from \<open>set Ks \<subseteq> K\<close> \<open>set Us \<subseteq> carrier R\<close> and \<open>K <#> (set Us) \<subseteq> E\<close>
show "v \<in> E" unfolding v(2)
proof (induct Ks Us rule: combine.induct)
case (1 k Ks u Us)
hence "k \<in> K" and "u \<in> set (u # Us)" by auto
hence "k \<otimes> u \<in> E"
using 1(4) unfolding set_mult_def by auto
moreover have "K <#> set Us \<subseteq> E"
using 1(4) unfolding set_mult_def by auto
hence "combine Ks Us \<in> E"
using 1 by auto
ultimately show ?case
using add.subgroupE(4)[OF assms(2)] by auto
next
case "2_1" thus ?case
using subgroup.one_closed[OF assms(2)] by auto
next
case "2_2" thus ?case
using subgroup.one_closed[OF assms(2)] by auto
qed
qed
qed
lemma Span_eq_generate:
assumes "set Us \<subseteq> carrier R" shows "Span K Us = generate (add_monoid R) (K <#> (set Us))"
proof (rule add.generateI)
show "subgroup (Span K Us) (add_monoid R)"
using Span_is_add_subgroup[OF assms] .
next
show "\<And>E. \<lbrakk> subgroup E (add_monoid R); K <#> set Us \<subseteq> E \<rbrakk> \<Longrightarrow> Span K Us \<subseteq> E"
using Span_min assms by blast
next
show "K <#> set Us \<subseteq> Span K Us"
using assms
proof (induct Us)
case Nil thus ?case
unfolding set_mult_def by auto
next
case (Cons u Us)
have "K <#> set (u # Us) = (K <#> { u }) \<union> (K <#> set Us)"
unfolding set_mult_def by auto
moreover have "\<And>k. k \<in> K \<Longrightarrow> k \<otimes> u \<in> Span K (u # Us)"
proof -
fix k assume k: "k \<in> K"
hence "combine [ k ] (u # Us) \<in> Span K (u # Us)"
using Span_eq_combine_set[OF Cons(2)] by (auto simp del: combine.simps)
moreover have "k \<in> carrier R" and "u \<in> carrier R"
using Cons(2) k subring_props(1) by (blast, auto)
ultimately show "k \<otimes> u \<in> Span K (u # Us)"
by (auto simp del: Span.simps)
qed
hence "K <#> { u } \<subseteq> Span K (u # Us)"
unfolding set_mult_def by auto
moreover have "K <#> set Us \<subseteq> Span K (u # Us)"
using mono_Span[of Us u] Cons by (auto simp del: Span.simps)
ultimately show ?case
using Cons by (auto simp del: Span.simps)
qed
qed
subsubsection \<open>Corollaries\<close>
corollary Span_same_set:
assumes "set Us \<subseteq> carrier R"
shows "set Us = set Vs \<Longrightarrow> Span K Us = Span K Vs"
using Span_eq_generate assms by auto
corollary Span_incl: "set Us \<subseteq> carrier R \<Longrightarrow> K <#> (set Us) \<subseteq> Span K Us"
using Span_eq_generate generate.incl[of _ _ "add_monoid R"] by auto
corollary Span_base_incl: "set Us \<subseteq> carrier R \<Longrightarrow> set Us \<subseteq> Span K Us"
proof -
assume A: "set Us \<subseteq> carrier R"
hence "{ \<one> } <#> set Us = set Us"
unfolding set_mult_def by force
moreover have "{ \<one> } <#> set Us \<subseteq> K <#> set Us"
using subring_props(3) unfolding set_mult_def by blast
ultimately show ?thesis
using Span_incl[OF A] by auto
qed
corollary mono_Span_sublist:
assumes "set Us \<subseteq> set Vs" "set Vs \<subseteq> carrier R"
shows "Span K Us \<subseteq> Span K Vs"
using add.mono_generate[OF mono_set_mult[OF _ assms(1), of K K R]]
Span_eq_generate[OF assms(2)] Span_eq_generate[of Us] assms
by auto
corollary mono_Span_append:
assumes "set Us \<subseteq> carrier R" "set Vs \<subseteq> carrier R"
shows "Span K Us \<subseteq> Span K (Us @ Vs)"
and "Span K Us \<subseteq> Span K (Vs @ Us)"
using mono_Span_sublist[of Us "Us @ Vs"] assms
Span_same_set[of "Us @ Vs" "Vs @ Us"] by auto
corollary mono_Span_subset:
assumes "set Us \<subseteq> Span K Vs" "set Vs \<subseteq> carrier R"
shows "Span K Us \<subseteq> Span K Vs"
proof (rule Span_min[OF _ Span_is_add_subgroup[OF assms(2)]])
show "set Us \<subseteq> carrier R"
using Span_subgroup_props(1)[OF assms(2)] assms by auto
show "K <#> set Us \<subseteq> Span K Vs"
using Span_smult_closed[OF assms(2)] assms(1) unfolding set_mult_def by blast
qed
lemma Span_strict_incl:
assumes "set Us \<subseteq> carrier R" "set Vs \<subseteq> carrier R"
shows "Span K Us \<subset> Span K Vs \<Longrightarrow> (\<exists>v \<in> set Vs. v \<notin> Span K Us)"
proof -
assume "Span K Us \<subset> Span K Vs" show "\<exists>v \<in> set Vs. v \<notin> Span K Us"
proof (rule ccontr)
assume "\<not> (\<exists>v \<in> set Vs. v \<notin> Span K Us)"
hence "Span K Vs \<subseteq> Span K Us"
using mono_Span_subset[OF _ assms(1), of Vs] by auto
from \<open>Span K Us \<subset> Span K Vs\<close> and \<open>Span K Vs \<subseteq> Span K Us\<close>
show False by simp
qed
qed
lemma Span_append_eq_set_add:
assumes "set Us \<subseteq> carrier R" and "set Vs \<subseteq> carrier R"
shows "Span K (Us @ Vs) = (Span K Us <+>\<^bsub>R\<^esub> Span K Vs)"
using assms
proof (induct Us)
case Nil thus ?case
using Span_subgroup_props(1)[OF Nil(2)] unfolding set_add_def' by force
next
case (Cons u Us)
hence in_carrier:
"u \<in> carrier R" "set Us \<subseteq> carrier R" "set Vs \<subseteq> carrier R"
by auto
have "line_extension K u (Span K Us <+>\<^bsub>R\<^esub> Span K Vs) = (Span K (u # Us) <+>\<^bsub>R\<^esub> Span K Vs)"
proof
show "line_extension K u (Span K Us <+>\<^bsub>R\<^esub> Span K Vs) \<subseteq> (Span K (u # Us) <+>\<^bsub>R\<^esub> Span K Vs)"
proof
fix v assume "v \<in> line_extension K u (Span K Us <+>\<^bsub>R\<^esub> Span K Vs)"
then obtain k u' v'
where v: "k \<in> K" "u' \<in> Span K Us" "v' \<in> Span K Vs" "v = k \<otimes> u \<oplus> (u' \<oplus> v')"
using line_extension_mem_iff[of v _ u "Span K Us <+>\<^bsub>R\<^esub> Span K Vs"]
unfolding set_add_def' by blast
hence "v = (k \<otimes> u \<oplus> u') \<oplus> v'"
using in_carrier(2-3)[THEN Span_subgroup_props(1)] in_carrier(1) subring_props(1)
by (metis (no_types, lifting) rev_subsetD ring_simprules(7) semiring_simprules(3))
moreover have "k \<otimes> u \<oplus> u' \<in> Span K (u # Us)"
using line_extension_mem_iff v(1-2) by auto
ultimately show "v \<in> Span K (u # Us) <+>\<^bsub>R\<^esub> Span K Vs"
unfolding set_add_def' using v(3) by auto
qed
next
show "Span K (u # Us) <+>\<^bsub>R\<^esub> Span K Vs \<subseteq> line_extension K u (Span K Us <+>\<^bsub>R\<^esub> Span K Vs)"
proof
fix v assume "v \<in> Span K (u # Us) <+>\<^bsub>R\<^esub> Span K Vs"
then obtain k u' v'
where v: "k \<in> K" "u' \<in> Span K Us" "v' \<in> Span K Vs" "v = (k \<otimes> u \<oplus> u') \<oplus> v'"
using line_extension_mem_iff[of _ _ u "Span K Us"] unfolding set_add_def' by auto
hence "v = (k \<otimes> u) \<oplus> (u' \<oplus> v')"
using in_carrier(2-3)[THEN Span_subgroup_props(1)] in_carrier(1) subring_props(1)
by (metis (no_types, lifting) rev_subsetD ring_simprules(5,7))
thus "v \<in> line_extension K u (Span K Us <+>\<^bsub>R\<^esub> Span K Vs)"
using line_extension_mem_iff[of "(k \<otimes> u) \<oplus> (u' \<oplus> v')" K u "Span K Us <+>\<^bsub>R\<^esub> Span K Vs"]
unfolding set_add_def' using v by auto
qed
qed
thus ?case
using Cons by auto
qed
subsection \<open>Characterisation of Linearly Independent "Sets"\<close>
declare independent_backwards [intro]
declare independent_in_carrier [intro]
lemma independent_distinct: "independent K Us \<Longrightarrow> distinct Us"
proof (induct Us rule: list.induct)
case Nil thus ?case by simp
next
case Cons thus ?case
using independent_backwards[OF Cons(2)]
independent_in_carrier[OF Cons(2)]
Span_base_incl
by auto
qed
lemma independent_strict_incl:
assumes "independent K (u # Us)" shows "Span K Us \<subset> Span K (u # Us)"
proof -
have "u \<in> Span K (u # Us)"
using Span_base_incl[OF independent_in_carrier[OF assms]] by auto
moreover have "Span K Us \<subseteq> Span K (u # Us)"
using mono_Span independent_in_carrier[OF assms] by auto
ultimately show ?thesis
using independent_backwards(1)[OF assms] by auto
qed
corollary independent_replacement:
assumes "independent K (u # Us)" and "independent K Vs"
shows "Span K (u # Us) \<subseteq> Span K Vs \<Longrightarrow> (\<exists>v \<in> set Vs. independent K (v # Us))"
proof -
assume "Span K (u # Us) \<subseteq> Span K Vs"
hence "Span K Us \<subset> Span K Vs"
using independent_strict_incl[OF assms(1)] by auto
then obtain v where v: "v \<in> set Vs" "v \<notin> Span K Us"
using Span_strict_incl[of Us Vs] assms[THEN independent_in_carrier] by auto
thus ?thesis
using li_Cons[of v K Us] assms independent_in_carrier[OF assms(2)] by auto
qed
lemma independent_split:
assumes "independent K (Us @ Vs)"
shows "independent K Vs"
and "independent K Us"
and "Span K Us \<inter> Span K Vs = { \<zero> }"
proof -
from assms show "independent K Vs"
by (induct Us) (auto)
next
from assms show "independent K Us"
proof (induct Us)
case Nil thus ?case by simp
next
case (Cons u Us')
hence u: "u \<in> carrier R" and "set Us' \<subseteq> carrier R" "set Vs \<subseteq> carrier R"
using independent_in_carrier[of K "(u # Us') @ Vs"] by auto
hence "Span K Us' \<subseteq> Span K (Us' @ Vs)"
using mono_Span_append(1) by simp
thus ?case
using independent_backwards[of K u "Us' @ Vs"] Cons li_Cons[OF u] by auto
qed
next
from assms show "Span K Us \<inter> Span K Vs = { \<zero> }"
proof (induct Us rule: list.induct)
case Nil thus ?case
using Span_subgroup_props(2)[OF independent_in_carrier[of K Vs]] by simp
next
case (Cons u Us)
hence IH: "Span K Us \<inter> Span K Vs = {\<zero>}" by auto
have in_carrier:
"u \<in> carrier R" "set Us \<subseteq> carrier R" "set Vs \<subseteq> carrier R" "set (u # Us) \<subseteq> carrier R"
using Cons(2)[THEN independent_in_carrier] by auto
hence "{ \<zero> } \<subseteq> Span K (u # Us) \<inter> Span K Vs"
using in_carrier(3-4)[THEN Span_subgroup_props(2)] by auto
moreover have "Span K (u # Us) \<inter> Span K Vs \<subseteq> { \<zero> }"
proof (rule ccontr)
assume "\<not> Span K (u # Us) \<inter> Span K Vs \<subseteq> {\<zero>}"
hence "\<exists>a. a \<noteq> \<zero> \<and> a \<in> Span K (u # Us) \<and> a \<in> Span K Vs" by auto
then obtain k u' v'
where u': "u' \<in> Span K Us" "u' \<in> carrier R"
and v': "v' \<in> Span K Vs" "v' \<in> carrier R" "v' \<noteq> \<zero>"
and k: "k \<in> K" "(k \<otimes> u \<oplus> u') = v'"
using line_extension_mem_iff[of _ _ u "Span K Us"] in_carrier(2-3)[THEN Span_subgroup_props(1)]
subring_props(1) by force
hence "v' = \<zero>" if "k = \<zero>"
using in_carrier(1) that IH by auto
hence diff_zero: "k \<noteq> \<zero>" using v'(3) by auto
have "k \<in> carrier R"
using subring_props(1) k(1) by blast
hence "k \<otimes> u = (\<ominus> u') \<oplus> v'"
using in_carrier(1) k(2) u'(2) v'(2) add.m_comm r_neg1 by auto
hence "k \<otimes> u \<in> Span K (Us @ Vs)"
using Span_subgroup_props(4)[OF in_carrier(2) u'(1)] v'(1)
Span_append_eq_set_add[OF in_carrier(2-3)] unfolding set_add_def' by blast
hence "u \<in> Span K (Us @ Vs)"
using Cons(2) Span_m_inv_simprule[OF _ _ in_carrier(1), of "Us @ Vs" k]
diff_zero k(1) in_carrier(2-3) by auto
moreover have "u \<notin> Span K (Us @ Vs)"
using independent_backwards(1)[of K u "Us @ Vs"] Cons(2) by auto
ultimately show False by simp
qed
ultimately show ?case by auto
qed
qed
lemma independent_append:
assumes "independent K Us" and "independent K Vs" and "Span K Us \<inter> Span K Vs = { \<zero> }"
shows "independent K (Us @ Vs)"
using assms
proof (induct Us rule: list.induct)
case Nil thus ?case by simp
next
case (Cons u Us)
hence in_carrier:
"u \<in> carrier R" "set Us \<subseteq> carrier R" "set Vs \<subseteq> carrier R" "set (u # Us) \<subseteq> carrier R"
using Cons(2-3)[THEN independent_in_carrier] by auto
hence "Span K Us \<subseteq> Span K (u # Us)"
using mono_Span by auto
hence "Span K Us \<inter> Span K Vs = { \<zero> }"
using Cons(4) Span_subgroup_props(2)[OF in_carrier(2)] by auto
hence "independent K (Us @ Vs)"
using Cons by auto
moreover have "u \<notin> Span K (Us @ Vs)"
proof (rule ccontr)
assume "\<not> u \<notin> Span K (Us @ Vs)"
then obtain u' v'
where u': "u' \<in> Span K Us" "u' \<in> carrier R"
and v': "v' \<in> Span K Vs" "v' \<in> carrier R" and u:"u = u' \<oplus> v'"
using Span_append_eq_set_add[OF in_carrier(2-3)] in_carrier(2-3)[THEN Span_subgroup_props(1)]
unfolding set_add_def' by blast
hence "u \<oplus> (\<ominus> u') = v'"
using in_carrier(1) by algebra
moreover have "u \<in> Span K (u # Us)" and "u' \<in> Span K (u # Us)"
using Span_base_incl[OF in_carrier(4)] mono_Span[OF in_carrier(2,1)] u'(1)
by (auto simp del: Span.simps)
hence "u \<oplus> (\<ominus> u') \<in> Span K (u # Us)"
using Span_subgroup_props(3-4)[OF in_carrier(4)] by (auto simp del: Span.simps)
ultimately have "u \<oplus> (\<ominus> u') = \<zero>"
using Cons(4) v'(1) by auto
hence "u = u'"
using Cons(4) v'(1) in_carrier(1) u'(2) \<open>u \<oplus> \<ominus> u' = v'\<close> u by auto
thus False
using u'(1) independent_backwards(1)[OF Cons(2)] by simp
qed
ultimately show ?case
using in_carrier(1) li_Cons by simp
qed
lemma independent_imp_trivial_combine:
assumes "independent K Us"
shows "\<And>Ks. \<lbrakk> set Ks \<subseteq> K; combine Ks Us = \<zero> \<rbrakk> \<Longrightarrow> set (take (length Us) Ks) \<subseteq> { \<zero> }"
using assms
proof (induct Us rule: list.induct)
case Nil thus ?case by simp
next
case (Cons u Us) thus ?case
proof (cases "Ks = []")
assume "Ks = []" thus ?thesis by auto
next
assume "Ks \<noteq> []"
then obtain k Ks' where k: "k \<in> K" and Ks': "set Ks' \<subseteq> K" and Ks: "Ks = k # Ks'"
using Cons(2) by (metis insert_subset list.exhaust_sel list.simps(15))
hence Us: "set Us \<subseteq> carrier R" and u: "u \<in> carrier R"
using independent_in_carrier[OF Cons(4)] by auto
have "u \<in> Span K Us" if "k \<noteq> \<zero>"
using that Span_mem_iff[OF Us u] Cons(3-4) Ks' k unfolding Ks by blast
hence k_zero: "k = \<zero>"
using independent_backwards[OF Cons(4)] by blast
hence "combine Ks' Us = \<zero>"
using combine_in_carrier[OF _ Us, of Ks'] Ks' u Cons(3) subring_props(1) unfolding Ks by auto
hence "set (take (length Us) Ks') \<subseteq> { \<zero> }"
using Cons(1)[OF Ks' _ independent_backwards(2)[OF Cons(4)]] by simp
thus ?thesis
using k_zero unfolding Ks by auto
qed
qed
lemma non_trivial_combine_imp_dependent:
assumes "set Ks \<subseteq> K" and "combine Ks Us = \<zero>" and "\<not> set (take (length Us) Ks) \<subseteq> { \<zero> }"
shows "dependent K Us"
using independent_imp_trivial_combine[OF _ assms(1-2)] assms(3) by blast
lemma trivial_combine_imp_independent:
assumes "set Us \<subseteq> carrier R"
and "\<And>Ks. \<lbrakk> set Ks \<subseteq> K; combine Ks Us = \<zero> \<rbrakk> \<Longrightarrow> set (take (length Us) Ks) \<subseteq> { \<zero> }"
shows "independent K Us"
using assms
proof (induct Us)
case Nil thus ?case by simp
next
case (Cons u Us)
hence Us: "set Us \<subseteq> carrier R" and u: "u \<in> carrier R" by auto
have "\<And>Ks. \<lbrakk> set Ks \<subseteq> K; combine Ks Us = \<zero> \<rbrakk> \<Longrightarrow> set (take (length Us) Ks) \<subseteq> { \<zero> }"
proof -
fix Ks assume Ks: "set Ks \<subseteq> K" and lin_c: "combine Ks Us = \<zero>"
hence "combine (\<zero> # Ks) (u # Us) = \<zero>"
using u subring_props(1) combine_in_carrier[OF _ Us] by auto
hence "set (take (length (u # Us)) (\<zero> # Ks)) \<subseteq> { \<zero> }"
using Cons(3)[of "\<zero> # Ks"] subring_props(2) Ks by auto
thus "set (take (length Us) Ks) \<subseteq> { \<zero> }" by auto
qed
hence "independent K Us"
using Cons(1)[OF Us] by simp
moreover have "u \<notin> Span K Us"
proof (rule ccontr)
assume "\<not> u \<notin> Span K Us"
then obtain k Ks where k: "k \<in> K" "k \<noteq> \<zero>" and Ks: "set Ks \<subseteq> K" and u: "combine (k # Ks) (u # Us) = \<zero>"
using Span_mem_iff[OF Us u] by auto
have "set (take (length (u # Us)) (k # Ks)) \<subseteq> { \<zero> }"
using Cons(3)[OF _ u] k(1) Ks by auto
hence "k = \<zero>" by auto
from \<open>k = \<zero>\<close> and \<open>k \<noteq> \<zero>\<close> show False by simp
qed
ultimately show ?case
using li_Cons[OF u] by simp
qed
corollary dependent_imp_non_trivial_combine:
assumes "set Us \<subseteq> carrier R" and "dependent K Us"
obtains Ks where "length Ks = length Us" "combine Ks Us = \<zero>" "set Ks \<subseteq> K" "set Ks \<noteq> { \<zero> }"
proof -
obtain Ks
where Ks: "set Ks \<subseteq> carrier R" "set Ks \<subseteq> K" "combine Ks Us = \<zero>" "\<not> set (take (length Us) Ks) \<subseteq> { \<zero> }"
using trivial_combine_imp_independent[OF assms(1)] assms(2) subring_props(1) by blast
obtain Ks'
where Ks': "set (take (length Us) Ks) \<subseteq> set Ks'" "set Ks' \<subseteq> set (take (length Us) Ks) \<union> { \<zero> }"
"length Ks' = length Us" "combine Ks' Us = \<zero>"
using combine_normalize[OF Ks(1) assms(1) Ks(3)] by metis
have "set (take (length Us) Ks) \<subseteq> set Ks"
by (simp add: set_take_subset)
hence "set Ks' \<subseteq> K"
using Ks(2) Ks'(2) subring_props(2) Un_commute by blast
moreover have "set Ks' \<noteq> { \<zero> }"
using Ks'(1) Ks(4) by auto
ultimately show thesis
using that Ks' by blast
qed
corollary unique_decomposition:
assumes "independent K Us"
shows "a \<in> Span K Us \<Longrightarrow> \<exists>!Ks. set Ks \<subseteq> K \<and> length Ks = length Us \<and> a = combine Ks Us"
proof -
note in_carrier = independent_in_carrier[OF assms]
assume "a \<in> Span K Us"
then obtain Ks where Ks: "set Ks \<subseteq> K" "length Ks = length Us" "a = combine Ks Us"
using Span_mem_iff_length_version[OF in_carrier] by blast
moreover
have "\<And>Ks'. \<lbrakk> set Ks' \<subseteq> K; length Ks' = length Us; a = combine Ks' Us \<rbrakk> \<Longrightarrow> Ks = Ks'"
proof -
fix Ks' assume Ks': "set Ks' \<subseteq> K" "length Ks' = length Us" "a = combine Ks' Us"
hence set_Ks: "set Ks \<subseteq> carrier R" and set_Ks': "set Ks' \<subseteq> carrier R"
using subring_props(1) Ks(1) by blast+
have same_length: "length Ks = length Ks'"
using Ks Ks' by simp
have "(combine Ks Us) \<oplus> ((\<ominus> \<one>) \<otimes> (combine Ks' Us)) = \<zero>"
using combine_in_carrier[OF set_Ks in_carrier]
combine_in_carrier[OF set_Ks' in_carrier] Ks(3) Ks'(3) by algebra
hence "(combine Ks Us) \<oplus> (combine (map ((\<otimes>) (\<ominus> \<one>)) Ks') Us) = \<zero>"
using combine_r_distr[OF set_Ks' in_carrier, of "\<ominus> \<one>"] subring_props by auto
moreover have set_map: "set (map ((\<otimes>) (\<ominus> \<one>)) Ks') \<subseteq> K"
using Ks'(1) subring_props by (induct Ks') (auto)
hence "set (map ((\<otimes>) (\<ominus> \<one>)) Ks') \<subseteq> carrier R"
using subring_props(1) by blast
ultimately have "combine (map2 (\<oplus>) Ks (map ((\<otimes>) (\<ominus> \<one>)) Ks')) Us = \<zero>"
using combine_add[OF Ks(2) _ set_Ks _ in_carrier, of "map ((\<otimes>) (\<ominus> \<one>)) Ks'"] Ks'(2) by auto
moreover have "set (map2 (\<oplus>) Ks (map ((\<otimes>) (\<ominus> \<one>)) Ks')) \<subseteq> K"
using Ks(1) set_map subring_props(7)
by (induct Ks) (auto, metis contra_subsetD in_set_zipE local.set_map set_ConsD subring_props(7))
ultimately have "set (take (length Us) (map2 (\<oplus>) Ks (map ((\<otimes>) (\<ominus> \<one>)) Ks'))) \<subseteq> { \<zero> }"
using independent_imp_trivial_combine[OF assms] by auto
hence "set (map2 (\<oplus>) Ks (map ((\<otimes>) (\<ominus> \<one>)) Ks')) \<subseteq> { \<zero> }"
using Ks(2) Ks'(2) by auto
thus "Ks = Ks'"
using set_Ks set_Ks' same_length
proof (induct Ks arbitrary: Ks')
case Nil thus?case by simp
next
case (Cons k Ks)
then obtain k' Ks'' where k': "Ks' = k' # Ks''"
by (metis Suc_length_conv)
have "Ks = Ks''"
using Cons unfolding k' by auto
moreover have "k = k'"
using Cons(2-4) l_minus minus_equality unfolding k' by (auto, fastforce)
ultimately show ?case
unfolding k' by simp
qed
qed
ultimately show ?thesis by blast
qed
subsection \<open>Replacement Theorem\<close>
lemma independent_rotate1_aux:
"independent K (u # Us @ Vs) \<Longrightarrow> independent K ((Us @ [u]) @ Vs)"
proof -
assume "independent K (u # Us @ Vs)"
hence li: "independent K [u]" "independent K Us" "independent K Vs"
and inter: "Span K [u] \<inter> Span K Us = { \<zero> }"
"Span K (u # Us) \<inter> Span K Vs = { \<zero> }"
using independent_split[of "u # Us" Vs] independent_split[of "[u]" Us] by auto
hence "independent K (Us @ [u])"
using independent_append[OF li(2,1)] by auto
moreover have "Span K (Us @ [u]) \<inter> Span K Vs = { \<zero> }"
using Span_same_set[of "u # Us" "Us @ [u]"] li(1-2)[THEN independent_in_carrier] inter(2) by auto
ultimately show "independent K ((Us @ [u]) @ Vs)"
using independent_append[OF _ li(3), of "Us @ [u]"] by simp
qed
corollary independent_rotate1:
"independent K (Us @ Vs) \<Longrightarrow> independent K ((rotate1 Us) @ Vs)"
using independent_rotate1_aux by (cases Us) (auto)
(*
corollary independent_rotate:
"independent K (Us @ Vs) \<Longrightarrow> independent K ((rotate n Us) @ Vs)"
using independent_rotate1 by (induct n) auto
lemma rotate_append: "rotate (length l) (l @ q) = q @ l"
by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap)
*)
corollary independent_same_set:
assumes "set Us = set Vs" and "length Us = length Vs"
shows "independent K Us \<Longrightarrow> independent K Vs"
proof -
assume "independent K Us" thus ?thesis
using assms
proof (induct Us arbitrary: Vs rule: list.induct)
case Nil thus ?case by simp
next
case (Cons u Us)
then obtain Vs' Vs'' where Vs: "Vs = Vs' @ (u # Vs'')"
by (metis list.set_intros(1) split_list)
have in_carrier: "u \<in> carrier R" "set Us \<subseteq> carrier R"
using independent_in_carrier[OF Cons(2)] by auto
have "distinct Vs"
using Cons(3-4) independent_distinct[OF Cons(2)]
by (metis card_distinct distinct_card)
hence "u \<notin> set (Vs' @ Vs'')" and "u \<notin> set Us"
using independent_distinct[OF Cons(2)] unfolding Vs by auto
hence set_eq: "set Us = set (Vs' @ Vs'')" and "length (Vs' @ Vs'') = length Us"
using Cons(3-4) unfolding Vs by auto