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