# HG changeset patch # User haftmann # Date 1423905855 -3600 # Node ID 9e6c484c93ff9c72791dad96b8f39a6f6d887c59 # Parent 8d2b1bfb60b457cf2bbe18e2e93ae6cb8d153dbe tuned diff -r 8d2b1bfb60b4 -r 9e6c484c93ff src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Sat Feb 14 10:24:15 2015 +0100 +++ b/src/HOL/Tools/semiring_normalizer.ML Sat Feb 14 10:24:15 2015 +0100 @@ -12,10 +12,6 @@ val del: attribute val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute - val funs: thm -> {is_const: morphism -> cterm -> bool, - dest_const: morphism -> cterm -> Rat.rat, - mk_const: morphism -> ctyp -> Rat.rat -> cterm, - conv: morphism -> Proof.context -> cterm -> thm} -> declaration val semiring_funs: thm -> declaration val field_funs: thm -> declaration @@ -102,6 +98,64 @@ get_first (match_inst entry) (sr_ops @ r_ops @ f_ops); in get_first match_struct (get ctxt) end; + + (* extra-logical functions *) + +fun funs raw_key {is_const, dest_const, mk_const, conv} phi = + Data.map (fn data => + let + val key = Morphism.thm phi raw_key; + val _ = AList.defined Thm.eq_thm data key orelse + raise THM ("No data entry for structure key", 0, [key]); + val fns = {is_const = is_const phi, dest_const = dest_const phi, + mk_const = mk_const phi, conv = conv phi}; + in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end); + +val semiring_norm_ss = + simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms semiring_norm}); + +fun semiring_funs raw_key = funs raw_key + {is_const = fn phi => can HOLogic.dest_number o Thm.term_of, + dest_const = fn phi => fn ct => + Rat.rat_of_int (snd + (HOLogic.dest_number (Thm.term_of ct) + handle TERM _ => error "ring_dest_const")), + mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT + (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"), + conv = fn phi => fn ctxt => + Simplifier.rewrite (put_simpset semiring_norm_ss ctxt) + then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_1_eq_1})}; + +fun field_funs raw_key = + let + fun numeral_is_const ct = + case term_of ct of + Const (@{const_name Fields.divide},_) $ a $ b => + can HOLogic.dest_number a andalso can HOLogic.dest_number b + | Const (@{const_name Fields.inverse},_)$t => can HOLogic.dest_number t + | t => can HOLogic.dest_number t + fun dest_const ct = ((case term_of ct of + Const (@{const_name Fields.divide},_) $ a $ b=> + Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) + | Const (@{const_name Fields.inverse},_)$t => + Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) + | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) + handle TERM _ => error "ring_dest_const") + fun mk_const phi cT x = + let val (a, b) = Rat.quotient_of_rat x + in if b = 1 then Numeral.mk_cnumber cT a + else Thm.apply + (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) + (Numeral.mk_cnumber cT a)) + (Numeral.mk_cnumber cT b) + end + in funs raw_key + {is_const = K numeral_is_const, + dest_const = K dest_const, + mk_const = mk_const, + conv = K Numeral_Simprocs.field_comp_conv} + end; + (* logical content *) @@ -157,71 +211,11 @@ val field = (f_ops, f_rules'); val ideal' = map (Thm.symmetric o mk_meta) ideal in - AList.delete Thm.eq_thm key #> - cons (key, ({vars = vars, semiring = semiring, - ring = ring, field = field, idom = idom, ideal = ideal'}, - {is_const = undefined, dest_const = undefined, mk_const = undefined, - conv = undefined})) - end); - - -(* extra-logical functions *) - -fun funs raw_key {is_const, dest_const, mk_const, conv} phi = - Data.map (fn data => - let - val key = Morphism.thm phi raw_key; - val _ = AList.defined Thm.eq_thm data key orelse - raise THM ("No data entry for structure key", 0, [key]); - val fns = {is_const = is_const phi, dest_const = dest_const phi, - mk_const = mk_const phi, conv = conv phi}; - in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end); - -val semiring_norm_ss = - simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms semiring_norm}); - -fun semiring_funs key = funs key - {is_const = fn phi => can HOLogic.dest_number o Thm.term_of, - dest_const = fn phi => fn ct => - Rat.rat_of_int (snd - (HOLogic.dest_number (Thm.term_of ct) - handle TERM _ => error "ring_dest_const")), - mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT - (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"), - conv = fn phi => fn ctxt => - Simplifier.rewrite (put_simpset semiring_norm_ss ctxt) - then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_1_eq_1})}; - -fun field_funs key = - let - fun numeral_is_const ct = - case term_of ct of - Const (@{const_name Fields.divide},_) $ a $ b => - can HOLogic.dest_number a andalso can HOLogic.dest_number b - | Const (@{const_name Fields.inverse},_)$t => can HOLogic.dest_number t - | t => can HOLogic.dest_number t - fun dest_const ct = ((case term_of ct of - Const (@{const_name Fields.divide},_) $ a $ b=> - Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) - | Const (@{const_name Fields.inverse},_)$t => - Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) - | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) - handle TERM _ => error "ring_dest_const") - fun mk_const phi cT x = - let val (a, b) = Rat.quotient_of_rat x - in if b = 1 then Numeral.mk_cnumber cT a - else Thm.apply - (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) - (Numeral.mk_cnumber cT a)) - (Numeral.mk_cnumber cT b) - end - in funs key - {is_const = K numeral_is_const, - dest_const = K dest_const, - mk_const = mk_const, - conv = K Numeral_Simprocs.field_comp_conv} - end; - + AList.update Thm.eq_thm (key, + ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal'}, + {is_const = undefined, dest_const = undefined, mk_const = undefined, + conv = undefined})) + end) (** auxiliary **)