# HG changeset patch # User wenzelm # Date 1441896257 -7200 # Node ID 3d5e01b427cb829d1bc1cf553ae37a47922ed5af # Parent 13b2fd8016928cded2396432124843a39fb3235e more standard local_theory operations; eliminated slightly odd @{cpat}; diff -r 13b2fd801692 -r 3d5e01b427cb src/HOL/Semiring_Normalization.thy --- a/src/HOL/Semiring_Normalization.thy Thu Sep 10 16:42:01 2015 +0200 +++ b/src/HOL/Semiring_Normalization.thy Thu Sep 10 16:44:17 2015 +0200 @@ -72,101 +72,120 @@ context comm_semiring_1 begin -declaration \ -let - val rules = @{lemma - "(a * m) + (b * m) = (a + b) * m" - "(a * m) + m = (a + 1) * m" - "m + (a * m) = (a + 1) * m" - "m + m = (1 + 1) * m" - "0 + a = a" - "a + 0 = a" - "a * b = b * a" - "(a + b) * c = (a * c) + (b * c)" - "0 * a = 0" - "a * 0 = 0" - "1 * a = a" - "a * 1 = a" - "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)" - "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))" - "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)" - "(lx * ly) * rx = (lx * rx) * ly" - "(lx * ly) * rx = lx * (ly * rx)" - "lx * (rx * ry) = (lx * rx) * ry" - "lx * (rx * ry) = rx * (lx * ry)" - "(a + b) + (c + d) = (a + c) + (b + d)" - "(a + b) + c = a + (b + c)" - "a + (c + d) = c + (a + d)" - "(a + b) + c = (a + c) + b" - "a + c = c + a" - "a + (c + d) = (a + c) + d" - "(x ^ p) * (x ^ q) = x ^ (p + q)" - "x * (x ^ q) = x ^ (Suc q)" - "(x ^ q) * x = x ^ (Suc q)" - "x * x = x\<^sup>2" - "(x * y) ^ q = (x ^ q) * (y ^ q)" - "(x ^ p) ^ q = x ^ (p * q)" - "x ^ 0 = 1" - "x ^ 1 = x" - "x * (y + z) = (x * y) + (x * z)" - "x ^ (Suc q) = x * (x ^ q)" - "x ^ (2*n) = (x ^ n) * (x ^ n)" - by (simp_all add: algebra_simps power_add power2_eq_square - power_mult_distrib power_mult del: one_add_one)} -in +lemma semiring_normalization_rules: + "(a * m) + (b * m) = (a + b) * m" + "(a * m) + m = (a + 1) * m" + "m + (a * m) = (a + 1) * m" + "m + m = (1 + 1) * m" + "0 + a = a" + "a + 0 = a" + "a * b = b * a" + "(a + b) * c = (a * c) + (b * c)" + "0 * a = 0" + "a * 0 = 0" + "1 * a = a" + "a * 1 = a" + "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)" + "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))" + "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)" + "(lx * ly) * rx = (lx * rx) * ly" + "(lx * ly) * rx = lx * (ly * rx)" + "lx * (rx * ry) = (lx * rx) * ry" + "lx * (rx * ry) = rx * (lx * ry)" + "(a + b) + (c + d) = (a + c) + (b + d)" + "(a + b) + c = a + (b + c)" + "a + (c + d) = c + (a + d)" + "(a + b) + c = (a + c) + b" + "a + c = c + a" + "a + (c + d) = (a + c) + d" + "(x ^ p) * (x ^ q) = x ^ (p + q)" + "x * (x ^ q) = x ^ (Suc q)" + "(x ^ q) * x = x ^ (Suc q)" + "x * x = x\<^sup>2" + "(x * y) ^ q = (x ^ q) * (y ^ q)" + "(x ^ p) ^ q = x ^ (p * q)" + "x ^ 0 = 1" + "x ^ 1 = x" + "x * (y + z) = (x * y) + (x * z)" + "x ^ (Suc q) = x * (x ^ q)" + "x ^ (2*n) = (x ^ n) * (x ^ n)" + by (simp_all add: algebra_simps power_add power2_eq_square + power_mult_distrib power_mult del: one_add_one) + +local_setup \ Semiring_Normalizer.declare @{thm comm_semiring_1_axioms} - {semiring = ([@{cpat "?x + ?y"}, @{cpat "?x * ?y"}, @{cpat "?x ^ ?n"}, @{cpat 0}, @{cpat 1}], - rules), ring = ([], []), field = ([], []), idom = [], ideal = []} -end\ + {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], + @{thms semiring_normalization_rules}), + ring = ([], []), + field = ([], []), + idom = [], + ideal = []} +\ end context comm_ring_1 begin -declaration \ -let - val rules = @{lemma - "- x = (- 1) * x" - "x - y = x + (- y)" - by simp_all} -in +lemma ring_normalization_rules: + "- x = (- 1) * x" + "x - y = x + (- y)" + by simp_all + +local_setup \ Semiring_Normalizer.declare @{thm comm_ring_1_axioms} - {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms}, - ring = ([@{cpat "?x - ?y"}, @{cpat "- ?x"}], rules), field = ([], []), idom = [], ideal = []} -end\ + {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], + @{thms semiring_normalization_rules}), + ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}), + field = ([], []), + idom = [], + ideal = []} +\ end context comm_semiring_1_cancel_crossproduct begin -declaration \Semiring_Normalizer.declare @{thm comm_semiring_1_cancel_crossproduct_axioms} - {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms}, - ring = ([], []), field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq}, ideal = []}\ +local_setup \ + Semiring_Normalizer.declare @{thm comm_semiring_1_cancel_crossproduct_axioms} + {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], + @{thms semiring_normalization_rules}), + ring = ([], []), + field = ([], []), + idom = @{thms crossproduct_noteq add_scale_eq_noteq}, + ideal = []} +\ end context idom begin -declaration \Semiring_Normalizer.declare @{thm idom_axioms} - {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_ring_1_axioms}, - ring = Semiring_Normalizer.the_ring @{context} @{thm comm_ring_1_axioms}, - field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq}, - ideal = @{thms right_minus_eq add_0_iff}}\ +local_setup \ + Semiring_Normalizer.declare @{thm idom_axioms} + {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], + @{thms semiring_normalization_rules}), + ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}), + field = ([], []), + idom = @{thms crossproduct_noteq add_scale_eq_noteq}, + ideal = @{thms right_minus_eq add_0_iff}} +\ end context field begin -declaration \Semiring_Normalizer.declare @{thm field_axioms} - {semiring = Semiring_Normalizer.the_semiring @{context} @{thm idom_axioms}, - ring = Semiring_Normalizer.the_ring @{context} @{thm idom_axioms}, - field = ([@{cpat "?x / ?y"}, @{cpat "inverse ?x"}], @{thms divide_inverse inverse_eq_divide}), - idom = Semiring_Normalizer.the_idom @{context} @{thm idom_axioms}, - ideal = Semiring_Normalizer.the_ideal @{context} @{thm idom_axioms}}\ +local_setup \ + Semiring_Normalizer.declare @{thm field_axioms} + {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], + @{thms semiring_normalization_rules}), + ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}), + field = ([@{term "x / y"}, @{term "inverse x"}], @{thms divide_inverse inverse_eq_divide}), + idom = @{thms crossproduct_noteq add_scale_eq_noteq}, + ideal = @{thms right_minus_eq add_0_iff}} +\ end diff -r 13b2fd801692 -r 3d5e01b427cb src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Thu Sep 10 16:42:01 2015 +0200 +++ b/src/HOL/Tools/semiring_normalizer.ML Thu Sep 10 16:44:17 2015 +0200 @@ -4,7 +4,7 @@ Normalization of expressions in semirings. *) -signature SEMIRING_NORMALIZER = +signature SEMIRING_NORMALIZER = sig type entry val match: Proof.context -> cterm -> entry option @@ -13,8 +13,9 @@ val the_field: Proof.context -> thm -> cterm list * thm list val the_idom: Proof.context -> thm -> thm list val the_ideal: Proof.context -> thm -> thm list - val declare: thm -> {semiring: cterm list * thm list, ring: cterm list * thm list, - field: cterm list * thm list, idom: thm list, ideal: thm list} -> declaration + val declare: thm -> {semiring: term list * thm list, ring: term list * thm list, + field: term list * thm list, idom: thm list, ideal: thm list} -> + local_theory -> local_theory val semiring_normalize_conv: Proof.context -> conv val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv @@ -40,7 +41,7 @@ sub: Proof.context -> conv} end -structure Semiring_Normalizer: SEMIRING_NORMALIZER = +structure Semiring_Normalizer: SEMIRING_NORMALIZER = struct (** data **) @@ -76,7 +77,7 @@ fun match ctxt tm = let fun match_inst - ({vars, semiring = (sr_ops, sr_rules), + ({vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal}, fns) pat = let @@ -92,7 +93,7 @@ val idom' = map substT idom; val ideal' = map substT ideal; - val result = ({vars = vars', semiring = semiring', + val result = ({vars = vars', semiring = semiring', ring = ring', field = field', idom = idom', ideal = ideal'}, fns); in SOME result end in (case try Thm.match (pat, tm) of @@ -105,7 +106,7 @@ get_first (match_inst entry) (sr_ops @ r_ops @ f_ops); in get_first match_struct (Data.get (Context.Proof ctxt)) end; - + (* extra-logical functions *) val semiring_norm_ss = @@ -137,9 +138,9 @@ fun dest_const ct = ((case Thm.term_of ct of Const (@{const_name Rings.divide},_) $ a $ b=> Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) - | Const (@{const_name Fields.inverse},_)$t => + | 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))) + | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) handle TERM _ => error "ring_dest_const") fun mk_const cT x = let val (a, b) = Rat.quotient_of_rat x @@ -165,62 +166,71 @@ val idomN = "idom"; fun declare raw_key - {semiring = raw_semiring, ring = raw_ring, field = raw_field, idom = raw_idom, ideal = raw_ideal} - phi context = + {semiring = raw_semiring0, ring = raw_ring0, field = raw_field0, idom = raw_idom, ideal = raw_ideal} + lthy = let - val ctxt = Context.proof_of context; - val key = Morphism.thm phi raw_key; - fun morphism_ops_rules (ops, rules) = (map (Morphism.cterm phi) ops, Morphism.fact phi rules); - val (sr_ops, sr_rules) = morphism_ops_rules raw_semiring; - val (r_ops, r_rules) = morphism_ops_rules raw_ring; - val (f_ops, f_rules) = morphism_ops_rules raw_field; - val idom = Morphism.fact phi raw_idom; - val ideal = Morphism.fact phi raw_ideal; - - fun check kind name xs n = - null xs orelse length xs = n orelse - error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); - val check_ops = check "operations"; - val check_rules = check "rules"; - val _ = - check_ops semiringN sr_ops 5 andalso - check_rules semiringN sr_rules 36 andalso - check_ops ringN r_ops 2 andalso - check_rules ringN r_rules 2 andalso - check_ops fieldN f_ops 2 andalso - check_rules fieldN f_rules 2 andalso - check_rules idomN idom 2; + val ctxt' = fold Variable.auto_fixes (fst raw_semiring0 @ fst raw_ring0 @ fst raw_field0) lthy; + val prepare_ops = apfst (Variable.export_terms ctxt' lthy #> map (Thm.cterm_of lthy)); + val raw_semiring = prepare_ops raw_semiring0; + val raw_ring = prepare_ops raw_ring0; + val raw_field = prepare_ops raw_field0; + in + lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context => + let + val ctxt = Context.proof_of context; + val key = Morphism.thm phi raw_key; + fun transform_ops_rules (ops, rules) = + (map (Morphism.cterm phi) ops, Morphism.fact phi rules); + val (sr_ops, sr_rules) = transform_ops_rules raw_semiring; + val (r_ops, r_rules) = transform_ops_rules raw_ring; + val (f_ops, f_rules) = transform_ops_rules raw_field; + val idom = Morphism.fact phi raw_idom; + val ideal = Morphism.fact phi raw_ideal; - val mk_meta = Local_Defs.meta_rewrite_rule ctxt; - val sr_rules' = map mk_meta sr_rules; - val r_rules' = map mk_meta r_rules; - val f_rules' = map mk_meta f_rules; + fun check kind name xs n = + null xs orelse length xs = n orelse + error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); + val check_ops = check "operations"; + val check_rules = check "rules"; + val _ = + check_ops semiringN sr_ops 5 andalso + check_rules semiringN sr_rules 36 andalso + check_ops ringN r_ops 2 andalso + check_rules ringN r_rules 2 andalso + check_ops fieldN f_ops 2 andalso + check_rules fieldN f_rules 2 andalso + check_rules idomN idom 2; + + val mk_meta = Local_Defs.meta_rewrite_rule ctxt; + val sr_rules' = map mk_meta sr_rules; + val r_rules' = map mk_meta r_rules; + val f_rules' = map mk_meta f_rules; + + fun rule i = nth sr_rules' (i - 1); - fun rule i = nth sr_rules' (i - 1); - - val (cx, cy) = Thm.dest_binop (hd sr_ops); - val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; - val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; - val ((clx, crx), (cly, cry)) = - rule 13 |> Thm.rhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop; - val ((ca, cb), (cc, cd)) = - rule 20 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop; - val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; - val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_arg; + val (cx, cy) = Thm.dest_binop (hd sr_ops); + val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; + val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; + val ((clx, crx), (cly, cry)) = + rule 13 |> Thm.rhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop; + val ((ca, cb), (cc, cd)) = + rule 20 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop; + val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; + val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_arg; + + val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; - val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; - - val semiring = (sr_ops, sr_rules'); - val ring = (r_ops, r_rules'); - val field = (f_ops, f_rules'); - val ideal' = map (Thm.symmetric o mk_meta) ideal - - in - context - |> Data.map (AList.update Thm.eq_thm (key, - ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal'}, - (if null f_ops then semiring_funs else field_funs)))) - end + val semiring = (sr_ops, sr_rules'); + val ring = (r_ops, r_rules'); + val field = (f_ops, f_rules'); + val ideal' = map (Thm.symmetric o mk_meta) ideal + in + context + |> Data.map (AList.update Thm.eq_thm (key, + ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal'}, + (if null f_ops then semiring_funs else field_funs)))) + end) + end; (** auxiliary **) @@ -255,7 +265,7 @@ fun zerone_conv ctxt cv = zero1_numeral_conv ctxt then_conv cv then_conv numeral01_conv ctxt; -val nat_add_ss = simpset_of +val nat_add_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms arith_simps} @ @{thms diff_nat_numeral} @ @{thms rel_simps} @ @{thms if_False if_True Nat.add_0 add_Suc add_numeral_left Suc_eq_plus1} @@ -308,9 +318,9 @@ end | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), true_tm, true_tm)); -val (divide_inverse, divide_tm, inverse_tm) = - (case (f_ops, f_rules) of - ([divide_pat, inverse_pat], [div_inv, _]) => +val (divide_inverse, divide_tm, inverse_tm) = + (case (f_ops, f_rules) of + ([divide_pat, inverse_pat], [div_inv, _]) => let val div_tm = funpow 2 Thm.dest_fun divide_pat val inv_tm = Thm.dest_fun inverse_pat in (div_inv, div_tm, inv_tm) @@ -420,7 +430,7 @@ else ((let val (lopr,r) = Thm.dest_comb tm val (opr,l) = Thm.dest_comb lopr - in if opr aconvc pow_tm andalso is_number r then l + in if opr aconvc pow_tm andalso is_number r then l else raise CTERM ("monomial_mul_conv",[tm]) end) handle CTERM _ => tm) (* FIXME !? *) fun vorder x y = @@ -803,9 +813,9 @@ let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv ctxt l)) r in Thm.transitive th1 (polynomial_pow_conv ctxt (concl th1)) end - else if opr aconvc divide_tm + else if opr aconvc divide_tm then - let val th1 = Thm.combination (Drule.arg_cong_rule opr (polynomial_conv ctxt l)) + let val th1 = Thm.combination (Drule.arg_cong_rule opr (polynomial_conv ctxt l)) (polynomial_conv ctxt r) val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv ctxt) (Thm.rhs_of th1) @@ -846,7 +856,7 @@ (* various normalizing conversions *) -fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, +fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = let val pow_conv = @@ -862,14 +872,14 @@ ({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) ctxt; -fun semiring_normalize_wrapper ctxt data = +fun semiring_normalize_wrapper ctxt data = semiring_normalize_ord_wrapper ctxt data simple_cterm_ord; fun semiring_normalize_ord_conv ctxt ord tm = (case match ctxt tm of NONE => Thm.reflexive tm | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm); - + fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; end;