1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri May 07 16:12:25 2010 +0200
1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri May 07 16:12:26 2010 +0200
1.3 @@ -700,14 +700,14 @@
1.4 val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
1.5 (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
1.6 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.7 - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.8 + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.9 in rth end
1.10 | ("x+t",[t]) =>
1.11 let
1.12 val T = ctyp_of_term x
1.13 val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
1.14 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.15 - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.16 + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.17 in rth end
1.18 | ("c*x",[c]) =>
1.19 let
1.20 @@ -744,14 +744,14 @@
1.21 val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
1.22 (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
1.23 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.24 - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.25 + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.26 in rth end
1.27 | ("x+t",[t]) =>
1.28 let
1.29 val T = ctyp_of_term x
1.30 val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
1.31 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.32 - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.33 + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.34 in rth end
1.35 | ("c*x",[c]) =>
1.36 let
1.37 @@ -786,14 +786,14 @@
1.38 val th = implies_elim
1.39 (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
1.40 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.41 - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.42 + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.43 in rth end
1.44 | ("x+t",[t]) =>
1.45 let
1.46 val T = ctyp_of_term x
1.47 val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
1.48 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.49 - (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.50 + (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.51 in rth end
1.52 | ("c*x",[c]) =>
1.53 let
1.54 @@ -822,7 +822,7 @@
1.55 val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
1.56 val nth = Conv.fconv_rule
1.57 (Conv.arg_conv (Conv.arg1_conv
1.58 - (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.59 + (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.60 val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
1.61 in rth end
1.62 | Const(@{const_name Orderings.less_eq},_)$a$b =>
1.63 @@ -831,7 +831,7 @@
1.64 val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
1.65 val nth = Conv.fconv_rule
1.66 (Conv.arg_conv (Conv.arg1_conv
1.67 - (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.68 + (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.69 val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
1.70 in rth end
1.71
1.72 @@ -841,7 +841,7 @@
1.73 val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
1.74 val nth = Conv.fconv_rule
1.75 (Conv.arg_conv (Conv.arg1_conv
1.76 - (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.77 + (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.78 val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
1.79 in rth end
1.80 | @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
2.1 --- a/src/HOL/IsaMakefile Fri May 07 16:12:25 2010 +0200
2.2 +++ b/src/HOL/IsaMakefile Fri May 07 16:12:26 2010 +0200
2.3 @@ -284,10 +284,9 @@
2.4 $(SRC)/Tools/Metis/metis.ML \
2.5 Tools/ATP_Manager/atp_manager.ML \
2.6 Tools/ATP_Manager/atp_systems.ML \
2.7 - Tools/Groebner_Basis/groebner.ML \
2.8 - Tools/Groebner_Basis/normalizer.ML \
2.9 Tools/choice_specification.ML \
2.10 Tools/int_arith.ML \
2.11 + Tools/groebner.ML \
2.12 Tools/list_code.ML \
2.13 Tools/meson.ML \
2.14 Tools/nat_numeral_simprocs.ML \
2.15 @@ -314,6 +313,7 @@
2.16 Tools/Quotient/quotient_term.ML \
2.17 Tools/Quotient/quotient_typ.ML \
2.18 Tools/recdef.ML \
2.19 + Tools/semiring_normalizer.ML \
2.20 Tools/Sledgehammer/meson_tactic.ML \
2.21 Tools/Sledgehammer/metis_tactics.ML \
2.22 Tools/Sledgehammer/sledgehammer_fact_filter.ML \
3.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri May 07 16:12:25 2010 +0200
3.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri May 07 16:12:26 2010 +0200
3.3 @@ -1194,8 +1194,8 @@
3.4 (* FIXME: Replace tryfind by get_first !! *)
3.5 fun real_nonlinear_prover proof_method ctxt =
3.6 let
3.7 - val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt
3.8 - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
3.9 + val {add,mul,neg,pow,sub,main} = Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
3.10 + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
3.11 simple_cterm_ord
3.12 val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
3.13 real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
3.14 @@ -1309,8 +1309,8 @@
3.15
3.16 fun real_nonlinear_subst_prover prover ctxt =
3.17 let
3.18 - val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt
3.19 - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
3.20 + val {add,mul,neg,pow,sub,main} = Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
3.21 + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
3.22 simple_cterm_ord
3.23
3.24 val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
4.1 --- a/src/HOL/Library/normarith.ML Fri May 07 16:12:25 2010 +0200
4.2 +++ b/src/HOL/Library/normarith.ML Fri May 07 16:12:26 2010 +0200
4.3 @@ -166,8 +166,8 @@
4.4 let
4.5 (* FIXME : Should be computed statically!! *)
4.6 val real_poly_conv =
4.7 - Normalizer.semiring_normalize_wrapper ctxt
4.8 - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
4.9 + Semiring_Normalizer.semiring_normalize_wrapper ctxt
4.10 + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
4.11 in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Numeral_Simprocs.field_comp_conv then_conv real_poly_conv)))
4.12 end;
4.13
4.14 @@ -277,8 +277,8 @@
4.15 let
4.16 (* FIXME: Should be computed statically!!*)
4.17 val real_poly_conv =
4.18 - Normalizer.semiring_normalize_wrapper ctxt
4.19 - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
4.20 + Semiring_Normalizer.semiring_normalize_wrapper ctxt
4.21 + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
4.22 val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
4.23 val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) []
4.24 val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check"
4.25 @@ -383,8 +383,8 @@
4.26 fun splitequation ctxt th acc =
4.27 let
4.28 val real_poly_neg_conv = #neg
4.29 - (Normalizer.semiring_normalizers_ord_wrapper ctxt
4.30 - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
4.31 + (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
4.32 + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
4.33 val (th1,th2) = conj_pair(rawrule th)
4.34 in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
4.35 end
5.1 --- a/src/HOL/Library/positivstellensatz.ML Fri May 07 16:12:25 2010 +0200
5.2 +++ b/src/HOL/Library/positivstellensatz.ML Fri May 07 16:12:26 2010 +0200
5.3 @@ -747,8 +747,8 @@
5.4 let
5.5 fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
5.6 val {add,mul,neg,pow,sub,main} =
5.7 - Normalizer.semiring_normalizers_ord_wrapper ctxt
5.8 - (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
5.9 + Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
5.10 + (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
5.11 simple_cterm_ord
5.12 in gen_real_arith ctxt
5.13 (cterm_of_rat, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv,
6.1 --- a/src/HOL/Semiring_Normalization.thy Fri May 07 16:12:25 2010 +0200
6.2 +++ b/src/HOL/Semiring_Normalization.thy Fri May 07 16:12:26 2010 +0200
6.3 @@ -7,10 +7,10 @@
6.4 theory Semiring_Normalization
6.5 imports Numeral_Simprocs Nat_Transfer
6.6 uses
6.7 - "Tools/Groebner_Basis/normalizer.ML"
6.8 + "Tools/semiring_normalizer.ML"
6.9 begin
6.10
6.11 -setup Normalizer.setup
6.12 +setup Semiring_Normalizer.setup
6.13
6.14 locale normalizing_semiring =
6.15 fixes add mul pwr r0 r1
6.16 @@ -159,7 +159,7 @@
6.17 proof
6.18 qed (simp_all add: algebra_simps)
6.19
6.20 -declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *}
6.21 +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *}
6.22
6.23 locale normalizing_ring = normalizing_semiring +
6.24 fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
6.25 @@ -186,7 +186,7 @@
6.26 proof
6.27 qed (simp_all add: diff_minus)
6.28
6.29 -declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *}
6.30 +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *}
6.31
6.32 locale normalizing_field = normalizing_ring +
6.33 fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
6.34 @@ -283,7 +283,7 @@
6.35 qed (auto simp add: add_ac)
6.36 qed (simp_all add: algebra_simps)
6.37
6.38 -declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *}
6.39 +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *}
6.40
6.41 interpretation normalizing_nat!: normalizing_semiring_cancel
6.42 "op +" "op *" "op ^" "0::nat" "1"
6.43 @@ -307,7 +307,7 @@
6.44 thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
6.45 qed
6.46
6.47 -declaration {* Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}
6.48 +declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}
6.49
6.50 locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field
6.51 begin
6.52 @@ -331,6 +331,6 @@
6.53 proof
6.54 qed (simp_all add: divide_inverse)
6.55
6.56 -declaration {* Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *}
6.57 +declaration {* Semiring_Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *}
6.58
6.59 end
7.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Fri May 07 16:12:25 2010 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,913 +0,0 @@
7.4 -(* Title: HOL/Tools/Groebner_Basis/normalizer.ML
7.5 - Author: Amine Chaieb, TU Muenchen
7.6 -
7.7 -Normalization of expressions in semirings.
7.8 -*)
7.9 -
7.10 -signature NORMALIZER =
7.11 -sig
7.12 - type entry
7.13 - val get: Proof.context -> (thm * entry) list
7.14 - val match: Proof.context -> cterm -> entry option
7.15 - val del: attribute
7.16 - val add: {semiring: cterm list * thm list, ring: cterm list * thm list,
7.17 - field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute
7.18 - val funs: thm -> {is_const: morphism -> cterm -> bool,
7.19 - dest_const: morphism -> cterm -> Rat.rat,
7.20 - mk_const: morphism -> ctyp -> Rat.rat -> cterm,
7.21 - conv: morphism -> Proof.context -> cterm -> thm} -> declaration
7.22 - val semiring_funs: thm -> declaration
7.23 - val field_funs: thm -> declaration
7.24 -
7.25 - val semiring_normalize_conv: Proof.context -> conv
7.26 - val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
7.27 - val semiring_normalize_wrapper: Proof.context -> entry -> conv
7.28 - val semiring_normalize_ord_wrapper: Proof.context -> entry
7.29 - -> (cterm -> cterm -> bool) -> conv
7.30 - val semiring_normalizers_conv: cterm list -> cterm list * thm list
7.31 - -> cterm list * thm list -> cterm list * thm list ->
7.32 - (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
7.33 - {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
7.34 - val semiring_normalizers_ord_wrapper: Proof.context -> entry ->
7.35 - (cterm -> cterm -> bool) ->
7.36 - {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
7.37 -
7.38 - val setup: theory -> theory
7.39 -end
7.40 -
7.41 -structure Normalizer: NORMALIZER =
7.42 -struct
7.43 -
7.44 -(** some conversion **)
7.45 -
7.46 -
7.47 -
7.48 -(** data **)
7.49 -
7.50 -type entry =
7.51 - {vars: cterm list,
7.52 - semiring: cterm list * thm list,
7.53 - ring: cterm list * thm list,
7.54 - field: cterm list * thm list,
7.55 - idom: thm list,
7.56 - ideal: thm list} *
7.57 - {is_const: cterm -> bool,
7.58 - dest_const: cterm -> Rat.rat,
7.59 - mk_const: ctyp -> Rat.rat -> cterm,
7.60 - conv: Proof.context -> cterm -> thm};
7.61 -
7.62 -structure Data = Generic_Data
7.63 -(
7.64 - type T = (thm * entry) list;
7.65 - val empty = [];
7.66 - val extend = I;
7.67 - val merge = AList.merge Thm.eq_thm (K true);
7.68 -);
7.69 -
7.70 -val get = Data.get o Context.Proof;
7.71 -
7.72 -fun match ctxt tm =
7.73 - let
7.74 - fun match_inst
7.75 - ({vars, semiring = (sr_ops, sr_rules),
7.76 - ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
7.77 - fns as {is_const, dest_const, mk_const, conv}) pat =
7.78 - let
7.79 - fun h instT =
7.80 - let
7.81 - val substT = Thm.instantiate (instT, []);
7.82 - val substT_cterm = Drule.cterm_rule substT;
7.83 -
7.84 - val vars' = map substT_cterm vars;
7.85 - val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
7.86 - val ring' = (map substT_cterm r_ops, map substT r_rules);
7.87 - val field' = (map substT_cterm f_ops, map substT f_rules);
7.88 - val idom' = map substT idom;
7.89 - val ideal' = map substT ideal;
7.90 -
7.91 - val result = ({vars = vars', semiring = semiring',
7.92 - ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
7.93 - in SOME result end
7.94 - in (case try Thm.match (pat, tm) of
7.95 - NONE => NONE
7.96 - | SOME (instT, _) => h instT)
7.97 - end;
7.98 -
7.99 - fun match_struct (_,
7.100 - entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
7.101 - get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
7.102 - in get_first match_struct (get ctxt) end;
7.103 -
7.104 -
7.105 -(* logical content *)
7.106 -
7.107 -val semiringN = "semiring";
7.108 -val ringN = "ring";
7.109 -val idomN = "idom";
7.110 -val idealN = "ideal";
7.111 -val fieldN = "field";
7.112 -
7.113 -fun undefined _ = raise Match;
7.114 -
7.115 -val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm);
7.116 -
7.117 -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
7.118 - field = (f_ops, f_rules), idom, ideal} =
7.119 - Thm.declaration_attribute (fn key => fn context => context |> Data.map
7.120 - let
7.121 - val ctxt = Context.proof_of context;
7.122 -
7.123 - fun check kind name xs n =
7.124 - null xs orelse length xs = n orelse
7.125 - error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
7.126 - val check_ops = check "operations";
7.127 - val check_rules = check "rules";
7.128 -
7.129 - val _ =
7.130 - check_ops semiringN sr_ops 5 andalso
7.131 - check_rules semiringN sr_rules 37 andalso
7.132 - check_ops ringN r_ops 2 andalso
7.133 - check_rules ringN r_rules 2 andalso
7.134 - check_ops fieldN f_ops 2 andalso
7.135 - check_rules fieldN f_rules 2 andalso
7.136 - check_rules idomN idom 2;
7.137 -
7.138 - val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
7.139 - val sr_rules' = map mk_meta sr_rules;
7.140 - val r_rules' = map mk_meta r_rules;
7.141 - val f_rules' = map mk_meta f_rules;
7.142 -
7.143 - fun rule i = nth sr_rules' (i - 1);
7.144 -
7.145 - val (cx, cy) = Thm.dest_binop (hd sr_ops);
7.146 - val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
7.147 - val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
7.148 - val ((clx, crx), (cly, cry)) =
7.149 - rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
7.150 - val ((ca, cb), (cc, cd)) =
7.151 - rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
7.152 - val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
7.153 - val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
7.154 -
7.155 - val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
7.156 - val semiring = (sr_ops, sr_rules');
7.157 - val ring = (r_ops, r_rules');
7.158 - val field = (f_ops, f_rules');
7.159 - val ideal' = map (symmetric o mk_meta) ideal
7.160 - in
7.161 - AList.delete Thm.eq_thm key #>
7.162 - cons (key, ({vars = vars, semiring = semiring,
7.163 - ring = ring, field = field, idom = idom, ideal = ideal'},
7.164 - {is_const = undefined, dest_const = undefined, mk_const = undefined,
7.165 - conv = undefined}))
7.166 - end);
7.167 -
7.168 -
7.169 -(* extra-logical functions *)
7.170 -
7.171 -fun funs raw_key {is_const, dest_const, mk_const, conv} phi =
7.172 - Data.map (fn data =>
7.173 - let
7.174 - val key = Morphism.thm phi raw_key;
7.175 - val _ = AList.defined Thm.eq_thm data key orelse
7.176 - raise THM ("No data entry for structure key", 0, [key]);
7.177 - val fns = {is_const = is_const phi, dest_const = dest_const phi,
7.178 - mk_const = mk_const phi, conv = conv phi};
7.179 - in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
7.180 -
7.181 -fun semiring_funs key = funs key
7.182 - {is_const = fn phi => can HOLogic.dest_number o Thm.term_of,
7.183 - dest_const = fn phi => fn ct =>
7.184 - Rat.rat_of_int (snd
7.185 - (HOLogic.dest_number (Thm.term_of ct)
7.186 - handle TERM _ => error "ring_dest_const")),
7.187 - mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT
7.188 - (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"),
7.189 - conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm})
7.190 - then_conv Simplifier.rewrite (HOL_basic_ss addsimps
7.191 - (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))};
7.192 -
7.193 -fun field_funs key =
7.194 - let
7.195 - fun numeral_is_const ct =
7.196 - case term_of ct of
7.197 - Const (@{const_name Rings.divide},_) $ a $ b =>
7.198 - can HOLogic.dest_number a andalso can HOLogic.dest_number b
7.199 - | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
7.200 - | t => can HOLogic.dest_number t
7.201 - fun dest_const ct = ((case term_of ct of
7.202 - Const (@{const_name Rings.divide},_) $ a $ b=>
7.203 - Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
7.204 - | Const (@{const_name Rings.inverse},_)$t =>
7.205 - Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
7.206 - | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
7.207 - handle TERM _ => error "ring_dest_const")
7.208 - fun mk_const phi cT x =
7.209 - let val (a, b) = Rat.quotient_of_rat x
7.210 - in if b = 1 then Numeral.mk_cnumber cT a
7.211 - else Thm.capply
7.212 - (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
7.213 - (Numeral.mk_cnumber cT a))
7.214 - (Numeral.mk_cnumber cT b)
7.215 - end
7.216 - in funs key
7.217 - {is_const = K numeral_is_const,
7.218 - dest_const = K dest_const,
7.219 - mk_const = mk_const,
7.220 - conv = K (K Numeral_Simprocs.field_comp_conv)}
7.221 - end;
7.222 -
7.223 -
7.224 -
7.225 -(** auxiliary **)
7.226 -
7.227 -fun is_comb ct =
7.228 - (case Thm.term_of ct of
7.229 - _ $ _ => true
7.230 - | _ => false);
7.231 -
7.232 -val concl = Thm.cprop_of #> Thm.dest_arg;
7.233 -
7.234 -fun is_binop ct ct' =
7.235 - (case Thm.term_of ct' of
7.236 - c $ _ $ _ => term_of ct aconv c
7.237 - | _ => false);
7.238 -
7.239 -fun dest_binop ct ct' =
7.240 - if is_binop ct ct' then Thm.dest_binop ct'
7.241 - else raise CTERM ("dest_binop: bad binop", [ct, ct'])
7.242 -
7.243 -fun inst_thm inst = Thm.instantiate ([], inst);
7.244 -
7.245 -val dest_numeral = term_of #> HOLogic.dest_number #> snd;
7.246 -val is_numeral = can dest_numeral;
7.247 -
7.248 -val numeral01_conv = Simplifier.rewrite
7.249 - (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]);
7.250 -val zero1_numeral_conv =
7.251 - Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]);
7.252 -fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv;
7.253 -val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
7.254 - @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"},
7.255 - @{thm "less_nat_number_of"}];
7.256 -
7.257 -val nat_add_conv =
7.258 - zerone_conv
7.259 - (Simplifier.rewrite
7.260 - (HOL_basic_ss
7.261 - addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
7.262 - @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
7.263 - @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
7.264 - @ map (fn th => th RS sym) @{thms numerals}));
7.265 -
7.266 -val zeron_tm = @{cterm "0::nat"};
7.267 -val onen_tm = @{cterm "1::nat"};
7.268 -val true_tm = @{cterm "True"};
7.269 -
7.270 -
7.271 -(** normalizing conversions **)
7.272 -
7.273 -(* core conversion *)
7.274 -
7.275 -fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
7.276 - (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
7.277 -let
7.278 -
7.279 -val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,
7.280 - pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
7.281 - pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
7.282 - pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
7.283 - pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;
7.284 -
7.285 -val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
7.286 -val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
7.287 -val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
7.288 -
7.289 -val dest_add = dest_binop add_tm
7.290 -val dest_mul = dest_binop mul_tm
7.291 -fun dest_pow tm =
7.292 - let val (l,r) = dest_binop pow_tm tm
7.293 - in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])
7.294 - end;
7.295 -val is_add = is_binop add_tm
7.296 -val is_mul = is_binop mul_tm
7.297 -fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);
7.298 -
7.299 -val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
7.300 - (case (r_ops, r_rules) of
7.301 - ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
7.302 - let
7.303 - val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
7.304 - val neg_tm = Thm.dest_fun neg_pat
7.305 - val dest_sub = dest_binop sub_tm
7.306 - val is_sub = is_binop sub_tm
7.307 - in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
7.308 - sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
7.309 - end
7.310 - | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
7.311 -
7.312 -val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) =
7.313 - (case (f_ops, f_rules) of
7.314 - ([divide_pat, inverse_pat], [div_inv, inv_div]) =>
7.315 - let val div_tm = funpow 2 Thm.dest_fun divide_pat
7.316 - val inv_tm = Thm.dest_fun inverse_pat
7.317 - in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
7.318 - end
7.319 - | _ => (TrueI, TrueI, true_tm, true_tm, K false));
7.320 -
7.321 -in fn variable_order =>
7.322 - let
7.323 -
7.324 -(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible. *)
7.325 -(* Also deals with "const * const", but both terms must involve powers of *)
7.326 -(* the same variable, or both be constants, or behaviour may be incorrect. *)
7.327 -
7.328 - fun powvar_mul_conv tm =
7.329 - let
7.330 - val (l,r) = dest_mul tm
7.331 - in if is_semiring_constant l andalso is_semiring_constant r
7.332 - then semiring_mul_conv tm
7.333 - else
7.334 - ((let
7.335 - val (lx,ln) = dest_pow l
7.336 - in
7.337 - ((let val (rx,rn) = dest_pow r
7.338 - val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
7.339 - val (tm1,tm2) = Thm.dest_comb(concl th1) in
7.340 - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
7.341 - handle CTERM _ =>
7.342 - (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
7.343 - val (tm1,tm2) = Thm.dest_comb(concl th1) in
7.344 - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
7.345 - handle CTERM _ =>
7.346 - ((let val (rx,rn) = dest_pow r
7.347 - val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
7.348 - val (tm1,tm2) = Thm.dest_comb(concl th1) in
7.349 - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
7.350 - handle CTERM _ => inst_thm [(cx,l)] pthm_32
7.351 -
7.352 -))
7.353 - end;
7.354 -
7.355 -(* Remove "1 * m" from a monomial, and just leave m. *)
7.356 -
7.357 - fun monomial_deone th =
7.358 - (let val (l,r) = dest_mul(concl th) in
7.359 - if l aconvc one_tm
7.360 - then transitive th (inst_thm [(ca,r)] pthm_13) else th end)
7.361 - handle CTERM _ => th;
7.362 -
7.363 -(* Conversion for "(monomial)^n", where n is a numeral. *)
7.364 -
7.365 - val monomial_pow_conv =
7.366 - let
7.367 - fun monomial_pow tm bod ntm =
7.368 - if not(is_comb bod)
7.369 - then reflexive tm
7.370 - else
7.371 - if is_semiring_constant bod
7.372 - then semiring_pow_conv tm
7.373 - else
7.374 - let
7.375 - val (lopr,r) = Thm.dest_comb bod
7.376 - in if not(is_comb lopr)
7.377 - then reflexive tm
7.378 - else
7.379 - let
7.380 - val (opr,l) = Thm.dest_comb lopr
7.381 - in
7.382 - if opr aconvc pow_tm andalso is_numeral r
7.383 - then
7.384 - let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
7.385 - val (l,r) = Thm.dest_comb(concl th1)
7.386 - in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
7.387 - end
7.388 - else
7.389 - if opr aconvc mul_tm
7.390 - then
7.391 - let
7.392 - val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33
7.393 - val (xy,z) = Thm.dest_comb(concl th1)
7.394 - val (x,y) = Thm.dest_comb xy
7.395 - val thl = monomial_pow y l ntm
7.396 - val thr = monomial_pow z r ntm
7.397 - in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
7.398 - end
7.399 - else reflexive tm
7.400 - end
7.401 - end
7.402 - in fn tm =>
7.403 - let
7.404 - val (lopr,r) = Thm.dest_comb tm
7.405 - val (opr,l) = Thm.dest_comb lopr
7.406 - in if not (opr aconvc pow_tm) orelse not(is_numeral r)
7.407 - then raise CTERM ("monomial_pow_conv", [tm])
7.408 - else if r aconvc zeron_tm
7.409 - then inst_thm [(cx,l)] pthm_35
7.410 - else if r aconvc onen_tm
7.411 - then inst_thm [(cx,l)] pthm_36
7.412 - else monomial_deone(monomial_pow tm l r)
7.413 - end
7.414 - end;
7.415 -
7.416 -(* Multiplication of canonical monomials. *)
7.417 - val monomial_mul_conv =
7.418 - let
7.419 - fun powvar tm =
7.420 - if is_semiring_constant tm then one_tm
7.421 - else
7.422 - ((let val (lopr,r) = Thm.dest_comb tm
7.423 - val (opr,l) = Thm.dest_comb lopr
7.424 - in if opr aconvc pow_tm andalso is_numeral r then l
7.425 - else raise CTERM ("monomial_mul_conv",[tm]) end)
7.426 - handle CTERM _ => tm) (* FIXME !? *)
7.427 - fun vorder x y =
7.428 - if x aconvc y then 0
7.429 - else
7.430 - if x aconvc one_tm then ~1
7.431 - else if y aconvc one_tm then 1
7.432 - else if variable_order x y then ~1 else 1
7.433 - fun monomial_mul tm l r =
7.434 - ((let val (lx,ly) = dest_mul l val vl = powvar lx
7.435 - in
7.436 - ((let
7.437 - val (rx,ry) = dest_mul r
7.438 - val vr = powvar rx
7.439 - val ord = vorder vl vr
7.440 - in
7.441 - if ord = 0
7.442 - then
7.443 - let
7.444 - val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15
7.445 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.446 - val (tm3,tm4) = Thm.dest_comb tm1
7.447 - val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
7.448 - val th3 = transitive th1 th2
7.449 - val (tm5,tm6) = Thm.dest_comb(concl th3)
7.450 - val (tm7,tm8) = Thm.dest_comb tm6
7.451 - val th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
7.452 - in transitive th3 (Drule.arg_cong_rule tm5 th4)
7.453 - end
7.454 - else
7.455 - let val th0 = if ord < 0 then pthm_16 else pthm_17
7.456 - val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
7.457 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.458 - val (tm3,tm4) = Thm.dest_comb tm2
7.459 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
7.460 - end
7.461 - end)
7.462 - handle CTERM _ =>
7.463 - (let val vr = powvar r val ord = vorder vl vr
7.464 - in
7.465 - if ord = 0 then
7.466 - let
7.467 - val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18
7.468 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.469 - val (tm3,tm4) = Thm.dest_comb tm1
7.470 - val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
7.471 - in transitive th1 th2
7.472 - end
7.473 - else
7.474 - if ord < 0 then
7.475 - let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
7.476 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.477 - val (tm3,tm4) = Thm.dest_comb tm2
7.478 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
7.479 - end
7.480 - else inst_thm [(ca,l),(cb,r)] pthm_09
7.481 - end)) end)
7.482 - handle CTERM _ =>
7.483 - (let val vl = powvar l in
7.484 - ((let
7.485 - val (rx,ry) = dest_mul r
7.486 - val vr = powvar rx
7.487 - val ord = vorder vl vr
7.488 - in if ord = 0 then
7.489 - let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
7.490 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.491 - val (tm3,tm4) = Thm.dest_comb tm1
7.492 - in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
7.493 - end
7.494 - else if ord > 0 then
7.495 - let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
7.496 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.497 - val (tm3,tm4) = Thm.dest_comb tm2
7.498 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
7.499 - end
7.500 - else reflexive tm
7.501 - end)
7.502 - handle CTERM _ =>
7.503 - (let val vr = powvar r
7.504 - val ord = vorder vl vr
7.505 - in if ord = 0 then powvar_mul_conv tm
7.506 - else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
7.507 - else reflexive tm
7.508 - end)) end))
7.509 - in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
7.510 - end
7.511 - end;
7.512 -(* Multiplication by monomial of a polynomial. *)
7.513 -
7.514 - val polynomial_monomial_mul_conv =
7.515 - let
7.516 - fun pmm_conv tm =
7.517 - let val (l,r) = dest_mul tm
7.518 - in
7.519 - ((let val (y,z) = dest_add r
7.520 - val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
7.521 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.522 - val (tm3,tm4) = Thm.dest_comb tm1
7.523 - val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
7.524 - in transitive th1 th2
7.525 - end)
7.526 - handle CTERM _ => monomial_mul_conv tm)
7.527 - end
7.528 - in pmm_conv
7.529 - end;
7.530 -
7.531 -(* Addition of two monomials identical except for constant multiples. *)
7.532 -
7.533 -fun monomial_add_conv tm =
7.534 - let val (l,r) = dest_add tm
7.535 - in if is_semiring_constant l andalso is_semiring_constant r
7.536 - then semiring_add_conv tm
7.537 - else
7.538 - let val th1 =
7.539 - if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)
7.540 - then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then
7.541 - inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02
7.542 - else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03
7.543 - else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)
7.544 - then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04
7.545 - else inst_thm [(cm,r)] pthm_05
7.546 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.547 - val (tm3,tm4) = Thm.dest_comb tm1
7.548 - val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
7.549 - val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
7.550 - val tm5 = concl th3
7.551 - in
7.552 - if (Thm.dest_arg1 tm5) aconvc zero_tm
7.553 - then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
7.554 - else monomial_deone th3
7.555 - end
7.556 - end;
7.557 -
7.558 -(* Ordering on monomials. *)
7.559 -
7.560 -fun striplist dest =
7.561 - let fun strip x acc =
7.562 - ((let val (l,r) = dest x in
7.563 - strip l (strip r acc) end)
7.564 - handle CTERM _ => x::acc) (* FIXME !? *)
7.565 - in fn x => strip x []
7.566 - end;
7.567 -
7.568 -
7.569 -fun powervars tm =
7.570 - let val ptms = striplist dest_mul tm
7.571 - in if is_semiring_constant (hd ptms) then tl ptms else ptms
7.572 - end;
7.573 -val num_0 = 0;
7.574 -val num_1 = 1;
7.575 -fun dest_varpow tm =
7.576 - ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)
7.577 - handle CTERM _ =>
7.578 - (tm,(if is_semiring_constant tm then num_0 else num_1)));
7.579 -
7.580 -val morder =
7.581 - let fun lexorder l1 l2 =
7.582 - case (l1,l2) of
7.583 - ([],[]) => 0
7.584 - | (vps,[]) => ~1
7.585 - | ([],vps) => 1
7.586 - | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
7.587 - if variable_order x1 x2 then 1
7.588 - else if variable_order x2 x1 then ~1
7.589 - else if n1 < n2 then ~1
7.590 - else if n2 < n1 then 1
7.591 - else lexorder vs1 vs2
7.592 - in fn tm1 => fn tm2 =>
7.593 - let val vdegs1 = map dest_varpow (powervars tm1)
7.594 - val vdegs2 = map dest_varpow (powervars tm2)
7.595 - val deg1 = fold (Integer.add o snd) vdegs1 num_0
7.596 - val deg2 = fold (Integer.add o snd) vdegs2 num_0
7.597 - in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
7.598 - else lexorder vdegs1 vdegs2
7.599 - end
7.600 - end;
7.601 -
7.602 -(* Addition of two polynomials. *)
7.603 -
7.604 -val polynomial_add_conv =
7.605 - let
7.606 - fun dezero_rule th =
7.607 - let
7.608 - val tm = concl th
7.609 - in
7.610 - if not(is_add tm) then th else
7.611 - let val (lopr,r) = Thm.dest_comb tm
7.612 - val l = Thm.dest_arg lopr
7.613 - in
7.614 - if l aconvc zero_tm
7.615 - then transitive th (inst_thm [(ca,r)] pthm_07) else
7.616 - if r aconvc zero_tm
7.617 - then transitive th (inst_thm [(ca,l)] pthm_08) else th
7.618 - end
7.619 - end
7.620 - fun padd tm =
7.621 - let
7.622 - val (l,r) = dest_add tm
7.623 - in
7.624 - if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07
7.625 - else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08
7.626 - else
7.627 - if is_add l
7.628 - then
7.629 - let val (a,b) = dest_add l
7.630 - in
7.631 - if is_add r then
7.632 - let val (c,d) = dest_add r
7.633 - val ord = morder a c
7.634 - in
7.635 - if ord = 0 then
7.636 - let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23
7.637 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.638 - val (tm3,tm4) = Thm.dest_comb tm1
7.639 - val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
7.640 - in dezero_rule (transitive th1 (combination th2 (padd tm2)))
7.641 - end
7.642 - else (* ord <> 0*)
7.643 - let val th1 =
7.644 - if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
7.645 - else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
7.646 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.647 - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
7.648 - end
7.649 - end
7.650 - else (* not (is_add r)*)
7.651 - let val ord = morder a r
7.652 - in
7.653 - if ord = 0 then
7.654 - let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26
7.655 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.656 - val (tm3,tm4) = Thm.dest_comb tm1
7.657 - val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
7.658 - in dezero_rule (transitive th1 th2)
7.659 - end
7.660 - else (* ord <> 0*)
7.661 - if ord > 0 then
7.662 - let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
7.663 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.664 - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
7.665 - end
7.666 - else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
7.667 - end
7.668 - end
7.669 - else (* not (is_add l)*)
7.670 - if is_add r then
7.671 - let val (c,d) = dest_add r
7.672 - val ord = morder l c
7.673 - in
7.674 - if ord = 0 then
7.675 - let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28
7.676 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.677 - val (tm3,tm4) = Thm.dest_comb tm1
7.678 - val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
7.679 - in dezero_rule (transitive th1 th2)
7.680 - end
7.681 - else
7.682 - if ord > 0 then reflexive tm
7.683 - else
7.684 - let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
7.685 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.686 - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
7.687 - end
7.688 - end
7.689 - else
7.690 - let val ord = morder l r
7.691 - in
7.692 - if ord = 0 then monomial_add_conv tm
7.693 - else if ord > 0 then dezero_rule(reflexive tm)
7.694 - else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
7.695 - end
7.696 - end
7.697 - in padd
7.698 - end;
7.699 -
7.700 -(* Multiplication of two polynomials. *)
7.701 -
7.702 -val polynomial_mul_conv =
7.703 - let
7.704 - fun pmul tm =
7.705 - let val (l,r) = dest_mul tm
7.706 - in
7.707 - if not(is_add l) then polynomial_monomial_mul_conv tm
7.708 - else
7.709 - if not(is_add r) then
7.710 - let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
7.711 - in transitive th1 (polynomial_monomial_mul_conv(concl th1))
7.712 - end
7.713 - else
7.714 - let val (a,b) = dest_add l
7.715 - val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10
7.716 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.717 - val (tm3,tm4) = Thm.dest_comb tm1
7.718 - val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
7.719 - val th3 = transitive th1 (combination th2 (pmul tm2))
7.720 - in transitive th3 (polynomial_add_conv (concl th3))
7.721 - end
7.722 - end
7.723 - in fn tm =>
7.724 - let val (l,r) = dest_mul tm
7.725 - in
7.726 - if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11
7.727 - else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12
7.728 - else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13
7.729 - else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14
7.730 - else pmul tm
7.731 - end
7.732 - end;
7.733 -
7.734 -(* Power of polynomial (optimized for the monomial and trivial cases). *)
7.735 -
7.736 -fun num_conv n =
7.737 - nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
7.738 - |> Thm.symmetric;
7.739 -
7.740 -
7.741 -val polynomial_pow_conv =
7.742 - let
7.743 - fun ppow tm =
7.744 - let val (l,n) = dest_pow tm
7.745 - in
7.746 - if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35
7.747 - else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36
7.748 - else
7.749 - let val th1 = num_conv n
7.750 - val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
7.751 - val (tm1,tm2) = Thm.dest_comb(concl th2)
7.752 - val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
7.753 - val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
7.754 - in transitive th4 (polynomial_mul_conv (concl th4))
7.755 - end
7.756 - end
7.757 - in fn tm =>
7.758 - if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm
7.759 - end;
7.760 -
7.761 -(* Negation. *)
7.762 -
7.763 -fun polynomial_neg_conv tm =
7.764 - let val (l,r) = Thm.dest_comb tm in
7.765 - if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
7.766 - let val th1 = inst_thm [(cx',r)] neg_mul
7.767 - val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
7.768 - in transitive th2 (polynomial_monomial_mul_conv (concl th2))
7.769 - end
7.770 - end;
7.771 -
7.772 -
7.773 -(* Subtraction. *)
7.774 -fun polynomial_sub_conv tm =
7.775 - let val (l,r) = dest_sub tm
7.776 - val th1 = inst_thm [(cx',l),(cy',r)] sub_add
7.777 - val (tm1,tm2) = Thm.dest_comb(concl th1)
7.778 - val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
7.779 - in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
7.780 - end;
7.781 -
7.782 -(* Conversion from HOL term. *)
7.783 -
7.784 -fun polynomial_conv tm =
7.785 - if is_semiring_constant tm then semiring_add_conv tm
7.786 - else if not(is_comb tm) then reflexive tm
7.787 - else
7.788 - let val (lopr,r) = Thm.dest_comb tm
7.789 - in if lopr aconvc neg_tm then
7.790 - let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
7.791 - in transitive th1 (polynomial_neg_conv (concl th1))
7.792 - end
7.793 - else if lopr aconvc inverse_tm then
7.794 - let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
7.795 - in transitive th1 (semiring_mul_conv (concl th1))
7.796 - end
7.797 - else
7.798 - if not(is_comb lopr) then reflexive tm
7.799 - else
7.800 - let val (opr,l) = Thm.dest_comb lopr
7.801 - in if opr aconvc pow_tm andalso is_numeral r
7.802 - then
7.803 - let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
7.804 - in transitive th1 (polynomial_pow_conv (concl th1))
7.805 - end
7.806 - else if opr aconvc divide_tm
7.807 - then
7.808 - let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l))
7.809 - (polynomial_conv r)
7.810 - val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
7.811 - (Thm.rhs_of th1)
7.812 - in transitive th1 th2
7.813 - end
7.814 - else
7.815 - if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
7.816 - then
7.817 - let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
7.818 - val f = if opr aconvc add_tm then polynomial_add_conv
7.819 - else if opr aconvc mul_tm then polynomial_mul_conv
7.820 - else polynomial_sub_conv
7.821 - in transitive th1 (f (concl th1))
7.822 - end
7.823 - else reflexive tm
7.824 - end
7.825 - end;
7.826 - in
7.827 - {main = polynomial_conv,
7.828 - add = polynomial_add_conv,
7.829 - mul = polynomial_mul_conv,
7.830 - pow = polynomial_pow_conv,
7.831 - neg = polynomial_neg_conv,
7.832 - sub = polynomial_sub_conv}
7.833 - end
7.834 -end;
7.835 -
7.836 -val nat_exp_ss =
7.837 - HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
7.838 - addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}];
7.839 -
7.840 -fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
7.841 -
7.842 -
7.843 -(* various normalizing conversions *)
7.844 -
7.845 -fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal},
7.846 - {conv, dest_const, mk_const, is_const}) ord =
7.847 - let
7.848 - val pow_conv =
7.849 - Conv.arg_conv (Simplifier.rewrite nat_exp_ss)
7.850 - then_conv Simplifier.rewrite
7.851 - (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
7.852 - then_conv conv ctxt
7.853 - val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
7.854 - in semiring_normalizers_conv vars semiring ring field dat ord end;
7.855 -
7.856 -fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
7.857 - #main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord);
7.858 -
7.859 -fun semiring_normalize_wrapper ctxt data =
7.860 - semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
7.861 -
7.862 -fun semiring_normalize_ord_conv ctxt ord tm =
7.863 - (case match ctxt tm of
7.864 - NONE => reflexive tm
7.865 - | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
7.866 -
7.867 -fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
7.868 -
7.869 -
7.870 -(** Isar setup **)
7.871 -
7.872 -local
7.873 -
7.874 -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
7.875 -fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
7.876 -fun keyword3 k1 k2 k3 =
7.877 - Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
7.878 -
7.879 -val opsN = "ops";
7.880 -val rulesN = "rules";
7.881 -
7.882 -val normN = "norm";
7.883 -val constN = "const";
7.884 -val delN = "del";
7.885 -
7.886 -val any_keyword =
7.887 - keyword2 semiringN opsN || keyword2 semiringN rulesN ||
7.888 - keyword2 ringN opsN || keyword2 ringN rulesN ||
7.889 - keyword2 fieldN opsN || keyword2 fieldN rulesN ||
7.890 - keyword2 idomN rulesN || keyword2 idealN rulesN;
7.891 -
7.892 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
7.893 -val terms = thms >> map Drule.dest_term;
7.894 -
7.895 -fun optional scan = Scan.optional scan [];
7.896 -
7.897 -in
7.898 -
7.899 -val setup =
7.900 - Attrib.setup @{binding normalizer}
7.901 - (Scan.lift (Args.$$$ delN >> K del) ||
7.902 - ((keyword2 semiringN opsN |-- terms) --
7.903 - (keyword2 semiringN rulesN |-- thms)) --
7.904 - (optional (keyword2 ringN opsN |-- terms) --
7.905 - optional (keyword2 ringN rulesN |-- thms)) --
7.906 - (optional (keyword2 fieldN opsN |-- terms) --
7.907 - optional (keyword2 fieldN rulesN |-- thms)) --
7.908 - optional (keyword2 idomN rulesN |-- thms) --
7.909 - optional (keyword2 idealN rulesN |-- thms)
7.910 - >> (fn ((((sr, r), f), id), idl) =>
7.911 - add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
7.912 - "semiring normalizer data";
7.913 -
7.914 -end;
7.915 -
7.916 -end;
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/Tools/semiring_normalizer.ML Fri May 07 16:12:26 2010 +0200
8.3 @@ -0,0 +1,909 @@
8.4 +(* Title: HOL/Tools/Groebner_Basis/normalizer.ML
8.5 + Author: Amine Chaieb, TU Muenchen
8.6 +
8.7 +Normalization of expressions in semirings.
8.8 +*)
8.9 +
8.10 +signature SEMIRING_NORMALIZER =
8.11 +sig
8.12 + type entry
8.13 + val get: Proof.context -> (thm * entry) list
8.14 + val match: Proof.context -> cterm -> entry option
8.15 + val del: attribute
8.16 + val add: {semiring: cterm list * thm list, ring: cterm list * thm list,
8.17 + field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute
8.18 + val funs: thm -> {is_const: morphism -> cterm -> bool,
8.19 + dest_const: morphism -> cterm -> Rat.rat,
8.20 + mk_const: morphism -> ctyp -> Rat.rat -> cterm,
8.21 + conv: morphism -> Proof.context -> cterm -> thm} -> declaration
8.22 + val semiring_funs: thm -> declaration
8.23 + val field_funs: thm -> declaration
8.24 +
8.25 + val semiring_normalize_conv: Proof.context -> conv
8.26 + val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
8.27 + val semiring_normalize_wrapper: Proof.context -> entry -> conv
8.28 + val semiring_normalize_ord_wrapper: Proof.context -> entry
8.29 + -> (cterm -> cterm -> bool) -> conv
8.30 + val semiring_normalizers_conv: cterm list -> cterm list * thm list
8.31 + -> cterm list * thm list -> cterm list * thm list ->
8.32 + (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
8.33 + {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
8.34 + val semiring_normalizers_ord_wrapper: Proof.context -> entry ->
8.35 + (cterm -> cterm -> bool) ->
8.36 + {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv}
8.37 +
8.38 + val setup: theory -> theory
8.39 +end
8.40 +
8.41 +structure Semiring_Normalizer: SEMIRING_NORMALIZER =
8.42 +struct
8.43 +
8.44 +(** data **)
8.45 +
8.46 +type entry =
8.47 + {vars: cterm list,
8.48 + semiring: cterm list * thm list,
8.49 + ring: cterm list * thm list,
8.50 + field: cterm list * thm list,
8.51 + idom: thm list,
8.52 + ideal: thm list} *
8.53 + {is_const: cterm -> bool,
8.54 + dest_const: cterm -> Rat.rat,
8.55 + mk_const: ctyp -> Rat.rat -> cterm,
8.56 + conv: Proof.context -> cterm -> thm};
8.57 +
8.58 +structure Data = Generic_Data
8.59 +(
8.60 + type T = (thm * entry) list;
8.61 + val empty = [];
8.62 + val extend = I;
8.63 + val merge = AList.merge Thm.eq_thm (K true);
8.64 +);
8.65 +
8.66 +val get = Data.get o Context.Proof;
8.67 +
8.68 +fun match ctxt tm =
8.69 + let
8.70 + fun match_inst
8.71 + ({vars, semiring = (sr_ops, sr_rules),
8.72 + ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal},
8.73 + fns as {is_const, dest_const, mk_const, conv}) pat =
8.74 + let
8.75 + fun h instT =
8.76 + let
8.77 + val substT = Thm.instantiate (instT, []);
8.78 + val substT_cterm = Drule.cterm_rule substT;
8.79 +
8.80 + val vars' = map substT_cterm vars;
8.81 + val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
8.82 + val ring' = (map substT_cterm r_ops, map substT r_rules);
8.83 + val field' = (map substT_cterm f_ops, map substT f_rules);
8.84 + val idom' = map substT idom;
8.85 + val ideal' = map substT ideal;
8.86 +
8.87 + val result = ({vars = vars', semiring = semiring',
8.88 + ring = ring', field = field', idom = idom', ideal = ideal'}, fns);
8.89 + in SOME result end
8.90 + in (case try Thm.match (pat, tm) of
8.91 + NONE => NONE
8.92 + | SOME (instT, _) => h instT)
8.93 + end;
8.94 +
8.95 + fun match_struct (_,
8.96 + entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
8.97 + get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
8.98 + in get_first match_struct (get ctxt) end;
8.99 +
8.100 +
8.101 +(* logical content *)
8.102 +
8.103 +val semiringN = "semiring";
8.104 +val ringN = "ring";
8.105 +val idomN = "idom";
8.106 +val idealN = "ideal";
8.107 +val fieldN = "field";
8.108 +
8.109 +fun undefined _ = raise Match;
8.110 +
8.111 +val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm);
8.112 +
8.113 +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
8.114 + field = (f_ops, f_rules), idom, ideal} =
8.115 + Thm.declaration_attribute (fn key => fn context => context |> Data.map
8.116 + let
8.117 + val ctxt = Context.proof_of context;
8.118 +
8.119 + fun check kind name xs n =
8.120 + null xs orelse length xs = n orelse
8.121 + error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
8.122 + val check_ops = check "operations";
8.123 + val check_rules = check "rules";
8.124 +
8.125 + val _ =
8.126 + check_ops semiringN sr_ops 5 andalso
8.127 + check_rules semiringN sr_rules 37 andalso
8.128 + check_ops ringN r_ops 2 andalso
8.129 + check_rules ringN r_rules 2 andalso
8.130 + check_ops fieldN f_ops 2 andalso
8.131 + check_rules fieldN f_rules 2 andalso
8.132 + check_rules idomN idom 2;
8.133 +
8.134 + val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
8.135 + val sr_rules' = map mk_meta sr_rules;
8.136 + val r_rules' = map mk_meta r_rules;
8.137 + val f_rules' = map mk_meta f_rules;
8.138 +
8.139 + fun rule i = nth sr_rules' (i - 1);
8.140 +
8.141 + val (cx, cy) = Thm.dest_binop (hd sr_ops);
8.142 + val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
8.143 + val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
8.144 + val ((clx, crx), (cly, cry)) =
8.145 + rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
8.146 + val ((ca, cb), (cc, cd)) =
8.147 + rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
8.148 + val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
8.149 + val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
8.150 +
8.151 + val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
8.152 + val semiring = (sr_ops, sr_rules');
8.153 + val ring = (r_ops, r_rules');
8.154 + val field = (f_ops, f_rules');
8.155 + val ideal' = map (symmetric o mk_meta) ideal
8.156 + in
8.157 + AList.delete Thm.eq_thm key #>
8.158 + cons (key, ({vars = vars, semiring = semiring,
8.159 + ring = ring, field = field, idom = idom, ideal = ideal'},
8.160 + {is_const = undefined, dest_const = undefined, mk_const = undefined,
8.161 + conv = undefined}))
8.162 + end);
8.163 +
8.164 +
8.165 +(* extra-logical functions *)
8.166 +
8.167 +fun funs raw_key {is_const, dest_const, mk_const, conv} phi =
8.168 + Data.map (fn data =>
8.169 + let
8.170 + val key = Morphism.thm phi raw_key;
8.171 + val _ = AList.defined Thm.eq_thm data key orelse
8.172 + raise THM ("No data entry for structure key", 0, [key]);
8.173 + val fns = {is_const = is_const phi, dest_const = dest_const phi,
8.174 + mk_const = mk_const phi, conv = conv phi};
8.175 + in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
8.176 +
8.177 +fun semiring_funs key = funs key
8.178 + {is_const = fn phi => can HOLogic.dest_number o Thm.term_of,
8.179 + dest_const = fn phi => fn ct =>
8.180 + Rat.rat_of_int (snd
8.181 + (HOLogic.dest_number (Thm.term_of ct)
8.182 + handle TERM _ => error "ring_dest_const")),
8.183 + mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT
8.184 + (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"),
8.185 + conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm})
8.186 + then_conv Simplifier.rewrite (HOL_basic_ss addsimps
8.187 + (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))};
8.188 +
8.189 +fun field_funs key =
8.190 + let
8.191 + fun numeral_is_const ct =
8.192 + case term_of ct of
8.193 + Const (@{const_name Rings.divide},_) $ a $ b =>
8.194 + can HOLogic.dest_number a andalso can HOLogic.dest_number b
8.195 + | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
8.196 + | t => can HOLogic.dest_number t
8.197 + fun dest_const ct = ((case term_of ct of
8.198 + Const (@{const_name Rings.divide},_) $ a $ b=>
8.199 + Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
8.200 + | Const (@{const_name Rings.inverse},_)$t =>
8.201 + Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
8.202 + | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
8.203 + handle TERM _ => error "ring_dest_const")
8.204 + fun mk_const phi cT x =
8.205 + let val (a, b) = Rat.quotient_of_rat x
8.206 + in if b = 1 then Numeral.mk_cnumber cT a
8.207 + else Thm.capply
8.208 + (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
8.209 + (Numeral.mk_cnumber cT a))
8.210 + (Numeral.mk_cnumber cT b)
8.211 + end
8.212 + in funs key
8.213 + {is_const = K numeral_is_const,
8.214 + dest_const = K dest_const,
8.215 + mk_const = mk_const,
8.216 + conv = K (K Numeral_Simprocs.field_comp_conv)}
8.217 + end;
8.218 +
8.219 +
8.220 +
8.221 +(** auxiliary **)
8.222 +
8.223 +fun is_comb ct =
8.224 + (case Thm.term_of ct of
8.225 + _ $ _ => true
8.226 + | _ => false);
8.227 +
8.228 +val concl = Thm.cprop_of #> Thm.dest_arg;
8.229 +
8.230 +fun is_binop ct ct' =
8.231 + (case Thm.term_of ct' of
8.232 + c $ _ $ _ => term_of ct aconv c
8.233 + | _ => false);
8.234 +
8.235 +fun dest_binop ct ct' =
8.236 + if is_binop ct ct' then Thm.dest_binop ct'
8.237 + else raise CTERM ("dest_binop: bad binop", [ct, ct'])
8.238 +
8.239 +fun inst_thm inst = Thm.instantiate ([], inst);
8.240 +
8.241 +val dest_numeral = term_of #> HOLogic.dest_number #> snd;
8.242 +val is_numeral = can dest_numeral;
8.243 +
8.244 +val numeral01_conv = Simplifier.rewrite
8.245 + (HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]);
8.246 +val zero1_numeral_conv =
8.247 + Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]);
8.248 +fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv;
8.249 +val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
8.250 + @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"},
8.251 + @{thm "less_nat_number_of"}];
8.252 +
8.253 +val nat_add_conv =
8.254 + zerone_conv
8.255 + (Simplifier.rewrite
8.256 + (HOL_basic_ss
8.257 + addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
8.258 + @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
8.259 + @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
8.260 + @ map (fn th => th RS sym) @{thms numerals}));
8.261 +
8.262 +val zeron_tm = @{cterm "0::nat"};
8.263 +val onen_tm = @{cterm "1::nat"};
8.264 +val true_tm = @{cterm "True"};
8.265 +
8.266 +
8.267 +(** normalizing conversions **)
8.268 +
8.269 +(* core conversion *)
8.270 +
8.271 +fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules)
8.272 + (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) =
8.273 +let
8.274 +
8.275 +val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08,
8.276 + pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16,
8.277 + pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24,
8.278 + pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32,
8.279 + pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules;
8.280 +
8.281 +val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars;
8.282 +val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
8.283 +val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat];
8.284 +
8.285 +val dest_add = dest_binop add_tm
8.286 +val dest_mul = dest_binop mul_tm
8.287 +fun dest_pow tm =
8.288 + let val (l,r) = dest_binop pow_tm tm
8.289 + in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm])
8.290 + end;
8.291 +val is_add = is_binop add_tm
8.292 +val is_mul = is_binop mul_tm
8.293 +fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm);
8.294 +
8.295 +val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') =
8.296 + (case (r_ops, r_rules) of
8.297 + ([sub_pat, neg_pat], [neg_mul, sub_add]) =>
8.298 + let
8.299 + val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
8.300 + val neg_tm = Thm.dest_fun neg_pat
8.301 + val dest_sub = dest_binop sub_tm
8.302 + val is_sub = is_binop sub_tm
8.303 + in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul |> concl |> Thm.dest_arg,
8.304 + sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
8.305 + end
8.306 + | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm));
8.307 +
8.308 +val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) =
8.309 + (case (f_ops, f_rules) of
8.310 + ([divide_pat, inverse_pat], [div_inv, inv_div]) =>
8.311 + let val div_tm = funpow 2 Thm.dest_fun divide_pat
8.312 + val inv_tm = Thm.dest_fun inverse_pat
8.313 + in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm)
8.314 + end
8.315 + | _ => (TrueI, TrueI, true_tm, true_tm, K false));
8.316 +
8.317 +in fn variable_order =>
8.318 + let
8.319 +
8.320 +(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible. *)
8.321 +(* Also deals with "const * const", but both terms must involve powers of *)
8.322 +(* the same variable, or both be constants, or behaviour may be incorrect. *)
8.323 +
8.324 + fun powvar_mul_conv tm =
8.325 + let
8.326 + val (l,r) = dest_mul tm
8.327 + in if is_semiring_constant l andalso is_semiring_constant r
8.328 + then semiring_mul_conv tm
8.329 + else
8.330 + ((let
8.331 + val (lx,ln) = dest_pow l
8.332 + in
8.333 + ((let val (rx,rn) = dest_pow r
8.334 + val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
8.335 + val (tm1,tm2) = Thm.dest_comb(concl th1) in
8.336 + transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
8.337 + handle CTERM _ =>
8.338 + (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
8.339 + val (tm1,tm2) = Thm.dest_comb(concl th1) in
8.340 + transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
8.341 + handle CTERM _ =>
8.342 + ((let val (rx,rn) = dest_pow r
8.343 + val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
8.344 + val (tm1,tm2) = Thm.dest_comb(concl th1) in
8.345 + transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
8.346 + handle CTERM _ => inst_thm [(cx,l)] pthm_32
8.347 +
8.348 +))
8.349 + end;
8.350 +
8.351 +(* Remove "1 * m" from a monomial, and just leave m. *)
8.352 +
8.353 + fun monomial_deone th =
8.354 + (let val (l,r) = dest_mul(concl th) in
8.355 + if l aconvc one_tm
8.356 + then transitive th (inst_thm [(ca,r)] pthm_13) else th end)
8.357 + handle CTERM _ => th;
8.358 +
8.359 +(* Conversion for "(monomial)^n", where n is a numeral. *)
8.360 +
8.361 + val monomial_pow_conv =
8.362 + let
8.363 + fun monomial_pow tm bod ntm =
8.364 + if not(is_comb bod)
8.365 + then reflexive tm
8.366 + else
8.367 + if is_semiring_constant bod
8.368 + then semiring_pow_conv tm
8.369 + else
8.370 + let
8.371 + val (lopr,r) = Thm.dest_comb bod
8.372 + in if not(is_comb lopr)
8.373 + then reflexive tm
8.374 + else
8.375 + let
8.376 + val (opr,l) = Thm.dest_comb lopr
8.377 + in
8.378 + if opr aconvc pow_tm andalso is_numeral r
8.379 + then
8.380 + let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
8.381 + val (l,r) = Thm.dest_comb(concl th1)
8.382 + in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
8.383 + end
8.384 + else
8.385 + if opr aconvc mul_tm
8.386 + then
8.387 + let
8.388 + val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33
8.389 + val (xy,z) = Thm.dest_comb(concl th1)
8.390 + val (x,y) = Thm.dest_comb xy
8.391 + val thl = monomial_pow y l ntm
8.392 + val thr = monomial_pow z r ntm
8.393 + in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
8.394 + end
8.395 + else reflexive tm
8.396 + end
8.397 + end
8.398 + in fn tm =>
8.399 + let
8.400 + val (lopr,r) = Thm.dest_comb tm
8.401 + val (opr,l) = Thm.dest_comb lopr
8.402 + in if not (opr aconvc pow_tm) orelse not(is_numeral r)
8.403 + then raise CTERM ("monomial_pow_conv", [tm])
8.404 + else if r aconvc zeron_tm
8.405 + then inst_thm [(cx,l)] pthm_35
8.406 + else if r aconvc onen_tm
8.407 + then inst_thm [(cx,l)] pthm_36
8.408 + else monomial_deone(monomial_pow tm l r)
8.409 + end
8.410 + end;
8.411 +
8.412 +(* Multiplication of canonical monomials. *)
8.413 + val monomial_mul_conv =
8.414 + let
8.415 + fun powvar tm =
8.416 + if is_semiring_constant tm then one_tm
8.417 + else
8.418 + ((let val (lopr,r) = Thm.dest_comb tm
8.419 + val (opr,l) = Thm.dest_comb lopr
8.420 + in if opr aconvc pow_tm andalso is_numeral r then l
8.421 + else raise CTERM ("monomial_mul_conv",[tm]) end)
8.422 + handle CTERM _ => tm) (* FIXME !? *)
8.423 + fun vorder x y =
8.424 + if x aconvc y then 0
8.425 + else
8.426 + if x aconvc one_tm then ~1
8.427 + else if y aconvc one_tm then 1
8.428 + else if variable_order x y then ~1 else 1
8.429 + fun monomial_mul tm l r =
8.430 + ((let val (lx,ly) = dest_mul l val vl = powvar lx
8.431 + in
8.432 + ((let
8.433 + val (rx,ry) = dest_mul r
8.434 + val vr = powvar rx
8.435 + val ord = vorder vl vr
8.436 + in
8.437 + if ord = 0
8.438 + then
8.439 + let
8.440 + val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15
8.441 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.442 + val (tm3,tm4) = Thm.dest_comb tm1
8.443 + val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
8.444 + val th3 = transitive th1 th2
8.445 + val (tm5,tm6) = Thm.dest_comb(concl th3)
8.446 + val (tm7,tm8) = Thm.dest_comb tm6
8.447 + val th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
8.448 + in transitive th3 (Drule.arg_cong_rule tm5 th4)
8.449 + end
8.450 + else
8.451 + let val th0 = if ord < 0 then pthm_16 else pthm_17
8.452 + val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
8.453 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.454 + val (tm3,tm4) = Thm.dest_comb tm2
8.455 + in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
8.456 + end
8.457 + end)
8.458 + handle CTERM _ =>
8.459 + (let val vr = powvar r val ord = vorder vl vr
8.460 + in
8.461 + if ord = 0 then
8.462 + let
8.463 + val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18
8.464 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.465 + val (tm3,tm4) = Thm.dest_comb tm1
8.466 + val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
8.467 + in transitive th1 th2
8.468 + end
8.469 + else
8.470 + if ord < 0 then
8.471 + let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
8.472 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.473 + val (tm3,tm4) = Thm.dest_comb tm2
8.474 + in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
8.475 + end
8.476 + else inst_thm [(ca,l),(cb,r)] pthm_09
8.477 + end)) end)
8.478 + handle CTERM _ =>
8.479 + (let val vl = powvar l in
8.480 + ((let
8.481 + val (rx,ry) = dest_mul r
8.482 + val vr = powvar rx
8.483 + val ord = vorder vl vr
8.484 + in if ord = 0 then
8.485 + let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
8.486 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.487 + val (tm3,tm4) = Thm.dest_comb tm1
8.488 + in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
8.489 + end
8.490 + else if ord > 0 then
8.491 + let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
8.492 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.493 + val (tm3,tm4) = Thm.dest_comb tm2
8.494 + in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
8.495 + end
8.496 + else reflexive tm
8.497 + end)
8.498 + handle CTERM _ =>
8.499 + (let val vr = powvar r
8.500 + val ord = vorder vl vr
8.501 + in if ord = 0 then powvar_mul_conv tm
8.502 + else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
8.503 + else reflexive tm
8.504 + end)) end))
8.505 + in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
8.506 + end
8.507 + end;
8.508 +(* Multiplication by monomial of a polynomial. *)
8.509 +
8.510 + val polynomial_monomial_mul_conv =
8.511 + let
8.512 + fun pmm_conv tm =
8.513 + let val (l,r) = dest_mul tm
8.514 + in
8.515 + ((let val (y,z) = dest_add r
8.516 + val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
8.517 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.518 + val (tm3,tm4) = Thm.dest_comb tm1
8.519 + val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
8.520 + in transitive th1 th2
8.521 + end)
8.522 + handle CTERM _ => monomial_mul_conv tm)
8.523 + end
8.524 + in pmm_conv
8.525 + end;
8.526 +
8.527 +(* Addition of two monomials identical except for constant multiples. *)
8.528 +
8.529 +fun monomial_add_conv tm =
8.530 + let val (l,r) = dest_add tm
8.531 + in if is_semiring_constant l andalso is_semiring_constant r
8.532 + then semiring_add_conv tm
8.533 + else
8.534 + let val th1 =
8.535 + if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l)
8.536 + then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then
8.537 + inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02
8.538 + else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03
8.539 + else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r)
8.540 + then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04
8.541 + else inst_thm [(cm,r)] pthm_05
8.542 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.543 + val (tm3,tm4) = Thm.dest_comb tm1
8.544 + val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
8.545 + val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
8.546 + val tm5 = concl th3
8.547 + in
8.548 + if (Thm.dest_arg1 tm5) aconvc zero_tm
8.549 + then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
8.550 + else monomial_deone th3
8.551 + end
8.552 + end;
8.553 +
8.554 +(* Ordering on monomials. *)
8.555 +
8.556 +fun striplist dest =
8.557 + let fun strip x acc =
8.558 + ((let val (l,r) = dest x in
8.559 + strip l (strip r acc) end)
8.560 + handle CTERM _ => x::acc) (* FIXME !? *)
8.561 + in fn x => strip x []
8.562 + end;
8.563 +
8.564 +
8.565 +fun powervars tm =
8.566 + let val ptms = striplist dest_mul tm
8.567 + in if is_semiring_constant (hd ptms) then tl ptms else ptms
8.568 + end;
8.569 +val num_0 = 0;
8.570 +val num_1 = 1;
8.571 +fun dest_varpow tm =
8.572 + ((let val (x,n) = dest_pow tm in (x,dest_numeral n) end)
8.573 + handle CTERM _ =>
8.574 + (tm,(if is_semiring_constant tm then num_0 else num_1)));
8.575 +
8.576 +val morder =
8.577 + let fun lexorder l1 l2 =
8.578 + case (l1,l2) of
8.579 + ([],[]) => 0
8.580 + | (vps,[]) => ~1
8.581 + | ([],vps) => 1
8.582 + | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
8.583 + if variable_order x1 x2 then 1
8.584 + else if variable_order x2 x1 then ~1
8.585 + else if n1 < n2 then ~1
8.586 + else if n2 < n1 then 1
8.587 + else lexorder vs1 vs2
8.588 + in fn tm1 => fn tm2 =>
8.589 + let val vdegs1 = map dest_varpow (powervars tm1)
8.590 + val vdegs2 = map dest_varpow (powervars tm2)
8.591 + val deg1 = fold (Integer.add o snd) vdegs1 num_0
8.592 + val deg2 = fold (Integer.add o snd) vdegs2 num_0
8.593 + in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
8.594 + else lexorder vdegs1 vdegs2
8.595 + end
8.596 + end;
8.597 +
8.598 +(* Addition of two polynomials. *)
8.599 +
8.600 +val polynomial_add_conv =
8.601 + let
8.602 + fun dezero_rule th =
8.603 + let
8.604 + val tm = concl th
8.605 + in
8.606 + if not(is_add tm) then th else
8.607 + let val (lopr,r) = Thm.dest_comb tm
8.608 + val l = Thm.dest_arg lopr
8.609 + in
8.610 + if l aconvc zero_tm
8.611 + then transitive th (inst_thm [(ca,r)] pthm_07) else
8.612 + if r aconvc zero_tm
8.613 + then transitive th (inst_thm [(ca,l)] pthm_08) else th
8.614 + end
8.615 + end
8.616 + fun padd tm =
8.617 + let
8.618 + val (l,r) = dest_add tm
8.619 + in
8.620 + if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07
8.621 + else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08
8.622 + else
8.623 + if is_add l
8.624 + then
8.625 + let val (a,b) = dest_add l
8.626 + in
8.627 + if is_add r then
8.628 + let val (c,d) = dest_add r
8.629 + val ord = morder a c
8.630 + in
8.631 + if ord = 0 then
8.632 + let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23
8.633 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.634 + val (tm3,tm4) = Thm.dest_comb tm1
8.635 + val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
8.636 + in dezero_rule (transitive th1 (combination th2 (padd tm2)))
8.637 + end
8.638 + else (* ord <> 0*)
8.639 + let val th1 =
8.640 + if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
8.641 + else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
8.642 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.643 + in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
8.644 + end
8.645 + end
8.646 + else (* not (is_add r)*)
8.647 + let val ord = morder a r
8.648 + in
8.649 + if ord = 0 then
8.650 + let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26
8.651 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.652 + val (tm3,tm4) = Thm.dest_comb tm1
8.653 + val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
8.654 + in dezero_rule (transitive th1 th2)
8.655 + end
8.656 + else (* ord <> 0*)
8.657 + if ord > 0 then
8.658 + let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
8.659 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.660 + in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
8.661 + end
8.662 + else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
8.663 + end
8.664 + end
8.665 + else (* not (is_add l)*)
8.666 + if is_add r then
8.667 + let val (c,d) = dest_add r
8.668 + val ord = morder l c
8.669 + in
8.670 + if ord = 0 then
8.671 + let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28
8.672 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.673 + val (tm3,tm4) = Thm.dest_comb tm1
8.674 + val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
8.675 + in dezero_rule (transitive th1 th2)
8.676 + end
8.677 + else
8.678 + if ord > 0 then reflexive tm
8.679 + else
8.680 + let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
8.681 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.682 + in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
8.683 + end
8.684 + end
8.685 + else
8.686 + let val ord = morder l r
8.687 + in
8.688 + if ord = 0 then monomial_add_conv tm
8.689 + else if ord > 0 then dezero_rule(reflexive tm)
8.690 + else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
8.691 + end
8.692 + end
8.693 + in padd
8.694 + end;
8.695 +
8.696 +(* Multiplication of two polynomials. *)
8.697 +
8.698 +val polynomial_mul_conv =
8.699 + let
8.700 + fun pmul tm =
8.701 + let val (l,r) = dest_mul tm
8.702 + in
8.703 + if not(is_add l) then polynomial_monomial_mul_conv tm
8.704 + else
8.705 + if not(is_add r) then
8.706 + let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
8.707 + in transitive th1 (polynomial_monomial_mul_conv(concl th1))
8.708 + end
8.709 + else
8.710 + let val (a,b) = dest_add l
8.711 + val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10
8.712 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.713 + val (tm3,tm4) = Thm.dest_comb tm1
8.714 + val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
8.715 + val th3 = transitive th1 (combination th2 (pmul tm2))
8.716 + in transitive th3 (polynomial_add_conv (concl th3))
8.717 + end
8.718 + end
8.719 + in fn tm =>
8.720 + let val (l,r) = dest_mul tm
8.721 + in
8.722 + if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11
8.723 + else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12
8.724 + else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13
8.725 + else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14
8.726 + else pmul tm
8.727 + end
8.728 + end;
8.729 +
8.730 +(* Power of polynomial (optimized for the monomial and trivial cases). *)
8.731 +
8.732 +fun num_conv n =
8.733 + nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
8.734 + |> Thm.symmetric;
8.735 +
8.736 +
8.737 +val polynomial_pow_conv =
8.738 + let
8.739 + fun ppow tm =
8.740 + let val (l,n) = dest_pow tm
8.741 + in
8.742 + if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35
8.743 + else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36
8.744 + else
8.745 + let val th1 = num_conv n
8.746 + val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
8.747 + val (tm1,tm2) = Thm.dest_comb(concl th2)
8.748 + val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
8.749 + val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
8.750 + in transitive th4 (polynomial_mul_conv (concl th4))
8.751 + end
8.752 + end
8.753 + in fn tm =>
8.754 + if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm
8.755 + end;
8.756 +
8.757 +(* Negation. *)
8.758 +
8.759 +fun polynomial_neg_conv tm =
8.760 + let val (l,r) = Thm.dest_comb tm in
8.761 + if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
8.762 + let val th1 = inst_thm [(cx',r)] neg_mul
8.763 + val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
8.764 + in transitive th2 (polynomial_monomial_mul_conv (concl th2))
8.765 + end
8.766 + end;
8.767 +
8.768 +
8.769 +(* Subtraction. *)
8.770 +fun polynomial_sub_conv tm =
8.771 + let val (l,r) = dest_sub tm
8.772 + val th1 = inst_thm [(cx',l),(cy',r)] sub_add
8.773 + val (tm1,tm2) = Thm.dest_comb(concl th1)
8.774 + val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
8.775 + in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
8.776 + end;
8.777 +
8.778 +(* Conversion from HOL term. *)
8.779 +
8.780 +fun polynomial_conv tm =
8.781 + if is_semiring_constant tm then semiring_add_conv tm
8.782 + else if not(is_comb tm) then reflexive tm
8.783 + else
8.784 + let val (lopr,r) = Thm.dest_comb tm
8.785 + in if lopr aconvc neg_tm then
8.786 + let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
8.787 + in transitive th1 (polynomial_neg_conv (concl th1))
8.788 + end
8.789 + else if lopr aconvc inverse_tm then
8.790 + let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
8.791 + in transitive th1 (semiring_mul_conv (concl th1))
8.792 + end
8.793 + else
8.794 + if not(is_comb lopr) then reflexive tm
8.795 + else
8.796 + let val (opr,l) = Thm.dest_comb lopr
8.797 + in if opr aconvc pow_tm andalso is_numeral r
8.798 + then
8.799 + let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
8.800 + in transitive th1 (polynomial_pow_conv (concl th1))
8.801 + end
8.802 + else if opr aconvc divide_tm
8.803 + then
8.804 + let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l))
8.805 + (polynomial_conv r)
8.806 + val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
8.807 + (Thm.rhs_of th1)
8.808 + in transitive th1 th2
8.809 + end
8.810 + else
8.811 + if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
8.812 + then
8.813 + let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
8.814 + val f = if opr aconvc add_tm then polynomial_add_conv
8.815 + else if opr aconvc mul_tm then polynomial_mul_conv
8.816 + else polynomial_sub_conv
8.817 + in transitive th1 (f (concl th1))
8.818 + end
8.819 + else reflexive tm
8.820 + end
8.821 + end;
8.822 + in
8.823 + {main = polynomial_conv,
8.824 + add = polynomial_add_conv,
8.825 + mul = polynomial_mul_conv,
8.826 + pow = polynomial_pow_conv,
8.827 + neg = polynomial_neg_conv,
8.828 + sub = polynomial_sub_conv}
8.829 + end
8.830 +end;
8.831 +
8.832 +val nat_exp_ss =
8.833 + HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
8.834 + addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}];
8.835 +
8.836 +fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
8.837 +
8.838 +
8.839 +(* various normalizing conversions *)
8.840 +
8.841 +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal},
8.842 + {conv, dest_const, mk_const, is_const}) ord =
8.843 + let
8.844 + val pow_conv =
8.845 + Conv.arg_conv (Simplifier.rewrite nat_exp_ss)
8.846 + then_conv Simplifier.rewrite
8.847 + (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
8.848 + then_conv conv ctxt
8.849 + val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
8.850 + in semiring_normalizers_conv vars semiring ring field dat ord end;
8.851 +
8.852 +fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
8.853 + #main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord);
8.854 +
8.855 +fun semiring_normalize_wrapper ctxt data =
8.856 + semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
8.857 +
8.858 +fun semiring_normalize_ord_conv ctxt ord tm =
8.859 + (case match ctxt tm of
8.860 + NONE => reflexive tm
8.861 + | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
8.862 +
8.863 +fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
8.864 +
8.865 +
8.866 +(** Isar setup **)
8.867 +
8.868 +local
8.869 +
8.870 +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
8.871 +fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
8.872 +fun keyword3 k1 k2 k3 =
8.873 + Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
8.874 +
8.875 +val opsN = "ops";
8.876 +val rulesN = "rules";
8.877 +
8.878 +val normN = "norm";
8.879 +val constN = "const";
8.880 +val delN = "del";
8.881 +
8.882 +val any_keyword =
8.883 + keyword2 semiringN opsN || keyword2 semiringN rulesN ||
8.884 + keyword2 ringN opsN || keyword2 ringN rulesN ||
8.885 + keyword2 fieldN opsN || keyword2 fieldN rulesN ||
8.886 + keyword2 idomN rulesN || keyword2 idealN rulesN;
8.887 +
8.888 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
8.889 +val terms = thms >> map Drule.dest_term;
8.890 +
8.891 +fun optional scan = Scan.optional scan [];
8.892 +
8.893 +in
8.894 +
8.895 +val setup =
8.896 + Attrib.setup @{binding normalizer}
8.897 + (Scan.lift (Args.$$$ delN >> K del) ||
8.898 + ((keyword2 semiringN opsN |-- terms) --
8.899 + (keyword2 semiringN rulesN |-- thms)) --
8.900 + (optional (keyword2 ringN opsN |-- terms) --
8.901 + optional (keyword2 ringN rulesN |-- thms)) --
8.902 + (optional (keyword2 fieldN opsN |-- terms) --
8.903 + optional (keyword2 fieldN rulesN |-- thms)) --
8.904 + optional (keyword2 idomN rulesN |-- thms) --
8.905 + optional (keyword2 idealN rulesN |-- thms)
8.906 + >> (fn ((((sr, r), f), id), idl) =>
8.907 + add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
8.908 + "semiring normalizer data";
8.909 +
8.910 +end;
8.911 +
8.912 +end;
9.1 --- a/src/HOL/ex/Groebner_Examples.thy Fri May 07 16:12:25 2010 +0200
9.2 +++ b/src/HOL/ex/Groebner_Examples.thy Fri May 07 16:12:26 2010 +0200
9.3 @@ -14,21 +14,21 @@
9.4 fixes x :: int
9.5 shows "x ^ 3 = x ^ 3"
9.6 apply (tactic {* ALLGOALS (CONVERSION
9.7 - (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
9.8 + (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
9.9 by (rule refl)
9.10
9.11 lemma
9.12 fixes x :: int
9.13 shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<twosuperior> + (80 * x + 32))))"
9.14 apply (tactic {* ALLGOALS (CONVERSION
9.15 - (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
9.16 + (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
9.17 by (rule refl)
9.18
9.19 schematic_lemma
9.20 fixes x :: int
9.21 shows "(x - (-2))^5 * (y - 78) ^ 8 = ?X"
9.22 apply (tactic {* ALLGOALS (CONVERSION
9.23 - (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
9.24 + (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
9.25 by (rule refl)
9.26
9.27 lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"