1structure ringLib :> ringLib = 2struct 3 4(* 5 app load ["ringNormTheory", "quote", "computeLib"]; 6*) 7 8open HolKernel Parse boolLib ternaryComparisonsTheory quoteTheory quote 9 computeLib; 10 11fun RING_ERR function message = 12 HOL_ERR{origin_structure = "ringLib", 13 origin_function = function, 14 message = message}; 15 16 17(* reify ring expressions: building a signature, which is the correspondence 18 between the semantic level operators and the syntactic level ones. *) 19 20fun ring_field q = 21 rhs(concl(REWRITE_CONV[ringTheory.ring_accessors] (Term q))); 22 23fun sring_field q = 24 rhs(concl(REWRITE_CONV[semi_ringTheory.semi_ring_accessors] (Term q))); 25 26fun inst_ty ty = inst [alpha |-> ty]; 27local fun pmc s = prim_mk_const {Name = s, Thy = "ringNorm"} 28 fun canon_pmc s = prim_mk_const {Name = s, Thy = "canonical"} 29 val pvar = pmc "Pvar" 30 val pcst = pmc "Pconst" 31 val pplus = pmc "Pplus" 32 val pmult = pmc "Pmult" 33 val popp = pmc "Popp" 34 val spvar = canon_pmc "SPvar" 35 val spcst = canon_pmc "SPconst" 36 val spplus = canon_pmc "SPplus" 37 val spmult = canon_pmc "SPmult" 38in 39fun polynom_sign ty ring = 40 let val (P,M,N) = case map ring_field [`RP ^ring`,`RM ^ring`,`RN ^ring`] 41 of [P,M,N] => (P,M,N) 42 | _ => raise Match 43 in 44 { Vars=inst_ty ty pvar, 45 Csts=inst_ty ty pcst, 46 Op1=[(N,inst_ty ty popp)], 47 Op2=[(P,inst_ty ty pplus),(M,inst_ty ty pmult)] } 48 end 49 50fun spolynom_sign ty sring = 51 let val (P,M) = case map sring_field [`SRP ^sring`,`SRM ^sring`] of 52 [P,M] => (P,M) 53 | _ => raise Match 54 in 55 { Vars=inst_ty ty spvar, 56 Csts=inst_ty ty spcst, 57 Op1=[], 58 Op2=[(P,inst_ty ty spplus), (M,inst_ty ty spmult)] } 59 end 60end; 61 62 63 64(* Get the type of (semi-)ring values from the correctness lemma *) 65val find_type = 66 snd o dom_rng o snd o dom_rng o snd o dest_const o 67 fst o strip_comb o rhs o snd o strip_forall o concl; 68 69fun is_ring_thm th = 70 let val (Rator,Rand) = dest_comb (concl th) in 71 case dest_thy_const Rator of 72 {Name="is_ring",Thy="ring",...} => true 73 | {Name="is_semi_ring", Thy="semi_ring",...} => false 74 | _ => raise RING_ERR "" "" 75 end 76 handle HOL_ERR _ => raise RING_ERR "is_ring" "mal-formed thm" 77; 78 79(* name is a prefix for the new constant names. *) 80fun import_ring name th = 81 let val ring = rand (concl th) 82 val { ics_aux_def, interp_cs_def, interp_m_def, interp_vl_def, 83 ivl_aux_def, interp_p_def, 84 canonical_sum_merge_def, monom_insert_def, 85 varlist_insert_def, canonical_sum_scalar_def, 86 canonical_sum_scalar2_def, canonical_sum_scalar3_def, 87 canonical_sum_prod_def, canonical_sum_simplify_def, 88 polynom_normalize_def, polynom_simplify_def, 89 polynom_simplify_ok,... } = 90 ringNormTheory.IMPORT 91 { Vals = [ring], 92 Inst = [th], 93 Rule = REWRITE_RULE[ringTheory.ring_accessors ], 94 Rename = fn s => SOME(name^"_"^s) } 95 in LIST_CONJ 96 [ th, 97 GSYM polynom_simplify_ok, 98 LIST_CONJ [ interp_p_def, varmap_find_def ], 99 LIST_CONJ 100 [ canonical_sum_merge_def, monom_insert_def, 101 varlist_insert_def, canonical_sum_scalar_def, 102 canonical_sum_scalar2_def, canonical_sum_scalar3_def, 103 canonical_sum_prod_def, canonical_sum_simplify_def, 104 ivl_aux_def, interp_vl_def, interp_m_def, ics_aux_def, interp_cs_def, 105 polynom_normalize_def, polynom_simplify_def ] ] 106 end; 107 108fun import_semi_ring name th = 109 let val sring = rand (concl th) 110 val { ics_aux_def, interp_cs_def, interp_m_def, interp_vl_def, 111 ivl_aux_def, interp_sp_def, 112 canonical_sum_merge_def, monom_insert_def, 113 varlist_insert_def, canonical_sum_scalar_def, 114 canonical_sum_scalar2_def, canonical_sum_scalar3_def, 115 canonical_sum_prod_def, canonical_sum_simplify_def, 116 spolynom_normalize_def, spolynom_simplify_def, 117 spolynomial_simplify_ok, ... } = 118 canonicalTheory.IMPORT 119 { Vals = [sring], 120 Inst = [th], 121 Rule = REWRITE_RULE[semi_ringTheory.semi_ring_accessors ], 122 Rename = fn s => SOME(name^"_"^s) } 123 in LIST_CONJ 124 [ th, 125 GSYM spolynomial_simplify_ok, 126 LIST_CONJ [ interp_sp_def, varmap_find_def ], 127 LIST_CONJ 128 [ canonical_sum_merge_def, monom_insert_def, 129 varlist_insert_def, canonical_sum_scalar_def, 130 canonical_sum_scalar2_def, canonical_sum_scalar3_def, 131 canonical_sum_prod_def, canonical_sum_simplify_def, 132 ivl_aux_def, interp_vl_def, interp_m_def, ics_aux_def, interp_cs_def, 133 spolynom_normalize_def, spolynom_simplify_def ] ] 134 end; 135 136fun mk_ring_thm nm th = 137 let val b = is_ring_thm th in 138 (if b then import_ring nm th else import_semi_ring nm th) 139 handle HOL_ERR _ => 140 raise RING_ERR "mk_ring_thm" "Error while importing ring definitions" 141 end; 142(* 143mk_ring_thm "int" (ASSUME���is_ring(ring int_0 int_1 $+ $* $~)���) 144mk_ring_thm "num" 145 (ASSUME ���is_semi_ring (semi_ring 0 1 $+ $* :num semi_ring)���) 146*) 147 148fun store_ring {Name, Theory} = 149 let val thm_nm = Name^"_ring_thms" 150 val ring_thm = mk_ring_thm Name Theory in 151 save_thm(thm_nm, ring_thm) 152 end; 153 154 155fun dest_ring_thm thm = 156 (case CONJ_LIST 4 thm of 157 [th1,th2,th3,th4] => 158 let val ring = rand (concl th1) 159 val ty = find_type th2 160 val sign = 161 if is_ring_thm th1 then polynom_sign ty ring 162 else spolynom_sign ty ring in 163 {Ty=ty,OpSign=sign,SoundThm=th2,LhsThm=th3,RhsThm=th4} 164 end 165 | _ => raise RING_ERR "" "") 166 handle HOL_ERR _ => raise RING_ERR "dest_ring_thm" "ill-formed ring thm"; 167 168 169 170(* Building and storing the conversions *) 171 172val initial_thms = 173 map lazyfy_thm [ COND_CLAUSES, AND_CLAUSES, NOT_CLAUSES, ordering_case_def ]; 174 175 176val lib_thms = 177 [ list_compare_def, index_compare_def, list_merge_def, 178 index_lt_def, ordering_eq_dec ]; 179 180 181fun comp_rws cst_rws lhs_thms rhs_thms = 182 let val rw_lhs = new_compset lhs_thms 183 val rw_rhs = new_compset initial_thms 184 val _ = add_thms (rhs_thms@lhs_thms@lib_thms@cst_rws) rw_rhs in 185 (rw_lhs, rw_rhs) 186 end; 187 188fun binop_eq ty = 189 let val eq = inst [alpha |-> ty] boolSyntax.equality 190 fun mk_eq th1 th2 = 191 CONV_RULE(RAND_CONV(REWRITE_CONV [])) 192 (MK_COMB(AP_TERM eq th1, th2)) 193 in mk_eq 194 end; 195 196(* Ring Database *) 197type convs = { NormConv : conv, EqConv : conv, 198 Reify : term list -> {Metamap : term, Poly : term list} } 199 200fun no_such_ring f ty = 201 RING_ERR f ("No ring declared on type "^Parse.type_to_string ty) 202 203val rings = 204 ref (Redblackmap.mkDict Type.compare) : (hol_type, convs) Redblackmap.dict ref; 205 206fun add_ring ty rng = 207 rings := Redblackmap.insert (!rings, ty,rng); 208 209fun find_apply nm (isel : convs -> ('a -> 'b)) tysel (x:'a) = 210 let 211 val ty = tysel x 212 val r = Redblackmap.find(!rings, ty) 213 handle Redblackmap.NotFound => raise no_such_ring nm ty 214 in 215 isel r x 216 end 217 218val RING_NORM_CONV = find_apply "RING_NORM_CONV" #NormConv type_of 219val RING_CONV = find_apply "RING_CONV" #EqConv (#3 o dest_eq_ty) 220val reify = find_apply "reify" #Reify (type_of o hd) 221 222fun declare_ring {RingThm,IsConst,Rewrites} = 223 let val {Ty,OpSign,SoundThm,LhsThm,RhsThm} = dest_ring_thm RingThm 224 val reify_fun = meta_expr Ty IsConst OpSign 225 val (lhs_rws,rhs_rws) = 226 comp_rws Rewrites (CONJUNCTS LhsThm) (CONJUNCTS RhsThm) 227 val simp_rule = 228 CONV_RULE(CBV_CONV lhs_rws THENC RAND_CONV (CBV_CONV rhs_rws)) 229 val mk_eq = binop_eq Ty 230 231 fun norm_conv t = 232 let val (Metamap,p) = case reify_fun [t] 233 of {Metamap,Poly=[p]} => (Metamap, p) 234 | _ => raise Match 235 val thm = SPECL[Metamap,p] SoundThm 236 in simp_rule thm 237 end 238 handle HOL_ERR _ => raise RING_ERR "norm_conv" "" 239 240 fun eq_conv t = 241 let val (lhs,rhs) = dest_eq t 242 val (Metamap,p1,p2) = case reify_fun [lhs,rhs] 243 of {Metamap,Poly=[p1,p2]} => (Metamap,p1,p2) 244 | _ => raise Match 245 val mthm = SPEC Metamap SoundThm 246 val th1 = simp_rule (SPEC p1 mthm) 247 val th2 = simp_rule (SPEC p2 mthm) 248 in mk_eq th1 th2 249 end 250 handle HOL_ERR _ => raise RING_ERR "eq_conv" "" 251 252 in add_ring Ty { NormConv=norm_conv, EqConv=eq_conv, Reify=reify_fun } 253 end; 254 255end; 256