1(* ========================================================================= *)
2(* GROUP THEORY TOOLS                                                        *)
3(* ========================================================================= *)
4
5structure groupTools :> groupTools =
6struct
7
8open HolKernel Parse boolLib bossLib groupTheory;
9
10(* ------------------------------------------------------------------------- *)
11(* Syntax operations.                                                        *)
12(* ------------------------------------------------------------------------- *)
13
14val group_inv_tm = ``group_inv``;
15
16fun dest_group_inv tm =
17    let
18      val (tm,x) = dest_comb tm
19      val (tm,f) = dest_comb tm
20      val _ = same_const tm group_inv_tm orelse raise ERR "group_inv_neg" ""
21    in
22      (f,x)
23    end;
24
25val is_group_inv = can dest_group_inv;
26
27val group_mult_tm = ``group_mult``;
28
29fun dest_group_mult tm =
30    let
31      val (tm,y) = dest_comb tm
32      val (tm,x) = dest_comb tm
33      val (tm,f) = dest_comb tm
34      val _ = same_const tm group_mult_tm orelse raise ERR "dest_group_mult" ""
35    in
36      (f,x,y)
37    end;
38
39val is_group_mult = can dest_group_mult;
40
41val group_exp_tm = ``group_exp``;
42
43fun dest_group_exp tm =
44    let
45      val (tm,n) = dest_comb tm
46      val (tm,x) = dest_comb tm
47      val (tm,f) = dest_comb tm
48      val _ = same_const tm group_exp_tm orelse raise ERR "dest_group_exp" ""
49    in
50      (f,x,n)
51    end;
52
53val is_group_exp = can dest_group_exp;
54
55(* ------------------------------------------------------------------------- *)
56(* AC normalization.                                                         *)
57(* ------------------------------------------------------------------------- *)
58
59val group_ac_conv =
60    {name = "group_ac_conv",
61     key = ``g.mult x y``,
62     conv = subtypeTools.binop_ac_conv
63              {term_compare = compare,
64               dest_binop = dest_group_mult,
65               dest_inv = dest_group_inv,
66               dest_exp = dest_group_exp,
67               assoc_th = group_assoc,
68               comm_th = group_comm,
69               comm_th' = group_comm',
70               id_ths = [],
71               simplify_ths = [],
72               combine_ths = [],
73               combine_ths' = []}};
74
75(* ------------------------------------------------------------------------- *)
76(* Subtype context.                                                          *)
77(* ------------------------------------------------------------------------- *)
78
79val context = subtypeTools.empty2;
80val context = subtypeTools.add_judgement2 AbelianGroup_Group context;
81val context = subtypeTools.add_judgement2 FiniteGroup_Group context;
82val context = subtypeTools.add_judgement2 FiniteAbelianGroup_FiniteGroup context;
83val context =
84    subtypeTools.add_judgement2 FiniteAbelianGroup_AbelianGroup context;
85val context = subtypeTools.add_reduction2 group_id_carrier context;
86val context = subtypeTools.add_reduction2 group_inv_carrier context;
87val context = subtypeTools.add_reduction2 group_mult_carrier context;
88val context = subtypeTools.add_rewrite2 group_lid context;
89val context = subtypeTools.add_rewrite2 group_linv context;
90val context = subtypeTools.add_rewrite2'' group_assoc context;
91val context = subtypeTools.add_rewrite2 group_rinv context;
92val context = subtypeTools.add_rewrite2 group_rid context;
93val context = subtypeTools.add_rewrite2' group_lcancel context;
94val context = subtypeTools.add_rewrite2' group_lcancel_id context;
95val context = subtypeTools.add_rewrite2' group_rcancel context;
96val context = subtypeTools.add_rewrite2' group_rcancel_id context;
97val context = subtypeTools.add_rewrite2' group_inv_cancel context;
98val context = subtypeTools.add_rewrite2 group_inv_inv context;
99val context = subtypeTools.add_rewrite2 group_inv_id context;
100val context = subtypeTools.add_rewrite2'' group_inv_mult context;
101val context = subtypeTools.add_reduction2 group_exp_carrier context;
102val context = subtypeTools.add_rewrite2 group_id_exp context;
103val context = subtypeTools.add_conversion2'' group_ac_conv context;
104val context = subtypeTools.add_reduction2 trivial_group context;
105val context = subtypeTools.add_reduction2 add_mod context;
106val context = subtypeTools.add_judgement2 Prime_Nonzero context;
107val context = subtypeTools.add_reduction2 mult_mod context;
108
109val group_context = context
110
111end
112