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